Relación 9

header {* R9: Deducción natural proposicional (1) *}

theory R9
imports Main 
begin

text {*
  --------------------------------------------------------------------- 
  El objetivo de esta relación es lemas usando sólo las reglas básicas
  de deducción natural de la lógica proposicional. 

  Las reglas básicas de la deducción natural necesarias son las1
  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 
  --------------------------------------------------------------------- 
*}

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 ⟶ r) ⊢ q ⟶ (p ⟶ r)
  ------------------------------------------------------------------ *}

-- "irealetei,julrobrel, pabflomar juaruipav domlloriv jaisalmen zoiruicha"
lemma ej1_auto:
  assumes "p ⟶ (q ⟶ r)"
  shows "q ⟶ (p ⟶ r)"
using assms
by auto

lemma ej1:
  assumes 1:"p ⟶ (q ⟶ r)"
  shows "q ⟶ (p ⟶ r)"
proof -
  {assume 2:"q"
    {assume 3:"p"
      have 4:"q⟶r" using 1 3 by (rule mp)
      have "r" using 4 2 by (rule mp)}
    then have "p⟶r" by (rule impI)}
  then show "q⟶(p⟶r)" by (rule impI)
qed

-- "diecabmen1"
lemma Ejercicio_1:
  assumes "p ⟶ (q ⟶ r)"
  shows "q ⟶ (p ⟶ r)"
proof -
  { assume "q"
    { assume "p"
      with assms have "q ⟶ r"  ..
      then have "r" using `q` ..  }
    then have "p ⟶ r" ..  }
    then show "q ⟶ (p ⟶ r)" ..
qed

-- "maresccas4"
lemma 
   assumes "p ⟶ (q ⟶ r)"
   shows "q ⟶ (p ⟶ r)"
proof
   assume "q"
   show "p ⟶ r"
   proof 
     assume "p"
     with `p ⟶ (q ⟶ r)` have "q ⟶ r" ..
     thus "r" using `q`..
   qed
qed


--"marescpla"

  lemma 01:
  assumes "p⟶(q⟶r)"
  shows "q ⟶ (p⟶r)"
 proof-
    {assume 1: "q"
      {assume 2: "p"
        have "q⟶r" using assms(1) 2  by (rule mp)
        then have "r" using 1 by (rule mp)}
      then have "p⟶r" ..}
    then show "q ⟶(p⟶r)" by (rule impI)
    qed



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

-- "irealetei,julrobrel, pabflomar, domlloriv jaisalmen zoiruicha"
lemma ej2_auto:
  assumes " p ⟶ (q ⟶ r)"
  shows "(p ⟶ q) ⟶ (p ⟶ r)"
using assms by auto

lemma ej2:
  assumes 1:" p ⟶ (q ⟶ r)"
  shows "(p ⟶ q) ⟶ (p ⟶ r)"
proof - 
 {assume 2:"(p ⟶ q)"
    {assume 3:"p"
      have 4:"q" using 2 3 by (rule mp)
      have 5:"q⟶r" using 1 3 by (rule mp)
      have "r" using 5 4 by (rule mp)}
    then have "p⟶r" by (rule impI)}
  then show "(p ⟶ q)⟶(p⟶r)" by (rule impI)
qed

-- "diecabmen1"
lemma Ejercicio_2:
  assumes "p ⟶ (q ⟶ r)"
  shows   "(p ⟶ q) ⟶ (p ⟶ r)"
proof 
  assume "p ⟶ q"
  show "p ⟶ r"
  proof
    assume "p"
    with  `p ⟶ q` have "q" ..
    have "q ⟶ r" using assms `p` ..
    then show "r" using `q` ..
  qed
qed

-- "maresccas4"
lemma 
  assumes "p ⟶ (q ⟶ r)"
  shows "(p ⟶ q) ⟶ (p ⟶ r)"
proof
  assume "p ⟶ q"
  show "p ⟶ r"
  proof
    assume "p"
    have "q" using `p ⟶ q` `p` ..
    have "q ⟶ r" using `p ⟶ (q ⟶ r)` `p` .. 
    show "r" using `q ⟶ r` `q`  ..
  qed
qed


--"marescpla"

  lemma 02:
  assumes "p⟶(q⟶r)"
  shows "(p⟶q) ⟶ (p⟶r)"
 proof-
    {assume 1: "p⟶q"
      {assume 2: "p"
        have "q" using 1 2 by (rule mp)
        have "q⟶r" using assms(1) 2 by (rule mp)
         then have "r" using `q` by (rule mp)}
      then have "p⟶r"..}
    then show "(p⟶q) ⟶ (p⟶r)" ..
  qed

-- "juaruipav"
lemma ej2-jua: 
assumes 1: " p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
proof 
  assume 2: " p ⟶ q"
  show "p ⟶ r"
    proof 
      assume 3: "p"
      have 4: "q" using 2 3 by (rule mp)
      have 5: "q⟶r" using 1 3 by (rule mp)
      show "r" using 5 4 by (rule mp)
    qed
qed

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

-- "irealetei, domlloriv, pabflomar jaisalmen zoiruicha"
lemma ej3_auto:"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
 by auto

lemma ej3:"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof - 
 { assume 1:"(p⟶(q⟶r))"
     {assume 3:"p⟶q"
       {assume 4:"p"
         have 5: "q⟶r" using 1 4 by (rule mp)
         have 6:"q" using 3 4 by (rule mp)
         have "r" using 5 6 by (rule mp)}
       then have "p⟶r" by (rule impI)}
     then have "(p⟶q)⟶p⟶r" by (rule impI)}
  then show "(p⟶(q⟶r))⟶((p⟶q)⟶p⟶r)" by (rule impI)  
qed

-- "diecabmen1, maresccas4"
lemma Ejercicio_3:
  "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof
  assume "p ⟶ q ⟶ r"
  show "(p ⟶ q) ⟶ p ⟶ r"
  proof 
    assume "p ⟶ q"
    show "p ⟶ r"
    proof
      assume "p"
      with  `p ⟶ q` have "q" ..
      have "q ⟶ r" using `p ⟶ q ⟶ r` `p` ..
      then show "r" using `q` ..
    qed
  qed
qed

--"julrobrel"
lemma ejer_3_auto:
  shows "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
by auto

thm ej2_auto

lemma ejer_3_detalle:
  shows "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof -
  show "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))" using ej2_auto by (rule impI)
qed


--"marescpla"
 lemma 03:
   "(p ⟶ (q ⟶ r))⟶((p ⟶ q) ⟶ (p ⟶ r))"
 proof-
   {assume 1: "(p ⟶ (q ⟶ r))"
    {assume 2: "(p ⟶ q)"
      {assume 3: "p"
        have "q" using 2 3 by (rule mp)
        have "q ⟶r" using 1 3 by (rule mp)
        then have "r" using `q` by (rule mp)}
      then have"p⟶r" by (rule impI)}
    then have "((p ⟶ q) ⟶ (p ⟶ r))" by (rule impI)}
   then show "(p ⟶ (q ⟶ r))⟶((p ⟶ q) ⟶ (p ⟶ r))" by (rule impI)
   qed

--"juaruipav"

lemma ej3-jua:  " (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof
    assume 1: "p ⟶ q ⟶ r"
    show "(p ⟶ q) ⟶ p ⟶ r"
    proof
        assume 2: "p⟶q"
        show "p ⟶ r"
        proof
           assume 3: "p"
           have 4:"q" using 2 3 ..
           have 5: "q⟶r" using 1 3  by (rule mp)
           show "r" using 5 4 ..
       qed
  qed
qed

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

-- "irealetei,julrobrel, domlloriv jaisalmen zoiruicha"
lemma ej4_auto:
  assumes "(p ⟶ q) ⟶ r"
  shows  "p ⟶ (q ⟶ r)"
using assms by auto

-- "maresccas4"
lemma
  assumes "(p ⟶ q) ⟶ r"
  shows "p ⟶ (q ⟶ r)"
proof
  assume "p"
  show "q ⟶ r"
  proof 
    assume "q"
    hence "p ⟶ q" ..
    show "r" using `(p ⟶ q) ⟶ r` `p ⟶ q` ..
  qed
qed

-- "juaruipav irealetei"
lemma ej4-jua: 
assumes 1: "(p ⟶ q) ⟶ r"
shows " p ⟶ (q ⟶ r)"
proof 
  assume 2: "p"
  show "q⟶r"
  proof
    assume 3: "q"
    have 4: "p⟶q" using 3 by (rule impI)
    show "r" using 1 4 by (rule mp)
    qed
qed

--"marescpla"
    lemma 04:
  assumes "(p ⟶ q) ⟶ r"
  shows "p ⟶ (q ⟶ r)"
 proof-
    {assume 1: "p"
      {assume 2: "q"
        then have "r" using 1 2 assms by simp}
      then have "q⟶r" by (rule impI)}
    then show "p⟶ (q ⟶ r)" by (rule impI)
   qed

section {* Conjunciones *}

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

-- "irealetei,julrobrel, domlloriv jaisalmen zoiruicha"
lemma ej5_auto:
  assumes "(p ⟶ q) ∧ (p ⟶ r)"
  shows  "p ⟶ q ∧ r"
using assms by auto

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

-- "diecabmen1, maresccas4"
lemma Ejercicio_5:
  assumes "(p ⟶ q) ∧ (p ⟶ r)"
  shows "p ⟶ q ∧ r"
proof
  assume "p"
  have "(p ⟶ q)" using assms ..
  then have "q" using `p` ..
  have "(p ⟶ r)" using assms ..
  then have "r" using `p` ..
  with `q` show "q ∧ r" ..
qed

--"julrobrel, pabflomar, marescpla(Pero usando assms en vez de la etiqueta 0)"
lemma ejer_5_detalle:
  assumes 0:"(p ⟶ q) ∧ (p ⟶ r)"
  shows "p ⟶ q ∧ r"
proof -
  have 1:"p⟶q" using 0 by (rule conjunct1)
  have 2:"p⟶r" using 0 by (rule conjunct2)
  {assume 3:"p"
     have 4:"q" using 1 3 by (rule mp)
     have 5:"r" using 2 3 by (rule mp)
     have 6:"q ∧ r" using 4 5 by (rule conjI)
  }then show "p ⟶ q ∧ r" by (rule impI)
qed

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


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

-- "irealetei,julrobrel jaisalmen zoiruicha"
lemma ej6_auto:
  assumes  "p ⟶ q ∧ r"
  shows  "(p ⟶ q) ∧ (p ⟶ r)"
using assms by auto
-- "pabflomar"
{* Me he peleado un buen rato intentando asumiendo solo una vez p. Al mirar el wiki y tal vi esta versión que hace lo que yo quería hacer usando sólo una ves una asumción. ¿Cómo se hace?
*}
lemma ej6:
  assumes  1:"p ⟶ q ∧ r"
  shows  "(p ⟶ q) ∧ (p ⟶ r)"
proof -
  {assume 2:"p"
    have 3:"q∧r" using 1 2 by (rule mp)
    have "q" using 3 by (rule conjunct1)}
    then have 4:"p⟶q"  by (rule impI)
  {assume 5:"p"
    have 6:"q∧r" using 1 5 by (rule mp)
    have "r" using 6 by (rule conjunct2)}
    then have 5:"p⟶r"  by (rule impI)
  show "(p⟶q) ∧ (p ⟶r)" using 4 5 by (rule conjI)
qed

-- "diecabmen1, maresccas4, domlloriv"
lemma Ejercicio_6:
  assumes "p ⟶ q ∧ r"
  shows "(p ⟶ q) ∧ (p ⟶ r)"
proof
  {assume "p"
  with assms have "q ∧ r" ..
  then have "q" ..}
  then show "p ⟶ q" ..
  {assume "p"
  with assms have "q ∧ r" ..
  then have "r" ..}
  then show "p ⟶ r" ..
qed

--"juaruipav"
lemma ej6-jua: 
assumes 1: " p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof
  {assume 2: "p"
   have 3:"q∧r" using 1 2 by (rule mp)
   have  "q" using 3 by (rule conjunct1)}
   then show "p⟶q" ..
  next
  {assume 5: "p"
   have 6:"q∧r" using 1 5 by (rule mp)
   have  "r" using 6 by (rule conjunct2)}
   then show "p⟶r" ..
qed

--"marescpla"
   lemma 06:
 assumes "p ⟶ q ∧ r"
 shows "(p ⟶ q) ∧ (p ⟶ r)"
 proof-
 {assume "p"
   with assms have "q ∧ r" by (rule mp)
   then have "q" by (rule conjunct1)}
   then have C: "p⟶q" by (rule impI)
 {assume "p"
   with assms have "q ∧ r" by (rule mp)
   have "r" using `q ∧ r` by (rule conjunct2)}
   then have "p ⟶ r" by (rule impI)
   with C show "(p ⟶ q) ∧ (p ⟶ r)" by (rule conjI)
 qed


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

-- "irealetei,julrobrel, pabflomar, domlloriv jaisalmen, zoiruicha"
lemma ej7_auto:
  assumes " p ∧ (q ⟶ r)"
  shows  "(p ⟶ q) ⟶ r"
using assms by auto

lemma ej7:
  assumes 1:" p ∧ (q ⟶ r)"
  shows  "(p ⟶ q) ⟶ r"
proof -
  have 2:"p" using 1 by (rule conjunct1)
  have 3:"q⟶r"  using 1 by (rule conjunct2)
  {assume 4:"p⟶q"
    have 5:"q" using 4 2 by (rule mp)
    have "r" using 3 5 by (rule mp)}
  then show "(p⟶q)⟶r" by (rule impI)
qed



-- "diecabmen1, maresccas4"
lemma Ejercicio_7:
  assumes "p ∧ (q ⟶ r)"
  shows "(p ⟶ q) ⟶ r"
proof
  assume "p ⟶ q"
  have "p" using assms  ..
  with `p ⟶ q` have "q" ..
  have "q ⟶ r" using assms ..
  then show "r" using `q` ..
qed


-- "juaruipav"
lemma ej7:
assumes 1: " p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
proof
  assume 2: " p ⟶ q "
  have 3:"p" using 1 by (rule conjunct1)
  have 4:"q⟶r" using 1 by (rule conjunct2)
  have 5:"q" using 2 3 by (rule mp)
  show "r" using 4 5 by (rule mp)
qed


--"marescpla"

   lemma 07:
 assumes "p ∧ (q ⟶ r)"
 shows "(p ⟶ q) ⟶ r"
 proof-
 {assume H: "(p ⟶ q)"
   have "p" using assms by (rule conjunct1)
   with H have "q"  by (rule mp)
   have "q⟶r" using assms by (rule conjunct2)
   then have "r" using `q` by (rule mp)}
 then show "(p ⟶ q) ⟶ r" by (rule impI)
 qed



section {* Disyunciones *}

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

-- "irealetei diecabmen1, julrobrel, jaisalmen, zoiruicha"
lemma ej8_auto:
  assumes "q ⟶ r"
  shows  "p ∨ q ⟶ p ∨ r"
using assms by auto

lemma ej8:
  assumes 1:"q ⟶ r"
  shows  "p ∨ q ⟶ p ∨ r"
proof -
  {assume 2:"p ∨ q"
    moreover
       {assume "p"
        then have "p ∨ r" by (rule disjI1)}
    moreover
      {assume 3:"q"
        have "r" using 1 3 by (rule mp)
        then have "p ∨ r" by (rule disjI2)}
    ultimately have "p ∨ r"  by (rule disjE)}
  then show "p ∨ q ⟶ p ∨ r" by (rule impI)
qed

--"julrobrel: no estoy seguro de que esto esté bien"
lemma ejer_8_detallado2:
   assumes 0:"q ⟶ r"
   shows   "p ∨ q ⟶ p ∨ r"
proof (cases)
  assume "¬p"
  show   "p ∨ q ⟶ p ∨ r" using 0 by simp
next
  assume "¬¬p"
  show   "p ∨ q ⟶ p ∨ r" using 0 by simp
qed

-- "maresccas4"
lemma 
  assumes "q ⟶ r"
  shows "(p ∨ q) ⟶ (p ∨ r)"
proof 
  assume "p ∨ q"
  thus "p ∨ r"
  proof 
    { assume "p"
      thus "p ∨ r" .. }
  next
    { assume "q"
      have "r" using assms `q` ..
      thus "p ∨ r" .. }
  qed
qed 

--"juaruipav: Si quito el moreover no pasa nada.. ¿y eso? tengo dos objetivos en proof"
lemma ej8: 
assumes 1: "  q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof 
  assume 2:"p ∨ q"
  thus " p ∨ r"
  proof 
    {assume 3: "p"
    then show  "p ∨ r" ..} 
moreover
   { assume 4: "q"
    have "r" using 1 4  by (rule mp)
    then show "p ∨ r" ..}
qed
qed


--"marescpla"

lemma 08:
    assumes "q⟶r"
    shows "p ∨ q ⟶ p ∨ r"
  proof-
  {assume 1: "p ∨ q"
    {assume "p"
      then have "p ∨ r" by (rule disjI1)}
    then have 2: "p⟹p ∨ r" by simp
    {assume q
      with assms have "r" by (rule mp)
      then have "p ∨ r" by (rule disjI2)}
    then have 3: "q⟹p ∨ r" by simp
    have "p ∨ q ⟹ p ∨ r" using 1 2 3 by (rule disjE)}
  then show "p ∨ q ⟶ p ∨ r" by (rule impI)
  qed



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

-- "irealetei diecabmen1, julrobrel, domlloriv, jaisamlem, zoiruicha"
lemma ej9_auto:
  assumes  "(p ⟶ r) ∧ (q ⟶ r)"
  shows   "p ∨ q ⟶ r"
using assms by auto

lemma ej9:
  assumes 1:"(p ⟶ r) ∧ (q ⟶ r)"
  shows   "p ∨ q ⟶ r"
proof -
  {assume  "p ∨ q "
  moreover 
    {assume 2:"p"
      have 3:"(p ⟶ r)" using 1 by (rule conjunct1) 
      have "r" using 3 2 by (rule mp)}
  moreover
    {assume 4:"q"
      have 5:"(q ⟶ r)" using 1 by (rule conjunct2)
      have "r" using 5 4 by (rule mp)}
  ultimately have  "r" ..}
  then show "p ∨ q ⟶ r" by (rule impI)
qed

lemma ejer_9_detalle:
   assumes 0:"(p ⟶ r) ∧ (q ⟶ r)" 
   shows "p ∨ q ⟶ r"
proof -
  {assume 1:"p∨q"
    moreover
    {assume 2:"p"
      have  3:"p⟶r" using 0 by (rule conjunct1)
      have  4:"r" using 3 2 by (rule mp)}
    moreover
    {assume 5:"q"
       have 6:"q⟶r" using 0 by (rule conjunct2)
       have 7:"r" using 6 5 by (rule mp)}
    ultimately have 8:"r" by (rule disjE)}
  then show "p ∨ q ⟶ r" by (rule impI)
qed

-- "maresccas4"
lemma
  assumes "(p ⟶ r) ∧ (q ⟶ r)"
  shows "p ∨ q ⟶ r"
proof 
  assume "p ∨ q"
  thus "r"
  proof 
    { assume "p"
      have "p ⟶ r" using assms ..
      thus "r" using `p` ..}
  next
    { assume "q"
      have "q ⟶ r" using assms ..
      thus "r" using `q`..}
  qed
qed

--"juaruipav"
lemma ej9: 
assumes 1:  "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
proof
  assume 2:  "p ∨ q"
  thus "r"
  proof
    {assume 3: "p"
     have 4: "p⟶r" using 1 by (rule conjunct1)
     show "r" using 4 3 by (rule mp)}
  moreover
     {assume 5: "q"
     have 6: "q⟶r" using 1 by (rule conjunct2)
     show "r" using 6 5 by (rule mp)}
  qed
qed  


--"marescpla"
  lemma 09:
    assumes "(p ⟶ r) ∧ (q ⟶ r)"
    shows "p ∨ q ⟶ r"
  proof-
  have "p⟶r" using assms by (rule conjunct1)
  have "q ⟶ r" using assms by (rule conjunct2)
  {assume 1: "p ∨ q"
    {assume "p"
      with `p⟶r` have "r" by (rule mp)}
  then have 2: "p⟹r" by simp
    {assume "q"
      with `q⟶r` have "r" by (rule mp)}
  then have 3: "q⟹r" by simp
  have "p ∨ q ⟹ r" using 1 2 3 by (rule disjE)}
  then show "p ∨ q ⟶ r" by (rule impI)
  qed



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

-- "irealetei diecabmen1, julrobrel, domlloriv, jaisalmen zoiruicha"
lemma ej10_auto:
  assumes  "p ∨ q ⟶ r"
  shows   "(p ⟶ r) ∧ (q ⟶ r)"
using assms by auto

lemma ej10:
  assumes  1:"p ∨ q ⟶ r"
  shows   "(p ⟶ r) ∧ (q ⟶ r)"
proof -
  {assume 2:"p"
    have 3:"p∨q" using 2 by (rule disjI1)
    have "r" using 1 3 by (rule mp)}
    then have 4:"p⟶r" by (rule impI)
  {assume 5:"q"
    have 6:"p∨q" using 5 by (rule disjI2)
    have 7:"r" using 1 6 by (rule mp)}
    then have 8:"q⟶r"  by (rule impI)
  show "(p⟶r)∧(q⟶r)" using 4 8 by (rule conjI)
qed

-- "maresccas4"
lemma
  assumes "p ∨ q ⟶ r"
  shows "(p ⟶ r) ∧ (q ⟶ r)"
proof
  { assume "p"
    have "p ∨ q" using `p` ..
    have "r" using assms `p ∨ q` ..}
  then show "p ⟶ r" ..
next
  { assume "q"
    have "p ∨ q" using `q` ..
    have "r" using assms `p ∨ q` ..}
  thus "q ⟶ r" ..
qed

--"juaruipav, pabflomar"
lemma ej10:
assumes 1:" p ∨ q ⟶ r" 
shows "(p ⟶ r) ∧ (q ⟶ r)"
proof
  {assume 2 :"p"
    have 3:  "p ∨ q" using 2 by (rule disjI1)
    have 4: "r" using 1 3 by (rule mp)}
    then show "p⟶r" .. 
moreover
  {assume 5 :"q"
    have 6:  "p ∨ q" using 5 by (rule disjI2)
    have 7: "r" using 1 6 by (rule mp)}
    then show "q⟶r" ..
qed

--"marescpla"
  lemma 10:
    assumes "p ∨ q ⟶ r"
    shows"(p ⟶ r) ∧ (q ⟶ r)"
  proof-
  {assume "p"
    then have "r" using assms by simp}
  then have 1: "p⟶r" by (rule impI)
  {assume "q"
    then have "r" using assms by simp}
  then have 2: "q⟶r" by (rule impI)
  show "(p ⟶ r) ∧ (q ⟶ r)" using 1 2 by (rule conjI)
  qed

end