Re: [isabelle] Problem with frule_tac substitution



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)

- Brian


On Mon, Feb 7, 2011 at 6:48 AM, Søren Haagerup <shaagerup at gmail.com> wrote:
> 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.