Relación 10

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

theory R10
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. 

  Los ejercicios son los de la asignatura de "Lógica informática" que se
  encuentran en http://goo.gl/yrPLn

  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
  · excluded_middle: ¬P ∨ 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

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

--"marescpla, pabflomar"

  lemma 01:
  assumes 1: "p ∨ q"
      and 2: "¬q"
  shows "p"
  using 1
  proof (rule disjE)
     {assume "p"  
        then show "p".}
     next
     {assume "q"
        with 2 show "p" by (rule notE)}
  qed

--"diecabmen1 maresccas4"
lemma Ejercicio_1:
  assumes "p ∨ q"
          "¬q"
  shows   "p"
  using assms(1)
proof (rule disjE)
  assume "p"
  then show "p" .
next
  assume "q"
  with `¬q` show "p" ..
qed

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

--"marescpla, pabflomar"

 lemma 02:
   assumes "p ∧ q"
   shows "¬(¬p ∨ ¬q)"
 proof (rule ccontr)
   assume "¬¬(¬p ∨ ¬q)"
   then have 1: "(¬p ∨ ¬q)" by (rule notnotD)
   show "False"
     using 1
     proof (rule disjE)
        {assume I: "¬p"
         have "p" using assms(1) by (rule conjunct1)
         with I show "False"..}
        {assume II: "¬q"
          have "q" using assms(1) by (rule conjunct2)
      with II show "False" ..}
     qed
   qed

--"diecabmen1 maresccas4"
lemma Ejercicio_2:
  assumes "p ∧ q"
  shows   "¬(¬p ∨ ¬q)"
proof 
  assume 1: "¬p ∨ ¬q"
  show False
  using 1
  proof (rule disjE)
    assume "¬p"
    have "p" using assms ..
    with `¬p` show False ..
  next
    assume "¬q"
    have "q" using assms ..
    with `¬q` show False ..
  qed
qed

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

-- "maresccas4"
lemma
  assumes "¬(p ∨ q)"
  shows "¬p ∧ ¬q"
proof
  { assume "p"
    then have "p ∨ q" ..
    with `¬(p ∨ q)` have False ..}
  thus "¬p" ..
next
  { assume "q"
    then have "p ∨ q" ..
    with `¬(p ∨ q)` have False ..}
  thus  "¬q" ..
qed

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

-- "maresccas4"
lemma 
  assumes "¬p ∧ ¬q"
  shows "¬(p ∨ q)"
proof
 assume "p ∨ q"
 show False
 using `p ∨ q`
 proof
   assume "p"
   have "¬p" using `¬p ∧ ¬q` ..
   thus False using `p` ..
 next
   assume "q"
   have "¬q" using `¬p ∧ ¬q` ..
   thus False using `q` ..
 qed
qed

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

-- "maresccas4"
lemma
  assumes "¬p ∨ ¬q"
  shows "¬(p ∧ q)"
proof
  assume "p ∧ q"
  show False
  using `¬p ∨ ¬q`
  proof
    assume "¬p"
    have "p" using `p ∧ q` ..
    with `¬p`show False ..
  next
    assume "¬q"
    have "q" using `p ∧ q` ..
    with `¬q` show False ..
  qed
qed

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

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

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

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

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

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

end