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

lemma ej_1: joslopjim4 marcabcar1
  assumes "p --> q"
          "p"
  shows "q"
proof -
  show "q" using assms(1) assms(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

lemma ej_2: joslopjim4 marcabcar1
  assumes "p ⟶ q"
          "q ⟶ r"
          "p" 
  shows "r"
proof -
  have "q" using `p⟶q` `p` by (rule mp)
  show "r" using `q⟶r` `q` 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

lemma ej_3: joslopjim4 marcabcar1
  assumes "p ⟶ (q ⟶ r)"
          "p ⟶ q"
          "p"
  shows "r"
proof -
  have "q" using `p⟶q` `p` by (rule mp)
  have "q⟶r" using `p ⟶ (q ⟶ r)` `p` by (rule mp)
  show "r" using `q⟶r` `q` 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 

lemma ej_4: joslopjim4 marcabcar1
  assumes "p ⟶ q"
          "q ⟶ r" 
  shows "p ⟶ r"
proof (rule impI)
  assume "p"
  have "q" using assms(1) `p` by (rule mp)
  show "r" using assms(2) `q` 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

lemma ej_5: joslopjim4 marcabcar1
  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 `p ⟶ (q ⟶ r)` `p` by (rule mp)
    show "r" using `q⟶r` `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

lemma ej_6: joslopjim4 marcabcar1
  assumes "p ⟶ (q ⟶ r)" 
  shows   "(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` by (rule mp)
    have "q" using `p⟶q` `p` by (rule mp)
    show "r" using `q⟶r` `q` 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 
 
lemma ej_7: joslopjim4 marcabcar1
  assumes "p"  
  shows   "q ⟶ p"
proof (rule impI)
  assume "q"
  show "p" using assms 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

lemma ej_8: joslopjim4 marcabcar1
  shows "p⟶(q⟶p)"
proof (rule impI)
  assume "p"
  show "q⟶p"
  proof (rule impI)
    assume "q"
    show "p" using `p` 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

lemma ej_9: joslopjim4 marcabcar1
  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 `p⟶q` `p` by (rule mp)
    show "r" using `q⟶r` `q` 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

lemma ej_10: joslopjim4 marcabcar1
  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"
      have "q ⟶ (r ⟶ s)" using `p ⟶ (q ⟶ (r ⟶ s))` `p` by (rule mp)
      have "r⟶s" using `q ⟶ (r ⟶ s)` `q`  by (rule mp)
      show "s" using `r-->s` `r` 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

lemma ej_11: joslopjim4 marcabcar1
  shows "(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" using `p⟶q` `p` by (rule mp)
      have "q⟶r" using `p⟶(q⟶r)` `p` by (rule mp)
      show "r" using `q⟶r` `q` 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

lemma ej_12: joslopjim4 marcabcar1
  assumes "(p ⟶ q) ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"
proof (rule impI)
  assume "p"
  show "q⟶r"
  proof (rule impI)
    assume "q"
    have "p⟶q"
    proof (rule impI)
    assume "p"
    show "q" using `q` by this
  qed
  show "r" using `(p ⟶ q) ⟶ r` `p⟶q` by (rule mp)
qed
qed

section {* Conjunciones *}

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

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

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

lemma ej_13: joslopjim4 marcabcar1
  assumes "p"
          "q" 
  shows "p ∧ q"
proof-
  show "p∧q" using `p` `q` by (rule conjI)
qed

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

lemma ejercicio_14: carmarria marmedmar3
  assumes "p ∧ q"  
  shows   "p"

proof -
  show "p" using assms by (rule conjunct1)
qed

lemma ej_14: joslopjim4 marcabcar1
  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 marmedmar3
  assumes "p ∧ q" 
  shows   "q"

proof -
  show q using assms(1) by (rule conjunct2)
qed

lemma ej_15: joslopjim4 marcabcar1
  assumes "p ∧ q" 
  shows   "q"
proof-
  show "q" using assms by (rule conjunct2)
qed
  

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

lemma ejercicio_16: carmarria marmedmar3
  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

lemma ej_16: joslopjim4 marcabcar1
  assumes "p ∧ (q ∧ r)"
  shows   "(p ∧ q) ∧ r"
proof-
  have "p" using assms by (rule conjunct1)
  have "q∧r" using assms by (rule conjunct2)
  have "q" using `q∧r` by (rule conjunct1)
  have "r" using `q∧r` by (rule conjunct2)
  have "p∧q" using `p` `q` by (rule conjI)
  show "(p∧q)∧r" using `p∧q` `r` 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 marmedmar3
  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
  

lemma ej_17: joslopjim4 marcabcar1
  assumes "(p ∧ q) ∧ r" 
  shows   "p ∧ (q ∧ r)"
proof-
  have "p∧q" using assms by (rule conjunct1)
  have "r" using assms by (rule conjunct2)
  have "p" using `p∧q` by (rule conjunct1)
  have "q" using `p∧q` by (rule conjunct2)
  have "q∧r" using `q` `r` by (rule conjI)
  show "p∧(q∧r)" using `p` `q∧r` 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

lemma ejercicio_18: marmedmar3
  assumes "p ∧ q" 
  shows   "p ⟶ q"
proof 
  assume "p" 
  show "q" using assms by (rule conjunct2) 
qed 

lemma ej_18: joslopjim4 marcabcar1
  assumes "p ∧ q" 
  shows   "p ⟶ q"
proof (rule impI)
  assume "p"
  show "q" using assms by (rule conjunct2)
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

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

lemma ej_19: joslopjim4 marcabcar1
  assumes "(p ⟶ q) ∧ (p ⟶ r)" 
  shows   "p ⟶ q ∧ r"
proof (rule impI)
  assume "p"
  have "p⟶q" using assms by (rule conjunct1)
  have "q" using `p⟶q` `p` by (rule mp)
  have "p⟶r" using assms by (rule conjunct2)
  have "r" using `p⟶r` `p` by (rule mp)
  show "q∧r" using `q` `r` by (rule conjI)
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

lemma ej_20: joslopjim4 marcabcar1
  assumes "p ⟶ q ∧ r" 
  shows   "(p ⟶ q) ∧ (p ⟶ r)"
proof-
  have "p⟶q"
  proof
  assume "p"
  have "q∧r" using assms `p` by (rule mp)
  show "q" using `q∧r` by (rule conjunct1)
qed
  have "p⟶r"
  proof
    assume "p"
    have "q∧r" using assms `p` by (rule mp)
    show "r" using `q∧r` by (rule conjunct2)
  qed
  show "(p⟶q)∧(p⟶r)" using `p⟶q` `p⟶r` 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

lemma ejercicio_21: marmedmar3
  assumes "p ⟶ (q ⟶ r)" 
  shows   "p ∧ q ⟶ r"
proof 
  assume "p ∧ q" 
  hence "p" by (rule conjunct1) 
  with assms have "(q ⟶ r)" by (rule mp)
  have "q" using `p ∧ q` by (rule conjunct2) 
  with `(q ⟶ r)` show "r" by (rule mp) 
qed 

lemma ej_21: joslopjim4 marcabcar1
  assumes "p ⟶ (q ⟶ r)" 
  shows   "p ∧ q ⟶ r"
proof (rule impI)
  assume "p∧q"
  have "p" using `p∧q` by (rule conjunct1)
  have "q" using `p∧q` by (rule conjunct2)
  have "q⟶r" using assms `p` by (rule mp)
  show "r" using `q⟶r` `q` by (rule mp)
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

lemma ejercicio_22: marmedmar3
  assumes "p ∧ q ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"
proof 
  assume "p" 
  show "(q ⟶ r)"
  proof 
    assume "q" 
    with `p` have "p ∧ q" by (rule conjI) 
    with assms show "r" by (rule mp) 
  qed 
qed

lemma ej_22: joslopjim4 marcabcar1
  assumes "p ∧ q ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"
proof (rule impI)
  assume "p"
  show "q⟶r"
  proof (rule impI)
    assume "q"
    have "p∧q" using `p` `q` by (rule conjI)
    show "r" using assms `p∧q` by (rule mp)
  qed
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
 
lemma ejercicio_23: marmedmar3
  assumes "(p ⟶ q) ⟶ r" 
  shows   "p ∧ q ⟶ r"
proof 
  assume "p ∧ q"
  have "p"  using `p ∧ q` by (rule conjunct1)
  have "q" using `p ∧ q` by (rule conjunct2) 
  hence "(p ⟶ q)" by (rule impI) 
  with assms show "r" by (rule mp) 
qed 

lemma ej_23: joslopjim4 marcabcar1
  assumes "(p ⟶ q) ⟶ r" 
  shows   "p ∧ q ⟶ r"
proof (rule impI)
  assume "p∧q"
  have "p⟶q"
  proof
  assume "p"
  show "q" using `p∧q` by (rule conjunct2)
qed
  show "r" using assms `p⟶q` by (rule mp)
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

lemma ejercicio_24: marmedmar3
  assumes "p ∧ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ r"
proof 
  assume  "(p ⟶ q)" 
  have "(q ⟶ r)" using assms by (rule conjunct2)
  have "p" using assms by (rule conjunct1)
  with `(p ⟶ q)` have "q" by (rule mp) 
  with `(q ⟶ r)` show "r" by (rule mp)
qed 

lemma ej_24: joslopjim4 marcabcar1
  assumes "p ∧ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ r"
proof (rule impI)
  assume "p⟶q"
  have "p" using assms by (rule conjunct1)
  have "q⟶r" using assms by (rule conjunct2)
  have "q" using `p⟶q` `p` by (rule mp)
  show "r" using `q⟶r` `q` by (rule mp)
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

lemma ej_25: joslopjim4 marcabcar1
  assumes "p"
  shows   "p ∨ q"
proof (rule disjI1)
  show "p" using assms by this
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

lemma ej_26: joslopjim4 marcabcar1
  assumes "q"
  shows   "p ∨ q"
proof (rule disjI2)
  show "q" using assms by this
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

lemma ej_27: joslopjim4 marcabcar1
  assumes "p ∨ q"
  shows   "q ∨ p"
  using assms
proof 
  assume "p"
  then show "q∨p" by(rule disjI2)
next
  assume "q"
  show "q∨p" using `q` by(rule disjI1)
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

lemma ej_28: joslopjim4 marcabcar1
  assumes "q ⟶ r" 
  shows   "p ∨ q ⟶ p ∨ r"
proof (rule impI)
  assume "p∨q" 
  show "p∨r"
  using `p∨q`
proof 
  assume "p"
  show "p∨r" using `p` by (rule disjI1)
  next
    assume "q"
    have "r" using assms `q` by (rule mp)
    show "p∨r" using `r` by (rule disjI2)
  qed
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
  
lemma ej_29: joslopjim4
  assumes "p ∨ p"
  shows   "p"
proof (rule ccontr)
  assume "¬p"
  show False
    using assms
  proof
    assume "p"
    show False using `¬p` `p` by (rule notE)
  next
    assume "p"
    show False using `¬p` `p` by (rule notE)
  qed
qed

lemma ejercicio_29: marcabcar1
  assumes "p ∨ p"
  shows   "p"
  using `p ∨ p`
proof (rule disjE)
  {assume "p"
    show "p" using `p` by this}
next
  {assume "p"
    show "p" using `p` by this}
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

lemma ej_30: joslopjim4 marcabcar1
  assumes "p" 
  shows   "p ∨ p"
proof (rule disjI1)
  show "p" using assms by this
qed

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

lemma ejercicio_31: carmarria
  assumes 1: "p ∨ (q ∨ r)" 
  shows   "(p ∨ q) ∨ r"
proof -
  have "p | (q | r)" using 1 by this
  moreover {assume 2: p
    have 3: "p | q" using 2 by (rule disjI1)
    have 4: "(p | q) | r" using 3 by (rule disjI1)
  }
  moreover {assume 5: "q | r"
    moreover {assume 6: q
      have 7: "p | q" using 6 by (rule disjI2)
      have 8: "(p | q) | r " using 7 by (rule disjI1)
    }
    moreover {assume 9: r
      have 10: "(p | q) | r " using 9 by (rule disjI2)
    }
      ultimately have 11: "(p | q) | r " by (rule disjE)
  }
  ultimately show "(p | q) | r " by (rule disjE)
qed

lemma ej_31: joslopjim4 marcabcar1
  assumes "p ∨ (q ∨ r)" 
  shows   "(p ∨ q) ∨ r"
  using assms
proof 
  assume "p"
  have "p∨q" using `p` by (rule disjI1)
  thus "(p ∨ q) ∨ r" by (rule disjI1)
next
  assume "q∨r"
  show "(p ∨ q) ∨ r"
    using `q∨r`
  proof 
    assume "q"
    have "p∨q" using `q` by (rule disjI2)
    show "(p ∨ q) ∨ r" using `p∨q` by (rule disjI1)
  next
    assume "r"
    show "(p ∨ q) ∨ r" using `r` by (rule disjI2)
  qed
qed

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

lemma ejercicio_32: carmarria
  assumes 1: "(p ∨ q) ∨ r" 
  shows   "p ∨ (q ∨ r)"
proof -
  have "(p | q) | r" using 1 by this
  moreover {assume 2: "p | q" 
    moreover {assume 3: p 
      have 4: "p | (q | r)" using 3 by (rule disjI1)
    }
    moreover {assume 5: q
      have 6: "q | r" using 5 by (rule disjI1)
      have 7: "p | (q | r)" using 6 by (rule disjI2)
    }
    ultimately have 8: " p | (q | r)" by (rule disjE)
  }
      moreover {assume 9: r
        have 10: "q | r" using 9 by (rule disjI2)
        have 11: "p | (q | r)" using 10 by (rule disjI2)
      }
      ultimately show "p | (q | r)" by (rule disjE)
    qed

lemma ej_32: joslopjim4 marcabcar1
  assumes "(p ∨ q) ∨ r" 
  shows   "p ∨ (q ∨ r)"
  using assms
proof
  assume "p∨q"
  show "p ∨ (q ∨ r)"
    using `p∨q`
  proof 
    assume "p"
    show "p ∨ (q ∨ r)" using `p` by (rule disjI1)
  next
    assume "q"
    have "q∨r" using `q` by (rule disjI1)
    show "p ∨ (q ∨ r)" using `q∨r` by (rule disjI2)
  qed
next
  assume "r"
  have "q∨r" using `r` by (rule disjI2)
  show "p ∨ (q ∨ r)" using `q∨r` by (rule disjI2)
qed

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

lemma ejercicio_33: carmarria
  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)
  moreover {assume 4: q
    have 5: "p & q" using 2 4 by (rule conjI)
    have 6: "(p & q) | (p & r)" using 5 by (rule disjI1)
  }
  moreover {assume 7: r
    have 8: "p & r" using 2 7 by (rule conjI)
    have 9: "(p & q) | (p & r)" using 8 by (rule disjI2)
  }
  ultimately show "(p & q) | (p & r)" by (rule disjE)
qed

lemma ej_33: joslopjim4 marcabcar1
  assumes "p ∧ (q ∨ r)" 
  shows   "(p ∧ q) ∨ (p ∧ r)"
proof-
  have "p" using assms by (rule conjunct1)
  have "q∨r" using assms by (rule conjunct2)
  show "(p ∧ q) ∨ (p ∧ r)"
  using `q∨r` 
proof (rule disjE)
assume "q"
  have "p∧q" using `p` `q` by (rule conjI)
  show "(p ∧ q) ∨ (p ∧ r)" using `p∧q` by (rule disjI1)
next
  assume "r"
  have "p∧r" using `p` `r` by (rule conjI)
  show "(p ∧ q) ∨ (p ∧ r)" using `p∧r` by (rule disjI2)
qed
qed

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

lemma ejercicio_34: carmarria
  assumes 1: "(p ∧ q) ∨ (p ∧ r)" 
  shows   "p ∧ (q ∨ r)"
proof -
  have "(p & q) | (p & r)" using 1 by this
  moreover {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 4 by (rule disjI1)
    have 6: "p & (q | r)" using 3 5 by (rule conjI)
  }
    moreover {assume 7: "p & r"
    have 8: p using 7 by (rule conjunct1)
    have 9: r using 7 by (rule conjunct2)
    have 10: "q | r" using 9 by (rule disjI2)
    have 11: "p & (q | r)" using 8 10 by (rule conjI)
  }
  ultimately show "p & (q | r)" by (rule disjE)
qed

lemma ej_34: joslopjim4 marcabcar1
  assumes "(p ∧ q) ∨ (p ∧ r)" 
  shows   "p ∧ (q ∨ r)"
  using assms
proof
  assume "p∧q"
  have "p" using `p∧q` by (rule conjunct1)
  have "q" using `p∧q` by (rule conjunct2)
  have "q∨r" using `q` by (rule disjI1)
  show "p∧(q∨r)" using `p` `q∨r` by (rule conjI)
next
  assume "p∧r"
  have "p" using `p∧r` by (rule conjunct1)
  have "r" using `p∧r` by (rule conjunct2)
  have "q∨r" using `r` by (rule disjI2)
  show "p∧(q∨r)" using `p` `q∨r` by (rule conjI)
qed

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

lemma ejercicio_35: carmarria
  assumes 1: "p ∨ (q ∧ r)" 
  shows   "(p ∨ q) ∧ (p ∨ r)"
proof -
  have "p | (q & r)" using 1 by this
  moreover {assume 2: p
    have 3: " p | q" using 2 by (rule disjI1)
    have 4: " p | r" using 2 by (rule disjI1)
    have 5: "(p | q) & (p | r)" using 3 4 by (rule conjI)
  }
  moreover {assume 6: "q & r" 
    have 7: q using 6 by (rule conjunct1)
    have 8: r using 6 by (rule conjunct2)
    have 9: "p | q" using 7 by (rule disjI2)
    have 10: "p | r" using 8 by (rule disjI2)
    have 11: "(p | q) & (p | r)" using 9 10 by (rule conjI)
  }
  ultimately show "(p | q) & (p | r)" by (rule disjE)
qed

lemma ej_35: joslopjim4 marcabcar1
  assumes "p ∨ (q ∧ r)" 
  shows   "(p ∨ q) ∧ (p ∨ r)"
  using assms
proof (rule disjE)
  assume "p"
  have "p∨q" using `p` by (rule disjI1)
  have "p∨r" using `p` by (rule disjI1)
  show "(p ∨ q) ∧ (p ∨ r)" using `p∨q` `p∨r` by (rule conjI)
next
  assume "q∧r"
  have "q" using `q∧r` by (rule conjunct1)
  have "r" using `q∧r` by (rule conjunct2)
  have "p∨q" using `q` by (rule disjI2)
  have "p∨r" using `r` by (rule disjI2)
  show "(p ∨ q) ∧ (p ∨ r)" using `p∨q` `p∨r` by (rule conjI)
qed

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

lemma ejercicio_36: carmarria
  assumes 1: "(p ∨ q) ∧ (p ∨ r)"
  shows   "p ∨ (q ∧ r)"
proof -
  have 2: "p | q" using 1 by (rule conjunct1)
  moreover {assume 3: p
    have 4: "p | (q & r)" using 3 by (rule disjI1)
  }
  moreover {assume 5: q
    have 6: "p | r" using 1 by (rule conjunct2)
    moreover {assume 7: p
      have 8: "p | (q & r)" using 7 by (rule disjI1)
    }
    moreover {assume 9: r
      have 10: "q & r" using 5 9 by (rule conjI)
      have 11: "p | (q & r)" using 10 by (rule disjI2)
    }
    ultimately have 12: "p | (q & r)" by (rule disjE)
  }
  ultimately show "p | (q & r)" by (rule disjE)
qed

lemma ej_36: joslopjim4 marcabcar1
  assumes "(p ∨ q) ∧ (p ∨ r)"
  shows   "p ∨ (q ∧ r)"
proof-
  have "p∨q" using assms by (rule conjunct1)
  have "p∨r" using assms by (rule conjunct2)
  show "p∨(q ∧ r)"
    using `p∨r`
  proof
    assume "p"
    show "p∨(q ∧ r)" using `p` by (rule disjI1)
  next
    assume "r"
    show "p∨(q ∧ r)"
      using `p∨q`
    proof
      assume "p"
      show "p∨(q ∧ r)" using `p` by (rule disjI1)
    next
      assume "q"
      have "q∧r" using `q` `r` by (rule conjI)
      show "p∨(q ∧ r)" using `q∧r` by (rule disjI2)
    qed
  qed
qed

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

lemma ejercicio_37: carmarria
  assumes 1: "(p ⟶ r) ∧ (q ⟶ r)" 
  shows   "p ∨ q ⟶ r"
proof -
  have 2: "p ⟶ r" using 1 by (rule conjunct1)
  have 3: "q ⟶ r" using 1 by (rule conjunct2)
  {assume 4: "p | q"
    moreover {assume 5: p
      have 6: r using 2 5 by (rule mp)
    }
    moreover {assume 7: q
      have 8: r using 3 7 by (rule mp)
    }
    ultimately have r by (rule disjE)
  }
  thus "p | q ⟶ r" by (rule impI)
qed

lemma ej_37: joslopjim4 marcabcar1
  assumes "(p ⟶ r) ∧ (q ⟶ r)" 
  shows   "p ∨ q ⟶ r"
proof (rule impI)
  assume "p∨q"
  have "p⟶r" using assms by (rule conjunct1)
  have "q⟶r" using assms by (rule conjunct2)
  show "r"
    using `p∨q`
  proof 
    assume "p"
    show "r" using `p⟶r` `p` by (rule mp)
  next
    assume "q"
    show "r" using `q⟶r` `q` by (rule mp)
  qed
qed

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

lemma ejercicio_38: carmarria
  assumes 1: "p ∨ q ⟶ r" 
  shows   "(p ⟶ r) ∧ (q ⟶ r)"
proof -
  {assume 2: p
    have 3: "p | q" using 2 by (rule disjI1)
    have 4: r using 1 3 by (rule mp)
  }
    hence 5: "p ⟶ r" by (rule impI)
  {assume 6: q
    have 7: "p | q" using 6 by (rule disjI2)
    have 8: r using 1 7 by (rule mp)
  }
  hence 9: "q ⟶ r" by (rule impI)
  show "(p ⟶ r) & (q ⟶ r)" using 5 9 by (rule conjI)
qed

lemma ej_38: joslopjim4 marcabcar1
  assumes "p ∨ q ⟶ r" 
  shows   "(p ⟶ r) ∧ (q ⟶ r)"
proof-
  have "p⟶r" 
  proof (rule impI)
  assume "p"
  have "p∨q" using `p` by (rule disjI1)
  show "r" using assms `p∨q` by (rule mp)
qed
  have "q⟶r"
  proof (rule impI)
    assume "q"
    have "p∨q" using `q` by (rule disjI2)
    show "r" using assms `p∨q` by (rule mp)
  qed
  show "(p ⟶ r) ∧ (q ⟶ r)" using `p⟶r` `q⟶r` by (rule conjI)
qed

section {* Negaciones *}

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

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

lemma ej_39: joslopjim4 marcabcar1
  assumes "p"
  shows   "¬¬p"
proof-
  show "¬¬p" using assms by (rule notnotI)
qed

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

lemma ejercicio_40: carmarria
  assumes "¬p" 
  shows   "p ⟶ q"
proof -
  {assume p
    have "~p" using assms(1) by this
    have False using `~p` `p` by (rule notE)
    have q using `False` by (rule FalseE)
  }
  thus "p ⟶ q" by (rule impI)
qed

lemma ej_40: joslopjim4 marcabcar1
  assumes "¬p" 
  shows   "p ⟶ q"
proof (rule impI)
  assume "p"
  show "q" using assms `p` by (rule notE)
qed

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

lemma ejercicio_41: carmarria
  assumes 1: "p ⟶ q"
  shows   "¬q ⟶ ¬p"
proof -
  {assume 2: "~q"
    have 3: "~p" using 1 2 by (rule mt)
  }
  thus 4: "~q ⟶ ~p" by (rule impI)
qed

lemma ej_41: joslopjim4 marcabcar1
  assumes "p ⟶ q"
  shows   "¬q ⟶ ¬p"
proof (rule impI)
  assume "¬q"
  show "¬p" using assms `¬q` by (rule mt)
qed

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

lemma ejercicio_42: carmarria
  assumes 1: "p∨q" and
          2: "¬q" 
  shows   "p"
proof -
  have " p | q" using 1 by this
  moreover {assume 3: p
  }
  moreover {assume 4: q
    have 5: False using 2 4 by (rule notE)
    have 6: p using 5 by (rule FalseE)
  }
  ultimately show p by (rule disjE)
qed

lemma ej_42: joslopjim4 marcabcar1
  assumes "p∨q"
          "¬q" 
  shows   "p"
  using assms(1)
proof 
  assume "p"
  show "p" using `p` by this
next
  assume "q"
  show "p" using assms(2) `q` by (rule notE)
qed

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

lemma ejercicio_43: carmarria
  assumes 1: "p ∨ q" and
          2: "¬p" 
        shows   "q"
proof -
  have " p | q" using 1 by this
  moreover {assume 3: p
    have 4: False using 2 3 by (rule notE)
    have 5: q using 4 by (rule FalseE)
  }
  moreover {assume 6: q
  }
  ultimately show q by (rule disjE)
qed

lemma ej_43: joslopjim4 marcabcar1
  assumes "p ∨ q"
          "¬p" 
  shows   "q"
  using assms(1)
proof
  assume "p"
  show "q" using assms(2) `p` by (rule notE)
next
  assume "q"
  show "q" using `q` by this
qed

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

lemma ejercicio_44: carmarria
  assumes 1: "p ∨ q" 
  shows   "¬(¬p ∧ ¬q)"
proof -
  have "p | q" using 1 by this
  moreover {assume 2: p
    {assume 3:"~p & ~q"
      have 4: "~p" using 3 by (rule conjunct1)
      have 5: False using 4 2 by (rule notE)
    }
    hence 6: "~(~p & ~q)" by (rule notI)
  }
  moreover {assume 7: q
    {assume 8: "~p & ~q"
      have 9: "~q" using 8 by (rule conjunct2)
      have 10: False using 9 7 by (rule notE)
    }
    hence 11: "~(~p & ~q)" by (rule notI)
  }
  ultimately show "~(~p & ~q)" by (rule disjE)
qed

lemma ej_44: joslopjim4 marcabcar1
  assumes "p∨q"
  shows "¬(¬p∧¬q)"
proof (rule notI)
  assume "¬p∧¬q"
  show False
    using assms
  proof
    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

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

lemma ejercicio_45: carmarria
  assumes 1: "p ∧ q" 
  shows   "¬(¬p ∨ ¬q)"
proof -
  {assume 2: "~p | ~q"
    moreover {assume 3: "~p"
      have 4: p using 1 by (rule conjunct1)
      have 5: False using 3 4 by (rule notE)
    }
    moreover {assume 6: "~q"
      have 7: q using 1 by (rule conjunct2)
      have 8: False using 6 7 by (rule notE)
    }
    ultimately have False by (rule disjE)
  }
  thus "~(~p | ~q)" by (rule notI)
qed

lemma ej_45: joslopjim4 marcabcar1
  assumes "p∧q"
  shows "¬(¬p∨¬q)"
proof (rule notI)
  assume "¬p∨¬q"
  then show False
  proof (rule disjE)
    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

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

lemma ejercicio_46: carmarria
  assumes 1: "¬(p ∨ q)" 
  shows   "¬p ∧ ¬q"
proof -
  {assume 2: p
    have 3: "p | q" using 2 by (rule disjI1)
    have 4: False using 1 3 by (rule notE)
  }
  hence 5: "~p" by (rule notI)
      {assume 6: q
    have 7: "p | q" using 6 by (rule disjI2)
    have 8: False using 1 7 by (rule notE)
  }
  hence 9: "~q" by (rule notI)
  show "~p & ~q" using 5 9 by (rule conjI)
qed

lemma ej_46: joslopjim4
  assumes "¬(p ∨ q)"
  shows "¬p ∧ ¬q"
proof (rule conjI)
  show "¬p"
  proof (rule ccontr)
    assume "¬¬p"
    have "p" using `¬¬p` by (rule notnotD)
    have "p∨q" using `p` by (rule disjI1)
    show False using assms `p∨q` by (rule notE)
  qed
  show "¬q"
  proof (rule ccontr)
    assume "¬¬q"
    have "q" using `¬¬q` by (rule notnotD)
    have "p∨q" using `q` by (rule disjI2)
    show False using assms `p∨q` by (rule notE)
  qed
qed

lemma ejercicio_46: marcabcar1
  assumes "¬(p ∨ q)" 
  shows   "¬p ∧ ¬q"
proof (rule conjI)
  show "¬p"
     proof (rule disjE)
       show "p∨¬p" by (rule excluded_middle)
        {assume "p"
          have "p ∨ q" using `p` by (rule disjI1)
          show "¬p" using `¬(p ∨ q)` and `p ∨ q` by (rule notE)}
      next
        {assume "¬p"
          show "¬p" using `¬p` by this}
      qed
   show "¬q"
     proof (rule disjE)
       show "q∨¬q" by (rule excluded_middle)
        {assume "q"
          have "p ∨ q" using `q` by (rule disjI2)
          show "¬q" using `¬(p ∨ q)` and `p ∨ q` by (rule notE)}
      next
        {assume "¬q"
          show "¬q" using `¬q` by this}
      qed
    qed

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

lemma ejercicio_47: carmarria
  assumes 1: "¬p ∧ ¬q" 
  shows   "¬(p ∨ q)"
proof -
  {assume 2: "p | q"
    moreover {assume 3: p
      have 4: "~p" using 1 by (rule conjunct1)
      have 5: False using 4 3 by (rule notE)
    }
    moreover {assume 6: q 
      have 7: "~q" using 1 by (rule conjunct2)
      have 8: False using 7 6 by (rule notE)
    }
    ultimately have 9: False by (rule disjE)
  }
  thus "~(p | q)" by (rule notI)
qed   

lemma ej_47: joslopjim4 marcabcar1
  assumes "¬p∧¬q"
  shows "¬(p∨q)"
proof (rule notI)
  assume "p∨q"
  then show 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

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

lemma ejercicio_48: carmarria
  assumes 1: "¬p ∨ ¬q"
  shows   "¬(p ∧ q)"
proof -
  have "~p | ~q" using 1 by this
  moreover {assume 2: "~p"
    {assume 3: "p & q"
      have 4: p using 3 by (rule conjunct1)
      have 5: False using 2 4 by (rule notE)
    }
    hence 6: "~(p & q)" by (rule notI)
  }
  moreover {assume 7: "~q"
      {assume 8: "p & q"
      have 9: q using 8 by (rule conjunct2)
      have 10: False using 7 9 by (rule notE)
    }
    hence 11: "~(p & q)" by (rule notI)
  }
  ultimately show "~(p & q)" by (rule disjE)
qed

lemma ej_48: joslopjim4 marcabcar1
  assumes "¬p ∨ ¬q"
  shows   "¬(p ∧ q)"
proof (rule notI)
  assume "p∧q"
  have "p" using `p∧q` by (rule conjunct1)
  have "q" using `p∧q` by (rule conjunct2)
  show False
  using assms
proof
  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

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

lemma ejercicio_49: carmarria
  "¬(p ∧ ¬p)"
proof -
  {assume 1: "p & ~p"
    have 2: p using 1 by (rule conjunct1)
    have 3: "~p" using 1 by (rule conjunct2)
    have 4: False using 3 2 by (rule notE)
  }
  thus "~(p & ~p)" by (rule notI)
qed

lemma ej_49: joslopjim4 marcacar1
  shows "¬(p∧¬p)"
proof
  assume "p∧¬p"
  have "p" using `p∧¬p` by (rule conjunct1)
  have "¬p" using `p∧¬p` by (rule conjunct2)
  show False using `¬p` `p` by (rule notE)
qed

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

lemma ejercicio_50: carmarria
  assumes 1: "p ∧ ¬p" 
  shows   "q"
proof -
  have 2: p using 1 by (rule conjunct1)
  have 3: "~p" using 1 by (rule conjunct2)
  have 4: False using 3 2 by (rule notE)
  show q using 4 by (rule FalseE)
qed
  
lemma ej_50: joslopjim4 marcabcar1
  assumes "p∧¬p"
  shows "q"
proof-
  have "p" using `p∧¬p` by (rule conjunct1)
  have "¬p" using `p∧¬p` by (rule conjunct2)
  have False using `¬p` `p` by (rule notE)
  then show "q" by (rule FalseE)
qed

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

lemma ejercicio_51: carmarria joslopjim4 marcabcar1
  assumes "¬¬p"
  shows   "p"
proof -
  show p using assms by (rule notnotD)
qed

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

lemma ejercicio_52: carmarria
  "p ∨ ¬p"
proof -
  {assume 1: "~(p | ~p)"
    {assume 2: p 
      have 3: "p | ~p" using 2 by (rule disjI1)
      have 4: False  using 1 3 by (rule notE)
    }
    hence 5: "~p" by (rule notI)
    have 6: "p | ~p" using 5 by (rule disjI2)
    have 7: False using 1 6 by (rule notE)
  }
    hence 8: "~~(p | ~p)" by (rule notI)
    show "p | ~p" using 8 by (rule notnotD)
qed
   
lemma ejercicio_52: marcabcar1
  "p ∨ ¬p"
proof (rule ccontr)
  {assume "¬(p ∨ ¬p)"
  have "¬p"
   proof (rule notI)
     {assume "p"
      have "p ∨ ¬p" using `p` by (rule disjI1)
      show "False" using `¬(p ∨ ¬p)`  and `(p ∨ ¬p)` by (rule notE)}
  qed
  have "p ∨ ¬p" using `¬p` by (rule disjI2)
  show "False" using `¬(p ∨ ¬p)` and `p ∨ ¬p` by (rule notE)}
qed 

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

lemma ej_53: joslopjim4
  shows "((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

lemma ejercicio_53: carmarria
  "((p ⟶ q) ⟶ p) ⟶ p"
proof -
  {assume 1: "(p ⟶ q) ⟶ p" 
    {assume 2:"~p"
      have 3: "~(p ⟶q)" using 1 2 by (rule mt)
      {assume 4: p
        have 5: False using 2 4 by (rule notE)
        have 6: q using 5 by (rule FalseE)
      }
      hence 7: "p ⟶q" by (rule impI)
      have 8: False using 3 7 by (rule notE)
    }
    hence 9: "~~p" by (rule notI)
    have 10: p using 9 by (rule notnotD)
  }
  thus "((p ⟶ q)⟶p)⟶p" by (rule impI)
qed

lemma ejercicio_53: marcabcar1
  "((p ⟶ q) ⟶ p) ⟶ p"
proof (rule impI)
  assume "(p ⟶ q) ⟶ p"
   show "p"
   proof (rule disjE)
     show "p ∨ ¬p" by (rule excluded_middle)
     {assume "p"
       show "p" using `p` by this}
   next
     {assume "¬p"
       have "¬(p⟶q)" using `(p ⟶ q) ⟶ p` and `¬p` by (rule mt)
       have "p⟶q"
       proof (rule impI)
         {assume "p"
           show "q" using `¬p` and `p` by (rule notE)}
       qed
       show "p" using `¬(p⟶q)` and `p⟶q` by (rule notE)}
   qed


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

lemma ej_54: joslopjim4
  assumes "¬q ⟶ ¬p"
  shows   "p ⟶ q"
proof (rule impI)
  assume "p"
  have "¬¬p" using `p` by (rule notnotI)
  have "¬¬q" using assms `¬¬p` by (rule mt)
  show "q" using `¬¬q` by (rule notnotD)
qed

lemma ejercicio_54: carmarria
  assumes 1: "¬q ⟶ ¬p"
  shows   "p ⟶ q"
proof -
  {assume 2: p
    have 3: "~~p" using 2 by (rule notnotI)
    have 4: "~~q" using 1 3 by (rule mt)
    have 5: q using 4 by (rule notnotD)
  }
  thus "p ⟶q" by (rule impI)
qed

lemma ejercicio_54: marcabcar1
  assumes "¬q ⟶ ¬p"
  shows   "p ⟶ q"
proof (rule impI)
  {assume "p"
    have "q∨¬q" by (rule excluded_middle)
    show "q"
    proof (rule disjE)
      show "q ∨ ¬q" using `q ∨ ¬q` by this
      {assume "q"
        show "q" using `q` by this}
    next
      {assume "¬q"
        have "¬p" using `¬q ⟶ ¬p` and `¬q` by (rule mp)
        show "q" using `¬p` and `p` by (rule notE)}
    qed}
  qed

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

lemma ejercicio_55: carmarria
  assumes 1: "¬(¬p ∧ ¬q)"
  shows   "p ∨ q"
proof - 
  {assume 2: "~(p | q)"
  {assume 3: "~p"
    {assume 4: "~q"
      have 5: "~p & ~q" using 3 4 by (rule conjI)
      have 6: False using 1 5 by (rule notE)
    }
      hence 7: "~~q" by (rule notI)
      have 8: q using 7 by (rule notnotD)
      have 9: "p | q" using 8 by (rule disjI2)
      have 10: False using 2 9 by (rule notE)
    }
    hence 11: "~~p" by (rule notI)
    have 12: p using 11 by(rule notnotD)
    have 13: "p | q" using 12 by (rule disjI1)
    have 14: False using 2 13 by (rule notE)
  }
  hence 15: "~~(p | q)" by (rule notI)
  show "p | q" using 15 by (rule notnotD)
qed

lemma ej_55: joslopjim4
  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"
    proof-
      have "¬q∨q" by (rule excluded_middle)
      thus "p∨q"
      proof
        assume "¬q"
        have "¬p∧¬q" using `¬p` `¬q` by (rule conjI)
        have False using assms `¬p∧¬q` by (rule notE)
        then show "p∨q" by (rule FalseE)
      next
        assume "q"
        show "p∨q" using `q` by (rule disjI2)
      qed
    qed
  next
    assume "p"
    show "p∨q" using `p` by (rule disjI1)
  qed
qed


lemma ejercicio_55:marcabcar1
  assumes "¬(¬p ∧ ¬q)"
  shows   "p ∨ q"
proof (rule disjE)
  show "p ∨ ¬p" by (rule excluded_middle)
  {assume "p"
    show "p ∨ q" using `p` by (rule disjI1)}
next
  {assume "¬p"
    show "p ∨ q"
    proof (rule disjE)
      show "q ∨ ¬q" by (rule excluded_middle)
      {assume "q"
        show "p ∨ q" using `q` by (rule disjI2)}
    next
      {assume "¬q"
        have "¬p ∧ ¬q" using `¬p` and `¬q` by (rule conjI)
        show "p ∨ q" using `¬(¬p ∧ ¬q)` and `(¬p ∧ ¬q)` by (rule notE)}
    qed}
qed

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

lemma ejercicio_56: carmarria
  assumes 1: "¬(¬p ∨ ¬q)" 
  shows   "p ∧ q"
proof -
    {assume 2: "~p"
      have 3: "~p | ~q" using 2 by (rule disjI1)
      have 4: False using 1 3 by (rule notE)
    }
    hence 5: "~~p" by (rule notI)
    have 6: p using 5 by (rule notnotD)
       {assume 7: "~q"
      have 8: "~p | ~q" using 7 by (rule disjI2)
      have 9: False using 1 8 by (rule notE)
    }
    hence 10: "~~q" by (rule notI)
    have 11: q using 10 by (rule notnotD)
    show 12: " p & q" using 6 11 by (rule conjI)
  qed

lemma ej_56: joslopjim4 marcabcar1
  assumes "¬(¬p ∨ ¬q)" 
  shows   "p ∧ q"
proof-
  have "¬p∨p" by (rule excluded_middle)
  thus "p∧q" 
  proof
    assume "¬p"
    have "¬p∨¬q" using `¬p` by (rule disjI1)
    have False using assms `¬p∨¬q` by (rule notE)
    then show "p∧q" by (rule FalseE)
  next
    assume "p"
    have "¬q∨q" by (rule excluded_middle)
    thus "p∧q"
    proof
      assume "q"
      show "p∧q" using `p` `q` by (rule conjI)
    next
      assume "¬q"
      have "¬p∨¬q" using `¬q` by (rule disjI2)
      have False using assms `¬p∨¬q` by (rule notE)
      then show "p∧q" by (rule FalseE)
    qed
  qed
qed

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

lemma ejercicio_57: carmarria
  assumes 1: "¬(p ∧ q)"
  shows   "¬p ∨ ¬q"
proof -
  {assume 2: "~(~p | ~q)"
  {assume 3: p
    {assume 4: q
      have 5: "p & q" using 3 4 by (rule conjI)
      have 6: False using 1 5 by (rule notE)
    }
    hence 7: "~q" by (rule notI)
    have 8: "~p | ~q" using 7 by (rule disjI2)
    have 9: False using 2 8 by (rule notE)
  }
  hence 10: "~p" by (rule notI)
  have 11: "~p | ~q" using 10 by (rule disjI1)
  have 12: False using 2 11 by (rule notE)
}
  hence 13: "~~(~p | ~q)" by (rule notI)
  show "~p | ~q" using 13 by (rule notnotD)
qed

lemma ej_57: joslopjim4 marcabcar1
  assumes "¬(p ∧ q)"
  shows   "¬p ∨ ¬q"
proof-
  have "¬p∨p" by (rule excluded_middle)
  thus "¬p∨¬q"
  proof (rule disjE)
    assume "¬p"
    show "¬p∨¬q" using `¬p` by (rule disjI1)
  next
    assume "p"
    have "¬q∨q" by (rule excluded_middle)
    thus "¬p∨¬q"
    proof (rule disjE)
      assume "¬q"
      show "¬p∨¬q" using `¬q` by (rule disjI2)
    next
      assume "q"
      have "p∧q" using `p` `q` by (rule conjI)
      have False using assms `p∧q` by (rule notE)
      then show "¬p∨¬q" by (rule FalseE)
    qed
  qed
qed

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

lemma ej_58: joslopjim4 marcabcar1
  shows "(p ⟶ q) ∨ (q ⟶ p)"
proof -
  have "¬p∨p" by (rule excluded_middle)
  thus "(p ⟶ q) ∨ (q ⟶ p)"
  proof (rule disjE)
    assume "¬p"
    show "(p ⟶ q) ∨ (q ⟶ p)"
    proof (rule disjI1)
      show "p⟶q"
      proof
        assume "p"
        show "q" using `¬p` `p` by (rule notE)
      qed
    qed
  next
    assume "p"
    show "(p ⟶ q) ∨ (q ⟶ p)"
    proof (rule disjI2)
      show "q⟶p"
    proof (rule impI)
      assume "q"
      show "p" using `p` by this
    qed
  qed
qed
qed

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

lemma ej_59: joslopjim4 marcabcar1
  assumes "p∧¬(q⟶r)"
  shows "(p∧q)∧¬r"
proof
  show "p∧q"
  proof
    show "p" using assms by (rule conjunct1)
  next
    show "q"
    proof (rule ccontr)
      assume "¬q"
      have "¬(q⟶r)" using assms by (rule conjunct2)
      have "q⟶r"
      proof
        assume "q"
        show "r" using `¬q` `q` by (rule notE)
      qed
      show False using `¬(q⟶r)` `q⟶r` by (rule notE)
    qed
  qed
next
  show "¬r"
  proof (rule notI)
    assume "r"
    have "q⟶r"
    proof
      assume "q" 
      show "r" using `r` by this
    qed
    have "¬(q⟶r)" using assms ..
    thus False using `q⟶r` ..
  qed
 qed

end