Relación 3

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

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

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

-- "Isabel Duarte"
lemma ejercicio_1b:
  assumes "p ⟶ q"
          "p"
  shows "q"
proof -
  show "q" using assms(1,2) by (rule mp)
qed
 
-- "Pedro G. Ros"
lemma ejercicio_1c:
  assumes 1: "p ⟶ q" and
          2: "p"
  shows "q"
using assms ..


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

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

-- "Isabel Duarte"
lemma ejercicio_2b:
  assumes "p ⟶ q"
          "q ⟶ r"
          "p" 
  shows "r"
proof -
  have "q" using assms(1,3) ..
  with `q ⟶ r` show "r" ..
qed

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

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

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


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


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

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

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

-- "José Mª Contreras"
lemma ejercicio_6a:
  assumes 1: "p ⟶ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ (p ⟶ r)"
proof -
 {assume 2: "p ⟶ q"
   {assume 3: "p"
    have 4: "q ⟶ r" using 1 3 ..
    have 5: "q" using 2 3 ..
    have "r"  using 4 5 ..}
   hence "p ⟶ r" by (rule impI)}
 thus "(p ⟶ q) ⟶ (p ⟶ r)" by (rule impI)
qed 

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

-- "Pedro G. Ros Reina"
lemma ejercicio_7:
  assumes "p"  
  shows   "q ⟶ p"
proof -
 {assume 1: "q"}
   show "q⟶ p" using assms(1) by (rule impI)
qed

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

-- "Pedro G. Ros"
lemma ejercicio_8:
  "p ⟶ (q ⟶ p)"
proof -
 {assume 1: "p"
   hence 2: "q ⟶ p" by (rule impI)}
 thus "p ⟶q⟶p" by (rule impI)
qed

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


-- "Carmen Martinez Navarro, Erlinda Menendez Perez" 


lemma ejercicio_9:
  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 "(q ⟶ r) ⟶ (p ⟶ r)" by (rule impI)
qed


text {* --------------------------------------------------------------- 
  Ejercicio 10. Demostrar
     p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
  ------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_10:
  assumes "p ⟶ (q ⟶ (r ⟶ s))" 
  shows   "r ⟶ (q ⟶ (p ⟶ s))"
proof 
  assume "r"
  show  "q⟶ (p⟶ s)" 
  proof 
    assume "q"
    show "p⟶ s"
    proof
      assume "p"
      with assms have "q⟶ r⟶ s" ..
      hence "r⟶ s" using `q` ..
      thus "s" using `r`..
    qed
  qed    
qed

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

lemma ejercicio_11a:
  "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof
  assume 1: "p ⟶ (q ⟶ r)"
  show 2: "(p ⟶ q) ⟶ (p ⟶ r)"
  proof 
    assume 3: "p⟶ q"
    show 4: "p⟶ r" 
    proof 
      assume 5: "p"
      have 6: "q" using 3 5 by (rule mp)
      have 7:"q⟶ r" using 1 5 by (rule mp)
      show  8: "r" using 7 6 ..
    qed
  qed          
qed


-- "Reme Sillero"

lemma ejercicio_11b:
  "(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"
          with `p ⟶ q` have "q" ..
          have "q ⟶ r" using `p⟶ (q ⟶ r)` `p` ..
          show "r" using `q ⟶ r` `q` ..
      qed
   qed
qed


text {* --------------------------------------------------------------- 
  Ejercicio 12. Demostrar
     (p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_12a:
  assumes "(p ⟶ q) ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"
proof -
  have 1: "(p⟶ q)⟶ r" using assms by this
  {assume 2: "p"
    {assume 3: "q"
      {assume 4: "p"
        have 5: "q" using 3 by this}
      hence 6: "p⟶ q"  ..
      have 7: "r" using assms 6 ..}
    hence 8: "q⟶ r" ..}
  thus 9: "p⟶ (q⟶ r)" ..
qed


section {* Conjunciones *}

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

-- "Pedro G. Ros Reina"

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

-- "Pedro G. Ros"
lemma ejercicio_13b:
  assumes 1:"p" and
          2:"q" 
  shows "p ∧ q"
using assms ..

text {* --------------------------------------------------------------- 
  Ejercicio 14. Demostrar
     p ∧ q ⊢ p
  ------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_14:
  assumes "p ∧ q"  
  shows   "p"
proof -
show "p" using assms by (rule conjunct1)
qed

-- "Pedro G. Ros Reina"
lemma ejercicio_14b:
  assumes "p ∧ q" 
  shows   "p"
using assms ..

text {* --------------------------------------------------------------- 
  Ejercicio 15. Demostrar
     p ∧ q ⊢ q
  ------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_15:
  assumes "p ∧ q" 
  shows   "q"
proof -
show "q" using assms by (rule conjunct2)
qed


-- "Pedro G. Ros Reina"
lemma ejercicio_15b:
  assumes "p ∧ q" 
  shows   "q"
using assms ..

text {* --------------------------------------------------------------- 
  Ejercicio 16. Demostrar
     p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
  ------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_16:
  assumes "p ∧ (q ∧ r)"
  shows   "(p ∧ q)∧ r"
proof -
have 1: "p" using assms by (rule conjunct1)
have 2: "(q ∧ r)" using assms by (rule conjunct2)
have 3: "q" using 2 by (rule conjunct1)
have 4: "r" using 2 by (rule conjunct2)
have 5: "(p∧q)" using 1 3 by (rule conjI)
show 6: "(p∧q) ∧ r" using 5 4 by (rule conjI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 17. Demostrar
     (p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
  ------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_17:
  assumes "(p∧ q) ∧ r" 
  shows   "p ∧ (q∧ r)"
proof -
have 1: "r" using assms by (rule conjunct2)
have 2: "(p∧q)" using assms by (rule conjunct1)
have 3: "p" using 2 by (rule conjunct1)
have 4: "q" using 2 by (rule conjunct2)
have 5: "(q∧r)" using 4 1 by (rule conjI)
show 6: "p∧(q∧r)" using 3 5 by (rule conjI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 18. Demostrar
     p ∧ q ⊢ p ⟶ q
  ------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_18:
  assumes "p ∧ q" 
  shows   "p ⟶ q"
proof -
have 1: "q" using assms by (rule conjunct2)
show "p⟶ q" using 1 by (rule impI)
qed


-- "Reme Sillero"
lemma ejercicio_18a:
  assumes "p ∧ q" 
  shows   "p ⟶ q"
   proof 
     assume "p"
     show "q" using assms .. 
   qed

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

-- "Carmen Martinez Navarro , Erlinda Menendez Perez"



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




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

-- "Jesús Horno Cobo"

lemma ejercicio_20:
  assumes 1:"p ⟶ q ∧ r" 
  shows   "(p ⟶ q) ∧ (p ⟶ r)"
proof -
  { assume 3: "p"
    have 4: "q ∧ r" using 1 3 by (rule mp)
    have 5: "q" using 4 by (rule conjunct1) }
  hence 6: "p ⟶ q" by (rule impI)
  { assume 7: "p"
    have 8: "q ∧ r" using 1 7 by (rule mp)
    have 9: "r" using 8 by (rule conjunct2) }
  hence 10: "p ⟶ r" by (rule impI)
 show "(p ⟶ q) ∧ (p ⟶ r)" using 6 10 by (rule conjI)
qed



-- "Antonio Jesús Molero"
lemma ejercicio_20a:
  assumes "p ⟶ q ∧ r" 
  shows   "(p ⟶ q) ∧ (p ⟶ r)"
proof (rule conjI)
  show "p ⟶ q"
    proof (rule impI)
      assume "p"
      with `p ⟶ q ∧ r` have "q ∧ r" ..
      thus "q" ..
    qed
 show "p ⟶ r"
    proof (rule impI)
      assume "p"
      with `p ⟶ q ∧ r` have "q ∧ r" ..
      thus "r" ..
    qed
qed



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

-- "Pedro G. Ros"
lemma ejercicio_21a:
  assumes 1:"p ⟶ (q ⟶ r)" 
  shows   "p ∧ q ⟶ r"
proof
  assume 2:"p∧q"
  show "r" 
  proof -
    have 3: "p" using 2 by (rule conjunct1)
    have 4: "q" using 2 ..
    have 5: "(q⟶ r)" using 1 3 ..
    show 6: "r" using 5 4 ..
  qed
qed

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

-- "Pedro G. Ros"
lemma ejercicio_22a:
  assumes "p ∧ q ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"
proof
  assume "p"
  show "q⟶ r"
  proof
    assume "q"
    have "p∧q" using `p` `q` ..
    show "r" using assms `p∧q`..
  qed
qed
text {* --------------------------------------------------------------- 
  Ejercicio 23. Demostrar
     (p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
  ------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_23a:
  assumes 1:"(p ⟶ q) ⟶ r" 
  shows   "p ∧ q ⟶ r" 
proof 
  assume 2:"p∧q"
  hence 3:"p"  ..
  have 4:"q" using 2 ..
  hence 5: "p⟶ q" ..
  show"r" using 1 5 by (rule mp)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 24. Demostrar
     p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_24a:
  assumes "p ∧ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ r"
proof 
  assume 0:"p⟶ q"
  show "r"
  proof -
    have 1: "p" using assms .. 
    have 2: "q" using 0 1 ..
    have 3: "q⟶ r" using assms ..
    show 3: "r" using 3 2 ..
  qed
qed

section {* Disyunciones *}

text {* --------------------------------------------------------------- 
  Ejercicio 25. Demostrar
     p ⊢ p ∨ q
  ------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_25:
  assumes "p"
  shows   "p ∨ q"
proof -
show "p∨q" using assms by (rule disjI1)
qed

-- "Pedro G. Ros Reina"
lemma ejercicio_25b:
  assumes "p"
  shows   "p ∨ q"
using assms ..

text {* --------------------------------------------------------------- 
  Ejercicio 26. Demostrar
     q ⊢ p ∨ q
  ------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_26:
  assumes "q"
  shows   "p ∨ q"
proof -
show "p∨q" using assms by (rule disjI2)
qed

-- "Pedro G. Ros Reina"
lemma ejercicio_26b:
  assumes "q"
  shows   "p ∨ q"
using assms ..


text {* --------------------------------------------------------------- 
  Ejercicio 27. Demostrar
     p ∨ q ⊢ q ∨ p
  ------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_27:
  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  

text {* --------------------------------------------------------------- 
  Ejercicio 28. Demostrar
     q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_28a:
  assumes "q ⟶ r" 
  shows   "p ∨ q ⟶ p ∨ r"
proof 
  assume 1: "p∨q"
  moreover
  {assume "p"
    hence "p∨r" by (rule disjI1)}
  moreover
  {assume "q"
    have "r" using assms `q`..
    hence "p∨r" ..}
  ultimately
  show "p∨r" ..
qed 

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

-- "Pedro Ros"
lemma ejercicio_29a:
  assumes "p ∨ p"
  shows   "p"
proof-
have "p∨p" using assms by this
  moreover
  {assume "p"
    hence "p" by this}
  moreover
  {assume "p"
    hence "p" by this}
  ultimately
  show "p" ..
qed
 
-- "Pedro Ros"
lemma ejercicio_29b:
  assumes "p ∨ p"
  shows   "p"
using assms ..


-- "Antonio Jesús Molero"
lemma ejercicio_29c:
  assumes "p ∨ p"
  shows   "p"
  using assms
proof (rule disjE)
  assume "p" 
  thus "p" by this
next
  assume "p"
  thus "p" by this
qed


text {* --------------------------------------------------------------- 
  Ejercicio 30. Demostrar
     p ⊢ p ∨ p
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_30a:
  assumes "p" 
  shows   "p ∨ p"
proof -
show "p∨p" using assms ..
qed

-- "Pedro Ros"
lemma ejercicio_30b:
  assumes "p" 
  shows   "p ∨ p"
using assms ..

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

-- "Pedro G. Ros"
lemma ejercicio_31a:
  assumes "p ∨ (q ∨ r)" 
  shows   "(p ∨ q) ∨ r"
proof -
  have 1: "p ∨ (q ∨ r)" using assms by this
  moreover
  {assume "p"
    hence "(p∨q)" ..
    hence "(p∨q)∨r" ..}
  moreover
  {assume "(q∨r)"
    moreover
    {assume "q"
      hence "(p∨q)"..
      hence "(p∨q)∨r" ..}
    moreover
    {assume "r"
      hence "(p∨q)∨r" ..}
    ultimately
    have "(p∨q)∨r"..}
  ultimately
  show "(p∨q)∨r" ..
qed
 
text {* --------------------------------------------------------------- 
  Ejercicio 32. Demostrar
     (p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
  ------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_32:
  assumes "(p ∨ q) ∨ r" 
  shows   "p ∨ (q ∨ r)"
using assms(1)
proof
  assume "p∨q"
  thus "p∨q∨r" 
    proof
    assume "p"
    thus "p∨q∨r" ..
    next
    assume "q"
    hence "q∨r" ..
    thus "p∨q∨r" ..
    qed
next
  assume "r"
  hence "q∨r" ..
  thus "p∨q∨r" ..
qed
 
text {* --------------------------------------------------------------- 
  Ejercicio 33. Demostrar
     p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
  ------------------------------------------------------------------ *}
-- "Pedro"
lemma ejercicio_33a:
  assumes "p ∧ (q ∨ r)" 
  shows   "(p ∧ q) ∨ (p ∧ r)"
proof -
  have 1: "p" using assms ..
  have 2: "q∨r" using assms ..
  moreover
  {assume 3: "q"
    have "(p∧q)" using 1 3 ..
    hence "(p ∧ q) ∨ (p ∧ r)" ..}
  moreover
  {assume 4: "r"
    have "p∧r" using 1 4 ..
    hence "(p ∧ q) ∨ (p ∧ r)" ..}
  ultimately
  show "(p ∧ q) ∨ (p ∧ r)" ..
qed
 
 
text {* --------------------------------------------------------------- 
  Ejercicio 34. Demostrar
     (p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
  ------------------------------------------------------------------ *}
 -- "Pedro Ros"
lemma ejercicio_34a:
  assumes "(p ∧ q) ∨ (p ∧ r)" 
  shows   "p ∧ (q ∨ r)"
proof -
  have 1: "(p ∧ q) ∨ (p ∧ r)" using assms by this
  moreover
  {assume "(p ∧ q)"
    hence "p" ..
    have "q" using `p ∧ q` ..
    hence "(q∨r)"..
    have "p∧(q∨r)" using `p``(q∨r)`..}
  moreover
  {assume "(p∧r)"
    hence "p" ..
    have "r" using `p ∧ r` ..
    hence "(q∨r)"..
    have "p∧(q∨r)" using `p``(q∨r)`..}
  ultimately
  show "p ∧ (q ∨ r)" ..
qed
 
text {* --------------------------------------------------------------- 
  Ejercicio 35. Demostrar
     p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
  ------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_35a:
  assumes "p ∨ (q ∧ r)" 
  shows   "(p ∨ q) ∧ (p ∨ r)"
proof -
  have 1: "p ∨ (q ∧ r)" using assms by this
  moreover
  {assume "p"
    hence 2: "(p∨q)" ..
    have 3: "(p∨r)" using `p` ..
    have 4: "(p ∨ q) ∧ (p ∨ r)" using 2 3 ..}
  moreover
  {assume 5:"(q∧r)"
    hence 6: "q" ..
    have 7: "r" using 5 ..
    have 8: "p∨q" using 6 ..
    have 9: "p∨r" using 7 ..
    have "(p ∨ q) ∧ (p ∨ r)"using 8 9 ..}
  ultimately
  show "(p ∨ q) ∧ (p ∨ r)" ..
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_36:
  assumes "(p ∨ q) ∧ (p ∨ r)"
  shows   "p ∨ (q ∧ r)"
proof -
  have "p∨q" using assms..
  moreover
    {assume "p"
     hence "p∨(q∧r)"..}
  moreover
    {assume "q"
     have "p∨r" using assms..
     moreover
     {assume "p"
      hence "p∨(q∧r)"..}
     moreover
     {assume "r"
      with `q` have "q∧r"..
      hence "p∨(q∧r)"..}
     ultimately have "p∨(q∧r)"..}
  ultimately show "p∨(q∧r)"..
qed

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


-- "Erlinda Menendez Perez , Carmen Martinez Navarro"




lemma ejercicio_37:
  assumes "(p ⟶ r) ∧ (q ⟶ r)" 
  shows   "p ∨ q ⟶ r"
proof (rule impI)
  assume 1: "p ∨ q"
  thus "r"
    proof (rule disjE)
      assume 2:"p"
         have 3: "p ⟶ r" using assms by (rule conjunct1)
         show "r" using 3 2 by (rule mp)
      next
      assume 5:"q"
         have 6: "q ⟶ r" using assms by (rule conjunct2)
         show "r" using 6 5 by (rule mp)
    qed
qed



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

-- "Raúl Montes Pajuelo"

lemma ejercicio_38:
  assumes "p ∨ q ⟶ r" 
  shows   "(p ⟶ r) ∧ (q ⟶ r)"
proof -
  {assume 1: "p"
    have 2:"p ∨ q" using 1 ..
    have 3: "r" using assms 2 ..} 
   hence 4: "p⟶r" ..
  {assume 5: "q"
    have 6: "p ∨ q" using 5 ..
    have 7: "r" using assms 6 ..}
  hence 8: "q⟶r" ..
  show "(p⟶r)∧(q⟶r)" using 4 8 ..
qed

section {* Negaciones *}

text {* --------------------------------------------------------------- 
  Ejercicio 39. Demostrar
     p ⊢ ¬¬p
  ------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_39:
  assumes "p"
  shows   "¬¬p"
proof -
show "¬¬p" using assms by (rule notnotI)
qed

-- "Pedro G. Ros Reina"
lemma ejercicio_39b:
  assumes "p"
  shows   "¬¬p"
using assms by (rule notnotI)

-- "Raúl Montes Pajuelo"

lemma ejercicio_39c:
  assumes "p"
  shows   "¬¬p"
proof (rule notI)
  assume "¬p"
  show False using `¬p` assms..
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_40:
  assumes "¬p" 
  shows   "p ⟶ q"
proof (rule impI)
  {assume 1: "p"
    show "q" using assms 1 by (rule notE)}
qed

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

-- "Raúl Montes Pajuelo"

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

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_42:
  assumes "p∨q"
          "¬q" 
  shows   "p"
proof -
  note `p∨q`
  moreover
  {assume "p"
    hence "p" by this}
  moreover
  {assume "q"
    with assms (2) have "p" ..}
  ultimately show "p" ..
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_43:
  assumes "p ∨ q"
          "¬p" 
  shows   "q"
proof -
  note `p∨q`
  moreover
  {assume "p"
   with assms (2) have False..
   hence "q"..}
  moreover
  {assume "q"
   hence "q" .}
  ultimately show "q"..
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_44:
  assumes "p ∨ q" 
  shows   "¬(¬p ∧ ¬q)"
proof -
  {assume "¬p∧¬q"
   note `p∨q`
   moreover
   {have "¬p" using `¬p∧¬q`by (rule conjunct1)
    assume "p"
    with `¬p`have False by (rule notE)}
   moreover
   {have "¬q" using `¬p∧¬q`by (rule conjunct2)
    assume "q"
    with `¬q`have False by (rule notE)}
   ultimately have False by (rule disjE)}
  thus "¬(¬p∧¬q)" by (rule notI)
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_45:
  assumes "p ∧ q" 
  shows   "¬(¬p ∨ ¬q)"
proof (rule notI)
  assume "¬p∨¬q"
  show False
  proof (rule disjE)
  {show "¬p∨¬q" using `¬p∨¬q`.
   next
   show "¬p⟹False"
   proof -
   {assume "¬p"
    have "p" using assms..
    with `¬p`show False..}
   qed
   next
   show "¬q⟹False"
   proof -
   {assume "¬q"
    have "q" using assms..
    with `¬q`show False..}
   qed}
  qed 
qed


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

-- "Raúl Montes Pajuelo"

lemma ejercicio_46:
  assumes "¬(p ∨ q)" 
  shows   "¬p ∧ ¬q"
proof (rule conjI)
  show "¬p"
  proof (rule notI)
  {assume "p"
   hence "p∨q"..
   with assms show False..}
  qed
  next
  show "¬q"
  proof (rule notI)
  {assume "q"
   hence "p∨q"..
   with assms show False..}
  qed
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_47:
  assumes "¬p ∧ ¬q" 
  shows   "¬(p ∨ q)"
proof (rule notI)
  assume "p∨q"
  show False
  proof (rule disjE)
  {show "p∨q" using `p∨q` .
   next
   show "p⟹False"
   proof -
   {have "¬p" using assms..
    assume "p"
    with `¬p`show False..}
   qed
   next
   show "q⟹False"
   proof -
   {have "¬q" using assms..
    assume "q"
    with `¬q`show False..}
   qed}
  qed
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_48:
  assumes "¬p ∨ ¬q"
  shows   "¬(p ∧ q)"
proof (rule disjE)
  show "¬p∨¬q" using assms .
  next
  show "¬p⟹¬(p∧q)"
  proof -
  {assume "¬p"
   show "¬(p∧q)"
   proof (rule notI)
   {assume "p∧q"
    hence "p"..
    with `¬p`show False..}
   qed}
  qed
  next
  show "¬q⟹¬(p∧q)"
  proof -
  {assume "¬q"
   show "¬(p∧q)"
   proof (rule notI)
   {assume "p∧q"
    hence "q"..
    with `¬q`show False..}
   qed}
  qed
qed

-- "Pedro Ros"
lemma ejercicio_48b:
  assumes "¬p ∨ ¬q"
  shows   "¬(p ∧ q)"
proof (rule disjE)
  show "¬p ∨ ¬q" using assms .
next
  assume 1: "¬p"
  show "¬(p∧q)"
  proof
  assume "p∧q"
  hence 2: "p" ..
  show  "False" using 1 2 ..
  qed
next
  assume 1: "¬q"
  show "¬(p∧q)"
  proof
  assume "p∧q"
  hence 2: "q" ..
  show  "False" using 1 2 ..
  qed
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_49:
  "¬(p ∧ ¬p)"
proof (rule notI)
  assume "p∧¬p"
  hence "¬p"..
  have "p" using `p∧¬p`..
  with `¬p`show False..
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_50:
  assumes "p ∧ ¬p" 
  shows   "q"
proof (rule notE)
  show "p" using assms ..
  show "¬p" using assms ..
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_51:
  assumes "¬¬p"
  shows   "p"
proof (rule ccontr)
  assume "¬p"
  with `¬¬p` show False..
qed

-- "Pedro Ros"
lemma ejercicio_51b:
  assumes "¬¬p"
  shows   "p"
using assms by (rule notnotD)

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_52:
  "p ∨ ¬p"
proof (rule ccontr)
  {assume "¬(p∨¬p)"
   have "p"
   proof (rule ccontr)
   {assume "¬p"
    hence "p∨¬p"..
    with `¬(p∨¬p)` show False..}
   qed
   hence "p∨¬p"..
   with `¬(p∨¬p)` show False..}
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_53:
  "((p ⟶ q) ⟶ p) ⟶ p"
proof (rule impI)
  assume "(p⟶q)⟶p"
  show "p"
  proof (rule ccontr)
    note `(p⟶q)⟶p`
    assume "¬p"
    with `(p⟶q)⟶p` have "¬(p⟶q)" by (rule mt)
    {assume "p"
     with `¬p` have "q" by (rule notE)}
    hence "p⟶q" by (rule impI)
    with `¬(p⟶q)` show False by (rule notE)
  qed
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_54:
  assumes "¬q ⟶ ¬p"
  shows   "p ⟶ q"
proof (rule impI)
 {assume "p"
  hence "¬¬p" by (rule notnotI)
  with `¬q⟶¬p` have "¬¬q" by (rule mt)
  show "q"
  proof (rule ccontr)
  {assume "¬q"
   with `¬¬q` show False..}
  qed}
qed

-- "Pedro Ros"
lemma ejercicio_54b:
  assumes "¬q ⟶ ¬p"
  shows   "p ⟶ q"
proof
assume "p"
hence "¬¬p" by (rule notnotI)
with assms have "¬¬q" by (rule mt)
thus q by (rule notnotD)
qed


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

-- "Raúl Montes Pajuelo"

lemma ejercicio_55:
  assumes "¬(¬p ∧ ¬q)"
  shows   "p ∨ q"
proof (rule disjE)
  show "¬p∨p"..
  show "¬p⟹p∨q"
  proof -
  {assume "¬p"
   have "q"
   proof (rule ccontr)
   {assume "¬q"
    with `¬p` have "¬p∧¬q"..
    with assms show False..}
   qed
   then show "p∨q"..}
  qed
  show "p⟹p∨q"
  proof -
  {assume "p"
   then show "p∨q"..}
  qed
qed

-- "Pedro Ros"
lemma ejercicio_55b:
  assumes "¬(¬p ∧ ¬q)"
  shows   "p ∨ q"
proof (rule ccontr)
assume "¬(p ∨ q)"
hence " ¬p ∧ ¬q" by (rule ejercicio_46)
with assms show "False" ..
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_56:
  assumes "¬(¬p ∨ ¬q)" 
  shows   "p ∧ q"
proof(rule conjI)
  show "p"
  proof(rule ccontr)
   {assume "¬p"
    hence "¬p∨¬q"..
    with assms show False..}
  qed
  show "q"
  proof(rule ccontr)
   {assume "¬q"
    hence "¬p∨¬q"..
    with assms show False..}
  qed
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_57:
  assumes "¬(p ∧ q)"
  shows   "¬p ∨ ¬q"
proof -
  have "¬p∨p"..
  moreover
   {assume "¬p"
    hence "¬p∨¬q"..}
  moreover
   {assume "p"
    have "¬q∨q"..
    moreover
    {assume "¬q"
     hence "¬p∨¬q"..}
    moreover
    {assume "q"
     with `p`have "p∧q"..
     with `¬(p∧q)` have "¬p∨¬q"..}
    ultimately have "¬p∨¬q"..}
  ultimately show "¬p∨¬q"..
qed

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

-- "Raúl Montes Pajuelo"

lemma ejercicio_58:
  "(p ⟶ q) ∨ (q ⟶ p)"
proof -
  have  "¬p ∨ p" ..
  moreover
  {assume "¬p"
    {assume "p"
     with `¬p` have "q" ..}
   hence "p⟶q" ..
   hence "(p⟶q)∨(q⟶p)" ..}
  moreover
  {assume "p"
    {assume "q"
     note `p`}
   hence "q⟶p"..
   hence "(p⟶q)∨(q⟶p)"..}
  ultimately show "(p⟶q)∨(q⟶p)" ..
qed

-- "Raúl Montes Pajuelo: Voy a añadir algunos ejercicios de examen más. Creo que es interesante tenerlos aquí resueltos"

text {* --------------------------------------------------------------- 
  Ejercicio 59: Examen de Septiembre del 2006. Demostrar
    (p ⟶ r) ∨ (q ⟶ s) ⊢ (p ∧ q) ⟶ (r ∨ s)
  ------------------------------------------------------------------ *}

-- "Raúl Montes Pajuelo"

lemma ejercicio_59:
  assumes "(p ⟶ r) ∨ (q ⟶ s)" 
  shows "(p ∧ q) ⟶ (r ∨ s)"
proof
  assume "p ∧ q"
  show "r ∨ s"
  proof (rule disjE)
    show "(p ⟶ r) ∨ (q ⟶ s)" using assms.
    next        
    show "p ⟶ r ⟹ r ∨ s"
    proof -
      assume "p ⟶ r"
      have "p" using `p ∧ q`..
      with `p ⟶ r`have "r"..
      thus "r ∨ s"..
    qed 
    next
    show "q ⟶ s ⟹ (r ∨ s)"
    proof -
      assume "q ⟶ s"
      have "q" using `p ∧ q`..
      with `q ⟶ s`have "s"..
      thus "r ∨ s"..
    qed
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 60: Examen de Junio del 2005. Demostrar
    p ∧ ¬(q ⟶ r) ⊢ (p ∧ q) ∧ ¬r
  ------------------------------------------------------------------ *}

-- "Raúl Montes Pajuelo"

lemma ejercicio_60:
assumes "p ∧ ¬(q ⟶ r)" 
  shows "(p ∧ q) ∧ ¬r"
proof (rule conjI)
  have "p" using assms..
  have "¬(q ⟶ r)" using assms..
  have "q"
  proof (rule ccontr)
    assume "¬q"
    have "q ⟶ r"
    proof
      assume "q"
      with `¬q` have False..
      thus "r"..
    qed
    with `¬(q ⟶ r)` show False..
  qed
  with `p` show "p ∧ q"..
  show "¬r"
  proof (rule notI)
    assume "r"
    have "q ⟶ r"
    proof
      assume "q"
      show "r" using `r`.
    qed
    with `¬(q ⟶ r)`show False..
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 61: Examen de Diciembre del 2005. Demostrar
    ⊢(p ⟶ ¬q) ∧ (p ⟶ ¬r)⟶(p ⟶ ¬(q ∨ r)) 
  ------------------------------------------------------------------ *}

-- "Raúl Montes Pajuelo"

lemma ejercicio_61:
  "(p ⟶ ¬q) ∧ (p ⟶ ¬r)⟶(p ⟶ ¬(q ∨ r))" 
proof (rule impI)
  assume "(p ⟶ ¬q) ∧ (p ⟶ ¬r)"
  show "(p ⟶ ¬(q ∨ r))"
  proof (rule impI)
    assume "p"
    show "¬(q ∨ r)"
    proof (rule notI)
      assume "q ∨ r"
      thus False
      proof
        assume "q"
        hence "¬¬q" by (rule notnotI)
        have "p ⟶ ¬q" using `(p ⟶ ¬q) ∧ (p ⟶ ¬r)`..
        have "¬p" using `p ⟶ ¬q` `¬¬q` by (rule mt)
        show False using `¬p` `p`..
        next
        assume "r"
        hence "¬¬r" by (rule notnotI)
        have "p ⟶ ¬r" using `(p ⟶ ¬q) ∧ (p ⟶ ¬r)`..
        have "¬p" using `p ⟶ ¬r` `¬¬r` by (rule mt)
        show False using `¬p` `p`..
      qed
    qed
  qed
qed

end