Email Gateway (Aug 18 2022 at 11:49): Email Gateway (Aug 18 2022 at 11:49):From: Peter Lammich <peter.lammich@uni-muenster.de>
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 THEWhen stuck at sorry I am faced with
using this:
(THE re. (nam, re) : Ops adt) = relgoal (1 subgoal):
1. (nam, rel) : Ops adtIn 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" sorrynext
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
Email Gateway (Aug 18 2022 at 11:49):From: Tjark Weber <tjark.weber@gmx.de>
Indeed. Think about the case where "(nam, re) : Ops adt" is false for any
choice of "re". "THE re. (nam, re) : Ops adt" will be defined regardless,
but you won't be able to prove much about it. In particular,
"(nam, (THE re. (nam, re) : Ops adt)) : Ops adt"
will of course not hold.
Tjark
Last updated: May 03 2024 at 04:19 UTC