Deducción natural proposicional con Isabelle/HOL

chapter ‹Tema 2a: Deducción natural proposicional con Isabelle/HOL›

theory T2a_Deduccion_natural_en_logica_proposicional_con_Isabelle
imports Main 
begin

text ‹En este tema 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://goo.gl/qsVpY y, más 
  concretamente, a la forma como se explica en la asignatura de 
  "Lógica informática" (LI) http://goo.gl/AwDiv
 
  La página al lado de cada ejemplo indica la página de las 
  transparencias de LI donde se encuentra la demostración.›

section ‹Reglas de la conjunción›

text ‹  Notas sobre la lógica: Las reglas de la conjunción son
  · conjI:      ⟦P; Q⟧ ⟹ P ∧ Q
  · conjunct1:  P ∧ Q ⟹ P
  · conjunct2:  P ∧ Q ⟹ Q  ›

thm conjI
thm conjunct1
thm conjunct2

subsection ‹Ejemplo 1›

text ‹Ejemplo 1 (p. 4). Demostrar que
     p ∧ q, r ⊢ q ∧ r. ›     

subsubsection ‹Demostración aplicativa›

lemma ejemplo_1: 
  "⟦p ∧ q; r⟧ ⟹ q ∧ r"
  apply (rule conjI)
   apply (erule conjunct2)
  apply assumption  
  done 

text ‹Nota sobre el lenguaje: En la demostración anterior se ha usado
  · "⟦ ... ⟧" para representar las hipótesis,
  · ";" para separar las hipótesis y
  · "⟹" para separar las hipótesis de la conclusión.›

subsubsection ‹Demostración detallada›

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

text ‹Notas sobre el lenguaje: En la demostración anterior se ha usado
  · "assumes" para indicar las hipótesis,
  · "and" para separar las hipótesis,
  · "shows" para indicar la conclusión,
  · "proof" para iniciar la prueba,
  · "qed" para terminar la pruebas,
  · "-" (después de "proof") para no usar el método por defecto,
  · "have" para establecer un paso,
  · "using" para usar hechos en un paso,
  · "by (rule ..)" para indicar la regla con la que se peueba un hecho,
  · "show" para establecer la conclusión.›

subsubsection ‹Demostración estructurada›

text ‹Se pueden dejar implícitas las reglas como sigue›

lemma ejemplo_1_2:
  assumes 1: "p ∧ q" and 
          2: "r" 
  shows "q ∧ r"     
proof -
  have 3: "q" using 1 .. 
  show 4: "q ∧ r" using 3 2 ..
qed

text ‹Nota sobre el lenguaje: En la demostración anterior se ha usado
  · ".." para indicar que se prueba por la regla correspondiente.›

text ‹Se pueden eliminar las etiquetas como sigue›

lemma ejemplo_1_3:
  assumes "p ∧ q" 
          "r" 
  shows   "q ∧ r"     
proof -
  have "q" using assms(1) ..
  then show "q ∧ r" using assms(2) ..
qed

text ‹
  Nota sobre el lenguaje: En la demostración anterior se ha usado
  · "assms(n)" para indicar la hipótesis n y
  · "then show" para demostrar la conclusión usando el hecho anterior.
  Además, no es necesario usar and entre las hipótesis.›

subsubsection ‹Demostración automática›

lemma ejemplo_1_4:
  assumes "p ∧ q" 
          "r" 
  shows   "q ∧ r"     
  using assms
  by auto

text ‹Nota sobre el lenguaje: En la demostración anterior se ha usado
  · "assms" para indicar las hipótesis y
  · "by auto" para demostrar la conclusión automáticamente.›

subsubsection ‹Demostración detallada hacia atrás›

text ‹Se puede hacer la demostración por razonamiento hacia atrás,
  como sigue›

lemma ejemplo_1_5:
  assumes "p ∧ q" 
      and "r" 
  shows   "q ∧ r"     
proof (rule conjI)
  show "q" using assms(1) by (rule conjunct2)
next
  show "r" using assms(2) by this
qed

text ‹Nota sobre el lenguaje: En la demostración anterior se ha usado
  · "proof (rule r)" para indicar que se hará la demostración con la
    regla r,
  · "next" para indicar el comienzo de la prueba del siguiente
    subobjetivo,
  · "this" para indicar el hecho actual.›

subsubsection ‹Demostración estructurada hacia atrás›

text ‹Se pueden dejar implícitas las reglas como sigue›

lemma ejemplo_1_6:
  assumes "p ∧ q" 
          "r" 
  shows   "q ∧ r"     
proof 
  show "q" using assms(1) ..
next
  show "r" using assms(2) . 
qed

text ‹Nota sobre el lenguaje: En la demostración anterior se ha usado
  · "." para indicar por el hecho actual.›

subsubsection ‹Demostraciones automáticas›

lemma ejemplo_1_7:
  assumes "p ∧ q" 
          "r" 
  shows   "q ∧ r"     
  using assms by simp

― ‹Se puede acortar como sigue›
lemma ejemplo_1_8_:
  "⟦p ∧ q; r⟧ ⟹ q ∧ r"
  by simp

section ‹Reglas de la doble negación›

subsection ‹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
  aunque, de momento, no detallamos su demostración.›

lemma notnotI [intro!]: "P ⟹ ¬¬ P"
  by auto

subsection ‹Ejemplo 2›

text ‹Ejemplo 2. (p. 5)
       p, ¬¬(q ∧ r) ⊢ ¬¬p ∧ r ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_2: 
  "⟦p; ¬¬(q ∧ r)⟧ ⟹ ¬¬p ∧ r"
  apply (rule conjI)
   apply (rule notnotI)
   apply assumption
  apply (drule notnotD)
  apply (erule conjunct2)
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_2_1:
  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 6: "¬¬p ∧ r" using 3 5 by (rule conjI)
qed        

subsubsection ‹Demostración estructurada›

― ‹Se puede eliminar etiquetas y reglas›
lemma ejemplo_2_2:
  assumes "p" 
          "¬¬(q ∧ r)" 
  shows   "¬¬p ∧ r"
proof -
  have "¬¬p" using assms(1) ..
  have "q ∧ r" using assms(2) by (rule notnotD)
  then have "r" ..
  with ‹¬¬p› show  "¬¬p ∧ r" ..
qed        

text ‹Nota sobre el lenguaje: En la demostración anterior se ha usado
  · ‹...› para referenciar un hecho y
  · "with P show Q" para indicar que con el hecho anterior junto con el
    hecho P se demuestra Q.›

subsubsection ‹Demostración detallada hacia atrás›

lemma ejemplo_2_3:
  assumes "p" 
          "¬¬(q ∧ r)" 
  shows   "¬¬p ∧ r"
proof  (rule conjI)
  show "¬¬p" using assms(1) by (rule notnotI)
next
  have "q ∧ r" using assms(2) by (rule notnotD) 
  then show "r" by (rule conjunct2)
qed 

subsubsection ‹Demostración estructurada hacia atrás›

text ‹Se puede eliminar las reglas en la demostración anterior, como
  sigue:›

lemma ejemplo_2_4:
  assumes "p" 
          "¬¬(q ∧ r)" 
  shows   "¬¬p ∧ r"
proof 
  show "¬¬p" using assms(1) ..
next
  have "q ∧ r" using assms(2) by (rule notnotD) 
  then show "r" .. 
qed

subsubsection ‹Demostraciones automáticas›

lemma ejemplo_2_5:
  assumes "p" 
          "¬¬(q ∧ r)" 
  shows   "¬¬p ∧ r"
  using assms
  by simp

― ‹Se puede simplificar›
lemma ejemplo_2_6: 
  "⟦p; ¬¬(q ∧ r)⟧ ⟹ ¬¬p ∧ r"
  by simp

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 ›

subsection ‹Ejemplo 3›

text ‹Ejemplo 3. (p. 6) Demostrar que
     ¬p ∧ q, ¬p ∧ q ⟶ r ∨ ¬p ⊢ r ∨ ¬p ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_3: 
  "⟦¬p ∧ q; ¬p ∧ q ⟶ r ∨ ¬p⟧ ⟹ r ∨ ¬p"
  apply (erule mp)
  apply assumption
  done

subsubsection ‹Demostración detallada›

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

subsubsection ‹Demostración estructurada›

lemma ejemplo_3_2:
  assumes "¬p ∧ q"
          "¬p ∧ q ⟶ r ∨ ¬p" 
  shows   "r ∨ ¬p"
proof -
  show "r ∨ ¬p" using assms(2,1) ..
qed    

subsubsection ‹Demostración automática›

lemma ejemplo_3_3:
  "⟦¬p ∧ q; ¬p ∧ q ⟶ r ∨ ¬p⟧ ⟹ r ∨ ¬p"
  by simp

subsection ‹Ejemplo 4›

text ‹Ejemplo 4 (p. 6) Demostrar que
     p, p ⟶ q, p ⟶ (q ⟶ r) ⊢ r ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_4:
  "⟦p; p ⟶ q; p ⟶ (q ⟶ r)⟧ ⟹ r"
  apply (drule mp)
   apply assumption
  apply (drule mp)
   apply assumption
  apply (drule mp)
   apply assumption+
  done    

subsubsection ‹Demostración detallada›

lemma ejemplo_4_1:
  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 6: "r" using 5 4 by (rule mp)
qed

subsubsection ‹Demostración estructurada›

lemma ejemplo_4_2:
  assumes "p"
          "p ⟶ q"
          "p ⟶ (q ⟶ r)" 
  shows "r"
proof -
  have "q" using assms(2,1) .. 
  have "q ⟶ r" using assms(3,1) ..
  then show "r" using ‹q› ..
qed

subsubsection ‹Demostración automática›

lemma ejemplo_4_3:
  "⟦p; p ⟶ q; p ⟶ (q ⟶ r)⟧ ⟹ r"
  by simp

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 
  aunque, de momento, sin detallar su demostración.›

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

subsection ‹Ejemplo 5›

text ‹Ejemplo 5 (p. 7). Demostrar
     p ⟶ (q ⟶ r), p, ¬r ⊢ ¬q ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_5: 
  "⟦p ⟶ (q ⟶ r); p; ¬r ⟧ ⟹ ¬q"
  apply (drule mp)
   apply assumption
  apply (erule mt)
  apply assumption
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_5_1:
  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    

subsubsection ‹Demostración estructurada›

lemma ejemplo_5_2:
  assumes "p ⟶ (q ⟶ r)"
          "p"
          "¬r" 
  shows   "¬q"
proof -
  have "q ⟶ r" using assms(1,2) ..
  then show "¬q" using assms(3) by (rule mt)
qed    

subsubsection ‹Demostración automática›

lemma ejemplo_5_3:
  assumes "p ⟶ (q ⟶ r)"
          "p"
          "¬r" 
  shows   "¬q"
  using assms
  by simp

lemma ejemplo_5_4: 
  "⟦p ⟶ (q ⟶ r); p; ¬r ⟧ ⟹ ¬q"
  by simp

subsection ‹Ejemplo 6›

text ‹Ejemplo 6. (p. 7) Demostrar 
     ¬p ⟶ q, ¬q ⊢ p ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_6: 
  "⟦¬p ⟶ q; ¬q⟧ ⟹ p"
  apply (drule mt)
   apply assumption
  apply (erule notnotD)
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_6_1:
  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

subsubsection ‹Demostración estructurada›

lemma ejemplo_6_2:
  assumes "¬p ⟶ q"
          "¬q" 
  shows   "p"
proof -
  have "¬¬p" using assms(1,2) by (rule mt)
  then show "p" by (rule notnotD)
qed

subsubsection ‹Demostración automática›

lemma ejemplo_6_3:
  "⟦¬p ⟶ q; ¬q⟧ ⟹ p"
  by simp

subsection ‹Ejemplo 7›

text ‹Ejemplo 7. (p. 7) Demostrar
     p ⟶ ¬q, q ⊢ ¬p ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_7: 
  "⟦p ⟶ ¬q; q⟧ ⟹ ¬p"  
  apply (erule mt)
  apply (erule notnotI)
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_7_1:
  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

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

subsubsection ‹Demostración automática›

lemma ejemplo_7_3:
  "⟦p ⟶ ¬q; q⟧ ⟹ ¬p"
  by simp

section ‹Regla de introducción del condicional›

text ‹La regla de introducción del condicional es
  · impI: (P ⟹ Q) ⟹ P ⟶ Q ›

subsection ‹Ejemplo 8›

text ‹Ejemplo 8. (p. 8) Demostrar
     p ⟶ q ⊢ ¬q ⟶ ¬p ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_8: 
  "p ⟶ q ⟹ ¬q ⟶ ¬p"
  apply (rule impI)
  apply (erule mt)
  apply assumption
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_8_1:
  assumes 1: "p ⟶ q" 
  shows "¬q ⟶ ¬p"
proof -
  { assume 2: "¬q"
    have "¬p" using 1 2 by (rule mt) } 
  then show "¬q ⟶ ¬p" by (rule impI)
qed    

text ‹Nota sobre el lenguaje: En la demostración anterior se ha usado
  · "{ ... }" para representar una caja.›

subsubsection ‹Demostración estructurada›

lemma ejemplo_8_2:
  assumes "p ⟶ q" 
  shows "¬q ⟶ ¬p"
proof 
  assume "¬q"
  with assms show "¬p" by (rule mt)
qed    

subsubsection ‹Demostración automática›

lemma ejemplo_8_3:
  assumes "p ⟶ q" 
  shows "¬q ⟶ ¬p"
  using assms
  by auto

subsection ‹Ejemplo 9›

text ‹Ejemplo 9. (p. 9) Demostrar
     ¬q ⟶ ¬p ⊢ p ⟶ ¬¬q ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_9: 
  "¬q ⟶ ¬p ⟹ p ⟶ ¬¬q"  
  apply (rule impI)
  apply (erule mt)
  apply (erule notnotI)
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_9_1: 
  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) } 
  then show "p ⟶ ¬¬q" by (rule impI)
qed

subsubsection ‹Demostración estructurada›

lemma ejemplo_9_2:
  assumes "¬q ⟶ ¬p" 
  shows    "p ⟶ ¬¬q"   
proof 
  assume "p"
  then have "¬¬p" by (rule notnotI)
  with assms show "¬¬q" by (rule mt)
qed

subsubsection ‹Demostración automática›

lemma ejemplo_9_3:
  assumes "¬q ⟶ ¬p" 
  shows "p ⟶ ¬¬q"   
  using assms
  by auto 

subsection ‹Ejemplo 10›

text ‹Ejemplo 10 (p. 9). Demostrar
     ⊢ p ⟶ p ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_10: 
  "p ⟶ p"
  apply (rule impI)
  apply assumption
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_10_1:
  "p ⟶ p"
proof -
  { assume 1: "p"
    have "p" using 1 by this }
  then show "p ⟶ p" by (rule impI) 
qed

subsubsection ‹Demostración estructurada›

lemma ejemplo_10_2:
  "p ⟶ p"
proof (rule impI)
qed

subsubsection ‹Demostración automática›

lemma ejemplo_10_3:
  "p ⟶ p"
  by simp 

subsection ‹Ejemplo 11›

text ‹Ejemplo 11 (p. 10) Demostrar
     ⊢ (q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_11:
  "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"  
  apply (rule impI)+  
  apply (erule mp)
  apply (drule mt)
   apply (erule notnotI)
  apply (erule notnotD)
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_11_1:
  "(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) } 
      then have "p ⟶ r" by (rule impI) } 
    then have "(¬q ⟶ ¬p) ⟶ p ⟶ r" by (rule impI) } 
  then show "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ p ⟶ r)" by (rule impI)
qed

― ‹La demostración hacia atrás es›
lemma ejemplo_11_2:
  "(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

subsubsection ‹Demostración estructurada›

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

― ‹La demostración sin etiquetas es› 
lemma ejemplo_11_4:
  "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
proof
  assume "q ⟶ r"
  show "(¬q ⟶ ¬p) ⟶ (p ⟶ r)"
  proof
    assume "¬q ⟶ ¬p"
    show "p ⟶ r"
    proof
      assume "p"
      then have "¬¬p" ..
      with ‹¬q ⟶ ¬p› have "¬¬q" by (rule mt)
      then have "q" by (rule notnotD)
      with ‹q ⟶ r› show "r" ..
    qed
  qed
qed

subsubsection ‹Demostración automática›

lemma ejemplo_11_5:
  "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
  by auto

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  ›

subsection ‹Ejemplo 12›

text ‹Ejemplo 12 (p. 11). Demostrar
     p ∨ q ⊢ q ∨ p ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_12: 
  "p ∨ q ⟹ q ∨ p"  
  apply (erule disjE)
   apply (erule disjI2)
   apply (erule disjI1)
  done

subsubsection ‹Demostración detallada›

― ‹La demostración detallada es›
lemma ejemplo_12_1:
  assumes "p ∨ q" 
  shows "q ∨ p"
proof -
  have "p ∨ q" using assms by this
  moreover
  { assume 2: "p"
    have "q ∨ p" using 2 by (rule disjI2) }
  moreover
  { assume 3: "q"
    have "q ∨ p" using 3 by (rule disjI1) }
  ultimately show "q ∨ p" by (rule disjE) 
qed    

text ‹
  Nota sobre el lenguaje: En la demostración anterior se ha usado
  · "moreover" para separar los bloques y
  · "ultimately" para unir los resultados de los bloques.›

subsubsection ‹Demostración estructurada›

― ‹La demostración detallada con reglas implícitas es›
lemma ejemplo_12_2:
  assumes "p ∨ q" 
  shows "q ∨ p"
proof -
  note ‹p ∨ q›
  moreover
  { assume "p"
    then have "q ∨ p" .. }
  moreover
  { assume "q"
    then have "q ∨ p" .. }
  ultimately show "q ∨ p" ..
qed    

text ‹Nota sobre el lenguaje: En la demostración anterior se ha usado
  · "note" para copiar un hecho.›

subsubsection ‹Demostración detallada hacia atrás›

lemma ejemplo_12_3:
  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    

subsubsection ‹Demostración estructurada hacia atrás›

lemma ejemplo_12_4:
  assumes "p ∨ q" 
  shows "q ∨ p"
using assms
proof 
  { assume  "p"
    then show "q ∨ p" .. }
next
  { assume "q"
    then show "q ∨ p" .. }
qed    

subsubsection ‹Demostración automática›

lemma ejemplo_12_5:
  assumes "p ∨ q" 
  shows "q ∨ p"
  using assms
  by auto

subsection ‹Ejemplo 13›

text ‹Ejemplo 13. (p. 12) Demostrar
     q ⟶ r ⊢ p ∨ q ⟶ p ∨ r ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_13: 
  "q ⟶ r ⟹ p ∨ q ⟶ p ∨ r"  
  apply (rule impI)
  apply (erule disjE)
   apply (erule disjI1)
  apply (drule mp)
   apply assumption
  apply (erule disjI2)
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_13_1:
  assumes 1: "q ⟶ r"
  shows "p ∨ q ⟶ p ∨ r"
proof (rule impI)
  assume 2: "p ∨ q"
  then show "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    

subsubsection ‹Demostración estructurada›

lemma ejemplo_13_2:
  assumes "q ⟶ r"
  shows "p ∨ q ⟶ p ∨ r"
proof 
  assume "p ∨ q"
  then show "p ∨ r"
  proof 
    { assume "p"
      then show "p ∨ r" .. }
  next
    { assume "q"
      have "r" using assms ‹q› ..
      then show "p ∨ r" .. }
  qed
qed    

subsubsection ‹Demostración automática›

lemma ejemplo_13_3:
  assumes "q ⟶ r"
  shows "p ∨ q ⟶ p ∨ r"
  using assms
  by auto

section ‹Regla de copia›

subsection ‹Ejemplo 14›

text ‹Ejemplo 14 (p. 13). Demostrar
     ⊢ p ⟶ (q ⟶ p) ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_14: 
  "p ⟶ (q ⟶ p)"  
  apply (rule impI)+
  apply assumption
  done

subsubsection ‹Demostración detallada›

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

subsubsection ‹Demostración estructurada›

lemma ejemplo_14_2:
  "p ⟶ (q ⟶ p)"
proof 
  assume "p"
  then show "q ⟶ p" ..
qed

subsubsection ‹Demostración automática›

lemma ejemplo_14_3:
  "p ⟶ (q ⟶ p)"
  by simp 

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 ›

subsection ‹Ejemplo 15›

text ‹Ejemplo 15 (p. 15). Demostrar
     ¬p ∨ q ⊢ p ⟶ q ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_15: 
  "¬p ∨ q ⟹ p ⟶ q"  
  apply (rule impI)
  apply (erule disjE)
   apply (erule notE)
   apply assumption+
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_15_1:
  assumes 1: "¬p ∨ q" 
  shows "p ⟶ q"
proof (rule impI)
  assume 2: "p"
  note 1
  then show "q"
  proof (rule disjE)
    { assume 3: "¬p"
      show "q" using 3 2 by (rule notE) }
  next
    { assume 4: "q"
      show "q" using 4 by this}
  qed
qed    

subsubsection ‹Demostración estructurada›

lemma ejemplo_15_2:
  assumes "¬p ∨ q" 
  shows "p ⟶ q"
proof 
  assume "p"
  note ‹¬p ∨ q›
  then show "q"
  proof
    assume "¬p"
    then show "q" using ‹p› .. 
  next
    assume "q"
      then show "q" .
  qed
qed    

subsubsection ‹Demostración automática›

lemma ejemplo_15_3:
  assumes "¬p ∨ q" 
  shows "p ⟶ q"
  using assms
  by auto

subsection ‹Ejemplo 16›

text ‹Ejemplo 16 (p. 16). Demostrar
     p ⟶ q, p ⟶ ¬q ⊢ ¬p ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_16: 
  "⟦p ⟶ q; p ⟶ ¬q⟧ ⟹ ¬p"  
  apply (rule notI)
  apply (drule mp)+
    apply assumption+
  apply (drule mp)
   apply assumption
  apply (erule notE)
  apply assumption
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_16_1:
  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

subsubsection ‹Demostración estructurada›

lemma ejemplo_16_2:
  assumes "p ⟶ q"
          "p ⟶ ¬q" 
  shows "¬p"    
proof 
  assume "p"
  have "q" using assms(1) ‹p› ..
  have "¬q" using assms(2) ‹p› ..
  then show False using ‹q› ..
qed

subsubsection ‹Demostración automática›

lemma ejemplo_16_3:
  assumes "p ⟶ q"
          "p ⟶ ¬q" 
  shows "¬p"    
  using assms
  by simp 

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 ›

subsection ‹Ejemplo 17›

text ‹Ejemplo 17 (p. 17) Demostrar
     (p ∧ q) ⟷ (q ∧ p) ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_17_4: 
  "(p ∧ q) ⟷ (q ∧ p)"  
  apply (rule iffI)
   apply (rule conjI)
    apply (erule conjunct2)
   apply (erule conjunct1)
    apply (rule conjI)
    apply (erule conjunct2)
  apply (erule conjunct1)
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_17_1:
  "(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

subsubsection ‹Demostración estructurada›

lemma ejemplo_17_2:
  "(p ∧ q) ⟷ (q ∧ p)"
proof 
  { assume 1: "p ∧ q"
    have "p" using 1 ..
    have "q" using 1 ..
    show "q ∧ p" using ‹q› ‹p› .. }
next
  { assume 2: "q ∧ p"
    have "q" using 2 ..
    have "p" using 2 ..
    show "p ∧ q" using ‹p› ‹q›  .. }
qed

subsubsection ‹Demostración automática›

lemma ejemplo_17_3:
  "(p ∧ q) ⟷ (q ∧ p)"
  by auto

subsection ‹Ejemplo 18›

text ‹Ejemplo 18 (p. 18). Demostrar
     p ⟷ q, p ∨ q ⊢ p ∧ q ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_18_4: 
  "⟦p ⟷ q; p ∨ q⟧ ⟹ p ∧ q"  
  apply (erule disjE)
   apply (rule conjI)
    apply assumption
   apply (erule iffD1)
   apply assumption
  apply (rule conjI)
   apply (erule iffD2)
   apply assumption+
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_18_1:
  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

subsubsection ‹Demostración estructurada›

lemma ejemplo_18_2:
  assumes "p ⟷ q"
          "p ∨ q"  
  shows  "p ∧ q"
using assms(2)
proof
  { assume "p"
    with assms(1) have "q" ..
    with ‹p› show "p ∧ q" .. }
next
  { assume "q"
    with assms(1) have "p" ..
    then show "p ∧ q" using ‹q› .. }
qed

subsubsection ‹Demostración automática›

lemma ejemplo_18_3:
  assumes "p ⟷ q"
          "p ∨ q"  
  shows "p ∧ q"
  using assms
  by simp 

section ‹Reglas derivadas›

subsection ‹Regla del modus tollens›

text ‹Ejemplo 19 (p. 20) Demostrar la regla del modus tollens a partir 
  de las reglas básicas.›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_20: 
  "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"  
  apply (rule notI)
  apply (drule mp)
   apply assumption
  apply (erule notE)
  apply assumption
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_20_1:
  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    

subsubsection ‹Demostración estructurada›

lemma ejemplo_20_2:
  assumes "F ⟶ G"
          "¬G" 
  shows   "¬F"
proof 
  assume "F"
  with assms(1) have "G" ..
  with assms(2) show False ..
qed    

subsubsection ‹Demostración automática›

lemma ejemplo_20_3:
  assumes "F ⟶ G"
          "¬G" 
  shows "¬F"
  using assms
  by simp 

subsection ‹Regla de la introducción de la doble negación›

text ‹Ejemplo 21 (p. 21) Demostrar la regla de introducción de la doble
  negación a partir de las reglas básicas.›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_21: 
  "F ⟹ ¬¬F"  
  apply (rule notI)
  apply (erule notE)
  apply assumption
  done

subsubsection ‹Demostración detallada›

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

subsubsection ‹Demostración estructurada›

lemma ejemplo_21_2:
  assumes "F" 
  shows "¬¬F"
proof 
  assume "¬F"
  then show False using assms ..
qed    

subsubsection ‹Demostración automática›

lemma ejemplo_21_3:
  assumes "F" 
  shows "¬¬F"
  using assms
  by simp 

subsection ‹Regla de reducción al absurdo›

text ‹La regla de reducción al absurdo en Isabelle se correponde con la
  regla clásica de contradicción 
  · ccontr: (¬P ⟹ False) ⟹ P ›

subsection ‹Ley del tercio excluso›

text ‹La ley del tercio excluso es 
  · excluded_middle: ¬P ∨ P ›

text ‹Ejemplo 22 (p. 23). Demostrar la ley del tercio excluso a partir de
  las reglas básicas.›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_22:
  "F ∨ ¬F"
  apply (rule ccontr)
  apply (rule_tac P="F" in notE)
   apply (rule notI)
   apply (erule notE)
   apply (erule disjI1)
  apply (rule notnotD)
  apply (rule notI)
  apply (erule notE)
  apply (erule disjI2)
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_22_1:
  "F ∨ ¬F"
proof (rule ccontr)
  assume 1: "¬(F ∨ ¬F)"
  then show False
  proof (rule notE)
    show "F ∨ ¬F"
    proof (rule disjI2)
      show "¬F"
      proof (rule notI)
        assume 2: "F"
        then have 3: "F ∨ ¬F" by (rule disjI1)
        show False using 1 3 by (rule notE)
      qed
    qed
  qed
qed

subsubsection ‹Demostración estructurada›

lemma ejemplo_22_2:
  "F ∨ ¬F"
proof (rule ccontr)
  assume "¬(F ∨ ¬F)"
  then show False
  proof (rule notE)
    show "F ∨ ¬F"
    proof (rule disjI2)
      show "¬F"
      proof (rule notI)
        assume "F"
        then have "F ∨ ¬F" ..
        with ‹¬(F ∨ ¬F)› show False ..
      qed
    qed
  qed
qed

subsubsection ‹Demostración automática›

lemma ejemplo_22_3:
  "F ∨ ¬F"
  by simp 

subsection ‹Ejemplo 23›

text ‹Ejemplo 23 (p. 24). Demostrar
     p ⟶ q ⊢ ¬p ∨ q ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_23: 
  "p ⟶ q ⟹ ¬p ∨ q"
  apply (cut_tac P="p" in excluded_middle)
  apply (erule disjE)
   apply (erule disjI1)
  apply (drule mp)
   apply assumption
  apply (erule disjI2)
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_23_1:
  assumes 1: "p ⟶ q" 
  shows "¬p ∨ q"
proof -
  have "¬p ∨ p" by (rule excluded_middle)
  then show "¬p ∨ q"
  proof (rule disjE)
    { assume "¬p"
      then show "¬p ∨ q" by (rule disjI1) }
  next
    { assume 2: "p"
      have "q" using 1 2 by (rule mp)
      then show "¬p ∨ q" by (rule disjI2) }
  qed
qed    

subsubsection ‹Demostración estructurada›

lemma ejemplo_23_2:
  assumes "p ⟶ q" 
  shows "¬p ∨ q"
proof -
  have "¬p ∨ p" ..
  then show "¬p ∨ q"
  proof 
    { assume "¬p"
      then show "¬p ∨ q" .. }
  next
    { assume "p"
      with assms have "q" ..
      then show "¬p ∨ q" .. }
  qed
qed    

subsubsection ‹Demostración automática›

lemma ejemplo_23_3:
  assumes "p ⟶ q" 
  shows "¬p ∨ q"
  using assms
  by simp 

section ‹Demostraciones por contradicción›

subsection ‹Ejemplo 24›

text ‹Ejemplo 24. Demostrar que 
     ¬p, p ∨ q ⊢ q ›

subsubsection ‹Demostración aplicativa›

lemma ejemplo_24_4: 
  "⟦¬p ; p ∨ q⟧ ⟹ q"  
  apply (erule disjE)
   apply (erule notE)
   apply assumption+
  done

subsubsection ‹Demostración detallada›

lemma ejemplo_24_1:
  assumes "¬p"
          "p ∨ q"
  shows   "q"
using ‹p ∨ q›
proof (rule disjE)
  assume "p"
  with assms(1) show "q" by contradiction 
next
  assume "q"
  then show "q" by assumption
qed

subsubsection ‹Demostración estructurada›

lemma ejemplo_24_2:
  assumes "¬p"
          "p ∨ q"
  shows "q"
using ‹p ∨ q›
proof 
  assume "p"
  with assms(1) show "q" ..
next
  assume "q"
  then show "q" .
qed

subsubsection ‹Demostración automática›

lemma ejemplo_24_3:
  assumes "¬p"
          "p ∨ q"
  shows "q"
  using assms
  by simp 

end