*To*: Andrei Popescu <uuomul at yahoo.com>*Subject*: Re: [isabelle] Isar macro definitions and polymorphism*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Fri, 13 Nov 2009 07:28:55 -0800*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <845107.40548.qm@web56101.mail.re3.yahoo.com>*References*: <mailman.23.1257998406.24135.cl-isabelle-users@lists.cam.ac.uk> <845107.40548.qm@web56101.mail.re3.yahoo.com>*Sender*: huffman.brian.c at gmail.com

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

**Follow-Ups**:**Re: [isabelle] Isar macro definitions and polymorphism***From:*Andrei Popescu

**References**:**[isabelle] Isar macro definitions and polymorphism***From:*Andrei Popescu

- Previous by Date: Re: [isabelle] Does anyone know how to get rid of => marker in PG4.0?
- Next by Date: Re: [isabelle] Does anyone know how to get rid of => marker in PG4.0?
- Previous by Thread: [isabelle] Isar macro definitions and polymorphism
- Next by Thread: Re: [isabelle] Isar macro definitions and polymorphism
- 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