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
(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>
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" sorry
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