First of all, there is the issue of currying versus uncurrying
again: if you want to write Twiddle(A, l, B) then you need to make
the type of Twiddle `:point#line#point->bool`, or if you want to
keep the type as ``:point->line->point->bool` you need to write
`Twiddle A l B`. Also, if you are going to make an actual
definition of Twiddle then you should delete the line that declares
the constant (since definitions already do that, and will complain
if the constant exists);
Thanks, John! This worked fine. I think I see why Tom Hales worked
with you: you help mathematicians, and you're enough of a
mathematician (your thesis has a lot of math in it) to be able to.
In my code below I use both your `point->line->point->bool' version of
Twiddle, plus an infix version which better expresses the math:
A,B same_side l
That's what Twiddle is supposed to say:
The points A and B are on the same side of the line l. I have a dumb
error message question at the end. But more substantively, I don't
understand how definitions implicitly declare the constants, e.g. in
parse_as_infix("same_side",(12, "right"));;
let same_side_DEF = new_definition
`A,B same_side l <=>
~(?X. (X on_line l) /\ Between(A, X, B))`;;
I'm only going to use the infix `same_side' as if I'd declared it it
to have your type `point->line->point->bool', but how does HOL Light
know that? I would have thought HOL Light would require instead
let same_side_DEF = new_definition
`! A B be point . ! l be line . A,B same_side l <=>
~(?X. (X on_line l) /\ Between(A, X, B))`;;
or something, maybe
! A:point B:point l:line . [...].
Below is a non-set-theory version of the Hilbert's incidence and
betweenness axioms. Axiom C4 turns out to be equivalents to axiom B4.
Even stating Hilbert's congruence axioms is arduous without sets, as
an angle is defined as a set of two rays, and a ray is defined as a
subset of a line. So I'll keep reading your dox about sets!
BTW I had an important typo in my last post, and meant to write
BR> Excellent! It's not as much work as you'd think, maybe, as
BR> reading my own proofs (which are more details than I'm I'm used
BR> to) might be HARDER than coding the proofs is HOL-Light/miz3.
My 13yo son can read my Hilbert paper better than I can, and he found
a ton of errors by going through it line by line. My skills at
math-paper-writing-error-detection don't work well at that (for math
folks) excessively high level of detail. But HOL Light will keep me
coding until it's correct!
--
Best,
Bill
(* Paste in these 2 commands:
hol_light> ocaml
#use "hol.ml";;
then paste in the following file*)
(* ================================================================= *)
(* HOL Light Hilbert geometry axiomatic proofs. *)
(* ================================================================= *)
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 Twiddle_DEF = new_definition
`Twiddle A l B <=>
~(?X. (X on_line l) /\ Between(A, X, B))`;;
parse_as_infix("same_side",(12, "right"));;
let same_side_DEF = new_definition
`A,B same_side l <=>
~(?X. (X on_line l) /\ Between(A, X, B))`;;
(* ------------------------------------------------------------------------- *)
(* The axioms. *)
(* ------------------------------------------------------------------------- *)
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))`;;
let C4 = new_axiom
`!A B C. ~ Collinear(A, B, C) ==>
A,B same_side l /\ B,C same_side l ==> A,C same_side l `;;
(* this doesn't work!!! *)
let B4prime = new_axiom
`!A B C. ~ Collinear(A, B, C) ==>
A,B same_side l /\ B,C same_side l ==> A,C same_side l `;;
(* error message is
let B4prime = new_axiom
^^^^^^^
Error: Unbound constructor B4prime
So HOL Light allows me to call the axiom C4 but not B4prime??? *)
------------------------------------------------------------------------------
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
