isabelle - 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

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

标签： isabelle

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