John, I'm over 400 lines now formalizing my Hilbert axiom paper
http://www.math.northwestern.edu/~richter/hilbert.pdf (code below) and
proved that being on the same side of a line defines an equivalence
relation. This is really a lot of fun, and my son likes it too: the
formalized mathematical proofs become more "concrete".
I know you're real busy, but I have three questions. My first 6 lemmas
here are all set-theory, and I wonder if I'm going about it the right
way. Also, I couldn't figure out how to define an equivalence
relation. It seems that there ought to be a way to define function
ER: point#point->bool ---> bool
(or something) testing if a relation is an equivalence relation.
Below you can see my partly successful effort. Also, my axiom B3 is
bulkier than I'd like. I want to say that exactly one of three things
is true, so I wrote
a \/ b \/ c /\ ~(a /\ b) /\ ~(a /\ c) /\ ~(b /\ c).
Is there a nice HOL Light way to say this?
--
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 of porting my axiomatic proofs to 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))`;;
let Reflexive_relation_DEF = new_definition
`Reflexive_Property <=>
!l:line A:point. ~(A IN l) ==> A,A same_side l`;;
let Symmetric_relation_DEF = new_definition
`Symmetric_Property <=>
!l:line A:point B:point. ~(A IN l) /\ ~(B IN l) ==>
A,B same_side l ==> B,A same_side l`;;
let Transitive_relation_DEF = new_definition
`Transitive_Property <=>
!l:line A:point B:point C:point.
~(A IN l) /\ ~(B IN l) /\ ~(C IN l) ==>
A,B same_side l /\ B,C same_side l ==> A,C same_side l`;;
(* ------------------------------------------------------------------------- *)
(* 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)) /\
~(Between(A, B, C) /\ Between(B, C, A)) /\
~(Between(A, B, C) /\ Between(C, A, B)) /\
~(Between(B, C, A) /\ Between(C, A, B))`;;
let B4 = new_axiom
`!l A B C. ~ Collinear(A, B, C) ==>
!l. ~(A IN l) /\ ~(B IN l) /\ ~(C IN l) ==>
(?X. X IN l /\ Between(A, X, C)) ==>
(?Y. Y IN l /\ Between(A, Y, B)) \/
(?Y. Y IN l /\ Between(B, Y, C))`;;
#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 NonEmptyMember_THM = thm `;
let p be A->bool;
assume ~(p = {}) [H1];
thus ?X. X IN p
proof
{} SUBSET p [X1] by EMPTY_SUBSET;
~(p SUBSET {}) by H1, SUBSET_EMPTY;
qed by -, SUBSET`;;
let DisjointOneNotOther_THM = thm `;
let x be A;
let l m be A->bool;
assume l INTER m = {} [H1];
assume x IN m [H2];
thus ~(x IN l)
proof
assume (x IN l);
x IN l INTER m by -, H2, IN_INTER;
F by -, NOT_IN_EMPTY, H1;
qed by -`;;
let IntersectionSingletonOneNotOther_THM = thm `;
let e x be A;
let l m be A->bool;
assume l INTER m = {x} [H1];
assume e IN l [H2];
assume ~(e = x) [H3];
thus ~(e IN m)
proof
assume e IN m;
e IN l INTER m by H2, -, IN_INTER;
e = x by -, H1, SingletonElement_THM;
F by -, H3;
qed by -`;;
let EquivIntersectionHelp_THM = thm `;
let a x be A;
let l m be A->bool;
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;
qed by -, H1, H2, IntersectionSingletonOneNotOther_THM`;;
let B4'_THM = thm `;
let l be line;
let A B C be point;
assume ~ Collinear(A, B, C) /\ ~(A IN l) /\ ~(B IN l) /\ ~(C IN l) [H1];
assume A,B same_side l /\ B,C same_side l [H2];
thus A,C same_side l
proof
~(?Y. Y IN l /\ Between(A, Y, B)) /\
~(?Y. Y IN l /\ Between(B, Y, C)) ==>
~(?X. X IN l /\ Between(A, X, C)) by H1, B4;
qed by -, H1, H2, same_side_DEF`;;
let BetweenLinear_THM = thm `;
let A C X be point;
let m be line;
assume A IN m /\ C IN m [H1];
assume Between(A, X, C) [H2];
thus X IN m
proof
~(A = C) /\ Collinear(A, X, C) [X1] by H2, B1;
consider l such that
A IN l /\ X IN l /\ C IN l [X2] by -, Collinear_DEF;
l = m by X1, -, H2, H1, I1;
qed by -, X2`;;
let CollinearLinear_THM = thm `;
let A C X be point;
let m be line;
assume A IN m /\ C IN m [H1];
assume Collinear(A, X, C) [H2];
assume ~(A = C) [H3];
thus X IN m
proof
consider l such that
A IN l /\ X IN l /\ C IN l [X1] by H2, Collinear_DEF;
l = m by H3, -, H1, I1;
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});
assume ~(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 -`;;
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
assume ~(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 -;
qed by X3, X4`;;
let SameSideReflexiveRelation_THM = thm `;
thus Reflexive_Property
proof
!l:line A:point. A,A same_side l
proof
let l be line;
let A be point;
~(?X. (X IN l) /\ Between(A, X, A)) by B1;
qed by -, same_side_DEF;
qed by -, Reflexive_relation_DEF`;;
let SameSideSymmetricRelation_THM = thm `;
thus Symmetric_Property
proof
!l:line A:point B:point. ~(A IN l) /\ ~(B IN l) ==>
A,B same_side l ==> B,A same_side l
proof
let l be line;
let A B be point;
assume A,B same_side l [H1];
assume ~(A IN l) /\ ~(B IN l);
~(?X. (X IN l) /\ Between(A, X, B)) by H1, same_side_DEF;
~(?X. (X IN l) /\ Between(B, X, A)) by -, B1;
qed by -, same_side_DEF;
qed by -, Symmetric_relation_DEF`;;
let SameSideTransitiveRelation_THM = thm `;
thus Transitive_Property
proof
!l:line A:point B:point C:point.
~(A IN l) /\ ~(B IN l) /\ ~(C IN l) ==>
A,B same_side l /\ B,C same_side l ==> A,C same_side l
proof
let l be line;
let A B C be point;
assume ~(A IN l) /\ ~(B IN l) /\ ~(C IN l) [H0];
assume A,B same_side l [H1];
assume B,C same_side l [H2];
A,C same_side l
proof
~ Collinear(A, B, C) \/ Collinear(A, B, C);
cases by -;
suppose ~ Collinear(A, B, C);
qed by -, H0, H1, H2, B4'_THM;
suppose Collinear(A, B, C) [Coll];
cases;
suppose A = B \/ A = C \/ B = C;
qed by -, H2, H0, SameSideReflexiveRelation_THM,
Reflexive_relation_DEF, H1;
suppose ~(A = B) /\ ~(A = C) /\ ~(B = C) [Distinct];
consider m such that
A IN m /\ C IN m [W1] by Distinct, I1;
~(l = m) [W2] by W1, H0;
cases;
suppose l INTER m = {} [Disjoint];
!X. Between(A, X, C) ==> ~(X IN l)
proof
let X be point;
assume Between(A, X, C);
X IN m by -, W1, BetweenLinear_THM;
~(X IN l) by -, Disjoint, DisjointOneNotOther_THM;
qed by -;
qed by -, same_side_DEF;
suppose ~(l INTER m = {}) [NotDisjoint];
consider X such that
X IN l INTER m by NotDisjoint, NonEmptyMember_THM;
X IN l /\ X IN m [U1] by -, IN_INTER;
l INTER m = {X} [U2] by W2, -, Line01infinity_THM;
consider E such that
E IN l /\ ~(E = X) [U3] by U1, I2;
~(E IN m) [U4] by U2, U3, IntersectionSingletonOneNotOther_THM;
~(E = B) by U3, H0;
consider B' such that
Between(E, B, B') by -, B2;
Between(B', B, E) [U5] by -, B1;
~(B' = E) /\ ~(B = E) /\ ~(B' = B) /\ Collinear(B', B, E) [U6] by
-, B1;
consider n such that
E IN n /\ B' IN n [U7] by -, I1;
B IN n [U8] by U7, U5, BetweenLinear_THM;
~(l = n) [U9] by H0, -;
l INTER n = {E} [U10] by U9, U7, U3, Line01infinity_THM;
~(B' IN l) [U11] by -, U7, U6,
IntersectionSingletonOneNotOther_THM;
~ Between(B, E, B') [U12] by U6, U5, B3;
B' IN n DELETE E /\ B IN n DELETE E by U7, U8, U6, IN_DELETE;
B, B' same_side l [U13] by U10, -, U12, EquivIntersection_THM;
~(m = n) [U14] by U7, U4;
B IN m by W1, Coll, Distinct, CollinearLinear_THM;
m INTER n = {B} [U15] by -, U8, U14, Line01infinity_THM;
~(A IN n) [U16] by -, W1, Distinct,
IntersectionSingletonOneNotOther_THM;
~ Collinear(A, B, B')
proof
assume Collinear(A, B, B');
consider k such that
A IN k /\ B IN k /\ B' IN k [V1] by -,
Collinear_DEF;
k = n by U6, -, U8, U7, I1;
F by -, U16, V1;
qed by -;
A,B' same_side l [U17] by -, H0, U11, H1, U13, B4'_THM;
~(C IN n) [U18] by U15, W1, Distinct,
IntersectionSingletonOneNotOther_THM;
C,B same_side l [U19] by H0, H2, SameSideSymmetricRelation_THM,
Symmetric_relation_DEF;
~ Collinear(C, B, B')
proof
assume Collinear(C, B, B');
consider k such that
C IN k /\ B IN k /\ B' IN k [V2] by -,
Collinear_DEF;
k = n by U6, -, U8, U7, I1;
F by -, U18, V2;
qed by -;
C,B' same_side l by -, H0, U11, U19, U13, B4'_THM;
B',C same_side l [U20] by H0, U11, -,
SameSideSymmetricRelation_THM,
Symmetric_relation_DEF;
~(B' IN m) [U21] by U15, U7, U6,
IntersectionSingletonOneNotOther_THM;
~ Collinear(A, B', C)
proof
assume Collinear(A, B', C);
consider k such that
A IN k /\ B' IN k /\ C IN k [V3] by -,
Collinear_DEF;
k = m by Distinct, W1, -, I1;
F by -, U21, V3;
qed by -;
A, C same_side l by -, H0, U11, U17, U20, B4'_THM;
qed by -;
end;
end;
end;
qed by -;
qed by -, Transitive_relation_DEF`;;
(* this doesn't work, I just get a ::#2 inference time-out
let SameSideEquivalenceRelation_THM = thm `;
thus Reflexive_Property /\ Symmetric_Property /\ Transitive_Property
proof
qed by SameSideReflexiveRelation_THM, SameSideTransitiveRelation_THM,
SameSideTransitiveRelation_THM, Reflexive_relation_DEF,
Symmetric_relation_DEF, Transitive_relation_DEF `;;
*)
------------------------------------------------------------------------------
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
