Mjoseh: Protegió «Rel 2» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

2020-03-17T16:12:19Z

Protegió «Rel 2» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « chapter ‹ R2: Deducción natural proposicional(I) › theory R2_sol imports Main begin text ‹ -------------------------------------…»

2020-03-17T16:12:08Z

Página creada con «<source lang = "isabelle"> chapter ‹ R2: Deducción natural proposicional(I) › theory R2_sol imports Main begin text ‹ -------------------------------------…»

Página nueva

<source lang = "isabelle">
chapter ‹ R2: Deducción natural proposicional(I) ›

theory R2_sol
imports Main
begin

text ‹
---------------------------------------------------------------------
El objetivo de esta relación es demostrar cada uno de los ejercicios
usando sólo las reglas básicas de deducción natural de la lógica
proposicional (sin usar el método auto).

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
------------------------------------------------------------------ ›

lemma ejercicio_1a:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
show "q" using 1 2 by (rule mp)
qed

lemma ejercicio_1b:
assumes "p ⟶ q"
"p"
shows "q"
proof -
show "q" using assms by (rule mp)
qed

lemma ejercicio_1c:
assumes "p ⟶ q"
"p"
shows "q"
proof -
show "q" using assms ..
qed

lemma ejercicio_1d:
assumes "p ⟶ q"
"p"
shows "q"
proof -
show "q" using assms by auto
qed

lemma ejercicio_1e: "⟦p ⟶ q; p⟧ ⟹ q"
apply (erule mp)
apply assumption
done

text ‹ ---------------------------------------------------------------
Ejercicio 2. Demostrar
p ⟶ q, q ⟶ r, p ⊢ r
------------------------------------------------------------------ ›

lemma ejercicio_2a:
assumes 1:"p ⟶ q" and
2:"q ⟶ r" and
3:"p"
shows "r"
proof -
have 4: "q" using 1 3 by (rule mp)
show 5: "r" using 2 4 by (rule mp)
qed

lemma ejercicio_2b:
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

lemma ejercicio_2c:
assumes "p ⟶ q" and
"q ⟶ r" and
"p"
shows "r"
proof -
have "q" using assms(1,3) ..
show "r" using assms(2) `q` ..
qed

lemma ejercicio_2d:
assumes "p ⟶ q" and
"q ⟶ r" and
"p"
shows "r"
proof -
show "r" using assms by auto
qed

lemma ej2_aplicativa: "⟦p ⟶ q; q ⟶ r; p⟧ ⟹ r"
apply (erule mp)+
apply assumption
done

text ‹ ---------------------------------------------------------------
Ejercicio 3. Demostrar
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r
------------------------------------------------------------------ ›

lemma ejercicio_3a:
assumes 1: "p ⟶ (q ⟶ r)" and
2: "p ⟶ q" and
3: "p"
shows "r"
proof -
have 4: "q ⟶ r" using 1 3 by (rule mp)
have 5: "q" using 2 3 by (rule mp)
show 6: "r" using 4 5 by (rule mp)
qed

lemma ejercicio_3b:
assumes "p ⟶ (q ⟶ r)" and
"p ⟶ q" and
"p"
shows "r"
proof -
have 4: "q ⟶ r" using assms(1,3) ..
have "q" using assms(2,3) ..
show "r" using 4 `q` ..
qed

lemma ejercicio_3c:
assumes "p ⟶ (q ⟶ r)" and
"p ⟶ q" and
"p"
shows "r"
proof -
have "q" using assms(2,3) ..
have "q ⟶ r" using assms(1,3) ..
then show "r" using `q` ..
qed

lemma ejercicio_3d:
assumes "p ⟶ (q ⟶ r)" and
"p ⟶ q" and
"p"
shows "r"
proof -
show "r" using assms by auto
qed

lemma ej3c: "⟦p ⟶ (q ⟶ r); p ⟶ q; p⟧ ⟹ r"
apply (drule mp)
apply assumption
apply (drule mp)
apply assumption
apply (drule mp)
apply assumption+
done

lemma ej3d: "⟦p ⟶ (q ⟶ r); p ⟶ q; p⟧ ⟹ r"
apply (drule mp, assumption+)+
done

thm impE

lemma ej3a: "⟦p ⟶ (q ⟶ r); p ⟶ q; p⟧ ⟹ r"
apply (erule impE)
apply assumption
apply (erule impE)
apply assumption
apply (erule impE)
apply assumption+
done

lemma ej3b: "⟦p ⟶ (q ⟶ r); p ⟶ q; p⟧ ⟹ r"
apply (erule impE, assumption+)+
done

text ‹ ---------------------------------------------------------------
Ejercicio 4. Demostrar
p ⟶ q, q ⟶ r ⊢ p ⟶ r
------------------------------------------------------------------ ›

lemma ejercicio_4a:
assumes 1: "p ⟶ q" and
2: "q ⟶ r"
shows "p ⟶ r"
proof -
{assume 3:"p"
have 4: "q" using 1 3 by (rule mp)
have 5: "r" using 2 4 by (rule mp)}
then show "p⟶ r" by (rule impI)
qed

lemma ejercicio_4b:
assumes 1: "p ⟶ q" and
2: "q ⟶ r"
shows "p ⟶ r"
proof (rule impI)
assume 3:"p"
have "q" using 1 3 by (rule mp)
show "r" using 2 `q` by (rule mp)
qed

lemma ejercicio_4c:
assumes "p ⟶ q" and
"q ⟶ r"
shows "p ⟶ r"
proof (rule impI)
assume "p"
have "q" using assms(1) `p` ..
show "r" using assms(2) `q` ..
qed

lemma ejercicio_4d:
assumes "p ⟶ q" and
"q ⟶ r"
shows "p ⟶ r"
using assms by auto

lemma ej4: "⟦p ⟶ q; q ⟶ r⟧ ⟹ p ⟶ r"
apply (rule impI)
apply (erule mp)
apply (erule mp)
apply assumption
done

text ‹ ---------------------------------------------------------------
Ejercicio 5. Demostrar
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)
------------------------------------------------------------------ ›

lemma ejercicio_5a:
assumes 1: "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
proof -
{assume 3: "q"
{assume 4: "p"
have "q ⟶ r" using 1 4 ..
then have 5: "r" using 3 ..}
then have 6: "p ⟶ r" by (rule impI)}
then show "q ⟶ (p ⟶ r)" by (rule impI)
qed

lemma ejercicio_5b:
assumes "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
proof (rule impI)
assume "q"
show "p ⟶ r"
proof (rule impI)
assume "p"
have "q ⟶ r" using assms(1) `p` ..
then show "r" using `q` ..
qed
qed

lemma ejercicio_5c:
assumes "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
proof (rule impI)
assume "q"
show "p ⟶ r"
proof
assume "p"
with assms(1) have "q ⟶ r" ..
then show "r" using `q` ..
qed
qed

lemma ejercicio_5d:
assumes "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
using assms by auto

lemma ej5: "p ⟶ (q ⟶ r) ⟹ q ⟶ (p ⟶ r)"
apply (rule impI)
apply (rule impI)
apply (drule mp, assumption)
apply (drule mp, assumption)
apply assumption
done

text ‹ ---------------------------------------------------------------
Ejercicio 6. Demostrar
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
------------------------------------------------------------------ ›

lemma ejercicio_6a:
assumes 1: "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
proof -
{assume 2: "p ⟶ q"
{assume 3: "p"
have 4: "q ⟶ r" using 1 3 ..
have 5: "q" using 2 3 ..
have "r" using 4 5 ..}
then have "p ⟶ r" by (rule impI)}
then show "(p ⟶ q) ⟶ (p ⟶ r)" by (rule impI)
qed

lemma ejercicio_6b:
assumes "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
proof (rule impI)
assume "p ⟶ q"
show "p ⟶ r"
proof (rule impI)
assume "p"
with `p ⟶ q` have "q" ..
have "q ⟶ r" using assms(1) `p` ..
then show "r" using `q` ..
qed
qed

lemma ejercicio_6c:
assumes "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
using assms by auto

lemma ej6: "p ⟶ (q ⟶ r) ⟹ (p ⟶ q) ⟶ (p ⟶ r)"
apply (rule impI)
apply (rule impI)
apply (drule mp, assumption)
apply (drule mp, assumption)
apply (drule mp, assumption+)
done

text ‹ ---------------------------------------------------------------
Ejercicio 7. Demostrar
p ⊢ q ⟶ p
------------------------------------------------------------------ ›

lemma ejercicio_7:
assumes "p"
shows "q ⟶ p"
proof (rule impI)
assume "q"
show "p" using assms(1) by this
qed

lemma ej7: "p ⟹ q ⟶ p"
apply (rule impI)
apply assumption
done

text ‹ ---------------------------------------------------------------
Ejercicio 8. Demostrar
⊢ p ⟶ (q ⟶ p)
------------------------------------------------------------------ ›

lemma ejercicio_8a:
"p ⟶ (q ⟶ p)"
proof (rule impI)
assume "p"
show "q ⟶ p"
proof (rule impI)
assume "q"
show "p" using `p` .
qed
qed

lemma ejercicio_8b:
"p ⟶ (q ⟶ p)"
by auto

lemma ej8: "p ⟶ (q ⟶ p)"
apply (rule impI)
apply (rule impI)
apply assumption
done

text ‹ ---------------------------------------------------------------
Ejercicio 9. Demostrar
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)
------------------------------------------------------------------ ›

lemma ejercicio_9a:
assumes "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"
proof (rule impI)
assume "q ⟶ r"
show "p ⟶ r"
proof (rule impI)
assume "p"
have "q" using assms(1) `p` ..
show "r" using `q ⟶ r` `q` ..
qed
qed

lemma ejercicio_9b:
assumes "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"
using assms by auto

lemma ej9: "p ⟶ q ⟹ (q ⟶ r) ⟶ (p ⟶ r)"
apply (rule impI)
apply (rule impI)
apply (drule mp, assumption)
apply (drule mp, assumption+)
done

text ‹ ---------------------------------------------------------------
Ejercicio 10. Demostrar
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
------------------------------------------------------------------ ›

lemma ejercicio_10a:
assumes "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
proof (rule impI)
assume "r"
show "q ⟶ (p ⟶ s)"
proof (rule impI)
assume "q"
show "p ⟶ s"
proof (rule impI)
assume "p"
with assms(1) have "q ⟶ (r ⟶ s)" ..
then have "r ⟶ s" using `q` ..
then show "s" using `r` ..
qed
qed
qed

lemma ejercicio_10b:
assumes "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
using assms by auto

lemma ej10: "p ⟶ (q ⟶ (r ⟶ s)) ⟹ r ⟶ (q ⟶ (p ⟶ s))"
apply (rule impI)+
apply (drule mp, assumption+)+
done

text ‹ ---------------------------------------------------------------
Ejercicio 11. Demostrar
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
------------------------------------------------------------------ ›

lemma ejercicio_11a:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof (rule impI)
assume "p ⟶ (q ⟶ r)"
show "(p ⟶ q) ⟶ (p ⟶ r)"
proof (rule impI)
assume "p ⟶ q"
show "p ⟶ r"
proof (rule impI)
assume "p"
have "q ⟶ r" using `p ⟶ (q ⟶ r)` `p`..
have "q" using `p ⟶ q` `p` ..
show "r" using `q ⟶ r` `q` ..
qed
qed
qed

lemma ejercicio_11b:
"(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` ..
then have "r" using `q` ..}
then have "p ⟶ r" ..}
then show "(p ⟶ q) ⟶ (p ⟶ r)" ..
qed

lemma ejercicio_11c:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
by auto

lemma ej11: "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
apply (rule impI)+
apply (drule mp, assumption+)+
done

text ‹ ---------------------------------------------------------------
Ejercicio 12. Demostrar
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ ›

lemma ejercicio_12a:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof (rule impI)
assume "p"
show "q ⟶ r"
proof (rule impI)
assume "q"
show "r"
proof -
{assume "p"
have "q" using `q` .}
then have "p ⟶ q" ..
show "r" using assms(1) `p ⟶ q` ..
qed
qed
qed

lemma ejercicio_12b:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof
assume "p"
{assume "q"
{assume "p"
have "q" using `q` .}
then have "p ⟶ q" ..
with assms(1) have "r" ..}
then show "q ⟶ r" ..
qed

lemma ejercicio_12c:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
using assms by auto

lemma ej12: "(p ⟶ q) ⟶ r ⟹ p ⟶ (q ⟶ r)"
apply (rule impI)+
apply (rule_tac P="p ⟶ q" in mp)
apply assumption
apply (rule impI)
apply assumption
done

section ‹ Conjunciones ›

text ‹ ---------------------------------------------------------------
Ejercicio 13. Demostrar
p, q ⊢ p ∧ q
------------------------------------------------------------------ ›

lemma ejercicio_13a:
assumes 1:"p" and
2:"q"
shows "p ∧ q"
proof -
show "p ∧ q" using 1 2 by (rule conjI)
qed

lemma ejercicio_13b:
assumes "p" and
"q"
shows "p ∧ q"
proof (rule conjI)
show "p" using assms(1) .
show "q" using assms(2) .
qed

lemma ejercicio_13c:
assumes "p" and
"q"
shows "p ∧ q"
using assms by auto

lemma ej13: "⟦p; q⟧ ⟹ p ∧ q"
apply (rule conjI)
apply assumption
apply assumption
done

text ‹ ---------------------------------------------------------------
Ejercicio 14. Demostrar
p ∧ q ⊢ p
------------------------------------------------------------------ ›
lemma ejercicio_14:
assumes "p ∧ q"
shows "p"
proof -
show "p" using assms by (rule conjunct1)
qed

lemma ej14: "p ∧ q ⟹ p"
apply (erule conjunct1)
done

text ‹ ---------------------------------------------------------------
Ejercicio 15. Demostrar
p ∧ q ⊢ q
------------------------------------------------------------------ ›
lemma ejercicio_15:
assumes "p ∧ q"
shows "q"
proof -
show "q" using assms by (rule conjunct2)
qed

lemma ej15: "p ∧ q ⟹ q"
apply (erule conjunct2)
done

text ‹ ---------------------------------------------------------------
Ejercicio 16. Demostrar
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
------------------------------------------------------------------ ›

lemma ejercicio_16a:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q)∧ r"
proof -
have 1: "p" using assms by (rule conjunct1)
have 2: "(q ∧ r)" using assms by (rule conjunct2)
have 3: "q" using 2 by (rule conjunct1)
have 4: "r" using 2 by (rule conjunct2)
have 5: "(p∧q)" using 1 3 by (rule conjI)
show "(p∧q) ∧ r" using 5 4 by (rule conjI)
qed

lemma ejercicio_16b:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q)∧ r"
proof (rule conjI)
show "p ∧ q"
proof (rule conjI)
show "p" using assms ..
next
have "q ∧ r" using assms ..
then show "q" ..
qed
next
have "q ∧ r" using assms ..
then show "r" ..
qed

lemma ejercicio_16c:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q)∧ r"
using assms by auto

lemma ej16: "p ∧ (q ∧ r) ⟹ (p ∧ q) ∧ r"
apply (rule conjI)
apply (rule conjI)
apply (erule conjunct1)
apply (drule conjunct2)
apply (erule conjunct1)
apply (drule conjunct2)
apply (erule conjunct2)
done

text ‹ ---------------------------------------------------------------
Ejercicio 17. Demostrar
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
------------------------------------------------------------------ ›
lemma ejercicio_17a:
assumes "(p∧ q) ∧ r"
shows "p ∧ (q∧ r)"
proof -
have 1: "r" using assms by (rule conjunct2)
have 2: "(p∧q)" using assms by (rule conjunct1)
have 3: "p" using 2 by (rule conjunct1)
have 4: "q" using 2 by (rule conjunct2)
have 5: "(q∧r)" using 4 1 by (rule conjI)
show "p∧(q∧r)" using 3 5 by (rule conjI)
qed

lemma ejercicio_17b:
assumes "(p∧ q) ∧ r"
shows "p ∧ (q∧ r)"
proof (rule conjI)
have "p ∧ q" using assms ..
then show "p" ..
next
show "q ∧ r"
proof (rule conjI)
have "p ∧ q" using assms ..
then show "q" ..
next
show "r" using assms ..
qed
qed

lemma ejercicio_17c:
assumes "(p∧ q) ∧ r"
shows "p ∧ (q∧ r)"
using assms by auto

lemma ej17: "(p ∧ q) ∧ r ⟹ p ∧ (q ∧ r)"
apply (rule conjI)
apply (drule conjunct1)
apply (erule conjunct1)
apply (rule conjI)
apply (drule conjunct1)
apply (erule conjunct2)
apply (erule conjunct2)
done

text ‹ ---------------------------------------------------------------
Ejercicio 18. Demostrar
p ∧ q ⊢ p ⟶ q
------------------------------------------------------------------ ›

lemma ejercicio_18a:
assumes "p ∧ q"
shows "p ⟶ q"
proof -
have 1: "q" using assms by (rule conjunct2)
show "p⟶ q" using 1 by (rule impI)
qed

lemma ejercicio_18b:
assumes "p ∧ q"
shows "p ⟶ q"
proof (rule impI)
assume "p"
show "q" using assms ..
qed

lemma ejercicio_18c:
assumes "p ∧ q"
shows "p ⟶ q"
using assms by auto

lemma ej18: "p ∧ q ⟹ p ⟶ q"
apply (rule impI)
apply (erule conjunct2)
done

text ‹ ---------------------------------------------------------------
Ejercicio 19. Demostrar
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r
------------------------------------------------------------------ ›

lemma ejercicio_19a:
assumes "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
proof (rule impI)
assume "p"
show "q ∧ r"
proof (rule conjI)
have "p ⟶ q" using assms ..
then show "q" using `p` ..
have "p ⟶ r" using assms ..
then show "r" using `p` ..
qed
qed

lemma ejercicio_19c:
assumes "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
using assms by auto

lemma ej19: "(p ⟶ q) ∧ (p ⟶ r) ⟹ p ⟶ q ∧ r"
apply (rule impI)
apply (rule conjI)
apply (drule conjunct1)
apply (drule mp)
apply assumption
apply assumption
apply (drule conjunct2)
apply (drule mp)
apply assumption
apply assumption
done

text ‹ ---------------------------------------------------------------
Ejercicio 20. Demostrar
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
------------------------------------------------------------------ ›

lemma ejercicio_20a:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof (rule conjI)
show "p ⟶ q"
proof (rule impI)
assume "p"
with `p ⟶ q ∧ r` have "q ∧ r" ..
then show "q" ..
qed
show "p ⟶ r"
proof (rule impI)
assume "p"
with `p ⟶ q ∧ r` have "q ∧ r" ..
then show "r" ..
qed
qed

lemma ejercicio_20c:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
using assms by auto

lemma ej20: "p ⟶ q ∧ r ⟹ (p ⟶ q) ∧ (p ⟶ r)"
apply (rule conjI)
apply (rule impI)
apply (drule mp)
apply assumption
apply (erule conjunct1)
apply (rule impI)
apply (drule mp)
apply assumption
apply (erule conjunct2)
done

text ‹ ---------------------------------------------------------------
Ejercicio 21. Demostrar
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ ›

lemma ejercicio_21a:
assumes "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
using assms by auto

lemma ejercicio_21b:
assumes "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
proof (rule impI)
assume "p ∧ q"
then have "p" ..
with `p ⟶ (q ⟶ r)` have "q ⟶ r" ..
have "q" using `p ∧ q` ..
with `q ⟶ r` show "r" ..
qed

lemma ejercicio_21c:
assumes "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
proof (rule impI)
assume "p ∧ q"
then have "p" ..
have "q" using `p ∧ q`..
have "q ⟶ r" using assms(1) `p` ..
then show "r" using `q` ..
qed

lemma ej21_1: "p ⟶ (q ⟶ r) ⟹ p ∧ q ⟶ r"
apply (rule impI)
apply (erule conjE)
apply (drule mp)
apply assumption
apply (drule mp)
apply assumption
apply assumption
done

text ‹ ---------------------------------------------------------------
Ejercicio 22. Demostrar
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ ›

lemma ejercicio_22a:
assumes "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof (rule impI)
assume "p"
show "q ⟶ r"
proof (rule impI)
assume "q"
with `p` have "p ∧ q" ..
with assms(1) show "r" ..
qed
qed

lemma ejercicio_22c:
assumes "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
using assms by auto

lemma ej22: "p ∧ q ⟶ r ⟹ p ⟶ (q ⟶ r)"
apply (rule impI)
apply (rule impI)
apply (drule mp)
apply (rule conjI)
apply assumption+
done

text ‹ ---------------------------------------------------------------
Ejercicio 23. Demostrar
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ ›

lemma ejercicio_23a:
assumes "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
proof (rule impI)
assume "p ∧ q"
then have "q" ..
have "p ⟶ q"
proof (rule impI)
assume "p"
show "q" using `q` .
qed
with assms(1) show "r" ..
qed

lemma ejercicio_23c:
assumes "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
using assms by auto

lemma ej23: "(p ⟶ q) ⟶ r ⟹ p ∧ q ⟶ r"
apply (rule impI)
apply (drule mp)
apply (rule impI)
apply (erule conjunct2)
apply assumption
done

text ‹ ---------------------------------------------------------------
Ejercicio 24. Demostrar
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
------------------------------------------------------------------ ›

lemma ejercicio_24b:
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
proof (rule impI)
assume "p ⟶ q"
have "p" using assms(1) ..
with `p ⟶ q` have "q" ..
have "q ⟶ r" using assms(1) ..
then show "r" using `q` ..
qed

lemma ejercicio_24c:
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
using assms by auto

lemma ej24: "p ∧ (q ⟶ r) ⟹ (p ⟶ q) ⟶ r"
apply (rule impI)
apply (erule conjE)
apply (drule mp)
apply assumption
apply (drule mp)
apply assumption+
done

end

</source>

← Revisión anterior	Revisión del 16:12 17 mar 2020
(Sin diferencias)

Rel 2 - Historial de revisiones

Mjoseh: Protegió «Rel 2» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « chapter ‹ R2: Deducción natural proposicional(I) › theory R2_sol imports Main begin text ‹ -------------------------------------…»