chapter {* R7: Deducción natural proposicional en Isabelle/HOL *}
theory R7_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
(* edupalhid *)
lemma notnotE: "¬¬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
------------------------------------------------------------------ *}
(*anddonram*)
lemma ej_1:
assumes 1: "¬q ⟶ ¬p"
shows "p ⟶ q"
proof (rule impI)
assume 2: "p"
show 3: "q"
proof (rule ccontr)
assume 4: "¬q"
have 5: "¬p" using 1 4 by (rule impE)
then show False using 2 by (rule notE)
qed
qed
(*luicedval cesgongut oscgonesc diwu2 rafcabgon jescudero rafferrod macmerflo davperriv jospermon1*)
lemma ej_1_2:
assumes 1: "¬q ⟶ ¬p"
shows "p ⟶ q"
proof -
{ assume 2: "p"
have 3: "¬¬p" using 2 by (rule notnotI)
have 4: "¬¬q" using 1 3 by (rule mt)
have 5: "q" using 4 by (rule notnotD) }
thus "p ⟶ q" by (rule impI)
qed
(* edupalhid*)
lemma ej_1_3:
assumes "¬q⟶¬p"
shows "p⟶q"
proof(rule impI)
assume 1:"p"
show "q"
proof-
have 2:"¬¬p" using 1 by (rule notnotI)
have "¬¬q" using assms(1) 2 by (rule mt)
then show "q" by (rule notnotE)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
¬(¬p ∧ ¬q) ⊢ p ∨ q
------------------------------------------------------------------ *}
(*anddonram luicedval oscgonesc diwu2 rafcabgon jescudero davperriv macmerflo jospermon1*)
lemma l_e_m:
"F ∨ ¬F"
by auto
lemma ej_2:
assumes 1:"¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof (rule disjE)
{
assume 2: "q"
show "p ∨ q" using 2 by (rule disjI2)
}
moreover{
assume 4:"¬q"
show "p ∨ q"
proof(rule disjI1)
show "p"
proof (rule ccontr)
assume 5:"¬p"
then have "¬p ∧ ¬q" using 4 by (rule conjI)
with 1 show False by (rule notE)
qed
qed
}
moreover
show 1: "q ∨ ¬q" by (rule l_e_m)
qed
(* cesgongut *)
lemma conjnotDM1:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof (rule ccontr)
assume "¬(p ∨ q)"
have "p"
proof (rule ccontr)
assume "¬p"
have "q"
proof (rule ccontr)
assume "¬q"
have "¬p ∧ ¬q" using `¬p` `¬q` ..
then show False using assms by contradiction
qed
then have "p ∨ q" by (rule disjI2)
then show False using `¬(p ∨ q)` by contradiction
qed
then have "p ∨ q" by (rule disjI1)
then show False using `¬(p ∨ q)` by contradiction
qed
(* edupalhid *)
lemma ej_2_2:
assumes 1:"¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof (cases)
assume "p"
then show "p ∨ q" by (rule disjI1)
next
assume "¬p"
then have "q" using 1 by simp
then show "p ∨ q" by (rule disjI2)
qed
text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
¬(¬p ∨ ¬q) ⊢ p ∧ q
------------------------------------------------------------------ *}
(*anddonram luicedval cesgongut oscgonesc diwu2 rafcabgon jescudero rafferrod macmerflo davperriv jospermon1*)
lemma ej_3:
assumes 1:" ¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof (rule conjI)
show "p"
proof (rule ccontr)
assume "¬p"
then have "(¬p ∨ ¬q)" by (rule disjI1)
with 1 show False by (rule notE)
qed
next
show "q"
proof (rule ccontr)
assume "¬q"
then have "(¬p ∨ ¬q)" by (rule disjI2)
with 1 show False by (rule notE)
qed
qed
(* edupalhid *)
lemma ej_3_2:
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
------------------------------------------------------------------ *}
(*anddonram luicedval rafcabgon jescudero rafferrod davperriv macmerflo jospermon1*)
lemma ej_4:
assumes 1: "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof(rule disjE)
{
assume 2:"p"
show "¬p ∨ ¬q"
proof (rule disjI2)
show "¬q"
proof (rule notI)
assume "q"
with 2 have "p∧q" by (rule conjI)
with 1 show False by (rule notE)
qed
qed
}
moreover
{
assume "¬p"
then show "¬p ∨ ¬q" by (rule disjI1)
}
moreover
show 1: "p ∨ ¬p" by (rule l_e_m)
qed
(* cesgongut oscgonesc diwu2 edupalhid*)
lemma conjDM1:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof (rule ccontr)
assume "¬(¬p ∨ ¬q)"
then have "p ∧ q" by (rule ej_3)
with assms show False by (rule notE)
qed
text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
⊢ (p ⟶ q) ∨ (q ⟶ p)
------------------------------------------------------------------ *}
(*anddonram luicedval oscgonesc diwu2 rafcabgon rafferrod macmerflo davperriv jospermon1*)
lemma ej_5:
shows "(p ⟶ q) ∨ (q ⟶ p)"
proof (rule disjE)
{
assume 2: "q"
show "(p ⟶ q) ∨ (q ⟶ p)"
proof(rule disjI1)
show "p ⟶ q" using 2 by (rule impI)
qed
}
moreover{
assume 4:" ¬q"
show "(p ⟶ q) ∨ (q ⟶ p)"
proof(rule disjI2)
show "q ⟶ p"
proof (rule impI)
assume 5:"q"
with 4 show "p" by (rule notE)
qed
qed
}
moreover
show 1: "q ∨ ¬q" by (rule l_e_m)
qed
(* cesgongut *)
lemma disjDM1:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof
show "¬p" proof (rule notI)
assume "p"
then have "p ∨ q" ..
then show False using assms by contradiction
qed
show "¬q" proof (rule notI)
assume "q"
then have "p ∨ q" ..
then show False using assms by contradiction
qed
qed
lemma notimpD1:
assumes "¬(p ⟶ q)"
shows "p ∧ ¬q"
proof
show "¬q" proof (rule notI)
assume "q"
have "p ⟶ q" proof (rule impI)
assume "p"
show "q" proof (rule ccontr)
assume "¬q"
then show False using `q` by contradiction
qed
qed
then show False using assms by contradiction
qed
next
show "p" proof (rule ccontr)
assume "¬p"
have "p ⟶ q" proof (rule impI)
assume "p"
show "q" proof (rule ccontr)
assume "¬q"
show False using `p` `¬p` by contradiction
qed
qed
then show False using assms by contradiction
qed
qed
lemma ej5b: "(p ⟶ q) ∨ (q ⟶ p)"
proof (rule ccontr)
assume "¬?thesis"
then have "¬(p ⟶ q) ∧ ¬(q ⟶ p)" by (rule disjDM1)
then have "¬(p ⟶ q)" ..
then have "p ∧ ¬q" by (rule notimpD1)
then have "p" ..
have "¬(q ⟶ p)" using `¬(p ⟶ q) ∧ ¬(q ⟶ p)` ..
then have "q ∧ ¬p" by (rule notimpD1)
then have "¬p" ..
then show False using `p` by contradiction
qed
(*edupalhid*)
lemma ej_5c:
shows "(p ⟶ q) ∨ (q ⟶ p)"
proof(cases)
assume "(p ⟶ q)"
then show "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI1)
next
assume "¬ (p ⟶ q)"
then have 1:"¬(¬p∨q)" using equiv by simp
have "p∧¬q" using 1 by auto
then have "q ⟶ p" by auto
then show "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI2)
qed
end
