# Re: [isabelle] THE elimination?

David Streader wrote:

Hi

` I need to use definite descriptions and can introduce THE using
``the_equality. But I have found no way to eliminate THE
`
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

In order to show anything about THE, you need a lemma like:
lemma UNIQUE: "\<exists>!r. (n,r)\<in>Ops x" sorry
i.e. stating that there is exactly one element associated with each name.
then, you can use theI', e.g. :
from as show "(nam, rel) \<in> Ops adt" using UNIQUE[THEN theI'] by fast

`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.
`
regards,
Peter

My intuitions tell me that this should be obvious but nothing works.
What Have I missed?
david

`lemma "\<forall> nam rel. ((OpsF nam) =rel) = ((nam, rel)\<in>
``(adtt.Ops adt))"
``proof (rule allI)+ fix nam rel show "(OpsF nam = rel) = ((nam, rel)
``\<in> Ops adt)"
` unfolding OpsF_def
proof
assume as: "(THE re. (nam, re) \<in> Ops adt) = rel" from as
show "(nam, rel) \<in> Ops adt" sorry
next

` assume sa: "(nam, rel) \<in> Ops adt" from sa ropsfun [where a=nam
``and relx=rel]
`` have "\<And> rely. (nam, rely) \<in> Ops adt \<Longrightarrow> rely
``= rel" by simp
`` with sa show "(THE rel. (nam, rel) \<in> Ops adt) = rel" apply
``(rule the_equality [where a=rel and P="\<lambda> rel.(nam, rel)
``\<in> Ops adt "])
` by auto
qed
qed

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