chapter ‹Tema 6: Deducción natural proposicional con Isabelle/HOL›
theory T6_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
