Email Gateway (Aug 19 2022 at 10:59): Email Gateway (Aug 19 2022 at 10:59):From: Lars Noschinski <noschinl@in.tum.de>
Roger, please not, that only the type of "?a" matters, not the value.
René used "SOME x. True" here to get an arbitrary value of the required
type. But the use of SOME is not essential here:
proof (rule someI)
show "Domain {(2,undefined), (3,undefined)} = {2,3}" by auto
qed
or (personally, I like this best)
proof (rule someI)
fix x show "Domain {(2,x), (3,x)} = {2,3}" by auto
qed
-- Lars
Email Gateway (Aug 19 2022 at 11:13):From: "Roger H." <s57076@hotmail.com>
Hello,
is this lemma true?
lemma "Domain (SOME r. Domain r = {2,3}) = {2,3}"
if yes, how can it be proved?
Thank you!
Email Gateway (Aug 19 2022 at 11:13):From: Lars Noschinski <noschinl@in.tum.de>
Hi Roger,
Email Gateway (Aug 19 2022 at 11:13):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Roger,
yes it is True, and the crucial lemma is "someI":
lemma "Domain (SOME r. Domain r = {2,3}) = {2,3}"
proof (rule someI)
let ?a = "SOME x. True"
show "Domain {(2,?a), (3,?a)} = {2,3}" by auto
qed
the "SOME x. True" is just some arbitrary element in
the range of your relation. (You did not specify the type
of the relation, hence the usage of the polymorphic SOME.
Kind regards,
René
Email Gateway (Aug 19 2022 at 11:14):From: Johannes Hölzl <hoelzl@in.tum.de>
Am Mittwoch, den 22.05.2013, 20:51 +0200 schrieb Roger H.:
Hello,
is this lemma true?
lemma "Domain (SOME r. Domain r = {2,3}) = {2,3}"
Yes this lemma is true, The SOME operator returns a fixed but arbitrary
element r which has the property "Domain r = {2,3}", if such an r
exists. You only need to provide a existence proof.
if yes, how can it be proved?
You can use find_theorems:
find_theorems "?P (SOME x. ?P x)"
This shows you a list of interesting theorems. They help you to reduce
your lemma to an existence proof.
In the existence proof you need to construct a relation with a domain of
"{2,3}" for example "{(2, 2), (3, 3)}".
Last updated: Nov 21 2024 at 12:39 UTC