Re: [isabelle] Hilbert's EPS operator question



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







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