src/Sequents/LK/Quantifiers.thy

only start jobs early if they are due (cf. 1966578feff8);

(*  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 "\<turnstile> (\<forall>x. P) \<longleftrightarrow> P"
  by fast

lemma "\<turnstile> (\<forall>x y. P(x,y)) \<longleftrightarrow> (\<forall>y x. P(x,y))"
  by fast

lemma "\<forall>u. P(u), \<forall>v. Q(v) \<turnstile> \<forall>u v. P(u) \<and> Q(v)"
  by fast


text "Permutation of existential quantifier."

lemma "\<turnstile> (\<exists>x y. P(x,y)) \<longleftrightarrow> (\<exists>y x. P(x,y))"
  by fast

lemma "\<turnstile> (\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> (\<forall>x. P(x)) \<and> (\<forall>x. Q(x))"
  by fast

(*Converse is invalid*)
lemma "\<turnstile> (\<forall>x. P(x)) \<or> (\<forall>x. Q(x)) \<longrightarrow> (\<forall>x. P(x) \<or> Q(x))"
  by fast


text "Pushing \<forall>into an implication."

lemma "\<turnstile> (\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x. Q(x)))"
  by fast

lemma "\<turnstile> (\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> Q)"
  by fast

lemma "\<turnstile> (\<exists>x. P)  \<longleftrightarrow>  P"
  by fast


text "Distribution of \<exists>over disjunction."

lemma "\<turnstile> (\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))"
  by fast

(*Converse is invalid*)
lemma "\<turnstile> (\<exists>x. P(x) \<and> Q(x)) \<longrightarrow> (\<exists>x. P(x)) \<and> (\<exists>x. Q(x))"
  by fast


text "Harder examples: classical theorems."

lemma "\<turnstile> (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<exists>x. Q(x)))"
  by fast

lemma "\<turnstile> (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
  by fast

lemma "\<turnstile> (\<forall>x. P(x)) \<or> Q \<longleftrightarrow> (\<forall>x. P(x) \<or> Q)"
  by fast


text "Basic test of quantifier reasoning"

lemma "\<turnstile> (\<exists>y. \<forall>x. Q(x,y)) \<longrightarrow> (\<forall>x. \<exists>y. Q(x,y))"
  by fast

lemma "\<turnstile> (\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))"
  by fast


text "The following are invalid!"

(*INVALID*)
lemma "\<turnstile> (\<forall>x. \<exists>y. Q(x,y)) \<longrightarrow> (\<exists>y. \<forall>x. Q(x,y))"
  apply fast?
  apply (rule _)
  oops

(*INVALID*)
lemma "\<turnstile> (\<exists>x. Q(x)) \<longrightarrow> (\<forall>x. Q(x))"
  apply fast?
  apply (rule _)
  oops

(*INVALID*)
schematic_goal "\<turnstile> P(?a) \<longrightarrow> (\<forall>x. P(x))"
  apply fast?
  apply (rule _)
  oops

(*INVALID*)
schematic_goal "\<turnstile> (P(?a) \<longrightarrow> (\<forall>x. Q(x))) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> Q(x))"
  apply fast?
  apply (rule _)
  oops


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

lemma "\<turnstile> (\<forall>x. P(x) \<longrightarrow> Q(x)) \<and> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))"
  by fast

(*An example of why exR should be delayed as long as possible*)
lemma "\<turnstile> (P \<longrightarrow> (\<exists>x. Q(x))) \<and> P \<longrightarrow> (\<exists>x. Q(x))"
  by fast


text "Solving for a Var"

schematic_goal "\<turnstile> (\<forall>x. P(x) \<longrightarrow> Q(f(x))) \<and> (\<forall>x. Q(x) \<longrightarrow> R(g(x))) \<and> P(d) \<longrightarrow> R(?a)"
  by fast


text "Principia Mathematica *11.53"

lemma "\<turnstile> (\<forall>x y. P(x) \<longrightarrow> Q(y)) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> (\<forall>y. Q(y)))"
  by fast


text "Principia Mathematica *11.55"

lemma "\<turnstile> (\<exists>x y. P(x) \<and> Q(x,y)) \<longleftrightarrow> (\<exists>x. P(x) \<and> (\<exists>y. Q(x,y)))"
  by fast


text "Principia Mathematica *11.61"

lemma "\<turnstile> (\<exists>y. \<forall>x. P(x) \<longrightarrow> Q(x,y)) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> (\<exists>y. Q(x,y)))"
  by fast


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

end