Re: [isabelle] THE elimination?



On Wednesday 07 May 2008 10:41, Peter Lammich wrote:
> David Streader wrote:

> > When stuck  at sorry I am faced with
> > using this:
> >  (THE re. (nam, re) : Ops adt) = rel
> >
> > goal (1 subgoal):
> > 1. (nam, rel) : Ops adt

> note that you cannot derive your statement just from the fact that (THE
> re. (nam, re) \<in> Ops adt) = rel, I think that is related to the fact
> that Isabelle has no notion of partial functions or undefined expressions.

Indeed.  Think about the case where  "(nam, re) : Ops adt"  is false for *any* 
choice of "re".  "THE re. (nam, re) : Ops adt"  will be defined regardless, 
but you won't be able to prove much about it.  In particular,
  "(nam, (THE re. (nam, re) : Ops adt)) : Ops adt"
will of course not hold.

Tjark





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