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
subsection "Cálculo de secuentes"
lemma "A ⟹ P ∧ Q"
apply (rule conjI)
oops
lemma "⟦A; P ∧ Q⟧ ⟹ R"
apply (erule conjE)
oops
lemma "A ⟹ P ∨ Q"
apply (rule disjI1)
oops
lemma "A ⟹ P ∨ Q"
apply (rule disjI2)
oops
lemma "⟦A; P ∨ Q⟧ ⟹ R"
apply (erule disjE)
oops
lemma "A ⟹ P ⟶ Q"
apply (rule impI)
oops
lemma "⟦A; P ⟶ Q⟧ ⟹ R"
apply (erule impE)
oops
lemma "⟦A; False⟧ ⟹ P"
apply (erule FalseE)
done
lemma "A ⟹ ¬P"
apply (rule notI)
oops
lemma "⟦A; P; ¬P⟧ ⟹ R"
apply (erule notE, assumption)
done
lemma "A ⟹ ¬P ∨ P"
apply (rule excluded_middle)
done
subsection "Ejemplos de pruebas"
lemma "((S ∨ R) ∧ ¬S) ⟶ R"
apply (rule impI) (* da (S ∨ R) ∧ ¬ S ⟹ R *)
apply (frule conjunct1) (* da ⟦(S ∨ R) ∧ ¬ S; S ∨ R⟧ ⟹ R *)
apply (erule disjE) (* da ⟦(S ∨ R) ∧ ¬ S; S⟧ ⟹ R
⟦(S ∨ R) ∧ ¬ S; R⟧ ⟹ R *)
apply (drule conjunct2) (* da ⟦S; ¬ S⟧ ⟹ R
⟦(S ∨ R) ∧ ¬ S; R⟧ ⟹ R *)
apply (erule notE) (* da S ⟹ S
⟦(S ∨ R) ∧ ¬ S; R⟧ ⟹ R *)
apply assumption+ (* da No subgoals! *)
done
lemma "(C ∨ P) ∧ (C ⟶ S) ∧ ¬P ⟶ S"
apply (rule impI) (* da (C ∨ P) ∧ (C ⟶ S) ∧ ¬ P ⟹ S *)
apply (erule conjE)+ (* da ⟦C ∨ P; C ⟶ S; ¬ P⟧ ⟹ S *)
apply (erule disjE) (* da ⟦C ⟶ S; ¬ P; C⟧ ⟹ S
⟦C ⟶ S; ¬ P; P⟧ ⟹ S *)
apply (erule impE) (* da ⟦¬ P; C⟧ ⟹ C
⟦¬ P; C; S⟧ ⟹ S
⟦C ⟶ S; ¬ P; P⟧ ⟹ S *)
apply assumption+ (* da ⟦C ⟶ S; ¬ P; P⟧ ⟹ S *)
apply (erule notE) (* da ⟦C ⟶ S; P⟧ ⟹ P *)
apply assumption (* da No subgoals! *)
done
subsection "La regla de corte"
lemma aux: "A ⟹ A ∨ B"
sorry
lemma "P ∧ Q ⟹ Q"
apply (cut_tac aux)
oops
lemma "¬(¬p ∧ ¬q) ⟹ p ∨ q"
apply (cut_tac P=p in excluded_middle)
apply (erule disjE)
apply (cut_tac P=q in excluded_middle)
apply (erule disjE)
apply (erule notE)
apply (rule conjI)
apply assumption+
apply (erule disjI2)
apply (erule disjI1)
done
text {* Ejemplo de case_tac *}
lemma "P ∧ Q ⟹ Q"
apply (case_tac "P") (* da ⟦P ∧ Q; P⟧ ⟹ Q
⟦P ∧ Q; ¬ P⟧ ⟹ Q *)
oops
text {* La demostración anterior usando case_tac *}
lemma "¬(¬p ∧ ¬q) ⟹ p ∨ q"
apply (case_tac p)
apply (erule disjI1)
apply (case_tac q)
apply (erule disjI2)
apply (erule notE)
apply (rule conjI)
apply assumption+
done
subsection "Ejemplo de demostración automática"
lemma "⟦A ∧ B; C ∧ (B ∧ D)⟧ ⟹ B ∧ D"
apply simp
done
section "Ejemplos del tema 2"
subsection {* Reglas de la conjunción *}
text {*
Ejemplo 1 (p. 4). Demostrar que
p ∧ q, r ⊢ q ∧ r.
*}
lemma ejemplo_1: "⟦p ∧ q; r⟧ ⟹ q ∧ r"
apply (rule conjI)
apply (erule conjunct2)
apply assumption
done
subsection {* Reglas de la doble negación *}
text {*
La regla de eliminación de la doble negación es
· notnotD: ¬¬ P ⟹ P
Para ajustarnos al tema de LI vamos a introducir la siguiente regla de
introducción de la doble negación
· notnotI: P ⟹ ¬¬ P
aunque, de momento, no detallamos su demostración.
*}
lemma notnotI [intro!]: "P ⟹ ¬¬ P"
by auto
text {*
Ejemplo 2. (p. 5)
p, ¬¬(q ∧ r) ⊢ ¬¬p ∧ r
*}
lemma ejemplo_2_A: "⟦p; ¬¬(q ∧ r) ⟧ ⟹ ¬¬p ∧ r"
apply (rule conjI)
apply (rule notnotI)
apply assumption
apply (drule notnotD)
apply (erule conjunct2)
done
subsection {* Regla de eliminación del condicional *}
text {*
La regla de eliminación del condicional es la regla del modus ponens
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
*}
text {*
Ejemplo 3. (p. 6) Demostrar que
¬p ∧ q, ¬p ∧ q ⟶ r ∨ ¬p ⊢ r ∨ ¬p
*}
lemma ejemplo_3: "⟦¬p ∧ q; ¬p ∧ q ⟶ r ∨ ¬p⟧ ⟹ r ∨ ¬p"
apply (erule mp)
apply assumption
done
text {*
Ejemplo 4 (p. 6) Demostrar que
p, p ⟶ q, p ⟶ (q ⟶ r) ⊢ r
*}
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
subsection {* Regla derivada del modus tollens *}
text {*
Para ajustarnos al tema de LI vamos a introducir la regla del modus
tollens
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
aunque, de momento, sin detallar su demostración.
*}
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto
text {*
Ejemplo 5 (p. 7). Demostrar
p ⟶ (q ⟶ r), p, ¬r ⊢ ¬q
*}
lemma ejemplo_5_: "⟦p ⟶ (q ⟶ r); p; ¬r ⟧ ⟹ ¬q"
apply (drule mp)
apply assumption
apply (erule mt)
apply assumption
done
text {*
Ejemplo 6. (p. 7) Demostrar
¬p ⟶ q, ¬q ⊢ p
*}
lemma ejemplo_6: "⟦¬p ⟶ q; ¬q⟧ ⟹ p"
apply (drule mt)
apply assumption
apply (erule notnotD)
done
text {*
Ejemplo 7. (p. 7) Demostrar
p ⟶ ¬q, q ⊢ ¬p
*}
lemma ejemplo_7: "⟦p ⟶ ¬q; q⟧ ⟹ ¬p"
apply (erule mt)
apply (erule notnotI)
done
subsection {* Regla de introducción del condicional *}
text {*
La regla de introducción del condicional es
· impI: (P ⟹ Q) ⟹ P ⟶ Q
*}
text {*
Ejemplo 8. (p. 8) Demostrar
p ⟶ q ⊢ ¬q ⟶ ¬p
*}
lemma ejemplo_8: "p ⟶ q ⟹ ¬q ⟶ ¬p"
apply (rule impI)
apply (erule mt)
apply assumption
done
text {*
Ejemplo 9. (p. 9) Demostrar
¬q ⟶ ¬p ⊢ p ⟶ ¬¬q
*}
lemma ejemplo_9: "¬q ⟶ ¬p ⟹ p ⟶ ¬¬q"
apply (rule impI)
apply (erule mt)
apply (rule notnotI)
apply assumption
done
text {*
Ejemplo 10 (p. 9). Demostrar
⊢ p ⟶ p
*}
lemma ejemplo_10: "p ⟶ p"
apply (rule impI)
apply assumption
done
text {*
Ejemplo 11 (p. 10) Demostrar
⊢ (q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))
*}
lemma ejemplo_11_A: "(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
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
*}
lemma ejemplo_12: "p ∨ q ⟹ q ∨ p"
apply (erule disjE)
apply (rule disjI2)
prefer 2
apply (rule disjI1)
apply assumption+
done
text {*
Ejemplo 13. (p. 12) Demostrar
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
*}
lemma ejemplo_13_A: "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
subsection {* Regla de copia *}
text {*
Ejemplo 14 (p. 13). Demostrar
⊢ p ⟶ (q ⟶ p)
*}
lemma ejemplo_14_A: "p ⟶ (q ⟶ p)"
apply (rule impI)+
apply assumption
done
subsection {* Reglas de la negación *}
text {*
La regla de eliminación de lo falso es
· FalseE: False ⟹ P
La regla de eliminación de la negación es
· notE: ⟦¬P; P⟧ ⟹ R
La regla de introducción de la negación es
· notI: (P ⟹ False) ⟹ ¬P
*}
text {*
Ejemplo 15 (p. 15). Demostrar
¬p ∨ q ⊢ p ⟶ q
*}
lemma ejemplo_15: "¬p ∨ q ⟹ p ⟶ q"
apply (rule impI)
apply (erule disjE)
apply (erule notE)
apply assumption+
done
text {*
Ejemplo 16 (p. 16). Demostrar
p ⟶ q, p ⟶ ¬q ⊢ ¬p
*}
lemma ejemplo_16_A: "⟦p ⟶ q; p ⟶ ¬q⟧ ⟹ ¬p"
apply (rule notI)
apply (drule mp)+
apply assumption+
apply (drule mp)
prefer 2
apply (erule notE)
apply assumption+
done
subsection {* Reglas del bicondicional *}
text {*
La regla de introducción del bicondicional es
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P ⟷ Q
Las reglas de eliminación del bicondicional son
· iffD1: ⟦Q ⟷ P; Q⟧ ⟹ P
· iffD2: ⟦P ⟷ Q; Q⟧ ⟹ P
*}
text {*
Ejemplo 17 (p. 17) Demostrar
*}
lemma ejemplo_17: "(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
text {*
Ejemplo 18 (p. 18). Demostrar
p ⟷ q, p ∨ q ⊢ p ∧ q
*}
lemma ejemplo_18_A: "⟦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
subsection {* Reglas derivadas *}
subsubsection {* Regla del modus tollens *}
text {*
Ejemplo 19 (p. 20) Demostrar la regla del modus tollens a partir de
las reglas básicas.
*}
lemma ejemplo_20: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
apply (rule notI)
apply (drule mp)
apply assumption
apply (erule notE)
apply assumption
done
subsubsection {* Regla de la introducción de la doble negación *}
text {*
Ejemplo 21 (p. 21) Demostrar la regla de introducción de la doble
negación a partir de las reglas básicas.
*}
lemma ejemplo_21_A: "F ⟹ ¬¬F"
apply (rule notI)
apply (erule notE)
apply assumption
done
subsubsection {* Regla de reducción al absurdo *}
text {*
La regla de reducción al absurdo en Isabelle se corresponde con la
regla clásica de contradicción
· ccontr: (¬P ⟹ False) ⟹ P
*}
subsubsection {* Ley del tercio excluso *}
text {*
La ley del tercio excluso es
· excluded_middle: ¬P ∨ P
*}
text {*
Ejemplo 22 (p. 23). Demostrar la ley del tercio excluso a partir de
las reglas básicas.
*}
lemma ejemplo_22: "F ∨ ¬F"
oops
text {*
Ejemplo 23 (p. 24). Demostrar
p ⟶ q ⊢ ¬p ∨ q
*}
lemma ejemplo_23: "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
subsection {* Demostraciones por contradicción *}
text {*
Ejemplo 24. Demostrar que
¬p, p ∨ q ⊢ q
*}
lemma ejemplo_24: "⟦¬p ; p ∨ q⟧ ⟹ q"
apply (erule disjE)
apply (erule notE)
apply assumption+
done
end
