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