You almost certainly don't want to put Segment into the arguments of your segless definition at all. The fact that your prefix version gets accepted is probably a buglet. Check by seeing what the type of your "working" segless is:
# type_of `segless` Can't you do something like s1 seg_less s2 <=> ... Michael On 29/06/12 16:47, Bill Richter wrote: > 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) > ------------------------------------------------------------------------------ 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
