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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and