*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] Isar macro definitions and polymorphism*From*: Andrei Popescu <uuomul at yahoo.com>*Date*: Fri, 13 Nov 2009 09:55:39 -0800 (PST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <cc2478ab0911130728v14327acbq5f5ea0b00a1fa67@mail.gmail.com>

Hello Brian, Many thanks for the detailed answer -- this does clarify everything. > I think the original source of all your confusion was with > the "term > f" and "term g" commands inside the proof script. In these > cases, > Isabelle does *not* assume that by "term f" you mean, "the > type of f > as it appears in the goal". That was precisely my source of confusion. Thinking about the way things are actually handled, I now see they make sense -- there is no reason why a polymorphic constant "f" should not be available in its full generality inside a proof that happens to fix an instance of it. Best regards, Andrei --- On Fri, 11/13/09, Brian Huffman <brianh at cs.pdx.edu> wrote: > From: Brian Huffman <brianh at cs.pdx.edu> > Subject: Re: [isabelle] Isar macro definitions and polymorphism > To: "Andrei Popescu" <uuomul at yahoo.com> > Cc: cl-isabelle-users at lists.cam.ac.uk > Date: Friday, November 13, 2009, 5:28 PM > Hi Andrei, > > If you turn on "Show Sorts" and "Show Consts", then you > should be able > to see what is going on with your example. > > On Thu, Nov 12, 2009 at 2:07 PM, Andrei Popescu <uuomul at yahoo.com> > wrote: > > Hello, > > > > I have trouble understanding the following behavior of > macros w.r.t. > > polymorphism. Consider the following situation: > > > > consts f :: "nat => 'a" > > consts g :: "'a => nat" > > > > lemma L1: fixes n::nat shows "g(f n) = undefined" > > At this point, 'a is a fixed, unspecified type. The "f" in > the goal > has type "nat => 'a" and the "g" in the goal has type > "'a => nat". If > you have "Show Sorts" turned on, then the goal display will > include a > line like "type variables: 'a :: type" telling you that 'a > is a fixed > type. > > > proof- > > term f (* has type "nat => 'b" OK *) > > term g (* has type "'b => nat" OK *) > > (* So my understanding was that, inside this proof, > 'b acts like a > > fixed unspecified type. *) > > Here, Isabelle is telling you that terms f and g are > polymorphic, > which it would usually denote with the types "nat => 'a" > and "'a => > nat", respectively. But since type variable 'a is already > used, > Isabelle uses the next available free type variable, which > is 'b. > > > term "g(f(n))" (* has type "nat" OK *) > > let ?c = "g(f n)" > > term "?c" > > (* ?c is now "%TYPE. g (f n)" and has type "'b > itself => nat" WHY? *) > > The term "g(f(n))" has type "nat", but there is also a free > variable > inside the term. The fully type-annotated term is > "(g::'b=>nat)((f::nat=>'b)(n::nat)) :: nat" (Remember > that 'b here > indicates polymorphism; it is not a fixed type in this > context.) > > The extra parameter of type 'b itself is Isabelle's way of > dealing > with this situation where term contains a free type > variable that does > not appear in the term's type. > > When defining a constant or abbreviation, all polymorphic > type > variables in the term are required to appear in the type of > the term. > For example, if you try the following definition command, > Isabelle > will give you a "Specification depends on extra type > variables" error: > > definition c :: "nat => nat" where "c n = g (f n)" > > When defining abbreviations with "let" inside a proof > script, Isabelle > has a workaround for this restriction: It adds an extra > parameter to > change the type from "nat" (which is not allowed since it > doesn't > mention 'b) to "'b itself => nat" (which is OK). > > > let ?d = "(g::'b => nat)((f::nat => 'b) n)" > > term ?d (* This did not work either *) > > This means exactly the same thing as the previous > definition of ?c. > > If you had instead typed > > let ?d = "(g::'a => nat)((f::nat => 'a) n)" > > Then the extra TYPE parameter would disappear. Since 'a is > a fixed > type variable in the proof context, it is OK to define an > abbreviation > for a term mentioning 'a whose type doesn't mention 'a. > > > (* Neither does this: *) > > have "?d _ = (g::'b => nat)((f::nat => 'b) > n)" sorry > > show ?thesis sorry > > qed > > > > But the following works as expected: > > > > lemma L2 fixes n::nat > > shows "(g::'b => nat)((f::nat => 'b) n) = > undefined" > > proof- > > term "g(f(n))" (* has type "nat" OK *) > > let ?d = "(g::'b => nat)((f::nat => 'b) n)" > > term "?d" (* has type "nat" OK *) > > show ?thesis sorry > > qed > > Yes, this one works because the type variable in term ?d > and the type > variable in the goal are the same. > > > >From outside, the two lemmas L1 and L2 are > identical. > > > > 1) Why is it that macros seemingly take into > consideration some > > extra generality? > > And what does this generality mean -- is it a form of > universal > > quantification over types? > > > > 2) What is the status difference between the type > variable > > 'b from L1 (that was provided automatically) and the > one from L2 (that > > was declared explicitly)? Before encountering the > above, I was > > assuming there is no difference. > > > > Thank you in advance for any explanations on this. > > > > Andrei > > I think the original source of all your confusion was with > the "term > f" and "term g" commands inside the proof script. In these > cases, > Isabelle does *not* assume that by "term f" you mean, "the > type of f > as it appears in the goal". > > Also, remember to use "Show Sorts" if you ever get confused > about > which type variables are fixed in a proof. > > Hope this helps, > - Brian >

**References**:**Re: [isabelle] Isar macro definitions and polymorphism***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Does anyone know how to get rid of => marker in PG4.0?
- Next by Date: [isabelle] PhD studentships: Reasoning about Relaxed Memory Models
- Previous by Thread: Re: [isabelle] Isar macro definitions and polymorphism
- Next by Thread: [isabelle] PhD studentships: Reasoning about Relaxed Memory Models
- Cl-isabelle-users November 2009 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