Demostración asistida por ordenador (2011-12) Demostración asistida por ordenador (2011-12)

header {* Deducción natural proposicional *}

theory Tema_3
imports Main 
begin

text {*
  En esta teoría se presentan los ejemplos del tema de deducción natural
  proposicional siguiendo la presentación de Huth y Ryan en su libro
  "Logic in Computer Science"
  http://www.cs.bham.ac.uk/research/projects/lics/ y, más concretamente,
  a la forma como se explica en la asignatura de "Lógica informática" y
  que puede verse en  
  http://www.cs.us.es/~jalonso/cursos/li/temas/tema-2.pdf
 
  La página al lado de cada teorema indica la página de las anteriores
  transparencias donde se encuentra la demostración.
*}

section {* Reglas de la conjunción *}

text {*
  La regla de introducción de la conjunción es
  · conjI:      ⟦P; Q⟧ ⟹ P ∧ Q
  Las reglas de eliminación de la conjunción son
  · conjunct1:  P ∧ Q ⟹ P
  · conjunct2:  P ∧ Q ⟹ Q  
*}

lemma -- "p. 4" 
  assumes 1: "p ∧ q" and 
          2: "r" 
  shows "q ∧ r"     
proof -
  have 3: "q" using 1 by (rule conjunct2)
  show "q ∧ r" using 3 2 by (rule conjI)
qed

lemma 
  assumes 1: "(p ∧ q) ∧ r" and 
          2: "s ∧ t" 
  shows "q ∧ s"
proof -
  have 3: "p ∧ q" using 1 by (rule conjunct1)
  have 4: "q" using 3 by (rule conjunct2)
  have 5: "s" using 2 by (rule conjunct1)
  show "q ∧ s" using 4 5 by (rule conjI)
qed

section {* Reglas de la doble negación *}

text {*
  La regla de eliminación de la doble negación es
  · notnotD: ¬¬ P ⟹ P
  Para ajustarnos al tema de LI vamos a introducir la siguiente regla de
  introducción de la doble negación
  . notnotI: P ⟹ ¬¬ P
  que, de momento, no detallamos su demostración.
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma -- "p. 5" 
  assumes 1: "p" and 
          2: "¬¬(q ∧ r)" 
  shows "¬¬p ∧ r"
proof -
  have 3: "¬¬p" using 1 by (rule notnotI)
  have 4: "q ∧ r" using 2 by (rule notnotD)
  have 5: "r" using 4 by (rule conjunct2)
  show "¬¬p ∧ r" using 3 5 by (rule conjI)
qed        

section {* Regla de eliminación del condicional *}

text {*
  La regla de eliminación del condicional es la regla del modus ponens
  · mp: ⟦P ⟶ Q; P⟧ ⟹ Q 
*}

lemma -- "p. 6"
  assumes 1: "¬p ∧ q" and 
          2: "¬p ∧ q ⟶ r ∨ ¬p" 
  shows "r ∨ ¬p"
proof -
  show "r ∨ ¬p" using 2 1 by (rule mp)
qed    

lemma -- "p. 6"
  assumes 1: "p" and 
          2: "p ⟶ q" and 
          3: "p ⟶ (q ⟶ r)" 
  shows "r"
proof -
  have 4: "q" using 2 1 by (rule mp)
  have 5: "q ⟶ r" using 3 1 by (rule mp)
  show "r" using 5 4 by (rule mp)
qed

section {* Regla derivada del modus tollens *}

text {*
  Para ajustarnos al tema de LI vamos a introducir la regla del modus
  tollens
  · mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F 
  sin, de momento, detallar su demostración.
*}

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

lemma -- "p. 7"
  assumes 1: "p ⟶ (q ⟶ r)" and 
          2: "p" and 
          3: "¬r" 
  shows "¬q"
proof -
  have 4: "q ⟶ r" using 1 2 by (rule mp)
  show "¬q" using 4 3 by (rule mt)
qed    

lemma -- "p. 7"
  assumes 1: "¬p ⟶ q" and 
          2: "¬q" 
  shows "p"
proof -
  have 3: "¬¬p" using 1 2 by (rule mt)
  show "p" using 3 by (rule notnotD)
qed

lemma 
  assumes 1: "p ⟶ ¬q" and 
          2: "q" 
  shows "¬p"
proof -
  have 3: "¬¬q" using 2 by (rule notnotI)
  show "¬p" using 1 3 by (rule mt)
qed

section {* Regla de introducción del condicional *}

text {*
  La regla de introducción del condicional es
  · impI: (P ⟹ Q) ⟹ P ⟶ Q
*}

lemma -- "p. 8"
  assumes 1: "p ⟶ q" 
  shows "¬q ⟶ ¬p"
proof -
  { assume 3: "¬q"
    have "¬p" using 1 3 by (rule mt)
  } thus "¬q ⟶ ¬p" by (rule impI)
qed    

lemma -- "p. 8"
  assumes 1: "p ⟶ q" 
  shows "¬q ⟶ ¬p"
proof (rule impI)
  assume 3: "¬q"
  show "¬p" using 1 3 by (rule mt)
qed    

lemma -- "p. 8"
  assumes 1: "p ⟶ q" 
  shows "¬q ⟶ ¬p"
proof
  assume 3: "¬q"
  show "¬p" using 1 3 by (rule mt)
qed    

lemma -- "p. 9"
  assumes 1: "¬q ⟶ ¬p" 
  shows "p ⟶ ¬¬q"   
proof -
  { assume 2: "p"
    have 3: "¬¬p" using 2 by (rule notnotI)
    have "¬¬q" using 1 3 by (rule mt)
  } thus "p ⟶ ¬¬q" by (rule impI)
qed


lemma -- "p. 9"
  assumes 1: "¬q ⟶ ¬p" 
  shows "p ⟶ ¬¬q"   
proof (rule impI)
  assume 2: "p"
  have 3: "¬¬p" using 2 by (rule notnotI)
  show "¬¬q" using 1 3 by (rule mt)
qed

lemma -- "p. 9"
  "p ⟶ p"
proof (rule impI)
qed

lemma -- "p. 10"
  "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
proof -
  { assume 1: "q ⟶ r"
    { assume 2: "¬q ⟶ ¬p"
      { assume 3: "p"
        have 4: "¬¬p" using 3 by (rule notnotI)
        have 5: "¬¬q" using 2 4 by (rule mt)
        have 6: "q" using 5 by (rule notnotD)
        have "r" using 1 6 by (rule mp) 
      } hence "p ⟶ r" by (rule impI)
    } hence "(¬q ⟶ ¬p) ⟶ p ⟶ r" by (rule impI)
  } thus "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ p ⟶ r)" by (rule impI)
qed

lemma -- "p. 10"
  "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
proof (rule impI)
  assume 1: "q ⟶ r"
  show "(¬q ⟶ ¬p) ⟶ (p ⟶ r)"
    proof (rule impI)
      assume 2: "¬q ⟶ ¬p"
      show "p ⟶ r"
        proof (rule impI)
          assume 3: "p"
          have 4: "¬¬p" using 3 by (rule notnotI)
          have 5: "¬¬q" using 2 4 by (rule mt)
          have 6: "q" using 5 by (rule notnotD)
          show "r" using 1 6 by (rule mp)
        qed
    qed
qed

lemma 
  assumes 1: "p ∧ q ⟶ r" 
  shows "p ⟶ (q ⟶ r)"
proof (rule impI)
  assume 2: "p"
  show "q ⟶ r" 
    proof (rule impI)
      assume 3: "q"
      have 4: "p ∧ q" using 2 3 by (rule conjI)
      show "r" using 1 4 by (rule mp)
    qed
qed

lemma 
  assumes 1: "p ⟶ (q ⟶ r)" 
  shows "p ∧ q ⟶ r"
proof (rule impI)
  assume 2: "p ∧ q"
  have 3: "p" using 2 by (rule conjunct1)
  have 4: "q ⟶ r" using 1 3 by (rule mp)
  have 5: "q" using 2 by (rule conjunct2)
  show "r" using 4 5 by (rule mp)
qed    

lemma 
  assumes 1: "p ⟶ q" 
  shows "p ∧ r ⟶ q ∧ r"
proof (rule impI)
  assume 2: "p ∧ r"
  have 3: "p" using 2 by (rule conjunct1)
  have 4: "q" using 1 3 by (rule mp)
  have 5: "r" using 2 by (rule conjunct2)
  show "q ∧ r" using 4 5 by (rule conjI)
qed

section {* Reglas de la disyunción *}

text {*
  Las reglas de la introducción de la disyunción son
  · disjI1: P ⟹ P ∨ Q
  · disjI2: Q ⟹ P ∨ Q
  La regla de elimación de la disyunción es
  · disjE:  ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R 
*}

lemma -- "p. 11"
  assumes 1: "p ∨ q" 
  shows "q ∨ p"
using 1
proof (rule disjE)
  { assume 2: "p"
    show "q ∨ p" using 2 by (rule disjI2) }
next
  { assume 3: "q"
    show "q ∨ p" using 3 by (rule disjI1) }
qed    

lemma -- "p. 12"
  assumes 1: "q ⟶ r"
  shows "p ∨ q ⟶ p ∨ r"
proof (rule impI)
  assume 2: "p ∨ q"
  thus "p ∨ r"
  proof (rule disjE)
    { assume 3: "p"
      show "p ∨ r" using 3 by (rule disjI1) }
  next
    { assume 4: "q"
      have 5: "r" using 1 4 by (rule mp)
      show "p ∨ r" using 5 by (rule disjI2) }
  qed
qed    

lemma 
  assumes 1: "(p ∨ q) ∨ r" 
  shows "p ∨ (q ∨ r)"
using 1
proof (rule disjE)
  { assume 2: "p ∨ q"
    thus "p ∨ (q ∨ r)"
    proof (rule disjE)
      { assume 3: "p"
        show "p ∨ (q ∨ r)" using 3 by (rule disjI1) }
    next
      { assume 4: "q"
        have 5: "q ∨ r" using 4 by (rule disjI1)
        show "p ∨ (q ∨ r)" using 5 by (rule disjI2) }
    qed }
next
  { assume 6: "r"
    have 7: "q ∨ r" using 6 by (rule disjI2)
    show "p ∨ (q ∨ r)" using 7 by (rule disjI2) }
qed    

lemma 
  assumes 1: "p ∧ (q ∨ r)" 
  shows "(p ∧ q) ∨ (p ∧ r)"
proof -
  have 2: "p" using 1 ..
  have "q ∨ r" using 1 ..
  thus "(p ∧ q) ∨ (p ∧ r)"
  proof (rule disjE)
    { assume 3: "q"
      have "p ∧ q" using 2 3 by (rule conjI)
      thus "(p ∧ q) ∨ (p ∧ r)" by (rule disjI1) }
  next
    { assume 4: "r"
      have "p ∧ r" using 2 4 by (rule conjI)
      thus "(p ∧ q) ∨ (p ∧ r)" by (rule disjI2) }
  qed
qed    

section {* Regla de copia *}

lemma -- "p. 13"
  "p ⟶ (q ⟶ p)"
proof (rule impI)
  assume 1: "p"
  show "q ⟶ p" 
  proof
    assume "q"
    show "p" using 1 by this
  qed
qed

lemma -- "p. 13"
  "p ⟶ (q ⟶ p)"
proof 
  assume "p"
  thus "q ⟶ p" by (rule impI)
qed

section {* Reglas de la negación *}

text {*
  La regla de eliminación de lo falso es
  · FalseE: False ⟹ P
  La regla de eliminación de la negación es
  · notE: ⟦¬P; P⟧ ⟹ R
  La regla de introducción de la negación es
  · notI: (P ⟹ False) ⟹ ¬P
*}

lemma -- "p. 15"
  assumes 1: "¬p ∨ q" 
  shows "p ⟶ q"
proof
  assume 2: "p"
  note 1
  thus "q"
  proof (rule disjE)
    { assume 3: "¬p"
      show "q" using 3 2 by (rule notE) }
  next
    { assume "q"
      thus "q" by this}
  qed
qed    

lemma -- "p. 16"
  assumes 1: "p ⟶ q" and 
          2: "p ⟶ ¬q" 
  shows "¬p"    
proof (rule notI)
  assume 3: "p"
  have 4: "q" using 1 3 by (rule mp)
  have 5: "¬q" using 2 3 by (rule mp)
  show False using 5 4 by (rule notE)
qed

lemma  
  assumes 1: "p ⟶ ¬p" 
  shows "¬p"
proof (rule notI)
  assume 2: "p"
  have 3: "¬p" using 1 2 by (rule mp)
  show False using 3 2 by (rule notE)
qed   

lemma 
  assumes 1: "p ∧ ¬q ⟶ r" and 
          2: "¬r" and 
          3: "p" 
  shows "q"    
proof -
  have "¬¬q"
  proof (rule notI)
    assume 4: "¬q"
    have 5: "p ∧ ¬q" using 3 4 by (rule conjI)
    have 6: "r" using 1 5 by (rule mp)
    show False using 2 6 by (rule notE)
  qed
  thus "q" by (rule notnotD)
qed

lemma 
  assumes 1: "p ⟶ (q ⟶ r)" and 
          2: "p" and 
          3: "¬r" 
  shows "¬q"
proof (rule notI)
  assume 4: "q"
  have 5: "q ⟶ r" using 1 2 by (rule mp)
  have 6: "r" using 5 4 by (rule mp)
  show False using 3 6 by (rule notE)
qed   

section {* Reglas del bicondicional *}

text {*
  La regla de introducción del bicondicional es
  · iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
  Las reglas de eliminación del bicondicional son
  · iffD1: ⟦Q = P; Q⟧ ⟹ P 
  · iffD2: ⟦P = Q; Q⟧ ⟹ P
*}

lemma -- "p. 17"
  "(p ∧ q) = (q ∧ p)"
proof (rule iffI)
  { assume 1: "p ∧ q"
    have 2: "p" using 1 by (rule conjunct1)
    have 3: "q" using 1 by (rule conjunct2)
    show "q ∧ p" using 3 2 by (rule conjI) }
next
  { assume 4: "q ∧ p"
    have 5: "q" using 4 by (rule conjunct1)
    have 6: "p" using 4 by (rule conjunct2)
    show "p ∧ q" using 6 5 by (rule conjI) }
qed

lemma -- "p. 18"
  assumes 1: "p = q" and 
          2: "p ∨ q"  
  shows "p ∧ q"
using 2
proof (rule disjE)
  { assume 3: "p"
    have 4: "q" using 1 3 by (rule iffD1)
    show "p ∧ q" using 3 4 by (rule conjI) }
next
  { assume 5: "q"
    have 6: "p" using 1 5 by (rule iffD2)
    show "p ∧ q" using 6 5 by (rule conjI) }
qed

section {* Reglas derivadas *}

subsection {* Regla del modus tollens *}

lemma -- "p. 20"
  assumes 1: "F ⟶ G" and 
          2: "¬G" 
  shows "¬F"
proof (rule notI)
  assume 3: "F"
  have 4: "G" using 1 3 by (rule mp)
  show False using 2 4 by (rule notE)
qed    

subsection {* Regla de la introducción de la doble negación *}

lemma -- "p. 21"
  assumes 1: "F" 
  shows "¬¬F"
proof (rule notI)
  assume 2: "¬F"
  show False using 2 1 by (rule notE)
qed    

subsection {* Regla de reducción al absurdo *}

lemma -- "p. 22" 
  assumes 1: "¬F ⟶ False" 
  shows "F"
proof -
  have 2: "¬¬F"
  proof (rule notI)
    assume 3: "¬F"
    show False using 1 3 by (rule mp)
  qed
  show "F" using 2 by (rule notnotD)
qed   

text {*
  La regla de reducción al absurdo en Isabelle se correponde con la
  regla de contradicción 
  · ccontr: (¬P ⟹ False) ⟹ P
*}

subsection {* Ley del tercio excluso *}

text {*
  La ley del tercio excluso es 
  · excluded_middle: ¬P ∨ P
  Puede demostrarse como se muestra a continuación.
*}

lemma -- "p. 23"
  "F ∨ ¬F"
proof (rule ccontr)
  assume 1: "¬(F ∨ ¬F)"
  thus False
  proof (rule notE)
    show "F ∨ ¬F"
    proof (rule disjI2)
      show "¬F"
      proof (rule notI)
        assume 2: "F"
        hence 3: "F ∨ ¬F" by (rule disjI1)
        show False using 1 3 by (rule notE)
      qed
    qed
  qed
qed
    
lemma -- "p. 24"
  assumes 1: "p ⟶ q" 
  shows "¬p ∨ q"
proof -
  have "¬p ∨ p" by (rule excluded_middle)
  thus "¬p ∨ q"
  proof (rule disjE)
    { assume "¬p"
      thus "¬p ∨ q" by (rule disjI1) }
  next
    { assume 2: "p"
      have "q" using 1 2 by (rule mp)
      thus "¬p ∨ q" by (rule disjI2) }
  qed
qed    

end