Diferencia entre revisiones de «GLC T1R1»
De DAO (Demostración asistida por ordenador)
(Página creada con '<source lang="isar"> header {* T1R1: Deducción natural proposicional *} theory T1R1 imports Main begin text {* ------------------------------------------------------------...') |
m (Texto reemplazado: «"isar"» por «"isabelle"») |
||
| Línea 1: | Línea 1: | ||
| − | <source lang=" | + | <source lang="isabelle"> |
header {* T1R1: Deducción natural proposicional *} | header {* T1R1: Deducción natural proposicional *} | ||
Revisión actual del 14:01 15 jul 2018
header {* T1R1: Deducción natural proposicional *}
theory T1R1
imports Main
begin
text {*
---------------------------------------------------------------------
El objetivo de esta relación es lemas usando sólo las reglas básicas
de deducción natural de la lógica proposicional.
Los ejercicios son los de la asignatura de "Lógica informática" que se
encuentran en http://goo.gl/yrPLn
Las reglas básicas de la deducción natural son las siguientes:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
· notnotI: P ⟹ ¬¬ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· 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
---------------------------------------------------------------------
*}
text {*
Se usarán las reglas notnotI y mt que demostramos a continuación.
*}
lemma notnotI: "P ⟹ ¬¬ P"
by auto
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto
section {* Implicaciones *}
text {* ---------------------------------------------------------------
Ejercicio 1. Demostrar
p ⟶ q, p ⊢ q
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_1_1:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
show "q" using 1 2 by (rule mp)
qed
-- "La demostración estructurada es"
lemma ejercicio_1_2:
assumes "p ⟶ q"
"p"
shows "q"
proof -
show "q" using assms ..
qed
-- "La demostración automática es"
lemma ejercicio_1_3:
assumes "p ⟶ q"
"p"
shows "q"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
p ⟶ q, q ⟶ r, p ⊢ r
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_2_1:
assumes 1: "p ⟶ q" and
2: "q ⟶ r" and
3: "p"
shows "r"
proof -
have 4: "q" using 1 3 by (rule mp)
show "r" using 2 4 by (rule mp)
qed
-- "La demostración estructurada es"
lemma ejercicio_2_2:
assumes "p ⟶ q"
"q ⟶ r"
"p"
shows "r"
proof -
have "q" using assms(1,3) ..
show "r" using assms(2) `q` ..
qed
-- "La demostración automática es"
lemma ejercicio_2_3:
assumes "p ⟶ q"
"q ⟶ r"
"p"
shows "r"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_3_1:
assumes 1: "p ⟶ (q ⟶ r)" and
2: "p ⟶ q" and
3: "p"
shows "r"
proof -
have 4: "q" using 2 3 by (rule mp)
have 5: "q ⟶ r" using 1 3 by (rule mp)
show "r" using 5 4 by (rule mp)
qed
-- "La demostración estructurada es"
lemma ejercicio_3_2:
assumes "p ⟶ (q ⟶ r)"
"p ⟶ q"
"p"
shows "r"
proof -
have "q" using assms(2,3) ..
have "q ⟶ r" using assms(1,3) ..
thus "r" using `q` ..
qed
-- "La demostración automática es"
lemma ejercicio_3_3:
assumes "p ⟶ (q ⟶ r)"
"p ⟶ q"
"p"
shows "r"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
p ⟶ q, q ⟶ r ⊢ p ⟶ r
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_4_1:
assumes 1: "p ⟶ q" and
2: "q ⟶ r"
shows "p ⟶ r"
proof (rule impI)
assume 3: "p"
have 4: "q" using 1 3 by (rule mp)
show "r" using 2 4 by (rule mp)
qed
-- "La demostración estructurada es"
lemma ejercicio_4_2:
assumes "p ⟶ q"
"q ⟶ r"
shows "p ⟶ r"
proof
assume "p"
with assms(1) have "q" ..
with assms(2) show "r" ..
qed
-- "La demostración automática es"
lemma ejercicio_4_3:
assumes "p ⟶ q"
"q ⟶ r"
shows "p ⟶ r"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_5_1:
assumes 1: "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
proof (rule impI)
assume 2: "q"
show "p ⟶ r"
proof (rule impI)
assume 3: "p"
have "q ⟶ r" using 1 3 by (rule mp)
thus "r" using 2 by (rule mp)
qed
qed
-- "La demostración estructurada es"
lemma ejercicio_5_2:
assumes "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
proof
assume "q"
show "p ⟶ r"
proof
assume "p"
with assms(1) have "q ⟶ r" ..
thus "r" using `q` ..
qed
qed
-- "La demostración automática es"
lemma ejercicio_5_3:
assumes "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_6_1:
assumes 1: "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
proof (rule impI)
assume 2: "p ⟶ q"
show "p ⟶ r"
proof (rule impI)
assume 3: "p"
have 4: "q" using 2 3 by (rule mp)
have 5: "q ⟶ r" using 1 3 by (rule mp)
show "r" using 5 4 by (rule mp)
qed
qed
-- "La demostración estructurada es"
lemma ejercicio_6_2:
assumes "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
proof
assume "p ⟶ q"
show "p ⟶ r"
proof
assume "p"
with `p ⟶ q` have "q" ..
have "q ⟶ r" using assms(1) `p` ..
thus "r" using `q` ..
qed
qed
-- "La demostración automática es"
lemma ejercicio_6_3:
assumes "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
p ⊢ q ⟶ p
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_7_1:
assumes 1: "p"
shows "q ⟶ p"
proof (rule impI)
assume 2: "q"
show "p" using 1 by this
qed
-- "La demostración estructurada es"
lemma ejercicio_7_2:
assumes "p"
shows "q ⟶ p"
proof
assume "q"
show "p" using assms(1) .
qed
-- "La demostración automática es"
lemma ejercicio_7_3:
assumes "p"
shows "q ⟶ p"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
⊢ p ⟶ (q ⟶ p)
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_8_1:
"p ⟶ (q ⟶ p)"
proof (rule impI)
assume 1: "p"
show "q ⟶ p"
proof (rule impI)
assume 2: "q"
show "p" using 1 by this
qed
qed
-- "La demostración estructurada es"
lemma ejercicio_8_2:
"p ⟶ (q ⟶ p)"
proof
assume "p"
show "q ⟶ p"
proof
assume "q"
show "p" using `p` .
qed
qed
-- "La demostración automática es"
lemma ejercicio_8_3:
"p ⟶ (q ⟶ p)"
by auto
text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_9_1:
assumes 1: "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"
proof (rule impI)
assume 2: "q ⟶ r"
show "p ⟶ r"
proof (rule impI)
assume 3: "p"
have 4: "q" using 1 3 by (rule mp)
show "r" using 2 4 by (rule mp)
qed
qed
-- "La demostración estructurada es"
lemma ejercicio_9_2:
assumes "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"
proof
assume "q ⟶ r"
show "p ⟶ r"
proof
assume "p"
with assms(1) have "q" ..
with `q ⟶ r` show "r" ..
qed
qed
-- "La demostración automática es"
lemma ejercicio_9_3:
assumes "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_10_1:
assumes 1: "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
proof -
{ assume 2: "r"
{ assume 3: "q"
{ assume 4: "p"
have 5: "q ⟶ (r ⟶ s)" using 1 4 by (rule mp)
have 6: "r ⟶ s" using 5 3 by (rule mp)
have 7: "s" using 6 2 by (rule mp) }
hence 8: "p ⟶ s" by (rule impI) }
hence 9: "q ⟶ (p ⟶ s)" by (rule impI) }
thus 10: "r ⟶ (q ⟶ (p ⟶ s))" by (rule impI)
qed
-- "Una variante de la demostración anterior es"
lemma ejercicio_10_1b:
assumes 1: "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
proof (rule impI)
assume 2: "r"
show "q ⟶ (p ⟶ s)"
proof (rule impI)
assume 3: "q"
show "p ⟶ s"
proof (rule impI)
assume 4: "p"
have 5: "q ⟶ (r ⟶ s)" using 1 4 by (rule mp)
have 6: "r ⟶ s" using 5 3 by (rule mp)
show "s" using 6 2 by (rule mp)
qed
qed
qed
-- "La demostración estructurada es"
lemma ejercicio_10_2:
assumes "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
proof
assume "r"
show "q ⟶ (p ⟶ s)"
proof
assume "q"
show "p ⟶ s"
proof
assume "p"
with assms(1) have "q ⟶ (r ⟶ s)" ..
hence "r ⟶ s" using `q` ..
thus "s" using `r` ..
qed
qed
qed
-- "La demostración automática es"
lemma ejercicio_10_3:
assumes "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 11. Demostrar
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_11_1:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof -
{ assume 1: "p ⟶ (q ⟶ r)"
{ assume 2: "p ⟶ q"
{ assume 3: "p"
have 4: "q" using 2 3 by (rule mp)
have 5: "q ⟶ r" using 1 3 by (rule mp)
have 6: "r" using 5 4 by (rule mp) }
hence 7: "p ⟶ r" by (rule impI) }
hence 8: "(p ⟶ q) ⟶ (p ⟶ r)" by (rule impI) }
thus "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))" by (rule impI)
qed
-- "La demostración estructurada es"
lemma ejercicio_11_2:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof
assume "p ⟶ (q ⟶ r)"
{ assume "p ⟶ q"
{ assume "p"
with `p ⟶ q` have "q" ..
have "q ⟶ r" using `p ⟶ (q ⟶ r)` `p` ..
hence "r" using `q` .. }
hence "p ⟶ r" .. }
thus "(p ⟶ q) ⟶ (p ⟶ r)" ..
qed
-- "La demostración automática es"
lemma ejercicio_11_3:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
by auto
text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_12_1:
assumes 1: "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof -
{ assume 2: "p"
{ assume 3: "q"
{ assume 4: "p"
have 5: "q" using 3 by this }
hence 6: "p ⟶ q" by (rule impI)
have 7: "r" using 1 6 by (rule mp) }
hence 8: "q ⟶ r" by (rule impI) }
thus 9: "p ⟶ (q ⟶ r)" by (rule impI)
qed
-- "La demostración estructurada es"
lemma ejercicio_12_2:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof
assume "p"
{ assume "q"
{ assume "p"
have "q" using `q` . }
hence "p ⟶ q" ..
with assms(1) have "r" .. }
thus "q ⟶ r" ..
qed
-- "La demostración automática es"
lemma ejercicio_12_3:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
using assms
by auto
section {* Conjunciones *}
text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar
p, q ⊢ p ∧ q
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_13_1:
assumes 1: "p" and
2: "q"
shows "p ∧ q"
proof -
show "p ∧ q" using assms by (rule conjI)
qed
-- "La demostración estructurada es"
lemma ejercicio_13_2:
assumes "p"
"q"
shows "p ∧ q"
proof
show "p" using assms(1) .
next
show "q" using assms(2) .
qed
-- "La demostración automática es"
lemma ejercicio_13_3:
assumes "p"
"q"
shows "p ∧ q"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 14. Demostrar
p ∧ q ⊢ p
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_14_1:
assumes 1: "p ∧ q"
shows "p"
proof -
show "p" using 1 by (rule conjunct1)
qed
-- "La demostración estructurada es"
lemma ejercicio_14_2:
assumes "p ∧ q"
shows "p"
proof -
show "p" using assms ..
qed
-- "La demostración automática es"
lemma ejercicio_14_3:
assumes "p ∧ q"
shows "p"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 15. Demostrar
p ∧ q ⊢ q
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_15_1:
assumes 1: "p ∧ q"
shows "q"
proof -
show "q" using 1 by (rule conjunct2)
qed
-- "La demostración estructurada es"
lemma ejercicio_15_2:
assumes "p ∧ q"
shows "q"
proof -
show "q" using assms ..
qed
-- "La demostración automática es"
lemma ejercicio_15_3:
assumes "p ∧ q"
shows "q"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_16_1:
assumes 1: "p ∧ (q ∧ r)"
shows "(p ∧ q) ∧ r"
proof -
have 2: "p" using 1 by (rule conjunct1)
have 3: "q ∧ r" using 1 by (rule conjunct2)
have 4: "q" using 3 by (rule conjunct1)
have 5: "p ∧ q" using 2 4 by (rule conjI)
have 6: "r" using 3 by (rule conjunct2)
show 7: "(p ∧ q) ∧ r" using 5 6 by (rule conjI)
qed
-- "La demostración estructurada es"
lemma ejercicio_16_2:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q) ∧ r"
proof
show "p ∧ q"
proof
show "p" using assms ..
next
have "q ∧ r" using assms ..
thus "q" ..
qed
next
have "q ∧ r" using assms ..
thus "r" ..
qed
-- "La demostración automática es"
lemma ejercicio_16_3:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q) ∧ r"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_17_1:
assumes 1: "(p ∧ q) ∧ r"
shows "p ∧ (q ∧ r)"
proof -
have 2: "p ∧ q" using 1 by (rule conjunct1)
have 3: "p" using 2 by (rule conjunct1)
have 4: "q" using 2 by (rule conjunct2)
have 5: "r" using 1 by (rule conjunct2)
have 6: "q ∧ r" using 4 5 by (rule conjI)
show 7: "p ∧ (q ∧ r)" using 3 6 by (rule conjI)
qed
-- "La demostración estructurada es"
lemma ejercicio_17_2:
assumes "(p ∧ q) ∧ r"
shows "p ∧ (q ∧ r)"
proof
have "p ∧ q" using assms ..
thus "p" ..
next
show "q ∧ r"
proof
have "p ∧ q" using assms ..
thus "q" ..
next
show "r" using assms ..
qed
qed
-- "La demostración automática es"
lemma ejercicio_17_3:
assumes "(p ∧ q) ∧ r"
shows "p ∧ (q ∧ r)"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar
p ∧ q ⊢ p ⟶ q
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_18_1:
assumes 1: "p ∧ q"
shows "p ⟶ q"
proof (rule impI)
assume 2: "p"
show "q" using 1 by (rule conjunct2)
qed
-- "La demostración estructurada es"
lemma ejercicio_18_2:
assumes "p ∧ q"
shows "p ⟶ q"
proof
assume "p"
show "q" using assms ..
qed
-- "La demostración automática es"
lemma ejercicio_18_3:
assumes "p ∧ q"
shows "p ⟶ q"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 19. Demostrar
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_19_1:
assumes 1: "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
proof (rule impI)
assume 2: "p"
have 3: "p ⟶ q" using 1 by (rule conjunct1)
have 4: "q" using 3 2 by (rule mp)
have 5: "p ⟶ r" using 1 by (rule conjunct2)
have 6: "r" using 5 2 by (rule mp)
show 7: "q ∧ r" using 4 6 by (rule conjI)
qed
-- "La demostración estructurada es"
lemma ejercicio_19_2:
assumes "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
proof
assume "p"
show "q ∧ r"
proof
have "p ⟶ q" using assms ..
thus "q" using `p` ..
next
have "p ⟶ r" using assms ..
thus "r" using `p` ..
qed
qed
-- "La demostración automática es"
lemma ejercicio_19_3:
assumes "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_20_1:
assumes 1: "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof (rule conjI)
show "p ⟶ q"
proof (rule impI)
assume 2: "p"
have "q ∧ r" using 1 2 by (rule mp)
thus "q" by (rule conjunct1)
qed
next
show "p ⟶ r"
proof (rule impI)
assume 3: "p"
have "q ∧ r" using 1 3 by (rule mp)
thus "r" by (rule conjunct2)
qed
qed
-- "La demostración estructurada es"
lemma ejercicio_20_2:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof
show "p ⟶ q"
proof
assume "p"
have "q ∧ r" using assms `p` ..
thus "q" ..
qed
next
show "p ⟶ r"
proof
assume "p"
have "q ∧ r" using assms `p` ..
thus "r" ..
qed
qed
-- "La demostración automática es"
lemma ejercicio_20_3:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_21_1:
assumes 1: "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
proof (rule impI)
assume 2: "p ∧ q"
have 3: "p" using 2 by (rule conjunct1)
have 4: "q" using 2 by (rule conjunct2)
have 5: "q ⟶ r" using 1 3 by (rule mp)
show 6: "r" using 5 4 by (rule mp)
qed
-- "La demostración estructurada es"
lemma ejercicio_21_2:
assumes "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
proof
assume "p ∧ q"
hence "p" ..
have "q" using `p ∧ q` ..
have "q ⟶ r" using assms(1) `p` ..
thus "r" using `q` ..
qed
-- "La demostración automática es"
lemma ejercicio_21_3:
assumes "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 22. Demostrar
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_22_1:
assumes 1: "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof (rule impI)
assume 2: "p"
{ assume 3: "q"
have 4: "p ∧ q" using 2 3 by (rule conjI)
have "r" using 1 4 by (rule mp) }
thus "q ⟶ r" by (rule impI)
qed
-- "La demostración estructurada es"
lemma ejercicio_22_2:
assumes "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof
assume "p"
show "q ⟶ r"
proof
assume "q"
with `p` have "p ∧ q" ..
with assms(1) show "r" ..
qed
qed
-- "La demostración automática es"
lemma ejercicio_22_3:
assumes "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 23. Demostrar
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_23_1:
assumes 1: "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
proof (rule impI)
assume 2: "p ∧ q"
have 3: "p ⟶ q"
proof (rule impI)
assume 4: "p"
show "q" using 2 by (rule conjunct2)
qed
show "r" using 1 3 by (rule mp)
qed
-- "La demostración estructurada es"
lemma ejercicio_23_2:
assumes "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
proof
assume "p ∧ q"
have "p ⟶ q"
proof
assume "p"
show "q" using `p ∧ q` ..
qed
with assms show "r" ..
qed
-- "La demostración automática es"
lemma ejercicio_23_3:
assumes "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_24_1:
assumes 1: "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
proof (rule impI)
assume 2: "p ⟶ q"
have 3: "p" using 1 by (rule conjunct1)
have 4: "q" using 2 3 by (rule mp)
have 5: "q ⟶ r" using 1 by (rule conjunct2)
thus "r" using 4 by (rule mp)
qed
-- "La demostración estructurada es"
lemma ejercicio_24_2:
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
proof
assume "p ⟶ q"
have "p" using assms ..
with `p ⟶ q` have "q" ..
have "q ⟶ r" using assms ..
thus "r" using `q` ..
qed
-- "La demostración automática es"
lemma ejercicio_24_3:
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
using assms
by auto
section {* Disyunciones *}
text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar
p ⊢ p ∨ q
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_25_1:
assumes 1: "p"
shows "p ∨ q"
proof -
show "p ∨ q" using 1 by (rule disjI1)
qed
-- "La demostración estructurada es"
lemma ejercicio_25_2:
assumes "p"
shows "p ∨ q"
proof -
show "p ∨ q" using assms ..
qed
-- "La demostración estructurada es"
lemma ejercicio_25_3:
assumes "p"
shows "p ∨ q"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 26. Demostrar
q ⊢ p ∨ q
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_26_1:
assumes 1: "q"
shows "p ∨ q"
proof -
show "p ∨ q" using 1 by (rule disjI2)
qed
-- "La demostración estructurada es"
lemma ejercicio_26_2:
assumes "q"
shows "p ∨ q"
proof -
show "p ∨ q" using assms ..
qed
-- "La demostración estructurada es"
lemma ejercicio_26_3:
assumes "q"
shows "p ∨ q"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 27. Demostrar
p ∨ q ⊢ q ∨ p
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_27_1:
assumes 1: "p ∨ q"
shows "q ∨ p"
using 1
proof (rule disjE)
assume "p"
thus "q ∨ p" by (rule disjI2)
next
assume "q"
thus "q ∨ p" by (rule disjI1)
qed
-- "La demostración estructurada es"
lemma ejercicio_27_2:
assumes "p ∨ q"
shows "q ∨ p"
using assms
proof
assume "p"
thus "q ∨ p" ..
next
assume "q"
thus "q ∨ p" ..
qed
-- "La demostración estructurada es"
lemma ejercicio_27_3:
assumes "p ∨ q"
shows "q ∨ p"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 28. Demostrar
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_28_1:
assumes 1: "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof (rule impI)
assume "p ∨ q"
thus "p ∨ r"
proof (rule disjE)
assume "p"
thus "p ∨ r" by (rule disjI1)
next
assume "q"
have "r" using assms `q` by (rule mp)
thus "p ∨ r" by (rule disjI2)
qed
qed
-- "La demostración estructurada es"
lemma ejercicio_28_2:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof
assume "p ∨ q"
thus "p ∨ r"
proof
assume "p"
thus "p ∨ r" ..
next
assume "q"
have "r" using assms `q` ..
thus "p ∨ r" ..
qed
qed
-- "La demostración automática es"
lemma ejercicio_28_3:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 29. Demostrar
p ∨ p ⊢ p
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_29_1:
assumes 1: "p ∨ p"
shows "p"
using 1
proof (rule disjE)
assume "p"
thus "p" by this
next
assume "p"
thus "p" by this
qed
-- "La demostración estructurada es"
lemma ejercicio_29_2:
assumes "p ∨ p"
shows "p"
using assms
proof
assume "p"
thus "p" .
next
assume "p"
thus "p" .
qed
-- "La demostración estructurada es"
lemma ejercicio_29_3:
assumes "p ∨ p"
shows "p"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 30. Demostrar
p ⊢ p ∨ p
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_30_1:
assumes 1: "p"
shows "p ∨ p"
proof -
show "p ∨ p" using 1 by (rule disjI1)
qed
-- "La demostración estructurada es"
lemma ejercicio_30_2:
assumes "p"
shows "p ∨ p"
proof -
show "p ∨ p" using assms ..
qed
-- "La demostración estructurada es"
lemma ejercicio_30_3:
assumes "p"
shows "p ∨ p"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 31. Demostrar
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_31_1:
assumes 1: "p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r"
using 1
proof (rule disjE)
assume "p"
hence "p ∨ q" by (rule disjI1)
thus "(p ∨ q) ∨ r" by (rule disjI1)
next
assume "q ∨ r"
thus "(p ∨ q) ∨ r"
proof (rule disjE)
assume "q"
hence "p ∨ q" by (rule disjI2)
thus "(p ∨ q) ∨ r" by (rule disjI1)
next
assume "r"
thus "(p ∨ q) ∨ r" by (rule disjI2)
qed
qed
-- "La demostración estructurada es"
lemma ejercicio_31_2:
assumes "p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r"
using assms
proof
assume "p"
hence "p ∨ q" ..
thus "(p ∨ q) ∨ r" ..
next
assume "q ∨ r"
thus "(p ∨ q) ∨ r"
proof
assume "q"
hence "p ∨ q" ..
thus "(p ∨ q) ∨ r" ..
next
assume "r"
thus "(p ∨ q) ∨ r" ..
qed
qed
-- "La demostración estructurada es"
lemma ejercicio_31_3:
assumes "p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 32. Demostrar
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_32_1:
assumes 1: "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
using 1
proof (rule disjE)
assume "p ∨ q"
thus "p ∨ (q ∨ r)"
proof (rule disjE)
assume "p"
thus "p ∨ (q ∨ r)" by (rule disjI1)
next
assume "q"
hence "q ∨ r" by (rule disjI1)
thus "p ∨ (q ∨ r)" by (rule disjI2)
qed
next
assume "r"
hence "q ∨ r" by (rule disjI2)
thus "p ∨ (q ∨ r)" by (rule disjI2)
qed
-- "La demostración estructurada es"
lemma ejercicio_32_2:
assumes "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
using assms
proof
assume "p ∨ q"
thus "p ∨ (q ∨ r)"
proof
assume "p"
thus "p ∨ (q ∨ r)" ..
next
assume "q"
hence "q ∨ r" ..
thus "p ∨ (q ∨ r)" ..
qed
next
assume "r"
hence "q ∨ r" ..
thus "p ∨ (q ∨ r)" ..
qed
-- "La demostración estructurada es"
lemma ejercicio_32_3:
assumes "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 33. Demostrar
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_33_1:
assumes 1: "p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
proof -
have 2: "p" using 1 by (rule conjunct1)
have 3: "q ∨ r" using 1 by (rule conjunct2)
thus "(p ∧ q) ∨ (p ∧ r)"
proof (rule disjE)
assume 4: "q"
have "p ∧ q" using 2 4 by (rule conjI)
thus "(p ∧ q) ∨ (p ∧ r)" by (rule disjI1)
next
assume 5: "r"
have "q ∨ r" using 1 by (rule conjunct2)
thus "(p ∧ q) ∨ (p ∧ r)"
proof (rule disjE)
assume "q"
have "p ∧ q" using `p` `q` by (rule conjI)
thus "(p ∧ q) ∨ (p ∧ r)" by (rule disjI1)
next
assume "r"
have "p ∧ r" using `p` `r` by (rule conjI)
thus "(p ∧ q) ∨ (p ∧ r)" by (rule disjI2)
qed
qed
qed
-- "La demostración estructurada es"
lemma ejercicio_33_2:
assumes "p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
proof -
have "p" using assms ..
have "q ∨ r" using assms ..
thus "(p ∧ q) ∨ (p ∧ r)"
proof
assume "q"
with `p` have "p ∧ q" ..
thus "(p ∧ q) ∨ (p ∧ r)" ..
next
assume "r"
hence "q ∨ r" ..
thus "(p ∧ q) ∨ (p ∧ r)"
proof
assume "q"
with `p` have "p ∧ q" ..
thus "(p ∧ q) ∨ (p ∧ r)" ..
next
assume "r"
with `p` have "p ∧ r" ..
thus "(p ∧ q) ∨ (p ∧ r)" ..
qed
qed
qed
-- "La demostración automática es"
lemma ejercicio_33_3:
assumes "p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 34. Demostrar
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_34_1:
assumes "(p ∧ q) ∨ (p ∧ r)"
shows "p ∧ (q ∨ r)"
using assms
proof (rule disjE)
assume 1: "p ∧ q"
show "p ∧ (q ∨ r)"
proof (rule conjI)
show "p" using 1 by (rule conjunct1)
next
have "q" using 1 by (rule conjunct2)
thus "q ∨ r" by (rule disjI1)
qed
next
assume 2: "p ∧ r"
hence 3: "p" by (rule conjunct1)
have "r" using 2 by (rule conjunct2)
hence 4: "q ∨ r" by (rule disjI2)
show "p ∧ (q ∨ r)" using 3 4 by (rule conjI)
qed
-- "La demostración estructurada es"
lemma ejercicio_34_2:
assumes "(p ∧ q) ∨ (p ∧ r)"
shows "p ∧ (q ∨ r)"
using assms
proof
assume "p ∧ q"
show "p ∧ (q ∨ r)"
proof
show "p" using `p ∧ q` ..
next
have "q" using `p ∧ q` ..
thus "q ∨ r" ..
qed
next
assume "p ∧ r"
hence "p" ..
have "r" using `p ∧ r` ..
hence "q ∨ r" ..
with `p` show "p ∧ (q ∨ r)" ..
qed
-- "La demostración estructurada es"
lemma ejercicio_34_3:
assumes "(p ∧ q) ∨ (p ∧ r)"
shows "p ∧ (q ∨ r)"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 35. Demostrar
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
------------------------------------------------------------------ *}
-- "La demostración estructurada es"
lemma ejercicio_35_1:
assumes "p ∨ (q ∧ r)"
shows "(p ∨ q) ∧ (p ∨ r)"
using assms
proof
assume "p"
show "(p ∨ q) ∧ (p ∨ r)"
proof
show "p ∨ q" using `p` ..
next
show "p ∨ r" using `p` ..
qed
next
assume "q ∧ r"
show "(p ∨ q) ∧ (p ∨ r)"
proof
have "q" using `q ∧ r` ..
thus "p ∨ q" ..
next
have "r" using `q ∧ r` ..
thus "p ∨ r" ..
qed
qed
-- "La demostración detallada es"
lemma ejercicio_35_2:
assumes "p ∨ (q ∧ r)"
shows "(p ∨ q) ∧ (p ∨ r)"
using assms
proof (rule disjE)
assume "p"
show "(p ∨ q) ∧ (p ∨ r)"
proof (rule conjI)
show "p ∨ q" using `p` by (rule disjI1)
next
show "p ∨ r" using `p` by (rule disjI1)
qed
next
assume "q ∧ r"
show "(p ∨ q) ∧ (p ∨ r)"
proof (rule conjI)
have "q" using `q ∧ r` ..
thus "p ∨ q" by (rule disjI2)
next
have "r" using `q ∧ r` by (rule conjunct2)
thus "p ∨ r" by (rule disjI2)
qed
qed
-- "La demostración automática es"
lemma ejercicio_35_3:
assumes "p ∨ (q ∧ r)"
shows "(p ∨ q) ∧ (p ∨ r)"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 36. Demostrar
(p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)
------------------------------------------------------------------ *}
-- "La demostración estructurada es"
lemma ejercicio_36_1:
assumes "(p ∨ q) ∧ (p ∨ r)"
shows "p ∨ (q ∧ r)"
proof -
have "p ∨ q" using assms ..
thus "p ∨ (q ∧ r)"
proof
assume "p"
thus "p ∨ (q ∧ r)" ..
next
assume "q"
have "p ∨ r" using assms ..
thus "p ∨ (q ∧ r)"
proof
assume "p"
thus "p ∨ (q ∧ r)" ..
next
assume "r"
with `q` have "q ∧ r" ..
thus "p ∨ (q ∧ r)" ..
qed
qed
qed
-- "La demostración detallada es"
lemma ejercicio_36_2:
assumes "(p ∨ q) ∧ (p ∨ r)"
shows "p ∨ (q ∧ r)"
proof -
have "p ∨ q" using assms by (rule conjunct1)
thus "p ∨ (q ∧ r)"
proof (rule disjE)
assume "p"
thus "p ∨ (q ∧ r)" by (rule disjI1)
next
assume "q"
have "p ∨ r" using assms by (rule conjunct2)
thus "p ∨ (q ∧ r)"
proof (rule disjE)
assume "p"
thus "p ∨ (q ∧ r)" by (rule disjI1)
next
assume "r"
have "q ∧ r" using `q` `r` by (rule conjI)
thus "p ∨ (q ∧ r)" by (rule disjI2)
qed
qed
qed
-- "La demostración automática es"
lemma ejercicio_36_3:
assumes "(p ∨ q) ∧ (p ∨ r)"
shows "p ∨ (q ∧ r)"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 37. Demostrar
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
------------------------------------------------------------------ *}
-- "La demostración estructurada es"
lemma ejercicio_37_1:
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
proof
assume "p ∨ q"
thus "r"
proof
assume "p"
have "p ⟶ r" using assms ..
thus "r" using `p` ..
next
assume "q"
have "q ⟶ r" using assms ..
thus "r" using `q` ..
qed
qed
-- "La demostración detallada es"
lemma ejercicio_37_2:
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
proof (rule impI)
assume "p ∨ q"
thus "r"
proof (rule disjE)
assume "p"
have "p ⟶ r" using assms by (rule conjunct1)
thus "r" using `p` by (rule mp)
next
assume "q"
have "q ⟶ r" using assms by (rule conjunct2)
thus "r" using `q` by (rule mp)
qed
qed
-- "La demostración automática es"
lemma ejercicio_37_3:
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 38. Demostrar
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
------------------------------------------------------------------ *}
-- "La demostración estructurada es"
lemma ejercicio_38_1:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
proof
show "p ⟶ r"
proof
assume "p"
hence "p ∨ q" ..
with assms show "r" ..
qed
next
show "q ⟶ r"
proof
assume "q"
hence "p ∨ q" ..
with assms show "r" ..
qed
qed
-- "La demostración detallada es"
lemma ejercicio_38_2:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
proof (rule conjI)
show "p ⟶ r"
proof (rule impI)
assume "p"
hence "p ∨ q" by (rule disjI1)
show "r" using assms `p ∨ q` by (rule mp)
qed
next
show "q ⟶ r"
proof (rule impI)
assume "q"
hence "p ∨ q" by (rule disjI2)
show "r" using assms `p ∨ q` by (rule mp)
qed
qed
-- "La demostración automática es"
lemma ejercicio_38_3:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
using assms
by auto
section {* Negación *}
text {* ---------------------------------------------------------------
Ejercicio 39. Demostrar
p ⊢ ¬¬p
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_39_1:
assumes "p"
shows "¬¬p"
proof -
show "¬¬p" using assms by (rule notnotI)
qed
-- "La demostración automática es"
lemma ejercicio_39_2:
assumes "p"
shows "¬¬p"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 40. Demostrar
¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}
-- "La demostración estructurada es"
lemma ejercicio_40_1:
assumes "¬p"
shows "p ⟶ q"
proof
assume "p"
with assms(1) show "q" ..
qed
-- "La demostración detallada es"
lemma ejercicio_40_2:
assumes "¬p"
shows "p ⟶ q"
proof (rule impI)
assume "p"
show "q" using assms(1) `p` by (rule notE)
qed
-- "La demostración automática es"
lemma ejercicio_40_3:
assumes "¬p"
shows "p ⟶ q"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 41. Demostrar
p ⟶ q ⊢ ¬q ⟶ ¬p
------------------------------------------------------------------ *}
-- "La demostración estructurada es"
lemma ejercicio_41_1:
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
proof
assume "¬q"
with assms(1) show "¬p" by (rule mt)
qed
-- "La demostración detallada es"
lemma ejercicio_41_2:
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
proof (rule impI)
assume "¬q"
show "¬p" using assms(1) `¬q` by (rule mt)
qed
-- "La demostración automática es"
lemma ejercicio_41_3:
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 42. Demostrar
p ∨ q, ¬q ⊢ p
------------------------------------------------------------------ *}
-- "La demostración estructurada es"
lemma ejercicio_42_1:
assumes "p ∨ q"
"¬q"
shows "p"
using assms(1)
proof
assume "p"
thus "p" .
next
assume "q"
with assms(2) show "p" ..
qed
-- "La demostración detallada es"
lemma ejercicio_42_2:
assumes "p ∨ q"
"¬q"
shows "p"
using assms(1)
proof (rule disjE)
assume "p"
thus "p" by this
next
assume "q"
show "p" using assms(2) `q` by (rule notE)
qed
-- "La demostración automática es"
lemma ejercicio_42_3:
assumes "p ∨ q"
"¬q"
shows "p"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 42. Demostrar
p ∨ q, ¬p ⊢ q
------------------------------------------------------------------ *}
-- "La demostración estructurada es"
lemma ejercicio_43_1:
assumes "p ∨ q"
"¬p"
shows "q"
using assms(1)
proof
assume "p"
with assms(2) show "q" ..
next
assume "q"
thus "q" .
qed
-- "La demostración detallada es"
lemma ejercicio_43_2:
assumes "p ∨ q"
"¬p"
shows "q"
using assms(1)
proof (rule disjE)
assume "p"
show "q" using assms(2) `p` by (rule notE)
next
assume "q"
thus "q" by this
qed
-- "La demostración automática es"
lemma ejercicio_43_3:
assumes "p ∨ q"
"¬p"
shows "q"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 44. Demostrar
p ∨ q ⊢ ¬(¬p ∧ ¬q)
------------------------------------------------------------------ *}
-- "La demostración estructurada es"
lemma ejercicio_44_1:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
proof
assume "¬p ∧ ¬q"
note `p ∨ q`
thus "False"
proof
assume "p"
have "¬p" using `¬p ∧ ¬q` ..
thus "False" using `p` ..
next
assume "q"
have "¬q" using `¬p ∧ ¬q` ..
thus "False" using `q` ..
qed
qed
-- "La demostración detallada es"
lemma ejercicio_44_2:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
proof (rule notI)
assume "¬p ∧ ¬q"
note `p ∨ q`
thus "False"
proof
assume "p"
have "¬p" using `¬p ∧ ¬q` by (rule conjunct1)
thus "False" using `p` by (rule notE)
next
assume "q"
have "¬q" using `¬p ∧ ¬q` by (rule conjunct2)
thus "False" using `q` by (rule notE)
qed
qed
-- "La demostración automática es"
lemma ejercicio_44_3:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 45. Demostrar
p ∧ q ⊢ ¬(¬p ∨ ¬q)
------------------------------------------------------------------ *}
-- "La demostración estructurada es"
lemma ejercicio_45_1:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"
proof
assume "¬p ∨ ¬q"
thus "False"
proof
assume "¬p"
have "p" using assms ..
with `¬p` show "False" ..
next
assume "¬q"
have "q" using assms ..
with `¬q` show "False" ..
qed
qed
-- "La demostración detallada es"
lemma ejercicio_45_2:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"
proof (rule notI)
assume "¬p ∨ ¬q"
thus "False"
proof
assume "¬p"
have "p" using assms by (rule conjunct1)
show "False" using `¬p` `p` by (rule notE)
next
assume "¬q"
have "q" using assms by (rule conjunct2)
show "False" using `¬q` `q` by (rule notE)
qed
qed
-- "La demostración automática es"
lemma ejercicio_45_3:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 46. Demostrar
¬(p ∨ q) ⊢ ¬p ∧ ¬q
------------------------------------------------------------------ *}
-- "La demostración estructurada es"
lemma ejercicio_46_1:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof
show "¬p"
proof
assume "p"
hence "p ∨ q" ..
with assms show "False" ..
qed
next
show "¬q"
proof
assume "q"
hence "p ∨ q" ..
with assms show "False" ..
qed
qed
-- "La demostración detallada es"
lemma ejercicio_46_2:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof (rule conjI)
show "¬p"
proof (rule notI)
assume "p"
hence "p ∨ q" by (rule disjI1)
show "False" using assms `p ∨ q` by (rule notE)
qed
next
show "¬q"
proof (rule notI)
assume "q"
hence "p ∨ q" by (rule disjI2)
show "False" using assms `p ∨ q` by (rule notE)
qed
qed
-- "La demostración automática es"
lemma ejercicio_46_3:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 47. Demostrar
¬p ∧ ¬q ⊢ ¬(p ∨ q)
------------------------------------------------------------------ *}
-- "La demostración estructurada es"
lemma ejercicio_47_1:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof
assume "p ∨ q"
thus False
proof
assume "p"
have "¬p" using assms ..
thus False using `p` ..
next
assume "q"
have "¬q" using assms ..
thus False using `q` ..
qed
qed
-- "La demostración detallada es"
lemma ejercicio_47_2:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof (rule notI)
assume "p ∨ q"
thus False
proof (rule disjE)
assume "p"
have "¬p" using assms by (rule conjunct1)
thus False using `p` by (rule notE)
next
assume "q"
have "¬q" using assms by (rule conjunct2)
thus False using `q` by (rule notE)
qed
qed
-- "La demostración automática es"
lemma ejercicio_47_3:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 48. Demostrar
¬p ∨ ¬q ⊢ ¬(p ∧ q)
------------------------------------------------------------------ *}
-- "La demostración estructurada es"
lemma ejercicio_48_1:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof
assume "p ∧ q"
note `¬p ∨ ¬ q`
thus False
proof
assume "¬p"
have "p" using `p ∧ q` ..
with `¬p` show False ..
next
assume "¬q"
have "q" using `p ∧ q` ..
with `¬q` show False ..
qed
qed
-- "La demostración detallada es"
lemma ejercicio_48_2:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof (rule notI)
assume "p ∧ q"
note `¬p ∨ ¬ q`
thus False
proof (rule disjE)
assume "¬p"
have "p" using `p ∧ q` by (rule conjunct1)
show False using `¬p` `p` by (rule notE)
next
assume "¬q"
have "q" using `p ∧ q` by (rule conjunct2)
show False using `¬q` `q` by (rule notE)
qed
qed
-- "La demostración automática es"
lemma ejercicio_48_3:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 49. Demostrar
⊢ ¬(p ∧ ¬p)
------------------------------------------------------------------ *}
-- "La demostración estructurada es"
lemma ejercicio_49_1:
"¬(p ∧ ¬p)"
proof
assume "p ∧ ¬p"
hence "p" ..
have "¬p" using `p ∧ ¬p` ..
thus False using `p` ..
qed
-- "La demostración detallada es"
lemma ejercicio_49_2:
"¬(p ∧ ¬p)"
proof (rule notI)
assume "p ∧ ¬p"
hence "p" by (rule conjunct1)
have "¬p" using `p ∧ ¬p` by (rule conjunct2)
thus False using `p` by (rule notE)
qed
-- "La demostración automática es"
lemma ejercicio_49_3:
"¬(p ∧ ¬p)"
by auto
text {* ---------------------------------------------------------------
Ejercicio 50. Demostrar
p ∧ ¬p ⊢ q
------------------------------------------------------------------ *}
-- "La demostración estructurada es"
lemma ejercicio_50_1:
assumes "p ∧ ¬p"
shows "q"
proof -
have "p" using assms ..
have "¬p" using assms ..
thus "q" using `p` ..
qed
-- "La demostración detallada es"
lemma ejercicio_50_2:
assumes "p ∧ ¬p"
shows "q"
proof -
have "p" using assms by (rule conjunct1)
have "¬p" using assms by (rule conjunct2)
thus "q" using `p` by (rule notE)
qed
-- "La demostración automática es"
lemma ejercicio_50_3:
assumes "p ∧ ¬p"
shows "q"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 51. Demostrar
¬¬p ⊢ p
------------------------------------------------------------------ *}
-- "La demostración detallada es"
lemma ejercicio_51_1:
assumes "¬¬p"
shows "p"
using assms
by (rule notnotD)
-- "La demostración automática es"
lemma ejercicio_51_2:
assumes "¬¬p"
shows "p"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 52. Demostrar
⊢ p ∨ ¬p
------------------------------------------------------------------ *}
-- "La demostración estructurada es"
lemma ejercicio_52_1:
"p ∨ ¬p"
proof -
have "¬¬p ∨ ¬p" ..
thus "p ∨ ¬p" by simp
qed
-- "La demostración detallada es"
lemma ejercicio_52_2:
"p ∨ ¬p"
proof -
have "¬¬p ∨ ¬p" by (rule excluded_middle)
thus "p ∨ ¬p" by simp
qed
-- "La demostración automática es"
lemma ejercicio_52_3:
"p ∨ ¬p"
by auto
text {* ---------------------------------------------------------------
Ejercicio 53. Demostrar
⊢ ((p ⟶ q) ⟶ p) ⟶ p
------------------------------------------------------------------ *}
-- "La demostración estructurada es"
lemma ejercicio_53_1:
"((p ⟶ q) ⟶ p) ⟶ p"
proof
assume "(p ⟶ q) ⟶ p"
show "p"
proof (rule ccontr)
assume "¬p"
have "¬(p ⟶ q)" using `(p ⟶ q) ⟶ p` `¬p` by (rule mt)
have "p ⟶ q"
proof
assume "p"
with `¬p` show "q" ..
qed
show False using `¬(p ⟶ q)` `p ⟶ q` ..
qed
qed
-- "La demostración detallada es"
lemma ejercicio_53_2:
"((p ⟶ q) ⟶ p) ⟶ p"
proof (rule impI)
assume "(p ⟶ q) ⟶ p"
show "p"
proof (rule ccontr)
assume "¬p"
have "¬(p ⟶ q)" using `(p ⟶ q) ⟶ p` `¬p` by (rule mt)
have "p ⟶ q"
proof (rule impI)
assume "p"
show "q" using `¬p` `p` by (rule notE)
qed
show False using `¬(p ⟶ q)` `p ⟶ q` by (rule notE)
qed
qed
-- "La demostración automática es"
lemma ejercicio_53_3:
"((p ⟶ q) ⟶ p) ⟶ p"
by auto
text {* ---------------------------------------------------------------
Ejercicio 54. Demostrar
¬q ⟶ ¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}
-- "La demostración estructurada es"
lemma ejercicio_54_1:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof
assume "p"
show "q"
proof (rule ccontr)
assume "¬q"
with assms have "¬p" ..
thus False using `p` ..
qed
qed
-- "La demostración detallada es"
lemma ejercicio_54_2:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof (rule impI)
assume "p"
show "q"
proof (rule ccontr)
assume "¬q"
have "¬p" using assms `¬q` by (rule mp)
thus False using `p` by (rule notE)
qed
qed
-- "La demostración automática es"
lemma ejercicio_54_3:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 55. Demostrar
¬(¬p ∧ ¬q) ⊢ p ∨ q
------------------------------------------------------------------ *}
-- "La demostración estructurada es"
lemma ejercicio_55_1:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof -
have "¬p ∨ p" ..
thus "p ∨ q"
proof
assume "¬p"
have "¬q ∨ q" ..
thus "p ∨ q"
proof
assume "¬q"
with `¬p` have "¬p ∧ ¬q" ..
with assms show "p ∨ q" ..
next
assume "q"
thus "p ∨ q" ..
qed
next
assume "p"
thus "p ∨ q" ..
qed
qed
-- "La demostración detallada es"
lemma ejercicio_55_2:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof -
have "¬p ∨ p" by (rule excluded_middle)
thus "p ∨ q"
proof
assume "¬p"
have "¬q ∨ q" by (rule excluded_middle)
thus "p ∨ q"
proof
assume "¬q"
have "¬p ∧ ¬q" using `¬p` `¬q` by (rule conjI)
show "p ∨ q" using assms `¬p ∧ ¬q` by (rule notE)
next
assume "q"
thus "p ∨ q" by (rule disjI2)
qed
next
assume "p"
thus "p ∨ q" by (rule disjI1)
qed
qed
-- "La demostración automática es"
lemma ejercicio_55_3:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 56. Demostrar
¬(¬p ∨ ¬q) ⊢ p ∧ q
------------------------------------------------------------------ *}
-- "La demostración estructurada es"
lemma ejercicio_56_1:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof
show "p"
proof (rule ccontr)
assume "¬p"
hence "¬p ∨ ¬q" ..
with assms show False ..
qed
next
show "q"
proof (rule ccontr)
assume "¬q"
hence "¬p ∨ ¬q" ..
with assms show False ..
qed
qed
-- "La demostración detallada es"
lemma ejercicio_56_2:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof (rule conjI)
show "p"
proof (rule ccontr)
assume "¬p"
hence "¬p ∨ ¬q" by (rule disjI1)
show False using assms `¬p ∨ ¬q` by (rule notE)
qed
next
show "q"
proof (rule ccontr)
assume "¬q"
hence "¬p ∨ ¬q" by (rule disjI2)
show False using assms `¬p ∨ ¬q` by (rule notE)
qed
qed
-- "La demostración automática es"
lemma ejercicio_56_3:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 57. Demostrar
¬(p ∧ q) ⊢ ¬p ∨ ¬q
------------------------------------------------------------------ *}
-- "La demostración estructurada es"
lemma ejercicio_57_1:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof -
have "¬p ∨ p" ..
thus "¬p ∨ ¬q"
proof
assume "¬p"
thus "¬p ∨ ¬q" ..
next
assume "p"
have "¬q ∨ q" ..
thus "¬p ∨ ¬q"
proof
assume "¬q"
thus "¬p ∨ ¬q" ..
next
assume "q"
with `p` have "p ∧ q" ..
with assms show "¬p ∨ ¬q" ..
qed
qed
qed
-- "La demostración detallada es"
lemma ejercicio_57_2:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof -
have "¬p ∨ p" by (rule excluded_middle)
thus "¬p ∨ ¬q"
proof (rule disjE)
assume "¬p"
thus "¬p ∨ ¬q" by (rule disjI1)
next
assume "p"
have "¬q ∨ q" by (rule excluded_middle)
thus "¬p ∨ ¬q"
proof
assume "¬q"
thus "¬p ∨ ¬q" by (rule disjI2)
next
assume "q"
have "p ∧ q" using `p` `q` by (rule conjI)
show "¬p ∨ ¬q" using assms `p ∧ q` by (rule notE)
qed
qed
qed
-- "La demostración automática es"
lemma ejercicio_57_3:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
using assms
by auto
text {* ---------------------------------------------------------------
Ejercicio 58. Demostrar
⊢ (p ⟶ q) ∨ (q ⟶ p)
------------------------------------------------------------------ *}
-- "La demostración estructurada es"
lemma ejercicio_58_1:
"(p ⟶ q) ∨ (q ⟶ p)"
proof -
have "¬p ∨ p" ..
thus "(p ⟶ q) ∨ (q ⟶ p)"
proof
assume "¬p"
have "p ⟶ q"
proof
assume "p"
with `¬p` show "q" ..
qed
thus "(p ⟶ q) ∨ (q ⟶ p)" ..
next
assume "p"
have "q ⟶ p"
proof
assume "q"
show "p" using `p` .
qed
thus "(p ⟶ q) ∨ (q ⟶ p)" ..
qed
qed
-- "La demostración detallada es"
lemma ejercicio_58_2:
"(p ⟶ q) ∨ (q ⟶ p)"
proof -
have "¬p ∨ p" by (rule excluded_middle)
thus "(p ⟶ q) ∨ (q ⟶ p)"
proof
assume "¬p"
have "p ⟶ q"
proof (rule impI)
assume "p"
show "q" using `¬p` `p` by (rule notE)
qed
thus "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI1)
next
assume "p"
have "q ⟶ p"
proof
assume "q"
show "p" using `p` by this
qed
thus "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI2)
qed
qed
-- "La demostración automática es"
lemma ejercicio_58_3:
"(p ⟶ q) ∨ (q ⟶ p)"
by auto
end