Re: [isabelle] Hilbert's EPS operator question



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.
On Nov 12, 2011 9:33 PM, <filip at matf.bg.ac.rs> wrote:

> 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.