Rob, thank you very much for answering my questions! That was smart
of you to notice this problem, which I have worried about:
your axioms seem to be loose about whether `(A, B) same_side l`
holds if A or B is on the line l.
I like your EquivRelOn R P solution (thanks for the correction), or we
can even define EquivRelOFF R I. I have two more questions.
1) Can you tell me why this didn't work?
let SameSideEquivalenceRelation_THM = thm `;
thus Reflexive_Property /\ Symmetric_Property /\ Transitive_Property
proof
qed by SameSideReflexiveRelation_THM, SameSideTransitiveRelation_THM,
SameSideTransitiveRelation_THM, Reflexive_relation_DEF,
Symmetric_relation_DEF, Transitive_relation_DEF `;;
I just got the error ::#2 inference time-out. I imagine I'll have the
same problem with your code. Maybe this is the wrong way to go about
proving that some relation is an equivalence relation.
2) I wrote a new definition I have a definition
let InteriorAngle_DEF = new_definition
`!A O B. int_angle(A, O, B) = if Collinear(A, O, B) then {} else
{P | ~(P IN line(O, A)) /\ ~(P IN line(O, B)) /\
P,B same_side line(O, A) /\ P,A same_side line(O, B)}`;;
I don't if it's working yet, but I would like to simplify this with a
variable declaration and then substitution
a = line(O, A)
b = line(O, B)
You must know how to do that.
--
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
