(*  Title:      Sequents/LK/Quantifiers.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1992  University of Cambridge

Classical sequent calculus: examples with quantifiers.
*)

theory Quantifiers
imports "../LK"
begin

lemma "⊨ (∀x. P) ⟷ P"
  by fast

lemma "⊨ (∀x y. P(x,y)) ⟷ (∀y x. P(x,y))"
  by fast

lemma "∀u. P(u), ∀v. Q(v) ⊨ ∀u v. P(u) ∧ Q(v)"
  by fast


text "Permutation of existential quantifier."

lemma "⊨ (∃x y. P(x,y)) ⟷ (∃y x. P(x,y))"
  by fast

lemma "⊨ (∀x. P(x) ∧ Q(x)) ⟷ (∀x. P(x)) ∧ (∀x. Q(x))"
  by fast

(*Converse is invalid*)
lemma "⊨ (∀x. P(x)) ∨ (∀x. Q(x)) ⟶ (∀x. P(x) ∨ Q(x))"
  by fast


text "Pushing ∀into an implication."

lemma "⊨ (∀x. P ⟶ Q(x)) ⟷ (P ⟶ (∀x. Q(x)))"
  by fast

lemma "⊨ (∀x. P(x) ⟶ Q) ⟷ ((∃x. P(x)) ⟶ Q)"
  by fast

lemma "⊨ (∃x. P) ⟷ P"
  by fast


text "Distribution of ∃over disjunction."

lemma "⊨ (∃x. P(x) ∨ Q(x)) ⟷ (∃x. P(x)) ∨ (∃x. Q(x))"
  by fast

(*Converse is invalid*)
lemma "⊨ (∃x. P(x) ∧ Q(x)) ⟶ (∃x. P(x)) ∧ (∃x. Q(x))"
  by fast


text "Harder examples: classical theorems."

lemma "⊨ (∃x. P ⟶ Q(x)) ⟷ (P ⟶ (∃x. Q(x)))"
  by fast

lemma "⊨ (∃x. P(x) ⟶ Q) ⟷ (∀x. P(x)) ⟶ Q"
  by fast

lemma "⊨ (∀x. P(x)) ∨ Q ⟷ (∀x. P(x) ∨ Q)"
  by fast


text "Basic test of quantifier reasoning"

lemma "⊨ (∃y. ∀x. Q(x,y)) ⟶ (∀x. ∃y. Q(x,y))"
  by fast

lemma "⊨ (∀x. Q(x)) ⟶ (∃x. Q(x))"
  by fast


text "The following are invalid!"

(*INVALID*)
lemma "⊨ (∀x. ∃y. Q(x,y)) ⟶ (∃y. ∀x. Q(x,y))"
  apply fast?
  apply (rule _)
  oops

(*INVALID*)
lemma "⊨ (∃x. Q(x)) ⟶ (∀x. Q(x))"
  apply fast?
  apply (rule _)
  oops

(*INVALID*)
schematic_goal "⊨ P(?a) ⟶ (∀x. P(x))"
  apply fast?
  apply (rule _)
  oops

(*INVALID*)
schematic_goal "⊨ (P(?a) ⟶ (∀x. Q(x))) ⟶ (∀x. P(x) ⟶ Q(x))"
  apply fast?
  apply (rule _)
  oops


text "Back to things that are provable..."

lemma "⊨ (∀x. P(x) ⟶ Q(x)) ∧ (∃x. P(x)) ⟶ (∃x. Q(x))"
  by fast

(*An example of why exR should be delayed as long as possible*)
lemma "⊨ (P ⟶ (∃x. Q(x))) ∧ P ⟶ (∃x. Q(x))"
  by fast


text "Solving for a Var"

schematic_goal "⊨ (∀x. P(x) ⟶ Q(f(x))) ∧ (∀x. Q(x) ⟶ R(g(x))) ∧ P(d) ⟶ R(?a)"
  by fast


text "Principia Mathematica *11.53"

lemma "⊨ (∀x y. P(x) ⟶ Q(y)) ⟷ ((∃x. P(x)) ⟶ (∀y. Q(y)))"
  by fast


text "Principia Mathematica *11.55"

lemma "⊨ (∃x y. P(x) ∧ Q(x,y)) ⟷ (∃x. P(x) ∧ (∃y. Q(x,y)))"
  by fast


text "Principia Mathematica *11.61"

lemma "⊨ (∃y. ∀x. P(x) ⟶ Q(x,y)) ⟶ (∀x. P(x) ⟶ (∃y. Q(x,y)))"
  by fast


(*21 August 88: loaded in 45.7 secs*)
(*18 September 2005: loaded in 0.114 secs*)

end