|
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 "~:" :: "['a, 'a set] => bool" (infixl 50) |
|
41 |
|
42 "@Finset" :: "args => 'a set" ("{(_)}") |
|
43 |
|
44 "@Coll" :: "[idt, bool] => 'a set" ("(1{_./ _})") |
|
45 "@SetCompr" :: "['a, idts, bool] => 'a set" ("(1{_ |/_./ _})") |
|
46 |
|
47 (* Big Intersection / Union *) |
|
48 |
|
49 "@INTER" :: "[idt, 'a set, 'b set] => 'b set" ("(3INT _:_./ _)" 10) |
|
50 "@UNION" :: "[idt, 'a set, 'b set] => 'b set" ("(3UN _:_./ _)" 10) |
|
51 |
|
52 (* Bounded Quantifiers *) |
|
53 |
|
54 "@Ball" :: "[idt, 'a set, bool] => bool" ("(3! _:_./ _)" 10) |
|
55 "@Bex" :: "[idt, 'a set, bool] => bool" ("(3? _:_./ _)" 10) |
|
56 "*Ball" :: "[idt, 'a set, bool] => bool" ("(3ALL _:_./ _)" 10) |
|
57 "*Bex" :: "[idt, 'a set, bool] => bool" ("(3EX _:_./ _)" 10) |
|
58 |
|
59 translations |
|
60 "x ~: y" == "~ (x : y)" |
|
61 "{x, xs}" == "insert x {xs}" |
|
62 "{x}" == "insert x {}" |
|
63 "{x. P}" == "Collect (%x. P)" |
|
64 "INT x:A. B" == "INTER A (%x. B)" |
|
65 "UN x:A. B" == "UNION A (%x. B)" |
|
66 "! x:A. P" == "Ball A (%x. P)" |
|
67 "? x:A. P" == "Bex A (%x. P)" |
|
68 "ALL x:A. P" => "Ball A (%x. P)" |
|
69 "EX x:A. P" => "Bex A (%x. P)" |
|
70 |
|
71 |
|
72 rules |
|
73 |
|
74 (* Isomorphisms between Predicates and Sets *) |
|
75 |
|
76 mem_Collect_eq "(a : {x.P(x)}) = P(a)" |
|
77 Collect_mem_eq "{x.x:A} = A" |
|
78 |
|
79 |
|
80 defs |
|
81 Ball_def "Ball A P == ! x. x:A --> P(x)" |
|
82 Bex_def "Bex A P == ? x. x:A & P(x)" |
|
83 subset_def "A <= B == ! x:A. x:B" |
|
84 Compl_def "Compl(A) == {x. ~x:A}" |
|
85 Un_def "A Un B == {x.x:A | x:B}" |
|
86 Int_def "A Int B == {x.x:A & x:B}" |
|
87 set_diff_def "A - B == {x. x:A & ~x:B}" |
|
88 INTER_def "INTER A B == {y. ! x:A. y: B(x)}" |
|
89 UNION_def "UNION A B == {y. ? x:A. y: B(x)}" |
|
90 INTER1_def "INTER1(B) == INTER {x.True} B" |
|
91 UNION1_def "UNION1(B) == UNION {x.True} B" |
|
92 Inter_def "Inter(S) == (INT x:S. x)" |
|
93 Union_def "Union(S) == (UN x:S. x)" |
|
94 Pow_def "Pow(A) == {B. B <= A}" |
|
95 empty_def "{} == {x. False}" |
|
96 insert_def "insert a B == {x.x=a} Un B" |
|
97 range_def "range(f) == {y. ? x. y=f(x)}" |
|
98 image_def "f``A == {y. ? x:A. y=f(x)}" |
|
99 inj_def "inj(f) == ! x y. f(x)=f(y) --> x=y" |
|
100 inj_onto_def "inj_onto f A == ! x:A. ! y:A. f(x)=f(y) --> x=y" |
|
101 surj_def "surj(f) == ! y. ? x. y=f(x)" |
|
102 |
|
103 end |
|
104 |
|
105 ML |
|
106 |
|
107 local |
|
108 |
|
109 (* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P} *) |
|
110 (* {y. ? x1..xn. y = e & P} is only translated if [0..n] subset bvs(e) *) |
|
111 |
|
112 val ex_tr = snd(mk_binder_tr("? ","Ex")); |
|
113 |
|
114 fun nvars(Const("_idts",_) $ _ $ idts) = nvars(idts)+1 |
|
115 | nvars(_) = 1; |
|
116 |
|
117 fun setcompr_tr[e,idts,b] = |
|
118 let val eq = Syntax.const("op =") $ Bound(nvars(idts)) $ e |
|
119 val P = Syntax.const("op &") $ eq $ b |
|
120 val exP = ex_tr [idts,P] |
|
121 in Syntax.const("Collect") $ Abs("",dummyT,exP) end; |
|
122 |
|
123 val ex_tr' = snd(mk_binder_tr' ("Ex","DUMMY")); |
|
124 |
|
125 fun setcompr_tr'[Abs(_,_,P)] = |
|
126 let fun ok(Const("Ex",_)$Abs(_,_,P),n) = ok(P,n+1) |
|
127 | ok(Const("op &",_) $ (Const("op =",_) $ Bound(m) $ e) $ _, n) = |
|
128 if n>0 andalso m=n andalso |
|
129 ((0 upto (n-1)) subset add_loose_bnos(e,0,[])) |
|
130 then () else raise Match |
|
131 |
|
132 fun tr'(_ $ abs) = |
|
133 let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr'[abs] |
|
134 in Syntax.const("@SetCompr") $ e $ idts $ Q end |
|
135 in ok(P,0); tr'(P) end; |
|
136 |
|
137 in |
|
138 |
|
139 val parse_translation = [("@SetCompr", setcompr_tr)]; |
|
140 val print_translation = [("Collect", setcompr_tr')]; |
|
141 val print_ast_translation = |
|
142 map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")]; |
|
143 |
|
144 end; |
|
145 |