1 |
|
2 (* Author: Florian Haftmann, TU Muenchen *) |
|
3 |
|
4 header {* Executable finite sets *} |
|
5 |
|
6 theory Code_Set |
|
7 imports List_Set |
|
8 begin |
|
9 |
|
10 lemma foldl_apply_inv: |
|
11 assumes "\<And>x. g (h x) = x" |
|
12 shows "foldl f (g s) xs = g (foldl (\<lambda>s x. h (f (g s) x)) s xs)" |
|
13 by (rule sym, induct xs arbitrary: s) (simp_all add: assms) |
|
14 |
|
15 subsection {* Lifting *} |
|
16 |
|
17 datatype 'a fset = Fset "'a set" |
|
18 |
|
19 primrec member :: "'a fset \<Rightarrow> 'a set" where |
|
20 "member (Fset A) = A" |
|
21 |
|
22 lemma Fset_member [simp]: |
|
23 "Fset (member A) = A" |
|
24 by (cases A) simp |
|
25 |
|
26 definition Set :: "'a list \<Rightarrow> 'a fset" where |
|
27 "Set xs = Fset (set xs)" |
|
28 |
|
29 lemma member_Set [simp]: |
|
30 "member (Set xs) = set xs" |
|
31 by (simp add: Set_def) |
|
32 |
|
33 code_datatype Set |
|
34 |
|
35 |
|
36 subsection {* Basic operations *} |
|
37 |
|
38 definition is_empty :: "'a fset \<Rightarrow> bool" where |
|
39 "is_empty A \<longleftrightarrow> List_Set.is_empty (member A)" |
|
40 |
|
41 lemma is_empty_Set [code]: |
|
42 "is_empty (Set xs) \<longleftrightarrow> null xs" |
|
43 by (simp add: is_empty_def is_empty_set) |
|
44 |
|
45 definition empty :: "'a fset" where |
|
46 "empty = Fset {}" |
|
47 |
|
48 lemma empty_Set [code]: |
|
49 "empty = Set []" |
|
50 by (simp add: empty_def Set_def) |
|
51 |
|
52 definition insert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
|
53 "insert x A = Fset (Set.insert x (member A))" |
|
54 |
|
55 lemma insert_Set [code]: |
|
56 "insert x (Set xs) = Set (List_Set.insert x xs)" |
|
57 by (simp add: insert_def Set_def insert_set) |
|
58 |
|
59 definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
|
60 "remove x A = Fset (List_Set.remove x (member A))" |
|
61 |
|
62 lemma remove_Set [code]: |
|
63 "remove x (Set xs) = Set (remove_all x xs)" |
|
64 by (simp add: remove_def Set_def remove_set) |
|
65 |
|
66 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where |
|
67 "map f A = Fset (image f (member A))" |
|
68 |
|
69 lemma map_Set [code]: |
|
70 "map f (Set xs) = Set (remdups (List.map f xs))" |
|
71 by (simp add: map_def Set_def) |
|
72 |
|
73 definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
|
74 "project P A = Fset (List_Set.project P (member A))" |
|
75 |
|
76 lemma project_Set [code]: |
|
77 "project P (Set xs) = Set (filter P xs)" |
|
78 by (simp add: project_def Set_def project_set) |
|
79 |
|
80 definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where |
|
81 "forall P A \<longleftrightarrow> Ball (member A) P" |
|
82 |
|
83 lemma forall_Set [code]: |
|
84 "forall P (Set xs) \<longleftrightarrow> list_all P xs" |
|
85 by (simp add: forall_def Set_def ball_set) |
|
86 |
|
87 definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where |
|
88 "exists P A \<longleftrightarrow> Bex (member A) P" |
|
89 |
|
90 lemma exists_Set [code]: |
|
91 "exists P (Set xs) \<longleftrightarrow> list_ex P xs" |
|
92 by (simp add: exists_def Set_def bex_set) |
|
93 |
|
94 |
|
95 subsection {* Functorial operations *} |
|
96 |
|
97 definition union :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
|
98 "union A B = Fset (member A \<union> member B)" |
|
99 |
|
100 lemma union_insert [code]: |
|
101 "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs" |
|
102 proof - |
|
103 have "foldl (\<lambda>A x. Set.insert x A) (member A) xs = |
|
104 member (foldl (\<lambda>A x. Fset (Set.insert x (member A))) A xs)" |
|
105 by (rule foldl_apply_inv) simp |
|
106 then show ?thesis by (simp add: union_def union_set insert_def) |
|
107 qed |
|
108 |
|
109 definition subtract :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
|
110 "subtract A B = Fset (member B - member A)" |
|
111 |
|
112 lemma subtract_remove [code]: |
|
113 "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs" |
|
114 proof - |
|
115 have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs = |
|
116 member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)" |
|
117 by (rule foldl_apply_inv) simp |
|
118 then show ?thesis by (simp add: subtract_def minus_set remove_def) |
|
119 qed |
|
120 |
|
121 |
|
122 subsection {* Derived operations *} |
|
123 |
|
124 lemma member_exists [code]: |
|
125 "member A y \<longleftrightarrow> exists (\<lambda>x. y = x) A" |
|
126 by (simp add: exists_def mem_def) |
|
127 |
|
128 definition subfset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where |
|
129 "subfset_eq A B \<longleftrightarrow> member A \<subseteq> member B" |
|
130 |
|
131 lemma subfset_eq_forall [code]: |
|
132 "subfset_eq A B \<longleftrightarrow> forall (\<lambda>x. member B x) A" |
|
133 by (simp add: subfset_eq_def subset_eq forall_def mem_def) |
|
134 |
|
135 definition subfset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where |
|
136 "subfset A B \<longleftrightarrow> member A \<subset> member B" |
|
137 |
|
138 lemma subfset_subfset_eq [code]: |
|
139 "subfset A B \<longleftrightarrow> subfset_eq A B \<and> \<not> subfset_eq B A" |
|
140 by (simp add: subfset_def subfset_eq_def subset) |
|
141 |
|
142 lemma eq_fset_subfset_eq [code]: |
|
143 "eq_class.eq A B \<longleftrightarrow> subfset_eq A B \<and> subfset_eq B A" |
|
144 by (cases A, cases B) (simp add: eq subfset_eq_def set_eq) |
|
145 |
|
146 definition inter :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
|
147 "inter A B = Fset (List_Set.project (member A) (member B))" |
|
148 |
|
149 lemma inter_project [code]: |
|
150 "inter A B = project (member A) B" |
|
151 by (simp add: inter_def project_def inter) |
|
152 |
|
153 |
|
154 subsection {* Misc operations *} |
|
155 |
|
156 lemma size_fset [code]: |
|
157 "fset_size f A = 0" |
|
158 "size A = 0" |
|
159 by (cases A, simp) (cases A, simp) |
|
160 |
|
161 lemma fset_case_code [code]: |
|
162 "fset_case f A = f (member A)" |
|
163 by (cases A) simp |
|
164 |
|
165 lemma fset_rec_code [code]: |
|
166 "fset_rec f A = f (member A)" |
|
167 by (cases A) simp |
|
168 |
|
169 end |
|