[isabelle] Hilbert's EPS operator question
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
assumes "EX P. incident P l1 & incident P l2"
shows "incident (mk_intersection l1 l2) l1" and
"incident (mk_intersection l1 l2) l2"
The problem arises in a degenerate case of parallel lines and I would like
to have something like:
"[| ~(EX P. incident P l1 & incident P l2); mk_intersection l1 l2 = P |]
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and