Freek and John, I'm over 1800 lines in my miz3 Hilbert paper formalization!
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar
Here's a bug report on a miz3 inference error I think I shouldn't have
gotten. I have a definition for a point belonging to the interior of
an angle that works fine. I make a similar but longer definition for
a point belonging to the interior of an triangle that doesn't work.
The obvious workaround worked fine for me
let InteriorTriangle_DEF = new_definition
`! A B C P.
P int_triangle A,B,C <=>
P int_angle A,B,C /\ P int_angle B,C,A /\ P int_angle C,A,B`;;
but I think miz3 should have handled my definition below.
--
Best,
Bill
(*
Paste in these 4 commands, in two mouse copy/pastes
cd ~/hol_light; ocaml
#use "hol.ml";;
#load "unix.cma";;
loadt "miz3/miz3.ml";;
into a terminal window or Emacs window running a shell via M-x shell.
Then paste in the following file. *)
horizon := 0;;
new_type("point",0);;
new_type_abbrev("point_set",`:point->bool`);;
new_constant("Between",`:point#point#point->bool`);;
new_constant("Line",`:point_set->bool`);;
parse_as_infix("same_side",(12, "right"));;
parse_as_infix("int_angle",(12, "right"));;
parse_as_infix("int_triangle",(12, "right"));;
let Interval_DEF = new_definition
`! A B X. open_int (A,B) X <=> Between (A,X,B)`;;
let Collinear_DEF = new_definition
`Collinear (A,B,C) <=>
? l. Line l /\ A IN l /\ B IN l /\ C IN l`;;
let same_side_DEF = new_definition
`A,B same_side l <=>
Line l /\ ~(? X. (X IN l) /\ X IN open_int (A,B))`;;
let InteriorAngle_DEF = new_definition
`! A O B P.
P int_angle A,O,B <=> ~Collinear (A,O,B) /\ ? a b.
Line a /\ O IN a /\ A IN a /\ Line b /\ O IN b /\ B IN b /\
~(P IN a) /\ ~(P IN b) /\ P,B same_side a /\ P,A same_side b`;;
let InteriorTriangle_DEF = new_definition
`! A O B P.
P int_triangle A,O,B <=> ~Collinear (A,O,B) /\ ? a b l.
Line a /\ O IN a /\ A IN a /\
Line b /\ O IN b /\ B IN b /\
Line l /\ A IN l /\ B IN l /\
~(P IN a) /\ ~(P IN b) /\ ~(P IN l) /\
P,B same_side a /\ P,O same_side l /\ P,A same_side b`;;
let EasyInterior_THM = thm `;
let A O B P be point;
assume P int_angle A,O,B [H1];
thus P = P
proof
consider a b such that
~Collinear (A,O,B) /\
Line a /\ O IN a /\ A IN a /\ Line b /\ O IN b /\ B IN b /\
~(P IN a) /\ ~(P IN b) /\ P,B same_side a /\ P,A same_side b by H1,
InteriorAngle_DEF;
qed by -`;;
(*
That works fine, and the output is
val EasyInterior_THM : thm = |- !A O B P. P int_angle A,O,B ==> P = P
*)
let HmmmInterior_THM = thm `;
let A O B P be point;
assume P int_triangle A,O,B [H1];
thus P = P
proof
consider a b l such that
~Collinear (A,O,B) /\
Line a /\ O IN a /\ A IN a /\
Line b /\ O IN b /\ B IN b /\
Line l /\ A IN l /\ B IN l /\
~(P IN a) /\ ~(P IN b) /\ ~(P IN l) /\
P,B same_side a /\ P,O same_side l /\ P,A same_side b by H1,
InteriorTriangle_DEF;
qed by -`;;
(*
This similar proof gets the #1 inference error after the first
statement of the proof.
*)
------------------------------------------------------------------------------
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
