Re: [isabelle] Struggling with type unification



The problem is that the function reflect is polymorphic, and when you simply state the induction hypotheses as you do, there is no reason to assume that the variables have the same types. To eliminate this difficulty, the Isar language includes abbreviations letting you refer to the various inductive cases. Then types are assigned correctly. I suggest writing your proof as follows:

theorem th_refl01isA: "reflect (reflect t) = t"
 proof (induct t)
   case Leaf
    show ?case by simp
 next
   case (Br x0 lt0 rt0)
     thus ?case by simp
 qed

Larry Paulson


On 30 Aug 2011, at 15:07, Alfio Martini wrote:

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