Re: [isabelle] THE elimination?

David Streader wrote:
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.


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


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
   assume as: "(THE re. (nam, re) \<in> Ops adt) = rel"  from as
   show "(nam, rel) \<in> Ops adt"    sorry

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

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