Re: [isabelle] Isar macro definitions and polymorphism



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
> 








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.