1 |
|
2 (* Author: Andreas Lochbihler, Uni Karlsruhe *) |
|
3 |
|
4 header {* Almost everywhere constant functions *} |
|
5 |
|
6 theory Fin_Fun |
|
7 imports Main Infinite_Set Enum |
|
8 begin |
|
9 |
|
10 text {* |
|
11 This theory defines functions which are constant except for finitely |
|
12 many points (FinFun) and introduces a type finfin along with a |
|
13 number of operators for them. The code generator is set up such that |
|
14 such functions can be represented as data in the generated code and |
|
15 all operators are executable. |
|
16 |
|
17 For details, see Formalising FinFuns - Generating Code for Functions as Data by A. Lochbihler in TPHOLs 2009. |
|
18 *} |
|
19 |
|
20 |
|
21 subsection {* The @{text "map_default"} operation *} |
|
22 |
|
23 definition map_default :: "'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
|
24 where "map_default b f a \<equiv> case f a of None \<Rightarrow> b | Some b' \<Rightarrow> b'" |
|
25 |
|
26 lemma map_default_delete [simp]: |
|
27 "map_default b (f(a := None)) = (map_default b f)(a := b)" |
|
28 by(simp add: map_default_def expand_fun_eq) |
|
29 |
|
30 lemma map_default_insert: |
|
31 "map_default b (f(a \<mapsto> b')) = (map_default b f)(a := b')" |
|
32 by(simp add: map_default_def expand_fun_eq) |
|
33 |
|
34 lemma map_default_empty [simp]: "map_default b empty = (\<lambda>a. b)" |
|
35 by(simp add: expand_fun_eq map_default_def) |
|
36 |
|
37 lemma map_default_inject: |
|
38 fixes g g' :: "'a \<rightharpoonup> 'b" |
|
39 assumes infin_eq: "\<not> finite (UNIV :: 'a set) \<or> b = b'" |
|
40 and fin: "finite (dom g)" and b: "b \<notin> ran g" |
|
41 and fin': "finite (dom g')" and b': "b' \<notin> ran g'" |
|
42 and eq': "map_default b g = map_default b' g'" |
|
43 shows "b = b'" "g = g'" |
|
44 proof - |
|
45 from infin_eq show bb': "b = b'" |
|
46 proof |
|
47 assume infin: "\<not> finite (UNIV :: 'a set)" |
|
48 from fin fin' have "finite (dom g \<union> dom g')" by auto |
|
49 with infin have "UNIV - (dom g \<union> dom g') \<noteq> {}" by(auto dest: finite_subset) |
|
50 then obtain a where a: "a \<notin> dom g \<union> dom g'" by auto |
|
51 hence "map_default b g a = b" "map_default b' g' a = b'" by(auto simp add: map_default_def) |
|
52 with eq' show "b = b'" by simp |
|
53 qed |
|
54 |
|
55 show "g = g'" |
|
56 proof |
|
57 fix x |
|
58 show "g x = g' x" |
|
59 proof(cases "g x") |
|
60 case None |
|
61 hence "map_default b g x = b" by(simp add: map_default_def) |
|
62 with bb' eq' have "map_default b' g' x = b'" by simp |
|
63 with b' have "g' x = None" by(simp add: map_default_def ran_def split: option.split_asm) |
|
64 with None show ?thesis by simp |
|
65 next |
|
66 case (Some c) |
|
67 with b have cb: "c \<noteq> b" by(auto simp add: ran_def) |
|
68 moreover from Some have "map_default b g x = c" by(simp add: map_default_def) |
|
69 with eq' have "map_default b' g' x = c" by simp |
|
70 ultimately have "g' x = Some c" using b' bb' by(auto simp add: map_default_def split: option.splits) |
|
71 with Some show ?thesis by simp |
|
72 qed |
|
73 qed |
|
74 qed |
|
75 |
|
76 subsection {* The finfun type *} |
|
77 |
|
78 typedef ('a,'b) finfun = "{f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}" |
|
79 proof - |
|
80 have "\<exists>f. finite {x. f x \<noteq> undefined}" |
|
81 proof |
|
82 show "finite {x. (\<lambda>y. undefined) x \<noteq> undefined}" by auto |
|
83 qed |
|
84 then show ?thesis by auto |
|
85 qed |
|
86 |
|
87 syntax |
|
88 "finfun" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ \<Rightarrow>\<^isub>f /_)" [22, 21] 21) |
|
89 |
|
90 lemma fun_upd_finfun: "y(a := b) \<in> finfun \<longleftrightarrow> y \<in> finfun" |
|
91 proof - |
|
92 { fix b' |
|
93 have "finite {a'. (y(a := b)) a' \<noteq> b'} = finite {a'. y a' \<noteq> b'}" |
|
94 proof(cases "b = b'") |
|
95 case True |
|
96 hence "{a'. (y(a := b)) a' \<noteq> b'} = {a'. y a' \<noteq> b'} - {a}" by auto |
|
97 thus ?thesis by simp |
|
98 next |
|
99 case False |
|
100 hence "{a'. (y(a := b)) a' \<noteq> b'} = insert a {a'. y a' \<noteq> b'}" by auto |
|
101 thus ?thesis by simp |
|
102 qed } |
|
103 thus ?thesis unfolding finfun_def by blast |
|
104 qed |
|
105 |
|
106 lemma const_finfun: "(\<lambda>x. a) \<in> finfun" |
|
107 by(auto simp add: finfun_def) |
|
108 |
|
109 lemma finfun_left_compose: |
|
110 assumes "y \<in> finfun" |
|
111 shows "g \<circ> y \<in> finfun" |
|
112 proof - |
|
113 from assms obtain b where "finite {a. y a \<noteq> b}" |
|
114 unfolding finfun_def by blast |
|
115 hence "finite {c. g (y c) \<noteq> g b}" |
|
116 proof(induct x\<equiv>"{a. y a \<noteq> b}" arbitrary: y) |
|
117 case empty |
|
118 hence "y = (\<lambda>a. b)" by(auto intro: ext) |
|
119 thus ?case by(simp) |
|
120 next |
|
121 case (insert x F) |
|
122 note IH = `\<And>y. F = {a. y a \<noteq> b} \<Longrightarrow> finite {c. g (y c) \<noteq> g b}` |
|
123 from `insert x F = {a. y a \<noteq> b}` `x \<notin> F` |
|
124 have F: "F = {a. (y(x := b)) a \<noteq> b}" by(auto) |
|
125 show ?case |
|
126 proof(cases "g (y x) = g b") |
|
127 case True |
|
128 hence "{c. g ((y(x := b)) c) \<noteq> g b} = {c. g (y c) \<noteq> g b}" by auto |
|
129 with IH[OF F] show ?thesis by simp |
|
130 next |
|
131 case False |
|
132 hence "{c. g (y c) \<noteq> g b} = insert x {c. g ((y(x := b)) c) \<noteq> g b}" by auto |
|
133 with IH[OF F] show ?thesis by(simp) |
|
134 qed |
|
135 qed |
|
136 thus ?thesis unfolding finfun_def by auto |
|
137 qed |
|
138 |
|
139 lemma assumes "y \<in> finfun" |
|
140 shows fst_finfun: "fst \<circ> y \<in> finfun" |
|
141 and snd_finfun: "snd \<circ> y \<in> finfun" |
|
142 proof - |
|
143 from assms obtain b c where bc: "finite {a. y a \<noteq> (b, c)}" |
|
144 unfolding finfun_def by auto |
|
145 have "{a. fst (y a) \<noteq> b} \<subseteq> {a. y a \<noteq> (b, c)}" |
|
146 and "{a. snd (y a) \<noteq> c} \<subseteq> {a. y a \<noteq> (b, c)}" by auto |
|
147 hence "finite {a. fst (y a) \<noteq> b}" |
|
148 and "finite {a. snd (y a) \<noteq> c}" using bc by(auto intro: finite_subset) |
|
149 thus "fst \<circ> y \<in> finfun" "snd \<circ> y \<in> finfun" |
|
150 unfolding finfun_def by auto |
|
151 qed |
|
152 |
|
153 lemma map_of_finfun: "map_of xs \<in> finfun" |
|
154 unfolding finfun_def |
|
155 by(induct xs)(auto simp add: Collect_neg_eq Collect_conj_eq Collect_imp_eq intro: finite_subset) |
|
156 |
|
157 lemma Diag_finfun: "(\<lambda>x. (f x, g x)) \<in> finfun \<longleftrightarrow> f \<in> finfun \<and> g \<in> finfun" |
|
158 by(auto intro: finite_subset simp add: Collect_neg_eq Collect_imp_eq Collect_conj_eq finfun_def) |
|
159 |
|
160 lemma finfun_right_compose: |
|
161 assumes g: "g \<in> finfun" and inj: "inj f" |
|
162 shows "g o f \<in> finfun" |
|
163 proof - |
|
164 from g obtain b where b: "finite {a. g a \<noteq> b}" unfolding finfun_def by blast |
|
165 moreover have "f ` {a. g (f a) \<noteq> b} \<subseteq> {a. g a \<noteq> b}" by auto |
|
166 moreover from inj have "inj_on f {a. g (f a) \<noteq> b}" by(rule subset_inj_on) blast |
|
167 ultimately have "finite {a. g (f a) \<noteq> b}" |
|
168 by(blast intro: finite_imageD[where f=f] finite_subset) |
|
169 thus ?thesis unfolding finfun_def by auto |
|
170 qed |
|
171 |
|
172 lemma finfun_curry: |
|
173 assumes fin: "f \<in> finfun" |
|
174 shows "curry f \<in> finfun" "curry f a \<in> finfun" |
|
175 proof - |
|
176 from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast |
|
177 moreover have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force) |
|
178 hence "{a. curry f a \<noteq> (\<lambda>b. c)} = fst ` {ab. f ab \<noteq> c}" |
|
179 by(auto simp add: curry_def expand_fun_eq) |
|
180 ultimately have "finite {a. curry f a \<noteq> (\<lambda>b. c)}" by simp |
|
181 thus "curry f \<in> finfun" unfolding finfun_def by blast |
|
182 |
|
183 have "snd ` {ab. f ab \<noteq> c} = {b. \<exists>a. f (a, b) \<noteq> c}" by(force) |
|
184 hence "{b. f (a, b) \<noteq> c} \<subseteq> snd ` {ab. f ab \<noteq> c}" by auto |
|
185 hence "finite {b. f (a, b) \<noteq> c}" by(rule finite_subset)(rule finite_imageI[OF c]) |
|
186 thus "curry f a \<in> finfun" unfolding finfun_def by auto |
|
187 qed |
|
188 |
|
189 lemmas finfun_simp = |
|
190 fst_finfun snd_finfun Abs_finfun_inverse Rep_finfun_inverse Abs_finfun_inject Rep_finfun_inject Diag_finfun finfun_curry |
|
191 lemmas finfun_iff = const_finfun fun_upd_finfun Rep_finfun map_of_finfun |
|
192 lemmas finfun_intro = finfun_left_compose fst_finfun snd_finfun |
|
193 |
|
194 lemma Abs_finfun_inject_finite: |
|
195 fixes x y :: "'a \<Rightarrow> 'b" |
|
196 assumes fin: "finite (UNIV :: 'a set)" |
|
197 shows "Abs_finfun x = Abs_finfun y \<longleftrightarrow> x = y" |
|
198 proof |
|
199 assume "Abs_finfun x = Abs_finfun y" |
|
200 moreover have "x \<in> finfun" "y \<in> finfun" unfolding finfun_def |
|
201 by(auto intro: finite_subset[OF _ fin]) |
|
202 ultimately show "x = y" by(simp add: Abs_finfun_inject) |
|
203 qed simp |
|
204 |
|
205 lemma Abs_finfun_inject_finite_class: |
|
206 fixes x y :: "('a :: finite) \<Rightarrow> 'b" |
|
207 shows "Abs_finfun x = Abs_finfun y \<longleftrightarrow> x = y" |
|
208 using finite_UNIV |
|
209 by(simp add: Abs_finfun_inject_finite) |
|
210 |
|
211 lemma Abs_finfun_inj_finite: |
|
212 assumes fin: "finite (UNIV :: 'a set)" |
|
213 shows "inj (Abs_finfun :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b)" |
|
214 proof(rule inj_onI) |
|
215 fix x y :: "'a \<Rightarrow> 'b" |
|
216 assume "Abs_finfun x = Abs_finfun y" |
|
217 moreover have "x \<in> finfun" "y \<in> finfun" unfolding finfun_def |
|
218 by(auto intro: finite_subset[OF _ fin]) |
|
219 ultimately show "x = y" by(simp add: Abs_finfun_inject) |
|
220 qed |
|
221 |
|
222 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro] |
|
223 |
|
224 lemma Abs_finfun_inverse_finite: |
|
225 fixes x :: "'a \<Rightarrow> 'b" |
|
226 assumes fin: "finite (UNIV :: 'a set)" |
|
227 shows "Rep_finfun (Abs_finfun x) = x" |
|
228 proof - |
|
229 from fin have "x \<in> finfun" |
|
230 by(auto simp add: finfun_def intro: finite_subset) |
|
231 thus ?thesis by simp |
|
232 qed |
|
233 |
|
234 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del] |
|
235 |
|
236 lemma Abs_finfun_inverse_finite_class: |
|
237 fixes x :: "('a :: finite) \<Rightarrow> 'b" |
|
238 shows "Rep_finfun (Abs_finfun x) = x" |
|
239 using finite_UNIV by(simp add: Abs_finfun_inverse_finite) |
|
240 |
|
241 lemma finfun_eq_finite_UNIV: "finite (UNIV :: 'a set) \<Longrightarrow> (finfun :: ('a \<Rightarrow> 'b) set) = UNIV" |
|
242 unfolding finfun_def by(auto intro: finite_subset) |
|
243 |
|
244 lemma finfun_finite_UNIV_class: "finfun = (UNIV :: ('a :: finite \<Rightarrow> 'b) set)" |
|
245 by(simp add: finfun_eq_finite_UNIV) |
|
246 |
|
247 lemma map_default_in_finfun: |
|
248 assumes fin: "finite (dom f)" |
|
249 shows "map_default b f \<in> finfun" |
|
250 unfolding finfun_def |
|
251 proof(intro CollectI exI) |
|
252 from fin show "finite {a. map_default b f a \<noteq> b}" |
|
253 by(auto simp add: map_default_def dom_def Collect_conj_eq split: option.splits) |
|
254 qed |
|
255 |
|
256 lemma finfun_cases_map_default: |
|
257 obtains b g where "f = Abs_finfun (map_default b g)" "finite (dom g)" "b \<notin> ran g" |
|
258 proof - |
|
259 obtain y where f: "f = Abs_finfun y" and y: "y \<in> finfun" by(cases f) |
|
260 from y obtain b where b: "finite {a. y a \<noteq> b}" unfolding finfun_def by auto |
|
261 let ?g = "(\<lambda>a. if y a = b then None else Some (y a))" |
|
262 have "map_default b ?g = y" by(simp add: expand_fun_eq map_default_def) |
|
263 with f have "f = Abs_finfun (map_default b ?g)" by simp |
|
264 moreover from b have "finite (dom ?g)" by(auto simp add: dom_def) |
|
265 moreover have "b \<notin> ran ?g" by(auto simp add: ran_def) |
|
266 ultimately show ?thesis by(rule that) |
|
267 qed |
|
268 |
|
269 |
|
270 subsection {* Kernel functions for type @{typ "'a \<Rightarrow>\<^isub>f 'b"} *} |
|
271 |
|
272 definition finfun_const :: "'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("\<lambda>\<^isup>f/ _" [0] 1) |
|
273 where [code del]: "(\<lambda>\<^isup>f b) = Abs_finfun (\<lambda>x. b)" |
|
274 |
|
275 definition finfun_update :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("_'(\<^sup>f/ _ := _')" [1000,0,0] 1000) |
|
276 where [code del]: "f(\<^sup>fa := b) = Abs_finfun ((Rep_finfun f)(a := b))" |
|
277 |
|
278 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro] |
|
279 |
|
280 lemma finfun_update_twist: "a \<noteq> a' \<Longrightarrow> f(\<^sup>f a := b)(\<^sup>f a' := b') = f(\<^sup>f a' := b')(\<^sup>f a := b)" |
|
281 by(simp add: finfun_update_def fun_upd_twist) |
|
282 |
|
283 lemma finfun_update_twice [simp]: |
|
284 "finfun_update (finfun_update f a b) a b' = finfun_update f a b'" |
|
285 by(simp add: finfun_update_def) |
|
286 |
|
287 lemma finfun_update_const_same: "(\<lambda>\<^isup>f b)(\<^sup>f a := b) = (\<lambda>\<^isup>f b)" |
|
288 by(simp add: finfun_update_def finfun_const_def expand_fun_eq) |
|
289 |
|
290 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del] |
|
291 |
|
292 subsection {* Code generator setup *} |
|
293 |
|
294 definition finfun_update_code :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("_'(\<^sup>f\<^sup>c/ _ := _')" [1000,0,0] 1000) |
|
295 where [simp, code del]: "finfun_update_code = finfun_update" |
|
296 |
|
297 code_datatype finfun_const finfun_update_code |
|
298 |
|
299 lemma finfun_update_const_code [code]: |
|
300 "(\<lambda>\<^isup>f b)(\<^sup>f a := b') = (if b = b' then (\<lambda>\<^isup>f b) else finfun_update_code (\<lambda>\<^isup>f b) a b')" |
|
301 by(simp add: finfun_update_const_same) |
|
302 |
|
303 lemma finfun_update_update_code [code]: |
|
304 "(finfun_update_code f a b)(\<^sup>f a' := b') = (if a = a' then f(\<^sup>f a := b') else finfun_update_code (f(\<^sup>f a' := b')) a b)" |
|
305 by(simp add: finfun_update_twist) |
|
306 |
|
307 |
|
308 subsection {* Setup for quickcheck *} |
|
309 |
|
310 notation fcomp (infixl "o>" 60) |
|
311 notation scomp (infixl "o\<rightarrow>" 60) |
|
312 |
|
313 definition (in term_syntax) valtermify_finfun_const :: |
|
314 "'b\<Colon>typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> ('a\<Colon>typerep \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Evaluation.term)" where |
|
315 "valtermify_finfun_const y = Code_Evaluation.valtermify finfun_const {\<cdot>} y" |
|
316 |
|
317 definition (in term_syntax) valtermify_finfun_update_code :: |
|
318 "'a\<Colon>typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> 'b\<Colon>typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Evaluation.term)" where |
|
319 "valtermify_finfun_update_code x y f = Code_Evaluation.valtermify finfun_update_code {\<cdot>} f {\<cdot>} x {\<cdot>} y" |
|
320 |
|
321 instantiation finfun :: (random, random) random |
|
322 begin |
|
323 |
|
324 primrec random_finfun_aux :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed" where |
|
325 "random_finfun_aux 0 j = Quickcheck.collapse (Random.select_weight |
|
326 [(1, Quickcheck.random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])" |
|
327 | "random_finfun_aux (Suc_code_numeral i) j = Quickcheck.collapse (Random.select_weight |
|
328 [(Suc_code_numeral i, Quickcheck.random j o\<rightarrow> (\<lambda>x. Quickcheck.random j o\<rightarrow> (\<lambda>y. random_finfun_aux i j o\<rightarrow> (\<lambda>f. Pair (valtermify_finfun_update_code x y f))))), |
|
329 (1, Quickcheck.random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])" |
|
330 |
|
331 definition |
|
332 "Quickcheck.random i = random_finfun_aux i i" |
|
333 |
|
334 instance .. |
|
335 |
|
336 end |
|
337 |
|
338 lemma random_finfun_aux_code [code]: |
|
339 "random_finfun_aux i j = Quickcheck.collapse (Random.select_weight |
|
340 [(i, Quickcheck.random j o\<rightarrow> (\<lambda>x. Quickcheck.random j o\<rightarrow> (\<lambda>y. random_finfun_aux (i - 1) j o\<rightarrow> (\<lambda>f. Pair (valtermify_finfun_update_code x y f))))), |
|
341 (1, Quickcheck.random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])" |
|
342 apply (cases i rule: code_numeral.exhaust) |
|
343 apply (simp_all only: random_finfun_aux.simps code_numeral_zero_minus_one Suc_code_numeral_minus_one) |
|
344 apply (subst select_weight_cons_zero) apply (simp only:) |
|
345 done |
|
346 |
|
347 no_notation fcomp (infixl "o>" 60) |
|
348 no_notation scomp (infixl "o\<rightarrow>" 60) |
|
349 |
|
350 |
|
351 subsection {* @{text "finfun_update"} as instance of @{text "fun_left_comm"} *} |
|
352 |
|
353 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro] |
|
354 |
|
355 interpretation finfun_update: fun_left_comm "\<lambda>a f. f(\<^sup>f a :: 'a := b')" |
|
356 proof |
|
357 fix a' a :: 'a |
|
358 fix b |
|
359 have "(Rep_finfun b)(a := b', a' := b') = (Rep_finfun b)(a' := b', a := b')" |
|
360 by(cases "a = a'")(auto simp add: fun_upd_twist) |
|
361 thus "b(\<^sup>f a := b')(\<^sup>f a' := b') = b(\<^sup>f a' := b')(\<^sup>f a := b')" |
|
362 by(auto simp add: finfun_update_def fun_upd_twist) |
|
363 qed |
|
364 |
|
365 lemma fold_finfun_update_finite_univ: |
|
366 assumes fin: "finite (UNIV :: 'a set)" |
|
367 shows "fold (\<lambda>a f. f(\<^sup>f a := b')) (\<lambda>\<^isup>f b) (UNIV :: 'a set) = (\<lambda>\<^isup>f b')" |
|
368 proof - |
|
369 { fix A :: "'a set" |
|
370 from fin have "finite A" by(auto intro: finite_subset) |
|
371 hence "fold (\<lambda>a f. f(\<^sup>f a := b')) (\<lambda>\<^isup>f b) A = Abs_finfun (\<lambda>a. if a \<in> A then b' else b)" |
|
372 proof(induct) |
|
373 case (insert x F) |
|
374 have "(\<lambda>a. if a = x then b' else (if a \<in> F then b' else b)) = (\<lambda>a. if a = x \<or> a \<in> F then b' else b)" |
|
375 by(auto intro: ext) |
|
376 with insert show ?case |
|
377 by(simp add: finfun_const_def fun_upd_def)(simp add: finfun_update_def Abs_finfun_inverse_finite[OF fin] fun_upd_def) |
|
378 qed(simp add: finfun_const_def) } |
|
379 thus ?thesis by(simp add: finfun_const_def) |
|
380 qed |
|
381 |
|
382 |
|
383 subsection {* Default value for FinFuns *} |
|
384 |
|
385 definition finfun_default_aux :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b" |
|
386 where [code del]: "finfun_default_aux f = (if finite (UNIV :: 'a set) then undefined else THE b. finite {a. f a \<noteq> b})" |
|
387 |
|
388 lemma finfun_default_aux_infinite: |
|
389 fixes f :: "'a \<Rightarrow> 'b" |
|
390 assumes infin: "infinite (UNIV :: 'a set)" |
|
391 and fin: "finite {a. f a \<noteq> b}" |
|
392 shows "finfun_default_aux f = b" |
|
393 proof - |
|
394 let ?B = "{a. f a \<noteq> b}" |
|
395 from fin have "(THE b. finite {a. f a \<noteq> b}) = b" |
|
396 proof(rule the_equality) |
|
397 fix b' |
|
398 assume "finite {a. f a \<noteq> b'}" (is "finite ?B'") |
|
399 with infin fin have "UNIV - (?B' \<union> ?B) \<noteq> {}" by(auto dest: finite_subset) |
|
400 then obtain a where a: "a \<notin> ?B' \<union> ?B" by auto |
|
401 thus "b' = b" by auto |
|
402 qed |
|
403 thus ?thesis using infin by(simp add: finfun_default_aux_def) |
|
404 qed |
|
405 |
|
406 |
|
407 lemma finite_finfun_default_aux: |
|
408 fixes f :: "'a \<Rightarrow> 'b" |
|
409 assumes fin: "f \<in> finfun" |
|
410 shows "finite {a. f a \<noteq> finfun_default_aux f}" |
|
411 proof(cases "finite (UNIV :: 'a set)") |
|
412 case True thus ?thesis using fin |
|
413 by(auto simp add: finfun_def finfun_default_aux_def intro: finite_subset) |
|
414 next |
|
415 case False |
|
416 from fin obtain b where b: "finite {a. f a \<noteq> b}" (is "finite ?B") |
|
417 unfolding finfun_def by blast |
|
418 with False show ?thesis by(simp add: finfun_default_aux_infinite) |
|
419 qed |
|
420 |
|
421 lemma finfun_default_aux_update_const: |
|
422 fixes f :: "'a \<Rightarrow> 'b" |
|
423 assumes fin: "f \<in> finfun" |
|
424 shows "finfun_default_aux (f(a := b)) = finfun_default_aux f" |
|
425 proof(cases "finite (UNIV :: 'a set)") |
|
426 case False |
|
427 from fin obtain b' where b': "finite {a. f a \<noteq> b'}" unfolding finfun_def by blast |
|
428 hence "finite {a'. (f(a := b)) a' \<noteq> b'}" |
|
429 proof(cases "b = b' \<and> f a \<noteq> b'") |
|
430 case True |
|
431 hence "{a. f a \<noteq> b'} = insert a {a'. (f(a := b)) a' \<noteq> b'}" by auto |
|
432 thus ?thesis using b' by simp |
|
433 next |
|
434 case False |
|
435 moreover |
|
436 { assume "b \<noteq> b'" |
|
437 hence "{a'. (f(a := b)) a' \<noteq> b'} = insert a {a. f a \<noteq> b'}" by auto |
|
438 hence ?thesis using b' by simp } |
|
439 moreover |
|
440 { assume "b = b'" "f a = b'" |
|
441 hence "{a'. (f(a := b)) a' \<noteq> b'} = {a. f a \<noteq> b'}" by auto |
|
442 hence ?thesis using b' by simp } |
|
443 ultimately show ?thesis by blast |
|
444 qed |
|
445 with False b' show ?thesis by(auto simp del: fun_upd_apply simp add: finfun_default_aux_infinite) |
|
446 next |
|
447 case True thus ?thesis by(simp add: finfun_default_aux_def) |
|
448 qed |
|
449 |
|
450 definition finfun_default :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'b" |
|
451 where [code del]: "finfun_default f = finfun_default_aux (Rep_finfun f)" |
|
452 |
|
453 lemma finite_finfun_default: "finite {a. Rep_finfun f a \<noteq> finfun_default f}" |
|
454 unfolding finfun_default_def by(simp add: finite_finfun_default_aux) |
|
455 |
|
456 lemma finfun_default_const: "finfun_default ((\<lambda>\<^isup>f b) :: 'a \<Rightarrow>\<^isub>f 'b) = (if finite (UNIV :: 'a set) then undefined else b)" |
|
457 apply(auto simp add: finfun_default_def finfun_const_def finfun_default_aux_infinite) |
|
458 apply(simp add: finfun_default_aux_def) |
|
459 done |
|
460 |
|
461 lemma finfun_default_update_const: |
|
462 "finfun_default (f(\<^sup>f a := b)) = finfun_default f" |
|
463 unfolding finfun_default_def finfun_update_def |
|
464 by(simp add: finfun_default_aux_update_const) |
|
465 |
|
466 subsection {* Recursion combinator and well-formedness conditions *} |
|
467 |
|
468 definition finfun_rec :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<Rightarrow> 'c" |
|
469 where [code del]: |
|
470 "finfun_rec cnst upd f \<equiv> |
|
471 let b = finfun_default f; |
|
472 g = THE g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g |
|
473 in fold (\<lambda>a. upd a (map_default b g a)) (cnst b) (dom g)" |
|
474 |
|
475 locale finfun_rec_wf_aux = |
|
476 fixes cnst :: "'b \<Rightarrow> 'c" |
|
477 and upd :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c" |
|
478 assumes upd_const_same: "upd a b (cnst b) = cnst b" |
|
479 and upd_commute: "a \<noteq> a' \<Longrightarrow> upd a b (upd a' b' c) = upd a' b' (upd a b c)" |
|
480 and upd_idemp: "b \<noteq> b' \<Longrightarrow> upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)" |
|
481 begin |
|
482 |
|
483 |
|
484 lemma upd_left_comm: "fun_left_comm (\<lambda>a. upd a (f a))" |
|
485 by(unfold_locales)(auto intro: upd_commute) |
|
486 |
|
487 lemma upd_upd_twice: "upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)" |
|
488 by(cases "b \<noteq> b'")(auto simp add: fun_upd_def upd_const_same upd_idemp) |
|
489 |
|
490 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro] |
|
491 |
|
492 lemma map_default_update_const: |
|
493 assumes fin: "finite (dom f)" |
|
494 and anf: "a \<notin> dom f" |
|
495 and fg: "f \<subseteq>\<^sub>m g" |
|
496 shows "upd a d (fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f)) = |
|
497 fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f)" |
|
498 proof - |
|
499 let ?upd = "\<lambda>a. upd a (map_default d g a)" |
|
500 let ?fr = "\<lambda>A. fold ?upd (cnst d) A" |
|
501 interpret gwf: fun_left_comm "?upd" by(rule upd_left_comm) |
|
502 |
|
503 from fin anf fg show ?thesis |
|
504 proof(induct A\<equiv>"dom f" arbitrary: f) |
|
505 case empty |
|
506 from `{} = dom f` have "f = empty" by(auto simp add: dom_def intro: ext) |
|
507 thus ?case by(simp add: finfun_const_def upd_const_same) |
|
508 next |
|
509 case (insert a' A) |
|
510 note IH = `\<And>f. \<lbrakk> a \<notin> dom f; f \<subseteq>\<^sub>m g; A = dom f\<rbrakk> \<Longrightarrow> upd a d (?fr (dom f)) = ?fr (dom f)` |
|
511 note fin = `finite A` note anf = `a \<notin> dom f` note a'nA = `a' \<notin> A` |
|
512 note domf = `insert a' A = dom f` note fg = `f \<subseteq>\<^sub>m g` |
|
513 |
|
514 from domf obtain b where b: "f a' = Some b" by auto |
|
515 let ?f' = "f(a' := None)" |
|
516 have "upd a d (?fr (insert a' A)) = upd a d (upd a' (map_default d g a') (?fr A))" |
|
517 by(subst gwf.fold_insert[OF fin a'nA]) rule |
|
518 also from b fg have "g a' = f a'" by(auto simp add: map_le_def intro: domI dest: bspec) |
|
519 hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def) |
|
520 also from anf domf have "a \<noteq> a'" by auto note upd_commute[OF this] |
|
521 also from domf a'nA anf fg have "a \<notin> dom ?f'" "?f' \<subseteq>\<^sub>m g" and A: "A = dom ?f'" by(auto simp add: ran_def map_le_def) |
|
522 note A also note IH[OF `a \<notin> dom ?f'` `?f' \<subseteq>\<^sub>m g` A] |
|
523 also have "upd a' (map_default d f a') (?fr (dom (f(a' := None)))) = ?fr (dom f)" |
|
524 unfolding domf[symmetric] gwf.fold_insert[OF fin a'nA] ga' unfolding A .. |
|
525 also have "insert a' (dom ?f') = dom f" using domf by auto |
|
526 finally show ?case . |
|
527 qed |
|
528 qed |
|
529 |
|
530 lemma map_default_update_twice: |
|
531 assumes fin: "finite (dom f)" |
|
532 and anf: "a \<notin> dom f" |
|
533 and fg: "f \<subseteq>\<^sub>m g" |
|
534 shows "upd a d'' (upd a d' (fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f))) = |
|
535 upd a d'' (fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f))" |
|
536 proof - |
|
537 let ?upd = "\<lambda>a. upd a (map_default d g a)" |
|
538 let ?fr = "\<lambda>A. fold ?upd (cnst d) A" |
|
539 interpret gwf: fun_left_comm "?upd" by(rule upd_left_comm) |
|
540 |
|
541 from fin anf fg show ?thesis |
|
542 proof(induct A\<equiv>"dom f" arbitrary: f) |
|
543 case empty |
|
544 from `{} = dom f` have "f = empty" by(auto simp add: dom_def intro: ext) |
|
545 thus ?case by(auto simp add: finfun_const_def finfun_update_def upd_upd_twice) |
|
546 next |
|
547 case (insert a' A) |
|
548 note IH = `\<And>f. \<lbrakk>a \<notin> dom f; f \<subseteq>\<^sub>m g; A = dom f\<rbrakk> \<Longrightarrow> upd a d'' (upd a d' (?fr (dom f))) = upd a d'' (?fr (dom f))` |
|
549 note fin = `finite A` note anf = `a \<notin> dom f` note a'nA = `a' \<notin> A` |
|
550 note domf = `insert a' A = dom f` note fg = `f \<subseteq>\<^sub>m g` |
|
551 |
|
552 from domf obtain b where b: "f a' = Some b" by auto |
|
553 let ?f' = "f(a' := None)" |
|
554 let ?b' = "case f a' of None \<Rightarrow> d | Some b \<Rightarrow> b" |
|
555 from domf have "upd a d'' (upd a d' (?fr (dom f))) = upd a d'' (upd a d' (?fr (insert a' A)))" by simp |
|
556 also note gwf.fold_insert[OF fin a'nA] |
|
557 also from b fg have "g a' = f a'" by(auto simp add: map_le_def intro: domI dest: bspec) |
|
558 hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def) |
|
559 also from anf domf have ana': "a \<noteq> a'" by auto note upd_commute[OF this] |
|
560 also note upd_commute[OF ana'] |
|
561 also from domf a'nA anf fg have "a \<notin> dom ?f'" "?f' \<subseteq>\<^sub>m g" and A: "A = dom ?f'" by(auto simp add: ran_def map_le_def) |
|
562 note A also note IH[OF `a \<notin> dom ?f'` `?f' \<subseteq>\<^sub>m g` A] |
|
563 also note upd_commute[OF ana'[symmetric]] also note ga'[symmetric] also note A[symmetric] |
|
564 also note gwf.fold_insert[symmetric, OF fin a'nA] also note domf |
|
565 finally show ?case . |
|
566 qed |
|
567 qed |
|
568 |
|
569 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del] |
|
570 |
|
571 lemma map_default_eq_id [simp]: "map_default d ((\<lambda>a. Some (f a)) |` {a. f a \<noteq> d}) = f" |
|
572 by(auto simp add: map_default_def restrict_map_def intro: ext) |
|
573 |
|
574 lemma finite_rec_cong1: |
|
575 assumes f: "fun_left_comm f" and g: "fun_left_comm g" |
|
576 and fin: "finite A" |
|
577 and eq: "\<And>a. a \<in> A \<Longrightarrow> f a = g a" |
|
578 shows "fold f z A = fold g z A" |
|
579 proof - |
|
580 interpret f: fun_left_comm f by(rule f) |
|
581 interpret g: fun_left_comm g by(rule g) |
|
582 { fix B |
|
583 assume BsubA: "B \<subseteq> A" |
|
584 with fin have "finite B" by(blast intro: finite_subset) |
|
585 hence "B \<subseteq> A \<Longrightarrow> fold f z B = fold g z B" |
|
586 proof(induct) |
|
587 case empty thus ?case by simp |
|
588 next |
|
589 case (insert a B) |
|
590 note finB = `finite B` note anB = `a \<notin> B` note sub = `insert a B \<subseteq> A` |
|
591 note IH = `B \<subseteq> A \<Longrightarrow> fold f z B = fold g z B` |
|
592 from sub anB have BpsubA: "B \<subset> A" and BsubA: "B \<subseteq> A" and aA: "a \<in> A" by auto |
|
593 from IH[OF BsubA] eq[OF aA] finB anB |
|
594 show ?case by(auto) |
|
595 qed |
|
596 with BsubA have "fold f z B = fold g z B" by blast } |
|
597 thus ?thesis by blast |
|
598 qed |
|
599 |
|
600 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro] |
|
601 |
|
602 lemma finfun_rec_upd [simp]: |
|
603 "finfun_rec cnst upd (f(\<^sup>f a' := b')) = upd a' b' (finfun_rec cnst upd f)" |
|
604 proof - |
|
605 obtain b where b: "b = finfun_default f" by auto |
|
606 let ?the = "\<lambda>f g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g" |
|
607 obtain g where g: "g = The (?the f)" by blast |
|
608 obtain y where f: "f = Abs_finfun y" and y: "y \<in> finfun" by (cases f) |
|
609 from f y b have bfin: "finite {a. y a \<noteq> b}" by(simp add: finfun_default_def finite_finfun_default_aux) |
|
610 |
|
611 let ?g = "(\<lambda>a. Some (y a)) |` {a. y a \<noteq> b}" |
|
612 from bfin have fing: "finite (dom ?g)" by auto |
|
613 have bran: "b \<notin> ran ?g" by(auto simp add: ran_def restrict_map_def) |
|
614 have yg: "y = map_default b ?g" by simp |
|
615 have gg: "g = ?g" unfolding g |
|
616 proof(rule the_equality) |
|
617 from f y bfin show "?the f ?g" |
|
618 by(auto)(simp add: restrict_map_def ran_def split: split_if_asm) |
|
619 next |
|
620 fix g' |
|
621 assume "?the f g'" |
|
622 hence fin': "finite (dom g')" and ran': "b \<notin> ran g'" |
|
623 and eq: "Abs_finfun (map_default b ?g) = Abs_finfun (map_default b g')" using f yg by auto |
|
624 from fin' fing have "map_default b ?g \<in> finfun" "map_default b g' \<in> finfun" by(blast intro: map_default_in_finfun)+ |
|
625 with eq have "map_default b ?g = map_default b g'" by simp |
|
626 with fing bran fin' ran' show "g' = ?g" by(rule map_default_inject[OF disjI2[OF refl], THEN sym]) |
|
627 qed |
|
628 |
|
629 show ?thesis |
|
630 proof(cases "b' = b") |
|
631 case True |
|
632 note b'b = True |
|
633 |
|
634 let ?g' = "(\<lambda>a. Some ((y(a' := b)) a)) |` {a. (y(a' := b)) a \<noteq> b}" |
|
635 from bfin b'b have fing': "finite (dom ?g')" |
|
636 by(auto simp add: Collect_conj_eq Collect_imp_eq intro: finite_subset) |
|
637 have brang': "b \<notin> ran ?g'" by(auto simp add: ran_def restrict_map_def) |
|
638 |
|
639 let ?b' = "\<lambda>a. case ?g' a of None \<Rightarrow> b | Some b \<Rightarrow> b" |
|
640 let ?b = "map_default b ?g" |
|
641 from upd_left_comm upd_left_comm fing' |
|
642 have "fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g') = fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g')" |
|
643 by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b b map_default_def) |
|
644 also interpret gwf: fun_left_comm "\<lambda>a. upd a (?b a)" by(rule upd_left_comm) |
|
645 have "fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g') = upd a' b' (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g))" |
|
646 proof(cases "y a' = b") |
|
647 case True |
|
648 with b'b have g': "?g' = ?g" by(auto simp add: restrict_map_def intro: ext) |
|
649 from True have a'ndomg: "a' \<notin> dom ?g" by auto |
|
650 from f b'b b show ?thesis unfolding g' |
|
651 by(subst map_default_update_const[OF fing a'ndomg map_le_refl, symmetric]) simp |
|
652 next |
|
653 case False |
|
654 hence domg: "dom ?g = insert a' (dom ?g')" by auto |
|
655 from False b'b have a'ndomg': "a' \<notin> dom ?g'" by auto |
|
656 have "fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g')) = |
|
657 upd a' (?b a') (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'))" |
|
658 using fing' a'ndomg' unfolding b'b by(rule gwf.fold_insert) |
|
659 hence "upd a' b (fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g'))) = |
|
660 upd a' b (upd a' (?b a') (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g')))" by simp |
|
661 also from b'b have g'leg: "?g' \<subseteq>\<^sub>m ?g" by(auto simp add: restrict_map_def map_le_def) |
|
662 note map_default_update_twice[OF fing' a'ndomg' this, of b "?b a'" b] |
|
663 also note map_default_update_const[OF fing' a'ndomg' g'leg, of b] |
|
664 finally show ?thesis unfolding b'b domg[unfolded b'b] by(rule sym) |
|
665 qed |
|
666 also have "The (?the (f(\<^sup>f a' := b'))) = ?g'" |
|
667 proof(rule the_equality) |
|
668 from f y b b'b brang' fing' show "?the (f(\<^sup>f a' := b')) ?g'" |
|
669 by(auto simp del: fun_upd_apply simp add: finfun_update_def) |
|
670 next |
|
671 fix g' |
|
672 assume "?the (f(\<^sup>f a' := b')) g'" |
|
673 hence fin': "finite (dom g')" and ran': "b \<notin> ran g'" |
|
674 and eq: "f(\<^sup>f a' := b') = Abs_finfun (map_default b g')" |
|
675 by(auto simp del: fun_upd_apply) |
|
676 from fin' fing' have "map_default b g' \<in> finfun" "map_default b ?g' \<in> finfun" |
|
677 by(blast intro: map_default_in_finfun)+ |
|
678 with eq f b'b b have "map_default b ?g' = map_default b g'" |
|
679 by(simp del: fun_upd_apply add: finfun_update_def) |
|
680 with fing' brang' fin' ran' show "g' = ?g'" |
|
681 by(rule map_default_inject[OF disjI2[OF refl], THEN sym]) |
|
682 qed |
|
683 ultimately show ?thesis unfolding finfun_rec_def Let_def b gg[unfolded g b] using bfin b'b b |
|
684 by(simp only: finfun_default_update_const map_default_def) |
|
685 next |
|
686 case False |
|
687 note b'b = this |
|
688 let ?g' = "?g(a' \<mapsto> b')" |
|
689 let ?b' = "map_default b ?g'" |
|
690 let ?b = "map_default b ?g" |
|
691 from fing have fing': "finite (dom ?g')" by auto |
|
692 from bran b'b have bnrang': "b \<notin> ran ?g'" by(auto simp add: ran_def) |
|
693 have ffmg': "map_default b ?g' = y(a' := b')" by(auto intro: ext simp add: map_default_def restrict_map_def) |
|
694 with f y have f_Abs: "f(\<^sup>f a' := b') = Abs_finfun (map_default b ?g')" by(auto simp add: finfun_update_def) |
|
695 have g': "The (?the (f(\<^sup>f a' := b'))) = ?g'" |
|
696 proof |
|
697 from fing' bnrang' f_Abs show "?the (f(\<^sup>f a' := b')) ?g'" by(auto simp add: finfun_update_def restrict_map_def) |
|
698 next |
|
699 fix g' assume "?the (f(\<^sup>f a' := b')) g'" |
|
700 hence f': "f(\<^sup>f a' := b') = Abs_finfun (map_default b g')" |
|
701 and fin': "finite (dom g')" and brang': "b \<notin> ran g'" by auto |
|
702 from fing' fin' have "map_default b ?g' \<in> finfun" "map_default b g' \<in> finfun" |
|
703 by(auto intro: map_default_in_finfun) |
|
704 with f' f_Abs have "map_default b g' = map_default b ?g'" by simp |
|
705 with fin' brang' fing' bnrang' show "g' = ?g'" |
|
706 by(rule map_default_inject[OF disjI2[OF refl]]) |
|
707 qed |
|
708 have dom: "dom (((\<lambda>a. Some (y a)) |` {a. y a \<noteq> b})(a' \<mapsto> b')) = insert a' (dom ((\<lambda>a. Some (y a)) |` {a. y a \<noteq> b}))" |
|
709 by auto |
|
710 show ?thesis |
|
711 proof(cases "y a' = b") |
|
712 case True |
|
713 hence a'ndomg: "a' \<notin> dom ?g" by auto |
|
714 from f y b'b True have yff: "y = map_default b (?g' |` dom ?g)" |
|
715 by(auto simp add: restrict_map_def map_default_def intro!: ext) |
|
716 hence f': "f = Abs_finfun (map_default b (?g' |` dom ?g))" using f by simp |
|
717 interpret g'wf: fun_left_comm "\<lambda>a. upd a (?b' a)" by(rule upd_left_comm) |
|
718 from upd_left_comm upd_left_comm fing |
|
719 have "fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g) = fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g)" |
|
720 by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b True map_default_def) |
|
721 thus ?thesis unfolding finfun_rec_def Let_def finfun_default_update_const b[symmetric] |
|
722 unfolding g' g[symmetric] gg g'wf.fold_insert[OF fing a'ndomg, of "cnst b", folded dom] |
|
723 by -(rule arg_cong2[where f="upd a'"], simp_all add: map_default_def) |
|
724 next |
|
725 case False |
|
726 hence "insert a' (dom ?g) = dom ?g" by auto |
|
727 moreover { |
|
728 let ?g'' = "?g(a' := None)" |
|
729 let ?b'' = "map_default b ?g''" |
|
730 from False have domg: "dom ?g = insert a' (dom ?g'')" by auto |
|
731 from False have a'ndomg'': "a' \<notin> dom ?g''" by auto |
|
732 have fing'': "finite (dom ?g'')" by(rule finite_subset[OF _ fing]) auto |
|
733 have bnrang'': "b \<notin> ran ?g''" by(auto simp add: ran_def restrict_map_def) |
|
734 interpret gwf: fun_left_comm "\<lambda>a. upd a (?b a)" by(rule upd_left_comm) |
|
735 interpret g'wf: fun_left_comm "\<lambda>a. upd a (?b' a)" by(rule upd_left_comm) |
|
736 have "upd a' b' (fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g''))) = |
|
737 upd a' b' (upd a' (?b a') (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')))" |
|
738 unfolding gwf.fold_insert[OF fing'' a'ndomg''] f .. |
|
739 also have g''leg: "?g |` dom ?g'' \<subseteq>\<^sub>m ?g" by(auto simp add: map_le_def) |
|
740 have "dom (?g |` dom ?g'') = dom ?g''" by auto |
|
741 note map_default_update_twice[where d=b and f = "?g |` dom ?g''" and a=a' and d'="?b a'" and d''=b' and g="?g", |
|
742 unfolded this, OF fing'' a'ndomg'' g''leg] |
|
743 also have b': "b' = ?b' a'" by(auto simp add: map_default_def) |
|
744 from upd_left_comm upd_left_comm fing'' |
|
745 have "fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'') = fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g'')" |
|
746 by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b map_default_def) |
|
747 with b' have "upd a' b' (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')) = |
|
748 upd a' (?b' a') (fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g''))" by simp |
|
749 also note g'wf.fold_insert[OF fing'' a'ndomg'', symmetric] |
|
750 finally have "upd a' b' (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g)) = |
|
751 fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g)" |
|
752 unfolding domg . } |
|
753 ultimately have "fold (\<lambda>a. upd a (?b' a)) (cnst b) (insert a' (dom ?g)) = |
|
754 upd a' b' (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g))" by simp |
|
755 thus ?thesis unfolding finfun_rec_def Let_def finfun_default_update_const b[symmetric] g[symmetric] g' dom[symmetric] |
|
756 using b'b gg by(simp add: map_default_insert) |
|
757 qed |
|
758 qed |
|
759 qed |
|
760 |
|
761 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del] |
|
762 |
|
763 end |
|
764 |
|
765 locale finfun_rec_wf = finfun_rec_wf_aux + |
|
766 assumes const_update_all: |
|
767 "finite (UNIV :: 'a set) \<Longrightarrow> fold (\<lambda>a. upd a b') (cnst b) (UNIV :: 'a set) = cnst b'" |
|
768 begin |
|
769 |
|
770 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro] |
|
771 |
|
772 lemma finfun_rec_const [simp]: |
|
773 "finfun_rec cnst upd (\<lambda>\<^isup>f c) = cnst c" |
|
774 proof(cases "finite (UNIV :: 'a set)") |
|
775 case False |
|
776 hence "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = c" by(simp add: finfun_default_const) |
|
777 moreover have "(THE g :: 'a \<rightharpoonup> 'b. (\<lambda>\<^isup>f c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g) = empty" |
|
778 proof |
|
779 show "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c empty) \<and> finite (dom empty) \<and> c \<notin> ran empty" |
|
780 by(auto simp add: finfun_const_def) |
|
781 next |
|
782 fix g :: "'a \<rightharpoonup> 'b" |
|
783 assume "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g" |
|
784 hence g: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c g)" and fin: "finite (dom g)" and ran: "c \<notin> ran g" by blast+ |
|
785 from g map_default_in_finfun[OF fin, of c] have "map_default c g = (\<lambda>a. c)" |
|
786 by(simp add: finfun_const_def) |
|
787 moreover have "map_default c empty = (\<lambda>a. c)" by simp |
|
788 ultimately show "g = empty" by-(rule map_default_inject[OF disjI2[OF refl] fin ran], auto) |
|
789 qed |
|
790 ultimately show ?thesis by(simp add: finfun_rec_def) |
|
791 next |
|
792 case True |
|
793 hence default: "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = undefined" by(simp add: finfun_default_const) |
|
794 let ?the = "\<lambda>g :: 'a \<rightharpoonup> 'b. (\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g) \<and> finite (dom g) \<and> undefined \<notin> ran g" |
|
795 show ?thesis |
|
796 proof(cases "c = undefined") |
|
797 case True |
|
798 have the: "The ?the = empty" |
|
799 proof |
|
800 from True show "?the empty" by(auto simp add: finfun_const_def) |
|
801 next |
|
802 fix g' |
|
803 assume "?the g'" |
|
804 hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g')" |
|
805 and fin: "finite (dom g')" and g: "undefined \<notin> ran g'" by simp_all |
|
806 from fin have "map_default undefined g' \<in> finfun" by(rule map_default_in_finfun) |
|
807 with fg have "map_default undefined g' = (\<lambda>a. c)" |
|
808 by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1]) |
|
809 with True show "g' = empty" |
|
810 by -(rule map_default_inject(2)[OF _ fin g], auto) |
|
811 qed |
|
812 show ?thesis unfolding finfun_rec_def using `finite UNIV` True |
|
813 unfolding Let_def the default by(simp) |
|
814 next |
|
815 case False |
|
816 have the: "The ?the = (\<lambda>a :: 'a. Some c)" |
|
817 proof |
|
818 from False True show "?the (\<lambda>a :: 'a. Some c)" |
|
819 by(auto simp add: map_default_def_raw finfun_const_def dom_def ran_def) |
|
820 next |
|
821 fix g' :: "'a \<rightharpoonup> 'b" |
|
822 assume "?the g'" |
|
823 hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g')" |
|
824 and fin: "finite (dom g')" and g: "undefined \<notin> ran g'" by simp_all |
|
825 from fin have "map_default undefined g' \<in> finfun" by(rule map_default_in_finfun) |
|
826 with fg have "map_default undefined g' = (\<lambda>a. c)" |
|
827 by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1]) |
|
828 with True False show "g' = (\<lambda>a::'a. Some c)" |
|
829 by -(rule map_default_inject(2)[OF _ fin g], auto simp add: dom_def ran_def map_default_def_raw) |
|
830 qed |
|
831 show ?thesis unfolding finfun_rec_def using True False |
|
832 unfolding Let_def the default by(simp add: dom_def map_default_def const_update_all) |
|
833 qed |
|
834 qed |
|
835 |
|
836 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del] |
|
837 |
|
838 end |
|
839 |
|
840 subsection {* Weak induction rule and case analysis for FinFuns *} |
|
841 |
|
842 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro] |
|
843 |
|
844 lemma finfun_weak_induct [consumes 0, case_names const update]: |
|
845 assumes const: "\<And>b. P (\<lambda>\<^isup>f b)" |
|
846 and update: "\<And>f a b. P f \<Longrightarrow> P (f(\<^sup>f a := b))" |
|
847 shows "P x" |
|
848 proof(induct x rule: Abs_finfun_induct) |
|
849 case (Abs_finfun y) |
|
850 then obtain b where "finite {a. y a \<noteq> b}" unfolding finfun_def by blast |
|
851 thus ?case using `y \<in> finfun` |
|
852 proof(induct x\<equiv>"{a. y a \<noteq> b}" arbitrary: y rule: finite_induct) |
|
853 case empty |
|
854 hence "\<And>a. y a = b" by blast |
|
855 hence "y = (\<lambda>a. b)" by(auto intro: ext) |
|
856 hence "Abs_finfun y = finfun_const b" unfolding finfun_const_def by simp |
|
857 thus ?case by(simp add: const) |
|
858 next |
|
859 case (insert a A) |
|
860 note IH = `\<And>y. \<lbrakk> y \<in> finfun; A = {a. y a \<noteq> b} \<rbrakk> \<Longrightarrow> P (Abs_finfun y)` |
|
861 note y = `y \<in> finfun` |
|
862 with `insert a A = {a. y a \<noteq> b}` `a \<notin> A` |
|
863 have "y(a := b) \<in> finfun" "A = {a'. (y(a := b)) a' \<noteq> b}" by auto |
|
864 from IH[OF this] have "P (finfun_update (Abs_finfun (y(a := b))) a (y a))" by(rule update) |
|
865 thus ?case using y unfolding finfun_update_def by simp |
|
866 qed |
|
867 qed |
|
868 |
|
869 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del] |
|
870 |
|
871 lemma finfun_exhaust_disj: "(\<exists>b. x = finfun_const b) \<or> (\<exists>f a b. x = finfun_update f a b)" |
|
872 by(induct x rule: finfun_weak_induct) blast+ |
|
873 |
|
874 lemma finfun_exhaust: |
|
875 obtains b where "x = (\<lambda>\<^isup>f b)" |
|
876 | f a b where "x = f(\<^sup>f a := b)" |
|
877 by(atomize_elim)(rule finfun_exhaust_disj) |
|
878 |
|
879 lemma finfun_rec_unique: |
|
880 fixes f :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'c" |
|
881 assumes c: "\<And>c. f (\<lambda>\<^isup>f c) = cnst c" |
|
882 and u: "\<And>g a b. f (g(\<^sup>f a := b)) = upd g a b (f g)" |
|
883 and c': "\<And>c. f' (\<lambda>\<^isup>f c) = cnst c" |
|
884 and u': "\<And>g a b. f' (g(\<^sup>f a := b)) = upd g a b (f' g)" |
|
885 shows "f = f'" |
|
886 proof |
|
887 fix g :: "'a \<Rightarrow>\<^isub>f 'b" |
|
888 show "f g = f' g" |
|
889 by(induct g rule: finfun_weak_induct)(auto simp add: c u c' u') |
|
890 qed |
|
891 |
|
892 |
|
893 subsection {* Function application *} |
|
894 |
|
895 definition finfun_apply :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b" ("_\<^sub>f" [1000] 1000) |
|
896 where [code del]: "finfun_apply = (\<lambda>f a. finfun_rec (\<lambda>b. b) (\<lambda>a' b c. if (a = a') then b else c) f)" |
|
897 |
|
898 interpretation finfun_apply_aux: finfun_rec_wf_aux "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c" |
|
899 by(unfold_locales) auto |
|
900 |
|
901 interpretation finfun_apply: finfun_rec_wf "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c" |
|
902 proof(unfold_locales) |
|
903 fix b' b :: 'a |
|
904 assume fin: "finite (UNIV :: 'b set)" |
|
905 { fix A :: "'b set" |
|
906 interpret fun_left_comm "\<lambda>a'. If (a = a') b'" by(rule finfun_apply_aux.upd_left_comm) |
|
907 from fin have "finite A" by(auto intro: finite_subset) |
|
908 hence "fold (\<lambda>a'. If (a = a') b') b A = (if a \<in> A then b' else b)" |
|
909 by induct auto } |
|
910 from this[of UNIV] show "fold (\<lambda>a'. If (a = a') b') b UNIV = b'" by simp |
|
911 qed |
|
912 |
|
913 lemma finfun_const_apply [simp, code]: "(\<lambda>\<^isup>f b)\<^sub>f a = b" |
|
914 by(simp add: finfun_apply_def) |
|
915 |
|
916 lemma finfun_upd_apply: "f(\<^sup>fa := b)\<^sub>f a' = (if a = a' then b else f\<^sub>f a')" |
|
917 and finfun_upd_apply_code [code]: "(finfun_update_code f a b)\<^sub>f a' = (if a = a' then b else f\<^sub>f a')" |
|
918 by(simp_all add: finfun_apply_def) |
|
919 |
|
920 lemma finfun_upd_apply_same [simp]: |
|
921 "f(\<^sup>fa := b)\<^sub>f a = b" |
|
922 by(simp add: finfun_upd_apply) |
|
923 |
|
924 lemma finfun_upd_apply_other [simp]: |
|
925 "a \<noteq> a' \<Longrightarrow> f(\<^sup>fa := b)\<^sub>f a' = f\<^sub>f a'" |
|
926 by(simp add: finfun_upd_apply) |
|
927 |
|
928 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro] |
|
929 |
|
930 lemma finfun_apply_Rep_finfun: |
|
931 "finfun_apply = Rep_finfun" |
|
932 proof(rule finfun_rec_unique) |
|
933 fix c show "Rep_finfun (\<lambda>\<^isup>f c) = (\<lambda>a. c)" by(auto simp add: finfun_const_def) |
|
934 next |
|
935 fix g a b show "Rep_finfun g(\<^sup>f a := b) = (\<lambda>c. if c = a then b else Rep_finfun g c)" |
|
936 by(auto simp add: finfun_update_def fun_upd_finfun Abs_finfun_inverse Rep_finfun intro: ext) |
|
937 qed(auto intro: ext) |
|
938 |
|
939 lemma finfun_ext: "(\<And>a. f\<^sub>f a = g\<^sub>f a) \<Longrightarrow> f = g" |
|
940 by(auto simp add: finfun_apply_Rep_finfun Rep_finfun_inject[symmetric] simp del: Rep_finfun_inject intro: ext) |
|
941 |
|
942 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del] |
|
943 |
|
944 lemma expand_finfun_eq: "(f = g) = (f\<^sub>f = g\<^sub>f)" |
|
945 by(auto intro: finfun_ext) |
|
946 |
|
947 lemma finfun_const_inject [simp]: "(\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b') \<equiv> b = b'" |
|
948 by(simp add: expand_finfun_eq expand_fun_eq) |
|
949 |
|
950 lemma finfun_const_eq_update: |
|
951 "((\<lambda>\<^isup>f b) = f(\<^sup>f a := b')) = (b = b' \<and> (\<forall>a'. a \<noteq> a' \<longrightarrow> f\<^sub>f a' = b))" |
|
952 by(auto simp add: expand_finfun_eq expand_fun_eq finfun_upd_apply) |
|
953 |
|
954 subsection {* Function composition *} |
|
955 |
|
956 definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>\<^isub>f 'a \<Rightarrow> 'c \<Rightarrow>\<^isub>f 'b" (infixr "\<circ>\<^isub>f" 55) |
|
957 where [code del]: "g \<circ>\<^isub>f f = finfun_rec (\<lambda>b. (\<lambda>\<^isup>f g b)) (\<lambda>a b c. c(\<^sup>f a := g b)) f" |
|
958 |
|
959 interpretation finfun_comp_aux: finfun_rec_wf_aux "(\<lambda>b. (\<lambda>\<^isup>f g b))" "(\<lambda>a b c. c(\<^sup>f a := g b))" |
|
960 by(unfold_locales)(auto simp add: finfun_upd_apply intro: finfun_ext) |
|
961 |
|
962 interpretation finfun_comp: finfun_rec_wf "(\<lambda>b. (\<lambda>\<^isup>f g b))" "(\<lambda>a b c. c(\<^sup>f a := g b))" |
|
963 proof |
|
964 fix b' b :: 'a |
|
965 assume fin: "finite (UNIV :: 'c set)" |
|
966 { fix A :: "'c set" |
|
967 from fin have "finite A" by(auto intro: finite_subset) |
|
968 hence "fold (\<lambda>(a :: 'c) c. c(\<^sup>f a := g b')) (\<lambda>\<^isup>f g b) A = |
|
969 Abs_finfun (\<lambda>a. if a \<in> A then g b' else g b)" |
|
970 by induct (simp_all add: finfun_const_def, auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite expand_fun_eq fin) } |
|
971 from this[of UNIV] show "fold (\<lambda>(a :: 'c) c. c(\<^sup>f a := g b')) (\<lambda>\<^isup>f g b) UNIV = (\<lambda>\<^isup>f g b')" |
|
972 by(simp add: finfun_const_def) |
|
973 qed |
|
974 |
|
975 lemma finfun_comp_const [simp, code]: |
|
976 "g \<circ>\<^isub>f (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f g c)" |
|
977 by(simp add: finfun_comp_def) |
|
978 |
|
979 lemma finfun_comp_update [simp]: "g \<circ>\<^isub>f (f(\<^sup>f a := b)) = (g \<circ>\<^isub>f f)(\<^sup>f a := g b)" |
|
980 and finfun_comp_update_code [code]: "g \<circ>\<^isub>f (finfun_update_code f a b) = finfun_update_code (g \<circ>\<^isub>f f) a (g b)" |
|
981 by(simp_all add: finfun_comp_def) |
|
982 |
|
983 lemma finfun_comp_apply [simp]: |
|
984 "(g \<circ>\<^isub>f f)\<^sub>f = g \<circ> f\<^sub>f" |
|
985 by(induct f rule: finfun_weak_induct)(auto simp add: finfun_upd_apply intro: ext) |
|
986 |
|
987 lemma finfun_comp_comp_collapse [simp]: "f \<circ>\<^isub>f g \<circ>\<^isub>f h = (f o g) \<circ>\<^isub>f h" |
|
988 by(induct h rule: finfun_weak_induct) simp_all |
|
989 |
|
990 lemma finfun_comp_const1 [simp]: "(\<lambda>x. c) \<circ>\<^isub>f f = (\<lambda>\<^isup>f c)" |
|
991 by(induct f rule: finfun_weak_induct)(auto intro: finfun_ext simp add: finfun_upd_apply) |
|
992 |
|
993 lemma finfun_comp_id1 [simp]: "(\<lambda>x. x) \<circ>\<^isub>f f = f" "id \<circ>\<^isub>f f = f" |
|
994 by(induct f rule: finfun_weak_induct) auto |
|
995 |
|
996 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro] |
|
997 |
|
998 lemma finfun_comp_conv_comp: "g \<circ>\<^isub>f f = Abs_finfun (g \<circ> finfun_apply f)" |
|
999 proof - |
|
1000 have "(\<lambda>f. g \<circ>\<^isub>f f) = (\<lambda>f. Abs_finfun (g \<circ> finfun_apply f))" |
|
1001 proof(rule finfun_rec_unique) |
|
1002 { fix c show "Abs_finfun (g \<circ> (\<lambda>\<^isup>f c)\<^sub>f) = (\<lambda>\<^isup>f g c)" |
|
1003 by(simp add: finfun_comp_def o_def)(simp add: finfun_const_def) } |
|
1004 { fix g' a b show "Abs_finfun (g \<circ> g'(\<^sup>f a := b)\<^sub>f) = (Abs_finfun (g \<circ> g'\<^sub>f))(\<^sup>f a := g b)" |
|
1005 proof - |
|
1006 obtain y where y: "y \<in> finfun" and g': "g' = Abs_finfun y" by(cases g') |
|
1007 moreover hence "(g \<circ> g'\<^sub>f) \<in> finfun" by(simp add: finfun_apply_Rep_finfun finfun_left_compose) |
|
1008 moreover have "g \<circ> y(a := b) = (g \<circ> y)(a := g b)" by(auto intro: ext) |
|
1009 ultimately show ?thesis by(simp add: finfun_comp_def finfun_update_def finfun_apply_Rep_finfun) |
|
1010 qed } |
|
1011 qed auto |
|
1012 thus ?thesis by(auto simp add: expand_fun_eq) |
|
1013 qed |
|
1014 |
|
1015 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del] |
|
1016 |
|
1017 |
|
1018 |
|
1019 definition finfun_comp2 :: "'b \<Rightarrow>\<^isub>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c" (infixr "\<^sub>f\<circ>" 55) |
|
1020 where [code del]: "finfun_comp2 g f = Abs_finfun (Rep_finfun g \<circ> f)" |
|
1021 |
|
1022 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro] |
|
1023 |
|
1024 lemma finfun_comp2_const [code, simp]: "finfun_comp2 (\<lambda>\<^isup>f c) f = (\<lambda>\<^isup>f c)" |
|
1025 by(simp add: finfun_comp2_def finfun_const_def comp_def) |
|
1026 |
|
1027 lemma finfun_comp2_update: |
|
1028 assumes inj: "inj f" |
|
1029 shows "finfun_comp2 (g(\<^sup>f b := c)) f = (if b \<in> range f then (finfun_comp2 g f)(\<^sup>f inv f b := c) else finfun_comp2 g f)" |
|
1030 proof(cases "b \<in> range f") |
|
1031 case True |
|
1032 from inj have "\<And>x. (Rep_finfun g)(f x := c) \<circ> f = (Rep_finfun g \<circ> f)(x := c)" by(auto intro!: ext dest: injD) |
|
1033 with inj True show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def finfun_right_compose) |
|
1034 next |
|
1035 case False |
|
1036 hence "(Rep_finfun g)(b := c) \<circ> f = Rep_finfun g \<circ> f" by(auto simp add: expand_fun_eq) |
|
1037 with False show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def) |
|
1038 qed |
|
1039 |
|
1040 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del] |
|
1041 |
|
1042 subsection {* A type class for computing the cardinality of a type's universe *} |
|
1043 |
|
1044 class card_UNIV = |
|
1045 fixes card_UNIV :: "'a itself \<Rightarrow> nat" |
|
1046 assumes card_UNIV: "card_UNIV x = card (UNIV :: 'a set)" |
|
1047 begin |
|
1048 |
|
1049 lemma card_UNIV_neq_0_finite_UNIV: |
|
1050 "card_UNIV x \<noteq> 0 \<longleftrightarrow> finite (UNIV :: 'a set)" |
|
1051 by(simp add: card_UNIV card_eq_0_iff) |
|
1052 |
|
1053 lemma card_UNIV_ge_0_finite_UNIV: |
|
1054 "card_UNIV x > 0 \<longleftrightarrow> finite (UNIV :: 'a set)" |
|
1055 by(auto simp add: card_UNIV intro: card_ge_0_finite finite_UNIV_card_ge_0) |
|
1056 |
|
1057 lemma card_UNIV_eq_0_infinite_UNIV: |
|
1058 "card_UNIV x = 0 \<longleftrightarrow> infinite (UNIV :: 'a set)" |
|
1059 by(simp add: card_UNIV card_eq_0_iff) |
|
1060 |
|
1061 definition is_list_UNIV :: "'a list \<Rightarrow> bool" |
|
1062 where "is_list_UNIV xs = (let c = card_UNIV (TYPE('a)) in if c = 0 then False else size (remdups xs) = c)" |
|
1063 |
|
1064 lemma is_list_UNIV_iff: |
|
1065 fixes xs :: "'a list" |
|
1066 shows "is_list_UNIV xs \<longleftrightarrow> set xs = UNIV" |
|
1067 proof |
|
1068 assume "is_list_UNIV xs" |
|
1069 hence c: "card_UNIV (TYPE('a)) > 0" and xs: "size (remdups xs) = card_UNIV (TYPE('a))" |
|
1070 unfolding is_list_UNIV_def by(simp_all add: Let_def split: split_if_asm) |
|
1071 from c have fin: "finite (UNIV :: 'a set)" by(auto simp add: card_UNIV_ge_0_finite_UNIV) |
|
1072 have "card (set (remdups xs)) = size (remdups xs)" by(subst distinct_card) auto |
|
1073 also note set_remdups |
|
1074 finally show "set xs = UNIV" using fin unfolding xs card_UNIV by-(rule card_eq_UNIV_imp_eq_UNIV) |
|
1075 next |
|
1076 assume xs: "set xs = UNIV" |
|
1077 from finite_set[of xs] have fin: "finite (UNIV :: 'a set)" unfolding xs . |
|
1078 hence "card_UNIV (TYPE ('a)) \<noteq> 0" unfolding card_UNIV_neq_0_finite_UNIV . |
|
1079 moreover have "size (remdups xs) = card (set (remdups xs))" |
|
1080 by(subst distinct_card) auto |
|
1081 ultimately show "is_list_UNIV xs" using xs by(simp add: is_list_UNIV_def Let_def card_UNIV) |
|
1082 qed |
|
1083 |
|
1084 lemma card_UNIV_eq_0_is_list_UNIV_False: |
|
1085 assumes cU0: "card_UNIV x = 0" |
|
1086 shows "is_list_UNIV = (\<lambda>xs. False)" |
|
1087 proof(rule ext) |
|
1088 fix xs :: "'a list" |
|
1089 from cU0 have "infinite (UNIV :: 'a set)" |
|
1090 by(auto simp only: card_UNIV_eq_0_infinite_UNIV) |
|
1091 moreover have "finite (set xs)" by(rule finite_set) |
|
1092 ultimately have "(UNIV :: 'a set) \<noteq> set xs" by(auto simp del: finite_set) |
|
1093 thus "is_list_UNIV xs = False" unfolding is_list_UNIV_iff by simp |
|
1094 qed |
|
1095 |
|
1096 end |
|
1097 |
|
1098 subsection {* Instantiations for @{text "card_UNIV"} *} |
|
1099 |
|
1100 subsubsection {* @{typ "nat"} *} |
|
1101 |
|
1102 instantiation nat :: card_UNIV begin |
|
1103 |
|
1104 definition card_UNIV_nat_def: |
|
1105 "card_UNIV_class.card_UNIV = (\<lambda>a :: nat itself. 0)" |
|
1106 |
|
1107 instance proof |
|
1108 fix x :: "nat itself" |
|
1109 show "card_UNIV x = card (UNIV :: nat set)" |
|
1110 unfolding card_UNIV_nat_def by simp |
|
1111 qed |
|
1112 |
|
1113 end |
|
1114 |
|
1115 subsubsection {* @{typ "int"} *} |
|
1116 |
|
1117 instantiation int :: card_UNIV begin |
|
1118 |
|
1119 definition card_UNIV_int_def: |
|
1120 "card_UNIV_class.card_UNIV = (\<lambda>a :: int itself. 0)" |
|
1121 |
|
1122 instance proof |
|
1123 fix x :: "int itself" |
|
1124 show "card_UNIV x = card (UNIV :: int set)" |
|
1125 unfolding card_UNIV_int_def by simp |
|
1126 qed |
|
1127 |
|
1128 end |
|
1129 |
|
1130 subsubsection {* @{typ "'a list"} *} |
|
1131 |
|
1132 instantiation list :: (type) card_UNIV begin |
|
1133 |
|
1134 definition card_UNIV_list_def: |
|
1135 "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a list itself. 0)" |
|
1136 |
|
1137 instance proof |
|
1138 fix x :: "'a list itself" |
|
1139 show "card_UNIV x = card (UNIV :: 'a list set)" |
|
1140 unfolding card_UNIV_list_def by(simp add: infinite_UNIV_listI) |
|
1141 qed |
|
1142 |
|
1143 end |
|
1144 |
|
1145 subsubsection {* @{typ "unit"} *} |
|
1146 |
|
1147 lemma card_UNIV_unit: "card (UNIV :: unit set) = 1" |
|
1148 unfolding UNIV_unit by simp |
|
1149 |
|
1150 instantiation unit :: card_UNIV begin |
|
1151 |
|
1152 definition card_UNIV_unit_def: |
|
1153 "card_UNIV_class.card_UNIV = (\<lambda>a :: unit itself. 1)" |
|
1154 |
|
1155 instance proof |
|
1156 fix x :: "unit itself" |
|
1157 show "card_UNIV x = card (UNIV :: unit set)" |
|
1158 by(simp add: card_UNIV_unit_def card_UNIV_unit) |
|
1159 qed |
|
1160 |
|
1161 end |
|
1162 |
|
1163 subsubsection {* @{typ "bool"} *} |
|
1164 |
|
1165 lemma card_UNIV_bool: "card (UNIV :: bool set) = 2" |
|
1166 unfolding UNIV_bool by simp |
|
1167 |
|
1168 instantiation bool :: card_UNIV begin |
|
1169 |
|
1170 definition card_UNIV_bool_def: |
|
1171 "card_UNIV_class.card_UNIV = (\<lambda>a :: bool itself. 2)" |
|
1172 |
|
1173 instance proof |
|
1174 fix x :: "bool itself" |
|
1175 show "card_UNIV x = card (UNIV :: bool set)" |
|
1176 by(simp add: card_UNIV_bool_def card_UNIV_bool) |
|
1177 qed |
|
1178 |
|
1179 end |
|
1180 |
|
1181 subsubsection {* @{typ "char"} *} |
|
1182 |
|
1183 lemma card_UNIV_char: "card (UNIV :: char set) = 256" |
|
1184 proof - |
|
1185 from enum_distinct |
|
1186 have "card (set (enum :: char list)) = length (enum :: char list)" |
|
1187 by - (rule distinct_card) |
|
1188 also have "set enum = (UNIV :: char set)" by auto |
|
1189 also note enum_chars |
|
1190 finally show ?thesis by (simp add: chars_def) |
|
1191 qed |
|
1192 |
|
1193 instantiation char :: card_UNIV begin |
|
1194 |
|
1195 definition card_UNIV_char_def: |
|
1196 "card_UNIV_class.card_UNIV = (\<lambda>a :: char itself. 256)" |
|
1197 |
|
1198 instance proof |
|
1199 fix x :: "char itself" |
|
1200 show "card_UNIV x = card (UNIV :: char set)" |
|
1201 by(simp add: card_UNIV_char_def card_UNIV_char) |
|
1202 qed |
|
1203 |
|
1204 end |
|
1205 |
|
1206 subsubsection {* @{typ "'a \<times> 'b"} *} |
|
1207 |
|
1208 instantiation * :: (card_UNIV, card_UNIV) card_UNIV begin |
|
1209 |
|
1210 definition card_UNIV_product_def: |
|
1211 "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<times> 'b) itself. card_UNIV (TYPE('a)) * card_UNIV (TYPE('b)))" |
|
1212 |
|
1213 instance proof |
|
1214 fix x :: "('a \<times> 'b) itself" |
|
1215 show "card_UNIV x = card (UNIV :: ('a \<times> 'b) set)" |
|
1216 by(simp add: card_UNIV_product_def card_UNIV UNIV_Times_UNIV[symmetric] card_cartesian_product del: UNIV_Times_UNIV) |
|
1217 qed |
|
1218 |
|
1219 end |
|
1220 |
|
1221 subsubsection {* @{typ "'a + 'b"} *} |
|
1222 |
|
1223 instantiation "+" :: (card_UNIV, card_UNIV) card_UNIV begin |
|
1224 |
|
1225 definition card_UNIV_sum_def: |
|
1226 "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a + 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b)) |
|
1227 in if ca \<noteq> 0 \<and> cb \<noteq> 0 then ca + cb else 0)" |
|
1228 |
|
1229 instance proof |
|
1230 fix x :: "('a + 'b) itself" |
|
1231 show "card_UNIV x = card (UNIV :: ('a + 'b) set)" |
|
1232 by (auto simp add: card_UNIV_sum_def card_UNIV card_eq_0_iff UNIV_Plus_UNIV[symmetric] finite_Plus_iff Let_def card_Plus simp del: UNIV_Plus_UNIV dest!: card_ge_0_finite) |
|
1233 qed |
|
1234 |
|
1235 end |
|
1236 |
|
1237 subsubsection {* @{typ "'a \<Rightarrow> 'b"} *} |
|
1238 |
|
1239 instantiation "fun" :: (card_UNIV, card_UNIV) card_UNIV begin |
|
1240 |
|
1241 definition card_UNIV_fun_def: |
|
1242 "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<Rightarrow> 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b)) |
|
1243 in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)" |
|
1244 |
|
1245 instance proof |
|
1246 fix x :: "('a \<Rightarrow> 'b) itself" |
|
1247 |
|
1248 { assume "0 < card (UNIV :: 'a set)" |
|
1249 and "0 < card (UNIV :: 'b set)" |
|
1250 hence fina: "finite (UNIV :: 'a set)" and finb: "finite (UNIV :: 'b set)" |
|
1251 by(simp_all only: card_ge_0_finite) |
|
1252 from finite_distinct_list[OF finb] obtain bs |
|
1253 where bs: "set bs = (UNIV :: 'b set)" and distb: "distinct bs" by blast |
|
1254 from finite_distinct_list[OF fina] obtain as |
|
1255 where as: "set as = (UNIV :: 'a set)" and dista: "distinct as" by blast |
|
1256 have cb: "card (UNIV :: 'b set) = length bs" |
|
1257 unfolding bs[symmetric] distinct_card[OF distb] .. |
|
1258 have ca: "card (UNIV :: 'a set) = length as" |
|
1259 unfolding as[symmetric] distinct_card[OF dista] .. |
|
1260 let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (n_lists (length as) bs)" |
|
1261 have "UNIV = set ?xs" |
|
1262 proof(rule UNIV_eq_I) |
|
1263 fix f :: "'a \<Rightarrow> 'b" |
|
1264 from as have "f = the \<circ> map_of (zip as (map f as))" |
|
1265 by(auto simp add: map_of_zip_map intro: ext) |
|
1266 thus "f \<in> set ?xs" using bs by(auto simp add: set_n_lists) |
|
1267 qed |
|
1268 moreover have "distinct ?xs" unfolding distinct_map |
|
1269 proof(intro conjI distinct_n_lists distb inj_onI) |
|
1270 fix xs ys :: "'b list" |
|
1271 assume xs: "xs \<in> set (n_lists (length as) bs)" |
|
1272 and ys: "ys \<in> set (n_lists (length as) bs)" |
|
1273 and eq: "the \<circ> map_of (zip as xs) = the \<circ> map_of (zip as ys)" |
|
1274 from xs ys have [simp]: "length xs = length as" "length ys = length as" |
|
1275 by(simp_all add: length_n_lists_elem) |
|
1276 have "map_of (zip as xs) = map_of (zip as ys)" |
|
1277 proof |
|
1278 fix x |
|
1279 from as bs have "\<exists>y. map_of (zip as xs) x = Some y" "\<exists>y. map_of (zip as ys) x = Some y" |
|
1280 by(simp_all add: map_of_zip_is_Some[symmetric]) |
|
1281 with eq show "map_of (zip as xs) x = map_of (zip as ys) x" |
|
1282 by(auto dest: fun_cong[where x=x]) |
|
1283 qed |
|
1284 with dista show "xs = ys" by(simp add: map_of_zip_inject) |
|
1285 qed |
|
1286 hence "card (set ?xs) = length ?xs" by(simp only: distinct_card) |
|
1287 moreover have "length ?xs = length bs ^ length as" by(simp add: length_n_lists) |
|
1288 ultimately have "card (UNIV :: ('a \<Rightarrow> 'b) set) = card (UNIV :: 'b set) ^ card (UNIV :: 'a set)" |
|
1289 using cb ca by simp } |
|
1290 moreover { |
|
1291 assume cb: "card (UNIV :: 'b set) = Suc 0" |
|
1292 then obtain b where b: "UNIV = {b :: 'b}" by(auto simp add: card_Suc_eq) |
|
1293 have eq: "UNIV = {\<lambda>x :: 'a. b ::'b}" |
|
1294 proof(rule UNIV_eq_I) |
|
1295 fix x :: "'a \<Rightarrow> 'b" |
|
1296 { fix y |
|
1297 have "x y \<in> UNIV" .. |
|
1298 hence "x y = b" unfolding b by simp } |
|
1299 thus "x \<in> {\<lambda>x. b}" by(auto intro: ext) |
|
1300 qed |
|
1301 have "card (UNIV :: ('a \<Rightarrow> 'b) set) = Suc 0" unfolding eq by simp } |
|
1302 ultimately show "card_UNIV x = card (UNIV :: ('a \<Rightarrow> 'b) set)" |
|
1303 unfolding card_UNIV_fun_def card_UNIV Let_def |
|
1304 by(auto simp del: One_nat_def)(auto simp add: card_eq_0_iff dest: finite_fun_UNIVD2 finite_fun_UNIVD1) |
|
1305 qed |
|
1306 |
|
1307 end |
|
1308 |
|
1309 subsubsection {* @{typ "'a option"} *} |
|
1310 |
|
1311 instantiation option :: (card_UNIV) card_UNIV |
|
1312 begin |
|
1313 |
|
1314 definition card_UNIV_option_def: |
|
1315 "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a option itself. let c = card_UNIV (TYPE('a)) |
|
1316 in if c \<noteq> 0 then Suc c else 0)" |
|
1317 |
|
1318 instance proof |
|
1319 fix x :: "'a option itself" |
|
1320 show "card_UNIV x = card (UNIV :: 'a option set)" |
|
1321 unfolding UNIV_option_conv |
|
1322 by(auto simp add: card_UNIV_option_def card_UNIV card_eq_0_iff Let_def intro: inj_Some dest: finite_imageD) |
|
1323 (subst card_insert_disjoint, auto simp add: card_eq_0_iff card_image inj_Some intro: finite_imageI card_ge_0_finite) |
|
1324 qed |
|
1325 |
|
1326 end |
|
1327 |
|
1328 |
|
1329 subsection {* Universal quantification *} |
|
1330 |
|
1331 definition finfun_All_except :: "'a list \<Rightarrow> 'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool" |
|
1332 where [code del]: "finfun_All_except A P \<equiv> \<forall>a. a \<in> set A \<or> P\<^sub>f a" |
|
1333 |
|
1334 lemma finfun_All_except_const: "finfun_All_except A (\<lambda>\<^isup>f b) \<longleftrightarrow> b \<or> set A = UNIV" |
|
1335 by(auto simp add: finfun_All_except_def) |
|
1336 |
|
1337 lemma finfun_All_except_const_finfun_UNIV_code [code]: |
|
1338 "finfun_All_except A (\<lambda>\<^isup>f b) = (b \<or> is_list_UNIV A)" |
|
1339 by(simp add: finfun_All_except_const is_list_UNIV_iff) |
|
1340 |
|
1341 lemma finfun_All_except_update: |
|
1342 "finfun_All_except A f(\<^sup>f a := b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)" |
|
1343 by(fastsimp simp add: finfun_All_except_def finfun_upd_apply) |
|
1344 |
|
1345 lemma finfun_All_except_update_code [code]: |
|
1346 fixes a :: "'a :: card_UNIV" |
|
1347 shows "finfun_All_except A (finfun_update_code f a b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)" |
|
1348 by(simp add: finfun_All_except_update) |
|
1349 |
|
1350 definition finfun_All :: "'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool" |
|
1351 where "finfun_All = finfun_All_except []" |
|
1352 |
|
1353 lemma finfun_All_const [simp]: "finfun_All (\<lambda>\<^isup>f b) = b" |
|
1354 by(simp add: finfun_All_def finfun_All_except_def) |
|
1355 |
|
1356 lemma finfun_All_update: "finfun_All f(\<^sup>f a := b) = (b \<and> finfun_All_except [a] f)" |
|
1357 by(simp add: finfun_All_def finfun_All_except_update) |
|
1358 |
|
1359 lemma finfun_All_All: "finfun_All P = All P\<^sub>f" |
|
1360 by(simp add: finfun_All_def finfun_All_except_def) |
|
1361 |
|
1362 |
|
1363 definition finfun_Ex :: "'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool" |
|
1364 where "finfun_Ex P = Not (finfun_All (Not \<circ>\<^isub>f P))" |
|
1365 |
|
1366 lemma finfun_Ex_Ex: "finfun_Ex P = Ex P\<^sub>f" |
|
1367 unfolding finfun_Ex_def finfun_All_All by simp |
|
1368 |
|
1369 lemma finfun_Ex_const [simp]: "finfun_Ex (\<lambda>\<^isup>f b) = b" |
|
1370 by(simp add: finfun_Ex_def) |
|
1371 |
|
1372 |
|
1373 subsection {* A diagonal operator for FinFuns *} |
|
1374 |
|
1375 definition finfun_Diag :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c \<Rightarrow> 'a \<Rightarrow>\<^isub>f ('b \<times> 'c)" ("(1'(_,/ _')\<^sup>f)" [0, 0] 1000) |
|
1376 where [code del]: "finfun_Diag f g = finfun_rec (\<lambda>b. Pair b \<circ>\<^isub>f g) (\<lambda>a b c. c(\<^sup>f a := (b, g\<^sub>f a))) f" |
|
1377 |
|
1378 interpretation finfun_Diag_aux: finfun_rec_wf_aux "\<lambda>b. Pair b \<circ>\<^isub>f g" "\<lambda>a b c. c(\<^sup>f a := (b, g\<^sub>f a))" |
|
1379 by(unfold_locales)(simp_all add: expand_finfun_eq expand_fun_eq finfun_upd_apply) |
|
1380 |
|
1381 interpretation finfun_Diag: finfun_rec_wf "\<lambda>b. Pair b \<circ>\<^isub>f g" "\<lambda>a b c. c(\<^sup>f a := (b, g\<^sub>f a))" |
|
1382 proof |
|
1383 fix b' b :: 'a |
|
1384 assume fin: "finite (UNIV :: 'c set)" |
|
1385 { fix A :: "'c set" |
|
1386 interpret fun_left_comm "\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))" by(rule finfun_Diag_aux.upd_left_comm) |
|
1387 from fin have "finite A" by(auto intro: finite_subset) |
|
1388 hence "fold (\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))) (Pair b \<circ>\<^isub>f g) A = |
|
1389 Abs_finfun (\<lambda>a. (if a \<in> A then b' else b, g\<^sub>f a))" |
|
1390 by(induct)(simp_all add: finfun_const_def finfun_comp_conv_comp o_def, |
|
1391 auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite expand_fun_eq fin) } |
|
1392 from this[of UNIV] show "fold (\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))) (Pair b \<circ>\<^isub>f g) UNIV = Pair b' \<circ>\<^isub>f g" |
|
1393 by(simp add: finfun_const_def finfun_comp_conv_comp o_def) |
|
1394 qed |
|
1395 |
|
1396 lemma finfun_Diag_const1: "(\<lambda>\<^isup>f b, g)\<^sup>f = Pair b \<circ>\<^isub>f g" |
|
1397 by(simp add: finfun_Diag_def) |
|
1398 |
|
1399 text {* |
|
1400 Do not use @{thm finfun_Diag_const1} for the code generator because @{term "Pair b"} is injective, i.e. if @{term g} is free of redundant updates, there is no need to check for redundant updates as is done for @{text "\<circ>\<^isub>f"}. |
|
1401 *} |
|
1402 |
|
1403 lemma finfun_Diag_const_code [code]: |
|
1404 "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))" |
|
1405 "(\<lambda>\<^isup>f b, g(\<^sup>f\<^sup>c a := c))\<^sup>f = (\<lambda>\<^isup>f b, g)\<^sup>f(\<^sup>f\<^sup>c a := (b, c))" |
|
1406 by(simp_all add: finfun_Diag_const1) |
|
1407 |
|
1408 lemma finfun_Diag_update1: "(f(\<^sup>f a := b), g)\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (b, g\<^sub>f a))" |
|
1409 and finfun_Diag_update1_code [code]: "(finfun_update_code f a b, g)\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (b, g\<^sub>f a))" |
|
1410 by(simp_all add: finfun_Diag_def) |
|
1411 |
|
1412 lemma finfun_Diag_const2: "(f, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>b. (b, c)) \<circ>\<^isub>f f" |
|
1413 by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1) |
|
1414 |
|
1415 lemma finfun_Diag_update2: "(f, g(\<^sup>f a := c))\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (f\<^sub>f a, c))" |
|
1416 by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1) |
|
1417 |
|
1418 lemma finfun_Diag_const_const [simp]: "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))" |
|
1419 by(simp add: finfun_Diag_const1) |
|
1420 |
|
1421 lemma finfun_Diag_const_update: |
|
1422 "(\<lambda>\<^isup>f b, g(\<^sup>f a := c))\<^sup>f = (\<lambda>\<^isup>f b, g)\<^sup>f(\<^sup>f a := (b, c))" |
|
1423 by(simp add: finfun_Diag_const1) |
|
1424 |
|
1425 lemma finfun_Diag_update_const: |
|
1426 "(f(\<^sup>f a := b), \<lambda>\<^isup>f c)\<^sup>f = (f, \<lambda>\<^isup>f c)\<^sup>f(\<^sup>f a := (b, c))" |
|
1427 by(simp add: finfun_Diag_def) |
|
1428 |
|
1429 lemma finfun_Diag_update_update: |
|
1430 "(f(\<^sup>f a := b), g(\<^sup>f a' := c))\<^sup>f = (if a = a' then (f, g)\<^sup>f(\<^sup>f a := (b, c)) else (f, g)\<^sup>f(\<^sup>f a := (b, g\<^sub>f a))(\<^sup>f a' := (f\<^sub>f a', c)))" |
|
1431 by(auto simp add: finfun_Diag_update1 finfun_Diag_update2) |
|
1432 |
|
1433 lemma finfun_Diag_apply [simp]: "(f, g)\<^sup>f\<^sub>f = (\<lambda>x. (f\<^sub>f x, g\<^sub>f x))" |
|
1434 by(induct f rule: finfun_weak_induct)(auto simp add: finfun_Diag_const1 finfun_Diag_update1 finfun_upd_apply intro: ext) |
|
1435 |
|
1436 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro] |
|
1437 |
|
1438 lemma finfun_Diag_conv_Abs_finfun: |
|
1439 "(f, g)\<^sup>f = Abs_finfun ((\<lambda>x. (Rep_finfun f x, Rep_finfun g x)))" |
|
1440 proof - |
|
1441 have "(\<lambda>f :: 'a \<Rightarrow>\<^isub>f 'b. (f, g)\<^sup>f) = (\<lambda>f. Abs_finfun ((\<lambda>x. (Rep_finfun f x, Rep_finfun g x))))" |
|
1442 proof(rule finfun_rec_unique) |
|
1443 { fix c show "Abs_finfun (\<lambda>x. (Rep_finfun (\<lambda>\<^isup>f c) x, Rep_finfun g x)) = Pair c \<circ>\<^isub>f g" |
|
1444 by(simp add: finfun_comp_conv_comp finfun_apply_Rep_finfun o_def finfun_const_def) } |
|
1445 { fix g' a b |
|
1446 show "Abs_finfun (\<lambda>x. (Rep_finfun g'(\<^sup>f a := b) x, Rep_finfun g x)) = |
|
1447 (Abs_finfun (\<lambda>x. (Rep_finfun g' x, Rep_finfun g x)))(\<^sup>f a := (b, g\<^sub>f a))" |
|
1448 by(auto simp add: finfun_update_def expand_fun_eq finfun_apply_Rep_finfun simp del: fun_upd_apply) simp } |
|
1449 qed(simp_all add: finfun_Diag_const1 finfun_Diag_update1) |
|
1450 thus ?thesis by(auto simp add: expand_fun_eq) |
|
1451 qed |
|
1452 |
|
1453 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del] |
|
1454 |
|
1455 lemma finfun_Diag_eq: "(f, g)\<^sup>f = (f', g')\<^sup>f \<longleftrightarrow> f = f' \<and> g = g'" |
|
1456 by(auto simp add: expand_finfun_eq expand_fun_eq) |
|
1457 |
|
1458 definition finfun_fst :: "'a \<Rightarrow>\<^isub>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" |
|
1459 where [code]: "finfun_fst f = fst \<circ>\<^isub>f f" |
|
1460 |
|
1461 lemma finfun_fst_const: "finfun_fst (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f fst bc)" |
|
1462 by(simp add: finfun_fst_def) |
|
1463 |
|
1464 lemma finfun_fst_update: "finfun_fst (f(\<^sup>f a := bc)) = (finfun_fst f)(\<^sup>f a := fst bc)" |
|
1465 and finfun_fst_update_code: "finfun_fst (finfun_update_code f a bc) = (finfun_fst f)(\<^sup>f a := fst bc)" |
|
1466 by(simp_all add: finfun_fst_def) |
|
1467 |
|
1468 lemma finfun_fst_comp_conv: "finfun_fst (f \<circ>\<^isub>f g) = (fst \<circ> f) \<circ>\<^isub>f g" |
|
1469 by(simp add: finfun_fst_def) |
|
1470 |
|
1471 lemma finfun_fst_conv [simp]: "finfun_fst (f, g)\<^sup>f = f" |
|
1472 by(induct f rule: finfun_weak_induct)(simp_all add: finfun_Diag_const1 finfun_fst_comp_conv o_def finfun_Diag_update1 finfun_fst_update) |
|
1473 |
|
1474 lemma finfun_fst_conv_Abs_finfun: "finfun_fst = (\<lambda>f. Abs_finfun (fst o Rep_finfun f))" |
|
1475 by(simp add: finfun_fst_def_raw finfun_comp_conv_comp finfun_apply_Rep_finfun) |
|
1476 |
|
1477 |
|
1478 definition finfun_snd :: "'a \<Rightarrow>\<^isub>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c" |
|
1479 where [code]: "finfun_snd f = snd \<circ>\<^isub>f f" |
|
1480 |
|
1481 lemma finfun_snd_const: "finfun_snd (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f snd bc)" |
|
1482 by(simp add: finfun_snd_def) |
|
1483 |
|
1484 lemma finfun_snd_update: "finfun_snd (f(\<^sup>f a := bc)) = (finfun_snd f)(\<^sup>f a := snd bc)" |
|
1485 and finfun_snd_update_code [code]: "finfun_snd (finfun_update_code f a bc) = (finfun_snd f)(\<^sup>f a := snd bc)" |
|
1486 by(simp_all add: finfun_snd_def) |
|
1487 |
|
1488 lemma finfun_snd_comp_conv: "finfun_snd (f \<circ>\<^isub>f g) = (snd \<circ> f) \<circ>\<^isub>f g" |
|
1489 by(simp add: finfun_snd_def) |
|
1490 |
|
1491 lemma finfun_snd_conv [simp]: "finfun_snd (f, g)\<^sup>f = g" |
|
1492 apply(induct f rule: finfun_weak_induct) |
|
1493 apply(auto simp add: finfun_Diag_const1 finfun_snd_comp_conv o_def finfun_Diag_update1 finfun_snd_update finfun_upd_apply intro: finfun_ext) |
|
1494 done |
|
1495 |
|
1496 lemma finfun_snd_conv_Abs_finfun: "finfun_snd = (\<lambda>f. Abs_finfun (snd o Rep_finfun f))" |
|
1497 by(simp add: finfun_snd_def_raw finfun_comp_conv_comp finfun_apply_Rep_finfun) |
|
1498 |
|
1499 lemma finfun_Diag_collapse [simp]: "(finfun_fst f, finfun_snd f)\<^sup>f = f" |
|
1500 by(induct f rule: finfun_weak_induct)(simp_all add: finfun_fst_const finfun_snd_const finfun_fst_update finfun_snd_update finfun_Diag_update_update) |
|
1501 |
|
1502 subsection {* Currying for FinFuns *} |
|
1503 |
|
1504 definition finfun_curry :: "('a \<times> 'b) \<Rightarrow>\<^isub>f 'c \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b \<Rightarrow>\<^isub>f 'c" |
|
1505 where [code del]: "finfun_curry = finfun_rec (finfun_const \<circ> finfun_const) (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c)))" |
|
1506 |
|
1507 interpretation finfun_curry_aux: finfun_rec_wf_aux "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))" |
|
1508 apply(unfold_locales) |
|
1509 apply(auto simp add: split_def finfun_update_twist finfun_upd_apply split_paired_all finfun_update_const_same) |
|
1510 done |
|
1511 |
|
1512 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro] |
|
1513 |
|
1514 interpretation finfun_curry: finfun_rec_wf "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))" |
|
1515 proof(unfold_locales) |
|
1516 fix b' b :: 'b |
|
1517 assume fin: "finite (UNIV :: ('c \<times> 'a) set)" |
|
1518 hence fin1: "finite (UNIV :: 'c set)" and fin2: "finite (UNIV :: 'a set)" |
|
1519 unfolding UNIV_Times_UNIV[symmetric] |
|
1520 by(fastsimp dest: finite_cartesian_productD1 finite_cartesian_productD2)+ |
|
1521 note [simp] = Abs_finfun_inverse_finite[OF fin] Abs_finfun_inverse_finite[OF fin1] Abs_finfun_inverse_finite[OF fin2] |
|
1522 { fix A :: "('c \<times> 'a) set" |
|
1523 interpret fun_left_comm "\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))) a b'" |
|
1524 by(rule finfun_curry_aux.upd_left_comm) |
|
1525 from fin have "finite A" by(auto intro: finite_subset) |
|
1526 hence "fold (\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))) a b') ((finfun_const \<circ> finfun_const) b) A = Abs_finfun (\<lambda>a. Abs_finfun (\<lambda>b''. if (a, b'') \<in> A then b' else b))" |
|
1527 by induct (simp_all, auto simp add: finfun_update_def finfun_const_def split_def finfun_apply_Rep_finfun intro!: arg_cong[where f="Abs_finfun"] ext) } |
|
1528 from this[of UNIV] |
|
1529 show "fold (\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))) a b') ((finfun_const \<circ> finfun_const) b) UNIV = (finfun_const \<circ> finfun_const) b'" |
|
1530 by(simp add: finfun_const_def) |
|
1531 qed |
|
1532 |
|
1533 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del] |
|
1534 |
|
1535 lemma finfun_curry_const [simp, code]: "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)" |
|
1536 by(simp add: finfun_curry_def) |
|
1537 |
|
1538 lemma finfun_curry_update [simp]: |
|
1539 "finfun_curry (f(\<^sup>f (a, b) := c)) = (finfun_curry f)(\<^sup>f a := ((finfun_curry f)\<^sub>f a)(\<^sup>f b := c))" |
|
1540 and finfun_curry_update_code [code]: |
|
1541 "finfun_curry (f(\<^sup>f\<^sup>c (a, b) := c)) = (finfun_curry f)(\<^sup>f a := ((finfun_curry f)\<^sub>f a)(\<^sup>f b := c))" |
|
1542 by(simp_all add: finfun_curry_def) |
|
1543 |
|
1544 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro] |
|
1545 |
|
1546 lemma finfun_Abs_finfun_curry: assumes fin: "f \<in> finfun" |
|
1547 shows "(\<lambda>a. Abs_finfun (curry f a)) \<in> finfun" |
|
1548 proof - |
|
1549 from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast |
|
1550 have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force) |
|
1551 hence "{a. curry f a \<noteq> (\<lambda>x. c)} = fst ` {ab. f ab \<noteq> c}" |
|
1552 by(auto simp add: curry_def expand_fun_eq) |
|
1553 with fin c have "finite {a. Abs_finfun (curry f a) \<noteq> (\<lambda>\<^isup>f c)}" |
|
1554 by(simp add: finfun_const_def finfun_curry) |
|
1555 thus ?thesis unfolding finfun_def by auto |
|
1556 qed |
|
1557 |
|
1558 lemma finfun_curry_conv_curry: |
|
1559 fixes f :: "('a \<times> 'b) \<Rightarrow>\<^isub>f 'c" |
|
1560 shows "finfun_curry f = Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun f) a))" |
|
1561 proof - |
|
1562 have "finfun_curry = (\<lambda>f :: ('a \<times> 'b) \<Rightarrow>\<^isub>f 'c. Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun f) a)))" |
|
1563 proof(rule finfun_rec_unique) |
|
1564 { fix c show "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)" by simp } |
|
1565 { fix f a c show "finfun_curry (f(\<^sup>f a := c)) = (finfun_curry f)(\<^sup>f fst a := ((finfun_curry f)\<^sub>f (fst a))(\<^sup>f snd a := c))" |
|
1566 by(cases a) simp } |
|
1567 { fix c show "Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun (\<lambda>\<^isup>f c)) a)) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)" |
|
1568 by(simp add: finfun_curry_def finfun_const_def curry_def) } |
|
1569 { fix g a b |
|
1570 show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (Rep_finfun g(\<^sup>f a := b)) aa)) = |
|
1571 (Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun g) a)))(\<^sup>f |
|
1572 fst a := ((Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun g) a)))\<^sub>f (fst a))(\<^sup>f snd a := b))" |
|
1573 by(cases a)(auto intro!: ext arg_cong[where f=Abs_finfun] simp add: finfun_curry_def finfun_update_def finfun_apply_Rep_finfun finfun_curry finfun_Abs_finfun_curry) } |
|
1574 qed |
|
1575 thus ?thesis by(auto simp add: expand_fun_eq) |
|
1576 qed |
|
1577 |
|
1578 subsection {* Executable equality for FinFuns *} |
|
1579 |
|
1580 lemma eq_finfun_All_ext: "(f = g) \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>\<^isub>f (f, g)\<^sup>f)" |
|
1581 by(simp add: expand_finfun_eq expand_fun_eq finfun_All_All o_def) |
|
1582 |
|
1583 instantiation finfun :: ("{card_UNIV,eq}",eq) eq begin |
|
1584 definition eq_finfun_def: "eq_class.eq f g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>\<^isub>f (f, g)\<^sup>f)" |
|
1585 instance by(intro_classes)(simp add: eq_finfun_All_ext eq_finfun_def) |
|
1586 end |
|
1587 |
|
1588 subsection {* Operator that explicitly removes all redundant updates in the generated representations *} |
|
1589 |
|
1590 definition finfun_clearjunk :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" |
|
1591 where [simp, code del]: "finfun_clearjunk = id" |
|
1592 |
|
1593 lemma finfun_clearjunk_const [code]: "finfun_clearjunk (\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b)" |
|
1594 by simp |
|
1595 |
|
1596 lemma finfun_clearjunk_update [code]: "finfun_clearjunk (finfun_update_code f a b) = f(\<^sup>f a := b)" |
|
1597 by simp |
|
1598 |
|
1599 end |
|