Email Gateway (Aug 19 2022 at 17:33): Email Gateway (Aug 19 2022 at 17:33):From: Wenda Li <wl302@cam.ac.uk>
Dear Isabelle experts,
As I have used the keyword "undefined" in my proofs, I am quite curious
about its properties. The following lemma is easily proved:
lemma "(undefined::rat) ∈ ℚ ∨ (undefined::rat) ∉ ℚ" by auto
but I cannot prove either of the following two lemmas:
lemma "(undefined::rat) ∈ ℚ" oops
lemma "(undefined::rat) ∉ ℚ" oops
Is it true that both of the last two propositions are unprovable within
Isabelle? If it is, I think it is a fun fact about the
non-constructivity in Isabelle.
Any comment is appreciated,
Wenda
Email Gateway (Aug 19 2022 at 17:33):From: Peter Lammich <lammich@in.tum.de>
This is true. Undefined is just some constant of type 'a
(instantiated to rat in your case), but there is no definition of it.
So you can prove only things about undefined that you can prove for all
elements of its type.
Your above example is an instance of the tautology "P | ~P", which is an
axiom of HOL, and completely independent of undefined or rat.
In general, for some type of type variable T, you can prove "P
(undefined::T)", iff you can prove
"ALL x::T. P x". But note that this statement itself (i.e.
"P (undefined::'a) <--> ALL x. P x")
is not a theorem in HOL.
Email Gateway (Aug 19 2022 at 17:34):From: Christian Sternagel <c.sternagel@gmail.com>
Well, actually, in your special case this is provable.
lemma "(undefined::rat) ∈ ℚ"
by (simp add: Rats_def)
The point being that by the type constraint "undefined::rat" you also
constrain "Rats" (i.e., ℚ) to type "rat set", for which we have "Rats =
(UNIV::rat set)".
So as Peter mentioned, since this property holds for any rat, it also
holds for "undefined".
cheers
chris
Last updated: Apr 25 2024 at 20:15 UTC