Sol 7

theory R7_sol
imports Main 
begin

text {*
  --------------------------------------------------------------------- 
  El objetivo de esta relación es escribir demostraciones usando sólo
  las reglas básicas de deducción natural de la lógica proposicional y
  los métodos rule, erule, frule, drule y assumption.

  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
  · conjE:          ⟦P ∧ Q; ⟦P; Q⟧ ⟹ R⟧ ⟹ R
  · notE:           ⟦¬P; P⟧ ⟹ R
  · notI:           (P ⟹ False) ⟹ ¬P
  · mp:             ⟦P ⟶ Q; P⟧ ⟹ Q 
  · mt:             ⟦F ⟶ G; ¬G⟧ ⟹ ¬F 
  · impI:           (P ⟹ Q) ⟹ P ⟶ Q
  · impE:           ⟦P ⟶ Q; P; Q ⟹ R⟧ ⟹ R
  · disjI1:         P ⟹ P ∨ Q
  · disjI2:         Q ⟹ P ∨ Q
  · disjE:          ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R 
  · FalseE:         False ⟹ P
  · iffI:           ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
  · iffD1:          ⟦Q = P; Q⟧ ⟹ P 
  · iffD2:          ⟦P = Q; Q⟧ ⟹ P
  · iffE:           ⟦P = Q; ⟦P ⟶ Q; Q ⟶ P⟧ ⟹ R⟧ ⟹ R
  · notnotD:        ¬¬ P ⟹ P
  · not_not:        P = ¬¬P
  · ccontr:         (¬P ⟹ False) ⟹ P
  · excluded_midle: ¬P ∨ P
  · classical:      (¬ P ⟹ P) ⟹ P
  · contrapos_nn    ⟦¬Q; P ⟹ Q⟧ ⟹ ¬P
  --------------------------------------------------------------------- 
*}

section {* Implicaciones *}

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

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

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

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

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

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

-- "La demostración detallada es"
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 ej5: "p ⟶ (q ⟶ r) ⟹ q ⟶ (p ⟶ r)"
  apply (rule impI)
  apply (rule impI)
  apply (erule impE, assumption)
  apply (erule impE, assumption+)
  done  
  
text {* --------------------------------------------------------------- 
  Ejercicio 6. Demostrar
     p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
  ------------------------------------------------------------------ *}

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

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

lemma ej7: "p ⟹ q ⟶ p"
  apply (rule impI)
  apply assumption
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 8. Demostrar
     ⊢ p ⟶ (q ⟶ p)
  ------------------------------------------------------------------ *}

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 ej9: "p ⟶ q ⟹ (q ⟶ r) ⟶ (p ⟶ r)"
  apply (rule impI)
  apply (rule impI)
  apply (erule impE, assumption)
  apply (erule impE, assumption+)
  done

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

lemma ej10: "p ⟶ (q ⟶ (r ⟶ s)) ⟹ r ⟶ (q ⟶ (p ⟶ s))"
  apply (rule impI)+
  apply (erule impE, assumption+)+
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 11. Demostrar
     ⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
  ------------------------------------------------------------------ *}

lemma ej11: "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
  apply (rule impI)+
  apply (erule impE, assumption+)+
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 12. Demostrar
     (p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
  ------------------------------------------------------------------ *}

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 ej13: "⟦p; q⟧ ⟹ p ∧ q"
  apply (rule conjI)
   apply assumption
  apply assumption
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 14. Demostrar
     p ∧ q ⊢ p
  ------------------------------------------------------------------ *}

lemma ej14: "p ∧ q ⟹ p"
  apply (erule conjunct1)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 15. Demostrar
     p ∧ q ⊢ q
  ------------------------------------------------------------------ *}

lemma ej15: "p ∧ q ⟹ q"
  apply (erule conjunct2)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 16. Demostrar
     p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
  ------------------------------------------------------------------ *}

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 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 ej18: "p ∧ q ⟹ p ⟶ q"
  apply (rule impI)
  apply (erule conjunct2)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 19. Demostrar
     (p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r   
  ------------------------------------------------------------------ *}

lemma ej19: "(p ⟶ q) ∧ (p ⟶ r) ⟹ p ⟶ q ∧ r"
  apply (rule impI)
  apply (rule conjI)
   apply (drule conjunct1)
   apply (erule impE)
    apply assumption
   apply assumption
  apply (drule conjunct2)
  apply (erule impE)
   apply assumption
  apply assumption
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 20. Demostrar
     p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
  ------------------------------------------------------------------ *}

lemma ej20: "p ⟶ q ∧ r ⟹ (p ⟶ q) ∧ (p ⟶ r)"
  apply (rule conjI)
   apply (rule impI)
   apply (erule impE)
    apply assumption
    apply (erule conjunct1)
  apply (rule impI)
  apply (erule impE)
   apply assumption
  apply (erule conjunct2)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 21. Demostrar
     p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r
  ------------------------------------------------------------------ *}

lemma ej21_1: "p ⟶ (q ⟶ r) ⟹ p ∧ q ⟶ r"
  apply (rule impI)
  apply (erule conjE)
  apply (erule impE)
   apply assumption
  apply (erule impE)
   apply assumption
  apply assumption
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 22. Demostrar
     p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)
  ------------------------------------------------------------------ *}

lemma ej22: "p ∧ q ⟶ r ⟹ p ⟶ (q ⟶ r)"
  apply (rule impI)
  apply (rule impI)
  apply (erule impE)
    apply (rule conjI)
    apply assumption+
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 23. Demostrar
     (p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
  ------------------------------------------------------------------ *}

lemma ej23: "(p ⟶ q) ⟶ r ⟹ p ∧ q ⟶ r"
  apply (rule impI)
  apply (erule impE)
   apply (rule impI)
   apply (erule conjunct2)
  apply assumption
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 24. Demostrar
     p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
  ------------------------------------------------------------------ *}

lemma ej24: "p ∧ (q ⟶ r) ⟹ (p ⟶ q) ⟶ r"
  apply (rule impI)
  apply (erule conjE)
  apply (erule impE)
   apply assumption
  apply (erule impE)
   apply assumption+
  done
    
section {* Disyunciones *}

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

lemma ej25: "p ⟹ p ∨ q"
  apply (erule disjI1)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 26. Demostrar
     q ⊢ p ∨ q
  ------------------------------------------------------------------ *}

lemma ej26: "q ⟹ p ∨ q"
  apply (erule disjI2)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 27. Demostrar
     p ∨ q ⊢ q ∨ p
  ------------------------------------------------------------------ *}

lemma ej27: "p ∨ q ⟹ q ∨ p"
  apply (erule disjE)
   apply (erule disjI2)
  apply (erule disjI1)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 28. Demostrar
     q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
  ------------------------------------------------------------------ *}

lemma ej28: "q ⟶ r ⟹ p ∨ q ⟶ p ∨ r"
  apply (rule impI)
  apply (erule disjE)
   apply (erule disjI1)
  apply (erule impE)
   apply assumption
  apply (erule disjI2)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 29. Demostrar
     p ∨ p ⊢ p
  ------------------------------------------------------------------ *}

lemma ej29: "p ∨ p ⟹ p"
  apply (erule disjE)
   apply assumption+
  done

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

lemma ej30: "p ⟹ p ∨ p"
  apply (erule disjI1)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 31. Demostrar
     p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r
  ------------------------------------------------------------------ *}

lemma ej31: "p ∨ (q ∨ r) ⟹ (p ∨ q) ∨ r"
  apply (erule disjE)
   apply (rule disjI1)
   apply (erule disjI1)
  apply (erule disjE)
   apply (rule disjI1)
   apply (erule disjI2)
  apply (erule disjI2)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 32. Demostrar
     (p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
  ------------------------------------------------------------------ *}

lemma ej32: "(p ∨ q) ∨ r ⟹ p ∨ (q ∨ r)"
  apply (erule disjE)
   apply (erule disjE)
    apply (erule disjI1)
   apply (rule disjI2)
   apply (erule disjI1)
  apply (rule disjI2)
  apply (erule disjI2)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 33. Demostrar
     p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
  ------------------------------------------------------------------ *}

lemma ej33: "p ∧ (q ∨ r) ⟹ (p ∧ q) ∨ (p ∧ r)"
  apply (erule conjE)
  apply (erule disjE)
   apply (rule disjI1)
   apply (rule conjI)
    apply assumption
   apply assumption
  apply (rule disjI2)
  apply (rule conjI)
   apply assumption
  apply assumption
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 34. Demostrar
     (p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
  ------------------------------------------------------------------ *}

lemma ej34: "(p ∧ q) ∨ (p ∧ r) ⟹ p ∧ (q ∨ r)"
  apply (rule conjI)
   apply (erule disjE)
    apply (erule conjunct1)
   apply (erule conjunct1)
  apply (erule disjE)
   apply (erule conjE)
   apply (rule disjI1)
   apply assumption
  apply (erule conjE)
  apply (erule disjI2)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 35. Demostrar
     p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
  ------------------------------------------------------------------ *}

lemma ej35: "p ∨ (q ∧ r) ⟹ (p ∨ q) ∧ (p ∨ r)"
  apply (erule disjE)
   apply (rule conjI)
    apply (erule disjI1)
   apply (erule disjI1)
  apply (erule conjE)
  apply (rule conjI)
   apply (erule disjI2)
  apply (erule disjI2)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 36. Demostrar
     (p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)
  ------------------------------------------------------------------ *}

lemma ej36: "(p ∨ q) ∧ (p ∨ r) ⟹ p ∨ (q ∧ r)"
  apply (erule conjE)
  apply (erule disjE)
   apply (erule disjI1)
  apply (erule disjE)
   apply (erule disjI1)
  apply (rule disjI2)
  apply (rule conjI)
   apply assumption+
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 37. Demostrar
     (p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
  ------------------------------------------------------------------ *}

lemma ej37: "(p ⟶ r) ∧ (q ⟶ r) ⟹ p ∨ q ⟶ r"
  apply (rule impI)
  apply (erule conjE)
  apply (erule disjE)
   apply (erule impE, assumption+)+
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 38. Demostrar
     p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
  ------------------------------------------------------------------ *}

lemma ej38: "p ∨ q ⟶ r ⟹ (p ⟶ r) ∧ (q ⟶ r)"
  apply (rule conjI)
   apply (rule impI)
   apply (erule impE)
    apply (erule disjI1)
   apply assumption
  apply (rule impI)
  apply (erule impE)
  apply (erule disjI2)
  apply assumption
  done
    
section {* Negación *}

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

lemma ej39: "p ⟹ ¬¬p"
  apply (rule notI)
  apply (erule notE)
  apply assumption
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 40. Demostrar
     ¬p ⊢ p ⟶ q
  ------------------------------------------------------------------ *}

lemma ej40: "¬p ⟹ p ⟶ q"
  apply (rule impI)
  apply (erule notE)
  apply assumption
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 41. Demostrar
     p ⟶ q ⊢ ¬q ⟶ ¬p
  ------------------------------------------------------------------ *}

lemma ej41: "p ⟶ q ⟹ ¬q ⟶ ¬p"
  apply (rule impI)
  apply (rule notI)
  apply (erule impE)
   apply assumption
  apply (erule notE)
  apply assumption
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 42. Demostrar
     p ∨ q, ¬q ⊢ p
  ------------------------------------------------------------------ *}

lemma ej42: "⟦p ∨ q; ¬q⟧ ⟹ p"
  apply (erule disjE)
   apply assumption
  apply (erule notE)
  apply assumption
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 43. Demostrar
     p ∨ q, ¬p ⊢ q
  ------------------------------------------------------------------ *}

lemma ej43: "⟦p ∨ q; ¬p⟧ ⟹ q"
  apply (erule disjE)
   apply (erule notE)
   apply assumption
  apply assumption
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 44. Demostrar
     p ∨ q ⊢ ¬(¬p ∧ ¬q)
  ------------------------------------------------------------------ *}

lemma ej44: "p ∨ q ⟹ ¬(¬p ∧ ¬q)"
  apply (rule notI)
  apply (erule conjE)
  apply (erule disjE)
   apply (erule notE, assumption)+
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 45. Demostrar
     p ∧ q ⊢ ¬(¬p ∨ ¬q)
  ------------------------------------------------------------------ *}

lemma ej45: "p ∧ q ⟹ ¬(¬p ∨ ¬q)"
  apply (rule notI)
  apply (erule conjE)
  apply (erule disjE)
   apply (erule notE, assumption)+
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 46. Demostrar
     ¬(p ∨ q) ⊢ ¬p ∧ ¬q
  ------------------------------------------------------------------ *}

lemma ej46: "¬(p ∨ q) ⟹ ¬p ∧ ¬q"
  apply (rule conjI)
   apply (rule notI)
   apply (erule notE)
   apply (erule disjI1)
  apply (rule notI)
  apply (erule notE)
  apply (erule disjI2)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 47. Demostrar
     ¬p ∧ ¬q ⊢ ¬(p ∨ q)
  ------------------------------------------------------------------ *}

lemma ej47: "¬p ∧ ¬q ⟹ ¬(p ∨ q)"
  apply (rule notI)
  apply (erule conjE)
  apply (erule disjE)
   apply (erule notE, assumption)+
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 48. Demostrar
     ¬p ∨ ¬q ⊢ ¬(p ∧ q)
  ------------------------------------------------------------------ *}

lemma ej48: "¬p ∨ ¬q ⟹ ¬(p ∧ q)"
  apply (rule notI)
  apply (erule conjE)
  apply (erule disjE)
   apply (erule notE, assumption)+
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 49. Demostrar
     ⊢ ¬(p ∧ ¬p)
  ------------------------------------------------------------------ *}

lemma ej49: "¬(p ∧ ¬p)"
  apply (rule notI)
  apply (erule conjE)
  apply (erule notE)
  apply assumption
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 50. Demostrar
     p ∧ ¬p ⊢ q
  ------------------------------------------------------------------ *}

lemma ej50: "p ∧ ¬p ⟹ q"
  apply (erule conjE)
  apply (erule notE)
  apply assumption
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 51. Demostrar
     ¬¬p ⊢ p
  ------------------------------------------------------------------ *}

lemma ej51: "¬¬p ⟹ p"
  apply (erule notnotD)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 52. Demostrar
     ⊢ p ∨ ¬p
  ------------------------------------------------------------------ *}

lemma ej52: "p ∨ ¬p"
  apply (cut_tac P="¬p" in excluded_middle)
  apply (erule disjE)
  apply (rule disjI1)
   apply (erule notnotD)
  apply (erule disjI2)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 53. Demostrar
     ⊢ ((p ⟶ q) ⟶ p) ⟶ p
  ------------------------------------------------------------------ *}

lemma ej53: "((p ⟶ q) ⟶ p) ⟶ p"
  apply (rule impI)
  apply (rule ccontr)
  apply (cut_tac P="p ⟶ q" in excluded_middle)
  apply (erule disjE)
   apply (erule_tac P="p ⟶ q" in notE)
   apply (rule impI)
   apply (erule notE)
   apply assumption
  apply (erule impE)
   apply assumption
  apply (erule notE)
  apply assumption
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 54. Demostrar
     ¬q ⟶ ¬p ⊢ p ⟶ q
  ------------------------------------------------------------------ *}

lemma ej54: "¬q ⟶ ¬p ⟹ p ⟶ q"
  apply (rule impI)
  apply (rule ccontr)
  apply (erule impE)
   apply assumption
  apply (erule notE)+
  apply assumption
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 55. Demostrar
     ¬(¬p ∧ ¬q) ⊢ p ∨ q
  ------------------------------------------------------------------ *}

lemma ej55: "¬(¬p ∧ ¬q) ⟹ p ∨ q"
  apply (cut_tac P=p in excluded_middle)
  apply (erule disjE)
    apply (cut_tac P=q in excluded_middle)
   apply (erule disjE)
    apply (erule notE)
    apply (rule conjI)
     apply assumption+
   apply (erule disjI2)
  apply (erule disjI1)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 56. Demostrar
     ¬(¬p ∨ ¬q) ⊢ p ∧ q
  ------------------------------------------------------------------ *}

lemma ej56: "¬(¬p ∨ ¬q) ⟹ p ∧ q"
  apply (rule conjI)
   apply (rule ccontr)
   apply (erule notE)
   apply (erule disjI1)
  apply (rule ccontr)
  apply (erule notE)
  apply (erule disjI2)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 57. Demostrar
     ¬(p ∧ q) ⊢ ¬p ∨ ¬q
  ------------------------------------------------------------------ *}

lemma ej57: "¬(p ∧ q) ⟹ ¬p ∨ ¬q"
  apply (cut_tac P=p in excluded_middle)
  apply (erule disjE)
   apply (erule disjI1)
  apply (cut_tac P=q in excluded_middle)
  apply (erule disjE)
   apply (erule disjI2)
  apply (erule notE)
  apply (rule conjI)
   apply assumption+
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 58. Demostrar
     ⊢ (p ⟶ q) ∨ (q ⟶ p)
  ------------------------------------------------------------------ *}

lemma ej58: "(p ⟶ q) ∨ (q ⟶ p)"
  apply (cut_tac P=p in excluded_middle)
  apply (erule disjE)
   apply (rule disjI1)
  apply (rule impI)
  apply (erule notE)
   apply assumption
  apply (rule disjI2)
  apply (rule impI)
  apply assumption
  done

end