Relación 10
De Razonamiento automático (2016-17)
Revisión del 17:27 1 feb 2017 de Marpoldia1 (discusión | contribuciones)
chapter {* R10: Formalización y argumentación con Isabelle/HOL *}
theory R10_Formalizacion_y_argmentacion
imports Main
begin
text {*
---------------------------------------------------------------------
El objetivo de esta es relación formalizar y demostrar la corrección
de los argumentos automáticamente y detalladamente usando sólo las reglas
básicas de deducción natural.
· 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
· allI: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
· allE: (⋀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⟧ ⟹ a: = 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
---------------------------------------------------------------------
*}
text {*
Se usarán las reglas notnotI, mt, no_ex y no_para_todo que demostramos
a continuación.
*}
lemma notnotI: "P ⟹ ¬¬ P"
by auto
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto
lemma no_ex: "¬(∃x. P(x)) ⟹ ∀x. ¬P(x)"
by auto
lemma no_para_todo: "¬(∀x. P(x)) ⟹ ∃x. ¬P(x)"
by auto
text {* ---------------------------------------------------------------
Ejercicio 1. Formalizar, y demostrar la corrección, del siguiente
argumento
Si la válvula está abierta o la monitorización está preparada,
entonces se envía una señal de reconocimiento y un mensaje de
funcionamiento al controlador del ordenador. Si se envía un mensaje
de funcionamiento al controlador del ordenador o el sistema está en
estado normal, entonces se aceptan las órdenes del operador. Por lo
tanto, si la válvula está abierta, entonces se aceptan las órdenes
del operador.
Usar A : La válvula está abierta.
P : La monitorización está preparada.
R : Envía una señal de reconocimiento.
F : Envía un mensaje de funcionamiento.
N : El sistema está en estado normal.
O, AO, OK : Se aceptan órdenes del operador.
------------------------------------------------------------------ *}
(* ivamenjim manmorjim1 crigomgom migtermor serrodcal bowma *)
(* Buscando, he detectado que 'O' es un carácter especial en Isabelle y que forma parte de su
sintaxis pre-definida, por lo que da problemas a la hora de formalizar y demostrar
el argumento planteado. Por lo tanto, en su lugar he usado "AO: Se aceptan órdenes del operador" *)
lemma ejercicio_1:
assumes 1: "(A ∨ P) ⟶ (R ∧ F)"
assumes 2: "(F ∨ N) ⟶ AO"
shows "A ⟶ AO"
proof -
{assume 3: "A"
have 4: "A ∨ P" using 3 by (rule disjI1)
have 5: "R ∧ F" using 1 4 by (rule mp)
have 6: "F" using 5 by (rule conjunct2)
have 7: "F ∨ N" using 6 by (rule disjI1)
have 8: "AO" using 2 7 by (rule mp)}
then show "A ⟶ AO" by (rule impI)
qed
(*danrodcha ferrenseg anaprarod marcarmor13 pablucoto marpoldia1 *)
lemma ej_1:
assumes "A ∨ P ⟶ R ∧ F" and
"F ∨ N ⟶ OK"
shows "A ⟶ OK"
proof (rule impI)
{assume "A"
hence "A ∨ P" by (rule disjI1)
with assms(1) have "R ∧ F" by (rule mp)
hence "F" by (rule conjE)
hence "F ∨ N" by (rule disjI1)
with assms(2) show "OK" by (rule mp)}
qed
(*pabrodmac paupeddeg*)
lemma ejercicio_1_1:
assumes "A ∨ P ⟶ R ∧ F"
"F ∨ N ⟶ Op"
shows "A ⟶ Op"
proof
assume "A"
hence "A ∨ P" by (rule disjI1)
have "R ∧ F" using `A ∨ P ⟶ R ∧ F` `A ∨ P` by (rule mp)
hence "F" by (rule conjE)
hence "F ∨ N" by (rule disjI1)
show "Op" using `F ∨ N ⟶ Op` `F ∨ N` by (rule mp)
qed
(*josgarsan*)
lemma ejericio_1_2:
assumes 1: "(A ∨ P) ⟶ (R ∧ F)" and
2: "(F ∨ N) ⟶ Op"
shows "A ⟶ Op"
proof
assume 3: A
have 4:"(A ∨ P)" using 3 by (rule disjI1)
have "(R ∧ F)" using 1 4 by (rule mp)
then have "F" by (rule conjunct2)
then have 5: "(F ∨ N)" by (rule disjI1)
show "Op" using 2 5 by (rule mp)
qed
(* fracorjim1 *)
lemma ejercicio_1_3:
assumes H1: "(A ∨ P) → (R ∧ F)" and
H2: "(F ∨ N) → O"
shows "A → O"
proof -
assume "A"
have "A ∨ P" by (rule disjI1)
hence "R ∧ F" using H1 by (rule mp)
hence "F" by (rule conjI2)
hence "F ∨ N" by (rule disjI1)
hence "O" using H2 by (rule mp)
thus "A → O"
qed
text {* ---------------------------------------------------------------
Ejercicio 2. Formalizar, y decidir la corrección, del siguiente
argumento
Hay estudiantes inteligentes y hay estudiantes trabajadores. Por
tanto, hay estudiantes inteligentes y trabajadores.
Usar I(x) para x es inteligente
T(x) para x es trabajador
------------------------------------------------------------------ *}
(* ivamenjim ferrenseg danrodcha anaprarod crigomgom marcarmor13 pabrodmac migtermor josgarsan serrodcal pablucoto fracorjim1 bowma paupeddeg *)
lemma ejercicio_2:
assumes "(∃x. I(x)) ∧ (∃x. T(x))"
shows "∃x. (I(x) ∧ T(x))"
quickcheck
oops
(* Encontrando el contraejemplo:
I = {a1}
x = a1
T = {a2}
xa = a2
*)
text {* ---------------------------------------------------------------
Ejercicio 3. Formalizar, y decidir la corrección, del siguiente
argumento
Los hermanos tienen el mismo padre. Juan es hermano de Luis. Carlos
es padre de Luis. Por tanto, Carlos es padre de Juan.
Usar H(x,y) para x es hermano de y
P(x,y) para x es padre de y
j para Juan
l para Luis
c para Carlos
------------------------------------------------------------------ *}
(* ivamenjim crigomgom serrodcal*)
lemma ejercicio_3:
assumes 1: "∀x y. P(x,y) ⟶ (∀z. (H(z,y) ⟶ P(x,z)))"
assumes 2: "H(j,l)"
assumes 3: "P(c,l)"
shows "P(c,j)"
proof -
have 4 : "∀y. P(c,y) ⟶ (∀z. (H(z,y) ⟶ P(c,z)))" using 1 by (rule allE)
have 5 : "P(c,l) ⟶ (∀z. (H(z,l) ⟶ P(c,z)))" using 4 by (rule allE)
then have 6 : "(∀z. (H(z,l) ⟶ P(c,z)))" using 3 by (rule mp)
have 7 : "H(j,l) ⟶ P(c,j)" using 6 by (rule allE)
then show "P(c,j)" using 2 by (rule mp)
qed
(* danrodcha anaprarod ferrenseg marcarmor13 pablucoto fracorjim1 *)
(* es casi igual que la anterior *)
lemma ej_3:
assumes "∀x y. P(x,y) ⟶ (∀z. (H(z,y) ⟶ P(x,z)))"
assumes "H(j,l)"
assumes "P(c,l)"
shows "P(c,j)"
proof (rule mp)
have 4 : "∀y. P(c,y) ⟶ (∀z. (H(z,y) ⟶ P(c,z)))" using assms(1) by (rule allE)
hence "P(c,l) ⟶ (∀z. (H(z,l) ⟶ P(c,z)))" by (rule allE)
hence "(∀z. (H(z,l) ⟶ P(c,z)))" using assms(3) by (rule mp)
thus "H(j,l) ⟶ P(c,j)" by (rule allE)
next
show "H(j,l)" using assms(2) by this
qed
(*pabrodmac*)
lemma ejercicio_3_1:
assumes "∀x y. H(x,y) ⟶ (∀ z. (P(z,y) ⟶ P(z,x)))"
"H(j,l)"
"P(c,l)"
shows "P(c,j)"
proof-
have "∀y. H(j,y) ⟶ (∀ z. (P(z,y) ⟶ P(z,j)))" using assms(1) by (rule allE)
hence "H(j,l) ⟶ (∀ z. (P(z,l) ⟶ P(z,j)))" by (rule allE)
hence "∀z. (P(z,l) ⟶ P(z,j))" using assms(2) by (rule mp)
hence "P(c,l) ⟶ P(c,j)" by (rule allE)
thus "P(c,j)" using assms(3) by (rule mp)
qed
(* migtermor josgarsan*)
lemma ejercicio_3_2:
assumes "∀x y z. (P(x,y) ∧ H(y,z)) ⟶ P(x,z)"
assumes "H(l,j)"
assumes "P(c,l)"
shows "P(c,j)"
proof -
have 1: "P(c,l) ∧ H(l,j)" using assms(3) assms(2) by (rule conjI)
have 2: "∀y z. (P(c,y) ∧ H(y,z)) ⟶ P(c,z)" using assms(1) by (rule allE)
then have 3: "∀z. (P(c,l) ∧ H(l,z)) ⟶ P(c,z)" by (rule allE)
then have 4: "(P(c,l) ∧ H(l,j)) ⟶ P(c,j)" by (rule allE)
then show "P(c,j)" using 1 by (rule mp)
qed
(* paupeddeg *)
lemma ejercicio_3_3:
assumes "∀x y. P(x,y) ⟶ (∀z. (H(z,y) ⟶ P(x,z)))"
"H(j,l)"
"P(c,l)"
shows "P(c,j)"
proof-
have "∀ y. P(c,y) ⟶ (∀z. (H(z,y) ⟶ P(c,z)))" using assms(1) by (rule allE)
hence "P(c,l) ⟶ (∀z. (H(z,l) ⟶ P(c,z)))" by (rule allE)
have "∀z. (H(z,l) ⟶ P(c,z))" using `P(c,l) ⟶ (∀z. (H(z,l) ⟶ P(c,z)))` `P(c,l)`
by (rule mp)
hence "H(j,l) ⟶ P(c,j)" by (rule allE)
show "P(c,j)" using `H(j,l) ⟶ P(c,j)` `H(j,l)` by (rule mp)
qed
text {* ---------------------------------------------------------------
Ejercicio 4. Formalizar, y decidir la corrección, del siguiente
argumento
Los aficionados al fútbol aplauden a cualquier futbolista
extranjero. Juanito no aplaude a futbolistas extranjeros. Por
tanto, si hay algún futbolista extranjero nacionalizado español,
Juanito no es aficionado al fútbol.
Usar Af(x) para x es aficicionado al fútbol
Ap(x,y) para x aplaude a y
E(x) para x es un futbolista extranjero
N(x) para x es un futbolista nacionalizado español
j para Juanito
------------------------------------------------------------------ *}
(* danrodcha ferrenseg pablucoto*)
(* danrodcha: Me gusta más la formalización de ana prado, aunque
son equivalentes *)
lemma ej_4:
assumes "∀x y. Af(x) ∧ E(y) ⟶ Ap(x,y)"
"∀x. Ap(j,x) ⟶ ¬ E(x)"
shows "(∃x. E(x) ∧ N(x)) ⟶ ¬Af(j)"
proof (rule impI)
assume "∃x. E(x) ∧ N(x)"
then obtain a where "E(a) ∧ N(a)" by (rule exE)
hence "E(a)" by (rule conjE)
show "¬ Af(j)"
proof (rule notI)
assume "Af(j)"
hence "Af(j) ∧ E(a)" using `E(a)` by (rule conjI)
have "∀y. Af(j) ∧ E(y) ⟶ Ap(j,y)" using assms(1) by (rule allE)
hence "Af(j) ∧ E(a) ⟶ Ap(j,a)" by (rule allE)
hence "Ap(j,a)" using `Af(j) ∧ E(a)` by (rule mp)
have "Ap(j,a) ⟶ ¬ E(a)" using assms(2) by (rule allE)
hence "¬ E(a)" using `Ap(j,a)` by (rule mp)
thus False using `E(a)` by (rule notE)
qed
qed
(* ivamenjim crigomgom marcarmor13 serrodcal bowma *)
lemma ejercicio_4:
assumes 1: "∀x y. Af(x) ∧ E(y) ⟶ Ap(x,y)"
assumes 2: "¬(∃x. E(x) ∧ Ap(j,x))"
shows "(∃x. E(x) ∧ N(x)) ⟶ ¬Af(j)"
proof (rule impI)
assume 3: "∃x. E(x) ∧ N(x)"
then obtain a where 4: "E(a) ∧ N(a)" by (rule exE)
then have 5: "E(a)" by (rule conjunct1)
show 6: "¬Af(j)"
proof (rule notI)
assume 7: "Af(j)"
then have 8: "Af(j) ∧ E(a)" using 5 by (rule conjI)
have 9: "∀y. Af(j) ∧ E(y) ⟶ Ap(j,y)" using 1 by (rule allE)
have 10: "Af(j) ∧ E(a) ⟶ Ap(j,a)" using 9 by (rule allE)
have 11: "Ap(j,a)" using 10 8 by (rule mp)
have 12: "E(a) ∧ Ap(j,a)" using 5 11 by (rule conjI)
have 13: "∃x. E(x) ∧ Ap(j,x)" using 12 by (rule exI)
show "False" using 2 13 by (rule notE)
qed
qed
(* anaprarod migtermor *)
(* Este auxiliar ya se probó en el ejercicio 4 de la rel 8 *)
lemma aux4: "¬(p∧q) ⟹¬p ∨ ¬q"
by (auto)
lemma ej_4:
assumes "∀x y. Af(x) ∧ E(y) ⟶ Ap(x,y)"
"∀ x.(E(x) ⟶ ¬ Ap(j,x))"
shows "(∃x. E(x) ∧ N(x)) ⟶ ¬Af(j)"
proof (rule impI)
{ assume "∃x. E(x) ∧ N(x)"
then obtain a where 1: "E(a) ∧ N(a)" by (rule exE)
have "∀ y. Af(j) ∧ E(y) ⟶ Ap(j,y)" using assms(1) by (rule allE)
hence 2: "Af(j) ∧ E(a) ⟶ Ap(j,a)" by (rule allE)
have 3: "E(a)" using 1 by (rule conjunct1)
have 4: "E(a) ⟶ ¬ Ap(j,a)" using assms(2) by (rule allE)
have 5: "¬ Ap(j,a)" using 4 3 by (rule mp)
have "¬(Af(j) ∧ E(a))" using 2 5 by (rule mt)
hence "¬ Af(j) ∨ ¬ E(a)" by (rule aux4)
thus " ¬Af(j)"
proof (rule disjE)
{assume "¬Af(j)"
thus "¬Af(j)" by this}
next
{assume 6: "¬ E(a)"
show "¬ Af(j)" using 6 3 by (rule notE)}
qed}
qed
(*pabrodmac*)
lemma ejercicio_4_1:
assumes "∀x y. Af(x) ∧ E(y) ⟶ Ap(x,y)"
"∀x. E(x)⟶ ¬Ap(j,x)"
shows "(∃x. N(x) ∧ E(x)) ⟶ ¬Af(j)"
proof
assume "∃x. N(x) ∧ E(x)"
then obtain b where "N(b) ∧ E(b)" by (rule exE)
hence "E(b)" by (rule conjunct2)
have "E(b)⟶ ¬Ap(j,b)" using assms(2) by (rule allE)
hence "¬Ap(j,b)" using `E(b)` by (rule mp)
have "∀y. Af(j) ∧ E(y) ⟶ Ap(j,y)" using assms(1) by (rule allE)
hence "Af(j) ∧ E(b) ⟶ Ap(j,b)" by (rule allE)
hence "¬Ap(j,b) ⟶ ¬(Af(j) ∧ E(b))" by (rule Set.not_mono)
hence "¬(Af(j) ∧ E(b))" using `¬Ap(j,b)` by (rule mp)
show "¬Af(j)"
proof
assume "Af(j)"
hence "Af(j) ∧ E(b)" using `E(b)` by (rule conjI)
show False using `¬(Af(j) ∧ E(b))` `Af(j) ∧ E(b)` by (rule notE)
qed
qed
(* paupeddeg *)
lemma ejercicio_4_2:
assumes "∀x y. Af(x)∧E(y) ⟶ Ap(x,y) "
"∀x. E(x) ⟶ ¬Ap(j,x)"
shows "(∃x. E(x)∧N(x)) ⟶ ¬Af(j) "
proof
assume "∃x. E(x)∧N(x)"
then obtain b where "E(b) ∧ N(b)" by (rule exE)
hence "E(b)" by (rule conjunct1)
have "E(b) ⟶¬Ap(j,b)" using assms(2) by (rule allE)
have "¬Ap(j,b)" using `E(b) ⟶¬Ap(j,b)` `E(b)` by (rule mp)
have "∀ y. Af(j)∧E(y) ⟶ Ap(j,y)" using assms(1) by (rule allE)
hence "Af(j)∧E(b) ⟶ Ap(j,b)" by (rule allE)
have "¬ (Af(j)∧E(b))" using `Af(j)∧E(b) ⟶ Ap(j,b)` `¬ Ap(j,b)` by (rule mt)
show "¬Af(j)"
proof
assume "Af(j)"
hence "Af(j)∧E(b)" using `E(b)` by (rule conjI)
show False using `¬ (Af(j)∧E(b))` `(Af(j)∧E(b))` by (rule notE)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 5. Formalizar, y decidir la corrección, del siguiente
argumento
El esposo de la hermana de Toni es Roberto. La hermana de Toni es
María. Por tanto, el esposo de María es Roberto.
Usar e(x) para el esposo de x
h para la hermana de Toni
m para María
r para Roberto
------------------------------------------------------------------ *}
(* ivamenjim *)
lemma ejercicio_5:
assumes 1: "e(h) = r"
assumes 2: "h = m"
shows "e(m) = r"
proof -
have 3: "e(h) = e(m)" using 2 by (rule arg_cong)
have 4: "e(m) = e(h)" using 3 by (rule sym)
then show "e(m) = r" using 1 by (rule trans)
qed
(* danrodcha anaprarod crigomgom ferrenseg marcarmor13 migtermor serrodcal pablucoto paupeddeg*)
lemma ej_5:
assumes "e(h) = r" and
"h = m"
shows "e(m) = r"
proof -
show "e(m) = r" using assms(2) assms(1) by (rule subst)
qed
(*pabrodmac*)
lemma ejercicio_5_1:
assumes "e(h)=r"
"h=m"
shows "e(m)=r"
proof-
show "e(m)=r" using assms(1) assms(2) by (rule HOL.back_subst)
qed
(*pabrodmac*)
lemma ejercicio_5_2:
assumes "e(h)=r"
"h=m"
shows "e(m)=r"
proof-
show "e(m)=r" using assms(2) assms(1) by (rule HOL.subst)
qed
(*pabrodmac*)
lemma ejercicio_5_3:
assumes "e(h)=r"
"h=m"
shows "e(m)=r"
proof-
have "e(h) = e(m)" using assms(2) by (rule arg_cong)
show "e(m)=r" using `e(h)=r` `e(h) = e(m)` by simp
qed
end