6 theory List_Cset |
6 theory List_Cset |
7 imports Cset |
7 imports Cset |
8 begin |
8 begin |
9 |
9 |
10 declare mem_def [simp] |
10 declare mem_def [simp] |
11 |
11 declare Cset.set_code [code del] |
12 definition set :: "'a list \<Rightarrow> 'a Cset.set" where |
|
13 "set xs = Set (List.set xs)" |
|
14 hide_const (open) set |
|
15 |
|
16 lemma member_set [simp]: |
|
17 "member (List_Cset.set xs) = set xs" |
|
18 by (simp add: set_def) |
|
19 hide_fact (open) member_set |
|
20 |
12 |
21 definition coset :: "'a list \<Rightarrow> 'a Cset.set" where |
13 definition coset :: "'a list \<Rightarrow> 'a Cset.set" where |
22 "coset xs = Set (- set xs)" |
14 "coset xs = Set (- set xs)" |
23 hide_const (open) coset |
15 hide_const (open) coset |
24 |
16 |
25 lemma member_coset [simp]: |
17 lemma member_coset [simp]: |
26 "member (List_Cset.coset xs) = - set xs" |
18 "member (List_Cset.coset xs) = - set xs" |
27 by (simp add: coset_def) |
19 by (simp add: coset_def) |
28 hide_fact (open) member_coset |
20 hide_fact (open) member_coset |
29 |
21 |
30 code_datatype List_Cset.set List_Cset.coset |
22 code_datatype Cset.set List_Cset.coset |
31 |
23 |
32 lemma member_code [code]: |
24 lemma member_code [code]: |
33 "member (List_Cset.set xs) = List.member xs" |
25 "member (Cset.set xs) = List.member xs" |
34 "member (List_Cset.coset xs) = Not \<circ> List.member xs" |
26 "member (List_Cset.coset xs) = Not \<circ> List.member xs" |
35 by (simp_all add: fun_eq_iff member_def fun_Compl_def bool_Compl_def) |
27 by (simp_all add: fun_eq_iff member_def fun_Compl_def bool_Compl_def) |
36 |
28 |
37 lemma member_image_UNIV [simp]: |
29 lemma member_image_UNIV [simp]: |
38 "member ` UNIV = UNIV" |
30 "member ` UNIV = UNIV" |
67 no_notation scomp (infixl "\<circ>\<rightarrow>" 60) |
59 no_notation scomp (infixl "\<circ>\<rightarrow>" 60) |
68 |
60 |
69 subsection {* Basic operations *} |
61 subsection {* Basic operations *} |
70 |
62 |
71 lemma is_empty_set [code]: |
63 lemma is_empty_set [code]: |
72 "Cset.is_empty (List_Cset.set xs) \<longleftrightarrow> List.null xs" |
64 "Cset.is_empty (Cset.set xs) \<longleftrightarrow> List.null xs" |
73 by (simp add: is_empty_set null_def) |
65 by (simp add: is_empty_set null_def) |
74 hide_fact (open) is_empty_set |
66 hide_fact (open) is_empty_set |
75 |
67 |
76 lemma empty_set [code]: |
68 lemma empty_set [code]: |
77 "bot = List_Cset.set []" |
69 "Cset.empty = Cset.set []" |
78 by (simp add: set_def) |
70 by (simp add: set_def) |
79 hide_fact (open) empty_set |
71 hide_fact (open) empty_set |
80 |
72 |
81 lemma UNIV_set [code]: |
73 lemma UNIV_set [code]: |
82 "top = List_Cset.coset []" |
74 "top = List_Cset.coset []" |
83 by (simp add: coset_def) |
75 by (simp add: coset_def) |
84 hide_fact (open) UNIV_set |
76 hide_fact (open) UNIV_set |
85 |
77 |
86 lemma remove_set [code]: |
78 lemma remove_set [code]: |
87 "Cset.remove x (List_Cset.set xs) = List_Cset.set (removeAll x xs)" |
79 "Cset.remove x (Cset.set xs) = Cset.set (removeAll x xs)" |
88 "Cset.remove x (List_Cset.coset xs) = List_Cset.coset (List.insert x xs)" |
80 "Cset.remove x (List_Cset.coset xs) = List_Cset.coset (List.insert x xs)" |
89 by (simp_all add: set_def coset_def) |
81 by (simp_all add: Cset.set_def coset_def) |
90 (metis List.set_insert More_Set.remove_def remove_set_compl) |
82 (metis List.set_insert More_Set.remove_def remove_set_compl) |
91 |
83 |
92 lemma insert_set [code]: |
84 lemma insert_set [code]: |
93 "Cset.insert x (List_Cset.set xs) = List_Cset.set (List.insert x xs)" |
85 "Cset.insert x (Cset.set xs) = Cset.set (List.insert x xs)" |
94 "Cset.insert x (List_Cset.coset xs) = List_Cset.coset (removeAll x xs)" |
86 "Cset.insert x (List_Cset.coset xs) = List_Cset.coset (removeAll x xs)" |
95 by (simp_all add: set_def coset_def) |
87 by (simp_all add: Cset.set_def coset_def) |
96 |
88 |
97 lemma map_set [code]: |
89 lemma map_set [code]: |
98 "Cset.map f (List_Cset.set xs) = List_Cset.set (remdups (List.map f xs))" |
90 "Cset.map f (Cset.set xs) = Cset.set (remdups (List.map f xs))" |
99 by (simp add: set_def) |
91 by (simp add: Cset.set_def) |
100 |
92 |
101 lemma filter_set [code]: |
93 lemma filter_set [code]: |
102 "Cset.filter P (List_Cset.set xs) = List_Cset.set (List.filter P xs)" |
94 "Cset.filter P (Cset.set xs) = Cset.set (List.filter P xs)" |
103 by (simp add: set_def project_set) |
95 by (simp add: Cset.set_def project_set) |
104 |
96 |
105 lemma forall_set [code]: |
97 lemma forall_set [code]: |
106 "Cset.forall P (List_Cset.set xs) \<longleftrightarrow> list_all P xs" |
98 "Cset.forall P (Cset.set xs) \<longleftrightarrow> list_all P xs" |
107 by (simp add: set_def list_all_iff) |
99 by (simp add: Cset.set_def list_all_iff) |
108 |
100 |
109 lemma exists_set [code]: |
101 lemma exists_set [code]: |
110 "Cset.exists P (List_Cset.set xs) \<longleftrightarrow> list_ex P xs" |
102 "Cset.exists P (Cset.set xs) \<longleftrightarrow> list_ex P xs" |
111 by (simp add: set_def list_ex_iff) |
103 by (simp add: Cset.set_def list_ex_iff) |
112 |
104 |
113 lemma card_set [code]: |
105 lemma card_set [code]: |
114 "Cset.card (List_Cset.set xs) = length (remdups xs)" |
106 "Cset.card (Cset.set xs) = length (remdups xs)" |
115 proof - |
107 proof - |
116 have "Finite_Set.card (set (remdups xs)) = length (remdups xs)" |
108 have "Finite_Set.card (set (remdups xs)) = length (remdups xs)" |
117 by (rule distinct_card) simp |
109 by (rule distinct_card) simp |
118 then show ?thesis by (simp add: set_def) |
110 then show ?thesis by (simp add: Cset.set_def) |
119 qed |
111 qed |
120 |
112 |
121 lemma compl_set [simp, code]: |
113 lemma compl_set [simp, code]: |
122 "- List_Cset.set xs = List_Cset.coset xs" |
114 "- Cset.set xs = List_Cset.coset xs" |
123 by (simp add: set_def coset_def) |
115 by (simp add: Cset.set_def coset_def) |
124 |
116 |
125 lemma compl_coset [simp, code]: |
117 lemma compl_coset [simp, code]: |
126 "- List_Cset.coset xs = List_Cset.set xs" |
118 "- List_Cset.coset xs = Cset.set xs" |
127 by (simp add: set_def coset_def) |
119 by (simp add: Cset.set_def coset_def) |
128 |
120 |
129 context complete_lattice |
121 context complete_lattice |
130 begin |
122 begin |
131 |
123 |
132 lemma Infimum_inf [code]: |
124 lemma Infimum_inf [code]: |
133 "Infimum (List_Cset.set As) = foldr inf As top" |
125 "Infimum (Cset.set As) = foldr inf As top" |
134 "Infimum (List_Cset.coset []) = bot" |
126 "Infimum (List_Cset.coset []) = bot" |
135 by (simp_all add: Inf_set_foldr Inf_UNIV) |
127 by (simp_all add: Inf_set_foldr Inf_UNIV) |
136 |
128 |
137 lemma Supremum_sup [code]: |
129 lemma Supremum_sup [code]: |
138 "Supremum (List_Cset.set As) = foldr sup As bot" |
130 "Supremum (Cset.set As) = foldr sup As bot" |
139 "Supremum (List_Cset.coset []) = top" |
131 "Supremum (List_Cset.coset []) = top" |
140 by (simp_all add: Sup_set_foldr Sup_UNIV) |
132 by (simp_all add: Sup_set_foldr Sup_UNIV) |
141 |
133 |
142 end |
134 end |
143 |
135 |
|
136 declare single_code [code del] |
|
137 lemma single_set [code]: |
|
138 "Cset.single a = Cset.set [a]" |
|
139 by(simp add: Cset.single_code) |
|
140 hide_fact (open) single_set |
|
141 |
|
142 lemma bind_set [code]: |
|
143 "Cset.bind (Cset.set xs) f = foldl (\<lambda>A x. sup A (f x)) (Cset.set []) xs" |
|
144 proof(rule sym) |
|
145 show "foldl (\<lambda>A x. sup A (f x)) (Cset.set []) xs = Cset.bind (Cset.set xs) f" |
|
146 by(induct xs rule: rev_induct)(auto simp add: Cset.bind_def Cset.set_def) |
|
147 qed |
|
148 hide_fact (open) bind_set |
|
149 |
|
150 lemma pred_of_cset_set [code]: |
|
151 "pred_of_cset (Cset.set xs) = foldr sup (map Predicate.single xs) bot" |
|
152 proof - |
|
153 have "pred_of_cset (Cset.set xs) = Predicate.Pred (\<lambda>x. x \<in> set xs)" |
|
154 by(auto simp add: Cset.pred_of_cset_def mem_def) |
|
155 moreover have "foldr sup (map Predicate.single xs) bot = \<dots>" |
|
156 by(induct xs)(auto simp add: bot_pred_def simp del: mem_def intro: pred_eqI, simp) |
|
157 ultimately show ?thesis by(simp) |
|
158 qed |
|
159 hide_fact (open) pred_of_cset_set |
144 |
160 |
145 subsection {* Derived operations *} |
161 subsection {* Derived operations *} |
146 |
162 |
147 lemma subset_eq_forall [code]: |
163 lemma subset_eq_forall [code]: |
148 "A \<le> B \<longleftrightarrow> Cset.forall (member B) A" |
164 "A \<le> B \<longleftrightarrow> Cset.forall (member B) A" |
191 ultimately show "inf A (List_Cset.coset xs) = foldr Cset.remove xs A" |
207 ultimately show "inf A (List_Cset.coset xs) = foldr Cset.remove xs A" |
192 by (simp add: foldr_fold) |
208 by (simp add: foldr_fold) |
193 qed |
209 qed |
194 |
210 |
195 lemma subtract_remove [code]: |
211 lemma subtract_remove [code]: |
196 "A - List_Cset.set xs = foldr Cset.remove xs A" |
212 "A - Cset.set xs = foldr Cset.remove xs A" |
197 "A - List_Cset.coset xs = List_Cset.set (List.filter (member A) xs)" |
213 "A - List_Cset.coset xs = Cset.set (List.filter (member A) xs)" |
198 by (simp_all only: diff_eq compl_set compl_coset inter_project) |
214 by (simp_all only: diff_eq compl_set compl_coset inter_project) |
199 |
215 |
200 lemma union_insert [code]: |
216 lemma union_insert [code]: |
201 "sup (List_Cset.set xs) A = foldr Cset.insert xs A" |
217 "sup (Cset.set xs) A = foldr Cset.insert xs A" |
202 "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)" |
218 "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)" |
203 proof - |
219 proof - |
204 have *: "\<And>x::'a. Cset.insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> member)" |
220 have *: "\<And>x::'a. Cset.insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> member)" |
205 by (simp add: fun_eq_iff) |
221 by (simp add: fun_eq_iff) |
206 have "member \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs = |
222 have "member \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs = |
207 fold Set.insert xs \<circ> member" |
223 fold Set.insert xs \<circ> member" |
208 by (rule fold_commute) (simp add: fun_eq_iff) |
224 by (rule fold_commute) (simp add: fun_eq_iff) |
209 then have "fold Set.insert xs (member A) = |
225 then have "fold Set.insert xs (member A) = |
210 member (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs A)" |
226 member (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs A)" |
211 by (simp add: fun_eq_iff) |
227 by (simp add: fun_eq_iff) |
212 then have "sup (List_Cset.set xs) A = fold Cset.insert xs A" |
228 then have "sup (Cset.set xs) A = fold Cset.insert xs A" |
213 by (simp add: union_set *) |
229 by (simp add: union_set *) |
214 moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y" |
230 moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y" |
215 by (auto simp add: * intro: ext) |
231 by (auto simp add: * intro: ext) |
216 ultimately show "sup (List_Cset.set xs) A = foldr Cset.insert xs A" |
232 ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A" |
217 by (simp add: foldr_fold) |
233 by (simp add: foldr_fold) |
218 show "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)" |
234 show "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)" |
219 by (auto simp add: coset_def) |
235 by (auto simp add: coset_def) |
220 qed |
236 qed |
221 |
237 |