src/CCL/Set.thy
changeset 0 a5a9c433f639
child 278 523518f44286
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/CCL/Set.thy	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,71 @@
     1.4 +(*  Title:      CCL/set.thy
     1.5 +    ID:         $Id$
     1.6 +
     1.7 +Modified version of HOL/set.thy that extends FOL
     1.8 +
     1.9 +*)
    1.10 +
    1.11 +Set = FOL +
    1.12 +
    1.13 +types
    1.14 +  set 1
    1.15 +
    1.16 +arities
    1.17 +  set :: (term) term
    1.18 +
    1.19 +consts
    1.20 +  Collect       :: "['a => o] => 'a set"                    (*comprehension*)
    1.21 +  Compl         :: "('a set) => 'a set"                     (*complement*)
    1.22 +  Int           :: "['a set, 'a set] => 'a set"         (infixl 70)
    1.23 +  Un            :: "['a set, 'a set] => 'a set"         (infixl 65)
    1.24 +  Union, Inter  :: "(('a set)set) => 'a set"                (*...of a set*)
    1.25 +  UNION, INTER  :: "['a set, 'a => 'b set] => 'b set"       (*general*)
    1.26 +  Ball, Bex     :: "['a set, 'a => o] => o"                 (*bounded quants*)
    1.27 +  mono          :: "['a set => 'b set] => o"                (*monotonicity*)
    1.28 +  ":"           :: "['a, 'a set] => o"                  (infixl 50) (*membership*)
    1.29 +  "<="          :: "['a set, 'a set] => o"              (infixl 50)
    1.30 +  singleton     :: "'a => 'a set"                       ("{_}")
    1.31 +  empty         :: "'a set"                             ("{}")
    1.32 +  "oo"          :: "['b => 'c, 'a => 'b, 'a] => 'c"     (infixr 50) (*composition*)
    1.33 +
    1.34 +  "@Coll"       :: "[idt, o] => 'a set"                 ("(1{_./ _})") (*collection*)
    1.35 +
    1.36 +  (* Big Intersection / Union *)
    1.37 +
    1.38 +  "@INTER"      :: "[idt, 'a set, 'b set] => 'b set"    ("(INT _:_./ _)" [0, 0, 0] 10)
    1.39 +  "@UNION"      :: "[idt, 'a set, 'b set] => 'b set"    ("(UN _:_./ _)" [0, 0, 0] 10)
    1.40 +
    1.41 +  (* Bounded Quantifiers *)
    1.42 +
    1.43 +  "@Ball"       :: "[idt, 'a set, o] => o"              ("(ALL _:_./ _)" [0, 0, 0] 10)
    1.44 +  "@Bex"        :: "[idt, 'a set, o] => o"              ("(EX _:_./ _)" [0, 0, 0] 10)
    1.45 +
    1.46 +
    1.47 +translations
    1.48 +  "{x. P}"      == "Collect(%x. P)"
    1.49 +  "INT x:A. B"  == "INTER(A, %x. B)"
    1.50 +  "UN x:A. B"   == "UNION(A, %x. B)"
    1.51 +  "ALL x:A. P"  == "Ball(A, %x. P)"
    1.52 +  "EX x:A. P"   == "Bex(A, %x. P)"
    1.53 +
    1.54 +
    1.55 +rules
    1.56 +  mem_Collect_iff       "(a : {x.P(x)}) <-> P(a)"
    1.57 +  set_extension         "A=B <-> (ALL x.x:A <-> x:B)"
    1.58 +
    1.59 +  Ball_def      "Ball(A, P)  == ALL x. x:A --> P(x)"
    1.60 +  Bex_def       "Bex(A, P)   == EX x. x:A & P(x)"
    1.61 +  mono_def      "mono(f)     == (ALL A B. A <= B --> f(A) <= f(B))"
    1.62 +  subset_def    "A <= B      == ALL x:A. x:B"
    1.63 +  singleton_def "{a}         == {x.x=a}"
    1.64 +  empty_def     "{}          == {x.False}"
    1.65 +  Un_def        "A Un B      == {x.x:A | x:B}"
    1.66 +  Int_def       "A Int B     == {x.x:A & x:B}"
    1.67 +  Compl_def     "Compl(A)    == {x. ~x:A}"
    1.68 +  INTER_def     "INTER(A, B) == {y. ALL x:A. y: B(x)}"
    1.69 +  UNION_def     "UNION(A, B) == {y. EX x:A. y: B(x)}"
    1.70 +  Inter_def     "Inter(S)    == (INT x:S. x)"
    1.71 +  Union_def     "Union(S)    == (UN x:S. x)"
    1.72 +
    1.73 +end
    1.74 +