[isabelle] THE elimination?
I need to use definite descriptions and can introduce THE using
But I have found no way to eliminate THE
When stuck at sorry I am faced with
(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?
lemma "\<forall> nam rel. ((OpsF nam) =rel) = ((nam, rel)\<in>
proof (rule allI)+ fix nam rel show "(OpsF nam = rel) = ((nam, rel)
\<in> Ops adt)"
assume as: "(THE re. (nam, re) \<in> Ops adt) = rel" from as
show "(nam, rel) \<in> Ops adt"
assume sa: "(nam, rel) \<in> Ops adt" from sa ropsfun [where a=nam
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 "])
This archive was generated by a fusion of
Pipermail (Mailman edition) and