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 5:"r" using 4 2 by (rule mp)}
    then have "p⟶r" by (rule impI)}
  then show "q⟶(p⟶r)" by (rule impI)
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

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

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

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

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

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

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
end