Thanks, Michael! After working your exercise, I see I didn't achieve
any set theory triumph, and have to go back to the drawing board:
# type_of `segless`;;
val it : hol_type =
`:(point->point->point->bool)->point->point->(point->point->point->bool)->point->point->bool
# type_of `Segment`;;
val it : hol_type = `:point->point->point->bool`
And that means that segless is a predicate with 6 arguments:
segless Segment A B Segment C D
But I guess I'm only using 4 of them, and could've defined instead
segless A B C D
That's fine, but it's not set theory, and it's not what I intended. I
meant for segless to have 2 arguments, just like ===:
new_constant("===",`:(point->bool)->(point->bool)->bool`);;
Can't you do something like
s1 seg_less s2 <=> ...
Hmm, I posted something that HOL Light likes, but I couldn't prove
anything with it:
parse_as_infix("seg_less",(12, "right"));;
let SegmentOrdering_DEF = new_definition
`s seg_less t <=>
? A B C D X. s = Segment A B /\ t = Segment C D /\
X IN open (C,D) /\ Segment A B === Segment C X`;;
I guess that's really what I want, and maybe I just didn't work hard
enough with it. I have to deal with the fact that given a segment s,
there may be more than one way to write it as s = Segment A B.
In fact, I prove there's at least two ways:
SegmentSymmetry_THM : thm = |- ∀ A B. Segment A B = Segment B A
--
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
