Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Hilbert's EPS operator question


view this post on Zulip Email Gateway (Aug 18 2022 at 18:43):

From: filip@matf.bg.ac.rs
Hello,

while formalizing some specific aspects of geometry, I came across a
question regarding Hilbert's EPS operator.

I defined an intersection of two lines using SOME operator:

definition mk_intersection where
"mk_intersection line1 line2 =
(SOME point. incident point line1 & incident point line2)"

If lines are not parallel it is easy to prove that
lemma LEMMA1:
assumes "EX P. incident P l1 & incident P l2"
shows "incident (mk_intersection l1 l2) l1" and
"incident (mk_intersection l1 l2) l2"
holds.

The problem arises in a degenerate case of parallel lines and I would like
to have something like:

lemma LEMMA2:
"[| ~(EX P. incident P l1 & incident P l2); mk_intersection l1 l2 = P |]
==> False"

However, I do not know how to prove this and I do not even know if it holds.

This question could be generalized to whether the following holds:
lemma "[| ~(EX x. P x); Q (SOME x. P x) |] ==> False"

If this does not hold (and I feel that it does not), is there any other
simple way of defining mk_intersection function such that both LEMMA1 and
LEMMA2 can be proved.

Of course, there is a possibility of using "is_intersection P l1 l2"
predicate instead of "mk_intersection l1 l2" function, but the informal
mathematics text that I am trying to formalize tends to be constructive
and heavily uses the intersection construction function (that I am trying
to formalize through "mk_intersection") and I would like to stick to this
approach (if possible).

Thank you in advance,
Filip

view this post on Zulip Email Gateway (Aug 18 2022 at 18:43):

From: Ramana Kumar <rk436@cam.ac.uk>
Hilbert choice (or the SOME binder) does not imply existence; if nothing
with the desired property exists, an arbitrary element of the type is
denoted.
So you're right that LEMMA2 does not hold.

You could define mk_intersection with a precondition asserting that the
lines aren't parallel. (Is natural number division done like that in
Isabelle/HOL?) You would have to repeat that condition in all appropriate
places, but locales could help make it look natural.

view this post on Zulip Email Gateway (Aug 18 2022 at 18:44):

From: Peter Lammich <lammich@in.tum.de>
Another standard way would be to use an option-datatype, and
let mk_intersect be None if the lines are parallel, and "Some point"
otherwise.

Peter


Last updated: Mar 28 2024 at 12:29 UTC