*To*: Søren Haagerup <shaagerup at gmail.com>*Subject*: Re: [isabelle] Problem with frule_tac substitution*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Tue, 8 Feb 2011 06:53:15 -0800*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <AANLkTintffdFWbPvwpnHi1gtPs8tr2PnwTKaCDW9TsJB@mail.gmail.com>*References*: <AANLkTintffdFWbPvwpnHi1gtPs8tr2PnwTKaCDW9TsJB@mail.gmail.com>*Sender*: huffman.brian.c at gmail.com

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

**References**:**[isabelle] Problem with frule_tac substitution***From:*Søren Haagerup

- Previous by Date: Re: [isabelle] Problem with frule_tac substitution
- Next by Date: [isabelle] Isabelle research groups in United States?
- Previous by Thread: Re: [isabelle] Problem with frule_tac substitution
- Next by Thread: [isabelle] Isabelle2011 Z3 issue
- Cl-isabelle-users February 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list