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 31: | Línea 31: | ||
apply assumption (* da No subgoals!*) | apply assumption (* da No subgoals!*) | ||
done | done | ||
− | + | ||
+ | text {* Explicaciones: | ||
+ | apply (drule_tac x=a in spec) | ||
+ | + Objetivo: "∀x. P x ⟹ ∃y. P y" | ||
+ | + spec: "∀x. ?P x ⟹ ?P ?x" | ||
+ | + spec "x=a": "∀x. ?P x ⟹ ?P a" | ||
+ | + Unificador de "∀x. P x" con | ||
+ | "∀x. ?P x" | ||
+ | es ?P/P | ||
+ | + Nuevo objetivo: "P a ⟹ ∃y. P y" | ||
+ | |||
+ | apply (rule_tac x=a in exI) | ||
+ | + Objetivo: "P a ⟹ ∃y. P y" | ||
+ | + exI: "?P ?x ⟹ ∃x. ?P x" | ||
+ | + exI "x=a": "?P a ⟹ ∃x. ?P x" | ||
+ | + Unificador de "∃y. P y" con | ||
+ | "∃x. ?P x" | ||
+ | es ?P/P | ||
+ | + Nuevo objetivo: "P a ⟹ P a" | ||
+ | *} | ||
+ | |||
text {* Ejemplo con spec y exI*} | text {* Ejemplo con spec y exI*} | ||
lemma "∀x. P x ⟹ ∃x. P x" | lemma "∀x. P x ⟹ ∃x. P x" | ||
Línea 37: | Línea 57: | ||
apply (erule spec) (* da No subgoals! *) | apply (erule spec) (* da No subgoals! *) | ||
done | done | ||
+ | |||
+ | text {* Explicaciones | ||
+ | apply (rule exI) | ||
+ | + Objetivo: "∀x. P x ⟹ ∃x. P x" | ||
+ | + exI: "?P ?x ⟹ ∃x. ?P x" | ||
+ | + Unificador de "∃x. P x" y | ||
+ | "∃x. ?P x" | ||
+ | es ?P/P | ||
+ | + Nuevo objetivo: "∀x. P x ⟹ P ?x" | ||
+ | |||
+ | apply (erule spec) | ||
+ | + Objetivo: "∀x. P x ⟹ P ?x" | ||
+ | + spec: "∀x. ?P x ⟹ ?P ?x" | ||
+ | + Unificador de ("?P ?x", "∀x. P x") y | ||
+ | ("?P ?x", "∀x. ?P x" | ||
+ | es ?P/P | ||
+ | + Nuevo objetivo: Vacío, porque erule aplica assumption a | ||
+ | "P ?x ⟹ P ?x" | ||
+ | *} | ||
text {* Ejemplo con allE y exI*} | text {* Ejemplo con allE y exI*} | ||
Línea 43: | Línea 82: | ||
apply (erule exI) (* da No subgoals! *) | apply (erule exI) (* da No subgoals! *) | ||
done | done | ||
− | + | ||
+ | text {* Explicaciones | ||
+ | apply (erule allE) | ||
+ | + Objetivo: "∀x. P x ⟹ ∃x. P x" | ||
+ | + allE: "⟦∀x. ?P x; ?P ?x ⟹ ?R⟧ ⟹ ?R" | ||
+ | + Unificador de ("?R", "∀x. ?P x") y | ||
+ | ("∃x. P x", "∀x. P x") | ||
+ | es ?R / ∃x. P x | ||
+ | ?P / P | ||
+ | + Nuevo objetivo: "P ?x ⟹ ∃x. P x" | ||
+ | |||
+ | apply (erule exI) | ||
+ | + Objetivo: "P ?x ⟹ ∃x. P x" | ||
+ | + exI: "?P ?x ⟹ ∃x. ?P x" | ||
+ | + Unificador de ("∃x. P x", "P ?x") y | ||
+ | ("∃x. ?P x", "?P ?x") | ||
+ | es ?P / P | ||
+ | ?x / x | ||
+ | + Nuevo objetivo: Vacío | ||
+ | *} | ||
+ | |||
text {* Ejemplo con erule_tac *} | text {* Ejemplo con erule_tac *} | ||
lemma "⟦∀x. P x ⟶ Q x; ∀y. P y⟧ ⟹ ∀z. Q z" | lemma "⟦∀x. P x ⟶ Q x; ∀y. P y⟧ ⟹ ∀z. Q z" | ||
Línea 55: | Línea 114: | ||
apply assumption+ (* da No subgoals! *) | apply assumption+ (* da No subgoals! *) | ||
done | done | ||
+ | |||
+ | thm impE | ||
+ | |||
+ | text {* Explicaciones | ||
+ | apply (rule allI) | ||
+ | + Objetivo: "⟦∀x. P x ⟶ Q x; ∀y. P y⟧ ⟹ ∀z. Q z" | ||
+ | + allI: "(⋀x. ?P x) ⟹ ∀x. ?P x" | ||
+ | + Unificador de "∀z. Q z" y | ||
+ | "∀x. ?P x" | ||
+ | es ?P / Q | ||
+ | + Ligadura: ⋀x / ⋀z | ||
+ | + Nuevo objetivo: "⋀z. ⟦∀x. P x ⟶ Q x; ∀y. P y⟧ ⟹ Q z" | ||
+ | |||
+ | apply (erule_tac x=z in allE) | ||
+ | + Objetivo: "⋀z. ⟦∀x. P x ⟶ Q x; ∀y. P y⟧ ⟹ Q z" | ||
+ | + allE: "⟦∀x. ?P x; ?P ?x ⟹ ?R⟧ ⟹ ?R" | ||
+ | + allE "x=z" "⟦∀x. ?P x; ?P z ⟹ ?R⟧ ⟹ ?R" | ||
+ | + Unificador de ("Q z", "∀x. P x ⟶ Q x") y | ||
+ | ("?R", "∀x. ?P x") | ||
+ | es ?R / Q z | ||
+ | ?P x / P x ⟶ Q x | ||
+ | + Nuevo objetivo: "⋀z. ⟦∀y. P y; P z ⟶ Q z⟧ ⟹ Q z" | ||
+ | + Nota: De "?P z ⟹ ?R" se obtiene la 2ª hipótesis y la conclusión. | ||
+ | |||
+ | apply (erule_tac x=z in allE) | ||
+ | + Objetivo: "⋀z. ⟦∀y. P y; P z ⟶ Q z⟧ ⟹ Q z" | ||
+ | + allE: "⟦∀x. ?P x; ?P ?x ⟹ ?R⟧ ⟹ ?R" | ||
+ | + allE "x=z" "⟦∀x. ?P x; ?P z ⟹ ?R⟧ ⟹ ?R" | ||
+ | + Unificador de ("Q z", "∀y. P y") y | ||
+ | ("?R", "∀x. ?P x") | ||
+ | es ?R / Q z | ||
+ | ?P / P | ||
+ | + Nuevo objetivo: "⋀z. ⟦P z ⟶ Q z; P z⟧ ⟹ Q z" | ||
+ | + Nota: De "?P z ⟹ ?R" se obtiene la 2ª hipótesis y la conclusión. | ||
+ | |||
+ | apply (erule impE) | ||
+ | + Objetivo: "⋀z. ⟦P z ⟶ Q z; P z⟧ ⟹ Q z" | ||
+ | + impE "⟦?P ⟶ ?Q; ?P; ?Q ⟹ ?R⟧ ⟹ ?R" | ||
+ | + Unificador de ("Q z", "P z ⟶ Q z") y | ||
+ | ("?R", "?P ⟶ ?Q") | ||
+ | es ?R / Q z | ||
+ | ?P / P z | ||
+ | ?Q /Q z | ||
+ | + Nuevos objetivos: "⋀z. P z ⟹ P z" | ||
+ | "⋀z. ⟦P z; Q z⟧ ⟹ Q z" | ||
+ | *} | ||
text {* Ejemplo sin erule_tac *} | text {* Ejemplo sin erule_tac *} | ||
Línea 66: | Línea 171: | ||
apply assumption (* da No subgoals *) | apply assumption (* da No subgoals *) | ||
done | done | ||
− | + | ||
+ | text {* | ||
+ | apply (rule allI) | ||
+ | + Objetivo: "⟦∀x. P x ⟶ Q x; ∀y. P y⟧ ⟹ ∀z. Q z" | ||
+ | + allI: "(⋀x. ?P x) ⟹ ∀x. ?P x" | ||
+ | + Unificador de "∀z. Q z" y | ||
+ | "∀x. ?P x" | ||
+ | es ?P / Q | ||
+ | + Ligadura: ⋀x / ⋀z | ||
+ | + Nuevo objetivo: "⋀z. ⟦∀x. P x ⟶ Q x; ∀y. P y⟧ ⟹ Q z" | ||
+ | |||
+ | apply (erule allE) | ||
+ | + Objetivo: "⋀z. ⟦∀x. P x ⟶ Q x; ∀y. P y⟧ ⟹ Q z" | ||
+ | + allE: "⟦∀x. ?P x; ?P ?x ⟹ ?R⟧ ⟹ ?R" | ||
+ | + Unificador de ("Q z", "∀x. P x ⟶ Q x") y | ||
+ | ("?R", "∀x. ?P x") | ||
+ | es ?R / Q z | ||
+ | ?P x / P x ⟶ Q x | ||
+ | + Nuevo objetivo: "⋀z. ⟦∀y. P y; P (?x2 z) ⟶ Q (?x2 z)⟧ ⟹ Q z" | ||
+ | |||
+ | apply (erule allE) | ||
+ | + Objetivo: "⋀z. ⟦∀y. P y; P (?x2 z) ⟶ Q (?x2 z)⟧ ⟹ Q z" | ||
+ | + allE: "⟦∀x. ?P x; ?P ?x ⟹ ?R⟧ ⟹ ?R" | ||
+ | + Unificador de ("Q z", "∀y. P y") y | ||
+ | ("?R", "∀x. ?P x") | ||
+ | es ?R / Q z | ||
+ | ?P / P | ||
+ | + Nuevo objetivo: "⋀z. ⟦P (?x2 z) ⟶ Q (?x2 z); P (?y4 z)⟧ ⟹ Q z" | ||
+ | |||
+ | apply (erule mp) | ||
+ | + Objetivo: "⋀z. ⟦P (?x2 z) ⟶ Q (?x2 z); P (?y4 z)⟧ ⟹ Q z" | ||
+ | + mp: "⟦?P ⟶ ?Q; ?P⟧ ⟹ ?Q" | ||
+ | + Unificador de ("Q z", "P (?x2 z) ⟶ Q (?x2 z)") y | ||
+ | ("?Q", "?P ⟶ ?Q") | ||
+ | es ?Q / Q z | ||
+ | ?x2 z/ z | ||
+ | ?P / P z | ||
+ | + Nuevo objetivo: "⋀z. P (?y4 z) ⟹ P z" | ||
+ | *} | ||
+ | |||
text {* Ejemplo con exE *} | text {* Ejemplo con exE *} | ||
lemma "(∃z. P z) ∧ Q ⟶ (∃y. P y ∧ Q)" | lemma "(∃z. P z) ∧ Q ⟶ (∃y. P y ∧ Q)" | ||
Línea 77: | Línea 221: | ||
apply assumption+ (* da No subgoals! *) | apply assumption+ (* da No subgoals! *) | ||
done | done | ||
+ | |||
+ | text {* Explicaciones: | ||
+ | apply (rule impI) | ||
+ | + Objetivo: "(∃z. P z) ∧ Q ⟶ (∃y. P y ∧ Q)" | ||
+ | + impI: "(?P ⟹ ?Q) ⟹ ?P ⟶ ?Q" | ||
+ | + Unificador de "(∃z. P z) ∧ Q ⟶ (∃y. P y ∧ Q)" y | ||
+ | "?P ⟶ ?Q" | ||
+ | es ?P / "(∃z. P z) ∧ Q" | ||
+ | ?Q / "∃y. P y ∧ Q" | ||
+ | + Nuevo objetivo: "(∃z. P z) ∧ Q ⟹ ∃y. P y ∧ Q" | ||
+ | |||
+ | apply (erule conjE) | ||
+ | + Objetivo: "(∃z. P z) ∧ Q ⟹ ∃y. P y ∧ Q" | ||
+ | + conjE: "⟦?P ∧ ?Q; ⟦?P; ?Q⟧ ⟹ ?R⟧ ⟹ ?R" | ||
+ | + Unificador de ("∃y. P y ∧ Q", "(∃z. P z) ∧ Q") y | ||
+ | ("?R", "?P ∧ ?Q") | ||
+ | es ?R / "∃y. P y ∧ Q" | ||
+ | ?P / "∃z. P z" | ||
+ | ?Q / Q | ||
+ | + Nuevo objetivo: "⟦∃z. P z; Q⟧ ⟹ ∃y. P y ∧ Q" | ||
+ | |||
+ | apply (erule exE) | ||
+ | + Objetivo: "⟦∃z. P z; Q⟧ ⟹ ∃y. P y ∧ Q" | ||
+ | + exE: "⟦∃x. ?P x; ⋀x. ?P x ⟹ ?Q⟧ ⟹ ?Q" | ||
+ | + Unificador de ("∃y. P y ∧ Q", "∃z. P z") y | ||
+ | ("?Q", "∃x. ?P x") | ||
+ | es ?Q / "∃y. P y ∧ Q" | ||
+ | ?P x / P z | ||
+ | + Nuevo objetivo: "⋀z. ⟦Q; P z⟧ ⟹ ∃y. P y ∧ Q" | ||
+ | |||
+ | apply (rule_tac x="z" in exI) | ||
+ | + Objetivo: "⋀z. ⟦Q; P z⟧ ⟹ ∃y. P y ∧ Q" | ||
+ | + exI: "?P ?x ⟹ ∃x. ?P x" | ||
+ | + exI "x=z" "?P z ⟹ ∃x. ?P x" | ||
+ | + Unificador de "∃y. P y ∧ Q" con | ||
+ | "∃x. ?P x" | ||
+ | es ?P x / P x ∧ Q | ||
+ | + Nuevo objetivo: "⋀z. ⟦Q; P z⟧ ⟹ P z ∧ Q" | ||
+ | |||
+ | apply (rule conjI) | ||
+ | + Objetivo: "⋀z. ⟦Q; P z⟧ ⟹ P z ∧ Q" | ||
+ | + conjI: "⟦?P; ?Q⟧ ⟹ ?P ∧ ?Q" | ||
+ | + Unificador de "P z ∧ Q" con | ||
+ | "?P ∧ ?Q" | ||
+ | es ?P / P z | ||
+ | ?Q / Q | ||
+ | + Nuevos objetivos: "⋀z. ⟦Q; P z⟧ ⟹ P z" | ||
+ | "⋀z. ⟦Q; P z⟧ ⟹ Q" | ||
+ | *} | ||
subsection "Cálculo de secuentes de primer orden" | subsection "Cálculo de secuentes de primer orden" | ||
Línea 83: | Línea 276: | ||
apply (rule allI) (* da ⋀x. A ⟹ P x *) | apply (rule allI) (* da ⋀x. A ⟹ P x *) | ||
oops | oops | ||
− | + | ||
+ | text {* Explicación | ||
+ | + Objetivo: "A ⟹ ∀x. P x" | ||
+ | + allI: "(⋀x. ?P x) ⟹ ∀x. ?P x" | ||
+ | + Unificador de "∀x. P x" y | ||
+ | "∀x. ?P x" | ||
+ | es ?P / P | ||
+ | + Nuevo objetivo: "⋀x. A ⟹ P x" | ||
+ | *} | ||
+ | |||
lemma "⟦A; ∀x. P x⟧ ⟹ Q" | lemma "⟦A; ∀x. P x⟧ ⟹ Q" | ||
apply (erule allE) (* da ⟦A; P ?x⟧ ⟹ Q *) | apply (erule allE) (* da ⟦A; P ?x⟧ ⟹ Q *) | ||
oops | oops | ||
+ | |||
+ | text {* Explicación | ||
+ | + Objetivo: "⟦A; ∀x. P x⟧ ⟹ Q" | ||
+ | + allI: "⟦∀x. ?P x; ?P ?x ⟹ ?R⟧ ⟹ ?R" | ||
+ | + Unificador de ("Q", "∀x. P x") y | ||
+ | ("?R·, "∀x. ?P x)" | ||
+ | es ?R / Q | ||
+ | ?P / P | ||
+ | + Nuevo objetivo: "⟦A; P ?x⟧ ⟹ Q" | ||
+ | *} | ||
lemma "⟦A; ∀x. P x⟧ ⟹ Q" | lemma "⟦A; ∀x. P x⟧ ⟹ Q" | ||
apply (erule_tac x=t in allE) (* da ⟦A; P t⟧ ⟹ Q *) | apply (erule_tac x=t in allE) (* da ⟦A; P t⟧ ⟹ Q *) | ||
oops | oops | ||
+ | |||
+ | text {* Explicación | ||
+ | + Objetivo: "⟦A; ∀x. P x⟧ ⟹ Q" | ||
+ | + allE: "⟦∀x. ?P x; ?P ?x ⟹ ?R⟧ ⟹ ?R" | ||
+ | + allE "x=t" "⟦∀x. ?P x; ?P t ⟹ ?R⟧ ⟹ ?R" | ||
+ | + Unificador de ("Q", "∀x. P x") y | ||
+ | ("?R·, "∀x. ?P x)" | ||
+ | es ?R / Q | ||
+ | ?P / P | ||
+ | + Nuevo objetivo: "⟦A; P ?t⟧ ⟹ Q" | ||
+ | *} | ||
lemma "⟦A; ∀x. P x⟧ ⟹ Q" | lemma "⟦A; ∀x. P x⟧ ⟹ Q" | ||
apply (frule spec) (* da ⟦A; ∀x. P x; P ?x⟧ ⟹ Q *) | apply (frule spec) (* da ⟦A; ∀x. P x; P ?x⟧ ⟹ Q *) | ||
oops | oops | ||
+ | |||
+ | text {* Explicación | ||
+ | + Objetivo: "⟦A; ∀x. P x⟧ ⟹ Q" | ||
+ | + spec: "∀x. ?P x ⟹ ?P ?x" | ||
+ | + Unificador de "∀x. P x" y | ||
+ | "∀x. ?P x" | ||
+ | es ?P / P | ||
+ | + Nuevo objetivo: "⟦A; ∀x. P x; P ?x⟧ ⟹ Q" | ||
+ | *} | ||
lemma "⟦A; ∀x. P x⟧ ⟹ Q" | lemma "⟦A; ∀x. P x⟧ ⟹ Q" | ||
apply (frule_tac x=t in spec) (* da ⟦A; ∀x. P x; P t⟧ ⟹ Q *) | apply (frule_tac x=t in spec) (* da ⟦A; ∀x. P x; P t⟧ ⟹ Q *) | ||
oops | oops | ||
+ | |||
+ | text {* Explicación | ||
+ | + Objetivo: "⟦A; ∀x. P x⟧ ⟹ Q" | ||
+ | + spec: "∀x. ?P x ⟹ ?P ?x" | ||
+ | + spec "x=t" "∀x. ?P x ⟹ ?P t" | ||
+ | + Unificador de "∀x. P x" y | ||
+ | "∀x. ?P x" | ||
+ | es ?P / P | ||
+ | + Nuevo objetivo: "⟦A; ∀x. P x; P t⟧ ⟹ Q" | ||
+ | *} | ||
lemma "A ⟹ ∃x. P x" | lemma "A ⟹ ∃x. P x" | ||
apply (rule exI) (* da A ⟹ P ?x *) | apply (rule exI) (* da A ⟹ P ?x *) | ||
oops | oops | ||
− | + | ||
+ | text {* Explicación | ||
+ | + Objetivo: "A ⟹ ∃x. P x" | ||
+ | + spec: "?P ?x ⟹ ∃x. ?P x" | ||
+ | + Unificador de "∃x. P x" y | ||
+ | "∃x. ?P x" | ||
+ | es ?P / P | ||
+ | + Nuevo objetivo: "A ⟹ P ?x" | ||
+ | *} | ||
+ | |||
lemma "A ⟹ ∃x. P x" | lemma "A ⟹ ∃x. P x" | ||
apply (rule_tac x=t in exI) (* da A ⟹ P t *) | apply (rule_tac x=t in exI) (* da A ⟹ P t *) | ||
oops | oops | ||
+ | |||
+ | text {* Explicación | ||
+ | + Objetivo: "A ⟹ ∃x. P x" | ||
+ | + spec: "?P ?x ⟹ ∃x. ?P x" | ||
+ | + spec "x=t": "?P t ⟹ ∃x. ?P x" | ||
+ | + Unificador de "∃x. P x" y | ||
+ | "∃x. ?P x" | ||
+ | es ?P / P | ||
+ | + Nuevo objetivo: "A ⟹ P t" | ||
+ | *} | ||
lemma "⟦A; ∃x. P x⟧ ⟹ Q" | lemma "⟦A; ∃x. P x⟧ ⟹ Q" | ||
apply (erule exE) (* da ⋀x. ⟦A; P x⟧ ⟹ Q *) | apply (erule exE) (* da ⋀x. ⟦A; P x⟧ ⟹ Q *) | ||
oops | oops | ||
+ | |||
+ | text {* Explicación | ||
+ | + Objetivo: "⟦A; ∃x. P x⟧ ⟹ Q" | ||
+ | + exE: "⟦∃x. ?P x; ⋀x. ?P x ⟹ ?Q⟧ ⟹ ?Q" | ||
+ | + Unificador de ("Q", "∃x. P x" y | ||
+ | ("?Q", "∃x. ?P x" | ||
+ | es ?Q / Q | ||
+ | ?P / P | ||
+ | + Nuevo objetivo: "⋀x. ⟦A; P x⟧ ⟹ Q" | ||
+ | *} | ||
section "Ejemplos del tema 6" | section "Ejemplos del tema 6" | ||
Línea 117: | Línea 388: | ||
lemma ej1: "⟦P(c); ∀x. (P(x) ⟶ ¬Q(x))⟧ ⟹ ¬Q(c)" | lemma ej1: "⟦P(c); ∀x. (P(x) ⟶ ¬Q(x))⟧ ⟹ ¬Q(c)" | ||
− | apply (erule allE) | + | apply (erule allE) (* da ⟦P c; P ?x ⟶ ¬ Q ?x⟧ ⟹ ¬ Q c *) |
− | apply (erule mp) | + | apply (erule mp) (* da P c ⟹ P c *) |
− | apply assumption | + | apply assumption (* da No subgoals! *) |
done | done | ||
+ | text {* Explicaciones | ||
+ | apply (erule allE) | ||
+ | + Objetivo: "⟦P(c); ∀x. (P(x) ⟶ ¬Q(x))⟧ ⟹ ¬Q(c)" | ||
+ | + allE: "⟦∀x. ?P x; ?P ?x ⟹ ?R⟧ ⟹ ?R" | ||
+ | + Unificador de ("¬Q(c)", "∀x. (P(x) ⟶ ¬Q(x))") y | ||
+ | ("?R", "∀x. ?P x") | ||
+ | es ?R / ¬Q(c) | ||
+ | ?P x / P(x) ⟶ ¬Q(x) | ||
+ | + Nuevo objetivo: "⟦P c; P ?x ⟶ ¬ Q ?x⟧ ⟹ ¬ Q c" | ||
+ | |||
+ | apply (erule mp) | ||
+ | + Objetivo: "⟦P c; P ?x ⟶ ¬ Q ?x⟧ ⟹ ¬ Q c" | ||
+ | + mp: "⟦?P ⟶ ?Q; ?P⟧ ⟹ ?Q" | ||
+ | + Unificador de ("¬ Q c", "P ?x ⟶ ¬ Q ?x") y | ||
+ | ("?Q", "?P ⟶ ?Q") | ||
+ | es ?Q / ¬ Q c | ||
+ | ?P / P c | ||
+ | + Nuevo objetivo: "P c ⟹ P c" | ||
+ | *} | ||
+ | |||
lemma ej2: "⟦∀x. (P x ⟶ ¬(Q x)); ∀y. P y⟧ ⟹ ∀z. ¬(Q z)" | lemma ej2: "⟦∀x. (P x ⟶ ¬(Q x)); ∀y. P y⟧ ⟹ ∀z. ¬(Q z)" | ||
− | apply (rule allI) | + | apply (rule allI) (* da ⋀z. ⟦P (?x2 z) ⟶ ¬ Q (?x2 z); |
− | apply (erule allE)+ | + | P (?y4 z)⟧ |
− | apply (erule mp) | + | ⟹ ¬ Q z*) |
− | apply assumption | + | 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 | done | ||
Línea 132: | Línea 427: | ||
lemma ej3: "∀x. P x ⟹ ∃y. P y" | lemma ej3: "∀x. P x ⟹ ∃y. P y" | ||
− | apply (erule allE) | + | apply (erule allE) (* da P ?x ⟹ ∃y. P y *) |
− | apply (erule exI) | + | apply (erule exI) (* da No subgoals! *) |
done | done | ||
lemma ej4: "⟦∀x. P x ⟶ Q x; ∃y. P y⟧ ⟹ ∃z. Q z" | lemma ej4: "⟦∀x. P x ⟶ Q x; ∃y. P y⟧ ⟹ ∃z. Q z" | ||
− | apply (erule exE) | + | apply (erule exE) (* da ⋀y. ⟦∀x. P x ⟶ Q x; P y⟧ ⟹ ∃z. Q z *) |
− | apply (erule allE) | + | apply (erule allE) (* da ⋀y. ⟦P y; P (?x2 y) ⟶ Q (?x2 y)⟧ ⟹ ∃z. Q z *) |
− | apply (rule exI) | + | apply (rule exI) (* da ⋀y. ⟦P y; P (?x2 y) ⟶ Q (?x2 y)⟧ ⟹ Q (?z4 y) *) |
− | apply (erule mp) | + | apply (erule mp) (* da ⋀y. P y ⟹ P (?x2 y) *) |
− | apply assumption | + | apply assumption (* da No subgoals! *) |
done | done | ||
Línea 147: | Línea 442: | ||
lemma ej5a: "¬(∀x. P x) ⟹ ∃y. ¬P y" | lemma ej5a: "¬(∀x. P x) ⟹ ∃y. ¬P y" | ||
− | apply (rule ccontr) | + | apply (rule ccontr) (* da ⟦¬ (∀x. P x); ∄y. ¬ P y⟧ ⟹ False *) |
− | apply (erule notE) | + | apply (erule notE) (* da ∄y. ¬ P y ⟹ ∀x. P x *) |
− | apply (rule allI) | + | apply (rule allI) (* da ⋀x. ∄y. ¬ P y ⟹ P x *) |
− | apply (rule ccontr) | + | apply (rule ccontr) (* da ⋀x. ⟦∄y. ¬ P y; ¬ P x⟧ ⟹ False *) |
− | apply (erule notE) | + | apply (erule notE) (* da ⋀x. ¬ P x ⟹ ∃y. ¬ P y *) |
− | apply (erule exI) | + | apply (erule exI) (* da No subgoals! *) |
done | done | ||
lemma ej5b: "∃x. ¬P x ⟹ ¬(∀y. P y)" | lemma ej5b: "∃x. ¬P x ⟹ ¬(∀y. P y)" | ||
− | apply (rule notI) | + | apply (rule notI) (* da ⟦∃x. ¬ P x; ∀y. P y⟧ ⟹ False *) |
− | apply (erule exE) | + | apply (erule exE) (* da ⋀x. ⟦∀y. P y; ¬ P x⟧ ⟹ False *) |
− | apply (erule allE) | + | apply (erule allE) (* da ⋀x. ⟦¬ P x; P (?y4 x)⟧ ⟹ False *) |
− | apply (erule notE) | + | apply (erule notE) (* da ⋀x. P (?y4 x) ⟹ P x *) |
− | apply assumption | + | apply assumption (* da No subgoals! *) |
done | done | ||
lemma ej5: "¬(∀x. P x) ⟷ (∃x. ¬P x)" | lemma ej5: "¬(∀x. P x) ⟷ (∃x. ¬P x)" | ||
− | apply (rule iffI) | + | apply (rule iffI) (* da ¬ (∀x. P x) ⟹ ∃x. ¬ P x |
− | apply (erule ej5a) | + | ∃x. ¬ P x ⟹ ¬ (∀x. P x) *) |
− | apply (erule ej5b) | + | apply (erule ej5a) (* da ∃x. ¬ P x ⟹ ¬ (∀x. P x) *) |
+ | apply (erule ej5b) (* da No subgoals! *) | ||
done | done | ||
lemma ej6a: "∀x. P(x) ∧ Q(x) ⟹ (∀x. P x) ∧ (∀x. Q x)" | lemma ej6a: "∀x. P(x) ∧ Q(x) ⟹ (∀x. P x) ∧ (∀x. Q x)" | ||
− | apply (rule conjI) | + | apply (rule conjI) (* da ∀x. P x ∧ Q x ⟹ ∀x. P x |
− | apply (rule allI) | + | ∀x. P x ∧ Q x ⟹ ∀x. Q x *) |
− | apply (erule allE) | + | apply (rule allI) (* da ⋀x. ∀x. P x ∧ Q x ⟹ P x |
− | apply (erule conjE) | + | ∀x. P x ∧ Q x ⟹ ∀x. Q x *) |
− | apply assumption | + | apply (erule allE) (* da ⋀x. P (?x5 x) ∧ Q (?x5 x) ⟹ P x |
− | apply (rule allI) | + | ∀x. P x ∧ Q x ⟹ ∀x. Q x *) |
− | apply (erule allE) | + | apply (erule conjE) (* da ⋀x. ⟦P (?x5 x); Q (?x5 x)⟧ ⟹ P x |
− | apply (erule conjE) | + | ∀x. P x ∧ Q x ⟹ ∀x. Q x *) |
− | apply assumption | + | apply assumption (* da ∀x. P x ∧ Q x ⟹ ∀x. Q x *) |
+ | apply (rule allI) (* da ⋀x. ∀x. P x ∧ Q x ⟹ Q x *) | ||
+ | apply (erule allE) (* da ⋀x. P (?x11 x) ∧ Q (?x11 x) ⟹ Q x *) | ||
+ | apply (erule conjE) (* da ⋀x. ⟦P (?x11 x); Q (?x11 x)⟧ ⟹ Q x *) | ||
+ | apply assumption (* da No subgoals! *) | ||
done | done | ||
lemma ej6b: "(∀x. P x) ∧ (∀x. Q x) ⟹ ∀x. P x ∧ Q x" | lemma ej6b: "(∀x. P x) ∧ (∀x. Q x) ⟹ ∀x. P x ∧ Q x" | ||
− | apply (rule allI) | + | apply (rule allI) (* da ⋀x. (∀x. P x) ∧ (∀x. Q x) ⟹ P x ∧ Q x *) |
− | apply (rule conjI) | + | apply (rule conjI) (* da ⋀x. (∀x. P x) ∧ (∀x. Q x) ⟹ P x |
− | apply (drule conjunct1) | + | ⋀x. (∀x. P x) ∧ (∀x. Q x) ⟹ Q x *) |
− | apply (erule spec) | + | apply (drule conjunct1) (* da ⋀x. ∀x. P x ⟹ P x |
− | apply (drule conjunct2) | + | ⋀x. (∀x. P x) ∧ (∀x. Q x) ⟹ Q x*) |
− | apply (erule spec) | + | apply (erule spec) (* da ⋀x. (∀x. P x) ∧ (∀x. Q x) ⟹ Q x *) |
+ | apply (drule conjunct2) (* da ⋀x. ∀x. Q x ⟹ Q x *) | ||
+ | apply (erule spec) (* da No subgoals! *) | ||
done | done | ||
lemma ej6: "(∀x. P x ∧ Q x) ⟷ (∀x. P x) ∧ (∀x. Q x)" | lemma ej6: "(∀x. P x ∧ Q x) ⟷ (∀x. P x) ∧ (∀x. Q x)" | ||
− | apply (rule iffI) | + | apply (rule iffI) (* da ∀x. P x ∧ Q x ⟹ (∀x. P x) ∧ (∀x. Q x) |
− | apply (erule ej6a) | + | (∀x. P x) ∧ (∀x. Q x) ⟹ ∀x. P x ∧ Q x *) |
− | apply (erule ej6b) | + | apply (erule ej6a) (* da (∀x. P x) ∧ (∀x. Q x) ⟹ ∀x. P x ∧ Q x *) |
+ | apply (erule ej6b) (* da No subgoals! *) | ||
done | done | ||
lemma ej7a: "(∃x. P x) ∨ (∃x. Q x) ⟹ ∃x. P x ∨ Q x" | lemma ej7a: "(∃x. P x) ∨ (∃x. Q x) ⟹ ∃x. P x ∨ Q x" | ||
− | apply (erule disjE) | + | apply (erule disjE) (* da ∃x. P x ⟹ ∃x. P x ∨ Q x |
− | apply (erule exE) | + | ∃x. Q x ⟹ ∃x. P x ∨ Q x *) |
− | apply (rule exI) | + | apply (erule exE) (* da ⋀x. P x ⟹ ∃x. P x ∨ Q x |
− | apply (erule disjI1) | + | ∃x. Q x ⟹ ∃x. P x ∨ Q x *) |
− | apply (erule exE) | + | apply (rule exI) (* da ⋀x. P x ⟹ P (?x5 x) ∨ Q (?x5 x) |
− | apply (rule exI) | + | ∃x. Q x ⟹ ∃x. P x ∨ Q x *) |
− | apply (erule disjI2) | + | apply (erule disjI1) (* da ∃x. Q x ⟹ ∃x. P x ∨ Q x *) |
+ | apply (erule exE) (* da ⋀x. Q x ⟹ ∃x. P x ∨ Q x *) | ||
+ | apply (rule exI) (* da ⋀x. Q x ⟹ P (?x10 x) ∨ Q (?x10 x) *) | ||
+ | apply (erule disjI2) (* da No subgoals! *) | ||
done | done | ||
lemma ej7b: "∃x. P x ∨ Q x ⟹ (∃x. P x) ∨ (∃x. Q x)" | lemma ej7b: "∃x. P x ∨ Q x ⟹ (∃x. P x) ∨ (∃x. Q x)" | ||
− | apply (erule exE) | + | apply (erule exE) (* da ⋀x. P x ∨ Q x ⟹ (∃x. P x) ∨ (∃x. Q x)*) |
− | apply (erule disjE) | + | apply (erule disjE) (* da ⋀x. P x ⟹ (∃x. P x) ∨ (∃x. Q x) |
− | apply (rule disjI1) | + | ⋀x. Q x ⟹ (∃x. P x) ∨ (∃x. Q x) *) |
− | apply (erule exI) | + | apply (rule disjI1) (* da ⋀x. P x ⟹ ∃x. P x |
− | apply (rule disjI2) | + | ⋀x. Q x ⟹ (∃x. P x) ∨ (∃x. Q x) *) |
− | apply (erule exI) | + | apply (erule exI) (* da ⋀x. Q x ⟹ (∃x. P x) ∨ (∃x. Q x) *) |
+ | apply (rule disjI2) (* da ⋀x. Q x ⟹ ∃x. Q x *) | ||
+ | apply (erule exI) (* da No subgoals! *) | ||
done | done | ||
lemma ej7: "(∃x. P x) ∨ (∃x. Q x) ⟷ (∃x. P x ∨ Q x)" | lemma ej7: "(∃x. P x) ∨ (∃x. Q x) ⟷ (∃x. P x ∨ Q x)" | ||
− | apply (rule iffI) | + | apply (rule iffI) (* da (∃x. P x) ∨ (∃x. Q x) ⟹ ∃x. P x ∨ Q x |
− | apply (erule ej7a) | + | ∃x. P x ∨ Q x ⟹ (∃x. P x) ∨ (∃x. Q x) *) |
− | apply (erule ej7b) | + | apply (erule ej7a) (* da ∃x. P x ∨ Q x ⟹ (∃x. P x) ∨ (∃x. Q x) *) |
+ | apply (erule ej7b) (* da No subgoals! *) | ||
done | done | ||
lemma ej8a: "∃x y. P x y ⟹ ∃y x. P x y" | lemma ej8a: "∃x y. P x y ⟹ ∃y x. P x y" | ||
− | apply (erule exE)+ | + | apply (erule exE)+ (* da ⋀x y. P x y ⟹ ∃y x. P x y *) |
− | apply (rule exI)+ | + | apply (rule exI)+ (* da ⋀x y. P x y ⟹ P (?x6 x y) (?y4 x y) *) |
− | apply assumption | + | apply assumption (* da No subgoals! *) |
done | done | ||
lemma ej8b: "∃y x. P x y ⟹ ∃x y. P x y" | lemma ej8b: "∃y x. P x y ⟹ ∃x y. P x y" | ||
− | apply (erule exE)+ | + | apply (erule exE)+ (* da ⋀y x. P x y ⟹ ∃x y. P x *) |
− | apply (rule exI)+ | + | apply (rule exI)+ (* da ⋀y x. P x y ⟹ P (?x4 y x) (?y6 y x)*) |
− | apply assumption | + | apply assumption (* da No subgoals! *) |
done | done | ||
lemma ej8: "(∃x y. P x y) ⟷ (∃y x. P x y)" | lemma ej8: "(∃x y. P x y) ⟷ (∃y x. P x y)" | ||
− | apply (rule iffI) | + | apply (rule iffI) (* da ∃x y. P x y ⟹ ∃y x. P x y |
− | apply (erule ej8a) | + | ∃y x. P x y ⟹ ∃x y. P x y *) |
− | apply (erule ej8b) | + | apply (erule ej8a) (* da ∃y x. P x y ⟹ ∃x y. P x y *) |
+ | apply (erule ej8b) (* da No subgoals! *) | ||
done | done | ||
end | end | ||
</source> | </source> | ||
− | |||
− | |||
− | |||
− | |||
− |
Revisión actual del 14:27 1 abr 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 {* Explicaciones:
apply (drule_tac x=a in spec)
+ Objetivo: "∀x. P x ⟹ ∃y. P y"
+ spec: "∀x. ?P x ⟹ ?P ?x"
+ spec "x=a": "∀x. ?P x ⟹ ?P a"
+ Unificador de "∀x. P x" con
"∀x. ?P x"
es ?P/P
+ Nuevo objetivo: "P a ⟹ ∃y. P y"
apply (rule_tac x=a in exI)
+ Objetivo: "P a ⟹ ∃y. P y"
+ exI: "?P ?x ⟹ ∃x. ?P x"
+ exI "x=a": "?P a ⟹ ∃x. ?P x"
+ Unificador de "∃y. P y" con
"∃x. ?P x"
es ?P/P
+ Nuevo objetivo: "P a ⟹ P a"
*}
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 {* Explicaciones
apply (rule exI)
+ Objetivo: "∀x. P x ⟹ ∃x. P x"
+ exI: "?P ?x ⟹ ∃x. ?P x"
+ Unificador de "∃x. P x" y
"∃x. ?P x"
es ?P/P
+ Nuevo objetivo: "∀x. P x ⟹ P ?x"
apply (erule spec)
+ Objetivo: "∀x. P x ⟹ P ?x"
+ spec: "∀x. ?P x ⟹ ?P ?x"
+ Unificador de ("?P ?x", "∀x. P x") y
("?P ?x", "∀x. ?P x"
es ?P/P
+ Nuevo objetivo: Vacío, porque erule aplica assumption a
"P ?x ⟹ P ?x"
*}
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 {* Explicaciones
apply (erule allE)
+ Objetivo: "∀x. P x ⟹ ∃x. P x"
+ allE: "⟦∀x. ?P x; ?P ?x ⟹ ?R⟧ ⟹ ?R"
+ Unificador de ("?R", "∀x. ?P x") y
("∃x. P x", "∀x. P x")
es ?R / ∃x. P x
?P / P
+ Nuevo objetivo: "P ?x ⟹ ∃x. P x"
apply (erule exI)
+ Objetivo: "P ?x ⟹ ∃x. P x"
+ exI: "?P ?x ⟹ ∃x. ?P x"
+ Unificador de ("∃x. P x", "P ?x") y
("∃x. ?P x", "?P ?x")
es ?P / P
?x / x
+ Nuevo objetivo: Vacío
*}
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
thm impE
text {* Explicaciones
apply (rule allI)
+ Objetivo: "⟦∀x. P x ⟶ Q x; ∀y. P y⟧ ⟹ ∀z. Q z"
+ allI: "(⋀x. ?P x) ⟹ ∀x. ?P x"
+ Unificador de "∀z. Q z" y
"∀x. ?P x"
es ?P / Q
+ Ligadura: ⋀x / ⋀z
+ Nuevo objetivo: "⋀z. ⟦∀x. P x ⟶ Q x; ∀y. P y⟧ ⟹ Q z"
apply (erule_tac x=z in allE)
+ Objetivo: "⋀z. ⟦∀x. P x ⟶ Q x; ∀y. P y⟧ ⟹ Q z"
+ allE: "⟦∀x. ?P x; ?P ?x ⟹ ?R⟧ ⟹ ?R"
+ allE "x=z" "⟦∀x. ?P x; ?P z ⟹ ?R⟧ ⟹ ?R"
+ Unificador de ("Q z", "∀x. P x ⟶ Q x") y
("?R", "∀x. ?P x")
es ?R / Q z
?P x / P x ⟶ Q x
+ Nuevo objetivo: "⋀z. ⟦∀y. P y; P z ⟶ Q z⟧ ⟹ Q z"
+ Nota: De "?P z ⟹ ?R" se obtiene la 2ª hipótesis y la conclusión.
apply (erule_tac x=z in allE)
+ Objetivo: "⋀z. ⟦∀y. P y; P z ⟶ Q z⟧ ⟹ Q z"
+ allE: "⟦∀x. ?P x; ?P ?x ⟹ ?R⟧ ⟹ ?R"
+ allE "x=z" "⟦∀x. ?P x; ?P z ⟹ ?R⟧ ⟹ ?R"
+ Unificador de ("Q z", "∀y. P y") y
("?R", "∀x. ?P x")
es ?R / Q z
?P / P
+ Nuevo objetivo: "⋀z. ⟦P z ⟶ Q z; P z⟧ ⟹ Q z"
+ Nota: De "?P z ⟹ ?R" se obtiene la 2ª hipótesis y la conclusión.
apply (erule impE)
+ Objetivo: "⋀z. ⟦P z ⟶ Q z; P z⟧ ⟹ Q z"
+ impE "⟦?P ⟶ ?Q; ?P; ?Q ⟹ ?R⟧ ⟹ ?R"
+ Unificador de ("Q z", "P z ⟶ Q z") y
("?R", "?P ⟶ ?Q")
es ?R / Q z
?P / P z
?Q /Q z
+ Nuevos objetivos: "⋀z. P z ⟹ P z"
"⋀z. ⟦P z; Q z⟧ ⟹ Q z"
*}
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 {*
apply (rule allI)
+ Objetivo: "⟦∀x. P x ⟶ Q x; ∀y. P y⟧ ⟹ ∀z. Q z"
+ allI: "(⋀x. ?P x) ⟹ ∀x. ?P x"
+ Unificador de "∀z. Q z" y
"∀x. ?P x"
es ?P / Q
+ Ligadura: ⋀x / ⋀z
+ Nuevo objetivo: "⋀z. ⟦∀x. P x ⟶ Q x; ∀y. P y⟧ ⟹ Q z"
apply (erule allE)
+ Objetivo: "⋀z. ⟦∀x. P x ⟶ Q x; ∀y. P y⟧ ⟹ Q z"
+ allE: "⟦∀x. ?P x; ?P ?x ⟹ ?R⟧ ⟹ ?R"
+ Unificador de ("Q z", "∀x. P x ⟶ Q x") y
("?R", "∀x. ?P x")
es ?R / Q z
?P x / P x ⟶ Q x
+ Nuevo objetivo: "⋀z. ⟦∀y. P y; P (?x2 z) ⟶ Q (?x2 z)⟧ ⟹ Q z"
apply (erule allE)
+ Objetivo: "⋀z. ⟦∀y. P y; P (?x2 z) ⟶ Q (?x2 z)⟧ ⟹ Q z"
+ allE: "⟦∀x. ?P x; ?P ?x ⟹ ?R⟧ ⟹ ?R"
+ Unificador de ("Q z", "∀y. P y") y
("?R", "∀x. ?P x")
es ?R / Q z
?P / P
+ Nuevo objetivo: "⋀z. ⟦P (?x2 z) ⟶ Q (?x2 z); P (?y4 z)⟧ ⟹ Q z"
apply (erule mp)
+ Objetivo: "⋀z. ⟦P (?x2 z) ⟶ Q (?x2 z); P (?y4 z)⟧ ⟹ Q z"
+ mp: "⟦?P ⟶ ?Q; ?P⟧ ⟹ ?Q"
+ Unificador de ("Q z", "P (?x2 z) ⟶ Q (?x2 z)") y
("?Q", "?P ⟶ ?Q")
es ?Q / Q z
?x2 z/ z
?P / P z
+ Nuevo objetivo: "⋀z. P (?y4 z) ⟹ P z"
*}
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
text {* Explicaciones:
apply (rule impI)
+ Objetivo: "(∃z. P z) ∧ Q ⟶ (∃y. P y ∧ Q)"
+ impI: "(?P ⟹ ?Q) ⟹ ?P ⟶ ?Q"
+ Unificador de "(∃z. P z) ∧ Q ⟶ (∃y. P y ∧ Q)" y
"?P ⟶ ?Q"
es ?P / "(∃z. P z) ∧ Q"
?Q / "∃y. P y ∧ Q"
+ Nuevo objetivo: "(∃z. P z) ∧ Q ⟹ ∃y. P y ∧ Q"
apply (erule conjE)
+ Objetivo: "(∃z. P z) ∧ Q ⟹ ∃y. P y ∧ Q"
+ conjE: "⟦?P ∧ ?Q; ⟦?P; ?Q⟧ ⟹ ?R⟧ ⟹ ?R"
+ Unificador de ("∃y. P y ∧ Q", "(∃z. P z) ∧ Q") y
("?R", "?P ∧ ?Q")
es ?R / "∃y. P y ∧ Q"
?P / "∃z. P z"
?Q / Q
+ Nuevo objetivo: "⟦∃z. P z; Q⟧ ⟹ ∃y. P y ∧ Q"
apply (erule exE)
+ Objetivo: "⟦∃z. P z; Q⟧ ⟹ ∃y. P y ∧ Q"
+ exE: "⟦∃x. ?P x; ⋀x. ?P x ⟹ ?Q⟧ ⟹ ?Q"
+ Unificador de ("∃y. P y ∧ Q", "∃z. P z") y
("?Q", "∃x. ?P x")
es ?Q / "∃y. P y ∧ Q"
?P x / P z
+ Nuevo objetivo: "⋀z. ⟦Q; P z⟧ ⟹ ∃y. P y ∧ Q"
apply (rule_tac x="z" in exI)
+ Objetivo: "⋀z. ⟦Q; P z⟧ ⟹ ∃y. P y ∧ Q"
+ exI: "?P ?x ⟹ ∃x. ?P x"
+ exI "x=z" "?P z ⟹ ∃x. ?P x"
+ Unificador de "∃y. P y ∧ Q" con
"∃x. ?P x"
es ?P x / P x ∧ Q
+ Nuevo objetivo: "⋀z. ⟦Q; P z⟧ ⟹ P z ∧ Q"
apply (rule conjI)
+ Objetivo: "⋀z. ⟦Q; P z⟧ ⟹ P z ∧ Q"
+ conjI: "⟦?P; ?Q⟧ ⟹ ?P ∧ ?Q"
+ Unificador de "P z ∧ Q" con
"?P ∧ ?Q"
es ?P / P z
?Q / Q
+ Nuevos objetivos: "⋀z. ⟦Q; P z⟧ ⟹ P z"
"⋀z. ⟦Q; P z⟧ ⟹ Q"
*}
subsection "Cálculo de secuentes de primer orden"
lemma "A ⟹ ∀x. P x"
apply (rule allI) (* da ⋀x. A ⟹ P x *)
oops
text {* Explicación
+ Objetivo: "A ⟹ ∀x. P x"
+ allI: "(⋀x. ?P x) ⟹ ∀x. ?P x"
+ Unificador de "∀x. P x" y
"∀x. ?P x"
es ?P / P
+ Nuevo objetivo: "⋀x. A ⟹ P x"
*}
lemma "⟦A; ∀x. P x⟧ ⟹ Q"
apply (erule allE) (* da ⟦A; P ?x⟧ ⟹ Q *)
oops
text {* Explicación
+ Objetivo: "⟦A; ∀x. P x⟧ ⟹ Q"
+ allI: "⟦∀x. ?P x; ?P ?x ⟹ ?R⟧ ⟹ ?R"
+ Unificador de ("Q", "∀x. P x") y
("?R·, "∀x. ?P x)"
es ?R / Q
?P / P
+ Nuevo objetivo: "⟦A; P ?x⟧ ⟹ Q"
*}
lemma "⟦A; ∀x. P x⟧ ⟹ Q"
apply (erule_tac x=t in allE) (* da ⟦A; P t⟧ ⟹ Q *)
oops
text {* Explicación
+ Objetivo: "⟦A; ∀x. P x⟧ ⟹ Q"
+ allE: "⟦∀x. ?P x; ?P ?x ⟹ ?R⟧ ⟹ ?R"
+ allE "x=t" "⟦∀x. ?P x; ?P t ⟹ ?R⟧ ⟹ ?R"
+ Unificador de ("Q", "∀x. P x") y
("?R·, "∀x. ?P x)"
es ?R / Q
?P / P
+ Nuevo objetivo: "⟦A; P ?t⟧ ⟹ Q"
*}
lemma "⟦A; ∀x. P x⟧ ⟹ Q"
apply (frule spec) (* da ⟦A; ∀x. P x; P ?x⟧ ⟹ Q *)
oops
text {* Explicación
+ Objetivo: "⟦A; ∀x. P x⟧ ⟹ Q"
+ spec: "∀x. ?P x ⟹ ?P ?x"
+ Unificador de "∀x. P x" y
"∀x. ?P x"
es ?P / P
+ Nuevo objetivo: "⟦A; ∀x. P x; P ?x⟧ ⟹ Q"
*}
lemma "⟦A; ∀x. P x⟧ ⟹ Q"
apply (frule_tac x=t in spec) (* da ⟦A; ∀x. P x; P t⟧ ⟹ Q *)
oops
text {* Explicación
+ Objetivo: "⟦A; ∀x. P x⟧ ⟹ Q"
+ spec: "∀x. ?P x ⟹ ?P ?x"
+ spec "x=t" "∀x. ?P x ⟹ ?P t"
+ Unificador de "∀x. P x" y
"∀x. ?P x"
es ?P / P
+ Nuevo objetivo: "⟦A; ∀x. P x; P t⟧ ⟹ Q"
*}
lemma "A ⟹ ∃x. P x"
apply (rule exI) (* da A ⟹ P ?x *)
oops
text {* Explicación
+ Objetivo: "A ⟹ ∃x. P x"
+ spec: "?P ?x ⟹ ∃x. ?P x"
+ Unificador de "∃x. P x" y
"∃x. ?P x"
es ?P / P
+ Nuevo objetivo: "A ⟹ P ?x"
*}
lemma "A ⟹ ∃x. P x"
apply (rule_tac x=t in exI) (* da A ⟹ P t *)
oops
text {* Explicación
+ Objetivo: "A ⟹ ∃x. P x"
+ spec: "?P ?x ⟹ ∃x. ?P x"
+ spec "x=t": "?P t ⟹ ∃x. ?P x"
+ Unificador de "∃x. P x" y
"∃x. ?P x"
es ?P / P
+ Nuevo objetivo: "A ⟹ P t"
*}
lemma "⟦A; ∃x. P x⟧ ⟹ Q"
apply (erule exE) (* da ⋀x. ⟦A; P x⟧ ⟹ Q *)
oops
text {* Explicación
+ Objetivo: "⟦A; ∃x. P x⟧ ⟹ Q"
+ exE: "⟦∃x. ?P x; ⋀x. ?P x ⟹ ?Q⟧ ⟹ ?Q"
+ Unificador de ("Q", "∃x. P x" y
("?Q", "∃x. ?P x"
es ?Q / Q
?P / P
+ Nuevo objetivo: "⋀x. ⟦A; P x⟧ ⟹ Q"
*}
section "Ejemplos del tema 6"
subsection {* Reglas del cuantificador universal *}
lemma ej1: "⟦P(c); ∀x. (P(x) ⟶ ¬Q(x))⟧ ⟹ ¬Q(c)"
apply (erule allE) (* da ⟦P c; P ?x ⟶ ¬ Q ?x⟧ ⟹ ¬ Q c *)
apply (erule mp) (* da P c ⟹ P c *)
apply assumption (* da No subgoals! *)
done
text {* Explicaciones
apply (erule allE)
+ Objetivo: "⟦P(c); ∀x. (P(x) ⟶ ¬Q(x))⟧ ⟹ ¬Q(c)"
+ allE: "⟦∀x. ?P x; ?P ?x ⟹ ?R⟧ ⟹ ?R"
+ Unificador de ("¬Q(c)", "∀x. (P(x) ⟶ ¬Q(x))") y
("?R", "∀x. ?P x")
es ?R / ¬Q(c)
?P x / P(x) ⟶ ¬Q(x)
+ Nuevo objetivo: "⟦P c; P ?x ⟶ ¬ Q ?x⟧ ⟹ ¬ Q c"
apply (erule mp)
+ Objetivo: "⟦P c; P ?x ⟶ ¬ Q ?x⟧ ⟹ ¬ Q c"
+ mp: "⟦?P ⟶ ?Q; ?P⟧ ⟹ ?Q"
+ Unificador de ("¬ Q c", "P ?x ⟶ ¬ Q ?x") y
("?Q", "?P ⟶ ?Q")
es ?Q / ¬ Q c
?P / P c
+ Nuevo objetivo: "P c ⟹ P c"
*}
lemma ej2: "⟦∀x. (P x ⟶ ¬(Q x)); ∀y. P y⟧ ⟹ ∀z. ¬(Q z)"
apply (rule allI) (* da ⋀z. ⟦P (?x2 z) ⟶ ¬ Q (?x2 z);
P (?y4 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
subsection "Reglas del cuantificador existencial"
lemma ej3: "∀x. P x ⟹ ∃y. P y"
apply (erule allE) (* da P ?x ⟹ ∃y. P y *)
apply (erule exI) (* da No subgoals! *)
done
lemma ej4: "⟦∀x. P x ⟶ Q x; ∃y. P y⟧ ⟹ ∃z. Q z"
apply (erule exE) (* da ⋀y. ⟦∀x. P x ⟶ Q x; P y⟧ ⟹ ∃z. Q z *)
apply (erule allE) (* da ⋀y. ⟦P y; P (?x2 y) ⟶ Q (?x2 y)⟧ ⟹ ∃z. Q z *)
apply (rule exI) (* da ⋀y. ⟦P y; P (?x2 y) ⟶ Q (?x2 y)⟧ ⟹ Q (?z4 y) *)
apply (erule mp) (* da ⋀y. P y ⟹ P (?x2 y) *)
apply assumption (* da No subgoals! *)
done
subsection "Demostraciones de equivalencias"
lemma ej5a: "¬(∀x. P x) ⟹ ∃y. ¬P y"
apply (rule ccontr) (* da ⟦¬ (∀x. P x); ∄y. ¬ P y⟧ ⟹ False *)
apply (erule notE) (* da ∄y. ¬ P y ⟹ ∀x. P x *)
apply (rule allI) (* da ⋀x. ∄y. ¬ P y ⟹ P x *)
apply (rule ccontr) (* da ⋀x. ⟦∄y. ¬ P y; ¬ P x⟧ ⟹ False *)
apply (erule notE) (* da ⋀x. ¬ P x ⟹ ∃y. ¬ P y *)
apply (erule exI) (* da No subgoals! *)
done
lemma ej5b: "∃x. ¬P x ⟹ ¬(∀y. P y)"
apply (rule notI) (* da ⟦∃x. ¬ P x; ∀y. P y⟧ ⟹ False *)
apply (erule exE) (* da ⋀x. ⟦∀y. P y; ¬ P x⟧ ⟹ False *)
apply (erule allE) (* da ⋀x. ⟦¬ P x; P (?y4 x)⟧ ⟹ False *)
apply (erule notE) (* da ⋀x. P (?y4 x) ⟹ P x *)
apply assumption (* da No subgoals! *)
done
lemma ej5: "¬(∀x. P x) ⟷ (∃x. ¬P x)"
apply (rule iffI) (* da ¬ (∀x. P x) ⟹ ∃x. ¬ P x
∃x. ¬ P x ⟹ ¬ (∀x. P x) *)
apply (erule ej5a) (* da ∃x. ¬ P x ⟹ ¬ (∀x. P x) *)
apply (erule ej5b) (* da No subgoals! *)
done
lemma ej6a: "∀x. P(x) ∧ Q(x) ⟹ (∀x. P x) ∧ (∀x. Q x)"
apply (rule conjI) (* da ∀x. P x ∧ Q x ⟹ ∀x. P x
∀x. P x ∧ Q x ⟹ ∀x. Q x *)
apply (rule allI) (* da ⋀x. ∀x. P x ∧ Q x ⟹ P x
∀x. P x ∧ Q x ⟹ ∀x. Q x *)
apply (erule allE) (* da ⋀x. P (?x5 x) ∧ Q (?x5 x) ⟹ P x
∀x. P x ∧ Q x ⟹ ∀x. Q x *)
apply (erule conjE) (* da ⋀x. ⟦P (?x5 x); Q (?x5 x)⟧ ⟹ P x
∀x. P x ∧ Q x ⟹ ∀x. Q x *)
apply assumption (* da ∀x. P x ∧ Q x ⟹ ∀x. Q x *)
apply (rule allI) (* da ⋀x. ∀x. P x ∧ Q x ⟹ Q x *)
apply (erule allE) (* da ⋀x. P (?x11 x) ∧ Q (?x11 x) ⟹ Q x *)
apply (erule conjE) (* da ⋀x. ⟦P (?x11 x); Q (?x11 x)⟧ ⟹ Q x *)
apply assumption (* da No subgoals! *)
done
lemma ej6b: "(∀x. P x) ∧ (∀x. Q x) ⟹ ∀x. P x ∧ Q x"
apply (rule allI) (* da ⋀x. (∀x. P x) ∧ (∀x. Q x) ⟹ P x ∧ Q x *)
apply (rule conjI) (* da ⋀x. (∀x. P x) ∧ (∀x. Q x) ⟹ P x
⋀x. (∀x. P x) ∧ (∀x. Q x) ⟹ Q x *)
apply (drule conjunct1) (* da ⋀x. ∀x. P x ⟹ P x
⋀x. (∀x. P x) ∧ (∀x. Q x) ⟹ Q x*)
apply (erule spec) (* da ⋀x. (∀x. P x) ∧ (∀x. Q x) ⟹ Q x *)
apply (drule conjunct2) (* da ⋀x. ∀x. Q x ⟹ Q x *)
apply (erule spec) (* da No subgoals! *)
done
lemma ej6: "(∀x. P x ∧ Q x) ⟷ (∀x. P x) ∧ (∀x. Q x)"
apply (rule iffI) (* da ∀x. P x ∧ Q x ⟹ (∀x. P x) ∧ (∀x. Q x)
(∀x. P x) ∧ (∀x. Q x) ⟹ ∀x. P x ∧ Q x *)
apply (erule ej6a) (* da (∀x. P x) ∧ (∀x. Q x) ⟹ ∀x. P x ∧ Q x *)
apply (erule ej6b) (* da No subgoals! *)
done
lemma ej7a: "(∃x. P x) ∨ (∃x. Q x) ⟹ ∃x. P x ∨ Q x"
apply (erule disjE) (* da ∃x. P x ⟹ ∃x. P x ∨ Q x
∃x. Q x ⟹ ∃x. P x ∨ Q x *)
apply (erule exE) (* da ⋀x. P x ⟹ ∃x. P x ∨ Q x
∃x. Q x ⟹ ∃x. P x ∨ Q x *)
apply (rule exI) (* da ⋀x. P x ⟹ P (?x5 x) ∨ Q (?x5 x)
∃x. Q x ⟹ ∃x. P x ∨ Q x *)
apply (erule disjI1) (* da ∃x. Q x ⟹ ∃x. P x ∨ Q x *)
apply (erule exE) (* da ⋀x. Q x ⟹ ∃x. P x ∨ Q x *)
apply (rule exI) (* da ⋀x. Q x ⟹ P (?x10 x) ∨ Q (?x10 x) *)
apply (erule disjI2) (* da No subgoals! *)
done
lemma ej7b: "∃x. P x ∨ Q x ⟹ (∃x. P x) ∨ (∃x. Q x)"
apply (erule exE) (* da ⋀x. P x ∨ Q x ⟹ (∃x. P x) ∨ (∃x. Q x)*)
apply (erule disjE) (* da ⋀x. P x ⟹ (∃x. P x) ∨ (∃x. Q x)
⋀x. Q x ⟹ (∃x. P x) ∨ (∃x. Q x) *)
apply (rule disjI1) (* da ⋀x. P x ⟹ ∃x. P x
⋀x. Q x ⟹ (∃x. P x) ∨ (∃x. Q x) *)
apply (erule exI) (* da ⋀x. Q x ⟹ (∃x. P x) ∨ (∃x. Q x) *)
apply (rule disjI2) (* da ⋀x. Q x ⟹ ∃x. Q x *)
apply (erule exI) (* da No subgoals! *)
done
lemma ej7: "(∃x. P x) ∨ (∃x. Q x) ⟷ (∃x. P x ∨ Q x)"
apply (rule iffI) (* da (∃x. P x) ∨ (∃x. Q x) ⟹ ∃x. P x ∨ Q x
∃x. P x ∨ Q x ⟹ (∃x. P x) ∨ (∃x. Q x) *)
apply (erule ej7a) (* da ∃x. P x ∨ Q x ⟹ (∃x. P x) ∨ (∃x. Q x) *)
apply (erule ej7b) (* da No subgoals! *)
done
lemma ej8a: "∃x y. P x y ⟹ ∃y x. P x y"
apply (erule exE)+ (* da ⋀x y. P x y ⟹ ∃y x. P x y *)
apply (rule exI)+ (* da ⋀x y. P x y ⟹ P (?x6 x y) (?y4 x y) *)
apply assumption (* da No subgoals! *)
done
lemma ej8b: "∃y x. P x y ⟹ ∃x y. P x y"
apply (erule exE)+ (* da ⋀y x. P x y ⟹ ∃x y. P x *)
apply (rule exI)+ (* da ⋀y x. P x y ⟹ P (?x4 y x) (?y6 y x)*)
apply assumption (* da No subgoals! *)
done
lemma ej8: "(∃x y. P x y) ⟷ (∃y x. P x y)"
apply (rule iffI) (* da ∃x y. P x y ⟹ ∃y x. P x y
∃y x. P x y ⟹ ∃x y. P x y *)
apply (erule ej8a) (* da ∃y x. P x y ⟹ ∃x y. P x y *)
apply (erule ej8b) (* da No subgoals! *)
done
end