Re: [isabelle] Struggling with type unification



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




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