Relación 1

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

theory Rel_1
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:
  assumes 1:"p ⟶ q" and  
          2:"p"
  shows "q"


(*Solución M.Cumplido*)

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

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

lemma ejercicio_2:
  assumes 1:"p ⟶ q" and
          2:"q ⟶ r" and
          3:"p" 
  shows "r"

(*Solución M.Cumplido*)
 proof -
   have 4: "q" using 1 3 by (rule mp)
   show 5: "r" using 2 4 by (rule mp)
qed

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

lemma ejercicio_3:
  assumes 1:"p ⟶ (q ⟶ r)" and
          2:"p ⟶ q" and 
          3:"p"
  shows "r"

(*Solución M.Cumplido*)
proof -
  have 4:"q ⟶ r" using 1 3 by (rule mp)
  show "r" using 2 4 3 by (rule ejercicio_2)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 4. Demostrar
     p ⟶ q, q ⟶ r ⊢ p ⟶ r
  ------------------------------------------------------------------ *}
lemma ejercicio_4:
  assumes 1:"p ⟶ q" and
          2:"q ⟶ r" 
  shows "p ⟶ r"


(*Solución M.Cumplido*)
proof -
   {assume 3:"p"
   have "r" using 1 2 3 by (rule ejercicio_2)}
   thus "p ⟶ r" by (rule impI)
qed

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

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

(*Solución M.Cumplido*)
proof -
  {assume 2: q
    {assume 3: p
     have 4:"q ⟶ r" using 1 3 by (rule mp) 
     have r using 4 2 by (rule mp)}
    hence "p ⟶ r" by (rule impI)}
  thus "q ⟶ (p ⟶ r)" by (rule impI)
qed

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

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

(*Solución M.Cumplido*)
proof -
{assume 2:"p ⟶ q"
    {assume 3: p 
    have 4: "q ⟶ r" using 1 3 by (rule mp)
    have 5: "p ⟶ r" using 2 4 by (rule ejercicio_4)
    have r using 5 3 by (rule mp)}
    hence "p ⟶ r" by (rule impI)}
thus  "(p ⟶ q) ⟶ (p ⟶ r)" by (rule impI)
qed

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

lemma ejercicio_7:
  assumes 1:"p"  
  shows   "q ⟶ p"

(*Solución M.Cumplido*)
proof -
{assume 2:q
  have 3: p
     proof (rule ccontr)
     assume 4:"¬p" 
     show False using 4 1 by (rule notE) 
     qed
}
thus "q⟶p" by (rule impI)
qed

lemma ejercicio_7_1:
  assumes "p"  
  shows   "q ⟶ p"
(*L.E. Caraballo*)
proof -
  { assume "q"
    have "p" using assms(1) by this
    }
  thus "q⟶p" by (rule impI)  
qed

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

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

(*Solución M.Cumplido*)
proof -
{assume 1: p
 {assume 2:q
  have 3: p
     proof (rule ccontr)
     assume 4:"¬p" 
     show False using 4 1 by (rule notE) 
     qed}
 hence "q⟶p" by (rule impI)}
thus  "p ⟶ (q ⟶ p)"  by (rule impI)
qed

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

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

(*Solución M.Cumplido*)
proof -
{assume 2:"q⟶r"
have 3:"p⟶r" using 1 2 by (rule ejercicio_4)}
thus "(q ⟶ r) ⟶ (p ⟶ r)" by (rule impI)
qed  

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


lemma ejercicio_10:
  assumes 1:"p ⟶ (q ⟶ (r ⟶ s))" 
  shows   "r ⟶ (q ⟶ (p ⟶ s))"

(*Solución M.Cumplido*)
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 s using 6 2 by (rule mp)
     }
    hence "p⟶ s" by (rule impI)
  }
  hence "q ⟶ (p ⟶ s)" by (rule impI)
}
thus  "r ⟶ (q ⟶ (p ⟶ s))" by (rule impI)
qed


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

lemma ejercicio_11:
  "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"


(*Solución M.Cumplido*)
proof -

{assume "p ⟶ (q ⟶ r)"
 hence  "(p ⟶ q) ⟶ (p ⟶ r)" by (rule ejercicio_6)
}
thus  "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))" by (rule impI) 
qed

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


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

(*Solución M.Cumplido*)
proof -
{assume 2:p
    {assume 3:q
     hence 4:"p⟶q"  by (rule ejercicio_7)
     have r using 1 4 by (rule mp) 
    }
    hence "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:
  assumes 1:"p" and
          2:"q" 
  shows "p ∧ q"

(*Solución M.Cumplido*)
proof -
show "p ∧ q" using 1 2 by (rule conjI)
qed 

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

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

(*Solución M.Cumplido*)
proof - 
show p using assms(1) by (rule conjunct1)
qed

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

lemma ejercicio_15:
  assumes "p ∧ q" 
  shows   "q"

(*Solución M.Cumplido*)
proof -
show q using assms(1) by (rule conjunct2)
qed

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

lemma ejercicio_16:
  assumes "p ∧ (q ∧ r)"
  shows   "(p ∧ q) ∧ r"

(*Solución M.Cumplido*)
proof -
have 1: p using assms(1) by (rule conjunct1)
have 2: "q & r" using assms(1) 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

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

lemma ejercicio_17:
  assumes "(p ∧ q) ∧ r" 
  shows   "p ∧ (q ∧ r)"

(*Solución M.Cumplido*)
proof -
have 1: "p & q" using assms(1) by (rule conjunct1)
have 2: "r" using assms(1) by (rule conjunct2)
have 3: q using 1 by (rule conjunct2)
have 4: p using 1 by (rule conjunct1)
have 5: "q & r" using 3 2 by (rule conjI)
show  "p ∧ (q ∧ r)" using 4 5 by (rule conjI)
qed

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

lemma ejercicio_18:
  assumes "p ∧ q" 
  shows   "p ⟶ q"

(*Solución M.Cumplido*)
proof -
{assume 1: p
 have 2: 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:
  assumes "(p ⟶ q) ∧ (p ⟶ r)" 
  shows   "p ⟶ q ∧ r"

(*Solución M.Cumplido*)
proof -
have 1: "p⟶q" using assms(1) by (rule conjunct1)
have 2: "p⟶r" using assms(1) by (rule conjunct2)
{assume 3: p
 have 4: q using 1 3 by (rule mp)
 have 5: r using 2 3 by (rule mp)
 have 6: "q & r" using 4 5 by (rule conjI)
}
thus "p⟶ q & r" by (rule impI)
qed



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

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

(*Solución M.Cumplido*)
proof -
{assume 1:p
have 2:"q & r" using assms(1) 1 by (rule mp)
have 3: q using 2 by (rule conjunct1)}
hence 4: "p⟶q" by (rule impI)

{assume 5:p
have 6:"q & r" using assms(1) 5 by (rule mp)
have 7: r using 6 by (rule conjunct2)}
hence 8: "p⟶r" by (rule impI)

show  "(p ⟶ q) ∧ (p ⟶ r)" using 4 8 by (rule conjI)
qed

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

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

(*Solución M.Cumplido*)
proof -

{assume 1:"p & q"
 have 2: p using 1 by (rule conjunct1)
 have 3: "q⟶r" using assms(1) 2 by (rule mp)
 have 4: q using 1 by (rule conjunct2)
 have 5: r using 3 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:
  assumes "p ∧ q ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"

(*Solución M.Cumplido*)
proof -
{ assume 1: p
  {assume 2: q
   have 3: "p & q" using 1 2 by (rule conjI)
   have 4: r using assms(1) 3 by (rule mp)
  }
  hence "q⟶r" by (rule impI)
}
thus "p⟶(q⟶r)" by (rule impI)
qed

lemma ejercicio_22_1:
  assumes "p ∧ q ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"
(*L.E.Caraballo*)
proof (rule impI)
  assume 1: "p"
  show "(q⟶r)"
  proof (rule impI)
    assume 2: "q"
    have 3: "p∧q" using 1 2 by (rule conjI)
    show "r" using assms 3 by (rule mp)
  qed
qed

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

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

(*Solución M.Cumplido*)
proof -
{assume 1: "p & q"
 have 2: "p⟶ q" using 1 by (rule ejercicio_18)
 have r using assms(1) 2 by (rule mp)
}
thus  "p ∧ q ⟶ r" by (rule impI)
qed
 
lemma ejercicio_23_1:
  assumes "(p ⟶ q) ⟶ r" 
  shows   "p ∧ q ⟶ r"
(*L.E.Caraballo*)
proof (rule impI)
  assume 1: "p∧q"
  have 2: "q" using 1 by (rule conjunct2)
  have 3: "p⟶q" using 2 by (rule ejercicio_7)
  show "r" using assms 3 by (rule mp)
qed

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

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

(*Solución M.Cumplido*)
proof -

have 1: p using assms(1) by (rule conjunct1)
have 2: "q⟶r" using assms(1) by (rule conjunct2)
{assume 3: "p⟶q"
 have 4: q using 3 1 by (rule mp)
 have r using 2 4 by (rule mp)
}
thus "(p⟶q)⟶r" by (rule impI)
qed

lemma ejercicio_24_1:
  assumes "p ∧ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ r"
(*L.E.Caraballo*)
proof (rule impI)
  assume 1: "p⟶q"
  have 2: "p" using assms by (rule conjunct1)
  have 3: "q⟶r" using assms by (rule conjunct2)
  have 4: "q" using 1 2 ..
  show 5: "r" using 3 4 ..
qed

section {* Disyunciones *}

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

lemma ejercicio_25:
  assumes "p"
  shows   "p ∨ q"

(*Solución M.Cumplido*)
proof -
show "p | q" using assms(1) by (rule disjI1)
qed

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

lemma ejercicio_26:
  assumes "q"
  shows   "p ∨ q"

(*Solución M.Cumplido*)
proof -
show "p | q" using assms(1) by (rule disjI2)
qed



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

lemma ejercicio_27:
  assumes "p ∨ q"
  shows   "q ∨ p"


(*Solución M.Cumplido*)
using assms(1)
proof (rule disjE)

{assume 1:p
 show 2: "q | p" using 1 by (rule disjI2)}
next
{assume 3:q
 show 4: "q | p" using 3 by (rule disjI1)}
qed


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

lemma ejercicio_28:
  assumes "q ⟶ r" 
  shows   "p ∨ q ⟶ p ∨ r"

(*Solución M.Cumplido*)
proof -
{assume 1: "p | q"
 have 2:"p | r" using 1
  proof (rule disjE)
  {assume p 
   thus "p | r" by (rule disjI1)}
  next
  {assume 3: q
   have r using assms(1) 3 by (rule mp)
   thus "p | r" by (rule disjI2)}
  qed}
thus  "p ∨ q ⟶ p ∨ r" by (rule impI)
qed

lemma ejercicio_28_1:
  assumes "q ⟶ r" 
  shows   "p ∨ q ⟶ p ∨ r"
(*L.E.Caraballo*)
proof (rule impI)
  assume 1: "p∨q"
  show "p∨r"
  using 1
  proof (rule disjE)
    { assume "p"
      thus "p∨r" by (rule disjI1)}
    { assume 2: "q"
      have "r" using assms 2 by (rule mp)
      thus "p∨r" by (rule disjI2)}    
  qed
qed

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

lemma ejercicio_29:
  assumes "p ∨ p"
  shows   "p"

(*Solución M.Cumplido*)
using assms(1)
proof (rule disjE)
{assume p
 thus p by this}
qed

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

lemma ejercicio_30:
  assumes "p" 
  shows   "p ∨ p"

(*Solución M.Cumplido*)
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"

(*Solución M.Cumplido*)
using assms(1)
proof (rule disjE)
{assume p
 hence "p | q" by (rule disjI1)
 thus  "(p ∨ q) ∨ r" by (rule disjI1)}

next
{assume 1: "q | r"
 show  "(p ∨ q) ∨ r" using 1
   
    proof (rule disjE)
    {assume q
     hence "p | q" by (rule disjI2)
     thus "(p ∨ q) ∨ r" by (rule disjI1)}
    next
    {assume r
     thus "(p ∨ q) ∨ r" by (rule disjI2) }
    qed
}
qed

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

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

(*Solución M.Cumplido*)
using assms(1)
proof (rule disjE)
{assume r
 hence "q | r" by (rule disjI2)
 thus  "p ∨ (q ∨ r)" by (rule disjI2)}

next
{assume 1: "p | q"
 show  "p ∨ (q ∨ r)" using 1
   
    proof (rule disjE)
    {assume q
     hence "q | r" by (rule disjI1)
     thus "p ∨ (q ∨ r)" by (rule disjI2)}
    next
    {assume p
     thus "p ∨ (q ∨ r)" by (rule disjI1) }
    qed
}
qed


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

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

(*Solución M.Cumplido*)
proof -
have 1: p using assms(1) by (rule conjunct1)
have 2: "q | r" using assms(1) by (rule conjunct2)
show "(p ∧ q) ∨ (p ∧ r)" using 2
    proof (rule disjE)
    {assume 3: q
     have 4: "p & q" using 1 3 by (rule conjI) 
     thus  "(p ∧ q) ∨ (p ∧ r)" by (rule disjI1)}
    next
    {assume 5:r
     have 6: "p & r" using 1 5 by (rule conjI)
     thus  "(p ∧ q) ∨ (p ∧ r)" by (rule disjI2)}     
    qed  
qed

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

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

(*Solución M.Cumplido*)
using assms(1)
proof (rule disjE)
{assume 1:"p & q"
 hence 2: p by (rule conjunct1)
 have q using 1 by (rule conjunct2)
 hence 3:"q | r" by (rule disjI1)
 show  "p ∧ (q ∨ r)" using 2 3 by (rule conjI)}
next
{assume 4:"p & r"
 hence 5: p by (rule conjunct1)
 have r using 4 by (rule conjunct2)
 hence 6:"q | r" by (rule disjI2)
 show  "p ∧ (q ∨ r)" using 5 6 by (rule conjI)}
qed


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

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

(*Solución M.Cumplido*)
using assms(1)
proof (rule disjE)
{assume 1: p
 have 2: "p | q" using 1 by (rule disjI1)
 have 3: "p | r" using 1 by (rule disjI1)
 show  "(p ∨ q) ∧ (p ∨ r)" using 2 3 by (rule conjI) }
next
{assume 4: "q & r"
 hence 5: q by (rule conjunct1)
 have 6: r using 4 by (rule conjunct2)
 have 7: "p | q" using 5 by (rule disjI2)
 have 8: "p | r" using 6 by (rule disjI2)
 show  "(p ∨ q) ∧ (p ∨ r)" using 7 8 by (rule conjI)}
qed

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

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

(*Solución M.Cumplido*)
proof -
have 1: "p | q" using assms(1) by (rule conjunct1)
have 2: "p | r" using assms(1) by (rule conjunct2)
have  "p ∨ (q ∧ r)" using 1
    proof (rule disjE)
    {assume p
     thus  "p ∨ (q ∧ r)" by (rule disjI1)}
    next
    {assume 3: q
     show  "p ∨ (q ∧ r)" using 2
          proof (rule disjE)
          {assume p
           thus  "p ∨ (q ∧ r)" by (rule disjI1)}
          next
          {assume 4: r 
           have "q & r" using 3 4 by (rule conjI) 
           thus "p ∨ (q ∧ r)" by (rule disjI2)}
          qed
     }
qed



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

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

(*Solución M.Cumplido*)
proof -
have 1: "p ⟶ r" using assms(1) by (rule conjunct1)
have 2: "q ⟶ r" using assms(1) by (rule conjunct2)
{assume 3: "p | q"
 have r using 3
    proof (rule disjE)
    {assume 4: p
     show r using 1 4 by (rule mp)}
    next
    {assume 5: q
     show r using 2 5 by (rule mp) }
    qed
}
thus  "p ∨ q ⟶ r" by (rule impI)
qed

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

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

(*Solución M.Cumplido*)
proof -
{assume p 
 hence 1:"p | q" by (rule disjI1)
 have r using assms(1) 1 by (rule mp)}
hence 2: "p ⟶ r" by (rule impI)

{assume q
 hence 3:"p | q" by (rule disjI2)
 have r using assms(1) 3 by (rule mp)}
hence 4: "q ⟶ r" by (rule impI)

show  "(p ⟶ r) ∧ (q ⟶ r)" using 2 4 by (rule conjI)
qed


section {* Negaciones *}
 
text {* --------------------------------------------------------------- 
  Ejercicio 39. Demostrar
     p ⊢ ¬¬p
  ------------------------------------------------------------------ *}
 
lemma ejercicio_39:
  assumes "p"
  shows   "¬¬p"

(*Solución M.Cumplido*)
proof -
show  "¬¬p" using assms(1) by (rule notnotI)
qed
 
text {* --------------------------------------------------------------- 
  Ejercicio 40. Demostrar
     ¬p ⊢ p ⟶ q
  ------------------------------------------------------------------ *}
 
lemma ejercicio_40:

  assumes "¬p" 
  shows   "p ⟶ q"

(*Solución M.Cumplido*)
proof -
{assume 1: p
 have q using assms(1) 1 by (rule notE)}
thus "p ⟶ q" by (rule impI)
qed
 
text {* --------------------------------------------------------------- 
  Ejercicio 41. Demostrar
     p ⟶ q ⊢ ¬q ⟶ ¬p
  ------------------------------------------------------------------ *}
 
lemma ejercicio_41:
  assumes "p ⟶ q"
  shows   "¬q ⟶ ¬p"

(*Solución M.Cumplido*)
proof -
{assume 1: "~q"
 have "~p" using assms(1) 1 by (rule mt) }
thus  "¬q ⟶ ¬p" by (rule impI)
qed
 
text {* --------------------------------------------------------------- 
  Ejercicio 42. Demostrar
     p∨q, ¬q ⊢ p
  ------------------------------------------------------------------ *}
 
lemma ejercicio_42:
  assumes "p∨q"
          "¬q" 
  shows   "p"

(*Solución M.Cumplido*)
using assms(1)
proof (rule disjE)
{assume p
 thus p by this}
next
{assume 1:q
 show p using assms(2) 1 by (rule notE)}
qed 


text {* --------------------------------------------------------------- 
  Ejercicio 43. Demostrar
     p ∨ q, ¬p ⊢ q
  ------------------------------------------------------------------ *}
 
lemma ejercicio_43:
  assumes "p ∨ q"
          "¬p" 
  shows   "q"

(*Solución M.Cumplido*)
using assms(1)
proof (rule disjE)
{assume q
 thus q by this}
next
{assume 1:p
 show q using assms(2) 1 by (rule notE)}
qed 
 
text {* --------------------------------------------------------------- 
  Ejercicio 44. Demostrar
     p ∨ q ⊢ ¬(¬p ∧ ¬q)
  ------------------------------------------------------------------ *}
 
lemma ejercicio_44:
  assumes "p ∨ q" 
  shows   "¬(¬p ∧ ¬q)"

(*Solución M.Cumplido*)
proof (rule notI)
assume 1:"¬p ∧ ¬q" 
have 2: "~p" using 1 by (rule conjunct1)
have 3: "~q" using 1 by (rule conjunct2)
show False using assms(1)
    proof (rule disjE)
    {assume 4:p
     show False using 2 4 by (rule notE)}
    next
    {assume 5:q
     show False using 3 5 by (rule notE)}    
    qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 45. Demostrar
     p ∧ q ⊢ ¬(¬p ∨ ¬q)
  ------------------------------------------------------------------ *}
 
lemma ejercicio_45:
  assumes "p ∧ q" 
  shows   "¬(¬p ∨ ¬q)"

(*Solución M.Cumplido*)
proof (rule notI)
assume 1: "¬p ∨ ¬q"
show False using 1
    proof (rule disjE)
     {assume 2: "~p" 
      have 3: p using assms(1) by (rule conjunct1)
      show False using 2 3 by (rule notE)}
     next
     {assume 4: "~q" 
      have 5: q using assms(1) by (rule conjunct2)
      show False using 4 5 by (rule notE)}
     qed
qed

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

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

(*Solución M.Cumplido*)
proof -
have 1:"~~(~p & ~q)"
    proof (rule notI)
    assume 2: "~(~p & ~q)"
    have 3:"~p"
      proof (rule notI)
      assume p 
      hence 4:"p | q" by (rule disjI1)
      show False using assms(1) 4 by (rule notE)
      qed
    have 5:"~q"
      proof (rule notI)
      assume q 
      hence 6:"p | q" by (rule disjI2)
      show False using assms(1) 6 by (rule notE)
      qed
    have 7: "~p & ~q" using 3 5 by (rule conjI)
    show False using 2 7 by (rule notE)
    qed
show  "¬p ∧ ¬q" using 1 by (rule notnotD)
qed

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

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

(*Solución M.Cumplido*)

proof(rule notI)
assume "p | q"
thus False 
    proof(rule disjE) 
    {assume 1: p
     have 2:"~p" using assms(1) by (rule conjunct1) 
     show False using 2 1 by (rule notE)}
    next
    {assume 3: q
     have 4: "~q" using assms(1) by (rule conjunct2)
     show False using 4 3 by (rule notE)}
    qed
qed

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

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

(*Solución M.Cumplido*)

proof (rule notI)
assume 1: "p & q"
have 2: p using 1 by (rule conjunct1)
have 3: q using 1 by (rule conjunct2)
show False using assms(1)
    proof (rule disjE)
    {assume 4:"~p"
     show False using 4 2 by (rule notE) }
    next
    {assume 5:"~q"
     show False using 5 3 by (rule notE) }
    qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 49. Demostrar
     ⊢ ¬(p ∧ ¬p)
  ------------------------------------------------------------------ *}
 
lemma ejercicio_49:
  "¬(p ∧ ¬p)"

(*Solución M.Cumplido*)
proof (rule notI)
assume 1:"p & ~p"
hence 2: p by (rule conjunct1)
have 3: "~p" using 1 by (rule conjunct2)
show False using 3 2 by (rule notE) 
qed
 
text {* --------------------------------------------------------------- 
  Ejercicio 50. Demostrar
     p ∧ ¬p ⊢ q
  ------------------------------------------------------------------ *}
 
lemma ejercicio_50:
  assumes "p ∧ ¬p" 
  shows   "q"

(*Solución M.Cumplido*)
proof -
have 1: p using assms(1) by (rule conjunct1)
have 2: "~p" using assms(1) by (rule conjunct2)
show "q" using 2 1 by (rule notE)
qed
 
text {* --------------------------------------------------------------- 
  Ejercicio 51. Demostrar
     ¬¬p ⊢ p
  ------------------------------------------------------------------ *}
 
lemma ejercicio_51:
  assumes "¬¬p"
  shows   "p"

(*Solución M.Cumplido*)
proof -
show p using assms(1) by (rule notnotD)
qed
 

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

lemma ejercicio_52:
  "p ∨ ¬p"

(*Solución M.Cumplido*)
proof(rule ccontr)
assume 1:"~(p | ~ p)"
hence "~p & ~~p" by (rule ejercicio_46)
hence "~p" by (rule conjunct1)
hence 2:"p | ~p" by (rule disjI2)
show False using 1 2 by (rule notE)
qed    

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

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

(*Solución M.Cumplido*)
proof -
{assume 1:"(p ⟶ q) ⟶ p"
 have p 
    proof(rule ccontr)
    assume 2:"~p"
    {assume 3:p
     have q using 2 3 by (rule notE)}
    hence 4:"p⟶q" by (rule impI)
    have 5: p using 1 4 by (rule mp)
    show False using 2 5 by (rule notE)
    qed
 }
thus "((p ⟶ q) ⟶ p) ⟶ p" by (rule impI)
qed

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

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


(*Solución M.Cumplido*)

proof -
{assume 1: p
hence 2: "~~p" by (rule notnotI)
have 3: "~~q" using assms(1) 2 by (rule mt)
hence q by (rule notnotD)}
thus "p⟶q" by (rule impI)
qed  

text {* --------------------------------------------------------------- 
  Ejercicio 55. Demostrar
     ¬(¬p ∧ ¬q) ⊢ p ∨ q
  ------------------------------------------------------------------ *}
 
lemma ejercicio_55:
  assumes "¬(¬p ∧ ¬q)"
  shows   "p ∨ q"

(*Solución M.Cumplido*)
proof(rule ccontr)
assume "~(p | q)"
hence 1: "~p & ~q" by (rule ejercicio_46)
show False using assms(1) 1 by (rule notE)
qed
 
text {* --------------------------------------------------------------- 
  Ejercicio 56. Demostrar
     ¬(¬p ∨ ¬q) ⊢ p ∧ q
  ------------------------------------------------------------------ *}
 
lemma ejercicio_56:
  assumes "¬(¬p ∨ ¬q)" 
  shows   "p ∧ q"

  (*Solución M.Cumplido*)
proof -
have 1: "~~p & ~~q" using assms(1) by (rule ejercicio_46)
have 2: "~~p" using 1 by (rule conjunct1)
have 3: "~~q" using 1 by (rule conjunct2)
have 4: p using 2 by (rule notnotD)
have 5: q using 3 by (rule notnotD)
show "p & q" using 4 5 by (rule conjI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 57. Demostrar
     ¬(p ∧ q) ⊢ ¬p ∨ ¬q
  ------------------------------------------------------------------ *}
 
lemma ejercicio_57:
  assumes "¬(p ∧ q)"
  shows   "¬p ∨ ¬q"

    (*Solución M.Cumplido*)
proof -
{assume 1: "~(¬p ∨ ¬q)"
hence 2: "p & q" by (rule ejercicio_56)}
hence 3: "¬(¬p | ¬q)⟶ (p & q)" by (rule impI)
have 4:"¬¬(¬p | ¬q)" using 3 assms(1) by (rule mt)
thus  "¬p ∨ ¬q" by (rule notnotD)
qed

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


(*Solución M.Cumplido*)
proof -
have  "q | ¬q" by (rule ejercicio_52)
thus  "(p ⟶ q) ∨ (q ⟶ p)" 
    proof (rule disjE)
    {assume q
     hence "p⟶q" by (rule ejercicio_7)
     thus  "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI1)}
    next
    {assume "¬q"
     hence "¬p⟶¬q" by (rule ejercicio_7)  
     hence "q⟶p" by (rule ejercicio_54) 
     thus  "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI2)}
    qed    
qed


end