Thanks, Rob! I found an interesting looking ProofPower paper of yours
www.lemma-one.com/papers/51.pdf and I'll try to read it.
Your SameSideEquivalenceRelation_THM fix worked perfectly, and I'm
puzzled, as I thought that was the first thing I tried. Anyway, it
works now, so thanks!
(You hadn't cited your theorem about symmetry, and you don't need
to unwind any definitions.)
That's what I thought, except I didn't know the word `unwind'.
Thanks for explaining the the local definitions with "let". 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? 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.
BTW how did you ever get so good at HOL Light?
--
Best,
Bill
------------------------------------------------------------------------------
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
