*To*: Alfio Martini <alfio.martini at acm.org>*Subject*: Re: [isabelle] Struggling with type unification*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Tue, 30 Aug 2011 15:17:06 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <CAAPnxw3in3N2CAd0-A-0cjD8oOJwv0MhTWTDWzGCRLDH4SnuuQ@mail.gmail.com>*References*: <CAAPnxw3in3N2CAd0-A-0cjD8oOJwv0MhTWTDWzGCRLDH4SnuuQ@mail.gmail.com>

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

**Follow-Ups**:**Re: [isabelle] Struggling with type unification***From:*Alfio Martini

**References**:**[isabelle] Struggling with type unification***From:*Alfio Martini

- Previous by Date: [isabelle] Struggling with type unification
- Next by Date: Re: [isabelle] Struggling with type unification
- Previous by Thread: [isabelle] Struggling with type unification
- Next by Thread: Re: [isabelle] Struggling with type unification
- Cl-isabelle-users August 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list