Theory Quantifiers_Int
section ‹First-Order Logic: quantifier examples (intuitionistic version)›
theory Quantifiers_Int
imports IFOL
begin
lemma ‹(∀x y. P(x,y)) ⟶ (∀y x. P(x,y))›
by (tactic "IntPr.fast_tac \<^context> 1")
lemma ‹(∃x y. P(x,y)) ⟶ (∃y x. P(x,y))›
by (tactic "IntPr.fast_tac \<^context> 1")
lemma ‹(∀x. P(x)) ∨ (∀x. Q(x)) ⟶ (∀x. P(x) ∨ Q(x))›
by (tactic "IntPr.fast_tac \<^context> 1")
lemma ‹(∀x. P ⟶ Q(x)) ⟷ (P ⟶ (∀x. Q(x)))›
by (tactic "IntPr.fast_tac \<^context> 1")
lemma ‹(∀x. P(x) ⟶ Q) ⟷ ((∃x. P(x)) ⟶ Q)›
by (tactic "IntPr.fast_tac \<^context> 1")
text ‹Some harder ones›
lemma ‹(∃x. P(x) ∨ Q(x)) ⟷ (∃x. P(x)) ∨ (∃x. Q(x))›
by (tactic "IntPr.fast_tac \<^context> 1")
lemma ‹(∃x. P(x) ∧ Q(x)) ⟶ (∃x. P(x)) ∧ (∃x. Q(x))›
by (tactic "IntPr.fast_tac \<^context> 1")
text ‹Basic test of quantifier reasoning›
lemma ‹(∃y. ∀x. Q(x,y)) ⟶ (∀x. ∃y. Q(x,y))›
by (tactic "IntPr.fast_tac \<^context> 1")
lemma ‹(∀x. Q(x)) ⟶ (∃x. Q(x))›
by (tactic "IntPr.fast_tac \<^context> 1")
text ‹The following should fail, as they are false!›
lemma ‹(∀x. ∃y. Q(x,y)) ⟶ (∃y. ∀x. Q(x,y))›
apply (tactic "IntPr.fast_tac \<^context> 1")?
oops
lemma ‹(∃x. Q(x)) ⟶ (∀x. Q(x))›
apply (tactic "IntPr.fast_tac \<^context> 1")?
oops
schematic_goal ‹P(?a) ⟶ (∀x. P(x))›
apply (tactic "IntPr.fast_tac \<^context> 1")?
oops
schematic_goal ‹(P(?a) ⟶ (∀x. Q(x))) ⟶ (∀x. P(x) ⟶ Q(x))›
apply (tactic "IntPr.fast_tac \<^context> 1")?
oops
text ‹Back to things that are provable \dots›
lemma ‹(∀x. P(x) ⟶ Q(x)) ∧ (∃x. P(x)) ⟶ (∃x. Q(x))›
by (tactic "IntPr.fast_tac \<^context> 1")
lemma ‹(P ⟶ (∃x. Q(x))) ∧ P ⟶ (∃x. Q(x))›
by (tactic "IntPr.fast_tac \<^context> 1")
schematic_goal ‹(∀x. P(x) ⟶ Q(f(x))) ∧ (∀x. Q(x) ⟶ R(g(x))) ∧ P(d) ⟶ R(?a)›
by (tactic "IntPr.fast_tac \<^context> 1")
lemma ‹(∀x. Q(x)) ⟶ (∃x. Q(x))›
by (tactic "IntPr.fast_tac \<^context> 1")
text ‹Some slow ones›
lemma ‹(∀x y. P(x) ⟶ Q(y)) ⟷ ((∃x. P(x)) ⟶ (∀y. Q(y)))›
by (tactic "IntPr.fast_tac \<^context> 1")
lemma ‹(∃x y. P(x) ∧ Q(x,y)) ⟷ (∃x. P(x) ∧ (∃y. Q(x,y)))›
by (tactic "IntPr.fast_tac \<^context> 1")
lemma ‹(∃y. ∀x. P(x) ⟶ Q(x,y)) ⟶ (∀x. P(x) ⟶ (∃y. Q(x,y)))›
by (tactic "IntPr.fast_tac \<^context> 1")
end