Acciones

Diferencia entre revisiones de «Relación 10»

De Razonamiento automático (2013-14)
m (Texto reemplazado: «isar» por «isabelle»)
 
(No se muestran 33 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 67: Línea 67:
 
   qed
 
   qed
  
−
--"diecabmen1 maresccas4"
+
--"diecabmen1 maresccas4 domlloriv"
 
lemma Ejercicio_1:
 
lemma Ejercicio_1:
 
   assumes "p ∨ q"
 
   assumes "p ∨ q"
Línea 79: Línea 79:
 
   assume "q"
 
   assume "q"
 
   with `¬q` show "p" ..
 
   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
 
qed
  
Línea 86: Línea 122:
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
  
−
--"marescpla, pabflomar"
+
--"marescpla, pabflomar,jaisalmen, zoiruicha"
  
 
  lemma 02:
 
  lemma 02:
Línea 106: Línea 142:
 
   qed
 
   qed
  
−
--"diecabmen1 maresccas4"
+
--"diecabmen1 maresccas4 domlloriv"
 
lemma Ejercicio_2:
 
lemma Ejercicio_2:
 
   assumes "p ∧ q"
 
   assumes "p ∧ q"
Línea 124: Línea 160:
 
   qed
 
   qed
 
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 146: Línea 226:
 
qed
 
qed
  
−
-- "diecabmen1"
+
-- "diecabmen1 pabflomar domlloriv"
 
lemma Ejercicio_3:
 
lemma Ejercicio_3:
 
   assumes "¬(p ∨ q)"
 
   assumes "¬(p ∨ q)"
Línea 160: Línea 240:
 
   then have "¬q" ..
 
   then have "¬q" ..
 
   with `¬p` show "¬p ∧ ¬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
 
qed
  
Línea 186: Línea 326:
 
qed
 
qed
  
−
-- "diecabmen1"
+
-- "diecabmen1 domlloriv,jaisalmen, zoiruicha"
 
lemma Ejercicio_4:
 
lemma Ejercicio_4:
 
   assumes "¬p ∧ ¬q"
 
   assumes "¬p ∧ ¬q"
Línea 203: Línea 343:
 
     then show False using `q` ..
 
     then show False using `q` ..
 
   qed
 
   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
 
qed
  
Línea 210: Línea 431:
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
  
−
-- "maresccas4 diecabmen1"
+
-- "maresccas4 diecabmen1 domlloriv, julrobrel,jaisalmen, zoiruicha"
 
lemma
 
lemma
 
   assumes "¬p ∨ ¬q"
 
   assumes "¬p ∨ ¬q"
Línea 228: Línea 449:
 
   qed
 
   qed
 
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 233: Línea 543:
 
     ⊢ ((p ⟶ q) ⟶ p) ⟶ p
 
     ⊢ ((p ⟶ q) ⟶ p) ⟶ p
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
−
-- "diecabmen1"
+
-- "diecabmen1 maresccas4 pabflomar juaruipav domlloriv,jaisalmen, zoiruicha"
 
lemma Ejercicio_6:
 
lemma Ejercicio_6:
 
   shows "((p ⟶ q) ⟶ p) ⟶ p"
 
   shows "((p ⟶ q) ⟶ p) ⟶ p"
Línea 249: Línea 559:
 
   qed
 
   qed
 
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 254: Línea 604:
 
     ¬q ⟶ ¬p ⊢ p ⟶ q
 
     ¬q ⟶ ¬p ⊢ p ⟶ q
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
−
-- "diecabmen1"
+
-- "diecabmen1 pabflomar"
 
lemma Ejercicio_7:
 
lemma Ejercicio_7:
 
   assumes "¬q ⟶ ¬p"
 
   assumes "¬q ⟶ ¬p"
Línea 264: Línea 614:
 
     then have False using `p` ..}
 
     then have False using `p` ..}
 
   then show "q" by (rule ccontr)
 
   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
 
qed
  
Línea 289: Línea 694:
 
   with `¬p ∨ p` show "p ∨ q" using `p ⟹ p ∨ q` ..
 
   with `¬p ∨ p` show "p ∨ q" using `p ⟹ p ∨ q` ..
 
qed
 
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 294: 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 299: 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 304: 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»