Diferencia entre revisiones de «Deducción natural en lógica de primer orden con Isabelle/HOL basada en tácticas»
De Lógica matemática y fundamentos (2018-19)
Línea 241: | Línea 241: | ||
end | end | ||
</source> | </source> | ||
+ | |||
+ | === Bibliografía === | ||
+ | |||
+ | * [http://www.phil.cmu.edu/~avigad/formal/FormalCheatSheet.pdf Isabelle / Proof General Cheat Sheet]. | ||
+ | * [https://isabelle.in.tum.de/dist/Isabelle2018/doc/tutorial.pdf Isabelle/HOL: A Proof Assistant for Higher-Order Logic]. |
Revisión del 08:17 26 mar 2019
theory T4b
imports Main
begin
section "Introducción"
subsection "Reglas de primer orden en Isabelle/HOL"
thm spec [no_vars]
(* da ∀x. P x ⟹ P x *)
thm allE [no_vars]
(* da ⟦∀x. P x; P x ⟹ R⟧ ⟹ R *)
thm allI [no_vars]
(* da (⋀x. P x) ⟹ ∀x. P x *)
thm exI
(* da ?P ?x ⟹ ∃x. ?P x *)
thm exE [no_vars]
(* da ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q *)
subsection "Ejemplos de demostraciones"
text {* Ejemplo con spec y exI*}
lemma "∀x. P x ⟹ ∃y. P y"
apply (drule_tac x=a in spec) (* da P a ⟹ ∃y. P y *)
apply (rule_tac x=a in exI) (* da P a ⟹ P a *)
apply assumption (* da No subgoals!*)
done
text {* Ejemplo con spec y exI*}
lemma "∀x. P x ⟹ ∃x. P x"
apply (rule exI) (* da ∀x. P x ⟹ P ?x *)
apply (erule spec) (* da No subgoals! *)
done
text {* Ejemplo con allE y exI*}
lemma "∀x. P x ⟹ ∃x. P x"
apply (erule allE) (* da P ?x ⟹ ∃x. P x*)
apply (erule exI) (* da No subgoals! *)
done
text {* Ejemplo con erule_tac *}
lemma "⟦∀x. P x ⟶ Q x; ∀y. P y⟧ ⟹ ∀z. Q z"
apply (rule allI) (* da ⋀z. ⟦∀x. P x ⟶ Q x; ∀y. P y⟧
⟹ Q z *)
apply (erule_tac x=z in allE) (* da ⋀z. ⟦∀y. P y; P z ⟶ Q z⟧
⟹ Q z *)
apply (erule_tac x=z in allE) (* da ⋀z. ⟦P z ⟶ Q z; P z⟧ ⟹ Q z *)
apply (erule impE) (* da ⋀z. P z ⟹ P z
⋀z. ⟦P z; Q z⟧ ⟹ Q z *)
apply assumption+ (* da No subgoals! *)
done
text {* Ejemplo sin erule_tac *}
lemma "⟦∀x. P x ⟶ Q x; ∀y. P y⟧ ⟹ ∀z. Q z"
apply (rule allI) (* da ⋀z. ⟦∀x. P x ⟶ Q x; ∀y. P y⟧ ⟹ Q z *)
apply (erule allE) (* da ⋀z. ⟦∀y. P y; P (?x2 z) ⟶ Q (?x2 z)⟧
⟹ Q z *)
apply (erule allE) (* da ⋀z. ⟦P (?x2 z) ⟶ Q (?x2 z); P (?y4 z)⟧
⟹ Q z *)
apply (erule mp) (* da ⋀z. P (?y4 z) ⟹ P z *)
apply assumption (* da No subgoals *)
done
text {* Ejemplo con exE *}
lemma "(∃z. P z) ∧ Q ⟶ (∃y. P y ∧ Q)"
apply (rule impI) (* da (∃z. P z) ∧ Q ⟹ ∃y. P y ∧ Q *)
apply (erule conjE) (* da ⟦∃z. P z; Q⟧ ⟹ ∃y. P y ∧ Q *)
apply (erule exE) (* da ⋀z. ⟦Q; P z⟧ ⟹ ∃y. P y ∧ Q *)
apply (rule_tac x="z" in exI) (* da ⋀z. ⟦Q; P z⟧ ⟹ P z ∧ Q *)
apply (rule conjI) (* da ⋀z. ⟦Q; P z⟧ ⟹ P z
⋀z. ⟦Q; P z⟧ ⟹ Q *)
apply assumption+ (* da No subgoals! *)
done
subsection "Cálculo de secuentes de primer orden"
lemma "A ⟹ ∀x. P x"
apply (rule allI) (* da ⋀x. A ⟹ P x *)
oops
lemma "⟦A; ∀x. P x⟧ ⟹ Q"
apply (erule allE) (* da ⟦A; P ?x⟧ ⟹ Q *)
oops
lemma "⟦A; ∀x. P x⟧ ⟹ Q"
apply (erule_tac x=t in allE) (* da ⟦A; P t⟧ ⟹ Q *)
oops
lemma "⟦A; ∀x. P x⟧ ⟹ Q"
apply (frule spec) (* da ⟦A; ∀x. P x; P ?x⟧ ⟹ Q *)
oops
lemma "⟦A; ∀x. P x⟧ ⟹ Q"
apply (frule_tac x=t in spec) (* da ⟦A; ∀x. P x; P t⟧ ⟹ Q *)
oops
lemma "A ⟹ ∃x. P x"
apply (rule exI) (* da A ⟹ P ?x *)
oops
lemma "A ⟹ ∃x. P x"
apply (rule_tac x=t in exI) (* da A ⟹ P t *)
oops
lemma "⟦A; ∃x. P x⟧ ⟹ Q"
apply (erule exE) (* da ⋀x. ⟦A; P x⟧ ⟹ Q *)
oops
section "Ejemplos del tema 6"
subsection {* Reglas del cuantificador universal *}
lemma ej1: "⟦P(c); ∀x. (P(x) ⟶ ¬Q(x))⟧ ⟹ ¬Q(c)"
apply (erule allE)
apply (erule mp)
apply assumption
done
lemma ej2: "⟦∀x. (P x ⟶ ¬(Q x)); ∀y. P y⟧ ⟹ ∀z. ¬(Q z)"
apply (rule allI)
apply (erule allE)+
apply (erule mp)
apply assumption
done
subsection "Reglas del cuantificador existencial"
lemma ej3: "∀x. P x ⟹ ∃y. P y"
apply (erule allE)
apply (erule exI)
done
lemma ej4: "⟦∀x. P x ⟶ Q x; ∃y. P y⟧ ⟹ ∃z. Q z"
apply (erule exE)
apply (erule allE)
apply (rule exI)
apply (erule mp)
apply assumption
done
subsection "Demostraciones de equivalencias"
lemma ej5a: "¬(∀x. P x) ⟹ ∃y. ¬P y"
apply (rule ccontr)
apply (erule notE)
apply (rule allI)
apply (rule ccontr)
apply (erule notE)
apply (erule exI)
done
lemma ej5b: "∃x. ¬P x ⟹ ¬(∀y. P y)"
apply (rule notI)
apply (erule exE)
apply (erule allE)
apply (erule notE)
apply assumption
done
lemma ej5: "¬(∀x. P x) ⟷ (∃x. ¬P x)"
apply (rule iffI)
apply (erule ej5a)
apply (erule ej5b)
done
lemma ej6a: "∀x. P(x) ∧ Q(x) ⟹ (∀x. P x) ∧ (∀x. Q x)"
apply (rule conjI)
apply (rule allI)
apply (erule allE)
apply (erule conjE)
apply assumption
apply (rule allI)
apply (erule allE)
apply (erule conjE)
apply assumption
done
lemma ej6b: "(∀x. P x) ∧ (∀x. Q x) ⟹ ∀x. P x ∧ Q x"
apply (rule allI)
apply (rule conjI)
apply (drule conjunct1)
apply (erule spec)
apply (drule conjunct2)
apply (erule spec)
done
lemma ej6: "(∀x. P x ∧ Q x) ⟷ (∀x. P x) ∧ (∀x. Q x)"
apply (rule iffI)
apply (erule ej6a)
apply (erule ej6b)
done
lemma ej7a: "(∃x. P x) ∨ (∃x. Q x) ⟹ ∃x. P x ∨ Q x"
apply (erule disjE)
apply (erule exE)
apply (rule exI)
apply (erule disjI1)
apply (erule exE)
apply (rule exI)
apply (erule disjI2)
done
lemma ej7b: "∃x. P x ∨ Q x ⟹ (∃x. P x) ∨ (∃x. Q x)"
apply (erule exE)
apply (erule disjE)
apply (rule disjI1)
apply (erule exI)
apply (rule disjI2)
apply (erule exI)
done
lemma ej7: "(∃x. P x) ∨ (∃x. Q x) ⟷ (∃x. P x ∨ Q x)"
apply (rule iffI)
apply (erule ej7a)
apply (erule ej7b)
done
lemma ej8a: "∃x y. P x y ⟹ ∃y x. P x y"
apply (erule exE)+
apply (rule exI)+
apply assumption
done
lemma ej8b: "∃y x. P x y ⟹ ∃x y. P x y"
apply (erule exE)+
apply (rule exI)+
apply assumption
done
lemma ej8: "(∃x y. P x y) ⟷ (∃y x. P x y)"
apply (rule iffI)
apply (erule ej8a)
apply (erule ej8b)
done
end