[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.