[isabelle] Struggling with type unification



Dear Isabelle Users,

In the following simple script, the Isar proof only works if I fix the types
of
both subtrees,  like I did. If I let their types unspecified (like in: fix
x0 and lt0 and rt0) it
gives a type unification error. From the proof state, one can see that it
happens
because the two induction hypothesis are assigned different type variables.

Could anyone elaborate a bit more on that for me?

Many Thanks!
---------------------------------------------------------------------------------------------------------------
theory newbies_tree_demo

imports Main

begin
 datatype 'a Tree = Leaf | Br  'a "'a Tree" "'a Tree"

 primrec reflect::"'a Tree => 'a Tree"
   where
     ref01:"reflect Leaf = Leaf" |
     rev02:"reflect (Br label lt rt) = Br label (reflect rt) (reflect lt)"

theorem th_refl01isA: "reflect (reflect t) = t"
  proof (induct t)
     show  "reflect (reflect Leaf) = Leaf" by simp
  next
     fix x0 and lt0::"'a Tree" and rt0::"'a Tree"
     assume IH1: "reflect (reflect lt0) = lt0"
     assume IH2: "reflect (reflect rt0) = rt0"
     show "reflect (reflect (Br x0 lt0 rt0)) = Br x0 lt0 rt0" by (simp
add:IH1 IH2)
  qed


-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Porto Alegre - RS - Brasil




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