*To*: filip at matf.bg.ac.rs*Subject*: Re: [isabelle] Hilbert's EPS operator question*From*: Ramana Kumar <rk436 at cam.ac.uk>*Date*: Sat, 12 Nov 2011 21:44:56 +0000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <50b7e7e92bc50a7e53f77a17c1cdea1b.squirrel@webmail.matf.bg.ac.rs>*References*: <50b7e7e92bc50a7e53f77a17c1cdea1b.squirrel@webmail.matf.bg.ac.rs>*Sender*: ramana.kumar at gmail.com

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

**Follow-Ups**:**Re: [isabelle] Hilbert's EPS operator question***From:*Peter Lammich

**References**:**[isabelle] Hilbert's EPS operator question***From:*filip

- Previous by Date: [isabelle] Hilbert's EPS operator question
- Next by Date: Re: [isabelle] Hilbert's EPS operator question
- Previous by Thread: [isabelle] Hilbert's EPS operator question
- Next by Thread: Re: [isabelle] Hilbert's EPS operator question
- Cl-isabelle-users November 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list