43241
|
1 |
|
|
2 |
(* Author: Florian Haftmann, TU Muenchen *)
|
|
3 |
|
|
4 |
header {* implementation of Cset.sets based on lists *}
|
|
5 |
|
|
6 |
theory List_Cset
|
|
7 |
imports Cset
|
|
8 |
begin
|
|
9 |
|
|
10 |
declare mem_def [simp]
|
|
11 |
|
|
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 |
|
|
21 |
definition coset :: "'a list \<Rightarrow> 'a Cset.set" where
|
|
22 |
"coset xs = Set (- set xs)"
|
|
23 |
hide_const (open) coset
|
|
24 |
|
|
25 |
lemma member_coset [simp]:
|
|
26 |
"member (List_Cset.coset xs) = - set xs"
|
|
27 |
by (simp add: coset_def)
|
|
28 |
hide_fact (open) member_coset
|
|
29 |
|
|
30 |
code_datatype List_Cset.set List_Cset.coset
|
|
31 |
|
|
32 |
lemma member_code [code]:
|
|
33 |
"member (List_Cset.set xs) = List.member xs"
|
|
34 |
"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)
|
|
36 |
|
|
37 |
lemma member_image_UNIV [simp]:
|
|
38 |
"member ` UNIV = UNIV"
|
|
39 |
proof -
|
|
40 |
have "\<And>A \<Colon> 'a set. \<exists>B \<Colon> 'a Cset.set. A = member B"
|
|
41 |
proof
|
|
42 |
fix A :: "'a set"
|
|
43 |
show "A = member (Set A)" by simp
|
|
44 |
qed
|
|
45 |
then show ?thesis by (simp add: image_def)
|
|
46 |
qed
|
|
47 |
|
|
48 |
definition (in term_syntax)
|
|
49 |
setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
|
|
50 |
\<Rightarrow> 'a Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
|
|
51 |
[code_unfold]: "setify xs = Code_Evaluation.valtermify List_Cset.set {\<cdot>} xs"
|
|
52 |
|
|
53 |
notation fcomp (infixl "\<circ>>" 60)
|
|
54 |
notation scomp (infixl "\<circ>\<rightarrow>" 60)
|
|
55 |
|
|
56 |
instantiation Cset.set :: (random) random
|
|
57 |
begin
|
|
58 |
|
|
59 |
definition
|
|
60 |
"Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))"
|
|
61 |
|
|
62 |
instance ..
|
|
63 |
|
|
64 |
end
|
|
65 |
|
|
66 |
no_notation fcomp (infixl "\<circ>>" 60)
|
|
67 |
no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
|
|
68 |
|
|
69 |
subsection {* Basic operations *}
|
|
70 |
|
|
71 |
lemma is_empty_set [code]:
|
|
72 |
"Cset.is_empty (List_Cset.set xs) \<longleftrightarrow> List.null xs"
|
|
73 |
by (simp add: is_empty_set null_def)
|
|
74 |
hide_fact (open) is_empty_set
|
|
75 |
|
|
76 |
lemma empty_set [code]:
|
|
77 |
"bot = List_Cset.set []"
|
|
78 |
by (simp add: set_def)
|
|
79 |
hide_fact (open) empty_set
|
|
80 |
|
|
81 |
lemma UNIV_set [code]:
|
|
82 |
"top = List_Cset.coset []"
|
|
83 |
by (simp add: coset_def)
|
|
84 |
hide_fact (open) UNIV_set
|
|
85 |
|
|
86 |
lemma remove_set [code]:
|
|
87 |
"Cset.remove x (List_Cset.set xs) = List_Cset.set (removeAll x xs)"
|
|
88 |
"Cset.remove x (List_Cset.coset xs) = List_Cset.coset (List.insert x xs)"
|
|
89 |
by (simp_all add: set_def coset_def)
|
|
90 |
(metis List.set_insert More_Set.remove_def remove_set_compl)
|
|
91 |
|
|
92 |
lemma insert_set [code]:
|
|
93 |
"Cset.insert x (List_Cset.set xs) = List_Cset.set (List.insert x xs)"
|
|
94 |
"Cset.insert x (List_Cset.coset xs) = List_Cset.coset (removeAll x xs)"
|
|
95 |
by (simp_all add: set_def coset_def)
|
|
96 |
|
|
97 |
lemma map_set [code]:
|
|
98 |
"Cset.map f (List_Cset.set xs) = List_Cset.set (remdups (List.map f xs))"
|
|
99 |
by (simp add: set_def)
|
|
100 |
|
|
101 |
lemma filter_set [code]:
|
|
102 |
"Cset.filter P (List_Cset.set xs) = List_Cset.set (List.filter P xs)"
|
|
103 |
by (simp add: set_def project_set)
|
|
104 |
|
|
105 |
lemma forall_set [code]:
|
|
106 |
"Cset.forall P (List_Cset.set xs) \<longleftrightarrow> list_all P xs"
|
|
107 |
by (simp add: set_def list_all_iff)
|
|
108 |
|
|
109 |
lemma exists_set [code]:
|
|
110 |
"Cset.exists P (List_Cset.set xs) \<longleftrightarrow> list_ex P xs"
|
|
111 |
by (simp add: set_def list_ex_iff)
|
|
112 |
|
|
113 |
lemma card_set [code]:
|
|
114 |
"Cset.card (List_Cset.set xs) = length (remdups xs)"
|
|
115 |
proof -
|
|
116 |
have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
|
|
117 |
by (rule distinct_card) simp
|
|
118 |
then show ?thesis by (simp add: set_def)
|
|
119 |
qed
|
|
120 |
|
|
121 |
lemma compl_set [simp, code]:
|
|
122 |
"- List_Cset.set xs = List_Cset.coset xs"
|
|
123 |
by (simp add: set_def coset_def)
|
|
124 |
|
|
125 |
lemma compl_coset [simp, code]:
|
|
126 |
"- List_Cset.coset xs = List_Cset.set xs"
|
|
127 |
by (simp add: set_def coset_def)
|
|
128 |
|
|
129 |
context complete_lattice
|
|
130 |
begin
|
|
131 |
|
|
132 |
lemma Infimum_inf [code]:
|
|
133 |
"Infimum (List_Cset.set As) = foldr inf As top"
|
|
134 |
"Infimum (List_Cset.coset []) = bot"
|
|
135 |
by (simp_all add: Inf_set_foldr Inf_UNIV)
|
|
136 |
|
|
137 |
lemma Supremum_sup [code]:
|
|
138 |
"Supremum (List_Cset.set As) = foldr sup As bot"
|
|
139 |
"Supremum (List_Cset.coset []) = top"
|
|
140 |
by (simp_all add: Sup_set_foldr Sup_UNIV)
|
|
141 |
|
|
142 |
end
|
|
143 |
|
|
144 |
|
|
145 |
subsection {* Derived operations *}
|
|
146 |
|
|
147 |
lemma subset_eq_forall [code]:
|
|
148 |
"A \<le> B \<longleftrightarrow> Cset.forall (member B) A"
|
|
149 |
by (simp add: subset_eq)
|
|
150 |
|
|
151 |
lemma subset_subset_eq [code]:
|
|
152 |
"A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a Cset.set)"
|
|
153 |
by (fact less_le_not_le)
|
|
154 |
|
|
155 |
instantiation Cset.set :: (type) equal
|
|
156 |
begin
|
|
157 |
|
|
158 |
definition [code]:
|
|
159 |
"HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a Cset.set)"
|
|
160 |
|
|
161 |
instance proof
|
|
162 |
qed (simp add: equal_set_def set_eq [symmetric] Cset.set_eq_iff)
|
|
163 |
|
|
164 |
end
|
|
165 |
|
|
166 |
lemma [code nbe]:
|
|
167 |
"HOL.equal (A :: 'a Cset.set) A \<longleftrightarrow> True"
|
|
168 |
by (fact equal_refl)
|
|
169 |
|
|
170 |
|
|
171 |
subsection {* Functorial operations *}
|
|
172 |
|
|
173 |
lemma inter_project [code]:
|
|
174 |
"inf A (List_Cset.set xs) = List_Cset.set (List.filter (Cset.member A) xs)"
|
|
175 |
"inf A (List_Cset.coset xs) = foldr Cset.remove xs A"
|
|
176 |
proof -
|
|
177 |
show "inf A (List_Cset.set xs) = List_Cset.set (List.filter (member A) xs)"
|
|
178 |
by (simp add: inter project_def set_def)
|
|
179 |
have *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member)"
|
|
180 |
by (simp add: fun_eq_iff More_Set.remove_def)
|
|
181 |
have "member \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs =
|
|
182 |
fold More_Set.remove xs \<circ> member"
|
|
183 |
by (rule fold_commute) (simp add: fun_eq_iff)
|
|
184 |
then have "fold More_Set.remove xs (member A) =
|
|
185 |
member (fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs A)"
|
|
186 |
by (simp add: fun_eq_iff)
|
|
187 |
then have "inf A (List_Cset.coset xs) = fold Cset.remove xs A"
|
|
188 |
by (simp add: Diff_eq [symmetric] minus_set *)
|
|
189 |
moreover have "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> Cset.remove y"
|
|
190 |
by (auto simp add: More_Set.remove_def * intro: ext)
|
|
191 |
ultimately show "inf A (List_Cset.coset xs) = foldr Cset.remove xs A"
|
|
192 |
by (simp add: foldr_fold)
|
|
193 |
qed
|
|
194 |
|
|
195 |
lemma subtract_remove [code]:
|
|
196 |
"A - List_Cset.set xs = foldr Cset.remove xs A"
|
|
197 |
"A - List_Cset.coset xs = List_Cset.set (List.filter (member A) xs)"
|
|
198 |
by (simp_all only: diff_eq compl_set compl_coset inter_project)
|
|
199 |
|
|
200 |
lemma union_insert [code]:
|
|
201 |
"sup (List_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)"
|
|
203 |
proof -
|
|
204 |
have *: "\<And>x::'a. Cset.insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> member)"
|
|
205 |
by (simp add: fun_eq_iff)
|
|
206 |
have "member \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs =
|
|
207 |
fold Set.insert xs \<circ> member"
|
|
208 |
by (rule fold_commute) (simp add: fun_eq_iff)
|
|
209 |
then have "fold Set.insert xs (member A) =
|
|
210 |
member (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs A)"
|
|
211 |
by (simp add: fun_eq_iff)
|
|
212 |
then have "sup (List_Cset.set xs) A = fold Cset.insert xs A"
|
|
213 |
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"
|
|
215 |
by (auto simp add: * intro: ext)
|
|
216 |
ultimately show "sup (List_Cset.set xs) A = foldr Cset.insert xs A"
|
|
217 |
by (simp add: foldr_fold)
|
|
218 |
show "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)"
|
|
219 |
by (auto simp add: coset_def)
|
|
220 |
qed
|
|
221 |
|
|
222 |
end |