Theory Hilbert_Neutral_3D

(* IsageoCoq - Hilbert_Neutral_3D.thy
Port part of GeoCoq 3.4.0 (https://geocoq.github.io/GeoCoq/)

Version 2.0.0 IsaGeoCoq
Copyright (C) 2021-2025 Roland Coghetto roland.coghetto ( a t ) cafr-msa2p.be

History
Version 1.0.0 IsaGeoCoq
Port part of GeoCoq 3.4.0 (https://geocoq.github.io/GeoCoq/) in Isabelle/Hol (Isabelle2021)
Copyright (C) 2021  Roland Coghetto roland_coghetto (at) hotmail.com

License: LGPL

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 2.1 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301  USA
*)

theory Hilbert_Neutral_3D

imports Hilbert_Neutral

begin

section "Hilbert - Geometry - Neutral 3D"

subsection "Axioms: neutral 3D"

locale Hilbert_neutral_3D = Hilbert_neutral_dimensionless IncidL IncidP EqL EqP IsL IsP BetH CongH CongaH
  for
    IncidL :: "'p ⇒ 'b ⇒ bool" and
    IncidP :: "'p ⇒ 'c ⇒ bool" and
    EqL ::"'b ⇒ 'b ⇒ bool" and
    EqP ::"'c ⇒ 'c ⇒ bool" and
    IsL ::"'b ⇒ bool" and
    IsP ::"'c ⇒ bool" and
    BetH ::"'p⇒'p⇒'p⇒bool" and
    CongH::"'p⇒'p⇒'p⇒'p⇒bool" and
    CongaH::"'p⇒'p⇒'p⇒'p⇒'p⇒'p⇒bool" +
  fixes HS1 HS2 HS3 HS4 :: 'p
  assumes plane_intersection: 
    "IsP p ∧ IsP q ∧ IncidP A p ∧ IncidP A q 
        ⟶ 
     (∃ B. IncidP B p ∧ IncidP B q ∧ A ≠ B)" 
    and   lower_dim_3: 
    "¬ (∃ p. IsP p ∧ IncidP HS1 p ∧ IncidP HS2 p ∧ IncidP HS3 p ∧ IncidP HS4 p)"

end