LMF2016: Deducción natural proposicional en Isabelle/HOL (2)
En la clase de hoy del curso Lógica matemática y fundamentos se ha continuado el estudio de la formalización en Isabelle/HOL de las demostraciones por deducción natural estudiadas en el tema 2 iniciado en la clase anterior.
Para cada uno de los ejemplos se ha presentado distintas demostraciones: detallada (que sea parecida a la mostrada en las transparencias), estructurada y automática.
La teoría con los ejemplos presentados en la clase es la siguiente:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 |
subsection {* Reglas de la disyunción *} text {* Las reglas de la introducción de la disyunción son · disjI1: P ⟹ P ∨ Q · disjI2: Q ⟹ P ∨ Q La regla de elimación de la disyunción es · disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R *} text {* Ejemplo 12 (p. 11). Demostrar p ∨ q ⊢ q ∨ p *} -- "La demostración detallada es" lemma ejemplo_12_1: assumes "p ∨ q" shows "q ∨ p" proof - have "p ∨ q" using assms by this moreover { assume 2: "p" have "q ∨ p" using 2 by (rule disjI2) } moreover { assume 3: "q" have "q ∨ p" using 3 by (rule disjI1) } ultimately show "q ∨ p" by (rule disjE) qed text {* Nota sobre el lenguaje: En la demostración anterior se ha usado · "moreover" para separar los bloques y · "ultimately" para unir los resultados de los bloques. *} -- "La demostración detallada con reglas implícitas es" lemma ejemplo_12_2: assumes "p ∨ q" shows "q ∨ p" proof - note `p ∨ q` moreover { assume "p" hence "q ∨ p" .. } moreover { assume "q" hence "q ∨ p" .. } ultimately show "q ∨ p" .. qed text {* Nota sobre el lenguaje: En la demostración anterior se ha usado · "note" para copiar un hecho. *} -- "La demostración hacia atrás es" lemma ejemplo_12_3: assumes 1: "p ∨ q" shows "q ∨ p" using 1 proof (rule disjE) { assume 2: "p" show "q ∨ p" using 2 by (rule disjI2) } next { assume 3: "q" show "q ∨ p" using 3 by (rule disjI1) } qed -- "La demostración hacia atrás con reglas implícitas es" lemma ejemplo_12_4: assumes "p ∨ q" shows "q ∨ p" using assms proof { assume "p" thus "q ∨ p" .. } next { assume "q" thus "q ∨ p" .. } qed -- "La demostración automática es" lemma ejemplo_12_5: assumes "p ∨ q" shows "q ∨ p" using assms by auto text {* Ejemplo 13. (p. 12) Demostrar q ⟶ r ⊢ p ∨ q ⟶ p ∨ r *} -- "La demostración detallada es" lemma ejemplo_13_1: assumes 1: "q ⟶ r" shows "p ∨ q ⟶ p ∨ r" proof (rule impI) assume 2: "p ∨ q" thus "p ∨ r" proof (rule disjE) { assume 3: "p" show "p ∨ r" using 3 by (rule disjI1) } next { assume 4: "q" have 5: "r" using 1 4 by (rule mp) show "p ∨ r" using 5 by (rule disjI2) } qed qed -- "La demostración estructurada es" lemma ejemplo_13_2: assumes "q ⟶ r" shows "p ∨ q ⟶ p ∨ r" proof assume "p ∨ q" thus "p ∨ r" proof { assume "p" thus "p ∨ r" .. } next { assume "q" have "r" using assms `q` .. thus "p ∨ r" .. } qed qed -- "La demostración automática es" lemma ejemplo_13_3: assumes "q ⟶ r" shows "p ∨ q ⟶ p ∨ r" using assms by auto |