Relación 3

header {* R3: Deducción natural proposicional *}

theory R3
imports Main 
begin

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

  Las reglas básicas de la deducción natural son las siguientes:
  · conjI:      ⟦P; Q⟧ ⟹ P ∧ Q
  · conjunct1:  P ∧ Q ⟹ P
  · conjunct2:  P ∧ Q ⟹ Q  
  · notnotD:    ¬¬ P ⟹ P
  · notnotI:    P ⟹ ¬¬ P
  · mp:         ⟦P ⟶ Q; P⟧ ⟹ Q 
  · mt:         ⟦F ⟶ G; ¬G⟧ ⟹ ¬F 
  · impI:       (P ⟹ Q) ⟹ P ⟶ Q
  · disjI1:     P ⟹ P ∨ Q
  · disjI2:     Q ⟹ P ∨ Q
  · disjE:      ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R 
  · FalseE:     False ⟹ P
  · notE:       ⟦¬P; P⟧ ⟹ R
  · notI:       (P ⟹ False) ⟹ ¬P
  · iffI:       ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
  · iffD1:      ⟦Q = P; Q⟧ ⟹ P 
  · iffD2:      ⟦P = Q; Q⟧ ⟹ P
  · ccontr:     (¬P ⟹ False) ⟹ P
  --------------------------------------------------------------------- 
*}

text {*
  Se usarán las reglas notnotI y mt que demostramos a continuación. *}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

section {* Implicaciones *}

text {* --------------------------------------------------------------- 
  Ejercicio 1. Demostrar
       p ⟶ q, p ⊢ q
  ------------------------------------------------------------------ *}

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

-- "Pedro"
lemma ejercicio_1b:
  assumes "p ⟶ q"
          "p"
  shows "q"
proof -
  show "q" using assms(1,2) by (rule mp)
qed
 
text {* --------------------------------------------------------------- 
  Ejercicio 2. Demostrar
     p ⟶ q, q ⟶ r, p ⊢ r
  ------------------------------------------------------------------ *}

-- "Pedro"
lemma ejercicio_2a:
  assumes 1:"p ⟶ q" and
          2:"q ⟶ r" and
          3:"p" 
  shows "r"
proof -
  have 4: "q" using 1 3 by (rule mp)
  show 5: "r" using 2 4 by (rule mp) 
qed
 
text {* --------------------------------------------------------------- 
  Ejercicio 3. Demostrar
     p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r
  ------------------------------------------------------------------ *}
 
-- "Pedro"
lemma ejercicio_3a:
  assumes 1: "p ⟶ (q ⟶ r)" and
          2: "p ⟶ q"       and
          3: "p"           
  shows "r"
proof -
   have 4: "q ⟶ r" using 1 3 by (rule mp)
   have 5: "q" using 2 3 by (rule mp)
   show 6: "r" using 4 5 by (rule mp)
qed
 
text {* --------------------------------------------------------------- 
  Ejercicio 4. Demostrar
     p ⟶ q, q ⟶ r ⊢ p ⟶ r
  ------------------------------------------------------------------ *}

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

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

text {* --------------------------------------------------------------- 
  Ejercicio 5. Demostrar
     p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)
  ------------------------------------------------------------------ *}

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

text {* --------------------------------------------------------------- 
  Ejercicio 6. Demostrar
     p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
  ------------------------------------------------------------------ *}

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

text {* --------------------------------------------------------------- 
  Ejercicio 7. Demostrar
     p ⊢ q ⟶ p
  ------------------------------------------------------------------ *}

-- "Pedro"
lemma ejercicio_7a:
  assumes "p"  
  shows   "q ⟶ p"
proof -
 {assume 1: "q"}
   show "q ⟶ p" using assms(1) by (rule impI)
qed

-- "Dani"
lemma ejercicio_7b:
  assumes "p"  
  shows   "q ⟶ p"
proof
  assume "q"
  show "p" using assms(1) .
qed


text {* --------------------------------------------------------------- 
  Ejercicio 8. Demostrar
     ⊢ p ⟶ (q ⟶ p)
  ------------------------------------------------------------------ *}

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

text {* --------------------------------------------------------------- 
  Ejercicio 9. Demostrar
     p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)
  ------------------------------------------------------------------ *}

-- "Pedro"
lemma ejercicio_9:
  assumes  1: "p ⟶ q"
  shows "(q ⟶ r) ⟶  (p ⟶ r)"
proof- 
   {assume 2: "q ⟶ r"
     {assume 3: "p"
       have 4: "q" using 1 3 by (rule mp)
       have 5: "r" using 2 4 by (rule mp)}
     hence 6: "p ⟶ r" by (rule impI)}
   thus "(q ⟶ r) ⟶ (p ⟶ r)" by (rule impI)
qed


text {* --------------------------------------------------------------- 
  Ejercicio 10. Demostrar
     p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
  ------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_10:
  assumes "p ⟶ (q ⟶ (r ⟶ s))" 
  shows   "r ⟶ (q ⟶ (p ⟶ s))"
proof 
  assume "r"
  show  "q⟶ (p⟶ s)" 
  proof 
    assume "q"
    show "p⟶ s"
    proof
      assume "p"
      with assms have "q⟶ r⟶ s" ..
      hence "r⟶ s" using `q` ..
      thus "s" using `r`..
    qed
  qed    
qed

text {* --------------------------------------------------------------- 
  Ejercicio 11. Demostrar
     ⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
  ------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_11a:
  "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
lemma ejercicio_11:
shows  "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof
  assume 1: "p ⟶ (q ⟶ r)"
  show 2: "(p ⟶ q) ⟶ (p ⟶ r)"
  proof 
    assume 3: "p⟶ q"
    show 4: "p⟶ r" 
    proof 
      assume 5: "p"
      have 6: "q" using 3 5 by (rule mp)
      have 7:"q⟶ r" using 1 5 by (rule mp)
      show  8: "r" using 7 6 ..
    qed
  qed          
qed

text {* --------------------------------------------------------------- 
  Ejercicio 12. Demostrar
     (p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
  ------------------------------------------------------------------ *}

lemma ejercicio_12:
  assumes "(p ⟶ q) ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"
oops

section {* Conjunciones *}

text {* --------------------------------------------------------------- 
  Ejercicio 13. Demostrar
     p, q ⊢  p ∧ q
  ------------------------------------------------------------------ *}

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

text {* --------------------------------------------------------------- 
  Ejercicio 14. Demostrar
     p ∧ q ⊢ p
  ------------------------------------------------------------------ *}

-- "Pedro"
lemma ejercicio_14:
  assumes "p ∧ q"  
  shows   "p"
proof -
show "p" using assms by (rule conjunct1)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 15. Demostrar
     p ∧ q ⊢ q
  ------------------------------------------------------------------ *}

-- "Pedro"
lemma ejercicio_15:
  assumes "p ∧ q" 
  shows   "q"
proof -
show "q" using assms by (rule conjunct2)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 16. Demostrar
     p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
  ------------------------------------------------------------------ *}

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

-- Dani (No estoy seguro de si el ejercicio hecho por Pedro funciona)
lemma ejercicio_16b:
  assumes "p ∧ (q ∧ r)"
  shows   "(p ∧ q) ∧ r"
proof
  have "p" using assms(1) by (rule conjunct1)
  have "q ∧ r" using assms(1) by (rule conjunct2)
  hence "q" by (rule conjunct1)
  show "p ∧ q" using `p` `q` by (rule conjI)
next
  have "q ∧ r" using assms(1) by (rule conjunct2)
  thus "r" ..
qed


text {* --------------------------------------------------------------- 
  Ejercicio 17. Demostrar
     (p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
  ------------------------------------------------------------------ *}

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

text {* --------------------------------------------------------------- 
  Ejercicio 18. Demostrar
     p ∧ q ⊢ p ⟶ q
  ------------------------------------------------------------------ *}

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

text {* --------------------------------------------------------------- 
  Ejercicio 19. Demostrar
     (p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r   
  ------------------------------------------------------------------ *}


-- "Pedro"
lemma ejercicio_19:
  assumes  1: "(p ⟶ q) ∧ (p ⟶ r)" 
  shows "p ⟶  (q ∧ r)"
proof (rule impI)
   assume 2: "p"
   have 3: "p ⟶ q" using assms by (rule conjunct1)
   have 4: "q" using 3 2 by (rule mp)
   have 5: "p ⟶ r" using assms by (rule conjunct2)
   have 6: "r" using 5 2 by (rule mp)
   show "q ∧ r" using 4 6 by (rule conjI)
qed




text {* --------------------------------------------------------------- 
  Ejercicio 20. Demostrar
     p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
  ------------------------------------------------------------------ *}

lemma ejercicio_20:
  assumes "p ⟶ q ∧ r" 
  shows   "(p ⟶ q) ∧ (p ⟶ r)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 21. Demostrar
     p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r
  ------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_21a:
  assumes 1:"p ⟶ (q ⟶ r)" 
  shows   "p ∧ q ⟶ r"
proof
  assume 2:"p∧q"
  show "r" 
  proof -
    have 3: "p" using 2 by (rule conjunct1)
    have 4: "q" using 2 ..
    have 5: "(q⟶ r)" using 1 3 ..
    show 6: "r" using 5 4 ..
  qed
qed


text {* --------------------------------------------------------------- 
  Ejercicio 22. Demostrar
     p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)
  ------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_22a:
  assumes "p ∧ q ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"
proof
  assume "p"
  show "q⟶ r"
  proof
    assume "q"
    have "p∧q" using `p` `q` ..
    show "r" using assms `p∧q`..
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 23. Demostrar
     (p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
  ------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_23a:
  assumes 1:"(p ⟶ q) ⟶ r" 
  shows   "p ∧ q ⟶ r" 
proof 
  assume 2:"p∧q"
  hence 3:"p"  ..
  have 4:"q" using 2 ..
  hence 5: "p⟶ q" ..
  show"r" using 1 5 by (rule mp)
qed

-- Dani
lemma ejercicio_23b:
  assumes "(p ⟶ q) ⟶ r" 
  shows   "p ∧ q ⟶ r"
proof
  assume "p ∧ q"
  hence p ..
  have q using `p ∧ q` ..
  hence "p ⟶ q" ..
  with assms(1) show "r" ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 24. Demostrar
     p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
  ------------------------------------------------------------------ *}

-- Dani
lemma ejercicio_24a:
  assumes "p ∧ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ r"
proof
  assume "p ⟶ q"
  have "p" using assms(1) ..
  with `p ⟶ q` have "q" ..
  have "q ⟶ r" using assms(1) ..
  thus "r" using `q` ..
qed


section {* Disyunciones *}

text {* --------------------------------------------------------------- 
  Ejercicio 25. Demostrar
     p ⊢ p ∨ q
  ------------------------------------------------------------------ *}

-- "Pedro"
lemma ejercicio_25:
  assumes "p"
  shows   "p ∨ q"
proof -
show "p∨q" using assms by (rule disjI1)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 26. Demostrar
     q ⊢ p ∨ q
  ------------------------------------------------------------------ *}

-- "Pedro"
lemma ejercicio_26:
  assumes "q"
  shows   "p ∨ q"
proof -
show "p∨q" using assms by (rule disjI2)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 27. Demostrar
     p ∨ q ⊢ q ∨ p
  ------------------------------------------------------------------ *}

-- "Pedro"
lemma ejercicio_27:
  assumes "p ∨ q"
  shows   "q ∨ p"
proof - 
have "p ∨ q" using assms by this
  moreover
  { assume 2: "p"
    have "q ∨ p" using 2 by (rule disjI2) }
  moreover
  { assume 3: "q"
    have "q ∨ p" using 3 by (rule disjI1) }
  ultimately show "q ∨ p" by (rule disjE) 
qed  

text {* --------------------------------------------------------------- 
  Ejercicio 28. Demostrar
     q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
  ------------------------------------------------------------------ *}
-- "Pedro"
lemma ejercicio_28a:
  assumes "q ⟶ r" 
  shows   "p ∨ q ⟶ p ∨ r"
proof 
  assume 1: "p∨q"
  moreover
  {assume "p"
    hence "p∨r" by (rule disjI1)}
  moreover
  {assume "q"
    have "r" using assms `q`..
    hence "p∨r" ..}
  ultimately
  show "p∨r" ..
qed 

text {* --------------------------------------------------------------- 
  Ejercicio 29. Demostrar
     p ∨ p ⊢ p
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_29a:
  assumes "p ∨ p"
  shows   "p"

proof-
have "p∨p" using assms by this
  moreover
  {assume "p"
    hence "p" by this}
  moreover
  {assume "p"
    hence "p" by this}
  ultimately
  show "p" ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 30. Demostrar
     p ⊢ p ∨ p
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_30a:
  assumes "p" 
  shows   "p ∨ p"
proof -
show "p∨p" using assms ..

text {* --------------------------------------------------------------- 
  Ejercicio 31. Demostrar
     p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r
  ------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_31a:
  assumes "p ∨ (q ∨ r)" 
  shows   "(p ∨ q) ∨ r"
proof -
  have 1: "p ∨ (q ∨ r)" using assms by this
  moreover
  {assume "p"
    hence "(p∨q)" ..
    hence "(p∨q)∨r" ..}
  moreover
  {assume "(q∨r)"
    moreover
    {assume "q"
      hence "(p∨q)"..
      hence "(p∨q)∨r" ..}
    moreover
    {assume "r"
      hence "(p∨q)∨r" ..}
    ultimately
    have "(p∨q)∨r"..}
  ultimately
  show "(p∨q)∨r" ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 32. Demostrar
     (p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
  ------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_32:
  assumes "(p ∨ q) ∨ r" 
  shows   "p ∨ (q ∨ r)"
using assms(1)
proof
  assume "p∨q"
  thus "p∨q∨r" 
    proof
    assume "p"
    thus "p∨q∨r" ..
    next
    assume "q"
    hence "q∨r" ..
    thus "p∨q∨r" ..
    qed
next
  assume "r"
  hence "q∨r" ..
  thus "p∨q∨r" ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 33. Demostrar
     p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
  ------------------------------------------------------------------ *}
-- "Pedro"
lemma ejercicio_33a:
  assumes "p ∧ (q ∨ r)" 
  shows   "(p ∧ q) ∨ (p ∧ r)"
proof -
  have 1: "p" using assms ..
  have 2: "q∨r" using assms ..
  moreover
  {assume 3: "q"
    have "(p∧q)" using 1 3 ..
    hence "(p ∧ q) ∨ (p ∧ r)" ..}
  moreover
  {assume 4: "r"
    have "p∧r" using 1 4 ..
    hence "(p ∧ q) ∨ (p ∧ r)" ..}
  ultimately
  show "(p ∧ q) ∨ (p ∧ r)" ..
qed


text {* --------------------------------------------------------------- 
  Ejercicio 34. Demostrar
     (p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
  ------------------------------------------------------------------ *}
 -- "Pedro Ros"
lemma ejercicio_34a:
  assumes "(p ∧ q) ∨ (p ∧ r)" 
  shows   "p ∧ (q ∨ r)"
proof -
  have 1: "(p ∧ q) ∨ (p ∧ r)" using assms by this
  moreover
  {assume "(p ∧ q)"
    hence "p" ..
    have "q" using `p ∧ q` ..
    hence "(q∨r)"..
    have "p∧(q∨r)" using `p``(q∨r)`..}
  moreover
  {assume "(p∧r)"
    hence "p" ..
    have "r" using `p ∧ r` ..
    hence "(q∨r)"..
    have "p∧(q∨r)" using `p``(q∨r)`..}
  ultimately
  show "p ∧ (q ∨ r)" ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 35. Demostrar
     p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_35a:
  assumes "p ∨ (q ∧ r)" 
  shows   "(p ∨ q) ∧ (p ∨ r)"
proof -
  have 1: "p ∨ (q ∧ r)" using assms by this
  moreover
  {assume "p"
    hence 2: "(p∨q)" ..
    have 3: "(p∨r)" using `p` ..
    have 4: "(p ∨ q) ∧ (p ∨ r)" using 2 3 ..}
  moreover
  {assume 5:"(q∧r)"
    hence 6: "q" ..
    have 7: "r" using 5 ..
    have 8: "p∨q" using 6 ..
    have 9: "p∨r" using 7 ..
    have "(p ∨ q) ∧ (p ∨ r)"using 8 9 ..}
  ultimately
  show "(p ∨ q) ∧ (p ∨ r)" ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 36. Demostrar
     (p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)
  ------------------------------------------------------------------ *}
text {* Pedro. Vienen demostradas en la teoría y necesito usarlas *}

lemma or2: "⟦P∨Q; ¬P⟧⟹ Q"
by auto

lemma LEM: "P ∨ ¬P"
by auto

lemma ejercicio_36a:
  assumes "(p ∨ q) ∧ (p ∨ r)"
  shows   "p ∨ (q ∧ r)"
using LEM
proof 
  have 1:"(p∨q)" using assms ..
  have 2: "(p∨r)" using assms ..
  assume "p"
  thus "p∨(q∧r)" ..
next
  have 1:"(p∨q)" using assms ..
  have 2: "(p∨r)" using assms ..
  assume "¬p"
  have "q" using 1 `¬p` by (rule or2)
  have "r" using 2 `¬p` by (rule or2)
  have "q∧r" using `q` `r` ..
  thus "p∨(q∧r)" .. 
qed

text {* --------------------------------------------------------------- 
  Ejercicio 37. Demostrar
     (p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
  ------------------------------------------------------------------ *}

lemma ejercicio_37a:
  assumes "(p ⟶ r) ∧ (q ⟶ r)" 
  shows   "p ∨ q ⟶ r"
proof (rule impI)
  assume 0:"p∨q"
  show "r"
  proof (rule disjE)
    show "p∨q" using 0 .
  next
    assume p
    have 1: "p⟶r" using assms ..
    thus r using `p` ..
  next
    assume q
    have 2: "q⟶r" using assms ..
    thus r using `q`..
  qed
qed


text {* --------------------------------------------------------------- 
  Ejercicio 38. Demostrar
     p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
  ------------------------------------------------------------------ *}


-- Dani
lemma ejercicio_38:
  assumes "p ∨ q ⟶ r" 
  shows   "(p ⟶ r) ∧ (q ⟶ r)"
proof
  show "p ⟶ r"
    proof
      assume p
      hence "p ∨ q" ..
      with assms show r ..
    qed
next
  show "q ⟶ r"
    proof
      assume q
      hence "p ∨ q" ..
      with assms show r ..
    qed
qed

section {* Negaciones *}

text {* --------------------------------------------------------------- 
  Ejercicio 39. Demostrar
     p ⊢ ¬¬p
  ------------------------------------------------------------------ *}

-- "Pedro"
lemma ejercicio_39:
  assumes "p"
  shows   "¬¬p"
proof -
show "¬¬p" using assms by (rule notnotI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 40. Demostrar
     ¬p ⊢ p ⟶ q
  ------------------------------------------------------------------ *}
lemma ejercicio_40:
  assumes "¬p" 
  shows   "p ⟶ q"
proof (rule impI)
assume p
with assms show q ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 41. Demostrar
     p ⟶ q ⊢ ¬q ⟶ ¬p
  ------------------------------------------------------------------ *}

lemma ejercicio_41:
  assumes "p ⟶ q"
  shows   "¬q ⟶ ¬p"
proof (rule impI)
  {assume "¬q"
   with assms show "¬p"  by (rule mt) }
qed

text {* --------------------------------------------------------------- 
  Ejercicio 42. Demostrar
     p∨q, ¬q ⊢ p
  ------------------------------------------------------------------ *}

lemma ejercicio_42:
  assumes "p∨q"
          "¬q" 
  shows   "p"
proof -
  note `p∨q`
  moreover
  {assume "p"
    hence "p" by this}
  moreover
  {assume "q"
    with assms (2) have "p" ..}
  ultimately show "p" ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 42. Demostrar
     p ∨ q, ¬p ⊢ q
  ------------------------------------------------------------------ *}

lemma ejercicio_43:
  assumes "p ∨ q"
          "¬p" 
  shows   "q"
proof -
  note `p∨q`
  moreover
  {assume "p"
   with assms (2) have False..
   hence "q"..}
  moreover
  {assume "q"
   hence "q" .}
  ultimately show "q"..
qed
text {* --------------------------------------------------------------- 
  Ejercicio 40. Demostrar
     p ∨ q ⊢ ¬(¬p ∧ ¬q)
  ------------------------------------------------------------------ *}
lemma ejercicio_44:
  assumes "p ∨ q" 
  shows   "¬(¬p ∧ ¬q)"
proof -
  {assume "¬p∧¬q"
   note `p∨q`
   moreover
   {have "¬p" using `¬p∧¬q`by (rule conjunct1)
    assume "p"
    with `¬p`have False by (rule notE)}
   moreover
   {have "¬q" using `¬p∧¬q`by (rule conjunct2)
    assume "q"
    with `¬q`have False by (rule notE)}
   ultimately have False by (rule disjE)}
  thus "¬(¬p∧¬q)" by (rule notI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 45. Demostrar
     p ∧ q ⊢ ¬(¬p ∨ ¬q)
  ------------------------------------------------------------------ *}

lemma ejercicio_45:
  assumes "p ∧ q" 
  shows   "¬(¬p ∨ ¬q)"
proof (rule notI)
  assume "¬p∨¬q"
  show False
  proof (rule disjE)
  {show "¬p∨¬q" using `¬p∨¬q`.
   next
   show "¬p⟹False"
   proof -
   {assume "¬p"
    have "p" using assms..
    with `¬p`show False..}
   qed
   next
   show "¬q⟹False"
   proof -
   {assume "¬q"
    have "q" using assms..
    with `¬q`show False..}
   qed}
  qed 
qed

text {* --------------------------------------------------------------- 
  Ejercicio 46. Demostrar
     ¬(p ∨ q) ⊢ ¬p ∧ ¬q
  ------------------------------------------------------------------ *}

lemma ejercicio_46:
  assumes "¬(p ∨ q)" 
  shows   "¬p ∧ ¬q"
proof (rule conjI)
  show "¬p"
  proof (rule notI)
  {assume "p"
   hence "p∨q"..
   with assms show False..}
  qed
  next
  show "¬q"
  proof (rule notI)
  {assume "q"
   hence "p∨q"..
   with assms show False..}
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 47. Demostrar
     ¬p ∧ ¬q ⊢ ¬(p ∨ q)
  ------------------------------------------------------------------ *}

lemma ejercicio_47:
  assumes "¬p ∧ ¬q" 
  shows   "¬(p ∨ q)"
proof (rule notI)
  assume "p∨q"
  show False
  proof (rule disjE)
  {show "p∨q" using `p∨q` .
   next
   show "p⟹False"
   proof -
   {have "¬p" using assms..
    assume "p"
    with `¬p`show False..}
   qed
   next
   show "q⟹False"
   proof -
   {have "¬q" using assms..
    assume "q"
    with `¬q`show False..}
   qed}
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 48. Demostrar
     ¬p ∨ ¬q ⊢ ¬(p ∧ q)
  ------------------------------------------------------------------ *}

lemma ejercicio_48b:
  assumes "¬p ∨ ¬q"
  shows   "¬(p ∧ q)"
proof (rule disjE)
  show "¬p ∨ ¬q" using assms .
next
  assume 1: "¬p"
  show "¬(p∧q)"
  proof
  assume "p∧q"
  hence 2: "p" ..
  show  "False" using 1 2 ..
  qed
next
  assume 1: "¬q"
  show "¬(p∧q)"
  proof
  assume "p∧q"
  hence 2: "q" ..
  show  "False" using 1 2 ..
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 49. Demostrar
     ⊢ ¬(p ∧ ¬p)
  ------------------------------------------------------------------ *}
lemma ejercicio_49:
  "¬(p ∧ ¬p)"
proof (rule notI)
  assume "p∧¬p"
  hence "¬p"..
  have "p" using `p∧¬p`..
  with `¬p`show False..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 50. Demostrar
     p ∧ ¬p ⊢ q
  ------------------------------------------------------------------ *}
lemma ejercicio_50:
  assumes "p ∧ ¬p" 
  shows   "q"
proof (rule notE)
  show "p" using assms ..
  show "¬p" using assms ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 51. Demostrar
     ¬¬p ⊢ p
  ------------------------------------------------------------------ *}

lemma ejercicio_51b:
  assumes "¬¬p"
  shows   "p"
using assms by (rule notnotD)

text {* --------------------------------------------------------------- 
  Ejercicio 52. Demostrar
     ⊢ p ∨ ¬p
  ------------------------------------------------------------------ *}

lemma ejercicio_52:
  "p ∨ ¬p"
proof (rule ccontr)
  {assume "¬(p∨¬p)"
   have "p"
   proof (rule ccontr)
   {assume "¬p"
    hence "p∨¬p"..
    with `¬(p∨¬p)` show False..}
   qed
   hence "p∨¬p"..
   with `¬(p∨¬p)` show False..}
qed

text {* --------------------------------------------------------------- 
  Ejercicio 53. Demostrar
     ⊢ ((p ⟶ q) ⟶ p) ⟶ p
  ------------------------------------------------------------------ *}
lemma ejercicio_53:
  "((p ⟶ q) ⟶ p) ⟶ p"
proof (rule impI)
  assume "(p⟶q)⟶p"
  show "p"
  proof (rule ccontr)
    note `(p⟶q)⟶p`
    assume "¬p"
    with `(p⟶q)⟶p` have "¬(p⟶q)" by (rule mt)
    {assume "p"
     with `¬p` have "q" by (rule notE)}
    hence "p⟶q" by (rule impI)
    with `¬(p⟶q)` show False by (rule notE)
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 54. Demostrar
     ¬q ⟶ ¬p ⊢ p ⟶ q
-------------------------------------------------------*}
lemma ejercicio_54b:
  assumes "¬q ⟶ ¬p"
  shows   "p ⟶ q"
proof
assume "p"
hence "¬¬p" by (rule notnotI)
with assms have "¬¬q" by (rule mt)
thus q by (rule notnotD)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 55. Demostrar
     ¬(¬p ∧ ¬q) ⊢ p ∨ q
  ------------------------------------------------------------------ *}

lemma ejercicio_55b:
  assumes "¬(¬p ∧ ¬q)"
  shows   "p ∨ q"
proof (rule ccontr)
assume "¬(p ∨ q)"
hence " ¬p ∧ ¬q" by (rule ejercicio_46)
with assms show "False" ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 56. Demostrar
     ¬(¬p ∨ ¬q) ⊢ p ∧ q
  ------------------------------------------------------------------ *}
lemma ejercicio_56:
  assumes "¬(¬p ∨ ¬q)" 
  shows   "p ∧ q"
proof(rule conjI)
  show "p"
  proof(rule ccontr)
   {assume "¬p"
    hence "¬p∨¬q"..
    with assms show False..}
  qed
  show "q"
  proof(rule ccontr)
   {assume "¬q"
    hence "¬p∨¬q"..
    with assms show False..}
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 57. Demostrar
     ¬(p ∧ q) ⊢ ¬p ∨ ¬q
  ------------------------------------------------------------------ *}
lemma ejercicio_57:
  assumes "¬(p ∧ q)"
  shows   "¬p ∨ ¬q"
proof -
  have "¬p∨p"..
  moreover
   {assume "¬p"
    hence "¬p∨¬q"..}
  moreover
   {assume "p"
    have "¬q∨q"..
    moreover
    {assume "¬q"
     hence "¬p∨¬q"..}
    moreover
    {assume "q"
     with `p`have "p∧q"..
     with `¬(p∧q)` have "¬p∨¬q"..}
    ultimately have "¬p∨¬q"..}
  ultimately show "¬p∨¬q"..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 58. Demostrar
     ⊢ (p ⟶ q) ∨ (q ⟶ p)
  ------------------------------------------------------------------ *}

lemma ejercicio_58:
  "(p ⟶ q) ∨ (q ⟶ p)"
proof -
  have  "¬p ∨ p" ..
  moreover
  {assume "¬p"
    {assume "p"
     with `¬p` have "q" ..}
   hence "p⟶q" ..
   hence "(p⟶q)∨(q⟶p)" ..}
  moreover
  {assume "p"
    {assume "q"
     note `p`}
   hence "q⟶p"..
   hence "(p⟶q)∨(q⟶p)"..}
  ultimately show "(p⟶q)∨(q⟶p)" ..
qed

end