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.