Rel 2

chapter  ‹  R2: Deducción natural proposicional(I)  ›

theory R2_sol
imports Main 
begin

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

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

text  ‹ 
  Se usarán las reglas notnotI y mt que demostramos a continuación.  ›

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

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

section  ‹  Implicaciones  ›

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

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

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

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


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

lemma ejercicio_1e: "⟦p ⟶ q; p⟧ ⟹ q" 
  apply (erule mp)
   apply assumption
  done
 
text  ‹  --------------------------------------------------------------- 
  Ejercicio 2. Demostrar
     p ⟶ q, q ⟶ r, p ⊢ r
  ------------------------------------------------------------------  ›

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

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

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

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

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


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

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

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

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

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

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

thm impE

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

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




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

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

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

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

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


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

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


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

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


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


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

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

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


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

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


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


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

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

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


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

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

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

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


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

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

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

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


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

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

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

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


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

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

lemma ejercicio_11b:
  "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof 
  assume "p ⟶ (q ⟶ r)"
  {assume "p ⟶  q"
    {assume "p"
      with `p ⟶  q` have "q" ..
      have "q ⟶ r" using `p ⟶ (q ⟶ r)` `p` ..
      then have "r" using `q` ..}
    then have "p ⟶  r" ..}
  then show "(p ⟶ q) ⟶ (p ⟶ r)" ..
qed


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

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


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

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

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

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

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


section  ‹  Conjunciones  ›

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

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

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

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

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


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

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


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

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


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

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

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

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


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


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


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

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

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


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

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

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

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

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


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

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

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

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


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

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

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

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


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

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

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


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

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


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

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

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

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


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

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


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

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


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

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

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

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

end