R14

chapter ‹R14: Una axiomatización de la Geometría›

theory R14
imports Main

begin

text ‹
  --------------------------------------------------------------------------------------------------
  Ejercicio 1. Hilbert publicó una axiomatización de la geometría que incluía los siguientes 
  axiomas:
  1. Por dos puntos distintos pasa una línea recta.
  2. Por dos puntos distintos no pasa más de una línea recta.
  3. Toda línea tiene al menos dos puntos.
  4. Existen al menos tres puntos no alineados.

  Usando la relacion en(p,l) para representar que el punto p está en la línea l, definir el entorno 
  local Geom en el que se verifiquen los 4 axiomas anteriores.
  --------------------------------------------------------------------------------------------------
›

locale Geom =
  fixes en :: "'p ⇒ 'l ⇒ bool"
  assumes linea_por_dos_puntos:       "a ≠ b ⟹ ∃l. en a l ∧ en b l" 
      and linea_por_dos_puntos_unica: "⟦a ≠ b; en a l; en b l; en a m; en b m⟧ ⟹ l = m"
      and dos_puntos_de_la_linea:     "∃a b. a ≠ b ∧ en a l ∧ en b l"
      and tres_puntos_no_alineados:   "∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ 
                                               ¬ (∃l. en a l ∧ en b l ∧ en c l)"
begin

text ‹
  --------------------------------------------------------------------------------------------------
  Nota: En los ejercicios siguientes se pide la demostración
  estructurada con el menor número de métodos automáticos posibles.
  --------------------------------------------------------------------------------------------------
›

text ‹
  --------------------------------------------------------------------------------------------------
  Ejercicio 2. Demostrar que
    ∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ (∀l. en a l ∧ en b l ⟶ ¬ en c l)
  --------------------------------------------------------------------------------------------------
›

― ‹ Demostración automática ›
lemma "∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ (∀l. en a l ∧ en b l ⟶ ¬ en c l)"
  oops

― ‹ Demostración estructurada ›
lemma tres_puntos_no_alineados_alt:
  "∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ (∀l. en a l ∧ en b l ⟶ ¬ en c l)"
oops       
  
text ‹
  --------------------------------------------------------------------------------------------------
  Ejercicio 3. Demostrar que no todos los puntos pertenecen a la misma línea.
  --------------------------------------------------------------------------------------------------
›

― ‹ Demostración automática ›
lemma "∀l. ∃x. ¬ en x l"
  oops

― ‹ Demostración estructurada ›
lemma punto_no_en_linea: "∀l. ∃x. ¬ en x l"
oops 

text ‹
  --------------------------------------------------------------------------------------------------
  Ejercicio 4. Demostrar que por cada punto pasa más de una línea.
  --------------------------------------------------------------------------------------------------
›

― ‹ Demostración automática ›
lemma "∃l m. en x l ∧ en x m ∧ l ≠ m"
  oops 

― ‹ Demostración estructurada ›
lemma dos_lineas_por_punto: "∃l m. en x l ∧ en x m ∧ l ≠ m"
 oops 

text ‹
  --------------------------------------------------------------------------------------------------
  Ejercicio 5. Demostrar que dos líneas distintas no pueden tener más de un punto común.
  --------------------------------------------------------------------------------------------------
›

― ‹ Demostración automática ›
lemma  
   assumes "l ≠ m" 
           "en x l" 
           "en x m" 
           "en y l" 
           "en y m" 
   shows "x = y"
  oops 

― ‹ Demostración estructurada ›
lemma interseccion_lineas_distintas: 
   assumes "l ≠ m" 
           "en x l" 
           "en x m" 
           "en y l" 
           "en y m" 
   shows "x = y"
oops

end

text ‹
  --------------------------------------------------------------------------------------------------
  Ejercicio 6. Extender el ámbito ("locale") Geom definiendo la relación colineal tal que
  (colineal a b c) se verifica si existe una línea recta que pasa por los puntos a, b y c.
  --------------------------------------------------------------------------------------------------
›

definition (in Geom) 
  colineal :: "'p ⇒ 'p ⇒ 'p ⇒ bool" 
  where "colineal a b c ≡ ∃l. en a l ∧ en b l ∧ en c l"

text ‹
  --------------------------------------------------------------------------------------------------
  Ejercicio 7. Demostrar que existen tres puntos a, b y c tales que
     ¬ colineal a b c
  --------------------------------------------------------------------------------------------------
›

― ‹ Demostración automática ›
lemma (in Geom) "∃a b c. ¬ colineal a b c"
  oops 

  ― ‹ Demostración estructurada ›
lemma (in Geom) "∃a b c. ¬ colineal a b c"
oops 

end