Rel 14 (sol)

theory R14_sol
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 ‹------------------------------------------------------------------
  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)"
  using tres_puntos_no_alineados by auto

― ‹ 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)"
proof -
  obtain a b c where distintos: "a ≠ b ∧ a ≠ c ∧ b ≠ c" 
                                 "¬ (∃l. en a l ∧ en b l ∧ en c l)" 
    using tres_puntos_no_alineados by blast
  then have "∀l. en a l ∧ en b l ⟶ ¬ en c l"
    by blast
  then show ?thesis 
    using distintos by blast
qed        

― ‹ Demostración detallada ›
lemma 
  "∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ (∀l. en a l ∧ en b l ⟶ ¬ en c l)"
proof -
  have 1: "∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ ¬ (∃l. en a l ∧ en b l ∧ en c l)" 
    by (rule tres_puntos_no_alineados)
  obtain a b c where 2: "a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ 
                         ¬ (∃l. en a l ∧ en b l ∧ en c l)" 
    using 1 by (elim exE)
  then have 3: "a ≠ b" 
    by (rule conjE)
  have 4: "a ≠ c ∧ b ≠ c ∧ ¬ (∃l. en a l ∧ en b l ∧ en c l)" 
    using 2 by (rule conjE)
  then have 5: "a ≠ c" 
    by (rule conjE)
  have 6: "b ≠ c ∧ ¬ (∃l. en a l ∧ en b l ∧ en c l)" 
    using 4 by (rule conjE)
  then have 7: "b ≠ c" 
    by (rule conjE)
  with 5 have 8: "a ≠ c ∧ b ≠ c"  
    by (rule conjI)
  with 3 have 9: "a ≠ b ∧ a ≠ c ∧ b ≠ c"  
    by (rule conjI)
  have  10: " ¬ (∃l. en a l ∧ en b l ∧ en c l)" 
    using 6 by (rule conjE)
  have 12: "∀l. en a l ∧ en b l ⟶ ¬ en c l"
  proof (rule allI)
    fix l
    show "en a l ∧ en b l ⟶ ¬ en c l"
    proof (rule impI)
      assume 11: "en a l ∧ en b l"
      show "¬ en c l"
      proof (rule notI)
        assume "en c l"
        hence "en a l ∧ en b l ∧ en c l" 
          using 11 by blast
        hence "∃l. en a l ∧ en b l ∧ en c l" 
          by (rule exI)
        with 10 show False 
          by (rule notE)
      qed
    qed
  qed
  have "a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ (∀l. en a l ∧ en b l ⟶ ¬ en c l)" 
    using 9 12 by blast
  then show 
    "∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ (∀l. en a l ∧ en b l ⟶ ¬ en c l)" 
    by (intro exI)
qed      

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"
  using tres_puntos_no_alineados_alt by auto

― ‹ Demostración estructurada ›
lemma punto_no_en_linea: "∀l. ∃x. ¬ en x l"
proof 
  fix l
  obtain a b c where l3: "¬ (en a l ∧ en b l ∧ en c l)" 
    using tres_puntos_no_alineados by blast 
  then show "∃x. ¬ en x l" by blast 
qed

― ‹Demostración detallada ›
lemma "∀l. ∃x. ¬ en x l"
proof (rule allI)
  fix l
  have "∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c 
                ∧ (∀l. en a l ∧ en b l ⟶ ¬ en c l)" 
    by (rule tres_puntos_no_alineados_alt)
  then obtain a b c where "a ≠ b ∧ a ≠ c ∧ b ≠ c 
                           ∧ (∀l. en a l ∧ en b l ⟶ ¬ en c l)" 
    by (elim exE)
  then have "∀l. en a l ∧ en b l ⟶ ¬ en c l" 
    by (elim conjE)
  then have 1:"en a l ∧ en b l ⟶ ¬ en c l" 
    by (rule allE)
  show "∃x. ¬ en x l"
  proof (cases)
    assume "¬ en a l" then show "∃x. ¬ en x l" 
      by (rule exI)
  next
    assume "¬ ¬ en a l"
    then have "en a l" 
      by (rule notnotD)
    then show "∃x. ¬ en x l"
    proof (cases)
      assume "en b l"
      with ‹en a l› have "en a l ∧ en b l" 
        by (rule conjI)
      with 1 have "¬ en c l" 
        by (rule mp)
      then show "∃x. ¬ en x l" 
        by (rule exI)
    next
      assume "¬ en b l" then show "∃x. ¬ en x l" 
        by (rule exI)
    qed
  qed
qed
                    
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"
  by (metis linea_por_dos_puntos tres_puntos_no_alineados_alt)

― ‹ Demostración estructurada ›
lemma dos_lineas_por_punto: "∃l m. en x l ∧ en x m ∧ l ≠ m"
proof -
  obtain z where "z ≠ x" using dos_puntos_de_la_linea 
    by metis
  then obtain l where xl: "en x l" and zl: "en z l" 
    using linea_por_dos_puntos by blast 
  obtain w where n_wl: "¬ en w l" 
    using punto_no_en_linea by blast
  obtain m where wm: "en x m" and zm: "en w m" 
    using linea_por_dos_puntos xl by metis
  then have "l ≠ m" 
    using n_wl by blast  
  then show ?thesis 
    using wm xl by blast 
qed

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"
  using assms linea_por_dos_puntos_unica by blast

― ‹ 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"
proof (rule ccontr)
  assume "x ≠ y" 
  then have "l = m" 
    using linea_por_dos_puntos_unica assms(2-5) by simp
  then show "False" 
    using assms(1) by simp
qed 

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"
  using colineal_def tres_puntos_no_alineados by blast

― ‹ Demostración estructurada ›
lemma (in Geom) "∃a b c. ¬ colineal a b c"
proof -
  have "∃a b c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ 
                ¬ (∃l. en a l ∧ en b l ∧ en c l)" 
    by (rule tres_puntos_no_alineados)
  then have "∃a b c. ¬ (∃l. en a l ∧ en b l ∧ en c l)" 
    by blast
  then show ?thesis 
    by (simp add: colineal_def)
qed

end