Mjoseh en 16:02 26 jun 2019

2019-06-26T16:02:01Z

Mjoseh en 16:01 26 jun 2019

2019-06-26T16:01:50Z

Página nueva

<source lang = "isabelle">

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 detallada *)
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

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 detallada sin auto *)
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

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 detallada *)
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 detallada *)
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 detallada *)
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

</source>

← Revisión anterior	Revisión del 16:02 26 jun 2019
(Sin diferencias)

Sol 14 - Historial de revisiones

Mjoseh en 16:02 26 jun 2019

Mjoseh en 16:01 26 jun 2019