Email Gateway (Aug 18 2022 at 18:43): 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
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.
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: Nov 21 2024 at 12:39 UTC