[isabelle] Isabelle2015-RC1: Rule instantiation in Eisbach
Dear Eisbach developers,
First of all, thanks for designing and implementing Eisbach. Unfortunately, I am
struggling with instantiating variables in rules when I write my own proof methods in Eisbach.
1. I select a rule R by matching a list L of theorems against a term, and
2. then instantiate a variable in R with a term obtained by matching the conclusion
against a pattern.
Unfortunately, I always get the error "More instantiations than variables in theorem"
although all the theorems in the list L contain at least one variable. I do not know where
this error comes from. Below is a small example:
theory Scratch imports Main "~~/src/HOL/Eisbach/Eisbach_Tools" begin
consts foo :: "'a â 'a â 'a â bool"
lemma my_thms: "foo x y z â z â y" "foo x y y â x â z" sorry
lemma "âz. A z â B"
match concl in "f x y" for f x y â â
match my_thms in R:"PROP P â f u v" for P u v â â
rule R[of x]
Thanks for any help,
PS: I am trying to build something similar to the apply_split method in the Eisbach paper
presented at ITP2014.
This archive was generated by a fusion of
Pipermail (Mailman edition) and