John, I see my problem, I had
new_constant("on_line",`:point#line->bool`);;
which I guess (for the Currying reasons you explained) isn't your
new_constant("on_line",`:point->line->bool`);;
My Hilbert axiom incidence & betweenness axiom code now works:
(* Paste in these 2 commands:
hol_light> ocaml
#use "hol.ml";; *)
new_type("point",0);;
new_type("line",0);;
new_constant("Between",`:point#point#point->bool`);;
new_constant("===",`:point#point->point#point->bool`);;
new_constant("on_line",`:point->line->bool`);;
parse_as_infix("on_line",(12, "right"));;
parse_as_infix("===",(12, "right"));;
parse_as_infix("cong",(12, "right"));;
let cong_DEF = new_definition
`A,B,C cong X,Y,Z <=>
A,B === X,Y /\ A,C === X,Z /\ B,C === Y,Z`;;
let is_ordered_DEF = new_definition
`is_ordered (A,B,C,D) <=>
Between (A,B,C) /\ Between (A,B,D) /\ Between (A,C,D) /\ Between (B,C,D)`;;
let Collinear_DEF = new_definition
`Collinear(A, B, C) <=>
?l. A on_line l /\ B on_line l /\ C on_line l`;;
let I1 = new_axiom
`!A B. ?! l. A on_line l /\ B on_line l`;;
let I2 = new_axiom
`!l. ? A B. A on_line l /\ B on_line l /\ ~(A = B)`;;
let I3 = new_axiom
`?A B C. ~ Collinear(A, B, C)`;;
let B1 = new_axiom
`! A B C. Between(A, B, C) ==> ~(A = B) /\ ~(A = C) /\ ~(B = C) /\
Between(C, B, A) /\ Collinear(A, B, C)`;;
let B2 = new_axiom
`! A B. ~(A = B) ==> ?C. Between(A, B, C)`;;
let B3 = new_axiom
`!A B C. ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ Collinear(A, B, C)
==> Between(A, B, C) \/ Between(B, C, A) \/ Between(C, A, B)`;;
let B4 = new_axiom
`!A B C. ~ Collinear(A, B, C) ==>
!l. ~(A on_line l) /\ ~(B on_line l) /\ ~(C on_line l) /\
?X. X on_line l /\ Between(A, X, B) ==>
?Y. Y on_line l /\ (Between(A, X, C) \/ Between(B, Y, C))`;;
(* no error messages!
--
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
