Assume I have the following predicate P and rule R:
locale example =
fixes P :: "int ⇒ int ⇒ bool"
assumes R: "⋀a b c. a ≥ 2 ⟹ P (a*b) (a*c)"
I now want to apply the rule to R to prove P 8 4, but of course a direct rule application fails:
lemma (in example) "P 8 4"
proof (rule R) (* FAILS *)
Instead I have to instantiate the equalities manually before using the rule:
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
The following example is a bit nicer. It only requires a specialized lemma for predicates with 2 arguments and it requires manually specifying the toplevel predicate name:
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
My question: Is there a better way to apply rules, when arguments do not have the exactly required form? Can the last example be improved somehow?
I have now written my own method named fuzzy_rule to do this:
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
Source is available at https://github.com/peterzeller/isabelle_fuzzy_rule