# [isabelle] Isar macro definitions and polymorphism

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"
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. *)
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? *)
let ?d = "(g::'b => nat)((f::nat => 'b) n)"
term ?d (* This did not work either *)
(* 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
>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

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