*To*: Ramana Kumar <rk436 at cam.ac.uk>*Subject*: Re: [isabelle] Hilbert's EPS operator question*From*: Peter Lammich <lammich at in.tum.de>*Date*: Sun, 13 Nov 2011 00:04:32 +0100*Cc*: isabelle-users at cl.cam.ac.uk, filip at matf.bg.ac.rs*In-reply-to*: <CAMej=27cqdZWFDh6gJ5RUqrokPLi64iHA697L4HGxfLTf=H1kA@mail.gmail.com>*References*: <50b7e7e92bc50a7e53f77a17c1cdea1b.squirrel@webmail.matf.bg.ac.rs> <CAMej=27cqdZWFDh6gJ5RUqrokPLi64iHA697L4HGxfLTf=H1kA@mail.gmail.com>

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 On Sa, 2011-11-12 at 21:44 +0000, Ramana Kumar wrote: > 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 > > > > > >

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

**Re: [isabelle] Hilbert's EPS operator question***From:*Ramana Kumar

- Previous by Date: Re: [isabelle] Hilbert's EPS operator question
- Next by Date: Re: [isabelle] primrec
- Previous by Thread: Re: [isabelle] Hilbert's EPS operator question
- Next by Thread: [isabelle] "partial order" type?
- 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