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