John, I wrote 200+ lines of miz3 code proving the first two lemmas of
my paper http://www.math.northwestern.edu/~richter/hilbert.pdf
Thanks again for your help in setting up my framework! I actually
discovered your "new_type_abbrev" myself reading the dox, and I think
I'm in complete agreement with you here:
This is why I think set constraints may work better, even at the
cost of slightly more involved statements.
So in other words, we won't define a type ":plane" taking into account
those constraints. Can you please look at my code below? The only
hard part was the set theory, which you may be able to improve on.
That's my first 4 thms, for which I needed to study section 2.9
"Theorems about sets and functions" of your reference manual.
I have a joke: I'm proving two easy-sounding results, the first being
Given two distinct lines l and m, if X IN l INTERS m, then l INTERS m = {X}.
Well, in my 2 line proof, I had a typo, writing B instead of X. I
wonder how many more typos I can find by formalizing my paper! Thanks
for the nice comment about my son, who already found lots of mistakes.
--
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. *)
(* ================================================================= *)
(* Thanks to Mizar folks who wrote an influential language I was able
to learn, Freek Wiedijk, who wrote the miz3 port of Mizar to HOL
Light, and especially John Harrison, who came up with the entire
framework here coding my Hilbert axiomatic proofs in HOL Light. *)
new_type("point",0);;
new_type_abbrev("line",`:point->bool`);;
new_constant("Between",`:point#point#point->bool`);;
new_constant("===",`:point#point->point#point->bool`);;
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 IN l /\ B IN l /\ C IN l`;;
let Twiddle_DEF = new_definition
`Twiddle A l B <=>
~(?X. (X IN 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 IN l) /\ Between(A, X, B))`;;
(* ------------------------------------------------------------------------- *)
(* The axioms. *)
(* ------------------------------------------------------------------------- *)
let I1 = new_axiom
`!A B. ~(A = B) ==> ?! l. A IN l /\ B IN l`;;
let I2 = new_axiom
`!l. ? A B. A IN l /\ B IN 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 IN l) /\ ~(B IN l) /\ ~(C IN l) /\
?X. X IN l /\ Between(A, X, B) ==>
?Y. Y IN l /\ (Between(A, X, C) \/ Between(B, Y, C))`;;
let B4' = new_axiom
`!A B C. ~ Collinear(A, B, C) ==>
A,B same_side l /\ B,C same_side l ==> A,C same_side l `;;
#load "unix.cma";;
loadt "miz3/miz3.ml";;
horizon := 0;;
let SingletonSubset_THM = thm `;
let p be A->bool;
let x be A;
assume x IN p [H1];
thus {x} SUBSET p
proof
{} SUBSET p by EMPTY_SUBSET;
{x} SUBSET p [X1] by -, H1, INSERT_SUBSET;
qed by -, X1`;;
let SingletonElement_THM = thm `;
let x a be A;
thus a IN {x} <=> a = x
proof
~(a IN {}) [X1] by NOT_IN_EMPTY;
a IN {x} ==> a = x [Imp1]
proof
assume a IN {x} [H1];
~(a IN {}) by NOT_IN_EMPTY;
qed by -, H1, IN_INSERT;
a = x ==> a IN {x} [Imp2]
proof
assume a = x;
a IN {x} by -, IN_INSERT;
qed by -;
qed by Imp1, Imp2`;;
let BiggerThanSingleton_THM = thm `;
let p be A->bool;
let x be A;
assume x IN p [H1];
assume ~(p = {x}) [H2];
thus ?a . a IN p /\ ~(a = x)
proof
{x} SUBSET p by H1, SingletonSubset_THM;
~(p SUBSET {x}) by -, H2, SUBSET_ANTISYM;
consider a such that
a IN p /\ ~(a IN {x}) [X1] by -, SUBSET;
~(a = x) by -, SingletonElement_THM;
qed by -, X1`;;
let Line01infinity_THM = thm `;
let X be point;
let l m be line;
assume ~(l = m) [H1];
assume X IN l /\ X IN m [H2];
thus l INTER m = {X}
proof
(l INTER m = {X}) \/ ~(l INTER m = {X});
cases by -;
suppose l INTER m = {X};
qed by -;
suppose ~(l INTER m = {X}) [H3];
X IN l INTER m by H2, IN_INTER;
consider A such that
A IN l INTER m /\ ~(A = X) [X1] by -, H3, BiggerThanSingleton_THM;
A IN l /\ X IN l /\ A IN m /\ X IN m by -, H2, IN_INTER;
l = m by -, X1, I1;
F by -, H1;
qed by -;
end;`;;
let EquivIntersectionHelp_THM = thm `;
let A X be point;
let l m be line;
assume l INTER m = {X} [H1];
assume A IN m DELETE X [H2];
thus ~(A IN l)
proof
A IN m /\ ~(A = X) [X1] by H2, IN_DELETE;
cases;
suppose ~(A IN l);
qed by -;
suppose (A IN l);
A IN l INTER m by -, X1, IN_INTER;
A = X by -, H1, SingletonElement_THM;
F by -, X1;
qed by -;
end`;;
let EquivIntersection_THM = thm `;
let A B X be point;
let l m be line;
assume l INTER m = {X} [H1];
assume A IN m DELETE X /\ B IN m DELETE X [H2];
assume ~ Between(A, X, B) [H3];
thus ~(A IN l) /\ ~(B IN l) /\ A,B same_side l
proof
A IN m /\ ~(A = X) [X1] by H2, IN_DELETE;
B IN m /\ ~(B = X) [X2] by H2, IN_DELETE;
~(A IN l) /\ ~(B IN l) [X3] by H1, H2, EquivIntersectionHelp_THM;
A,B same_side l [X4]
proof
cases;
suppose A,B same_side l;
qed by -;
suppose ~(A,B same_side l);
consider G such that
(G IN l) /\ Between(A, G, B) [X5] by -, same_side_DEF;
~(A = B) /\ Collinear(A, G, B) [X6] by -, B1;
consider k such that
A IN k /\ G IN k /\ B IN k [X7] by -, Collinear_DEF;
k = m by -, X1, X2, X6, I1;
G IN l INTER m by -, X5, X7, IN_INTER;
G = X by -, H1, SingletonElement_THM;
Between(A, X, B) by -, X5;
F by -, H3;
qed by -;
end;
qed by X3, X4`;;
------------------------------------------------------------------------------
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
