23854
|
1 |
(* Title: HOL/Library/Executable_Set.thy
|
|
2 |
Author: Stefan Berghofer, TU Muenchen
|
|
3 |
*)
|
|
4 |
|
|
5 |
header {* Implementation of finite sets by lists *}
|
|
6 |
|
|
7 |
theory Executable_Set
|
31847
|
8 |
imports Main Code_Set
|
23854
|
9 |
begin
|
|
10 |
|
31847
|
11 |
subsection {* Derived set operations *}
|
|
12 |
|
|
13 |
declare member [code]
|
23854
|
14 |
|
28522
|
15 |
definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
|
|
16 |
"subset = op \<le>"
|
|
17 |
|
|
18 |
declare subset_def [symmetric, code unfold]
|
|
19 |
|
31847
|
20 |
lemma [code]:
|
|
21 |
"subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
|
|
22 |
by (simp add: subset_def subset_eq)
|
28522
|
23 |
|
|
24 |
definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
|
|
25 |
[code del]: "eq_set = op ="
|
|
26 |
|
29107
|
27 |
(* FIXME allow for Stefan's code generator:
|
|
28 |
declare set_eq_subset[code unfold]
|
|
29 |
*)
|
|
30 |
|
23854
|
31 |
lemma [code]:
|
31847
|
32 |
"eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
|
|
33 |
by (simp add: eq_set_def set_eq)
|
23854
|
34 |
|
31847
|
35 |
declare inter [code]
|
23854
|
36 |
|
31847
|
37 |
declare Inter_image_eq [symmetric, code]
|
|
38 |
declare Union_image_eq [symmetric, code]
|
23854
|
39 |
|
|
40 |
|
31847
|
41 |
subsection {* Rewrites for primitive operations *}
|
23854
|
42 |
|
31847
|
43 |
declare List_Set.project_def [symmetric, code unfold]
|
23854
|
44 |
|
|
45 |
|
31847
|
46 |
subsection {* code generator setup *}
|
23854
|
47 |
|
31847
|
48 |
text {* eliminate popular infixes *}
|
23854
|
49 |
|
|
50 |
ML {*
|
|
51 |
nonfix inter;
|
|
52 |
nonfix union;
|
|
53 |
nonfix subset;
|
|
54 |
*}
|
|
55 |
|
31847
|
56 |
text {* type @{typ "'a fset"} *}
|
|
57 |
|
|
58 |
types_code
|
|
59 |
fset ("(_/ list)")
|
|
60 |
|
|
61 |
consts_code
|
|
62 |
Set ("_")
|
|
63 |
|
|
64 |
text {* primitive operations *}
|
|
65 |
|
|
66 |
definition flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
|
|
67 |
"flip f a b = f b a"
|
23854
|
68 |
|
|
69 |
consts_code
|
31847
|
70 |
"Set.empty" ("{*Code_Set.empty*}")
|
|
71 |
"List_Set.is_empty" ("{*Code_Set.is_empty*}")
|
|
72 |
"Set.insert" ("{*Code_Set.insert*}")
|
|
73 |
"List_Set.remove" ("{*Code_Set.remove*}")
|
|
74 |
"Set.image" ("{*Code_Set.map*}")
|
|
75 |
"List_Set.project" ("{*Code_Set.filter*}")
|
|
76 |
"Ball" ("{*flip Code_Set.forall*}")
|
|
77 |
"Bex" ("{*flip Code_Set.exists*}")
|
|
78 |
"op \<union>" ("{*Code_Set.union*}")
|
|
79 |
"op \<inter>" ("{*Code_Set.inter*}")
|
|
80 |
"op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip subtract*}")
|
|
81 |
"Set.Union" ("{*Code_Set.union*}")
|
|
82 |
"Set.Inter" ("{*Code_Set.inter*}")
|
|
83 |
fold ("{*foldl o flip*}")
|
23854
|
84 |
|
31847
|
85 |
end |