Relación 8
De Razonamiento automático (2016-17)
Revisión del 13:39 16 ene 2017 de Danrodcha (discusión | contribuciones)
chapter {* R8: Deducción natural proposicional en Isabelle/HOL *}
theory R8_Deduccion_natural_proposicional
imports Main
begin
text {*
Demostrar o refutar los siguientes lemas usando sólo 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
· 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 y not_ex 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
text {* ---------------------------------------------------------------
Ejercicio 1. Demostrar
¬q ⟶ ¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}
(* marcarmor13 jeamacpov *)
--"usando un supuesto ¬¬p"
lemma ejercicio_1:
assumes 1: "¬q ⟶ ¬p" and
2: "¬¬p"
shows "p ⟶ q"
proof -
have 3: "¬¬q" using 1 2 by (rule mt)
have 4: "q" using 3 by (rule notnotD)
show "p ⟶ q" using 4 by (rule impI)
qed
(*pablucoto*)
lemma ejercicio_1_2:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof -
{assume "p"
hence "¬¬p" by (rule notnotI)
with `¬q ⟶ ¬p` have "¬¬q" by (rule mt)
hence "q" by (rule notnotD)}
then show "p ⟶ q" by (rule impI)
qed
(* ivamenjim *)
lemma ejercicio_1_3:
assumes 1: "¬q ⟶ ¬p"
shows "p ⟶ q"
proof -
{assume 2:"p"
then have 3: "¬¬p" by (rule notnotI)
have 4: "¬¬q" using 1 3 by (rule mt)
then have 5: "q" by (rule notnotD)}
thus "p ⟶ q" by (rule impI)
qed
(* bowma *)
lemma ejercicio_1_4:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof -
{assume "p"
hence "¬¬p" by (rule notnotI)
with assms have "¬¬q" by (rule mt)
then have "q" by (rule notnotD)}
thus "p ⟶ q" by (rule impI)
qed
（* bowma danrodcha *)
"quita la limitación de -"
lemma ejercicio_1_5:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof
assume "p"
hence "¬¬p" by (rule notnotI)
with assms have "¬¬q" by (rule mt)
thus "q" by (rule notnotD)
qed
text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
¬(¬p ∧ ¬q) ⊢ p ∨ q
------------------------------------------------------------------ *}
(* marcarmor13 jeamacpov *)
--"usando un supuesto ¬p ∧ ¬q"
lemma ejercicio_2:
assumes 1: "¬(¬p ∧ ¬q)" and
2:"¬p ∧ ¬q"
shows "p ∨ q"
proof-
have 3: "p"using 1 2 by (rule notE)
show "p ∨ q" using 3 by (rule disjI1)
qed
(* ivamenjim *)
lemma ejercicio_2_2:
assumes 1: "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof -
{assume 2:"(¬p ∧ ¬q)"
have "p" using 1 2 by (rule notE)
then have "p ∨ q" by (rule disjI1)}
thus "p ∨ q" by auto
qed
(* pablucoto *)
lemma aux_ejercicio2:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof
{assume "p"
hence "p ∨ q" by (rule disjI1)
with `¬(p ∨ q)` have "False" by (rule notE)}
then show "¬p" ..
next
{assume "q"
hence "p ∨ q" by (rule disjI2)
with `¬(p ∨ q)` have "False" by (rule notE)}
then show "¬q" ..
qed
lemma ejercicio_2_3:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof -
{assume 2:"¬(p ∨ q)"
hence "¬p ∧ ¬q" by (rule aux_ejercicio2)
with `¬(¬p ∧ ¬q)` have "False" ..}
then show "p ∨ q" by (rule ccontr)
qed
(* danrodcha *)
lemma ej_2:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof -
have "¬p ∨ p" by (rule excluded_middle)
thus "p ∨ q"
proof (rule disjE)
{ assume "¬p"
have "¬q ∨ q" by (rule excluded_middle)
thus "p ∨ q"
proof (rule disjE)
{ assume "¬q"
with `¬p` have "¬p ∧ ¬q" by (rule conjI)
with assms show "p ∨ q" by (rule notE)}
next
{ assume "q"
then show "p ∨ q" by (rule disjI2)}
qed}
next
{ assume "p"
thus "p ∨ q" by (rule disjI1)}
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
¬(¬p ∨ ¬q) ⊢ p ∧ q
------------------------------------------------------------------ *}
(* marcarmor13 jeamacpov *)
--"usando un supuesto ¬p ∨ ¬q"
lemma ejercicio_3:
assumes 1: "¬(¬p ∨ ¬q)" and
2:"¬p ∨ ¬q"
shows "p ∧ q"
proof-
have 3: "p"using 1 2 by (rule notE)
have 4: "q"using 1 2 by (rule notE)
show "p ∧ q" using 3 4 by (rule conjI)
qed
(* pablucoto *)
lemma ejercicio_3_2:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof
have "¬¬p ∧ ¬¬q" using assms(1) by (rule aux_ejercicio2)
hence "¬¬p" by (rule conjunct1)
show "p" using `¬¬p` by (rule notnotD)
next
have "¬¬p ∧ ¬¬q" using assms(1) by (rule aux_ejercicio2)
have "¬¬q" using `¬¬p ∧ ¬¬q` by (rule conjunct2)
show "q" using `¬¬q` by (rule notnotD)
qed
(* ivamenjim *)
lemma aux: "¬(p ∨ q) ⟹ ¬p ∧ ¬q"
by auto
lemma ejercicio_3_3:
assumes 1: "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof
have 2: "¬¬p ∧ ¬¬q" using 1 by (rule aux)
have 3: "¬¬p" using 2 ..
have 4: "¬¬q" using 2 ..
show "p" using 3 by (rule notnotD)
show "q" using 4 by (rule notnotD)
qed
(* danrodcha *)
lemma ej_3:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof (rule conjI)
{ assume "¬p"
hence "¬p ∨ ¬q" by (rule disjI1)
with assms have False by (rule notE)}
then show "p" by (rule ccontr)
{ assume "¬q"
hence "¬p ∨ ¬q" by (rule disjI2)
with assms have False by (rule notE)}
then show "q" by (rule ccontr)
qed
text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
¬(p ∧ q) ⊢ ¬p ∨ ¬q
------------------------------------------------------------------ *}
(* marcarmor13 jeamacpov *)
--"usando un supuesto p ∧ q"
lemma ejercicio_4:
assumes 1: " ¬(p ∧ q)" and
2:"p ∧ q"
shows "¬p ∨ ¬q"
proof-
have 3: "¬p"using 1 2 by (rule notE)
show "¬p ∨ ¬q" using 3 by (rule disjI1)
qed
(* ivamenjim *)
lemma ejercicio_4:
assumes 1: "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof -
{assume 2:"(p ∧ q)"
have "¬p" using 1 2 by (rule notE)
then have "¬p ∨ ¬q" by (rule disjI1)}
thus "¬p ∨ ¬q" by auto
qed
( * pablucoto *)
lemma ejercicio_4:
assumes " ¬(p ∧ q)"
shows " ¬p ∨ ¬q"
proof -
{ assume 2: "¬(¬p ∨ ¬q)"
hence "p ∧ q" by (rule ejercicio_3_2)
with assms(1) have "False" .. }
then show " ¬p ∨ ¬q" by (rule ccontr)
qed
(*danrodcha *)
lemma ej_4:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof (rule ccontr)
assume "¬ (¬ p ∨ ¬ q)"
hence "p ∧ q" by (rule ej_3)
with assms show False by (rule notE)
qed
text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
⊢ (p ⟶ q) ∨ (q ⟶ p)
------------------------------------------------------------------ *}
(* marcarmor13 jeamacpov *)
--"usando un supuesto q"
lemma ejercicio_5:
assumes 1: "q"
shows "(p ⟶ q) ∨ (q ⟶ p)"
proof-
have 2: "p ⟶ q" using 1 by (rule impI)
show "(p ⟶ q) ∨ (q ⟶ p)" using 2 by (rule disjI1)
qed
(* ivamenjim *)
lemma ejercicio_5:
shows "(p ⟶ q) ∨ (q ⟶ p)"
proof -
{assume 1:"q"
have "(p ⟶ q)" using 1 by (rule impI)
then have "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI1)}
thus "(p ⟶ q) ∨ (q ⟶ p)" by auto
qed
(* danrodcha *)
lemma ej_5:
shows "(p ⟶ q) ∨ (q ⟶ p)"
proof -
have "¬p ∨ p" by (rule excluded_middle)
thus "(p ⟶ q) ∨ (q ⟶ p)"
proof (rule disjE)
{ assume "¬p"
have "¬q ∨ q" by (rule excluded_middle)
thus "(p ⟶ q) ∨ (q ⟶ p)"
proof (rule disjE)
{assume "¬q"
hence "¬p ⟶ ¬q" by (rule impI)
{ assume "q"
hence "¬¬q" by (rule notnotI)
with `¬p ⟶ ¬q` have "¬¬p" by (rule mt)
hence "p" by (rule notnotD)}
hence "q ⟶ p" by (rule impI)
thus "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI2)}
next
{assume "q"
hence "(p ⟶ q)" by (rule impI)
thus "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI1)}
qed}
next
{assume "p"
hence "q ⟶ p" by (rule impI)
thus "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI2)}
qed
qed
end