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: clasohm@923: types clasohm@923: 'a set clasohm@923: clasohm@923: arities clasohm@923: set :: (term) term clasohm@923: clasohm@923: instance clasohm@923: set :: (term) {ord, minus} clasohm@923: clasohm@923: consts clasohm@1370: "{}" :: 'a set ("{}") clasohm@1370: insert :: ['a, 'a set] => 'a set clasohm@1370: Collect :: ('a => bool) => 'a set (*comprehension*) clasohm@1370: Compl :: ('a set) => 'a set (*complement*) 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*) clasohm@1370: UNION1 :: ['a => 'b set] => 'b set (binder "UN " 10) clasohm@1370: INTER1 :: ['a => 'b set] => 'b set (binder "INT " 10) 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: wenzelm@2261: wenzelm@2261: (** Additional concrete syntax **) wenzelm@2261: clasohm@923: syntax clasohm@923: wenzelm@2261: "op :" :: ['a, 'a set] => bool ("op :") nipkow@1531: wenzelm@2261: UNIV :: 'a set wenzelm@2261: wenzelm@2261: (* Infix syntax for non-membership *) clasohm@923: wenzelm@2261: "op ~:" :: ['a, 'a set] => bool ("(_/ ~: _)" [50, 51] 50) wenzelm@2261: "op ~:" :: ['a, 'a set] => bool ("op ~:") 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: 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 nipkow@1531: "UNIV" == "Compl {}" 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)" clasohm@923: "INT x:A. B" == "INTER A (%x. B)" clasohm@923: "UN x:A. B" == "UNION 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@2388: "_setle" :: ['a set, 'a set] => bool ("(_/ <= _)" [50, 51] 50) wenzelm@2388: "_setle" :: ['a set, 'a set] => bool ("op <=") wenzelm@2684: "_setless" :: ['a set, 'a set] => bool ("(_/ < _)" [50, 51] 50) wenzelm@2684: "_setless" :: ['a set, 'a set] => bool ("op <") clasohm@923: wenzelm@2261: syntax (symbols) wenzelm@2388: "_setle" :: ['a set, 'a set] => bool ("(_/ \\ _)" [50, 51] 50) wenzelm@2388: "_setle" :: ['a set, 'a set] => bool ("op \\") wenzelm@2684: "_setless" :: ['a set, 'a set] => bool ("(_/ \\ _)" [50, 51] 50) wenzelm@2684: "_setless" :: ['a set, 'a set] => bool ("op \\") wenzelm@2261: "op Int" :: ['a set, 'a set] => 'a set (infixl "\\" 70) wenzelm@2261: "op Un" :: ['a set, 'a set] => 'a set (infixl "\\" 65) wenzelm@2261: "op :" :: ['a, 'a set] => bool ("(_/ \\ _)" [50, 51] 50) wenzelm@2261: "op :" :: ['a, 'a set] => bool ("op \\") wenzelm@2261: "op ~:" :: ['a, 'a set] => bool ("(_/ \\ _)" [50, 51] 50) wenzelm@2261: "op ~:" :: ['a, 'a set] => bool ("op \\") wenzelm@2261: "UN " :: [idts, bool] => bool ("(3\\ _./ _)" 10) wenzelm@2261: "INT " :: [idts, bool] => bool ("(3\\ _./ _)" 10) wenzelm@2261: "@UNION" :: [pttrn, 'a set, 'b set] => 'b set ("(3\\ _\\_./ _)" 10) wenzelm@2261: "@INTER" :: [pttrn, 'a set, 'b set] => 'b set ("(3\\ _\\_./ _)" 10) wenzelm@2261: Union :: (('a set) set) => 'a set ("\\ _" [90] 90) wenzelm@2261: Inter :: (('a set) set) => 'a set ("\\ _" [90] 90) 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@2372: wenzelm@2372: syntax (symbols output) 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@2261: wenzelm@2412: translations wenzelm@2965: "op \\" => "op <= :: [_ set, _ set] => bool" wenzelm@2965: "op \\" => "op < :: [_ set, _ set] => bool" wenzelm@2412: wenzelm@2261: wenzelm@2261: wenzelm@2261: (** Rules and definitions **) wenzelm@2261: clasohm@923: rules clasohm@923: clasohm@923: (* Isomorphisms between Predicates and Sets *) clasohm@923: clasohm@923: mem_Collect_eq "(a : {x.P(x)}) = P(a)" clasohm@923: 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" oheimb@2393: Compl_def "Compl A == {x. ~x:A}" clasohm@923: Un_def "A Un B == {x.x:A | x:B}" clasohm@923: 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: INTER1_def "INTER1 B == INTER {x.True} B" oheimb@2393: UNION1_def "UNION1 B == UNION {x.True} B" 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}" clasohm@923: 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@2388: fun le_tr' (*op <=*) (Type ("fun", (Type ("set", _) :: _))) ts = wenzelm@2388: list_comb (Syntax.const "_setle", ts) wenzelm@2388: | le_tr' (*op <=*) _ _ = raise Match; wenzelm@2388: wenzelm@2684: fun less_tr' (*op <*) (Type ("fun", (Type ("set", _) :: _))) ts = wenzelm@2684: list_comb (Syntax.const "_setless", ts) wenzelm@2684: | 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;