DAO (Demostración asistida por ordenador) DAO (Demostración asistida por ordenador)

header {* Tema 3: Deducción natural proposicional con Isabelle/HOL *}

theory T3 imports Main begin

text {*

 En esta sección 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. *}

subsection {* Reglas de la conjunción *}

text {*

 Ejemplo 1 (p. 4). Demostrar que
    p ∧ q, r ⊢ q ∧ r.
 *}     

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

• }

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) ..
 thus "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
 · "thus" para demostrar la conclusión usando el hecho anterior.
 Además, no es necesario usar and entre las hipótesis. *}

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. *}

text {* Se puede automatizar totalmente la demostración como sigue *}

lemma ejemplo_1_5:

 "⟦p ∧ q; r⟧ ⟹ q ∧ r"

by auto

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. *}

text {* Se puede hacer la demostración por razonamiento hacia atrás,

 como sigue *}

lemma ejemplo_1_6:

 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. *}

text {* Se pueden dejar implícitas las reglas como sigue *}

lemma ejemplo_1_7:

 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. *}

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

text {*

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

• }

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

-- "La demostración estructurada es" 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)
 hence "r" ..
 with `¬¬p` show  "¬¬p ∧ r" ..

qed

text {*

 Nota sobre el lenguaje: En la demostración anterior se ha usado
 · "hence" para indicar que se tiene por el hecho anterior,
 · `...` para referenciar un hecho y
 · "with P show Q" para indicar que con el hecho anterior junto con el
   hecho P se demuestra Q. *}

-- "La demostración automática es" lemma ejemplo_2_3:

 assumes "p" 
         "¬¬(q ∧ r)" 
 shows   "¬¬p ∧ r"

using assms by auto

text {* Se puede demostrar hacia atrás *}

lemma ejemplo_2_4:

 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) 
 thus "r" by (rule conjunct2)

qed

text {* Se puede eliminar las reglas en la demostración anterior, como

 sigue: *}

lemma ejemplo_2_5:

 assumes "p" 
         "¬¬(q ∧ r)" 
 shows   "¬¬p ∧ r"

proof

 show "¬¬p" using assms(1) ..

next

 have "q ∧ r" using assms(2) by (rule notnotD) 
 thus "r" .. 

qed

subsection {* 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 

• }

text {*

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

• }

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

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

-- "La demostración automática es" lemma ejemplo_3_3:

 assumes "¬p ∧ q"
         "¬p ∧ q ⟶ r ∨ ¬p" 
 shows   "r ∨ ¬p"

using assms by auto

text {*

 Ejemplo 4 (p. 6) Demostrar que
    p, p ⟶ q, p ⟶ (q ⟶ r) ⊢ r
*}

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

-- "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) ..
 thus "r" using `q` ..

qed

-- "La demostración automática es" lemma ejemplo_4_3:

 "⟦p; p ⟶ q; p ⟶ (q ⟶ r)⟧ ⟹ r"

by auto

subsection {* 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 auto

text {*

 Ejemplo 5 (p. 7). Demostrar
    p ⟶ (q ⟶ r), p, ¬r ⊢ ¬q
*}

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

-- "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) ..
 thus "¬q" using assms(3) by (rule mt)

qed

-- "La demostración automática es" lemma ejemplo_5_3:

 assumes "p ⟶ (q ⟶ r)"
         "p"
         "¬r" 
 shows   "¬q"

using assms by auto

text {*

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

• }

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

-- "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)
 thus "p" by (rule notnotD)

qed

-- "La demostración automática es" lemma ejemplo_6_3:

 "⟦¬p ⟶ q; ¬q⟧ ⟹ p"

by auto

text {*

 Ejemplo 7. (p. 7) Demostrar
    p ⟶ ¬q, q ⊢ ¬p
 *}

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

-- "La demostración estructurada es" lemma ejemplo_7_3:

 "⟦p ⟶ ¬q; q⟧ ⟹ ¬p"

by auto

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

text {*

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

• }

text {*

 Ejemplo 8. (p. 8) Demostrar
    p ⟶ q ⊢ ¬q ⟶ ¬p

• }

-- "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) } 
 thus "¬q ⟶ ¬p" by (rule impI)

qed

text {*

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

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

-- "La demostración automática es" lemma ejemplo_8_3:

 assumes "p ⟶ q" 
 shows "¬q ⟶ ¬p"

using assms by auto

text {*

 Ejemplo 9. (p. 9) Demostrar
    ¬q ⟶ ¬p ⊢ p ⟶ ¬¬q

• }

-- "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) } 
 thus "p ⟶ ¬¬q" by (rule impI)

qed

-- "La demostración estructurada es" lemma ejemplo_9_2:

 assumes "¬q ⟶ ¬p" 
 shows    "p ⟶ ¬¬q"   

proof

 assume "p"
 hence "¬¬p" by (rule notnotI)
 with assms show "¬¬q" by (rule mt)

qed

-- "La demostración automática es" lemma ejemplo_9_3:

 assumes "¬q ⟶ ¬p" 
 shows "p ⟶ ¬¬q"   

using assms by auto

text {*

 Ejemplo 10 (p. 9). Demostrar
    ⊢ p ⟶ p

• }

-- "La demostración detallada es" lemma ejemplo_10_1:

 "p ⟶ p"

proof -

 { assume 1: "p"
   have "p" using 1 by this }
 thus "p ⟶ p" by (rule impI) 

qed

-- "La demostración estructurada es" lemma ejemplo_10_2:

 "p ⟶ p"

proof (rule impI) qed

-- "La demostración automática es" lemma ejemplo_10_3:

 "p ⟶ p"

by auto

text {*

 Ejemplo 11 (p. 10) Demostrar
    ⊢ (q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))
*}

-- "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) } 
     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

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

-- "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"
     hence "¬¬p" ..
     with `¬q ⟶ ¬p` have "¬¬q" by (rule mt)
     hence "q" by (rule notnotD)
     with `q ⟶ r` show "r" ..
   qed
 qed

qed

-- "La demostración automática es" lemma ejemplo_11_5:

 "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"

by auto

subsection {* 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 

• }

text {*

 Ejemplo 12 (p. 11). Demostrar
    p ∨ q ⊢ q ∨ p

• }

-- "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. *}

-- "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"
   hence "q ∨ p" .. }
 moreover
 { assume "q"
   hence "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. *}

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

-- "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"
   thus "q ∨ p" .. }

next

 { assume "q"
   thus "q ∨ p" .. }

qed

-- "La demostración automática es" lemma ejemplo_12_5:

 assumes "p ∨ q" 
 shows "q ∨ p"

using assms by auto

text {*

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

• }

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

-- "La demostración estructurada es" lemma ejemplo_13_2:

 assumes "q ⟶ r"
 shows "p ∨ q ⟶ p ∨ r"

proof

 assume "p ∨ q"
 thus "p ∨ r"
 proof 
   { assume "p"
     thus "p ∨ r" .. }
 next
   { assume "q"
     have "r" using assms `q` ..
     thus "p ∨ r" .. }
 qed

qed

-- "La demostración automática es" lemma ejemplo_13_3:

 assumes "q ⟶ r"
 shows "p ∨ q ⟶ p ∨ r"

using assms by auto

subsection {* Regla de copia *}

text {*

 Ejemplo 14 (p. 13). Demostrar
    ⊢ p ⟶ (q ⟶ p)

• }

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

-- "La demostración estructurada es" lemma ejemplo_14_2:

 "p ⟶ (q ⟶ p)"

proof

 assume "p"
 thus "q ⟶ p" ..

qed

-- "La demostración automática es" lemma ejemplo_14_3:

 "p ⟶ (q ⟶ p)"

by auto

subsection {* 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

• }

text {*

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

• }

-- "La demostración detallada es" lemma ejemplo_15_1:

 assumes 1: "¬p ∨ q" 
 shows "p ⟶ q"

proof (rule impI)

 assume 2: "p"
 note 1
 thus "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

-- "La demostración estructurada es" lemma ejemplo_15_2:

 assumes "¬p ∨ q" 
 shows "p ⟶ q"

proof

 assume "p"
 note `¬p ∨ q`
 thus "q"
 proof
   { assume "¬p"
     thus "q" using `p` .. }
 next
   { assume "q"
     thus "q" . }
 qed

qed

-- "La demostración automática es" lemma ejemplo_15_3:

 assumes "¬p ∨ q" 
 shows "p ⟶ q"

using assms by auto

text {*

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

• }

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

-- "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` ..
 thus False using `q` ..

qed

-- "La demostración automática es" lemma ejemplo_16_3:

 assumes "p ⟶ q"
         "p ⟶ ¬q" 
 shows "¬p"    

using assms by auto

subsection {* 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

• }

text {*

 Ejemplo 17 (p. 17) Demostrar

• }

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

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

-- "La demostración automática es" lemma ejemplo_17_3:

 "(p ∧ q) ⟷ (q ∧ p)"

by auto

text {*

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

• }

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

-- "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" ..
   thus "p ∧ q" using `q` .. }

qed

-- "La demostración automática es" lemma ejemplo_18_3:

 assumes "p ⟷ q"
         "p ∨ q"  
 shows "p ∧ q"

using assms by auto

subsection {* Reglas derivadas *}

subsubsection {* Regla del modus tollens *}

text {*

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

• }

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

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

-- "La demostración automática es" lemma ejemplo_20_3:

 assumes "F ⟶ G"
         "¬G" 
 shows "¬F"

using assms by auto

subsubsection {* 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.

• }

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

-- "La demostración estructurada es" lemma ejemplo_21_2:

 assumes "F" 
 shows "¬¬F"

proof

 assume "¬F"
 thus False using assms ..

qed

-- "La demostración automática es" lemma ejemplo_21_3:

 assumes "F" 
 shows "¬¬F"

using assms by auto

subsubsection {* 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

• }

subsubsection {* 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.  

• }

-- "La demostración detallada es" lemma ejemplo_22_1:

 "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

-- "La demostración estructurada es" lemma ejemplo_22_2:

 "F ∨ ¬F"

proof (rule ccontr)

 assume "¬(F ∨ ¬F)"
 thus False
 proof (rule notE)
   show "F ∨ ¬F"
   proof (rule disjI2)
     show "¬F"
     proof (rule notI)
       assume "F"
       hence "F ∨ ¬F" ..
       with `¬(F ∨ ¬F)`show False ..
     qed
   qed
 qed

qed

-- "La demostración automática es" lemma ejemplo_22_3:

 "F ∨ ¬F"

using assms by auto

text {*

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

• }

-- "La demostración detallada es" lemma ejemplo_23_1:

 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

-- "La demostración estructurada es" lemma ejemplo_23_2:

 assumes "p ⟶ q" 
 shows "¬p ∨ q"

proof -

 have "¬p ∨ p" ..
 thus "¬p ∨ q"
 proof 
   { assume "¬p"
     thus "¬p ∨ q" .. }
 next
   { assume "p"
     with assms have "q" ..
     thus "¬p ∨ q" .. }
 qed

qed

-- "La demostración automática es" lemma ejemplo_23_3:

 assumes "p ⟶ q" 
 shows "¬p ∨ q"

using assms by auto

subsection {* Demostraciones por contradicción *}

text {*

 Ejemplo 24. Demostrar que 
    ¬p, p ∨ q ⊢ q

• }

-- "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"
 thus "q" by assumption

qed

-- "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"
 thus "q" .

qed

-- "La demostración automática es" lemma ejemplo_24_3:

 assumes "¬p"
         "p ∨ q"
 shows "q"

using assms by auto

end