|
1 (* Title: HOL/Quotient_Examples/Lift_FSet.thy |
|
2 Author: Brian Huffman, TU Munich |
|
3 *) |
|
4 |
|
5 header {* Lifting and transfer with a finite set type *} |
|
6 |
|
7 theory Lift_FSet |
|
8 imports "~~/src/HOL/Library/Quotient_List" |
|
9 begin |
|
10 |
|
11 subsection {* Equivalence relation and quotient type definition *} |
|
12 |
|
13 definition list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
|
14 where [simp]: "list_eq xs ys \<longleftrightarrow> set xs = set ys" |
|
15 |
|
16 lemma reflp_list_eq: "reflp list_eq" |
|
17 unfolding reflp_def by simp |
|
18 |
|
19 lemma symp_list_eq: "symp list_eq" |
|
20 unfolding symp_def by simp |
|
21 |
|
22 lemma transp_list_eq: "transp list_eq" |
|
23 unfolding transp_def by simp |
|
24 |
|
25 lemma equivp_list_eq: "equivp list_eq" |
|
26 by (intro equivpI reflp_list_eq symp_list_eq transp_list_eq) |
|
27 |
|
28 quotient_type 'a fset = "'a list" / "list_eq" |
|
29 by (rule equivp_list_eq) |
|
30 |
|
31 subsection {* Lifted constant definitions *} |
|
32 |
|
33 lift_definition fnil :: "'a fset" is "[]" |
|
34 by simp |
|
35 |
|
36 lift_definition fcons :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Cons |
|
37 by simp |
|
38 |
|
39 lift_definition fappend :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is append |
|
40 by simp |
|
41 |
|
42 lift_definition fmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" is map |
|
43 by simp |
|
44 |
|
45 lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is filter |
|
46 by simp |
|
47 |
|
48 lift_definition fset :: "'a fset \<Rightarrow> 'a set" is set |
|
49 by simp |
|
50 |
|
51 text {* Constants with nested types (like concat) yield a more |
|
52 complicated proof obligation. *} |
|
53 |
|
54 lemma list_all2_cr_fset: |
|
55 "list_all2 cr_fset xs ys \<longleftrightarrow> map abs_fset xs = ys" |
|
56 unfolding cr_fset_def |
|
57 apply safe |
|
58 apply (erule list_all2_induct, simp, simp) |
|
59 apply (simp add: list_all2_map2 List.list_all2_refl) |
|
60 done |
|
61 |
|
62 lemma abs_fset_eq_iff: "abs_fset xs = abs_fset ys \<longleftrightarrow> list_eq xs ys" |
|
63 using Quotient_rel [OF Quotient_fset] by simp |
|
64 |
|
65 lift_definition fconcat :: "'a fset fset \<Rightarrow> 'a fset" is concat |
|
66 proof - |
|
67 fix xss yss :: "'a list list" |
|
68 assume "(list_all2 cr_fset OO list_eq OO (list_all2 cr_fset)\<inverse>\<inverse>) xss yss" |
|
69 then obtain uss vss where |
|
70 "list_all2 cr_fset xss uss" and "list_eq uss vss" and |
|
71 "list_all2 cr_fset yss vss" by clarsimp |
|
72 hence "list_eq (map abs_fset xss) (map abs_fset yss)" |
|
73 unfolding list_all2_cr_fset by simp |
|
74 thus "list_eq (concat xss) (concat yss)" |
|
75 apply (simp add: set_eq_iff image_def) |
|
76 apply safe |
|
77 apply (rename_tac xs, drule_tac x="abs_fset xs" in spec) |
|
78 apply (drule iffD1, fast, clarsimp simp add: abs_fset_eq_iff, fast) |
|
79 apply (rename_tac xs, drule_tac x="abs_fset xs" in spec) |
|
80 apply (drule iffD2, fast, clarsimp simp add: abs_fset_eq_iff, fast) |
|
81 done |
|
82 qed |
|
83 |
|
84 text {* Note that the generated transfer rule contains a composition |
|
85 of relations. The transfer rule is not yet very useful in this form. *} |
|
86 |
|
87 lemma "(list_all2 cr_fset OO cr_fset ===> cr_fset) concat fconcat" |
|
88 by (fact fconcat.transfer) |
|
89 |
|
90 |
|
91 subsection {* Using transfer with type @{text "fset"} *} |
|
92 |
|
93 text {* The correspondence relation @{text "cr_fset"} can only relate |
|
94 @{text "list"} and @{text "fset"} types with the same element type. |
|
95 To relate nested types like @{text "'a list list"} and |
|
96 @{text "'a fset fset"}, we define a parameterized version of the |
|
97 correspondence relation, @{text "cr_fset'"}. *} |
|
98 |
|
99 definition cr_fset' :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b fset \<Rightarrow> bool" |
|
100 where "cr_fset' R = list_all2 R OO cr_fset" |
|
101 |
|
102 lemma right_unique_cr_fset' [transfer_rule]: |
|
103 "right_unique A \<Longrightarrow> right_unique (cr_fset' A)" |
|
104 unfolding cr_fset'_def |
|
105 by (intro right_unique_OO right_unique_list_all2 fset.right_unique) |
|
106 |
|
107 lemma right_total_cr_fset' [transfer_rule]: |
|
108 "right_total A \<Longrightarrow> right_total (cr_fset' A)" |
|
109 unfolding cr_fset'_def |
|
110 by (intro right_total_OO right_total_list_all2 fset.right_total) |
|
111 |
|
112 lemma bi_total_cr_fset' [transfer_rule]: |
|
113 "bi_total A \<Longrightarrow> bi_total (cr_fset' A)" |
|
114 unfolding cr_fset'_def |
|
115 by (intro bi_total_OO bi_total_list_all2 fset.bi_total) |
|
116 |
|
117 text {* Transfer rules for @{text "cr_fset'"} can be derived from the |
|
118 existing transfer rules for @{text "cr_fset"} together with the |
|
119 transfer rules for the polymorphic raw constants. *} |
|
120 |
|
121 text {* Note that the proofs below all have a similar structure and |
|
122 could potentially be automated. *} |
|
123 |
|
124 lemma fnil_transfer [transfer_rule]: |
|
125 "(cr_fset' A) [] fnil" |
|
126 unfolding cr_fset'_def |
|
127 apply (rule relcomppI) |
|
128 apply (rule Nil_transfer) |
|
129 apply (rule fnil.transfer) |
|
130 done |
|
131 |
|
132 lemma fcons_transfer [transfer_rule]: |
|
133 "(A ===> cr_fset' A ===> cr_fset' A) Cons fcons" |
|
134 unfolding cr_fset'_def |
|
135 apply (intro fun_relI) |
|
136 apply (elim relcomppE) |
|
137 apply (rule relcomppI) |
|
138 apply (erule (1) Cons_transfer [THEN fun_relD, THEN fun_relD]) |
|
139 apply (erule fcons.transfer [THEN fun_relD, THEN fun_relD, OF refl]) |
|
140 done |
|
141 |
|
142 lemma fappend_transfer [transfer_rule]: |
|
143 "(cr_fset' A ===> cr_fset' A ===> cr_fset' A) append fappend" |
|
144 unfolding cr_fset'_def |
|
145 apply (intro fun_relI) |
|
146 apply (elim relcomppE) |
|
147 apply (rule relcomppI) |
|
148 apply (erule (1) append_transfer [THEN fun_relD, THEN fun_relD]) |
|
149 apply (erule (1) fappend.transfer [THEN fun_relD, THEN fun_relD]) |
|
150 done |
|
151 |
|
152 lemma fmap_transfer [transfer_rule]: |
|
153 "((A ===> B) ===> cr_fset' A ===> cr_fset' B) map fmap" |
|
154 unfolding cr_fset'_def |
|
155 apply (intro fun_relI) |
|
156 apply (elim relcomppE) |
|
157 apply (rule relcomppI) |
|
158 apply (erule (1) map_transfer [THEN fun_relD, THEN fun_relD]) |
|
159 apply (erule fmap.transfer [THEN fun_relD, THEN fun_relD, OF refl]) |
|
160 done |
|
161 |
|
162 lemma ffilter_transfer [transfer_rule]: |
|
163 "((A ===> op =) ===> cr_fset' A ===> cr_fset' A) filter ffilter" |
|
164 unfolding cr_fset'_def |
|
165 apply (intro fun_relI) |
|
166 apply (elim relcomppE) |
|
167 apply (rule relcomppI) |
|
168 apply (erule (1) filter_transfer [THEN fun_relD, THEN fun_relD]) |
|
169 apply (erule ffilter.transfer [THEN fun_relD, THEN fun_relD, OF refl]) |
|
170 done |
|
171 |
|
172 lemma fset_transfer [transfer_rule]: |
|
173 "(cr_fset' A ===> set_rel A) set fset" |
|
174 unfolding cr_fset'_def |
|
175 apply (intro fun_relI) |
|
176 apply (elim relcomppE) |
|
177 apply (drule fset.transfer [THEN fun_relD]) |
|
178 apply (erule subst) |
|
179 apply (erule set_transfer [THEN fun_relD]) |
|
180 done |
|
181 |
|
182 lemma fconcat_transfer [transfer_rule]: |
|
183 "(cr_fset' (cr_fset' A) ===> cr_fset' A) concat fconcat" |
|
184 unfolding cr_fset'_def |
|
185 unfolding list_all2_OO |
|
186 apply (intro fun_relI) |
|
187 apply (elim relcomppE) |
|
188 apply (rule relcomppI) |
|
189 apply (erule concat_transfer [THEN fun_relD]) |
|
190 apply (rule fconcat.transfer [THEN fun_relD]) |
|
191 apply (erule (1) relcomppI) |
|
192 done |
|
193 |
|
194 lemma list_eq_transfer [transfer_rule]: |
|
195 assumes [transfer_rule]: "bi_unique A" |
|
196 shows "(list_all2 A ===> list_all2 A ===> op =) list_eq list_eq" |
|
197 unfolding list_eq_def [abs_def] by transfer_prover |
|
198 |
|
199 lemma fset_eq_transfer [transfer_rule]: |
|
200 assumes "bi_unique A" |
|
201 shows "(cr_fset' A ===> cr_fset' A ===> op =) list_eq (op =)" |
|
202 unfolding cr_fset'_def |
|
203 apply (intro fun_relI) |
|
204 apply (elim relcomppE) |
|
205 apply (rule trans) |
|
206 apply (erule (1) list_eq_transfer [THEN fun_relD, THEN fun_relD, OF assms]) |
|
207 apply (erule (1) fset.rel_eq_transfer [THEN fun_relD, THEN fun_relD]) |
|
208 done |
|
209 |
|
210 text {* We don't need the original transfer rules any more: *} |
|
211 |
|
212 lemmas [transfer_rule del] = |
|
213 fset.bi_total fset.right_total fset.right_unique |
|
214 fnil.transfer fcons.transfer fappend.transfer fmap.transfer |
|
215 ffilter.transfer fset.transfer fconcat.transfer fset.rel_eq_transfer |
|
216 |
|
217 subsection {* Transfer examples *} |
|
218 |
|
219 text {* The @{text "transfer"} method replaces equality on @{text |
|
220 "fset"} with the @{text "list_eq"} relation on lists, which is |
|
221 logically equivalent. *} |
|
222 |
|
223 lemma "fmap f (fmap g xs) = fmap (f \<circ> g) xs" |
|
224 apply transfer |
|
225 apply simp |
|
226 done |
|
227 |
|
228 text {* The @{text "transfer'"} variant can replace equality on @{text |
|
229 "fset"} with equality on @{text "list"}, which is logically stronger |
|
230 but sometimes more convenient. *} |
|
231 |
|
232 lemma "fmap f (fmap g xs) = fmap (f \<circ> g) xs" |
|
233 apply transfer' |
|
234 apply (rule map_map) |
|
235 done |
|
236 |
|
237 lemma "ffilter p (fmap f xs) = fmap f (ffilter (p \<circ> f) xs)" |
|
238 apply transfer' |
|
239 apply (rule filter_map) |
|
240 done |
|
241 |
|
242 lemma "ffilter p (ffilter q xs) = ffilter (\<lambda>x. q x \<and> p x) xs" |
|
243 apply transfer' |
|
244 apply (rule filter_filter) |
|
245 done |
|
246 |
|
247 lemma "fset (fcons x xs) = insert x (fset xs)" |
|
248 apply transfer |
|
249 apply (rule set.simps) |
|
250 done |
|
251 |
|
252 lemma "fset (fappend xs ys) = fset xs \<union> fset ys" |
|
253 apply transfer |
|
254 apply (rule set_append) |
|
255 done |
|
256 |
|
257 lemma "fset (fconcat xss) = (\<Union>xs\<in>fset xss. fset xs)" |
|
258 apply transfer |
|
259 apply (rule set_concat) |
|
260 done |
|
261 |
|
262 lemma "\<forall>x\<in>fset xs. f x = g x \<Longrightarrow> fmap f xs = fmap g xs" |
|
263 apply transfer |
|
264 apply (simp cong: map_cong del: set_map) |
|
265 done |
|
266 |
|
267 lemma "fnil = fconcat xss \<longleftrightarrow> (\<forall>xs\<in>fset xss. xs = fnil)" |
|
268 apply transfer |
|
269 apply simp |
|
270 done |
|
271 |
|
272 lemma "fconcat (fmap (\<lambda>x. fcons x fnil) xs) = xs" |
|
273 apply transfer' |
|
274 apply simp |
|
275 done |
|
276 |
|
277 lemma concat_map_concat: "concat (map concat xsss) = concat (concat xsss)" |
|
278 by (induct xsss, simp_all) |
|
279 |
|
280 lemma "fconcat (fmap fconcat xss) = fconcat (fconcat xss)" |
|
281 apply transfer' |
|
282 apply (rule concat_map_concat) |
|
283 done |
|
284 |
|
285 end |