Examen 3
De Lógica matemática y fundamentos (2018-19)
Revisión del 12:33 8 jul 2019 de Jalonso (discusión | contribuciones)
text ‹Examen de Lógica Matemática y Fundamentos (5 julio 2019)›
theory examen_3_05_jul_sol
imports Main
begin
text ‹Nota: En las demostraciones se pueden las reglas básicas de
deducción natural de la lógica proposicional, de los cuantificadores
y de la igualdad:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
· excluded_middle: (¬P ∨ P)
· allE: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
· allI: (⋀x. P x) ⟹ ∀x. P x
· exI: P x ⟹ ∃x. P x
· exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q
· refl: t = t
· subst: ⟦s = t; P s⟧ ⟹ P t
· trans: ⟦r = s; s = t⟧ ⟹ r = t
· sym: s = t ⟹ t = s
· not_sym: t ≠ s ⟹ s ≠ t
· ssubst: ⟦t = s; P s⟧ ⟹ P t
· box_equals: ⟦a = b; a = c; b = d⟧ ⟹ c = d
· arg_cong: x = y ⟹ f x = f y
· fun_cong: f = g ⟹ f x = g x
· cong: ⟦f = g; x = y⟧ ⟹ f x = g y
También se pueden usar las reglas notnotI y mt que demostramos a
continuación. ›
lemma notnotI: "P ⟹ ¬¬ P"
by auto
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto
text ‹-----------------------------------------------------------------
Ejercicio 1. (2.5 puntos) Demostrar detalladamente que la siguiente
fórmula es una tautología:
p ∨ (q ⟶ ¬(p ⟷ q))
Nota: No usar ninguno de los métodos automáticos: simp, simp_all,
auto, blast, force, fast, arith o metis
--------------------------------------------------------------------›
(* Demostración declarativa. *)
lemma "p ∨ (q ⟶ ¬(p ⟷ q))"
proof -
have "¬p ∨ p" by (rule excluded_middle)
then show "p ∨ (q ⟶ ¬(p ⟷ q))"
proof
assume "¬p"
have "q ⟶ ¬(p ⟷ q)"
proof
assume "q"
show "¬(p ⟷ q)"
proof
assume "p ⟷ q"
then have "p" using `q` by (rule iffD2)
with `¬p` show False by (rule notE)
qed
qed
then show "p ∨ (q ⟶ ¬(p ⟷ q))" by (rule disjI2)
next
assume "p"
then show "p ∨ (q ⟶ ¬(p ⟷ q))" by (rule disjI1)
qed
qed
(* Demostración aplicativa. *)
lemma "p ∨ (q ⟶ ¬(p ⟷ q))"
apply (case_tac "p")
apply (erule disjI1)
apply (rule disjI2)
apply (rule impI)
apply (rule notI)
apply (drule iffD2)
apply assumption
apply (erule notE)
apply assumption
done
text ‹-----------------------------------------------------------------
Ejercicio 2. (2.5 puntos) Se puede formalizar la teoría de las tallas
usando los siguientes símbolos
P x representa que x es de la talla pequeña
M x representa que x es de la talla mediana
G x representa que x es de la talla grande
Mayor x y representa que la talla de x es mayor que la de y.
Los axiomas de las tallas son
∃x. P x
∃x. M x
∃x. G x
∀x y. G x ∧ M y ⟶ Mayor x y
∀x y. M x ∧ P y ⟶ Mayor x y
∀x y z . Mayor x y ∧ Mayor y z ⟶ Mayor x z
∀x. ¬(Mayor x x)
Demostrar detalladamente que la fórmula
∀x. ¬(P x) ∨ ¬(M x)
es consecuencia de los axiomas de las tallas.
Nota: No usar ninguno de los métodos automáticos: simp, simp_all,
auto, blast, force, fast, arith o metis
--------------------------------------------------------------------›
(* Demostración declarativa *)
lemma
assumes "∃x. P x"
"∃x. M x"
"∃x. G x"
"∀x y. G x ∧ M y ⟶ Mayor x y"
"∀x y. M x ∧ P y ⟶ Mayor x y"
"∀x y z . Mayor x y ∧ Mayor y z ⟶ Mayor x z"
"∀x. ¬(Mayor x x)"
shows "∀x. ¬(P x) ∨ ¬(M x)"
proof
fix a
have "¬(P a) ∨ P a" by (rule excluded_middle)
then show "¬(P a) ∨ ¬(M a)"
proof
assume "¬(P a)"
then show "¬(P a) ∨ ¬(M a)" by (rule disjI1)
next
assume "P a"
have "~(M a)"
proof
assume "M a"
have "~(Mayor a a)" using assms(7) by (rule allE)
moreover
have "Mayor a a"
proof -
have "∀y. M a ∧ P y ⟶ Mayor a y" using assms(5) by (rule allE)
then have "M a ∧ P a ⟶ Mayor a a" by (rule allE)
moreover
have "M a ∧ P a" using `M a` `P a` by (rule conjI)
ultimately show "Mayor a a" by (rule mp)
qed
ultimately show False by (rule notE)
qed
then show "¬ P a ∨ ¬ M a" by (rule disjI2)
qed
qed
(* Demostración aplicativa *)
lemma "⟦∃x. P x;
∃x. M x;
∃x. G x;
∀x y. M x ∧ P y ⟶ Mayor x y;
∀x y. G x ∧ M y ⟶ Mayor x y;
∀x y z . Mayor x y ∧ Mayor y z ⟶ Mayor x z;
∀x. ¬(Mayor x x)⟧⟹
∀x. ¬(P x) ∨ ¬(M x)"
apply (rule allI)
apply (case_tac "P x")
prefer 2
apply (rule disjI1, assumption)
apply (rule disjI2)
apply (rule notI)
apply (erule_tac x = x in allE)
apply (erule_tac x = x in allE)
apply (erule_tac x = x in allE)
apply (erule_tac x = x in allE)
apply (erule_tac x = x in allE)
apply (erule notE)
apply (drule mp)
apply (rule conjI, assumption+)
done
text ‹-----------------------------------------------------------------
Ejercicio 3 (2.5 puntos) Consideremos el árbol binario definido por
datatype 'a arbol = H
| N "'a" "'a arbol" "'a arbol"
Por ejemplo, el árbol
e
/ \
/ \
c g
/ \ / \
se representa por "N e (N c H H) (N g H H)".
Se define las funciones
fun nHojas :: "'a arbol ⇒ nat" where
"nHojas H = 1"
| "nHojas (N x i d) = nHojas i + nHojas d"
fun nHojasAaux :: "'a arbol ⇒ nat ⇒ nat" where
"nHojasAaux H n = n + 1"
| "nHojasAaux (N x i d) n = nHojasAaux i (nHojasAaux d n)"
definition nHojasA :: "'a arbol ⇒ nat" where
"nHojasA a ≡ nHojasAaux a 0"
tales que
+ (nHojas a) es el número de hojas del árbol a. Por ejemplo,
nHojas (N e (N c H H) (N g H H)) = 4
+ (nHojasAA a) es el número de hojas del árbol a, calculado
con la función auxiliar nHojasAaux que usa un acumulador. Por
ejemplo,
nHojasA (N e (N c H H) (N g H H)) = 4
Demostrar estructuradamente (es decir, mediante una demostración
declarativa) que las funciones nHojas y nHojasA son equivalentes;
es decir,
nHojasA a = nHojas a
Notas:
1. Los únicos métodos que se pueden usar son induct, (simp only: ...)
y this.
2. En las demostraciones por introducción del cuantificador universal
hay que explicitar el tipo de las variables introducidas con fix.
Por ejemplo, en lugar de
fix x t n
hay que escribir
fix x :: 'a and t :: "'a arbol" and and n :: nat
-------------------------------------------------------------------›
datatype 'a arbol = H
| N "'a" "'a arbol" "'a arbol"
fun nHojas :: "'a arbol ⇒ nat" where
"nHojas H = 1"
| "nHojas (N x i d) = nHojas i + nHojas d"
fun nHojasAaux :: "'a arbol ⇒ nat ⇒ nat" where
"nHojasAaux H n = n + 1"
| "nHojasAaux (N x i d) n = nHojasAaux i (nHojasAaux d n)"
definition nHojasA :: "'a arbol ⇒ nat" where
"nHojasA a ≡ nHojasAaux a 0"
value "nHojas (N e (N c H H) (N g H H)) = 4"
value "nHojasA (N e (N c H H) (N g H H)) = 4"
lemma nHojasA:
"nHojasAaux a n = (nHojas a) + n"
proof (induct a arbitrary: n)
fix n
have "nHojasAaux H n = n + 1" by (simp only: nHojasAaux.simps(1))
also have "… = nHojas H + n" by (simp only: nHojas.simps(1))
finally show "nHojasAaux H n = nHojas H + n" by this
next
fix x :: 'a and
i :: "'a arbol" and
d :: "'a arbol" and
n :: nat
assume HI1: "⋀n. nHojasAaux i n = nHojas i + n"
and HI2: "⋀n. nHojasAaux d n = nHojas d + n"
have "nHojasAaux (N x i d) n = nHojasAaux i (nHojasAaux d n)"
by (simp only: nHojasAaux.simps(2))
also have "… = nHojasAaux i (nHojas d + n)"
by (simp only: HI2)
also have "… = nHojas i + (nHojas d + n)"
by (simp only: HI1)
also have "… = nHojas (N x i d) + n"
by (simp only: nHojas.simps(2))
finally show "nHojasAaux (N x i d) n = nHojas (N x i d) + n"
by this
qed
(* Demostración aplicativa del lema anterior *)
lemma "nHojasAaux a n = (nHojas a) + n"
apply (induct a arbitrary: n)
apply (simp only: nHojasAaux.simps(1))
apply (simp only: nHojas.simps(1))
apply (simp only: nHojasAaux.simps(2))
apply (simp only: nHojas.simps(2))
done
lemma "nHojasA a = nHojas a"
proof -
have "nHojasA a = nHojasAaux a 0" by (simp only: nHojasA_def)
also have "… = (nHojas a)" by (simp only: nHojasA)
finally show "nHojasA a = nHojas a" by this
qed
text ‹---------------------------------------------------------------
Ejercicio 4. (2.5 puntos) Demostrar detalladamente que los grupos
booleanos son conmutativos; es decir, si G un grupo tal que
x ⋅ x = 1
para todo x de G, entonces
x ⋅ y = y ⋅ x
para todo x, y de G.
Nota: No usar ninguno de los métodos automáticos: auto, blast, force,
fast, arith o metis
Nota: Los únicos métodos que se pueden usar son (simp only: ...) o
rule.
------------------------------------------------------------------›
locale grupo =
fixes prod :: "['a, 'a] ⇒ 'a" (infixl "⋅" 70)
and neutro ("𝟭")
and inverso ("_^" [100] 100)
assumes asociativa: "(x ⋅ y) ⋅ z = x ⋅ (y ⋅ z)"
and neutro_i: "𝟭 ⋅ x = x"
and neutro_d: "x ⋅ 𝟭 = x"
and inverso_i: "x^ ⋅ x = 𝟭"
(* Notas sobre notación:
* El producto es ⋅ y se escribe con \ cdot (sin espacio entre ellos).
* El neutro es 𝟭 y se escribe con \ y one (sin espacio entre ellos).
* El inverso de x es x^ y se escribe pulsando 2 veces en ^. *)
context grupo
begin
(* Una demostración declarativa es *)
lemma
assumes "∀x. x ⋅ x = 𝟭"
shows "∀x. ∀y. x ⋅ y = y ⋅ x"
proof (rule allI)+
fix a b
show "a ⋅ b = b ⋅ a"
proof -
have "(b ⋅ a) ⋅ (b ⋅ a) = 𝟭" by (simp only: assms)
then have "b ⋅ ((b ⋅ a) ⋅ (b ⋅ a)) = b ⋅ 𝟭" by (rule arg_cong)
then have "b ⋅ ((b ⋅ a) ⋅ (b ⋅ a)) = b" by (simp only: neutro_d)
then have "(b ⋅ b) ⋅ (a ⋅ (b ⋅ a)) = b" by (simp only: asociativa)
then have "𝟭 ⋅ (a ⋅ (b ⋅ a)) = b" by (simp only: assms)
then have "a ⋅ (b ⋅ a) = b" by (simp only: neutro_i)
then have "(a ⋅ (b ⋅ a)) ⋅ a = b ⋅ a" by (rule arg_cong)
then have "(a ⋅ b) ⋅ (a ⋅ a) = b ⋅ a" by (simp only: asociativa)
then have "(a ⋅ b) ⋅ 𝟭 = b ⋅ a" by (simp only: assms)
then show "a ⋅ b = b ⋅ a" by (simp only: neutro_d)
qed
qed
end
end