John, thanks for the camlp5 response, and I'll work on it later.
Here's a strange bug report. I think I'm going about this wrong (I
should use HOL sets instead), but something doesn't work, and it does
work if I first evaluate code that doesn't look relevant.
(* Paste in these 2 commands:
hol_light> ocaml
#use "hol.ml";;
pasting this in gives an error message *)
new_type("point",0);;
new_type("line",0);;
new_constant("on_line",`:point#line->bool`);;
new_constant("Between",`:point#point#point->bool`);;
new_constant("===",`:point#point->point#point->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`;;
(* Error message for Collinear is
Exception: Failure "typechecking error (initial type assignment)".
If I evaluate some other code first, the beginning of my Tarski code,
however, I get no error message. So start a HOL Light session over:
hol_light> ocaml
#use "hol.ml";;
and paste in this instead: *)
new_type("point",0);;
new_constant("===",`:point#point->point#point->bool`);;
new_constant("Between",`:point#point#point->bool`);;
parse_as_infix("===",(12, "right"));;
parse_as_infix("cong",(12, "right"));;
parse_as_infix("on_line",(12, "right"));;
parse_as_infix("equal_line",(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 Line_DEF = new_definition
`x on_line a,b <=>
~(a = b) /\ (Between (a,b,x) \/ Between (a,x,b) \/ Between (x,a,b))`;;
let LineEq_DEF = new_definition
`a,b equal_line x,y <=>
~(a = b) /\ ~(x = y) /\ ! c . c on_line a,b <=> c on_line x,y`;;
let A1 = new_axiom
`!a b. a,b === b,a`;;
let A2 = new_axiom
`!a b p q r s. a,b === p,q /\ a,b === r,s ==> p,q === r,s`;;
let A3 = new_axiom
`!a b c. a,b === c,c ==> a = b`;;
let A4 = new_axiom
`!a q b c. ?x. Between(q,a,x) /\ a,x === b,c`;;
let A5 = new_axiom
`!a b c x a' b' c' x'.
~(a = b) /\ a,b,c cong a',b',c' /\
Between(a,b,x) /\ Between(a',b',x') /\ b,x === b',x'
==> c,x === c',x'`;;
let A6 = new_axiom
`!a b. Between(a,b,a) ==> a = b`;;
let A7 = new_axiom
`!a b p q z.
Between(a,p,z) /\ Between(b,q,z) ==>
?x. Between(p,x,b) /\ Between(q,x,a)`;;
#load "unix.cma";;
loadt "miz3/miz3.ml";;
new_type("point",0);;
new_type("line",0);;
new_constant("on_line",`:point#line->bool`);;
new_constant("Between",`:point#point#point->bool`);;
new_constant("===",`:point#point->point#point->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 message
--
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
