author  haftmann 
Mon, 18 Dec 2006 08:21:31 +0100  
changeset 21875  5df10a17644e 
parent 21572  7442833ea2b6 
child 21911  e29bcab0c81c 
permissions  rwrr 
17632  1 
(* Title: HOL/Library/ExecutableSet.thy 
2 
ID: $Id$ 

3 
Author: Stefan Berghofer, TU Muenchen 

4 
*) 

5 

6 
header {* Implementation of finite sets by lists *} 

7 

8 
theory ExecutableSet 

9 
imports Main 

10 
begin 

11 

21323  12 
section {* Definitional rewrites *} 
20597  13 

14 
instance set :: (eq) eq .. 

19791  15 

21385
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

16 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21385
diff
changeset

17 
minus_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where 
21385
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

18 
"minus_set xs ys = ys  xs" 
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

19 

cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

20 
lemma [code inline]: 
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

21 
"op  = (\<lambda>xs ys. minus_set ys xs)" 
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

22 
unfolding minus_set_def .. 
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

23 

cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

24 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21385
diff
changeset

25 
subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21385
diff
changeset

26 
"subset = op \<subseteq>" 
21385
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

27 

cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

28 
lemmas [symmetric, code inline] = subset_def 
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

29 

21572  30 
definition 
31 
strict_subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where 

32 
"strict_subset = op \<subset>" 

33 

34 
lemmas [symmetric, code inline] = strict_subset_def 

35 

21153  36 
lemma [code target: Set]: 
21385
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

37 
"A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" 
17632  38 
by blast 
39 

20597  40 
lemma [code func]: 
21572  41 
"(A\<Colon>'a\<Colon>eq set) = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" 
42 
by blast 

43 

44 
lemma [code func]: 

21385
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

45 
"subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)" 
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

46 
unfolding subset_def Set.subset_def .. 
20597  47 

21572  48 
lemma [code func]: 
49 
"strict_subset A B \<longleftrightarrow> subset A B \<and> A \<noteq> B" 

50 
unfolding subset_def strict_subset_def by blast 

51 

21323  52 
lemma [code]: 
53 
"a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)" 

54 
unfolding bex_triv_one_point1 .. 

17632  55 

21385
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

56 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21385
diff
changeset

57 
filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21385
diff
changeset

58 
"filter_set P xs = {x\<in>xs. P x}" 
20597  59 

21385
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

60 
lemmas [symmetric, code inline] = filter_set_def 
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

61 

cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

62 

cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

63 
section {* Operations on lists *} 
19791  64 

65 
subsection {* Basic definitions *} 

66 

67 
definition 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21385
diff
changeset

68 
flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where 
19791  69 
"flip f a b = f b a" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21385
diff
changeset

70 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21385
diff
changeset

71 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21385
diff
changeset

72 
member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where 
19791  73 
"member xs x = (x \<in> set xs)" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21385
diff
changeset

74 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21385
diff
changeset

75 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21385
diff
changeset

76 
insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
19791  77 
"insertl x xs = (if member xs x then xs else x#xs)" 
78 

79 
lemma 

80 
[code target: List]: "member [] y = False" 

81 
and [code target: List]: "member (x#xs) y = (y = x \<or> member xs y)" 

82 
unfolding member_def by (induct xs) simp_all 

83 

84 
consts 

85 
drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" 

86 

87 
primrec 

88 
"drop_first f [] = []" 

89 
"drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)" 

90 
declare drop_first.simps [code del] 

91 
declare drop_first.simps [code target: List] 

92 

93 
declare remove1.simps [code del] 

94 
lemma [code target: List]: 

95 
"remove1 x xs = (if member xs x then drop_first (\<lambda>y. y = x) xs else xs)" 

96 
proof (cases "member xs x") 

97 
case False thus ?thesis unfolding member_def by (induct xs) auto 

98 
next 

99 
case True 

100 
have "remove1 x xs = drop_first (\<lambda>y. y = x) xs" by (induct xs) simp_all 

101 
with True show ?thesis by simp 

102 
qed 

103 

104 
lemma member_nil [simp]: 

105 
"member [] = (\<lambda>x. False)" 

106 
proof 

107 
fix x 

108 
show "member [] x = False" unfolding member_def by simp 

109 
qed 

110 

111 
lemma member_insertl [simp]: 

112 
"x \<in> set (insertl x xs)" 

113 
unfolding insertl_def member_def mem_iff by simp 

114 

115 
lemma insertl_member [simp]: 

116 
fixes xs x 

117 
assumes member: "member xs x" 

118 
shows "insertl x xs = xs" 

119 
using member unfolding insertl_def by simp 

120 

121 
lemma insertl_not_member [simp]: 

122 
fixes xs x 

123 
assumes member: "\<not> (member xs x)" 

124 
shows "insertl x xs = x # xs" 

125 
using member unfolding insertl_def by simp 

126 

127 
lemma foldr_remove1_empty [simp]: 

128 
"foldr remove1 xs [] = []" 

129 
by (induct xs) simp_all 

130 

131 

132 
subsection {* Derived definitions *} 

133 

20934  134 
function unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset

135 
where 
19791  136 
"unionl [] ys = ys" 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset

137 
 "unionl xs ys = foldr insertl xs ys" 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset

138 
by pat_completeness auto 
21321  139 
termination by lexicographic_order 
140 

19791  141 
lemmas unionl_def = unionl.simps(2) 
142 

20934  143 
function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset

144 
where 
19791  145 
"intersect [] ys = []" 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset

146 
 "intersect xs [] = []" 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset

147 
 "intersect xs ys = filter (member xs) ys" 
21321  148 
by pat_completeness auto 
149 
termination by lexicographic_order 

150 

19791  151 
lemmas intersect_def = intersect.simps(3) 
152 

20934  153 
function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset

154 
where 
19791  155 
"subtract [] ys = ys" 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset

156 
 "subtract xs [] = []" 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset

157 
 "subtract xs ys = foldr remove1 xs ys" 
21321  158 
by pat_completeness auto 
159 
termination by lexicographic_order 

160 

19791  161 
lemmas subtract_def = subtract.simps(3) 
162 

20934  163 
function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset

164 
where 
19791  165 
"map_distinct f [] = []" 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset

166 
 "map_distinct f xs = foldr (insertl o f) xs []" 
21321  167 
by pat_completeness auto 
168 
termination by lexicographic_order 

169 

19791  170 
lemmas map_distinct_def = map_distinct.simps(2) 
171 

20934  172 
function unions :: "'a list list \<Rightarrow> 'a list" 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset

173 
where 
19791  174 
"unions [] = []" 
175 
"unions xs = foldr unionl xs []" 

21321  176 
by pat_completeness auto 
177 
termination by lexicographic_order 

178 

19791  179 
lemmas unions_def = unions.simps(2) 
180 

20934  181 
consts intersects :: "'a list list \<Rightarrow> 'a list" 
19791  182 
primrec 
183 
"intersects (x#xs) = foldr intersect xs x" 

184 

185 
definition 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21385
diff
changeset

186 
map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where 
19791  187 
"map_union xs f = unions (map f xs)" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21385
diff
changeset

188 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21385
diff
changeset

189 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21385
diff
changeset

190 
map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where 
19791  191 
"map_inter xs f = intersects (map f xs)" 
192 

193 

194 
section {* Isomorphism proofs *} 

195 

196 
lemma iso_member: 

197 
"member xs x = (x \<in> set xs)" 

198 
unfolding member_def mem_iff .. 

199 

200 
lemma iso_insert: 

201 
"set (insertl x xs) = insert x (set xs)" 

202 
unfolding insertl_def iso_member by (simp add: Set.insert_absorb) 

203 

204 
lemma iso_remove1: 

205 
assumes distnct: "distinct xs" 

206 
shows "set (remove1 x xs) = set xs  {x}" 

21385
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

207 
using distnct set_remove1_eq by auto 
19791  208 

209 
lemma iso_union: 

210 
"set (unionl xs ys) = set xs \<union> set ys" 

20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset

211 
unfolding unionl_def 
21385
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

212 
by (induct xs arbitrary: ys) (simp_all add: iso_insert) 
19791  213 

214 
lemma iso_intersect: 

215 
"set (intersect xs ys) = set xs \<inter> set ys" 

216 
unfolding intersect_def Int_def by (simp add: Int_def iso_member) auto 

217 

218 
lemma iso_subtract: 

219 
fixes ys 

220 
assumes distnct: "distinct ys" 

21385
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

221 
shows "set (subtract xs ys) = minus_set (set xs) (set ys)" 
19791  222 
and "distinct (subtract xs ys)" 
21385
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

223 
unfolding subtract_def minus_set_def 
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

224 
using distnct by (induct xs arbitrary: ys) auto 
19791  225 

226 
lemma iso_map_distinct: 

227 
"set (map_distinct f xs) = image f (set xs)" 

228 
unfolding map_distinct_def by (induct xs) (simp_all add: iso_insert) 

229 

230 
lemma iso_unions: 

231 
"set (unions xss) = \<Union> set (map set xss)" 

232 
unfolding unions_def proof (induct xss) 

233 
case Nil show ?case by simp 

234 
next 

235 
case (Cons xs xss) thus ?case by (induct xs) (simp_all add: iso_insert) 

236 
qed 

237 

238 
lemma iso_intersects: 

239 
"set (intersects (xs#xss)) = \<Inter> set (map set (xs#xss))" 

240 
by (induct xss) (simp_all add: Int_def iso_member, auto) 

241 

242 
lemma iso_UNION: 

243 
"set (map_union xs f) = UNION (set xs) (set o f)" 

244 
unfolding map_union_def iso_unions by simp 

245 

246 
lemma iso_INTER: 

247 
"set (map_inter (x#xs) f) = INTER (set (x#xs)) (set o f)" 

248 
unfolding map_inter_def iso_intersects by (induct xs) (simp_all add: iso_member, auto) 

249 

250 
definition 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21385
diff
changeset

251 
Blall :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where 
19791  252 
"Blall = flip list_all" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21385
diff
changeset

253 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21385
diff
changeset

254 
Blex :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where 
19791  255 
"Blex = flip list_ex" 
256 

257 
lemma iso_Ball: 

258 
"Blall xs f = Ball (set xs) f" 

259 
unfolding Blall_def flip_def by (induct xs) simp_all 

260 

261 
lemma iso_Bex: 

262 
"Blex xs f = Bex (set xs) f" 

263 
unfolding Blex_def flip_def by (induct xs) simp_all 

264 

21385
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

265 
lemma iso_filter: 
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

266 
"set (filter P xs) = filter_set P (set xs)" 
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

267 
unfolding filter_set_def by (induct xs) auto 
19791  268 

269 
section {* code generator setup *} 

270 

21008  271 
ML {* 
272 
nonfix inter; 

273 
nonfix union; 

21875  274 
nonfix subset; 
21008  275 
*} 
276 

21191  277 
code_modulename SML 
278 
ExecutableSet List 

21385
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

279 
Set List 
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

280 

cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

281 
code_modulename Haskell 
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

282 
ExecutableSet List 
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

283 
Set List 
20934  284 

21063  285 
definition [code inline]: 
20934  286 
"empty_list = []" 
287 

288 
lemma [code func]: 

289 
"insert (x \<Colon> 'a\<Colon>eq) = insert x" .. 

290 

291 
lemma [code func]: 

292 
"(xs \<Colon> 'a\<Colon>eq set) \<union> ys = xs \<union> ys" .. 

293 

294 
lemma [code func]: 

295 
"(xs \<Colon> 'a\<Colon>eq set) \<inter> ys = xs \<inter> ys" .. 

296 

21385
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

297 
lemma [code func]: 
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

298 
"minus_set xs = minus_set (xs \<Colon> 'a\<Colon>eq set)" .. 
20934  299 

300 
lemma [code func]: 

301 
"image (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq) = image f" .. 

302 

303 
lemma [code func]: 

304 
"UNION xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = UNION xs f" .. 

305 

306 
lemma [code func]: 

307 
"INTER xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = INTER xs f" .. 

308 

309 
lemma [code func]: 

310 
"Ball (xs \<Colon> 'a\<Colon>type set) = Ball xs" .. 

311 

312 
lemma [code func]: 

313 
"Bex (xs \<Colon> 'a\<Colon>type set) = Bex xs" .. 

314 

21385
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

315 
lemma [code func]: 
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

316 
"filter_set P (xs \<Colon> 'a\<Colon>type set) = filter_set P xs" .. 
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

317 

20934  318 
code_abstype "'a set" "'a list" where 
21115  319 
"{}" \<equiv> empty_list 
20934  320 
insert \<equiv> insertl 
321 
"op \<union>" \<equiv> unionl 

322 
"op \<inter>" \<equiv> intersect 

21385
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

323 
minus_set \<equiv> subtract 
20934  324 
image \<equiv> map_distinct 
325 
Union \<equiv> unions 

326 
Inter \<equiv> intersects 

327 
UNION \<equiv> map_union 

328 
INTER \<equiv> map_inter 

329 
Ball \<equiv> Blall 

330 
Bex \<equiv> Blex 

21385
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

331 
filter_set \<equiv> filter 
20934  332 

21385
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

333 
code_gen "{}" insert "op \<union>" "op \<inter>" minus_set 
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

334 
image Union Inter UNION INTER Ball Bex filter_set (SML ) 
20934  335 

336 

19791  337 
subsection {* type serializations *} 
338 

17632  339 
types_code 
340 
set ("_ list") 

341 
attach (term_of) {* 

342 
fun term_of_set f T [] = Const ("{}", Type ("set", [T])) 

343 
 term_of_set f T (x :: xs) = Const ("insert", 

344 
T > Type ("set", [T]) > Type ("set", [T])) $ f x $ term_of_set f T xs; 

345 
*} 

346 
attach (test) {* 

347 
fun gen_set' aG i j = frequency 

348 
[(i, fn () => aG j :: gen_set' aG (i1) j), (1, fn () => [])] () 

349 
and gen_set aG i = gen_set' aG i i; 

350 
*} 

351 

19791  352 

353 
subsection {* const serializations *} 

18702  354 

17632  355 
consts_code 
356 
"{}" ("[]") 

19791  357 
"insert" ("{*insertl*}") 
358 
"op Un" ("{*unionl*}") 

359 
"op Int" ("{*intersect*}") 

360 
"HOL.minus" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" 

361 
("{*flip subtract*}") 

362 
"image" ("{*map_distinct*}") 

363 
"Union" ("{*unions*}") 

364 
"Inter" ("{*intersects*}") 

365 
"UNION" ("{*map_union*}") 

366 
"INTER" ("{*map_inter*}") 

367 
"Ball" ("{*Blall*}") 

368 
"Bex" ("{*Blex*}") 

21385
cf398bb8a8be
added filter_set; adaptions to more strict type discipline for code lemmas
haftmann
parents:
21323
diff
changeset

369 
"filter_set" ("{*filter*}") 
17632  370 

371 
end 