John and Freek, I finished porting my Tarski geometry Mizar code to miz3, and it's about 2/3 the size!!! Thank you again for your help! John, your `parse_as_infix' advice worked perfectly.
You did a good job of boiling down the essential core. Thanks, John! I spent years working for Richard Stallman, who taught me to write (Emacs) bug reports. It didn't help my math career, but it was great to find folks who WANTED to hear about their errors! I found a workaround for this problem that I feel is a better solution. I didn't know how to nest cases in Mizar, but Freek's grammar showed me how to do it. Two comment about miz3: 1) I was able to write 1500 lines of Mizar code without any good Mizar dox because the error messages were informative enough. The miz3 error messages are not nearly as good, and I'll accept Freek's word that HOL Light causes this. But we can make do with baffling error messages if the dox are good enough. I would sit down right now and write up the syntax & semantics of miz3 if I knew what they were. 2) We don't need strict miz3 compliance with Mizar. Mizar was extremely successful in showing that lots of folks can write up lots of formal proofs, without being a HOL Light or Coq code wizard. But at this point Mizar is like an old pyramid, and we need spaceships. -- Best, Bill (* Paste in these 2 commands: hol_light> ocaml #use "hol.ml";; then paste in the following file*) (* ================================================================= *) (* HOL Light Tarski geometry axiomatic proofs up to Gupta's theorem. *) (* ================================================================= *) (* Proof assistants like HOL Light can be used to help teach rigorous axiomatic geometry in high school using Hilbert's axioms, and introduce students to the world of formal proofs, which should become a hot area in debugging computer software. This is a port, mostly due to John Harrison, of Mizar code, which was heavily influenced by Julien Narboux's Coq pseudo-code http://dpt-info.u-strasbg.fr/~narboux/tarski.html and Wojciech A. Trybulec's incsp_1.miz in the MML library on axioms of incidence geometry. We partially prove the theorem of the 1983 book Metamathematische Methoden in der Geometrie by Schwabhäuser, Szmielew, and Tarski, that Tarski's (extremely weak!) plane geometry axioms imply Hilbert's axioms. We get about as far as Narboux, with Gupta's amazing proof which implies Hilbert's axiom I1 that two points determine a line. 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 of porting my axiomatic proofs to HOL Light. *) new_type("point",0);; parse_as_infix("===",(12, "right"));; parse_as_infix("cong",(12, "right"));; parse_as_infix("on_line",(12, "right"));; parse_as_infix("equal_line",(12, "right"));; new_constant("===",`:point#point->point#point->bool`);; new_constant("Between",`:point#point#point->bool`);; 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 Line_DEF = new_definition `x on_line a,b <=> ~(a = b) /\ (Between (a,b,x) \/ Between (a,x,b) \/ Between (x,a,b))`;; let LineEq_DEF = new_definition `a,b equal_line x,y <=> ~(a = b) /\ ~(x = y) /\ ! c . c on_line a,b <=> c on_line x,y`;; (* ------------------------------------------------------------------------- *) (* The axioms. *) (* ------------------------------------------------------------------------- *) let A1 = new_axiom `!a b. a,b === b,a`;; let A2 = new_axiom `!a b p q r s. a,b === p,q /\ a,b === r,s ==> p,q === r,s`;; let A3 = new_axiom `!a b c. a,b === c,c ==> a = b`;; let A4 = new_axiom `!a q b c. ?x. Between(q,a,x) /\ a,x === b,c`;; let A5 = new_axiom `!a b c x a' b' c' x'. ~(a = b) /\ a,b,c cong a',b',c' /\ Between(a,b,x) /\ Between(a',b',x') /\ b,x === b',x' ==> c,x === c',x'`;; let A6 = new_axiom `!a b. Between(a,b,a) ==> a = b`;; let A7 = new_axiom `!a b p q z. Between(a,p,z) /\ Between(b,q,z) ==> ?x. Between(p,x,b) /\ Between(q,x,a)`;; (* A4 is the Segment Construction axiom, A5 is the SAS axiom and A7 is the Inner Pasch axiom. There are 4 more axioms we're not using yet: there exist 3 non-collinear points; 3 points equidistant from 2 distinct points are collinear; Euclid's parallel postulate; a first order version of Hilbert's Dedekind Cuts axiom. We shall say we apply SAS to a+cbx and a'+c'b'x'. Normally one applies SAS by showing cb = c'b' bx = b'x' (which we assume) and angle cbx cong angle c'b'x'. One might prove the angle congruence by showing that the triangles abc /\ a'b'c' were congruent by SSS (which we also assume) and then apply the theorem that complements of congruent angles are congruent. Hence Tarski's axiom. *) (* ------------------------------------------------------------------------- *) (* Now Mizarlight versions of the actual proofs. *) (* ------------------------------------------------------------------------- *) #load "unix.cma";; loadt "miz3/miz3.ml";; horizon := 0;; let EquivReflexive = thm `; !a b. a,b === a,b proof let a b be point; b,a === a,b by A1; qed by -, A2`;; let EquivSymmetric = thm `; !a b c d. a,b === c,d ==> c,d === a,b proof let a b c d be point; assume a,b === c,d [1]; a,b === a,b by EquivReflexive; qed by -, 1, A2`;; let EquivTransitive = thm `; !a b p q r s . a,b === p,q /\ p,q === r,s ==> a,b === r,s proof let a b p q r s be point; assume a,b === p,q [H1]; assume p,q === r,s [H2]; p,q === a,b by H1, EquivSymmetric; qed by -, H2, A2`;; let Baaa_THM = thm `; !a b. Between (a,a,a) /\ a,a === b,b proof let a b be point; consider x such that Between (a,a,x) /\ a,x === b,b [X1] by A4; a = x by -, A3; qed by -, X1`;; let Bqaa_THM = thm `; !a q. Between(q,a,a) proof let a q be point; consider x such that Between(q,a,x) /\ a,x === a,a [X1] by A4; a = x by -, A3; qed by -, X1`;; let C1_THM = thm `; let a b x y be point; assume ~(a = b) [H1]; assume Between (a,b,x) [H2]; assume Between (a,b,y) [H3]; assume b,x === b,y [H4]; thus y = x proof a,b === a,b /\ a,y === a,y /\ b,y === b,y by EquivReflexive; a,b,y cong a,b,y by -, cong_DEF; y,x === y,y by -, H1, H2, H3, H4, A5; qed by -, A3`;; let Bsymmetry_THM = thm `; let a p z be point; thus Between (a,p,z) ==> Between (z,p,a) proof assume Between (a,p,z) [H1]; Between (p,z,z) by Bqaa_THM; consider x such that Between (p,x,p) /\ Between (z,x,a) [X1] by -, H1, A7; x = p by -, A6; qed by -, X1`;; let Baaq_THM = thm `; let a q be point; thus Between (a,a,q) proof Between (q,a,a) by Bqaa_THM; qed by -, Bsymmetry_THM`;; let BEquality_THM = thm `; let a b c be point; thus Between (a,b,c) /\ Between (b,a,c) ==> a = b proof assume Between (a,b,c) [H1]; assume Between (b,a,c); ? x . Between (b,x,b) /\ Between (a,x,a) by -, H1, A7; consider x such that Between (b,x,b) /\ Between (a,x,a) [X1] by -; b = x by X1, A6; Between (a,b,a) by -, X1; qed by -, A6`;; let B124and234then123_THM = thm `; let a b c d be point; assume Between (a,b,d) [H1]; assume Between (b,c,d) [H2]; thus Between (a,b,c) proof ? x . Between (b,x,b) /\ Between (c,x,a) by H1, H2, A7; consider x such that Between (b,x,b) /\ Between (c,x,a) [X1] by -; b = x by X1, A6; Between (c,b,a) by -, X1; qed by -, Bsymmetry_THM`;; let BTransitivity_THM = thm `; let a b c d be point; assume ~(b = c) [H1]; assume Between (a,b,c) [H2]; assume Between (b,c,d) [H3]; thus Between (a,c,d) proof consider x such that Between (a,c,x) /\ c,x === c,d [X1] by A4; Between (x,c,a) [X2] by -, Bsymmetry_THM; Between (c,b,a) by H2, Bsymmetry_THM; Between (x,c,b) by -, X2, B124and234then123_THM; Between (b,c,x) by -, Bsymmetry_THM; x = d by -, H1, H3, X1, C1_THM; qed by -, X1`;; let BTransitivityOrdered_THM = thm `; let a b c d be point; assume ~(b = c) [H1]; assume Between (a,b,c) [H2]; assume Between (b,c,d) [H3]; thus is_ordered (a,b,c,d) proof Between (a,c,d) [X1] by H1, H2, H3, BTransitivity_THM; Between (d,c,b) [X2] by H3, Bsymmetry_THM; Between (c,b,a) by -, H2, Bsymmetry_THM; Between (d,b,a) by -, H1, X2, BTransitivity_THM; Between (a,b,d) by -, Bsymmetry_THM; qed by H2, -, X1, H3, is_ordered_DEF`;; let B124and234Ordered_THM = thm `; let a b c d be point; assume Between (a,b,d) [H1]; assume Between (b,c,d) [H2]; thus is_ordered (a,b,c,d) proof cases; suppose b = c [P1]; Between (a,b,c) [P2] by -, Bqaa_THM; Between (a,c,d) by P1, H1; qed by P2, H1, -, H2, is_ordered_DEF; suppose ~(b = c) [Q1]; Between (a,b,c) by H1, H2, B124and234then123_THM; qed by -, Q1, H2, BTransitivityOrdered_THM; end`;; let SegmentAddition_THM = thm `; let a b c a' b' c' be point; assume Between (a,b,c) [H1]; assume Between (a',b',c') [H2]; assume a,b === a',b' [H3]; assume b,c === b',c' [H4]; thus a,c === a',c' proof cases; suppose a = b [Y1]; a,a === a',b' by H3, Y1; a',b' === a,a by -, EquivSymmetric; a' = b' by -, A3; qed by -, H4, Y1; suppose ~(a = b) [Z1]; b,a === a,b by A1; b,a === a',b' [Z2] by -, H3, EquivTransitive; a',b' === b',a' by A1; b,a === b',a' [Z3] by -, Z2, EquivTransitive; a,a === a',a' by Baaa_THM; a,b,a cong a',b',a' by -, H3, Z3, cong_DEF; qed by -, Z1, H1, H2, H4, A5; end`;; let CongruenceDoubleSymmetry_THM = thm `; let a b c d be point; assume a,b === c,d [H1]; thus b,a === d,c proof b,a === a,b /\ c,d === d,c [X1] by H1, A1; a,b === d,c by H1, X1, EquivTransitive; qed by -, X1, EquivTransitive`;; let C1prime_THM = thm `; let a b x y be point; assume ~(a = b) [H1]; assume Between (a,b,x) [H2]; assume Between (a,b,y) [H3]; assume a,x === a,y [H4]; thus x = y proof consider m such that Between (b,a,m) /\ a,m === a,b [X1] by A4; Between (m,a,b) [X2] by X1, Bsymmetry_THM; ~(m = a) [X3] by X1, EquivSymmetric, A3, H1; is_ordered (m,a,b,x) by H1, X2, H2, BTransitivityOrdered_THM; Between (m,a,x) [X4] by -, is_ordered_DEF; is_ordered (m,a,b,y) by H1, X2, H3, BTransitivityOrdered_THM; Between (m,a,y) by -, is_ordered_DEF; qed by -, X3, X4, H4, C1_THM`;; let SegmentSubtraction_THM = thm `; let a b c a' b' c' be point; assume Between (a,b,c) [H1]; assume Between (a',b',c') [H2]; assume a,b === a',b' [H3]; assume a,c === a',c' [H4]; thus b,c === b',c' proof cases; suppose a = b [Y1]; a,a === a',b' by -, H3; a',b' === a,a by -, EquivSymmetric; a' = b' by -, A3; qed by -, H4, Y1; suppose ~(a = b) [Z1]; consider x such that Between (a,b,x) /\ b,x === b',c' [Z2] by A4; a,x === a',c' [Z3] by Z2, H2, H3, SegmentAddition_THM; a',c' === a,c by H4, EquivSymmetric; a,x === a,c by -, Z3, EquivTransitive; x = c by -, Z1, Z2, H1, C1prime_THM; qed by -, Z2; end`;; let EasyAngleTransport_THM = thm `; let a O b be point; assume ~(O = a) [H1]; thus ? x y . Between (b,O,x) /\ Between (a,O,y) /\ x,y,O cong a,b,O proof consider x such that Between (b,O,x) /\ O,x === O,a [X2] by A4; x,O === a,O [X3] by -, CongruenceDoubleSymmetry_THM; a,O === x,O [X4] by -, EquivSymmetric; a,x === x,a by A1; a,O,x cong x,O,a [X5] by X4, -, X2, cong_DEF; consider y such that Between (a,O,y) /\ O,y === O,b [X6] by A4; Between (x,O,b) by X2 ,Bsymmetry_THM; x,y === a,b [X7] by H1, X5, X6, -, A5; y,O === b,O by X6, CongruenceDoubleSymmetry_THM; x,y,O cong a,b,O by X7, X3, -, cong_DEF; qed by X2, X6, -`;; let B123and134Ordered_THM = thm `; let a b c d be point; assume Between (a,b,c) [H1]; assume Between (a,c,d) [H2]; thus is_ordered (a,b,c,d) proof Between (d,c,a) /\ Between (c,b,a) by H2, H1, Bsymmetry_THM; is_ordered (d,c,b,a) by -, B124and234Ordered_THM; Between (d,b,a) /\ Between (d,c,b) by -, is_ordered_DEF; Between (a,b,d) /\ Between (b,c,d) by -, Bsymmetry_THM; qed by -, H1, H2, is_ordered_DEF`;; let BextendToLine_THM = thm `; let a b c d be point; assume ~(a = b) [H1]; assume Between (a,b,c) [H2]; assume Between (a,b,d) [H3]; thus ? x . is_ordered (a,b,c,x) /\ is_ordered (a,b,d,x) proof consider u such that Between (a,c,u) /\ c,u === b,d [X1] by A4; is_ordered (a,b,c,u) [X2] by H2, X1, B123and134Ordered_THM; Between (b,c,u) by X2, is_ordered_DEF; Between (u,c,b) [X3] by -, Bsymmetry_THM; u,c === c,u by A1; u,c === b,d [X4] by -, X1, EquivTransitive; Between (a,b,u) [X5] by X2, is_ordered_DEF; consider x such that Between (a,d,x) /\ d,x === b,c [Y1] by A4; is_ordered (a,b,d,x) [Y2] by H3, Y1, B123and134Ordered_THM; Between (b,d,x) [Y3] by -, is_ordered_DEF; b,c === d,x [Y4] by Y1, EquivSymmetric; c,b === b,c by A1; c,b === d,x [Y5] by -, Y4, EquivTransitive; Between (a,b,x) [Y6] by Y2, is_ordered_DEF; u,b === b,x [X6] by X3, Y3, X4, Y5, SegmentAddition_THM; b,u === u,b by A1; b,u === b,x by -, X6, EquivTransitive; u = x by -, H1, X5, Y6, C1_THM; qed by -, X2, Y2`;; let GuptaEasy_THM = thm `; let a b c d be point; assume ~(a = b) [H1]; assume Between (a,b,c) [H2]; assume Between (a,b,d) [H3]; assume ~(b = c) [H4]; assume ~(b = d) [H5]; thus ~ Between (c,b,d) proof cases; suppose ~ Between (c,b,d); qed by -; suppose Between (c,b,d) [H6]; ? x . is_ordered (a,b,c,x) /\ is_ordered (a,b,d,x) by H1, H2, H3, BextendToLine_THM; consider x such that is_ordered (a,b,c,x) /\ is_ordered (a,b,d,x) [X1] by -; Between (b,d,x) by X1, is_ordered_DEF; is_ordered (c,b,d,x) by -, H5, H6, BTransitivityOrdered_THM; Between (b,c,x) /\ Between (c,b,x) by -, X1, is_ordered_DEF; b = c [X2] by -, BEquality_THM; F by -, H4, X2; qed by -; end`;; (* The next result is like SAS: there are 5 pairs of segments 4 equivalent. We say we apply Inner5Segments to abc-x and a'b'c'-x' *) let Inner5Segments_THM = thm `; let a b c x a' b' c' x' be point; assume a,b,c cong a',b',c' [H1]; assume Between (a,x,c) [H2]; assume Between (a',x',c') [H3]; assume c,x === c',x' [H4]; thus b,x === b',x' proof a,b === a',b' /\ a,c === a',c' /\ b,c === b',c' [X1] by H1, cong_DEF; cases; suppose x = c [Case1]; c',x' === c,c by H4, Case1, EquivSymmetric; x' = c' by -, A3; qed by -, Case1, X1; suppose ~(x = c) [Case2]; ~(a = c) [X2] by H2, A6, Case2; consider y such that Between (a,c,y) /\ c,y === a,c [X3] by A4; consider y' such that Between (a',c',y') /\ c',y' === a,c [X4] by A4; a,c === c',y' by X4, EquivSymmetric; c,y === c',y' [X5] by -, X3, EquivTransitive; c,b === c',b' [X6] by X1, CongruenceDoubleSymmetry_THM; a,c,b cong a',c',b' by cong_DEF, X1, X6; b,y === b',y' [X7] by -, X2, X3, X4, X5, A5; ~(y = c) [X8] by X3, EquivSymmetric, A3, X2; Between (y,c,a) /\ Between (c,x,a) by X3, H2, Bsymmetry_THM; Between (y,c,x) [X9] by -, B124and234then123_THM; Between (y',c',a') /\ Between (c',x',a') by -, X4, H3, Bsymmetry_THM; Between (y',c',x') [X10] by -, B124and234then123_THM; y,c === y',c' /\ y,b === y',b' by X5, X7, CongruenceDoubleSymmetry_THM; y,c,b cong y',c',b' by -, cong_DEF, X6; qed by -, X8, X9, X10, H4, A5; end`;; let RhombusDiagBisect_THM = thm `; let b c d c' d' be point; assume Between (b,c,d') [H1]; assume Between (b,d,c') [H2]; assume c,d' === c,d [H3]; assume d,c' === c,d [H4]; assume d',c' === c,d [H5]; thus ? e . Between (c,e,c') /\ Between (d,e,d') /\ c,e === c',e /\ d,e === d',e proof Between (d',c,b) /\ Between (c',d,b) [X1] by H1, H2, Bsymmetry_THM; consider e such that Between (c,e,c') /\ Between (d,e,d') [X2] by X1, A7; c,d === c,d' [X3] by H3, EquivSymmetric; c,c' === c,c' [X4] by EquivReflexive; c,d === d',c' by H5, EquivSymmetric; d,c' === d',c' by -, H4, EquivTransitive; c,d,c' cong c,d',c' by -, X3, X4, cong_DEF; d,e === d',e [X5] by -, X2, EquivReflexive, Inner5Segments_THM; d,c === c,d [X6] by A1; c,d === d,c' by H4, EquivSymmetric; d,c === d,c' [X7] by -, X6, EquivTransitive; d,d' === d,d' [X8] by EquivReflexive; c,d === d',c' [X9] by H5, EquivSymmetric; d',c' === c',d' by A1; c,d === c',d' by -, X9, EquivTransitive; c,d' === c',d' [X10] by -, H3, EquivTransitive; d,d' === d,d' by EquivReflexive; d,c,d' cong d,c',d' by -, X7, X8, X10, cong_DEF; c,e === c',e by -, X2, EquivReflexive, Inner5Segments_THM; qed by -, X2, X5`;; let FlatNormal_THM = thm `; let a b c d d' e be point; assume Between (b,c,d') [H1]; assume Between (d,e,d') [H2]; assume c,d' === c,d [H3]; assume d,e === d',e [H4]; assume ~(c = d) [H5]; assume ~(e = d) [H6]; thus ? p r q . Between (p,r,q) /\ Between (r,c,d') /\ Between (e,c,p) /\ r,c,p cong r,c,q /\ r,c === e,c /\ p,r === d,e proof ~(c = d') by H5, H3, EquivSymmetric, A3; consider p r such that Between (e,c,p) /\ Between (d',c,r) /\ p,r,c cong d',e,c [X1] by -, EasyAngleTransport_THM; p,r === d',e /\ p,c === d',c /\ r,c === e,c [X2] by -, X1, cong_DEF; d',e === d,e by H4, EquivSymmetric; p,r === d,e [X3] by -, X2, EquivTransitive; ~(p = r) [X4] by -, EquivSymmetric, H6, A3; consider q such that Between (p,r,q) /\ r,q === e,d [X5] by A4; Between (d',e,d) [X6] by H2, Bsymmetry_THM; c,p === c,d' by -, X2, CongruenceDoubleSymmetry_THM; c,p === c,d [X7] by -, H3, EquivTransitive; :: Apply SAS to p+crq /\ d'+ced c,q=== c,d by X4, X1, X5, X6, A5; c,d=== c,q by -, EquivSymmetric; c,p=== c,q [X8] by -, X7, EquivTransitive; r,c=== r,c [X9] by EquivReflexive; r,p=== e,d [X10] by X3, CongruenceDoubleSymmetry_THM; e,d=== r,q by X5, EquivSymmetric; r,p=== r,q by -, X10, EquivTransitive; r,c,p cong r,c,q [X11] by -, X9, X8, cong_DEF; Between (r,c,d') [X12] by X1, Bsymmetry_THM; qed by -, X5, X11, X12, X2, X1, X3`;; let EqDist2PointsBetween_THM = thm `; let a b c p q be point; assume ~(a = b) [H1]; assume Between (a,b,c) [H2]; assume a,p === a,q /\ b,p === b,q [H3]; thus c,p === c,q ::a & b are equidistant from p & q. Apply SAS to a+pbc /\ a+qbc. proof a,b === a,b /\ b,c === b,c [X1] by EquivReflexive; a,b,p cong a,b,q by -, H3, cong_DEF; p,c === q,c by H1, -, H2, X1, A5; qed by -, CongruenceDoubleSymmetry_THM`;; let EqDist2PointsInnerBetween_THM = thm `; let a x c p q be point; assume Between (a,x,c) [H1]; assume a,p === a,q /\ c,p === c,q [H2]; thus x,p === x,q ::a and c are equidistant from p and q. Apply Inner5Segments to ::apb-x /\ aqb-x. proof a,c === a,c /\ c,x === c,x [X1] by EquivReflexive; p,c === q,c by H2, CongruenceDoubleSymmetry_THM; a,p,c cong a,q,c by -, H2, X1, cong_DEF; p,x === q,x by -, H1, X1, Inner5Segments_THM; qed by -, CongruenceDoubleSymmetry_THM`;; let Gupta_THM = thm `; let a b c d be point; assume ~(a = b) [H1]; assume Between (a,b,c) [H2]; assume Between (a,b,d) [H3]; thus Between (b,d,c) \/ Between (b,c,d) proof cases; suppose b = c \/ b = d \/ c = d; Between (b,d,c) \/ Between (b,c,d) by -, Baaq_THM, Bqaa_THM; qed by -; suppose ~(b = c) /\ ~(b = d) /\ ~(c = d) [H4]; assume ~ (Between (b,d,c)) [H5]; consider d' such that Between (a,c,d') /\ c,d' === c,d [X1] by A4; consider c' such that Between (a,d,c') /\ d,c' === c,d [X2] by A4; is_ordered (a,b,c,d') by H2, X1, B123and134Ordered_THM; Between (a,b,d') /\ Between (b,c,d') [X3] by -, is_ordered_DEF; is_ordered (a,b,d,c') by H3, X2, B123and134Ordered_THM; Between (a,b,c') /\ Between (b,d,c') [X4] by -, is_ordered_DEF; ~(c = d') [X5] by X1, H4, A3, EquivSymmetric; ~(d = c') [X6] by X2, H4, A3, EquivSymmetric; ~(b = d') [X7] by X3, H4, A6; ~(b = c') [X8] by X4, H4, A6; :: In the proof below, we prove a stronger result than :: BextendToLine_THM with much the same proof. We find u /\ b' :: with essentially a,b,c,d',u and a b,d,c',b' ordered 5-tuples :: with d'u === db /\ cb' === bc. *) consider u such that Between (c,d',u) /\ d',u === b,d [Y1] by A4; is_ordered (b,c,d',u) by X5, X3, Y1, BTransitivityOrdered_THM; Between (b,c,u) /\ Between (b,d',u) [Y2] by -, is_ordered_DEF; consider b' such that Between (d,c',b') /\ c',b' === b,c [Y3] by A4; is_ordered (b,d,c',b') by X6, X4, Y3, BTransitivityOrdered_THM; Between (b,d,b') /\ Between (b,c',b') [Y4] by -, is_ordered_DEF; Between (c',d,b) [Y5] by X4, Bsymmetry_THM; d,c' === c',d /\ b,d === d,b [Y6] by A1; c,d === d,c' by X2, EquivSymmetric; c,d' === d,c' by -, X1, EquivTransitive; c,d' === c',d [Y7] by -, Y6, EquivTransitive; d',u === d,b by Y1, Y6, EquivTransitive; c,u === c',b [Y8] by -, Y1, Y5, Y7, SegmentAddition_THM; c',b' === b',c' /\ b',b === b,b' [Y9] by A1; b,c === c',b' by Y3, EquivSymmetric; b,c === b',c' [Y10] by -, Y9, EquivTransitive; Between (b',c',b) by Y4, Bsymmetry_THM; b,u === b',b by -, Y2, Y10, Y8, SegmentAddition_THM; b,u === b,b' [Y11] by -, Y9, EquivTransitive; is_ordered (a,b,d',u) [Y12] by X7, X3, Y2, BTransitivityOrdered_THM; is_ordered (a,b,c',b') by X8, X4, Y4, BTransitivityOrdered_THM; Between (a,b,u) /\ Between (a,b,b') by -, Y12, is_ordered_DEF; u = b' [Y13] by -, H1, Y11, C1_THM; :: Show c'd' === cd by applying SAS to b+c'cd /\ b'+cc'd. c',b === c,b' by Y13, Y8, EquivSymmetric; b,c' === b',c [Z1] by -, CongruenceDoubleSymmetry_THM; c,c' === c',c by A1; b,c,c' cong b',c',c [Z2] by -, Y10, Z1, cong_DEF; Between (b',c',d) by Y3, Bsymmetry_THM; c',d' === c,d [Z3] by -, H4, Z2, X3, Y7, A5; d',c' === c',d' by A1; d',c' === c,d by -, Z3, EquivTransitive; :: c,d',c',d is a "flat" rhombus. The diagonals bisect each other. consider e such that Between (c,e,c') /\ Between (d,e,d') /\ c,e === c',e /\ d,e === d',e [Z4] by -, X3, X4, X1, X2, RhombusDiagBisect_THM; ~(e = c) [U1] proof cases; suppose ~(e = c); qed by -; suppose e = c [U2]; c' = e by U2, Z4, EquivSymmetric, A3; c' = c by -, U2; Between (b,d,c) [U3] by -, X4; F by -, U3, H5; qed by -; end; e = d [V1] proof cases; suppose e = d; qed by -; suppose ~(e = d) [V2]; consider p r q such that Between (p,r,q) /\ Between (r,c,d') /\ Between (e,c,p) /\ r,c,p cong r,c,q /\ r,c === e,c /\ p,r === d,e [W1] by X3, Z4, X1, H4, V2, FlatNormal_THM; r,p === r,q /\ c,p === c,q [W2] by W1, cong_DEF; :: r and c are equidistant from p and q, r <> c, Between r,c,d', thus also d' ~(c = r) by W1, U1, EquivSymmetric, A3; d',p === d',q [W3] by -, W1, W2, EqDist2PointsBetween_THM; :: c and d' are equidistant from p and q, c <> d', :: Between c,d',b', thus also b'. Between (c,d',b') by Y1, Y13; b',p === b',q [W4] by -, X5, W2, W3, EqDist2PointsBetween_THM; :: d' and c are equidistant from p and q, d' <> c, Between d',c,b, thus also b. Between (d',c,b) by X3, Bsymmetry_THM; b,p === b,q [W5] by -, X5, W3, W2, EqDist2PointsBetween_THM; :: b and b' are equidistant from p and q, Between b,c',b, thus also c'. c',p === c',q [W7]by Y4, W4, W5, EqDist2PointsInnerBetween_THM; :: c' and c are equidistant from p and q, c' <> c, Between c',c,p, thus also p. Between (c',e,c) by Z4, Bsymmetry_THM; is_ordered (c',e,c,p) by -, U1, W1, BTransitivityOrdered_THM; Between (c',c,p) [W8] by -, is_ordered_DEF; ~(c' = c) by Z4, U1, A6; p,p === p,q by -, W8, W7, W2, EqDist2PointsBetween_THM; :: Now we deduce a contradiction from p = q. q = p by -, EquivSymmetric, A3; p = r by -, W1, A6; e = d [W9] by -, W1, EquivSymmetric, A3; F by -, W9, V2; qed by -; end; d' = e by V1, Z4, EquivSymmetric, A3; d' = d by -, V1; Between (b,c,d) by -, X3; qed by -; end`;; (* Using Gupta's theorem, we prove Hilbert's axiom I3; a line is determined by two points. *) let I1part1_THM = thm `; let a b x be point; assume ~(a = b) [H1]; assume ~(a = x) [H2]; assume x on_line a,b [H3]; thus ! c . c on_line a,b ==> c on_line a,x proof let c be point; assume c on_line a,b [H4]; Between (a,b,x) \/ Between (a,x,b) \/ Between (x,a,b) [X1] by H3, Line_DEF; Between (a,b,c) \/ Between (a,c,b) \/ Between (c,a,b) [X2] by H4, Line_DEF; x = b \/ b = c \/ (~(x = b) /\ ~(b = c)); cases by -; suppose x = b [Case1]; qed by -, H4; suppose b = c [Case3]; Between (a,c,x) \/ Between (a,x,c) \/ Between (x,a,c) by -, X1; Between (a,c,x) \/ Between (a,x,c) \/ Between (c,a,x) by -, Bsymmetry_THM; qed by -, H2, Line_DEF; suppose ~(x = b) /\ ~(b = c) [Case2]; Between (a,x,c) \/ Between (a,c,x) \/ Between (x,a,c) [P] proof cases by X1; suppose Between (a,b,x) [Y1]; cases by X2; suppose Between (a,b,c) [Y11]; Between (b,x,c) \/ Between (b,c,x) by -, Y1, H1, Gupta_THM; is_ordered (a,b,x,c) \/ is_ordered (a,b,c,x) by Case2, Y1, Y11, -, BTransitivityOrdered_THM; Between (a,x,c) \/ Between (a,c,x) by -, is_ordered_DEF; qed by -; suppose Between (a,c,b); is_ordered (a,c,b,x) by -, Y1, B123and134Ordered_THM; qed by -, is_ordered_DEF; suppose Between (c,a,b); is_ordered (c,a,b,x) by H1, -, Y1, BTransitivityOrdered_THM; Between (c,a,x) by -, is_ordered_DEF; qed by -, Bsymmetry_THM; end; suppose Between (a,x,b) [Y2]; cases by X2; suppose Between (a,b,c); is_ordered (a,x,b,c) by -, Y2, B123and134Ordered_THM; qed by -, is_ordered_DEF; suppose Between (a,c,b) [Y22]; consider m such that Between (b,a,m) /\ a,m === a,b [X5] by -, A4; ~(a = m) [X6] by H1, X5, EquivSymmetric, A3; Between (m,a,b) by X5, Bsymmetry_THM; :: m,a,c,b & m,a,x,b Between (m,a,c) /\ Between (m,a,x) by -, Y22, Y2, B124and234then123_THM; Between (a,c,x) \/ Between (a,x,c) by -, X6, Gupta_THM; qed by -; suppose Between (c,a,b); Between (c,a,x) by -, Y2, B124and234then123_THM; :: c,a,x,b qed by -, Bsymmetry_THM; end; suppose Between (x,a,b) [Y3]; cases by X2; suppose Between (a,b,c); is_ordered (x,a,b,c) by H1, -, Y3, BTransitivityOrdered_THM; qed by -, is_ordered_DEF; suppose Between (a,c,b); qed by Y3, -, B124and234then123_THM; :: x,a,c,b suppose Between (c,a,b); Between (b,a,x) /\ Between (b,a,c) by Y3, -, Bsymmetry_THM; Between (a,x,c) \/ Between (a,c,x) by -, H1, Gupta_THM; qed by -; end; end; Between (a,x,c) \/ Between (a,c,x) \/ Between (c,a,x) by P, Bsymmetry_THM; c on_line a,x by -, H2, Line_DEF; qed by -; end`;; let I1part2_THM = thm `; let a b x be point; assume ~(a = b) [H1]; assume ~(a = x) [H2]; assume x on_line a,b [H3]; thus a,b equal_line a,x proof ! c . c on_line a,b <=> c on_line a,x [P] proof let c be point; c on_line a,b ==> c on_line a,x [Imp1] proof assume c on_line a,b; c on_line a,x by -, H1, H2, H3, I1part1_THM; qed by -; c on_line a,x ==> c on_line a,b [Imp2] proof assume c on_line a,x [H4]; Between (a,b,x) \/ Between (a,x,b) \/ Between (x,a,b) by H3, Line_DEF; Between (a,b,x) \/ Between (a,x,b) \/ Between (b,a,x) by -, Bsymmetry_THM; b on_line a,x by -, H2, Line_DEF; c on_line a,b by -, H1, H2, H4, I1part1_THM; qed by -; qed by Imp1, Imp2; qed by H1, H2, P, LineEq_DEF`;; let I1part2_THM = thm `; let a b x be point; assume ~(a = b) [H1]; assume ~(a = x) [H2]; assume x on_line a,b [H3]; thus a,b equal_line a,x proof Between (a,b,x) \/ Between (a,x,b) \/ Between (x,a,b) by H3, Line_DEF; Between (a,b,x) \/ Between (a,x,b) \/ Between (b,a,x) by -, Bsymmetry_THM; b on_line a,x [Z1] by -, H2, Line_DEF; ! c . c on_line a,b ==> c on_line a,x [Z2] by H1, H2, H3, I1part1_THM; ! c . c on_line a,x ==> c on_line a,b [Z3] by H1, H2, Z1, I1part1_THM; ! c . c on_line a,x <=> c on_line a,b by Z2, Z3; qed by H1, H2, -, LineEq_DEF`;; let LineEqRefl_THM = thm `; let a b be point; assume ~(a = b) [H1]; thus a,b equal_line a,b proof ! c . c on_line a,b <=> c on_line a,b; a,b equal_line a,b by -, H1, LineEq_DEF; qed by -`;; let LineEqA1_THM = thm `; let a b be point; assume ~(a = b) [H1]; thus a,b equal_line b,a proof ! c . c on_line a,b <=> c on_line b,a [P] proof let c be point; c on_line a,b ==> c on_line b,a [Imp1] proof assume c on_line a,b; Between (a,b,c) \/ Between (a,c,b) \/ Between (c,a,b) by -, Line_DEF; Between (c,b,a) \/ Between (b,c,a) \/ Between (b,a,c) by -, Bsymmetry_THM; qed by -, H1, Line_DEF; c on_line b,a ==> c on_line a,b [Imp2] proof assume c on_line b,a [H3]; Between (b,a,c) \/ Between (b,c,a) \/ Between (c,b,a) by -, Line_DEF; Between (c,a,b) \/ Between (a,c,b) \/ Between (a,b,c) by -, Bsymmetry_THM; qed by -, H1, Line_DEF; qed by Imp1, Imp2; qed by H1, P, LineEq_DEF`;; let LineEqSymmetric_THM = thm `; let a b c d be point; assume ~(a = b) /\ ~(c = d) [H1]; assume a,b equal_line c,d [H2]; thus c,d equal_line a,b proof ! x . x on_line a,b <=> x on_line c,d by H2, LineEq_DEF; ! x . x on_line c,d <=> x on_line a,b by -; c,d equal_line a,b by -, H1, LineEq_DEF; qed by -`;; let LineEqTrans_THM = thm `; let a b c d e f be point; assume ~(a = b) /\ ~(c = d) /\ ~(e = f) [H1]; assume a,b equal_line c,d [H2]; assume c,d equal_line e,f [H3]; thus a,b equal_line e,f proof (! y . y on_line a,b <=> y on_line c,d) /\ (! y . y on_line c,d <=> y on_line e,f) [X2] by H2, H3, LineEq_DEF; (! y . y on_line a,b <=> y on_line e,f) by -; qed by -, H1, LineEq_DEF`;; let onlineEq_THM = thm `; let a b c d x be point; assume ~(a = b) /\ ~(c = d) [H1]; assume x on_line a,b [H2]; assume a,b equal_line c,d [H3]; thus x on_line c,d proof ! y . y on_line a,b <=> y on_line c,d by -, LineEq_DEF; qed by -, H2`;; let I1part2Reverse_THM = thm `; let a b y be point; assume ~(a = b) /\ ~(b = y) [H1]; assume y on_line a,b [H3]; thus a,b equal_line y,b proof a,b equal_line b,a /\ b,y equal_line y,b [Y1] by H1, LineEqA1_THM; y on_line b,a by H3, Y1, onlineEq_THM; b,a equal_line b,y by -, H1, Y1, I1part2_THM; a,b equal_line b,y by -, H1, Y1, LineEqTrans_THM; a,b equal_line y,b by -, H1, Y1, LineEqTrans_THM; qed by -`;; let I1_THM = thm `; let a b x y be point; assume ~(a = b) [H1]; assume ~(x = y) [H2]; assume a on_line x,y [H3]; assume b on_line x,y [H4]; thus x,y equal_line a,b proof cases; suppose (x = b) [H5]; ~(b = y) [P1] by -, H2; b,a equal_line a,b [P2] by H1, LineEqA1_THM; x,y equal_line b,y [P3] by H2, H5, LineEqRefl_THM; a on_line b,y by H3, H5; b,y equal_line b,a by -, P1, H1, I1part2_THM; x,y equal_line b,a by -, H1, H2, P1, P3, LineEqTrans_THM; qed by -, H1, H2, P2, LineEqTrans_THM; suppose ~(x = b) [H6]; x,y equal_line x,b [P4] by -, H2, H6, H4, I1part2_THM; a on_line x,b by -, H2, H6, H3, onlineEq_THM; x,b equal_line a,b by -, H6, H1, I1part2Reverse_THM; qed by H1, H2, H6, P4, -, LineEqTrans_THM; end`;; ------------------------------------------------------------------------------ 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
