[isabelle] Problem with frule_tac substitution
Dear Isabelle users
I started playing around with Isabelle last week, and have stumbled
upon a problem with applying "frule_tac" with a specific lemma.
I have got the following lemma:
lemma promotion_theorem: "!! b1 b2 h f c . [|assoc b1; assoc b2;
promotable h b1 b2; cata c f b1|] ==> cata (h o c) (h o f) b2"
which I want to apply in a different lemma by:
apply(frule_tac h="h" and f="f" and c="catafunc f b1" and b2="b2" in
Isabelle says "No such variable in theorem: ?b2".
apply(frule_tac h="h" and f="f" and c="catafunc f b1" in promotion_theorem)
instead, I see that b2 shows up as ?b2.2.
I now tried
apply(frule_tac h="h" and f="f" and c="catafunc f b1" and ?b2.2="b2"
but still no luck.
According to http://isabelle.in.tum.de/dist/Isabelle2011/doc/isar-ref.pdf
p. 134 it is correct to precede variables with a question mark, if
they contain dots.
My document can be downloaded here:
and is completely self-contained. The error shows up when applying the
This archive was generated by a fusion of
Pipermail (Mailman edition) and