Re: [isabelle] Isar macro definitions and polymorphism



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.