src/HOL/Set.thy
author oheimb
Tue Apr 23 16:58:21 1996 +0200 (1996-04-23)
changeset 1672 2c109cd2fdd0
parent 1531 e5eb247ad13c
child 1674 33aff4d854e4
permissions -rw-r--r--
repaired critical proofs depending on the order inside non-confluent SimpSets,
(temporarily) removed problematic rule less_Suc_eq form simpset_of "Nat"
     1 (*  Title:      HOL/Set.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1993  University of Cambridge
     5 *)
     6 
     7 Set = Ord +
     8 
     9 types
    10   'a set
    11 
    12 arities
    13   set :: (term) term
    14 
    15 instance
    16   set :: (term) {ord, minus}
    17 
    18 consts
    19   "{}"          :: 'a set                           ("{}")
    20   insert        :: ['a, 'a set] => 'a set
    21   Collect       :: ('a => bool) => 'a set               (*comprehension*)
    22   Compl         :: ('a set) => 'a set                   (*complement*)
    23   Int           :: ['a set, 'a set] => 'a set       (infixl 70)
    24   Un            :: ['a set, 'a set] => 'a set       (infixl 65)
    25   UNION, INTER  :: ['a set, 'a => 'b set] => 'b set     (*general*)
    26   UNION1        :: ['a => 'b set] => 'b set         (binder "UN " 10)
    27   INTER1        :: ['a => 'b set] => 'b set         (binder "INT " 10)
    28   Union, Inter  :: (('a set)set) => 'a set              (*of a set*)
    29   Pow           :: 'a set => 'a set set                 (*powerset*)
    30   range         :: ('a => 'b) => 'b set                 (*of function*)
    31   Ball, Bex     :: ['a set, 'a => bool] => bool         (*bounded quantifiers*)
    32   inj, surj     :: ('a => 'b) => bool                   (*inj/surjective*)
    33   inj_onto      :: ['a => 'b, 'a set] => bool
    34   "``"          :: ['a => 'b, 'a set] => ('b set)   (infixl 90)
    35   ":"           :: ['a, 'a set] => bool             (infixl 50) (*membership*)
    36 
    37 
    38 syntax
    39 
    40   UNIV         :: 'a set
    41 
    42   "~:"          :: ['a, 'a set] => bool             (infixl 50)
    43 
    44   "@Finset"     :: args => 'a set                   ("{(_)}")
    45 
    46   "@Coll"       :: [pttrn, bool] => 'a set          ("(1{_./ _})")
    47   "@SetCompr"   :: ['a, idts, bool] => 'a set       ("(1{_ |/_./ _})")
    48 
    49   (* Big Intersection / Union *)
    50 
    51   "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3INT _:_./ _)" 10)
    52   "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3UN _:_./ _)" 10)
    53 
    54   (* Bounded Quantifiers *)
    55 
    56   "@Ball"       :: [pttrn, 'a set, bool] => bool      ("(3! _:_./ _)" 10)
    57   "@Bex"        :: [pttrn, 'a set, bool] => bool      ("(3? _:_./ _)" 10)
    58   "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3ALL _:_./ _)" 10)
    59   "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" 10)
    60 
    61 translations
    62   "UNIV"        == "Compl {}"
    63   "x ~: y"      == "~ (x : y)"
    64   "{x, xs}"     == "insert x {xs}"
    65   "{x}"         == "insert x {}"
    66   "{x. P}"      == "Collect (%x. P)"
    67   "INT x:A. B"  == "INTER A (%x. B)"
    68   "UN x:A. B"   == "UNION A (%x. B)"
    69   "! x:A. P"    == "Ball A (%x. P)"
    70   "? x:A. P"    == "Bex A (%x. P)"
    71   "ALL x:A. P"  => "Ball A (%x. P)"
    72   "EX x:A. P"   => "Bex A (%x. P)"
    73 
    74 
    75 rules
    76 
    77   (* Isomorphisms between Predicates and Sets *)
    78 
    79   mem_Collect_eq    "(a : {x.P(x)}) = P(a)"
    80   Collect_mem_eq    "{x.x:A} = A"
    81 
    82 
    83 defs
    84   Ball_def      "Ball A P       == ! x. x:A --> P(x)"
    85   Bex_def       "Bex A P        == ? x. x:A & P(x)"
    86   subset_def    "A <= B         == ! x:A. x:B"
    87   Compl_def     "Compl(A)       == {x. ~x:A}"
    88   Un_def        "A Un B         == {x.x:A | x:B}"
    89   Int_def       "A Int B        == {x.x:A & x:B}"
    90   set_diff_def  "A - B          == {x. x:A & ~x:B}"
    91   INTER_def     "INTER A B      == {y. ! x:A. y: B(x)}"
    92   UNION_def     "UNION A B      == {y. ? x:A. y: B(x)}"
    93   INTER1_def    "INTER1(B)      == INTER {x.True} B"
    94   UNION1_def    "UNION1(B)      == UNION {x.True} B"
    95   Inter_def     "Inter(S)       == (INT x:S. x)"
    96   Union_def     "Union(S)       == (UN x:S. x)"
    97   Pow_def       "Pow(A)         == {B. B <= A}"
    98   empty_def     "{}             == {x. False}"
    99   insert_def    "insert a B     == {x.x=a} Un B"
   100   range_def     "range(f)       == {y. ? x. y=f(x)}"
   101   image_def     "f``A           == {y. ? x:A. y=f(x)}"
   102   inj_def       "inj(f)         == ! x y. f(x)=f(y) --> x=y"
   103   inj_onto_def  "inj_onto f A   == ! x:A. ! y:A. f(x)=f(y) --> x=y"
   104   surj_def      "surj(f)        == ! y. ? x. y=f(x)"
   105 
   106 (* start 8bit 1 *)
   107 syntax
   108   ""		:: "['a set, 'a set] => 'a set"       (infixl 70)
   109   ""		:: "['a set, 'a set] => 'a set"       (infixl 65)
   110   ""		:: "['a, 'a set] => bool"             (infixl 50)
   111   ""		:: "['a, 'a set] => bool"             (infixl 50)
   112   GUnion	:: "(('a set)set) => 'a set"          ("_" [90] 90)
   113   GInter	:: "(('a set)set) => 'a set"          ("_" [90] 90)
   114   GUNION1       :: "['a => 'b set] => 'b set"         (binder " " 10)
   115   GINTER1       :: "['a => 'b set] => 'b set"         (binder " " 10)
   116   GINTER	:: "[pttrn, 'a set, 'b set] => 'b set"  ("(3 __./ _)" 10)
   117   GUNION	:: "[pttrn, 'a set, 'b set] => 'b set"  ("(3 __./ _)" 10)
   118   GBall		:: "[pttrn, 'a set, bool] => bool"      ("(3 __./ _)" 10)
   119   GBex		:: "[pttrn, 'a set, bool] => bool"      ("(3 __./ _)" 10)
   120 
   121 translations
   122   "x  y"      == "(x : y)"
   123   "x  y"      == "(x : y)"
   124   "x  y"      == "x Int y"
   125   "x  y"      == "x Un  y"
   126   "X"        == "Inter X" 
   127   "X"        == "Union X"
   128   "x.A"      == "INT x.A"
   129   "x.A"      == "UN x.A"
   130   "xA. B"   == "INT x:A. B"
   131   "xA. B"   == "UN x:A. B"
   132   "xA. P"    == "! x:A. P"
   133   "xA. P"    == "? x:A. P"
   134 (* end 8bit 1 *)
   135 
   136 end
   137 
   138 ML
   139 
   140 local
   141 
   142 (* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P}      *)
   143 (* {y. ? x1..xn. y = e & P} is only translated if [0..n] subset bvs(e) *)
   144 
   145 val ex_tr = snd(mk_binder_tr("? ","Ex"));
   146 
   147 fun nvars(Const("_idts",_) $ _ $ idts) = nvars(idts)+1
   148   | nvars(_) = 1;
   149 
   150 fun setcompr_tr[e,idts,b] =
   151   let val eq = Syntax.const("op =") $ Bound(nvars(idts)) $ e
   152       val P = Syntax.const("op &") $ eq $ b
   153       val exP = ex_tr [idts,P]
   154   in Syntax.const("Collect") $ Abs("",dummyT,exP) end;
   155 
   156 val ex_tr' = snd(mk_binder_tr' ("Ex","DUMMY"));
   157 
   158 fun setcompr_tr'[Abs(_,_,P)] =
   159   let fun ok(Const("Ex",_)$Abs(_,_,P),n) = ok(P,n+1)
   160         | ok(Const("op &",_) $ (Const("op =",_) $ Bound(m) $ e) $ _, n) =
   161             if n>0 andalso m=n andalso
   162               ((0 upto (n-1)) subset add_loose_bnos(e,0,[]))
   163             then () else raise Match
   164 
   165       fun tr'(_ $ abs) =
   166         let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr'[abs]
   167         in Syntax.const("@SetCompr") $ e $ idts $ Q end
   168   in ok(P,0); tr'(P) end;
   169 
   170 in
   171 
   172 val parse_translation = [("@SetCompr", setcompr_tr)];
   173 val print_translation = [("Collect", setcompr_tr')];
   174 val print_ast_translation =
   175   map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];
   176 
   177 end;
   178