Relación 4

chapter {* R4: Deducción natural proposicional *}

theory R4
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
  ------------------------------------------------------------------ *}

lemma ejercicio_1: josrodjim2 carmarria inmbenber marmedmar3
  assumes 1: "p ⟶ q" and
          2: "p"
  shows "q"

proof -
  show 1: "q" using 1 2  by (rule mp)
qed


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

lemma ejercicio_2: josrodjim2 carmarria inmbenber marmedmar3
  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


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

lemma ejercicio_3: josrodjim2 carmarria inmbenber marmedmar3
  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


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

lemma ejercicio_4: josrodjim2
  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)}
  hence 6: "p ⟶ r"  using 3 5  by (rule impI)
  show "p⟶r" using 6 by this

oops

lemma ejercicio_4: carmarria
  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
lemma ejercicio_4: inmbenber
  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

lemma ejercicio_4:marmedmar3
  assumes "p ⟶ q"
          "q ⟶ r" 
        shows "p ⟶ r"
proof 
  assume "p" 
   with assms(1) have "q" by (rule mp)
  with assms(2) show "r" by (rule mp)
qed 

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

lemma ejercicio_5: josrodjim2 (NO DA ERROR, PERO SI ALERTA)
  assumes "p ⟶ (q ⟶ r)" 
  shows   "q ⟶ (p ⟶ r)"

proof -

  { assume 2: "q"
    {assume 3: "p"
      have 4: "q ⟶r" using 1 3 by (rule mp)
      have 5: "r" using 4 2 by (rule mp)}
    hence 6: "p⟶r" using 3 5 by (rule impI)}
    hence 7: "q ⟶ (p ⟶ r)" using 2 6 by (rule impI)
    show "q ⟶ (p ⟶ r)" using 7 by this
 
oops

lemma ejercicio_5: carmarria 
  assumes 1: "p ⟶ (q ⟶ r)" 
  shows   "q ⟶ (p ⟶ r)"

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

lemma ejercicio_5: inmbenber
  assumes 1: "p ⟶ (q ⟶ r)" 
  shows   "q ⟶ (p ⟶ r)"

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

lemma ejercicio_5: marmedmar3
  assumes "p ⟶ (q ⟶ r)" 
  shows   "q ⟶ (p ⟶ r)"
proof 
  assume "q"
  show "(p ⟶ r)"
  proof 
    assume "p" 
    with assms(1) have "(q ⟶ r)" by (rule mp)
    thus "r" using  `q` by (rule mp) 
  qed 
qed

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

lemma ejercicio_6:josrodjim2
  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 by (rule mp)
      have 5: "q" using 2 3 by (rule mp)
      have 6: "r" using 4 5 by (rule mp)}
      hence 7: "p⟶r" using 3 6 by (rule impI)}
      hence  8: "(p ⟶ q) ⟶ (p ⟶ r)" using 2 7 by (rule impI)
      show  "(p ⟶ q) ⟶ (p ⟶ r)" using 8 by this
oops

lemma ejercicio_6: carmarria, inmbenber
  assumes 1: "p ⟶ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ (p ⟶ r)"
proof -
  {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)
  }
  thus "(p ⟶ q) ⟶ (p ⟶ r)" by (rule impI)
      qed

lemma ejercicio_6:marmedmar3
  assumes 1:  "p ⟶ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ (p ⟶ r)"
proof 
  assume 2: "(p ⟶ q)" 
  show "(p ⟶ r)" 
  proof 
    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

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

lemma ejercicio_7: (NO SE QUE ESTA MAL)
  assumes "p"  
  shows   "q ⟶ p"

proof -

  { assume 2:  "q"
    have 3: "p" using 1
 }
  hence  4: "q⟶p" using  2 3   by (rule impI)

show "q⟶p" using 4  by this
    
oops

lemma ejercicio_7: carmarria, inmbenber
  assumes 1: "p"  
  shows   "q ⟶ p"
proof -
  {assume 2: "q"
    have 3: "p" using 1 by this}
  thus "q ⟶ p" by (rule impI)
      qed
     
lemma ejercicio_7:marmedmar3
  assumes "p"  
  shows   "q ⟶ p"
proof 
  assume "q" 
  show "p" using assms(1) by this
qed 
  

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

lemma ejercicio_8: carmarria
  "p ⟶ (q ⟶ p)"

proof -
  {assume 1: p
    {assume 2: q
      have 3: p using 1 by this
    }
    hence 4: "q ⟶ p" by (rule impI)
  }
  thus "p ⟶ (q ⟶ p)" by (rule impI)
      qed

lemma ejercicio_8: marmedmar3
  "p ⟶ (q ⟶ p)"
proof
  assume 1:  "p"
  show "(q ⟶ p)"
  proof 
    assume 2:  "q" 
    show "p" using 1 by this 
  qed
qed
text {* --------------------------------------------------------------- 
  Ejercicio 9. Demostrar
     p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)
  ------------------------------------------------------------------ *}

lemma ejercicio_9: carmarria
  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 7: "(q ⟶ r) ⟶ (p ⟶ r)" by (rule impI)
      qed

lemma ejercicio_9: marmedmar3
  assumes "p ⟶ q" 
  shows   "(q ⟶ r) ⟶ (p ⟶ r)"
proof 
  assume "(q ⟶ r)" 
  show "(p ⟶ r)"
  proof 
    assume "p" 
    with `(p ⟶ q)` have "q" by (rule mp)
    with `(q ⟶ r)` show "r" by (rule mp)
  qed
qed
text {* --------------------------------------------------------------- 
  Ejercicio 10. Demostrar
     p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
  ------------------------------------------------------------------ *}

lemma ejercicio_10: carmarria
  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  "r ⟶ (q ⟶ (p ⟶ s))" by (rule impI)
      qed

lemma ejercicio_10: marmedmar3
  assumes 1: "p ⟶ (q ⟶ (r ⟶ s))" 
  shows   "r ⟶ (q ⟶ (p ⟶ s))"
proof 
  assume 2:  "r"
  show "(q ⟶ (p ⟶ s))"
  proof 
    assume 3:  "q" 
    show "(p ⟶ s)"
    proof 
      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


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

lemma ejercicio_11: carmarria
  "(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

lemma ejercicio_11: marmedmar3
  "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof 
  assume 1: "(p ⟶ (q ⟶ r))" 
  show "((p ⟶ q) ⟶ (p ⟶ r))"
  proof 
    assume 2: "(p ⟶ q)" 
    show "(p ⟶ r)" 
    proof 
      assume 3: "p" 
      have 4: "(q ⟶ r)" using 1 3 by (rule mp) 
      have 5: "q" using 2 3 by (rule mp) 
      show "r" using 4 5 by (rule mp) 
    qed
  qed
qed


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

lemma ejercicio_12: carmarria
  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 "p ⟶ (q ⟶ r)" by (rule impI)
qed

section {* Conjunciones *}

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

lemma ejercicio_13: carmarria
  assumes "p"
          "q" 
  shows "p ∧ q"

proof-
  show "p \<and> q" using assms(1) assms(2) by (rule conjI)
qed

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

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

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

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

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

lemma ejercicio_16: carmarria
  assumes 1: "p ∧ (q ∧ r)"
  shows   "(p ∧ q) ∧ r"
proof -
  have 2: "q \<and> r" using 1 by (rule conjunct2)
  have 3: p using 1 by (rule conjunct1)
  have 4: q using 2 by (rule conjunct1)
  have 5: r using 2 by (rule conjunct2)
  have 6: "p \<and> q" using 3 4 by (rule conjI)
  show "(p \<and> q) \<and> r" using 6 5 by (rule conjI)
qed

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

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

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

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

lemma ejercicio_18: carmarria
  assumes "p ∧ q" 
  shows   "p ⟶ q"
proof -
  {assume p
    have q using assms(1) by (rule conjunct2)
  }
  thus "p ⟶ q" by (rule impI)
qed

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

lemma ejercicio_19: carmarria
  assumes 1: "(p ⟶ q) ∧ (p ⟶ r)" 
  shows   "p ⟶ q ∧ r"
proof -
  {assume 2: p
    have 3: "p ⟶ q" using 1 by (rule conjunct1)
    have 4: "p ⟶ r" using 1 by (rule conjunct2)
    have 5: q using 3 2 by (rule mp)
    have 6: r using 4 2 by (rule mp)
    have 7: "q \<and> r" using 5 6 by (rule conjI)
  }
  thus "p ⟶ q \<and> r" by (rule impI)
qed

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

lemma ejercicio_20: carmarria
  assumes 1: "p ⟶ q ∧ r" 
  shows   "(p ⟶ q) ∧ (p ⟶ r)"
proof -
  {assume 2: p
    have 3: "q \<and> r" using 1 2 by (rule mp)
    have 4: q using 3 by (rule conjunct1)
  }
  hence 5: "p ⟶ q" by (rule impI)
  {assume 6: p
      have 7: "q \<and> r" using 1 6 by (rule mp)
      have 8: r using 7 by (rule conjunct2)
    }
    hence 9: "p ⟶ r" by (rule impI)
    show "(p ⟶ q) \<and> (p ⟶ r)" using 5 9 by (rule conjI)
  qed

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

lemma ejercicio_21: carmarria
  assumes 1: "p ⟶ (q ⟶ r)" 
  shows   "p ∧ q ⟶ r"
proof -
  {assume 2: "p \<and> 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)
    have 6: r using 5 4 by (rule mp)
  }
  thus "p ∧ q ⟶ r" by (rule impI)
qed

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

lemma ejercicio_22: carmarria
  assumes "p ∧ q ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"
proof -
  {assume p
    {assume q
      have "p \<and> q" using `p` `q` by (rule conjI)
      have r using assms(1) `p \<and> q` by (rule mp)
    }
    hence "q ⟶ r" by (rule impI)
  }
  thus "p ⟶ (q ⟶ r)" by (rule impI)
qed

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

lemma ejercicio_23: carmarria
  assumes "(p ⟶ q) ⟶ r" 
  shows   "p ∧ q ⟶ r"
proof -
  {assume "p \<and> q" 
    {assume p
      have q using `p \<and> q` by (rule conjunct2)
    }
    hence "p ⟶ q" by (rule impI)
    have r using assms(1) `p ⟶ q` by (rule mp)
  }
  thus "p \<and> q ⟶ r" by (rule impI)
qed

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

lemma ejercicio_24: carmarria
  assumes 1: "p ∧ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ r"
proof -
  {assume 2: "p ⟶ q" 
    have 3: p using 1 by (rule conjunct1)
    have 4: "q ⟶ r" using 1 by (rule conjunct2)
    have 5: q using 2 3 by (rule mp)
    have 6: r using 4 5 by (rule mp)
  }
  thus "(p ⟶ q) ⟶ r" by (rule impI)
qed

section {* Disyunciones *}

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

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

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

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

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

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

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

lemma ejercicio_28: carmarria
  assumes "q ⟶ r" 
  shows   "p ∨ q ⟶ p ∨ r"
proof -
  {assume "p | q" 
    moreover
    {assume p
      have "p | r" using `p` by (rule disjI1)
    }
    moreover
    {assume q
      have r using assms(1) `q` by (rule mp)
      have "p | r" using `r` by (rule disjI2)
    }
    ultimately have  "p | r" by (rule disjE)
}
  thus "p | q ⟶ p | r" by (rule impI)
qed

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

lemma ejercicio_29: carmarria
  assumes "p ∨ p"
  shows   "p"
proof -
  have "p | p" using assms(1) by this
  moreover 
  {assume p
  }
  moreover
  {assume p
  }
  ultimately show p by (rule disjE)
qed
  

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

lemma ejercicio_30: carmarria
  assumes "p" 
  shows   "p ∨ p"
proof -
  show "p | p" using assms(1) by (rule disjI1)
qed

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

lemma ejercicio_31:
  assumes "p ∨ (q ∨ r)" 
  shows   "(p ∨ q) ∨ r"
oops

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

lemma ejercicio_32:
  assumes "(p ∨ q) ∨ r" 
  shows   "p ∨ (q ∨ r)"
oops

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

lemma ejercicio_33:
  assumes "p ∧ (q ∨ r)" 
  shows   "(p ∧ q) ∨ (p ∧ r)"
oops

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

lemma ejercicio_34:
  assumes "(p ∧ q) ∨ (p ∧ r)" 
  shows   "p ∧ (q ∨ r)"
oops

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

lemma ejercicio_35:
  assumes "p ∨ (q ∧ r)" 
  shows   "(p ∨ q) ∧ (p ∨ r)"
oops

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

lemma ejercicio_36:
  assumes "(p ∨ q) ∧ (p ∨ r)"
  shows   "p ∨ (q ∧ r)"
oops

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

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

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

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

section {* Negaciones *}

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

lemma ejercicio_39:
  assumes "p"
  shows   "¬¬p"
oops

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

lemma ejercicio_40:
  assumes "¬p" 
  shows   "p ⟶ q"
oops

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

lemma ejercicio_41:
  assumes "p ⟶ q"
  shows   "¬q ⟶ ¬p"
oops

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

lemma ejercicio_42:
  assumes "p∨q"
          "¬q" 
  shows   "p"
oops

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

lemma ejercicio_43:
  assumes "p ∨ q"
          "¬p" 
  shows   "q"
oops

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

lemma ejercicio_44:
  assumes "p ∨ q" 
  shows   "¬(¬p ∧ ¬q)"
oops

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

lemma ejercicio_45:
  assumes "p ∧ q" 
  shows   "¬(¬p ∨ ¬q)"
oops

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

lemma ejercicio_46:
  assumes "¬(p ∨ q)" 
  shows   "¬p ∧ ¬q"
oops

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

lemma ejercicio_47:
  assumes "¬p ∧ ¬q" 
  shows   "¬(p ∨ q)"
oops

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

lemma ejercicio_48:
  assumes "¬p ∨ ¬q"
  shows   "¬(p ∧ q)"
oops

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

lemma ejercicio_49:
  "¬(p ∧ ¬p)"
oops

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

lemma ejercicio_50:
  assumes "p ∧ ¬p" 
  shows   "q"
oops

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

lemma ejercicio_51:
  assumes "¬¬p"
  shows   "p"
oops

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

lemma ejercicio_52:
  "p ∨ ¬p"
oops

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

lemma ejercicio_53:
  "((p ⟶ q) ⟶ p) ⟶ p"
oops

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

lemma ejercicio_54:
  assumes "¬q ⟶ ¬p"
  shows   "p ⟶ q"
oops

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

lemma ejercicio_55:
  assumes "¬(¬p ∧ ¬q)"
  shows   "p ∨ q"
oops

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

lemma ejercicio_56:
  assumes "¬(¬p ∨ ¬q)" 
  shows   "p ∧ q"
oops

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

lemma ejercicio_57:
  assumes "¬(p ∧ q)"
  shows   "¬p ∨ ¬q"
oops

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

lemma ejercicio_58:
  "(p ⟶ q) ∨ (q ⟶ p)"
oops

end