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