Ver el código de «GLC T1R1» - DAO (Demostración asistida por ordenador)

<source lang="isabelle">
header {* T1R1: Deducción natural proposicional *}

theory T1R1
imports Main 
begin

text {*
  --------------------------------------------------------------------- 
  El objetivo de esta relación es lemas usando sólo las reglas básicas
  de deducción natural de la lógica proposicional. 

  Los ejercicios son los de la asignatura de "Lógica informática" que se
  encuentran en http://goo.gl/yrPLn

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

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

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

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

section {* Implicaciones *}

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

-- "La demostración detallada es"
lemma ejercicio_1_1:
  assumes 1: "p ⟶ q" and
          2: "p"
  shows "q"
proof - 
   show "q" using 1 2 by (rule mp)
qed

-- "La demostración estructurada es"
lemma ejercicio_1_2:
  assumes "p ⟶ q"
          "p"
  shows "q"
proof - 
   show "q" using assms ..
qed

-- "La demostración automática es"
lemma ejercicio_1_3:
  assumes "p ⟶ q"
          "p"
  shows "q"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_2_1:
  assumes 1: "p ⟶ q" and 
          2: "q ⟶ r" and 
          3: "p" 
  shows "r"
proof -
  have 4: "q" using 1 3 by (rule mp)
  show "r" using 2 4 by (rule mp)
qed

-- "La demostración estructurada es"
lemma ejercicio_2_2:
  assumes "p ⟶ q"
          "q ⟶ r"
          "p" 
  shows "r"
proof -
  have "q" using assms(1,3) ..
  show "r" using assms(2) `q` ..
qed

-- "La demostración automática es"
lemma ejercicio_2_3:
  assumes "p ⟶ q"
          "q ⟶ r"
          "p" 
  shows "r"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_3_1:
  assumes 1: "p ⟶ (q ⟶ r)" and 
          2: "p ⟶ q" and  
          3: "p"
  shows "r"
proof -
  have 4: "q" using 2 3 by (rule mp)
  have 5: "q ⟶ r" using 1 3 by (rule mp)
  show "r" using 5 4 by (rule mp)
qed

-- "La demostración estructurada es"
lemma ejercicio_3_2:
  assumes "p ⟶ (q ⟶ r)"
          "p ⟶ q"
          "p"
  shows   "r"
proof -
  have "q" using assms(2,3) ..
  have "q ⟶ r" using assms(1,3) ..
  thus "r" using `q` ..
qed

-- "La demostración automática es"
lemma ejercicio_3_3:
  assumes "p ⟶ (q ⟶ r)"
          "p ⟶ q"
          "p"
  shows   "r"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_4_1:
  assumes 1: "p ⟶ q" and 
          2: "q ⟶ r" 
  shows "p ⟶ r"
proof (rule impI)
  assume 3: "p"
  have 4: "q" using 1 3 by (rule mp)
  show "r" using 2 4 by (rule mp)
qed

-- "La demostración estructurada es"
lemma ejercicio_4_2:
  assumes "p ⟶ q"
          "q ⟶ r" 
  shows   "p ⟶ r"
proof
  assume "p"
  with assms(1) have "q" ..
  with assms(2) show "r" ..
qed

-- "La demostración automática es"
lemma ejercicio_4_3:
  assumes "p ⟶ q"
          "q ⟶ r" 
  shows   "p ⟶ r"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_5_1:
  assumes 1: "p ⟶ (q ⟶ r)" 
  shows   "q ⟶ (p ⟶ r)"
proof (rule impI)
  assume 2: "q"
  show "p ⟶ r"
  proof (rule impI)
    assume 3: "p"
    have "q ⟶ r" using 1 3 by (rule mp)
    thus "r" using 2 by (rule mp)
  qed
qed

-- "La demostración estructurada es"
lemma ejercicio_5_2:
  assumes "p ⟶ (q ⟶ r)" 
  shows   "q ⟶ (p ⟶ r)"
proof 
  assume "q"
  show "p ⟶ r"
  proof 
    assume "p"
    with assms(1) have "q ⟶ r" ..
    thus "r" using `q` ..
  qed
qed

-- "La demostración automática es"
lemma ejercicio_5_3:
  assumes "p ⟶ (q ⟶ r)" 
  shows   "q ⟶ (p ⟶ r)"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_6_1:
  assumes 1: "p ⟶ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ (p ⟶ r)"
proof (rule impI)
  assume 2: "p ⟶ q"
  show "p ⟶ r"
  proof (rule impI)
    assume 3: "p"
    have 4: "q" using 2 3 by (rule mp)
    have 5: "q ⟶ r" using 1 3 by (rule mp)
    show "r" using 5 4 by (rule mp)
  qed
qed

-- "La demostración estructurada es"
lemma ejercicio_6_2:
  assumes "p ⟶ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ (p ⟶ r)"
proof 
  assume "p ⟶ q"
  show "p ⟶ r"
  proof 
    assume "p"
    with `p ⟶ q` have "q" ..
    have "q ⟶ r" using assms(1) `p` ..
    thus "r" using `q` ..
  qed
qed

-- "La demostración automática es"
lemma ejercicio_6_3:
  assumes "p ⟶ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ (p ⟶ r)"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_7_1:
  assumes 1: "p"  
  shows      "q ⟶ p"
proof (rule impI)
  assume 2: "q"
  show "p" using 1 by this
qed

-- "La demostración estructurada es"
lemma ejercicio_7_2:
  assumes "p"  
  shows   "q ⟶ p"
proof 
  assume "q"
  show "p" using assms(1) .
qed

-- "La demostración automática es"
lemma ejercicio_7_3:
  assumes "p"  
  shows   "q ⟶ p"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_8_1:
  "p ⟶ (q ⟶ p)"
proof (rule impI)
  assume 1: "p"
  show "q ⟶ p"
  proof (rule impI)
    assume 2: "q"
    show "p" using 1 by this
  qed
qed

-- "La demostración estructurada es"
lemma ejercicio_8_2:
  "p ⟶ (q ⟶ p)"
proof 
  assume "p"
  show "q ⟶ p"
  proof 
    assume "q"
    show "p" using `p` .
  qed
qed

-- "La demostración automática es"
lemma ejercicio_8_3:
  "p ⟶ (q ⟶ p)"
by auto

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

-- "La demostración detallada es"
lemma ejercicio_9_1:
  assumes 1: "p ⟶ q" 
  shows      "(q ⟶ r) ⟶ (p ⟶ r)"
proof (rule impI)
  assume 2: "q ⟶ r"
  show "p ⟶ r"
  proof (rule impI)
    assume 3: "p"
    have 4: "q" using 1 3 by (rule mp)
    show "r" using 2 4 by (rule mp) 
  qed
qed

-- "La demostración estructurada es"
lemma ejercicio_9_2:
  assumes "p ⟶ q" 
  shows   "(q ⟶ r) ⟶ (p ⟶ r)"
proof 
  assume "q ⟶ r"
  show "p ⟶ r"
  proof 
    assume "p"
    with assms(1) have "q" ..
    with `q ⟶ r` show "r" ..
  qed
qed

-- "La demostración automática es"
lemma ejercicio_9_3:
  assumes "p ⟶ q" 
  shows   "(q ⟶ r) ⟶ (p ⟶ r)"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_10_1:
  assumes 1: "p ⟶ (q ⟶ (r ⟶ s))" 
  shows      "r ⟶ (q ⟶ (p ⟶ s))"
proof -
  { assume 2: "r"
    { assume 3: "q"
      { assume 4: "p"
        have 5: "q ⟶ (r ⟶ s)" using 1 4 by (rule mp)
        have 6: "r ⟶ s" using 5 3 by (rule mp)
        have 7: "s" using 6 2 by (rule mp) }
      hence 8: "p ⟶ s" by (rule impI) }
    hence 9: "q ⟶ (p ⟶ s)" by (rule impI) }
  thus 10: "r ⟶ (q ⟶ (p ⟶ s))" by (rule impI) 
qed

-- "Una variante de la demostración anterior es"
lemma ejercicio_10_1b:
  assumes 1: "p ⟶ (q ⟶ (r ⟶ s))" 
  shows      "r ⟶ (q ⟶ (p ⟶ s))"
proof (rule impI)
  assume 2: "r"
  show "q ⟶ (p ⟶ s)"
  proof (rule impI)
    assume 3: "q"
    show "p ⟶ s"
    proof (rule impI)
      assume 4: "p"
      have 5: "q ⟶ (r ⟶ s)" using 1 4 by (rule mp)
      have 6: "r ⟶ s" using 5 3 by (rule mp)
      show "s" using 6 2 by (rule mp)
    qed
  qed
qed

-- "La demostración estructurada es"
lemma ejercicio_10_2:
  assumes "p ⟶ (q ⟶ (r ⟶ s))" 
  shows   "r ⟶ (q ⟶ (p ⟶ s))"
proof 
  assume "r"
  show "q ⟶ (p ⟶ s)"
  proof 
    assume "q"
    show "p ⟶ s"
    proof 
      assume "p"
      with assms(1) have "q ⟶ (r ⟶ s)" ..
      hence "r ⟶ s" using `q` ..
      thus "s" using `r` ..
    qed
  qed
qed

-- "La demostración automática es"
lemma ejercicio_10_3:
  assumes "p ⟶ (q ⟶ (r ⟶ s))" 
  shows   "r ⟶ (q ⟶ (p ⟶ s))"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_11_1:
  "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof -
  { assume 1: "p ⟶ (q ⟶ r)"
    { assume 2: "p ⟶ q"
      { assume 3: "p"
        have 4: "q" using 2 3 by (rule mp)
        have 5: "q ⟶ r" using 1 3 by (rule mp)
        have 6: "r" using 5 4 by (rule mp) }
      hence 7: "p ⟶ r" by (rule impI) }
    hence 8: "(p ⟶ q) ⟶ (p ⟶ r)" by (rule impI) }
  thus "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))" by (rule impI)
qed 

-- "La demostración estructurada es"
lemma ejercicio_11_2:
  "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof 
  assume "p ⟶ (q ⟶ r)"
  { assume "p ⟶ q"
    { assume "p"
      with `p ⟶ q` have "q" ..
      have "q ⟶ r" using `p ⟶ (q ⟶ r)` `p` ..
      hence "r" using `q` .. }
    hence "p ⟶ r" .. }
  thus "(p ⟶ q) ⟶ (p ⟶ r)" .. 
qed 

-- "La demostración automática es"
lemma ejercicio_11_3:
  "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
by auto

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

-- "La demostración detallada es"
lemma ejercicio_12_1:
  assumes 1: "(p ⟶ q) ⟶ r" 
  shows      "p ⟶ (q ⟶ r)"
proof -
  { assume 2: "p"
    { assume 3: "q"
      { assume 4: "p"
        have 5: "q" using 3 by this } 
      hence 6: "p ⟶ q" by (rule impI)
      have 7: "r" using 1 6 by (rule mp) } 
    hence 8: "q ⟶ r" by (rule impI) } 
  thus 9: "p ⟶ (q ⟶ r)" by (rule impI) 
qed

-- "La demostración estructurada es"
lemma ejercicio_12_2:
  assumes "(p ⟶ q) ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"
proof 
  assume "p"
  { assume "q"
    { assume "p"
      have "q" using `q` . } 
    hence "p ⟶ q" ..
    with assms(1) have "r" .. } 
  thus "q ⟶ r" ..
qed

-- "La demostración automática es"
lemma ejercicio_12_3:
  assumes "(p ⟶ q) ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"
using assms
by auto

section {* Conjunciones *}

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

-- "La demostración detallada es"
lemma ejercicio_13_1:
  assumes 1: "p" and 
          2: "q" 
  shows "p ∧ q"
proof -
  show "p ∧ q" using assms by (rule conjI)
qed

-- "La demostración estructurada es"
lemma ejercicio_13_2:
  assumes "p"
          "q" 
  shows "p ∧ q"
proof 
  show "p" using assms(1) .
next
  show "q" using assms(2) .
qed

-- "La demostración automática es"
lemma ejercicio_13_3:
  assumes "p"
          "q" 
  shows "p ∧ q"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_14_1:
  assumes 1: "p ∧ q"  
  shows      "p"
proof -
  show "p" using 1 by (rule conjunct1)
qed 

-- "La demostración estructurada es"
lemma ejercicio_14_2:
  assumes "p ∧ q"  
  shows   "p"
proof -
  show "p" using assms ..
qed 

-- "La demostración automática es"
lemma ejercicio_14_3:
  assumes "p ∧ q"  
  shows   "p"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_15_1:
  assumes 1: "p ∧ q" 
  shows      "q"
proof -
  show "q" using 1 by (rule conjunct2)
qed 

-- "La demostración estructurada es"
lemma ejercicio_15_2:
  assumes "p ∧ q" 
  shows   "q"
proof -
  show "q" using assms ..
qed 

-- "La demostración automática es"
lemma ejercicio_15_3:
  assumes "p ∧ q" 
  shows   "q"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_16_1:
  assumes 1: "p ∧ (q ∧ r)"
  shows      "(p ∧ q) ∧ r"
proof -
  have 2: "p" using 1 by (rule conjunct1)
  have 3: "q ∧ r" using 1 by (rule conjunct2)
  have 4: "q" using 3 by (rule conjunct1)
  have 5: "p ∧ q" using 2 4 by (rule conjI)
  have 6: "r" using 3 by (rule conjunct2)
  show 7: "(p ∧ q) ∧ r" using 5 6 by (rule conjI)
qed

-- "La demostración estructurada es"
lemma ejercicio_16_2:
  assumes "p ∧ (q ∧ r)"
  shows   "(p ∧ q) ∧ r"
proof 
  show "p ∧ q"
  proof
    show "p" using assms ..
  next
    have "q ∧ r" using assms ..
    thus "q" ..
  qed
next
    have "q ∧ r" using assms ..
    thus "r" ..
qed

-- "La demostración automática es"
lemma ejercicio_16_3:
  assumes "p ∧ (q ∧ r)"
  shows   "(p ∧ q) ∧ r"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_17_1:
  assumes 1: "(p ∧ q) ∧ r" 
  shows      "p ∧ (q ∧ r)"
proof -
  have 2: "p ∧ q" using 1 by (rule conjunct1)
  have 3: "p" using 2 by (rule conjunct1)
  have 4: "q" using 2 by (rule conjunct2)
  have 5: "r" using 1 by (rule conjunct2)
  have 6: "q ∧ r" using 4 5 by (rule conjI)
  show 7: "p ∧ (q ∧ r)" using 3 6 by (rule conjI)
qed

-- "La demostración estructurada es"
lemma ejercicio_17_2:
  assumes "(p ∧ q) ∧ r" 
  shows   "p ∧ (q ∧ r)"
proof 
  have "p ∧ q" using assms ..
  thus "p" ..
next
  show "q ∧ r"
  proof
    have "p ∧ q" using assms ..
    thus "q" ..
  next
    show "r" using assms ..
  qed
qed

-- "La demostración automática es"
lemma ejercicio_17_3:
  assumes "(p ∧ q) ∧ r" 
  shows   "p ∧ (q ∧ r)"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_18_1:
  assumes 1: "p ∧ q" 
  shows      "p ⟶ q"
proof (rule impI)
  assume 2: "p"
  show "q" using 1 by (rule conjunct2)
qed

-- "La demostración estructurada es"
lemma ejercicio_18_2:
  assumes "p ∧ q" 
  shows   "p ⟶ q"
proof 
  assume "p"
  show "q" using assms ..
qed

-- "La demostración automática es"
lemma ejercicio_18_3:
  assumes "p ∧ q" 
  shows   "p ⟶ q"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_19_1:
  assumes 1: "(p ⟶ q) ∧ (p ⟶ r)" 
  shows      "p ⟶ q ∧ r"
proof (rule impI)
  assume 2: "p"
  have 3: "p ⟶ q" using 1 by (rule conjunct1)
  have 4: "q" using 3 2 by (rule mp)
  have 5: "p ⟶ r" using 1 by (rule conjunct2)
  have 6: "r" using 5 2 by (rule mp)
  show 7: "q ∧ r" using 4 6 by (rule conjI)
qed

-- "La demostración estructurada es"
lemma ejercicio_19_2:
  assumes "(p ⟶ q) ∧ (p ⟶ r)" 
  shows   "p ⟶ q ∧ r"
proof 
  assume "p"
  show "q ∧ r"
  proof
    have "p ⟶ q" using assms ..
    thus "q" using `p` ..
  next
    have "p ⟶ r" using assms ..
    thus "r" using `p` ..
  qed
qed

-- "La demostración automática es"
lemma ejercicio_19_3:
  assumes "(p ⟶ q) ∧ (p ⟶ r)" 
  shows   "p ⟶ q ∧ r"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_20_1:
  assumes 1: "p ⟶ q ∧ r" 
  shows      "(p ⟶ q) ∧ (p ⟶ r)"
proof (rule conjI)
  show "p ⟶ q" 
  proof (rule impI)
    assume 2: "p"
    have "q ∧ r" using 1 2 by (rule mp)
    thus "q" by (rule conjunct1)
  qed
next 
  show "p ⟶ r"
  proof (rule impI)
    assume 3: "p"
    have "q ∧ r" using 1 3 by (rule mp)
    thus "r" by (rule conjunct2)
  qed
qed 

-- "La demostración estructurada es"
lemma ejercicio_20_2:
  assumes "p ⟶ q ∧ r" 
  shows   "(p ⟶ q) ∧ (p ⟶ r)"
proof 
  show "p ⟶ q" 
  proof 
    assume "p"
    have "q ∧ r" using assms `p` ..
    thus "q" ..
  qed
next 
  show "p ⟶ r"
  proof 
    assume "p"
    have "q ∧ r" using assms `p` ..
    thus "r" ..
  qed
qed 

-- "La demostración automática es"
lemma ejercicio_20_3:
  assumes "p ⟶ q ∧ r" 
  shows   "(p ⟶ q) ∧ (p ⟶ r)"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_21_1:
  assumes 1: "p ⟶ (q ⟶ r)" 
  shows      "p ∧ q ⟶ r"
proof (rule impI)
  assume 2: "p ∧ q"
  have 3: "p" using 2 by (rule conjunct1)
  have 4: "q" using 2 by (rule conjunct2)
  have 5: "q ⟶ r" using 1 3 by (rule mp)
  show 6: "r" using 5 4 by (rule mp)
qed

-- "La demostración estructurada es"
lemma ejercicio_21_2:
  assumes "p ⟶ (q ⟶ r)" 
  shows   "p ∧ q ⟶ r"
proof 
  assume "p ∧ q"
  hence "p" ..
  have "q" using `p ∧ q` ..
  have "q ⟶ r" using assms(1) `p` ..
  thus "r" using `q` ..
qed

-- "La demostración automática es"
lemma ejercicio_21_3:
  assumes "p ⟶ (q ⟶ r)" 
  shows   "p ∧ q ⟶ r"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_22_1:
  assumes 1: "p ∧ q ⟶ r" 
  shows      "p ⟶ (q ⟶ r)"
proof (rule impI)
  assume 2: "p"
  { assume 3: "q"
    have 4: "p ∧ q" using 2 3 by (rule conjI)
    have "r" using 1 4 by (rule mp) } 
  thus "q ⟶ r" by (rule impI)  
qed

-- "La demostración estructurada es"
lemma ejercicio_22_2:
  assumes "p ∧ q ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"
proof 
  assume "p"
  show "q ⟶ r"
  proof
    assume "q"
    with `p` have "p ∧ q" ..
    with  assms(1) show "r" .. 
  qed
qed

-- "La demostración automática es"
lemma ejercicio_22_3:
  assumes "p ∧ q ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_23_1:
  assumes 1: "(p ⟶ q) ⟶ r" 
  shows      "p ∧ q ⟶ r"
proof (rule impI)
  assume 2: "p ∧ q"
  have 3: "p ⟶ q"
  proof (rule impI)
    assume 4: "p"
    show "q" using 2 by (rule conjunct2)
  qed
  show "r" using 1 3 by (rule mp)
qed

-- "La demostración estructurada es"
lemma ejercicio_23_2:
  assumes "(p ⟶ q) ⟶ r" 
  shows   "p ∧ q ⟶ r"
proof 
  assume "p ∧ q"
  have "p ⟶ q"
  proof
    assume "p"
    show "q" using `p ∧ q` ..
  qed
  with assms show "r" ..
qed

-- "La demostración automática es"
lemma ejercicio_23_3:
  assumes "(p ⟶ q) ⟶ r" 
  shows   "p ∧ q ⟶ r"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_24_1:
  assumes 1: "p ∧ (q ⟶ r)" 
  shows      "(p ⟶ q) ⟶ r"
proof (rule impI)
  assume 2: "p ⟶ q"
  have 3: "p" using 1 by (rule conjunct1)
  have 4: "q" using 2 3 by (rule mp)
  have 5: "q ⟶ r" using 1 by (rule conjunct2)
  thus "r" using 4 by (rule mp) 
qed

-- "La demostración estructurada es"
lemma ejercicio_24_2:
  assumes "p ∧ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ r"
proof 
  assume "p ⟶ q"
  have "p" using assms ..
  with `p ⟶ q` have "q" ..
  have "q ⟶ r" using assms ..
  thus "r" using `q` ..
qed

-- "La demostración automática es"
lemma ejercicio_24_3:
  assumes "p ∧ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ r"
using assms
by auto

section {* Disyunciones *}

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

-- "La demostración detallada es"
lemma ejercicio_25_1:
  assumes 1: "p"
  shows      "p ∨ q"
proof -
  show "p ∨ q" using 1 by (rule disjI1)
qed

-- "La demostración estructurada es"
lemma ejercicio_25_2:
  assumes "p"
  shows   "p ∨ q"
proof -
  show "p ∨ q" using assms ..
qed

-- "La demostración estructurada es"
lemma ejercicio_25_3:
  assumes "p"
  shows   "p ∨ q"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_26_1:
  assumes 1: "q"
  shows      "p ∨ q"
proof -
  show "p ∨ q" using 1 by (rule disjI2)
qed

-- "La demostración estructurada es"
lemma ejercicio_26_2:
  assumes "q"
  shows   "p ∨ q"
proof -
  show "p ∨ q" using assms ..
qed

-- "La demostración estructurada es"
lemma ejercicio_26_3:
  assumes "q"
  shows   "p ∨ q"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_27_1:
  assumes 1: "p ∨ q"
  shows      "q ∨ p"
using 1
proof (rule disjE)
  assume "p"
  thus "q ∨ p" by (rule disjI2)
next
  assume "q"
  thus "q ∨ p" by (rule disjI1)
qed

-- "La demostración estructurada es"
lemma ejercicio_27_2:
  assumes "p ∨ q"
  shows   "q ∨ p"
using assms
proof 
  assume "p"
  thus "q ∨ p" ..
next
  assume "q"
  thus "q ∨ p" ..
qed

-- "La demostración estructurada es"
lemma ejercicio_27_3:
  assumes "p ∨ q"
  shows   "q ∨ p"
using assms
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 28. Demostrar
     q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
  ------------------------------------------------------------------ *}

-- "La demostración detallada es"
lemma ejercicio_28_1:
  assumes 1: "q ⟶ r" 
  shows      "p ∨ q ⟶ p ∨ r"
proof (rule impI)
  assume "p ∨ q"
  thus "p ∨ r"
  proof (rule disjE)
    assume "p"
    thus "p ∨ r" by (rule disjI1)
  next
    assume "q"
    have "r" using assms `q` by (rule mp)
    thus "p ∨ r" by (rule disjI2)
  qed
qed

-- "La demostración estructurada es"
lemma ejercicio_28_2:
  assumes "q ⟶ r" 
  shows   "p ∨ q ⟶ p ∨ r"
proof 
  assume "p ∨ q"
  thus "p ∨ r"
  proof 
    assume "p"
    thus "p ∨ r" ..
  next
    assume "q"
    have "r" using assms `q` ..
    thus "p ∨ r" ..
  qed
qed

-- "La demostración automática es"
lemma ejercicio_28_3:
  assumes "q ⟶ r" 
  shows   "p ∨ q ⟶ p ∨ r"
using assms
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 29. Demostrar
     p ∨ p ⊢ p
  ------------------------------------------------------------------ *}

-- "La demostración detallada es"
lemma ejercicio_29_1:
  assumes 1: "p ∨ p"
  shows      "p"
using 1
proof (rule disjE)
  assume "p"
  thus "p" by this
next
  assume "p"
  thus "p" by this
qed

-- "La demostración estructurada es"
lemma ejercicio_29_2:
  assumes "p ∨ p"
  shows   "p"
using assms
proof 
  assume "p"
  thus "p" .
next
  assume "p"
  thus "p" .
qed

-- "La demostración estructurada es"
lemma ejercicio_29_3:
  assumes "p ∨ p"
  shows   "p"
using assms
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 30. Demostrar
     p ⊢ p ∨ p
  ------------------------------------------------------------------ *}

-- "La demostración detallada es"
lemma ejercicio_30_1:
  assumes 1: "p" 
  shows      "p ∨ p"
proof -
  show "p ∨ p" using 1 by (rule disjI1)
qed

-- "La demostración estructurada es"
lemma ejercicio_30_2:
  assumes "p" 
  shows   "p ∨ p"
proof -
  show "p ∨ p" using assms ..
qed

-- "La demostración estructurada es"
lemma ejercicio_30_3:
  assumes "p" 
  shows   "p ∨ p"
using assms
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 31. Demostrar
     p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r
  ------------------------------------------------------------------ *}

-- "La demostración detallada es"
lemma ejercicio_31_1:
  assumes 1: "p ∨ (q ∨ r)" 
  shows      "(p ∨ q) ∨ r"
using 1
proof (rule disjE)
  assume "p"
  hence "p ∨ q" by (rule disjI1)
  thus "(p ∨ q) ∨ r" by (rule disjI1)
next
  assume "q ∨ r"
  thus "(p ∨ q) ∨ r"
  proof (rule disjE)
    assume "q"
    hence "p ∨ q" by (rule disjI2)
    thus "(p ∨ q) ∨ r" by (rule disjI1)
  next
    assume "r"
    thus "(p ∨ q) ∨ r" by (rule disjI2)
  qed
qed

-- "La demostración estructurada es"
lemma ejercicio_31_2:
  assumes "p ∨ (q ∨ r)" 
  shows   "(p ∨ q) ∨ r"
using assms
proof 
  assume "p"
  hence "p ∨ q" ..
  thus "(p ∨ q) ∨ r" ..
next
  assume "q ∨ r"
  thus "(p ∨ q) ∨ r"
  proof 
    assume "q"
    hence "p ∨ q" ..
    thus "(p ∨ q) ∨ r" ..
  next
    assume "r"
    thus "(p ∨ q) ∨ r" ..
  qed
qed

-- "La demostración estructurada es"
lemma ejercicio_31_3:
  assumes "p ∨ (q ∨ r)" 
  shows   "(p ∨ q) ∨ r"
using assms
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 32. Demostrar
     (p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
  ------------------------------------------------------------------ *}

-- "La demostración detallada es"
lemma ejercicio_32_1:
  assumes 1: "(p ∨ q) ∨ r" 
  shows      "p ∨ (q ∨ r)"
using 1
proof (rule disjE)
  assume "p ∨ q"
  thus "p ∨ (q ∨ r)"
  proof (rule disjE)
    assume "p"
    thus "p ∨ (q ∨ r)" by (rule disjI1)
  next
    assume "q"
    hence "q ∨ r" by (rule disjI1)
    thus "p ∨ (q ∨ r)" by (rule disjI2)
  qed
next
  assume "r"
  hence "q ∨ r" by (rule disjI2)
  thus "p ∨ (q ∨ r)" by (rule disjI2)
qed

-- "La demostración estructurada es"
lemma ejercicio_32_2:
  assumes "(p ∨ q) ∨ r" 
  shows   "p ∨ (q ∨ r)"
using assms
proof 
  assume "p ∨ q"
  thus "p ∨ (q ∨ r)"
  proof 
    assume "p"
    thus "p ∨ (q ∨ r)" ..
  next
    assume "q"
    hence "q ∨ r" ..
    thus "p ∨ (q ∨ r)" ..
  qed
next
  assume "r"
  hence "q ∨ r" .. 
  thus "p ∨ (q ∨ r)" ..
qed

-- "La demostración estructurada es"
lemma ejercicio_32_3:
  assumes "(p ∨ q) ∨ r" 
  shows   "p ∨ (q ∨ r)"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_33_1:
  assumes 1: "p ∧ (q ∨ r)" 
  shows      "(p ∧ q) ∨ (p ∧ r)"
proof -
  have 2: "p" using 1 by (rule conjunct1)
  have 3: "q ∨ r" using 1 by (rule conjunct2)
  thus "(p ∧ q) ∨ (p ∧ r)"
  proof (rule disjE)
    assume 4: "q"
    have "p ∧ q" using 2 4 by (rule conjI)
    thus "(p ∧ q) ∨ (p ∧ r)" by (rule disjI1)
  next
    assume 5: "r"
    have "q ∨ r" using 1 by (rule conjunct2)
    thus "(p ∧ q) ∨ (p ∧ r)"
    proof (rule disjE)
      assume "q"
      have "p ∧ q" using `p` `q` by (rule conjI) 
      thus "(p ∧ q) ∨ (p ∧ r)" by (rule disjI1)
    next
      assume "r"
      have "p ∧ r" using `p` `r` by (rule conjI) 
      thus "(p ∧ q) ∨ (p ∧ r)" by (rule disjI2)
    qed
  qed
qed

-- "La demostración estructurada es"
lemma ejercicio_33_2:
  assumes "p ∧ (q ∨ r)" 
  shows   "(p ∧ q) ∨ (p ∧ r)"
proof -
  have "p" using assms ..
  have "q ∨ r" using assms .. 
  thus "(p ∧ q) ∨ (p ∧ r)"
  proof 
    assume "q"
    with `p` have "p ∧ q" ..
    thus "(p ∧ q) ∨ (p ∧ r)" ..
  next
    assume "r"
    hence "q ∨ r" ..
    thus "(p ∧ q) ∨ (p ∧ r)"
    proof 
      assume "q"
      with `p` have "p ∧ q" ..
      thus "(p ∧ q) ∨ (p ∧ r)" ..
    next
      assume "r"
      with `p` have "p ∧ r" ..
      thus "(p ∧ q) ∨ (p ∧ r)" ..
    qed
  qed
qed

-- "La demostración automática es"
lemma ejercicio_33_3:
  assumes "p ∧ (q ∨ r)" 
  shows   "(p ∧ q) ∨ (p ∧ r)"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_34_1:
  assumes "(p ∧ q) ∨ (p ∧ r)" 
  shows   "p ∧ (q ∨ r)"
using assms
proof (rule disjE)
  assume 1: "p ∧ q"
  show "p ∧ (q ∨ r)"
  proof (rule conjI)
    show "p" using 1 by (rule conjunct1)
  next
    have "q" using 1 by (rule conjunct2)
    thus "q ∨ r" by (rule disjI1)
  qed
next
  assume 2: "p ∧ r"
  hence 3: "p" by (rule conjunct1)
  have "r" using 2 by (rule conjunct2)
  hence 4: "q ∨ r" by (rule disjI2)
  show "p ∧ (q ∨ r)" using 3 4 by (rule conjI) 
qed

-- "La demostración estructurada es"
lemma ejercicio_34_2:
  assumes "(p ∧ q) ∨ (p ∧ r)" 
  shows   "p ∧ (q ∨ r)"
using assms
proof 
  assume "p ∧ q"
  show "p ∧ (q ∨ r)"
  proof 
    show "p" using `p ∧ q` ..
  next
    have "q" using `p ∧ q` ..
    thus "q ∨ r" ..
  qed
next
  assume "p ∧ r"
  hence "p" ..
  have "r" using `p ∧ r` ..
  hence "q ∨ r" .. 
  with `p` show "p ∧ (q ∨ r)" ..
qed

-- "La demostración estructurada es"
lemma ejercicio_34_3:
  assumes "(p ∧ q) ∨ (p ∧ r)" 
  shows   "p ∧ (q ∨ r)"
using assms
by auto

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

-- "La demostración estructurada es"
lemma ejercicio_35_1:
  assumes "p ∨ (q ∧ r)" 
  shows   "(p ∨ q) ∧ (p ∨ r)"
using assms
proof
  assume "p"
  show "(p ∨ q) ∧ (p ∨ r)"
  proof
    show "p ∨ q" using `p` ..
  next
    show "p ∨ r" using `p` ..
  qed
next
  assume "q ∧ r"
  show "(p ∨ q) ∧ (p ∨ r)"
  proof
    have "q" using `q ∧ r` ..
    thus "p ∨ q" ..
  next
    have "r" using `q ∧ r` ..
    thus "p ∨ r" ..
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_35_2:
  assumes "p ∨ (q ∧ r)" 
  shows   "(p ∨ q) ∧ (p ∨ r)"
using assms
proof (rule disjE)
  assume "p"
  show "(p ∨ q) ∧ (p ∨ r)"
  proof (rule conjI)
    show "p ∨ q" using `p` by (rule disjI1)
  next
    show "p ∨ r" using `p` by (rule disjI1)
  qed
next
  assume "q ∧ r"
  show "(p ∨ q) ∧ (p ∨ r)"
  proof (rule conjI)
    have "q" using `q ∧ r` ..
    thus "p ∨ q" by (rule disjI2)
  next
    have "r" using `q ∧ r` by (rule conjunct2)
    thus "p ∨ r" by (rule disjI2)
  qed
qed

-- "La demostración automática es"
lemma ejercicio_35_3:
  assumes "p ∨ (q ∧ r)" 
  shows   "(p ∨ q) ∧ (p ∨ r)"
using assms
by auto

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

-- "La demostración estructurada es"
lemma ejercicio_36_1:
  assumes "(p ∨ q) ∧ (p ∨ r)"
  shows   "p ∨ (q ∧ r)"
proof -
  have "p ∨ q" using assms ..
  thus "p ∨ (q ∧ r)"
  proof 
    assume "p"
    thus "p ∨ (q ∧ r)" ..
  next
    assume "q"
    have "p ∨ r" using assms ..
    thus "p ∨ (q ∧ r)"
    proof
      assume "p"
      thus "p ∨ (q ∧ r)" ..
    next
      assume "r"
      with `q` have "q ∧ r" ..
      thus "p ∨ (q ∧ r)" ..
    qed 
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_36_2:
  assumes "(p ∨ q) ∧ (p ∨ r)"
  shows   "p ∨ (q ∧ r)"
proof -
  have "p ∨ q" using assms by (rule conjunct1)
  thus "p ∨ (q ∧ r)"
  proof (rule disjE)
    assume "p"
    thus "p ∨ (q ∧ r)" by (rule disjI1)
  next
    assume "q"
    have "p ∨ r" using assms by (rule conjunct2)
    thus "p ∨ (q ∧ r)"
    proof (rule disjE)
      assume "p"
      thus "p ∨ (q ∧ r)" by (rule disjI1)
    next
      assume "r"
      have "q ∧ r" using `q` `r` by (rule conjI)
      thus "p ∨ (q ∧ r)" by (rule disjI2)
    qed 
  qed
qed

-- "La demostración automática es"
lemma ejercicio_36_3:
  assumes "(p ∨ q) ∧ (p ∨ r)"
  shows   "p ∨ (q ∧ r)"
using assms
by auto

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

-- "La demostración estructurada es"
lemma ejercicio_37_1:
  assumes "(p ⟶ r) ∧ (q ⟶ r)" 
  shows   "p ∨ q ⟶ r"
proof
  assume "p ∨ q"
  thus "r"
  proof 
    assume "p"
    have "p ⟶ r" using assms ..
    thus "r" using `p` ..
  next
    assume "q"
    have "q ⟶ r" using assms ..
    thus "r" using `q` ..
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_37_2:
  assumes "(p ⟶ r) ∧ (q ⟶ r)" 
  shows   "p ∨ q ⟶ r"
proof (rule impI)
  assume "p ∨ q"
  thus "r"
  proof (rule disjE)
    assume "p"
    have "p ⟶ r" using assms by (rule conjunct1)
    thus "r" using `p` by (rule mp)
  next
    assume "q"
    have "q ⟶ r" using assms by (rule conjunct2)
    thus "r" using `q` by (rule mp)
  qed
qed

-- "La demostración automática es"
lemma ejercicio_37_3:
  assumes "(p ⟶ r) ∧ (q ⟶ r)" 
  shows   "p ∨ q ⟶ r"
using assms
by auto

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

-- "La demostración estructurada es"
lemma ejercicio_38_1:
  assumes "p ∨ q ⟶ r" 
  shows   "(p ⟶ r) ∧ (q ⟶ r)"
proof
  show "p ⟶ r"
  proof
    assume "p"
    hence "p ∨ q" ..
    with assms show "r" ..
  qed
next
  show "q ⟶ r"
  proof
    assume "q"
    hence "p ∨ q" ..
    with assms show "r" ..
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_38_2:
  assumes "p ∨ q ⟶ r" 
  shows   "(p ⟶ r) ∧ (q ⟶ r)"
proof (rule conjI)
  show "p ⟶ r"
  proof (rule impI)
    assume "p"
    hence "p ∨ q" by (rule disjI1)
    show "r" using assms `p ∨ q` by (rule mp)
  qed
next
  show "q ⟶ r"
  proof (rule impI)
    assume "q"
    hence "p ∨ q" by (rule disjI2)
    show "r" using assms `p ∨ q` by (rule mp)
  qed
qed

-- "La demostración automática es"
lemma ejercicio_38_3:
  assumes "p ∨ q ⟶ r" 
  shows   "(p ⟶ r) ∧ (q ⟶ r)"
using assms
by auto

section {* Negación *}

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

-- "La demostración detallada es"
lemma ejercicio_39_1:
  assumes "p"
  shows   "¬¬p"
proof -
  show "¬¬p" using assms by (rule notnotI)
qed

-- "La demostración automática es"
lemma ejercicio_39_2:
  assumes "p"
  shows   "¬¬p"
using assms
by auto

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

-- "La demostración estructurada es"
lemma ejercicio_40_1:
  assumes "¬p" 
  shows   "p ⟶ q"
proof
  assume "p"
  with assms(1) show "q" ..
qed

-- "La demostración detallada es"
lemma ejercicio_40_2:
  assumes "¬p" 
  shows   "p ⟶ q"
proof (rule impI)
  assume "p"
  show "q" using assms(1) `p` by (rule notE)
qed

-- "La demostración automática es"
lemma ejercicio_40_3:
  assumes "¬p" 
  shows   "p ⟶ q"
using assms
by auto

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

-- "La demostración estructurada es"
lemma ejercicio_41_1:
  assumes "p ⟶ q"
  shows   "¬q ⟶ ¬p"
proof
  assume "¬q"
  with assms(1) show "¬p" by (rule mt)
qed

-- "La demostración detallada es"
lemma ejercicio_41_2:
  assumes "p ⟶ q"
  shows   "¬q ⟶ ¬p"
proof (rule impI)
  assume "¬q"
  show "¬p" using assms(1) `¬q` by (rule mt)
qed

-- "La demostración automática es"
lemma ejercicio_41_3:
  assumes "p ⟶ q"
  shows   "¬q ⟶ ¬p"
using assms
by auto

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

-- "La demostración estructurada es"
lemma ejercicio_42_1:
  assumes "p ∨ q"
          "¬q" 
  shows   "p"
using assms(1)
proof
  assume "p"
  thus "p" .
next
  assume "q"
  with assms(2) show "p" ..
qed

-- "La demostración detallada es"
lemma ejercicio_42_2:
  assumes "p ∨ q"
          "¬q" 
  shows   "p"
using assms(1)
proof (rule disjE)
  assume "p"
  thus "p" by this
next
  assume "q"
  show "p" using assms(2) `q` by (rule notE)
qed

-- "La demostración automática es"
lemma ejercicio_42_3:
  assumes "p ∨ q"
          "¬q" 
  shows   "p"
using assms
by auto

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

-- "La demostración estructurada es"
lemma ejercicio_43_1:
  assumes "p ∨ q"
          "¬p" 
  shows   "q"
using assms(1)
proof
  assume "p"
  with assms(2) show "q" ..
next
  assume "q"
  thus "q" .
qed

-- "La demostración detallada es"
lemma ejercicio_43_2:
  assumes "p ∨ q"
          "¬p" 
  shows   "q"
using assms(1)
proof (rule disjE)
  assume "p"
  show "q" using assms(2) `p` by (rule notE)
next
  assume "q"
  thus "q" by this
qed

-- "La demostración automática es"
lemma ejercicio_43_3:
  assumes "p ∨ q"
          "¬p" 
  shows   "q"
using assms
by auto

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

-- "La demostración estructurada es"
lemma ejercicio_44_1:
  assumes "p ∨ q" 
  shows   "¬(¬p ∧ ¬q)"
proof
  assume "¬p ∧ ¬q"
  note `p ∨ q`
  thus "False" 
  proof
    assume "p"
    have "¬p" using `¬p ∧ ¬q` .. 
    thus "False" using `p` ..
  next 
    assume "q"
    have "¬q" using `¬p ∧ ¬q` .. 
    thus "False" using `q` ..
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_44_2:
  assumes "p ∨ q" 
  shows   "¬(¬p ∧ ¬q)"
proof (rule notI)
  assume "¬p ∧ ¬q"
  note `p ∨ q`
  thus "False" 
  proof
    assume "p"
    have "¬p" using `¬p ∧ ¬q` by (rule conjunct1) 
    thus "False" using `p` by (rule notE)
  next 
    assume "q"
    have "¬q" using `¬p ∧ ¬q` by (rule conjunct2)
    thus "False" using `q` by (rule notE)
  qed
qed

-- "La demostración automática es"
lemma ejercicio_44_3:
  assumes "p ∨ q" 
  shows   "¬(¬p ∧ ¬q)"
using assms
by auto

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

-- "La demostración estructurada es"
lemma ejercicio_45_1:
  assumes "p ∧ q" 
  shows   "¬(¬p ∨ ¬q)"
proof
  assume "¬p ∨ ¬q"
  thus "False"
  proof
    assume "¬p"
    have "p" using assms ..
    with `¬p` show "False" ..
  next
    assume "¬q"
    have "q" using assms ..
    with `¬q` show "False" ..
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_45_2:
  assumes "p ∧ q" 
  shows   "¬(¬p ∨ ¬q)"
proof (rule notI)
  assume "¬p ∨ ¬q"
  thus "False"
  proof
    assume "¬p"
    have "p" using assms by (rule conjunct1)
    show "False" using `¬p` `p` by (rule notE)
  next
    assume "¬q"
    have "q" using assms by (rule conjunct2)
    show "False" using `¬q` `q` by (rule notE)
  qed
qed

-- "La demostración automática es"
lemma ejercicio_45_3:
  assumes "p ∧ q" 
  shows   "¬(¬p ∨ ¬q)"
using assms
by auto

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

-- "La demostración estructurada es"
lemma ejercicio_46_1:
  assumes "¬(p ∨ q)" 
  shows   "¬p ∧ ¬q"
proof 
  show "¬p"
  proof
    assume "p"
    hence "p ∨ q" ..
    with assms show "False" ..
  qed
next
  show "¬q"
  proof
    assume "q"
    hence "p ∨ q" ..
    with assms show "False" ..
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_46_2:
  assumes "¬(p ∨ q)" 
  shows   "¬p ∧ ¬q"
proof (rule conjI)
  show "¬p"
  proof (rule notI)
    assume "p"
    hence "p ∨ q" by (rule disjI1)
    show "False" using assms `p ∨ q` by (rule notE)
  qed
next
  show "¬q"
  proof (rule notI)
    assume "q"
    hence "p ∨ q" by (rule disjI2)
    show "False" using assms `p ∨ q` by (rule notE)
  qed
qed

-- "La demostración automática es"
lemma ejercicio_46_3:
  assumes "¬(p ∨ q)" 
  shows   "¬p ∧ ¬q"
using assms
by auto

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

-- "La demostración estructurada es"
lemma ejercicio_47_1:
  assumes "¬p ∧ ¬q" 
  shows   "¬(p ∨ q)"
proof
  assume "p ∨ q"
  thus False
  proof
    assume "p"
    have "¬p" using assms ..
    thus False using `p` ..
  next
    assume "q"
    have "¬q" using assms ..
    thus False using `q` ..
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_47_2:
  assumes "¬p ∧ ¬q" 
  shows   "¬(p ∨ q)"
proof (rule notI)
  assume "p ∨ q"
  thus False
  proof (rule disjE)
    assume "p"
    have "¬p" using assms by (rule conjunct1)
    thus False using `p` by (rule notE)
  next
    assume "q"
    have "¬q" using assms by (rule conjunct2)
    thus False using `q` by (rule notE)
  qed
qed

-- "La demostración automática es"
lemma ejercicio_47_3:
  assumes "¬p ∧ ¬q" 
  shows   "¬(p ∨ q)"
using assms
by auto

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

-- "La demostración estructurada es"
lemma ejercicio_48_1:
  assumes "¬p ∨ ¬q"
  shows   "¬(p ∧ q)"
proof
  assume "p ∧ q"
  note `¬p ∨ ¬ q`
  thus False
  proof
    assume "¬p"
    have "p" using `p ∧ q` ..
    with `¬p` show False ..
  next
    assume "¬q"
    have "q" using `p ∧ q` ..
    with `¬q` show False ..
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_48_2:
  assumes "¬p ∨ ¬q"
  shows   "¬(p ∧ q)"
proof (rule notI)
  assume "p ∧ q"
  note `¬p ∨ ¬ q`
  thus False
  proof (rule disjE)
    assume "¬p"
    have "p" using `p ∧ q` by (rule conjunct1)
    show False using `¬p` `p` by (rule notE)
  next
    assume "¬q"
    have "q" using `p ∧ q` by (rule conjunct2)
    show False using `¬q` `q` by (rule notE)
  qed
qed

-- "La demostración automática es"
lemma ejercicio_48_3:
  assumes "¬p ∨ ¬q"
  shows   "¬(p ∧ q)"
using assms
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 49. Demostrar
     ⊢ ¬(p ∧ ¬p)
  ------------------------------------------------------------------ *}

-- "La demostración estructurada es"
lemma ejercicio_49_1:
  "¬(p ∧ ¬p)"
proof
  assume "p ∧ ¬p"
  hence "p" ..
  have "¬p" using `p ∧ ¬p` ..
  thus False using `p` .. 
qed

-- "La demostración detallada es"
lemma ejercicio_49_2:
  "¬(p ∧ ¬p)"
proof (rule notI)
  assume "p ∧ ¬p"
  hence "p" by (rule conjunct1)
  have "¬p" using `p ∧ ¬p` by (rule conjunct2)
  thus False using `p` by (rule notE)
qed

-- "La demostración automática es"
lemma ejercicio_49_3:
  "¬(p ∧ ¬p)"
by auto

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

-- "La demostración estructurada es"
lemma ejercicio_50_1:
  assumes "p ∧ ¬p" 
  shows   "q"
proof -
  have "p" using assms ..
  have "¬p" using assms ..
  thus "q" using `p` ..
qed

-- "La demostración detallada es"
lemma ejercicio_50_2:
  assumes "p ∧ ¬p" 
  shows   "q"
proof -
  have "p" using assms by (rule conjunct1)
  have "¬p" using assms by (rule conjunct2)
  thus "q" using `p` by (rule notE)
qed

-- "La demostración automática es"
lemma ejercicio_50_3:
  assumes "p ∧ ¬p" 
  shows   "q"
using assms
by auto

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

-- "La demostración detallada es"
lemma ejercicio_51_1:
  assumes "¬¬p"
  shows   "p"
using assms
by (rule notnotD)

-- "La demostración automática es"
lemma ejercicio_51_2:
  assumes "¬¬p"
  shows   "p"
using assms
by auto

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

-- "La demostración estructurada es"
lemma ejercicio_52_1:
  "p ∨ ¬p"
proof -
  have "¬¬p ∨ ¬p" ..
  thus "p ∨ ¬p" by simp
qed

-- "La demostración detallada es"
lemma ejercicio_52_2:
  "p ∨ ¬p"
proof -
  have "¬¬p ∨ ¬p" by (rule excluded_middle)
  thus "p ∨ ¬p" by simp
qed

-- "La demostración automática es"
lemma ejercicio_52_3:
  "p ∨ ¬p"
by auto

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

-- "La demostración estructurada es"
lemma ejercicio_53_1:
  "((p ⟶ q) ⟶ p) ⟶ p"
proof
  assume "(p ⟶ q) ⟶ p"
  show "p"
  proof (rule ccontr)
    assume "¬p"
    have "¬(p ⟶ q)" using `(p ⟶ q) ⟶ p` `¬p` by (rule mt)
    have "p ⟶ q"
    proof
      assume "p"
      with `¬p` show "q" ..
    qed
    show False using `¬(p ⟶ q)` `p ⟶ q` .. 
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_53_2:
  "((p ⟶ q) ⟶ p) ⟶ p"
proof (rule impI)
  assume "(p ⟶ q) ⟶ p"
  show "p"
  proof (rule ccontr)
    assume "¬p"
    have "¬(p ⟶ q)" using `(p ⟶ q) ⟶ p` `¬p` by (rule mt)
    have "p ⟶ q"
    proof (rule impI)
      assume "p"
      show "q" using `¬p` `p` by (rule notE)
    qed
    show False using `¬(p ⟶ q)` `p ⟶ q` by (rule notE) 
  qed
qed

-- "La demostración automática es"
lemma ejercicio_53_3:
  "((p ⟶ q) ⟶ p) ⟶ p"
by auto

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

-- "La demostración estructurada es"
lemma ejercicio_54_1:
  assumes "¬q ⟶ ¬p"
  shows   "p ⟶ q"
proof
  assume "p"
  show "q"
  proof (rule ccontr)
    assume "¬q"
    with assms have "¬p" ..
    thus False using `p` ..
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_54_2:
  assumes "¬q ⟶ ¬p"
  shows   "p ⟶ q"
proof (rule impI)
  assume "p"
  show "q"
  proof (rule ccontr)
    assume "¬q"
    have "¬p" using assms `¬q` by (rule mp)
    thus False using `p` by (rule notE)
  qed
qed

-- "La demostración automática es"
lemma ejercicio_54_3:
  assumes "¬q ⟶ ¬p"
  shows   "p ⟶ q"
using assms
by auto

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

-- "La demostración estructurada es"
lemma ejercicio_55_1:
  assumes "¬(¬p ∧ ¬q)"
  shows   "p ∨ q"
proof -
  have "¬p ∨ p" ..
  thus "p ∨ q"
  proof
    assume "¬p"
    have "¬q ∨ q" ..
    thus "p ∨ q"
    proof
      assume "¬q"
      with `¬p` have "¬p ∧ ¬q" ..
      with assms show "p ∨ q" ..
    next
      assume "q"
      thus "p ∨ q" ..
    qed
  next
    assume "p"
    thus "p ∨ q" ..
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_55_2:
  assumes "¬(¬p ∧ ¬q)"
  shows   "p ∨ q"
proof -
  have "¬p ∨ p" by (rule excluded_middle)
  thus "p ∨ q"
  proof
    assume "¬p"
    have "¬q ∨ q" by (rule excluded_middle)
    thus "p ∨ q"
    proof
      assume "¬q"
      have "¬p ∧ ¬q" using `¬p` `¬q` by (rule conjI)
      show "p ∨ q" using assms `¬p ∧ ¬q` by (rule notE)
    next
      assume "q"
      thus "p ∨ q" by (rule disjI2)
    qed
  next
    assume "p"
    thus "p ∨ q" by (rule disjI1)
  qed
qed

-- "La demostración automática es"
lemma ejercicio_55_3:
  assumes "¬(¬p ∧ ¬q)"
  shows   "p ∨ q"
using assms
by auto

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

-- "La demostración estructurada es"
lemma ejercicio_56_1:
  assumes "¬(¬p ∨ ¬q)" 
  shows   "p ∧ q"
proof
  show "p"
  proof (rule ccontr)
    assume "¬p"
    hence "¬p ∨ ¬q" ..
    with assms show False ..
  qed
next
  show "q"
  proof (rule ccontr)
    assume "¬q"
    hence "¬p ∨ ¬q" ..
    with assms show False ..
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_56_2:
  assumes "¬(¬p ∨ ¬q)" 
  shows   "p ∧ q"
proof (rule conjI)
  show "p"
  proof (rule ccontr)
    assume "¬p"
    hence "¬p ∨ ¬q" by (rule disjI1)
    show False using assms `¬p ∨ ¬q` by (rule notE)
  qed
next
  show "q"
  proof (rule ccontr)
    assume "¬q"
    hence "¬p ∨ ¬q" by (rule disjI2)
    show False using assms `¬p ∨ ¬q` by (rule notE)
  qed
qed

-- "La demostración automática es"
lemma ejercicio_56_3:
  assumes "¬(¬p ∨ ¬q)" 
  shows   "p ∧ q"
using assms
by auto

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

-- "La demostración estructurada es"
lemma ejercicio_57_1:
  assumes "¬(p ∧ q)"
  shows   "¬p ∨ ¬q"
proof -
  have "¬p ∨ p" ..
  thus "¬p ∨ ¬q"
  proof
    assume "¬p"
    thus "¬p ∨ ¬q" ..
  next
    assume "p"
    have "¬q ∨ q" ..
    thus "¬p ∨ ¬q" 
    proof
      assume "¬q"
      thus "¬p ∨ ¬q" ..
    next
      assume "q"
      with `p` have "p ∧ q" ..
      with assms show "¬p ∨ ¬q" ..
    qed
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_57_2:
  assumes "¬(p ∧ q)"
  shows   "¬p ∨ ¬q"
proof -
  have "¬p ∨ p" by (rule excluded_middle)
  thus "¬p ∨ ¬q"
  proof (rule disjE)
    assume "¬p"
    thus "¬p ∨ ¬q" by (rule disjI1)
  next
    assume "p"
    have "¬q ∨ q" by (rule excluded_middle)
    thus "¬p ∨ ¬q" 
    proof
      assume "¬q"
      thus "¬p ∨ ¬q" by (rule disjI2)
    next
      assume "q"
      have "p ∧ q" using `p` `q` by (rule conjI)
      show "¬p ∨ ¬q" using assms `p ∧ q` by (rule notE) 
    qed
  qed
qed

-- "La demostración automática es"
lemma ejercicio_57_3:
  assumes "¬(p ∧ q)"
  shows   "¬p ∨ ¬q"
using assms
by auto

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

-- "La demostración estructurada es"
lemma ejercicio_58_1:
  "(p ⟶ q) ∨ (q ⟶ p)"
proof -
  have "¬p ∨ p" ..
  thus "(p ⟶ q) ∨ (q ⟶ p)"
  proof
    assume "¬p"
    have "p ⟶ q"
    proof
      assume "p"
      with `¬p` show "q" ..
    qed
    thus "(p ⟶ q) ∨ (q ⟶ p)" ..
  next
    assume "p"
    have "q ⟶ p"
    proof
      assume "q"
      show "p" using `p` .
    qed
    thus "(p ⟶ q) ∨ (q ⟶ p)" ..
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_58_2:
  "(p ⟶ q) ∨ (q ⟶ p)"
proof -
  have "¬p ∨ p" by (rule excluded_middle)
  thus "(p ⟶ q) ∨ (q ⟶ p)"
  proof
    assume "¬p"
    have "p ⟶ q"
    proof (rule impI)
      assume "p"
      show "q" using `¬p` `p` by (rule notE)
    qed
    thus "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI1)
  next
    assume "p"
    have "q ⟶ p"
    proof
      assume "q"
      show "p" using `p` by this
    qed
    thus "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI2)
  qed
qed

-- "La demostración automática es"
lemma ejercicio_58_3:
  "(p ⟶ q) ∨ (q ⟶ p)"
by auto

end
</source>