Thanks to all the help I got here, I'm doing fine formalizing my paper http://www.math.northwestern.edu/~richter/hilbert.pdf http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz I've formalized 12 of my 18 pages on Hilbert plane geometry, and got past the hard part, formalizing the set theory involved in segments and angles, both subsets of the Hilbert plane. In particular I proved the SAS, ASA and Angle Subtraction theorems, stated below together with the definitions and congruence axioms needed.
I'd like to discuss how HOL Light and miz3 actually checking my proofs, as I want my formalization to be a selling point for my paper. John's HOL Light documentation doesn't seem to explain the proof mechanism, but http://hol.sourceforge.net/documentation.html, looks good, and I think I need to read the HOL Logic manual. I'm not good enough at HOL Light to read the miz3.ml code, and even HOL Light experts would have trouble, because miz3 is a very ambitious project to combine declarative (all I'm using) and procedural proofs. John's purple FOL book explains how to implement a Mizar style proof assistant in FOL. John even suggested that his purple book code is all I need. Freek explained that I'm getting heavy miz3 use out of MESON, but I see that John's code http://www.cl.cam.ac.uk/~jrh13/atp/index.html includes meson.ml: MESON-type model elimination Could I really switch to John's purple FOL code? Maybe more reasonably, could one implement John's purple book Mizar code tactics.ml: Tactics and Mizar-style proofs in HOL Light? I'm not of course looking for an improvement in speed or durability, but only in understanding. -- Best, Bill SAS_THM : thm = |- ∀ A B C A' B' C'. ¬Collinear A B C ∧ ¬Collinear A' B' C' ⇒ seg A B ≡ seg A' B' ∧ seg A C ≡ seg A' C' ⇒ angle B A C ≡ angle B' A' C' ⇒ A,B,C ≅ A',B',C' ASA_THM : thm = |- ∀ A B C A' B' C'. ¬Collinear A B C ∧ ¬Collinear A' B' C' ⇒ seg B C ≡ seg B' C' ⇒ angle A B C ≡ angle A' B' C' ⇒ angle B C A ≡ angle B' C' A' ⇒ A,B,C ≅ A',B',C' AngleSubtraction_THM : thm = |- ∀ A O B A' O' B' G G'. ¬Collinear A O B ∧ ¬Collinear A' O' B' ⇒ G ∈ int_angle A O B ∧ G' ∈ int_angle A' O' B' ⇒ angle A O B ≡ angle A' O' B' ⇒ angle A O G ≡ angle A' O' G' ⇒ angle B O G ≡ angle B' O' G' Segment_DEF : thm = |- ∀ A B. seg A B = {A, B} ∪ open (A,B) SEGMENT : thm = |- ∀ s. Segment s ⇔ (∃ A B. s = seg A B ∧ ¬(A = B)) SegmentOrdering_DEF : thm = |- ∀ t s. s seg_less t ⇔ Segment s ∧ Segment t ∧ (∃ C D X. t = seg C D ∧ X ∈ open (C,D) ∧ s ≡ seg C X) Angle_DEF : thm = |- ∀ A O B. angle A O B = ray O A ∪ ray O B ANGLE : thm = |- ∀alpha. Angle alpha ⇔ (∃ A O B. alpha = angle A O B ∧ ¬Collinear A O B) TriangleCong_DEF : thm = |- ∀ A B C A' B' C'. A,B,C ≅ A',B',C' ⇔ ¬Collinear A B C ∧ ¬Collinear A' B' C' ∧ seg A B ≡ seg A' B' ∧ seg A C ≡ seg A' C' ∧ seg B C ≡ seg B' C' ∧ angle A B C ≡ angle A' B' C' ∧ angle B C A ≡ angle B' C' A' ∧ angle C A B ≡ angle C' A' B' C1 : thm = |- ∀ s O Z. Segment s ∧ ¬(O = Z) ⇒ (∃! P. P ∈ ray O Z ━ O ∧ seg O P ≡ s) C2Reflexive : thm = |- Segment s ⇒ s ≡ s C2Symmetric : thm = |- Segment s ∧ Segment t ∧ s ≡ t ⇒ t ≡ s C2Transitive : thm = |- Segment s ∧ Segment t ∧ Segment u ∧ s ≡ t ∧ t ≡ u ⇒ s ≡ u C3 : thm = |- ∀ A B C A' B' C'. B ∈ open (A,C) ∧ B' ∈ open (A',C') ∧ seg A B ≡ seg A' B' ∧ seg B C ≡ seg B' C' ⇒ seg A C ≡ seg A' C' C4 : thm = |- ∀alpha O A l Y. Angle alpha ∧ ¬(O = A) ∧ Line l ∧ O ∈ l ∧ A ∈ l ∧ ¬(Y ∈ l) ⇒ (∃! r. Ray r ∧ (∃B. ¬(O = B) ∧ r = ray O B ∧ ¬(B ∈ l) ∧ B,Y same_side l ∧ angle A O B ≡ alpha)) C5Reflexive : thm = |- Angle alpha ⇒ alpha ≡ alpha C5Symmetric : thm = |- Angle alpha ∧ Angle beta ∧ alpha ≡ beta ⇒ beta ≡ alpha C5Transitive : thm = |- Angle alpha ∧ Angle beta ∧ Angle gamma ∧ alpha ≡ beta ∧ beta ≡ gamma ⇒ alpha ≡ gamma C6 : thm = |- ∀A B C A' B' C'. ¬Collinear A B C ∧ ¬Collinear A' B' C' ∧ seg A B ≡ seg A' B' ∧ seg A C ≡ seg A' C' ∧ angle B A C ≡ angle B' A' C' ⇒ angle A B C ≡ angle A' B' C' ------------------------------------------------------------------------------ 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
