# Theory Quantifiers_Int

theory Quantifiers_Int
imports IFOL
```(*  Title:      FOL/ex/Quantifiers_Int.thy
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright   1991  University of Cambridge
*)

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")

― ‹Converse is false›
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")

― ‹Converse is false›
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›

― ‹TRUE›
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")

― ‹An example of why exI should be delayed as long as possible›
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›

― ‹Principia Mathematica *11.53›
lemma "(∀x y. P(x) ⟶ Q(y)) ⟷ ((∃x. P(x)) ⟶ (∀y. Q(y)))"
by (tactic "IntPr.fast_tac @{context} 1")

(*Principia Mathematica *11.55  *)
lemma "(∃x y. P(x) ∧ Q(x,y)) ⟷ (∃x. P(x) ∧ (∃y. Q(x,y)))"
by (tactic "IntPr.fast_tac @{context} 1")

(*Principia Mathematica *11.61  *)
lemma "(∃y. ∀x. P(x) ⟶ Q(x,y)) ⟶ (∀x. P(x) ⟶ (∃y. Q(x,y)))"
by (tactic "IntPr.fast_tac @{context} 1")

end
```