John & Freek, I'm sorry, I just goofed, I really want to get rid of
two lines of code, not just one. Here's the last thm of
http://www.math.northwestern.edu/~richter/OpenIntervalHilbertAxiom.ml
let TwosidesTriangle2aLine_THM = thm `;
let A B C be point;
let l be point_set;
assume Line l /\ ~Collinear (A,B,C) [H1];
thus A,B same_side l \/ B,C same_side l \/ A,C same_side l
proof
(A,B same_side l \/ B,C same_side l) \/ A,C same_side l
proof
assume ~(A,B same_side l \/ B,C same_side l);
~(A,B same_side l) /\ ~(B,C same_side l) [H2] by -;
[...]
I think this should have worked:
thus A,B same_side l \/ B,C same_side l \/ A,C same_side l
proof
assume ~(A,B same_side l) /\ ~(B,C same_side l) [H2];
[...]
I would have thought that miz3 would understand that
alpha \/ beta \/ gamma
is equivalent to
~alpha /\ ~beta ==> gamma
It looks to me that I needed to tell miz3 two facts:
alpha \/ beta \/ gamma <=> (alpha \/ beta) \/ gamma
~(alpha \/ beta) <=> ~alpha /\ ~beta
But I could easily be misunderstanding Mizar, miz3 and 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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
