[isabelle] THE elimination?



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

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.