Flexible/Fuzzy 规则在 Isabelle/HOL 中的应用

Question

假设我有以下谓词 P 和规则 R:

locale example =
  fixes P :: "int ⇒ int ⇒ bool"
  assumes R: "⋀a b c. a ≥ 2 ⟹ P (a*b) (a*c)"

我现在想将规则应用到R来证明P 8 4，但是当然直接应用规则失败了：

lemma (in example) "P 8 4"
proof (rule R)  (* FAILS *)

相反，我必须在使用规则之前手动实例化等式：

lemma (in example) "P 8 4"
proof -
  have "P (4*2) (4*1)"
    by (rule R, simp)
  thus "P 8 4" 
    by simp
qed

lemma (in example) "P 8 4"
  using R[where a=2 and b=4 and c=2] by simp

下面的例子比较好。它只需要一个专门用于带有 2 个参数的谓词的引理，并且需要手动指定顶级谓词名称：

lemma back_subst2: "⟦P x' y'; x' = x; y' = y⟧ ⟹ P x y" 
  by force

lemma (in example) "P 8 4"
proof (rule back_subst2[where P=P], rule R)
  show "2 ≤ (2 :: int)" by simp
  show "2*4 = (8::int)" by simp
  show "2*2 = (4::int)" by simp
qed

我的问题：当参数没有完全要求的形式时，是否有更好的方法来应用规则？最后一个例子可以改进吗？

Answer 1

我现在已经编写了自己的名为 fuzzy_rule 的方法来执行此操作：

lemma (in example) "P 8 4"
proof (fuzzy_rule R)
  show "2 ≤ (2 :: int)" by simp
  show "2*4 = (8::int)" by simp
  show "2*2 = (4::int)" by simp
qed

来源可在 https://github.com/peterzeller/isabelle_fuzzy_rule

Flexible/Fuzzy 规则在 Isabelle/HOL 中的应用

Flexible/Fuzzy rule application in Isabelle/HOL

isabelle