Theory Quantifiers

(*  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