# Theory Set

Up to index of Isabelle/CCL

theory Set
imports FOL
uses [Set.ML]
begin

    (*  Title:      CCL/Set.thy
        ID:         $Id: Set.thy,v 1.5 2005/09/17 15:35:28 wenzelm Exp $
    *)

    header {* Extending FOL by a modified version of HOL set theory *}

    theory Set
    imports FOL
    begin

    global

    typedecl 'a set
    arities set :: ("term") "term"

    consts
      Collect       :: "['a => o] => 'a set"                    (*comprehension*)
      Compl         :: "('a set) => 'a set"                     (*complement*)
      Int           :: "['a set, 'a set] => 'a set"         (infixl 70)
      Un            :: "['a set, 'a set] => 'a set"         (infixl 65)
      Union         :: "(('a set)set) => 'a set"                (*...of a set*)
      Inter         :: "(('a set)set) => 'a set"                (*...of a set*)
      UNION         :: "['a set, 'a => 'b set] => 'b set"       (*general*)
      INTER         :: "['a set, 'a => 'b set] => 'b set"       (*general*)
      Ball          :: "['a set, 'a => o] => o"                 (*bounded quants*)
      Bex           :: "['a set, 'a => o] => o"                 (*bounded quants*)
      mono          :: "['a set => 'b set] => o"                (*monotonicity*)
      ":"           :: "['a, 'a set] => o"                  (infixl 50) (*membership*)
      "<="          :: "['a set, 'a set] => o"              (infixl 50)
      singleton     :: "'a => 'a set"                       ("{_}")
      empty         :: "'a set"                             ("{}")
      "oo"          :: "['b => 'c, 'a => 'b, 'a] => 'c"     (infixr 50) (*composition*)

    syntax
      "@Coll"       :: "[idt, o] => 'a set"                 ("(1{_./ _})") (*collection*)

      (* Big Intersection / Union *)

      "@INTER"      :: "[idt, 'a set, 'b set] => 'b set"    ("(INT _:_./ _)" [0, 0, 0] 10)
      "@UNION"      :: "[idt, 'a set, 'b set] => 'b set"    ("(UN _:_./ _)" [0, 0, 0] 10)

      (* Bounded Quantifiers *)

      "@Ball"       :: "[idt, 'a set, o] => o"              ("(ALL _:_./ _)" [0, 0, 0] 10)
      "@Bex"        :: "[idt, 'a set, o] => o"              ("(EX _:_./ _)" [0, 0, 0] 10)

    translations
      "{x. P}"      == "Collect(%x. P)"
      "INT x:A. B"  == "INTER(A, %x. B)"
      "UN x:A. B"   == "UNION(A, %x. B)"
      "ALL x:A. P"  == "Ball(A, %x. P)"
      "EX x:A. P"   == "Bex(A, %x. P)"

    local

    axioms
      mem_Collect_iff:       "(a : {x. P(x)}) <-> P(a)"
      set_extension:         "A=B <-> (ALL x. x:A <-> x:B)"

    defs
      Ball_def:      "Ball(A, P)  == ALL x. x:A --> P(x)"
      Bex_def:       "Bex(A, P)   == EX x. x:A & P(x)"
      mono_def:      "mono(f)     == (ALL A B. A <= B --> f(A) <= f(B))"
      subset_def:    "A <= B      == ALL x:A. x:B"
      singleton_def: "{a}         == {x. x=a}"
      empty_def:     "{}          == {x. False}"
      Un_def:        "A Un B      == {x. x:A | x:B}"
      Int_def:       "A Int B     == {x. x:A & x:B}"
      Compl_def:     "Compl(A)    == {x. ~x:A}"
      INTER_def:     "INTER(A, B) == {y. ALL x:A. y: B(x)}"
      UNION_def:     "UNION(A, B) == {y. EX x:A. y: B(x)}"
      Inter_def:     "Inter(S)    == (INT x:S. x)"
      Union_def:     "Union(S)    == (UN x:S. x)"

    ML {* use_legacy_bindings (the_context ()) *}

    end

theorem CollectI:

      P(a) ==> a : Collect(P)

theorem CollectD:

      a : Collect(P) ==> P(a)

theorem set_ext:

      (!!x. x : A <-> x : B) ==> A = B

theorem ballI:

      (!!x. x : A ==> P(x)) ==> Ball(A, P)

theorem bspec:

      [| Ball(A, P); x : A |] ==> P(x)

theorem ballE:

      [| Ball(A, P); P(x) ==> Q; ¬ x : A ==> Q |] ==> Q

theorem bexI:

      [| P(x); x : A |] ==> Bex(A, P)

theorem bexCI:

      [| EX x:A. ¬ P(x) ==> P(a); a : A |] ==> Bex(A, P)

theorem bexE:

      [| Bex(A, P); !!x. [| x : A; P(x) |] ==> Q |] ==> Q

theorem ball_rew:

      (ALL x:A. True) <-> True

theorem ball_cong:

      [| A = A'; !!x. x : A' ==> P(x) <-> P'(x) |] ==> Ball(A, P) <-> Ball(A', P')

theorem bex_cong:

      [| A = A'; !!x. x : A' ==> P(x) <-> P'(x) |] ==> Bex(A, P) <-> Bex(A', P')

theorem subsetI:

      (!!x. x : A ==> x : B) ==> A <= B

theorem subsetD:

      [| A <= B; c : A |] ==> c : B

theorem subsetCE:

      [| A <= B; ¬ c : A ==> P; c : B ==> P |] ==> P

theorem subset_refl:

      A <= A

theorem subset_trans:

      [| A <= B; B <= C |] ==> A <= C

theorem subset_antisym:

      [| A <= B; B <= A |] ==> A = B

theorem equalityD1:

      A = B ==> A <= B

theorem equalityD2:

      A = B ==> B <= A

theorem equalityE:

      [| A = B; [| A <= B; B <= A |] ==> P |] ==> P

theorem equalityCE:

      [| A = B; [| c : A; c : B |] ==> P; [| ¬ c : A; ¬ c : B |] ==> P |] ==> P

theorem setup_induction:

      [| p : A; !!z. z : A ==> p = z --> R |] ==> R

theorem trivial_set:

      {x. x : A} = A

theorem UnI1:

      c : A ==> c : A Un B

theorem UnI2:

      c : B ==> c : A Un B

theorem UnCI:

      (¬ c : B ==> c : A) ==> c : A Un B

theorem UnE:

      [| c : A Un B; c : A ==> P; c : B ==> P |] ==> P

theorem IntI:

      [| c : A; c : B |] ==> c : A Int B

theorem IntD1:

      c : A Int B ==> c : A

theorem IntD2:

      c : A Int B ==> c : B

theorem IntE:

      [| c : A Int B; [| c : A; c : B |] ==> P |] ==> P

theorem ComplI:

      (c : A ==> False) ==> c : Compl(A)

theorem ComplD:

      c : Compl(A) ==> ¬ c : A

theorem empty_eq:

      {x. False} = {}

theorem emptyD:

      a : {} ==> P

theorem not_emptyD:

      A ≠ {} ==> ∃x. x : A

theorem singletonI:

      a : {a}

theorem singletonD:

      b : {a} ==> b = a

theorem UN_I:

      [| a : A; b : B(a) |] ==> b : UNION(A, B)

theorem UN_E:

      [| b : UNION(A, B); !!x. [| x : A; b : B(x) |] ==> R |] ==> R

theorem UN_cong:

      [| A = B; !!x. x : B ==> C(x) = D(x) |] ==> UNION(A, C) = UNION(B, D)

theorem INT_I:

      (!!x. x : A ==> b : B(x)) ==> b : INTER(A, B)

theorem INT_D:

      [| b : INTER(A, B); a : A |] ==> b : B(a)

theorem INT_E:

      [| b : INTER(A, B); b : B(a) ==> R; ¬ a : A ==> R |] ==> R

theorem INT_cong:

      [| A = B; !!x. x : B ==> C(x) = D(x) |] ==> INTER(A, C) = INTER(B, D)

theorem UnionI:

      [| X : C; A : X |] ==> A : Union(C)

theorem UnionE:

      [| A : Union(C); !!X. [| A : X; X : C |] ==> R |] ==> R

theorem InterI:

      (!!X. X : C ==> A : X) ==> A : Inter(C)

theorem InterD:

      [| A : Inter(C); X : C |] ==> A : X

theorem InterE:

      [| A : Inter(C); A : X ==> R; ¬ X : C ==> R |] ==> R