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

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"
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

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

-- "irealetei"
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


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

-- "irealetei"
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"
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

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

-- "irealetei"
lemma ej4_auto:
  assumes "(p ⟶ q) ⟶ r"
  shows  "p ⟶ (q ⟶ r)"
using assms by auto
section {* Conjunciones *}

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

-- "irealetei"
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

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

-- "irealetei"
lemma ej6_auto:
  assumes  "p ⟶ q ∧ r"
  shows  "(p ⟶ q) ∧ (p ⟶ r)"
using assms by auto

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

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

-- "irealetei"
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


section {* Disyunciones *}

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

-- "irealetei"
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

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

-- "irealetei"
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

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

-- "irealetei"
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

end