[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.

Abstractly,
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"
apply(
  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]
    â
  â
)
oops

end


Thanks for any help,
Andreas

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 MHonArc.