*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] Struggling with type unification*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Tue, 30 Aug 2011 11:21:02 -0300*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <D2309571-F9C4-40E8-88B9-6BA6F60C5D01@cam.ac.uk>*References*: <CAAPnxw3in3N2CAd0-A-0cjD8oOJwv0MhTWTDWzGCRLDH4SnuuQ@mail.gmail.com> <D2309571-F9C4-40E8-88B9-6BA6F60C5D01@cam.ac.uk>*Sender*: alfio.martini at gmail.com

Dear Lawrence, Many thanks for the quick and helpful reply! Best! On Tue, Aug 30, 2011 at 11:17 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote: > 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 > > -- Alfio Ricardo Martini PhD in Computer Science (TU Berlin) Associate Professor at Faculty of Informatics (PUCRS) Porto Alegre - RS - Brasil

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

**Re: [isabelle] Struggling with type unification***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] Struggling with type unification
- Next by Date: Re: [isabelle] list_size_pointwise
- Previous by Thread: Re: [isabelle] Struggling with type unification
- Next by Thread: Re: [isabelle] Lattices and syntactic classes
- 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