Relación 8

chapter {* R8: Deducción natural proposicional en Isabelle/HOL *}

theory R8_Deduccion_natural_proposicional
imports Main 
begin

text {*
  Demostrar o refutar los siguientes lemas usando sólo las reglas
  básicas de deducción natural de la lógica proposicional, de los
  cuantificadores y de la igualdad: 
  · conjI:      ⟦P; Q⟧ ⟹ P ∧ Q
  · conjunct1:  P ∧ Q ⟹ P
  · conjunct2:  P ∧ Q ⟹ Q  
  · notnotD:    ¬¬ P ⟹ P
  · mp:         ⟦P ⟶ Q; P⟧ ⟹ Q 
  · 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

  · allI:       ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
  · allE:       (⋀x. P x) ⟹ ∀x. P x
  · exI:        P x ⟹ ∃x. P x
  · exE:        ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q

  · refl:       t = t
  · subst:      ⟦s = t; P s⟧ ⟹ P t
  · trans:      ⟦r = s; s = t⟧ ⟹ r = t
  · sym:        s = t ⟹ t = s
  · not_sym:    t ≠ s ⟹ s ≠ t
  · ssubst:     ⟦t = s; P s⟧ ⟹ P t
  · box_equals: ⟦a = b; a = c; b = d⟧ ⟹ a: = d
  · arg_cong:   x = y ⟹ f x = f y
  · fun_cong:   f = g ⟹ f x = g x
  · cong:       ⟦f = g; x = y⟧ ⟹ f x = g y
*}

text {*
  Se usarán las reglas notnotI, mt y not_ex que demostramos a continuación.
  *}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma no_ex: "¬(∃x. P(x)) ⟹ ∀x. ¬P(x)"
by auto

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

(* marcarmor13 *)
--"usando un supuesto ¬¬p"
lemma ejercicio_1:
 assumes 1: "¬q ⟶ ¬p" and 
         2: "¬¬p"  
 shows "p ⟶ q"
proof -
 have 3: "¬¬q" using 1 2  by (rule mt)
 have 4: "q" using 3 by (rule  notnotD)
 show "p ⟶ q" using 4 by (rule impI)
qed

(* pablucoto jeamacpov migtermor *)
lemma ejercicio_1_2:
  assumes "¬q ⟶ ¬p" 
  shows "p ⟶ q"
proof -
  {assume "p"
   hence "¬¬p" by (rule notnotI)
   with `¬q ⟶ ¬p` have "¬¬q" by (rule mt)  
   hence "q" by (rule notnotD)}
   then show "p ⟶ q" by (rule impI)
qed

(* ivamenjim serrodcal anaprarod marpoldia1 manmorjim1 crigomgom juancabsou ferrenseg fraortmoy rubgonmar *)
lemma ejercicio_1_3:
  assumes 1: "¬q ⟶ ¬p" 
  shows      "p ⟶ q"
proof -
  {assume 2:"p"
   then have 3: "¬¬p" by (rule notnotI)
   have 4: "¬¬q" using 1 3 by (rule mt)
   then have 5: "q" by (rule notnotD)}
  thus "p ⟶ q" by (rule impI)
qed   

(* bowma *)
lemma ejercicio_1_4:
 assumes "¬q ⟶ ¬p"
 shows "p ⟶ q"
proof -
 {assume "p"
  hence "¬¬p" by (rule notnotI)
  with assms have "¬¬q" by (rule mt)
  then have "q" by (rule notnotD)}
  thus "p ⟶ q" by (rule impI)
qed

(* bowma danrodcha paupeddeg pabrodmac fracorjim1 *)
lemma ejercicio_1_5:
 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

(* josgarsan *)
lemma ejercicio_1_6:
 assumes 1: "¬q ⟶ ¬p"
 shows "p ⟶ q"
proof (cases)
assume "p"
 then show "p⟶q" using 1 by simp 
next
 assume "¬p"
 then show "p⟶q" by simp
qed

(* dancorgar *)
lemma ejercicio_1_7:
  assumes "¬q ⟶ ¬p"
  shows "p ⟶ q"
proof-
  {assume "p"
   assume "¬q"
   have "¬p" using assms(1) `¬q` by (rule mp)}
  thus "p ⟶ q"
  apply simp
  apply (rule ccontr)
  apply simp
  done
qed

(* antsancab1 *)
lemma ejercicio_1:
  assumes 1: "¬q ⟶ ¬p"
  shows "p ⟶ q"
proof -
  {assume p
  hence "¬¬p" by (rule notnotI)
  with 1 have "¬¬q" by (rule mt)
  hence "q" by (rule notnotD)
  }
  then show "p ⟶ q" by (rule impI)
qed

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

(* marcarmor13 *)
-- "usando un supuesto ¬p ∧ ¬q"
lemma ejercicio_2:
  assumes 1: "¬(¬p ∧ ¬q)" and
          2: "¬p ∧ ¬q"       
  shows "p ∨ q"
proof -
  have 3: "p" using 1 2 by (rule notE)
  show "p ∨ q" using 3 by (rule disjI1)
qed

(* Comentario: No se corresponde con el enunciado. *)

(* ivamenjim serrodcal marpoldia1 antsancab1 *)
lemma ejercicio_2_2:
  assumes 1: "¬(¬p ∧ ¬q)"
  shows      "p ∨ q"
proof -
   { assume 2: "(¬p ∧ ¬q)"
     have "p" using 1 2 by (rule notE)
     then have "p ∨ q" by (rule disjI1)}
   thus "p ∨ q" by auto
qed

(* Comentario: Usa auto. *)

(* pablucoto jeamacpov *)
lemma aux_ejercicio2:
  assumes "¬(p ∨ q)"
  shows "¬p ∧ ¬q"
proof
  { assume "p"
    hence "p ∨ q" by  (rule disjI1)  
    with  `¬(p ∨ q)` have "False" by (rule notE)}
  then show "¬p" ..
next
  { assume "q"
    hence "p ∨ q" by (rule disjI2)
    with  `¬(p ∨ q)` have "False" by (rule notE)}
  then show "¬q" ..
qed

lemma ejercicio_2_3:
  assumes "¬(¬p ∧ ¬q)"
  shows "p ∨ q"
proof -
  { assume 2: "¬(p ∨ q)"  
    hence "¬p ∧ ¬q" by (rule  aux_ejercicio2)
    with  `¬(¬p ∧ ¬q)` have "False" ..}
  then show "p ∨ q" by (rule ccontr)
qed

(* danrodcha bowma *)
lemma ej_2:
  assumes "¬(¬p ∧ ¬q)"
  shows "p ∨ q"
proof -
  have "¬p ∨ p" by (rule excluded_middle)
  thus "p ∨ q"
  proof (rule disjE)
    { assume "¬p"
      have "¬q ∨ q" by (rule excluded_middle)
      thus "p ∨ q"
      proof (rule disjE)
      { 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" by (rule disjI2)}
      qed}
    next
    { assume "p"
      thus "p ∨ q" by (rule disjI1)}
    qed
qed

(* anaprarod crigomgom juancabsou ferrenseg fraortmoy fracorjim1 rubgonmar *)
(* Igual que el anterior pero con etiquetas *)
lemma ejercicio_2_4:
  assumes 0:  "¬(¬p ∧ ¬q)"
  shows   "p ∨ q"
proof-
  have "¬p ∨ p" by (rule excluded_middle)
  thus "p ∨ q"
  proof (rule disjE)
    { assume 1: "¬p" 
      have "¬q ∨ q" by (rule excluded_middle)
      thus "p ∨ q"
      proof (rule disjE)
        { assume 2: "¬q"
          have 3: "(¬p ∧ ¬q)" using 1 2 by (rule conjI)
          have "p ∨ q" using 0 3 by (rule notE)
          thus "p ∨ q" by this}
        next
        { assume 4: "q"
          have "p ∨ q" using 4 by (rule disjI2)
          thus "p ∨ q" by this}
        qed}
    next
    { assume 5: "p"
      have "p ∨ q" using 5 by (rule disjI1)
      thus "p ∨ q" by this}
   qed
qed

(* migtermor *)
lemma lem:
 shows "p ∨ ¬p"
proof -
 {assume 1: "¬(p∨¬p)"
  {assume 2: "p"
   then have 3: "p∨¬p" by (rule disjI1)
   also have 4: "False" using 1 3 by (rule notE)}
  then have 5: "¬p" by (rule notI)
  then have 6: "p∨¬p" by (rule disjI2)
  also have 7: "False" using 1 6 by (rule notE)}
 thus "p∨¬p" by (rule ccontr)
qed

lemma ejercicio_2_5:
 assumes 1: "¬(¬p∧¬q)"
 shows "p∨q"
proof -
 have 2: "p∨¬p" by (rule lem)
 moreover
 {assume 3: p 
  then have 4: "p∨q" by (rule disjI1)}
 moreover
 {assume 6: "¬p"
  {assume 7: "¬q"
   also have 8: "¬p∧¬q" using 6 7 by (rule conjI)
   have 9: "False" using 1 8 by (rule notE)}
  then have 10: "q" by (rule ccontr)
  then have 11: "p∨q" by (rule disjI2)}
 ultimately show "p∨q" by (rule disjE)
qed

(* paupeddeg pabrodmac *)
lemma aux1:
  assumes "¬(p ∧ q)"
  shows "¬p ∨ ¬q"
proof -
  have "¬p ∨ p" by (rule excluded_middle)
  thus "¬p ∨ ¬q"
  proof
    {assume "¬p"
    thus "¬p ∨ ¬q" by (rule disjI1)}
    next
    {assume "p"
      have "¬q"
      proof
      {assume "q"
      have "(p ∧ q)" using `p` `q`  by (rule conjI)
      show "False"  using `¬(p ∧ q)` `p ∧ q` by (rule notE)}
      qed
      thus "¬p ∨ ¬q" by (rule disjI2)}
      qed
qed
  
lemma ejercicio_2_5b:
  assumes "¬(¬p ∧ ¬q)"
  shows "p ∨ q" 
proof -
  have "¬¬p ∨ ¬¬q" using assms  by (rule aux1)
  moreover
  {assume "¬¬p"
    hence "p" by (rule notnotD)
    hence "p ∨ q" by (rule disjI1) }
  moreover
  {assume "¬¬q"
    hence "q" by (rule notnotD)
    hence "p ∨ q" by (rule disjI2) }
  ultimately show "p ∨ q" by (rule disjE)
qed

(* pabrodmac *)
lemma ejercicio_2_6:
 assumes "¬(¬p ∧ ¬q)"
 shows "p ∨ q"     
proof -
have "¬¬p ∨ ¬¬q" using assms by (rule Meson.not_conjD)
  moreover
  { assume "¬¬p"
    hence "p" by (rule notnotD)
    hence "p ∨ q" by (rule disjI1) }
  moreover
  { assume "¬¬q"
    then have "q" by (rule notnotD)
    hence "p ∨ q" by (rule disjI2) }
  ultimately show "p ∨ q" by (rule disjE)
qed

(* dancorgar *)
lemma ejercicio_2_7:
  assumes "¬(¬p ∧ ¬q)"
  shows "p ∨ q"
proof-
  {assume "(¬p ∧ ¬q)"
   have "p" using assms `(¬p ∧ ¬q)` by (rule notE)
   then have "p ∨ q"  by (rule disjI1)}
  then show "p ∨ q"
  apply simp
  apply (rule ccontr)
  apply simp
  done
qed

(* josgarsan *)
lemma ejercicio_2_8:
 assumes 1: " ¬(¬p ∧ ¬q)"
 shows "p ∨ q"
proof (cases)
 assume "p"
 then show "p ∨ q" using disjI1 by simp
next
 assume "¬p"
 then have "q" using 1 conjunct2 by simp
 then show "p ∨ q" using disjI2 by simp
qed   

(* Comentario: Uso de simp. *)

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

(* marcarmor13 serrodcal marpoldia1 antsancab1 *)
--"usando un supuesto ¬p ∨ ¬q"
lemma ejercicio_3:
  assumes 1: "¬(¬p ∨ ¬q)" and
          2:"¬p ∨ ¬q"       
  shows "p ∧ q"
proof-
  have 3: "p"using 1 2 by (rule notE)
  have 4: "q"using 1 2 by (rule notE)
  show "p ∧ q" using 3 4 by (rule conjI)
qed

(* Comentario: Uso de la negación de la hipótesis. *)

(* pablucoto jeamacpov *)
lemma ejercicio_3_2:  
  assumes "¬(¬p ∨ ¬q)"
  shows "p ∧ q"
proof  
  have "¬¬p ∧ ¬¬q" using assms(1) by (rule  aux_ejercicio2)  
  hence "¬¬p"  by (rule conjunct1)
  show "p" using `¬¬p` by (rule notnotD)
next 
  have "¬¬p ∧ ¬¬q" using assms(1) by (rule  aux_ejercicio2)  
  have "¬¬q" using `¬¬p ∧ ¬¬q`  by (rule conjunct2) 
  show "q" using `¬¬q` by (rule notnotD)
qed

(* ivamenjim *)
lemma aux: "¬(p ∨ q) ⟹ ¬p ∧ ¬q"
by auto

lemma ejercicio_3_3:
  assumes 1: "¬(¬p ∨ ¬q)"
  shows "p ∧ q"
proof
  have 2: "¬¬p ∧ ¬¬q" using 1 by (rule aux)
  have 3: "¬¬p" using 2 ..
  have 4: "¬¬q" using 2 ..
  show "p" using 3 by (rule notnotD)
  show "q" using 4 by (rule notnotD)
qed

(* Comentario: Uso de auxiliar con auto. *)

(* danrodcha migtermor bowma *)
lemma ej_3:
  assumes "¬(¬p ∨ ¬q)"
  shows "p ∧ q"
  proof (rule conjI)
  { assume "¬p"
    hence "¬p ∨ ¬q" by (rule disjI1)
    with assms have False by (rule notE)}
  then show "p" by (rule ccontr)
  { assume "¬q"
    hence "¬p ∨ ¬q" by (rule disjI2)
    with assms have False by (rule notE)}
  then show "q" by (rule ccontr)
qed

(* anaprarod crigomgom juancabsou ferrenseg fraortmoy fracorjim1 rubgonmar *)
(* Igual que el anterior pero con etiquetas *)
lemma ejercicio_3_4:
  assumes "¬(¬p ∨ ¬q)"
  shows "p ∧ q"
proof (rule conjI)  
  {assume 1: "¬p"
    hence 2: "¬p ∨ ¬q" by (rule disjI1)
    have "False" using assms 2 by (rule notE)}
  thus 3: "p" by (rule ccontr)
  {assume 4: "¬q"
    hence 5: "¬p ∨ ¬q" by (rule disjI2)
    have "False" using assms 5 by (rule notE)}
  thus 6: "q" by (rule ccontr)
qed

(* paupeddeg pabrodmac *)
lemma aux2:
  assumes "¬(p ∨ q)"
  shows "¬p ∧ ¬q"
proof -
  have "¬p ∨ p" by (rule excluded_middle)
  thus "¬p ∧ ¬q"
  proof
    {assume "¬p" 
      have "¬q ∨ q" by (rule excluded_middle)
      thus "¬p ∧ ¬q"
      proof
        {assume "¬q"
          show "¬p ∧ ¬q" using `¬p` `¬q` by (rule conjI)}  
        {assume "q"
           hence "(p ∨ q)"  by (rule disjI2)
           have "False"  using `¬(p ∨ q)` `p ∨ q` by (rule notE)
           thus "¬p ∧ ¬q" by (rule FalseE) }
         qed}
    {assume "p"
        hence "(p ∨ q)"  by (rule disjI1)
        have "False"  using `¬(p ∨ q)` `p ∨ q` by (rule notE) 
        thus "¬p ∧ ¬q" by (rule FalseE) }
qed
qed
      
lemma ejercicio_3_5:
  assumes  "¬(¬p ∨ ¬q)"
  shows "p ∧ q"
proof -
  have "¬¬p ∧ ¬¬q" using assms by (rule aux2)
  hence "¬¬p" by (rule conjunct1)
  hence "p" by (rule notnotD)
  have "¬¬q" using `¬¬p ∧ ¬¬q` by (rule conjunct2)
  hence "q" by (rule notnotD) 
  show  "p ∧ q" using  `p` `q` by (rule conjI) 
qed

(* pabrodmac *)
lemma ejercicio_3_6:
  assumes "¬(¬p ∨ ¬q)"
  shows "p ∧ q" 
proof 
  have "¬¬p ∧ ¬¬q" using assms by (rule Meson.not_disjD)
  hence "¬¬p"  by (rule conjunct1)
  show "p" using `¬¬p` by (rule notnotD)
next
  have "¬¬p ∧ ¬¬q" using assms by (rule Meson.not_disjD)
  hence "¬¬q"  by (rule conjunct2)
  show "q" using `¬¬q` by (rule notnotD)
qed   

(* pabrodmac *)
lemma ejercicio_3_7:
  assumes "¬(¬p ∨ ¬q)"
  shows "p ∧ q" 
proof 
  have "¬¬p ∧ ¬¬q" using assms by (rule Meson.not_disjD)
  have "¬¬p" using `¬¬p ∧ ¬¬q`  by (rule conjunct1)
  have "¬¬q" using `¬¬p ∧ ¬¬q`  by (rule conjunct2)
  show "p" using `¬¬p` by (rule notnotD)
  show "q" using `¬¬q` by (rule notnotD)
qed

(* dancorgar *)
lemma ejercicio_3_8:
  assumes "¬(¬p ∨ ¬q)"
  shows "p ∧ q"
proof -
  {assume "(¬p ∨ ¬q)"
   have "p" using assms `(¬p ∨ ¬q)` by (rule notE)
   have "q" using assms `(¬p ∨ ¬q)` by (rule notE)
   have "p ∧ q" using `p` `q`  by (rule conjI)}
  then show "p ∧ q"
  apply simp
  apply (rule ccontr)
  apply simp
  done
qed

(* josgarsan *)
lemma ejercicio_3_9:
  assumes 1: "¬(¬p ∨ ¬q)"
  shows   "p ∧ q"
proof (rule ccontr)
  assume "¬(p ∧ q)"
  then show False using 1 by simp
qed

(* Comentario: Uso de simp. *)

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

(* marcarmor13 serrodcal *)
--"usando un supuesto p ∧ q"
lemma ejercicio_4_1:
  assumes 1: " ¬(p ∧ q)" and
          2: "p ∧ q"       
  shows "¬p ∨ ¬q"
proof -
  have 3: "¬p"using 1 2 by (rule notE)
  show "¬p ∨ ¬q" using 3  by (rule disjI1)
qed

(* Comentario: Uso de la negación de la hipótesis.*)

(* ivamenjim marpoldia1 ferrenseg fraortmoy rubgonmar antsancab1 *)
lemma ejercicio_4_2:
  assumes 1: "¬(p ∧ q)"
  shows      "¬p ∨ ¬q"
proof -
   {assume 2:"(p ∧ q)"
   have "¬p" using 1 2 by (rule notE)
   then have "¬p ∨ ¬q" by (rule disjI1)}
   thus "¬p ∨ ¬q" by auto
qed  

(* Comentario: Uso de auto. *)

(* pablucoto jeamacpov crigomgom juancabsou *)
lemma ejercicio_4_3:
  assumes  " ¬(p ∧ q)"
  shows    " ¬p ∨ ¬q"
proof -
 { assume 2: "¬(¬p ∨ ¬q)"
   hence "p ∧ q" by (rule ejercicio_3_2)  
   with assms(1) have  "False" .. } 
 then show " ¬p ∨ ¬q" by (rule ccontr)
qed

(*danrodcha anaprarod bowma *)
lemma ej_4:
  assumes "¬(p ∧ q)"
  shows "¬p ∨ ¬q"
  proof (rule ccontr)
    assume "¬ (¬ p ∨ ¬ q)"
    hence "p ∧ q" by (rule ej_3)
    with assms show False  by (rule notE)
qed

(* anaprarod *)
(* sin usar el ejercicio anterior *)
lemma ejercicio_4_4: 
  assumes "¬(p ∧ q)"
  shows "¬p ∨ ¬q"
proof -
  have "¬p ∨ p" by (rule excluded_middle)
  thus "¬p ∨ ¬q"
  proof (rule disjE)
    {assume "¬p"
      thus "¬p ∨ ¬q" by (rule disjI1)}
    next
    {assume 1:"p"
      have "¬q ∨ q" by (rule excluded_middle)
      thus "¬p ∨ ¬q"
      proof (rule disjE)
        {assume "¬q"
          thus "¬p ∨ ¬q" by (rule disjI2)}
        next
        {assume 2:"q"
          have 3:"p ∧ q" using 1 2 by (rule conjI)
          have "¬p ∨ ¬q" using assms 3 by (rule notE)
          thus "¬p ∨ ¬q" by this}
      qed}
   qed
qed

(* migtermor *)
lemma ejercicio_4_5:
 assumes 1: "¬(p∧q)"
 shows "¬p∨¬q"
proof -
 have 2: "p∨¬p" by (rule lem)
 moreover
 {assume 3: "p" 
  {assume 4: "q"
   also have 5: "p∧q" using 3 4 by (rule conjI)
   have 6: "False" using assms 5 by (rule notE)}
  then have 7: "¬q" by (rule notI)
  then have 8: "¬p∨¬q" by (rule disjI2)}
 moreover
 {assume 9: "¬p"
  then have "¬p∨¬q" by (rule disjI1)}
 ultimately show "¬p∨¬q" by (rule disjE)
qed

(* paupeddeg pabrodmac*)
lemma ejercicio_4_6:
  assumes "¬(p ∧ q)"
  shows "¬p ∨ ¬q"
proof -
  have "¬p ∨ p" by (rule excluded_middle)
  thus "¬p ∨ ¬q"
  proof
    { assume "¬p"
     thus "¬p ∨ ¬q" by (rule disjI1)}
  next
    { assume "p"
      have "¬q"
      proof
      { assume "q"
        have "(p ∧ q)" using `p` `q`  by (rule conjI)
        show "False"  using `¬(p ∧ q)` `p ∧ q` by (rule notE)}
      qed
      thus "¬p ∨ ¬q" by (rule disjI2)}
      qed
qed

(* pabrodmac*)
lemma ejercicio_4_7:
  assumes "¬(p ∧ q)"
  shows "¬p ∨ ¬q" 
proof -
  show "¬p ∨ ¬q" using assms by (rule Meson.not_conjD)
qed

(* dancorgar *)
lemma ejercicio_4_8:
  assumes "¬(p ∧ q)"
  shows "¬p ∨ ¬q"
proof-
  {assume "(p ∧ q)"
   have "¬p" using assms `(p ∧ q)` by (rule notE)
   then have "¬p ∨ ¬q"  by (rule disjI1)}
  then show "¬p ∨ ¬q"
  apply simp
  apply (rule ccontr)
  apply simp
  done
qed

(* josgarsan *)
lemma ejercicio_4:
  assumes 1: "¬(p ∧ q)"
  shows "¬p ∨ ¬q"
proof (rule ccontr)
  assume "¬(¬ p ∨ ¬ q)"
  then show False using 1 by simp
qed   

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

(* marcarmor13 jeamacpov serrodcal juancabsou *)
--"usando un supuesto q"
lemma ejercicio_5_1:
  assumes 1: "q" 
  shows "(p ⟶ q) ∨ (q ⟶ p)"
proof-
  have 2: "p ⟶ q" using 1 by (rule impI)
  show "(p ⟶ q) ∨ (q ⟶ p)" using 2  by (rule disjI1)
qed

(* Comentario: Hipótesis extra.*)

(* ivamenjim marpoldia1 ferrenseg fraortmoy rubgonmar antsancab1 *)
lemma ejercicio_5_2:
  shows "(p ⟶ q) ∨ (q ⟶ p)"     
proof -
  {assume 1:"q"
   have "(p ⟶ q)" using 1 by (rule impI)
   then have "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI1)}
   thus "(p ⟶ q) ∨ (q ⟶ p)" by auto
qed  

(* Comentario: Uso de auto. *)

(* danrodcha pablucoto *)
lemma ej_5:
  shows "(p ⟶ q) ∨ (q ⟶ p)"
proof -
  have "¬p ∨ p" by (rule excluded_middle)
  thus "(p ⟶ q) ∨ (q ⟶ p)"
  proof (rule disjE)
    { assume "¬p" 
      have "¬q ∨ q" by (rule excluded_middle)
      thus "(p ⟶ q) ∨ (q ⟶ p)"
      proof (rule disjE)
      {assume "¬q"
        hence "¬p ⟶ ¬q" by (rule impI)
         { assume "q"
           hence "¬¬q" by (rule notnotI)
           with `¬p ⟶ ¬q` have "¬¬p" by (rule mt) 
           hence "p" by (rule notnotD)}
         hence "q ⟶ p" by (rule impI)
         thus "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI2)}
      next
      {assume "q"
        hence "(p ⟶ q)" by (rule impI)
        thus "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI1)}
      qed}
    next
    {assume "p"
     hence "q ⟶ p" by (rule impI)
     thus "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI2)}
    qed
qed

(* anaprarod *)
(* Muy parecida a la anterior pero con algunas etiquetas
   y con algunas implicaciones más detalladas *)
lemma ejercicio_5_3:
  shows "(p ⟶ q) ∨ (q ⟶ p)"
proof-
  have "¬p ∨ p" by (rule excluded_middle)
  thus "(p ⟶ q) ∨ (q ⟶ p)"
  proof (rule disjE)
    {assume "¬p"
      have "¬q ∨ q" by (rule excluded_middle)
      thus "(p ⟶ q) ∨ (q ⟶ p)"
      proof (rule disjE)
        {assume  "¬q"
          hence 1: "¬p ⟶ ¬q" by (rule impI) 
          {assume "q"
            hence 2: "¬¬q" by (rule notnotI)
            have "¬¬p" using 1 2 by (rule mt)
            hence "p" by (rule notnotD)}
          hence "q ⟶ p" by (rule impI)
          thus "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI2)}
        next
        {assume 3: "q"
          {assume "p"
            have "q" using 3 by this}
          hence "p ⟶ q" by (rule impI)
          thus "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI1)}
        qed}
    next
    {assume 4: "p"
      {assume "q"
        have "p" using 4 by this}
      hence "q ⟶ p" by (rule impI)
      thus "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI2)}
    qed
qed

(* migtermor *)
lemma ejercicio_5_4:             
  shows "(p ⟶ q) ∨ (q ⟶ p)"
proof -
 have 1: "q∨¬q" by (rule lem)
 moreover 
 {assume 2: "q"   
  have 3: "p ⟶ q" using 2 by (rule impI)
  then have 4: "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI1)}
 moreover
 {assume 5: "¬q"   
  have 6: "¬p⟶¬q" using 5 by (rule impI)
  then have 7: "q⟶p" by (rule ejercicio_1_2)
  then have "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI2)}
 ultimately show "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjE)
qed

(* paupeddeg pabrodmac crigomgom bowma *)
lemma aux3:
  assumes "¬q ∨ p"
  shows "q ⟶ p"
proof -
note `¬q ∨ p`
moreover
 {assume "¬q"
   have "q ⟶ p"
   proof
    assume "q" 
    show "p" using `¬q``q`by (rule notE)
    qed} 
moreover
 {assume "p"
   have "q ⟶ p"
   proof
    assume "q"
    show "p" using `p` by this
    qed}
ultimately show "q ⟶ p" by (rule disjE)
qed    
        
lemma ejercicio_5_5:
  shows "(p ⟶ q) ∨ (q ⟶ p)"
proof -
  have "¬p ∨ p" by (rule excluded_middle) 
  thus "(p ⟶ q) ∨ (q ⟶ p)"
  proof
    {assume "¬p"
     hence "¬p ∨ q" by (rule disjI1)
     hence "p ⟶ q" by (rule aux3)
     thus "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI1)} 
    {assume "p"
     hence "¬q ∨ p" by (rule disjI2)
     hence "q ⟶ p" by (rule aux3)
     thus "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI2)} 
  qed
qed

(*pabrodmac*)       
lemma ejercicio_5_6: 
  "(p ⟶ q) ∨ (q ⟶ p)"
proof -
  have "¬(p ⟶ q) ∨ (p ⟶ q)" by (rule excluded_middle)
  thus "(p ⟶ q) ∨ (q ⟶ p)"
  proof 
    { assume "¬(p ⟶ q)"
      hence "p ∧ ¬ q" by (rule Meson.not_impD)
      have "(q ⟶ p)"
      proof
      assume "q"
      show "p" using `p ∧ ¬ q` by (rule conjunct1)
      qed
      thus "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI2) }
  next
    { assume "p ⟶ q"
     then show "(p ⟶ q) ∨ (q ⟶ p)"  by (rule disjI1) }
  qed
qed 

(* josgarsan *)
lemma ejercicio_5_7:
  shows "(p ⟶ q) ∨ (q ⟶ p)"
proof (cases)
  assume "p"
  then show "(p ⟶ q) ∨ (q ⟶ p)" by simp
next
  assume "¬p"
  then show "(p ⟶ q) ∨ (q ⟶ p)" by simp
qed

(* Comentario: Uso de simp. *)

(* dancorgar *)
lemma ejercicio_5_8:
  shows "(p ⟶ q) ∨ (q ⟶ p)"
proof (cases)
  assume "p"
  have "(q ⟶ p)" using `p` by (rule impI)
  then show "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI2)
next
  assume "¬p"
  have "(p ⟶ q)" using `¬p` by simp
  then show "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI1)
qed  

end