Theory OrdQuant

(*  Title:      ZF/OrdQuant.thy
    Authors:    Krzysztof Grabczewski and L C Paulson
*)

section ‹Special quantifiers›

theory OrdQuant imports Ordinal begin

subsection ‹Quantifiers and union operator for ordinals›

definition
  (* Ordinal Quantifiers *)
  oall :: "[i, i  o]  o"  where
    "oall(A, P)  x. x<A  P(x)"

definition
  oex :: "[i, i  o]  o"  where
    "oex(A, P)   x. x<A  P(x)"

definition
  (* Ordinal Union *)
  OUnion :: "[i, i  i]  i"  where
    "OUnion(i,B)  {z: xi. B(x). Ord(i)}"

syntax
  "_oall"     :: "[idt, i, o]  o"        ((3_<_./ _) 10)
  "_oex"      :: "[idt, i, o]  o"        ((3_<_./ _) 10)
  "_OUNION"   :: "[idt, i, i]  i"        ((3_<_./ _) 10)
translations
  "x<a. P"  "CONST oall(a, λx. P)"
  "x<a. P"  "CONST oex(a, λx. P)"
  "x<a. B"  "CONST OUnion(a, λx. B)"


subsubsection ‹simplification of the new quantifiers›


(*MOST IMPORTANT that this is added to the simpset BEFORE Ord_atomize
  is proved.  Ord_atomize would convert this rule to
    x < 0 ⟹ P(x) ≡ True, which causes dire effects!*)
lemma [simp]: "(x<0. P(x))"
by (simp add: oall_def)

lemma [simp]: "¬(x<0. P(x))"
by (simp add: oex_def)

lemma [simp]: "(x<succ(i). P(x)) <-> (Ord(i)  P(i)  (x<i. P(x)))"
apply (simp add: oall_def le_iff)
apply (blast intro: lt_Ord2)
done

lemma [simp]: "(x<succ(i). P(x)) <-> (Ord(i)  (P(i) | (x<i. P(x))))"
apply (simp add: oex_def le_iff)
apply (blast intro: lt_Ord2)
done

subsubsection ‹Union over ordinals›

lemma Ord_OUN [intro,simp]:
     "x. x<A  Ord(B(x))  Ord(x<A. B(x))"
by (simp add: OUnion_def ltI Ord_UN)

lemma OUN_upper_lt:
     "a<A;  i < b(a);  Ord(x<A. b(x))  i < (x<A. b(x))"
by (unfold OUnion_def lt_def, blast )

lemma OUN_upper_le:
     "a<A;  ib(a);  Ord(x<A. b(x))  i  (x<A. b(x))"
apply (unfold OUnion_def, auto)
apply (rule UN_upper_le )
apply (auto simp add: lt_def)
done

lemma Limit_OUN_eq: "Limit(i)  (x<i. x) = i"
by (simp add: OUnion_def Limit_Union_eq Limit_is_Ord)

(* No < version of this theorem: consider that @{term"(⋃i∈nat.i)=nat"}! *)
lemma OUN_least:
     "(x. x<A  B(x)  C)  (x<A. B(x))  C"
by (simp add: OUnion_def UN_least ltI)

lemma OUN_least_le:
     "Ord(i);  x. x<A  b(x)  i  (x<A. b(x))  i"
by (simp add: OUnion_def UN_least_le ltI Ord_0_le)

lemma le_implies_OUN_le_OUN:
     "x. x<A  c(x)  d(x)  (x<A. c(x))  (x<A. d(x))"
by (blast intro: OUN_least_le OUN_upper_le le_Ord2 Ord_OUN)

lemma OUN_UN_eq:
     "(x. x  A  Ord(B(x)))
       (z < (xA. B(x)). C(z)) = (xA. z < B(x). C(z))"
by (simp add: OUnion_def)

lemma OUN_Union_eq:
     "(x. x  X  Ord(x))
       (z < (X). C(z)) = (xX. z < x. C(z))"
by (simp add: OUnion_def)

(*So that rule_format will get rid of this quantifier...*)
lemma atomize_oall [symmetric, rulify]:
     "(x. x<A  P(x))  Trueprop (x<A. P(x))"
by (simp add: oall_def atomize_all atomize_imp)

subsubsection ‹universal quantifier for ordinals›

lemma oallI [intro!]:
    "x. x<A  P(x)  x<A. P(x)"
by (simp add: oall_def)

lemma ospec: "x<A. P(x);  x<A  P(x)"
by (simp add: oall_def)

lemma oallE:
    "x<A. P(x);  P(x)  Q;  ¬x<A  Q  Q"
by (simp add: oall_def, blast)

lemma rev_oallE [elim]:
    "x<A. P(x);  ¬x<A  Q;  P(x)  Q  Q"
by (simp add: oall_def, blast)


(*Trival rewrite rule.  @{term"(∀x<a.P)<->P"} holds only if a is not 0!*)
lemma oall_simp [simp]: "(x<a. True) <-> True"
by blast

(*Congruence rule for rewriting*)
lemma oall_cong [cong]:
    "a=a';  x. x<a'  P(x) <-> P'(x)
      oall(a, λx. P(x)) <-> oall(a', λx. P'(x))"
by (simp add: oall_def)


subsubsection ‹existential quantifier for ordinals›

lemma oexI [intro]:
    "P(x);  x<A  x<A. P(x)"
apply (simp add: oex_def, blast)
done

(*Not of the general form for such rules... *)
lemma oexCI:
   "x<A. ¬P(x)  P(a);  a<A  x<A. P(x)"
apply (simp add: oex_def, blast)
done

lemma oexE [elim!]:
    "x<A. P(x);  x. x<A; P(x)  Q  Q"
apply (simp add: oex_def, blast)
done

lemma oex_cong [cong]:
    "a=a';  x. x<a'  P(x) <-> P'(x)
      oex(a, λx. P(x)) <-> oex(a', λx. P'(x))"
apply (simp add: oex_def cong add: conj_cong)
done


subsubsection ‹Rules for Ordinal-Indexed Unions›

lemma OUN_I [intro]: "a<i;  b  B(a)  b: (z<i. B(z))"
by (unfold OUnion_def lt_def, blast)

lemma OUN_E [elim!]:
    "b  (z<i. B(z));  a.b  B(a);  a<i  R  R"
apply (unfold OUnion_def lt_def, blast)
done

lemma OUN_iff: "b  (x<i. B(x)) <-> (x<i. b  B(x))"
by (unfold OUnion_def oex_def lt_def, blast)

lemma OUN_cong [cong]:
    "i=j;  x. x<j  C(x)=D(x)  (x<i. C(x)) = (x<j. D(x))"
by (simp add: OUnion_def lt_def OUN_iff)

lemma lt_induct:
    "i<k;  x.x<k;  y<x. P(y)  P(x)    P(i)"
apply (simp add: lt_def oall_def)
apply (erule conjE)
apply (erule Ord_induct, assumption, blast)
done


subsection ‹Quantification over a class›

definition
  "rall"     :: "[io, io]  o"  where
    "rall(M, P)  x. M(x)  P(x)"

definition
  "rex"      :: "[io, io]  o"  where
    "rex(M, P)  x. M(x)  P(x)"

syntax
  "_rall"     :: "[pttrn, io, o]  o"        ((3_[_]./ _) 10)
  "_rex"      :: "[pttrn, io, o]  o"        ((3_[_]./ _) 10)
translations
  "x[M]. P"  "CONST rall(M, λx. P)"
  "x[M]. P"  "CONST rex(M, λx. P)"


subsubsection‹Relativized universal quantifier›

lemma rallI [intro!]: "x. M(x)  P(x)  x[M]. P(x)"
by (simp add: rall_def)

lemma rspec: "x[M]. P(x); M(x)  P(x)"
by (simp add: rall_def)

(*Instantiates x first: better for automatic theorem proving?*)
lemma rev_rallE [elim]:
    "x[M]. P(x);  ¬ M(x)  Q;  P(x)  Q  Q"
by (simp add: rall_def, blast)

lemma rallE: "x[M]. P(x);  P(x)  Q;  ¬ M(x)  Q  Q"
by blast

(*Trival rewrite rule;   (∀x[M].P)<->P holds only if A is nonempty!*)
lemma rall_triv [simp]: "(x[M]. P)  ((x. M(x))  P)"
by (simp add: rall_def)

(*Congruence rule for rewriting*)
lemma rall_cong [cong]:
    "(x. M(x)  P(x) <-> P'(x))  (x[M]. P(x)) <-> (x[M]. P'(x))"
by (simp add: rall_def)


subsubsection‹Relativized existential quantifier›

lemma rexI [intro]: "P(x); M(x)  x[M]. P(x)"
by (simp add: rex_def, blast)

(*The best argument order when there is only one M(x)*)
lemma rev_rexI: "M(x);  P(x)  x[M]. P(x)"
by blast

(*Not of the general form for such rules... *)
lemma rexCI: "x[M]. ¬P(x)  P(a); M(a)  x[M]. P(x)"
by blast

lemma rexE [elim!]: "x[M]. P(x);  x. M(x); P(x)  Q  Q"
by (simp add: rex_def, blast)

(*We do not even have (∃x[M]. True) <-> True unless A is nonempty⋀*)
lemma rex_triv [simp]: "(x[M]. P)  ((x. M(x))  P)"
by (simp add: rex_def)

lemma rex_cong [cong]:
    "(x. M(x)  P(x) <-> P'(x))  (x[M]. P(x)) <-> (x[M]. P'(x))"
by (simp add: rex_def cong: conj_cong)

lemma rall_is_ball [simp]: "(x[λz. zA]. P(x)) <-> (xA. P(x))"
by blast

lemma rex_is_bex [simp]: "(x[λz. zA]. P(x)) <-> (xA. P(x))"
by blast

lemma atomize_rall: "(x. M(x)  P(x))  Trueprop (x[M]. P(x))"
by (simp add: rall_def atomize_all atomize_imp)

declare atomize_rall [symmetric, rulify]

lemma rall_simps1:
     "(x[M]. P(x)  Q)   <-> (x[M]. P(x))  ((x[M]. False) | Q)"
     "(x[M]. P(x) | Q)   <-> ((x[M]. P(x)) | Q)"
     "(x[M]. P(x)  Q) <-> ((x[M]. P(x))  Q)"
     "(¬(x[M]. P(x))) <-> (x[M]. ¬P(x))"
by blast+

lemma rall_simps2:
     "(x[M]. P  Q(x))   <-> ((x[M]. False) | P)  (x[M]. Q(x))"
     "(x[M]. P | Q(x))   <-> (P | (x[M]. Q(x)))"
     "(x[M]. P  Q(x)) <-> (P  (x[M]. Q(x)))"
by blast+

lemmas rall_simps [simp] = rall_simps1 rall_simps2

lemma rall_conj_distrib:
    "(x[M]. P(x)  Q(x)) <-> ((x[M]. P(x))  (x[M]. Q(x)))"
by blast

lemma rex_simps1:
     "(x[M]. P(x)  Q) <-> ((x[M]. P(x))  Q)"
     "(x[M]. P(x) | Q) <-> (x[M]. P(x)) | ((x[M]. True)  Q)"
     "(x[M]. P(x)  Q) <-> ((x[M]. P(x))  ((x[M]. True)  Q))"
     "(¬(x[M]. P(x))) <-> (x[M]. ¬P(x))"
by blast+

lemma rex_simps2:
     "(x[M]. P  Q(x)) <-> (P  (x[M]. Q(x)))"
     "(x[M]. P | Q(x)) <-> ((x[M]. True)  P) | (x[M]. Q(x))"
     "(x[M]. P  Q(x)) <-> (((x[M]. False) | P)  (x[M]. Q(x)))"
by blast+

lemmas rex_simps [simp] = rex_simps1 rex_simps2

lemma rex_disj_distrib:
    "(x[M]. P(x) | Q(x)) <-> ((x[M]. P(x)) | (x[M]. Q(x)))"
by blast


subsubsection‹One-point rule for bounded quantifiers›

lemma rex_triv_one_point1 [simp]: "(x[M]. x=a) <-> ( M(a))"
by blast

lemma rex_triv_one_point2 [simp]: "(x[M]. a=x) <-> ( M(a))"
by blast

lemma rex_one_point1 [simp]: "(x[M]. x=a  P(x)) <-> ( M(a)  P(a))"
by blast

lemma rex_one_point2 [simp]: "(x[M]. a=x  P(x)) <-> ( M(a)  P(a))"
by blast

lemma rall_one_point1 [simp]: "(x[M]. x=a  P(x)) <-> ( M(a)  P(a))"
by blast

lemma rall_one_point2 [simp]: "(x[M]. a=x  P(x)) <-> ( M(a)  P(a))"
by blast


subsubsection‹Sets as Classes›

definition
  setclass :: "[i,i]  o"       (##_› [40] 40)  where
   "setclass(A)  λx. x  A"

lemma setclass_iff [simp]: "setclass(A,x) <-> x  A"
by (simp add: setclass_def)

lemma rall_setclass_is_ball [simp]: "(x[##A]. P(x)) <-> (xA. P(x))"
by auto

lemma rex_setclass_is_bex [simp]: "(x[##A]. P(x)) <-> (xA. P(x))"
by auto


ML
val Ord_atomize =
  atomize ([(const_nameoall, @{thms ospec}), (const_namerall, @{thms rspec})] @
    ZF_conn_pairs, ZF_mem_pairs);
declaration fn _ =>
  Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt =>
    map mk_eq o Ord_atomize o Variable.gen_all ctxt))

text ‹Setting up the one-point-rule simproc›

simproc_setup defined_rex ("x[M]. P(x)  Q(x)") = K (Quantifier1.rearrange_Bex (fn ctxt => unfold_tac ctxt @{thms rex_def}))

simproc_setup defined_rall ("x[M]. P(x)  Q(x)") = K (Quantifier1.rearrange_Ball (fn ctxt => unfold_tac ctxt @{thms rall_def}))

end