2 (* Author: Andreas Lochbihler, Uni Karlsruhe *)
4 header {* Almost everywhere constant functions *}
7 imports Main Infinite_Set Enum
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.
17 For details, see Formalising FinFuns - Generating Code for Functions as Data by A. Lochbihler in TPHOLs 2009.
20 subsection {* Auxiliary definitions and lemmas *}
22 (*FIXME move these to Finite_Set.thy*)
23 lemma card_ge_0_finite:
24 "card A > 0 \<Longrightarrow> finite A"
25 by(rule ccontr, drule card_infinite, simp)
27 lemma finite_UNIV_card_ge_0:
28 "finite (UNIV :: 'a set) \<Longrightarrow> card (UNIV :: 'a set) > 0"
31 lemma card_eq_UNIV_imp_eq_UNIV:
32 assumes fin: "finite (UNIV :: 'a set)"
33 and card: "card A = card (UNIV :: 'a set)"
34 shows "A = (UNIV :: 'a set)"
37 show "A \<subseteq> UNIV" by simp
38 show "UNIV \<subseteq> A"
44 hence "A \<subset> UNIV" by auto
45 from psubset_card_mono[OF fin this] card show False by simp
50 lemma finite_fun_UNIVD2: assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
51 shows "finite (UNIV :: 'b set)"
53 from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))"
54 by(rule finite_imageI)
55 moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary)"
56 by(rule UNIV_eq_I) auto
57 ultimately show "finite (UNIV :: 'b set)" by simp
60 lemma finite_fun_UNIVD1: assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
61 and card: "card (UNIV :: 'b set) \<noteq> Suc 0"
62 shows "finite (UNIV :: 'a set)"
64 from fin have finb: "finite (UNIV :: 'b set)" by(rule finite_fun_UNIVD2)
65 with card have "card (UNIV :: 'b set) \<ge> Suc (Suc 0)"
66 by(cases "card (UNIV :: 'b set)")(auto simp add: card_eq_0_iff)
67 then obtain n where "card (UNIV :: 'b set) = Suc (Suc n)" "n = card (UNIV :: 'b set) - 2" by(auto)
68 then obtain b1 b2 where b1b2: "(b1 :: 'b) \<noteq> (b2 :: 'b)" by(auto simp add: card_Suc_eq)
69 from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1))" by(rule finite_imageI)
70 moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1)"
73 from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" by(simp add: inv_def)
74 thus "x \<in> range (\<lambda>f\<Colon>'a \<Rightarrow> 'b. inv f b1)" by blast
76 ultimately show "finite (UNIV :: 'a set)" by simp
79 (*FIXME move to Map.thy*)
80 lemma restrict_map_insert: "f |` (insert a A) = (f |` A)(a := f a)"
81 by(auto simp add: restrict_map_def intro: ext)
83 definition map_default :: "'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
84 where "map_default b f a \<equiv> case f a of None \<Rightarrow> b | Some b' \<Rightarrow> b'"
86 lemma map_default_delete [simp]:
87 "map_default b (f(a := None)) = (map_default b f)(a := b)"
88 by(simp add: map_default_def expand_fun_eq)
90 lemma map_default_insert:
91 "map_default b (f(a \<mapsto> b')) = (map_default b f)(a := b')"
92 by(simp add: map_default_def expand_fun_eq)
94 lemma map_default_empty [simp]: "map_default b empty = (\<lambda>a. b)"
95 by(simp add: expand_fun_eq map_default_def)
97 lemma map_default_inject:
98 fixes g g' :: "'a \<rightharpoonup> 'b"
99 assumes infin_eq: "\<not> finite (UNIV :: 'a set) \<or> b = b'"
100 and fin: "finite (dom g)" and b: "b \<notin> ran g"
101 and fin': "finite (dom g')" and b': "b' \<notin> ran g'"
102 and eq': "map_default b g = map_default b' g'"
103 shows "b = b'" "g = g'"
105 from infin_eq show bb': "b = b'"
107 assume infin: "\<not> finite (UNIV :: 'a set)"
108 from fin fin' have "finite (dom g \<union> dom g')" by auto
109 with infin have "UNIV - (dom g \<union> dom g') \<noteq> {}" by(auto dest: finite_subset)
110 then obtain a where a: "a \<notin> dom g \<union> dom g'" by auto
111 hence "map_default b g a = b" "map_default b' g' a = b'" by(auto simp add: map_default_def)
112 with eq' show "b = b'" by simp
121 hence "map_default b g x = b" by(simp add: map_default_def)
122 with bb' eq' have "map_default b' g' x = b'" by simp
123 with b' have "g' x = None" by(simp add: map_default_def ran_def split: option.split_asm)
124 with None show ?thesis by simp
127 with b have cb: "c \<noteq> b" by(auto simp add: ran_def)
128 moreover from Some have "map_default b g x = c" by(simp add: map_default_def)
129 with eq' have "map_default b' g' x = c" by simp
130 ultimately have "g' x = Some c" using b' bb' by(auto simp add: map_default_def split: option.splits)
131 with Some show ?thesis by simp
136 subsection {* The finfun type *}
138 typedef ('a,'b) finfun = "{f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}"
140 apply(rule_tac x="\<lambda>x. arbitrary" in exI)
145 "finfun" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ \<Rightarrow>\<^isub>f /_)" [22, 21] 21)
147 lemma fun_upd_finfun: "y(a := b) \<in> finfun \<longleftrightarrow> y \<in> finfun"
150 have "finite {a'. (y(a := b)) a' \<noteq> b'} = finite {a'. y a' \<noteq> b'}"
151 proof(cases "b = b'")
153 hence "{a'. (y(a := b)) a' \<noteq> b'} = {a'. y a' \<noteq> b'} - {a}" by auto
157 hence "{a'. (y(a := b)) a' \<noteq> b'} = insert a {a'. y a' \<noteq> b'}" by auto
160 thus ?thesis unfolding finfun_def by blast
163 lemma const_finfun: "(\<lambda>x. a) \<in> finfun"
164 by(auto simp add: finfun_def)
166 lemma finfun_left_compose:
167 assumes "y \<in> finfun"
168 shows "g \<circ> y \<in> finfun"
170 from assms obtain b where "finite {a. y a \<noteq> b}"
171 unfolding finfun_def by blast
172 hence "finite {c. g (y c) \<noteq> g b}"
173 proof(induct x\<equiv>"{a. y a \<noteq> b}" arbitrary: y)
175 hence "y = (\<lambda>a. b)" by(auto intro: ext)
179 note IH = `\<And>y. F = {a. y a \<noteq> b} \<Longrightarrow> finite {c. g (y c) \<noteq> g b}`
180 from `insert x F = {a. y a \<noteq> b}` `x \<notin> F`
181 have F: "F = {a. (y(x := b)) a \<noteq> b}" by(auto)
183 proof(cases "g (y x) = g b")
185 hence "{c. g ((y(x := b)) c) \<noteq> g b} = {c. g (y c) \<noteq> g b}" by auto
186 with IH[OF F] show ?thesis by simp
189 hence "{c. g (y c) \<noteq> g b} = insert x {c. g ((y(x := b)) c) \<noteq> g b}" by auto
190 with IH[OF F] show ?thesis by(simp)
193 thus ?thesis unfolding finfun_def by auto
196 lemma assumes "y \<in> finfun"
197 shows fst_finfun: "fst \<circ> y \<in> finfun"
198 and snd_finfun: "snd \<circ> y \<in> finfun"
200 from assms obtain b c where bc: "finite {a. y a \<noteq> (b, c)}"
201 unfolding finfun_def by auto
202 have "{a. fst (y a) \<noteq> b} \<subseteq> {a. y a \<noteq> (b, c)}"
203 and "{a. snd (y a) \<noteq> c} \<subseteq> {a. y a \<noteq> (b, c)}" by auto
204 hence "finite {a. fst (y a) \<noteq> b}"
205 and "finite {a. snd (y a) \<noteq> c}" using bc by(auto intro: finite_subset)
206 thus "fst \<circ> y \<in> finfun" "snd \<circ> y \<in> finfun"
207 unfolding finfun_def by auto
210 lemma map_of_finfun: "map_of xs \<in> finfun"
212 by(induct xs)(auto simp add: Collect_neg_eq Collect_conj_eq Collect_imp_eq intro: finite_subset)
214 lemma Diag_finfun: "(\<lambda>x. (f x, g x)) \<in> finfun \<longleftrightarrow> f \<in> finfun \<and> g \<in> finfun"
215 by(auto intro: finite_subset simp add: Collect_neg_eq Collect_imp_eq Collect_conj_eq finfun_def)
217 lemma finfun_right_compose:
218 assumes g: "g \<in> finfun" and inj: "inj f"
219 shows "g o f \<in> finfun"
221 from g obtain b where b: "finite {a. g a \<noteq> b}" unfolding finfun_def by blast
222 moreover have "f ` {a. g (f a) \<noteq> b} \<subseteq> {a. g a \<noteq> b}" by auto
223 moreover from inj have "inj_on f {a. g (f a) \<noteq> b}" by(rule subset_inj_on) blast
224 ultimately have "finite {a. g (f a) \<noteq> b}"
225 by(blast intro: finite_imageD[where f=f] finite_subset)
226 thus ?thesis unfolding finfun_def by auto
230 assumes fin: "f \<in> finfun"
231 shows "curry f \<in> finfun" "curry f a \<in> finfun"
233 from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast
234 moreover have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force)
235 hence "{a. curry f a \<noteq> (\<lambda>b. c)} = fst ` {ab. f ab \<noteq> c}"
236 by(auto simp add: curry_def expand_fun_eq)
237 ultimately have "finite {a. curry f a \<noteq> (\<lambda>b. c)}" by simp
238 thus "curry f \<in> finfun" unfolding finfun_def by blast
240 have "snd ` {ab. f ab \<noteq> c} = {b. \<exists>a. f (a, b) \<noteq> c}" by(force)
241 hence "{b. f (a, b) \<noteq> c} \<subseteq> snd ` {ab. f ab \<noteq> c}" by auto
242 hence "finite {b. f (a, b) \<noteq> c}" by(rule finite_subset)(rule finite_imageI[OF c])
243 thus "curry f a \<in> finfun" unfolding finfun_def by auto
247 fst_finfun snd_finfun Abs_finfun_inverse Rep_finfun_inverse Abs_finfun_inject Rep_finfun_inject Diag_finfun finfun_curry
248 lemmas finfun_iff = const_finfun fun_upd_finfun Rep_finfun map_of_finfun
249 lemmas finfun_intro = finfun_left_compose fst_finfun snd_finfun
251 lemma Abs_finfun_inject_finite:
252 fixes x y :: "'a \<Rightarrow> 'b"
253 assumes fin: "finite (UNIV :: 'a set)"
254 shows "Abs_finfun x = Abs_finfun y \<longleftrightarrow> x = y"
256 assume "Abs_finfun x = Abs_finfun y"
257 moreover have "x \<in> finfun" "y \<in> finfun" unfolding finfun_def
258 by(auto intro: finite_subset[OF _ fin])
259 ultimately show "x = y" by(simp add: Abs_finfun_inject)
262 lemma Abs_finfun_inject_finite_class:
263 fixes x y :: "('a :: finite) \<Rightarrow> 'b"
264 shows "Abs_finfun x = Abs_finfun y \<longleftrightarrow> x = y"
266 by(simp add: Abs_finfun_inject_finite)
268 lemma Abs_finfun_inj_finite:
269 assumes fin: "finite (UNIV :: 'a set)"
270 shows "inj (Abs_finfun :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b)"
272 fix x y :: "'a \<Rightarrow> 'b"
273 assume "Abs_finfun x = Abs_finfun y"
274 moreover have "x \<in> finfun" "y \<in> finfun" unfolding finfun_def
275 by(auto intro: finite_subset[OF _ fin])
276 ultimately show "x = y" by(simp add: Abs_finfun_inject)
279 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
281 lemma Abs_finfun_inverse_finite:
282 fixes x :: "'a \<Rightarrow> 'b"
283 assumes fin: "finite (UNIV :: 'a set)"
284 shows "Rep_finfun (Abs_finfun x) = x"
286 from fin have "x \<in> finfun"
287 by(auto simp add: finfun_def intro: finite_subset)
291 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
293 lemma Abs_finfun_inverse_finite_class:
294 fixes x :: "('a :: finite) \<Rightarrow> 'b"
295 shows "Rep_finfun (Abs_finfun x) = x"
296 using finite_UNIV by(simp add: Abs_finfun_inverse_finite)
298 lemma finfun_eq_finite_UNIV: "finite (UNIV :: 'a set) \<Longrightarrow> (finfun :: ('a \<Rightarrow> 'b) set) = UNIV"
299 unfolding finfun_def by(auto intro: finite_subset)
301 lemma finfun_finite_UNIV_class: "finfun = (UNIV :: ('a :: finite \<Rightarrow> 'b) set)"
302 by(simp add: finfun_eq_finite_UNIV)
304 lemma map_default_in_finfun:
305 assumes fin: "finite (dom f)"
306 shows "map_default b f \<in> finfun"
308 proof(intro CollectI exI)
309 from fin show "finite {a. map_default b f a \<noteq> b}"
310 by(auto simp add: map_default_def dom_def Collect_conj_eq split: option.splits)
313 lemma finfun_cases_map_default:
314 obtains b g where "f = Abs_finfun (map_default b g)" "finite (dom g)" "b \<notin> ran g"
316 obtain y where f: "f = Abs_finfun y" and y: "y \<in> finfun" by(cases f)
317 from y obtain b where b: "finite {a. y a \<noteq> b}" unfolding finfun_def by auto
318 let ?g = "(\<lambda>a. if y a = b then None else Some (y a))"
319 have "map_default b ?g = y" by(simp add: expand_fun_eq map_default_def)
320 with f have "f = Abs_finfun (map_default b ?g)" by simp
321 moreover from b have "finite (dom ?g)" by(auto simp add: dom_def)
322 moreover have "b \<notin> ran ?g" by(auto simp add: ran_def)
323 ultimately show ?thesis by(rule that)
327 subsection {* Kernel functions for type @{typ "'a \<Rightarrow>\<^isub>f 'b"} *}
329 definition finfun_const :: "'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("\<lambda>\<^isup>f/ _" [0] 1)
330 where [code del]: "(\<lambda>\<^isup>f b) = Abs_finfun (\<lambda>x. b)"
332 definition finfun_update :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("_'(\<^sup>f/ _ := _')" [1000,0,0] 1000)
333 where [code del]: "f(\<^sup>fa := b) = Abs_finfun ((Rep_finfun f)(a := b))"
335 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
337 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)"
338 by(simp add: finfun_update_def fun_upd_twist)
340 lemma finfun_update_twice [simp]:
341 "finfun_update (finfun_update f a b) a b' = finfun_update f a b'"
342 by(simp add: finfun_update_def)
344 lemma finfun_update_const_same: "(\<lambda>\<^isup>f b)(\<^sup>f a := b) = (\<lambda>\<^isup>f b)"
345 by(simp add: finfun_update_def finfun_const_def expand_fun_eq)
347 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
349 subsection {* Code generator setup *}
351 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)
352 where [simp, code del]: "finfun_update_code = finfun_update"
354 code_datatype finfun_const finfun_update_code
356 lemma finfun_update_const_code [code]:
357 "(\<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')"
358 by(simp add: finfun_update_const_same)
360 lemma finfun_update_update_code [code]:
361 "(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)"
362 by(simp add: finfun_update_twist)
365 subsection {* Setup for quickcheck *}
367 notation fcomp (infixl "o>" 60)
368 notation scomp (infixl "o\<rightarrow>" 60)
370 definition (in term_syntax) valtermify_finfun_const ::
371 "'b\<Colon>typerep \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> ('a\<Colon>typerep \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Eval.term)" where
372 "valtermify_finfun_const y = Code_Eval.valtermify finfun_const {\<cdot>} y"
374 definition (in term_syntax) valtermify_finfun_update_code ::
375 "'a\<Colon>typerep \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> 'b\<Colon>typerep \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Eval.term)" where
376 "valtermify_finfun_update_code x y f = Code_Eval.valtermify finfun_update_code {\<cdot>} f {\<cdot>} x {\<cdot>} y"
378 instantiation finfun :: (random, random) random
381 primrec random_finfun' :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
382 "random_finfun' 0 j = Quickcheck.collapse (Random.select_default 0
383 (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))
384 (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y))))"
385 | "random_finfun' (Suc_code_numeral i) j = Quickcheck.collapse (Random.select_default i
386 (random j o\<rightarrow> (\<lambda>x. random j o\<rightarrow> (\<lambda>y. random_finfun' i j o\<rightarrow> (\<lambda>f. Pair (valtermify_finfun_update_code x y f)))))
387 (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y))))"
390 "random i = random_finfun' i i"
396 lemma select_default_zero:
397 "Random.select_default 0 y y = Random.select_default 0 x y"
398 by (simp add: select_default_def)
400 lemma random_finfun'_code [code]:
401 "random_finfun' i j = Quickcheck.collapse (Random.select_default (i - 1)
402 (random j o\<rightarrow> (\<lambda>x. random j o\<rightarrow> (\<lambda>y. random_finfun' (i - 1) j o\<rightarrow> (\<lambda>f. Pair (valtermify_finfun_update_code x y f)))))
403 (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y))))"
404 apply (cases i rule: code_numeral.exhaust)
405 apply (simp_all only: random_finfun'.simps code_numeral_zero_minus_one Suc_code_numeral_minus_one)
406 apply (subst select_default_zero) apply (simp only:)
409 no_notation fcomp (infixl "o>" 60)
410 no_notation scomp (infixl "o\<rightarrow>" 60)
413 subsection {* @{text "finfun_update"} as instance of @{text "fun_left_comm"} *}
415 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
417 interpretation finfun_update: fun_left_comm "\<lambda>a f. f(\<^sup>f a :: 'a := b')"
421 have "(Rep_finfun b)(a := b', a' := b') = (Rep_finfun b)(a' := b', a := b')"
422 by(cases "a = a'")(auto simp add: fun_upd_twist)
423 thus "b(\<^sup>f a := b')(\<^sup>f a' := b') = b(\<^sup>f a' := b')(\<^sup>f a := b')"
424 by(auto simp add: finfun_update_def fun_upd_twist)
427 lemma fold_finfun_update_finite_univ:
428 assumes fin: "finite (UNIV :: 'a set)"
429 shows "fold (\<lambda>a f. f(\<^sup>f a := b')) (\<lambda>\<^isup>f b) (UNIV :: 'a set) = (\<lambda>\<^isup>f b')"
432 from fin have "finite A" by(auto intro: finite_subset)
433 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)"
436 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)"
438 with insert show ?case
439 by(simp add: finfun_const_def fun_upd_def)(simp add: finfun_update_def Abs_finfun_inverse_finite[OF fin] fun_upd_def)
440 qed(simp add: finfun_const_def) }
441 thus ?thesis by(simp add: finfun_const_def)
445 subsection {* Default value for FinFuns *}
447 definition finfun_default_aux :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"
448 where [code del]: "finfun_default_aux f = (if finite (UNIV :: 'a set) then arbitrary else THE b. finite {a. f a \<noteq> b})"
450 lemma finfun_default_aux_infinite:
451 fixes f :: "'a \<Rightarrow> 'b"
452 assumes infin: "infinite (UNIV :: 'a set)"
453 and fin: "finite {a. f a \<noteq> b}"
454 shows "finfun_default_aux f = b"
456 let ?B = "{a. f a \<noteq> b}"
457 from fin have "(THE b. finite {a. f a \<noteq> b}) = b"
458 proof(rule the_equality)
460 assume "finite {a. f a \<noteq> b'}" (is "finite ?B'")
461 with infin fin have "UNIV - (?B' \<union> ?B) \<noteq> {}" by(auto dest: finite_subset)
462 then obtain a where a: "a \<notin> ?B' \<union> ?B" by auto
463 thus "b' = b" by auto
465 thus ?thesis using infin by(simp add: finfun_default_aux_def)
469 lemma finite_finfun_default_aux:
470 fixes f :: "'a \<Rightarrow> 'b"
471 assumes fin: "f \<in> finfun"
472 shows "finite {a. f a \<noteq> finfun_default_aux f}"
473 proof(cases "finite (UNIV :: 'a set)")
474 case True thus ?thesis using fin
475 by(auto simp add: finfun_def finfun_default_aux_def intro: finite_subset)
478 from fin obtain b where b: "finite {a. f a \<noteq> b}" (is "finite ?B")
479 unfolding finfun_def by blast
480 with False show ?thesis by(simp add: finfun_default_aux_infinite)
483 lemma finfun_default_aux_update_const:
484 fixes f :: "'a \<Rightarrow> 'b"
485 assumes fin: "f \<in> finfun"
486 shows "finfun_default_aux (f(a := b)) = finfun_default_aux f"
487 proof(cases "finite (UNIV :: 'a set)")
489 from fin obtain b' where b': "finite {a. f a \<noteq> b'}" unfolding finfun_def by blast
490 hence "finite {a'. (f(a := b)) a' \<noteq> b'}"
491 proof(cases "b = b' \<and> f a \<noteq> b'")
493 hence "{a. f a \<noteq> b'} = insert a {a'. (f(a := b)) a' \<noteq> b'}" by auto
494 thus ?thesis using b' by simp
498 { assume "b \<noteq> b'"
499 hence "{a'. (f(a := b)) a' \<noteq> b'} = insert a {a. f a \<noteq> b'}" by auto
500 hence ?thesis using b' by simp }
502 { assume "b = b'" "f a = b'"
503 hence "{a'. (f(a := b)) a' \<noteq> b'} = {a. f a \<noteq> b'}" by auto
504 hence ?thesis using b' by simp }
505 ultimately show ?thesis by blast
507 with False b' show ?thesis by(auto simp del: fun_upd_apply simp add: finfun_default_aux_infinite)
509 case True thus ?thesis by(simp add: finfun_default_aux_def)
512 definition finfun_default :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'b"
513 where [code del]: "finfun_default f = finfun_default_aux (Rep_finfun f)"
515 lemma finite_finfun_default: "finite {a. Rep_finfun f a \<noteq> finfun_default f}"
516 unfolding finfun_default_def by(simp add: finite_finfun_default_aux)
518 lemma finfun_default_const: "finfun_default ((\<lambda>\<^isup>f b) :: 'a \<Rightarrow>\<^isub>f 'b) = (if finite (UNIV :: 'a set) then arbitrary else b)"
519 apply(auto simp add: finfun_default_def finfun_const_def finfun_default_aux_infinite)
520 apply(simp add: finfun_default_aux_def)
523 lemma finfun_default_update_const:
524 "finfun_default (f(\<^sup>f a := b)) = finfun_default f"
525 unfolding finfun_default_def finfun_update_def
526 by(simp add: finfun_default_aux_update_const)
528 subsection {* Recursion combinator and well-formedness conditions *}
530 definition finfun_rec :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<Rightarrow> 'c"
532 "finfun_rec cnst upd f \<equiv>
533 let b = finfun_default f;
534 g = THE g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g
535 in fold (\<lambda>a. upd a (map_default b g a)) (cnst b) (dom g)"
537 locale finfun_rec_wf_aux =
538 fixes cnst :: "'b \<Rightarrow> 'c"
539 and upd :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c"
540 assumes upd_const_same: "upd a b (cnst b) = cnst b"
541 and upd_commute: "a \<noteq> a' \<Longrightarrow> upd a b (upd a' b' c) = upd a' b' (upd a b c)"
542 and upd_idemp: "b \<noteq> b' \<Longrightarrow> upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)"
546 lemma upd_left_comm: "fun_left_comm (\<lambda>a. upd a (f a))"
547 by(unfold_locales)(auto intro: upd_commute)
549 lemma upd_upd_twice: "upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)"
550 by(cases "b \<noteq> b'")(auto simp add: fun_upd_def upd_const_same upd_idemp)
552 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
554 lemma map_default_update_const:
555 assumes fin: "finite (dom f)"
556 and anf: "a \<notin> dom f"
557 and fg: "f \<subseteq>\<^sub>m g"
558 shows "upd a d (fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f)) =
559 fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f)"
561 let ?upd = "\<lambda>a. upd a (map_default d g a)"
562 let ?fr = "\<lambda>A. fold ?upd (cnst d) A"
563 interpret gwf: fun_left_comm "?upd" by(rule upd_left_comm)
565 from fin anf fg show ?thesis
566 proof(induct A\<equiv>"dom f" arbitrary: f)
568 from `{} = dom f` have "f = empty" by(auto simp add: dom_def intro: ext)
569 thus ?case by(simp add: finfun_const_def upd_const_same)
572 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)`
573 note fin = `finite A` note anf = `a \<notin> dom f` note a'nA = `a' \<notin> A`
574 note domf = `insert a' A = dom f` note fg = `f \<subseteq>\<^sub>m g`
576 from domf obtain b where b: "f a' = Some b" by auto
577 let ?f' = "f(a' := None)"
578 have "upd a d (?fr (insert a' A)) = upd a d (upd a' (map_default d g a') (?fr A))"
579 by(subst gwf.fold_insert[OF fin a'nA]) rule
580 also from b fg have "g a' = f a'" by(auto simp add: map_le_def intro: domI dest: bspec)
581 hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def)
582 also from anf domf have "a \<noteq> a'" by auto note upd_commute[OF this]
583 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)
584 note A also note IH[OF `a \<notin> dom ?f'` `?f' \<subseteq>\<^sub>m g` A]
585 also have "upd a' (map_default d f a') (?fr (dom (f(a' := None)))) = ?fr (dom f)"
586 unfolding domf[symmetric] gwf.fold_insert[OF fin a'nA] ga' unfolding A ..
587 also have "insert a' (dom ?f') = dom f" using domf by auto
592 lemma map_default_update_twice:
593 assumes fin: "finite (dom f)"
594 and anf: "a \<notin> dom f"
595 and fg: "f \<subseteq>\<^sub>m g"
596 shows "upd a d'' (upd a d' (fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f))) =
597 upd a d'' (fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f))"
599 let ?upd = "\<lambda>a. upd a (map_default d g a)"
600 let ?fr = "\<lambda>A. fold ?upd (cnst d) A"
601 interpret gwf: fun_left_comm "?upd" by(rule upd_left_comm)
603 from fin anf fg show ?thesis
604 proof(induct A\<equiv>"dom f" arbitrary: f)
606 from `{} = dom f` have "f = empty" by(auto simp add: dom_def intro: ext)
607 thus ?case by(auto simp add: finfun_const_def finfun_update_def upd_upd_twice)
610 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))`
611 note fin = `finite A` note anf = `a \<notin> dom f` note a'nA = `a' \<notin> A`
612 note domf = `insert a' A = dom f` note fg = `f \<subseteq>\<^sub>m g`
614 from domf obtain b where b: "f a' = Some b" by auto
615 let ?f' = "f(a' := None)"
616 let ?b' = "case f a' of None \<Rightarrow> d | Some b \<Rightarrow> b"
617 from domf have "upd a d'' (upd a d' (?fr (dom f))) = upd a d'' (upd a d' (?fr (insert a' A)))" by simp
618 also note gwf.fold_insert[OF fin a'nA]
619 also from b fg have "g a' = f a'" by(auto simp add: map_le_def intro: domI dest: bspec)
620 hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def)
621 also from anf domf have ana': "a \<noteq> a'" by auto note upd_commute[OF this]
622 also note upd_commute[OF ana']
623 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)
624 note A also note IH[OF `a \<notin> dom ?f'` `?f' \<subseteq>\<^sub>m g` A]
625 also note upd_commute[OF ana'[symmetric]] also note ga'[symmetric] also note A[symmetric]
626 also note gwf.fold_insert[symmetric, OF fin a'nA] also note domf
631 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
633 lemma map_default_eq_id [simp]: "map_default d ((\<lambda>a. Some (f a)) |` {a. f a \<noteq> d}) = f"
634 by(auto simp add: map_default_def restrict_map_def intro: ext)
636 lemma finite_rec_cong1:
637 assumes f: "fun_left_comm f" and g: "fun_left_comm g"
639 and eq: "\<And>a. a \<in> A \<Longrightarrow> f a = g a"
640 shows "fold f z A = fold g z A"
642 interpret f: fun_left_comm f by(rule f)
643 interpret g: fun_left_comm g by(rule g)
645 assume BsubA: "B \<subseteq> A"
646 with fin have "finite B" by(blast intro: finite_subset)
647 hence "B \<subseteq> A \<Longrightarrow> fold f z B = fold g z B"
649 case empty thus ?case by simp
652 note finB = `finite B` note anB = `a \<notin> B` note sub = `insert a B \<subseteq> A`
653 note IH = `B \<subseteq> A \<Longrightarrow> fold f z B = fold g z B`
654 from sub anB have BpsubA: "B \<subset> A" and BsubA: "B \<subseteq> A" and aA: "a \<in> A" by auto
655 from IH[OF BsubA] eq[OF aA] finB anB
658 with BsubA have "fold f z B = fold g z B" by blast }
659 thus ?thesis by blast
662 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
664 lemma finfun_rec_upd [simp]:
665 "finfun_rec cnst upd (f(\<^sup>f a' := b')) = upd a' b' (finfun_rec cnst upd f)"
667 obtain b where b: "b = finfun_default f" by auto
668 let ?the = "\<lambda>f g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g"
669 obtain g where g: "g = The (?the f)" by blast
670 obtain y where f: "f = Abs_finfun y" and y: "y \<in> finfun" by (cases f)
671 from f y b have bfin: "finite {a. y a \<noteq> b}" by(simp add: finfun_default_def finite_finfun_default_aux)
673 let ?g = "(\<lambda>a. Some (y a)) |` {a. y a \<noteq> b}"
674 from bfin have fing: "finite (dom ?g)" by auto
675 have bran: "b \<notin> ran ?g" by(auto simp add: ran_def restrict_map_def)
676 have yg: "y = map_default b ?g" by simp
677 have gg: "g = ?g" unfolding g
678 proof(rule the_equality)
679 from f y bfin show "?the f ?g"
680 by(auto)(simp add: restrict_map_def ran_def split: split_if_asm)
684 hence fin': "finite (dom g')" and ran': "b \<notin> ran g'"
685 and eq: "Abs_finfun (map_default b ?g) = Abs_finfun (map_default b g')" using f yg by auto
686 from fin' fing have "map_default b ?g \<in> finfun" "map_default b g' \<in> finfun" by(blast intro: map_default_in_finfun)+
687 with eq have "map_default b ?g = map_default b g'" by simp
688 with fing bran fin' ran' show "g' = ?g" by(rule map_default_inject[OF disjI2[OF refl], THEN sym])
692 proof(cases "b' = b")
696 let ?g' = "(\<lambda>a. Some ((y(a' := b)) a)) |` {a. (y(a' := b)) a \<noteq> b}"
697 from bfin b'b have fing': "finite (dom ?g')"
698 by(auto simp add: Collect_conj_eq Collect_imp_eq intro: finite_subset)
699 have brang': "b \<notin> ran ?g'" by(auto simp add: ran_def restrict_map_def)
701 let ?b' = "\<lambda>a. case ?g' a of None \<Rightarrow> b | Some b \<Rightarrow> b"
702 let ?b = "map_default b ?g"
703 from upd_left_comm upd_left_comm fing'
704 have "fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g') = fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g')"
705 by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b b map_default_def)
706 also interpret gwf: fun_left_comm "\<lambda>a. upd a (?b a)" by(rule upd_left_comm)
707 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))"
708 proof(cases "y a' = b")
710 with b'b have g': "?g' = ?g" by(auto simp add: restrict_map_def intro: ext)
711 from True have a'ndomg: "a' \<notin> dom ?g" by auto
712 from f b'b b show ?thesis unfolding g'
713 by(subst map_default_update_const[OF fing a'ndomg map_le_refl, symmetric]) simp
716 hence domg: "dom ?g = insert a' (dom ?g')" by auto
717 from False b'b have a'ndomg': "a' \<notin> dom ?g'" by auto
718 have "fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g')) =
719 upd a' (?b a') (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'))"
720 using fing' a'ndomg' unfolding b'b by(rule gwf.fold_insert)
721 hence "upd a' b (fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g'))) =
722 upd a' b (upd a' (?b a') (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g')))" by simp
723 also from b'b have g'leg: "?g' \<subseteq>\<^sub>m ?g" by(auto simp add: restrict_map_def map_le_def)
724 note map_default_update_twice[OF fing' a'ndomg' this, of b "?b a'" b]
725 also note map_default_update_const[OF fing' a'ndomg' g'leg, of b]
726 finally show ?thesis unfolding b'b domg[unfolded b'b] by(rule sym)
728 also have "The (?the (f(\<^sup>f a' := b'))) = ?g'"
729 proof(rule the_equality)
730 from f y b b'b brang' fing' show "?the (f(\<^sup>f a' := b')) ?g'"
731 by(auto simp del: fun_upd_apply simp add: finfun_update_def)
734 assume "?the (f(\<^sup>f a' := b')) g'"
735 hence fin': "finite (dom g')" and ran': "b \<notin> ran g'"
736 and eq: "f(\<^sup>f a' := b') = Abs_finfun (map_default b g')"
737 by(auto simp del: fun_upd_apply)
738 from fin' fing' have "map_default b g' \<in> finfun" "map_default b ?g' \<in> finfun"
739 by(blast intro: map_default_in_finfun)+
740 with eq f b'b b have "map_default b ?g' = map_default b g'"
741 by(simp del: fun_upd_apply add: finfun_update_def)
742 with fing' brang' fin' ran' show "g' = ?g'"
743 by(rule map_default_inject[OF disjI2[OF refl], THEN sym])
745 ultimately show ?thesis unfolding finfun_rec_def Let_def b gg[unfolded g b] using bfin b'b b
746 by(simp only: finfun_default_update_const map_default_def)
750 let ?g' = "?g(a' \<mapsto> b')"
751 let ?b' = "map_default b ?g'"
752 let ?b = "map_default b ?g"
753 from fing have fing': "finite (dom ?g')" by auto
754 from bran b'b have bnrang': "b \<notin> ran ?g'" by(auto simp add: ran_def)
755 have ffmg': "map_default b ?g' = y(a' := b')" by(auto intro: ext simp add: map_default_def restrict_map_def)
756 with f y have f_Abs: "f(\<^sup>f a' := b') = Abs_finfun (map_default b ?g')" by(auto simp add: finfun_update_def)
757 have g': "The (?the (f(\<^sup>f a' := b'))) = ?g'"
759 from fing' bnrang' f_Abs show "?the (f(\<^sup>f a' := b')) ?g'" by(auto simp add: finfun_update_def restrict_map_def)
761 fix g' assume "?the (f(\<^sup>f a' := b')) g'"
762 hence f': "f(\<^sup>f a' := b') = Abs_finfun (map_default b g')"
763 and fin': "finite (dom g')" and brang': "b \<notin> ran g'" by auto
764 from fing' fin' have "map_default b ?g' \<in> finfun" "map_default b g' \<in> finfun"
765 by(auto intro: map_default_in_finfun)
766 with f' f_Abs have "map_default b g' = map_default b ?g'" by simp
767 with fin' brang' fing' bnrang' show "g' = ?g'"
768 by(rule map_default_inject[OF disjI2[OF refl]])
770 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}))"
773 proof(cases "y a' = b")
775 hence a'ndomg: "a' \<notin> dom ?g" by auto
776 from f y b'b True have yff: "y = map_default b (?g' |` dom ?g)"
777 by(auto simp add: restrict_map_def map_default_def intro!: ext)
778 hence f': "f = Abs_finfun (map_default b (?g' |` dom ?g))" using f by simp
779 interpret g'wf: fun_left_comm "\<lambda>a. upd a (?b' a)" by(rule upd_left_comm)
780 from upd_left_comm upd_left_comm fing
781 have "fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g) = fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g)"
782 by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b True map_default_def)
783 thus ?thesis unfolding finfun_rec_def Let_def finfun_default_update_const b[symmetric]
784 unfolding g' g[symmetric] gg g'wf.fold_insert[OF fing a'ndomg, of "cnst b", folded dom]
785 by -(rule arg_cong2[where f="upd a'"], simp_all add: map_default_def)
788 hence "insert a' (dom ?g) = dom ?g" by auto
790 let ?g'' = "?g(a' := None)"
791 let ?b'' = "map_default b ?g''"
792 from False have domg: "dom ?g = insert a' (dom ?g'')" by auto
793 from False have a'ndomg'': "a' \<notin> dom ?g''" by auto
794 have fing'': "finite (dom ?g'')" by(rule finite_subset[OF _ fing]) auto
795 have bnrang'': "b \<notin> ran ?g''" by(auto simp add: ran_def restrict_map_def)
796 interpret gwf: fun_left_comm "\<lambda>a. upd a (?b a)" by(rule upd_left_comm)
797 interpret g'wf: fun_left_comm "\<lambda>a. upd a (?b' a)" by(rule upd_left_comm)
798 have "upd a' b' (fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g''))) =
799 upd a' b' (upd a' (?b a') (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')))"
800 unfolding gwf.fold_insert[OF fing'' a'ndomg''] f ..
801 also have g''leg: "?g |` dom ?g'' \<subseteq>\<^sub>m ?g" by(auto simp add: map_le_def)
802 have "dom (?g |` dom ?g'') = dom ?g''" by auto
803 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",
804 unfolded this, OF fing'' a'ndomg'' g''leg]
805 also have b': "b' = ?b' a'" by(auto simp add: map_default_def)
806 from upd_left_comm upd_left_comm fing''
807 have "fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'') = fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g'')"
808 by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b map_default_def)
809 with b' have "upd a' b' (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')) =
810 upd a' (?b' a') (fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g''))" by simp
811 also note g'wf.fold_insert[OF fing'' a'ndomg'', symmetric]
812 finally have "upd a' b' (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g)) =
813 fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g)"
815 ultimately have "fold (\<lambda>a. upd a (?b' a)) (cnst b) (insert a' (dom ?g)) =
816 upd a' b' (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g))" by simp
817 thus ?thesis unfolding finfun_rec_def Let_def finfun_default_update_const b[symmetric] g[symmetric] g' dom[symmetric]
818 using b'b gg by(simp add: map_default_insert)
823 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
827 locale finfun_rec_wf = finfun_rec_wf_aux +
828 assumes const_update_all:
829 "finite (UNIV :: 'a set) \<Longrightarrow> fold (\<lambda>a. upd a b') (cnst b) (UNIV :: 'a set) = cnst b'"
832 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
834 lemma finfun_rec_const [simp]:
835 "finfun_rec cnst upd (\<lambda>\<^isup>f c) = cnst c"
836 proof(cases "finite (UNIV :: 'a set)")
838 hence "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = c" by(simp add: finfun_default_const)
839 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"
841 show "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c empty) \<and> finite (dom empty) \<and> c \<notin> ran empty"
842 by(auto simp add: finfun_const_def)
844 fix g :: "'a \<rightharpoonup> 'b"
845 assume "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g"
846 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+
847 from g map_default_in_finfun[OF fin, of c] have "map_default c g = (\<lambda>a. c)"
848 by(simp add: finfun_const_def)
849 moreover have "map_default c empty = (\<lambda>a. c)" by simp
850 ultimately show "g = empty" by-(rule map_default_inject[OF disjI2[OF refl] fin ran], auto)
852 ultimately show ?thesis by(simp add: finfun_rec_def)
855 hence default: "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = arbitrary" by(simp add: finfun_default_const)
856 let ?the = "\<lambda>g :: 'a \<rightharpoonup> 'b. (\<lambda>\<^isup>f c) = Abs_finfun (map_default arbitrary g) \<and> finite (dom g) \<and> arbitrary \<notin> ran g"
858 proof(cases "c = arbitrary")
860 have the: "The ?the = empty"
862 from True show "?the empty" by(auto simp add: finfun_const_def)
866 hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default arbitrary g')"
867 and fin: "finite (dom g')" and g: "arbitrary \<notin> ran g'" by simp_all
868 from fin have "map_default arbitrary g' \<in> finfun" by(rule map_default_in_finfun)
869 with fg have "map_default arbitrary g' = (\<lambda>a. c)"
870 by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1])
871 with True show "g' = empty"
872 by -(rule map_default_inject(2)[OF _ fin g], auto)
874 show ?thesis unfolding finfun_rec_def using `finite UNIV` True
875 unfolding Let_def the default by(simp)
878 have the: "The ?the = (\<lambda>a :: 'a. Some c)"
880 from False True show "?the (\<lambda>a :: 'a. Some c)"
881 by(auto simp add: map_default_def_raw finfun_const_def dom_def ran_def)
883 fix g' :: "'a \<rightharpoonup> 'b"
885 hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default arbitrary g')"
886 and fin: "finite (dom g')" and g: "arbitrary \<notin> ran g'" by simp_all
887 from fin have "map_default arbitrary g' \<in> finfun" by(rule map_default_in_finfun)
888 with fg have "map_default arbitrary g' = (\<lambda>a. c)"
889 by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1])
890 with True False show "g' = (\<lambda>a::'a. Some c)"
891 by -(rule map_default_inject(2)[OF _ fin g], auto simp add: dom_def ran_def map_default_def_raw)
893 show ?thesis unfolding finfun_rec_def using True False
894 unfolding Let_def the default by(simp add: dom_def map_default_def const_update_all)
898 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
902 subsection {* Weak induction rule and case analysis for FinFuns *}
904 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
906 lemma finfun_weak_induct [consumes 0, case_names const update]:
907 assumes const: "\<And>b. P (\<lambda>\<^isup>f b)"
908 and update: "\<And>f a b. P f \<Longrightarrow> P (f(\<^sup>f a := b))"
910 proof(induct x rule: Abs_finfun_induct)
912 then obtain b where "finite {a. y a \<noteq> b}" unfolding finfun_def by blast
913 thus ?case using `y \<in> finfun`
914 proof(induct x\<equiv>"{a. y a \<noteq> b}" arbitrary: y rule: finite_induct)
916 hence "\<And>a. y a = b" by blast
917 hence "y = (\<lambda>a. b)" by(auto intro: ext)
918 hence "Abs_finfun y = finfun_const b" unfolding finfun_const_def by simp
919 thus ?case by(simp add: const)
922 note IH = `\<And>y. \<lbrakk> y \<in> finfun; A = {a. y a \<noteq> b} \<rbrakk> \<Longrightarrow> P (Abs_finfun y)`
923 note y = `y \<in> finfun`
924 with `insert a A = {a. y a \<noteq> b}` `a \<notin> A`
925 have "y(a := b) \<in> finfun" "A = {a'. (y(a := b)) a' \<noteq> b}" by auto
926 from IH[OF this] have "P (finfun_update (Abs_finfun (y(a := b))) a (y a))" by(rule update)
927 thus ?case using y unfolding finfun_update_def by simp
931 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
933 lemma finfun_exhaust_disj: "(\<exists>b. x = finfun_const b) \<or> (\<exists>f a b. x = finfun_update f a b)"
934 by(induct x rule: finfun_weak_induct) blast+
936 lemma finfun_exhaust:
937 obtains b where "x = (\<lambda>\<^isup>f b)"
938 | f a b where "x = f(\<^sup>f a := b)"
939 by(atomize_elim)(rule finfun_exhaust_disj)
941 lemma finfun_rec_unique:
942 fixes f :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'c"
943 assumes c: "\<And>c. f (\<lambda>\<^isup>f c) = cnst c"
944 and u: "\<And>g a b. f (g(\<^sup>f a := b)) = upd g a b (f g)"
945 and c': "\<And>c. f' (\<lambda>\<^isup>f c) = cnst c"
946 and u': "\<And>g a b. f' (g(\<^sup>f a := b)) = upd g a b (f' g)"
949 fix g :: "'a \<Rightarrow>\<^isub>f 'b"
951 by(induct g rule: finfun_weak_induct)(auto simp add: c u c' u')
955 subsection {* Function application *}
957 definition finfun_apply :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b" ("_\<^sub>f" [1000] 1000)
958 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)"
960 interpretation finfun_apply_aux: finfun_rec_wf_aux "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c"
961 by(unfold_locales) auto
963 interpretation finfun_apply: finfun_rec_wf "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c"
964 proof(unfold_locales)
966 assume fin: "finite (UNIV :: 'b set)"
968 interpret fun_left_comm "\<lambda>a'. If (a = a') b'" by(rule finfun_apply_aux.upd_left_comm)
969 from fin have "finite A" by(auto intro: finite_subset)
970 hence "fold (\<lambda>a'. If (a = a') b') b A = (if a \<in> A then b' else b)"
972 from this[of UNIV] show "fold (\<lambda>a'. If (a = a') b') b UNIV = b'" by simp
975 lemma finfun_const_apply [simp, code]: "(\<lambda>\<^isup>f b)\<^sub>f a = b"
976 by(simp add: finfun_apply_def)
978 lemma finfun_upd_apply: "f(\<^sup>fa := b)\<^sub>f a' = (if a = a' then b else f\<^sub>f a')"
979 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')"
980 by(simp_all add: finfun_apply_def)
982 lemma finfun_upd_apply_same [simp]:
983 "f(\<^sup>fa := b)\<^sub>f a = b"
984 by(simp add: finfun_upd_apply)
986 lemma finfun_upd_apply_other [simp]:
987 "a \<noteq> a' \<Longrightarrow> f(\<^sup>fa := b)\<^sub>f a' = f\<^sub>f a'"
988 by(simp add: finfun_upd_apply)
990 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
992 lemma finfun_apply_Rep_finfun:
993 "finfun_apply = Rep_finfun"
994 proof(rule finfun_rec_unique)
995 fix c show "Rep_finfun (\<lambda>\<^isup>f c) = (\<lambda>a. c)" by(auto simp add: finfun_const_def)
997 fix g a b show "Rep_finfun g(\<^sup>f a := b) = (\<lambda>c. if c = a then b else Rep_finfun g c)"
998 by(auto simp add: finfun_update_def fun_upd_finfun Abs_finfun_inverse Rep_finfun intro: ext)
1001 lemma finfun_ext: "(\<And>a. f\<^sub>f a = g\<^sub>f a) \<Longrightarrow> f = g"
1002 by(auto simp add: finfun_apply_Rep_finfun Rep_finfun_inject[symmetric] simp del: Rep_finfun_inject intro: ext)
1004 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1006 lemma expand_finfun_eq: "(f = g) = (f\<^sub>f = g\<^sub>f)"
1007 by(auto intro: finfun_ext)
1009 lemma finfun_const_inject [simp]: "(\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b') \<equiv> b = b'"
1010 by(simp add: expand_finfun_eq expand_fun_eq)
1012 lemma finfun_const_eq_update:
1013 "((\<lambda>\<^isup>f b) = f(\<^sup>f a := b')) = (b = b' \<and> (\<forall>a'. a \<noteq> a' \<longrightarrow> f\<^sub>f a' = b))"
1014 by(auto simp add: expand_finfun_eq expand_fun_eq finfun_upd_apply)
1016 subsection {* Function composition *}
1018 definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>\<^isub>f 'a \<Rightarrow> 'c \<Rightarrow>\<^isub>f 'b" (infixr "\<circ>\<^isub>f" 55)
1019 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"
1021 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))"
1022 by(unfold_locales)(auto simp add: finfun_upd_apply intro: finfun_ext)
1024 interpretation finfun_comp: finfun_rec_wf "(\<lambda>b. (\<lambda>\<^isup>f g b))" "(\<lambda>a b c. c(\<^sup>f a := g b))"
1027 assume fin: "finite (UNIV :: 'c set)"
1029 from fin have "finite A" by(auto intro: finite_subset)
1030 hence "fold (\<lambda>(a :: 'c) c. c(\<^sup>f a := g b')) (\<lambda>\<^isup>f g b) A =
1031 Abs_finfun (\<lambda>a. if a \<in> A then g b' else g b)"
1032 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) }
1033 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')"
1034 by(simp add: finfun_const_def)
1037 lemma finfun_comp_const [simp, code]:
1038 "g \<circ>\<^isub>f (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f g c)"
1039 by(simp add: finfun_comp_def)
1041 lemma finfun_comp_update [simp]: "g \<circ>\<^isub>f (f(\<^sup>f a := b)) = (g \<circ>\<^isub>f f)(\<^sup>f a := g b)"
1042 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)"
1043 by(simp_all add: finfun_comp_def)
1045 lemma finfun_comp_apply [simp]:
1046 "(g \<circ>\<^isub>f f)\<^sub>f = g \<circ> f\<^sub>f"
1047 by(induct f rule: finfun_weak_induct)(auto simp add: finfun_upd_apply intro: ext)
1049 lemma finfun_comp_comp_collapse [simp]: "f \<circ>\<^isub>f g \<circ>\<^isub>f h = (f o g) \<circ>\<^isub>f h"
1050 by(induct h rule: finfun_weak_induct) simp_all
1052 lemma finfun_comp_const1 [simp]: "(\<lambda>x. c) \<circ>\<^isub>f f = (\<lambda>\<^isup>f c)"
1053 by(induct f rule: finfun_weak_induct)(auto intro: finfun_ext simp add: finfun_upd_apply)
1055 lemma finfun_comp_id1 [simp]: "(\<lambda>x. x) \<circ>\<^isub>f f = f" "id \<circ>\<^isub>f f = f"
1056 by(induct f rule: finfun_weak_induct) auto
1058 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1060 lemma finfun_comp_conv_comp: "g \<circ>\<^isub>f f = Abs_finfun (g \<circ> finfun_apply f)"
1062 have "(\<lambda>f. g \<circ>\<^isub>f f) = (\<lambda>f. Abs_finfun (g \<circ> finfun_apply f))"
1063 proof(rule finfun_rec_unique)
1064 { fix c show "Abs_finfun (g \<circ> (\<lambda>\<^isup>f c)\<^sub>f) = (\<lambda>\<^isup>f g c)"
1065 by(simp add: finfun_comp_def o_def)(simp add: finfun_const_def) }
1066 { 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)"
1068 obtain y where y: "y \<in> finfun" and g': "g' = Abs_finfun y" by(cases g')
1069 moreover hence "(g \<circ> g'\<^sub>f) \<in> finfun" by(simp add: finfun_apply_Rep_finfun finfun_left_compose)
1070 moreover have "g \<circ> y(a := b) = (g \<circ> y)(a := g b)" by(auto intro: ext)
1071 ultimately show ?thesis by(simp add: finfun_comp_def finfun_update_def finfun_apply_Rep_finfun)
1074 thus ?thesis by(auto simp add: expand_fun_eq)
1077 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1081 definition finfun_comp2 :: "'b \<Rightarrow>\<^isub>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c" (infixr "\<^sub>f\<circ>" 55)
1082 where [code del]: "finfun_comp2 g f = Abs_finfun (Rep_finfun g \<circ> f)"
1084 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1086 lemma finfun_comp2_const [code, simp]: "finfun_comp2 (\<lambda>\<^isup>f c) f = (\<lambda>\<^isup>f c)"
1087 by(simp add: finfun_comp2_def finfun_const_def comp_def)
1089 lemma finfun_comp2_update:
1090 assumes inj: "inj f"
1091 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)"
1092 proof(cases "b \<in> range f")
1094 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)
1095 with inj True show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def finfun_right_compose)
1098 hence "(Rep_finfun g)(b := c) \<circ> f = Rep_finfun g \<circ> f" by(auto simp add: expand_fun_eq)
1099 with False show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def)
1102 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1104 subsection {* A type class for computing the cardinality of a type's universe *}
1107 fixes card_UNIV :: "'a itself \<Rightarrow> nat"
1108 assumes card_UNIV: "card_UNIV x = card (UNIV :: 'a set)"
1111 lemma card_UNIV_neq_0_finite_UNIV:
1112 "card_UNIV x \<noteq> 0 \<longleftrightarrow> finite (UNIV :: 'a set)"
1113 by(simp add: card_UNIV card_eq_0_iff)
1115 lemma card_UNIV_ge_0_finite_UNIV:
1116 "card_UNIV x > 0 \<longleftrightarrow> finite (UNIV :: 'a set)"
1117 by(auto simp add: card_UNIV intro: card_ge_0_finite finite_UNIV_card_ge_0)
1119 lemma card_UNIV_eq_0_infinite_UNIV:
1120 "card_UNIV x = 0 \<longleftrightarrow> infinite (UNIV :: 'a set)"
1121 by(simp add: card_UNIV card_eq_0_iff)
1123 definition is_list_UNIV :: "'a list \<Rightarrow> bool"
1124 where "is_list_UNIV xs = (let c = card_UNIV (TYPE('a)) in if c = 0 then False else size (remdups xs) = c)"
1126 lemma is_list_UNIV_iff:
1127 fixes xs :: "'a list"
1128 shows "is_list_UNIV xs \<longleftrightarrow> set xs = UNIV"
1130 assume "is_list_UNIV xs"
1131 hence c: "card_UNIV (TYPE('a)) > 0" and xs: "size (remdups xs) = card_UNIV (TYPE('a))"
1132 unfolding is_list_UNIV_def by(simp_all add: Let_def split: split_if_asm)
1133 from c have fin: "finite (UNIV :: 'a set)" by(auto simp add: card_UNIV_ge_0_finite_UNIV)
1134 have "card (set (remdups xs)) = size (remdups xs)" by(subst distinct_card) auto
1135 also note set_remdups
1136 finally show "set xs = UNIV" using fin unfolding xs card_UNIV by-(rule card_eq_UNIV_imp_eq_UNIV)
1138 assume xs: "set xs = UNIV"
1139 from finite_set[of xs] have fin: "finite (UNIV :: 'a set)" unfolding xs .
1140 hence "card_UNIV (TYPE ('a)) \<noteq> 0" unfolding card_UNIV_neq_0_finite_UNIV .
1141 moreover have "size (remdups xs) = card (set (remdups xs))"
1142 by(subst distinct_card) auto
1143 ultimately show "is_list_UNIV xs" using xs by(simp add: is_list_UNIV_def Let_def card_UNIV)
1146 lemma card_UNIV_eq_0_is_list_UNIV_False:
1147 assumes cU0: "card_UNIV x = 0"
1148 shows "is_list_UNIV = (\<lambda>xs. False)"
1151 from cU0 have "infinite (UNIV :: 'a set)"
1152 by(auto simp only: card_UNIV_eq_0_infinite_UNIV)
1153 moreover have "finite (set xs)" by(rule finite_set)
1154 ultimately have "(UNIV :: 'a set) \<noteq> set xs" by(auto simp del: finite_set)
1155 thus "is_list_UNIV xs = False" unfolding is_list_UNIV_iff by simp
1160 subsection {* Instantiations for @{text "card_UNIV"} *}
1162 subsubsection {* @{typ "nat"} *}
1164 instantiation nat :: card_UNIV begin
1166 definition card_UNIV_nat_def:
1167 "card_UNIV_class.card_UNIV = (\<lambda>a :: nat itself. 0)"
1170 fix x :: "nat itself"
1171 show "card_UNIV x = card (UNIV :: nat set)"
1172 unfolding card_UNIV_nat_def by simp
1177 subsubsection {* @{typ "int"} *}
1179 instantiation int :: card_UNIV begin
1181 definition card_UNIV_int_def:
1182 "card_UNIV_class.card_UNIV = (\<lambda>a :: int itself. 0)"
1185 fix x :: "int itself"
1186 show "card_UNIV x = card (UNIV :: int set)"
1187 unfolding card_UNIV_int_def by simp
1192 subsubsection {* @{typ "'a list"} *}
1194 instantiation list :: (type) card_UNIV begin
1196 definition card_UNIV_list_def:
1197 "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a list itself. 0)"
1200 fix x :: "'a list itself"
1201 show "card_UNIV x = card (UNIV :: 'a list set)"
1202 unfolding card_UNIV_list_def by(simp add: infinite_UNIV_listI)
1207 subsubsection {* @{typ "unit"} *}
1209 lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
1210 unfolding UNIV_unit by simp
1212 instantiation unit :: card_UNIV begin
1214 definition card_UNIV_unit_def:
1215 "card_UNIV_class.card_UNIV = (\<lambda>a :: unit itself. 1)"
1218 fix x :: "unit itself"
1219 show "card_UNIV x = card (UNIV :: unit set)"
1220 by(simp add: card_UNIV_unit_def card_UNIV_unit)
1225 subsubsection {* @{typ "bool"} *}
1227 lemma card_UNIV_bool: "card (UNIV :: bool set) = 2"
1228 unfolding UNIV_bool by simp
1230 instantiation bool :: card_UNIV begin
1232 definition card_UNIV_bool_def:
1233 "card_UNIV_class.card_UNIV = (\<lambda>a :: bool itself. 2)"
1236 fix x :: "bool itself"
1237 show "card_UNIV x = card (UNIV :: bool set)"
1238 by(simp add: card_UNIV_bool_def card_UNIV_bool)
1243 subsubsection {* @{typ "char"} *}
1245 lemma card_UNIV_char: "card (UNIV :: char set) = 256"
1248 have "card (set (enum :: char list)) = length (enum :: char list)"
1249 by -(rule distinct_card)
1250 also have "set enum = (UNIV :: char set)" by auto
1252 finally show ?thesis by simp
1255 instantiation char :: card_UNIV begin
1257 definition card_UNIV_char_def:
1258 "card_UNIV_class.card_UNIV = (\<lambda>a :: char itself. 256)"
1261 fix x :: "char itself"
1262 show "card_UNIV x = card (UNIV :: char set)"
1263 by(simp add: card_UNIV_char_def card_UNIV_char)
1268 subsubsection {* @{typ "'a \<times> 'b"} *}
1270 instantiation * :: (card_UNIV, card_UNIV) card_UNIV begin
1272 definition card_UNIV_product_def:
1273 "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<times> 'b) itself. card_UNIV (TYPE('a)) * card_UNIV (TYPE('b)))"
1276 fix x :: "('a \<times> 'b) itself"
1277 show "card_UNIV x = card (UNIV :: ('a \<times> 'b) set)"
1278 by(simp add: card_UNIV_product_def card_UNIV UNIV_Times_UNIV[symmetric] card_cartesian_product del: UNIV_Times_UNIV)
1283 subsubsection {* @{typ "'a + 'b"} *}
1285 instantiation "+" :: (card_UNIV, card_UNIV) card_UNIV begin
1287 definition card_UNIV_sum_def:
1288 "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a + 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
1289 in if ca \<noteq> 0 \<and> cb \<noteq> 0 then ca + cb else 0)"
1292 fix x :: "('a + 'b) itself"
1293 show "card_UNIV x = card (UNIV :: ('a + 'b) set)"
1294 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)
1299 subsubsection {* @{typ "'a \<Rightarrow> 'b"} *}
1301 instantiation "fun" :: (card_UNIV, card_UNIV) card_UNIV begin
1303 definition card_UNIV_fun_def:
1304 "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<Rightarrow> 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
1305 in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)"
1308 fix x :: "('a \<Rightarrow> 'b) itself"
1310 { assume "0 < card (UNIV :: 'a set)"
1311 and "0 < card (UNIV :: 'b set)"
1312 hence fina: "finite (UNIV :: 'a set)" and finb: "finite (UNIV :: 'b set)"
1313 by(simp_all only: card_ge_0_finite)
1314 from finite_distinct_list[OF finb] obtain bs
1315 where bs: "set bs = (UNIV :: 'b set)" and distb: "distinct bs" by blast
1316 from finite_distinct_list[OF fina] obtain as
1317 where as: "set as = (UNIV :: 'a set)" and dista: "distinct as" by blast
1318 have cb: "card (UNIV :: 'b set) = length bs"
1319 unfolding bs[symmetric] distinct_card[OF distb] ..
1320 have ca: "card (UNIV :: 'a set) = length as"
1321 unfolding as[symmetric] distinct_card[OF dista] ..
1322 let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (n_lists (length as) bs)"
1323 have "UNIV = set ?xs"
1324 proof(rule UNIV_eq_I)
1325 fix f :: "'a \<Rightarrow> 'b"
1326 from as have "f = the \<circ> map_of (zip as (map f as))"
1327 by(auto simp add: map_of_zip_map intro: ext)
1328 thus "f \<in> set ?xs" using bs by(auto simp add: set_n_lists)
1330 moreover have "distinct ?xs" unfolding distinct_map
1331 proof(intro conjI distinct_n_lists distb inj_onI)
1332 fix xs ys :: "'b list"
1333 assume xs: "xs \<in> set (n_lists (length as) bs)"
1334 and ys: "ys \<in> set (n_lists (length as) bs)"
1335 and eq: "the \<circ> map_of (zip as xs) = the \<circ> map_of (zip as ys)"
1336 from xs ys have [simp]: "length xs = length as" "length ys = length as"
1337 by(simp_all add: length_n_lists_elem)
1338 have "map_of (zip as xs) = map_of (zip as ys)"
1341 from as bs have "\<exists>y. map_of (zip as xs) x = Some y" "\<exists>y. map_of (zip as ys) x = Some y"
1342 by(simp_all add: map_of_zip_is_Some[symmetric])
1343 with eq show "map_of (zip as xs) x = map_of (zip as ys) x"
1344 by(auto dest: fun_cong[where x=x])
1346 with dista show "xs = ys" by(simp add: map_of_zip_inject)
1348 hence "card (set ?xs) = length ?xs" by(simp only: distinct_card)
1349 moreover have "length ?xs = length bs ^ length as" by(simp add: length_n_lists)
1350 ultimately have "card (UNIV :: ('a \<Rightarrow> 'b) set) = card (UNIV :: 'b set) ^ card (UNIV :: 'a set)"
1351 using cb ca by simp }
1353 assume cb: "card (UNIV :: 'b set) = Suc 0"
1354 then obtain b where b: "UNIV = {b :: 'b}" by(auto simp add: card_Suc_eq)
1355 have eq: "UNIV = {\<lambda>x :: 'a. b ::'b}"
1356 proof(rule UNIV_eq_I)
1357 fix x :: "'a \<Rightarrow> 'b"
1359 have "x y \<in> UNIV" ..
1360 hence "x y = b" unfolding b by simp }
1361 thus "x \<in> {\<lambda>x. b}" by(auto intro: ext)
1363 have "card (UNIV :: ('a \<Rightarrow> 'b) set) = Suc 0" unfolding eq by simp }
1364 ultimately show "card_UNIV x = card (UNIV :: ('a \<Rightarrow> 'b) set)"
1365 unfolding card_UNIV_fun_def card_UNIV Let_def
1366 by(auto simp del: One_nat_def)(auto simp add: card_eq_0_iff dest: finite_fun_UNIVD2 finite_fun_UNIVD1)
1371 subsubsection {* @{typ "'a option"} *}
1373 instantiation option :: (card_UNIV) card_UNIV
1376 definition card_UNIV_option_def:
1377 "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a option itself. let c = card_UNIV (TYPE('a))
1378 in if c \<noteq> 0 then Suc c else 0)"
1381 fix x :: "'a option itself"
1382 show "card_UNIV x = card (UNIV :: 'a option set)"
1383 unfolding UNIV_option_conv
1384 by(auto simp add: card_UNIV_option_def card_UNIV card_eq_0_iff Let_def intro: inj_Some dest: finite_imageD)
1385 (subst card_insert_disjoint, auto simp add: card_eq_0_iff card_image inj_Some intro: finite_imageI card_ge_0_finite)
1391 subsection {* Universal quantification *}
1393 definition finfun_All_except :: "'a list \<Rightarrow> 'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
1394 where [code del]: "finfun_All_except A P \<equiv> \<forall>a. a \<in> set A \<or> P\<^sub>f a"
1396 lemma finfun_All_except_const: "finfun_All_except A (\<lambda>\<^isup>f b) \<longleftrightarrow> b \<or> set A = UNIV"
1397 by(auto simp add: finfun_All_except_def)
1399 lemma finfun_All_except_const_finfun_UNIV_code [code]:
1400 "finfun_All_except A (\<lambda>\<^isup>f b) = (b \<or> is_list_UNIV A)"
1401 by(simp add: finfun_All_except_const is_list_UNIV_iff)
1403 lemma finfun_All_except_update:
1404 "finfun_All_except A f(\<^sup>f a := b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
1405 by(fastsimp simp add: finfun_All_except_def finfun_upd_apply)
1407 lemma finfun_All_except_update_code [code]:
1408 fixes a :: "'a :: card_UNIV"
1409 shows "finfun_All_except A (finfun_update_code f a b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
1410 by(simp add: finfun_All_except_update)
1412 definition finfun_All :: "'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
1413 where "finfun_All = finfun_All_except []"
1415 lemma finfun_All_const [simp]: "finfun_All (\<lambda>\<^isup>f b) = b"
1416 by(simp add: finfun_All_def finfun_All_except_def)
1418 lemma finfun_All_update: "finfun_All f(\<^sup>f a := b) = (b \<and> finfun_All_except [a] f)"
1419 by(simp add: finfun_All_def finfun_All_except_update)
1421 lemma finfun_All_All: "finfun_All P = All P\<^sub>f"
1422 by(simp add: finfun_All_def finfun_All_except_def)
1425 definition finfun_Ex :: "'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
1426 where "finfun_Ex P = Not (finfun_All (Not \<circ>\<^isub>f P))"
1428 lemma finfun_Ex_Ex: "finfun_Ex P = Ex P\<^sub>f"
1429 unfolding finfun_Ex_def finfun_All_All by simp
1431 lemma finfun_Ex_const [simp]: "finfun_Ex (\<lambda>\<^isup>f b) = b"
1432 by(simp add: finfun_Ex_def)
1435 subsection {* A diagonal operator for FinFuns *}
1437 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)
1438 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"
1440 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))"
1441 by(unfold_locales)(simp_all add: expand_finfun_eq expand_fun_eq finfun_upd_apply)
1443 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))"
1446 assume fin: "finite (UNIV :: 'c set)"
1448 interpret fun_left_comm "\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))" by(rule finfun_Diag_aux.upd_left_comm)
1449 from fin have "finite A" by(auto intro: finite_subset)
1450 hence "fold (\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))) (Pair b \<circ>\<^isub>f g) A =
1451 Abs_finfun (\<lambda>a. (if a \<in> A then b' else b, g\<^sub>f a))"
1452 by(induct)(simp_all add: finfun_const_def finfun_comp_conv_comp o_def,
1453 auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite expand_fun_eq fin) }
1454 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"
1455 by(simp add: finfun_const_def finfun_comp_conv_comp o_def)
1458 lemma finfun_Diag_const1: "(\<lambda>\<^isup>f b, g)\<^sup>f = Pair b \<circ>\<^isub>f g"
1459 by(simp add: finfun_Diag_def)
1462 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"}.
1465 lemma finfun_Diag_const_code [code]:
1466 "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))"
1467 "(\<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))"
1468 by(simp_all add: finfun_Diag_const1)
1470 lemma finfun_Diag_update1: "(f(\<^sup>f a := b), g)\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (b, g\<^sub>f a))"
1471 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))"
1472 by(simp_all add: finfun_Diag_def)
1474 lemma finfun_Diag_const2: "(f, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>b. (b, c)) \<circ>\<^isub>f f"
1475 by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
1477 lemma finfun_Diag_update2: "(f, g(\<^sup>f a := c))\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (f\<^sub>f a, c))"
1478 by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
1480 lemma finfun_Diag_const_const [simp]: "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))"
1481 by(simp add: finfun_Diag_const1)
1483 lemma finfun_Diag_const_update:
1484 "(\<lambda>\<^isup>f b, g(\<^sup>f a := c))\<^sup>f = (\<lambda>\<^isup>f b, g)\<^sup>f(\<^sup>f a := (b, c))"
1485 by(simp add: finfun_Diag_const1)
1487 lemma finfun_Diag_update_const:
1488 "(f(\<^sup>f a := b), \<lambda>\<^isup>f c)\<^sup>f = (f, \<lambda>\<^isup>f c)\<^sup>f(\<^sup>f a := (b, c))"
1489 by(simp add: finfun_Diag_def)
1491 lemma finfun_Diag_update_update:
1492 "(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)))"
1493 by(auto simp add: finfun_Diag_update1 finfun_Diag_update2)
1495 lemma finfun_Diag_apply [simp]: "(f, g)\<^sup>f\<^sub>f = (\<lambda>x. (f\<^sub>f x, g\<^sub>f x))"
1496 by(induct f rule: finfun_weak_induct)(auto simp add: finfun_Diag_const1 finfun_Diag_update1 finfun_upd_apply intro: ext)
1498 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1500 lemma finfun_Diag_conv_Abs_finfun:
1501 "(f, g)\<^sup>f = Abs_finfun ((\<lambda>x. (Rep_finfun f x, Rep_finfun g x)))"
1503 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))))"
1504 proof(rule finfun_rec_unique)
1505 { fix c show "Abs_finfun (\<lambda>x. (Rep_finfun (\<lambda>\<^isup>f c) x, Rep_finfun g x)) = Pair c \<circ>\<^isub>f g"
1506 by(simp add: finfun_comp_conv_comp finfun_apply_Rep_finfun o_def finfun_const_def) }
1508 show "Abs_finfun (\<lambda>x. (Rep_finfun g'(\<^sup>f a := b) x, Rep_finfun g x)) =
1509 (Abs_finfun (\<lambda>x. (Rep_finfun g' x, Rep_finfun g x)))(\<^sup>f a := (b, g\<^sub>f a))"
1510 by(auto simp add: finfun_update_def expand_fun_eq finfun_apply_Rep_finfun simp del: fun_upd_apply) simp }
1511 qed(simp_all add: finfun_Diag_const1 finfun_Diag_update1)
1512 thus ?thesis by(auto simp add: expand_fun_eq)
1515 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1517 lemma finfun_Diag_eq: "(f, g)\<^sup>f = (f', g')\<^sup>f \<longleftrightarrow> f = f' \<and> g = g'"
1518 by(auto simp add: expand_finfun_eq expand_fun_eq)
1520 definition finfun_fst :: "'a \<Rightarrow>\<^isub>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b"
1521 where [code]: "finfun_fst f = fst \<circ>\<^isub>f f"
1523 lemma finfun_fst_const: "finfun_fst (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f fst bc)"
1524 by(simp add: finfun_fst_def)
1526 lemma finfun_fst_update: "finfun_fst (f(\<^sup>f a := bc)) = (finfun_fst f)(\<^sup>f a := fst bc)"
1527 and finfun_fst_update_code: "finfun_fst (finfun_update_code f a bc) = (finfun_fst f)(\<^sup>f a := fst bc)"
1528 by(simp_all add: finfun_fst_def)
1530 lemma finfun_fst_comp_conv: "finfun_fst (f \<circ>\<^isub>f g) = (fst \<circ> f) \<circ>\<^isub>f g"
1531 by(simp add: finfun_fst_def)
1533 lemma finfun_fst_conv [simp]: "finfun_fst (f, g)\<^sup>f = f"
1534 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)
1536 lemma finfun_fst_conv_Abs_finfun: "finfun_fst = (\<lambda>f. Abs_finfun (fst o Rep_finfun f))"
1537 by(simp add: finfun_fst_def_raw finfun_comp_conv_comp finfun_apply_Rep_finfun)
1540 definition finfun_snd :: "'a \<Rightarrow>\<^isub>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c"
1541 where [code]: "finfun_snd f = snd \<circ>\<^isub>f f"
1543 lemma finfun_snd_const: "finfun_snd (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f snd bc)"
1544 by(simp add: finfun_snd_def)
1546 lemma finfun_snd_update: "finfun_snd (f(\<^sup>f a := bc)) = (finfun_snd f)(\<^sup>f a := snd bc)"
1547 and finfun_snd_update_code [code]: "finfun_snd (finfun_update_code f a bc) = (finfun_snd f)(\<^sup>f a := snd bc)"
1548 by(simp_all add: finfun_snd_def)
1550 lemma finfun_snd_comp_conv: "finfun_snd (f \<circ>\<^isub>f g) = (snd \<circ> f) \<circ>\<^isub>f g"
1551 by(simp add: finfun_snd_def)
1553 lemma finfun_snd_conv [simp]: "finfun_snd (f, g)\<^sup>f = g"
1554 apply(induct f rule: finfun_weak_induct)
1555 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)
1558 lemma finfun_snd_conv_Abs_finfun: "finfun_snd = (\<lambda>f. Abs_finfun (snd o Rep_finfun f))"
1559 by(simp add: finfun_snd_def_raw finfun_comp_conv_comp finfun_apply_Rep_finfun)
1561 lemma finfun_Diag_collapse [simp]: "(finfun_fst f, finfun_snd f)\<^sup>f = f"
1562 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)
1564 subsection {* Currying for FinFuns *}
1566 definition finfun_curry :: "('a \<times> 'b) \<Rightarrow>\<^isub>f 'c \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b \<Rightarrow>\<^isub>f 'c"
1567 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)))"
1569 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))"
1570 apply(unfold_locales)
1571 apply(auto simp add: split_def finfun_update_twist finfun_upd_apply split_paired_all finfun_update_const_same)
1574 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1576 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))"
1577 proof(unfold_locales)
1579 assume fin: "finite (UNIV :: ('c \<times> 'a) set)"
1580 hence fin1: "finite (UNIV :: 'c set)" and fin2: "finite (UNIV :: 'a set)"
1581 unfolding UNIV_Times_UNIV[symmetric]
1582 by(fastsimp dest: finite_cartesian_productD1 finite_cartesian_productD2)+
1583 note [simp] = Abs_finfun_inverse_finite[OF fin] Abs_finfun_inverse_finite[OF fin1] Abs_finfun_inverse_finite[OF fin2]
1584 { fix A :: "('c \<times> 'a) set"
1585 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'"
1586 by(rule finfun_curry_aux.upd_left_comm)
1587 from fin have "finite A" by(auto intro: finite_subset)
1588 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))"
1589 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) }
1591 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'"
1592 by(simp add: finfun_const_def)
1595 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1597 lemma finfun_curry_const [simp, code]: "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
1598 by(simp add: finfun_curry_def)
1600 lemma finfun_curry_update [simp]:
1601 "finfun_curry (f(\<^sup>f (a, b) := c)) = (finfun_curry f)(\<^sup>f a := ((finfun_curry f)\<^sub>f a)(\<^sup>f b := c))"
1602 and finfun_curry_update_code [code]:
1603 "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))"
1604 by(simp_all add: finfun_curry_def)
1606 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1608 lemma finfun_Abs_finfun_curry: assumes fin: "f \<in> finfun"
1609 shows "(\<lambda>a. Abs_finfun (curry f a)) \<in> finfun"
1611 from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast
1612 have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force)
1613 hence "{a. curry f a \<noteq> (\<lambda>x. c)} = fst ` {ab. f ab \<noteq> c}"
1614 by(auto simp add: curry_def expand_fun_eq)
1615 with fin c have "finite {a. Abs_finfun (curry f a) \<noteq> (\<lambda>\<^isup>f c)}"
1616 by(simp add: finfun_const_def finfun_curry)
1617 thus ?thesis unfolding finfun_def by auto
1620 lemma finfun_curry_conv_curry:
1621 fixes f :: "('a \<times> 'b) \<Rightarrow>\<^isub>f 'c"
1622 shows "finfun_curry f = Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun f) a))"
1624 have "finfun_curry = (\<lambda>f :: ('a \<times> 'b) \<Rightarrow>\<^isub>f 'c. Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun f) a)))"
1625 proof(rule finfun_rec_unique)
1626 { fix c show "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)" by simp }
1627 { 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))"
1629 { fix c show "Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun (\<lambda>\<^isup>f c)) a)) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
1630 by(simp add: finfun_curry_def finfun_const_def curry_def) }
1632 show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (Rep_finfun g(\<^sup>f a := b)) aa)) =
1633 (Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun g) a)))(\<^sup>f
1634 fst a := ((Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun g) a)))\<^sub>f (fst a))(\<^sup>f snd a := b))"
1635 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) }
1637 thus ?thesis by(auto simp add: expand_fun_eq)
1640 subsection {* Executable equality for FinFuns *}
1642 lemma eq_finfun_All_ext: "(f = g) \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>\<^isub>f (f, g)\<^sup>f)"
1643 by(simp add: expand_finfun_eq expand_fun_eq finfun_All_All o_def)
1645 instantiation finfun :: ("{card_UNIV,eq}",eq) eq begin
1646 definition eq_finfun_def: "eq_class.eq f g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>\<^isub>f (f, g)\<^sup>f)"
1647 instance by(intro_classes)(simp add: eq_finfun_All_ext eq_finfun_def)
1650 subsection {* Operator that explicitly removes all redundant updates in the generated representations *}
1652 definition finfun_clearjunk :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b"
1653 where [simp, code del]: "finfun_clearjunk = id"
1655 lemma finfun_clearjunk_const [code]: "finfun_clearjunk (\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b)"
1658 lemma finfun_clearjunk_update [code]: "finfun_clearjunk (finfun_update_code f a b) = f(\<^sup>f a := b)"