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