Diferencia entre revisiones de «Deducción natural proposicional con Isabelle/HOL»
De Lógica matemática y fundamentos (2018-19)
(No se muestran 2 ediciones intermedias del mismo usuario) | |||
Línea 1: | Línea 1: | ||
<source lang="isabelle"> | <source lang="isabelle"> | ||
− | chapter | + | chapter ‹Tema 2a: Deducción natural proposicional con Isabelle/HOL› |
theory T2a_Deduccion_natural_en_logica_proposicional_con_Isabelle | theory T2a_Deduccion_natural_en_logica_proposicional_con_Isabelle | ||
Línea 6: | Línea 6: | ||
begin | begin | ||
− | text | + | 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 | |
− | proposicional siguiendo la presentación de Huth y Ryan en su | + | libro "Logic in Computer Science" http://goo.gl/qsVpY y, más |
− | "Logic in Computer Science" http://goo.gl/qsVpY y, más concretamente, | + | 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 | + | 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 | + | text ‹ Notas sobre la lógica: Las reglas de la conjunción son |
− | + | · conjI: ⟦P; Q⟧ ⟹ P ∧ Q | |
− | p ∧ q, r ⊢ q ∧ r. | + | · 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: | lemma ejemplo_1_1: | ||
assumes 1: "p ∧ q" and | assumes 1: "p ∧ q" and | ||
Línea 32: | Línea 56: | ||
qed | qed | ||
− | text | + | text ‹Notas sobre el lenguaje: En la demostración anterior se ha usado |
− | |||
· "assumes" para indicar las hipótesis, | · "assumes" para indicar las hipótesis, | ||
· "and" para separar las hipótesis, | · "and" para separar las hipótesis, | ||
Línea 43: | Línea 66: | ||
· "using" para usar hechos en un paso, | · "using" para usar hechos en un paso, | ||
· "by (rule ..)" para indicar la regla con la que se peueba un hecho, | · "by (rule ..)" para indicar la regla con la que se peueba un hecho, | ||
− | · "show" para establecer la conclusión. | + | · "show" para establecer la conclusión.› |
− | + | subsubsection ‹Demostración estructurada› | |
− | |||
− | |||
− | |||
− | |||
− | text | + | text ‹Se pueden dejar implícitas las reglas como sigue› |
lemma ejemplo_1_2: | lemma ejemplo_1_2: | ||
Línea 62: | Línea 81: | ||
qed | qed | ||
− | text | + | text ‹Nota sobre el lenguaje: En la demostración anterior se ha usado |
− | + | · ".." para indicar que se prueba por la regla correspondiente.› | |
− | · ".." para indicar que se prueba por la regla correspondiente. | ||
− | text | + | text ‹Se pueden eliminar las etiquetas como sigue› |
lemma ejemplo_1_3: | lemma ejemplo_1_3: | ||
Línea 74: | Línea 92: | ||
proof - | proof - | ||
have "q" using assms(1) .. | have "q" using assms(1) .. | ||
− | + | then show "q ∧ r" using assms(2) .. | |
qed | qed | ||
− | text | + | text ‹ |
Nota sobre el lenguaje: En la demostración anterior se ha usado | Nota sobre el lenguaje: En la demostración anterior se ha usado | ||
· "assms(n)" para indicar la hipótesis n y | · "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. | + | Además, no es necesario usar and entre las hipótesis.› |
+ | |||
+ | subsubsection ‹Demostración automática› | ||
− | |||
− | |||
lemma ejemplo_1_4: | lemma ejemplo_1_4: | ||
assumes "p ∧ q" | assumes "p ∧ q" | ||
"r" | "r" | ||
shows "q ∧ r" | shows "q ∧ r" | ||
− | using assms | + | using assms |
− | by auto | + | by auto |
− | text | + | text ‹Nota sobre el lenguaje: En la demostración anterior se ha usado |
− | |||
· "assms" para indicar las hipótesis y | · "assms" para indicar las hipótesis y | ||
− | · "by auto" para demostrar la conclusión automáticamente. | + | · "by auto" para demostrar la conclusión automáticamente.› |
+ | |||
+ | subsubsection ‹Demostración detallada hacia atrás› | ||
− | text | + | text ‹Se puede hacer la demostración por razonamiento hacia atrás, |
+ | como sigue› | ||
lemma ejemplo_1_5: | lemma ejemplo_1_5: | ||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
assumes "p ∧ q" | assumes "p ∧ q" | ||
and "r" | and "r" | ||
Línea 122: | Línea 129: | ||
qed | qed | ||
− | text | + | 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 | · "proof (rule r)" para indicar que se hará la demostración con la | ||
regla r, | regla r, | ||
· "next" para indicar el comienzo de la prueba del siguiente | · "next" para indicar el comienzo de la prueba del siguiente | ||
subobjetivo, | subobjetivo, | ||
− | · "this" para indicar el hecho actual. | + | · "this" para indicar el hecho actual.› |
+ | |||
+ | subsubsection ‹Demostración estructurada hacia atrás› | ||
− | text | + | text ‹Se pueden dejar implícitas las reglas como sigue› |
− | lemma | + | lemma ejemplo_1_6: |
assumes "p ∧ q" | assumes "p ∧ q" | ||
"r" | "r" | ||
Línea 142: | Línea 150: | ||
qed | qed | ||
− | text | + | text ‹Nota sobre el lenguaje: En la demostración anterior se ha usado |
− | + | · "." para indicar por el hecho actual.› | |
− | · "." 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 | + | subsection ‹Reglas de la doble negación› |
− | text | + | text ‹La regla de eliminación de la doble negación es |
− | |||
· notnotD: ¬¬ P ⟹ P | · notnotD: ¬¬ P ⟹ P | ||
Línea 155: | Línea 176: | ||
introducción de la doble negación | introducción de la doble negación | ||
· notnotI: P ⟹ ¬¬ P | · notnotI: P ⟹ ¬¬ P | ||
− | aunque, de momento, no detallamos su demostración. | + | aunque, de momento, no detallamos su demostración.› |
− | |||
lemma notnotI [intro!]: "P ⟹ ¬¬ P" | lemma notnotI [intro!]: "P ⟹ ¬¬ P" | ||
− | by auto | + | 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: | lemma ejemplo_2_1: | ||
assumes 1: "p" and | assumes 1: "p" and | ||
Línea 178: | Línea 210: | ||
qed | qed | ||
− | ― | + | subsubsection ‹Demostración estructurada› |
+ | |||
+ | ― ‹Se puede eliminar etiquetas y reglas› | ||
lemma ejemplo_2_2: | lemma ejemplo_2_2: | ||
assumes "p" | assumes "p" | ||
Línea 184: | Línea 218: | ||
shows "¬¬p ∧ r" | shows "¬¬p ∧ r" | ||
proof - | proof - | ||
− | have | + | have "¬¬p" using assms(1) .. |
− | have | + | have "q ∧ r" using assms(2) by (rule notnotD) |
− | + | then have "r" .. | |
− | with | + | with ‹¬¬p› show "¬¬p ∧ r" .. |
qed | qed | ||
− | text | + | 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 | · "with P show Q" para indicar que con el hecho anterior junto con el | ||
− | hecho P se demuestra Q. | + | hecho P se demuestra Q.› |
+ | |||
+ | subsubsection ‹Demostración detallada hacia atrás› | ||
− | |||
lemma ejemplo_2_3: | lemma ejemplo_2_3: | ||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
assumes "p" | assumes "p" | ||
"¬¬(q ∧ r)" | "¬¬(q ∧ r)" | ||
Línea 215: | Línea 239: | ||
next | next | ||
have "q ∧ r" using assms(2) by (rule notnotD) | have "q ∧ r" using assms(2) by (rule notnotD) | ||
− | + | then show "r" by (rule conjunct2) | |
qed | qed | ||
− | + | subsubsection ‹Demostración estructurada hacia atrás› | |
− | |||
− | lemma | + | text ‹Se puede eliminar las reglas en la demostración anterior, como |
+ | sigue:› | ||
+ | |||
+ | lemma ejemplo_2_4: | ||
assumes "p" | assumes "p" | ||
"¬¬(q ∧ r)" | "¬¬(q ∧ r)" | ||
Línea 229: | Línea 255: | ||
next | next | ||
have "q ∧ r" using assms(2) by (rule notnotD) | have "q ∧ r" using assms(2) by (rule notnotD) | ||
− | + | then show "r" .. | |
qed | 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 | + | text ‹La regla de eliminación del condicional es la regla del modus |
− | + | ponens | |
− | · mp: ⟦P ⟶ Q; P⟧ ⟹ Q | + | · mp: ⟦P ⟶ Q; P⟧ ⟹ Q › |
− | |||
− | text | + | subsection ‹Ejemplo 3› |
− | + | ||
− | ¬p ∧ q, ¬p ∧ q ⟶ r ∨ ¬p ⊢ r ∨ ¬p | + | 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: | lemma ejemplo_3_1: | ||
assumes 1: "¬p ∧ q" and | assumes 1: "¬p ∧ q" and | ||
Línea 253: | Línea 301: | ||
qed | qed | ||
− | + | subsubsection ‹Demostración estructurada› | |
+ | |||
lemma ejemplo_3_2: | lemma ejemplo_3_2: | ||
assumes "¬p ∧ q" | assumes "¬p ∧ q" | ||
Línea 262: | Línea 311: | ||
qed | qed | ||
− | + | subsubsection ‹Demostración automática› | |
+ | |||
lemma ejemplo_3_3: | 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: | lemma ejemplo_4_1: | ||
assumes 1: "p" and | assumes 1: "p" and | ||
Línea 287: | Línea 347: | ||
qed | qed | ||
− | + | subsubsection ‹Demostración estructurada› | |
+ | |||
lemma ejemplo_4_2: | lemma ejemplo_4_2: | ||
assumes "p" | assumes "p" | ||
Línea 296: | Línea 357: | ||
have "q" using assms(2,1) .. | have "q" using assms(2,1) .. | ||
have "q ⟶ r" using assms(3,1) .. | have "q ⟶ r" using assms(3,1) .. | ||
− | + | then show "r" using ‹q› .. | |
qed | qed | ||
− | + | subsubsection ‹Demostración automática› | |
+ | |||
lemma ejemplo_4_3: | lemma ejemplo_4_3: | ||
"⟦p; p ⟶ q; p ⟶ (q ⟶ r)⟧ ⟹ r" | "⟦p; p ⟶ q; p ⟶ (q ⟶ r)⟧ ⟹ r" | ||
− | by | + | by simp |
− | + | section ‹Regla derivada del modus tollens› | |
− | text | + | text ‹Para ajustarnos al tema de LI vamos a introducir la regla del |
− | + | modus tollens | |
− | tollens | ||
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F | · mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F | ||
− | aunque, de momento, sin detallar su demostración. | + | aunque, de momento, sin detallar su demostración.› |
− | |||
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F" | lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F" | ||
− | by | + | 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: | lemma ejemplo_5_1: | ||
assumes 1: "p ⟶ (q ⟶ r)" and | assumes 1: "p ⟶ (q ⟶ r)" and | ||
Línea 332: | Línea 403: | ||
qed | qed | ||
− | + | subsubsection ‹Demostración estructurada› | |
+ | |||
lemma ejemplo_5_2: | lemma ejemplo_5_2: | ||
assumes "p ⟶ (q ⟶ r)" | assumes "p ⟶ (q ⟶ r)" | ||
Línea 340: | Línea 412: | ||
proof - | proof - | ||
have "q ⟶ r" using assms(1,2) .. | have "q ⟶ r" using assms(1,2) .. | ||
− | + | then show "¬q" using assms(3) by (rule mt) | |
qed | qed | ||
− | + | subsubsection ‹Demostración automática› | |
+ | |||
lemma ejemplo_5_3: | lemma ejemplo_5_3: | ||
assumes "p ⟶ (q ⟶ r)" | assumes "p ⟶ (q ⟶ r)" | ||
Línea 349: | Línea 422: | ||
"¬r" | "¬r" | ||
shows "¬q" | shows "¬q" | ||
− | using assms | + | using assms |
− | by | + | 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: | lemma ejemplo_6_1: | ||
assumes 1: "¬p ⟶ q" and | assumes 1: "¬p ⟶ q" and | ||
Línea 367: | Línea 454: | ||
qed | qed | ||
− | + | subsubsection ‹Demostración estructurada› | |
+ | |||
lemma ejemplo_6_2: | lemma ejemplo_6_2: | ||
assumes "¬p ⟶ q" | assumes "¬p ⟶ q" | ||
Línea 374: | Línea 462: | ||
proof - | proof - | ||
have "¬¬p" using assms(1,2) by (rule mt) | have "¬¬p" using assms(1,2) by (rule mt) | ||
− | + | then show "p" by (rule notnotD) | |
qed | qed | ||
− | + | subsubsection ‹Demostración automática› | |
+ | |||
lemma ejemplo_6_3: | lemma ejemplo_6_3: | ||
"⟦¬p ⟶ q; ¬q⟧ ⟹ p" | "⟦¬p ⟶ q; ¬q⟧ ⟹ p" | ||
− | by | + | 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: | lemma ejemplo_7_1: | ||
assumes 1: "p ⟶ ¬q" and | assumes 1: "p ⟶ ¬q" and | ||
Línea 397: | Línea 495: | ||
qed | qed | ||
− | |||
lemma ejemplo_7_2: | lemma ejemplo_7_2: | ||
assumes "p ⟶ ¬q" | assumes "p ⟶ ¬q" | ||
Línea 407: | Línea 504: | ||
qed | qed | ||
− | + | subsubsection ‹Demostración automática› | |
+ | |||
lemma ejemplo_7_3: | lemma ejemplo_7_3: | ||
"⟦p ⟶ ¬q; q⟧ ⟹ ¬p" | "⟦p ⟶ ¬q; q⟧ ⟹ ¬p" | ||
− | by | + | by simp |
+ | |||
+ | section ‹Regla de introducción del condicional› | ||
+ | |||
+ | text ‹La regla de introducción del condicional es | ||
+ | · impI: (P ⟹ Q) ⟹ P ⟶ Q › | ||
− | subsection | + | subsection ‹Ejemplo 8› |
− | text | + | 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: | lemma ejemplo_8_1: | ||
assumes 1: "p ⟶ q" | assumes 1: "p ⟶ q" | ||
Línea 431: | Línea 537: | ||
{ assume 2: "¬q" | { assume 2: "¬q" | ||
have "¬p" using 1 2 by (rule mt) } | have "¬p" using 1 2 by (rule mt) } | ||
− | + | then show "¬q ⟶ ¬p" by (rule impI) | |
qed | qed | ||
− | text | + | text ‹Nota sobre el lenguaje: En la demostración anterior se ha usado |
− | + | · "{ ... }" para representar una caja.› | |
− | · "{ ... }" para representar una caja. | + | |
+ | subsubsection ‹Demostración estructurada› | ||
− | |||
lemma ejemplo_8_2: | lemma ejemplo_8_2: | ||
assumes "p ⟶ q" | assumes "p ⟶ q" | ||
Línea 447: | Línea 553: | ||
qed | qed | ||
− | + | subsubsection ‹Demostración automática› | |
+ | |||
lemma ejemplo_8_3: | lemma ejemplo_8_3: | ||
assumes "p ⟶ q" | assumes "p ⟶ q" | ||
shows "¬q ⟶ ¬p" | shows "¬q ⟶ ¬p" | ||
− | using assms | + | using assms |
− | by auto | + | 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: | lemma ejemplo_9_1: | ||
assumes 1: "¬q ⟶ ¬p" | assumes 1: "¬q ⟶ ¬p" | ||
Línea 467: | Línea 584: | ||
have 3: "¬¬p" using 2 by (rule notnotI) | have 3: "¬¬p" using 2 by (rule notnotI) | ||
have "¬¬q" using 1 3 by (rule mt) } | have "¬¬q" using 1 3 by (rule mt) } | ||
− | + | then show "p ⟶ ¬¬q" by (rule impI) | |
qed | qed | ||
− | + | subsubsection ‹Demostración estructurada› | |
+ | |||
lemma ejemplo_9_2: | lemma ejemplo_9_2: | ||
assumes "¬q ⟶ ¬p" | assumes "¬q ⟶ ¬p" | ||
Línea 476: | Línea 594: | ||
proof | proof | ||
assume "p" | assume "p" | ||
− | + | then have "¬¬p" by (rule notnotI) | |
with assms show "¬¬q" by (rule mt) | with assms show "¬¬q" by (rule mt) | ||
qed | qed | ||
− | + | subsubsection ‹Demostración automática› | |
+ | |||
lemma ejemplo_9_3: | lemma ejemplo_9_3: | ||
assumes "¬q ⟶ ¬p" | assumes "¬q ⟶ ¬p" | ||
shows "p ⟶ ¬¬q" | shows "p ⟶ ¬¬q" | ||
− | using assms | + | using assms |
− | by auto | + | 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: | lemma ejemplo_10_1: | ||
"p ⟶ p" | "p ⟶ p" | ||
Línea 498: | Línea 626: | ||
{ assume 1: "p" | { assume 1: "p" | ||
have "p" using 1 by this } | have "p" using 1 by this } | ||
− | + | then show "p ⟶ p" by (rule impI) | |
qed | qed | ||
− | + | subsubsection ‹Demostración estructurada› | |
+ | |||
lemma ejemplo_10_2: | lemma ejemplo_10_2: | ||
"p ⟶ p" | "p ⟶ p" | ||
Línea 507: | Línea 636: | ||
qed | qed | ||
− | + | subsubsection ‹Demostración automática› | |
+ | |||
lemma ejemplo_10_3: | lemma ejemplo_10_3: | ||
"p ⟶ p" | "p ⟶ p" | ||
− | by | + | 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: | lemma ejemplo_11_1: | ||
"(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))" | "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))" | ||
Línea 528: | Línea 670: | ||
have 6: "q" using 5 by (rule notnotD) | have 6: "q" using 5 by (rule notnotD) | ||
have "r" using 1 6 by (rule mp) } | 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 | qed | ||
Línea 552: | Línea 694: | ||
qed | qed | ||
− | + | subsubsection ‹Demostración estructurada› | |
+ | |||
lemma ejemplo_11_3: | lemma ejemplo_11_3: | ||
"(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))" | "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))" | ||
Línea 582: | Línea 725: | ||
proof | proof | ||
assume "p" | assume "p" | ||
− | + | then have "¬¬p" .. | |
− | with | + | with ‹¬q ⟶ ¬p› have "¬¬q" by (rule mt) |
− | + | then have "q" by (rule notnotD) | |
− | with | + | with ‹q ⟶ r› show "r" .. |
qed | qed | ||
qed | qed | ||
qed | qed | ||
− | + | subsubsection ‹Demostración automática› | |
+ | |||
lemma ejemplo_11_5: | lemma ejemplo_11_5: | ||
"(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))" | "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))" | ||
− | by auto | + | by auto |
− | + | section ‹Reglas de la disyunción› | |
− | text | + | text ‹Las reglas de la introducción de la disyunción son |
− | |||
· disjI1: P ⟹ P ∨ Q | · disjI1: P ⟹ P ∨ Q | ||
· disjI2: Q ⟹ P ∨ Q | · disjI2: Q ⟹ P ∨ Q | ||
La regla de elimación de la disyunción es | La regla de elimación de la disyunción es | ||
− | · disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R | + | · disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R › |
− | |||
− | text | + | subsection ‹Ejemplo 12› |
− | + | ||
− | p ∨ q ⊢ q ∨ p | + | 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› | ― ‹La demostración detallada es› | ||
Línea 625: | Línea 778: | ||
qed | qed | ||
− | text | + | text ‹ |
Nota sobre el lenguaje: En la demostración anterior se ha usado | Nota sobre el lenguaje: En la demostración anterior se ha usado | ||
· "moreover" para separar los bloques y | · "moreover" para separar los bloques y | ||
− | · "ultimately" para unir los resultados de los bloques. | + | · "ultimately" para unir los resultados de los bloques.› |
− | + | ||
+ | subsubsection ‹Demostración estructurada› | ||
+ | |||
― ‹La demostración detallada con reglas implícitas es› | ― ‹La demostración detallada con reglas implícitas es› | ||
lemma ejemplo_12_2: | lemma ejemplo_12_2: | ||
Línea 635: | Línea 790: | ||
shows "q ∨ p" | shows "q ∨ p" | ||
proof - | proof - | ||
− | note | + | note ‹p ∨ q› |
moreover | moreover | ||
{ assume "p" | { assume "p" | ||
− | + | then have "q ∨ p" .. } | |
moreover | moreover | ||
{ assume "q" | { assume "q" | ||
− | + | then have "q ∨ p" .. } | |
ultimately show "q ∨ p" .. | ultimately show "q ∨ p" .. | ||
qed | qed | ||
− | text | + | text ‹Nota sobre el lenguaje: En la demostración anterior se ha usado |
− | + | · "note" para copiar un hecho.› | |
− | · "note" para copiar un hecho. | + | |
+ | subsubsection ‹Demostración detallada hacia atrás› | ||
− | |||
lemma ejemplo_12_3: | lemma ejemplo_12_3: | ||
assumes 1: "p ∨ q" | assumes 1: "p ∨ q" | ||
Línea 662: | Línea 817: | ||
qed | qed | ||
− | + | subsubsection ‹Demostración estructurada hacia atrás› | |
+ | |||
lemma ejemplo_12_4: | lemma ejemplo_12_4: | ||
assumes "p ∨ q" | assumes "p ∨ q" | ||
Línea 669: | Línea 825: | ||
proof | proof | ||
{ assume "p" | { assume "p" | ||
− | + | then show "q ∨ p" .. } | |
next | next | ||
{ assume "q" | { assume "q" | ||
− | + | then show "q ∨ p" .. } | |
qed | qed | ||
− | + | subsubsection ‹Demostración automática› | |
+ | |||
lemma ejemplo_12_5: | lemma ejemplo_12_5: | ||
assumes "p ∨ q" | assumes "p ∨ q" | ||
shows "q ∨ p" | shows "q ∨ p" | ||
− | using assms | + | using assms |
− | by auto | + | 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: | lemma ejemplo_13_1: | ||
assumes 1: "q ⟶ r" | assumes 1: "q ⟶ r" | ||
Línea 693: | Línea 863: | ||
proof (rule impI) | proof (rule impI) | ||
assume 2: "p ∨ q" | assume 2: "p ∨ q" | ||
− | + | then show "p ∨ r" | |
proof (rule disjE) | proof (rule disjE) | ||
{ assume 3: "p" | { assume 3: "p" | ||
Línea 704: | Línea 874: | ||
qed | qed | ||
− | + | subsubsection ‹Demostración estructurada› | |
+ | |||
lemma ejemplo_13_2: | lemma ejemplo_13_2: | ||
assumes "q ⟶ r" | assumes "q ⟶ r" | ||
Línea 710: | Línea 881: | ||
proof | proof | ||
assume "p ∨ q" | assume "p ∨ q" | ||
− | + | then show "p ∨ r" | |
proof | proof | ||
{ assume "p" | { assume "p" | ||
− | + | then show "p ∨ r" .. } | |
next | next | ||
{ assume "q" | { assume "q" | ||
− | have "r" using assms | + | have "r" using assms ‹q› .. |
− | + | then show "p ∨ r" .. } | |
qed | qed | ||
qed | qed | ||
− | + | subsubsection ‹Demostración automática› | |
+ | |||
lemma ejemplo_13_3: | lemma ejemplo_13_3: | ||
assumes "q ⟶ r" | assumes "q ⟶ r" | ||
shows "p ∨ q ⟶ p ∨ r" | shows "p ∨ q ⟶ p ∨ r" | ||
− | using assms | + | using assms |
− | by auto | + | 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: | lemma ejemplo_14_1: | ||
"p ⟶ (q ⟶ p)" | "p ⟶ (q ⟶ p)" | ||
Línea 747: | Línea 928: | ||
qed | qed | ||
− | + | subsubsection ‹Demostración estructurada› | |
+ | |||
lemma ejemplo_14_2: | lemma ejemplo_14_2: | ||
"p ⟶ (q ⟶ p)" | "p ⟶ (q ⟶ p)" | ||
proof | proof | ||
assume "p" | assume "p" | ||
− | + | then show "q ⟶ p" .. | |
qed | qed | ||
− | + | subsubsection ‹Demostración automática› | |
+ | |||
lemma ejemplo_14_3: | lemma ejemplo_14_3: | ||
"p ⟶ (q ⟶ p)" | "p ⟶ (q ⟶ p)" | ||
− | by | + | by simp |
− | + | section ‹Reglas de la negación› | |
− | text | + | text ‹La regla de eliminación de lo falso es |
− | |||
· FalseE: False ⟹ P | · FalseE: False ⟹ P | ||
La regla de eliminación de la negación es | La regla de eliminación de la negación es | ||
· notE: ⟦¬P; P⟧ ⟹ R | · notE: ⟦¬P; P⟧ ⟹ R | ||
La regla de introducción de la negación es | La regla de introducción de la negación es | ||
− | · notI: (P ⟹ False) ⟹ ¬P | + | · 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: | lemma ejemplo_15_1: | ||
assumes 1: "¬p ∨ q" | assumes 1: "¬p ∨ q" | ||
Línea 783: | Línea 975: | ||
assume 2: "p" | assume 2: "p" | ||
note 1 | note 1 | ||
− | + | then show "q" | |
proof (rule disjE) | proof (rule disjE) | ||
{ assume 3: "¬p" | { assume 3: "¬p" | ||
Línea 793: | Línea 985: | ||
qed | qed | ||
− | + | subsubsection ‹Demostración estructurada› | |
+ | |||
lemma ejemplo_15_2: | lemma ejemplo_15_2: | ||
assumes "¬p ∨ q" | assumes "¬p ∨ q" | ||
Línea 799: | Línea 992: | ||
proof | proof | ||
assume "p" | assume "p" | ||
− | note | + | note ‹¬p ∨ q› |
− | + | then show "q" | |
proof | proof | ||
assume "¬p" | assume "¬p" | ||
− | + | then show "q" using ‹p› .. | |
next | next | ||
assume "q" | assume "q" | ||
− | + | then show "q" . | |
qed | qed | ||
qed | qed | ||
− | + | subsubsection ‹Demostración automática› | |
+ | |||
lemma ejemplo_15_3: | lemma ejemplo_15_3: | ||
assumes "¬p ∨ q" | assumes "¬p ∨ q" | ||
shows "p ⟶ q" | shows "p ⟶ q" | ||
− | using assms | + | using assms |
− | by auto | + | 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: | lemma ejemplo_16_1: | ||
assumes 1: "p ⟶ q" and | assumes 1: "p ⟶ q" and | ||
Línea 834: | Línea 1042: | ||
qed | qed | ||
− | + | subsubsection ‹Demostración estructurada› | |
+ | |||
lemma ejemplo_16_2: | lemma ejemplo_16_2: | ||
assumes "p ⟶ q" | assumes "p ⟶ q" | ||
Línea 841: | Línea 1050: | ||
proof | proof | ||
assume "p" | assume "p" | ||
− | have "q" using assms(1) | + | have "q" using assms(1) ‹p› .. |
− | have "¬q" using assms(2) | + | have "¬q" using assms(2) ‹p› .. |
− | + | then show False using ‹q› .. | |
qed | qed | ||
− | + | subsubsection ‹Demostración automática› | |
+ | |||
lemma ejemplo_16_3: | lemma ejemplo_16_3: | ||
assumes "p ⟶ q" | assumes "p ⟶ q" | ||
"p ⟶ ¬q" | "p ⟶ ¬q" | ||
shows "¬p" | shows "¬p" | ||
− | using assms | + | using assms |
− | by | + | by simp |
− | + | section ‹Reglas del bicondicional› | |
− | text | + | text ‹La regla de introducción del bicondicional es |
− | |||
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P ⟷ Q | · iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P ⟷ Q | ||
Las reglas de eliminación del bicondicional son | Las reglas de eliminación del bicondicional son | ||
· iffD1: ⟦Q ⟷ P; Q⟧ ⟹ P | · iffD1: ⟦Q ⟷ P; Q⟧ ⟹ P | ||
− | · iffD2: ⟦P ⟷ Q; 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: | lemma ejemplo_17_1: | ||
"(p ∧ q) ⟷ (q ∧ p)" | "(p ∧ q) ⟷ (q ∧ p)" | ||
Línea 884: | Línea 1106: | ||
qed | qed | ||
− | + | subsubsection ‹Demostración estructurada› | |
+ | |||
lemma ejemplo_17_2: | lemma ejemplo_17_2: | ||
"(p ∧ q) ⟷ (q ∧ p)" | "(p ∧ q) ⟷ (q ∧ p)" | ||
Línea 891: | Línea 1114: | ||
have "p" using 1 .. | have "p" using 1 .. | ||
have "q" using 1 .. | have "q" using 1 .. | ||
− | show "q ∧ p" using | + | show "q ∧ p" using ‹q› ‹p› .. } |
next | next | ||
{ assume 2: "q ∧ p" | { assume 2: "q ∧ p" | ||
have "q" using 2 .. | have "q" using 2 .. | ||
have "p" using 2 .. | have "p" using 2 .. | ||
− | show "p ∧ q" using | + | show "p ∧ q" using ‹p› ‹q› .. } |
qed | qed | ||
− | + | subsubsection ‹Demostración automática› | |
+ | |||
lemma ejemplo_17_3: | lemma ejemplo_17_3: | ||
"(p ∧ q) ⟷ (q ∧ p)" | "(p ∧ q) ⟷ (q ∧ p)" | ||
− | by auto | + | 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: | lemma ejemplo_18_1: | ||
assumes 1: "p ⟷ q" and | assumes 1: "p ⟷ q" and | ||
Línea 925: | Línea 1164: | ||
qed | qed | ||
− | + | subsubsection ‹Demostración estructurada› | |
+ | |||
lemma ejemplo_18_2: | lemma ejemplo_18_2: | ||
assumes "p ⟷ q" | assumes "p ⟷ q" | ||
Línea 934: | Línea 1174: | ||
{ assume "p" | { assume "p" | ||
with assms(1) have "q" .. | with assms(1) have "q" .. | ||
− | with | + | with ‹p› show "p ∧ q" .. } |
next | next | ||
{ assume "q" | { assume "q" | ||
with assms(1) have "p" .. | with assms(1) have "p" .. | ||
− | + | then show "p ∧ q" using ‹q› .. } | |
qed | qed | ||
− | + | subsubsection ‹Demostración automática› | |
+ | |||
lemma ejemplo_18_3: | lemma ejemplo_18_3: | ||
assumes "p ⟷ q" | assumes "p ⟷ q" | ||
"p ∨ q" | "p ∨ q" | ||
shows "p ∧ q" | shows "p ∧ q" | ||
− | using assms | + | using assms |
− | by | + | 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: | lemma ejemplo_20_1: | ||
assumes 1: "F ⟶ G" and | assumes 1: "F ⟶ G" and | ||
Línea 969: | Línea 1220: | ||
qed | qed | ||
− | + | subsubsection ‹Demostración estructurada› | |
+ | |||
lemma ejemplo_20_2: | lemma ejemplo_20_2: | ||
assumes "F ⟶ G" | assumes "F ⟶ G" | ||
Línea 980: | Línea 1232: | ||
qed | qed | ||
− | + | subsubsection ‹Demostración automática› | |
+ | |||
lemma ejemplo_20_3: | lemma ejemplo_20_3: | ||
assumes "F ⟶ G" | assumes "F ⟶ G" | ||
"¬G" | "¬G" | ||
shows "¬F" | shows "¬F" | ||
− | using assms | + | using assms |
− | by | + | 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: | lemma ejemplo_21_1: | ||
assumes 1: "F" | assumes 1: "F" | ||
Línea 1004: | Línea 1265: | ||
qed | qed | ||
− | + | subsubsection ‹Demostración estructurada› | |
+ | |||
lemma ejemplo_21_2: | lemma ejemplo_21_2: | ||
assumes "F" | assumes "F" | ||
Línea 1010: | Línea 1272: | ||
proof | proof | ||
assume "¬F" | assume "¬F" | ||
− | + | then show False using assms .. | |
qed | qed | ||
− | + | subsubsection ‹Demostración automática› | |
+ | |||
lemma ejemplo_21_3: | lemma ejemplo_21_3: | ||
assumes "F" | assumes "F" | ||
shows "¬¬F" | shows "¬¬F" | ||
− | using assms | + | using assms |
− | by | + | by simp |
− | + | subsection ‹Regla de reducción al absurdo› | |
− | text | + | text ‹La regla de reducción al absurdo en Isabelle se correponde con la |
− | |||
regla clásica de contradicción | regla clásica de contradicción | ||
− | · ccontr: (¬P ⟹ False) ⟹ P | + | · 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 | + | 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: | lemma ejemplo_22_1: | ||
"F ∨ ¬F" | "F ∨ ¬F" | ||
proof (rule ccontr) | proof (rule ccontr) | ||
assume 1: "¬(F ∨ ¬F)" | assume 1: "¬(F ∨ ¬F)" | ||
− | + | then show False | |
proof (rule notE) | proof (rule notE) | ||
show "F ∨ ¬F" | show "F ∨ ¬F" | ||
Línea 1052: | Línea 1325: | ||
proof (rule notI) | proof (rule notI) | ||
assume 2: "F" | assume 2: "F" | ||
− | + | then have 3: "F ∨ ¬F" by (rule disjI1) | |
show False using 1 3 by (rule notE) | show False using 1 3 by (rule notE) | ||
qed | qed | ||
Línea 1058: | Línea 1331: | ||
qed | qed | ||
qed | qed | ||
− | + | ||
− | + | subsubsection ‹Demostración estructurada› | |
+ | |||
lemma ejemplo_22_2: | lemma ejemplo_22_2: | ||
"F ∨ ¬F" | "F ∨ ¬F" | ||
proof (rule ccontr) | proof (rule ccontr) | ||
assume "¬(F ∨ ¬F)" | assume "¬(F ∨ ¬F)" | ||
− | + | then show False | |
proof (rule notE) | proof (rule notE) | ||
show "F ∨ ¬F" | show "F ∨ ¬F" | ||
Línea 1071: | Línea 1345: | ||
proof (rule notI) | proof (rule notI) | ||
assume "F" | assume "F" | ||
− | + | then have "F ∨ ¬F" .. | |
− | with | + | with ‹¬(F ∨ ¬F)› show False .. |
qed | qed | ||
qed | qed | ||
qed | qed | ||
qed | qed | ||
− | + | ||
− | + | subsubsection ‹Demostración automática› | |
+ | |||
lemma ejemplo_22_3: | lemma ejemplo_22_3: | ||
"F ∨ ¬F" | "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: | lemma ejemplo_23_1: | ||
assumes 1: "p ⟶ q" | assumes 1: "p ⟶ q" | ||
Línea 1095: | Línea 1382: | ||
proof - | proof - | ||
have "¬p ∨ p" by (rule excluded_middle) | have "¬p ∨ p" by (rule excluded_middle) | ||
− | + | then show "¬p ∨ q" | |
proof (rule disjE) | proof (rule disjE) | ||
{ assume "¬p" | { assume "¬p" | ||
− | + | then show "¬p ∨ q" by (rule disjI1) } | |
next | next | ||
{ assume 2: "p" | { assume 2: "p" | ||
have "q" using 1 2 by (rule mp) | have "q" using 1 2 by (rule mp) | ||
− | + | then show "¬p ∨ q" by (rule disjI2) } | |
qed | qed | ||
qed | qed | ||
− | + | subsubsection ‹Demostración estructurada› | |
+ | |||
lemma ejemplo_23_2: | lemma ejemplo_23_2: | ||
assumes "p ⟶ q" | assumes "p ⟶ q" | ||
Línea 1112: | Línea 1400: | ||
proof - | proof - | ||
have "¬p ∨ p" .. | have "¬p ∨ p" .. | ||
− | + | then show "¬p ∨ q" | |
proof | proof | ||
{ assume "¬p" | { assume "¬p" | ||
− | + | then show "¬p ∨ q" .. } | |
next | next | ||
{ assume "p" | { assume "p" | ||
with assms have "q" .. | with assms have "q" .. | ||
− | + | then show "¬p ∨ q" .. } | |
qed | qed | ||
qed | qed | ||
− | + | subsubsection ‹Demostración automática› | |
+ | |||
lemma ejemplo_23_3: | lemma ejemplo_23_3: | ||
assumes "p ⟶ q" | assumes "p ⟶ q" | ||
shows "¬p ∨ q" | shows "¬p ∨ q" | ||
− | using assms | + | using assms |
− | by | + | 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: | lemma ejemplo_24_1: | ||
assumes "¬p" | assumes "¬p" | ||
"p ∨ q" | "p ∨ q" | ||
shows "q" | shows "q" | ||
− | using | + | using ‹p ∨ q› |
proof (rule disjE) | proof (rule disjE) | ||
assume "p" | assume "p" | ||
Línea 1148: | Línea 1447: | ||
next | next | ||
assume "q" | assume "q" | ||
− | + | then show "q" by assumption | |
qed | qed | ||
− | + | subsubsection ‹Demostración estructurada› | |
+ | |||
lemma ejemplo_24_2: | lemma ejemplo_24_2: | ||
assumes "¬p" | assumes "¬p" | ||
"p ∨ q" | "p ∨ q" | ||
shows "q" | shows "q" | ||
− | using | + | using ‹p ∨ q› |
proof | proof | ||
assume "p" | assume "p" | ||
Línea 1162: | Línea 1462: | ||
next | next | ||
assume "q" | assume "q" | ||
− | + | then show "q" . | |
qed | qed | ||
− | + | subsubsection ‹Demostración automática› | |
+ | |||
lemma ejemplo_24_3: | lemma ejemplo_24_3: | ||
assumes "¬p" | assumes "¬p" | ||
"p ∨ q" | "p ∨ q" | ||
shows "q" | shows "q" | ||
− | using assms | + | using assms |
− | by | + | by simp |
end | end | ||
</source> | </source> |
Revisión actual del 21:39 19 feb 2020
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