On 29 May 2012, at 06:06, Bill Richter wrote:

> Your code
> doesn't work for me yet, but maybe that's a problem with my definition
> of the function line, which is a bad variable name, so I changed it:
> 
> let Line_DEF = new_definition
>  `!A B.  Line(A, B) = if (A = B) then {} else (@l. A IN l /\ B IN l)`;;
> 
> let InteriorAngle_DEF = new_definition
> `!A O B. int_angle(A, O, B) =
>    if Collinear(A, O, B) then {} else
>    let a = Line(O, A) in
>    let b = Line(O, B) in
>      {P | ~(P IN a) /\ ~(P IN b) /\
>      P,B same_side a /\ P,A same_side b}`;;
> 
> 
> I have your InteriorAngle_DEF, which looks great, and thanks for
> writing it.  Does my Line_DEF look OK?  

It looks to me like it probably means the right thing, but ultimately, deciding 
how to formalise something is a matter of taste and judgment. If it works in 
the context of your axioms, my inclination would have been to try a single set 
comprehension describing the points on the line:

> let Line_DEF = new_definition
>  `!A B.  Line(A, B) = {X | ~(A = B) /\ (Collinear(X, A, B) \/ Collinear(A, X, 
> B) \/ Collinear(A, B, X))}`;;

I would expect that to be easier to work with than your formulation with the 
Hilibert-choice operator (@), but it just may not be what you want to say.


> I have a thm which gets no
> error message until the last line 
> 
>    thus G IN int_angle(A, O, B) by H1, Distinct, I3, notGina, notGinb, 
> Gsim_aB,
>    Gsim_bA, InteriorAngle_DEF ;
> 
> and Freek's miz3 error message is #2 inference time-out, which means
> that miz3 couldn't prove this assertion G IN int_angle(A, O, B).
> Well, I could believe I messed up something that complicated, and I'll
> try some things. 

I'm afraid I really don't know anything more than a few headline facts about 
miz3 - I just strike lucky with your last miz3 problem and I don't know enough 
about it to help with this one.

Regards,

Rob.


------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Reply via email to