clasohm@923: (*  Title:      HOL/Set.thy
clasohm@923:     ID:         $Id$
clasohm@923:     Author:     Tobias Nipkow
clasohm@923:     Copyright   1993  University of Cambridge
clasohm@923: *)
clasohm@923: 
clasohm@923: Set = Ord +
clasohm@923: 
wenzelm@2261: 
wenzelm@2261: (** Core syntax **)
wenzelm@2261: 
wenzelm@3947: global
wenzelm@3947: 
clasohm@923: types
clasohm@923:   'a set
clasohm@923: 
clasohm@923: arities
clasohm@923:   set :: (term) term
clasohm@923: 
clasohm@923: instance
oheimb@4761:   set :: (term) {ord, minus, power} (* only ('a * 'a) set should be in power! *)
clasohm@923: 
wenzelm@3820: syntax
wenzelm@3820:   "op :"        :: ['a, 'a set] => bool             ("op :")
wenzelm@3820: 
clasohm@923: consts
clasohm@1370:   "{}"          :: 'a set                           ("{}")
paulson@4159:   UNIV          :: 'a set
clasohm@1370:   insert        :: ['a, 'a set] => 'a set
clasohm@1370:   Collect       :: ('a => bool) => 'a set               (*comprehension*)
clasohm@1370:   Int           :: ['a set, 'a set] => 'a set       (infixl 70)
clasohm@1370:   Un            :: ['a set, 'a set] => 'a set       (infixl 65)
clasohm@1370:   UNION, INTER  :: ['a set, 'a => 'b set] => 'b set     (*general*)
wenzelm@2261:   Union, Inter  :: (('a set) set) => 'a set             (*of a set*)
clasohm@1370:   Pow           :: 'a set => 'a set set                 (*powerset*)
clasohm@1370:   range         :: ('a => 'b) => 'b set                 (*of function*)
clasohm@1370:   Ball, Bex     :: ['a set, 'a => bool] => bool         (*bounded quantifiers*)
paulson@1962:   "``"          :: ['a => 'b, 'a set] => ('b set)   (infixr 90)
wenzelm@2261:   (*membership*)
wenzelm@2261:   "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50, 51] 50)
clasohm@923: 
clasohm@923: 
paulson@5492: (*For compatibility: DELETE after one release*)
paulson@5492: syntax Compl :: ('a set) => 'a set   (*complement*)
paulson@5492: translations "Compl A"  => "- A"
wenzelm@2261: 
wenzelm@2261: (** Additional concrete syntax **)
wenzelm@2261: 
clasohm@923: syntax
clasohm@923: 
paulson@5492: 
wenzelm@2261:   (* Infix syntax for non-membership *)
clasohm@923: 
wenzelm@3820:   "op ~:"       :: ['a, 'a set] => bool               ("op ~:")
wenzelm@2261:   "op ~:"       :: ['a, 'a set] => bool               ("(_/ ~: _)" [50, 51] 50)
clasohm@923: 
wenzelm@2261:   "@Finset"     :: args => 'a set                     ("{(_)}")
wenzelm@2261: 
wenzelm@2261:   "@Coll"       :: [pttrn, bool] => 'a set            ("(1{_./ _})")
wenzelm@2261:   "@SetCompr"   :: ['a, idts, bool] => 'a set         ("(1{_ |/_./ _})")
clasohm@923: 
clasohm@923:   (* Big Intersection / Union *)
clasohm@923: 
paulson@4159:   INTER1        :: [pttrns, 'a => 'b set] => 'b set   ("(3INT _./ _)" 10)
paulson@4159:   UNION1        :: [pttrns, 'a => 'b set] => 'b set   ("(3UN _./ _)" 10)
paulson@4159: 
clasohm@1370:   "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3INT _:_./ _)" 10)
clasohm@1370:   "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3UN _:_./ _)" 10)
clasohm@923: 
clasohm@923:   (* Bounded Quantifiers *)
clasohm@923: 
wenzelm@2368:   "@Ball"       :: [pttrn, 'a set, bool] => bool      ("(3! _:_./ _)" [0, 0, 10] 10)
wenzelm@2368:   "@Bex"        :: [pttrn, 'a set, bool] => bool      ("(3? _:_./ _)" [0, 0, 10] 10)
wenzelm@2368:   "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3ALL _:_./ _)" [0, 0, 10] 10)
wenzelm@2368:   "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" [0, 0, 10] 10)
clasohm@923: 
clasohm@923: translations
wenzelm@2261:   "range f"     == "f``UNIV"
clasohm@923:   "x ~: y"      == "~ (x : y)"
clasohm@923:   "{x, xs}"     == "insert x {xs}"
clasohm@923:   "{x}"         == "insert x {}"
clasohm@923:   "{x. P}"      == "Collect (%x. P)"
paulson@4159:   "UN x y. B"   == "UN x. UN y. B"
paulson@4159:   "UN x. B"     == "UNION UNIV (%x. B)"
paulson@4159:   "INT x y. B"   == "INT x. INT y. B"
paulson@4159:   "INT x. B"    == "INTER UNIV (%x. B)"
paulson@4159:   "UN x:A. B"   == "UNION A (%x. B)"
clasohm@923:   "INT x:A. B"  == "INTER A (%x. B)"
clasohm@923:   "! x:A. P"    == "Ball A (%x. P)"
clasohm@923:   "? x:A. P"    == "Bex A (%x. P)"
clasohm@923:   "ALL x:A. P"  => "Ball A (%x. P)"
clasohm@923:   "EX x:A. P"   => "Bex A (%x. P)"
clasohm@923: 
wenzelm@2388: syntax ("" output)
wenzelm@3820:   "_setle"      :: ['a set, 'a set] => bool           ("op <=")
wenzelm@2388:   "_setle"      :: ['a set, 'a set] => bool           ("(_/ <= _)" [50, 51] 50)
wenzelm@3820:   "_setless"    :: ['a set, 'a set] => bool           ("op <")
wenzelm@2684:   "_setless"    :: ['a set, 'a set] => bool           ("(_/ < _)" [50, 51] 50)
clasohm@923: 
wenzelm@2261: syntax (symbols)
wenzelm@3820:   "_setle"      :: ['a set, 'a set] => bool           ("op \\<subseteq>")
wenzelm@2388:   "_setle"      :: ['a set, 'a set] => bool           ("(_/ \\<subseteq> _)" [50, 51] 50)
wenzelm@3820:   "_setless"    :: ['a set, 'a set] => bool           ("op \\<subset>")
wenzelm@2684:   "_setless"    :: ['a set, 'a set] => bool           ("(_/ \\<subset> _)" [50, 51] 50)
wenzelm@2261:   "op Int"      :: ['a set, 'a set] => 'a set         (infixl "\\<inter>" 70)
wenzelm@2261:   "op Un"       :: ['a set, 'a set] => 'a set         (infixl "\\<union>" 65)
wenzelm@3820:   "op :"        :: ['a, 'a set] => bool               ("op \\<in>")
wenzelm@2261:   "op :"        :: ['a, 'a set] => bool               ("(_/ \\<in> _)" [50, 51] 50)
wenzelm@3820:   "op ~:"       :: ['a, 'a set] => bool               ("op \\<notin>")
wenzelm@2261:   "op ~:"       :: ['a, 'a set] => bool               ("(_/ \\<notin> _)" [50, 51] 50)
wenzelm@2261:   "UN "         :: [idts, bool] => bool               ("(3\\<Union> _./ _)" 10)
wenzelm@2261:   "INT "        :: [idts, bool] => bool               ("(3\\<Inter> _./ _)" 10)
paulson@4159:   "UNION1"      :: [pttrn, 'b set] => 'b set          ("(3\\<Union> _./ _)" 10)
paulson@4159:   "INTER1"      :: [pttrn, 'b set] => 'b set          ("(3\\<Inter> _./ _)" 10)
wenzelm@2261:   "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Union> _\\<in>_./ _)" 10)
wenzelm@2261:   "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Inter> _\\<in>_./ _)" 10)
wenzelm@2261:   Union         :: (('a set) set) => 'a set           ("\\<Union> _" [90] 90)
wenzelm@2261:   Inter         :: (('a set) set) => 'a set           ("\\<Inter> _" [90] 90)
wenzelm@2368:   "@Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
wenzelm@2368:   "@Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
wenzelm@2372: 
wenzelm@2372: syntax (symbols output)
wenzelm@2368:   "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
wenzelm@2368:   "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
wenzelm@2261: 
wenzelm@2412: translations
wenzelm@2965:   "op \\<subseteq>" => "op <= :: [_ set, _ set] => bool"
wenzelm@2965:   "op \\<subset>" => "op <  :: [_ set, _ set] => bool"
wenzelm@2412: 
wenzelm@2261: 
wenzelm@2261: 
wenzelm@2261: (** Rules and definitions **)
wenzelm@2261: 
wenzelm@3947: local
wenzelm@3947: 
clasohm@923: rules
clasohm@923: 
clasohm@923:   (* Isomorphisms between Predicates and Sets *)
clasohm@923: 
wenzelm@3842:   mem_Collect_eq    "(a : {x. P(x)}) = P(a)"
wenzelm@3842:   Collect_mem_eq    "{x. x:A} = A"
clasohm@923: 
clasohm@923: 
clasohm@923: defs
wenzelm@2261: 
clasohm@923:   Ball_def      "Ball A P       == ! x. x:A --> P(x)"
clasohm@923:   Bex_def       "Bex A P        == ? x. x:A & P(x)"
clasohm@923:   subset_def    "A <= B         == ! x:A. x:B"
nipkow@3222:   psubset_def   "A < B          == (A::'a set) <= B & ~ A=B"
paulson@5492:   Compl_def     "- A            == {x. ~x:A}"
wenzelm@3842:   Un_def        "A Un B         == {x. x:A | x:B}"
wenzelm@3842:   Int_def       "A Int B        == {x. x:A & x:B}"
clasohm@923:   set_diff_def  "A - B          == {x. x:A & ~x:B}"
clasohm@923:   INTER_def     "INTER A B      == {y. ! x:A. y: B(x)}"
clasohm@923:   UNION_def     "UNION A B      == {y. ? x:A. y: B(x)}"
oheimb@2393:   Inter_def     "Inter S        == (INT x:S. x)"
oheimb@2393:   Union_def     "Union S        == (UN x:S. x)"
oheimb@2393:   Pow_def       "Pow A          == {B. B <= A}"
clasohm@923:   empty_def     "{}             == {x. False}"
paulson@4159:   UNIV_def      "UNIV           == {x. True}"
wenzelm@3842:   insert_def    "insert a B     == {x. x=a} Un B"
clasohm@923:   image_def     "f``A           == {y. ? x:A. y=f(x)}"
regensbu@1273: 
clasohm@923: end
clasohm@923: 
wenzelm@2261: 
clasohm@923: ML
clasohm@923: 
clasohm@923: local
clasohm@923: 
wenzelm@2388: (* Set inclusion *)
wenzelm@2388: 
wenzelm@4151: fun le_tr' _ (*op <=*) (Type ("fun", (Type ("set", _) :: _))) ts =
wenzelm@2388:       list_comb (Syntax.const "_setle", ts)
wenzelm@4151:   | le_tr' _ (*op <=*) _ _ = raise Match;
wenzelm@2388: 
wenzelm@4151: fun less_tr' _ (*op <*) (Type ("fun", (Type ("set", _) :: _))) ts =
wenzelm@2684:       list_comb (Syntax.const "_setless", ts)
wenzelm@4151:   | less_tr' _ (*op <*) _ _ = raise Match;
wenzelm@2684: 
wenzelm@2388: 
clasohm@923: (* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P}      *)
clasohm@923: (* {y. ? x1..xn. y = e & P} is only translated if [0..n] subset bvs(e) *)
clasohm@923: 
clasohm@923: val ex_tr = snd(mk_binder_tr("? ","Ex"));
clasohm@923: 
clasohm@923: fun nvars(Const("_idts",_) $ _ $ idts) = nvars(idts)+1
clasohm@923:   | nvars(_) = 1;
clasohm@923: 
clasohm@923: fun setcompr_tr[e,idts,b] =
clasohm@923:   let val eq = Syntax.const("op =") $ Bound(nvars(idts)) $ e
clasohm@923:       val P = Syntax.const("op &") $ eq $ b
clasohm@923:       val exP = ex_tr [idts,P]
clasohm@923:   in Syntax.const("Collect") $ Abs("",dummyT,exP) end;
clasohm@923: 
clasohm@923: val ex_tr' = snd(mk_binder_tr' ("Ex","DUMMY"));
clasohm@923: 
clasohm@923: fun setcompr_tr'[Abs(_,_,P)] =
clasohm@923:   let fun ok(Const("Ex",_)$Abs(_,_,P),n) = ok(P,n+1)
clasohm@923:         | ok(Const("op &",_) $ (Const("op =",_) $ Bound(m) $ e) $ _, n) =
clasohm@923:             if n>0 andalso m=n andalso
clasohm@923:               ((0 upto (n-1)) subset add_loose_bnos(e,0,[]))
clasohm@923:             then () else raise Match
clasohm@923: 
clasohm@923:       fun tr'(_ $ abs) =
clasohm@923:         let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr'[abs]
clasohm@923:         in Syntax.const("@SetCompr") $ e $ idts $ Q end
clasohm@923:   in ok(P,0); tr'(P) end;
clasohm@923: 
clasohm@923: in
clasohm@923: 
clasohm@923: val parse_translation = [("@SetCompr", setcompr_tr)];
clasohm@923: val print_translation = [("Collect", setcompr_tr')];
wenzelm@2684: val typed_print_translation = [("op <=", le_tr'), ("op <", less_tr')];
clasohm@923: val print_ast_translation =
clasohm@923:   map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];
clasohm@923: 
clasohm@923: end;