src/HOL/Set.thy
changeset 923 ff1574a81019
child 1068 e0f2dffab506
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Set.thy	Fri Mar 03 12:02:25 1995 +0100
     1.3 @@ -0,0 +1,145 @@
     1.4 +(*  Title:      HOL/Set.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +*)
     1.9 +
    1.10 +Set = Ord +
    1.11 +
    1.12 +types
    1.13 +  'a set
    1.14 +
    1.15 +arities
    1.16 +  set :: (term) term
    1.17 +
    1.18 +instance
    1.19 +  set :: (term) {ord, minus}
    1.20 +
    1.21 +consts
    1.22 +  "{}"          :: "'a set"                           ("{}")
    1.23 +  insert        :: "['a, 'a set] => 'a set"
    1.24 +  Collect       :: "('a => bool) => 'a set"               (*comprehension*)
    1.25 +  Compl         :: "('a set) => 'a set"                   (*complement*)
    1.26 +  Int           :: "['a set, 'a set] => 'a set"       (infixl 70)
    1.27 +  Un            :: "['a set, 'a set] => 'a set"       (infixl 65)
    1.28 +  UNION, INTER  :: "['a set, 'a => 'b set] => 'b set"     (*general*)
    1.29 +  UNION1        :: "['a => 'b set] => 'b set"         (binder "UN " 10)
    1.30 +  INTER1        :: "['a => 'b set] => 'b set"         (binder "INT " 10)
    1.31 +  Union, Inter  :: "(('a set)set) => 'a set"              (*of a set*)
    1.32 +  Pow           :: "'a set => 'a set set"                 (*powerset*)
    1.33 +  range         :: "('a => 'b) => 'b set"                 (*of function*)
    1.34 +  Ball, Bex     :: "['a set, 'a => bool] => bool"         (*bounded quantifiers*)
    1.35 +  inj, surj     :: "('a => 'b) => bool"                   (*inj/surjective*)
    1.36 +  inj_onto      :: "['a => 'b, 'a set] => bool"
    1.37 +  "``"          :: "['a => 'b, 'a set] => ('b set)"   (infixl 90)
    1.38 +  ":"           :: "['a, 'a set] => bool"             (infixl 50) (*membership*)
    1.39 +
    1.40 +
    1.41 +syntax
    1.42 +
    1.43 +  "~:"          :: "['a, 'a set] => bool"             (infixl 50)
    1.44 +
    1.45 +  "@Finset"     :: "args => 'a set"                   ("{(_)}")
    1.46 +
    1.47 +  "@Coll"       :: "[idt, bool] => 'a set"            ("(1{_./ _})")
    1.48 +  "@SetCompr"   :: "['a, idts, bool] => 'a set"       ("(1{_ |/_./ _})")
    1.49 +
    1.50 +  (* Big Intersection / Union *)
    1.51 +
    1.52 +  "@INTER"      :: "[idt, 'a set, 'b set] => 'b set"  ("(3INT _:_./ _)" 10)
    1.53 +  "@UNION"      :: "[idt, 'a set, 'b set] => 'b set"  ("(3UN _:_./ _)" 10)
    1.54 +
    1.55 +  (* Bounded Quantifiers *)
    1.56 +
    1.57 +  "@Ball"       :: "[idt, 'a set, bool] => bool"      ("(3! _:_./ _)" 10)
    1.58 +  "@Bex"        :: "[idt, 'a set, bool] => bool"      ("(3? _:_./ _)" 10)
    1.59 +  "*Ball"       :: "[idt, 'a set, bool] => bool"      ("(3ALL _:_./ _)" 10)
    1.60 +  "*Bex"        :: "[idt, 'a set, bool] => bool"      ("(3EX _:_./ _)" 10)
    1.61 +
    1.62 +translations
    1.63 +  "x ~: y"      == "~ (x : y)"
    1.64 +  "{x, xs}"     == "insert x {xs}"
    1.65 +  "{x}"         == "insert x {}"
    1.66 +  "{x. P}"      == "Collect (%x. P)"
    1.67 +  "INT x:A. B"  == "INTER A (%x. B)"
    1.68 +  "UN x:A. B"   == "UNION A (%x. B)"
    1.69 +  "! x:A. P"    == "Ball A (%x. P)"
    1.70 +  "? x:A. P"    == "Bex A (%x. P)"
    1.71 +  "ALL x:A. P"  => "Ball A (%x. P)"
    1.72 +  "EX x:A. P"   => "Bex A (%x. P)"
    1.73 +
    1.74 +
    1.75 +rules
    1.76 +
    1.77 +  (* Isomorphisms between Predicates and Sets *)
    1.78 +
    1.79 +  mem_Collect_eq    "(a : {x.P(x)}) = P(a)"
    1.80 +  Collect_mem_eq    "{x.x:A} = A"
    1.81 +
    1.82 +
    1.83 +defs
    1.84 +  Ball_def      "Ball A P       == ! x. x:A --> P(x)"
    1.85 +  Bex_def       "Bex A P        == ? x. x:A & P(x)"
    1.86 +  subset_def    "A <= B         == ! x:A. x:B"
    1.87 +  Compl_def     "Compl(A)       == {x. ~x:A}"
    1.88 +  Un_def        "A Un B         == {x.x:A | x:B}"
    1.89 +  Int_def       "A Int B        == {x.x:A & x:B}"
    1.90 +  set_diff_def  "A - B          == {x. x:A & ~x:B}"
    1.91 +  INTER_def     "INTER A B      == {y. ! x:A. y: B(x)}"
    1.92 +  UNION_def     "UNION A B      == {y. ? x:A. y: B(x)}"
    1.93 +  INTER1_def    "INTER1(B)      == INTER {x.True} B"
    1.94 +  UNION1_def    "UNION1(B)      == UNION {x.True} B"
    1.95 +  Inter_def     "Inter(S)       == (INT x:S. x)"
    1.96 +  Union_def     "Union(S)       == (UN x:S. x)"
    1.97 +  Pow_def       "Pow(A)         == {B. B <= A}"
    1.98 +  empty_def     "{}             == {x. False}"
    1.99 +  insert_def    "insert a B     == {x.x=a} Un B"
   1.100 +  range_def     "range(f)       == {y. ? x. y=f(x)}"
   1.101 +  image_def     "f``A           == {y. ? x:A. y=f(x)}"
   1.102 +  inj_def       "inj(f)         == ! x y. f(x)=f(y) --> x=y"
   1.103 +  inj_onto_def  "inj_onto f A   == ! x:A. ! y:A. f(x)=f(y) --> x=y"
   1.104 +  surj_def      "surj(f)        == ! y. ? x. y=f(x)"
   1.105 +
   1.106 +end
   1.107 +
   1.108 +ML
   1.109 +
   1.110 +local
   1.111 +
   1.112 +(* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P}      *)
   1.113 +(* {y. ? x1..xn. y = e & P} is only translated if [0..n] subset bvs(e) *)
   1.114 +
   1.115 +val ex_tr = snd(mk_binder_tr("? ","Ex"));
   1.116 +
   1.117 +fun nvars(Const("_idts",_) $ _ $ idts) = nvars(idts)+1
   1.118 +  | nvars(_) = 1;
   1.119 +
   1.120 +fun setcompr_tr[e,idts,b] =
   1.121 +  let val eq = Syntax.const("op =") $ Bound(nvars(idts)) $ e
   1.122 +      val P = Syntax.const("op &") $ eq $ b
   1.123 +      val exP = ex_tr [idts,P]
   1.124 +  in Syntax.const("Collect") $ Abs("",dummyT,exP) end;
   1.125 +
   1.126 +val ex_tr' = snd(mk_binder_tr' ("Ex","DUMMY"));
   1.127 +
   1.128 +fun setcompr_tr'[Abs(_,_,P)] =
   1.129 +  let fun ok(Const("Ex",_)$Abs(_,_,P),n) = ok(P,n+1)
   1.130 +        | ok(Const("op &",_) $ (Const("op =",_) $ Bound(m) $ e) $ _, n) =
   1.131 +            if n>0 andalso m=n andalso
   1.132 +              ((0 upto (n-1)) subset add_loose_bnos(e,0,[]))
   1.133 +            then () else raise Match
   1.134 +
   1.135 +      fun tr'(_ $ abs) =
   1.136 +        let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr'[abs]
   1.137 +        in Syntax.const("@SetCompr") $ e $ idts $ Q end
   1.138 +  in ok(P,0); tr'(P) end;
   1.139 +
   1.140 +in
   1.141 +
   1.142 +val parse_translation = [("@SetCompr", setcompr_tr)];
   1.143 +val print_translation = [("Collect", setcompr_tr')];
   1.144 +val print_ast_translation =
   1.145 +  map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];
   1.146 +
   1.147 +end;
   1.148 +