My set theory segment ordering works as a prefix (but not infix)!
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar
# val SegmentsOrdering_DEF : thm =
|- !D A B C.
segless Segment A B Segment C D <=>
(?X. X IN open (C,D) /\ Segment A B === Segment C X)
# val SegmentOrderingTransitive_THM : thm =
|- !A B C D E F.
~(A = B) /\ ~(C = D) /\ ~(E = F)
==> segless Segment A B Segment C D
==> segless Segment C D Segment E F
==> segless Segment A B Segment E F
I'm really happy about that. I had to prove a few segment congruence
results in order to run this test. It doesn't work as an infix,
though, and I'm getting an error message I can't understand:
new_type("point",0);;
new_type_abbrev("point_set",`:point->bool`);;
new_constant("Between",`:point->point->point->bool`);;
new_constant("===",`:(point->bool)->(point->bool)->bool`);;
parse_as_infix("===",(12, "right"));;
parse_as_infix("seg_less",(12, "right"));;
let Interval_DEF = new_definition
`! A B X. open (A,B) X <=> Between A X B`;;
let Segment_DEF = new_definition
`Segment A B = {A, B} UNION open (A,B)`;;
let SegmentOrdering_DEF = new_definition
`Segment A B seg_less Segment C D <=>
? X. X IN open (C,D) /\ Segment A B === Segment C X`;;
(*
All's fine until SegmentOrdering_DEF, which gets the Error message
Exception: Failure "new_definition: term not closed".
This puzzles me because the definition works if it's a prefix:
val SegmentsOrdering_DEF : thm =
|- !D A B C.
segless Segment A B Segment C D <=>
(?X. X IN open (C,D) /\ Segment A B === Segment C X)
--
Best,
Bill *)
let SegmentsOrdering_DEF = new_definition
`segless Segment A B Segment C D <=>
? X. X IN open (C,D) /\ Segment A B === Segment C X`;;
------------------------------------------------------------------------------
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
