1 (* Author: Andreas Lochbihler, Uni Karlsruhe *)
3 section \<open>Almost everywhere constant functions\<close>
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 subsection \<open>The \<open>map_default\<close> operation\<close>
22 definition map_default :: "'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
23 where "map_default b f a \<equiv> case f a of None \<Rightarrow> b | Some b' \<Rightarrow> b'"
25 lemma map_default_delete [simp]:
26 "map_default b (f(a := None)) = (map_default b f)(a := b)"
27 by(simp add: map_default_def fun_eq_iff)
29 lemma map_default_insert:
30 "map_default b (f(a \<mapsto> b')) = (map_default b f)(a := b')"
31 by(simp add: map_default_def fun_eq_iff)
33 lemma map_default_empty [simp]: "map_default b empty = (\<lambda>a. b)"
34 by(simp add: fun_eq_iff map_default_def)
36 lemma map_default_inject:
37 fixes g g' :: "'a \<rightharpoonup> 'b"
38 assumes infin_eq: "\<not> finite (UNIV :: 'a set) \<or> b = b'"
39 and fin: "finite (dom g)" and b: "b \<notin> ran g"
40 and fin': "finite (dom g')" and b': "b' \<notin> ran g'"
41 and eq': "map_default b g = map_default b' g'"
42 shows "b = b'" "g = g'"
44 from infin_eq show bb': "b = b'"
46 assume infin: "\<not> finite (UNIV :: 'a set)"
47 from fin fin' have "finite (dom g \<union> dom g')" by auto
48 with infin have "UNIV - (dom g \<union> dom g') \<noteq> {}" by(auto dest: finite_subset)
49 then obtain a where a: "a \<notin> dom g \<union> dom g'" by auto
50 hence "map_default b g a = b" "map_default b' g' a = b'" by(auto simp add: map_default_def)
51 with eq' show "b = b'" by simp
60 hence "map_default b g x = b" by(simp add: map_default_def)
61 with bb' eq' have "map_default b' g' x = b'" by simp
62 with b' have "g' x = None" by(simp add: map_default_def ran_def split: option.split_asm)
63 with None show ?thesis by simp
66 with b have cb: "c \<noteq> b" by(auto simp add: ran_def)
67 moreover from Some have "map_default b g x = c" by(simp add: map_default_def)
68 with eq' have "map_default b' g' x = c" by simp
69 ultimately have "g' x = Some c" using b' bb' by(auto simp add: map_default_def split: option.splits)
70 with Some show ?thesis by simp
75 subsection \<open>The finfun type\<close>
77 definition "finfun = {f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}"
79 typedef ('a,'b) finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set"
80 morphisms finfun_apply Abs_finfun
82 have "\<exists>f. finite {x. f x \<noteq> undefined}"
84 show "finite {x. (\<lambda>y. undefined) x \<noteq> undefined}" by auto
86 then show ?thesis unfolding finfun_def by auto
89 type_notation finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
91 setup_lifting type_definition_finfun
93 lemma fun_upd_finfun: "y(a := b) \<in> finfun \<longleftrightarrow> y \<in> finfun"
96 have "finite {a'. (y(a := b)) a' \<noteq> b'} = finite {a'. y a' \<noteq> b'}"
99 hence "{a'. (y(a := b)) a' \<noteq> b'} = {a'. y a' \<noteq> b'} - {a}" by auto
103 hence "{a'. (y(a := b)) a' \<noteq> b'} = insert a {a'. y a' \<noteq> b'}" by auto
106 thus ?thesis unfolding finfun_def by blast
109 lemma const_finfun: "(\<lambda>x. a) \<in> finfun"
110 by(auto simp add: finfun_def)
112 lemma finfun_left_compose:
113 assumes "y \<in> finfun"
114 shows "g \<circ> y \<in> finfun"
116 from assms obtain b where "finite {a. y a \<noteq> b}"
117 unfolding finfun_def by blast
118 hence "finite {c. g (y c) \<noteq> g b}"
119 proof(induct "{a. y a \<noteq> b}" arbitrary: y)
121 hence "y = (\<lambda>a. b)" by(auto)
125 note IH = \<open>\<And>y. F = {a. y a \<noteq> b} \<Longrightarrow> finite {c. g (y c) \<noteq> g b}\<close>
126 from \<open>insert x F = {a. y a \<noteq> b}\<close> \<open>x \<notin> F\<close>
127 have F: "F = {a. (y(x := b)) a \<noteq> b}" by(auto)
129 proof(cases "g (y x) = g b")
131 hence "{c. g ((y(x := b)) c) \<noteq> g b} = {c. g (y c) \<noteq> g b}" by auto
132 with IH[OF F] show ?thesis by simp
135 hence "{c. g (y c) \<noteq> g b} = insert x {c. g ((y(x := b)) c) \<noteq> g b}" by auto
136 with IH[OF F] show ?thesis by(simp)
139 thus ?thesis unfolding finfun_def by auto
142 lemma assumes "y \<in> finfun"
143 shows fst_finfun: "fst \<circ> y \<in> finfun"
144 and snd_finfun: "snd \<circ> y \<in> finfun"
146 from assms obtain b c where bc: "finite {a. y a \<noteq> (b, c)}"
147 unfolding finfun_def by auto
148 have "{a. fst (y a) \<noteq> b} \<subseteq> {a. y a \<noteq> (b, c)}"
149 and "{a. snd (y a) \<noteq> c} \<subseteq> {a. y a \<noteq> (b, c)}" by auto
150 hence "finite {a. fst (y a) \<noteq> b}"
151 and "finite {a. snd (y a) \<noteq> c}" using bc by(auto intro: finite_subset)
152 thus "fst \<circ> y \<in> finfun" "snd \<circ> y \<in> finfun"
153 unfolding finfun_def by auto
156 lemma map_of_finfun: "map_of xs \<in> finfun"
158 by(induct xs)(auto simp add: Collect_neg_eq Collect_conj_eq Collect_imp_eq intro: finite_subset)
160 lemma Diag_finfun: "(\<lambda>x. (f x, g x)) \<in> finfun \<longleftrightarrow> f \<in> finfun \<and> g \<in> finfun"
161 by(auto intro: finite_subset simp add: Collect_neg_eq Collect_imp_eq Collect_conj_eq finfun_def)
163 lemma finfun_right_compose:
164 assumes g: "g \<in> finfun" and inj: "inj f"
165 shows "g o f \<in> finfun"
167 from g obtain b where b: "finite {a. g a \<noteq> b}" unfolding finfun_def by blast
168 moreover have "f ` {a. g (f a) \<noteq> b} \<subseteq> {a. g a \<noteq> b}" by auto
169 moreover from inj have "inj_on f {a. g (f a) \<noteq> b}" by(rule subset_inj_on) blast
170 ultimately have "finite {a. g (f a) \<noteq> b}"
171 by(blast intro: finite_imageD[where f=f] finite_subset)
172 thus ?thesis unfolding finfun_def by auto
176 assumes fin: "f \<in> finfun"
177 shows "curry f \<in> finfun" "curry f a \<in> finfun"
179 from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast
180 moreover have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force)
181 hence "{a. curry f a \<noteq> (\<lambda>b. c)} = fst ` {ab. f ab \<noteq> c}"
182 by(auto simp add: curry_def fun_eq_iff)
183 ultimately have "finite {a. curry f a \<noteq> (\<lambda>b. c)}" by simp
184 thus "curry f \<in> finfun" unfolding finfun_def by blast
186 have "snd ` {ab. f ab \<noteq> c} = {b. \<exists>a. f (a, b) \<noteq> c}" by(force)
187 hence "{b. f (a, b) \<noteq> c} \<subseteq> snd ` {ab. f ab \<noteq> c}" by auto
188 hence "finite {b. f (a, b) \<noteq> c}" by(rule finite_subset)(rule finite_imageI[OF c])
189 thus "curry f a \<in> finfun" unfolding finfun_def by auto
193 fst_finfun[simp] snd_finfun[simp] Abs_finfun_inverse[simp]
194 finfun_apply_inverse[simp] Abs_finfun_inject[simp] finfun_apply_inject[simp]
195 Diag_finfun[simp] finfun_curry[simp]
196 const_finfun[iff] fun_upd_finfun[iff] finfun_apply[iff] map_of_finfun[iff]
197 finfun_left_compose[intro] fst_finfun[intro] snd_finfun[intro]
199 lemma Abs_finfun_inject_finite:
200 fixes x y :: "'a \<Rightarrow> 'b"
201 assumes fin: "finite (UNIV :: 'a set)"
202 shows "Abs_finfun x = Abs_finfun y \<longleftrightarrow> x = y"
204 assume "Abs_finfun x = Abs_finfun y"
205 moreover have "x \<in> finfun" "y \<in> finfun" unfolding finfun_def
206 by(auto intro: finite_subset[OF _ fin])
207 ultimately show "x = y" by(simp add: Abs_finfun_inject)
210 lemma Abs_finfun_inject_finite_class:
211 fixes x y :: "('a :: finite) \<Rightarrow> 'b"
212 shows "Abs_finfun x = Abs_finfun y \<longleftrightarrow> x = y"
214 by(simp add: Abs_finfun_inject_finite)
216 lemma Abs_finfun_inj_finite:
217 assumes fin: "finite (UNIV :: 'a set)"
218 shows "inj (Abs_finfun :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>f 'b)"
220 fix x y :: "'a \<Rightarrow> 'b"
221 assume "Abs_finfun x = Abs_finfun y"
222 moreover have "x \<in> finfun" "y \<in> finfun" unfolding finfun_def
223 by(auto intro: finite_subset[OF _ fin])
224 ultimately show "x = y" by(simp add: Abs_finfun_inject)
227 lemma Abs_finfun_inverse_finite:
228 fixes x :: "'a \<Rightarrow> 'b"
229 assumes fin: "finite (UNIV :: 'a set)"
230 shows "finfun_apply (Abs_finfun x) = x"
233 from fin have "x \<in> finfun"
234 by(auto simp add: finfun_def intro: finite_subset)
238 lemma Abs_finfun_inverse_finite_class:
239 fixes x :: "('a :: finite) \<Rightarrow> 'b"
240 shows "finfun_apply (Abs_finfun x) = x"
241 using finite_UNIV by(simp add: Abs_finfun_inverse_finite)
243 lemma finfun_eq_finite_UNIV: "finite (UNIV :: 'a set) \<Longrightarrow> (finfun :: ('a \<Rightarrow> 'b) set) = UNIV"
244 unfolding finfun_def by(auto intro: finite_subset)
246 lemma finfun_finite_UNIV_class: "finfun = (UNIV :: ('a :: finite \<Rightarrow> 'b) set)"
247 by(simp add: finfun_eq_finite_UNIV)
249 lemma map_default_in_finfun:
250 assumes fin: "finite (dom f)"
251 shows "map_default b f \<in> finfun"
253 proof(intro CollectI exI)
254 from fin show "finite {a. map_default b f a \<noteq> b}"
255 by(auto simp add: map_default_def dom_def Collect_conj_eq split: option.splits)
258 lemma finfun_cases_map_default:
259 obtains b g where "f = Abs_finfun (map_default b g)" "finite (dom g)" "b \<notin> ran g"
261 obtain y where f: "f = Abs_finfun y" and y: "y \<in> finfun" by(cases f)
262 from y obtain b where b: "finite {a. y a \<noteq> b}" unfolding finfun_def by auto
263 let ?g = "(\<lambda>a. if y a = b then None else Some (y a))"
264 have "map_default b ?g = y" by(simp add: fun_eq_iff map_default_def)
265 with f have "f = Abs_finfun (map_default b ?g)" by simp
266 moreover from b have "finite (dom ?g)" by(auto simp add: dom_def)
267 moreover have "b \<notin> ran ?g" by(auto simp add: ran_def)
268 ultimately show ?thesis by(rule that)
272 subsection \<open>Kernel functions for type @{typ "'a \<Rightarrow>f 'b"}\<close>
274 lift_definition finfun_const :: "'b \<Rightarrow> 'a \<Rightarrow>f 'b" ("K$/ _" [0] 1)
275 is "\<lambda> b x. b" by (rule const_finfun)
277 lift_definition finfun_update :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>f 'b" ("_'(_ $:= _')" [1000,0,0] 1000) is "fun_upd"
278 by (simp add: fun_upd_finfun)
280 lemma finfun_update_twist: "a \<noteq> a' \<Longrightarrow> f(a $:= b)(a' $:= b') = f(a' $:= b')(a $:= b)"
281 by transfer (simp add: fun_upd_twist)
283 lemma finfun_update_twice [simp]:
284 "f(a $:= b)(a $:= b') = f(a $:= b')"
287 lemma finfun_update_const_same: "(K$ b)(a $:= b) = (K$ b)"
288 by transfer (simp add: fun_eq_iff)
290 subsection \<open>Code generator setup\<close>
292 definition finfun_update_code :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>f 'b"
293 where [simp, code del]: "finfun_update_code = finfun_update"
295 code_datatype finfun_const finfun_update_code
297 lemma finfun_update_const_code [code]:
298 "(K$ b)(a $:= b') = (if b = b' then (K$ b) else finfun_update_code (K$ b) a b')"
299 by(simp add: finfun_update_const_same)
301 lemma finfun_update_update_code [code]:
302 "(finfun_update_code f a b)(a' $:= b') = (if a = a' then f(a $:= b') else finfun_update_code (f(a' $:= b')) a b)"
303 by(simp add: finfun_update_twist)
306 subsection \<open>Setup for quickcheck\<close>
308 quickcheck_generator finfun constructors: finfun_update_code, "finfun_const :: 'b \<Rightarrow> 'a \<Rightarrow>f 'b"
310 subsection \<open>\<open>finfun_update\<close> as instance of \<open>comp_fun_commute\<close>\<close>
312 interpretation finfun_update: comp_fun_commute "\<lambda>a f. f(a :: 'a $:= b')"
316 show "(\<lambda>f. f(a $:= b')) \<circ> (\<lambda>f. f(a' $:= b')) = (\<lambda>f. f(a' $:= b')) \<circ> (\<lambda>f. f(a $:= b'))"
319 have "(finfun_apply b)(a := b', a' := b') = (finfun_apply b)(a' := b', a := b')"
320 by(cases "a = a'")(auto simp add: fun_upd_twist)
321 then have "b(a $:= b')(a' $:= b') = b(a' $:= b')(a $:= b')"
322 by(auto simp add: finfun_update_def fun_upd_twist)
323 then show "((\<lambda>f. f(a $:= b')) \<circ> (\<lambda>f. f(a' $:= b'))) b = ((\<lambda>f. f(a' $:= b')) \<circ> (\<lambda>f. f(a $:= b'))) b"
324 by (simp add: fun_eq_iff)
328 lemma fold_finfun_update_finite_univ:
329 assumes fin: "finite (UNIV :: 'a set)"
330 shows "Finite_Set.fold (\<lambda>a f. f(a $:= b')) (K$ b) (UNIV :: 'a set) = (K$ b')"
333 from fin have "finite A" by(auto intro: finite_subset)
334 hence "Finite_Set.fold (\<lambda>a f. f(a $:= b')) (K$ b) A = Abs_finfun (\<lambda>a. if a \<in> A then b' else b)"
337 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)"
339 with insert show ?case
340 by(simp add: finfun_const_def fun_upd_def)(simp add: finfun_update_def Abs_finfun_inverse_finite[OF fin] fun_upd_def)
341 qed(simp add: finfun_const_def) }
342 thus ?thesis by(simp add: finfun_const_def)
346 subsection \<open>Default value for FinFuns\<close>
348 definition finfun_default_aux :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"
349 where [code del]: "finfun_default_aux f = (if finite (UNIV :: 'a set) then undefined else THE b. finite {a. f a \<noteq> b})"
351 lemma finfun_default_aux_infinite:
352 fixes f :: "'a \<Rightarrow> 'b"
353 assumes infin: "\<not> finite (UNIV :: 'a set)"
354 and fin: "finite {a. f a \<noteq> b}"
355 shows "finfun_default_aux f = b"
357 let ?B = "{a. f a \<noteq> b}"
358 from fin have "(THE b. finite {a. f a \<noteq> b}) = b"
359 proof(rule the_equality)
361 assume "finite {a. f a \<noteq> b'}" (is "finite ?B'")
362 with infin fin have "UNIV - (?B' \<union> ?B) \<noteq> {}" by(auto dest: finite_subset)
363 then obtain a where a: "a \<notin> ?B' \<union> ?B" by auto
364 thus "b' = b" by auto
366 thus ?thesis using infin by(simp add: finfun_default_aux_def)
370 lemma finite_finfun_default_aux:
371 fixes f :: "'a \<Rightarrow> 'b"
372 assumes fin: "f \<in> finfun"
373 shows "finite {a. f a \<noteq> finfun_default_aux f}"
374 proof(cases "finite (UNIV :: 'a set)")
375 case True thus ?thesis using fin
376 by(auto simp add: finfun_def finfun_default_aux_def intro: finite_subset)
379 from fin obtain b where b: "finite {a. f a \<noteq> b}" (is "finite ?B")
380 unfolding finfun_def by blast
381 with False show ?thesis by(simp add: finfun_default_aux_infinite)
384 lemma finfun_default_aux_update_const:
385 fixes f :: "'a \<Rightarrow> 'b"
386 assumes fin: "f \<in> finfun"
387 shows "finfun_default_aux (f(a := b)) = finfun_default_aux f"
388 proof(cases "finite (UNIV :: 'a set)")
390 from fin obtain b' where b': "finite {a. f a \<noteq> b'}" unfolding finfun_def by blast
391 hence "finite {a'. (f(a := b)) a' \<noteq> b'}"
392 proof(cases "b = b' \<and> f a \<noteq> b'")
394 hence "{a. f a \<noteq> b'} = insert a {a'. (f(a := b)) a' \<noteq> b'}" by auto
395 thus ?thesis using b' by simp
399 { assume "b \<noteq> b'"
400 hence "{a'. (f(a := b)) a' \<noteq> b'} = insert a {a. f a \<noteq> b'}" by auto
401 hence ?thesis using b' by simp }
403 { assume "b = b'" "f a = b'"
404 hence "{a'. (f(a := b)) a' \<noteq> b'} = {a. f a \<noteq> b'}" by auto
405 hence ?thesis using b' by simp }
406 ultimately show ?thesis by blast
408 with False b' show ?thesis by(auto simp del: fun_upd_apply simp add: finfun_default_aux_infinite)
410 case True thus ?thesis by(simp add: finfun_default_aux_def)
413 lift_definition finfun_default :: "'a \<Rightarrow>f 'b \<Rightarrow> 'b"
414 is "finfun_default_aux" .
416 lemma finite_finfun_default: "finite {a. finfun_apply f a \<noteq> finfun_default f}"
417 by transfer (erule finite_finfun_default_aux)
419 lemma finfun_default_const: "finfun_default ((K$ b) :: 'a \<Rightarrow>f 'b) = (if finite (UNIV :: 'a set) then undefined else b)"
420 by(transfer)(auto simp add: finfun_default_aux_infinite finfun_default_aux_def)
422 lemma finfun_default_update_const:
423 "finfun_default (f(a $:= b)) = finfun_default f"
424 by transfer (simp add: finfun_default_aux_update_const)
426 lemma finfun_default_const_code [code]:
427 "finfun_default ((K$ c) :: 'a :: card_UNIV \<Rightarrow>f 'b) = (if CARD('a) = 0 then c else undefined)"
428 by(simp add: finfun_default_const)
430 lemma finfun_default_update_code [code]:
431 "finfun_default (finfun_update_code f a b) = finfun_default f"
432 by(simp add: finfun_default_update_const)
434 subsection \<open>Recursion combinator and well-formedness conditions\<close>
436 definition finfun_rec :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow>f 'b) \<Rightarrow> 'c"
438 "finfun_rec cnst upd f \<equiv>
439 let b = finfun_default f;
440 g = THE g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g
441 in Finite_Set.fold (\<lambda>a. upd a (map_default b g a)) (cnst b) (dom g)"
443 locale finfun_rec_wf_aux =
444 fixes cnst :: "'b \<Rightarrow> 'c"
445 and upd :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c"
446 assumes upd_const_same: "upd a b (cnst b) = cnst b"
447 and upd_commute: "a \<noteq> a' \<Longrightarrow> upd a b (upd a' b' c) = upd a' b' (upd a b c)"
448 and upd_idemp: "b \<noteq> b' \<Longrightarrow> upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)"
452 lemma upd_left_comm: "comp_fun_commute (\<lambda>a. upd a (f a))"
453 by(unfold_locales)(auto intro: upd_commute simp add: fun_eq_iff)
455 lemma upd_upd_twice: "upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)"
456 by(cases "b \<noteq> b'")(auto simp add: fun_upd_def upd_const_same upd_idemp)
458 lemma map_default_update_const:
459 assumes fin: "finite (dom f)"
460 and anf: "a \<notin> dom f"
461 and fg: "f \<subseteq>\<^sub>m g"
462 shows "upd a d (Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f)) =
463 Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f)"
465 let ?upd = "\<lambda>a. upd a (map_default d g a)"
466 let ?fr = "\<lambda>A. Finite_Set.fold ?upd (cnst d) A"
467 interpret gwf: comp_fun_commute "?upd" by(rule upd_left_comm)
469 from fin anf fg show ?thesis
470 proof(induct "dom f" arbitrary: f)
472 from \<open>{} = dom f\<close> have "f = empty" by(auto simp add: dom_def)
473 thus ?case by(simp add: finfun_const_def upd_const_same)
476 note IH = \<open>\<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)\<close>
477 note fin = \<open>finite A\<close> note anf = \<open>a \<notin> dom f\<close> note a'nA = \<open>a' \<notin> A\<close>
478 note domf = \<open>insert a' A = dom f\<close> note fg = \<open>f \<subseteq>\<^sub>m g\<close>
480 from domf obtain b where b: "f a' = Some b" by auto
481 let ?f' = "f(a' := None)"
482 have "upd a d (?fr (insert a' A)) = upd a d (upd a' (map_default d g a') (?fr A))"
483 by(subst gwf.fold_insert[OF fin a'nA]) rule
484 also from b fg have "g a' = f a'" by(auto simp add: map_le_def intro: domI dest: bspec)
485 hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def)
486 also from anf domf have "a \<noteq> a'" by auto note upd_commute[OF this]
487 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)
488 note A also note IH[OF A \<open>a \<notin> dom ?f'\<close> \<open>?f' \<subseteq>\<^sub>m g\<close>]
489 also have "upd a' (map_default d f a') (?fr (dom (f(a' := None)))) = ?fr (dom f)"
490 unfolding domf[symmetric] gwf.fold_insert[OF fin a'nA] ga' unfolding A ..
491 also have "insert a' (dom ?f') = dom f" using domf by auto
496 lemma map_default_update_twice:
497 assumes fin: "finite (dom f)"
498 and anf: "a \<notin> dom f"
499 and fg: "f \<subseteq>\<^sub>m g"
500 shows "upd a d'' (upd a d' (Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f))) =
501 upd a d'' (Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f))"
503 let ?upd = "\<lambda>a. upd a (map_default d g a)"
504 let ?fr = "\<lambda>A. Finite_Set.fold ?upd (cnst d) A"
505 interpret gwf: comp_fun_commute "?upd" by(rule upd_left_comm)
507 from fin anf fg show ?thesis
508 proof(induct "dom f" arbitrary: f)
510 from \<open>{} = dom f\<close> have "f = empty" by(auto simp add: dom_def)
511 thus ?case by(auto simp add: finfun_const_def finfun_update_def upd_upd_twice)
514 note IH = \<open>\<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))\<close>
515 note fin = \<open>finite A\<close> note anf = \<open>a \<notin> dom f\<close> note a'nA = \<open>a' \<notin> A\<close>
516 note domf = \<open>insert a' A = dom f\<close> note fg = \<open>f \<subseteq>\<^sub>m g\<close>
518 from domf obtain b where b: "f a' = Some b" by auto
519 let ?f' = "f(a' := None)"
520 let ?b' = "case f a' of None \<Rightarrow> d | Some b \<Rightarrow> b"
521 from domf have "upd a d'' (upd a d' (?fr (dom f))) = upd a d'' (upd a d' (?fr (insert a' A)))" by simp
522 also note gwf.fold_insert[OF fin a'nA]
523 also from b fg have "g a' = f a'" by(auto simp add: map_le_def intro: domI dest: bspec)
524 hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def)
525 also from anf domf have ana': "a \<noteq> a'" by auto note upd_commute[OF this]
526 also note upd_commute[OF ana']
527 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)
528 note A also note IH[OF A \<open>a \<notin> dom ?f'\<close> \<open>?f' \<subseteq>\<^sub>m g\<close>]
529 also note upd_commute[OF ana'[symmetric]] also note ga'[symmetric] also note A[symmetric]
530 also note gwf.fold_insert[symmetric, OF fin a'nA] also note domf
535 lemma map_default_eq_id [simp]: "map_default d ((\<lambda>a. Some (f a)) |` {a. f a \<noteq> d}) = f"
536 by(auto simp add: map_default_def restrict_map_def)
538 lemma finite_rec_cong1:
539 assumes f: "comp_fun_commute f" and g: "comp_fun_commute g"
541 and eq: "\<And>a. a \<in> A \<Longrightarrow> f a = g a"
542 shows "Finite_Set.fold f z A = Finite_Set.fold g z A"
544 interpret f: comp_fun_commute f by(rule f)
545 interpret g: comp_fun_commute g by(rule g)
547 assume BsubA: "B \<subseteq> A"
548 with fin have "finite B" by(blast intro: finite_subset)
549 hence "B \<subseteq> A \<Longrightarrow> Finite_Set.fold f z B = Finite_Set.fold g z B"
551 case empty thus ?case by simp
554 note finB = \<open>finite B\<close> note anB = \<open>a \<notin> B\<close> note sub = \<open>insert a B \<subseteq> A\<close>
555 note IH = \<open>B \<subseteq> A \<Longrightarrow> Finite_Set.fold f z B = Finite_Set.fold g z B\<close>
556 from sub anB have BpsubA: "B \<subset> A" and BsubA: "B \<subseteq> A" and aA: "a \<in> A" by auto
557 from IH[OF BsubA] eq[OF aA] finB anB
560 with BsubA have "Finite_Set.fold f z B = Finite_Set.fold g z B" by blast }
561 thus ?thesis by blast
564 lemma finfun_rec_upd [simp]:
565 "finfun_rec cnst upd (f(a' $:= b')) = upd a' b' (finfun_rec cnst upd f)"
568 obtain b where b: "b = finfun_default f" by auto
569 let ?the = "\<lambda>f g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g"
570 obtain g where g: "g = The (?the f)" by blast
571 obtain y where f: "f = Abs_finfun y" and y: "y \<in> finfun" by (cases f)
572 from f y b have bfin: "finite {a. y a \<noteq> b}" by(simp add: finfun_default_def finite_finfun_default_aux)
574 let ?g = "(\<lambda>a. Some (y a)) |` {a. y a \<noteq> b}"
575 from bfin have fing: "finite (dom ?g)" by auto
576 have bran: "b \<notin> ran ?g" by(auto simp add: ran_def restrict_map_def)
577 have yg: "y = map_default b ?g" by simp
578 have gg: "g = ?g" unfolding g
579 proof(rule the_equality)
580 from f y bfin show "?the f ?g"
581 by(auto)(simp add: restrict_map_def ran_def split: split_if_asm)
585 hence fin': "finite (dom g')" and ran': "b \<notin> ran g'"
586 and eq: "Abs_finfun (map_default b ?g) = Abs_finfun (map_default b g')" using f yg by auto
587 from fin' fing have "map_default b ?g \<in> finfun" "map_default b g' \<in> finfun" by(blast intro: map_default_in_finfun)+
588 with eq have "map_default b ?g = map_default b g'" by simp
589 with fing bran fin' ran' show "g' = ?g" by(rule map_default_inject[OF disjI2[OF refl], THEN sym])
593 proof(cases "b' = b")
597 let ?g' = "(\<lambda>a. Some ((y(a' := b)) a)) |` {a. (y(a' := b)) a \<noteq> b}"
598 from bfin b'b have fing': "finite (dom ?g')"
599 by(auto simp add: Collect_conj_eq Collect_imp_eq intro: finite_subset)
600 have brang': "b \<notin> ran ?g'" by(auto simp add: ran_def restrict_map_def)
602 let ?b' = "\<lambda>a. case ?g' a of None \<Rightarrow> b | Some b \<Rightarrow> b"
603 let ?b = "map_default b ?g"
604 from upd_left_comm upd_left_comm fing'
605 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')"
606 by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b b map_default_def)
607 also interpret gwf: comp_fun_commute "\<lambda>a. upd a (?b a)" by(rule upd_left_comm)
608 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))"
609 proof(cases "y a' = b")
611 with b'b have g': "?g' = ?g" by(auto simp add: restrict_map_def)
612 from True have a'ndomg: "a' \<notin> dom ?g" by auto
613 from f b'b b show ?thesis unfolding g'
614 by(subst map_default_update_const[OF fing a'ndomg map_le_refl, symmetric]) simp
617 hence domg: "dom ?g = insert a' (dom ?g')" by auto
618 from False b'b have a'ndomg': "a' \<notin> dom ?g'" by auto
619 have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g')) =
620 upd a' (?b a') (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'))"
621 using fing' a'ndomg' unfolding b'b by(rule gwf.fold_insert)
622 hence "upd a' b (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g'))) =
623 upd a' b (upd a' (?b a') (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g')))" by simp
624 also from b'b have g'leg: "?g' \<subseteq>\<^sub>m ?g" by(auto simp add: restrict_map_def map_le_def)
625 note map_default_update_twice[OF fing' a'ndomg' this, of b "?b a'" b]
626 also note map_default_update_const[OF fing' a'ndomg' g'leg, of b]
627 finally show ?thesis unfolding b'b domg[unfolded b'b] by(rule sym)
629 also have "The (?the (f(a' $:= b'))) = ?g'"
630 proof(rule the_equality)
631 from f y b b'b brang' fing' show "?the (f(a' $:= b')) ?g'"
632 by(auto simp del: fun_upd_apply simp add: finfun_update_def)
635 assume "?the (f(a' $:= b')) g'"
636 hence fin': "finite (dom g')" and ran': "b \<notin> ran g'"
637 and eq: "f(a' $:= b') = Abs_finfun (map_default b g')"
638 by(auto simp del: fun_upd_apply)
639 from fin' fing' have "map_default b g' \<in> finfun" "map_default b ?g' \<in> finfun"
640 by(blast intro: map_default_in_finfun)+
641 with eq f b'b b have "map_default b ?g' = map_default b g'"
642 by(simp del: fun_upd_apply add: finfun_update_def)
643 with fing' brang' fin' ran' show "g' = ?g'"
644 by(rule map_default_inject[OF disjI2[OF refl], THEN sym])
646 ultimately show ?thesis unfolding finfun_rec_def Let_def b gg[unfolded g b] using bfin b'b b
647 by(simp only: finfun_default_update_const map_default_def)
651 let ?g' = "?g(a' \<mapsto> b')"
652 let ?b' = "map_default b ?g'"
653 let ?b = "map_default b ?g"
654 from fing have fing': "finite (dom ?g')" by auto
655 from bran b'b have bnrang': "b \<notin> ran ?g'" by(auto simp add: ran_def)
656 have ffmg': "map_default b ?g' = y(a' := b')" by(auto simp add: map_default_def restrict_map_def)
657 with f y have f_Abs: "f(a' $:= b') = Abs_finfun (map_default b ?g')" by(auto simp add: finfun_update_def)
658 have g': "The (?the (f(a' $:= b'))) = ?g'"
659 proof (rule the_equality)
660 from fing' bnrang' f_Abs show "?the (f(a' $:= b')) ?g'"
661 by(auto simp add: finfun_update_def restrict_map_def)
663 fix g' assume "?the (f(a' $:= b')) g'"
664 hence f': "f(a' $:= b') = Abs_finfun (map_default b g')"
665 and fin': "finite (dom g')" and brang': "b \<notin> ran g'" by auto
666 from fing' fin' have "map_default b ?g' \<in> finfun" "map_default b g' \<in> finfun"
667 by(auto intro: map_default_in_finfun)
668 with f' f_Abs have "map_default b g' = map_default b ?g'" by simp
669 with fin' brang' fing' bnrang' show "g' = ?g'"
670 by(rule map_default_inject[OF disjI2[OF refl]])
672 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}))"
675 proof(cases "y a' = b")
677 hence a'ndomg: "a' \<notin> dom ?g" by auto
678 from f y b'b True have yff: "y = map_default b (?g' |` dom ?g)"
679 by(auto simp add: restrict_map_def map_default_def intro!: ext)
680 hence f': "f = Abs_finfun (map_default b (?g' |` dom ?g))" using f by simp
681 interpret g'wf: comp_fun_commute "\<lambda>a. upd a (?b' a)" by(rule upd_left_comm)
682 from upd_left_comm upd_left_comm fing
683 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)"
684 by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b True map_default_def)
685 thus ?thesis unfolding finfun_rec_def Let_def finfun_default_update_const b[symmetric]
686 unfolding g' g[symmetric] gg g'wf.fold_insert[OF fing a'ndomg, of "cnst b", folded dom]
687 by -(rule arg_cong2[where f="upd a'"], simp_all add: map_default_def)
690 hence "insert a' (dom ?g) = dom ?g" by auto
692 let ?g'' = "?g(a' := None)"
693 let ?b'' = "map_default b ?g''"
694 from False have domg: "dom ?g = insert a' (dom ?g'')" by auto
695 from False have a'ndomg'': "a' \<notin> dom ?g''" by auto
696 have fing'': "finite (dom ?g'')" by(rule finite_subset[OF _ fing]) auto
697 have bnrang'': "b \<notin> ran ?g''" by(auto simp add: ran_def restrict_map_def)
698 interpret gwf: comp_fun_commute "\<lambda>a. upd a (?b a)" by(rule upd_left_comm)
699 interpret g'wf: comp_fun_commute "\<lambda>a. upd a (?b' a)" by(rule upd_left_comm)
700 have "upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g''))) =
701 upd a' b' (upd a' (?b a') (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')))"
702 unfolding gwf.fold_insert[OF fing'' a'ndomg''] f ..
703 also have g''leg: "?g |` dom ?g'' \<subseteq>\<^sub>m ?g" by(auto simp add: map_le_def)
704 have "dom (?g |` dom ?g'') = dom ?g''" by auto
705 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",
706 unfolded this, OF fing'' a'ndomg'' g''leg]
707 also have b': "b' = ?b' a'" by(auto simp add: map_default_def)
708 from upd_left_comm upd_left_comm fing''
709 have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'') =
710 Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g'')"
711 by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b map_default_def)
712 with b' have "upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')) =
713 upd a' (?b' a') (Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g''))" by simp
714 also note g'wf.fold_insert[OF fing'' a'ndomg'', symmetric]
715 finally have "upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g)) =
716 Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g)"
718 ultimately have "Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (insert a' (dom ?g)) =
719 upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g))" by simp
720 thus ?thesis unfolding finfun_rec_def Let_def finfun_default_update_const b[symmetric] g[symmetric] g' dom[symmetric]
721 using b'b gg by(simp add: map_default_insert)
728 locale finfun_rec_wf = finfun_rec_wf_aux +
729 assumes const_update_all:
730 "finite (UNIV :: 'a set) \<Longrightarrow> Finite_Set.fold (\<lambda>a. upd a b') (cnst b) (UNIV :: 'a set) = cnst b'"
733 lemma finfun_rec_const [simp]: includes finfun shows
734 "finfun_rec cnst upd (K$ c) = cnst c"
735 proof(cases "finite (UNIV :: 'a set)")
737 hence "finfun_default ((K$ c) :: 'a \<Rightarrow>f 'b) = c" by(simp add: finfun_default_const)
738 moreover have "(THE g :: 'a \<rightharpoonup> 'b. (K$ c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g) = empty"
739 proof (rule the_equality)
740 show "(K$ c) = Abs_finfun (map_default c empty) \<and> finite (dom empty) \<and> c \<notin> ran empty"
741 by(auto simp add: finfun_const_def)
743 fix g :: "'a \<rightharpoonup> 'b"
744 assume "(K$ c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g"
745 hence g: "(K$ c) = Abs_finfun (map_default c g)" and fin: "finite (dom g)" and ran: "c \<notin> ran g" by blast+
746 from g map_default_in_finfun[OF fin, of c] have "map_default c g = (\<lambda>a. c)"
747 by(simp add: finfun_const_def)
748 moreover have "map_default c empty = (\<lambda>a. c)" by simp
749 ultimately show "g = empty" by-(rule map_default_inject[OF disjI2[OF refl] fin ran], auto)
751 ultimately show ?thesis by(simp add: finfun_rec_def)
754 hence default: "finfun_default ((K$ c) :: 'a \<Rightarrow>f 'b) = undefined" by(simp add: finfun_default_const)
755 let ?the = "\<lambda>g :: 'a \<rightharpoonup> 'b. (K$ c) = Abs_finfun (map_default undefined g) \<and> finite (dom g) \<and> undefined \<notin> ran g"
757 proof(cases "c = undefined")
759 have the: "The ?the = empty"
760 proof (rule the_equality)
761 from True show "?the empty" by(auto simp add: finfun_const_def)
765 hence fg: "(K$ c) = Abs_finfun (map_default undefined g')"
766 and fin: "finite (dom g')" and g: "undefined \<notin> ran g'" by simp_all
767 from fin have "map_default undefined g' \<in> finfun" by(rule map_default_in_finfun)
768 with fg have "map_default undefined g' = (\<lambda>a. c)"
769 by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1, symmetric])
770 with True show "g' = empty"
771 by -(rule map_default_inject(2)[OF _ fin g], auto)
773 show ?thesis unfolding finfun_rec_def using \<open>finite UNIV\<close> True
774 unfolding Let_def the default by(simp)
777 have the: "The ?the = (\<lambda>a :: 'a. Some c)"
778 proof (rule the_equality)
779 from False True show "?the (\<lambda>a :: 'a. Some c)"
780 by(auto simp add: map_default_def [abs_def] finfun_const_def dom_def ran_def)
782 fix g' :: "'a \<rightharpoonup> 'b"
784 hence fg: "(K$ c) = Abs_finfun (map_default undefined g')"
785 and fin: "finite (dom g')" and g: "undefined \<notin> ran g'" by simp_all
786 from fin have "map_default undefined g' \<in> finfun" by(rule map_default_in_finfun)
787 with fg have "map_default undefined g' = (\<lambda>a. c)"
788 by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1])
789 with True False show "g' = (\<lambda>a::'a. Some c)"
790 by - (rule map_default_inject(2)[OF _ fin g],
791 auto simp add: dom_def ran_def map_default_def [abs_def])
793 show ?thesis unfolding finfun_rec_def using True False
794 unfolding Let_def the default by(simp add: dom_def map_default_def const_update_all)
800 subsection \<open>Weak induction rule and case analysis for FinFuns\<close>
802 lemma finfun_weak_induct [consumes 0, case_names const update]:
803 assumes const: "\<And>b. P (K$ b)"
804 and update: "\<And>f a b. P f \<Longrightarrow> P (f(a $:= b))"
807 proof(induct x rule: Abs_finfun_induct)
809 then obtain b where "finite {a. y a \<noteq> b}" unfolding finfun_def by blast
810 thus ?case using \<open>y \<in> finfun\<close>
811 proof(induct "{a. y a \<noteq> b}" arbitrary: y rule: finite_induct)
813 hence "\<And>a. y a = b" by blast
814 hence "y = (\<lambda>a. b)" by(auto)
815 hence "Abs_finfun y = finfun_const b" unfolding finfun_const_def by simp
816 thus ?case by(simp add: const)
819 note IH = \<open>\<And>y. \<lbrakk> A = {a. y a \<noteq> b}; y \<in> finfun \<rbrakk> \<Longrightarrow> P (Abs_finfun y)\<close>
820 note y = \<open>y \<in> finfun\<close>
821 with \<open>insert a A = {a. y a \<noteq> b}\<close> \<open>a \<notin> A\<close>
822 have "A = {a'. (y(a := b)) a' \<noteq> b}" "y(a := b) \<in> finfun" by auto
823 from IH[OF this] have "P (finfun_update (Abs_finfun (y(a := b))) a (y a))" by(rule update)
824 thus ?case using y unfolding finfun_update_def by simp
828 lemma finfun_exhaust_disj: "(\<exists>b. x = finfun_const b) \<or> (\<exists>f a b. x = finfun_update f a b)"
829 by(induct x rule: finfun_weak_induct) blast+
831 lemma finfun_exhaust:
832 obtains b where "x = (K$ b)"
833 | f a b where "x = f(a $:= b)"
834 by(atomize_elim)(rule finfun_exhaust_disj)
836 lemma finfun_rec_unique:
837 fixes f :: "'a \<Rightarrow>f 'b \<Rightarrow> 'c"
838 assumes c: "\<And>c. f (K$ c) = cnst c"
839 and u: "\<And>g a b. f (g(a $:= b)) = upd g a b (f g)"
840 and c': "\<And>c. f' (K$ c) = cnst c"
841 and u': "\<And>g a b. f' (g(a $:= b)) = upd g a b (f' g)"
844 fix g :: "'a \<Rightarrow>f 'b"
846 by(induct g rule: finfun_weak_induct)(auto simp add: c u c' u')
850 subsection \<open>Function application\<close>
852 notation finfun_apply (infixl "$" 999)
854 interpretation finfun_apply_aux: finfun_rec_wf_aux "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c"
855 by(unfold_locales) auto
857 interpretation finfun_apply: finfun_rec_wf "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c"
858 proof(unfold_locales)
860 assume fin: "finite (UNIV :: 'b set)"
862 interpret comp_fun_commute "\<lambda>a'. If (a = a') b'" by(rule finfun_apply_aux.upd_left_comm)
863 from fin have "finite A" by(auto intro: finite_subset)
864 hence "Finite_Set.fold (\<lambda>a'. If (a = a') b') b A = (if a \<in> A then b' else b)"
866 from this[of UNIV] show "Finite_Set.fold (\<lambda>a'. If (a = a') b') b UNIV = b'" by simp
869 lemma finfun_apply_def: "op $ = (\<lambda>f a. finfun_rec (\<lambda>b. b) (\<lambda>a' b c. if (a = a') then b else c) f)"
870 proof(rule finfun_rec_unique)
871 fix c show "op $ (K$ c) = (\<lambda>a. c)" by(simp add: finfun_const.rep_eq)
873 fix g a b show "op $ g(a $:= b) = (\<lambda>c. if c = a then b else g $ c)"
874 by(auto simp add: finfun_update_def fun_upd_finfun Abs_finfun_inverse finfun_apply)
877 lemma finfun_upd_apply: "f(a $:= b) $ a' = (if a = a' then b else f $ a')"
878 and finfun_upd_apply_code [code]: "(finfun_update_code f a b) $ a' = (if a = a' then b else f $ a')"
879 by(simp_all add: finfun_apply_def)
881 lemma finfun_const_apply [simp, code]: "(K$ b) $ a = b"
882 by(simp add: finfun_apply_def)
884 lemma finfun_upd_apply_same [simp]:
886 by(simp add: finfun_upd_apply)
888 lemma finfun_upd_apply_other [simp]:
889 "a \<noteq> a' \<Longrightarrow> f(a $:= b) $ a' = f $ a'"
890 by(simp add: finfun_upd_apply)
892 lemma finfun_ext: "(\<And>a. f $ a = g $ a) \<Longrightarrow> f = g"
893 by(auto simp add: finfun_apply_inject[symmetric])
895 lemma expand_finfun_eq: "(f = g) = (op $ f = op $ g)"
896 by(auto intro: finfun_ext)
898 lemma finfun_upd_triv [simp]: "f(x $:= f $ x) = f"
899 by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
901 lemma finfun_const_inject [simp]: "(K$ b) = (K$ b') \<equiv> b = b'"
902 by(simp add: expand_finfun_eq fun_eq_iff)
904 lemma finfun_const_eq_update:
905 "((K$ b) = f(a $:= b')) = (b = b' \<and> (\<forall>a'. a \<noteq> a' \<longrightarrow> f $ a' = b))"
906 by(auto simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
908 subsection \<open>Function composition\<close>
910 definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>f 'a \<Rightarrow> 'c \<Rightarrow>f 'b" (infixr "o$" 55)
911 where [code del]: "g o$ f = finfun_rec (\<lambda>b. (K$ g b)) (\<lambda>a b c. c(a $:= g b)) f"
913 notation (xsymbols) finfun_comp (infixr "\<circ>$" 55)
915 interpretation finfun_comp_aux: finfun_rec_wf_aux "(\<lambda>b. (K$ g b))" "(\<lambda>a b c. c(a $:= g b))"
916 by(unfold_locales)(auto simp add: finfun_upd_apply intro: finfun_ext)
918 interpretation finfun_comp: finfun_rec_wf "(\<lambda>b. (K$ g b))" "(\<lambda>a b c. c(a $:= g b))"
921 assume fin: "finite (UNIV :: 'c set)"
923 from fin have "finite A" by(auto intro: finite_subset)
924 hence "Finite_Set.fold (\<lambda>(a :: 'c) c. c(a $:= g b')) (K$ g b) A =
925 Abs_finfun (\<lambda>a. if a \<in> A then g b' else g b)"
926 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) }
927 from this[of UNIV] show "Finite_Set.fold (\<lambda>(a :: 'c) c. c(a $:= g b')) (K$ g b) UNIV = (K$ g b')"
928 by(simp add: finfun_const_def)
931 lemma finfun_comp_const [simp, code]:
932 "g \<circ>$ (K$ c) = (K$ g c)"
933 by(simp add: finfun_comp_def)
935 lemma finfun_comp_update [simp]: "g \<circ>$ (f(a $:= b)) = (g \<circ>$ f)(a $:= g b)"
936 and finfun_comp_update_code [code]:
937 "g \<circ>$ (finfun_update_code f a b) = finfun_update_code (g \<circ>$ f) a (g b)"
938 by(simp_all add: finfun_comp_def)
940 lemma finfun_comp_apply [simp]:
941 "op $ (g \<circ>$ f) = g \<circ> op $ f"
942 by(induct f rule: finfun_weak_induct)(auto simp add: finfun_upd_apply)
944 lemma finfun_comp_comp_collapse [simp]: "f \<circ>$ g \<circ>$ h = (f \<circ> g) \<circ>$ h"
945 by(induct h rule: finfun_weak_induct) simp_all
947 lemma finfun_comp_const1 [simp]: "(\<lambda>x. c) \<circ>$ f = (K$ c)"
948 by(induct f rule: finfun_weak_induct)(auto intro: finfun_ext simp add: finfun_upd_apply)
950 lemma finfun_comp_id1 [simp]: "(\<lambda>x. x) \<circ>$ f = f" "id \<circ>$ f = f"
951 by(induct f rule: finfun_weak_induct) auto
953 lemma finfun_comp_conv_comp: "g \<circ>$ f = Abs_finfun (g \<circ> op $ f)"
956 have "(\<lambda>f. g \<circ>$ f) = (\<lambda>f. Abs_finfun (g \<circ> op $ f))"
957 proof(rule finfun_rec_unique)
958 { fix c show "Abs_finfun (g \<circ> op $ (K$ c)) = (K$ g c)"
959 by(simp add: finfun_comp_def o_def)(simp add: finfun_const_def) }
960 { fix g' a b show "Abs_finfun (g \<circ> op $ g'(a $:= b)) = (Abs_finfun (g \<circ> op $ g'))(a $:= g b)"
962 obtain y where y: "y \<in> finfun" and g': "g' = Abs_finfun y" by(cases g')
963 moreover from g' have "(g \<circ> op $ g') \<in> finfun" by(simp add: finfun_left_compose)
964 moreover have "g \<circ> y(a := b) = (g \<circ> y)(a := g b)" by(auto)
965 ultimately show ?thesis by(simp add: finfun_comp_def finfun_update_def)
968 thus ?thesis by(auto simp add: fun_eq_iff)
971 definition finfun_comp2 :: "'b \<Rightarrow>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>f 'c" (infixr "$o" 55)
972 where [code del]: "g $o f = Abs_finfun (op $ g \<circ> f)"
974 notation (xsymbol) finfun_comp2 (infixr "$\<circ>" 55)
976 lemma finfun_comp2_const [code, simp]: "finfun_comp2 (K$ c) f = (K$ c)"
978 by(simp add: finfun_comp2_def finfun_const_def comp_def)
980 lemma finfun_comp2_update:
983 shows "finfun_comp2 (g(b $:= c)) f = (if b \<in> range f then (finfun_comp2 g f)(inv f b $:= c) else finfun_comp2 g f)"
984 proof(cases "b \<in> range f")
986 from inj have "\<And>x. (op $ g)(f x := c) \<circ> f = (op $ g \<circ> f)(x := c)" by(auto intro!: ext dest: injD)
987 with inj True show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def finfun_right_compose)
990 hence "(op $ g)(b := c) \<circ> f = op $ g \<circ> f" by(auto simp add: fun_eq_iff)
991 with False show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def)
994 subsection \<open>Universal quantification\<close>
996 definition finfun_All_except :: "'a list \<Rightarrow> 'a \<Rightarrow>f bool \<Rightarrow> bool"
997 where [code del]: "finfun_All_except A P \<equiv> \<forall>a. a \<in> set A \<or> P $ a"
999 lemma finfun_All_except_const: "finfun_All_except A (K$ b) \<longleftrightarrow> b \<or> set A = UNIV"
1000 by(auto simp add: finfun_All_except_def)
1002 lemma finfun_All_except_const_finfun_UNIV_code [code]:
1003 "finfun_All_except A (K$ b) = (b \<or> is_list_UNIV A)"
1004 by(simp add: finfun_All_except_const is_list_UNIV_iff)
1006 lemma finfun_All_except_update:
1007 "finfun_All_except A f(a $:= b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
1008 by(fastforce simp add: finfun_All_except_def finfun_upd_apply)
1010 lemma finfun_All_except_update_code [code]:
1011 fixes a :: "'a :: card_UNIV"
1012 shows "finfun_All_except A (finfun_update_code f a b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
1013 by(simp add: finfun_All_except_update)
1015 definition finfun_All :: "'a \<Rightarrow>f bool \<Rightarrow> bool"
1016 where "finfun_All = finfun_All_except []"
1018 lemma finfun_All_const [simp]: "finfun_All (K$ b) = b"
1019 by(simp add: finfun_All_def finfun_All_except_def)
1021 lemma finfun_All_update: "finfun_All f(a $:= b) = (b \<and> finfun_All_except [a] f)"
1022 by(simp add: finfun_All_def finfun_All_except_update)
1024 lemma finfun_All_All: "finfun_All P = All (op $ P)"
1025 by(simp add: finfun_All_def finfun_All_except_def)
1028 definition finfun_Ex :: "'a \<Rightarrow>f bool \<Rightarrow> bool"
1029 where "finfun_Ex P = Not (finfun_All (Not \<circ>$ P))"
1031 lemma finfun_Ex_Ex: "finfun_Ex P = Ex (op $ P)"
1032 unfolding finfun_Ex_def finfun_All_All by simp
1034 lemma finfun_Ex_const [simp]: "finfun_Ex (K$ b) = b"
1035 by(simp add: finfun_Ex_def)
1038 subsection \<open>A diagonal operator for FinFuns\<close>
1040 definition finfun_Diag :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow>f 'c \<Rightarrow> 'a \<Rightarrow>f ('b \<times> 'c)" ("(1'($_,/ _$'))" [0, 0] 1000)
1041 where [code del]: "($f, g$) = finfun_rec (\<lambda>b. Pair b \<circ>$ g) (\<lambda>a b c. c(a $:= (b, g $ a))) f"
1043 interpretation finfun_Diag_aux: finfun_rec_wf_aux "\<lambda>b. Pair b \<circ>$ g" "\<lambda>a b c. c(a $:= (b, g $ a))"
1044 by(unfold_locales)(simp_all add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
1046 interpretation finfun_Diag: finfun_rec_wf "\<lambda>b. Pair b \<circ>$ g" "\<lambda>a b c. c(a $:= (b, g $ a))"
1049 assume fin: "finite (UNIV :: 'c set)"
1051 interpret comp_fun_commute "\<lambda>a c. c(a $:= (b', g $ a))" by(rule finfun_Diag_aux.upd_left_comm)
1052 from fin have "finite A" by(auto intro: finite_subset)
1053 hence "Finite_Set.fold (\<lambda>a c. c(a $:= (b', g $ a))) (Pair b \<circ>$ g) A =
1054 Abs_finfun (\<lambda>a. (if a \<in> A then b' else b, g $ a))"
1055 by(induct)(simp_all add: finfun_const_def finfun_comp_conv_comp o_def,
1056 auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite fun_eq_iff fin) }
1057 from this[of UNIV] show "Finite_Set.fold (\<lambda>a c. c(a $:= (b', g $ a))) (Pair b \<circ>$ g) UNIV = Pair b' \<circ>$ g"
1058 by(simp add: finfun_const_def finfun_comp_conv_comp o_def)
1061 lemma finfun_Diag_const1: "($K$ b, g$) = Pair b \<circ>$ g"
1062 by(simp add: finfun_Diag_def)
1065 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 @{term "op \<circ>$"}.
1068 lemma finfun_Diag_const_code [code]:
1069 "($K$ b, K$ c$) = (K$ (b, c))"
1070 "($K$ b, finfun_update_code g a c$) = finfun_update_code ($K$ b, g$) a (b, c)"
1071 by(simp_all add: finfun_Diag_const1)
1073 lemma finfun_Diag_update1: "($f(a $:= b), g$) = ($f, g$)(a $:= (b, g $ a))"
1074 and finfun_Diag_update1_code [code]: "($finfun_update_code f a b, g$) = ($f, g$)(a $:= (b, g $ a))"
1075 by(simp_all add: finfun_Diag_def)
1077 lemma finfun_Diag_const2: "($f, K$ c$) = (\<lambda>b. (b, c)) \<circ>$ f"
1078 by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
1080 lemma finfun_Diag_update2: "($f, g(a $:= c)$) = ($f, g$)(a $:= (f $ a, c))"
1081 by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
1083 lemma finfun_Diag_const_const [simp]: "($K$ b, K$ c$) = (K$ (b, c))"
1084 by(simp add: finfun_Diag_const1)
1086 lemma finfun_Diag_const_update:
1087 "($K$ b, g(a $:= c)$) = ($K$ b, g$)(a $:= (b, c))"
1088 by(simp add: finfun_Diag_const1)
1090 lemma finfun_Diag_update_const:
1091 "($f(a $:= b), K$ c$) = ($f, K$ c$)(a $:= (b, c))"
1092 by(simp add: finfun_Diag_def)
1094 lemma finfun_Diag_update_update:
1095 "($f(a $:= b), g(a' $:= c)$) = (if a = a' then ($f, g$)(a $:= (b, c)) else ($f, g$)(a $:= (b, g $ a))(a' $:= (f $ a', c)))"
1096 by(auto simp add: finfun_Diag_update1 finfun_Diag_update2)
1098 lemma finfun_Diag_apply [simp]: "op $ ($f, g$) = (\<lambda>x. (f $ x, g $ x))"
1099 by(induct f rule: finfun_weak_induct)(auto simp add: finfun_Diag_const1 finfun_Diag_update1 finfun_upd_apply)
1101 lemma finfun_Diag_conv_Abs_finfun:
1102 "($f, g$) = Abs_finfun ((\<lambda>x. (f $ x, g $ x)))"
1105 have "(\<lambda>f :: 'a \<Rightarrow>f 'b. ($f, g$)) = (\<lambda>f. Abs_finfun ((\<lambda>x. (f $ x, g $ x))))"
1106 proof(rule finfun_rec_unique)
1107 { fix c show "Abs_finfun (\<lambda>x. ((K$ c) $ x, g $ x)) = Pair c \<circ>$ g"
1108 by(simp add: finfun_comp_conv_comp o_def finfun_const_def) }
1110 show "Abs_finfun (\<lambda>x. (g'(a $:= b) $ x, g $ x)) =
1111 (Abs_finfun (\<lambda>x. (g' $ x, g $ x)))(a $:= (b, g $ a))"
1112 by(auto simp add: finfun_update_def fun_eq_iff simp del: fun_upd_apply) simp }
1113 qed(simp_all add: finfun_Diag_const1 finfun_Diag_update1)
1114 thus ?thesis by(auto simp add: fun_eq_iff)
1117 lemma finfun_Diag_eq: "($f, g$) = ($f', g'$) \<longleftrightarrow> f = f' \<and> g = g'"
1118 by(auto simp add: expand_finfun_eq fun_eq_iff)
1120 definition finfun_fst :: "'a \<Rightarrow>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>f 'b"
1121 where [code]: "finfun_fst f = fst \<circ>$ f"
1123 lemma finfun_fst_const: "finfun_fst (K$ bc) = (K$ fst bc)"
1124 by(simp add: finfun_fst_def)
1126 lemma finfun_fst_update: "finfun_fst (f(a $:= bc)) = (finfun_fst f)(a $:= fst bc)"
1127 and finfun_fst_update_code: "finfun_fst (finfun_update_code f a bc) = (finfun_fst f)(a $:= fst bc)"
1128 by(simp_all add: finfun_fst_def)
1130 lemma finfun_fst_comp_conv: "finfun_fst (f \<circ>$ g) = (fst \<circ> f) \<circ>$ g"
1131 by(simp add: finfun_fst_def)
1133 lemma finfun_fst_conv [simp]: "finfun_fst ($f, g$) = f"
1134 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)
1136 lemma finfun_fst_conv_Abs_finfun: "finfun_fst = (\<lambda>f. Abs_finfun (fst \<circ> op $ f))"
1137 by(simp add: finfun_fst_def [abs_def] finfun_comp_conv_comp)
1140 definition finfun_snd :: "'a \<Rightarrow>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>f 'c"
1141 where [code]: "finfun_snd f = snd \<circ>$ f"
1143 lemma finfun_snd_const: "finfun_snd (K$ bc) = (K$ snd bc)"
1144 by(simp add: finfun_snd_def)
1146 lemma finfun_snd_update: "finfun_snd (f(a $:= bc)) = (finfun_snd f)(a $:= snd bc)"
1147 and finfun_snd_update_code [code]: "finfun_snd (finfun_update_code f a bc) = (finfun_snd f)(a $:= snd bc)"
1148 by(simp_all add: finfun_snd_def)
1150 lemma finfun_snd_comp_conv: "finfun_snd (f \<circ>$ g) = (snd \<circ> f) \<circ>$ g"
1151 by(simp add: finfun_snd_def)
1153 lemma finfun_snd_conv [simp]: "finfun_snd ($f, g$) = g"
1154 apply(induct f rule: finfun_weak_induct)
1155 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)
1158 lemma finfun_snd_conv_Abs_finfun: "finfun_snd = (\<lambda>f. Abs_finfun (snd \<circ> op $ f))"
1159 by(simp add: finfun_snd_def [abs_def] finfun_comp_conv_comp)
1161 lemma finfun_Diag_collapse [simp]: "($finfun_fst f, finfun_snd f$) = f"
1162 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)
1164 subsection \<open>Currying for FinFuns\<close>
1166 definition finfun_curry :: "('a \<times> 'b) \<Rightarrow>f 'c \<Rightarrow> 'a \<Rightarrow>f 'b \<Rightarrow>f 'c"
1167 where [code del]: "finfun_curry = finfun_rec (finfun_const \<circ> finfun_const) (\<lambda>(a, b) c f. f(a $:= (f $ a)(b $:= c)))"
1169 interpretation finfun_curry_aux: finfun_rec_wf_aux "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(a $:= (f $ a)(b $:= c))"
1170 apply(unfold_locales)
1171 apply(auto simp add: split_def finfun_update_twist finfun_upd_apply split_paired_all finfun_update_const_same)
1174 interpretation finfun_curry: finfun_rec_wf "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(a $:= (f $ a)(b $:= c))"
1175 proof(unfold_locales)
1177 assume fin: "finite (UNIV :: ('c \<times> 'a) set)"
1178 hence fin1: "finite (UNIV :: 'c set)" and fin2: "finite (UNIV :: 'a set)"
1179 unfolding UNIV_Times_UNIV[symmetric]
1180 by(fastforce dest: finite_cartesian_productD1 finite_cartesian_productD2)+
1181 note [simp] = Abs_finfun_inverse_finite[OF fin] Abs_finfun_inverse_finite[OF fin1] Abs_finfun_inverse_finite[OF fin2]
1182 { fix A :: "('c \<times> 'a) set"
1183 interpret comp_fun_commute "\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(a $:= (f $ a)(b $:= c))) a b'"
1184 by(rule finfun_curry_aux.upd_left_comm)
1185 from fin have "finite A" by(auto intro: finite_subset)
1186 hence "Finite_Set.fold (\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(a $:= (f $ a)(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))"
1187 by induct (simp_all, auto simp add: finfun_update_def finfun_const_def split_def intro!: arg_cong[where f="Abs_finfun"] ext) }
1189 show "Finite_Set.fold (\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(a $:= (f $ a)(b $:= c))) a b') ((finfun_const \<circ> finfun_const) b) UNIV = (finfun_const \<circ> finfun_const) b'"
1190 by(simp add: finfun_const_def)
1193 lemma finfun_curry_const [simp, code]: "finfun_curry (K$ c) = (K$ K$ c)"
1194 by(simp add: finfun_curry_def)
1196 lemma finfun_curry_update [simp]:
1197 "finfun_curry (f((a, b) $:= c)) = (finfun_curry f)(a $:= (finfun_curry f $ a)(b $:= c))"
1198 and finfun_curry_update_code [code]:
1199 "finfun_curry (finfun_update_code f (a, b) c) = (finfun_curry f)(a $:= (finfun_curry f $ a)(b $:= c))"
1200 by(simp_all add: finfun_curry_def)
1202 lemma finfun_Abs_finfun_curry: assumes fin: "f \<in> finfun"
1203 shows "(\<lambda>a. Abs_finfun (curry f a)) \<in> finfun"
1206 from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast
1207 have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force)
1208 hence "{a. curry f a \<noteq> (\<lambda>x. c)} = fst ` {ab. f ab \<noteq> c}"
1209 by(auto simp add: curry_def fun_eq_iff)
1210 with fin c have "finite {a. Abs_finfun (curry f a) \<noteq> (K$ c)}"
1211 by(simp add: finfun_const_def finfun_curry)
1212 thus ?thesis unfolding finfun_def by auto
1215 lemma finfun_curry_conv_curry:
1216 fixes f :: "('a \<times> 'b) \<Rightarrow>f 'c"
1217 shows "finfun_curry f = Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply f) a))"
1220 have "finfun_curry = (\<lambda>f :: ('a \<times> 'b) \<Rightarrow>f 'c. Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply f) a)))"
1221 proof(rule finfun_rec_unique)
1222 fix c show "finfun_curry (K$ c) = (K$ K$ c)" by simp
1224 show "finfun_curry (f(a $:= c)) = (finfun_curry f)(fst a $:= (finfun_curry f $ (fst a))(snd a $:= c))"
1226 show "Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply (K$ c)) a)) = (K$ K$ c)"
1227 by(simp add: finfun_curry_def finfun_const_def curry_def)
1229 show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (op $ g(a $:= b)) aa)) =
1230 (Abs_finfun (\<lambda>a. Abs_finfun (curry (op $ g) a)))(
1231 fst a $:= ((Abs_finfun (\<lambda>a. Abs_finfun (curry (op $ g) a))) $ (fst a))(snd a $:= b))"
1232 by(cases a)(auto intro!: ext arg_cong[where f=Abs_finfun] simp add: finfun_curry_def finfun_update_def finfun_Abs_finfun_curry)
1234 thus ?thesis by(auto simp add: fun_eq_iff)
1237 subsection \<open>Executable equality for FinFuns\<close>
1239 lemma eq_finfun_All_ext: "(f = g) \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>$ ($f, g$))"
1240 by(simp add: expand_finfun_eq fun_eq_iff finfun_All_All o_def)
1242 instantiation finfun :: ("{card_UNIV,equal}",equal) equal begin
1243 definition eq_finfun_def [code]: "HOL.equal f g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>$ ($f, g$))"
1244 instance by(intro_classes)(simp add: eq_finfun_All_ext eq_finfun_def)
1248 "HOL.equal (f :: _ \<Rightarrow>f _) f \<longleftrightarrow> True"
1249 by (fact equal_refl)
1251 subsection \<open>An operator that explicitly removes all redundant updates in the generated representations\<close>
1253 definition finfun_clearjunk :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow>f 'b"
1254 where [simp, code del]: "finfun_clearjunk = id"
1256 lemma finfun_clearjunk_const [code]: "finfun_clearjunk (K$ b) = (K$ b)"
1259 lemma finfun_clearjunk_update [code]:
1260 "finfun_clearjunk (finfun_update_code f a b) = f(a $:= b)"
1263 subsection \<open>The domain of a FinFun as a FinFun\<close>
1265 definition finfun_dom :: "('a \<Rightarrow>f 'b) \<Rightarrow> ('a \<Rightarrow>f bool)"
1266 where [code del]: "finfun_dom f = Abs_finfun (\<lambda>a. f $ a \<noteq> finfun_default f)"
1268 lemma finfun_dom_const:
1269 "finfun_dom ((K$ c) :: 'a \<Rightarrow>f 'b) = (K$ finite (UNIV :: 'a set) \<and> c \<noteq> undefined)"
1270 unfolding finfun_dom_def finfun_default_const
1271 by(auto)(simp_all add: finfun_const_def)
1274 @{term "finfun_dom" } raises an exception when called on a FinFun whose domain is a finite type.
1275 For such FinFuns, the default value (and as such the domain) is undefined.
1278 lemma finfun_dom_const_code [code]:
1279 "finfun_dom ((K$ c) :: ('a :: card_UNIV) \<Rightarrow>f 'b) =
1280 (if CARD('a) = 0 then (K$ False) else Code.abort (STR ''finfun_dom called on finite type'') (\<lambda>_. finfun_dom (K$ c)))"
1281 by(simp add: finfun_dom_const card_UNIV card_eq_0_iff)
1283 lemma finfun_dom_finfunI: "(\<lambda>a. f $ a \<noteq> finfun_default f) \<in> finfun"
1284 using finite_finfun_default[of f]
1285 by(simp add: finfun_def exI[where x=False])
1287 lemma finfun_dom_update [simp]:
1288 "finfun_dom (f(a $:= b)) = (finfun_dom f)(a $:= (b \<noteq> finfun_default f))"
1289 including finfun unfolding finfun_dom_def finfun_update_def
1290 apply(simp add: finfun_default_update_const finfun_dom_finfunI)
1291 apply(fold finfun_update.rep_eq)
1292 apply(simp add: finfun_upd_apply fun_eq_iff fun_upd_def finfun_default_update_const)
1295 lemma finfun_dom_update_code [code]:
1296 "finfun_dom (finfun_update_code f a b) = finfun_update_code (finfun_dom f) a (b \<noteq> finfun_default f)"
1299 lemma finite_finfun_dom: "finite {x. finfun_dom f $ x}"
1300 proof(induct f rule: finfun_weak_induct)
1303 by (cases "finite (UNIV :: 'a set) \<and> b \<noteq> undefined")
1304 (auto simp add: finfun_dom_const UNIV_def [symmetric] Set.empty_def [symmetric])
1307 have "{x. finfun_dom f(a $:= b) $ x} =
1308 (if b = finfun_default f then {x. finfun_dom f $ x} - {a} else insert a {x. finfun_dom f $ x})"
1309 by (auto simp add: finfun_upd_apply split: split_if_asm)
1310 thus ?case using update by simp
1314 subsection \<open>The domain of a FinFun as a sorted list\<close>
1316 definition finfun_to_list :: "('a :: linorder) \<Rightarrow>f 'b \<Rightarrow> 'a list"
1318 "finfun_to_list f = (THE xs. set xs = {x. finfun_dom f $ x} \<and> sorted xs \<and> distinct xs)"
1320 lemma set_finfun_to_list [simp]: "set (finfun_to_list f) = {x. finfun_dom f $ x}" (is ?thesis1)
1321 and sorted_finfun_to_list: "sorted (finfun_to_list f)" (is ?thesis2)
1322 and distinct_finfun_to_list: "distinct (finfun_to_list f)" (is ?thesis3)
1323 proof (atomize (full))
1324 show "?thesis1 \<and> ?thesis2 \<and> ?thesis3"
1325 unfolding finfun_to_list_def
1326 by(rule theI')(rule finite_sorted_distinct_unique finite_finfun_dom)+
1329 lemma finfun_const_False_conv_bot: "op $ (K$ False) = bot"
1332 lemma finfun_const_True_conv_top: "op $ (K$ True) = top"
1335 lemma finfun_to_list_const:
1336 "finfun_to_list ((K$ c) :: ('a :: {linorder} \<Rightarrow>f 'b)) =
1337 (if \<not> finite (UNIV :: 'a set) \<or> c = undefined then [] else THE xs. set xs = UNIV \<and> sorted xs \<and> distinct xs)"
1338 by(auto simp add: finfun_to_list_def finfun_const_False_conv_bot finfun_const_True_conv_top finfun_dom_const)
1340 lemma finfun_to_list_const_code [code]:
1341 "finfun_to_list ((K$ c) :: ('a :: {linorder, card_UNIV} \<Rightarrow>f 'b)) =
1342 (if CARD('a) = 0 then [] else Code.abort (STR ''finfun_to_list called on finite type'') (\<lambda>_. finfun_to_list ((K$ c) :: ('a \<Rightarrow>f 'b))))"
1343 by(auto simp add: finfun_to_list_const card_UNIV card_eq_0_iff)
1345 lemma remove1_insort_insert_same:
1346 "x \<notin> set xs \<Longrightarrow> remove1 x (insort_insert x xs) = xs"
1347 by (metis insort_insert_insort remove1_insort)
1349 lemma finfun_dom_conv:
1350 "finfun_dom f $ x \<longleftrightarrow> f $ x \<noteq> finfun_default f"
1351 by(induct f rule: finfun_weak_induct)(auto simp add: finfun_dom_const finfun_default_const finfun_default_update_const finfun_upd_apply)
1353 lemma finfun_to_list_update:
1354 "finfun_to_list (f(a $:= b)) =
1355 (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
1356 proof(subst finfun_to_list_def, rule the_equality)
1358 assume "set xs = {x. finfun_dom f(a $:= b) $ x} \<and> sorted xs \<and> distinct xs"
1359 hence eq: "set xs = {x. finfun_dom f(a $:= b) $ x}"
1360 and [simp]: "sorted xs" "distinct xs" by simp_all
1361 show "xs = (if b = finfun_default f then remove1 a (finfun_to_list f) else insort_insert a (finfun_to_list f))"
1362 proof(cases "b = finfun_default f")
1365 proof(cases "finfun_dom f $ a")
1367 have "finfun_to_list f = insort_insert a xs"
1368 unfolding finfun_to_list_def
1369 proof(rule the_equality)
1370 have "set (insort_insert a xs) = insert a (set xs)" by(simp add: set_insort_insert)
1372 have "insert a {x. finfun_dom f(a $:= b) $ x} = {x. finfun_dom f $ x}" using True
1373 by(auto simp add: finfun_upd_apply split: split_if_asm)
1374 finally show 1: "set (insort_insert a xs) = {x. finfun_dom f $ x} \<and> sorted (insort_insert a xs) \<and> distinct (insort_insert a xs)"
1375 by(simp add: sorted_insort_insert distinct_insort_insert)
1378 assume "set xs' = {x. finfun_dom f $ x} \<and> sorted xs' \<and> distinct xs'"
1379 thus "xs' = insort_insert a xs" using 1 by(auto dest: sorted_distinct_set_unique)
1381 with eq True show ?thesis by(simp add: remove1_insort_insert_same)
1384 hence "f $ a = b" by(auto simp add: finfun_dom_conv)
1385 hence f: "f(a $:= b) = f" by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
1386 from eq have "finfun_to_list f = xs" unfolding f finfun_to_list_def
1387 by(auto elim: sorted_distinct_set_unique intro!: the_equality)
1388 with eq False show ?thesis unfolding f by(simp add: remove1_idem)
1393 proof(cases "finfun_dom f $ a")
1395 have "finfun_to_list f = xs"
1396 unfolding finfun_to_list_def
1397 proof(rule the_equality)
1398 have "finfun_dom f = finfun_dom f(a $:= b)" using False True
1399 by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
1400 with eq show 1: "set xs = {x. finfun_dom f $ x} \<and> sorted xs \<and> distinct xs"
1401 by(simp del: finfun_dom_update)
1404 assume "set xs' = {x. finfun_dom f $ x} \<and> sorted xs' \<and> distinct xs'"
1405 thus "xs' = xs" using 1 by(auto elim: sorted_distinct_set_unique)
1407 thus ?thesis using False True eq by(simp add: insort_insert_triv)
1410 have "finfun_to_list f = remove1 a xs"
1411 unfolding finfun_to_list_def
1412 proof(rule the_equality)
1413 have "set (remove1 a xs) = set xs - {a}" by simp
1415 have "{x. finfun_dom f(a $:= b) $ x} - {a} = {x. finfun_dom f $ x}" using False
1416 by(auto simp add: finfun_upd_apply split: split_if_asm)
1417 finally show 1: "set (remove1 a xs) = {x. finfun_dom f $ x} \<and> sorted (remove1 a xs) \<and> distinct (remove1 a xs)"
1418 by(simp add: sorted_remove1)
1421 assume "set xs' = {x. finfun_dom f $ x} \<and> sorted xs' \<and> distinct xs'"
1422 thus "xs' = remove1 a xs" using 1 by(blast intro: sorted_distinct_set_unique)
1424 thus ?thesis using False eq \<open>b \<noteq> finfun_default f\<close>
1425 by (simp add: insort_insert_insort insort_remove1)
1428 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)
1430 lemma finfun_to_list_update_code [code]:
1431 "finfun_to_list (finfun_update_code f a b) =
1432 (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
1433 by(simp add: finfun_to_list_update)
1435 text \<open>More type class instantiations\<close>
1437 lemma card_eq_1_iff: "card A = 1 \<longleftrightarrow> A \<noteq> {} \<and> (\<forall>x\<in>A. \<forall>y\<in>A. x = y)"
1438 (is "?lhs \<longleftrightarrow> ?rhs")
1443 assume A: "x \<in> A" "y \<in> A" and neq: "x \<noteq> y"
1444 have "finite A" using \<open>?lhs\<close> by(simp add: card_ge_0_finite)
1445 from neq have "2 = card {x, y}" by simp
1446 also have "\<dots> \<le> card A" using A \<open>finite A\<close>
1447 by(auto intro: card_mono)
1448 finally have False using \<open>?lhs\<close> by simp }
1449 ultimately show ?rhs by auto
1452 hence "A = {THE x. x \<in> A}"
1453 by safe (auto intro: theI the_equality[symmetric])
1454 also have "card \<dots> = 1" by simp
1458 lemma card_UNIV_finfun:
1459 defines "F == finfun :: ('a \<Rightarrow> 'b) set"
1460 shows "CARD('a \<Rightarrow>f 'b) = (if CARD('a) \<noteq> 0 \<and> CARD('b) \<noteq> 0 \<or> CARD('b) = 1 then CARD('b) ^ CARD('a) else 0)"
1461 proof(cases "0 < CARD('a) \<and> 0 < CARD('b) \<or> CARD('b) = 1")
1463 from True have "F = UNIV"
1465 assume b: "CARD('b) = 1"
1466 hence "\<forall>x :: 'b. x = undefined"
1467 by(auto simp add: card_eq_1_iff simp del: One_nat_def)
1468 thus ?thesis by(auto simp add: finfun_def F_def intro: exI[where x=undefined])
1469 qed(auto simp add: finfun_def card_gt_0_iff F_def intro: finite_subset[where B=UNIV])
1470 moreover have "CARD('a \<Rightarrow>f 'b) = card F"
1471 unfolding type_definition.Abs_image[OF type_definition_finfun, symmetric]
1472 by(auto intro!: card_image inj_onI simp add: Abs_finfun_inject F_def)
1473 ultimately show ?thesis by(simp add: card_fun)
1476 hence infinite: "\<not> (finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set))"
1477 and b: "CARD('b) \<noteq> 1" by(simp_all add: card_eq_0_iff)
1478 from b obtain b1 b2 :: 'b where "b1 \<noteq> b2"
1479 by(auto simp add: card_eq_1_iff simp del: One_nat_def)
1480 let ?f = "\<lambda>a a' :: 'a. if a = a' then b1 else b2"
1481 from infinite have "\<not> finite (UNIV :: ('a \<Rightarrow>f 'b) set)"
1482 proof(rule contrapos_nn[OF _ conjI])
1483 assume finite: "finite (UNIV :: ('a \<Rightarrow>f 'b) set)"
1485 unfolding type_definition.Abs_image[OF type_definition_finfun, symmetric] F_def
1486 by(rule finite_imageD)(auto intro: inj_onI simp add: Abs_finfun_inject)
1487 hence "finite (range ?f)"
1488 by(rule finite_subset[rotated 1])(auto simp add: F_def finfun_def \<open>b1 \<noteq> b2\<close> intro!: exI[where x=b2])
1489 thus "finite (UNIV :: 'a set)"
1490 by(rule finite_imageD)(auto intro: inj_onI simp add: fun_eq_iff \<open>b1 \<noteq> b2\<close> split: split_if_asm)
1492 from finite have "finite (range (\<lambda>b. ((K$ b) :: 'a \<Rightarrow>f 'b)))"
1493 by(rule finite_subset[rotated 1]) simp
1494 thus "finite (UNIV :: 'b set)"
1495 by(rule finite_imageD)(auto intro!: inj_onI)
1497 with False show ?thesis by auto
1500 lemma finite_UNIV_finfun:
1501 "finite (UNIV :: ('a \<Rightarrow>f 'b) set) \<longleftrightarrow>
1502 (finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set) \<or> CARD('b) = 1)"
1503 (is "?lhs \<longleftrightarrow> ?rhs")
1505 have "?lhs \<longleftrightarrow> CARD('a \<Rightarrow>f 'b) > 0" by(simp add: card_gt_0_iff)
1506 also have "\<dots> \<longleftrightarrow> CARD('a) > 0 \<and> CARD('b) > 0 \<or> CARD('b) = 1"
1507 by(simp add: card_UNIV_finfun)
1508 also have "\<dots> = ?rhs" by(simp add: card_gt_0_iff)
1509 finally show ?thesis .
1512 instantiation finfun :: (finite_UNIV, card_UNIV) finite_UNIV begin
1513 definition "finite_UNIV = Phantom('a \<Rightarrow>f 'b)
1514 (let cb = of_phantom (card_UNIV :: 'b card_UNIV)
1515 in cb = 1 \<or> of_phantom (finite_UNIV :: 'a finite_UNIV) \<and> cb \<noteq> 0)"
1517 by intro_classes (auto simp add: finite_UNIV_finfun_def Let_def card_UNIV finite_UNIV finite_UNIV_finfun card_gt_0_iff)
1520 instantiation finfun :: (card_UNIV, card_UNIV) card_UNIV begin
1521 definition "card_UNIV = Phantom('a \<Rightarrow>f 'b)
1522 (let ca = of_phantom (card_UNIV :: 'a card_UNIV);
1523 cb = of_phantom (card_UNIV :: 'b card_UNIV)
1524 in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)"
1525 instance by intro_classes (simp add: card_UNIV_finfun_def card_UNIV Let_def card_UNIV_finfun)
1528 text \<open>Deactivate syntax again. Import theory \<open>FinFun_Syntax\<close> to reactivate it again\<close>
1531 finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
1534 finfun_const ("K$/ _" [0] 1) and
1535 finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and
1536 finfun_apply (infixl "$" 999) and
1537 finfun_comp (infixr "o$" 55) and
1538 finfun_comp2 (infixr "$o" 55) and
1539 finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000)
1541 no_notation (xsymbols)
1542 finfun_comp (infixr "\<circ>$" 55) and
1543 finfun_comp2 (infixr "$\<circ>" 55)