[isabelle] Hilbert's EPS operator question



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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.