Acciones

Diferencia entre revisiones de «Relación 10»

De Razonamiento automático (2013-14)
m (Texto reemplazado: «isar» por «isabelle»)
 
(No se muestran 44 ediciones intermedias de 10 usuarios)
Línea 1: Línea 1:
−
<source lang="isar">
+
<source lang="isabelle">
 
header {* R10: Deducción natural proposicional *}
 
header {* R10: Deducción natural proposicional *}
  
Línea 52: Línea 52:
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
  
−
--"marescpla, pabflomar"
+
--"marescpla, pabflomar, jaisalmen, zoiruicha"
  
 
   lemma 01:
 
   lemma 01:
Línea 66: Línea 66:
 
         with 2 show "p" by (rule notE)}
 
         with 2 show "p" by (rule notE)}
 
   qed
 
   qed
 +
 +
--"diecabmen1 maresccas4 domlloriv"
 +
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
 +
 +
--"juaruipav, julrobrel"
 +
lemma ej1_juaruipav:
 +
assumes 1:"p ∨ q"
 +
    and 2: "¬q"
 +
shows "p"
 +
using 1
 +
proof
 +
  assume 3:"p"
 +
  then show "p" .
 +
next
 +
  assume 4:"q"
 +
  show "p" using 2 4 by (rule notE)
 +
qed
 +
 +
--"irealetei, julrobrel"
 +
lemma ej1_auto:
 +
  assumes 1:"p ∨ q"
 +
  assumes 2:"¬q"
 +
  shows "p"
 +
using assms by auto
 +
 +
lemma ej1:
 +
  assumes 1:"p ∨ q"
 +
  assumes 2:"¬q"
 +
  shows "p"
 +
proof -
 +
  note 1
 +
  moreover
 +
  {assume "p"
 +
    then have "p" .}
 +
  moreover
 +
  {assume 3:"q"
 +
    have "p" using 2 3 ..}
 +
ultimately show "p" ..
 +
qed
  
 
text {* ---------------------------------------------------------------  
 
text {* ---------------------------------------------------------------  
Línea 71: Línea 121:
 
     p ∧ q ⊢ ¬(¬p ∨ ¬q)
 
     p ∧ q ⊢ ¬(¬p ∨ ¬q)
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
 +
 +
--"marescpla, pabflomar,jaisalmen, zoiruicha"
 +
 +
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 domlloriv"
 +
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
 +
 +
 +
--"juaruipav"
 +
 +
lemma ej2_juaruipav:
 +
assumes 1:"p ∧ q"
 +
shows "¬(¬p ∨ ¬q)" 
 +
proof
 +
  assume 2: "¬ p ∨ ¬ q"
 +
  show "False"
 +
  using 2
 +
  proof
 +
    assume 3: "¬q"
 +
    have 4:"q" using 1 by (rule conjunct2)
 +
    show "False" using 3 4 by (rule notE)
 +
next
 +
    assume 5: "¬p"
 +
    have 6:"p" using 1 by (rule conjunct1)
 +
    show "False" using 5 6 by (rule notE)
 +
  qed
 +
qed
 +
 +
--"irealetei, julrobrel"
 +
lemma ej2_auto:
 +
  assumes 1:"p ∧ q"
 +
  shows  "¬(¬p ∨ ¬q)"
 +
using assms by auto
 +
 +
lemma ej2:
 +
  assumes 1:"p ∧ q"
 +
  shows  "¬(¬p ∨ ¬q)"
 +
proof
 +
  assume "¬p ∨ ¬q"
 +
  moreover
 +
  {assume 2:"¬p"
 +
    have 3:"p" using 1 ..
 +
    have "False" using 2 3 ..}
 +
  moreover
 +
  {assume 2:"¬q"
 +
    have 3:"q" using 1 ..
 +
    have "False" using 2 3 ..}
 +
ultimately show "False" ..
 +
qed
 +
  
 
text {* ---------------------------------------------------------------  
 
text {* ---------------------------------------------------------------  
Línea 76: Línea 209:
 
     ¬(p ∨ q) ⊢ ¬p ∧ ¬q
 
     ¬(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 domlloriv"
 +
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,jaisalmen, zoiruicha"
 +
  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
 +
 +
--"juaruipav"
 +
 +
lemma ej3_juaruipav:
 +
assumes 1: " ¬(p ∨ q)"
 +
shows " ¬p ∧ ¬q"
 +
proof
 +
  {assume 2:"p"
 +
  have 3: "p∨q" using 2 by (rule disjI1)
 +
  have 4: "False" using 1 3 by (rule notE)}
 +
  then show "¬p"  ..
 +
next
 +
  {assume 5:"q"
 +
  have 6: "p∨q" using 5 by (rule disjI2)
 +
  have 7: "False" using 1 6 by (rule notE)}
 +
  then show "¬q"  ..
 +
  qed
 +
 +
--"irealetei, julrobrel"
 +
lemma ej3_auto:
 +
  assumes "¬(p ∨ q)"
 +
  shows  "¬p ∧ ¬q"
 +
using assms by auto
 +
 +
lemma ej3:
 +
  assumes 0:"¬(p ∨ q)"
 +
  shows  "¬p ∧ ¬q"
 +
proof
 +
  {assume "p"
 +
    then have 2:"p ∨ q" ..
 +
    have "False" using 0 2 ..}
 +
  then show "¬p" ..
 +
  next
 +
{assume "q"
 +
    then have 2:"p ∨ q" ..
 +
    have "False" using 0 2 ..}
 +
  then show "¬q" ..
 +
qed
  
 
text {* ---------------------------------------------------------------  
 
text {* ---------------------------------------------------------------  
Línea 81: Línea 306:
 
     ¬p ∧ ¬q ⊢ ¬(p ∨ q)
 
     ¬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 domlloriv,jaisalmen, zoiruicha"
 +
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
 +
 +
--"juaruipav, julrobrel"
 +
lemma ej4_juaruipav:
 +
assumes 1:" ¬p ∧ ¬q"
 +
shows "¬(p ∨ q)"
 +
proof
 +
  assume 2: " p ∨ q"
 +
  show "False"
 +
  using 2
 +
  proof
 +
    assume 3:"p"
 +
    have 4:"¬p" using 1 by (rule conjunct1)
 +
    show "False" using 4 3 by (rule notE)
 +
  next
 +
    assume 5:"q"
 +
    have 6:"¬q" using 1 by (rule conjunct2)
 +
    show "False" using 6 5 by (rule notE)
 +
  qed
 +
qed
 +
 +
--"irealetei"
 +
lemma ej4_auto:
 +
  assumes "¬p ∧ ¬q"
 +
  shows  "¬(p ∨ q)"
 +
using assms by auto
 +
 +
lemma ej4:
 +
  assumes 0:"¬p ∧ ¬q"
 +
  shows  "¬(p ∨ q)"
 +
proof
 +
  assume "p ∨ q"
 +
  moreover
 +
  {assume 1:"p"
 +
    have "¬p" using 0 ..
 +
    then have  "False" using 1 ..}
 +
  moreover
 +
  {assume 1:"q"
 +
    have "¬q" using 0 ..
 +
    then have  "False" using 1 ..}
 +
ultimately show "False" ..
 +
qed
  
 
text {* ---------------------------------------------------------------  
 
text {* ---------------------------------------------------------------  
Línea 86: Línea 430:
 
     ¬p ∨ ¬q ⊢ ¬(p ∧ q)
 
     ¬p ∨ ¬q ⊢ ¬(p ∧ q)
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
 +
 +
-- "maresccas4 diecabmen1 domlloriv, julrobrel,jaisalmen, zoiruicha"
 +
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
 +
 +
--"juaruipav"
 +
lemma ej5_juaruipav:
 +
assumes 1:"¬p ∨ ¬q"
 +
shows " ¬(p ∧ q)"
 +
using 1
 +
proof
 +
    assume 2: "¬p"
 +
    show "¬ (p ∧ q)"
 +
    proof
 +
      assume 3: " p ∧ q"
 +
      have 4:"p" using 3 by (rule conjunct1)
 +
      show "False " using 2 4 by (rule notE)
 +
    qed
 +
next
 +
    assume 5: "¬q"
 +
    show "¬ (p ∧ q)"
 +
    proof
 +
      assume 6: " p ∧ q"
 +
      have 7:"q" using 6 by (rule conjunct2)
 +
      show "False " using 5 7 by (rule notE)
 +
    qed
 +
 +
qed
 +
 +
--"irealetei"
 +
lemma ej5_auto:
 +
  assumes "¬p ∨ ¬q"
 +
  shows  "¬(p ∧ q)"
 +
using assms by auto
 +
 +
lemma ej5:
 +
  assumes 0:"¬p ∨ ¬q"
 +
  shows  "¬(p ∧ q)"
 +
proof
 +
  assume 1:"p ∧ q"
 +
  have 2:"p" using 1 ..
 +
  have 3:"q" using 1 ..
 +
  show "False" using 0
 +
  proof
 +
    assume "¬p"
 +
    then show "False" using 2 ..
 +
  next
 +
    assume "¬q"
 +
    then show "False" using 3 ..
 +
  qed
 +
qed 
 +
  
 
text {* ---------------------------------------------------------------  
 
text {* ---------------------------------------------------------------  
Línea 91: Línea 543:
 
     ⊢ ((p ⟶ q) ⟶ p) ⟶ p
 
     ⊢ ((p ⟶ q) ⟶ p) ⟶ p
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
 +
-- "diecabmen1 maresccas4 pabflomar juaruipav domlloriv,jaisalmen, zoiruicha"
 +
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
 +
 +
--"irealetei, julrobrel"
 +
lemma ej6_auto:"((p ⟶ q) ⟶ p) ⟶ p"
 +
using assms by auto
 +
 +
lemma ej6:"((p ⟶ q) ⟶ p) ⟶ p"
 +
proof
 +
  assume 1:"(p ⟶ q)⟶p"
 +
  show "p"
 +
  proof (rule ccontr)
 +
    assume 2:"¬p"
 +
    have 4:"¬(p⟶q)" using 1 2 by (rule mt)
 +
    {assume 5:"p"
 +
    have "False" using 2 5 ..
 +
    then have "q" ..}
 +
    then have 6:"p⟶q" ..
 +
    show "False" using 4 6 ..
 +
  qed
 +
qed
 +
   
  
 
text {* ---------------------------------------------------------------  
 
text {* ---------------------------------------------------------------  
Línea 96: Línea 604:
 
     ¬q ⟶ ¬p ⊢ p ⟶ q
 
     ¬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,jaisalmen, zoiruicha"
 +
  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
 +
 +
 +
--"juaruipav, julrobrel, domlloriv"
 +
 +
lemma ej7_juaruipav:
 +
assumes 1: "¬q ⟶ ¬p"
 +
shows "p ⟶ q"
 +
proof
 +
  assume 2: "p"
 +
  have 3: "¬¬p" using 2 by (rule notnotI)
 +
  have 4: "¬¬q" using 1 3 by (rule mt)
 +
  show "q" using 4 by (rule notnotD)
 +
qed
 +
 +
--"irealetei"
 +
lemma ej7_auto:
 +
  assumes "¬q ⟶ ¬p"
 +
  shows "p ⟶ q"
 +
using assms by auto
 +
 +
lemma ej7:
 +
  assumes 0:"¬q ⟶ ¬p"
 +
  shows "p ⟶ q"
 +
proof -
 +
  {assume 1:"p"
 +
  then have 2:"¬¬p" by (rule notnotI)
 +
  have "¬¬q" using 0 2 by (rule mt)
 +
  then have "q" by (rule notnotD)}
 +
  then show "p ⟶ q" ..
 +
qed
  
 
text {* ---------------------------------------------------------------  
 
text {* ---------------------------------------------------------------  
Línea 101: Línea 675:
 
     ¬(¬p ∧ ¬q) ⊢ p ∨ q
 
     ¬(¬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
 +
 +
--"irealetei, julrobrel"
 +
lemma ej8_auto:
 +
  assumes "¬(¬p ∧ ¬q)"
 +
  shows "p ∨ q"
 +
using assms by auto
 +
 +
lemma ej8:
 +
  assumes 0:"¬(¬p ∧ ¬q)"
 +
  shows "p ∨ q"
 +
proof -
 +
  {assume 1:"¬(p ∨ q)"
 +
  have 2:"¬p ∧ ¬q" using 1 by (rule ej3)
 +
  have "False" using 0 2 ..}
 +
  then show "p ∨ q" by (rule ccontr)
 +
qed 
 +
  
 
text {* ---------------------------------------------------------------  
 
text {* ---------------------------------------------------------------  
Línea 106: Línea 730:
 
     ¬(¬p ∨ ¬q) ⊢ p ∧ q
 
     ¬(¬p ∨ ¬q) ⊢ p ∧ q
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
 +
-- "diecabmen1, maresccas4 domlloriv"
 +
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
 +
 +
 +
--"juaruipav"
 +
lemma ej9_juaruipav:
 +
  assumes 1: " ¬(¬p ∨ ¬q)"
 +
  shows " p ∧ q"
 +
  proof
 +
    have 2:"(¬¬p)∧(¬¬q)" using 1 by (rule ej3_juaruipav)
 +
    have "(¬¬p)" using 2 by (rule conjunct1)
 +
    then show "p" by (rule notnotD) 
 +
    next
 +
    have 3:"(¬¬p)∧(¬¬q)" using 1 by (rule ej3_juaruipav)
 +
    have "(¬¬q)" using 3 by (rule conjunct2)
 +
    then show "q" by (rule notnotD)
 +
  qed
 +
 +
--"irealetei, julrobrel"
 +
lemma ej9_auto:
 +
  assumes "¬(¬p ∨ ¬q)"
 +
  shows "p ∧ q"
 +
using assms by auto
 +
 +
lemma ej9:
 +
  assumes 0:"¬(¬p ∨ ¬q)"
 +
  shows "p ∧ q"
 +
proof
 +
  {assume "¬p"
 +
  then have 1:"¬p ∨ ¬q" ..
 +
    have "False" using 0 1 ..}
 +
    then show "p" by (rule ccontr)
 +
  next
 +
  {assume "¬q"
 +
    then have 1:"¬p ∨ ¬q" ..
 +
    have "False" using 0 1 ..}
 +
  then show "q" by (rule ccontr)
 +
qed
 +
  
 
text {* ---------------------------------------------------------------  
 
text {* ---------------------------------------------------------------  
Línea 111: Línea 799:
 
     ¬(p ∧ q) ⊢ ¬p ∨ ¬q
 
     ¬(p ∧ q) ⊢ ¬p ∨ ¬q
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
 +
-- "pabflomar, julrobrel, juaruipav, domlloriv"
 +
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
 +
 +
--"irealetei"
 +
lemma ej10_auto:
 +
  assumes "¬(p ∧ q)"
 +
  shows "¬p ∨ ¬q"
 +
using assms by auto
 +
 +
lemma ej10:
 +
  assumes 0:"¬(p ∧ q)"
 +
  shows "¬p ∨ ¬q"
 +
proof -
 +
  {assume 1:"¬(¬p ∨ ¬q)"
 +
  have 2:"p ∧ q" using 1 by (rule ej9)
 +
  have 3:"False" using 0 2 .. }
 +
  then show "¬p ∨ ¬q" by (rule ccontr)
 +
qed
  
 
text {* ---------------------------------------------------------------  
 
text {* ---------------------------------------------------------------  
Línea 116: Línea 906:
 
     ⊢ (p ⟶ q) ∨ (q ⟶ p)
 
     ⊢ (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, julrobrel"
 +
{* 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
 +
 +
-- "irealetei domlloriv juaruipav"
 +
 +
lemma ej11_auto:"(p ⟶ q) ∨ (q ⟶ p)"
 +
using assms by auto
 +
 +
lemma ej11:
 +
  shows "(p ⟶ q) ∨ (q ⟶ p)"
 +
proof -
 +
  have 1:"¬(p ⟶ q) ∨ (p ⟶ q) " by (rule excluded_middle)
 +
  then show "(p ⟶ q) ∨ (q ⟶ p)"
 +
  proof
 +
    note 1
 +
    moreover
 +
    {assume "p⟶q"
 +
    then show "(p ⟶ q) ∨ (q ⟶ p)" ..}
 +
    moreover
 +
    {assume 2:"¬(p ⟶ q)"
 +
      {assume 3:"q"
 +
        {assume "p"
 +
          have "q" using 3 .}
 +
        then have 4:"p⟶q" ..
 +
        have "False" using 2 4 ..
 +
        then have "p" ..}
 +
      then have "q⟶p" ..
 +
      then show "(p ⟶ q) ∨ (q ⟶ p)" ..}
 +
    qed     
 +
qed
  
 
end
 
end
 
</source>
 
</source>

Revisión actual del 17:46 16 jul 2018

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, jaisalmen, zoiruicha"

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

--"juaruipav, julrobrel"
 lemma ej1_juaruipav:
 assumes 1:"p ∨ q"
     and 2: "¬q"
 shows "p"
 using 1
 proof
  assume 3:"p"
  then show "p" .
 next
  assume 4:"q"
  show "p" using 2 4 by (rule notE)
qed

--"irealetei, julrobrel"
lemma ej1_auto:
  assumes 1:"p ∨ q"
  assumes 2:"¬q"
  shows "p"
using assms by auto

lemma ej1:
  assumes 1:"p ∨ q"
  assumes 2:"¬q"
  shows "p"
proof - 
  note 1
  moreover
  {assume "p"
    then have "p" .}
  moreover
  {assume 3:"q"
    have "p" using 2 3 ..}
 ultimately show "p" ..
qed

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

--"marescpla, pabflomar,jaisalmen, zoiruicha"

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


--"juaruipav"

lemma ej2_juaruipav:
 assumes 1:"p ∧ q"
 shows "¬(¬p ∨ ¬q)"  
 proof 
  assume 2: "¬ p ∨ ¬ q"
  show "False"
  using 2
  proof
    assume 3: "¬q"
    have 4:"q" using 1 by (rule conjunct2)
    show "False" using 3 4 by (rule notE) 
 next
    assume 5: "¬p"
    have 6:"p" using 1 by (rule conjunct1)
    show "False" using 5 6 by (rule notE) 
   qed
 qed

--"irealetei, julrobrel"
lemma ej2_auto:
  assumes 1:"p ∧ q"
  shows  "¬(¬p ∨ ¬q)"
using assms by auto

lemma ej2:
  assumes 1:"p ∧ q"
  shows  "¬(¬p ∨ ¬q)"
proof
  assume "¬p ∨ ¬q"
  moreover
  {assume 2:"¬p" 
    have 3:"p" using 1 ..
    have "False" using 2 3 ..}
  moreover
  {assume 2:"¬q" 
    have 3:"q" using 1 ..
    have "False" using 2 3 ..}
ultimately show "False" ..
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 domlloriv"
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,jaisalmen, zoiruicha"
  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

--"juaruipav"

lemma ej3_juaruipav:
 assumes 1: " ¬(p ∨ q)"
 shows " ¬p ∧ ¬q"
 proof 
  {assume 2:"p"
  have 3: "p∨q" using 2 by (rule disjI1)
  have 4: "False" using 1 3 by (rule notE)}
  then show "¬p"  ..
next
  {assume 5:"q"
  have 6: "p∨q" using 5 by (rule disjI2)
  have 7: "False" using 1 6 by (rule notE)}
  then show "¬q"  ..
  qed

--"irealetei, julrobrel"
lemma ej3_auto:
  assumes "¬(p ∨ q)"
  shows  "¬p ∧ ¬q"
using assms by auto

lemma ej3:
  assumes 0:"¬(p ∨ q)"
  shows  "¬p ∧ ¬q"
proof
  {assume "p"
    then have 2:"p ∨ q" ..
    have "False" using 0 2 ..}
  then show "¬p" ..
  next
 {assume "q"
    then have 2:"p ∨ q" ..
    have "False" using 0 2 ..}
  then show "¬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

-- "diecabmen1 domlloriv,jaisalmen, zoiruicha"
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

--"juaruipav, julrobrel"
lemma ej4_juaruipav:
assumes 1:" ¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof 
  assume 2: " p ∨ q"
  show "False"
  using 2
  proof
     assume 3:"p"
     have 4:"¬p" using 1 by (rule conjunct1)
     show "False" using 4 3 by (rule notE) 
  next 
     assume 5:"q"
     have 6:"¬q" using 1 by (rule conjunct2)
     show "False" using 6 5 by (rule notE)
   qed
qed

--"irealetei"
lemma ej4_auto:
  assumes "¬p ∧ ¬q"
  shows  "¬(p ∨ q)"
using assms by auto

lemma ej4:
  assumes 0:"¬p ∧ ¬q"
  shows  "¬(p ∨ q)"
proof
  assume "p ∨ q"
  moreover
  {assume 1:"p"
    have "¬p" using 0 ..
    then have  "False" using 1 ..}
  moreover
  {assume 1:"q"
    have "¬q" using 0 ..
    then have  "False" using 1 ..}
ultimately show "False" ..
qed

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

-- "maresccas4 diecabmen1 domlloriv, julrobrel,jaisalmen, zoiruicha"
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

--"juaruipav"
lemma ej5_juaruipav:
 assumes 1:"¬p ∨ ¬q"
 shows " ¬(p ∧ q)"
 using 1
 proof 
    assume 2: "¬p"
    show "¬ (p ∧ q)"
    proof
      assume 3: " p ∧ q"
      have 4:"p" using 3 by (rule conjunct1)
      show "False " using 2 4 by (rule notE)
    qed
next
    assume 5: "¬q"
    show "¬ (p ∧ q)"
    proof
      assume 6: " p ∧ q"
      have 7:"q" using 6 by (rule conjunct2)
      show "False " using 5 7 by (rule notE)
    qed

qed

--"irealetei"
lemma ej5_auto:
  assumes "¬p ∨ ¬q"
  shows  "¬(p ∧ q)"
using assms by auto

lemma ej5:
  assumes 0:"¬p ∨ ¬q"
  shows  "¬(p ∧ q)"
proof 
  assume 1:"p ∧ q"
  have 2:"p" using 1 ..
  have 3:"q" using 1 ..
  show "False" using 0
  proof
    assume "¬p"
    then show "False" using 2 ..
  next 
    assume "¬q"
    then show "False" using 3 ..
  qed
qed  


text {* --------------------------------------------------------------- 
  Ejercicio 6. Demostrar
     ⊢ ((p ⟶ q) ⟶ p) ⟶ p
  ------------------------------------------------------------------ *}
-- "diecabmen1 maresccas4 pabflomar juaruipav domlloriv,jaisalmen, zoiruicha"
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

--"irealetei, julrobrel"
lemma ej6_auto:"((p ⟶ q) ⟶ p) ⟶ p"
using assms by auto

lemma ej6:"((p ⟶ q) ⟶ p) ⟶ p"
proof 
  assume 1:"(p ⟶ q)⟶p"
  show "p"
  proof (rule ccontr)
    assume 2:"¬p"
    have 4:"¬(p⟶q)" using 1 2 by (rule mt) 
    {assume 5:"p"
    have "False" using 2 5 ..
    then have "q" ..}
    then have 6:"p⟶q" ..
    show "False" using 4 6 .. 
  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,jaisalmen, zoiruicha"
  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


--"juaruipav, julrobrel, domlloriv"

lemma ej7_juaruipav:
assumes 1: "¬q ⟶ ¬p" 
shows "p ⟶ q"
proof 
  assume 2: "p"
  have 3: "¬¬p" using 2 by (rule notnotI)
  have 4: "¬¬q" using 1 3 by (rule mt)
  show "q" using 4 by (rule notnotD)
qed

--"irealetei"
lemma ej7_auto:
   assumes "¬q ⟶ ¬p"
   shows "p ⟶ q"
using assms by auto

lemma ej7:
   assumes 0:"¬q ⟶ ¬p"
   shows "p ⟶ q"
proof -
  {assume 1:"p"
  then have 2:"¬¬p" by (rule notnotI)
  have "¬¬q" using 0 2 by (rule mt)
  then have "q" by (rule notnotD)}
  then show "p ⟶ q" ..
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

--"irealetei, julrobrel"
lemma ej8_auto:
   assumes "¬(¬p ∧ ¬q)"
   shows "p ∨ q"
using assms by auto

lemma ej8:
   assumes 0:"¬(¬p ∧ ¬q)"
   shows "p ∨ q"
proof -
  {assume 1:"¬(p ∨ q)"
  have 2:"¬p ∧ ¬q" using 1 by (rule ej3)
  have "False" using 0 2 ..}
  then show "p ∨ q" by (rule ccontr)
qed  


text {* --------------------------------------------------------------- 
  Ejercicio 9. Demostrar
     ¬(¬p ∨ ¬q) ⊢ p ∧ q
  ------------------------------------------------------------------ *}
-- "diecabmen1, maresccas4 domlloriv"
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


--"juaruipav"
lemma ej9_juaruipav:
  assumes 1: " ¬(¬p ∨ ¬q)" 
  shows " p ∧ q"
  proof 
    have 2:"(¬¬p)∧(¬¬q)" using 1 by (rule ej3_juaruipav)
    have "(¬¬p)" using 2 by (rule conjunct1)
    then show "p" by (rule notnotD)   
    next
    have 3:"(¬¬p)∧(¬¬q)" using 1 by (rule ej3_juaruipav)
    have "(¬¬q)" using 3 by (rule conjunct2)
    then show "q" by (rule notnotD)
  qed

--"irealetei, julrobrel"
lemma ej9_auto:
   assumes "¬(¬p ∨ ¬q)"
   shows "p ∧ q"
using assms by auto

lemma ej9:
   assumes 0:"¬(¬p ∨ ¬q)"
   shows "p ∧ q"
proof 
   {assume "¬p"
   then have 1:"¬p ∨ ¬q" ..
     have "False" using 0 1 ..}
     then show "p" by (rule ccontr)
   next
   {assume "¬q"
     then have 1:"¬p ∨ ¬q" ..
     have "False" using 0 1 ..}
   then show "q" by (rule ccontr)
qed


text {* --------------------------------------------------------------- 
  Ejercicio 10. Demostrar
     ¬(p ∧ q) ⊢ ¬p ∨ ¬q
  ------------------------------------------------------------------ *}
-- "pabflomar, julrobrel, juaruipav, domlloriv"
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

--"irealetei"
lemma ej10_auto:
   assumes "¬(p ∧ q)"
   shows "¬p ∨ ¬q"
using assms by auto

lemma ej10:
   assumes 0:"¬(p ∧ q)"
   shows "¬p ∨ ¬q"
proof -
  {assume 1:"¬(¬p ∨ ¬q)"
  have 2:"p ∧ q" using 1 by (rule ej9)
  have 3:"False" using 0 2 .. }
  then show "¬p ∨ ¬q" by (rule ccontr)
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, julrobrel"
{* 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

-- "irealetei domlloriv juaruipav"

lemma ej11_auto:"(p ⟶ q) ∨ (q ⟶ p)"
using assms by auto

 lemma ej11:
  shows "(p ⟶ q) ∨ (q ⟶ p)"
proof -
  have 1:"¬(p ⟶ q) ∨ (p ⟶ q) " by (rule excluded_middle)
  then show "(p ⟶ q) ∨ (q ⟶ p)"
  proof 
    note 1
    moreover
    {assume "p⟶q"
    then show "(p ⟶ q) ∨ (q ⟶ p)" ..}
    moreover
    {assume 2:"¬(p ⟶ q)"
      {assume 3:"q"
        {assume "p"
          have "q" using 3 .}
        then have 4:"p⟶q" ..
        have "False" using 2 4 ..
        then have "p" ..}
      then have "q⟶p" ..
      then show "(p ⟶ q) ∨ (q ⟶ p)" ..}
    qed       
qed

end
Obtenido de «https://www.glc.us.es/~jalonso/RA2013/index.php?title=Relación_10&oldid=666»