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
