src/CCL/Set.thy
author wenzelm
Mon Oct 20 10:48:22 1997 +0200 (1997-10-20)
changeset 3935 52c14fe8f16b
parent 3837 d7f033c74b38
child 17456 bcf7544875b2
permissions -rw-r--r--
adapted to qualified names;
clasohm@0
     1
(*  Title:      CCL/set.thy
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
clasohm@0
     4
Modified version of HOL/set.thy that extends FOL
clasohm@0
     5
clasohm@0
     6
*)
clasohm@0
     7
clasohm@0
     8
Set = FOL +
clasohm@0
     9
wenzelm@3935
    10
global
wenzelm@3935
    11
clasohm@0
    12
types
clasohm@278
    13
  'a set
clasohm@0
    14
clasohm@0
    15
arities
clasohm@0
    16
  set :: (term) term
clasohm@0
    17
clasohm@0
    18
consts
clasohm@0
    19
  Collect       :: "['a => o] => 'a set"                    (*comprehension*)
clasohm@0
    20
  Compl         :: "('a set) => 'a set"                     (*complement*)
clasohm@0
    21
  Int           :: "['a set, 'a set] => 'a set"         (infixl 70)
clasohm@0
    22
  Un            :: "['a set, 'a set] => 'a set"         (infixl 65)
clasohm@0
    23
  Union, Inter  :: "(('a set)set) => 'a set"                (*...of a set*)
clasohm@0
    24
  UNION, INTER  :: "['a set, 'a => 'b set] => 'b set"       (*general*)
clasohm@0
    25
  Ball, Bex     :: "['a set, 'a => o] => o"                 (*bounded quants*)
clasohm@0
    26
  mono          :: "['a set => 'b set] => o"                (*monotonicity*)
clasohm@0
    27
  ":"           :: "['a, 'a set] => o"                  (infixl 50) (*membership*)
clasohm@0
    28
  "<="          :: "['a set, 'a set] => o"              (infixl 50)
clasohm@0
    29
  singleton     :: "'a => 'a set"                       ("{_}")
clasohm@0
    30
  empty         :: "'a set"                             ("{}")
clasohm@0
    31
  "oo"          :: "['b => 'c, 'a => 'b, 'a] => 'c"     (infixr 50) (*composition*)
clasohm@0
    32
wenzelm@3935
    33
syntax
clasohm@0
    34
  "@Coll"       :: "[idt, o] => 'a set"                 ("(1{_./ _})") (*collection*)
clasohm@0
    35
clasohm@0
    36
  (* Big Intersection / Union *)
clasohm@0
    37
clasohm@0
    38
  "@INTER"      :: "[idt, 'a set, 'b set] => 'b set"    ("(INT _:_./ _)" [0, 0, 0] 10)
clasohm@0
    39
  "@UNION"      :: "[idt, 'a set, 'b set] => 'b set"    ("(UN _:_./ _)" [0, 0, 0] 10)
clasohm@0
    40
clasohm@0
    41
  (* Bounded Quantifiers *)
clasohm@0
    42
clasohm@0
    43
  "@Ball"       :: "[idt, 'a set, o] => o"              ("(ALL _:_./ _)" [0, 0, 0] 10)
clasohm@0
    44
  "@Bex"        :: "[idt, 'a set, o] => o"              ("(EX _:_./ _)" [0, 0, 0] 10)
clasohm@0
    45
clasohm@0
    46
clasohm@0
    47
translations
clasohm@0
    48
  "{x. P}"      == "Collect(%x. P)"
clasohm@0
    49
  "INT x:A. B"  == "INTER(A, %x. B)"
clasohm@0
    50
  "UN x:A. B"   == "UNION(A, %x. B)"
clasohm@0
    51
  "ALL x:A. P"  == "Ball(A, %x. P)"
clasohm@0
    52
  "EX x:A. P"   == "Bex(A, %x. P)"
clasohm@0
    53
wenzelm@3935
    54
local
clasohm@0
    55
clasohm@0
    56
rules
wenzelm@3837
    57
  mem_Collect_iff       "(a : {x. P(x)}) <-> P(a)"
wenzelm@3837
    58
  set_extension         "A=B <-> (ALL x. x:A <-> x:B)"
clasohm@0
    59
clasohm@0
    60
  Ball_def      "Ball(A, P)  == ALL x. x:A --> P(x)"
clasohm@0
    61
  Bex_def       "Bex(A, P)   == EX x. x:A & P(x)"
clasohm@0
    62
  mono_def      "mono(f)     == (ALL A B. A <= B --> f(A) <= f(B))"
clasohm@0
    63
  subset_def    "A <= B      == ALL x:A. x:B"
wenzelm@3837
    64
  singleton_def "{a}         == {x. x=a}"
wenzelm@3837
    65
  empty_def     "{}          == {x. False}"
wenzelm@3837
    66
  Un_def        "A Un B      == {x. x:A | x:B}"
wenzelm@3837
    67
  Int_def       "A Int B     == {x. x:A & x:B}"
clasohm@0
    68
  Compl_def     "Compl(A)    == {x. ~x:A}"
clasohm@0
    69
  INTER_def     "INTER(A, B) == {y. ALL x:A. y: B(x)}"
clasohm@0
    70
  UNION_def     "UNION(A, B) == {y. EX x:A. y: B(x)}"
clasohm@0
    71
  Inter_def     "Inter(S)    == (INT x:S. x)"
clasohm@0
    72
  Union_def     "Union(S)    == (UN x:S. x)"
clasohm@0
    73
clasohm@0
    74
end
clasohm@0
    75