LMF2018: Deducción natural proposicional con las tácticas Isabelle/HOL
En la clase de hoy del curso de Lógica matemática y fundamentos se ha estudiado cómo construir las pruebas por deducción natural usando las tácticas de Isabelle/HOL.
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 133 134 135 136 137 138 139 140 141 142 143 144 |
theory T2b imports Main begin section "Introducción" subsection "Enunciado de teoremas" theorem primerEjemplo: "(A ⟶ B) ∨ (B ⟶ A)" oops subsection "Demostración por asunción" lemma "⟦A; B; C⟧ ⟹ B" apply assumption done subsection "Ejemplo de aplicación de rule" text {* 1º ejemplo de aplicación de rule *} lemma "A ∧ B ⟹ B ∧ A" apply (rule conjI) oops text {* 2º ejemplo de aplicación de rule *} lemma "A ∧ B ⟹ B ∨ A" apply (rule disjI1) oops lemma "⟦(A ∧ B) ∨ C; D⟧ ⟹ B ∨ C" apply (rule disjE) apply assumption oops subsection "Ejemplo de demostración con rule y assumption" theorem K: "A ⟶ (B ⟶ A)" apply (rule impI) (* da A ⟹ B ⟶ A *) apply (rule impI) (* da ⟦A; B⟧ ⟹ A *) apply assumption (* da No subgoals! *) done subsection "Ejemplo de derivación con hipótesis" text {* Derivación de A, B ⊢ A ∧ (B ∧ A) *} theorem "⟦A; B⟧ ⟹ A ∧ (B ∧ A)" apply (rule conjI) (* da ⟦A; B⟧ ⟹ A ⟦A; B⟧ ⟹ B ∧ A *) apply assumption (* da ⟦A; B⟧ ⟹ B ∧ A *) apply (rule conjI) (* da ⟦A; B⟧ ⟹ B ⟦A; B⟧ ⟹ A *) apply assumption (* da ⟦A; B⟧ ⟹ A *) apply assumption (* da No subgoals *) done text {* La prueba anterior se puede simplificar usando assumption+ *} theorem "⟦A; B⟧ ⟹ A ∧ (B ∧ A)" apply (rule conjI) (* da ⟦A; B⟧ ⟹ A ⟦A; B⟧ ⟹ B ∧ A *) apply assumption (* da ⟦A; B⟧ ⟹ B ∧ A *) apply (rule conjI) (* da ⟦A; B⟧ ⟹ B ⟦A; B⟧ ⟹ A *) apply assumption+ (* da No subgoals *) done subsection "Ejemplo de aplicación de erule" lemma "⟦(A ∧ B) ∨ C; D⟧ ⟹ B ∨ C" apply (erule disjE) oops text {* Demostración con erule *} lemma "A ∨ B ⟹ B ∨ A" apply (erule disjE) (* da A ⟹ B ∨ A B ⟹ B ∨ A*) apply (rule disjI2) (* da A ⟹ A B ⟹ B ∨ A *) apply assumption (* da B ⟹ B ∨ A *) apply (rule disjI1) (* da B ⟹ B *) apply assumption (* da No subgoals *) done text {* Variación de la demostración anterior cambiando erule por rule *} lemma "A ∨ B ⟹ B ∨ A" apply (rule disjE) (* da A ∨ B ⟹ ?P ∨ ?Q ⟦A ∨ B; ?P⟧ ⟹ B ∨ A ⟦A ∨ B; ?Q⟧ ⟹ B ∨ A *) apply assumption (* da ⟦A ∨ B; A⟧ ⟹ B ∨ A ⟦A ∨ B; B⟧ ⟹ B ∨ A *) apply (rule disjI2) (* da ⟦A ∨ B; A⟧ ⟹ A ⟦A ∨ B; B⟧ ⟹ B ∨ A*) apply assumption (* da ⟦A ∨ B; B⟧ ⟹ B ∨ A *) apply (rule disjI1) (* da ⟦A ∨ B; B⟧ ⟹ B *) apply assumption (* da No subgoals! *) done subsection "Ejemplo de aplicación de drule" lemma "⟦A ⟶ B; A ∧ C⟧ ⟹ B ∧ C" apply (drule mp) oops text {* Demostración con drule *} lemma "A ∧ B ⟹ A" apply (drule conjunct1) (* da A ⟹ A *) apply assumption (* da No subgoals! *) done subsection "Ejemplo de aplicación de frule" lemma "⟦A ⟶ B; A ∧ C⟧ ⟹ B ∧ C" apply (frule mp) oops text {* Demostración con frule *} lemma "A ∧ B ⟹ A" apply (frule conjunct1) (* da ⟦A ∧ B; A⟧ ⟹ A *) apply assumption (* da No subgoals! *) done subsection "Ejemplo de aplicación de erule_tac" lemma "⟦A ∧ B; C ∧ (B ∧ D)⟧ ⟹ B ∧ D" apply (erule_tac Q="B ∧ D" in conjE) apply assumption done lemma "⟦A ∧ B; C ∧ (B ∧ D)⟧ ⟹ B ∧ D" apply (erule conjE) oops text {* Demostración con erule_tac *} lemma "⟦A ∧ B; C ∧ D⟧ ⟹ D" apply (erule_tac P=C in conjE) (* da ⟦A ∧ B; C; D⟧ ⟹ D *) apply assumption (* da No subgoals! *) done text {* Demostración sin erule_tac *} lemma "⟦A ∧ B; C ∧ D⟧ ⟹ D" apply (erule conjE) (* da ⟦C ∧ D; A; B⟧ ⟹ D *) apply (erule conjE) (* da ⟦A; B; C; D⟧ ⟹ D *) apply assumption (* da No subgoals! *) done end |