Email Gateway (Aug 18 2022 at 17:14): Email Gateway (Aug 18 2022 at 17:14):From: Søren Haagerup <shaagerup@gmail.com>
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
Email Gateway (Aug 18 2022 at 17:14):From: Lawrence Paulson <lp15@cam.ac.uk>
It is ?b2.2 in the new subgoal, but ?b2.0 in the original theorem.
Generally, avoid explicit instantiations if you can.
Larry Paulson
Email Gateway (Aug 18 2022 at 17:14):From: Brian Huffman <brianh@cs.pdx.edu>
Hi Søren,
In Isabelle, a schematic variable is represented in ML as an
indexname, which is a pair of a string and and integer. The parsing
rules have some weird special cases for variable names that end with
digits. (See section 3.1 of isar-ref.)
x, ?x, x0, ?x0, and ?x.0 parse as ("x", 0)
x2, ?x2 and ?x.2 parse as ("x", 2)
?x2.0 parses as ("x2", 0)
In your case, you want to refer to the variable ("b2", 0). But the
name b2 inconveniently refers to ("b", 2), so you will have to use the
admittedly awkward name ?b2.0 instead.
Honestly, I think the above parsing rules are quite confusing, and
should be changed. I instantiate variables in theorems quite often,
and many theorems use variable names that end in digits, but I almost
never need to refer to variables with indices other than 0. Maybe at
one time, it was more common to refer to indexnames like ("b", 2) than
ones like ("b2", 0), but this seems outdated now.
I would propose to simplify the parsing rules to work like this: Any
variable name with index 0 can be referred to without a question mark
or dot, and a dot is always required for indices other than 0.
x, ?x and ?x.0 parse as ("x", 0)
x0, ?x0 and ?x0.0 parse as ("x0", 0)
x2, ?x2 and ?x2.0 parse as ("x2", 0)
?x.2 parses as ("x", 2)
Last updated: Apr 18 2024 at 16:19 UTC