Ver el código de «Rel 3»

<source lang = "isabelle">
chapter ‹ R3: Deducción natural proposicional(II) ›

theory R3_sol
imports Main 
begin

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

  Para cada ejercicio dar una demostración estructurada y otra
  aplicativa.

  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 ‹ Disyunciones ›

text ‹ --------------------------------------------------------------- 
  Ejercicio 25. Demostrar
     p ⊢ p ∨ q
  ------------------------------------------------------------------ ›
lemma ejercicio_25:
  assumes "p"
  shows   "p ∨ q"
proof -
show "p∨q" using assms by (rule disjI1)
qed

lemma ej25: "p ⟹ p ∨ q"
  apply (erule disjI1)
  done
    
text ‹ --------------------------------------------------------------- 
  Ejercicio 26. Demostrar
     q ⊢ p ∨ q
  ------------------------------------------------------------------ ›
lemma ejercicio_26:
  assumes "q"
  shows   "p ∨ q"
proof -
show "p∨q" using assms by (rule disjI2)
qed

lemma ej26: "q ⟹ p ∨ q"
  apply (erule disjI2)
  done

text ‹ --------------------------------------------------------------- 
  Ejercicio 27. Demostrar
     p ∨ q ⊢ q ∨ p
  ------------------------------------------------------------------ ›
lemma ejercicio_27a:
  assumes "p ∨ q"
  shows   "q ∨ p"
proof - 
have "p ∨ q" using assms by this
  moreover
  { assume 2: "p"
    have "q ∨ p" using 2 by (rule disjI2) }
  moreover
  { assume 3: "q"
    have "q ∨ p" using 3 by (rule disjI1) }
  ultimately show "q ∨ p" by (rule disjE) 
qed  

lemma ejercicio_27b:
  assumes "p ∨ q"
  shows   "q ∨ p"
proof - 
  note `p ∨ q`
  moreover
  { assume "p"
    then have "q ∨ p" ..}
  moreover
  { assume "q"
    then have "q ∨ p" .. }
  ultimately show "q ∨ p" .. 
qed  


lemma ejercicio_27c:
  assumes "p ∨ q"
  shows   "q ∨ p"
  using assms
proof (rule disjE)
  assume "p"
  then show "q ∨ p" ..
next
  assume "q"
  then show "q ∨ p" ..
qed

lemma ejercicio_27d:
  assumes "p ∨ q"
  shows   "q ∨ p"
  using assms by auto

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 ejercicio_28b:
  assumes "q ⟶ r" 
  shows   "p ∨ q ⟶ p ∨ r"
proof (rule impI)
  assume "p ∨ q"
  show "p ∨ r"
    using `p ∨ q`
    proof (rule disjE)
      assume "p"
      then show "p ∨ r" ..
      next
      assume "q"
      with assms(1) have "r" ..
      then show "p ∨ r" ..
    qed
qed

lemma ejercicio_28c:
  assumes "q ⟶ r" 
  shows   "p ∨ q ⟶ p ∨ r"
  using assms by auto

lemma ej28: "q ⟶ r ⟹ p ∨ q ⟶ p ∨ r"
  apply (rule impI)
  apply (erule disjE)
   apply (erule disjI1)
  apply (drule mp)
   apply assumption
  apply (erule disjI2)
  done

text ‹ --------------------------------------------------------------- 
  Ejercicio 29. Demostrar
     p ∨ p ⊢ p
  ------------------------------------------------------------------ ›

lemma ejercicio_29b:
  assumes "p ∨ p"
  shows   "p"
  using assms
proof (rule disjE)
  assume "p"
  then show "p" .
next
  assume "p"
  then show "p" .
qed

lemma ejercicio_29c:
  assumes "p ∨ p"
  shows   "p"
  using assms by auto

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

text ‹ --------------------------------------------------------------- 
  Ejercicio 30. Demostrar
     p ⊢ p ∨ p
  ------------------------------------------------------------------ ›

lemma ejercicio_30a:
  assumes "p" 
  shows   "p ∨ p"
  using assms
proof (rule disjI1)
qed

lemma ejercicio_30b:
  assumes "p" 
  shows   "p ∨ p"
  using assms by auto

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

lemma ejercicio_31a:
  assumes "p ∨ (q ∨ r)" 
  shows   "(p ∨ q) ∨ r"
  using assms
proof (rule disjE)
  assume "p"
  then have "p ∨ q" by (rule disjI1)
  then show "(p ∨ q) ∨ r" by (rule disjI1)
next
  assume "q ∨ r" 
  then show "(p ∨ q) ∨ r"
    proof (rule disjE)
      assume "q"
      then have "p ∨ q" by (rule disjI2)
      then show "(p ∨ q) ∨ r" by (rule disjI1)
  next
    assume "r"
    then show "(p ∨ q) ∨ r" by (rule disjI2)
  qed
qed

lemma ejercicio_31b:
  assumes "p ∨ (q ∨ r)" 
  shows   "(p ∨ q) ∨ r"
  using assms by auto

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 ejercicio_32:
  assumes "(p ∨ q) ∨ r" 
  shows   "p ∨ (q ∨ r)"
oops

lemma ejercicio_32b:
  assumes "(p ∨ q) ∨ r" 
  shows   "p ∨ (q ∨ r)"
  using ‹(p ∨ q) ∨ r›
proof (rule disjE)
  assume "p ∨ q" 
  then show "p ∨ (q ∨ r)"
  proof (rule disjE)
    assume "p" 
    then show "p ∨ (q ∨ r)" by (rule disjI1)
  next
    assume "q" 
    then have "q ∨ r" by (rule disjI1)
    then show "p ∨ (q ∨ r)" by (rule disjI2)
  qed
next
  assume "r" 
  then have "q ∨ r" by (rule disjI2)
  then show "p ∨ (q ∨ r)" by (rule disjI2)
qed

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 ejercicio_33:
  assumes "p ∧ (q ∨ r)" 
  shows   "(p ∧ q) ∨ (p ∧ r)"
oops

lemma ejercicio_33b:
  assumes "p ∧ (q ∨ r)" 
  shows   "(p ∧ q) ∨ (p ∧ r)"
proof-
  have "p" using ‹p ∧ (q ∨ r)› by (rule conjunct1)
  show "(p ∧ q) ∨ (p ∧ r)"
  proof (rule disjE)
    assume "q" 
    have "p ∧ q" using ‹p› ‹q› by (rule conjI)
    then show "(p ∧ q) ∨ (p ∧ r)" by (rule disjI1)
  next
    assume "r" 
    have "p ∧ r" using ‹p› ‹r› by (rule conjI)
    then show "(p ∧ q) ∨ (p ∧ r)" by (rule disjI2)
  next
    show "q ∨ r" using ‹p ∧ (q ∨ r)› by (rule conjunct2)
  qed
qed


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 ejercicio_34a:
  assumes "(p ∧ q) ∨ (p ∧ r)" 
  shows   "p ∧ (q ∨ r)"
  using assms
proof 
  assume "p∧q"
  show "p ∧ (q ∨ r)"
    proof (rule conjI)
      show "p" using `p∧q` ..
    next
      have "q" using `p∧q` ..
      then show "q∨r" by (rule disjI1)
    qed
  next
  assume "p∧r"
  show "p ∧ (q ∨ r)"
    proof (rule conjI)
      show "p" using `p∧r` ..
    next
      have "r" using `p∧r` ..
      then show "q∨r" by (rule disjI2)
    qed
qed

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

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 ejercicio_35:
  assumes "p ∨ (q ∧ r)" 
  shows   "(p ∨ q) ∧ (p ∨ r)"
oops

lemma ejercicio_35b:
  assumes "p ∨ (q ∧ r)" 
  shows   "(p ∨ q) ∧ (p ∨ r)"
  using ‹p ∨ (q ∧ r)› 
proof (rule disjE)
  assume "p" 
  then have "p ∨ r" by (rule disjI1)
  have "p ∨ q" using ‹p› by (rule disjI1)
  then show "(p ∨ q) ∧ (p ∨ r)" using ‹p ∨ r› by (rule conjI)
next
  assume "q ∧ r"
  then have "r" by (rule conjunct2)
  then have "p ∨ r" by (rule disjI2)
  have "q" using ‹q ∧ r› by (rule conjunct1)
  then have "p ∨ q" by (rule disjI2)
  then show "(p ∨ q) ∧ (p ∨ r)" using ‹p ∨ r› by (rule conjI)
qed

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 ejercicio_36a:
  assumes "(p ∨ q) ∧ (p ∨ r)"
  shows   "p ∨ (q ∧ r)"
proof -
  have "p ∨ q" using assms ..
  then show "p ∨ (q ∧ r)"
  proof
    assume "p"
    then show "p ∨ (q ∧ r)" by (rule disjI1)
  next 
    assume "q"
      have "p ∨ r" using assms ..
      then show "p ∨ (q ∧ r)"
      proof
        assume "p"
        then show "p ∨ (q∧r)" by (rule disjI1)
      next
        assume "r"
        with `q` have "q ∧ r" ..
        then show "p ∨ (q ∧ r)" by (rule disjI2)
      qed
    qed
qed

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

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 ejercicio_37:
  assumes "(p ⟶ r) ∧ (q ⟶ r)" 
  shows   "p ∨ q ⟶ r"
proof (rule impI)
  assume "p ∨ q"
  then show "r"
    proof
      assume "p"
      have "p ⟶ r" using assms by (rule conjunct1)
      then show "r" using `p` ..
    next
      assume "q"
      have "q ⟶ r" using assms by (rule conjunct2)
      then show "r" using `q` ..
    qed
qed

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

lemma ej37: "(p ⟶ r) ∧ (q ⟶ r) ⟹ p ∨ q ⟶ r"
  apply (rule impI)
  apply (erule conjE)
  apply (erule disjE)
   apply (drule mp, assumption+)+
  done
    
text ‹ --------------------------------------------------------------- 
  Ejercicio 38. Demostrar
     p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
  ------------------------------------------------------------------ ›

lemma ejercicio_38a:
  assumes "p ∨ q ⟶ r" 
  shows   "(p ⟶ r) ∧ (q ⟶ r)"
  proof (rule conjI)
    show "p ⟶ r"
      proof (rule impI)
        assume "p"
        then have "p ∨ q" ..
        with assms show "r" by (rule mp)
      qed
  next
    show "q ⟶ r"
      proof (rule impI)
        assume "q"
        then have "p ∨ q" ..
        with assms show "r" by (rule mp)
      qed
    qed

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

lemma ej38: "p ∨ q ⟶ r ⟹ (p ⟶ r) ∧ (q ⟶ r)"
  apply (rule conjI)
   apply (rule impI)
   apply (drule mp)
    apply (erule disjI1)
   apply assumption
  apply (rule impI)
  apply (drule mp)
  apply (erule disjI2)
  apply assumption
  done

section ‹ Negaciones ›
text ‹ --------------------------------------------------------------- 
  Ejercicio 39. Demostrar
     p ⊢ ¬¬p
  ------------------------------------------------------------------ ›
lemma ejercicio_39:
  assumes "p"
  shows   "¬¬p"
proof -
show "¬¬p" using assms by (rule notnotI)
qed

lemma ej39: "p ⟹ ¬¬p"
  apply (rule notI)
  apply (erule notE)
  apply assumption
  done

text ‹ --------------------------------------------------------------- 
  Ejercicio 40. Demostrar
     ¬p ⊢ p ⟶ q
  ------------------------------------------------------------------ ›

lemma ejercicio_40a:
  assumes "¬p" 
  shows   "p ⟶ q"
proof
  assume "p"
  with assms show "q" by (rule notE)
qed

lemma ejercicio_40b:
  assumes "¬p" 
  shows   "p ⟶ q"
  using assms by auto

lemma ej40: "¬p ⟹ p ⟶ q"
  apply (rule impI)
  apply (erule notE)
  apply assumption
  done

text ‹ --------------------------------------------------------------- 
  Ejercicio 41. Demostrar
     p ⟶ q ⊢ ¬q ⟶ ¬p
  ------------------------------------------------------------------ ›

lemma ejercicio_41:
  assumes "p ⟶ q"
  shows   "¬q ⟶ ¬p"
proof
  assume "¬q"
  with assms show "¬p" by (rule mt)
qed

lemma ejercicio_41b:
  assumes "p ⟶ q"
  shows   "¬q ⟶ ¬p"
  using assms by auto


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 ejercicio_42a:
  assumes "p∨q"
          "¬q" 
  shows   "p"
  using assms(1)
  proof 
    assume "p" then show "p" .
  next
    assume "q" 
    with assms(2) show "p" by (rule notE)
  qed

lemma ejercicio_42b:
  assumes "p∨q"
          "¬q" 
  shows   "p"
  using assms by auto

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 ejercicio_43a:
  assumes "p ∨ q"
          "¬p" 
  shows   "q"
  using assms(1)
  proof
    assume "p"
    with assms(2) show "q" by (rule notE)
  next
    assume "q" then show q .
  qed


lemma ejercicio_43b:
  assumes "p ∨ q"
          "¬p" 
  shows   "q"
  using assms by auto

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 ejercicio_44a:
  assumes "p ∨ q" 
  shows   "¬(¬p ∧ ¬q)"
  using assms
  proof 
    assume "p"
    show "¬(¬p ∧ ¬q)"
      proof (rule notI)
        assume "¬p ∧ ¬q"
        then have "¬p" by (rule conjunct1)
        then show False using `p` by (rule notE)
      qed
  next
    assume "q"
    show "¬(¬p ∧ ¬q)"
      proof (rule notI)
        assume "¬p ∧ ¬q"
        then have "¬q" by (rule conjunct2)
        then show False using `q` by (rule notE)
      qed
  qed


lemma ejercicio_44b:
  assumes "p ∨ q" 
  shows   "¬(¬p ∧ ¬q)"
  proof (rule notI)
    assume "¬p ∧ ¬q"
    show False using assms 
      proof (rule disjE)
        assume "p"
        have "¬p" using `¬p ∧ ¬q` by (rule conjunct1)
        then show False using `p` by (rule notE)
      next
        assume "q"
        have "¬q" using `¬p ∧ ¬q` by (rule conjunct2)
        then show False using `q` by (rule notE)
      qed
  qed

lemma ejercicio_44c:
  assumes "p ∨ q" 
  shows   "¬(¬p ∧ ¬q)"
  using assms by auto

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 ejercicio_45a:
  assumes "p ∧ q" 
  shows   "¬(¬p ∨ ¬q)"
  proof
    assume "¬p ∨ ¬q"
    then show False
      proof (rule disjE)
        assume "¬p"
        have "p" using assms ..
        with `¬ p` show False ..
      next
        assume "¬q"
        have "q" using assms by (rule conjunct2)
        with `¬ q` show False by (rule notE)
      qed
  qed


lemma ejercicio_45c:
  assumes "p ∧ q" 
  shows   "¬(¬p ∨ ¬q)"
  using assms by auto

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 ejercicio_46a:
  assumes "¬(p ∨ q)" 
  shows   "¬p ∧ ¬q"
  proof
    show "¬p"
    proof
      assume "p"
      then have "p ∨ q" by (rule disjI1)
      with assms show False by (rule notE)
    qed
  next
    show "¬q"
    proof
      assume "q"
      then have "p ∨ q" ..
      with assms show False ..
    qed
  qed

lemma ejercicio_46c:
  assumes "¬(p ∨ q)" 
  shows   "¬p ∧ ¬q"
  using assms by auto

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 ejercicio_47a:
  assumes "¬p ∧ ¬q" 
  shows   "¬(p ∨ q)"
  proof
    assume "p ∨ q"
    then show False
      proof
        assume "p"
        have "¬p" using assms by (rule conjunct1)
        then show False using `p` by (rule notE)
      next
        assume "q"
        have "¬q" using assms by (rule conjunct2)
        then show False using `q` by (rule notE)
      qed
    qed


lemma ejercicio_47c:
  assumes "¬p ∧ ¬q" 
  shows   "¬(p ∨ q)"
  using assms by auto

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 ejercicio_48a:
  assumes "¬p ∨ ¬q"
  shows   "¬(p ∧ q)"
  using assms
  proof
    assume "¬p"
    show "¬(p ∧ q)"
      proof
        assume "p ∧ q"
        then have "p" by (rule conjunct1)
        with `¬p` show False by (rule notE)
      qed
  next
    assume "¬q"
    show "¬(p ∧ q)"
      proof
        assume "p ∧ q"
        then have "q" ..
        with `¬q` show False ..
      qed
  qed


lemma ejercicio_48b:
  assumes "¬p ∨ ¬q"
  shows   "¬(p ∧ q)"
proof
  assume "p ∧ q"
  show False
  using assms
  proof
    assume "¬p"
    have "p" using `p ∧ q` ..
    with `¬p` show False ..
  next
    assume "¬q"
    have "q" using `p ∧ q` ..
    with `¬q` show False ..
  qed
qed

lemma ejercicio_48c:
  assumes "¬p ∨ ¬q"
  shows   "¬(p ∧ q)"
  using assms by auto

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 ejercicio_49a:
  "¬(p ∧ ¬p)"
proof
  assume "p ∧ ¬p"
  then have "p" ..
  have "¬ p" using `p ∧ ¬p` ..
  then show False using `p` ..
qed

lemma ejercicio_49b:
  "¬(p ∧ ¬p)"
  by auto

lemma ej49: "¬(p ∧ ¬p)"
  apply (rule notI)
  apply (erule conjE)
  apply (erule notE)
  apply assumption
  done

text ‹ --------------------------------------------------------------- 
  Ejercicio 50. Demostrar
     p ∧ ¬p ⊢ q
  ------------------------------------------------------------------ ›

lemma ejercicio_50:
  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 ejercicio_50b:
  assumes "p ∧ ¬p" 
  shows   "q"
proof (rule notE)
  show "p" using ‹p ∧ ¬p› by (rule conjunct1)
  show "¬p" using ‹p ∧ ¬p› by (rule conjunct2)
qed

lemma ej50: "p ∧ ¬p ⟹ q"
  apply (erule conjE)
  apply (erule notE)
  apply assumption
  done

text ‹ --------------------------------------------------------------- 
  Ejercicio 51. Demostrar
     ¬¬p ⊢ p
  ------------------------------------------------------------------ ›

lemma ejercicio_51a:
  assumes "¬¬p"
  shows   "p"
  using assms by (rule notnotD)

lemma ejercicio_51b:
  assumes "¬¬p"
  shows   "p"
  using assms by auto

lemma ej51: "¬¬p ⟹ p"
  apply (erule notnotD)
  done

text ‹ --------------------------------------------------------------- 
  Ejercicio 52. Demostrar
     ⊢ p ∨ ¬p
  ------------------------------------------------------------------ ›

lemma ejercicio_52a:
  "p ∨ ¬p"
proof -
  have "¬¬p ∨ ¬p" ..
  then show "p ∨ ¬p" by simp
qed

lemma ejercicio_52b:
  "p ∨ ¬p"
proof -
  have "¬p ∨ p" ..
  then show "p ∨ ¬p" by (rule ejercicio_27a)
qed


lemma ejercicio_52c:
  "p ∨ ¬p"
  by auto

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 ejercicio_53b:
  "((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` ..
    qed
qed


lemma ejercicio_53a:
  "((p ⟶ q) ⟶ p) ⟶ p"
proof (rule impI)
  assume "(p ⟶ q) ⟶ p"
  have "¬p ∨ p" by (rule excluded_middle)
  then show "p"
  proof (rule disjE)
    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 "p" using `¬(p⟶ q)` `p⟶ q` by (rule notE)
  next
    assume "p"
     then show "p" .
 qed
qed



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

lemma ej53: "((p ⟶ q) ⟶ p) ⟶ p"
  apply (rule impI)
  apply (rule ccontr)
  (*   apply (case_tac "p ⟶ q") *)
  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 ejercicio_54:
  assumes "¬q ⟶ ¬p"
  shows   "p ⟶ q"
proof
  assume "p"
  then have "¬¬p" by (rule notnotI)
  with assms have "¬¬q" by (rule mt)
  then show "q" by (rule notnotD)
qed

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 ejercicio_55a:
  assumes "¬(¬p ∧ ¬q)"
  shows   "p ∨ q"
proof -
  have "¬p ∨ p" ..
  then show "p∨q"
    proof
      assume "¬p"
      have "¬q ∨ q" ..
      then show "p∨q"
      proof
        assume "¬q"
        with `¬p` have "¬p ∧ ¬q" by (rule conjI)
        with assms show "p∨q" by (rule notE)
      next
        assume "q"
        then show "p ∨ q" ..
      qed
    next
      assume "p"
      then show "p ∨q" ..
    qed
qed

lemma ejercicio_55c:
  assumes "¬(¬p ∧ ¬q)"
  shows   "p ∨ q"
  using assms by auto

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 ejercicio_56a:
  assumes "¬(¬p ∨ ¬q)" 
  shows   "p ∧ q"
  proof
    show "p"
    proof -
      have "¬p ∨ p" ..
      then show "p"
      proof
        assume "¬p"
        then have "¬p ∨ ¬q" by (rule disjI1)
        with `¬(¬p ∨ ¬q)` show "p" by (rule notE)
      next
        assume "p" then show "p" .
      qed
    qed
  next
    show "q"
   proof -
      have "¬q ∨ q" ..
      then show "q"
      proof
        assume "¬q"
        then have "¬p ∨ ¬q" by (rule disjI2)
        with `¬(¬p ∨ ¬q)` show "q" by (rule notE)
      next
        assume "q" then show "q" .
      qed
    qed
  qed


lemma ejercicio_56c:
  assumes "¬(¬p ∨ ¬q)" 
  shows   "p ∧ q"
  using assms by auto

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 ejercicio_57a:
  assumes "¬(p ∧ q)"
  shows   "¬p ∨ ¬q"
proof -
  have "¬p ∨p" ..
  then show "¬p ∨ ¬q"
  proof 
    assume "¬p"
    then show "¬p ∨ ¬q" ..
  next
    assume "p"
      have "¬q ∨ q" ..
      then show "¬p ∨ ¬q"
      proof
        assume "¬q"
        then show "¬p ∨ ¬q" ..
      next
        assume "q"
        with `p` have "p∧q" by (rule conjI)
        with assms show "¬p ∨ ¬q" by (rule notE)
      qed
  qed
qed

lemma ejercicio_57c:
  assumes "¬(p ∧ q)"
  shows   "¬p ∨ ¬q"
  using assms by auto

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

lemma ej57_b:
   "⟦¬(p ∧ q)⟧ ⟹ ¬p ∨ ¬q"
  apply (rule ccontr)
  apply (erule notE)
  apply (rule conjI)
   apply (rule ccontr)
   apply (erule notE)
  apply (rule disjI1)
   apply assumption
  apply (rule ccontr)
  apply (erule notE)
  apply (rule disjI2)
  apply assumption
  done

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

lemma ejercicio_58a:
  "(p ⟶ q) ∨ (q ⟶ p)"
proof -
  have "¬p ∨ p" by (rule excluded_middle)
  then show "(p ⟶ q) ∨ (q ⟶ p)"
  proof 
    assume "¬p"
    show "(p ⟶ q) ∨ (q ⟶ p)"
      proof (rule disjI1)
        show "p ⟶ q"
          proof
            assume "p"
            with `¬ p` show "q" 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` .
        qed
      qed
  qed
qed


lemma ejercicio_58b:
  "(p ⟶ q) ∨ (q ⟶ p)"
proof -
  have "¬p ∨ p" .. (* by (rule excluded_middle) *)
  then show "(p ⟶ q) ∨ (q ⟶ p)"
  proof
    assume "¬p"
    show "(p ⟶ q) ∨ (q ⟶ p)"
      proof (rule disjI1)
        show "p ⟶ q"
          proof
            assume "p"
            with `¬ p` show "q" .. (* 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` .
        qed
      qed
  qed
qed


lemma ejercicio_58c:
  "(p ⟶ q) ∨ (q ⟶ p)"
  by auto

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


</source>