https://www.glc.us.es/~jalonso/DAO2012/api.php?action=feedcontributions&feedformat=atom&user=Dancapmer
Demostración asistida por ordenador (2012-13) - Contribuciones del usuario [es]
2026-07-18T23:42:04Z
Contribuciones del usuario
MediaWiki 1.31.14
https://www.glc.us.es/~jalonso/DAO2012/index.php?title=Relaci%C3%B3n_3&diff=111
Relación 3
2013-03-20T14:07:07Z
<p>Dancapmer: </p>
<hr />
<div><source lang="isar"><br />
header {* R3: Deducción natural proposicional *}<br />
<br />
theory R3<br />
imports Main <br />
begin<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
El objetivo de esta relación es demostrar cada uno de los ejercicios<br />
usando sólo las reglas básicas de deducción natural de la lógica<br />
proposicional (sin usar el método auto).<br />
<br />
Las reglas básicas de la deducción natural son las siguientes:<br />
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q<br />
· conjunct1: P ∧ Q ⟹ P<br />
· conjunct2: P ∧ Q ⟹ Q <br />
· notnotD: ¬¬ P ⟹ P<br />
· notnotI: P ⟹ ¬¬ P<br />
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q <br />
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F <br />
· impI: (P ⟹ Q) ⟹ P ⟶ Q<br />
· disjI1: P ⟹ P ∨ Q<br />
· disjI2: Q ⟹ P ∨ Q<br />
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R <br />
· FalseE: False ⟹ P<br />
· notE: ⟦¬P; P⟧ ⟹ R<br />
· notI: (P ⟹ False) ⟹ ¬P<br />
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q<br />
· iffD1: ⟦Q = P; Q⟧ ⟹ P <br />
· iffD2: ⟦P = Q; Q⟧ ⟹ P<br />
· ccontr: (¬P ⟹ False) ⟹ P<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
text {*<br />
Se usarán las reglas notnotI y mt que demostramos a continuación. *}<br />
<br />
lemma notnotI: "P ⟹ ¬¬ P"<br />
by auto<br />
<br />
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"<br />
by auto<br />
<br />
section {* Implicaciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 1. Demostrar<br />
p ⟶ q, p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_1a:<br />
assumes 1: "p ⟶ q" and<br />
2: "p"<br />
shows "q"<br />
proof -<br />
show 3: "q" using 1 2 by (rule mp) <br />
qed<br />
<br />
-- "Pedro"<br />
lemma ejercicio_1b:<br />
assumes "p ⟶ q"<br />
"p"<br />
shows "q"<br />
proof -<br />
show "q" using assms(1,2) by (rule mp)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 2. Demostrar<br />
p ⟶ q, q ⟶ r, p ⊢ r<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_2a:<br />
assumes 1:"p ⟶ q" and<br />
2:"q ⟶ r" and<br />
3:"p" <br />
shows "r"<br />
proof -<br />
have 4: "q" using 1 3 by (rule mp)<br />
show 5: "r" using 2 4 by (rule mp) <br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 3. Demostrar<br />
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_3a:<br />
assumes 1: "p ⟶ (q ⟶ r)" and<br />
2: "p ⟶ q" and<br />
3: "p" <br />
shows "r"<br />
proof -<br />
have 4: "q ⟶ r" using 1 3 by (rule mp)<br />
have 5: "q" using 2 3 by (rule mp)<br />
show 6: "r" using 4 5 by (rule mp)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 4. Demostrar<br />
p ⟶ q, q ⟶ r ⊢ p ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_4a:<br />
assumes 1: "p ⟶ q" and<br />
2: "q ⟶ r" <br />
shows "p ⟶ r"<br />
proof -<br />
{assume 3:"p" <br />
have 4: "q" using 1 3 by (rule mp)<br />
have 5: "r" using 2 4 by (rule mp)}<br />
thus "p ⟶ r" by (rule impI)<br />
qed<br />
<br />
-- "Pedro"<br />
lemma ejercicio_4d:<br />
assumes "p ⟶ q" and<br />
"q ⟶ r" <br />
shows "p ⟶ r"<br />
using assms by auto<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 5. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_5a:<br />
assumes 1: "p ⟶ (q ⟶ r)" <br />
shows "q ⟶ (p ⟶ r)"<br />
proof -<br />
{assume 3: "q"<br />
{assume 4: "p"<br />
have "q ⟶ r" using 1 4 ..<br />
hence 5: "r" using 3 ..}<br />
hence 6: "p ⟶ r" by (rule impI)}<br />
thus "q ⟶ (p ⟶ r)" by (rule impI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 6. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_6a:<br />
assumes 1: "p ⟶ (q ⟶ r)" <br />
shows "(p ⟶ q) ⟶ (p ⟶ r)"<br />
proof -<br />
{assume 2: "p ⟶ q"<br />
{assume 3: "p"<br />
have 4: "q ⟶ r" using 1 3 ..<br />
have 5: "q" using 2 3 ..<br />
have "r" using 4 5 ..}<br />
hence "p ⟶ r" by (rule impI)}<br />
thus "(p ⟶ q) ⟶ (p ⟶ r)" by (rule impI)<br />
qed <br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 7. Demostrar<br />
p ⊢ q ⟶ p<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_7a:<br />
assumes "p" <br />
shows "q ⟶ p"<br />
proof -<br />
{assume 1: "q"}<br />
show "q ⟶ p" using assms(1) by (rule impI)<br />
qed<br />
<br />
-- "Dani"<br />
lemma ejercicio_7b:<br />
assumes "p" <br />
shows "q ⟶ p"<br />
proof<br />
assume "q"<br />
show "p" using assms(1) .<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 8. Demostrar<br />
⊢ p ⟶ (q ⟶ p)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Dani"<br />
lemma ejercicio_8a:<br />
"p ⟶ (q ⟶ p)"<br />
proof<br />
assume "p"<br />
show "q ⟶ p"<br />
proof<br />
assume "q"<br />
show "p" using `p` .<br />
qed<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 9. Demostrar<br />
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_9:<br />
assumes 1: "p ⟶ q"<br />
shows "(q ⟶ r) ⟶ (p ⟶ r)"<br />
proof- <br />
{assume 2: "q ⟶ r"<br />
{assume 3: "p"<br />
have 4: "q" using 1 3 by (rule mp)<br />
have 5: "r" using 2 4 by (rule mp)}<br />
hence 6: "p ⟶ r" by (rule impI)}<br />
thus "(q ⟶ r) ⟶ (p ⟶ r)" by (rule impI)<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 10. Demostrar<br />
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_10:<br />
assumes "p ⟶ (q ⟶ (r ⟶ s))" <br />
shows "r ⟶ (q ⟶ (p ⟶ s))"<br />
proof <br />
assume "r"<br />
show "q⟶ (p⟶ s)" <br />
proof <br />
assume "q"<br />
show "p⟶ s"<br />
proof<br />
assume "p"<br />
with assms have "q⟶ r⟶ s" ..<br />
hence "r⟶ s" using `q` ..<br />
thus "s" using `r`..<br />
qed<br />
qed <br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 11. Demostrar<br />
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_11a:<br />
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"<br />
lemma ejercicio_11:<br />
shows "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"<br />
proof<br />
assume 1: "p ⟶ (q ⟶ r)"<br />
show 2: "(p ⟶ q) ⟶ (p ⟶ r)"<br />
proof <br />
assume 3: "p⟶ q"<br />
show 4: "p⟶ r" <br />
proof <br />
assume 5: "p"<br />
have 6: "q" using 3 5 by (rule mp)<br />
have 7:"q⟶ r" using 1 5 by (rule mp)<br />
show 8: "r" using 7 6 ..<br />
qed<br />
qed <br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 12. Demostrar<br />
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_12:<br />
assumes "(p ⟶ q) ⟶ r" <br />
shows "p ⟶ (q ⟶ r)"<br />
oops<br />
<br />
section {* Conjunciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 13. Demostrar<br />
p, q ⊢ p ∧ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_13:<br />
assumes 1:"p" and<br />
2:"q" <br />
shows "p ∧ q"<br />
proof -<br />
show "p ∧ q" using 1 2 by (rule conjI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 14. Demostrar<br />
p ∧ q ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_14:<br />
assumes "p ∧ q" <br />
shows "p"<br />
proof -<br />
show "p" using assms by (rule conjunct1)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 15. Demostrar<br />
p ∧ q ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_15:<br />
assumes "p ∧ q" <br />
shows "q"<br />
proof -<br />
show "q" using assms by (rule conjunct2)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 16. Demostrar<br />
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_16a:<br />
assumes "p ∧ (q ∧ r)"<br />
shows "(p ∧ q)∧ r"<br />
proof -<br />
have 1: "p" using assms by (rule conjunct1)<br />
have 2: "(q ∧ r)" using assms by (rule conjunct2)<br />
have 3: "q" using 2 by (rule conjunct1)<br />
have 4: "r" using 2 by (rule conjunct2)<br />
have 5: "(p∧q)" using 1 3 by (rule conjI)<br />
show 6: "(p∧q) ∧ r" using 5 4 by (rule conjI)<br />
qed<br />
<br />
-- Dani (No estoy seguro de si el ejercicio hecho por Pedro funciona)<br />
lemma ejercicio_16b:<br />
assumes "p ∧ (q ∧ r)"<br />
shows "(p ∧ q) ∧ r"<br />
proof<br />
have "p" using assms(1) by (rule conjunct1)<br />
have "q ∧ r" using assms(1) by (rule conjunct2)<br />
hence "q" by (rule conjunct1)<br />
show "p ∧ q" using `p` `q` by (rule conjI)<br />
next<br />
have "q ∧ r" using assms(1) by (rule conjunct2)<br />
thus "r" ..<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 17. Demostrar<br />
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_17:<br />
assumes "(p∧ q) ∧ r" <br />
shows "p ∧ (q∧ r)"<br />
proof -<br />
have 1: "r" using assms by (rule conjunct2)<br />
have 2: "(p∧q)" using assms by (rule conjunct1)<br />
have 3: "p" using 2 by (rule conjunct1)<br />
have 4: "q" using 2 by (rule conjunct2)<br />
have 5: "(q∧r)" using 4 1 by (rule conjI)<br />
show 6: "p∧(q∧r)" using 3 5 by (rule conjI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 18. Demostrar<br />
p ∧ q ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_18:<br />
assumes "p ∧ q" <br />
shows "p ⟶ q"<br />
proof -<br />
have 1: "q" using assms by (rule conjunct2)<br />
show "p⟶ q" using 1 by (rule impI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 19. Demostrar<br />
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r <br />
------------------------------------------------------------------ *}<br />
<br />
<br />
-- "Pedro"<br />
lemma ejercicio_19:<br />
assumes 1: "(p ⟶ q) ∧ (p ⟶ r)" <br />
shows "p ⟶ (q ∧ r)"<br />
proof (rule impI)<br />
assume 2: "p"<br />
have 3: "p ⟶ q" using assms by (rule conjunct1)<br />
have 4: "q" using 3 2 by (rule mp)<br />
have 5: "p ⟶ r" using assms by (rule conjunct2)<br />
have 6: "r" using 5 2 by (rule mp)<br />
show "q ∧ r" using 4 6 by (rule conjI)<br />
qed<br />
<br />
<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 20. Demostrar<br />
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_20:<br />
assumes "p ⟶ q ∧ r" <br />
shows "(p ⟶ q) ∧ (p ⟶ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 21. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_21a:<br />
assumes 1:"p ⟶ (q ⟶ r)" <br />
shows "p ∧ q ⟶ r"<br />
proof<br />
assume 2:"p∧q"<br />
show "r" <br />
proof -<br />
have 3: "p" using 2 by (rule conjunct1)<br />
have 4: "q" using 2 ..<br />
have 5: "(q⟶ r)" using 1 3 ..<br />
show 6: "r" using 5 4 ..<br />
qed<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 22. Demostrar<br />
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_22a:<br />
assumes "p ∧ q ⟶ r" <br />
shows "p ⟶ (q ⟶ r)"<br />
proof<br />
assume "p"<br />
show "q⟶ r"<br />
proof<br />
assume "q"<br />
have "p∧q" using `p` `q` ..<br />
show "r" using assms `p∧q`..<br />
qed<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 23. Demostrar<br />
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_23a:<br />
assumes 1:"(p ⟶ q) ⟶ r" <br />
shows "p ∧ q ⟶ r" <br />
proof <br />
assume 2:"p∧q"<br />
hence 3:"p" ..<br />
have 4:"q" using 2 ..<br />
hence 5: "p⟶ q" ..<br />
show"r" using 1 5 by (rule mp)<br />
qed<br />
<br />
-- Dani<br />
lemma ejercicio_23b:<br />
assumes "(p ⟶ q) ⟶ r" <br />
shows "p ∧ q ⟶ r"<br />
proof<br />
assume "p ∧ q"<br />
hence p ..<br />
have q using `p ∧ q` ..<br />
hence "p ⟶ q" ..<br />
with assms(1) show "r" ..<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 24. Demostrar<br />
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
-- Dani<br />
lemma ejercicio_24a:<br />
assumes "p ∧ (q ⟶ r)" <br />
shows "(p ⟶ q) ⟶ r"<br />
proof<br />
assume "p ⟶ q"<br />
have "p" using assms(1) ..<br />
with `p ⟶ q` have "q" ..<br />
have "q ⟶ r" using assms(1) ..<br />
thus "r" using `q` ..<br />
qed<br />
<br />
<br />
section {* Disyunciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 25. Demostrar<br />
p ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_25:<br />
assumes "p"<br />
shows "p ∨ q"<br />
proof -<br />
show "p∨q" using assms by (rule disjI1)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 26. Demostrar<br />
q ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_26:<br />
assumes "q"<br />
shows "p ∨ q"<br />
proof -<br />
show "p∨q" using assms by (rule disjI2)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 27. Demostrar<br />
p ∨ q ⊢ q ∨ p<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_27:<br />
assumes "p ∨ q"<br />
shows "q ∨ p"<br />
proof - <br />
have "p ∨ q" using assms by this<br />
moreover<br />
{ assume 2: "p"<br />
have "q ∨ p" using 2 by (rule disjI2) }<br />
moreover<br />
{ assume 3: "q"<br />
have "q ∨ p" using 3 by (rule disjI1) }<br />
ultimately show "q ∨ p" by (rule disjE) <br />
qed <br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 28. Demostrar<br />
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r<br />
------------------------------------------------------------------ *}<br />
-- "Pedro"<br />
lemma ejercicio_28a:<br />
assumes "q ⟶ r" <br />
shows "p ∨ q ⟶ p ∨ r"<br />
proof <br />
assume 1: "p∨q"<br />
moreover<br />
{assume "p"<br />
hence "p∨r" by (rule disjI1)}<br />
moreover<br />
{assume "q"<br />
have "r" using assms `q`..<br />
hence "p∨r" ..}<br />
ultimately<br />
show "p∨r" ..<br />
qed <br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 29. Demostrar<br />
p ∨ p ⊢ p<br />
------------------------------------------------------------------ *}<br />
-- "Pedro Ros"<br />
lemma ejercicio_29a:<br />
assumes "p ∨ p"<br />
shows "p"<br />
<br />
proof-<br />
have "p∨p" using assms by this<br />
moreover<br />
{assume "p"<br />
hence "p" by this}<br />
moreover<br />
{assume "p"<br />
hence "p" by this}<br />
ultimately<br />
show "p" ..<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 30. Demostrar<br />
p ⊢ p ∨ p<br />
------------------------------------------------------------------ *}<br />
-- "Pedro Ros"<br />
lemma ejercicio_30a:<br />
assumes "p" <br />
shows "p ∨ p"<br />
proof -<br />
show "p∨p" using assms ..<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 31. Demostrar<br />
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_31a:<br />
assumes "p ∨ (q ∨ r)" <br />
shows "(p ∨ q) ∨ r"<br />
proof -<br />
have 1: "p ∨ (q ∨ r)" using assms by this<br />
moreover<br />
{assume "p"<br />
hence "(p∨q)" ..<br />
hence "(p∨q)∨r" ..}<br />
moreover<br />
{assume "(q∨r)"<br />
moreover<br />
{assume "q"<br />
hence "(p∨q)"..<br />
hence "(p∨q)∨r" ..}<br />
moreover<br />
{assume "r"<br />
hence "(p∨q)∨r" ..}<br />
ultimately<br />
have "(p∨q)∨r"..}<br />
ultimately<br />
show "(p∨q)∨r" ..<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 32. Demostrar<br />
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_32:<br />
assumes "(p ∨ q) ∨ r" <br />
shows "p ∨ (q ∨ r)"<br />
using assms(1)<br />
proof<br />
assume "p∨q"<br />
thus "p∨q∨r" <br />
proof<br />
assume "p"<br />
thus "p∨q∨r" ..<br />
next<br />
assume "q"<br />
hence "q∨r" ..<br />
thus "p∨q∨r" ..<br />
qed<br />
next<br />
assume "r"<br />
hence "q∨r" ..<br />
thus "p∨q∨r" ..<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 33. Demostrar<br />
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)<br />
------------------------------------------------------------------ *}<br />
-- "Pedro"<br />
lemma ejercicio_33a:<br />
assumes "p ∧ (q ∨ r)" <br />
shows "(p ∧ q) ∨ (p ∧ r)"<br />
proof -<br />
have 1: "p" using assms ..<br />
have 2: "q∨r" using assms ..<br />
moreover<br />
{assume 3: "q"<br />
have "(p∧q)" using 1 3 ..<br />
hence "(p ∧ q) ∨ (p ∧ r)" ..}<br />
moreover<br />
{assume 4: "r"<br />
have "p∧r" using 1 4 ..<br />
hence "(p ∧ q) ∨ (p ∧ r)" ..}<br />
ultimately<br />
show "(p ∧ q) ∨ (p ∧ r)" ..<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 34. Demostrar<br />
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)<br />
------------------------------------------------------------------ *}<br />
-- "Pedro Ros"<br />
lemma ejercicio_34a:<br />
assumes "(p ∧ q) ∨ (p ∧ r)" <br />
shows "p ∧ (q ∨ r)"<br />
proof -<br />
have 1: "(p ∧ q) ∨ (p ∧ r)" using assms by this<br />
moreover<br />
{assume "(p ∧ q)"<br />
hence "p" ..<br />
have "q" using `p ∧ q` ..<br />
hence "(q∨r)"..<br />
have "p∧(q∨r)" using `p``(q∨r)`..}<br />
moreover<br />
{assume "(p∧r)"<br />
hence "p" ..<br />
have "r" using `p ∧ r` ..<br />
hence "(q∨r)"..<br />
have "p∧(q∨r)" using `p``(q∨r)`..}<br />
ultimately<br />
show "p ∧ (q ∨ r)" ..<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 35. Demostrar<br />
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)<br />
------------------------------------------------------------------ *}<br />
-- "Pedro Ros"<br />
lemma ejercicio_35a:<br />
assumes "p ∨ (q ∧ r)" <br />
shows "(p ∨ q) ∧ (p ∨ r)"<br />
proof -<br />
have 1: "p ∨ (q ∧ r)" using assms by this<br />
moreover<br />
{assume "p"<br />
hence 2: "(p∨q)" ..<br />
have 3: "(p∨r)" using `p` ..<br />
have 4: "(p ∨ q) ∧ (p ∨ r)" using 2 3 ..}<br />
moreover<br />
{assume 5:"(q∧r)"<br />
hence 6: "q" ..<br />
have 7: "r" using 5 ..<br />
have 8: "p∨q" using 6 ..<br />
have 9: "p∨r" using 7 ..<br />
have "(p ∨ q) ∧ (p ∨ r)"using 8 9 ..}<br />
ultimately<br />
show "(p ∨ q) ∧ (p ∨ r)" ..<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 36. Demostrar<br />
(p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)<br />
------------------------------------------------------------------ *}<br />
text {* Pedro. Vienen demostradas en la teoría y necesito usarlas *}<br />
<br />
lemma or2: "⟦P∨Q; ¬P⟧⟹ Q"<br />
by auto<br />
<br />
lemma LEM: "P ∨ ¬P"<br />
by auto<br />
<br />
lemma ejercicio_36a:<br />
assumes "(p ∨ q) ∧ (p ∨ r)"<br />
shows "p ∨ (q ∧ r)"<br />
using LEM<br />
proof <br />
have 1:"(p∨q)" using assms ..<br />
have 2: "(p∨r)" using assms ..<br />
assume "p"<br />
thus "p∨(q∧r)" ..<br />
next<br />
have 1:"(p∨q)" using assms ..<br />
have 2: "(p∨r)" using assms ..<br />
assume "¬p"<br />
have "q" using 1 `¬p` by (rule or2)<br />
have "r" using 2 `¬p` by (rule or2)<br />
have "q∧r" using `q` `r` ..<br />
thus "p∨(q∧r)" .. <br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 37. Demostrar<br />
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_37a:<br />
assumes "(p ⟶ r) ∧ (q ⟶ r)" <br />
shows "p ∨ q ⟶ r"<br />
proof (rule impI)<br />
assume 0:"p∨q"<br />
show "r"<br />
proof (rule disjE)<br />
show "p∨q" using 0 .<br />
next<br />
assume p<br />
have 1: "p⟶r" using assms ..<br />
thus r using `p` ..<br />
next<br />
assume q<br />
have 2: "q⟶r" using assms ..<br />
thus r using `q`..<br />
qed<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 38. Demostrar<br />
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
<br />
-- Dani<br />
lemma ejercicio_38:<br />
assumes "p ∨ q ⟶ r" <br />
shows "(p ⟶ r) ∧ (q ⟶ r)"<br />
proof<br />
show "p ⟶ r"<br />
proof<br />
assume p<br />
hence "p ∨ q" ..<br />
with assms show r ..<br />
qed<br />
next<br />
show "q ⟶ r"<br />
proof<br />
assume q<br />
hence "p ∨ q" ..<br />
with assms show r ..<br />
qed<br />
qed<br />
<br />
section {* Negaciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 39. Demostrar<br />
p ⊢ ¬¬p<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_39:<br />
assumes "p"<br />
shows "¬¬p"<br />
proof -<br />
show "¬¬p" using assms by (rule notnotI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 40. Demostrar<br />
¬p ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_40:<br />
assumes "¬p" <br />
shows "p ⟶ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 41. Demostrar<br />
p ⟶ q ⊢ ¬q ⟶ ¬p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_41:<br />
assumes "p ⟶ q"<br />
shows "¬q ⟶ ¬p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 42. Demostrar<br />
p∨q, ¬q ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_42:<br />
assumes "p∨q"<br />
"¬q" <br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 42. Demostrar<br />
p ∨ q, ¬p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_43:<br />
assumes "p ∨ q"<br />
"¬p" <br />
shows "q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 40. Demostrar<br />
p ∨ q ⊢ ¬(¬p ∧ ¬q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_44:<br />
assumes "p ∨ q" <br />
shows "¬(¬p ∧ ¬q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 45. Demostrar<br />
p ∧ q ⊢ ¬(¬p ∨ ¬q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_45:<br />
assumes "p ∧ q" <br />
shows "¬(¬p ∨ ¬q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 46. Demostrar<br />
¬(p ∨ q) ⊢ ¬p ∧ ¬q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_46:<br />
assumes "¬(p ∨ q)" <br />
shows "¬p ∧ ¬q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 47. Demostrar<br />
¬p ∧ ¬q ⊢ ¬(p ∨ q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_47:<br />
assumes "¬p ∧ ¬q" <br />
shows "¬(p ∨ q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 48. Demostrar<br />
¬p ∨ ¬q ⊢ ¬(p ∧ q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_48:<br />
assumes "¬p ∨ ¬q"<br />
shows "¬(p ∧ q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 49. Demostrar<br />
⊢ ¬(p ∧ ¬p)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_49:<br />
"¬(p ∧ ¬p)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 50. Demostrar<br />
p ∧ ¬p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_50:<br />
assumes "p ∧ ¬p" <br />
shows "q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 51. Demostrar<br />
¬¬p ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_51:<br />
assumes "¬¬p"<br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 52. Demostrar<br />
⊢ p ∨ ¬p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_52:<br />
"p ∨ ¬p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 53. Demostrar<br />
⊢ ((p ⟶ q) ⟶ p) ⟶ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_53:<br />
"((p ⟶ q) ⟶ p) ⟶ p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 54. Demostrar<br />
¬q ⟶ ¬p ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_54:<br />
assumes "¬q ⟶ ¬p"<br />
shows "p ⟶ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 55. Demostrar<br />
¬(¬p ∧ ¬q) ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_55:<br />
assumes "¬(¬p ∧ ¬q)"<br />
shows "p ∨ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 56. Demostrar<br />
¬(¬p ∨ ¬q) ⊢ p ∧ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_56:<br />
assumes "¬(¬p ∨ ¬q)" <br />
shows "p ∧ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 57. Demostrar<br />
¬(p ∧ q) ⊢ ¬p ∨ ¬q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_57:<br />
assumes "¬(p ∧ q)"<br />
shows "¬p ∨ ¬q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 58. Demostrar<br />
⊢ (p ⟶ q) ∨ (q ⟶ p)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_58:<br />
"(p ⟶ q) ∨ (q ⟶ p)"<br />
oops<br />
<br />
end<br />
</source></div>
Dancapmer
https://www.glc.us.es/~jalonso/DAO2012/index.php?title=Relaci%C3%B3n_3&diff=100
Relación 3
2013-03-12T12:56:13Z
<p>Dancapmer: </p>
<hr />
<div><source lang="isar"><br />
header {* R3: Deducción natural proposicional *}<br />
<br />
theory R3<br />
imports Main <br />
begin<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
El objetivo de esta relación es demostrar cada uno de los ejercicios<br />
usando sólo las reglas básicas de deducción natural de la lógica<br />
proposicional (sin usar el método auto).<br />
<br />
Las reglas básicas de la deducción natural son las siguientes:<br />
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q<br />
· conjunct1: P ∧ Q ⟹ P<br />
· conjunct2: P ∧ Q ⟹ Q <br />
· notnotD: ¬¬ P ⟹ P<br />
· notnotI: P ⟹ ¬¬ P<br />
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q <br />
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F <br />
· impI: (P ⟹ Q) ⟹ P ⟶ Q<br />
· disjI1: P ⟹ P ∨ Q<br />
· disjI2: Q ⟹ P ∨ Q<br />
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R <br />
· FalseE: False ⟹ P<br />
· notE: ⟦¬P; P⟧ ⟹ R<br />
· notI: (P ⟹ False) ⟹ ¬P<br />
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q<br />
· iffD1: ⟦Q = P; Q⟧ ⟹ P <br />
· iffD2: ⟦P = Q; Q⟧ ⟹ P<br />
· ccontr: (¬P ⟹ False) ⟹ P<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
text {*<br />
Se usarán las reglas notnotI y mt que demostramos a continuación. *}<br />
<br />
lemma notnotI: "P ⟹ ¬¬ P"<br />
by auto<br />
<br />
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"<br />
by auto<br />
<br />
section {* Implicaciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 1. Demostrar<br />
p ⟶ q, p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_1a:<br />
assumes 1: "p ⟶ q" and<br />
2: "p"<br />
shows "q"<br />
proof -<br />
show 3: "q" using 1 2 by (rule mp) <br />
qed<br />
<br />
-- "Pedro"<br />
lemma ejercicio_1b:<br />
assumes "p ⟶ q"<br />
"p"<br />
shows "q"<br />
proof -<br />
show "q" using assms(1,2) by (rule mp)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 2. Demostrar<br />
p ⟶ q, q ⟶ r, p ⊢ r<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_2a:<br />
assumes 1:"p ⟶ q" and<br />
2:"q ⟶ r" and<br />
3:"p" <br />
shows "r"<br />
proof -<br />
have 4: "q" using 1 3 by (rule mp)<br />
show 5: "r" using 2 4 by (rule mp) <br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 3. Demostrar<br />
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_3a:<br />
assumes 1: "p ⟶ (q ⟶ r)" and<br />
2: "p ⟶ q" and<br />
3: "p" <br />
shows "r"<br />
proof -<br />
have 4: "q ⟶ r" using 1 3 by (rule mp)<br />
have 5: "q" using 2 3 by (rule mp)<br />
show 6: "r" using 4 5 by (rule mp)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 4. Demostrar<br />
p ⟶ q, q ⟶ r ⊢ p ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_4a:<br />
assumes 1: "p ⟶ q" and<br />
2: "q ⟶ r" <br />
shows "p ⟶ r"<br />
proof -<br />
{assume 3:"p" <br />
have 4: "q" using 1 3 by (rule mp)<br />
have 5: "r" using 2 4 by (rule mp)}<br />
thus "p ⟶ r" by (rule impI)<br />
qed<br />
<br />
-- "Pedro"<br />
lemma ejercicio_4d:<br />
assumes "p ⟶ q" and<br />
"q ⟶ r" <br />
shows "p ⟶ r"<br />
using assms by auto<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 5. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_5a:<br />
assumes 1: "p ⟶ (q ⟶ r)" <br />
shows "q ⟶ (p ⟶ r)"<br />
proof -<br />
{assume 3: "q"<br />
{assume 4: "p"<br />
have "q ⟶ r" using 1 4 ..<br />
hence 5: "r" using 3 ..}<br />
hence 6: "p ⟶ r" by (rule impI)}<br />
thus "q ⟶ (p ⟶ r)" by (rule impI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 6. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_6a:<br />
assumes 1: "p ⟶ (q ⟶ r)" <br />
shows "(p ⟶ q) ⟶ (p ⟶ r)"<br />
proof -<br />
{assume 2: "p ⟶ q"<br />
{assume 3: "p"<br />
have 4: "q ⟶ r" using 1 3 ..<br />
have 5: "q" using 2 3 ..<br />
have "r" using 4 5 ..}<br />
hence "p ⟶ r" by (rule impI)}<br />
thus "(p ⟶ q) ⟶ (p ⟶ r)" by (rule impI)<br />
qed <br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 7. Demostrar<br />
p ⊢ q ⟶ p<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_7a:<br />
assumes "p" <br />
shows "q ⟶ p"<br />
proof -<br />
{assume 1: "q"}<br />
show "q ⟶ p" using assms(1) by (rule impI)<br />
qed<br />
<br />
-- "Dani"<br />
lemma ejercicio_7b:<br />
assumes "p" <br />
shows "q ⟶ p"<br />
proof<br />
assume "q"<br />
show "p" using assms(1) .<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 8. Demostrar<br />
⊢ p ⟶ (q ⟶ p)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Dani"<br />
lemma ejercicio_8a:<br />
"p ⟶ (q ⟶ p)"<br />
proof<br />
assume "p"<br />
show "q ⟶ p"<br />
proof<br />
assume "q"<br />
show "p" using `p` .<br />
qed<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 9. Demostrar<br />
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_9:<br />
assumes 1: "p ⟶ q"<br />
shows "(q ⟶ r) ⟶ (p ⟶ r)"<br />
proof- <br />
{assume 2: "q ⟶ r"<br />
{assume 3: "p"<br />
have 4: "q" using 1 3 by (rule mp)<br />
have 5: "r" using 2 4 by (rule mp)}<br />
hence 6: "p ⟶ r" by (rule impI)}<br />
thus "(q ⟶ r) ⟶ (p ⟶ r)" by (rule impI)<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 10. Demostrar<br />
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_10:<br />
assumes "p ⟶ (q ⟶ (r ⟶ s))" <br />
shows "r ⟶ (q ⟶ (p ⟶ s))"<br />
proof <br />
assume "r"<br />
show "q⟶ (p⟶ s)" <br />
proof <br />
assume "q"<br />
show "p⟶ s"<br />
proof<br />
assume "p"<br />
with assms have "q⟶ r⟶ s" ..<br />
hence "r⟶ s" using `q` ..<br />
thus "s" using `r`..<br />
qed<br />
qed <br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 11. Demostrar<br />
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_11a:<br />
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"<br />
lemma ejercicio_11:<br />
shows "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"<br />
proof<br />
assume 1: "p ⟶ (q ⟶ r)"<br />
show 2: "(p ⟶ q) ⟶ (p ⟶ r)"<br />
proof <br />
assume 3: "p⟶ q"<br />
show 4: "p⟶ r" <br />
proof <br />
assume 5: "p"<br />
have 6: "q" using 3 5 by (rule mp)<br />
have 7:"q⟶ r" using 1 5 by (rule mp)<br />
show 8: "r" using 7 6 ..<br />
qed<br />
qed <br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 12. Demostrar<br />
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_12:<br />
assumes "(p ⟶ q) ⟶ r" <br />
shows "p ⟶ (q ⟶ r)"<br />
oops<br />
<br />
section {* Conjunciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 13. Demostrar<br />
p, q ⊢ p ∧ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_13:<br />
assumes 1:"p" and<br />
2:"q" <br />
shows "p ∧ q"<br />
proof -<br />
show "p ∧ q" using 1 2 by (rule conjI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 14. Demostrar<br />
p ∧ q ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_14:<br />
assumes "p ∧ q" <br />
shows "p"<br />
proof -<br />
show "p" using assms by (rule conjunct1)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 15. Demostrar<br />
p ∧ q ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_15:<br />
assumes "p ∧ q" <br />
shows "q"<br />
proof -<br />
show "q" using assms by (rule conjunct2)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 16. Demostrar<br />
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_16a:<br />
assumes "p ∧ (q ∧ r)"<br />
shows "(p ∧ q)∧ r"<br />
proof -<br />
have 1: "p" using assms by (rule conjunct1)<br />
have 2: "(q ∧ r)" using assms by (rule conjunct2)<br />
have 3: "q" using 2 by (rule conjunct1)<br />
have 4: "r" using 2 by (rule conjunct2)<br />
have 5: "(p∧q)" using 1 3 by (rule conjI)<br />
show 6: "(p∧q) ∧ r" using 5 4 by (rule conjI)<br />
qed<br />
<br />
-- Dani (No estoy seguro de si el ejercicio hecho por Pedro funciona)<br />
lemma ejercicio_16b:<br />
assumes "p ∧ (q ∧ r)"<br />
shows "(p ∧ q) ∧ r"<br />
proof<br />
have "p" using assms(1) by (rule conjunct1)<br />
have "q ∧ r" using assms(1) by (rule conjunct2)<br />
hence "q" by (rule conjunct1)<br />
show "p ∧ q" using `p` `q` by (rule conjI)<br />
next<br />
have "q ∧ r" using assms(1) by (rule conjunct2)<br />
thus "r" ..<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 17. Demostrar<br />
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_17:<br />
assumes "(p∧ q) ∧ r" <br />
shows "p ∧ (q∧ r)"<br />
proof -<br />
have 1: "r" using assms by (rule conjunct2)<br />
have 2: "(p∧q)" using assms by (rule conjunct1)<br />
have 3: "p" using 2 by (rule conjunct1)<br />
have 4: "q" using 2 by (rule conjunct2)<br />
have 5: "(q∧r)" using 4 1 by (rule conjI)<br />
show 6: "p∧(q∧r)" using 3 5 by (rule conjI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 18. Demostrar<br />
p ∧ q ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_18:<br />
assumes "p ∧ q" <br />
shows "p ⟶ q"<br />
proof -<br />
have 1: "q" using assms by (rule conjunct2)<br />
show "p⟶ q" using 1 by (rule impI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 19. Demostrar<br />
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r <br />
------------------------------------------------------------------ *}<br />
<br />
<br />
-- "Pedro"<br />
lemma ejercicio_19:<br />
assumes 1: "(p ⟶ q) ∧ (p ⟶ r)" <br />
shows "p ⟶ (q ∧ r)"<br />
proof (rule impI)<br />
assume 2: "p"<br />
have 3: "p ⟶ q" using assms by (rule conjunct1)<br />
have 4: "q" using 3 2 by (rule mp)<br />
have 5: "p ⟶ r" using assms by (rule conjunct2)<br />
have 6: "r" using 5 2 by (rule mp)<br />
show "q ∧ r" using 4 6 by (rule conjI)<br />
qed<br />
<br />
<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 20. Demostrar<br />
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_20:<br />
assumes "p ⟶ q ∧ r" <br />
shows "(p ⟶ q) ∧ (p ⟶ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 21. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_21a:<br />
assumes 1:"p ⟶ (q ⟶ r)" <br />
shows "p ∧ q ⟶ r"<br />
proof<br />
assume 2:"p∧q"<br />
show "r" <br />
proof -<br />
have 3: "p" using 2 by (rule conjunct1)<br />
have 4: "q" using 2 ..<br />
have 5: "(q⟶ r)" using 1 3 ..<br />
show 6: "r" using 5 4 ..<br />
qed<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 22. Demostrar<br />
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_22a:<br />
assumes "p ∧ q ⟶ r" <br />
shows "p ⟶ (q ⟶ r)"<br />
proof<br />
assume "p"<br />
show "q⟶ r"<br />
proof<br />
assume "q"<br />
have "p∧q" using `p` `q` ..<br />
show "r" using assms `p∧q`..<br />
qed<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 23. Demostrar<br />
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_23a:<br />
assumes 1:"(p ⟶ q) ⟶ r" <br />
shows "p ∧ q ⟶ r" <br />
proof <br />
assume 2:"p∧q"<br />
hence 3:"p" ..<br />
have 4:"q" using 2 ..<br />
hence 5: "p⟶ q" ..<br />
show"r" using 1 5 by (rule mp)<br />
qed<br />
<br />
-- Dani<br />
lemma ejercicio_23b:<br />
assumes "(p ⟶ q) ⟶ r" <br />
shows "p ∧ q ⟶ r"<br />
proof<br />
assume "p ∧ q"<br />
hence p ..<br />
have q using `p ∧ q` ..<br />
hence "p ⟶ q" ..<br />
with assms(1) show "r" ..<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 24. Demostrar<br />
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
-- Dani<br />
lemma ejercicio_24a:<br />
assumes "p ∧ (q ⟶ r)" <br />
shows "(p ⟶ q) ⟶ r"<br />
proof<br />
assume "p ⟶ q"<br />
have "p" using assms(1) ..<br />
with `p ⟶ q` have "q" ..<br />
have "q ⟶ r" using assms(1) ..<br />
thus "r" using `q` ..<br />
qed<br />
<br />
section {* Disyunciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 25. Demostrar<br />
p ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_25:<br />
assumes "p"<br />
shows "p ∨ q"<br />
proof -<br />
show "p∨q" using assms by (rule disjI1)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 26. Demostrar<br />
q ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_26:<br />
assumes "q"<br />
shows "p ∨ q"<br />
proof -<br />
show "p∨q" using assms by (rule disjI2)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 27. Demostrar<br />
p ∨ q ⊢ q ∨ p<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_27:<br />
assumes "p ∨ q"<br />
shows "q ∨ p"<br />
proof - <br />
have "p ∨ q" using assms by this<br />
moreover<br />
{ assume 2: "p"<br />
have "q ∨ p" using 2 by (rule disjI2) }<br />
moreover<br />
{ assume 3: "q"<br />
have "q ∨ p" using 3 by (rule disjI1) }<br />
ultimately show "q ∨ p" by (rule disjE) <br />
qed <br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 28. Demostrar<br />
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_28:<br />
assumes "q ⟶ r" <br />
shows "p ∨ q ⟶ p ∨ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 29. Demostrar<br />
p ∨ p ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_29:<br />
assumes "p ∨ p"<br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 30. Demostrar<br />
p ⊢ p ∨ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_30:<br />
assumes "p" <br />
shows "p ∨ p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 31. Demostrar<br />
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_31:<br />
assumes "p ∨ (q ∨ r)" <br />
shows "(p ∨ q) ∨ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 32. Demostrar<br />
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_32:<br />
assumes "(p ∨ q) ∨ r" <br />
shows "p ∨ (q ∨ r)"<br />
using assms(1)<br />
proof<br />
assume "p∨q"<br />
thus "p∨q∨r" <br />
proof<br />
assume "p"<br />
thus "p∨q∨r" ..<br />
next<br />
assume "q"<br />
hence "q∨r" ..<br />
thus "p∨q∨r" ..<br />
qed<br />
next<br />
assume "r"<br />
hence "q∨r" ..<br />
thus "p∨q∨r" ..<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 33. Demostrar<br />
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_33:<br />
assumes "p ∧ (q ∨ r)" <br />
shows "(p ∧ q) ∨ (p ∧ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 34. Demostrar<br />
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_34:<br />
assumes "(p ∧ q) ∨ (p ∧ r)" <br />
shows "p ∧ (q ∨ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 35. Demostrar<br />
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_35:<br />
assumes "p ∨ (q ∧ r)" <br />
shows "(p ∨ q) ∧ (p ∨ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 36. Demostrar<br />
(p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_36:<br />
assumes "(p ∨ q) ∧ (p ∨ r)"<br />
shows "p ∨ (q ∧ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 37. Demostrar<br />
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_37:<br />
assumes "(p ⟶ r) ∧ (q ⟶ r)" <br />
shows "p ∨ q ⟶ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 38. Demostrar<br />
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_38:<br />
assumes "p ∨ q ⟶ r" <br />
shows "(p ⟶ r) ∧ (q ⟶ r)"<br />
oops<br />
<br />
section {* Negaciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 39. Demostrar<br />
p ⊢ ¬¬p<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_39:<br />
assumes "p"<br />
shows "¬¬p"<br />
proof -<br />
show "¬¬p" using assms by (rule notnotI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 40. Demostrar<br />
¬p ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_40:<br />
assumes "¬p" <br />
shows "p ⟶ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 41. Demostrar<br />
p ⟶ q ⊢ ¬q ⟶ ¬p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_41:<br />
assumes "p ⟶ q"<br />
shows "¬q ⟶ ¬p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 42. Demostrar<br />
p∨q, ¬q ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_42:<br />
assumes "p∨q"<br />
"¬q" <br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 42. Demostrar<br />
p ∨ q, ¬p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_43:<br />
assumes "p ∨ q"<br />
"¬p" <br />
shows "q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 40. Demostrar<br />
p ∨ q ⊢ ¬(¬p ∧ ¬q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_44:<br />
assumes "p ∨ q" <br />
shows "¬(¬p ∧ ¬q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 45. Demostrar<br />
p ∧ q ⊢ ¬(¬p ∨ ¬q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_45:<br />
assumes "p ∧ q" <br />
shows "¬(¬p ∨ ¬q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 46. Demostrar<br />
¬(p ∨ q) ⊢ ¬p ∧ ¬q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_46:<br />
assumes "¬(p ∨ q)" <br />
shows "¬p ∧ ¬q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 47. Demostrar<br />
¬p ∧ ¬q ⊢ ¬(p ∨ q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_47:<br />
assumes "¬p ∧ ¬q" <br />
shows "¬(p ∨ q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 48. Demostrar<br />
¬p ∨ ¬q ⊢ ¬(p ∧ q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_48:<br />
assumes "¬p ∨ ¬q"<br />
shows "¬(p ∧ q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 49. Demostrar<br />
⊢ ¬(p ∧ ¬p)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_49:<br />
"¬(p ∧ ¬p)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 50. Demostrar<br />
p ∧ ¬p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_50:<br />
assumes "p ∧ ¬p" <br />
shows "q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 51. Demostrar<br />
¬¬p ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_51:<br />
assumes "¬¬p"<br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 52. Demostrar<br />
⊢ p ∨ ¬p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_52:<br />
"p ∨ ¬p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 53. Demostrar<br />
⊢ ((p ⟶ q) ⟶ p) ⟶ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_53:<br />
"((p ⟶ q) ⟶ p) ⟶ p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 54. Demostrar<br />
¬q ⟶ ¬p ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_54:<br />
assumes "¬q ⟶ ¬p"<br />
shows "p ⟶ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 55. Demostrar<br />
¬(¬p ∧ ¬q) ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_55:<br />
assumes "¬(¬p ∧ ¬q)"<br />
shows "p ∨ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 56. Demostrar<br />
¬(¬p ∨ ¬q) ⊢ p ∧ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_56:<br />
assumes "¬(¬p ∨ ¬q)" <br />
shows "p ∧ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 57. Demostrar<br />
¬(p ∧ q) ⊢ ¬p ∨ ¬q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_57:<br />
assumes "¬(p ∧ q)"<br />
shows "¬p ∨ ¬q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 58. Demostrar<br />
⊢ (p ⟶ q) ∨ (q ⟶ p)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_58:<br />
"(p ⟶ q) ∨ (q ⟶ p)"<br />
oops<br />
<br />
end<br />
</source></div>
Dancapmer
https://www.glc.us.es/~jalonso/DAO2012/index.php?title=Relaci%C3%B3n_3&diff=99
Relación 3
2013-03-12T11:59:56Z
<p>Dancapmer: </p>
<hr />
<div><source lang="isar"><br />
header {* R3: Deducción natural proposicional *}<br />
<br />
theory R3<br />
imports Main <br />
begin<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
El objetivo de esta relación es demostrar cada uno de los ejercicios<br />
usando sólo las reglas básicas de deducción natural de la lógica<br />
proposicional (sin usar el método auto).<br />
<br />
Las reglas básicas de la deducción natural son las siguientes:<br />
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q<br />
· conjunct1: P ∧ Q ⟹ P<br />
· conjunct2: P ∧ Q ⟹ Q <br />
· notnotD: ¬¬ P ⟹ P<br />
· notnotI: P ⟹ ¬¬ P<br />
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q <br />
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F <br />
· impI: (P ⟹ Q) ⟹ P ⟶ Q<br />
· disjI1: P ⟹ P ∨ Q<br />
· disjI2: Q ⟹ P ∨ Q<br />
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R <br />
· FalseE: False ⟹ P<br />
· notE: ⟦¬P; P⟧ ⟹ R<br />
· notI: (P ⟹ False) ⟹ ¬P<br />
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q<br />
· iffD1: ⟦Q = P; Q⟧ ⟹ P <br />
· iffD2: ⟦P = Q; Q⟧ ⟹ P<br />
· ccontr: (¬P ⟹ False) ⟹ P<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
text {*<br />
Se usarán las reglas notnotI y mt que demostramos a continuación. *}<br />
<br />
lemma notnotI: "P ⟹ ¬¬ P"<br />
by auto<br />
<br />
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"<br />
by auto<br />
<br />
section {* Implicaciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 1. Demostrar<br />
p ⟶ q, p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_1a:<br />
assumes 1: "p ⟶ q" and<br />
2: "p"<br />
shows "q"<br />
proof -<br />
show 3: "q" using 1 2 by (rule mp) <br />
qed<br />
<br />
-- "Pedro"<br />
lemma ejercicio_1b:<br />
assumes "p ⟶ q"<br />
"p"<br />
shows "q"<br />
proof -<br />
show "q" using assms(1,2) by (rule mp)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 2. Demostrar<br />
p ⟶ q, q ⟶ r, p ⊢ r<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_2a:<br />
assumes 1:"p ⟶ q" and<br />
2:"q ⟶ r" and<br />
3:"p" <br />
shows "r"<br />
proof -<br />
have 4: "q" using 1 3 by (rule mp)<br />
show 5: "r" using 2 4 by (rule mp) <br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 3. Demostrar<br />
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_3a:<br />
assumes 1: "p ⟶ (q ⟶ r)" and<br />
2: "p ⟶ q" and<br />
3: "p" <br />
shows "r"<br />
proof -<br />
have 4: "q ⟶ r" using 1 3 by (rule mp)<br />
have 5: "q" using 2 3 by (rule mp)<br />
show 6: "r" using 4 5 by (rule mp)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 4. Demostrar<br />
p ⟶ q, q ⟶ r ⊢ p ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_4a:<br />
assumes 1: "p ⟶ q" and<br />
2: "q ⟶ r" <br />
shows "p ⟶ r"<br />
proof -<br />
{assume 3:"p" <br />
have 4: "q" using 1 3 by (rule mp)<br />
have 5: "r" using 2 4 by (rule mp)}<br />
thus "p ⟶ r" by (rule impI)<br />
qed<br />
<br />
-- "Pedro"<br />
lemma ejercicio_4d:<br />
assumes "p ⟶ q" and<br />
"q ⟶ r" <br />
shows "p ⟶ r"<br />
using assms by auto<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 5. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_5a:<br />
assumes 1: "p ⟶ (q ⟶ r)" <br />
shows "q ⟶ (p ⟶ r)"<br />
proof -<br />
{assume 3: "q"<br />
{assume 4: "p"<br />
have "q ⟶ r" using 1 4 ..<br />
hence 5: "r" using 3 ..}<br />
hence 6: "p ⟶ r" by (rule impI)}<br />
thus "q ⟶ (p ⟶ r)" by (rule impI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 6. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_6a:<br />
assumes 1: "p ⟶ (q ⟶ r)" <br />
shows "(p ⟶ q) ⟶ (p ⟶ r)"<br />
proof -<br />
{assume 2: "p ⟶ q"<br />
{assume 3: "p"<br />
have 4: "q ⟶ r" using 1 3 ..<br />
have 5: "q" using 2 3 ..<br />
have "r" using 4 5 ..}<br />
hence "p ⟶ r" by (rule impI)}<br />
thus "(p ⟶ q) ⟶ (p ⟶ r)" by (rule impI)<br />
qed <br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 7. Demostrar<br />
p ⊢ q ⟶ p<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_7a:<br />
assumes "p" <br />
shows "q ⟶ p"<br />
proof -<br />
{assume 1: "q"}<br />
show "q ⟶ p" using assms(1) by (rule impI)<br />
qed<br />
<br />
-- "Dani"<br />
lemma ejercicio_7b:<br />
assumes "p" <br />
shows "q ⟶ p"<br />
proof<br />
assume "q"<br />
show "p" using assms(1) .<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 8. Demostrar<br />
⊢ p ⟶ (q ⟶ p)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Dani"<br />
lemma ejercicio_8a:<br />
"p ⟶ (q ⟶ p)"<br />
proof<br />
assume "p"<br />
show "q ⟶ p"<br />
proof<br />
assume "q"<br />
show "p" using `p` .<br />
qed<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 9. Demostrar<br />
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_9:<br />
assumes 1: "p ⟶ q"<br />
shows "(q ⟶ r) ⟶ (p ⟶ r)"<br />
proof- <br />
{assume 2: "q ⟶ r"<br />
{assume 3: "p"<br />
have 4: "q" using 1 3 by (rule mp)<br />
have 5: "r" using 2 4 by (rule mp)}<br />
hence 6: "p ⟶ r" by (rule impI)}<br />
thus "(q ⟶ r) ⟶ (p ⟶ r)" by (rule impI)<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 10. Demostrar<br />
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_10:<br />
assumes "p ⟶ (q ⟶ (r ⟶ s))" <br />
shows "r ⟶ (q ⟶ (p ⟶ s))"<br />
proof <br />
assume "r"<br />
show "q⟶ (p⟶ s)" <br />
proof <br />
assume "q"<br />
show "p⟶ s"<br />
proof<br />
assume "p"<br />
with assms have "q⟶ r⟶ s" ..<br />
hence "r⟶ s" using `q` ..<br />
thus "s" using `r`..<br />
qed<br />
qed <br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 11. Demostrar<br />
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_11a:<br />
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"<br />
lemma ejercicio_11:<br />
shows "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"<br />
proof<br />
assume 1: "p ⟶ (q ⟶ r)"<br />
show 2: "(p ⟶ q) ⟶ (p ⟶ r)"<br />
proof <br />
assume 3: "p⟶ q"<br />
show 4: "p⟶ r" <br />
proof <br />
assume 5: "p"<br />
have 6: "q" using 3 5 by (rule mp)<br />
have 7:"q⟶ r" using 1 5 by (rule mp)<br />
show 8: "r" using 7 6 ..<br />
qed<br />
qed <br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 12. Demostrar<br />
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_12:<br />
assumes "(p ⟶ q) ⟶ r" <br />
shows "p ⟶ (q ⟶ r)"<br />
oops<br />
<br />
section {* Conjunciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 13. Demostrar<br />
p, q ⊢ p ∧ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_13:<br />
assumes 1:"p" and<br />
2:"q" <br />
shows "p ∧ q"<br />
proof -<br />
show "p ∧ q" using 1 2 by (rule conjI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 14. Demostrar<br />
p ∧ q ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_14:<br />
assumes "p ∧ q" <br />
shows "p"<br />
proof -<br />
show "p" using assms by (rule conjunct1)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 15. Demostrar<br />
p ∧ q ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_15:<br />
assumes "p ∧ q" <br />
shows "q"<br />
proof -<br />
show "q" using assms by (rule conjunct2)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 16. Demostrar<br />
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_16a:<br />
assumes "p ∧ (q ∧ r)"<br />
shows "(p ∧ q)∧ r"<br />
proof -<br />
have 1: "p" using assms by (rule conjunct1)<br />
have 2: "(q ∧ r)" using assms by (rule conjunct2)<br />
have 3: "q" using 2 by (rule conjunct1)<br />
have 4: "r" using 2 by (rule conjunct2)<br />
have 5: "(p∧q)" using 1 3 by (rule conjI)<br />
show 6: "(p∧q) ∧ r" using 5 4 by (rule conjI)<br />
qed<br />
<br />
-- Dani (No estoy de si el ejercicio hecho por Pedro funciona)<br />
lemma ejercicio_16b:<br />
assumes "p ∧ (q ∧ r)"<br />
shows "(p ∧ q) ∧ r"<br />
proof<br />
have "p" using assms(1) by (rule conjunct1)<br />
have "q ∧ r" using assms(1) by (rule conjunct2)<br />
hence "q" by (rule conjunct1)<br />
show "p ∧ q" using `p` `q` by (rule conjI)<br />
next<br />
have "q ∧ r" using assms(1) by (rule conjunct2)<br />
thus "r" ..<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 17. Demostrar<br />
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_17:<br />
assumes "(p∧ q) ∧ r" <br />
shows "p ∧ (q∧ r)"<br />
proof -<br />
have 1: "r" using assms by (rule conjunct2)<br />
have 2: "(p∧q)" using assms by (rule conjunct1)<br />
have 3: "p" using 2 by (rule conjunct1)<br />
have 4: "q" using 2 by (rule conjunct2)<br />
have 5: "(q∧r)" using 4 1 by (rule conjI)<br />
show 6: "p∧(q∧r)" using 3 5 by (rule conjI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 18. Demostrar<br />
p ∧ q ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_18:<br />
assumes "p ∧ q" <br />
shows "p ⟶ q"<br />
proof -<br />
have 1: "q" using assms by (rule conjunct2)<br />
show "p⟶ q" using 1 by (rule impI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 19. Demostrar<br />
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r <br />
------------------------------------------------------------------ *}<br />
<br />
<br />
-- "Pedro"<br />
lemma ejercicio_19:<br />
assumes 1: "(p ⟶ q) ∧ (p ⟶ r)" <br />
shows "p ⟶ (q ∧ r)"<br />
proof (rule impI)<br />
assume 2: "p"<br />
have 3: "p ⟶ q" using assms by (rule conjunct1)<br />
have 4: "q" using 3 2 by (rule mp)<br />
have 5: "p ⟶ r" using assms by (rule conjunct2)<br />
have 6: "r" using 5 2 by (rule mp)<br />
show "q ∧ r" using 4 6 by (rule conjI)<br />
qed<br />
<br />
<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 20. Demostrar<br />
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_20:<br />
assumes "p ⟶ q ∧ r" <br />
shows "(p ⟶ q) ∧ (p ⟶ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 21. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_21a:<br />
assumes 1:"p ⟶ (q ⟶ r)" <br />
shows "p ∧ q ⟶ r"<br />
proof<br />
assume 2:"p∧q"<br />
show "r" <br />
proof -<br />
have 3: "p" using 2 by (rule conjunct1)<br />
have 4: "q" using 2 ..<br />
have 5: "(q⟶ r)" using 1 3 ..<br />
show 6: "r" using 5 4 ..<br />
qed<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 22. Demostrar<br />
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_22a:<br />
assumes "p ∧ q ⟶ r" <br />
shows "p ⟶ (q ⟶ r)"<br />
proof<br />
assume "p"<br />
show "q⟶ r"<br />
proof<br />
assume "q"<br />
have "p∧q" using `p` `q` ..<br />
show "r" using assms `p∧q`..<br />
qed<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 23. Demostrar<br />
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_23a:<br />
assumes 1:"(p ⟶ q) ⟶ r" <br />
shows "p ∧ q ⟶ r" <br />
proof <br />
assume 2:"p∧q"<br />
hence 3:"p" ..<br />
have 4:"q" using 2 ..<br />
hence 5: "p⟶ q" ..<br />
show"r" using 1 5 by (rule mp)<br />
qed<br />
<br />
-- Dani<br />
lemma ejercicio_23b:<br />
assumes "(p ⟶ q) ⟶ r" <br />
shows "p ∧ q ⟶ r"<br />
proof<br />
assume "p ∧ q"<br />
hence p ..<br />
have q using `p ∧ q` ..<br />
hence "p ⟶ q" ..<br />
with assms(1) show "r" ..<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 24. Demostrar<br />
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
-- Dani<br />
lemma ejercicio_24a:<br />
assumes "p ∧ (q ⟶ r)" <br />
shows "(p ⟶ q) ⟶ r"<br />
proof<br />
assume "p ⟶ q"<br />
have "p" using assms(1) ..<br />
with `p ⟶ q` have "q" ..<br />
have "q ⟶ r" using assms(1) ..<br />
thus "r" using `q` ..<br />
qed<br />
<br />
section {* Disyunciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 25. Demostrar<br />
p ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_25:<br />
assumes "p"<br />
shows "p ∨ q"<br />
proof -<br />
show "p∨q" using assms by (rule disjI1)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 26. Demostrar<br />
q ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_26:<br />
assumes "q"<br />
shows "p ∨ q"<br />
proof -<br />
show "p∨q" using assms by (rule disjI2)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 27. Demostrar<br />
p ∨ q ⊢ q ∨ p<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_27:<br />
assumes "p ∨ q"<br />
shows "q ∨ p"<br />
proof - <br />
have "p ∨ q" using assms by this<br />
moreover<br />
{ assume 2: "p"<br />
have "q ∨ p" using 2 by (rule disjI2) }<br />
moreover<br />
{ assume 3: "q"<br />
have "q ∨ p" using 3 by (rule disjI1) }<br />
ultimately show "q ∨ p" by (rule disjE) <br />
qed <br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 28. Demostrar<br />
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_28:<br />
assumes "q ⟶ r" <br />
shows "p ∨ q ⟶ p ∨ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 29. Demostrar<br />
p ∨ p ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_29:<br />
assumes "p ∨ p"<br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 30. Demostrar<br />
p ⊢ p ∨ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_30:<br />
assumes "p" <br />
shows "p ∨ p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 31. Demostrar<br />
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_31:<br />
assumes "p ∨ (q ∨ r)" <br />
shows "(p ∨ q) ∨ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 32. Demostrar<br />
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_32:<br />
assumes "(p ∨ q) ∨ r" <br />
shows "p ∨ (q ∨ r)"<br />
using assms(1)<br />
proof<br />
assume "p∨q"<br />
thus "p∨q∨r" <br />
proof<br />
assume "p"<br />
thus "p∨q∨r" ..<br />
next<br />
assume "q"<br />
hence "q∨r" ..<br />
thus "p∨q∨r" ..<br />
qed<br />
next<br />
assume "r"<br />
hence "q∨r" ..<br />
thus "p∨q∨r" ..<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 33. Demostrar<br />
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_33:<br />
assumes "p ∧ (q ∨ r)" <br />
shows "(p ∧ q) ∨ (p ∧ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 34. Demostrar<br />
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_34:<br />
assumes "(p ∧ q) ∨ (p ∧ r)" <br />
shows "p ∧ (q ∨ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 35. Demostrar<br />
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_35:<br />
assumes "p ∨ (q ∧ r)" <br />
shows "(p ∨ q) ∧ (p ∨ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 36. Demostrar<br />
(p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_36:<br />
assumes "(p ∨ q) ∧ (p ∨ r)"<br />
shows "p ∨ (q ∧ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 37. Demostrar<br />
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_37:<br />
assumes "(p ⟶ r) ∧ (q ⟶ r)" <br />
shows "p ∨ q ⟶ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 38. Demostrar<br />
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_38:<br />
assumes "p ∨ q ⟶ r" <br />
shows "(p ⟶ r) ∧ (q ⟶ r)"<br />
oops<br />
<br />
section {* Negaciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 39. Demostrar<br />
p ⊢ ¬¬p<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_39:<br />
assumes "p"<br />
shows "¬¬p"<br />
proof -<br />
show "¬¬p" using assms by (rule notnotI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 40. Demostrar<br />
¬p ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_40:<br />
assumes "¬p" <br />
shows "p ⟶ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 41. Demostrar<br />
p ⟶ q ⊢ ¬q ⟶ ¬p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_41:<br />
assumes "p ⟶ q"<br />
shows "¬q ⟶ ¬p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 42. Demostrar<br />
p∨q, ¬q ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_42:<br />
assumes "p∨q"<br />
"¬q" <br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 42. Demostrar<br />
p ∨ q, ¬p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_43:<br />
assumes "p ∨ q"<br />
"¬p" <br />
shows "q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 40. Demostrar<br />
p ∨ q ⊢ ¬(¬p ∧ ¬q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_44:<br />
assumes "p ∨ q" <br />
shows "¬(¬p ∧ ¬q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 45. Demostrar<br />
p ∧ q ⊢ ¬(¬p ∨ ¬q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_45:<br />
assumes "p ∧ q" <br />
shows "¬(¬p ∨ ¬q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 46. Demostrar<br />
¬(p ∨ q) ⊢ ¬p ∧ ¬q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_46:<br />
assumes "¬(p ∨ q)" <br />
shows "¬p ∧ ¬q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 47. Demostrar<br />
¬p ∧ ¬q ⊢ ¬(p ∨ q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_47:<br />
assumes "¬p ∧ ¬q" <br />
shows "¬(p ∨ q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 48. Demostrar<br />
¬p ∨ ¬q ⊢ ¬(p ∧ q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_48:<br />
assumes "¬p ∨ ¬q"<br />
shows "¬(p ∧ q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 49. Demostrar<br />
⊢ ¬(p ∧ ¬p)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_49:<br />
"¬(p ∧ ¬p)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 50. Demostrar<br />
p ∧ ¬p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_50:<br />
assumes "p ∧ ¬p" <br />
shows "q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 51. Demostrar<br />
¬¬p ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_51:<br />
assumes "¬¬p"<br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 52. Demostrar<br />
⊢ p ∨ ¬p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_52:<br />
"p ∨ ¬p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 53. Demostrar<br />
⊢ ((p ⟶ q) ⟶ p) ⟶ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_53:<br />
"((p ⟶ q) ⟶ p) ⟶ p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 54. Demostrar<br />
¬q ⟶ ¬p ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_54:<br />
assumes "¬q ⟶ ¬p"<br />
shows "p ⟶ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 55. Demostrar<br />
¬(¬p ∧ ¬q) ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_55:<br />
assumes "¬(¬p ∧ ¬q)"<br />
shows "p ∨ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 56. Demostrar<br />
¬(¬p ∨ ¬q) ⊢ p ∧ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_56:<br />
assumes "¬(¬p ∨ ¬q)" <br />
shows "p ∧ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 57. Demostrar<br />
¬(p ∧ q) ⊢ ¬p ∨ ¬q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_57:<br />
assumes "¬(p ∧ q)"<br />
shows "¬p ∨ ¬q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 58. Demostrar<br />
⊢ (p ⟶ q) ∨ (q ⟶ p)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_58:<br />
"(p ⟶ q) ∨ (q ⟶ p)"<br />
oops<br />
<br />
end<br />
</source></div>
Dancapmer
https://www.glc.us.es/~jalonso/DAO2012/index.php?title=Relaci%C3%B3n_3&diff=98
Relación 3
2013-03-12T11:47:04Z
<p>Dancapmer: </p>
<hr />
<div><source lang="isar"><br />
header {* R3: Deducción natural proposicional *}<br />
<br />
theory R3<br />
imports Main <br />
begin<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
El objetivo de esta relación es demostrar cada uno de los ejercicios<br />
usando sólo las reglas básicas de deducción natural de la lógica<br />
proposicional (sin usar el método auto).<br />
<br />
Las reglas básicas de la deducción natural son las siguientes:<br />
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q<br />
· conjunct1: P ∧ Q ⟹ P<br />
· conjunct2: P ∧ Q ⟹ Q <br />
· notnotD: ¬¬ P ⟹ P<br />
· notnotI: P ⟹ ¬¬ P<br />
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q <br />
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F <br />
· impI: (P ⟹ Q) ⟹ P ⟶ Q<br />
· disjI1: P ⟹ P ∨ Q<br />
· disjI2: Q ⟹ P ∨ Q<br />
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R <br />
· FalseE: False ⟹ P<br />
· notE: ⟦¬P; P⟧ ⟹ R<br />
· notI: (P ⟹ False) ⟹ ¬P<br />
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q<br />
· iffD1: ⟦Q = P; Q⟧ ⟹ P <br />
· iffD2: ⟦P = Q; Q⟧ ⟹ P<br />
· ccontr: (¬P ⟹ False) ⟹ P<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
text {*<br />
Se usarán las reglas notnotI y mt que demostramos a continuación. *}<br />
<br />
lemma notnotI: "P ⟹ ¬¬ P"<br />
by auto<br />
<br />
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"<br />
by auto<br />
<br />
section {* Implicaciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 1. Demostrar<br />
p ⟶ q, p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_1a:<br />
assumes 1: "p ⟶ q" and<br />
2: "p"<br />
shows "q"<br />
proof -<br />
show 3: "q" using 1 2 by (rule mp) <br />
qed<br />
<br />
-- "Pedro"<br />
lemma ejercicio_1b:<br />
assumes "p ⟶ q"<br />
"p"<br />
shows "q"<br />
proof -<br />
show "q" using assms(1,2) by (rule mp)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 2. Demostrar<br />
p ⟶ q, q ⟶ r, p ⊢ r<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_2a:<br />
assumes 1:"p ⟶ q" and<br />
2:"q ⟶ r" and<br />
3:"p" <br />
shows "r"<br />
proof -<br />
have 4: "q" using 1 3 by (rule mp)<br />
show 5: "r" using 2 4 by (rule mp) <br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 3. Demostrar<br />
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_3a:<br />
assumes 1: "p ⟶ (q ⟶ r)" and<br />
2: "p ⟶ q" and<br />
3: "p" <br />
shows "r"<br />
proof -<br />
have 4: "q ⟶ r" using 1 3 by (rule mp)<br />
have 5: "q" using 2 3 by (rule mp)<br />
show 6: "r" using 4 5 by (rule mp)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 4. Demostrar<br />
p ⟶ q, q ⟶ r ⊢ p ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_4a:<br />
assumes 1: "p ⟶ q" and<br />
2: "q ⟶ r" <br />
shows "p ⟶ r"<br />
proof -<br />
{assume 3:"p" <br />
have 4: "q" using 1 3 by (rule mp)<br />
have 5: "r" using 2 4 by (rule mp)}<br />
thus "p ⟶ r" by (rule impI)<br />
qed<br />
<br />
-- "Pedro"<br />
lemma ejercicio_4d:<br />
assumes "p ⟶ q" and<br />
"q ⟶ r" <br />
shows "p ⟶ r"<br />
using assms by auto<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 5. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_5a:<br />
assumes 1: "p ⟶ (q ⟶ r)" <br />
shows "q ⟶ (p ⟶ r)"<br />
proof -<br />
{assume 3: "q"<br />
{assume 4: "p"<br />
have "q ⟶ r" using 1 4 ..<br />
hence 5: "r" using 3 ..}<br />
hence 6: "p ⟶ r" by (rule impI)}<br />
thus "q ⟶ (p ⟶ r)" by (rule impI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 6. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_6a:<br />
assumes 1: "p ⟶ (q ⟶ r)" <br />
shows "(p ⟶ q) ⟶ (p ⟶ r)"<br />
proof -<br />
{assume 2: "p ⟶ q"<br />
{assume 3: "p"<br />
have 4: "q ⟶ r" using 1 3 ..<br />
have 5: "q" using 2 3 ..<br />
have "r" using 4 5 ..}<br />
hence "p ⟶ r" by (rule impI)}<br />
thus "(p ⟶ q) ⟶ (p ⟶ r)" by (rule impI)<br />
qed <br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 7. Demostrar<br />
p ⊢ q ⟶ p<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_7a:<br />
assumes "p" <br />
shows "q ⟶ p"<br />
proof -<br />
{assume 1: "q"}<br />
show "q ⟶ p" using assms(1) by (rule impI)<br />
qed<br />
<br />
-- "Dani"<br />
lemma ejercicio_7b:<br />
assumes "p" <br />
shows "q ⟶ p"<br />
proof<br />
assume "q"<br />
show "p" using assms(1) .<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 8. Demostrar<br />
⊢ p ⟶ (q ⟶ p)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Dani"<br />
lemma ejercicio_8a:<br />
"p ⟶ (q ⟶ p)"<br />
proof<br />
assume "p"<br />
show "q ⟶ p"<br />
proof<br />
assume "q"<br />
show "p" using `p` .<br />
qed<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 9. Demostrar<br />
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_9:<br />
assumes 1: "p ⟶ q"<br />
shows "(q ⟶ r) ⟶ (p ⟶ r)"<br />
proof- <br />
{assume 2: "q ⟶ r"<br />
{assume 3: "p"<br />
have 4: "q" using 1 3 by (rule mp)<br />
have 5: "r" using 2 4 by (rule mp)}<br />
hence 6: "p ⟶ r" by (rule impI)}<br />
thus "(q ⟶ r) ⟶ (p ⟶ r)" by (rule impI)<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 10. Demostrar<br />
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_10:<br />
assumes "p ⟶ (q ⟶ (r ⟶ s))" <br />
shows "r ⟶ (q ⟶ (p ⟶ s))"<br />
proof <br />
assume "r"<br />
show "q⟶ (p⟶ s)" <br />
proof <br />
assume "q"<br />
show "p⟶ s"<br />
proof<br />
assume "p"<br />
with assms have "q⟶ r⟶ s" ..<br />
hence "r⟶ s" using `q` ..<br />
thus "s" using `r`..<br />
qed<br />
qed <br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 11. Demostrar<br />
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_11a:<br />
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"<br />
lemma ejercicio_11:<br />
shows "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"<br />
proof<br />
assume 1: "p ⟶ (q ⟶ r)"<br />
show 2: "(p ⟶ q) ⟶ (p ⟶ r)"<br />
proof <br />
assume 3: "p⟶ q"<br />
show 4: "p⟶ r" <br />
proof <br />
assume 5: "p"<br />
have 6: "q" using 3 5 by (rule mp)<br />
have 7:"q⟶ r" using 1 5 by (rule mp)<br />
show 8: "r" using 7 6 ..<br />
qed<br />
qed <br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 12. Demostrar<br />
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_12:<br />
assumes "(p ⟶ q) ⟶ r" <br />
shows "p ⟶ (q ⟶ r)"<br />
oops<br />
<br />
section {* Conjunciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 13. Demostrar<br />
p, q ⊢ p ∧ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_13:<br />
assumes 1:"p" and<br />
2:"q" <br />
shows "p ∧ q"<br />
proof -<br />
show "p ∧ q" using 1 2 by (rule conjI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 14. Demostrar<br />
p ∧ q ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_14:<br />
assumes "p ∧ q" <br />
shows "p"<br />
proof -<br />
show "p" using assms by (rule conjunct1)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 15. Demostrar<br />
p ∧ q ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_15:<br />
assumes "p ∧ q" <br />
shows "q"<br />
proof -<br />
show "q" using assms by (rule conjunct2)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 16. Demostrar<br />
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_16:<br />
assumes "p ∧ (q ∧ r)"<br />
shows "(p ∧ q)∧ r"<br />
proof -<br />
have 1: "p" using assms by (rule conjunct1)<br />
have 2: "(q ∧ r)" using assms by (rule conjunct2)<br />
have 3: "q" using 2 by (rule conjunct1)<br />
have 4: "r" using 2 by (rule conjunct2)<br />
have 5: "(p∧q)" using 1 3 by (rule conjI)<br />
show 6: "(p∧q) ∧ r" using 5 4 by (rule conjI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 17. Demostrar<br />
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_17:<br />
assumes "(p∧ q) ∧ r" <br />
shows "p ∧ (q∧ r)"<br />
proof -<br />
have 1: "r" using assms by (rule conjunct2)<br />
have 2: "(p∧q)" using assms by (rule conjunct1)<br />
have 3: "p" using 2 by (rule conjunct1)<br />
have 4: "q" using 2 by (rule conjunct2)<br />
have 5: "(q∧r)" using 4 1 by (rule conjI)<br />
show 6: "p∧(q∧r)" using 3 5 by (rule conjI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 18. Demostrar<br />
p ∧ q ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_18:<br />
assumes "p ∧ q" <br />
shows "p ⟶ q"<br />
proof -<br />
have 1: "q" using assms by (rule conjunct2)<br />
show "p⟶ q" using 1 by (rule impI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 19. Demostrar<br />
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r <br />
------------------------------------------------------------------ *}<br />
<br />
<br />
-- "Pedro"<br />
lemma ejercicio_19:<br />
assumes 1: "(p ⟶ q) ∧ (p ⟶ r)" <br />
shows "p ⟶ (q ∧ r)"<br />
proof (rule impI)<br />
assume 2: "p"<br />
have 3: "p ⟶ q" using assms by (rule conjunct1)<br />
have 4: "q" using 3 2 by (rule mp)<br />
have 5: "p ⟶ r" using assms by (rule conjunct2)<br />
have 6: "r" using 5 2 by (rule mp)<br />
show "q ∧ r" using 4 6 by (rule conjI)<br />
qed<br />
<br />
<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 20. Demostrar<br />
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_20:<br />
assumes "p ⟶ q ∧ r" <br />
shows "(p ⟶ q) ∧ (p ⟶ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 21. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_21a:<br />
assumes 1:"p ⟶ (q ⟶ r)" <br />
shows "p ∧ q ⟶ r"<br />
proof<br />
assume 2:"p∧q"<br />
show "r" <br />
proof -<br />
have 3: "p" using 2 by (rule conjunct1)<br />
have 4: "q" using 2 ..<br />
have 5: "(q⟶ r)" using 1 3 ..<br />
show 6: "r" using 5 4 ..<br />
qed<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 22. Demostrar<br />
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_22a:<br />
assumes "p ∧ q ⟶ r" <br />
shows "p ⟶ (q ⟶ r)"<br />
proof<br />
assume "p"<br />
show "q⟶ r"<br />
proof<br />
assume "q"<br />
have "p∧q" using `p` `q` ..<br />
show "r" using assms `p∧q`..<br />
qed<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 23. Demostrar<br />
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_23a:<br />
assumes 1:"(p ⟶ q) ⟶ r" <br />
shows "p ∧ q ⟶ r" <br />
proof <br />
assume 2:"p∧q"<br />
hence 3:"p" ..<br />
have 4:"q" using 2 ..<br />
hence 5: "p⟶ q" ..<br />
show"r" using 1 5 by (rule mp)<br />
qed<br />
<br />
-- Dani<br />
lemma ejercicio_23b:<br />
assumes "(p ⟶ q) ⟶ r" <br />
shows "p ∧ q ⟶ r"<br />
proof<br />
assume "p ∧ q"<br />
hence p ..<br />
have q using `p ∧ q` ..<br />
hence "p ⟶ q" ..<br />
with assms(1) show "r" ..<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 24. Demostrar<br />
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
-- Dani<br />
lemma ejercicio_24a:<br />
assumes "p ∧ (q ⟶ r)" <br />
shows "(p ⟶ q) ⟶ r"<br />
proof<br />
assume "p ⟶ q"<br />
have "p" using assms(1) ..<br />
with `p ⟶ q` have "q" ..<br />
have "q ⟶ r" using assms(1) ..<br />
thus "r" using `q` ..<br />
qed<br />
<br />
section {* Disyunciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 25. Demostrar<br />
p ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_25:<br />
assumes "p"<br />
shows "p ∨ q"<br />
proof -<br />
show "p∨q" using assms by (rule disjI1)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 26. Demostrar<br />
q ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_26:<br />
assumes "q"<br />
shows "p ∨ q"<br />
proof -<br />
show "p∨q" using assms by (rule disjI2)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 27. Demostrar<br />
p ∨ q ⊢ q ∨ p<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_27:<br />
assumes "p ∨ q"<br />
shows "q ∨ p"<br />
proof - <br />
have "p ∨ q" using assms by this<br />
moreover<br />
{ assume 2: "p"<br />
have "q ∨ p" using 2 by (rule disjI2) }<br />
moreover<br />
{ assume 3: "q"<br />
have "q ∨ p" using 3 by (rule disjI1) }<br />
ultimately show "q ∨ p" by (rule disjE) <br />
qed <br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 28. Demostrar<br />
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_28:<br />
assumes "q ⟶ r" <br />
shows "p ∨ q ⟶ p ∨ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 29. Demostrar<br />
p ∨ p ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_29:<br />
assumes "p ∨ p"<br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 30. Demostrar<br />
p ⊢ p ∨ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_30:<br />
assumes "p" <br />
shows "p ∨ p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 31. Demostrar<br />
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_31:<br />
assumes "p ∨ (q ∨ r)" <br />
shows "(p ∨ q) ∨ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 32. Demostrar<br />
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_32:<br />
assumes "(p ∨ q) ∨ r" <br />
shows "p ∨ (q ∨ r)"<br />
using assms(1)<br />
proof<br />
assume "p∨q"<br />
thus "p∨q∨r" <br />
proof<br />
assume "p"<br />
thus "p∨q∨r" ..<br />
next<br />
assume "q"<br />
hence "q∨r" ..<br />
thus "p∨q∨r" ..<br />
qed<br />
next<br />
assume "r"<br />
hence "q∨r" ..<br />
thus "p∨q∨r" ..<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 33. Demostrar<br />
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_33:<br />
assumes "p ∧ (q ∨ r)" <br />
shows "(p ∧ q) ∨ (p ∧ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 34. Demostrar<br />
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_34:<br />
assumes "(p ∧ q) ∨ (p ∧ r)" <br />
shows "p ∧ (q ∨ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 35. Demostrar<br />
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_35:<br />
assumes "p ∨ (q ∧ r)" <br />
shows "(p ∨ q) ∧ (p ∨ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 36. Demostrar<br />
(p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_36:<br />
assumes "(p ∨ q) ∧ (p ∨ r)"<br />
shows "p ∨ (q ∧ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 37. Demostrar<br />
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_37:<br />
assumes "(p ⟶ r) ∧ (q ⟶ r)" <br />
shows "p ∨ q ⟶ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 38. Demostrar<br />
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_38:<br />
assumes "p ∨ q ⟶ r" <br />
shows "(p ⟶ r) ∧ (q ⟶ r)"<br />
oops<br />
<br />
section {* Negaciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 39. Demostrar<br />
p ⊢ ¬¬p<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_39:<br />
assumes "p"<br />
shows "¬¬p"<br />
proof -<br />
show "¬¬p" using assms by (rule notnotI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 40. Demostrar<br />
¬p ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_40:<br />
assumes "¬p" <br />
shows "p ⟶ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 41. Demostrar<br />
p ⟶ q ⊢ ¬q ⟶ ¬p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_41:<br />
assumes "p ⟶ q"<br />
shows "¬q ⟶ ¬p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 42. Demostrar<br />
p∨q, ¬q ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_42:<br />
assumes "p∨q"<br />
"¬q" <br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 42. Demostrar<br />
p ∨ q, ¬p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_43:<br />
assumes "p ∨ q"<br />
"¬p" <br />
shows "q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 40. Demostrar<br />
p ∨ q ⊢ ¬(¬p ∧ ¬q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_44:<br />
assumes "p ∨ q" <br />
shows "¬(¬p ∧ ¬q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 45. Demostrar<br />
p ∧ q ⊢ ¬(¬p ∨ ¬q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_45:<br />
assumes "p ∧ q" <br />
shows "¬(¬p ∨ ¬q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 46. Demostrar<br />
¬(p ∨ q) ⊢ ¬p ∧ ¬q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_46:<br />
assumes "¬(p ∨ q)" <br />
shows "¬p ∧ ¬q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 47. Demostrar<br />
¬p ∧ ¬q ⊢ ¬(p ∨ q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_47:<br />
assumes "¬p ∧ ¬q" <br />
shows "¬(p ∨ q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 48. Demostrar<br />
¬p ∨ ¬q ⊢ ¬(p ∧ q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_48:<br />
assumes "¬p ∨ ¬q"<br />
shows "¬(p ∧ q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 49. Demostrar<br />
⊢ ¬(p ∧ ¬p)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_49:<br />
"¬(p ∧ ¬p)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 50. Demostrar<br />
p ∧ ¬p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_50:<br />
assumes "p ∧ ¬p" <br />
shows "q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 51. Demostrar<br />
¬¬p ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_51:<br />
assumes "¬¬p"<br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 52. Demostrar<br />
⊢ p ∨ ¬p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_52:<br />
"p ∨ ¬p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 53. Demostrar<br />
⊢ ((p ⟶ q) ⟶ p) ⟶ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_53:<br />
"((p ⟶ q) ⟶ p) ⟶ p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 54. Demostrar<br />
¬q ⟶ ¬p ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_54:<br />
assumes "¬q ⟶ ¬p"<br />
shows "p ⟶ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 55. Demostrar<br />
¬(¬p ∧ ¬q) ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_55:<br />
assumes "¬(¬p ∧ ¬q)"<br />
shows "p ∨ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 56. Demostrar<br />
¬(¬p ∨ ¬q) ⊢ p ∧ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_56:<br />
assumes "¬(¬p ∨ ¬q)" <br />
shows "p ∧ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 57. Demostrar<br />
¬(p ∧ q) ⊢ ¬p ∨ ¬q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_57:<br />
assumes "¬(p ∧ q)"<br />
shows "¬p ∨ ¬q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 58. Demostrar<br />
⊢ (p ⟶ q) ∨ (q ⟶ p)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_58:<br />
"(p ⟶ q) ∨ (q ⟶ p)"<br />
oops<br />
<br />
end<br />
</source></div>
Dancapmer
https://www.glc.us.es/~jalonso/DAO2012/index.php?title=Relaci%C3%B3n_3&diff=97
Relación 3
2013-03-12T11:41:08Z
<p>Dancapmer: </p>
<hr />
<div><source lang="isar"><br />
header {* R3: Deducción natural proposicional *}<br />
<br />
theory R3<br />
imports Main <br />
begin<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
El objetivo de esta relación es demostrar cada uno de los ejercicios<br />
usando sólo las reglas básicas de deducción natural de la lógica<br />
proposicional (sin usar el método auto).<br />
<br />
Las reglas básicas de la deducción natural son las siguientes:<br />
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q<br />
· conjunct1: P ∧ Q ⟹ P<br />
· conjunct2: P ∧ Q ⟹ Q <br />
· notnotD: ¬¬ P ⟹ P<br />
· notnotI: P ⟹ ¬¬ P<br />
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q <br />
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F <br />
· impI: (P ⟹ Q) ⟹ P ⟶ Q<br />
· disjI1: P ⟹ P ∨ Q<br />
· disjI2: Q ⟹ P ∨ Q<br />
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R <br />
· FalseE: False ⟹ P<br />
· notE: ⟦¬P; P⟧ ⟹ R<br />
· notI: (P ⟹ False) ⟹ ¬P<br />
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q<br />
· iffD1: ⟦Q = P; Q⟧ ⟹ P <br />
· iffD2: ⟦P = Q; Q⟧ ⟹ P<br />
· ccontr: (¬P ⟹ False) ⟹ P<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
text {*<br />
Se usarán las reglas notnotI y mt que demostramos a continuación. *}<br />
<br />
lemma notnotI: "P ⟹ ¬¬ P"<br />
by auto<br />
<br />
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"<br />
by auto<br />
<br />
section {* Implicaciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 1. Demostrar<br />
p ⟶ q, p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_1a:<br />
assumes 1: "p ⟶ q" and<br />
2: "p"<br />
shows "q"<br />
proof -<br />
show 3: "q" using 1 2 by (rule mp) <br />
qed<br />
<br />
-- "Pedro"<br />
lemma ejercicio_1b:<br />
assumes "p ⟶ q"<br />
"p"<br />
shows "q"<br />
proof -<br />
show "q" using assms(1,2) by (rule mp)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 2. Demostrar<br />
p ⟶ q, q ⟶ r, p ⊢ r<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_2a:<br />
assumes 1:"p ⟶ q" and<br />
2:"q ⟶ r" and<br />
3:"p" <br />
shows "r"<br />
proof -<br />
have 4: "q" using 1 3 by (rule mp)<br />
show 5: "r" using 2 4 by (rule mp) <br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 3. Demostrar<br />
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_3a:<br />
assumes 1: "p ⟶ (q ⟶ r)" and<br />
2: "p ⟶ q" and<br />
3: "p" <br />
shows "r"<br />
proof -<br />
have 4: "q ⟶ r" using 1 3 by (rule mp)<br />
have 5: "q" using 2 3 by (rule mp)<br />
show 6: "r" using 4 5 by (rule mp)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 4. Demostrar<br />
p ⟶ q, q ⟶ r ⊢ p ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_4a:<br />
assumes 1: "p ⟶ q" and<br />
2: "q ⟶ r" <br />
shows "p ⟶ r"<br />
proof -<br />
{assume 3:"p" <br />
have 4: "q" using 1 3 by (rule mp)<br />
have 5: "r" using 2 4 by (rule mp)}<br />
thus "p ⟶ r" by (rule impI)<br />
qed<br />
<br />
-- "Pedro"<br />
lemma ejercicio_4d:<br />
assumes "p ⟶ q" and<br />
"q ⟶ r" <br />
shows "p ⟶ r"<br />
using assms by auto<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 5. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_5a:<br />
assumes 1: "p ⟶ (q ⟶ r)" <br />
shows "q ⟶ (p ⟶ r)"<br />
proof -<br />
{assume 3: "q"<br />
{assume 4: "p"<br />
have "q ⟶ r" using 1 4 ..<br />
hence 5: "r" using 3 ..}<br />
hence 6: "p ⟶ r" by (rule impI)}<br />
thus "q ⟶ (p ⟶ r)" by (rule impI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 6. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_6a:<br />
assumes 1: "p ⟶ (q ⟶ r)" <br />
shows "(p ⟶ q) ⟶ (p ⟶ r)"<br />
proof -<br />
{assume 2: "p ⟶ q"<br />
{assume 3: "p"<br />
have 4: "q ⟶ r" using 1 3 ..<br />
have 5: "q" using 2 3 ..<br />
have "r" using 4 5 ..}<br />
hence "p ⟶ r" by (rule impI)}<br />
thus "(p ⟶ q) ⟶ (p ⟶ r)" by (rule impI)<br />
qed <br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 7. Demostrar<br />
p ⊢ q ⟶ p<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_7a:<br />
assumes "p" <br />
shows "q ⟶ p"<br />
proof -<br />
{assume 1: "q"}<br />
show "q ⟶ p" using assms(1) by (rule impI)<br />
qed<br />
<br />
-- "Dani"<br />
lemma ejercicio_7b:<br />
assumes "p" <br />
shows "q ⟶ p"<br />
proof<br />
assume "q"<br />
show "p" using assms(1) .<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 8. Demostrar<br />
⊢ p ⟶ (q ⟶ p)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Dani"<br />
lemma ejercicio_8a:<br />
"p ⟶ (q ⟶ p)"<br />
proof<br />
assume "p"<br />
show "q ⟶ p"<br />
proof<br />
assume "q"<br />
show "p" using `p` .<br />
qed<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 9. Demostrar<br />
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_9:<br />
assumes 1: "p ⟶ q"<br />
shows "(q ⟶ r) ⟶ (p ⟶ r)"<br />
proof- <br />
{assume 2: "q ⟶ r"<br />
{assume 3: "p"<br />
have 4: "q" using 1 3 by (rule mp)<br />
have 5: "r" using 2 4 by (rule mp)}<br />
hence 6: "p ⟶ r" by (rule impI)}<br />
thus "(q ⟶ r) ⟶ (p ⟶ r)" by (rule impI)<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 10. Demostrar<br />
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_10:<br />
assumes "p ⟶ (q ⟶ (r ⟶ s))" <br />
shows "r ⟶ (q ⟶ (p ⟶ s))"<br />
proof <br />
assume "r"<br />
show "q⟶ (p⟶ s)" <br />
proof <br />
assume "q"<br />
show "p⟶ s"<br />
proof<br />
assume "p"<br />
with assms have "q⟶ r⟶ s" ..<br />
hence "r⟶ s" using `q` ..<br />
thus "s" using `r`..<br />
qed<br />
qed <br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 11. Demostrar<br />
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_11a:<br />
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"<br />
lemma ejercicio_11:<br />
shows "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"<br />
proof<br />
assume 1: "p ⟶ (q ⟶ r)"<br />
show 2: "(p ⟶ q) ⟶ (p ⟶ r)"<br />
proof <br />
assume 3: "p⟶ q"<br />
show 4: "p⟶ r" <br />
proof <br />
assume 5: "p"<br />
have 6: "q" using 3 5 by (rule mp)<br />
have 7:"q⟶ r" using 1 5 by (rule mp)<br />
show 8: "r" using 7 6 ..<br />
qed<br />
qed <br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 12. Demostrar<br />
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_12:<br />
assumes "(p ⟶ q) ⟶ r" <br />
shows "p ⟶ (q ⟶ r)"<br />
oops<br />
<br />
section {* Conjunciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 13. Demostrar<br />
p, q ⊢ p ∧ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_13:<br />
assumes 1:"p" and<br />
2:"q" <br />
shows "p ∧ q"<br />
proof -<br />
show "p ∧ q" using 1 2 by (rule conjI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 14. Demostrar<br />
p ∧ q ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_14:<br />
assumes "p ∧ q" <br />
shows "p"<br />
proof -<br />
show "p" using assms by (rule conjunct1)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 15. Demostrar<br />
p ∧ q ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_15:<br />
assumes "p ∧ q" <br />
shows "q"<br />
proof -<br />
show "q" using assms by (rule conjunct2)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 16. Demostrar<br />
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_16:<br />
assumes "p ∧ (q ∧ r)"<br />
shows "(p ∧ q)∧ r"<br />
proof -<br />
have 1: "p" using assms by (rule conjunct1)<br />
have 2: "(q ∧ r)" using assms by (rule conjunct2)<br />
have 3: "q" using 2 by (rule conjunct1)<br />
have 4: "r" using 2 by (rule conjunct2)<br />
have 5: "(p∧q)" using 1 3 by (rule conjI)<br />
show 6: "(p∧q) ∧ r" using 5 4 by (rule conjI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 17. Demostrar<br />
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_17:<br />
assumes "(p∧ q) ∧ r" <br />
shows "p ∧ (q∧ r)"<br />
proof -<br />
have 1: "r" using assms by (rule conjunct2)<br />
have 2: "(p∧q)" using assms by (rule conjunct1)<br />
have 3: "p" using 2 by (rule conjunct1)<br />
have 4: "q" using 2 by (rule conjunct2)<br />
have 5: "(q∧r)" using 4 1 by (rule conjI)<br />
show 6: "p∧(q∧r)" using 3 5 by (rule conjI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 18. Demostrar<br />
p ∧ q ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_18:<br />
assumes "p ∧ q" <br />
shows "p ⟶ q"<br />
proof -<br />
have 1: "q" using assms by (rule conjunct2)<br />
show "p⟶ q" using 1 by (rule impI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 19. Demostrar<br />
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r <br />
------------------------------------------------------------------ *}<br />
<br />
<br />
-- "Pedro"<br />
lemma ejercicio_19:<br />
assumes 1: "(p ⟶ q) ∧ (p ⟶ r)" <br />
shows "p ⟶ (q ∧ r)"<br />
proof (rule impI)<br />
assume 2: "p"<br />
have 3: "p ⟶ q" using assms by (rule conjunct1)<br />
have 4: "q" using 3 2 by (rule mp)<br />
have 5: "p ⟶ r" using assms by (rule conjunct2)<br />
have 6: "r" using 5 2 by (rule mp)<br />
show "q ∧ r" using 4 6 by (rule conjI)<br />
qed<br />
<br />
<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 20. Demostrar<br />
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_20:<br />
assumes "p ⟶ q ∧ r" <br />
shows "(p ⟶ q) ∧ (p ⟶ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 21. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_21a:<br />
assumes 1:"p ⟶ (q ⟶ r)" <br />
shows "p ∧ q ⟶ r"<br />
proof<br />
assume 2:"p∧q"<br />
show "r" <br />
proof -<br />
have 3: "p" using 2 by (rule conjunct1)<br />
have 4: "q" using 2 ..<br />
have 5: "(q⟶ r)" using 1 3 ..<br />
show 6: "r" using 5 4 ..<br />
qed<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 22. Demostrar<br />
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_22a:<br />
assumes "p ∧ q ⟶ r" <br />
shows "p ⟶ (q ⟶ r)"<br />
proof<br />
assume "p"<br />
show "q⟶ r"<br />
proof<br />
assume "q"<br />
have "p∧q" using `p` `q` ..<br />
show "r" using assms `p∧q`..<br />
qed<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 23. Demostrar<br />
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_23a:<br />
assumes 1:"(p ⟶ q) ⟶ r" <br />
shows "p ∧ q ⟶ r" <br />
proof <br />
assume 2:"p∧q"<br />
hence 3:"p" ..<br />
have 4:"q" using 2 ..<br />
hence 5: "p⟶ q" ..<br />
show"r" using 1 5 by (rule mp)<br />
qed<br />
<br />
-- Dani<br />
lemma ejercicio_23b:<br />
assumes "(p ⟶ q) ⟶ r" <br />
shows "p ∧ q ⟶ r"<br />
proof<br />
assume "p ∧ q"<br />
hence p ..<br />
have q using `p ∧ q` ..<br />
hence "p ⟶ q" ..<br />
with assms(1) show "r" ..<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 24. Demostrar<br />
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_24:<br />
assumes "p ∧ (q ⟶ r)" <br />
shows "(p ⟶ q) ⟶ r"<br />
oops<br />
<br />
section {* Disyunciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 25. Demostrar<br />
p ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_25:<br />
assumes "p"<br />
shows "p ∨ q"<br />
proof -<br />
show "p∨q" using assms by (rule disjI1)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 26. Demostrar<br />
q ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_26:<br />
assumes "q"<br />
shows "p ∨ q"<br />
proof -<br />
show "p∨q" using assms by (rule disjI2)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 27. Demostrar<br />
p ∨ q ⊢ q ∨ p<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_27:<br />
assumes "p ∨ q"<br />
shows "q ∨ p"<br />
proof - <br />
have "p ∨ q" using assms by this<br />
moreover<br />
{ assume 2: "p"<br />
have "q ∨ p" using 2 by (rule disjI2) }<br />
moreover<br />
{ assume 3: "q"<br />
have "q ∨ p" using 3 by (rule disjI1) }<br />
ultimately show "q ∨ p" by (rule disjE) <br />
qed <br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 28. Demostrar<br />
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_28:<br />
assumes "q ⟶ r" <br />
shows "p ∨ q ⟶ p ∨ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 29. Demostrar<br />
p ∨ p ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_29:<br />
assumes "p ∨ p"<br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 30. Demostrar<br />
p ⊢ p ∨ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_30:<br />
assumes "p" <br />
shows "p ∨ p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 31. Demostrar<br />
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_31:<br />
assumes "p ∨ (q ∨ r)" <br />
shows "(p ∨ q) ∨ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 32. Demostrar<br />
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)<br />
------------------------------------------------------------------ *}<br />
-- "Pedro G. Ros"<br />
lemma ejercicio_32:<br />
assumes "(p ∨ q) ∨ r" <br />
shows "p ∨ (q ∨ r)"<br />
using assms(1)<br />
proof<br />
assume "p∨q"<br />
thus "p∨q∨r" <br />
proof<br />
assume "p"<br />
thus "p∨q∨r" ..<br />
next<br />
assume "q"<br />
hence "q∨r" ..<br />
thus "p∨q∨r" ..<br />
qed<br />
next<br />
assume "r"<br />
hence "q∨r" ..<br />
thus "p∨q∨r" ..<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 33. Demostrar<br />
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_33:<br />
assumes "p ∧ (q ∨ r)" <br />
shows "(p ∧ q) ∨ (p ∧ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 34. Demostrar<br />
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_34:<br />
assumes "(p ∧ q) ∨ (p ∧ r)" <br />
shows "p ∧ (q ∨ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 35. Demostrar<br />
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_35:<br />
assumes "p ∨ (q ∧ r)" <br />
shows "(p ∨ q) ∧ (p ∨ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 36. Demostrar<br />
(p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_36:<br />
assumes "(p ∨ q) ∧ (p ∨ r)"<br />
shows "p ∨ (q ∧ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 37. Demostrar<br />
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_37:<br />
assumes "(p ⟶ r) ∧ (q ⟶ r)" <br />
shows "p ∨ q ⟶ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 38. Demostrar<br />
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_38:<br />
assumes "p ∨ q ⟶ r" <br />
shows "(p ⟶ r) ∧ (q ⟶ r)"<br />
oops<br />
<br />
section {* Negaciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 39. Demostrar<br />
p ⊢ ¬¬p<br />
------------------------------------------------------------------ *}<br />
<br />
-- "Pedro"<br />
lemma ejercicio_39:<br />
assumes "p"<br />
shows "¬¬p"<br />
proof -<br />
show "¬¬p" using assms by (rule notnotI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 40. Demostrar<br />
¬p ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_40:<br />
assumes "¬p" <br />
shows "p ⟶ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 41. Demostrar<br />
p ⟶ q ⊢ ¬q ⟶ ¬p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_41:<br />
assumes "p ⟶ q"<br />
shows "¬q ⟶ ¬p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 42. Demostrar<br />
p∨q, ¬q ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_42:<br />
assumes "p∨q"<br />
"¬q" <br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 42. Demostrar<br />
p ∨ q, ¬p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_43:<br />
assumes "p ∨ q"<br />
"¬p" <br />
shows "q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 40. Demostrar<br />
p ∨ q ⊢ ¬(¬p ∧ ¬q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_44:<br />
assumes "p ∨ q" <br />
shows "¬(¬p ∧ ¬q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 45. Demostrar<br />
p ∧ q ⊢ ¬(¬p ∨ ¬q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_45:<br />
assumes "p ∧ q" <br />
shows "¬(¬p ∨ ¬q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 46. Demostrar<br />
¬(p ∨ q) ⊢ ¬p ∧ ¬q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_46:<br />
assumes "¬(p ∨ q)" <br />
shows "¬p ∧ ¬q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 47. Demostrar<br />
¬p ∧ ¬q ⊢ ¬(p ∨ q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_47:<br />
assumes "¬p ∧ ¬q" <br />
shows "¬(p ∨ q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 48. Demostrar<br />
¬p ∨ ¬q ⊢ ¬(p ∧ q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_48:<br />
assumes "¬p ∨ ¬q"<br />
shows "¬(p ∧ q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 49. Demostrar<br />
⊢ ¬(p ∧ ¬p)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_49:<br />
"¬(p ∧ ¬p)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 50. Demostrar<br />
p ∧ ¬p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_50:<br />
assumes "p ∧ ¬p" <br />
shows "q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 51. Demostrar<br />
¬¬p ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_51:<br />
assumes "¬¬p"<br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 52. Demostrar<br />
⊢ p ∨ ¬p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_52:<br />
"p ∨ ¬p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 53. Demostrar<br />
⊢ ((p ⟶ q) ⟶ p) ⟶ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_53:<br />
"((p ⟶ q) ⟶ p) ⟶ p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 54. Demostrar<br />
¬q ⟶ ¬p ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_54:<br />
assumes "¬q ⟶ ¬p"<br />
shows "p ⟶ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 55. Demostrar<br />
¬(¬p ∧ ¬q) ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_55:<br />
assumes "¬(¬p ∧ ¬q)"<br />
shows "p ∨ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 56. Demostrar<br />
¬(¬p ∨ ¬q) ⊢ p ∧ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_56:<br />
assumes "¬(¬p ∨ ¬q)" <br />
shows "p ∧ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 57. Demostrar<br />
¬(p ∧ q) ⊢ ¬p ∨ ¬q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_57:<br />
assumes "¬(p ∧ q)"<br />
shows "¬p ∨ ¬q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 58. Demostrar<br />
⊢ (p ⟶ q) ∨ (q ⟶ p)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_58:<br />
"(p ⟶ q) ∨ (q ⟶ p)"<br />
oops<br />
<br />
end<br />
</source></div>
Dancapmer
https://www.glc.us.es/~jalonso/DAO2012/index.php?title=Relaci%C3%B3n_3&diff=83
Relación 3
2013-03-07T10:29:44Z
<p>Dancapmer: </p>
<hr />
<div><source lang="isar"><br />
header {* R3: Deducción natural proposicional *}<br />
<br />
theory R3<br />
imports Main <br />
begin<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
El objetivo de esta relación es demostrar cada uno de los ejercicios<br />
usando sólo las reglas básicas de deducción natural de la lógica<br />
proposicional (sin usar el método auto).<br />
<br />
Las reglas básicas de la deducción natural son las siguientes:<br />
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q<br />
· conjunct1: P ∧ Q ⟹ P<br />
· conjunct2: P ∧ Q ⟹ Q <br />
· notnotD: ¬¬ P ⟹ P<br />
· notnotI: P ⟹ ¬¬ P<br />
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q <br />
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F <br />
· impI: (P ⟹ Q) ⟹ P ⟶ Q<br />
· disjI1: P ⟹ P ∨ Q<br />
· disjI2: Q ⟹ P ∨ Q<br />
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R <br />
· FalseE: False ⟹ P<br />
· notE: ⟦¬P; P⟧ ⟹ R<br />
· notI: (P ⟹ False) ⟹ ¬P<br />
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q<br />
· iffD1: ⟦Q = P; Q⟧ ⟹ P <br />
· iffD2: ⟦P = Q; Q⟧ ⟹ P<br />
· ccontr: (¬P ⟹ False) ⟹ P<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
text {*<br />
Se usarán las reglas notnotI y mt que demostramos a continuación. *}<br />
<br />
lemma notnotI: "P ⟹ ¬¬ P"<br />
by auto<br />
<br />
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"<br />
by auto<br />
<br />
section {* Implicaciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 1. Demostrar<br />
p ⟶ q, p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_1a:<br />
assumes 1: "p ⟶ q" and<br />
2: "p"<br />
shows "q"<br />
proof -<br />
show 3: "q" using 1 2 by (rule mp) <br />
qed<br />
<br />
lemma ejercicio_1b:<br />
assumes "p ⟶ q"<br />
"p"<br />
shows "q"<br />
proof -<br />
show "q" using assms(1,2) by (rule mp)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 2. Demostrar<br />
p ⟶ q, q ⟶ r, p ⊢ r<br />
------------------------------------------------------------------ *}<br />
<br />
<br />
lemma ejercicio_2a:<br />
assumes 1:"p ⟶ q" and<br />
2:"q ⟶ r" and<br />
3:"p" <br />
shows "r"<br />
proof -<br />
have 4: "q" using 1 3 by (rule mp)<br />
show 5: "r" using 2 4 by (rule mp) <br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 3. Demostrar<br />
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r<br />
------------------------------------------------------------------ *}<br />
<br />
<br />
lemma ejercicio_3a:<br />
assumes 1: "p ⟶ (q ⟶ r)" and<br />
2: "p ⟶ q" and<br />
3: "p" <br />
shows "r"<br />
proof -<br />
have 4: "q ⟶ r" using 1 3 by (rule mp)<br />
have 5: "q" using 2 3 by (rule mp)<br />
show 6: "r" using 4 5 by (rule mp)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 4. Demostrar<br />
p ⟶ q, q ⟶ r ⊢ p ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_4a:<br />
assumes 1: "p ⟶ q" and<br />
2: "q ⟶ r" <br />
shows "p ⟶ r"<br />
proof -<br />
{assume 3:"p" <br />
have 4: "q" using 1 3 by (rule mp)<br />
have 5: "r" using 2 4 by (rule mp)}<br />
thus "p ⟶ r" by (rule impI)<br />
qed<br />
<br />
<br />
lemma ejercicio_4d:<br />
assumes "p ⟶ q" and<br />
"q ⟶ r" <br />
shows "p ⟶ r"<br />
using assms by auto<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 5. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
<br />
lemma ejercicio_5a:<br />
assumes 1: "p ⟶ (q ⟶ r)" <br />
shows "q ⟶ (p ⟶ r)"<br />
proof -<br />
{assume 3: "q"<br />
{assume 4: "p"<br />
have "q ⟶ r" using 1 4 ..<br />
hence 5: "r" using 3 ..}<br />
hence 6: "p ⟶ r" by (rule impI)}<br />
thus "q ⟶ (p ⟶ r)" by (rule impI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 6. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_6a:<br />
assumes 1: "p ⟶ (q ⟶ r)" <br />
shows "(p ⟶ q) ⟶ (p ⟶ r)"<br />
proof -<br />
{assume 2: "p ⟶ q"<br />
{assume 3: "p"<br />
have 4: "q ⟶ r" using 1 3 ..<br />
have 5: "q" using 2 3 ..<br />
have "r" using 4 5 ..}<br />
hence "p ⟶ r" by (rule impI)}<br />
thus "(p ⟶ q) ⟶ (p ⟶ r)" by (rule impI)<br />
qed <br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 7. Demostrar<br />
p ⊢ q ⟶ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_7a:<br />
assumes "p" <br />
shows "q ⟶ p"<br />
proof -<br />
{assume 1: "q"}<br />
show "q ⟶ p" using assms(1) by (rule impI)<br />
qed<br />
<br />
-- Dani<br />
lemma ejercicio_7b:<br />
assumes "p" <br />
shows "q ⟶ p"<br />
proof<br />
assume "q"<br />
show "p" using assms(1) .<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 8. Demostrar<br />
⊢ p ⟶ (q ⟶ p)<br />
------------------------------------------------------------------ *}<br />
<br />
-- Dani<br />
lemma ejercicio_8a:<br />
"p ⟶ (q ⟶ p)"<br />
proof<br />
assume "p"<br />
show "q ⟶ p"<br />
proof<br />
assume "q"<br />
show "p" using `p` .<br />
qed<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 9. Demostrar<br />
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
<br />
lemma ejercicio_9:<br />
assumes 1: "p ⟶ q"<br />
shows "(q ⟶ r) ⟶ (p ⟶ r)"<br />
proof- <br />
{assume 2: "q ⟶ r"<br />
{assume 3: "p"<br />
have 4: "q" using 1 3 by (rule mp)<br />
have 5: "r" using 2 4 by (rule mp)}<br />
hence 6: "p ⟶ r" by (rule impI)}<br />
thus "(q ⟶ r) ⟶ (p ⟶ r)" by (rule impI)<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 10. Demostrar<br />
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_10:<br />
assumes "p ⟶ (q ⟶ (r ⟶ s))" <br />
shows "r ⟶ (q ⟶ (p ⟶ s))"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 11. Demostrar<br />
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_11:<br />
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 12. Demostrar<br />
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_12:<br />
assumes "(p ⟶ q) ⟶ r" <br />
shows "p ⟶ (q ⟶ r)"<br />
oops<br />
<br />
section {* Conjunciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 13. Demostrar<br />
p, q ⊢ p ∧ q<br />
------------------------------------------------------------------ *}<br />
<br />
<br />
<br />
lemma ejercicio_13:<br />
assumes 1:"p" and<br />
2:"q" <br />
shows "p ∧ q"<br />
proof -<br />
show "p ∧ q" using 1 2 by (rule conjI)<br />
qed<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 14. Demostrar<br />
p ∧ q ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_14:<br />
assumes "p ∧ q" <br />
shows "p"<br />
proof -<br />
show "p" using assms by (rule conjunct1)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 15. Demostrar<br />
p ∧ q ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_15:<br />
assumes "p ∧ q" <br />
shows "q"<br />
proof -<br />
show "q" using assms by (rule conjunct2)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 16. Demostrar<br />
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_16:<br />
assumes "p ∧ (q ∧ r)"<br />
shows "(p ∧ q)∧ r"<br />
proof -<br />
have 1: "p" using assms by (rule conjunct1)<br />
have 2: "(q ∧ r)" using assms by (rule conjunct2)<br />
have 3: "q" using 2 by (rule conjunct1)<br />
have 4: "r" using 2 by (rule conjunct2)<br />
have 5: "(p∧q)" using 1 3 by (rule conjI)<br />
show 6: "(p∧q) ∧ r" using 5 4 by (rule conjI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 17. Demostrar<br />
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_17:<br />
assumes "(p∧ q) ∧ r" <br />
shows "p ∧ (q∧ r)"<br />
proof -<br />
have 1: "r" using assms by (rule conjunct2)<br />
have 2: "(p∧q)" using assms by (rule conjunct1)<br />
have 3: "p" using 2 by (rule conjunct1)<br />
have 4: "q" using 2 by (rule conjunct2)<br />
have 5: "(q∧r)" using 4 1 by (rule conjI)<br />
show 6: "p∧(q∧r)" using 3 5 by (rule conjI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 18. Demostrar<br />
p ∧ q ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_18:<br />
assumes "p ∧ q" <br />
shows "p ⟶ q"<br />
proof -<br />
have 1: "q" using assms by (rule conjunct2)<br />
show "p⟶ q" using 1 by (rule impI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 19. Demostrar<br />
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r <br />
------------------------------------------------------------------ *}<br />
<br />
<br />
lemma ejercicio_19:<br />
assumes 1: "(p ⟶ q) ∧ (p ⟶ r)" <br />
shows "p ⟶ (q ∧ r)"<br />
proof (rule impI)<br />
assume 2: "p"<br />
have 3: "p ⟶ q" using assms by (rule conjunct1)<br />
have 4: "q" using 3 2 by (rule mp)<br />
have 5: "p ⟶ r" using assms by (rule conjunct2)<br />
have 6: "r" using 5 2 by (rule mp)<br />
show "q ∧ r" using 4 6 by (rule conjI)<br />
qed<br />
<br />
<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 20. Demostrar<br />
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_20:<br />
assumes "p ⟶ q ∧ r" <br />
shows "(p ⟶ q) ∧ (p ⟶ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 21. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_21:<br />
assumes "p ⟶ (q ⟶ r)" <br />
shows "p ∧ q ⟶ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 22. Demostrar<br />
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_22:<br />
assumes "p ∧ q ⟶ r" <br />
shows "p ⟶ (q ⟶ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 23. Demostrar<br />
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_23:<br />
assumes "(p ⟶ q) ⟶ r" <br />
shows "p ∧ q ⟶ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 24. Demostrar<br />
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_24:<br />
assumes "p ∧ (q ⟶ r)" <br />
shows "(p ⟶ q) ⟶ r"<br />
oops<br />
<br />
section {* Disyunciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 25. Demostrar<br />
p ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_25:<br />
assumes "p"<br />
shows "p ∨ q"<br />
proof -<br />
show "p∨q" using assms by (rule disjI1)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 26. Demostrar<br />
q ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_26:<br />
assumes "q"<br />
shows "p ∨ q"<br />
proof -<br />
show "p∨q" using assms by (rule disjI2)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 27. Demostrar<br />
p ∨ q ⊢ q ∨ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_27:<br />
assumes "p ∨ q"<br />
shows "q ∨ p"<br />
proof - <br />
have "p ∨ q" using assms by this<br />
moreover<br />
{ assume 2: "p"<br />
have "q ∨ p" using 2 by (rule disjI2) }<br />
moreover<br />
{ assume 3: "q"<br />
have "q ∨ p" using 3 by (rule disjI1) }<br />
ultimately show "q ∨ p" by (rule disjE) <br />
qed <br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 28. Demostrar<br />
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_28:<br />
assumes "q ⟶ r" <br />
shows "p ∨ q ⟶ p ∨ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 29. Demostrar<br />
p ∨ p ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_29:<br />
assumes "p ∨ p"<br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 30. Demostrar<br />
p ⊢ p ∨ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_30:<br />
assumes "p" <br />
shows "p ∨ p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 31. Demostrar<br />
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_31:<br />
assumes "p ∨ (q ∨ r)" <br />
shows "(p ∨ q) ∨ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 32. Demostrar<br />
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_32:<br />
assumes "(p ∨ q) ∨ r" <br />
shows "p ∨ (q ∨ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 33. Demostrar<br />
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_33:<br />
assumes "p ∧ (q ∨ r)" <br />
shows "(p ∧ q) ∨ (p ∧ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 34. Demostrar<br />
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_34:<br />
assumes "(p ∧ q) ∨ (p ∧ r)" <br />
shows "p ∧ (q ∨ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 35. Demostrar<br />
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_35:<br />
assumes "p ∨ (q ∧ r)" <br />
shows "(p ∨ q) ∧ (p ∨ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 36. Demostrar<br />
(p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_36:<br />
assumes "(p ∨ q) ∧ (p ∨ r)"<br />
shows "p ∨ (q ∧ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 37. Demostrar<br />
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_37:<br />
assumes "(p ⟶ r) ∧ (q ⟶ r)" <br />
shows "p ∨ q ⟶ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 38. Demostrar<br />
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_38:<br />
assumes "p ∨ q ⟶ r" <br />
shows "(p ⟶ r) ∧ (q ⟶ r)"<br />
oops<br />
<br />
section {* Negaciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 39. Demostrar<br />
p ⊢ ¬¬p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_39:<br />
assumes "p"<br />
shows "¬¬p"<br />
proof -<br />
show "¬¬p" using assms by (rule notnotI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 40. Demostrar<br />
¬p ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_40:<br />
assumes "¬p" <br />
shows "p ⟶ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 41. Demostrar<br />
p ⟶ q ⊢ ¬q ⟶ ¬p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_41:<br />
assumes "p ⟶ q"<br />
shows "¬q ⟶ ¬p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 42. Demostrar<br />
p∨q, ¬q ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_42:<br />
assumes "p∨q"<br />
"¬q" <br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 42. Demostrar<br />
p ∨ q, ¬p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_43:<br />
assumes "p ∨ q"<br />
"¬p" <br />
shows "q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 40. Demostrar<br />
p ∨ q ⊢ ¬(¬p ∧ ¬q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_44:<br />
assumes "p ∨ q" <br />
shows "¬(¬p ∧ ¬q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 45. Demostrar<br />
p ∧ q ⊢ ¬(¬p ∨ ¬q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_45:<br />
assumes "p ∧ q" <br />
shows "¬(¬p ∨ ¬q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 46. Demostrar<br />
¬(p ∨ q) ⊢ ¬p ∧ ¬q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_46:<br />
assumes "¬(p ∨ q)" <br />
shows "¬p ∧ ¬q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 47. Demostrar<br />
¬p ∧ ¬q ⊢ ¬(p ∨ q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_47:<br />
assumes "¬p ∧ ¬q" <br />
shows "¬(p ∨ q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 48. Demostrar<br />
¬p ∨ ¬q ⊢ ¬(p ∧ q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_48:<br />
assumes "¬p ∨ ¬q"<br />
shows "¬(p ∧ q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 49. Demostrar<br />
⊢ ¬(p ∧ ¬p)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_49:<br />
"¬(p ∧ ¬p)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 50. Demostrar<br />
p ∧ ¬p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_50:<br />
assumes "p ∧ ¬p" <br />
shows "q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 51. Demostrar<br />
¬¬p ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_51:<br />
assumes "¬¬p"<br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 52. Demostrar<br />
⊢ p ∨ ¬p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_52:<br />
"p ∨ ¬p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 53. Demostrar<br />
⊢ ((p ⟶ q) ⟶ p) ⟶ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_53:<br />
"((p ⟶ q) ⟶ p) ⟶ p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 54. Demostrar<br />
¬q ⟶ ¬p ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_54:<br />
assumes "¬q ⟶ ¬p"<br />
shows "p ⟶ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 55. Demostrar<br />
¬(¬p ∧ ¬q) ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_55:<br />
assumes "¬(¬p ∧ ¬q)"<br />
shows "p ∨ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 56. Demostrar<br />
¬(¬p ∨ ¬q) ⊢ p ∧ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_56:<br />
assumes "¬(¬p ∨ ¬q)" <br />
shows "p ∧ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 57. Demostrar<br />
¬(p ∧ q) ⊢ ¬p ∨ ¬q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_57:<br />
assumes "¬(p ∧ q)"<br />
shows "¬p ∨ ¬q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 58. Demostrar<br />
⊢ (p ⟶ q) ∨ (q ⟶ p)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_58:<br />
"(p ⟶ q) ∨ (q ⟶ p)"<br />
oops<br />
<br />
end<br />
</source></div>
Dancapmer
https://www.glc.us.es/~jalonso/DAO2012/index.php?title=Relaci%C3%B3n_3&diff=82
Relación 3
2013-03-07T10:25:27Z
<p>Dancapmer: </p>
<hr />
<div><source lang="isar"><br />
header {* R3: Deducción natural proposicional *}<br />
<br />
theory R3<br />
imports Main <br />
begin<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
El objetivo de esta relación es demostrar cada uno de los ejercicios<br />
usando sólo las reglas básicas de deducción natural de la lógica<br />
proposicional (sin usar el método auto).<br />
<br />
Las reglas básicas de la deducción natural son las siguientes:<br />
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q<br />
· conjunct1: P ∧ Q ⟹ P<br />
· conjunct2: P ∧ Q ⟹ Q <br />
· notnotD: ¬¬ P ⟹ P<br />
· notnotI: P ⟹ ¬¬ P<br />
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q <br />
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F <br />
· impI: (P ⟹ Q) ⟹ P ⟶ Q<br />
· disjI1: P ⟹ P ∨ Q<br />
· disjI2: Q ⟹ P ∨ Q<br />
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R <br />
· FalseE: False ⟹ P<br />
· notE: ⟦¬P; P⟧ ⟹ R<br />
· notI: (P ⟹ False) ⟹ ¬P<br />
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q<br />
· iffD1: ⟦Q = P; Q⟧ ⟹ P <br />
· iffD2: ⟦P = Q; Q⟧ ⟹ P<br />
· ccontr: (¬P ⟹ False) ⟹ P<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
text {*<br />
Se usarán las reglas notnotI y mt que demostramos a continuación. *}<br />
<br />
lemma notnotI: "P ⟹ ¬¬ P"<br />
by auto<br />
<br />
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"<br />
by auto<br />
<br />
section {* Implicaciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 1. Demostrar<br />
p ⟶ q, p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_1a:<br />
assumes 1: "p ⟶ q" and<br />
2: "p"<br />
shows "q"<br />
proof -<br />
show 3: "q" using 1 2 by (rule mp) <br />
qed<br />
<br />
lemma ejercicio_1b:<br />
assumes "p ⟶ q"<br />
"p"<br />
shows "q"<br />
proof -<br />
show "q" using assms(1,2) by (rule mp)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 2. Demostrar<br />
p ⟶ q, q ⟶ r, p ⊢ r<br />
------------------------------------------------------------------ *}<br />
<br />
<br />
lemma ejercicio_2a:<br />
assumes 1:"p ⟶ q" and<br />
2:"q ⟶ r" and<br />
3:"p" <br />
shows "r"<br />
proof -<br />
have 4: "q" using 1 3 by (rule mp)<br />
show 5: "r" using 2 4 by (rule mp) <br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 3. Demostrar<br />
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r<br />
------------------------------------------------------------------ *}<br />
<br />
<br />
lemma ejercicio_3a:<br />
assumes 1: "p ⟶ (q ⟶ r)" and<br />
2: "p ⟶ q" and<br />
3: "p" <br />
shows "r"<br />
proof -<br />
have 4: "q ⟶ r" using 1 3 by (rule mp)<br />
have 5: "q" using 2 3 by (rule mp)<br />
show 6: "r" using 4 5 by (rule mp)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 4. Demostrar<br />
p ⟶ q, q ⟶ r ⊢ p ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_4a:<br />
assumes 1: "p ⟶ q" and<br />
2: "q ⟶ r" <br />
shows "p ⟶ r"<br />
proof -<br />
{assume 3:"p" <br />
have 4: "q" using 1 3 by (rule mp)<br />
have 5: "r" using 2 4 by (rule mp)}<br />
thus "p ⟶ r" by (rule impI)<br />
qed<br />
<br />
<br />
lemma ejercicio_4d:<br />
assumes "p ⟶ q" and<br />
"q ⟶ r" <br />
shows "p ⟶ r"<br />
using assms by auto<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 5. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
<br />
lemma ejercicio_5a:<br />
assumes 1: "p ⟶ (q ⟶ r)" <br />
shows "q ⟶ (p ⟶ r)"<br />
proof -<br />
{assume 3: "q"<br />
{assume 4: "p"<br />
have "q ⟶ r" using 1 4 ..<br />
hence 5: "r" using 3 ..}<br />
hence 6: "p ⟶ r" by (rule impI)}<br />
thus "q ⟶ (p ⟶ r)" by (rule impI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 6. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_6a:<br />
assumes 1: "p ⟶ (q ⟶ r)" <br />
shows "(p ⟶ q) ⟶ (p ⟶ r)"<br />
proof -<br />
{assume 2: "p ⟶ q"<br />
{assume 3: "p"<br />
have 4: "q ⟶ r" using 1 3 ..<br />
have 5: "q" using 2 3 ..<br />
have "r" using 4 5 ..}<br />
hence "p ⟶ r" by (rule impI)}<br />
thus "(p ⟶ q) ⟶ (p ⟶ r)" by (rule impI)<br />
qed <br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 7. Demostrar<br />
p ⊢ q ⟶ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_7a:<br />
assumes "p" <br />
shows "q ⟶ p"<br />
proof -<br />
{assume 1: "q"}<br />
show "q ⟶ p" using assms(1) by (rule impI)<br />
qed<br />
<br />
-- Dani<br />
lemma ejercicio_7b:<br />
assumes "p" <br />
shows "q ⟶ p"<br />
proof<br />
assume "q"<br />
show "p" using assms(1) .<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 8. Demostrar<br />
⊢ p ⟶ (q ⟶ p)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_8:<br />
"p ⟶ (q ⟶ p)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 9. Demostrar<br />
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
<br />
lemma ejercicio_9:<br />
assumes 1: "p ⟶ q"<br />
shows "(q ⟶ r) ⟶ (p ⟶ r)"<br />
proof- <br />
{assume 2: "q ⟶ r"<br />
{assume 3: "p"<br />
have 4: "q" using 1 3 by (rule mp)<br />
have 5: "r" using 2 4 by (rule mp)}<br />
hence 6: "p ⟶ r" by (rule impI)}<br />
thus "(q ⟶ r) ⟶ (p ⟶ r)" by (rule impI)<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 10. Demostrar<br />
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_10:<br />
assumes "p ⟶ (q ⟶ (r ⟶ s))" <br />
shows "r ⟶ (q ⟶ (p ⟶ s))"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 11. Demostrar<br />
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_11:<br />
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 12. Demostrar<br />
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_12:<br />
assumes "(p ⟶ q) ⟶ r" <br />
shows "p ⟶ (q ⟶ r)"<br />
oops<br />
<br />
section {* Conjunciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 13. Demostrar<br />
p, q ⊢ p ∧ q<br />
------------------------------------------------------------------ *}<br />
<br />
<br />
<br />
lemma ejercicio_13:<br />
assumes 1:"p" and<br />
2:"q" <br />
shows "p ∧ q"<br />
proof -<br />
show "p ∧ q" using 1 2 by (rule conjI)<br />
qed<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 14. Demostrar<br />
p ∧ q ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_14:<br />
assumes "p ∧ q" <br />
shows "p"<br />
proof -<br />
show "p" using assms by (rule conjunct1)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 15. Demostrar<br />
p ∧ q ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_15:<br />
assumes "p ∧ q" <br />
shows "q"<br />
proof -<br />
show "q" using assms by (rule conjunct2)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 16. Demostrar<br />
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_16:<br />
assumes "p ∧ (q ∧ r)"<br />
shows "(p ∧ q)∧ r"<br />
proof -<br />
have 1: "p" using assms by (rule conjunct1)<br />
have 2: "(q ∧ r)" using assms by (rule conjunct2)<br />
have 3: "q" using 2 by (rule conjunct1)<br />
have 4: "r" using 2 by (rule conjunct2)<br />
have 5: "(p∧q)" using 1 3 by (rule conjI)<br />
show 6: "(p∧q) ∧ r" using 5 4 by (rule conjI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 17. Demostrar<br />
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_17:<br />
assumes "(p∧ q) ∧ r" <br />
shows "p ∧ (q∧ r)"<br />
proof -<br />
have 1: "r" using assms by (rule conjunct2)<br />
have 2: "(p∧q)" using assms by (rule conjunct1)<br />
have 3: "p" using 2 by (rule conjunct1)<br />
have 4: "q" using 2 by (rule conjunct2)<br />
have 5: "(q∧r)" using 4 1 by (rule conjI)<br />
show 6: "p∧(q∧r)" using 3 5 by (rule conjI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 18. Demostrar<br />
p ∧ q ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_18:<br />
assumes "p ∧ q" <br />
shows "p ⟶ q"<br />
proof -<br />
have 1: "q" using assms by (rule conjunct2)<br />
show "p⟶ q" using 1 by (rule impI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 19. Demostrar<br />
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r <br />
------------------------------------------------------------------ *}<br />
<br />
<br />
lemma ejercicio_19:<br />
assumes 1: "(p ⟶ q) ∧ (p ⟶ r)" <br />
shows "p ⟶ (q ∧ r)"<br />
proof (rule impI)<br />
assume 2: "p"<br />
have 3: "p ⟶ q" using assms by (rule conjunct1)<br />
have 4: "q" using 3 2 by (rule mp)<br />
have 5: "p ⟶ r" using assms by (rule conjunct2)<br />
have 6: "r" using 5 2 by (rule mp)<br />
show "q ∧ r" using 4 6 by (rule conjI)<br />
qed<br />
<br />
<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 20. Demostrar<br />
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_20:<br />
assumes "p ⟶ q ∧ r" <br />
shows "(p ⟶ q) ∧ (p ⟶ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 21. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_21:<br />
assumes "p ⟶ (q ⟶ r)" <br />
shows "p ∧ q ⟶ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 22. Demostrar<br />
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_22:<br />
assumes "p ∧ q ⟶ r" <br />
shows "p ⟶ (q ⟶ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 23. Demostrar<br />
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_23:<br />
assumes "(p ⟶ q) ⟶ r" <br />
shows "p ∧ q ⟶ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 24. Demostrar<br />
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_24:<br />
assumes "p ∧ (q ⟶ r)" <br />
shows "(p ⟶ q) ⟶ r"<br />
oops<br />
<br />
section {* Disyunciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 25. Demostrar<br />
p ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_25:<br />
assumes "p"<br />
shows "p ∨ q"<br />
proof -<br />
show "p∨q" using assms by (rule disjI1)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 26. Demostrar<br />
q ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_26:<br />
assumes "q"<br />
shows "p ∨ q"<br />
proof -<br />
show "p∨q" using assms by (rule disjI2)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 27. Demostrar<br />
p ∨ q ⊢ q ∨ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_27:<br />
assumes "p ∨ q"<br />
shows "q ∨ p"<br />
proof - <br />
have "p ∨ q" using assms by this<br />
moreover<br />
{ assume 2: "p"<br />
have "q ∨ p" using 2 by (rule disjI2) }<br />
moreover<br />
{ assume 3: "q"<br />
have "q ∨ p" using 3 by (rule disjI1) }<br />
ultimately show "q ∨ p" by (rule disjE) <br />
qed <br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 28. Demostrar<br />
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_28:<br />
assumes "q ⟶ r" <br />
shows "p ∨ q ⟶ p ∨ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 29. Demostrar<br />
p ∨ p ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_29:<br />
assumes "p ∨ p"<br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 30. Demostrar<br />
p ⊢ p ∨ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_30:<br />
assumes "p" <br />
shows "p ∨ p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 31. Demostrar<br />
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_31:<br />
assumes "p ∨ (q ∨ r)" <br />
shows "(p ∨ q) ∨ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 32. Demostrar<br />
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_32:<br />
assumes "(p ∨ q) ∨ r" <br />
shows "p ∨ (q ∨ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 33. Demostrar<br />
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_33:<br />
assumes "p ∧ (q ∨ r)" <br />
shows "(p ∧ q) ∨ (p ∧ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 34. Demostrar<br />
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_34:<br />
assumes "(p ∧ q) ∨ (p ∧ r)" <br />
shows "p ∧ (q ∨ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 35. Demostrar<br />
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_35:<br />
assumes "p ∨ (q ∧ r)" <br />
shows "(p ∨ q) ∧ (p ∨ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 36. Demostrar<br />
(p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_36:<br />
assumes "(p ∨ q) ∧ (p ∨ r)"<br />
shows "p ∨ (q ∧ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 37. Demostrar<br />
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_37:<br />
assumes "(p ⟶ r) ∧ (q ⟶ r)" <br />
shows "p ∨ q ⟶ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 38. Demostrar<br />
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_38:<br />
assumes "p ∨ q ⟶ r" <br />
shows "(p ⟶ r) ∧ (q ⟶ r)"<br />
oops<br />
<br />
section {* Negaciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 39. Demostrar<br />
p ⊢ ¬¬p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_39:<br />
assumes "p"<br />
shows "¬¬p"<br />
proof -<br />
show "¬¬p" using assms by (rule notnotI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 40. Demostrar<br />
¬p ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_40:<br />
assumes "¬p" <br />
shows "p ⟶ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 41. Demostrar<br />
p ⟶ q ⊢ ¬q ⟶ ¬p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_41:<br />
assumes "p ⟶ q"<br />
shows "¬q ⟶ ¬p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 42. Demostrar<br />
p∨q, ¬q ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_42:<br />
assumes "p∨q"<br />
"¬q" <br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 42. Demostrar<br />
p ∨ q, ¬p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_43:<br />
assumes "p ∨ q"<br />
"¬p" <br />
shows "q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 40. Demostrar<br />
p ∨ q ⊢ ¬(¬p ∧ ¬q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_44:<br />
assumes "p ∨ q" <br />
shows "¬(¬p ∧ ¬q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 45. Demostrar<br />
p ∧ q ⊢ ¬(¬p ∨ ¬q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_45:<br />
assumes "p ∧ q" <br />
shows "¬(¬p ∨ ¬q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 46. Demostrar<br />
¬(p ∨ q) ⊢ ¬p ∧ ¬q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_46:<br />
assumes "¬(p ∨ q)" <br />
shows "¬p ∧ ¬q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 47. Demostrar<br />
¬p ∧ ¬q ⊢ ¬(p ∨ q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_47:<br />
assumes "¬p ∧ ¬q" <br />
shows "¬(p ∨ q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 48. Demostrar<br />
¬p ∨ ¬q ⊢ ¬(p ∧ q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_48:<br />
assumes "¬p ∨ ¬q"<br />
shows "¬(p ∧ q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 49. Demostrar<br />
⊢ ¬(p ∧ ¬p)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_49:<br />
"¬(p ∧ ¬p)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 50. Demostrar<br />
p ∧ ¬p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_50:<br />
assumes "p ∧ ¬p" <br />
shows "q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 51. Demostrar<br />
¬¬p ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_51:<br />
assumes "¬¬p"<br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 52. Demostrar<br />
⊢ p ∨ ¬p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_52:<br />
"p ∨ ¬p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 53. Demostrar<br />
⊢ ((p ⟶ q) ⟶ p) ⟶ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_53:<br />
"((p ⟶ q) ⟶ p) ⟶ p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 54. Demostrar<br />
¬q ⟶ ¬p ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_54:<br />
assumes "¬q ⟶ ¬p"<br />
shows "p ⟶ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 55. Demostrar<br />
¬(¬p ∧ ¬q) ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_55:<br />
assumes "¬(¬p ∧ ¬q)"<br />
shows "p ∨ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 56. Demostrar<br />
¬(¬p ∨ ¬q) ⊢ p ∧ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_56:<br />
assumes "¬(¬p ∨ ¬q)" <br />
shows "p ∧ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 57. Demostrar<br />
¬(p ∧ q) ⊢ ¬p ∨ ¬q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_57:<br />
assumes "¬(p ∧ q)"<br />
shows "¬p ∨ ¬q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 58. Demostrar<br />
⊢ (p ⟶ q) ∨ (q ⟶ p)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_58:<br />
"(p ⟶ q) ∨ (q ⟶ p)"<br />
oops<br />
<br />
end<br />
</source></div>
Dancapmer
https://www.glc.us.es/~jalonso/DAO2012/index.php?title=Relaci%C3%B3n_3&diff=81
Relación 3
2013-03-07T10:24:41Z
<p>Dancapmer: </p>
<hr />
<div><source lang="isar"><br />
header {* R3: Deducción natural proposicional *}<br />
<br />
theory R3<br />
imports Main <br />
begin<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
El objetivo de esta relación es demostrar cada uno de los ejercicios<br />
usando sólo las reglas básicas de deducción natural de la lógica<br />
proposicional (sin usar el método auto).<br />
<br />
Las reglas básicas de la deducción natural son las siguientes:<br />
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q<br />
· conjunct1: P ∧ Q ⟹ P<br />
· conjunct2: P ∧ Q ⟹ Q <br />
· notnotD: ¬¬ P ⟹ P<br />
· notnotI: P ⟹ ¬¬ P<br />
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q <br />
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F <br />
· impI: (P ⟹ Q) ⟹ P ⟶ Q<br />
· disjI1: P ⟹ P ∨ Q<br />
· disjI2: Q ⟹ P ∨ Q<br />
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R <br />
· FalseE: False ⟹ P<br />
· notE: ⟦¬P; P⟧ ⟹ R<br />
· notI: (P ⟹ False) ⟹ ¬P<br />
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q<br />
· iffD1: ⟦Q = P; Q⟧ ⟹ P <br />
· iffD2: ⟦P = Q; Q⟧ ⟹ P<br />
· ccontr: (¬P ⟹ False) ⟹ P<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
text {*<br />
Se usarán las reglas notnotI y mt que demostramos a continuación. *}<br />
<br />
lemma notnotI: "P ⟹ ¬¬ P"<br />
by auto<br />
<br />
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"<br />
by auto<br />
<br />
section {* Implicaciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 1. Demostrar<br />
p ⟶ q, p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_1a:<br />
assumes 1: "p ⟶ q" and<br />
2: "p"<br />
shows "q"<br />
proof -<br />
show 3: "q" using 1 2 by (rule mp) <br />
qed<br />
<br />
lemma ejercicio_1b:<br />
assumes "p ⟶ q"<br />
"p"<br />
shows "q"<br />
proof -<br />
show "q" using assms(1,2) by (rule mp)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 2. Demostrar<br />
p ⟶ q, q ⟶ r, p ⊢ r<br />
------------------------------------------------------------------ *}<br />
<br />
<br />
lemma ejercicio_2a:<br />
assumes 1:"p ⟶ q" and<br />
2:"q ⟶ r" and<br />
3:"p" <br />
shows "r"<br />
proof -<br />
have 4: "q" using 1 3 by (rule mp)<br />
show 5: "r" using 2 4 by (rule mp) <br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 3. Demostrar<br />
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r<br />
------------------------------------------------------------------ *}<br />
<br />
<br />
lemma ejercicio_3a:<br />
assumes 1: "p ⟶ (q ⟶ r)" and<br />
2: "p ⟶ q" and<br />
3: "p" <br />
shows "r"<br />
proof -<br />
have 4: "q ⟶ r" using 1 3 by (rule mp)<br />
have 5: "q" using 2 3 by (rule mp)<br />
show 6: "r" using 4 5 by (rule mp)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 4. Demostrar<br />
p ⟶ q, q ⟶ r ⊢ p ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_4a:<br />
assumes 1: "p ⟶ q" and<br />
2: "q ⟶ r" <br />
shows "p ⟶ r"<br />
proof -<br />
{assume 3:"p" <br />
have 4: "q" using 1 3 by (rule mp)<br />
have 5: "r" using 2 4 by (rule mp)}<br />
thus "p ⟶ r" by (rule impI)<br />
qed<br />
<br />
<br />
lemma ejercicio_4d:<br />
assumes "p ⟶ q" and<br />
"q ⟶ r" <br />
shows "p ⟶ r"<br />
using assms by auto<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 5. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
<br />
lemma ejercicio_5a:<br />
assumes 1: "p ⟶ (q ⟶ r)" <br />
shows "q ⟶ (p ⟶ r)"<br />
proof -<br />
{assume 3: "q"<br />
{assume 4: "p"<br />
have "q ⟶ r" using 1 4 ..<br />
hence 5: "r" using 3 ..}<br />
hence 6: "p ⟶ r" by (rule impI)}<br />
thus "q ⟶ (p ⟶ r)" by (rule impI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 6. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_6a:<br />
assumes 1: "p ⟶ (q ⟶ r)" <br />
shows "(p ⟶ q) ⟶ (p ⟶ r)"<br />
proof -<br />
{assume 2: "p ⟶ q"<br />
{assume 3: "p"<br />
have 4: "q ⟶ r" using 1 3 ..<br />
have 5: "q" using 2 3 ..<br />
have "r" using 4 5 ..}<br />
hence "p ⟶ r" by (rule impI)}<br />
thus "(p ⟶ q) ⟶ (p ⟶ r)" by (rule impI)<br />
qed <br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 7. Demostrar<br />
p ⊢ q ⟶ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_7a:<br />
assumes "p" <br />
shows "q ⟶ p"<br />
proof -<br />
{assume 1: "q"}<br />
show "q⟶ p" using assms(1) by (rule impI)<br />
qed<br />
<br />
-- Dani<br />
lemma ejercicio_7b:<br />
assumes "p" <br />
shows "q \<longrightarrow> p"<br />
proof<br />
assume "q"<br />
show "p" using assms(1) .<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 8. Demostrar<br />
⊢ p ⟶ (q ⟶ p)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_8:<br />
"p ⟶ (q ⟶ p)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 9. Demostrar<br />
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
<br />
lemma ejercicio_9:<br />
assumes 1: "p ⟶ q"<br />
shows "(q ⟶ r) ⟶ (p ⟶ r)"<br />
proof- <br />
{assume 2: "q ⟶ r"<br />
{assume 3: "p"<br />
have 4: "q" using 1 3 by (rule mp)<br />
have 5: "r" using 2 4 by (rule mp)}<br />
hence 6: "p ⟶ r" by (rule impI)}<br />
thus "(q ⟶ r) ⟶ (p ⟶ r)" by (rule impI)<br />
qed<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 10. Demostrar<br />
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_10:<br />
assumes "p ⟶ (q ⟶ (r ⟶ s))" <br />
shows "r ⟶ (q ⟶ (p ⟶ s))"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 11. Demostrar<br />
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_11:<br />
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 12. Demostrar<br />
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_12:<br />
assumes "(p ⟶ q) ⟶ r" <br />
shows "p ⟶ (q ⟶ r)"<br />
oops<br />
<br />
section {* Conjunciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 13. Demostrar<br />
p, q ⊢ p ∧ q<br />
------------------------------------------------------------------ *}<br />
<br />
<br />
<br />
lemma ejercicio_13:<br />
assumes 1:"p" and<br />
2:"q" <br />
shows "p ∧ q"<br />
proof -<br />
show "p ∧ q" using 1 2 by (rule conjI)<br />
qed<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 14. Demostrar<br />
p ∧ q ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_14:<br />
assumes "p ∧ q" <br />
shows "p"<br />
proof -<br />
show "p" using assms by (rule conjunct1)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 15. Demostrar<br />
p ∧ q ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_15:<br />
assumes "p ∧ q" <br />
shows "q"<br />
proof -<br />
show "q" using assms by (rule conjunct2)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 16. Demostrar<br />
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_16:<br />
assumes "p ∧ (q ∧ r)"<br />
shows "(p ∧ q)∧ r"<br />
proof -<br />
have 1: "p" using assms by (rule conjunct1)<br />
have 2: "(q ∧ r)" using assms by (rule conjunct2)<br />
have 3: "q" using 2 by (rule conjunct1)<br />
have 4: "r" using 2 by (rule conjunct2)<br />
have 5: "(p∧q)" using 1 3 by (rule conjI)<br />
show 6: "(p∧q) ∧ r" using 5 4 by (rule conjI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 17. Demostrar<br />
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_17:<br />
assumes "(p∧ q) ∧ r" <br />
shows "p ∧ (q∧ r)"<br />
proof -<br />
have 1: "r" using assms by (rule conjunct2)<br />
have 2: "(p∧q)" using assms by (rule conjunct1)<br />
have 3: "p" using 2 by (rule conjunct1)<br />
have 4: "q" using 2 by (rule conjunct2)<br />
have 5: "(q∧r)" using 4 1 by (rule conjI)<br />
show 6: "p∧(q∧r)" using 3 5 by (rule conjI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 18. Demostrar<br />
p ∧ q ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_18:<br />
assumes "p ∧ q" <br />
shows "p ⟶ q"<br />
proof -<br />
have 1: "q" using assms by (rule conjunct2)<br />
show "p⟶ q" using 1 by (rule impI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 19. Demostrar<br />
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r <br />
------------------------------------------------------------------ *}<br />
<br />
<br />
lemma ejercicio_19:<br />
assumes 1: "(p ⟶ q) ∧ (p ⟶ r)" <br />
shows "p ⟶ (q ∧ r)"<br />
proof (rule impI)<br />
assume 2: "p"<br />
have 3: "p ⟶ q" using assms by (rule conjunct1)<br />
have 4: "q" using 3 2 by (rule mp)<br />
have 5: "p ⟶ r" using assms by (rule conjunct2)<br />
have 6: "r" using 5 2 by (rule mp)<br />
show "q ∧ r" using 4 6 by (rule conjI)<br />
qed<br />
<br />
<br />
<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 20. Demostrar<br />
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_20:<br />
assumes "p ⟶ q ∧ r" <br />
shows "(p ⟶ q) ∧ (p ⟶ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 21. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_21:<br />
assumes "p ⟶ (q ⟶ r)" <br />
shows "p ∧ q ⟶ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 22. Demostrar<br />
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_22:<br />
assumes "p ∧ q ⟶ r" <br />
shows "p ⟶ (q ⟶ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 23. Demostrar<br />
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_23:<br />
assumes "(p ⟶ q) ⟶ r" <br />
shows "p ∧ q ⟶ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 24. Demostrar<br />
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_24:<br />
assumes "p ∧ (q ⟶ r)" <br />
shows "(p ⟶ q) ⟶ r"<br />
oops<br />
<br />
section {* Disyunciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 25. Demostrar<br />
p ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_25:<br />
assumes "p"<br />
shows "p ∨ q"<br />
proof -<br />
show "p∨q" using assms by (rule disjI1)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 26. Demostrar<br />
q ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_26:<br />
assumes "q"<br />
shows "p ∨ q"<br />
proof -<br />
show "p∨q" using assms by (rule disjI2)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 27. Demostrar<br />
p ∨ q ⊢ q ∨ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_27:<br />
assumes "p ∨ q"<br />
shows "q ∨ p"<br />
proof - <br />
have "p ∨ q" using assms by this<br />
moreover<br />
{ assume 2: "p"<br />
have "q ∨ p" using 2 by (rule disjI2) }<br />
moreover<br />
{ assume 3: "q"<br />
have "q ∨ p" using 3 by (rule disjI1) }<br />
ultimately show "q ∨ p" by (rule disjE) <br />
qed <br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 28. Demostrar<br />
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_28:<br />
assumes "q ⟶ r" <br />
shows "p ∨ q ⟶ p ∨ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 29. Demostrar<br />
p ∨ p ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_29:<br />
assumes "p ∨ p"<br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 30. Demostrar<br />
p ⊢ p ∨ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_30:<br />
assumes "p" <br />
shows "p ∨ p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 31. Demostrar<br />
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_31:<br />
assumes "p ∨ (q ∨ r)" <br />
shows "(p ∨ q) ∨ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 32. Demostrar<br />
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_32:<br />
assumes "(p ∨ q) ∨ r" <br />
shows "p ∨ (q ∨ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 33. Demostrar<br />
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_33:<br />
assumes "p ∧ (q ∨ r)" <br />
shows "(p ∧ q) ∨ (p ∧ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 34. Demostrar<br />
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_34:<br />
assumes "(p ∧ q) ∨ (p ∧ r)" <br />
shows "p ∧ (q ∨ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 35. Demostrar<br />
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_35:<br />
assumes "p ∨ (q ∧ r)" <br />
shows "(p ∨ q) ∧ (p ∨ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 36. Demostrar<br />
(p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_36:<br />
assumes "(p ∨ q) ∧ (p ∨ r)"<br />
shows "p ∨ (q ∧ r)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 37. Demostrar<br />
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_37:<br />
assumes "(p ⟶ r) ∧ (q ⟶ r)" <br />
shows "p ∨ q ⟶ r"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 38. Demostrar<br />
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_38:<br />
assumes "p ∨ q ⟶ r" <br />
shows "(p ⟶ r) ∧ (q ⟶ r)"<br />
oops<br />
<br />
section {* Negaciones *}<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 39. Demostrar<br />
p ⊢ ¬¬p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_39:<br />
assumes "p"<br />
shows "¬¬p"<br />
proof -<br />
show "¬¬p" using assms by (rule notnotI)<br />
qed<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 40. Demostrar<br />
¬p ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_40:<br />
assumes "¬p" <br />
shows "p ⟶ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 41. Demostrar<br />
p ⟶ q ⊢ ¬q ⟶ ¬p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_41:<br />
assumes "p ⟶ q"<br />
shows "¬q ⟶ ¬p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 42. Demostrar<br />
p∨q, ¬q ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_42:<br />
assumes "p∨q"<br />
"¬q" <br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 42. Demostrar<br />
p ∨ q, ¬p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_43:<br />
assumes "p ∨ q"<br />
"¬p" <br />
shows "q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 40. Demostrar<br />
p ∨ q ⊢ ¬(¬p ∧ ¬q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_44:<br />
assumes "p ∨ q" <br />
shows "¬(¬p ∧ ¬q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 45. Demostrar<br />
p ∧ q ⊢ ¬(¬p ∨ ¬q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_45:<br />
assumes "p ∧ q" <br />
shows "¬(¬p ∨ ¬q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 46. Demostrar<br />
¬(p ∨ q) ⊢ ¬p ∧ ¬q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_46:<br />
assumes "¬(p ∨ q)" <br />
shows "¬p ∧ ¬q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 47. Demostrar<br />
¬p ∧ ¬q ⊢ ¬(p ∨ q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_47:<br />
assumes "¬p ∧ ¬q" <br />
shows "¬(p ∨ q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 48. Demostrar<br />
¬p ∨ ¬q ⊢ ¬(p ∧ q)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_48:<br />
assumes "¬p ∨ ¬q"<br />
shows "¬(p ∧ q)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 49. Demostrar<br />
⊢ ¬(p ∧ ¬p)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_49:<br />
"¬(p ∧ ¬p)"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 50. Demostrar<br />
p ∧ ¬p ⊢ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_50:<br />
assumes "p ∧ ¬p" <br />
shows "q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 51. Demostrar<br />
¬¬p ⊢ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_51:<br />
assumes "¬¬p"<br />
shows "p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 52. Demostrar<br />
⊢ p ∨ ¬p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_52:<br />
"p ∨ ¬p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 53. Demostrar<br />
⊢ ((p ⟶ q) ⟶ p) ⟶ p<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_53:<br />
"((p ⟶ q) ⟶ p) ⟶ p"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 54. Demostrar<br />
¬q ⟶ ¬p ⊢ p ⟶ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_54:<br />
assumes "¬q ⟶ ¬p"<br />
shows "p ⟶ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 55. Demostrar<br />
¬(¬p ∧ ¬q) ⊢ p ∨ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_55:<br />
assumes "¬(¬p ∧ ¬q)"<br />
shows "p ∨ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 56. Demostrar<br />
¬(¬p ∨ ¬q) ⊢ p ∧ q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_56:<br />
assumes "¬(¬p ∨ ¬q)" <br />
shows "p ∧ q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 57. Demostrar<br />
¬(p ∧ q) ⊢ ¬p ∨ ¬q<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_57:<br />
assumes "¬(p ∧ q)"<br />
shows "¬p ∨ ¬q"<br />
oops<br />
<br />
text {* --------------------------------------------------------------- <br />
Ejercicio 58. Demostrar<br />
⊢ (p ⟶ q) ∨ (q ⟶ p)<br />
------------------------------------------------------------------ *}<br />
<br />
lemma ejercicio_58:<br />
"(p ⟶ q) ∨ (q ⟶ p)"<br />
oops<br />
<br />
end<br />
</source></div>
Dancapmer