Email Gateway (Aug 19 2022 at 08:02): Email Gateway (Aug 19 2022 at 08:02):From: Mark Wassell <mpwassell@gmail.com>
Hi,
I am looking for some information on The :: ('a => bool) => 'a
I see in HOL.thy that it is listed in the axioms and there is an
abbreviation for THE that uses it. The tutorial covers THE in the section
on the definite description operator and I see a number of lemmas involving
THE. However I can find very little on The.
How can I prove theorems that involve The? For example, it would seem that
EX x. f x ==> a = The f ==> f a
should hold and that the following is true.
The f = (THE x. f x)
My usual tactic of grepping thy files and searching the PDF files is
failing me here for obvious reasons.
Mark
Email Gateway (Aug 19 2022 at 08:03):From: Lawrence Paulson <lp15@cam.ac.uk>
The following theorems (which you can find in .../src/HOL/HOL.thy) should cover all your needs.
the_equality
theI
theI2
the1I2
Your first conjecture isn't true, because The is a definite description operator: the specified entity must be unique. If you want the Hilbert indefinite description operator, along with the axiom of choice, then you need Eps.
Your second conjecture is simply a syntactic identity.
Larry Paulson
Email Gateway (Aug 19 2022 at 08:03):From: Joachim Breitner <breitner@kit.edu>
Hi Mark,
Am Dienstag, den 31.07.2012, 08:59 +0100 schrieb Mark Wassell:
I am looking for some information on The :: ('a => bool) => 'a
I see in HOL.thy that it is listed in the axioms and there is an
abbreviation for THE that uses it. The tutorial covers THE in the section
on the definite description operator and I see a number of lemmas involving
THE. However I can find very little on The.How can I prove theorems that involve The? For example, it would seem that
EX x. f x ==> a = The f ==> f a
should hold
You seem to confuse The and Eps (aka "SOME x. f x", from
Hilbert_Choice.thy) The is only defined when there is exactly one
element that satisfies the predicate. So you can either prove
lemma "∃! x. f x ==> a = The f ==> f a"
by(erule ssubst, erule the1I2)
or
lemma "∃ x. f x ==> a = Eps f ==> f a"
by(erule ssubst, erule exE, rule someI)
and that the following is true.
The f = (THE x. f x)
Yes, this is true and only looks different:
lemma "The f = (THE x. f x)"
by (rule refl)
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 08:03):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear Mark,
On 07/31/2012 04:59 PM, Mark Wassell wrote:
I am looking for some information on The :: ('a => bool) => 'a
I see in HOL.thy that it is listed in the axioms and there is an
abbreviation for THE that uses it.
Well, it's not an abbreviation but a syntax translation (sorry for
nitpicking, but those differences occasionally matter). The net outcome
is that we can write "THE x. f x" interchangeably with "The f". What I'm
trying to say is that everything you find on 'THE' (where lemma names
usually use the lowercase "the") is in fact a statement about 'The'
(i.e., informally speaking The and THE are the same). The axiomatization
in HOL is
the_eq_trivial: "(THE x. x = a) = (a::'a)"
(which could equivalently be written as "The (%x. x = a) = (a::'a)").
How can I prove theorems that involve The? For example, it would seem that
EX x. f x ==> a = The f ==> f a
This is not a valid fact as can be found out by nitpicking again (sorry
for the joke, I mean the Isabelle tool nitpick this time). Just type
lemma "Ex x. f x ==> a = The f ==> f a"
nitpick
and nitpick will show you a counter-example.
The f = (THE x. f x)
This is just reflexivity of "op =", since the left-hand side and
right-hand side are equal (just using syntactic sugar on the right).
lemma "The f = (THE x. f x)"
by (rule refl)
cheers
chris
Last updated: Apr 16 2024 at 08:18 UTC