[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
promotion_theorem)

Isabelle says "No such variable in theorem: ?b2".
Trying with
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"
in promotion_theorem)
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:
http://www.imada.sdu.dk/~sorenh07/misc/isabelle/Draft4.thy
and is completely self-contained. The error shows up when applying the
last statement.

Any ideas?

Best regards,
Søren Haagerup





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.