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›

subsection ‹Ejemplo 1›

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

subsubsection ‹Demostración detallada›

― ‹La demostración detallada es›
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.

  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  
›

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›

text ‹Se puede automatizar la demostración como sigue›
  
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›

― ‹La demostración automática es›
lemma ejemplo_1_8_:
  "⟦p ∧ q; r⟧ ⟹ q ∧ r"
  by simp

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 aplicativa›

― ‹La demostración aplicativa es›
lemma ejemplo_1_9: 
  "⟦p ∧ q; r⟧ ⟹ q ∧ r"
  apply (rule conjI)
   apply (erule conjunct2)
  apply assumption  
  done 

text ‹Explicaciones:
  apply (rule conjI)
  + Objetivo:         ⟦p ∧ q; r⟧ ⟹ q ∧ r
  + conjI:            ⟦?P; ?Q⟧ ⟹ ?P ∧ ?Q
  + Unificador de     q ∧ r
    y                 ?P ∧ ?Q
    es                ?P/q, ?Q/r
  + Nuevos objetivos: ⟦p ∧ q; r⟧ ⟹ q
                      ⟦p ∧ q; r⟧ ⟹ r  

  apply (erule conjunct2)
  + Objetivo:         ⟦p ∧ q; r⟧ ⟹ q
  + conjunct2:        ?P ∧ ?Q ⟹ ?Q
  + Unificador de     p ∧ q
    y                 ?P ∧ ?Q
    es                ?P/p, ?Q/q
  + Nuevo objetivo:   Nada  
›

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 detallada›

― ‹La demostración detallada es›
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›

text ‹Se puede demostrar 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›

― ‹La demostración automática es›
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

subsubsection ‹Demostración aplicativa›

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

text ‹Explicaciones:
  apply (rule conjI)
  + Objetivo:         ⟦p; ¬¬(q ∧ r)⟧ ⟹ ¬¬p ∧ r
  + conjI:            ⟦?P; ?Q⟧ ⟹ ?P ∧ ?Q
  + Unificador de     ¬¬p ∧ r
    y                 ?P ∧ ?Q
    es                ?P/¬¬p, ?Q/r
  + Nuevos objetivos: ⟦p; ¬ ¬ (q ∧ r)⟧ ⟹ ¬ ¬ p
                      ⟦p; ¬ ¬ (q ∧ r)⟧ ⟹ r  

  apply (rule notnotI)
  + Objetivo:         ⟦p; ¬ ¬ (q ∧ r)⟧ ⟹ ¬ ¬ p
  + notnotI:          ?P ⟹ ¬ ¬ ?P
  + Unificador de     ¬ ¬ p
    y                 ¬ ¬ ?P
    es                ?P/p
  + Nuevo objetivo:   ⟦p; ¬ ¬ (q ∧ r)⟧ ⟹ p  

  apply (drule notnotD)
  + Objetivo:         ⟦p; ¬ ¬ (q ∧ r)⟧ ⟹ r
  + notnotD:          ¬ ¬ ?P ⟹ ?P
  + Unificador de     ¬ ¬ (q ∧ r)
    y                 ¬ ¬ ?P
    es                ?P/(q ∧ r)
  + Nuevo objetivo:   ⟦p; q ∧ r⟧ ⟹ r  

  apply (erule conjunct2)
  + Objetivo:         ⟦p; q ∧ r⟧ ⟹ r
  + conjunct2:        ?P ∧ ?Q ⟹ ?Q
  + Unificador de     q ∧ r
    y                 ?P ∧ ?Q
    es                ?P/q, ?Q/r
  + Nuevo objetivo:   Nada  
›

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 detallada›

― ‹La demostración detallada es›
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›

― ‹La demostración estructurada es›
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 aplicativa›

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

text ‹Explicaciones:
  apply (erule mp)
  + Objetivo:         ⟦¬p ∧ q; ¬p ∧ q ⟶ r ∨ ¬p⟧ ⟹ r ∨ ¬p
  + mp:               ⟦?P ⟶ ?Q; ?P⟧ ⟹ ?Q
  + Unificador de     ¬p ∧ q ⟶ r ∨ ¬p 
    y                 ?P ⟶ ?Q
    es                ?P/¬p ∧ q, ?Q/r ∨ ¬p
  + Nuevos objetivos: ¬ p ∧ q ⟹ ¬ p ∧ q  
›

subsubsection ‹Demostración automática›

lemma ejemplo_3_4:
  "⟦¬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 detallada›

― ‹La demostración detallada es›
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›

― ‹La demostración estructurada es›
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 aplicativa›

lemma ejemplo_4_3:
  "⟦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 automática›

lemma ejemplo_4_4:
  "⟦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 detallada›

― ‹La demostración detallada es›
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›

― ‹La demostración estructurada es›
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

subsubsection ‹Demostración aplicativa›

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

subsection ‹Ejemplo 6›

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

subsubsection ‹Demostración detallada›

― ‹La demostración detallada es›
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›

― ‹La demostración estructurada es›
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

subsubsection ‹Demostración aplicativa›

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

subsection ‹Ejemplo 7›

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

subsubsection ‹Demostración detallada›

― ‹La demostración detallada es›
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

― ‹La demostración detallada es›
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

subsubsection ‹Demostración aplicativa›

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

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 detallada›

― ‹La demostración detallada es›
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›

― ‹La demostración estructurada es›
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

subsubsection ‹Demostración automática›

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

subsection ‹Ejemplo 9›

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

subsubsection ‹Demostración detallada›

― ‹La demostración detallada es›
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›

― ‹La demostración estructurada es›
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›

― ‹La demostración automática es›
lemma ejemplo_9_3:
  assumes "¬q ⟶ ¬p" 
  shows "p ⟶ ¬¬q"   
  using assms
  by auto 

subsubsection ‹Demostración aplicativa›

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

subsection ‹Ejemplo 10›

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

subsubsection ‹Demostración detallada›

― ‹La demostración detallada es›
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›

― ‹La demostración estructurada es›
lemma ejemplo_10_2:
  "p ⟶ p"
proof (rule impI)
qed

subsubsection ‹Demostración automática›

― ‹La demostración automática es›
lemma ejemplo_10_3:
  "p ⟶ p"
  by simp 

subsubsection ‹Demostración aplicativa›

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

subsection ‹Ejemplo 11›

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

subsubsection ‹Demostración detallada›

― ‹La demostración detallada es›
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›

― ‹La demostración hacia atrás con reglas implícitas es›
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›

― ‹La demostración automática es›
lemma ejemplo_11_5:
  "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
  by auto

subsubsection ‹Demostración aplicativa›

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

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 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›

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

― ‹La demostración hacia atrás con reglas implícitas es›
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›

― ‹La demostración automática es›
lemma ejemplo_12_5:
  assumes "p ∨ q" 
  shows "q ∨ p"
  using assms
  by auto

subsubsection ‹Demostración aplicativa›

lemma ejemplo_12_6: 
  "p ∨ q ⟹ q ∨ p"  
  apply (erule disjE)
   apply (rule disjI2)
   prefer 2
   apply (rule disjI1)
   apply assumption+ 
  done

subsection ‹Ejemplo 13›

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

subsubsection ‹Demostración detallada›

― ‹La demostración detallada es› 
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›

― ‹La demostración estructurada es› 
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›

― ‹La demostración automática es› 
lemma ejemplo_13_3:
  assumes "q ⟶ r"
  shows "p ∨ q ⟶ p ∨ r"
  using assms
  by auto

subsubsection ‹Demostración aplicativa›

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

section ‹Regla de copia›

subsection ‹Ejemplo 14›

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

subsubsection ‹Demostración detallada›

― ‹La demostración detallada es›
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›

― ‹La demostración estructurada es›
lemma ejemplo_14_2:
  "p ⟶ (q ⟶ p)"
proof 
  assume "p"
  then show "q ⟶ p" ..
qed

subsubsection ‹Demostración automática›

― ‹La demostración automática es›
lemma ejemplo_14_3:
  "p ⟶ (q ⟶ p)"
  by simp 

subsubsection ‹Demostración aplicativa›

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

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 detallada›

― ‹La demostración detallada es›
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›

― ‹La demostración estructurada es›
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›

― ‹La demostración automática es›
lemma ejemplo_15_3:
  assumes "¬p ∨ q" 
  shows "p ⟶ q"
  using assms
  by auto

subsubsection ‹Demostración aplicativa›

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

subsection ‹Ejemplo 16›

text ‹Ejemplo 16 (p. 16). Demostrar
     p ⟶ q, p ⟶ ¬q ⊢ ¬p
›
subsubsection ‹Demostración detallada›

― ‹La demostración detallada es›
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›

― ‹La demostración estructurada es›
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›

― ‹La demostración automática es›
lemma ejemplo_16_3:
  assumes "p ⟶ q"
          "p ⟶ ¬q" 
  shows "¬p"    
  using assms
  by simp 

subsubsection ‹Demostración aplicativa›

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

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 detallada›

― ‹La demostración detallada es›
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›

― ‹La demostración estructurada es›
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›

― ‹La demostración automática es›
lemma ejemplo_17_3:
  "(p ∧ q) ⟷ (q ∧ p)"
  by auto

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

subsection ‹Ejemplo 18›

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

subsubsection ‹Demostración detallada›

― ‹La demostración detallada es›
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›

― ‹La demostración estructurada es›
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›

― ‹La demostración automática es›
lemma ejemplo_18_3:
  assumes "p ⟷ q"
          "p ∨ q"  
  shows "p ∧ q"
  using assms
  by simp 

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

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 detallada›

― ‹La demostración detallada es›
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›

― ‹La demostración estructurada es›
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›

― ‹La demostración automática es›
lemma ejemplo_20_3:
  assumes "F ⟶ G"
          "¬G" 
  shows "¬F"
  using assms
  by simp 

subsubsection ‹Demostración aplicativa›

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

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 detallada›

― ‹La demostración detallada es›
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›

― ‹La demostración estructurada es›
lemma ejemplo_21_2:
  assumes "F" 
  shows "¬¬F"
proof 
  assume "¬F"
  then show False using assms ..
qed    

subsubsection ‹Demostración automática›

― ‹La demostración automática es›
lemma ejemplo_21_3:
  assumes "F" 
  shows "¬¬F"
  using assms
  by simp 

subsubsection ‹Demostración aplicativa›

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

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 detallada›

― ‹La demostración detallada es›
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›

― ‹La demostración estructurada es›
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›

― ‹La demostración automática es›
lemma ejemplo_22_3:
  "F ∨ ¬F"
  using assms
  by simp 

subsection ‹Ejemplo 23›

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

subsubsection ‹Demostración detallada›

― ‹La demostración detallada es›
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›

― ‹La demostración estructurada es›
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›

― ‹La demostración automática es›
lemma ejemplo_23_3:
  assumes "p ⟶ q" 
  shows "¬p ∨ q"
  using assms
  by simp 

subsubsection ‹Demostración aplicativa›

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

section ‹Demostraciones por contradicción›

subsection ‹Ejemplo 24›

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

subsubsection ‹Demostración detallada›

― ‹La demostración detallada es›
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›

― ‹La demostración estructurada es›
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›

― ‹La demostración automática es›
lemma ejemplo_24_3:
  assumes "¬p"
          "p ∨ q"
  shows "q"
  using assms
  by simp 

subsubsection ‹Demostración aplicativa›

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

end