Isabelle:将引理调整为 `rule` 方法所需的形式

Question

我定义了一个名为step_g的归纳关系。这是推理规则之一:

G_No_Op:
  "∀j ∈ the (T i). ¬ (eval_bool p (the (γ ⇩t⇩s j)))
  ⟹ step_g a i T (γ, (Barrier, p)) (Some γ)"

我想在证明中调用此规则，因此我输入

apply (rule step_g.G_No_Op)

但是不能应用该规则，因为它的结论必须已经具有特定的形式(两个 γ 必须匹配)。所以我像这样调整规则:

lemma G_No_Op_helper:
  "⟦ ∀j ∈ the (T i). ¬ (eval_bool p (the (γ ⇩t⇩s j))) ; γ = γ' ⟧
  ⟹ step_g a i T (γ, (Barrier, p)) (Some γ')"
by (simp add: step_g.G_No_Op)

现在，当我调用规则 G_No_Op_helper 时，“两个 γ 必须匹配”的要求成为需要证明的子目标。

从G_No_Op到G_No_Op_helper的转换看起来相当机械。我的问题是:有没有办法让伊莎贝尔自动执行此操作？

---

编辑。我想出了一个“最小的工作示例”。下面，引理A等价于A2，但是规则A并不能帮助证明定理，只有规则A2 有效。

consts foo :: "nat ⇒ nat ⇒ nat ⇒ bool"

lemma A: "x < y ⟹ foo y x x"
sorry

lemma A2: "⟦ x < y ; x = z ⟧ ⟹ foo y x z"
sorry

theorem "foo y x z"
apply (rule A)

Answer 1

据我所知，没有任何东西可以使这些事情自动化。人们可能可以将其实现为一种属性，即

thm A[generalised x]

获得类似A2的东西。该属性将替换给定变量的每次出现(即此处的 x)，但定理结论中的​​第一个变量将替换为新变量 x' 并添加前提x' = x 到定理。

对于比我更擅长 Isabelle/ML 的人来说，实现这一点应该不难——也许阅读本文的一些高级 Isabelle/ML 黑客可以对这个想法发表评论。