1 (* Author: Andreas Lochbihler, Uni Karlsruhe *)
3 header {* Almost everywhere constant functions *}
10 This theory defines functions which are constant except for finitely
11 many points (FinFun) and introduces a type finfin along with a
12 number of operators for them. The code generator is set up such that
13 such functions can be represented as data in the generated code and
14 all operators are executable.
16 For details, see Formalising FinFuns - Generating Code for Functions as Data by A. Lochbihler in TPHOLs 2009.
20 definition "code_abort" :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a"
21 where [simp, code del]: "code_abort f = f ()"
23 code_abort "code_abort"
25 hide_const (open) "code_abort"
27 subsection {* The @{text "map_default"} operation *}
29 definition map_default :: "'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
30 where "map_default b f a \<equiv> case f a of None \<Rightarrow> b | Some b' \<Rightarrow> b'"
32 lemma map_default_delete [simp]:
33 "map_default b (f(a := None)) = (map_default b f)(a := b)"
34 by(simp add: map_default_def fun_eq_iff)
36 lemma map_default_insert:
37 "map_default b (f(a \<mapsto> b')) = (map_default b f)(a := b')"
38 by(simp add: map_default_def fun_eq_iff)
40 lemma map_default_empty [simp]: "map_default b empty = (\<lambda>a. b)"
41 by(simp add: fun_eq_iff map_default_def)
43 lemma map_default_inject:
44 fixes g g' :: "'a \<rightharpoonup> 'b"
45 assumes infin_eq: "\<not> finite (UNIV :: 'a set) \<or> b = b'"
46 and fin: "finite (dom g)" and b: "b \<notin> ran g"
47 and fin': "finite (dom g')" and b': "b' \<notin> ran g'"
48 and eq': "map_default b g = map_default b' g'"
49 shows "b = b'" "g = g'"
51 from infin_eq show bb': "b = b'"
53 assume infin: "\<not> finite (UNIV :: 'a set)"
54 from fin fin' have "finite (dom g \<union> dom g')" by auto
55 with infin have "UNIV - (dom g \<union> dom g') \<noteq> {}" by(auto dest: finite_subset)
56 then obtain a where a: "a \<notin> dom g \<union> dom g'" by auto
57 hence "map_default b g a = b" "map_default b' g' a = b'" by(auto simp add: map_default_def)
58 with eq' show "b = b'" by simp
67 hence "map_default b g x = b" by(simp add: map_default_def)
68 with bb' eq' have "map_default b' g' x = b'" by simp
69 with b' have "g' x = None" by(simp add: map_default_def ran_def split: option.split_asm)
70 with None show ?thesis by simp
73 with b have cb: "c \<noteq> b" by(auto simp add: ran_def)
74 moreover from Some have "map_default b g x = c" by(simp add: map_default_def)
75 with eq' have "map_default b' g' x = c" by simp
76 ultimately have "g' x = Some c" using b' bb' by(auto simp add: map_default_def split: option.splits)
77 with Some show ?thesis by simp
82 subsection {* The finfun type *}
84 definition "finfun = {f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}"
86 typedef (open) ('a,'b) finfun ("(_ \<Rightarrow>\<^isub>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set"
87 morphisms finfun_apply Abs_finfun
89 have "\<exists>f. finite {x. f x \<noteq> undefined}"
91 show "finite {x. (\<lambda>y. undefined) x \<noteq> undefined}" by auto
93 then show ?thesis unfolding finfun_def by auto
96 setup_lifting type_definition_finfun
98 lemma fun_upd_finfun: "y(a := b) \<in> finfun \<longleftrightarrow> y \<in> finfun"
101 have "finite {a'. (y(a := b)) a' \<noteq> b'} = finite {a'. y a' \<noteq> b'}"
102 proof(cases "b = b'")
104 hence "{a'. (y(a := b)) a' \<noteq> b'} = {a'. y a' \<noteq> b'} - {a}" by auto
108 hence "{a'. (y(a := b)) a' \<noteq> b'} = insert a {a'. y a' \<noteq> b'}" by auto
111 thus ?thesis unfolding finfun_def by blast
114 lemma const_finfun: "(\<lambda>x. a) \<in> finfun"
115 by(auto simp add: finfun_def)
117 lemma finfun_left_compose:
118 assumes "y \<in> finfun"
119 shows "g \<circ> y \<in> finfun"
121 from assms obtain b where "finite {a. y a \<noteq> b}"
122 unfolding finfun_def by blast
123 hence "finite {c. g (y c) \<noteq> g b}"
124 proof(induct "{a. y a \<noteq> b}" arbitrary: y)
126 hence "y = (\<lambda>a. b)" by(auto intro: ext)
130 note IH = `\<And>y. F = {a. y a \<noteq> b} \<Longrightarrow> finite {c. g (y c) \<noteq> g b}`
131 from `insert x F = {a. y a \<noteq> b}` `x \<notin> F`
132 have F: "F = {a. (y(x := b)) a \<noteq> b}" by(auto)
134 proof(cases "g (y x) = g b")
136 hence "{c. g ((y(x := b)) c) \<noteq> g b} = {c. g (y c) \<noteq> g b}" by auto
137 with IH[OF F] show ?thesis by simp
140 hence "{c. g (y c) \<noteq> g b} = insert x {c. g ((y(x := b)) c) \<noteq> g b}" by auto
141 with IH[OF F] show ?thesis by(simp)
144 thus ?thesis unfolding finfun_def by auto
147 lemma assumes "y \<in> finfun"
148 shows fst_finfun: "fst \<circ> y \<in> finfun"
149 and snd_finfun: "snd \<circ> y \<in> finfun"
151 from assms obtain b c where bc: "finite {a. y a \<noteq> (b, c)}"
152 unfolding finfun_def by auto
153 have "{a. fst (y a) \<noteq> b} \<subseteq> {a. y a \<noteq> (b, c)}"
154 and "{a. snd (y a) \<noteq> c} \<subseteq> {a. y a \<noteq> (b, c)}" by auto
155 hence "finite {a. fst (y a) \<noteq> b}"
156 and "finite {a. snd (y a) \<noteq> c}" using bc by(auto intro: finite_subset)
157 thus "fst \<circ> y \<in> finfun" "snd \<circ> y \<in> finfun"
158 unfolding finfun_def by auto
161 lemma map_of_finfun: "map_of xs \<in> finfun"
163 by(induct xs)(auto simp add: Collect_neg_eq Collect_conj_eq Collect_imp_eq intro: finite_subset)
165 lemma Diag_finfun: "(\<lambda>x. (f x, g x)) \<in> finfun \<longleftrightarrow> f \<in> finfun \<and> g \<in> finfun"
166 by(auto intro: finite_subset simp add: Collect_neg_eq Collect_imp_eq Collect_conj_eq finfun_def)
168 lemma finfun_right_compose:
169 assumes g: "g \<in> finfun" and inj: "inj f"
170 shows "g o f \<in> finfun"
172 from g obtain b where b: "finite {a. g a \<noteq> b}" unfolding finfun_def by blast
173 moreover have "f ` {a. g (f a) \<noteq> b} \<subseteq> {a. g a \<noteq> b}" by auto
174 moreover from inj have "inj_on f {a. g (f a) \<noteq> b}" by(rule subset_inj_on) blast
175 ultimately have "finite {a. g (f a) \<noteq> b}"
176 by(blast intro: finite_imageD[where f=f] finite_subset)
177 thus ?thesis unfolding finfun_def by auto
181 assumes fin: "f \<in> finfun"
182 shows "curry f \<in> finfun" "curry f a \<in> finfun"
184 from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast
185 moreover have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force)
186 hence "{a. curry f a \<noteq> (\<lambda>b. c)} = fst ` {ab. f ab \<noteq> c}"
187 by(auto simp add: curry_def fun_eq_iff)
188 ultimately have "finite {a. curry f a \<noteq> (\<lambda>b. c)}" by simp
189 thus "curry f \<in> finfun" unfolding finfun_def by blast
191 have "snd ` {ab. f ab \<noteq> c} = {b. \<exists>a. f (a, b) \<noteq> c}" by(force)
192 hence "{b. f (a, b) \<noteq> c} \<subseteq> snd ` {ab. f ab \<noteq> c}" by auto
193 hence "finite {b. f (a, b) \<noteq> c}" by(rule finite_subset)(rule finite_imageI[OF c])
194 thus "curry f a \<in> finfun" unfolding finfun_def by auto
198 fst_finfun snd_finfun Abs_finfun_inverse finfun_apply_inverse Abs_finfun_inject finfun_apply_inject Diag_finfun finfun_curry
199 lemmas finfun_iff = const_finfun fun_upd_finfun finfun_apply map_of_finfun
200 lemmas finfun_intro = finfun_left_compose fst_finfun snd_finfun
202 lemma Abs_finfun_inject_finite:
203 fixes x y :: "'a \<Rightarrow> 'b"
204 assumes fin: "finite (UNIV :: 'a set)"
205 shows "Abs_finfun x = Abs_finfun y \<longleftrightarrow> x = y"
207 assume "Abs_finfun x = Abs_finfun y"
208 moreover have "x \<in> finfun" "y \<in> finfun" unfolding finfun_def
209 by(auto intro: finite_subset[OF _ fin])
210 ultimately show "x = y" by(simp add: Abs_finfun_inject)
213 lemma Abs_finfun_inject_finite_class:
214 fixes x y :: "('a :: finite) \<Rightarrow> 'b"
215 shows "Abs_finfun x = Abs_finfun y \<longleftrightarrow> x = y"
217 by(simp add: Abs_finfun_inject_finite)
219 lemma Abs_finfun_inj_finite:
220 assumes fin: "finite (UNIV :: 'a set)"
221 shows "inj (Abs_finfun :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b)"
223 fix x y :: "'a \<Rightarrow> 'b"
224 assume "Abs_finfun x = Abs_finfun y"
225 moreover have "x \<in> finfun" "y \<in> finfun" unfolding finfun_def
226 by(auto intro: finite_subset[OF _ fin])
227 ultimately show "x = y" by(simp add: Abs_finfun_inject)
230 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
232 lemma Abs_finfun_inverse_finite:
233 fixes x :: "'a \<Rightarrow> 'b"
234 assumes fin: "finite (UNIV :: 'a set)"
235 shows "finfun_apply (Abs_finfun x) = x"
237 from fin have "x \<in> finfun"
238 by(auto simp add: finfun_def intro: finite_subset)
242 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
244 lemma Abs_finfun_inverse_finite_class:
245 fixes x :: "('a :: finite) \<Rightarrow> 'b"
246 shows "finfun_apply (Abs_finfun x) = x"
247 using finite_UNIV by(simp add: Abs_finfun_inverse_finite)
249 lemma finfun_eq_finite_UNIV: "finite (UNIV :: 'a set) \<Longrightarrow> (finfun :: ('a \<Rightarrow> 'b) set) = UNIV"
250 unfolding finfun_def by(auto intro: finite_subset)
252 lemma finfun_finite_UNIV_class: "finfun = (UNIV :: ('a :: finite \<Rightarrow> 'b) set)"
253 by(simp add: finfun_eq_finite_UNIV)
255 lemma map_default_in_finfun:
256 assumes fin: "finite (dom f)"
257 shows "map_default b f \<in> finfun"
259 proof(intro CollectI exI)
260 from fin show "finite {a. map_default b f a \<noteq> b}"
261 by(auto simp add: map_default_def dom_def Collect_conj_eq split: option.splits)
264 lemma finfun_cases_map_default:
265 obtains b g where "f = Abs_finfun (map_default b g)" "finite (dom g)" "b \<notin> ran g"
267 obtain y where f: "f = Abs_finfun y" and y: "y \<in> finfun" by(cases f)
268 from y obtain b where b: "finite {a. y a \<noteq> b}" unfolding finfun_def by auto
269 let ?g = "(\<lambda>a. if y a = b then None else Some (y a))"
270 have "map_default b ?g = y" by(simp add: fun_eq_iff map_default_def)
271 with f have "f = Abs_finfun (map_default b ?g)" by simp
272 moreover from b have "finite (dom ?g)" by(auto simp add: dom_def)
273 moreover have "b \<notin> ran ?g" by(auto simp add: ran_def)
274 ultimately show ?thesis by(rule that)
278 subsection {* Kernel functions for type @{typ "'a \<Rightarrow>\<^isub>f 'b"} *}
280 lift_definition finfun_const :: "'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("\<lambda>\<^isup>f/ _" [0] 1)
281 is "\<lambda> b x. b" by (rule const_finfun)
283 lift_definition finfun_update :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("_'(\<^sup>f/ _ := _')" [1000,0,0] 1000) is "fun_upd" by (simp add: fun_upd_finfun)
285 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
287 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)"
288 by transfer (simp add: fun_upd_twist)
290 lemma finfun_update_twice [simp]:
291 "finfun_update (finfun_update f a b) a b' = finfun_update f a b'"
294 lemma finfun_update_const_same: "(\<lambda>\<^isup>f b)(\<^sup>f a := b) = (\<lambda>\<^isup>f b)"
295 by transfer (simp add: fun_eq_iff)
297 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
299 subsection {* Code generator setup *}
301 definition finfun_update_code :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("_'(\<^sup>fc/ _ := _')" [1000,0,0] 1000)
302 where [simp, code del]: "finfun_update_code = finfun_update"
304 code_datatype finfun_const finfun_update_code
306 lemma finfun_update_const_code [code]:
307 "(\<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')"
308 by(simp add: finfun_update_const_same)
310 lemma finfun_update_update_code [code]:
311 "(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)"
312 by(simp add: finfun_update_twist)
315 subsection {* Setup for quickcheck *}
317 quickcheck_generator finfun constructors: finfun_update_code, "finfun_const :: 'b => 'a \<Rightarrow>\<^isub>f 'b"
319 subsection {* @{text "finfun_update"} as instance of @{text "comp_fun_commute"} *}
321 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
323 interpretation finfun_update: comp_fun_commute "\<lambda>a f. f(\<^sup>f a :: 'a := b')"
326 show "(\<lambda>f. f(\<^sup>f a := b')) \<circ> (\<lambda>f. f(\<^sup>f a' := b')) = (\<lambda>f. f(\<^sup>f a' := b')) \<circ> (\<lambda>f. f(\<^sup>f a := b'))"
329 have "(finfun_apply b)(a := b', a' := b') = (finfun_apply b)(a' := b', a := b')"
330 by(cases "a = a'")(auto simp add: fun_upd_twist)
331 then have "b(\<^sup>f a := b')(\<^sup>f a' := b') = b(\<^sup>f a' := b')(\<^sup>f a := b')"
332 by(auto simp add: finfun_update_def fun_upd_twist)
333 then show "((\<lambda>f. f(\<^sup>f a := b')) \<circ> (\<lambda>f. f(\<^sup>f a' := b'))) b = ((\<lambda>f. f(\<^sup>f a' := b')) \<circ> (\<lambda>f. f(\<^sup>f a := b'))) b"
334 by (simp add: fun_eq_iff)
338 lemma fold_finfun_update_finite_univ:
339 assumes fin: "finite (UNIV :: 'a set)"
340 shows "Finite_Set.fold (\<lambda>a f. f(\<^sup>f a := b')) (\<lambda>\<^isup>f b) (UNIV :: 'a set) = (\<lambda>\<^isup>f b')"
343 from fin have "finite A" by(auto intro: finite_subset)
344 hence "Finite_Set.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)"
347 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)"
349 with insert show ?case
350 by(simp add: finfun_const_def fun_upd_def)(simp add: finfun_update_def Abs_finfun_inverse_finite[OF fin] fun_upd_def)
351 qed(simp add: finfun_const_def) }
352 thus ?thesis by(simp add: finfun_const_def)
356 subsection {* Default value for FinFuns *}
358 definition finfun_default_aux :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"
359 where [code del]: "finfun_default_aux f = (if finite (UNIV :: 'a set) then undefined else THE b. finite {a. f a \<noteq> b})"
361 lemma finfun_default_aux_infinite:
362 fixes f :: "'a \<Rightarrow> 'b"
363 assumes infin: "\<not> finite (UNIV :: 'a set)"
364 and fin: "finite {a. f a \<noteq> b}"
365 shows "finfun_default_aux f = b"
367 let ?B = "{a. f a \<noteq> b}"
368 from fin have "(THE b. finite {a. f a \<noteq> b}) = b"
369 proof(rule the_equality)
371 assume "finite {a. f a \<noteq> b'}" (is "finite ?B'")
372 with infin fin have "UNIV - (?B' \<union> ?B) \<noteq> {}" by(auto dest: finite_subset)
373 then obtain a where a: "a \<notin> ?B' \<union> ?B" by auto
374 thus "b' = b" by auto
376 thus ?thesis using infin by(simp add: finfun_default_aux_def)
380 lemma finite_finfun_default_aux:
381 fixes f :: "'a \<Rightarrow> 'b"
382 assumes fin: "f \<in> finfun"
383 shows "finite {a. f a \<noteq> finfun_default_aux f}"
384 proof(cases "finite (UNIV :: 'a set)")
385 case True thus ?thesis using fin
386 by(auto simp add: finfun_def finfun_default_aux_def intro: finite_subset)
389 from fin obtain b where b: "finite {a. f a \<noteq> b}" (is "finite ?B")
390 unfolding finfun_def by blast
391 with False show ?thesis by(simp add: finfun_default_aux_infinite)
394 lemma finfun_default_aux_update_const:
395 fixes f :: "'a \<Rightarrow> 'b"
396 assumes fin: "f \<in> finfun"
397 shows "finfun_default_aux (f(a := b)) = finfun_default_aux f"
398 proof(cases "finite (UNIV :: 'a set)")
400 from fin obtain b' where b': "finite {a. f a \<noteq> b'}" unfolding finfun_def by blast
401 hence "finite {a'. (f(a := b)) a' \<noteq> b'}"
402 proof(cases "b = b' \<and> f a \<noteq> b'")
404 hence "{a. f a \<noteq> b'} = insert a {a'. (f(a := b)) a' \<noteq> b'}" by auto
405 thus ?thesis using b' by simp
409 { assume "b \<noteq> b'"
410 hence "{a'. (f(a := b)) a' \<noteq> b'} = insert a {a. f a \<noteq> b'}" by auto
411 hence ?thesis using b' by simp }
413 { assume "b = b'" "f a = b'"
414 hence "{a'. (f(a := b)) a' \<noteq> b'} = {a. f a \<noteq> b'}" by auto
415 hence ?thesis using b' by simp }
416 ultimately show ?thesis by blast
418 with False b' show ?thesis by(auto simp del: fun_upd_apply simp add: finfun_default_aux_infinite)
420 case True thus ?thesis by(simp add: finfun_default_aux_def)
423 lift_definition finfun_default :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'b"
424 is "finfun_default_aux" ..
426 lemma finite_finfun_default: "finite {a. finfun_apply f a \<noteq> finfun_default f}"
427 apply transfer apply (erule finite_finfun_default_aux)
428 unfolding Rel_def fun_rel_def cr_finfun_def by simp
430 lemma finfun_default_const: "finfun_default ((\<lambda>\<^isup>f b) :: 'a \<Rightarrow>\<^isub>f 'b) = (if finite (UNIV :: 'a set) then undefined else b)"
432 apply(auto simp add: finfun_default_aux_infinite)
433 apply(simp add: finfun_default_aux_def)
436 lemma finfun_default_update_const:
437 "finfun_default (f(\<^sup>f a := b)) = finfun_default f"
438 by transfer (simp add: finfun_default_aux_update_const)
440 lemma finfun_default_const_code [code]:
441 "finfun_default ((\<lambda>\<^isup>f c) :: ('a :: card_UNIV) \<Rightarrow>\<^isub>f 'b) = (if card_UNIV (TYPE('a)) = 0 then c else undefined)"
442 by(simp add: finfun_default_const card_UNIV_eq_0_infinite_UNIV)
444 lemma finfun_default_update_code [code]:
445 "finfun_default (finfun_update_code f a b) = finfun_default f"
446 by(simp add: finfun_default_update_const)
448 subsection {* Recursion combinator and well-formedness conditions *}
450 definition finfun_rec :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<Rightarrow> 'c"
452 "finfun_rec cnst upd f \<equiv>
453 let b = finfun_default f;
454 g = THE g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g
455 in Finite_Set.fold (\<lambda>a. upd a (map_default b g a)) (cnst b) (dom g)"
457 locale finfun_rec_wf_aux =
458 fixes cnst :: "'b \<Rightarrow> 'c"
459 and upd :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c"
460 assumes upd_const_same: "upd a b (cnst b) = cnst b"
461 and upd_commute: "a \<noteq> a' \<Longrightarrow> upd a b (upd a' b' c) = upd a' b' (upd a b c)"
462 and upd_idemp: "b \<noteq> b' \<Longrightarrow> upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)"
466 lemma upd_left_comm: "comp_fun_commute (\<lambda>a. upd a (f a))"
467 by(unfold_locales)(auto intro: upd_commute simp add: fun_eq_iff)
469 lemma upd_upd_twice: "upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)"
470 by(cases "b \<noteq> b'")(auto simp add: fun_upd_def upd_const_same upd_idemp)
472 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
474 lemma map_default_update_const:
475 assumes fin: "finite (dom f)"
476 and anf: "a \<notin> dom f"
477 and fg: "f \<subseteq>\<^sub>m g"
478 shows "upd a d (Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f)) =
479 Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f)"
481 let ?upd = "\<lambda>a. upd a (map_default d g a)"
482 let ?fr = "\<lambda>A. Finite_Set.fold ?upd (cnst d) A"
483 interpret gwf: comp_fun_commute "?upd" by(rule upd_left_comm)
485 from fin anf fg show ?thesis
486 proof(induct "dom f" arbitrary: f)
488 from `{} = dom f` have "f = empty" by(auto simp add: dom_def intro: ext)
489 thus ?case by(simp add: finfun_const_def upd_const_same)
492 note IH = `\<And>f. \<lbrakk> A = dom f; a \<notin> dom f; f \<subseteq>\<^sub>m g \<rbrakk> \<Longrightarrow> upd a d (?fr (dom f)) = ?fr (dom f)`
493 note fin = `finite A` note anf = `a \<notin> dom f` note a'nA = `a' \<notin> A`
494 note domf = `insert a' A = dom f` note fg = `f \<subseteq>\<^sub>m g`
496 from domf obtain b where b: "f a' = Some b" by auto
497 let ?f' = "f(a' := None)"
498 have "upd a d (?fr (insert a' A)) = upd a d (upd a' (map_default d g a') (?fr A))"
499 by(subst gwf.fold_insert[OF fin a'nA]) rule
500 also from b fg have "g a' = f a'" by(auto simp add: map_le_def intro: domI dest: bspec)
501 hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def)
502 also from anf domf have "a \<noteq> a'" by auto note upd_commute[OF this]
503 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)
504 note A also note IH[OF A `a \<notin> dom ?f'` `?f' \<subseteq>\<^sub>m g`]
505 also have "upd a' (map_default d f a') (?fr (dom (f(a' := None)))) = ?fr (dom f)"
506 unfolding domf[symmetric] gwf.fold_insert[OF fin a'nA] ga' unfolding A ..
507 also have "insert a' (dom ?f') = dom f" using domf by auto
512 lemma map_default_update_twice:
513 assumes fin: "finite (dom f)"
514 and anf: "a \<notin> dom f"
515 and fg: "f \<subseteq>\<^sub>m g"
516 shows "upd a d'' (upd a d' (Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f))) =
517 upd a d'' (Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f))"
519 let ?upd = "\<lambda>a. upd a (map_default d g a)"
520 let ?fr = "\<lambda>A. Finite_Set.fold ?upd (cnst d) A"
521 interpret gwf: comp_fun_commute "?upd" by(rule upd_left_comm)
523 from fin anf fg show ?thesis
524 proof(induct "dom f" arbitrary: f)
526 from `{} = dom f` have "f = empty" by(auto simp add: dom_def intro: ext)
527 thus ?case by(auto simp add: finfun_const_def finfun_update_def upd_upd_twice)
530 note IH = `\<And>f. \<lbrakk>A = dom f; a \<notin> dom f; f \<subseteq>\<^sub>m g\<rbrakk> \<Longrightarrow> upd a d'' (upd a d' (?fr (dom f))) = upd a d'' (?fr (dom f))`
531 note fin = `finite A` note anf = `a \<notin> dom f` note a'nA = `a' \<notin> A`
532 note domf = `insert a' A = dom f` note fg = `f \<subseteq>\<^sub>m g`
534 from domf obtain b where b: "f a' = Some b" by auto
535 let ?f' = "f(a' := None)"
536 let ?b' = "case f a' of None \<Rightarrow> d | Some b \<Rightarrow> b"
537 from domf have "upd a d'' (upd a d' (?fr (dom f))) = upd a d'' (upd a d' (?fr (insert a' A)))" by simp
538 also note gwf.fold_insert[OF fin a'nA]
539 also from b fg have "g a' = f a'" by(auto simp add: map_le_def intro: domI dest: bspec)
540 hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def)
541 also from anf domf have ana': "a \<noteq> a'" by auto note upd_commute[OF this]
542 also note upd_commute[OF ana']
543 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)
544 note A also note IH[OF A `a \<notin> dom ?f'` `?f' \<subseteq>\<^sub>m g`]
545 also note upd_commute[OF ana'[symmetric]] also note ga'[symmetric] also note A[symmetric]
546 also note gwf.fold_insert[symmetric, OF fin a'nA] also note domf
551 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
553 lemma map_default_eq_id [simp]: "map_default d ((\<lambda>a. Some (f a)) |` {a. f a \<noteq> d}) = f"
554 by(auto simp add: map_default_def restrict_map_def intro: ext)
556 lemma finite_rec_cong1:
557 assumes f: "comp_fun_commute f" and g: "comp_fun_commute g"
559 and eq: "\<And>a. a \<in> A \<Longrightarrow> f a = g a"
560 shows "Finite_Set.fold f z A = Finite_Set.fold g z A"
562 interpret f: comp_fun_commute f by(rule f)
563 interpret g: comp_fun_commute g by(rule g)
565 assume BsubA: "B \<subseteq> A"
566 with fin have "finite B" by(blast intro: finite_subset)
567 hence "B \<subseteq> A \<Longrightarrow> Finite_Set.fold f z B = Finite_Set.fold g z B"
569 case empty thus ?case by simp
572 note finB = `finite B` note anB = `a \<notin> B` note sub = `insert a B \<subseteq> A`
573 note IH = `B \<subseteq> A \<Longrightarrow> Finite_Set.fold f z B = Finite_Set.fold g z B`
574 from sub anB have BpsubA: "B \<subset> A" and BsubA: "B \<subseteq> A" and aA: "a \<in> A" by auto
575 from IH[OF BsubA] eq[OF aA] finB anB
578 with BsubA have "Finite_Set.fold f z B = Finite_Set.fold g z B" by blast }
579 thus ?thesis by blast
582 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
584 lemma finfun_rec_upd [simp]:
585 "finfun_rec cnst upd (f(\<^sup>f a' := b')) = upd a' b' (finfun_rec cnst upd f)"
587 obtain b where b: "b = finfun_default f" by auto
588 let ?the = "\<lambda>f g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g"
589 obtain g where g: "g = The (?the f)" by blast
590 obtain y where f: "f = Abs_finfun y" and y: "y \<in> finfun" by (cases f)
591 from f y b have bfin: "finite {a. y a \<noteq> b}" by(simp add: finfun_default_def finite_finfun_default_aux)
593 let ?g = "(\<lambda>a. Some (y a)) |` {a. y a \<noteq> b}"
594 from bfin have fing: "finite (dom ?g)" by auto
595 have bran: "b \<notin> ran ?g" by(auto simp add: ran_def restrict_map_def)
596 have yg: "y = map_default b ?g" by simp
597 have gg: "g = ?g" unfolding g
598 proof(rule the_equality)
599 from f y bfin show "?the f ?g"
600 by(auto)(simp add: restrict_map_def ran_def split: split_if_asm)
604 hence fin': "finite (dom g')" and ran': "b \<notin> ran g'"
605 and eq: "Abs_finfun (map_default b ?g) = Abs_finfun (map_default b g')" using f yg by auto
606 from fin' fing have "map_default b ?g \<in> finfun" "map_default b g' \<in> finfun" by(blast intro: map_default_in_finfun)+
607 with eq have "map_default b ?g = map_default b g'" by simp
608 with fing bran fin' ran' show "g' = ?g" by(rule map_default_inject[OF disjI2[OF refl], THEN sym])
612 proof(cases "b' = b")
616 let ?g' = "(\<lambda>a. Some ((y(a' := b)) a)) |` {a. (y(a' := b)) a \<noteq> b}"
617 from bfin b'b have fing': "finite (dom ?g')"
618 by(auto simp add: Collect_conj_eq Collect_imp_eq intro: finite_subset)
619 have brang': "b \<notin> ran ?g'" by(auto simp add: ran_def restrict_map_def)
621 let ?b' = "\<lambda>a. case ?g' a of None \<Rightarrow> b | Some b \<Rightarrow> b"
622 let ?b = "map_default b ?g"
623 from upd_left_comm upd_left_comm fing'
624 have "Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g') = Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g')"
625 by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b b map_default_def)
626 also interpret gwf: comp_fun_commute "\<lambda>a. upd a (?b a)" by(rule upd_left_comm)
627 have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g') = upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g))"
628 proof(cases "y a' = b")
630 with b'b have g': "?g' = ?g" by(auto simp add: restrict_map_def intro: ext)
631 from True have a'ndomg: "a' \<notin> dom ?g" by auto
632 from f b'b b show ?thesis unfolding g'
633 by(subst map_default_update_const[OF fing a'ndomg map_le_refl, symmetric]) simp
636 hence domg: "dom ?g = insert a' (dom ?g')" by auto
637 from False b'b have a'ndomg': "a' \<notin> dom ?g'" by auto
638 have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g')) =
639 upd a' (?b a') (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'))"
640 using fing' a'ndomg' unfolding b'b by(rule gwf.fold_insert)
641 hence "upd a' b (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g'))) =
642 upd a' b (upd a' (?b a') (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g')))" by simp
643 also from b'b have g'leg: "?g' \<subseteq>\<^sub>m ?g" by(auto simp add: restrict_map_def map_le_def)
644 note map_default_update_twice[OF fing' a'ndomg' this, of b "?b a'" b]
645 also note map_default_update_const[OF fing' a'ndomg' g'leg, of b]
646 finally show ?thesis unfolding b'b domg[unfolded b'b] by(rule sym)
648 also have "The (?the (f(\<^sup>f a' := b'))) = ?g'"
649 proof(rule the_equality)
650 from f y b b'b brang' fing' show "?the (f(\<^sup>f a' := b')) ?g'"
651 by(auto simp del: fun_upd_apply simp add: finfun_update_def)
654 assume "?the (f(\<^sup>f a' := b')) g'"
655 hence fin': "finite (dom g')" and ran': "b \<notin> ran g'"
656 and eq: "f(\<^sup>f a' := b') = Abs_finfun (map_default b g')"
657 by(auto simp del: fun_upd_apply)
658 from fin' fing' have "map_default b g' \<in> finfun" "map_default b ?g' \<in> finfun"
659 by(blast intro: map_default_in_finfun)+
660 with eq f b'b b have "map_default b ?g' = map_default b g'"
661 by(simp del: fun_upd_apply add: finfun_update_def)
662 with fing' brang' fin' ran' show "g' = ?g'"
663 by(rule map_default_inject[OF disjI2[OF refl], THEN sym])
665 ultimately show ?thesis unfolding finfun_rec_def Let_def b gg[unfolded g b] using bfin b'b b
666 by(simp only: finfun_default_update_const map_default_def)
670 let ?g' = "?g(a' \<mapsto> b')"
671 let ?b' = "map_default b ?g'"
672 let ?b = "map_default b ?g"
673 from fing have fing': "finite (dom ?g')" by auto
674 from bran b'b have bnrang': "b \<notin> ran ?g'" by(auto simp add: ran_def)
675 have ffmg': "map_default b ?g' = y(a' := b')" by(auto intro: ext simp add: map_default_def restrict_map_def)
676 with f y have f_Abs: "f(\<^sup>f a' := b') = Abs_finfun (map_default b ?g')" by(auto simp add: finfun_update_def)
677 have g': "The (?the (f(\<^sup>f a' := b'))) = ?g'"
678 proof (rule the_equality)
679 from fing' bnrang' f_Abs show "?the (f(\<^sup>f a' := b')) ?g'" by(auto simp add: finfun_update_def restrict_map_def)
681 fix g' assume "?the (f(\<^sup>f a' := b')) g'"
682 hence f': "f(\<^sup>f a' := b') = Abs_finfun (map_default b g')"
683 and fin': "finite (dom g')" and brang': "b \<notin> ran g'" by auto
684 from fing' fin' have "map_default b ?g' \<in> finfun" "map_default b g' \<in> finfun"
685 by(auto intro: map_default_in_finfun)
686 with f' f_Abs have "map_default b g' = map_default b ?g'" by simp
687 with fin' brang' fing' bnrang' show "g' = ?g'"
688 by(rule map_default_inject[OF disjI2[OF refl]])
690 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}))"
693 proof(cases "y a' = b")
695 hence a'ndomg: "a' \<notin> dom ?g" by auto
696 from f y b'b True have yff: "y = map_default b (?g' |` dom ?g)"
697 by(auto simp add: restrict_map_def map_default_def intro!: ext)
698 hence f': "f = Abs_finfun (map_default b (?g' |` dom ?g))" using f by simp
699 interpret g'wf: comp_fun_commute "\<lambda>a. upd a (?b' a)" by(rule upd_left_comm)
700 from upd_left_comm upd_left_comm fing
701 have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g) = Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g)"
702 by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b True map_default_def)
703 thus ?thesis unfolding finfun_rec_def Let_def finfun_default_update_const b[symmetric]
704 unfolding g' g[symmetric] gg g'wf.fold_insert[OF fing a'ndomg, of "cnst b", folded dom]
705 by -(rule arg_cong2[where f="upd a'"], simp_all add: map_default_def)
708 hence "insert a' (dom ?g) = dom ?g" by auto
710 let ?g'' = "?g(a' := None)"
711 let ?b'' = "map_default b ?g''"
712 from False have domg: "dom ?g = insert a' (dom ?g'')" by auto
713 from False have a'ndomg'': "a' \<notin> dom ?g''" by auto
714 have fing'': "finite (dom ?g'')" by(rule finite_subset[OF _ fing]) auto
715 have bnrang'': "b \<notin> ran ?g''" by(auto simp add: ran_def restrict_map_def)
716 interpret gwf: comp_fun_commute "\<lambda>a. upd a (?b a)" by(rule upd_left_comm)
717 interpret g'wf: comp_fun_commute "\<lambda>a. upd a (?b' a)" by(rule upd_left_comm)
718 have "upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g''))) =
719 upd a' b' (upd a' (?b a') (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')))"
720 unfolding gwf.fold_insert[OF fing'' a'ndomg''] f ..
721 also have g''leg: "?g |` dom ?g'' \<subseteq>\<^sub>m ?g" by(auto simp add: map_le_def)
722 have "dom (?g |` dom ?g'') = dom ?g''" by auto
723 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",
724 unfolded this, OF fing'' a'ndomg'' g''leg]
725 also have b': "b' = ?b' a'" by(auto simp add: map_default_def)
726 from upd_left_comm upd_left_comm fing''
727 have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'') = Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g'')"
728 by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b map_default_def)
729 with b' have "upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')) =
730 upd a' (?b' a') (Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g''))" by simp
731 also note g'wf.fold_insert[OF fing'' a'ndomg'', symmetric]
732 finally have "upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g)) =
733 Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g)"
735 ultimately have "Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (insert a' (dom ?g)) =
736 upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g))" by simp
737 thus ?thesis unfolding finfun_rec_def Let_def finfun_default_update_const b[symmetric] g[symmetric] g' dom[symmetric]
738 using b'b gg by(simp add: map_default_insert)
743 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
747 locale finfun_rec_wf = finfun_rec_wf_aux +
748 assumes const_update_all:
749 "finite (UNIV :: 'a set) \<Longrightarrow> Finite_Set.fold (\<lambda>a. upd a b') (cnst b) (UNIV :: 'a set) = cnst b'"
752 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
754 lemma finfun_rec_const [simp]:
755 "finfun_rec cnst upd (\<lambda>\<^isup>f c) = cnst c"
756 proof(cases "finite (UNIV :: 'a set)")
758 hence "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = c" by(simp add: finfun_default_const)
759 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"
760 proof (rule the_equality)
761 show "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c empty) \<and> finite (dom empty) \<and> c \<notin> ran empty"
762 by(auto simp add: finfun_const_def)
764 fix g :: "'a \<rightharpoonup> 'b"
765 assume "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g"
766 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+
767 from g map_default_in_finfun[OF fin, of c] have "map_default c g = (\<lambda>a. c)"
768 by(simp add: finfun_const_def)
769 moreover have "map_default c empty = (\<lambda>a. c)" by simp
770 ultimately show "g = empty" by-(rule map_default_inject[OF disjI2[OF refl] fin ran], auto)
772 ultimately show ?thesis by(simp add: finfun_rec_def)
775 hence default: "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = undefined" by(simp add: finfun_default_const)
776 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"
778 proof(cases "c = undefined")
780 have the: "The ?the = empty"
781 proof (rule the_equality)
782 from True show "?the empty" by(auto simp add: finfun_const_def)
786 hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g')"
787 and fin: "finite (dom g')" and g: "undefined \<notin> ran g'" by simp_all
788 from fin have "map_default undefined g' \<in> finfun" by(rule map_default_in_finfun)
789 with fg have "map_default undefined g' = (\<lambda>a. c)"
790 by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1])
791 with True show "g' = empty"
792 by -(rule map_default_inject(2)[OF _ fin g], auto)
794 show ?thesis unfolding finfun_rec_def using `finite UNIV` True
795 unfolding Let_def the default by(simp)
798 have the: "The ?the = (\<lambda>a :: 'a. Some c)"
799 proof (rule the_equality)
800 from False True show "?the (\<lambda>a :: 'a. Some c)"
801 by(auto simp add: map_default_def [abs_def] finfun_const_def dom_def ran_def)
803 fix g' :: "'a \<rightharpoonup> 'b"
805 hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g')"
806 and fin: "finite (dom g')" and g: "undefined \<notin> ran g'" by simp_all
807 from fin have "map_default undefined g' \<in> finfun" by(rule map_default_in_finfun)
808 with fg have "map_default undefined g' = (\<lambda>a. c)"
809 by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1])
810 with True False show "g' = (\<lambda>a::'a. Some c)"
811 by - (rule map_default_inject(2)[OF _ fin g],
812 auto simp add: dom_def ran_def map_default_def [abs_def])
814 show ?thesis unfolding finfun_rec_def using True False
815 unfolding Let_def the default by(simp add: dom_def map_default_def const_update_all)
819 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
823 subsection {* Weak induction rule and case analysis for FinFuns *}
825 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
827 lemma finfun_weak_induct [consumes 0, case_names const update]:
828 assumes const: "\<And>b. P (\<lambda>\<^isup>f b)"
829 and update: "\<And>f a b. P f \<Longrightarrow> P (f(\<^sup>f a := b))"
831 proof(induct x rule: Abs_finfun_induct)
833 then obtain b where "finite {a. y a \<noteq> b}" unfolding finfun_def by blast
834 thus ?case using `y \<in> finfun`
835 proof(induct "{a. y a \<noteq> b}" arbitrary: y rule: finite_induct)
837 hence "\<And>a. y a = b" by blast
838 hence "y = (\<lambda>a. b)" by(auto intro: ext)
839 hence "Abs_finfun y = finfun_const b" unfolding finfun_const_def by simp
840 thus ?case by(simp add: const)
843 note IH = `\<And>y. \<lbrakk> A = {a. y a \<noteq> b}; y \<in> finfun \<rbrakk> \<Longrightarrow> P (Abs_finfun y)`
844 note y = `y \<in> finfun`
845 with `insert a A = {a. y a \<noteq> b}` `a \<notin> A`
846 have "A = {a'. (y(a := b)) a' \<noteq> b}" "y(a := b) \<in> finfun" by auto
847 from IH[OF this] have "P (finfun_update (Abs_finfun (y(a := b))) a (y a))" by(rule update)
848 thus ?case using y unfolding finfun_update_def by simp
852 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
854 lemma finfun_exhaust_disj: "(\<exists>b. x = finfun_const b) \<or> (\<exists>f a b. x = finfun_update f a b)"
855 by(induct x rule: finfun_weak_induct) blast+
857 lemma finfun_exhaust:
858 obtains b where "x = (\<lambda>\<^isup>f b)"
859 | f a b where "x = f(\<^sup>f a := b)"
860 by(atomize_elim)(rule finfun_exhaust_disj)
862 lemma finfun_rec_unique:
863 fixes f :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'c"
864 assumes c: "\<And>c. f (\<lambda>\<^isup>f c) = cnst c"
865 and u: "\<And>g a b. f (g(\<^sup>f a := b)) = upd g a b (f g)"
866 and c': "\<And>c. f' (\<lambda>\<^isup>f c) = cnst c"
867 and u': "\<And>g a b. f' (g(\<^sup>f a := b)) = upd g a b (f' g)"
870 fix g :: "'a \<Rightarrow>\<^isub>f 'b"
872 by(induct g rule: finfun_weak_induct)(auto simp add: c u c' u')
876 subsection {* Function application *}
878 notation finfun_apply ("_\<^sub>f" [1000] 1000)
880 interpretation finfun_apply_aux: finfun_rec_wf_aux "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c"
881 by(unfold_locales) auto
883 interpretation finfun_apply: finfun_rec_wf "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c"
884 proof(unfold_locales)
886 assume fin: "finite (UNIV :: 'b set)"
888 interpret comp_fun_commute "\<lambda>a'. If (a = a') b'" by(rule finfun_apply_aux.upd_left_comm)
889 from fin have "finite A" by(auto intro: finite_subset)
890 hence "Finite_Set.fold (\<lambda>a'. If (a = a') b') b A = (if a \<in> A then b' else b)"
892 from this[of UNIV] show "Finite_Set.fold (\<lambda>a'. If (a = a') b') b UNIV = b'" by simp
895 lemma finfun_apply_def: "finfun_apply = (\<lambda>f a. finfun_rec (\<lambda>b. b) (\<lambda>a' b c. if (a = a') then b else c) f)"
896 proof(rule finfun_rec_unique)
897 fix c show "finfun_apply (\<lambda>\<^isup>f c) = (\<lambda>a. c)" by(simp add: finfun_const.rep_eq)
899 fix g a b show "finfun_apply g(\<^sup>f a := b) = (\<lambda>c. if c = a then b else finfun_apply g c)"
900 by(auto simp add: finfun_update_def fun_upd_finfun Abs_finfun_inverse finfun_apply)
903 lemma finfun_upd_apply: "f(\<^sup>fa := b)\<^sub>f a' = (if a = a' then b else f\<^sub>f a')"
904 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')"
905 by(simp_all add: finfun_apply_def)
907 lemma finfun_const_apply [simp, code]: "(\<lambda>\<^isup>f b)\<^sub>f a = b"
908 by(simp add: finfun_apply_def)
910 lemma finfun_upd_apply_same [simp]:
911 "f(\<^sup>fa := b)\<^sub>f a = b"
912 by(simp add: finfun_upd_apply)
914 lemma finfun_upd_apply_other [simp]:
915 "a \<noteq> a' \<Longrightarrow> f(\<^sup>fa := b)\<^sub>f a' = f\<^sub>f a'"
916 by(simp add: finfun_upd_apply)
918 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
920 lemma finfun_ext: "(\<And>a. f\<^sub>f a = g\<^sub>f a) \<Longrightarrow> f = g"
921 by(auto simp add: finfun_apply_inject[symmetric] simp del: finfun_apply_inject)
923 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
925 lemma expand_finfun_eq: "(f = g) = (f\<^sub>f = g\<^sub>f)"
926 by(auto intro: finfun_ext)
928 lemma finfun_const_inject [simp]: "(\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b') \<equiv> b = b'"
929 by(simp add: expand_finfun_eq fun_eq_iff)
931 lemma finfun_const_eq_update:
932 "((\<lambda>\<^isup>f b) = f(\<^sup>f a := b')) = (b = b' \<and> (\<forall>a'. a \<noteq> a' \<longrightarrow> f\<^sub>f a' = b))"
933 by(auto simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
935 subsection {* Function composition *}
937 definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>\<^isub>f 'a \<Rightarrow> 'c \<Rightarrow>\<^isub>f 'b" (infixr "\<circ>\<^isub>f" 55)
938 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"
940 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))"
941 by(unfold_locales)(auto simp add: finfun_upd_apply intro: finfun_ext)
943 interpretation finfun_comp: finfun_rec_wf "(\<lambda>b. (\<lambda>\<^isup>f g b))" "(\<lambda>a b c. c(\<^sup>f a := g b))"
946 assume fin: "finite (UNIV :: 'c set)"
948 from fin have "finite A" by(auto intro: finite_subset)
949 hence "Finite_Set.fold (\<lambda>(a :: 'c) c. c(\<^sup>f a := g b')) (\<lambda>\<^isup>f g b) A =
950 Abs_finfun (\<lambda>a. if a \<in> A then g b' else g b)"
951 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 fun_eq_iff fin) }
952 from this[of UNIV] show "Finite_Set.fold (\<lambda>(a :: 'c) c. c(\<^sup>f a := g b')) (\<lambda>\<^isup>f g b) UNIV = (\<lambda>\<^isup>f g b')"
953 by(simp add: finfun_const_def)
956 lemma finfun_comp_const [simp, code]:
957 "g \<circ>\<^isub>f (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f g c)"
958 by(simp add: finfun_comp_def)
960 lemma finfun_comp_update [simp]: "g \<circ>\<^isub>f (f(\<^sup>f a := b)) = (g \<circ>\<^isub>f f)(\<^sup>f a := g b)"
961 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)"
962 by(simp_all add: finfun_comp_def)
964 lemma finfun_comp_apply [simp]:
965 "(g \<circ>\<^isub>f f)\<^sub>f = g \<circ> f\<^sub>f"
966 by(induct f rule: finfun_weak_induct)(auto simp add: finfun_upd_apply intro: ext)
968 lemma finfun_comp_comp_collapse [simp]: "f \<circ>\<^isub>f g \<circ>\<^isub>f h = (f o g) \<circ>\<^isub>f h"
969 by(induct h rule: finfun_weak_induct) simp_all
971 lemma finfun_comp_const1 [simp]: "(\<lambda>x. c) \<circ>\<^isub>f f = (\<lambda>\<^isup>f c)"
972 by(induct f rule: finfun_weak_induct)(auto intro: finfun_ext simp add: finfun_upd_apply)
974 lemma finfun_comp_id1 [simp]: "(\<lambda>x. x) \<circ>\<^isub>f f = f" "id \<circ>\<^isub>f f = f"
975 by(induct f rule: finfun_weak_induct) auto
977 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
979 lemma finfun_comp_conv_comp: "g \<circ>\<^isub>f f = Abs_finfun (g \<circ> finfun_apply f)"
981 have "(\<lambda>f. g \<circ>\<^isub>f f) = (\<lambda>f. Abs_finfun (g \<circ> finfun_apply f))"
982 proof(rule finfun_rec_unique)
983 { fix c show "Abs_finfun (g \<circ> (\<lambda>\<^isup>f c)\<^sub>f) = (\<lambda>\<^isup>f g c)"
984 by(simp add: finfun_comp_def o_def)(simp add: finfun_const_def) }
985 { 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)"
987 obtain y where y: "y \<in> finfun" and g': "g' = Abs_finfun y" by(cases g')
988 moreover hence "(g \<circ> g'\<^sub>f) \<in> finfun" by(simp add: finfun_left_compose)
989 moreover have "g \<circ> y(a := b) = (g \<circ> y)(a := g b)" by(auto intro: ext)
990 ultimately show ?thesis by(simp add: finfun_comp_def finfun_update_def)
993 thus ?thesis by(auto simp add: fun_eq_iff)
996 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
998 definition finfun_comp2 :: "'b \<Rightarrow>\<^isub>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c" (infixr "\<^sub>f\<circ>" 55)
999 where [code del]: "finfun_comp2 g f = Abs_finfun (finfun_apply g \<circ> f)"
1001 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1003 lemma finfun_comp2_const [code, simp]: "finfun_comp2 (\<lambda>\<^isup>f c) f = (\<lambda>\<^isup>f c)"
1004 by(simp add: finfun_comp2_def finfun_const_def comp_def)
1006 lemma finfun_comp2_update:
1007 assumes inj: "inj f"
1008 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)"
1009 proof(cases "b \<in> range f")
1011 from inj have "\<And>x. (finfun_apply g)(f x := c) \<circ> f = (finfun_apply g \<circ> f)(x := c)" by(auto intro!: ext dest: injD)
1012 with inj True show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def finfun_right_compose)
1015 hence "(finfun_apply g)(b := c) \<circ> f = finfun_apply g \<circ> f" by(auto simp add: fun_eq_iff)
1016 with False show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def)
1019 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1022 subsection {* Universal quantification *}
1024 definition finfun_All_except :: "'a list \<Rightarrow> 'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
1025 where [code del]: "finfun_All_except A P \<equiv> \<forall>a. a \<in> set A \<or> P\<^sub>f a"
1027 lemma finfun_All_except_const: "finfun_All_except A (\<lambda>\<^isup>f b) \<longleftrightarrow> b \<or> set A = UNIV"
1028 by(auto simp add: finfun_All_except_def)
1030 lemma finfun_All_except_const_finfun_UNIV_code [code]:
1031 "finfun_All_except A (\<lambda>\<^isup>f b) = (b \<or> is_list_UNIV A)"
1032 by(simp add: finfun_All_except_const is_list_UNIV_iff)
1034 lemma finfun_All_except_update:
1035 "finfun_All_except A f(\<^sup>f a := b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
1036 by(fastforce simp add: finfun_All_except_def finfun_upd_apply)
1038 lemma finfun_All_except_update_code [code]:
1039 fixes a :: "'a :: card_UNIV"
1040 shows "finfun_All_except A (finfun_update_code f a b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
1041 by(simp add: finfun_All_except_update)
1043 definition finfun_All :: "'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
1044 where "finfun_All = finfun_All_except []"
1046 lemma finfun_All_const [simp]: "finfun_All (\<lambda>\<^isup>f b) = b"
1047 by(simp add: finfun_All_def finfun_All_except_def)
1049 lemma finfun_All_update: "finfun_All f(\<^sup>f a := b) = (b \<and> finfun_All_except [a] f)"
1050 by(simp add: finfun_All_def finfun_All_except_update)
1052 lemma finfun_All_All: "finfun_All P = All P\<^sub>f"
1053 by(simp add: finfun_All_def finfun_All_except_def)
1056 definition finfun_Ex :: "'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
1057 where "finfun_Ex P = Not (finfun_All (Not \<circ>\<^isub>f P))"
1059 lemma finfun_Ex_Ex: "finfun_Ex P = Ex P\<^sub>f"
1060 unfolding finfun_Ex_def finfun_All_All by simp
1062 lemma finfun_Ex_const [simp]: "finfun_Ex (\<lambda>\<^isup>f b) = b"
1063 by(simp add: finfun_Ex_def)
1066 subsection {* A diagonal operator for FinFuns *}
1068 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)
1069 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"
1071 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))"
1072 by(unfold_locales)(simp_all add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
1074 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))"
1077 assume fin: "finite (UNIV :: 'c set)"
1079 interpret comp_fun_commute "\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))" by(rule finfun_Diag_aux.upd_left_comm)
1080 from fin have "finite A" by(auto intro: finite_subset)
1081 hence "Finite_Set.fold (\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))) (Pair b \<circ>\<^isub>f g) A =
1082 Abs_finfun (\<lambda>a. (if a \<in> A then b' else b, g\<^sub>f a))"
1083 by(induct)(simp_all add: finfun_const_def finfun_comp_conv_comp o_def,
1084 auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite fun_eq_iff fin) }
1085 from this[of UNIV] show "Finite_Set.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"
1086 by(simp add: finfun_const_def finfun_comp_conv_comp o_def)
1089 lemma finfun_Diag_const1: "(\<lambda>\<^isup>f b, g)\<^sup>f = Pair b \<circ>\<^isub>f g"
1090 by(simp add: finfun_Diag_def)
1093 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"}.
1096 lemma finfun_Diag_const_code [code]:
1097 "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))"
1098 "(\<lambda>\<^isup>f b, g(\<^sup>fc a := c))\<^sup>f = (\<lambda>\<^isup>f b, g)\<^sup>f(\<^sup>fc a := (b, c))"
1099 by(simp_all add: finfun_Diag_const1)
1101 lemma finfun_Diag_update1: "(f(\<^sup>f a := b), g)\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (b, g\<^sub>f a))"
1102 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))"
1103 by(simp_all add: finfun_Diag_def)
1105 lemma finfun_Diag_const2: "(f, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>b. (b, c)) \<circ>\<^isub>f f"
1106 by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
1108 lemma finfun_Diag_update2: "(f, g(\<^sup>f a := c))\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (f\<^sub>f a, c))"
1109 by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
1111 lemma finfun_Diag_const_const [simp]: "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))"
1112 by(simp add: finfun_Diag_const1)
1114 lemma finfun_Diag_const_update:
1115 "(\<lambda>\<^isup>f b, g(\<^sup>f a := c))\<^sup>f = (\<lambda>\<^isup>f b, g)\<^sup>f(\<^sup>f a := (b, c))"
1116 by(simp add: finfun_Diag_const1)
1118 lemma finfun_Diag_update_const:
1119 "(f(\<^sup>f a := b), \<lambda>\<^isup>f c)\<^sup>f = (f, \<lambda>\<^isup>f c)\<^sup>f(\<^sup>f a := (b, c))"
1120 by(simp add: finfun_Diag_def)
1122 lemma finfun_Diag_update_update:
1123 "(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)))"
1124 by(auto simp add: finfun_Diag_update1 finfun_Diag_update2)
1126 lemma finfun_Diag_apply [simp]: "(f, g)\<^sup>f\<^sub>f = (\<lambda>x. (f\<^sub>f x, g\<^sub>f x))"
1127 by(induct f rule: finfun_weak_induct)(auto simp add: finfun_Diag_const1 finfun_Diag_update1 finfun_upd_apply intro: ext)
1129 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1131 lemma finfun_Diag_conv_Abs_finfun:
1132 "(f, g)\<^sup>f = Abs_finfun ((\<lambda>x. (finfun_apply f x, finfun_apply g x)))"
1134 have "(\<lambda>f :: 'a \<Rightarrow>\<^isub>f 'b. (f, g)\<^sup>f) = (\<lambda>f. Abs_finfun ((\<lambda>x. (finfun_apply f x, finfun_apply g x))))"
1135 proof(rule finfun_rec_unique)
1136 { fix c show "Abs_finfun (\<lambda>x. (finfun_apply (\<lambda>\<^isup>f c) x, finfun_apply g x)) = Pair c \<circ>\<^isub>f g"
1137 by(simp add: finfun_comp_conv_comp o_def finfun_const_def) }
1139 show "Abs_finfun (\<lambda>x. (finfun_apply g'(\<^sup>f a := b) x, finfun_apply g x)) =
1140 (Abs_finfun (\<lambda>x. (finfun_apply g' x, finfun_apply g x)))(\<^sup>f a := (b, g\<^sub>f a))"
1141 by(auto simp add: finfun_update_def fun_eq_iff simp del: fun_upd_apply) simp }
1142 qed(simp_all add: finfun_Diag_const1 finfun_Diag_update1)
1143 thus ?thesis by(auto simp add: fun_eq_iff)
1146 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1148 lemma finfun_Diag_eq: "(f, g)\<^sup>f = (f', g')\<^sup>f \<longleftrightarrow> f = f' \<and> g = g'"
1149 by(auto simp add: expand_finfun_eq fun_eq_iff)
1151 definition finfun_fst :: "'a \<Rightarrow>\<^isub>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b"
1152 where [code]: "finfun_fst f = fst \<circ>\<^isub>f f"
1154 lemma finfun_fst_const: "finfun_fst (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f fst bc)"
1155 by(simp add: finfun_fst_def)
1157 lemma finfun_fst_update: "finfun_fst (f(\<^sup>f a := bc)) = (finfun_fst f)(\<^sup>f a := fst bc)"
1158 and finfun_fst_update_code: "finfun_fst (finfun_update_code f a bc) = (finfun_fst f)(\<^sup>f a := fst bc)"
1159 by(simp_all add: finfun_fst_def)
1161 lemma finfun_fst_comp_conv: "finfun_fst (f \<circ>\<^isub>f g) = (fst \<circ> f) \<circ>\<^isub>f g"
1162 by(simp add: finfun_fst_def)
1164 lemma finfun_fst_conv [simp]: "finfun_fst (f, g)\<^sup>f = f"
1165 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)
1167 lemma finfun_fst_conv_Abs_finfun: "finfun_fst = (\<lambda>f. Abs_finfun (fst o finfun_apply f))"
1168 by(simp add: finfun_fst_def [abs_def] finfun_comp_conv_comp)
1171 definition finfun_snd :: "'a \<Rightarrow>\<^isub>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c"
1172 where [code]: "finfun_snd f = snd \<circ>\<^isub>f f"
1174 lemma finfun_snd_const: "finfun_snd (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f snd bc)"
1175 by(simp add: finfun_snd_def)
1177 lemma finfun_snd_update: "finfun_snd (f(\<^sup>f a := bc)) = (finfun_snd f)(\<^sup>f a := snd bc)"
1178 and finfun_snd_update_code [code]: "finfun_snd (finfun_update_code f a bc) = (finfun_snd f)(\<^sup>f a := snd bc)"
1179 by(simp_all add: finfun_snd_def)
1181 lemma finfun_snd_comp_conv: "finfun_snd (f \<circ>\<^isub>f g) = (snd \<circ> f) \<circ>\<^isub>f g"
1182 by(simp add: finfun_snd_def)
1184 lemma finfun_snd_conv [simp]: "finfun_snd (f, g)\<^sup>f = g"
1185 apply(induct f rule: finfun_weak_induct)
1186 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)
1189 lemma finfun_snd_conv_Abs_finfun: "finfun_snd = (\<lambda>f. Abs_finfun (snd o finfun_apply f))"
1190 by(simp add: finfun_snd_def [abs_def] finfun_comp_conv_comp)
1192 lemma finfun_Diag_collapse [simp]: "(finfun_fst f, finfun_snd f)\<^sup>f = f"
1193 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)
1195 subsection {* Currying for FinFuns *}
1197 definition finfun_curry :: "('a \<times> 'b) \<Rightarrow>\<^isub>f 'c \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b \<Rightarrow>\<^isub>f 'c"
1198 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)))"
1200 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))"
1201 apply(unfold_locales)
1202 apply(auto simp add: split_def finfun_update_twist finfun_upd_apply split_paired_all finfun_update_const_same)
1205 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1207 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))"
1208 proof(unfold_locales)
1210 assume fin: "finite (UNIV :: ('c \<times> 'a) set)"
1211 hence fin1: "finite (UNIV :: 'c set)" and fin2: "finite (UNIV :: 'a set)"
1212 unfolding UNIV_Times_UNIV[symmetric]
1213 by(fastforce dest: finite_cartesian_productD1 finite_cartesian_productD2)+
1214 note [simp] = Abs_finfun_inverse_finite[OF fin] Abs_finfun_inverse_finite[OF fin1] Abs_finfun_inverse_finite[OF fin2]
1215 { fix A :: "('c \<times> 'a) set"
1216 interpret comp_fun_commute "\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))) a b'"
1217 by(rule finfun_curry_aux.upd_left_comm)
1218 from fin have "finite A" by(auto intro: finite_subset)
1219 hence "Finite_Set.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))"
1220 by induct (simp_all, auto simp add: finfun_update_def finfun_const_def split_def intro!: arg_cong[where f="Abs_finfun"] ext) }
1222 show "Finite_Set.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'"
1223 by(simp add: finfun_const_def)
1226 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1228 lemma finfun_curry_const [simp, code]: "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
1229 by(simp add: finfun_curry_def)
1231 lemma finfun_curry_update [simp]:
1232 "finfun_curry (f(\<^sup>f (a, b) := c)) = (finfun_curry f)(\<^sup>f a := ((finfun_curry f)\<^sub>f a)(\<^sup>f b := c))"
1233 and finfun_curry_update_code [code]:
1234 "finfun_curry (f(\<^sup>fc (a, b) := c)) = (finfun_curry f)(\<^sup>f a := ((finfun_curry f)\<^sub>f a)(\<^sup>f b := c))"
1235 by(simp_all add: finfun_curry_def)
1237 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1239 lemma finfun_Abs_finfun_curry: assumes fin: "f \<in> finfun"
1240 shows "(\<lambda>a. Abs_finfun (curry f a)) \<in> finfun"
1242 from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast
1243 have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force)
1244 hence "{a. curry f a \<noteq> (\<lambda>x. c)} = fst ` {ab. f ab \<noteq> c}"
1245 by(auto simp add: curry_def fun_eq_iff)
1246 with fin c have "finite {a. Abs_finfun (curry f a) \<noteq> (\<lambda>\<^isup>f c)}"
1247 by(simp add: finfun_const_def finfun_curry)
1248 thus ?thesis unfolding finfun_def by auto
1251 lemma finfun_curry_conv_curry:
1252 fixes f :: "('a \<times> 'b) \<Rightarrow>\<^isub>f 'c"
1253 shows "finfun_curry f = Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply f) a))"
1255 have "finfun_curry = (\<lambda>f :: ('a \<times> 'b) \<Rightarrow>\<^isub>f 'c. Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply f) a)))"
1256 proof(rule finfun_rec_unique)
1257 { fix c show "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)" by simp }
1258 { 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))"
1260 { fix c show "Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply (\<lambda>\<^isup>f c)) a)) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
1261 by(simp add: finfun_curry_def finfun_const_def curry_def) }
1263 show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (finfun_apply g(\<^sup>f a := b)) aa)) =
1264 (Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply g) a)))(\<^sup>f
1265 fst a := ((Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply g) a)))\<^sub>f (fst a))(\<^sup>f snd a := b))"
1266 by(cases a)(auto intro!: ext arg_cong[where f=Abs_finfun] simp add: finfun_curry_def finfun_update_def finfun_curry finfun_Abs_finfun_curry) }
1268 thus ?thesis by(auto simp add: fun_eq_iff)
1271 subsection {* Executable equality for FinFuns *}
1273 lemma eq_finfun_All_ext: "(f = g) \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>\<^isub>f (f, g)\<^sup>f)"
1274 by(simp add: expand_finfun_eq fun_eq_iff finfun_All_All o_def)
1276 instantiation finfun :: ("{card_UNIV,equal}",equal) equal begin
1277 definition eq_finfun_def [code]: "HOL.equal f g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>\<^isub>f (f, g)\<^sup>f)"
1278 instance by(intro_classes)(simp add: eq_finfun_All_ext eq_finfun_def)
1282 "HOL.equal (f :: _ \<Rightarrow>\<^isub>f _) f \<longleftrightarrow> True"
1283 by (fact equal_refl)
1285 subsection {* An operator that explicitly removes all redundant updates in the generated representations *}
1287 definition finfun_clearjunk :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b"
1288 where [simp, code del]: "finfun_clearjunk = id"
1290 lemma finfun_clearjunk_const [code]: "finfun_clearjunk (\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b)"
1293 lemma finfun_clearjunk_update [code]: "finfun_clearjunk (finfun_update_code f a b) = f(\<^sup>f a := b)"
1296 subsection {* The domain of a FinFun as a FinFun *}
1298 definition finfun_dom :: "('a \<Rightarrow>\<^isub>f 'b) \<Rightarrow> ('a \<Rightarrow>\<^isub>f bool)"
1299 where [code del]: "finfun_dom f = Abs_finfun (\<lambda>a. f\<^sub>f a \<noteq> finfun_default f)"
1301 lemma finfun_dom_const:
1302 "finfun_dom ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = (\<lambda>\<^isup>f finite (UNIV :: 'a set) \<and> c \<noteq> undefined)"
1303 unfolding finfun_dom_def finfun_default_const
1304 by(auto)(simp_all add: finfun_const_def)
1307 @{term "finfun_dom" } raises an exception when called on a FinFun whose domain is a finite type.
1308 For such FinFuns, the default value (and as such the domain) is undefined.
1311 lemma finfun_dom_const_code [code]:
1312 "finfun_dom ((\<lambda>\<^isup>f c) :: ('a :: card_UNIV) \<Rightarrow>\<^isub>f 'b) =
1313 (if card_UNIV (TYPE('a)) = 0 then (\<lambda>\<^isup>f False) else FinFun.code_abort (\<lambda>_. finfun_dom (\<lambda>\<^isup>f c)))"
1314 unfolding card_UNIV_eq_0_infinite_UNIV
1315 by(simp add: finfun_dom_const)
1317 lemma finfun_dom_finfunI: "(\<lambda>a. f\<^sub>f a \<noteq> finfun_default f) \<in> finfun"
1318 using finite_finfun_default[of f]
1319 by(simp add: finfun_def exI[where x=False])
1321 lemma finfun_dom_update [simp]:
1322 "finfun_dom (f(\<^sup>f a := b)) = (finfun_dom f)(\<^sup>f a := (b \<noteq> finfun_default f))"
1323 unfolding finfun_dom_def finfun_update_def
1324 apply(simp add: finfun_default_update_const fun_upd_apply finfun_dom_finfunI)
1325 apply(fold finfun_update.rep_eq)
1326 apply(simp add: finfun_upd_apply fun_eq_iff fun_upd_def finfun_default_update_const)
1329 lemma finfun_dom_update_code [code]:
1330 "finfun_dom (finfun_update_code f a b) = finfun_update_code (finfun_dom f) a (b \<noteq> finfun_default f)"
1333 lemma finite_finfun_dom: "finite {x. (finfun_dom f)\<^sub>f x}"
1334 proof(induct f rule: finfun_weak_induct)
1337 by (cases "finite (UNIV :: 'a set) \<and> b \<noteq> undefined")
1338 (auto simp add: finfun_dom_const UNIV_def [symmetric] Set.empty_def [symmetric])
1341 have "{x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} =
1342 (if b = finfun_default f then {x. (finfun_dom f)\<^sub>f x} - {a} else insert a {x. (finfun_dom f)\<^sub>f x})"
1343 by (auto simp add: finfun_upd_apply split: split_if_asm)
1344 thus ?case using update by simp
1348 subsection {* The domain of a FinFun as a sorted list *}
1350 definition finfun_to_list :: "('a :: linorder) \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a list"
1352 "finfun_to_list f = (THE xs. set xs = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs \<and> distinct xs)"
1354 lemma set_finfun_to_list [simp]: "set (finfun_to_list f) = {x. (finfun_dom f)\<^sub>f x}" (is ?thesis1)
1355 and sorted_finfun_to_list: "sorted (finfun_to_list f)" (is ?thesis2)
1356 and distinct_finfun_to_list: "distinct (finfun_to_list f)" (is ?thesis3)
1358 have "?thesis1 \<and> ?thesis2 \<and> ?thesis3"
1359 unfolding finfun_to_list_def
1360 by(rule theI')(rule finite_sorted_distinct_unique finite_finfun_dom)+
1361 thus ?thesis1 ?thesis2 ?thesis3 by simp_all
1364 lemma finfun_const_False_conv_bot: "(\<lambda>\<^isup>f False)\<^sub>f = bot"
1367 lemma finfun_const_True_conv_top: "(\<lambda>\<^isup>f True)\<^sub>f = top"
1370 lemma finfun_to_list_const:
1371 "finfun_to_list ((\<lambda>\<^isup>f c) :: ('a :: {linorder} \<Rightarrow>\<^isub>f 'b)) =
1372 (if \<not> finite (UNIV :: 'a set) \<or> c = undefined then [] else THE xs. set xs = UNIV \<and> sorted xs \<and> distinct xs)"
1373 by(auto simp add: finfun_to_list_def finfun_const_False_conv_bot finfun_const_True_conv_top finfun_dom_const)
1375 lemma finfun_to_list_const_code [code]:
1376 "finfun_to_list ((\<lambda>\<^isup>f c) :: ('a :: {linorder, card_UNIV} \<Rightarrow>\<^isub>f 'b)) =
1377 (if card_UNIV (TYPE('a)) = 0 then [] else FinFun.code_abort (\<lambda>_. finfun_to_list ((\<lambda>\<^isup>f c) :: ('a \<Rightarrow>\<^isub>f 'b))))"
1378 unfolding card_UNIV_eq_0_infinite_UNIV
1379 by(auto simp add: finfun_to_list_const)
1381 lemma remove1_insort_insert_same:
1382 "x \<notin> set xs \<Longrightarrow> remove1 x (insort_insert x xs) = xs"
1383 by (metis insort_insert_insort remove1_insort)
1385 lemma finfun_dom_conv:
1386 "(finfun_dom f)\<^sub>f x \<longleftrightarrow> f\<^sub>f x \<noteq> finfun_default f"
1387 by(induct f rule: finfun_weak_induct)(auto simp add: finfun_dom_const finfun_default_const finfun_default_update_const finfun_upd_apply)
1389 lemma finfun_to_list_update:
1390 "finfun_to_list (f(\<^sup>f a := b)) =
1391 (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
1392 proof(subst finfun_to_list_def, rule the_equality)
1394 assume "set xs = {x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} \<and> sorted xs \<and> distinct xs"
1395 hence eq: "set xs = {x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x}"
1396 and [simp]: "sorted xs" "distinct xs" by simp_all
1397 show "xs = (if b = finfun_default f then remove1 a (finfun_to_list f) else insort_insert a (finfun_to_list f))"
1398 proof(cases "b = finfun_default f")
1401 proof(cases "(finfun_dom f)\<^sub>f a")
1403 have "finfun_to_list f = insort_insert a xs"
1404 unfolding finfun_to_list_def
1405 proof(rule the_equality)
1406 have "set (insort_insert a xs) = insert a (set xs)" by(simp add: set_insort_insert)
1408 have "insert a {x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} = {x. (finfun_dom f)\<^sub>f x}" using True
1409 by(auto simp add: finfun_upd_apply split: split_if_asm)
1410 finally show 1: "set (insort_insert a xs) = {x. (finfun_dom f)\<^sub>f x} \<and> sorted (insort_insert a xs) \<and> distinct (insort_insert a xs)"
1411 by(simp add: sorted_insort_insert distinct_insort_insert)
1414 assume "set xs' = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs' \<and> distinct xs'"
1415 thus "xs' = insort_insert a xs" using 1 by(auto dest: sorted_distinct_set_unique)
1417 with eq True show ?thesis by(simp add: remove1_insort_insert_same)
1420 hence "f\<^sub>f a = b" by(auto simp add: finfun_dom_conv)
1421 hence f: "f(\<^sup>f a := b) = f" by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
1422 from eq have "finfun_to_list f = xs" unfolding f finfun_to_list_def
1423 by(auto elim: sorted_distinct_set_unique intro!: the_equality)
1424 with eq False show ?thesis unfolding f by(simp add: remove1_idem)
1429 proof(cases "(finfun_dom f)\<^sub>f a")
1431 have "finfun_to_list f = xs"
1432 unfolding finfun_to_list_def
1433 proof(rule the_equality)
1434 have "finfun_dom f = finfun_dom f(\<^sup>f a := b)" using False True
1435 by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
1436 with eq show 1: "set xs = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs \<and> distinct xs"
1437 by(simp del: finfun_dom_update)
1440 assume "set xs' = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs' \<and> distinct xs'"
1441 thus "xs' = xs" using 1 by(auto elim: sorted_distinct_set_unique)
1443 thus ?thesis using False True eq by(simp add: insort_insert_triv)
1446 have "finfun_to_list f = remove1 a xs"
1447 unfolding finfun_to_list_def
1448 proof(rule the_equality)
1449 have "set (remove1 a xs) = set xs - {a}" by simp
1451 have "{x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} - {a} = {x. (finfun_dom f)\<^sub>f x}" using False
1452 by(auto simp add: finfun_upd_apply split: split_if_asm)
1453 finally show 1: "set (remove1 a xs) = {x. (finfun_dom f)\<^sub>f x} \<and> sorted (remove1 a xs) \<and> distinct (remove1 a xs)"
1454 by(simp add: sorted_remove1)
1457 assume "set xs' = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs' \<and> distinct xs'"
1458 thus "xs' = remove1 a xs" using 1 by(blast intro: sorted_distinct_set_unique)
1460 thus ?thesis using False eq `b \<noteq> finfun_default f`
1461 by (simp add: insort_insert_insort insort_remove1)
1464 qed (auto simp add: distinct_finfun_to_list sorted_finfun_to_list sorted_remove1 set_insort_insert sorted_insort_insert distinct_insort_insert finfun_upd_apply split: split_if_asm)
1466 lemma finfun_to_list_update_code [code]:
1467 "finfun_to_list (finfun_update_code f a b) =
1468 (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
1469 by(simp add: finfun_to_list_update)