John, here's a more coherent reply, with 800 lines of code below.
miz3 may not know that, say, the formulas S = {x | P x} and
!x. xIN S <=> P x are equivalent, as you might have expected.
Yes, but there's a way around this that's good enough for me! I don't
actually need to use this set notation { } here:
let Ray_DEF = new_definition
`!A B X. ray(A, B) = {X | ~(A = B) /\ Collinear(A, B, X) /\ ~Between(X, A,
B)}`;;
This definition works fine for me:
let Ray_DEF = new_definition
`!A B X. ray(A, B) X <=> ~(A = B) /\ Collinear(A, B, X) /\ ~Between(X, A,
B)`;;
What's important isn't {} in the definition, but being able to treat
ray(A, B) as a set, as I can, e.g. in this simple example:
let OriginInRay_THM = thm `;
let O Q be point;
assume ~(Q = O) [H1];
thus O IN ray(O, Q)
proof
~Between (O,O,Q) [OOQ] by B1;
consider l such that
O IN l /\ Q IN l by H1, I1;
Collinear (O,Q,O) by -, Collinear_DEF;
qed by H1, -, OOQ, IN, Ray_DEF`;;
For a much more interesting example, see the last result
RayWellDefined_THM : thm =
|- !O P Q. ~(Q = O) ==> P IN ray (O,Q) DELETE O ==> ray (O,P) = ray (O,Q)
where I prove the rays are equal by showing each is a subset of the
other. That's the kind of set theory I can't do without, and I have
it, thanks to the first definition in sets.ml
let IN = new_definition
`!P:A->bool. !x. x IN P <=> P x`;;
--
Best,
Bill
(* Paste in these 2 commands
cd ~/hol_light; ocaml
#use "hol.ml";;
and 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. *)
#load "unix.cma";;
loadt "miz3/miz3.ml";;
horizon := 0;;
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"));;
parse_as_infix("same_side",(12, "right"));;
parse_as_infix("int_angle",(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:line. 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))`;;
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`;;
let Ray_DEF = new_definition
`!A B X. ray(A, B) X <=> ~(A = B) /\ Collinear(A, B, X) /\ ~Between(X, A,
B)`;;
(*
exec GOAL_TAC;
p();;
let Angle_DEF = new_definition
`!A O B. Angle(A, O, B) = if Collinear(A, O, B) then {} else
{ray(O, A), ray(O, B)}`;;
*)
let InteriorAngle_DEF = new_definition
`!A O B P.
P int_angle A,O,B <=> ~Collinear(A, O, B) /\ ?a b.
O IN a /\ A IN a /\ O IN b /\ B IN b /\
~(P IN a) /\ ~(P IN b) /\ P,B same_side a /\ P,A same_side 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:point B:point C:point. ~(A = B) /\ ~(A = C) /\ ~(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))`;;
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, SING_SUBSET;
~(p SUBSET {x}) by -, H2, SUBSET_ANTISYM;
consider a such that
a IN p /\ ~(a IN {x}) [X1] by -, SUBSET;
~(a = x) by -, IN_SING;
qed by -, X1`;;
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, IN_SING;
F by -, H3;
qed by -`;;
let CollinearSymmetry_THM = thm `;
let A B C be point;
assume Collinear (A, B, C) [H1];
thus Collinear (A, C, B) /\ Collinear(B, A, C) /\ Collinear(B, C, A) /\
Collinear(C, A, B) /\ Collinear(C, B, A)
proof
consider l such that A IN l /\ B IN l /\ C IN l by H1, Collinear_DEF;
qed by -, Collinear_DEF`;;
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 DoubleSubsetEqual_THM = thm `;
let s t be A->bool;
assume s SUBSET t [H1];
assume t SUBSET s [H2];
thus s = t
proof
!x:A. x IN s ==> x IN t [sSt] by H1, SUBSET;
!x:A. x IN t ==> x IN s [tSs] by H2, SUBSET;
!x:A. x IN s <=> x IN t [sEt] by sSt, tSs;
s = t by -, EXTENSION;
qed by -`;;
let OnePointImpliesAnother_THM = thm `;
let P be point;
thus ?Q:point. ~(Q = P)
proof
consider A B C such that
~(A = B) /\ ~(A = C) /\ ~(B = C) /\ ~Collinear(A, B, C) [X1] by I3;
cases;
suppose B = P;
~(A = B) by -, X1;
qed by -;
suppose ~(B = P);
qed by -;
end`;;
let ExistsPointOffLine_THM = thm `;
let l be line;
thus ?Q:point. ~(Q IN l)
proof
consider A B C such that
~(A = B) /\ ~(A = C) /\ ~(B = C) /\ ~Collinear(A, B, C) [useI3] by I3;
cases;
suppose ~(A IN l) \/ ~(B IN l) \/ ~(C IN l);
qed by -;
suppose (A IN l) /\ (B IN l) /\ (C IN l);
Collinear(A, B, C) by -, Collinear_DEF;
F by -, useI3;
qed by -;
end`;;
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 B C be point;
let m be line;
assume A IN m /\ C IN m [H1];
assume Between(A, B, C) \/ Between(B, C, A) \/ Between(C, A, B) [H2];
thus B IN m
proof
~(A = C) /\
(Collinear(A,B,C) \/ Collinear(B,C,A) \/ Collinear(C,A,B)) [X1] by H2, B1;
consider l such that
A IN l /\ B 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 B C be point;
let m be line;
assume A IN m /\ C IN m [H1];
assume Collinear(A,B,C) \/ Collinear(B,C,A) \/ Collinear(C,A,B) [H2];
assume ~(A = C) [H3];
thus B IN m
proof
consider l such that
A IN l /\ B IN l /\ C IN l [X1] by H2, Collinear_DEF;
l = m by H3, -, H1, I1;
qed by -, X1`;;
let NonCollinearImpliesDistinct_THM = thm `;
let A B C be point;
assume ~Collinear(A, B, C) [H1];
thus ~(A = B) /\ ~(A = C) /\ ~(B = C)
proof
cases;
suppose A = B /\ B = C [C1];
consider Q such that ~(Q = A) by OnePointImpliesAnother_THM;
consider l such that A IN l /\ Q IN l by -, I1;
Collinear(A, B, C) by -, C1, Collinear_DEF;
qed by -, H1;
suppose ~(A = B) /\ B = C [C2];
consider l such that A IN l /\ B IN l by -, I1;
Collinear(A, B, C) by -, C2, Collinear_DEF;
qed by -, H1;
suppose ~(B = C) [C3];
consider l such that B IN l /\ C IN l [X1] by C3, I1;
~(A = B) [U]
proof
assume A = B;
Collinear(A, B, C) by -, X1, Collinear_DEF;
qed by -, H1;
~(A = C) [V]
proof
assume A = C;
Collinear(A, B, C) by -, X1, Collinear_DEF;
qed by -, H1;
qed by U, V, C3;
end`;;
let OriginInRay_THM = thm `;
let O Q be point;
assume ~(Q = O) [H1];
thus O IN ray(O, Q)
proof
~Between (O,O,Q) [OOQ] by B1;
consider l such that
O IN l /\ Q IN l by H1, I1;
Collinear (O,Q,O) by -, Collinear_DEF;
qed by H1, -, OOQ, IN, Ray_DEF`;;
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, IN_SING;
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, MEMBER_NOT_EMPTY;
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') by U6, U7, U8, I1, U16, Collinear_DEF;
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') by U6, U7, U8, I1, U18, Collinear_DEF;
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) by Distinct, W1, I1, U21, Collinear_DEF;
A, C same_side l by -, H0, U11, U17, U20, B4'_THM;
qed by -;
end;
end;
end;
qed by -;
qed by -, Transitive_relation_DEF`;;
let SameSideEquivalenceRelation_THM = thm `;
thus Reflexive_Property /\ Symmetric_Property /\ Transitive_Property
proof
qed by SameSideReflexiveRelation_THM, SameSideSymmetricRelation_THM,
SameSideTransitiveRelation_THM`;;
let ConverseCrossbar_THM = thm `;
let O A B G be point;
assume ~Collinear(A, O, B) [H1];
assume Between(A, G, B) [H2];
thus G int_angle A,O,B
proof
~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by H1,
NonCollinearImpliesDistinct_THM;
consider a such that O IN a /\ A IN a [aOA] by -,
I1;
consider b such that O IN b /\ B IN b [bOB] by Distinct,
I1;
consider l such that A IN l /\ B IN l [lAB] by Distinct,
I1;
~(B IN a) by H1, aOA, Collinear_DEF;
~(a = l) by -, lAB;
a INTER l = {A} [alA] by -, aOA, lAB,
Line01infinity_THM;
~(A = G) /\ ~(A = B) /\ ~(G = B) /\ Between(B, G, A) /\ Collinear(A, G, B)
[X1] by H2,
B1;
~ Between(G, A, B) [notGAB] by -, H2, B3,
B1;
G IN l [Ginl] by lAB, H2,
BetweenLinear_THM;
~(G IN a) [notGina] by alA, Ginl, X1,
IntersectionSingletonOneNotOther_THM;
G IN l DELETE A /\ B IN l DELETE A by Ginl, lAB, X1, IN_DELETE;
G,B same_side a [Gsim_aB] by alA, -, notGAB,
EquivIntersection_THM;
:: same argument shows G,A same_side b
~(A IN b) by H1, bOB, Collinear_DEF;
~(b = l) by -, lAB;
b INTER l = {B} [blB] by -, bOB, lAB,
Line01infinity_THM;
~ Between(G, B, A) [notGBA] by H2, B1, B3;
~(G IN b) [notGinb] by blB, Ginl, X1,
IntersectionSingletonOneNotOther_THM;
G IN l DELETE B /\ A IN l DELETE B by Ginl, lAB, X1, IN_DELETE;
G,A same_side b [Gsim_bA]by blB, -, notGBA,
EquivIntersection_THM;
qed by H1, aOA, bOB, notGina, notGinb, Gsim_aB, Gsim_bA, InteriorAngle_DEF`;;
let InteriorHelp_THM = thm `;
let A O B P be point;
let a b be line;
assume O IN a /\ A IN a /\ O IN b /\ B IN b
[aOAbOB];
assume P int_angle A,O,B [P_AOB];
thus ~(P IN a) /\ ~(P IN b) /\ P,B same_side a /\ P,A same_side b
proof
consider alpha beta such that ~Collinear (A,O,B) /\
O IN alpha /\ A IN alpha /\ O IN beta /\B IN beta /\
~(P IN alpha) /\ ~(P IN beta) /\
P,B same_side alpha /\ P,A same_side beta [exists] by P_AOB,
InteriorAngle_DEF;
~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by -,
NonCollinearImpliesDistinct_THM;
alpha = a /\ beta = b by -, aOAbOB, exists, I1;
qed by -, exists`;;
let WholeRayInterior_THM = thm `;
let A O B X P be point;
assume ~Collinear(A, O, B) [H1];
assume X int_angle A,O,B [H2];
assume P IN ray(O,X) [H3];
assume ~(P = O) [H4];
thus P int_angle A,O,B
proof
~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by H1,
NonCollinearImpliesDistinct_THM;
consider a such that O IN a /\ A IN a [a_OA] by Distinct, I1;
consider b such that O IN b /\ B IN b [b_OB] by Distinct, I1;
~(X IN a) /\ ~(X IN b) /\ X,B same_side a /\ X,A same_side b [XintAOB] by
H2, a_OA, b_OB, InteriorHelp_THM;
~(O = X) /\ Collinear(O, X, P) /\ ~ Between(P, O, X) [P_OX] by H3, IN,
Ray_DEF;
consider x such that O IN x /\ X IN x [x_OX] by P_OX, I1;
:: P IN x [Pin_x] by x_OX, P_OX, Collinear_DEF, CollinearLinear_THM;
P IN x [Pin_x] by x_OX, P_OX, CollinearLinear_THM;
P IN x DELETE O [Pin_x_O] by Pin_x, H4, IN_DELETE;
X IN x DELETE O [Xin_x_O] by x_OX, P_OX, IN_DELETE;
~(x = a) /\ ~(x = b) [x_not_ab] by XintAOB, x_OX;
a INTER x = {O} /\ b INTER x = {O} [axb_intO] by x_not_ab, x_OX, a_OA,
b_OB, Line01infinity_THM;
~(P IN a) /\ P,X same_side a [Psim_aX] by axb_intO, Pin_x_O, Xin_x_O, P_OX,
EquivIntersection_THM;
~(P IN b) /\ P,X same_side b [Psim_bX] by axb_intO, Pin_x_O, Xin_x_O, P_OX,
EquivIntersection_THM;
P,B same_side a /\ P,A same_side b by Psim_aX, Psim_bX, XintAOB, a_OA,
b_OB, H1, Collinear_DEF,
SameSideTransitiveRelation_THM,
Transitive_relation_DEF;
qed by H1, a_OA, b_OB, Psim_aX, Psim_bX, -, InteriorAngle_DEF`;;
let AngleOrdering_THM = thm `;
let O A P Q be point;
let a be line;
assume ~(O = A) [H1];
assume O IN a /\ A IN a [H2];
assume ~(P IN a) /\ ~(Q IN a) [H3];
assume P, Q same_side a [H4];
assume ~Collinear(P, O, Q) [H5];
thus P int_angle Q,O,A \/ Q int_angle P,O,A
proof
~(P = O) /\ ~(P = Q) /\ ~(O = Q) [Distinct] by H5,
NonCollinearImpliesDistinct_THM;
consider p such that O IN p /\ P IN p [p_OP] by Distinct, I1;
consider q such that O IN q /\ Q IN q [q_OQ] by Distinct, I1;
~(q = a) by H3, q_OQ;
q INTER a = {O} by -, H2, q_OQ, Line01infinity_THM;
~(A IN q) by -, H2, H1, IntersectionSingletonOneNotOther_THM;
~(P IN q) [notPq] by q_OQ, H5, Collinear_DEF;
~(p = q) by -, p_OP;
p INTER q = {O} by -, p_OP, q_OQ, Line01infinity_THM;
~Collinear(Q, O, A) [QOA_noncol] by H1, H2, I1, H3, Collinear_DEF;
~Collinear (P,O,A) [POA_noncol] by H1, H2, I1, H3, Collinear_DEF;
assume ~(P int_angle Q,O,A) [notP_QOA];
Q int_angle P,O,A
proof
~(P, A same_side q) by QOA_noncol, H2, q_OQ, H3,
notPq, H4, notP_QOA, InteriorAngle_DEF;
consider G such that (G IN q) /\ Between(P, G, A) [existG] by -,
same_side_DEF;
G int_angle P,O,A [G_POA] by POA_noncol, existG, ConverseCrossbar_THM;
~(G IN a) /\ G,P same_side a [Gsim_aP] by -, InteriorAngle_DEF, H1, H2,
I1;
~(G = O) [GnotO] by -, H2;
G,Q same_side a by Gsim_aP, H3, H4,
SameSideTransitiveRelation_THM, Transitive_relation_DEF;
~Between (Q,O,G) [notQOG] by -, same_side_DEF, H2, B1;
Collinear(O,G,Q) by q_OQ, existG, Collinear_DEF;
Q IN ray(O,G) by GnotO, -, notQOG, IN, Ray_DEF;
qed by POA_noncol, G_POA, -, Distinct, WholeRayInterior_THM;
qed by -`;;
let InteriorReflectionInterior_THM = thm `;
let A O B D A' be point;
assume ~Collinear(A, O, B) [H1];
assume D int_angle A,O,B [H2];
assume Between(A, O, A') [H3];
thus B int_angle D,O,A'
proof
~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by H1,
NonCollinearImpliesDistinct_THM;
consider a such that
O IN a /\ A IN a [a_OA] by Distinct, I1;
consider b such that
O IN b /\ B IN b [b_OB] by Distinct, I1;
~(A IN b) [notAb] by b_OB, H1, Collinear_DEF;
~(B IN a) [notBa] by a_OA, H1, Collinear_DEF;
~(a = b) by -, b_OB;
b INTER a = {O} [ab_O] by -, a_OA, b_OB, Line01infinity_THM;
A' IN a [A'a] by H3, a_OA, BetweenLinear_THM;
A' IN a DELETE O by A'a, H3, B1, IN_DELETE;
~(A' IN b) [notA'b] by ab_O, -, EquivIntersectionHelp_THM;
~(A,A' same_side b) [Ansim_bA'] by b_OB, H3, same_side_DEF ;
~(D IN a) /\ ~(D IN b) /\
D,B same_side a /\ D,A same_side b [DintAOB] by a_OA, b_OB, H2,
InteriorHelp_THM;
~(D,A' same_side b) [Dnsim_bA']
proof
assume D,A' same_side b;
A',D same_side b by DintAOB, notA'b, -, SameSideSymmetricRelation_THM,
Symmetric_relation_DEF;
A',A same_side b by DintAOB, notA'b, notAb, -,
SameSideTransitiveRelation_THM, Transitive_relation_DEF;
A,A' same_side b by notA'b, notAb, -, SameSideSymmetricRelation_THM,
Symmetric_relation_DEF;
F by -, Ansim_bA';
qed by -;
~(D int_angle B,O,A') [notD_BOA']
proof
assume D int_angle B,O,A';
D,A' same_side b by b_OB, a_OA, A'a, -, DintAOB, InteriorHelp_THM;
F by -, Dnsim_bA';
qed by -;
~Collinear (D,O,B) [DOB_noncol] by Distinct, b_OB, I1, DintAOB,
Collinear_DEF;
~(O = A') by H3, B1;
B int_angle D,O,A' by -, a_OA, A'a, DintAOB, notBa, DOB_noncol, notD_BOA',
AngleOrdering_THM;
qed by -`;;
let Crossbar_THM = thm `;
let O A B D be point;
assume ~Collinear(A, O, B) [H1];
assume D int_angle A,O,B [H2];
thus ?G. Between(A, G, B) /\ G IN ray(O, D)
proof
~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by H1,
NonCollinearImpliesDistinct_THM;
consider a such that
O IN a /\ A IN a [a_OA] by Distinct, I1;
consider b such that
O IN b /\ B IN b [b_OB] by Distinct, I1;
~(B IN a) [notBa] by a_OA, H1, Collinear_DEF;
~(D IN a) /\ ~(D IN b) /\ D,B same_side a [D_AOB] by a_OA, b_OB, H2,
InteriorHelp_THM;
~(D = O) [DnotO] by D_AOB, a_OA;
consider l such that
O IN l /\ D IN l [l_OD] by -, I1;
~(a = l) /\ ~(b = l) [abl_distinct] by l_OD, D_AOB, b_OB, notBa;
a INTER l = {O} [alO] by abl_distinct, a_OA, l_OD, Line01infinity_THM;
b INTER l = {O} [blO] by abl_distinct, b_OB, l_OD, Line01infinity_THM;
~(A IN l) /\ ~(B IN l) [ABnot_l] by alO, blO, a_OA, b_OB, Distinct,
IntersectionSingletonOneNotOther_THM;
consider A' such that Between(A, O, A') [AOA'] by Distinct, B2;
A' IN a [A'a] by a_OA, -, BetweenLinear_THM;
~(A' = O) [A'notO] by AOA', B1;
~(A,A' same_side l) [Ansim_lA'] by l_OD, AOA', same_side_DEF;
~(A' IN l) [A'not_l] by alO, A'a, A'notO,
IntersectionSingletonOneNotOther_THM;
B int_angle D,O,A' by H1, H2, AOA', InteriorReflectionInterior_THM;
B,A' same_side l [Bsim_lA'] by l_OD, a_OA, A'a, -, InteriorHelp_THM;
~(A,B same_side l) [Ansim_lB]
proof
assume A,B same_side l;
A,A' same_side l by ABnot_l, A'not_l, -, Bsim_lA',
SameSideTransitiveRelation_THM, Transitive_relation_DEF;
qed by -, Ansim_lA';
consider G such that
Between(A, G, B) /\ G IN l [AGB] by Ansim_lB, same_side_DEF;
Collinear (O,D,G) [ODGcol] by AGB, l_OD, Collinear_DEF;
G int_angle A,O,B by H1, AGB, ConverseCrossbar_THM;
~(G IN a) /\ G,B same_side a [Gsim_aB] by a_OA, b_OB, -, InteriorHelp_THM;
D,B same_side a by a_OA, b_OB, H2, InteriorHelp_THM;
B,D same_side a by notBa, D_AOB, -, SameSideSymmetricRelation_THM,
Symmetric_relation_DEF;
G,D same_side a [Gsim_aD] by Gsim_aB, notBa, D_AOB, Gsim_aB, -,
SameSideTransitiveRelation_THM, Transitive_relation_DEF;
~Between(G, O, D) by a_OA, -, same_side_DEF;
G IN ray(O,D) [G_OD] by DnotO, ODGcol, -, IN, Ray_DEF;
qed by AGB, G_OD`;;
(*
exec GOAL_TAC;
p();;
*)
let IntervalTransitivity_THM = thm `;
let O P Q R be point;
let m be line;
assume O IN m [H1];
assume P IN m DELETE O /\ Q IN m DELETE O /\ R IN m DELETE O [H2];
assume ~Between(P, O, Q) /\ ~Between(Q, O, R) [H3];
thus ~Between(P, O, R)
proof
P IN m /\ Q IN m /\ R IN m /\ ~(P = O) /\ ~(Q = O) /\ ~(R = O) [H2'] by H2,
IN_DELETE;
consider E such that
~(E IN m) [notEm] by ExistsPointOffLine_THM;
~(O = E) by H1, notEm;
consider l such that
O IN l /\ E IN l [OE_l] by -, I1;
~(m = l) by notEm, OE_l;
l INTER m = {O} [ml_O] by -, H1, OE_l,
Line01infinity_THM;
~(P IN l) /\ ~(Q IN l) /\ ~(R IN l) [PQRnotl] by ml_O, H2',
IntersectionSingletonOneNotOther_THM;
P,Q same_side l /\ Q,R same_side l [Psim_lQsim_lR] by ml_O, H2, H3,
PQRnotl, EquivIntersection_THM;
P,R same_side l [Psim_lR] by PQRnotl, Psim_lQsim_lR,
SameSideTransitiveRelation_THM,
Transitive_relation_DEF;
qed by OE_l, -, same_side_DEF`;;
let RayLine_THM = thm `;
let O P X be point;
let l be line;
assume O IN l /\ P IN l [H1];
assume X IN ray(O,P) [H2];
thus X IN l
proof
~(O = P) /\ Collinear (O,P,X) by H2, IN, Ray_DEF;
X IN l by H1, -, CollinearLinear_THM;
qed by -`;;
let RayWellDefinedHalfway_THM = thm `;
let O P Q be point;
assume ~(Q = O) [H1];
assume P IN ray(O, Q) DELETE O [H2];
thus ray(O, P) SUBSET ray(O, Q)
proof
consider m such that
O IN m /\ Q IN m [OQm] by H1, I1;
P IN ray(O, Q) /\ ~(P = O) [H2'] by H2, IN_DELETE;
P IN m [Pm] by OQm, H2', RayLine_THM;
P IN m DELETE O /\ Q IN m DELETE O [PQm_O] by Pm, H2', OQm, H1, IN_DELETE;
~Between (P, O, Q) [notPOQ] by H2', IN, Ray_DEF;
!X. X IN ray(O, P) ==> X IN ray(O, Q)
proof
let X be point;
assume X IN ray(O, P) [XrOP];
X IN m [Xm] by OQm, Pm, H2', -, RayLine_THM;
Collinear (O, Q, X) [OQXcol] by OQm, Xm, Collinear_DEF;
~Between (X, O, P) [notXOP] by XrOP, IN, Ray_DEF;
cases;
suppose X = O;
X IN ray(O, Q) by H1, -, OriginInRay_THM;
qed by -;
suppose ~(X = O) [notXO];
X IN m DELETE O by Xm, notXO, IN_DELETE;
~Between(X, O, Q) by OQm, -, PQm_O, notXOP, notPOQ,
IntervalTransitivity_THM;
X IN ray(O, Q) by H1, OQXcol, -, IN, Ray_DEF;
qed by -;
end;
qed by -, SUBSET`;;
let RayWellDefined_THM = thm `;
let O P Q be point;
assume ~(Q = O) [H1];
assume P IN ray(O, Q) DELETE O [H2];
thus ray(O, P) = ray(O, Q)
proof
ray (O,P) SUBSET ray (O,Q) [PsubsetQ] by H1, H2,
RayWellDefinedHalfway_THM;
P IN ray(O, Q) /\ ~(P = O) [H2'] by H2, IN_DELETE;
Collinear (O, Q, P) /\ ~Between (P, O, Q) [notPOQ] by H2', IN, Ray_DEF;
Collinear (O, P, Q) [OQPcol] by notPOQ, CollinearSymmetry_THM;
~Between (Q, O, P) [notQOP] by notPOQ, B1;
Q IN ray(O, P) by H2', OQPcol, notQOP, IN, Ray_DEF;
Q IN ray(O, P) DELETE O [QrOP_O] by -, H1, IN_DELETE;
ray (O,Q) SUBSET ray (O,P) [QsubsetP] by H2', QrOP_O,
RayWellDefinedHalfway_THM;
qed by PsubsetQ, QsubsetP, DoubleSubsetEqual_THM `;;
------------------------------------------------------------------------------
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
