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

-- "diecabmen1 pabflomar"
lemma Ejercicio_3:
  assumes "¬(p ∨ q)"
  shows   "¬p ∧ ¬q"
proof -
  { assume "p"
    then have "p ∨ q" ..
    with assms have False ..}
  then have "¬p" ..
  { assume "q"
    then have "p ∨ q" ..
    with  assms have False ..}
  then have "¬q" ..
  with `¬p` show "¬p ∧ ¬q" ..
qed


--"marescpla"
  lemma 03:
      assumes 1:"¬(p ∨ q)"
      shows "¬p ∧ ¬q"
  proof
  show "¬p"
    proof (rule ccontr)
    {assume "¬¬p"
      then have "p" by (rule notnotD)
      then have "p ∨ q" by (rule disjI1)
      with 1 show "False" ..}
    qed 
  show "¬q"
    proof (rule ccontr)
    {assume "¬¬q"
      then have "q" by (rule notnotD)
      then have "p ∨ q" by (rule disjI2)
      with 1 show "False" ..}
    qed
  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

-- "diecabmen1"
lemma Ejercicio_4:
  assumes "¬p ∧ ¬q"
  shows   "¬(p ∨ q)"
proof
  assume "p ∨ q"
  show False
  using `p ∨ q`
  proof
    assume "p"
    have "¬p" using assms ..
    then show False using `p` ..
  next
    assume "q"
    have "¬q" using assms ..
    then show False using `q` ..
  qed
qed


--"marescpla"
  lemma 04:
      assumes 1:"¬p ∧ ¬q"
      shows "¬(p ∨ q)"
   proof (rule ccontr)
      have 2: "¬p" using 1 by (rule conjunct1)
      have 3: "¬q" using 1 by (rule conjunct2)
      assume "¬¬(p ∨ q)"
       then have 4:"(p ∨ q)" by (rule notnotD)
       then show False
         proof (rule disjE)
           note 4
           {assume "p"
             with 2 show False ..}
           {assume "q"
             with 3 show False ..}
         qed
   qed

-- "pabflomar"

lemma ej4_pfm:
  assumes 0:"¬p ∧ ¬q"
  shows "¬(p ∨ q)"
proof 
  assume 1:"p ∨ q"
  show False
  using 1
  proof 
    assume 1:"p"
    have 2: "¬p" using 0 by (rule conjunct1)
    then show False using `p` ..
    next
    assume 1:"q"
    have 2: "¬q" using 0 by (rule conjunct2)
    then show False using `q` ..
  qed
qed
text {* --------------------------------------------------------------- 
  Ejercicio 5. Demostrar
     ¬p ∨ ¬q ⊢ ¬(p ∧ q)
  ------------------------------------------------------------------ *}

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


--"marescpla"

  lemma 05:
      assumes 1:"¬p ∨ ¬q"
      shows "¬(p ∧ q)"
   proof (rule ccontr)
       assume "¬¬(p ∧ q)"
       then have 4:"(p ∧ q)" by (rule notnotD)
       have p using 4 by (rule conjunct1)
       have q using 4 by (rule conjunct2)
       show False
       using 1
       proof (rule disjE)
          {assume "¬p"
            then show False using `p` ..}
          {assume "¬q"
            then show False using `q`..}
       qed
   qed


-- "pabflomar"
lemma ej5_pfm:
  assumes "¬p ∨ ¬q"
  shows "¬(p ∧ q)"
proof 
  assume "p ∧ q"
  show False
  using `¬p ∨ ¬q`
  proof 
    assume "¬p"
    have "p" using `p ∧ q` by (rule conjunct1)
    with `¬p` show False by (rule notE)
    next
    assume "¬q"
    have "q" using `p ∧ q` by (rule conjunct2)
    with `¬q` show False by (rule notE)
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 6. Demostrar
     ⊢ ((p ⟶ q) ⟶ p) ⟶ p
  ------------------------------------------------------------------ *}
-- "diecabmen1 maresccas4 pabflomar"
lemma Ejercicio_6:
  shows "((p ⟶ q) ⟶ p) ⟶ p"
proof
  assume "(p ⟶ q) ⟶ p"
  show "p"
  proof (rule ccontr)
    assume "¬p"
    with `(p ⟶ q) ⟶ p` have "¬(p ⟶ q)" by (rule mt)
    { assume "p"
      with `¬p` have False ..
      then have "q" ..}
    then have "p ⟶ q" ..
    with `¬(p ⟶ q)` show False ..
  qed
qed


--"marescpla"

  lemma 06:
     "((p ⟶ q) ⟶ p) ⟶ p"     
   proof
     assume 1: "((p ⟶ q) ⟶ p)"
     show "p"
     proof(rule ccontr)
        assume "¬p"
        with 1 have 2: "¬(p⟶q)" by (rule mt)
        then show "False"
        proof
           {assume "p"
             with `¬p` have "q" by (rule notE)}
           then show "(p⟶q)" by (rule impI)
        qed
     qed
  qed


text {* --------------------------------------------------------------- 
  Ejercicio 7. Demostrar
     ¬q ⟶ ¬p ⊢ p ⟶ q
  ------------------------------------------------------------------ *}
-- "diecabmen1 pabflomar"
lemma Ejercicio_7:
  assumes "¬q ⟶ ¬p"
  shows "p ⟶ q"
proof
  assume "p"
  { assume "¬q"
    with assms have "¬p" ..
    then have False using `p` ..}
  then show "q" by (rule ccontr)
qed


--"marescpla"
  lemma 07:
    assumes "¬q ⟶ ¬p"
    shows "p ⟶ q"
  proof (rule impI)
    {assume 1: "p"
          {assume "¬q"
            with assms have "¬p" ..
            then have "False" using 1 ..}
     then have "¬¬q" by (rule notI)
     then show "q" by (rule notnotD)}
  qed

-- "maresccas4"
lemma
  assumes "¬q ⟶ ¬p"
  shows "p ⟶ q"
proof
  assume "p"
  then have "¬¬p" by (rule notnotI)
  with assms(1) have "¬¬q" by (rule mt)
  then show "q" by (rule notnotD)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 8. Demostrar
     ¬(¬p ∧ ¬q) ⊢ p ∨ q
  ------------------------------------------------------------------ *}
-- "diecabmen1"
lemma Ejercicio_8:
  assumes "¬(¬p ∧ ¬q)"
  shows   "p ∨ q"
proof -
  have "¬p ∨ p" ..
  { assume "p"
    then have "p ∨ q" ..}
  { assume "¬p"
    have "¬q ∨ q" ..
    { assume "q"
      then have "p ∨ q" ..}
    { assume "¬q"
      with `¬p` have "¬p ∧ ¬q" ..
      with assms have False ..
      then have "p ∨ q" ..}
    with `¬q ∨ q` have "p ∨ q" using `q ⟹ p ∨ q` ..}
  with `¬p ∨ p` show "p ∨ q" using `p ⟹ p ∨ q` ..
qed



--"marescpla pabflomar (No se usar otro lema sin usar el simp) maresccas4 (rule 03, en lugar de simp)"
{* Marco lleva razón. GRACIAS!!! *}

  lemma 08:
    assumes "¬(¬p ∧ ¬q)"
    shows "p ∨ q"
  proof (rule ccontr)
    assume "¬(p ∨ q)"
    then have "¬p ∧ ¬q" by (rule 03)
    with assms show "False" ..
  qed



text {* --------------------------------------------------------------- 
  Ejercicio 9. Demostrar
     ¬(¬p ∨ ¬q) ⊢ p ∧ q
  ------------------------------------------------------------------ *}
-- "diecabmen1, maresccas4"
lemma Ejercicio_9:
  assumes "¬(¬p ∨ ¬q)"
  shows   "p ∧ q"
proof
  { assume "¬p"
    then have "¬p ∨ ¬q" ..
    with assms have False ..}
  then show "p" by (rule ccontr)
  { assume "¬q"
    then have "¬p ∨ ¬q" ..
    with assms have False ..}
  then show "q" by (rule ccontr)
qed

-- "pabflomar, marescpla"

lemma ej9_pfm:
  assumes " ¬(¬p ∨ ¬q)"
  shows "p ∧ q"
proof 
  have 1: "¬¬p ∧ ¬¬q" using assms by (rule ej3_pfm)
  have 2: "¬¬p" using 1 by (rule  conjunct1) 
  have 3: "¬¬q" using 1 by (rule  conjunct2)
  show "p" using 2 by (rule notnotD)
  show "q" using 3 by (rule notnotD)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 10. Demostrar
     ¬(p ∧ q) ⊢ ¬p ∨ ¬q
  ------------------------------------------------------------------ *}
-- "pabflomar"
lemma ej10_pfm:
  assumes "¬(p ∧ q)"
  shows "¬p ∨ ¬q"
proof (rule ccontr)
  assume 1:"¬ (¬ p ∨ ¬ q)"
  show False
  proof -
    have "p ∧ q" using 1 by (rule ej9_pfm)
    with assms show False by (rule notE)
  qed
qed



-- "diecabmen1"
lemma Ejercicio_10:
  assumes "¬(p ∧ q)"
  shows   "¬p ∨ ¬q"
proof -
  have "¬p ∨ p" ..
  { assume "p"
    have "¬q ∨ q" ..
    { assume "q"
      with `p` have "p ∧ q" ..
      with assms have False ..
      then have "¬p ∨ ¬q" ..}
    { assume "¬q"
      then have "¬p ∨ ¬q" ..}
    with `¬q ∨ q` have "¬p ∨ ¬q" using `q ⟹ ¬ p ∨ ¬ q` ..}
  { assume "¬p"
    then have "¬p ∨ ¬q" ..}
  with `¬p ∨ p` show "¬p ∨ ¬q" using ` p ⟹ ¬ p ∨ ¬ q` ..
qed

-- "maresccas4"
lemma a10:
  assumes "¬(¬p ∨ ¬q)"
  shows "p ∧ q"
proof
  { assume "¬p"
    then have "¬p ∨ ¬q" ..
    with `¬(¬p ∨ ¬q)` have False ..}
  hence "¬¬p" ..
  thus "p" by (rule notnotD)
  { assume "¬q"
    then have "¬p ∨ ¬q" ..
    with `¬(¬p ∨ ¬q)` have False ..}
  hence "¬¬q" ..
  thus "q" by (rule notnotD)
qed

lemma 10:
  assumes "¬(p ∧ q)"
  shows "¬p ∨ ¬q"
proof (rule ccontr)
  assume "¬(¬p ∨ ¬q)"
  then have "p ∧ q" by (rule a10)
  with assms(1) show False ..
qed


text {* -----
  Ejercicio 9 haciendo uso del Ejercicio 10
 ----------*}
lemma 
  assumes "¬(¬p ∨ ¬q)"
  shows "p ∧ q"
proof (rule ccontr)
  assume "¬(p ∧ q)"
  then have "¬p ∨ ¬q" by (rule 10)
  with assms(1) show False ..
qed



--"marescpla"

  lemma 10:
    assumes "¬(p ∧ q)"
    shows "¬p ∨ ¬q"
  proof (rule ccontr)
    assume "¬(¬p ∨ ¬q)"
    then have 1:"p ∧ q" by (rule 09)
    with assms show "False" ..
  qed


text {* --------------------------------------------------------------- 
  Ejercicio 11. Demostrar
     ⊢ (p ⟶ q) ∨ (q ⟶ p)
  ------------------------------------------------------------------ *}
-- "diecabmen1"
lemma Ejercicio_11:
  shows "(p ⟶ q) ∨ (q ⟶ p)"
proof -
  have "¬(p ⟶ q) ∨ (p ⟶ q)" ..
  { assume "(p ⟶ q)"
    then have "(p ⟶ q) ∨ (q ⟶ p)" ..}
  { assume "¬(p ⟶ q)"
    { assume "q"
      { assume "p"
        have "q" using `q` .}
      then have "p ⟶ q" ..
      with `¬(p ⟶ q)` have False ..
      then have "p" ..}
    then have "q ⟶ p" ..
    then have "(p ⟶ q) ∨ (q ⟶ p)" ..}
  with `¬(p ⟶ q) ∨ (p ⟶ q)` show "(p ⟶ q) ∨ (q ⟶ p)" using `p ⟶ q ⟹ (p ⟶ q) ∨ (q ⟶ p)` ..
qed

-- "maresccas4"
lemma
  shows "(p ⟶ q) ∨ (q ⟶ p)"
proof -
  have 1:"¬(p ⟶ q) ∨ (p ⟶ q)" ..
  show "(p ⟶ q) ∨ (q ⟶ p)"
  using 1
  proof
    assume "p ⟶ q"
    then show "(p ⟶ q) ∨ (q ⟶ p)" ..
  next
    {  assume "¬(p ⟶ q)"
       {  assume "q"
          {  assume "p"
             have "q" using `q` .}
          then have "p ⟶ q" ..
          with `¬(p ⟶ q)` have False ..
          then have "p" .. }
       then have "q ⟶ p" ..
       then show "(p ⟶ q) ∨ (q ⟶ p)" ..}
  qed
qed

-- "pabflomar"
{* Sólo cambia respecto de marco en el cambio del . por by this *}
lemma
  shows "(p ⟶ q) ∨ (q ⟶ p)"
proof -
  have 1:"¬(p ⟶ q) ∨ (p ⟶ q)" ..
  show "(p ⟶ q) ∨ (q ⟶ p)"
  using 1
  proof
    assume "p ⟶ q"
    then show "(p ⟶ q) ∨ (q ⟶ p)" ..
    next
    {  assume "¬(p ⟶ q)"
       {  assume "q"
          {  assume "p"
             have "q" using `q` by this
          }
          then have "p ⟶ q" ..
          with `¬(p ⟶ q)` have False ..
          then have "p" .. 
    }
    then have "q ⟶ p" ..
    then show "(p ⟶ q) ∨ (q ⟶ p)" ..}
  qed
qed


end