src/HOL/Library/FinFun.thy
 author Andreas Lochbihler Tue May 29 15:31:58 2012 +0200 (2012-05-29) changeset 48028 a5377f6d9f14 child 48029 9d9c9069abbc permissions -rw-r--r--
move FinFuns from AFP to repository
1 (* Author: Andreas Lochbihler, Uni Karlsruhe *)
3 header {* Almost everywhere constant functions *}
5 theory FinFun
6 imports Card_Univ
7 begin
9 text {*
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.
17 *}
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)"
36 lemma map_default_insert:
37   "map_default b (f(a \<mapsto> b')) = (map_default b f)(a := b')"
40 lemma map_default_empty [simp]: "map_default b empty = (\<lambda>a. b)"
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'"
50 proof -
51   from infin_eq show bb': "b = b'"
52   proof
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
59   qed
61   show "g = g'"
62   proof
63     fix x
64     show "g x = g' x"
65     proof(cases "g x")
66       case None
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
71     next
72       case (Some c)
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
78     qed
79   qed
80 qed
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 proof -
88   have "\<exists>f. finite {x. f x \<noteq> undefined}"
89   proof
90     show "finite {x. (\<lambda>y. undefined) x \<noteq> undefined}" by auto
91   qed
92   then show ?thesis unfolding finfun_def by auto
93 qed
95 setup_lifting type_definition_finfun
97 lemma fun_upd_finfun: "y(a := b) \<in> finfun \<longleftrightarrow> y \<in> finfun"
98 proof -
99   { fix b'
100     have "finite {a'. (y(a := b)) a' \<noteq> b'} = finite {a'. y a' \<noteq> b'}"
101     proof(cases "b = b'")
102       case True
103       hence "{a'. (y(a := b)) a' \<noteq> b'} = {a'. y a' \<noteq> b'} - {a}" by auto
104       thus ?thesis by simp
105     next
106       case False
107       hence "{a'. (y(a := b)) a' \<noteq> b'} = insert a {a'. y a' \<noteq> b'}" by auto
108       thus ?thesis by simp
109     qed }
110   thus ?thesis unfolding finfun_def by blast
111 qed
113 lemma const_finfun: "(\<lambda>x. a) \<in> finfun"
116 lemma finfun_left_compose:
117   assumes "y \<in> finfun"
118   shows "g \<circ> y \<in> finfun"
119 proof -
120   from assms obtain b where "finite {a. y a \<noteq> b}"
121     unfolding finfun_def by blast
122   hence "finite {c. g (y c) \<noteq> g b}"
123   proof(induct "{a. y a \<noteq> b}" arbitrary: y)
124     case empty
125     hence "y = (\<lambda>a. b)" by(auto intro: ext)
126     thus ?case by(simp)
127   next
128     case (insert x F)
129     note IH = `\<And>y. F = {a. y a \<noteq> b} \<Longrightarrow> finite {c. g (y c) \<noteq> g b}`
130     from `insert x F = {a. y a \<noteq> b}` `x \<notin> F`
131     have F: "F = {a. (y(x := b)) a \<noteq> b}" by(auto)
132     show ?case
133     proof(cases "g (y x) = g b")
134       case True
135       hence "{c. g ((y(x := b)) c) \<noteq> g b} = {c. g (y c) \<noteq> g b}" by auto
136       with IH[OF F] show ?thesis by simp
137     next
138       case False
139       hence "{c. g (y c) \<noteq> g b} = insert x {c. g ((y(x := b)) c) \<noteq> g b}" by auto
140       with IH[OF F] show ?thesis by(simp)
141     qed
142   qed
143   thus ?thesis unfolding finfun_def by auto
144 qed
146 lemma assumes "y \<in> finfun"
147   shows fst_finfun: "fst \<circ> y \<in> finfun"
148   and snd_finfun: "snd \<circ> y \<in> finfun"
149 proof -
150   from assms obtain b c where bc: "finite {a. y a \<noteq> (b, c)}"
151     unfolding finfun_def by auto
152   have "{a. fst (y a) \<noteq> b} \<subseteq> {a. y a \<noteq> (b, c)}"
153     and "{a. snd (y a) \<noteq> c} \<subseteq> {a. y a \<noteq> (b, c)}" by auto
154   hence "finite {a. fst (y a) \<noteq> b}"
155     and "finite {a. snd (y a) \<noteq> c}" using bc by(auto intro: finite_subset)
156   thus "fst \<circ> y \<in> finfun" "snd \<circ> y \<in> finfun"
157     unfolding finfun_def by auto
158 qed
160 lemma map_of_finfun: "map_of xs \<in> finfun"
161 unfolding finfun_def
162 by(induct xs)(auto simp add: Collect_neg_eq Collect_conj_eq Collect_imp_eq intro: finite_subset)
164 lemma Diag_finfun: "(\<lambda>x. (f x, g x)) \<in> finfun \<longleftrightarrow> f \<in> finfun \<and> g \<in> finfun"
165 by(auto intro: finite_subset simp add: Collect_neg_eq Collect_imp_eq Collect_conj_eq finfun_def)
167 lemma finfun_right_compose:
168   assumes g: "g \<in> finfun" and inj: "inj f"
169   shows "g o f \<in> finfun"
170 proof -
171   from g obtain b where b: "finite {a. g a \<noteq> b}" unfolding finfun_def by blast
172   moreover have "f ` {a. g (f a) \<noteq> b} \<subseteq> {a. g a \<noteq> b}" by auto
173   moreover from inj have "inj_on f {a.  g (f a) \<noteq> b}" by(rule subset_inj_on) blast
174   ultimately have "finite {a. g (f a) \<noteq> b}"
175     by(blast intro: finite_imageD[where f=f] finite_subset)
176   thus ?thesis unfolding finfun_def by auto
177 qed
179 lemma finfun_curry:
180   assumes fin: "f \<in> finfun"
181   shows "curry f \<in> finfun" "curry f a \<in> finfun"
182 proof -
183   from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast
184   moreover have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force)
185   hence "{a. curry f a \<noteq> (\<lambda>b. c)} = fst ` {ab. f ab \<noteq> c}"
186     by(auto simp add: curry_def fun_eq_iff)
187   ultimately have "finite {a. curry f a \<noteq> (\<lambda>b. c)}" by simp
188   thus "curry f \<in> finfun" unfolding finfun_def by blast
190   have "snd ` {ab. f ab \<noteq> c} = {b. \<exists>a. f (a, b) \<noteq> c}" by(force)
191   hence "{b. f (a, b) \<noteq> c} \<subseteq> snd ` {ab. f ab \<noteq> c}" by auto
192   hence "finite {b. f (a, b) \<noteq> c}" by(rule finite_subset)(rule finite_imageI[OF c])
193   thus "curry f a \<in> finfun" unfolding finfun_def by auto
194 qed
196 lemmas finfun_simp =
197   fst_finfun snd_finfun Abs_finfun_inverse Rep_finfun_inverse Abs_finfun_inject Rep_finfun_inject Diag_finfun finfun_curry
198 lemmas finfun_iff = const_finfun fun_upd_finfun Rep_finfun map_of_finfun
199 lemmas finfun_intro = finfun_left_compose fst_finfun snd_finfun
201 lemma Abs_finfun_inject_finite:
202   fixes x y :: "'a \<Rightarrow> 'b"
203   assumes fin: "finite (UNIV :: 'a set)"
204   shows "Abs_finfun x = Abs_finfun y \<longleftrightarrow> x = y"
205 proof
206   assume "Abs_finfun x = Abs_finfun y"
207   moreover have "x \<in> finfun" "y \<in> finfun" unfolding finfun_def
208     by(auto intro: finite_subset[OF _ fin])
209   ultimately show "x = y" by(simp add: Abs_finfun_inject)
210 qed simp
212 lemma Abs_finfun_inject_finite_class:
213   fixes x y :: "('a :: finite) \<Rightarrow> 'b"
214   shows "Abs_finfun x = Abs_finfun y \<longleftrightarrow> x = y"
215 using finite_UNIV
218 lemma Abs_finfun_inj_finite:
219   assumes fin: "finite (UNIV :: 'a set)"
220   shows "inj (Abs_finfun :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b)"
221 proof(rule inj_onI)
222   fix x y :: "'a \<Rightarrow> 'b"
223   assume "Abs_finfun x = Abs_finfun y"
224   moreover have "x \<in> finfun" "y \<in> finfun" unfolding finfun_def
225     by(auto intro: finite_subset[OF _ fin])
226   ultimately show "x = y" by(simp add: Abs_finfun_inject)
227 qed
229 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
231 lemma Abs_finfun_inverse_finite:
232   fixes x :: "'a \<Rightarrow> 'b"
233   assumes fin: "finite (UNIV :: 'a set)"
234   shows "Rep_finfun (Abs_finfun x) = x"
235 proof -
236   from fin have "x \<in> finfun"
237     by(auto simp add: finfun_def intro: finite_subset)
238   thus ?thesis by simp
239 qed
241 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
243 lemma Abs_finfun_inverse_finite_class:
244   fixes x :: "('a :: finite) \<Rightarrow> 'b"
245   shows "Rep_finfun (Abs_finfun x) = x"
246 using finite_UNIV by(simp add: Abs_finfun_inverse_finite)
248 lemma finfun_eq_finite_UNIV: "finite (UNIV :: 'a set) \<Longrightarrow> (finfun :: ('a \<Rightarrow> 'b) set) = UNIV"
249 unfolding finfun_def by(auto intro: finite_subset)
251 lemma finfun_finite_UNIV_class: "finfun = (UNIV :: ('a :: finite \<Rightarrow> 'b) set)"
254 lemma map_default_in_finfun:
255   assumes fin: "finite (dom f)"
256   shows "map_default b f \<in> finfun"
257 unfolding finfun_def
258 proof(intro CollectI exI)
259   from fin show "finite {a. map_default b f a \<noteq> b}"
260     by(auto simp add: map_default_def dom_def Collect_conj_eq split: option.splits)
261 qed
263 lemma finfun_cases_map_default:
264   obtains b g where "f = Abs_finfun (map_default b g)" "finite (dom g)" "b \<notin> ran g"
265 proof -
266   obtain y where f: "f = Abs_finfun y" and y: "y \<in> finfun" by(cases f)
267   from y obtain b where b: "finite {a. y a \<noteq> b}" unfolding finfun_def by auto
268   let ?g = "(\<lambda>a. if y a = b then None else Some (y a))"
269   have "map_default b ?g = y" by(simp add: fun_eq_iff map_default_def)
270   with f have "f = Abs_finfun (map_default b ?g)" by simp
271   moreover from b have "finite (dom ?g)" by(auto simp add: dom_def)
272   moreover have "b \<notin> ran ?g" by(auto simp add: ran_def)
273   ultimately show ?thesis by(rule that)
274 qed
277 subsection {* Kernel functions for type @{typ "'a \<Rightarrow>\<^isub>f 'b"} *}
279 lift_definition finfun_const :: "'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("\<lambda>\<^isup>f/ _" [0] 1)
280 is "\<lambda> b x. b" by (rule const_finfun)
282 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)
284 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
286 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)"
287 by transfer (simp add: fun_upd_twist)
289 lemma finfun_update_twice [simp]:
290   "finfun_update (finfun_update f a b) a b' = finfun_update f a b'"
291 by transfer simp
293 lemma finfun_update_const_same: "(\<lambda>\<^isup>f b)(\<^sup>f a := b) = (\<lambda>\<^isup>f b)"
294 by transfer (simp add: fun_eq_iff)
296 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
298 subsection {* Code generator setup *}
300 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)
301 where [simp, code del]: "finfun_update_code = finfun_update"
303 code_datatype finfun_const finfun_update_code
305 lemma finfun_update_const_code [code]:
306   "(\<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')"
309 lemma finfun_update_update_code [code]:
310   "(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)"
314 subsection {* Setup for quickcheck *}
316 quickcheck_generator finfun constructors: finfun_update_code, "finfun_const :: 'b => 'a \<Rightarrow>\<^isub>f 'b"
318 subsection {* @{text "finfun_update"} as instance of @{text "comp_fun_commute"} *}
320 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
322 interpretation finfun_update: comp_fun_commute "\<lambda>a f. f(\<^sup>f a :: 'a := b')"
323 proof
324   fix a a' :: 'a
325   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'))"
326   proof
327     fix b
328     have "(Rep_finfun b)(a := b', a' := b') = (Rep_finfun b)(a' := b', a := b')"
329       by(cases "a = a'")(auto simp add: fun_upd_twist)
330     then have "b(\<^sup>f a := b')(\<^sup>f a' := b') = b(\<^sup>f a' := b')(\<^sup>f a := b')"
331       by(auto simp add: finfun_update_def fun_upd_twist)
332     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   qed
335 qed
337 lemma fold_finfun_update_finite_univ:
338   assumes fin: "finite (UNIV :: 'a set)"
339   shows "Finite_Set.fold (\<lambda>a f. f(\<^sup>f a := b')) (\<lambda>\<^isup>f b) (UNIV :: 'a set) = (\<lambda>\<^isup>f b')"
340 proof -
341   { fix A :: "'a set"
342     from fin have "finite A" by(auto intro: finite_subset)
343     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)"
344     proof(induct)
345       case (insert x F)
346       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)"
347         by(auto intro: ext)
348       with insert show ?case
351   thus ?thesis by(simp add: finfun_const_def)
352 qed
355 subsection {* Default value for FinFuns *}
357 definition finfun_default_aux :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"
358 where [code del]: "finfun_default_aux f = (if finite (UNIV :: 'a set) then undefined else THE b. finite {a. f a \<noteq> b})"
360 lemma finfun_default_aux_infinite:
361   fixes f :: "'a \<Rightarrow> 'b"
362   assumes infin: "\<not> finite (UNIV :: 'a set)"
363   and fin: "finite {a. f a \<noteq> b}"
364   shows "finfun_default_aux f = b"
365 proof -
366   let ?B = "{a. f a \<noteq> b}"
367   from fin have "(THE b. finite {a. f a \<noteq> b}) = b"
368   proof(rule the_equality)
369     fix b'
370     assume "finite {a. f a \<noteq> b'}" (is "finite ?B'")
371     with infin fin have "UNIV - (?B' \<union> ?B) \<noteq> {}" by(auto dest: finite_subset)
372     then obtain a where a: "a \<notin> ?B' \<union> ?B" by auto
373     thus "b' = b" by auto
374   qed
375   thus ?thesis using infin by(simp add: finfun_default_aux_def)
376 qed
379 lemma finite_finfun_default_aux:
380   fixes f :: "'a \<Rightarrow> 'b"
381   assumes fin: "f \<in> finfun"
382   shows "finite {a. f a \<noteq> finfun_default_aux f}"
383 proof(cases "finite (UNIV :: 'a set)")
384   case True thus ?thesis using fin
385     by(auto simp add: finfun_def finfun_default_aux_def intro: finite_subset)
386 next
387   case False
388   from fin obtain b where b: "finite {a. f a \<noteq> b}" (is "finite ?B")
389     unfolding finfun_def by blast
390   with False show ?thesis by(simp add: finfun_default_aux_infinite)
391 qed
393 lemma finfun_default_aux_update_const:
394   fixes f :: "'a \<Rightarrow> 'b"
395   assumes fin: "f \<in> finfun"
396   shows "finfun_default_aux (f(a := b)) = finfun_default_aux f"
397 proof(cases "finite (UNIV :: 'a set)")
398   case False
399   from fin obtain b' where b': "finite {a. f a \<noteq> b'}" unfolding finfun_def by blast
400   hence "finite {a'. (f(a := b)) a' \<noteq> b'}"
401   proof(cases "b = b' \<and> f a \<noteq> b'")
402     case True
403     hence "{a. f a \<noteq> b'} = insert a {a'. (f(a := b)) a' \<noteq> b'}" by auto
404     thus ?thesis using b' by simp
405   next
406     case False
407     moreover
408     { assume "b \<noteq> b'"
409       hence "{a'. (f(a := b)) a' \<noteq> b'} = insert a {a. f a \<noteq> b'}" by auto
410       hence ?thesis using b' by simp }
411     moreover
412     { assume "b = b'" "f a = b'"
413       hence "{a'. (f(a := b)) a' \<noteq> b'} = {a. f a \<noteq> b'}" by auto
414       hence ?thesis using b' by simp }
415     ultimately show ?thesis by blast
416   qed
417   with False b' show ?thesis by(auto simp del: fun_upd_apply simp add: finfun_default_aux_infinite)
418 next
419   case True thus ?thesis by(simp add: finfun_default_aux_def)
420 qed
422 lift_definition finfun_default :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'b"
423 is "finfun_default_aux" ..
425 lemma finite_finfun_default: "finite {a. Rep_finfun f a \<noteq> finfun_default f}"
426 apply transfer apply (erule finite_finfun_default_aux)
427 unfolding Rel_def fun_rel_def cr_finfun_def by simp
429 lemma finfun_default_const: "finfun_default ((\<lambda>\<^isup>f b) :: 'a \<Rightarrow>\<^isub>f 'b) = (if finite (UNIV :: 'a set) then undefined else b)"
430 apply(transfer)
433 done
435 lemma finfun_default_update_const:
436   "finfun_default (f(\<^sup>f a := b)) = finfun_default f"
437 by transfer (simp add: finfun_default_aux_update_const)
439 lemma finfun_default_const_code [code]:
440   "finfun_default ((\<lambda>\<^isup>f c) :: ('a :: card_UNIV) \<Rightarrow>\<^isub>f 'b) = (if card_UNIV (TYPE('a)) = 0 then c else undefined)"
443 lemma finfun_default_update_code [code]:
444   "finfun_default (finfun_update_code f a b) = finfun_default f"
447 subsection {* Recursion combinator and well-formedness conditions *}
449 definition finfun_rec :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<Rightarrow> 'c"
450 where [code del]:
451   "finfun_rec cnst upd f \<equiv>
452    let b = finfun_default f;
453        g = THE g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g
454    in Finite_Set.fold (\<lambda>a. upd a (map_default b g a)) (cnst b) (dom g)"
456 locale finfun_rec_wf_aux =
457   fixes cnst :: "'b \<Rightarrow> 'c"
458   and upd :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c"
459   assumes upd_const_same: "upd a b (cnst b) = cnst b"
460   and upd_commute: "a \<noteq> a' \<Longrightarrow> upd a b (upd a' b' c) = upd a' b' (upd a b c)"
461   and upd_idemp: "b \<noteq> b' \<Longrightarrow> upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)"
462 begin
465 lemma upd_left_comm: "comp_fun_commute (\<lambda>a. upd a (f a))"
466 by(unfold_locales)(auto intro: upd_commute simp add: fun_eq_iff)
468 lemma upd_upd_twice: "upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)"
469 by(cases "b \<noteq> b'")(auto simp add: fun_upd_def upd_const_same upd_idemp)
471 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
473 lemma map_default_update_const:
474   assumes fin: "finite (dom f)"
475   and anf: "a \<notin> dom f"
476   and fg: "f \<subseteq>\<^sub>m g"
477   shows "upd a d  (Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f)) =
478          Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f)"
479 proof -
480   let ?upd = "\<lambda>a. upd a (map_default d g a)"
481   let ?fr = "\<lambda>A. Finite_Set.fold ?upd (cnst d) A"
482   interpret gwf: comp_fun_commute "?upd" by(rule upd_left_comm)
484   from fin anf fg show ?thesis
485   proof(induct "dom f" arbitrary: f)
486     case empty
487     from `{} = dom f` have "f = empty" by(auto simp add: dom_def intro: ext)
488     thus ?case by(simp add: finfun_const_def upd_const_same)
489   next
490     case (insert a' A)
491     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)`
492     note fin = `finite A` note anf = `a \<notin> dom f` note a'nA = `a' \<notin> A`
493     note domf = `insert a' A = dom f` note fg = `f \<subseteq>\<^sub>m g`
495     from domf obtain b where b: "f a' = Some b" by auto
496     let ?f' = "f(a' := None)"
497     have "upd a d (?fr (insert a' A)) = upd a d (upd a' (map_default d g a') (?fr A))"
498       by(subst gwf.fold_insert[OF fin a'nA]) rule
499     also from b fg have "g a' = f a'" by(auto simp add: map_le_def intro: domI dest: bspec)
500     hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def)
501     also from anf domf have "a \<noteq> a'" by auto note upd_commute[OF this]
502     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)
503     note A also note IH[OF A `a \<notin> dom ?f'` `?f' \<subseteq>\<^sub>m g`]
504     also have "upd a' (map_default d f a') (?fr (dom (f(a' := None)))) = ?fr (dom f)"
505       unfolding domf[symmetric] gwf.fold_insert[OF fin a'nA] ga' unfolding A ..
506     also have "insert a' (dom ?f') = dom f" using domf by auto
507     finally show ?case .
508   qed
509 qed
511 lemma map_default_update_twice:
512   assumes fin: "finite (dom f)"
513   and anf: "a \<notin> dom f"
514   and fg: "f \<subseteq>\<^sub>m g"
515   shows "upd a d'' (upd a d' (Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f))) =
516          upd a d'' (Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f))"
517 proof -
518   let ?upd = "\<lambda>a. upd a (map_default d g a)"
519   let ?fr = "\<lambda>A. Finite_Set.fold ?upd (cnst d) A"
520   interpret gwf: comp_fun_commute "?upd" by(rule upd_left_comm)
522   from fin anf fg show ?thesis
523   proof(induct "dom f" arbitrary: f)
524     case empty
525     from `{} = dom f` have "f = empty" by(auto simp add: dom_def intro: ext)
526     thus ?case by(auto simp add: finfun_const_def finfun_update_def upd_upd_twice)
527   next
528     case (insert a' A)
529     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))`
530     note fin = `finite A` note anf = `a \<notin> dom f` note a'nA = `a' \<notin> A`
531     note domf = `insert a' A = dom f` note fg = `f \<subseteq>\<^sub>m g`
533     from domf obtain b where b: "f a' = Some b" by auto
534     let ?f' = "f(a' := None)"
535     let ?b' = "case f a' of None \<Rightarrow> d | Some b \<Rightarrow> b"
536     from domf have "upd a d'' (upd a d' (?fr (dom f))) = upd a d'' (upd a d' (?fr (insert a' A)))" by simp
537     also note gwf.fold_insert[OF fin a'nA]
538     also from b fg have "g a' = f a'" by(auto simp add: map_le_def intro: domI dest: bspec)
539     hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def)
540     also from anf domf have ana': "a \<noteq> a'" by auto note upd_commute[OF this]
541     also note upd_commute[OF ana']
542     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)
543     note A also note IH[OF A `a \<notin> dom ?f'` `?f' \<subseteq>\<^sub>m g`]
544     also note upd_commute[OF ana'[symmetric]] also note ga'[symmetric] also note A[symmetric]
545     also note gwf.fold_insert[symmetric, OF fin a'nA] also note domf
546     finally show ?case .
547   qed
548 qed
550 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
552 lemma map_default_eq_id [simp]: "map_default d ((\<lambda>a. Some (f a)) |` {a. f a \<noteq> d}) = f"
553 by(auto simp add: map_default_def restrict_map_def intro: ext)
555 lemma finite_rec_cong1:
556   assumes f: "comp_fun_commute f" and g: "comp_fun_commute g"
557   and fin: "finite A"
558   and eq: "\<And>a. a \<in> A \<Longrightarrow> f a = g a"
559   shows "Finite_Set.fold f z A = Finite_Set.fold g z A"
560 proof -
561   interpret f: comp_fun_commute f by(rule f)
562   interpret g: comp_fun_commute g by(rule g)
563   { fix B
564     assume BsubA: "B \<subseteq> A"
565     with fin have "finite B" by(blast intro: finite_subset)
566     hence "B \<subseteq> A \<Longrightarrow> Finite_Set.fold f z B = Finite_Set.fold g z B"
567     proof(induct)
568       case empty thus ?case by simp
569     next
570       case (insert a B)
571       note finB = `finite B` note anB = `a \<notin> B` note sub = `insert a B \<subseteq> A`
572       note IH = `B \<subseteq> A \<Longrightarrow> Finite_Set.fold f z B = Finite_Set.fold g z B`
573       from sub anB have BpsubA: "B \<subset> A" and BsubA: "B \<subseteq> A" and aA: "a \<in> A" by auto
574       from IH[OF BsubA] eq[OF aA] finB anB
575       show ?case by(auto)
576     qed
577     with BsubA have "Finite_Set.fold f z B = Finite_Set.fold g z B" by blast }
578   thus ?thesis by blast
579 qed
581 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
583 lemma finfun_rec_upd [simp]:
584   "finfun_rec cnst upd (f(\<^sup>f a' := b')) = upd a' b' (finfun_rec cnst upd f)"
585 proof -
586   obtain b where b: "b = finfun_default f" by auto
587   let ?the = "\<lambda>f g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g"
588   obtain g where g: "g = The (?the f)" by blast
589   obtain y where f: "f = Abs_finfun y" and y: "y \<in> finfun" by (cases f)
590   from f y b have bfin: "finite {a. y a \<noteq> b}" by(simp add: finfun_default_def finite_finfun_default_aux)
592   let ?g = "(\<lambda>a. Some (y a)) |` {a. y a \<noteq> b}"
593   from bfin have fing: "finite (dom ?g)" by auto
594   have bran: "b \<notin> ran ?g" by(auto simp add: ran_def restrict_map_def)
595   have yg: "y = map_default b ?g" by simp
596   have gg: "g = ?g" unfolding g
597   proof(rule the_equality)
598     from f y bfin show "?the f ?g"
599       by(auto)(simp add: restrict_map_def ran_def split: split_if_asm)
600   next
601     fix g'
602     assume "?the f g'"
603     hence fin': "finite (dom g')" and ran': "b \<notin> ran g'"
604       and eq: "Abs_finfun (map_default b ?g) = Abs_finfun (map_default b g')" using f yg by auto
605     from fin' fing have "map_default b ?g \<in> finfun" "map_default b g' \<in> finfun" by(blast intro: map_default_in_finfun)+
606     with eq have "map_default b ?g = map_default b g'" by simp
607     with fing bran fin' ran' show "g' = ?g" by(rule map_default_inject[OF disjI2[OF refl], THEN sym])
608   qed
610   show ?thesis
611   proof(cases "b' = b")
612     case True
613     note b'b = True
615     let ?g' = "(\<lambda>a. Some ((y(a' := b)) a)) |` {a. (y(a' := b)) a \<noteq> b}"
616     from bfin b'b have fing': "finite (dom ?g')"
617       by(auto simp add: Collect_conj_eq Collect_imp_eq intro: finite_subset)
618     have brang': "b \<notin> ran ?g'" by(auto simp add: ran_def restrict_map_def)
620     let ?b' = "\<lambda>a. case ?g' a of None \<Rightarrow> b | Some b \<Rightarrow> b"
621     let ?b = "map_default b ?g"
622     from upd_left_comm upd_left_comm fing'
623     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')"
624       by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b b map_default_def)
625     also interpret gwf: comp_fun_commute "\<lambda>a. upd a (?b a)" by(rule upd_left_comm)
626     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))"
627     proof(cases "y a' = b")
628       case True
629       with b'b have g': "?g' = ?g" by(auto simp add: restrict_map_def intro: ext)
630       from True have a'ndomg: "a' \<notin> dom ?g" by auto
631       from f b'b b show ?thesis unfolding g'
632         by(subst map_default_update_const[OF fing a'ndomg map_le_refl, symmetric]) simp
633     next
634       case False
635       hence domg: "dom ?g = insert a' (dom ?g')" by auto
636       from False b'b have a'ndomg': "a' \<notin> dom ?g'" by auto
637       have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g')) =
638             upd a' (?b a') (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'))"
639         using fing' a'ndomg' unfolding b'b by(rule gwf.fold_insert)
640       hence "upd a' b (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g'))) =
641              upd a' b (upd a' (?b a') (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g')))" by simp
642       also from b'b have g'leg: "?g' \<subseteq>\<^sub>m ?g" by(auto simp add: restrict_map_def map_le_def)
643       note map_default_update_twice[OF fing' a'ndomg' this, of b "?b a'" b]
644       also note map_default_update_const[OF fing' a'ndomg' g'leg, of b]
645       finally show ?thesis unfolding b'b domg[unfolded b'b] by(rule sym)
646     qed
647     also have "The (?the (f(\<^sup>f a' := b'))) = ?g'"
648     proof(rule the_equality)
649       from f y b b'b brang' fing' show "?the (f(\<^sup>f a' := b')) ?g'"
650         by(auto simp del: fun_upd_apply simp add: finfun_update_def)
651     next
652       fix g'
653       assume "?the (f(\<^sup>f a' := b')) g'"
654       hence fin': "finite (dom g')" and ran': "b \<notin> ran g'"
655         and eq: "f(\<^sup>f a' := b') = Abs_finfun (map_default b g')"
656         by(auto simp del: fun_upd_apply)
657       from fin' fing' have "map_default b g' \<in> finfun" "map_default b ?g' \<in> finfun"
658         by(blast intro: map_default_in_finfun)+
659       with eq f b'b b have "map_default b ?g' = map_default b g'"
660         by(simp del: fun_upd_apply add: finfun_update_def)
661       with fing' brang' fin' ran' show "g' = ?g'"
662         by(rule map_default_inject[OF disjI2[OF refl], THEN sym])
663     qed
664     ultimately show ?thesis unfolding finfun_rec_def Let_def b gg[unfolded g b] using bfin b'b b
665       by(simp only: finfun_default_update_const map_default_def)
666   next
667     case False
668     note b'b = this
669     let ?g' = "?g(a' \<mapsto> b')"
670     let ?b' = "map_default b ?g'"
671     let ?b = "map_default b ?g"
672     from fing have fing': "finite (dom ?g')" by auto
673     from bran b'b have bnrang': "b \<notin> ran ?g'" by(auto simp add: ran_def)
674     have ffmg': "map_default b ?g' = y(a' := b')" by(auto intro: ext simp add: map_default_def restrict_map_def)
675     with f y have f_Abs: "f(\<^sup>f a' := b') = Abs_finfun (map_default b ?g')" by(auto simp add: finfun_update_def)
676     have g': "The (?the (f(\<^sup>f a' := b'))) = ?g'"
677     proof (rule the_equality)
678       from fing' bnrang' f_Abs show "?the (f(\<^sup>f a' := b')) ?g'" by(auto simp add: finfun_update_def restrict_map_def)
679     next
680       fix g' assume "?the (f(\<^sup>f a' := b')) g'"
681       hence f': "f(\<^sup>f a' := b') = Abs_finfun (map_default b g')"
682         and fin': "finite (dom g')" and brang': "b \<notin> ran g'" by auto
683       from fing' fin' have "map_default b ?g' \<in> finfun" "map_default b g' \<in> finfun"
684         by(auto intro: map_default_in_finfun)
685       with f' f_Abs have "map_default b g' = map_default b ?g'" by simp
686       with fin' brang' fing' bnrang' show "g' = ?g'"
687         by(rule map_default_inject[OF disjI2[OF refl]])
688     qed
689     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}))"
690       by auto
691     show ?thesis
692     proof(cases "y a' = b")
693       case True
694       hence a'ndomg: "a' \<notin> dom ?g" by auto
695       from f y b'b True have yff: "y = map_default b (?g' |` dom ?g)"
696         by(auto simp add: restrict_map_def map_default_def intro!: ext)
697       hence f': "f = Abs_finfun (map_default b (?g' |` dom ?g))" using f by simp
698       interpret g'wf: comp_fun_commute "\<lambda>a. upd a (?b' a)" by(rule upd_left_comm)
699       from upd_left_comm upd_left_comm fing
700       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)"
701         by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b True map_default_def)
702       thus ?thesis unfolding finfun_rec_def Let_def finfun_default_update_const b[symmetric]
703         unfolding g' g[symmetric] gg g'wf.fold_insert[OF fing a'ndomg, of "cnst b", folded dom]
704         by -(rule arg_cong2[where f="upd a'"], simp_all add: map_default_def)
705     next
706       case False
707       hence "insert a' (dom ?g) = dom ?g" by auto
708       moreover {
709         let ?g'' = "?g(a' := None)"
710         let ?b'' = "map_default b ?g''"
711         from False have domg: "dom ?g = insert a' (dom ?g'')" by auto
712         from False have a'ndomg'': "a' \<notin> dom ?g''" by auto
713         have fing'': "finite (dom ?g'')" by(rule finite_subset[OF _ fing]) auto
714         have bnrang'': "b \<notin> ran ?g''" by(auto simp add: ran_def restrict_map_def)
715         interpret gwf: comp_fun_commute "\<lambda>a. upd a (?b a)" by(rule upd_left_comm)
716         interpret g'wf: comp_fun_commute "\<lambda>a. upd a (?b' a)" by(rule upd_left_comm)
717         have "upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g''))) =
718               upd a' b' (upd a' (?b a') (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')))"
719           unfolding gwf.fold_insert[OF fing'' a'ndomg''] f ..
720         also have g''leg: "?g |` dom ?g'' \<subseteq>\<^sub>m ?g" by(auto simp add: map_le_def)
721         have "dom (?g |` dom ?g'') = dom ?g''" by auto
722         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",
723                                      unfolded this, OF fing'' a'ndomg'' g''leg]
724         also have b': "b' = ?b' a'" by(auto simp add: map_default_def)
725         from upd_left_comm upd_left_comm fing''
726         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'')"
727           by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b map_default_def)
728         with b' have "upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')) =
729                      upd a' (?b' a') (Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g''))" by simp
730         also note g'wf.fold_insert[OF fing'' a'ndomg'', symmetric]
731         finally have "upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g)) =
732                    Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g)"
733           unfolding domg . }
734       ultimately have "Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (insert a' (dom ?g)) =
735                     upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g))" by simp
736       thus ?thesis unfolding finfun_rec_def Let_def finfun_default_update_const b[symmetric] g[symmetric] g' dom[symmetric]
737         using b'b gg by(simp add: map_default_insert)
738     qed
739   qed
740 qed
742 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
744 end
746 locale finfun_rec_wf = finfun_rec_wf_aux +
747   assumes const_update_all:
748   "finite (UNIV :: 'a set) \<Longrightarrow> Finite_Set.fold (\<lambda>a. upd a b') (cnst b) (UNIV :: 'a set) = cnst b'"
749 begin
751 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
753 lemma finfun_rec_const [simp]:
754   "finfun_rec cnst upd (\<lambda>\<^isup>f c) = cnst c"
755 proof(cases "finite (UNIV :: 'a set)")
756   case False
757   hence "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = c" by(simp add: finfun_default_const)
758   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"
759   proof (rule the_equality)
760     show "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c empty) \<and> finite (dom empty) \<and> c \<notin> ran empty"
762   next
763     fix g :: "'a \<rightharpoonup> 'b"
764     assume "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g"
765     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+
766     from g map_default_in_finfun[OF fin, of c] have "map_default c g = (\<lambda>a. c)"
768     moreover have "map_default c empty = (\<lambda>a. c)" by simp
769     ultimately show "g = empty" by-(rule map_default_inject[OF disjI2[OF refl] fin ran], auto)
770   qed
771   ultimately show ?thesis by(simp add: finfun_rec_def)
772 next
773   case True
774   hence default: "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = undefined" by(simp add: finfun_default_const)
775   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"
776   show ?thesis
777   proof(cases "c = undefined")
778     case True
779     have the: "The ?the = empty"
780     proof (rule the_equality)
781       from True show "?the empty" by(auto simp add: finfun_const_def)
782     next
783       fix g'
784       assume "?the g'"
785       hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g')"
786         and fin: "finite (dom g')" and g: "undefined \<notin> ran g'" by simp_all
787       from fin have "map_default undefined g' \<in> finfun" by(rule map_default_in_finfun)
788       with fg have "map_default undefined g' = (\<lambda>a. c)"
789         by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1])
790       with True show "g' = empty"
791         by -(rule map_default_inject(2)[OF _ fin g], auto)
792     qed
793     show ?thesis unfolding finfun_rec_def using `finite UNIV` True
794       unfolding Let_def the default by(simp)
795   next
796     case False
797     have the: "The ?the = (\<lambda>a :: 'a. Some c)"
798     proof (rule the_equality)
799       from False True show "?the (\<lambda>a :: 'a. Some c)"
800         by(auto simp add: map_default_def [abs_def] finfun_const_def dom_def ran_def)
801     next
802       fix g' :: "'a \<rightharpoonup> 'b"
803       assume "?the g'"
804       hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g')"
805         and fin: "finite (dom g')" and g: "undefined \<notin> ran g'" by simp_all
806       from fin have "map_default undefined g' \<in> finfun" by(rule map_default_in_finfun)
807       with fg have "map_default undefined g' = (\<lambda>a. c)"
808         by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1])
809       with True False show "g' = (\<lambda>a::'a. Some c)"
810         by - (rule map_default_inject(2)[OF _ fin g],
811           auto simp add: dom_def ran_def map_default_def [abs_def])
812     qed
813     show ?thesis unfolding finfun_rec_def using True False
814       unfolding Let_def the default by(simp add: dom_def map_default_def const_update_all)
815   qed
816 qed
818 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
820 end
822 subsection {* Weak induction rule and case analysis for FinFuns *}
824 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
826 lemma finfun_weak_induct [consumes 0, case_names const update]:
827   assumes const: "\<And>b. P (\<lambda>\<^isup>f b)"
828   and update: "\<And>f a b. P f \<Longrightarrow> P (f(\<^sup>f a := b))"
829   shows "P x"
830 proof(induct x rule: Abs_finfun_induct)
831   case (Abs_finfun y)
832   then obtain b where "finite {a. y a \<noteq> b}" unfolding finfun_def by blast
833   thus ?case using `y \<in> finfun`
834   proof(induct "{a. y a \<noteq> b}" arbitrary: y rule: finite_induct)
835     case empty
836     hence "\<And>a. y a = b" by blast
837     hence "y = (\<lambda>a. b)" by(auto intro: ext)
838     hence "Abs_finfun y = finfun_const b" unfolding finfun_const_def by simp
839     thus ?case by(simp add: const)
840   next
841     case (insert a A)
842     note IH = `\<And>y. \<lbrakk> A = {a. y a \<noteq> b}; y \<in> finfun  \<rbrakk> \<Longrightarrow> P (Abs_finfun y)`
843     note y = `y \<in> finfun`
844     with `insert a A = {a. y a \<noteq> b}` `a \<notin> A`
845     have "A = {a'. (y(a := b)) a' \<noteq> b}" "y(a := b) \<in> finfun" by auto
846     from IH[OF this] have "P (finfun_update (Abs_finfun (y(a := b))) a (y a))" by(rule update)
847     thus ?case using y unfolding finfun_update_def by simp
848   qed
849 qed
851 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
853 lemma finfun_exhaust_disj: "(\<exists>b. x = finfun_const b) \<or> (\<exists>f a b. x = finfun_update f a b)"
854 by(induct x rule: finfun_weak_induct) blast+
856 lemma finfun_exhaust:
857   obtains b where "x = (\<lambda>\<^isup>f b)"
858         | f a b where "x = f(\<^sup>f a := b)"
859 by(atomize_elim)(rule finfun_exhaust_disj)
861 lemma finfun_rec_unique:
862   fixes f :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'c"
863   assumes c: "\<And>c. f (\<lambda>\<^isup>f c) = cnst c"
864   and u: "\<And>g a b. f (g(\<^sup>f a := b)) = upd g a b (f g)"
865   and c': "\<And>c. f' (\<lambda>\<^isup>f c) = cnst c"
866   and u': "\<And>g a b. f' (g(\<^sup>f a := b)) = upd g a b (f' g)"
867   shows "f = f'"
868 proof
869   fix g :: "'a \<Rightarrow>\<^isub>f 'b"
870   show "f g = f' g"
871     by(induct g rule: finfun_weak_induct)(auto simp add: c u c' u')
872 qed
875 subsection {* Function application *}
877 definition finfun_apply :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b" ("_\<^sub>f" [1000] 1000)
878 where [code del]: "finfun_apply = (\<lambda>f a. finfun_rec (\<lambda>b. b) (\<lambda>a' b c. if (a = a') then b else c) f)"
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)
885   fix b' b :: 'a
886   assume fin: "finite (UNIV :: 'b set)"
887   { fix A :: "'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)"
891       by induct auto }
892   from this[of UNIV] show "Finite_Set.fold (\<lambda>a'. If (a = a') b') b UNIV = b'" by simp
893 qed
895 lemma finfun_const_apply [simp, code]: "(\<lambda>\<^isup>f b)\<^sub>f a = b"
898 lemma finfun_upd_apply: "f(\<^sup>fa := b)\<^sub>f a' = (if a = a' then b else f\<^sub>f a')"
899   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')"
902 lemma finfun_upd_apply_same [simp]:
903   "f(\<^sup>fa := b)\<^sub>f a = b"
906 lemma finfun_upd_apply_other [simp]:
907   "a \<noteq> a' \<Longrightarrow> f(\<^sup>fa := b)\<^sub>f a' = f\<^sub>f a'"
910 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
912 lemma finfun_apply_Rep_finfun:
913   "finfun_apply = Rep_finfun"
914 proof(rule finfun_rec_unique)
915   fix c show "Rep_finfun (\<lambda>\<^isup>f c) = (\<lambda>a. c)" by(auto simp add: finfun_const_def)
916 next
917   fix g a b show "Rep_finfun g(\<^sup>f a := b) = (\<lambda>c. if c = a then b else Rep_finfun g c)"
918     by(auto simp add: finfun_update_def fun_upd_finfun Abs_finfun_inverse Rep_finfun intro: ext)
919 qed(auto intro: ext)
921 lemma finfun_ext: "(\<And>a. f\<^sub>f a = g\<^sub>f a) \<Longrightarrow> f = g"
922 by(auto simp add: finfun_apply_Rep_finfun Rep_finfun_inject[symmetric] simp del: Rep_finfun_inject intro: ext)
924 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
926 lemma expand_finfun_eq: "(f = g) = (f\<^sub>f = g\<^sub>f)"
927 by(auto intro: finfun_ext)
929 lemma finfun_const_inject [simp]: "(\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b') \<equiv> b = b'"
932 lemma finfun_const_eq_update:
933   "((\<lambda>\<^isup>f b) = f(\<^sup>f a := b')) = (b = b' \<and> (\<forall>a'. a \<noteq> a' \<longrightarrow> f\<^sub>f a' = b))"
934 by(auto simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
936 subsection {* Function composition *}
938 definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>\<^isub>f 'a \<Rightarrow> 'c \<Rightarrow>\<^isub>f 'b" (infixr "\<circ>\<^isub>f" 55)
939 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"
941 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))"
942 by(unfold_locales)(auto simp add: finfun_upd_apply intro: finfun_ext)
944 interpretation finfun_comp: finfun_rec_wf "(\<lambda>b. (\<lambda>\<^isup>f g b))" "(\<lambda>a b c. c(\<^sup>f a := g b))"
945 proof
946   fix b' b :: 'a
947   assume fin: "finite (UNIV :: 'c set)"
948   { fix A :: "'c set"
949     from fin have "finite A" by(auto intro: finite_subset)
950     hence "Finite_Set.fold (\<lambda>(a :: 'c) c. c(\<^sup>f a := g b')) (\<lambda>\<^isup>f g b) A =
951       Abs_finfun (\<lambda>a. if a \<in> A then g b' else g b)"
952       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) }
953   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')"
955 qed
957 lemma finfun_comp_const [simp, code]:
958   "g \<circ>\<^isub>f (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f g c)"
961 lemma finfun_comp_update [simp]: "g \<circ>\<^isub>f (f(\<^sup>f a := b)) = (g \<circ>\<^isub>f f)(\<^sup>f a := g b)"
962   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)"
965 lemma finfun_comp_apply [simp]:
966   "(g \<circ>\<^isub>f f)\<^sub>f = g \<circ> f\<^sub>f"
967 by(induct f rule: finfun_weak_induct)(auto simp add: finfun_upd_apply intro: ext)
969 lemma finfun_comp_comp_collapse [simp]: "f \<circ>\<^isub>f g \<circ>\<^isub>f h = (f o g) \<circ>\<^isub>f h"
970 by(induct h rule: finfun_weak_induct) simp_all
972 lemma finfun_comp_const1 [simp]: "(\<lambda>x. c) \<circ>\<^isub>f f = (\<lambda>\<^isup>f c)"
973 by(induct f rule: finfun_weak_induct)(auto intro: finfun_ext simp add: finfun_upd_apply)
975 lemma finfun_comp_id1 [simp]: "(\<lambda>x. x) \<circ>\<^isub>f f = f" "id \<circ>\<^isub>f f = f"
976 by(induct f rule: finfun_weak_induct) auto
978 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
980 lemma finfun_comp_conv_comp: "g \<circ>\<^isub>f f = Abs_finfun (g \<circ> finfun_apply f)"
981 proof -
982   have "(\<lambda>f. g \<circ>\<^isub>f f) = (\<lambda>f. Abs_finfun (g \<circ> finfun_apply f))"
983   proof(rule finfun_rec_unique)
984     { fix c show "Abs_finfun (g \<circ> (\<lambda>\<^isup>f c)\<^sub>f) = (\<lambda>\<^isup>f g c)"
986     { 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       proof -
988         obtain y where y: "y \<in> finfun" and g': "g' = Abs_finfun y" by(cases g')
989         moreover hence "(g \<circ> g'\<^sub>f) \<in> finfun" by(simp add: finfun_apply_Rep_finfun finfun_left_compose)
990         moreover have "g \<circ> y(a := b) = (g \<circ> y)(a := g b)" by(auto intro: ext)
991         ultimately show ?thesis by(simp add: finfun_comp_def finfun_update_def finfun_apply_Rep_finfun)
992       qed }
993   qed auto
994   thus ?thesis by(auto simp add: fun_eq_iff)
995 qed
997 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
999 definition finfun_comp2 :: "'b \<Rightarrow>\<^isub>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c" (infixr "\<^sub>f\<circ>" 55)
1000 where [code del]: "finfun_comp2 g f = Abs_finfun (Rep_finfun g \<circ> f)"
1002 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1004 lemma finfun_comp2_const [code, simp]: "finfun_comp2 (\<lambda>\<^isup>f c) f = (\<lambda>\<^isup>f c)"
1005 by(simp add: finfun_comp2_def finfun_const_def comp_def)
1007 lemma finfun_comp2_update:
1008   assumes inj: "inj f"
1009   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)"
1010 proof(cases "b \<in> range f")
1011   case True
1012   from inj have "\<And>x. (Rep_finfun g)(f x := c) \<circ> f = (Rep_finfun g \<circ> f)(x := c)" by(auto intro!: ext dest: injD)
1013   with inj True show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def finfun_right_compose)
1014 next
1015   case False
1016   hence "(Rep_finfun g)(b := c) \<circ> f = Rep_finfun g \<circ> f" by(auto simp add: fun_eq_iff)
1017   with False show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def)
1018 qed
1020 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1024 subsection {* Universal quantification *}
1026 definition finfun_All_except :: "'a list \<Rightarrow> 'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
1027 where [code del]: "finfun_All_except A P \<equiv> \<forall>a. a \<in> set A \<or> P\<^sub>f a"
1029 lemma finfun_All_except_const: "finfun_All_except A (\<lambda>\<^isup>f b) \<longleftrightarrow> b \<or> set A = UNIV"
1032 lemma finfun_All_except_const_finfun_UNIV_code [code]:
1033   "finfun_All_except A (\<lambda>\<^isup>f b) = (b \<or> is_list_UNIV A)"
1036 lemma finfun_All_except_update:
1037   "finfun_All_except A f(\<^sup>f a := b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
1038 by(fastforce simp add: finfun_All_except_def finfun_upd_apply)
1040 lemma finfun_All_except_update_code [code]:
1041   fixes a :: "'a :: card_UNIV"
1042   shows "finfun_All_except A (finfun_update_code f a b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
1045 definition finfun_All :: "'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
1046 where "finfun_All = finfun_All_except []"
1048 lemma finfun_All_const [simp]: "finfun_All (\<lambda>\<^isup>f b) = b"
1051 lemma finfun_All_update: "finfun_All f(\<^sup>f a := b) = (b \<and> finfun_All_except [a] f)"
1054 lemma finfun_All_All: "finfun_All P = All P\<^sub>f"
1058 definition finfun_Ex :: "'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
1059 where "finfun_Ex P = Not (finfun_All (Not \<circ>\<^isub>f P))"
1061 lemma finfun_Ex_Ex: "finfun_Ex P = Ex P\<^sub>f"
1062 unfolding finfun_Ex_def finfun_All_All by simp
1064 lemma finfun_Ex_const [simp]: "finfun_Ex (\<lambda>\<^isup>f b) = b"
1068 subsection {* A diagonal operator for FinFuns *}
1070 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)
1071 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"
1073 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))"
1074 by(unfold_locales)(simp_all add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
1076 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 proof
1078   fix b' b :: 'a
1079   assume fin: "finite (UNIV :: 'c set)"
1080   { fix A :: "'c set"
1081     interpret comp_fun_commute "\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))" by(rule finfun_Diag_aux.upd_left_comm)
1082     from fin have "finite A" by(auto intro: finite_subset)
1083     hence "Finite_Set.fold (\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))) (Pair b \<circ>\<^isub>f g) A =
1084       Abs_finfun (\<lambda>a. (if a \<in> A then b' else b, g\<^sub>f a))"
1085       by(induct)(simp_all add: finfun_const_def finfun_comp_conv_comp o_def,
1086                  auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite fun_eq_iff fin) }
1087   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"
1088     by(simp add: finfun_const_def finfun_comp_conv_comp o_def)
1089 qed
1091 lemma finfun_Diag_const1: "(\<lambda>\<^isup>f b, g)\<^sup>f = Pair b \<circ>\<^isub>f g"
1094 text {*
1095   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 *}
1098 lemma finfun_Diag_const_code [code]:
1099   "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))"
1100   "(\<lambda>\<^isup>f b, g(\<^sup>fc a := c))\<^sup>f = (\<lambda>\<^isup>f b, g)\<^sup>f(\<^sup>fc a := (b, c))"
1103 lemma finfun_Diag_update1: "(f(\<^sup>f a := b), g)\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (b, g\<^sub>f a))"
1104   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))"
1107 lemma finfun_Diag_const2: "(f, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>b. (b, c)) \<circ>\<^isub>f f"
1108 by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
1110 lemma finfun_Diag_update2: "(f, g(\<^sup>f a := c))\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (f\<^sub>f a, c))"
1111 by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
1113 lemma finfun_Diag_const_const [simp]: "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))"
1116 lemma finfun_Diag_const_update:
1117   "(\<lambda>\<^isup>f b, g(\<^sup>f a := c))\<^sup>f = (\<lambda>\<^isup>f b, g)\<^sup>f(\<^sup>f a := (b, c))"
1120 lemma finfun_Diag_update_const:
1121   "(f(\<^sup>f a := b), \<lambda>\<^isup>f c)\<^sup>f = (f, \<lambda>\<^isup>f c)\<^sup>f(\<^sup>f a := (b, c))"
1124 lemma finfun_Diag_update_update:
1125   "(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)))"
1126 by(auto simp add: finfun_Diag_update1 finfun_Diag_update2)
1128 lemma finfun_Diag_apply [simp]: "(f, g)\<^sup>f\<^sub>f = (\<lambda>x. (f\<^sub>f x, g\<^sub>f x))"
1129 by(induct f rule: finfun_weak_induct)(auto simp add: finfun_Diag_const1 finfun_Diag_update1 finfun_upd_apply intro: ext)
1131 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1133 lemma finfun_Diag_conv_Abs_finfun:
1134   "(f, g)\<^sup>f = Abs_finfun ((\<lambda>x. (Rep_finfun f x, Rep_finfun g x)))"
1135 proof -
1136   have "(\<lambda>f :: 'a \<Rightarrow>\<^isub>f 'b. (f, g)\<^sup>f) = (\<lambda>f. Abs_finfun ((\<lambda>x. (Rep_finfun f x, Rep_finfun g x))))"
1137   proof(rule finfun_rec_unique)
1138     { fix c show "Abs_finfun (\<lambda>x. (Rep_finfun (\<lambda>\<^isup>f c) x, Rep_finfun g x)) = Pair c \<circ>\<^isub>f g"
1139         by(simp add: finfun_comp_conv_comp finfun_apply_Rep_finfun o_def finfun_const_def) }
1140     { fix g' a b
1141       show "Abs_finfun (\<lambda>x. (Rep_finfun g'(\<^sup>f a := b) x, Rep_finfun g x)) =
1142             (Abs_finfun (\<lambda>x. (Rep_finfun g' x, Rep_finfun g x)))(\<^sup>f a := (b, g\<^sub>f a))"
1143         by(auto simp add: finfun_update_def fun_eq_iff finfun_apply_Rep_finfun simp del: fun_upd_apply) simp }
1145   thus ?thesis by(auto simp add: fun_eq_iff)
1146 qed
1148 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1150 lemma finfun_Diag_eq: "(f, g)\<^sup>f = (f', g')\<^sup>f \<longleftrightarrow> f = f' \<and> g = g'"
1151 by(auto simp add: expand_finfun_eq fun_eq_iff)
1153 definition finfun_fst :: "'a \<Rightarrow>\<^isub>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b"
1154 where [code]: "finfun_fst f = fst \<circ>\<^isub>f f"
1156 lemma finfun_fst_const: "finfun_fst (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f fst bc)"
1159 lemma finfun_fst_update: "finfun_fst (f(\<^sup>f a := bc)) = (finfun_fst f)(\<^sup>f a := fst bc)"
1160   and finfun_fst_update_code: "finfun_fst (finfun_update_code f a bc) = (finfun_fst f)(\<^sup>f a := fst bc)"
1163 lemma finfun_fst_comp_conv: "finfun_fst (f \<circ>\<^isub>f g) = (fst \<circ> f) \<circ>\<^isub>f g"
1166 lemma finfun_fst_conv [simp]: "finfun_fst (f, g)\<^sup>f = f"
1167 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)
1169 lemma finfun_fst_conv_Abs_finfun: "finfun_fst = (\<lambda>f. Abs_finfun (fst o Rep_finfun f))"
1170 by(simp add: finfun_fst_def [abs_def] finfun_comp_conv_comp finfun_apply_Rep_finfun)
1173 definition finfun_snd :: "'a \<Rightarrow>\<^isub>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c"
1174 where [code]: "finfun_snd f = snd \<circ>\<^isub>f f"
1176 lemma finfun_snd_const: "finfun_snd (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f snd bc)"
1179 lemma finfun_snd_update: "finfun_snd (f(\<^sup>f a := bc)) = (finfun_snd f)(\<^sup>f a := snd bc)"
1180   and finfun_snd_update_code [code]: "finfun_snd (finfun_update_code f a bc) = (finfun_snd f)(\<^sup>f a := snd bc)"
1183 lemma finfun_snd_comp_conv: "finfun_snd (f \<circ>\<^isub>f g) = (snd \<circ> f) \<circ>\<^isub>f g"
1186 lemma finfun_snd_conv [simp]: "finfun_snd (f, g)\<^sup>f = g"
1187 apply(induct f rule: finfun_weak_induct)
1188 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 done
1191 lemma finfun_snd_conv_Abs_finfun: "finfun_snd = (\<lambda>f. Abs_finfun (snd o Rep_finfun f))"
1192 by(simp add: finfun_snd_def [abs_def] finfun_comp_conv_comp finfun_apply_Rep_finfun)
1194 lemma finfun_Diag_collapse [simp]: "(finfun_fst f, finfun_snd f)\<^sup>f = f"
1195 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)
1197 subsection {* Currying for FinFuns *}
1199 definition finfun_curry :: "('a \<times> 'b) \<Rightarrow>\<^isub>f 'c \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b \<Rightarrow>\<^isub>f 'c"
1200 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)))"
1202 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))"
1203 apply(unfold_locales)
1204 apply(auto simp add: split_def finfun_update_twist finfun_upd_apply split_paired_all finfun_update_const_same)
1205 done
1207 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1209 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))"
1210 proof(unfold_locales)
1211   fix b' b :: 'b
1212   assume fin: "finite (UNIV :: ('c \<times> 'a) set)"
1213   hence fin1: "finite (UNIV :: 'c set)" and fin2: "finite (UNIV :: 'a set)"
1214     unfolding UNIV_Times_UNIV[symmetric]
1215     by(fastforce dest: finite_cartesian_productD1 finite_cartesian_productD2)+
1216   note [simp] = Abs_finfun_inverse_finite[OF fin] Abs_finfun_inverse_finite[OF fin1] Abs_finfun_inverse_finite[OF fin2]
1217   { fix A :: "('c \<times> 'a) set"
1218     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'"
1219       by(rule finfun_curry_aux.upd_left_comm)
1220     from fin have "finite A" by(auto intro: finite_subset)
1221     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))"
1222       by induct (simp_all, auto simp add: finfun_update_def finfun_const_def split_def finfun_apply_Rep_finfun intro!: arg_cong[where f="Abs_finfun"] ext) }
1223   from this[of UNIV]
1224   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'"
1226 qed
1228 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1230 lemma finfun_curry_const [simp, code]: "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
1233 lemma finfun_curry_update [simp]:
1234   "finfun_curry (f(\<^sup>f (a, b) := c)) = (finfun_curry f)(\<^sup>f a := ((finfun_curry f)\<^sub>f a)(\<^sup>f b := c))"
1235   and finfun_curry_update_code [code]:
1236   "finfun_curry (f(\<^sup>fc (a, b) := c)) = (finfun_curry f)(\<^sup>f a := ((finfun_curry f)\<^sub>f a)(\<^sup>f b := c))"
1239 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1241 lemma finfun_Abs_finfun_curry: assumes fin: "f \<in> finfun"
1242   shows "(\<lambda>a. Abs_finfun (curry f a)) \<in> finfun"
1243 proof -
1244   from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast
1245   have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force)
1246   hence "{a. curry f a \<noteq> (\<lambda>x. c)} = fst ` {ab. f ab \<noteq> c}"
1247     by(auto simp add: curry_def fun_eq_iff)
1248   with fin c have "finite {a.  Abs_finfun (curry f a) \<noteq> (\<lambda>\<^isup>f c)}"
1250   thus ?thesis unfolding finfun_def by auto
1251 qed
1253 lemma finfun_curry_conv_curry:
1254   fixes f :: "('a \<times> 'b) \<Rightarrow>\<^isub>f 'c"
1255   shows "finfun_curry f = Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun f) a))"
1256 proof -
1257   have "finfun_curry = (\<lambda>f :: ('a \<times> 'b) \<Rightarrow>\<^isub>f 'c. Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun f) a)))"
1258   proof(rule finfun_rec_unique)
1259     { fix c show "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)" by simp }
1260     { 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))"
1261         by(cases a) simp }
1262     { fix c show "Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun (\<lambda>\<^isup>f c)) a)) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
1263         by(simp add: finfun_curry_def finfun_const_def curry_def) }
1264     { fix g a b
1265       show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (Rep_finfun g(\<^sup>f a := b)) aa)) =
1266        (Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun g) a)))(\<^sup>f
1267        fst a := ((Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun g) a)))\<^sub>f (fst a))(\<^sup>f snd a := b))"
1268         by(cases a)(auto intro!: ext arg_cong[where f=Abs_finfun] simp add: finfun_curry_def finfun_update_def finfun_apply_Rep_finfun finfun_curry finfun_Abs_finfun_curry) }
1269   qed
1270   thus ?thesis by(auto simp add: fun_eq_iff)
1271 qed
1273 subsection {* Executable equality for FinFuns *}
1275 lemma eq_finfun_All_ext: "(f = g) \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>\<^isub>f (f, g)\<^sup>f)"
1276 by(simp add: expand_finfun_eq fun_eq_iff finfun_All_All o_def)
1278 instantiation finfun :: ("{card_UNIV,equal}",equal) equal begin
1279 definition eq_finfun_def [code]: "HOL.equal f g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>\<^isub>f (f, g)\<^sup>f)"
1280 instance by(intro_classes)(simp add: eq_finfun_All_ext eq_finfun_def)
1281 end
1283 lemma [code nbe]:
1284   "HOL.equal (f :: _ \<Rightarrow>\<^isub>f _) f \<longleftrightarrow> True"
1285   by (fact equal_refl)
1287 subsection {* An operator that explicitly removes all redundant updates in the generated representations *}
1289 definition finfun_clearjunk :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b"
1290 where [simp, code del]: "finfun_clearjunk = id"
1292 lemma finfun_clearjunk_const [code]: "finfun_clearjunk (\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b)"
1293 by simp
1295 lemma finfun_clearjunk_update [code]: "finfun_clearjunk (finfun_update_code f a b) = f(\<^sup>f a := b)"
1296 by simp
1298 subsection {* The domain of a FinFun as a FinFun *}
1300 definition finfun_dom :: "('a \<Rightarrow>\<^isub>f 'b) \<Rightarrow> ('a \<Rightarrow>\<^isub>f bool)"
1301 where [code del]: "finfun_dom f = Abs_finfun (\<lambda>a. f\<^sub>f a \<noteq> finfun_default f)"
1303 lemma finfun_dom_const:
1304   "finfun_dom ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = (\<lambda>\<^isup>f finite (UNIV :: 'a set) \<and> c \<noteq> undefined)"
1305 unfolding finfun_dom_def finfun_default_const
1308 text {*
1309   @{term "finfun_dom" } raises an exception when called on a FinFun whose domain is a finite type.
1310   For such FinFuns, the default value (and as such the domain) is undefined.
1311 *}
1313 lemma finfun_dom_const_code [code]:
1314   "finfun_dom ((\<lambda>\<^isup>f c) :: ('a :: card_UNIV) \<Rightarrow>\<^isub>f 'b) =
1315    (if card_UNIV (TYPE('a)) = 0 then (\<lambda>\<^isup>f False) else FinFun.code_abort (\<lambda>_. finfun_dom (\<lambda>\<^isup>f c)))"
1316 unfolding card_UNIV_eq_0_infinite_UNIV
1319 lemma finfun_dom_finfunI: "(\<lambda>a. f\<^sub>f a \<noteq> finfun_default f) \<in> finfun"
1320 using finite_finfun_default[of f]
1321 by(simp add: finfun_def finfun_apply_Rep_finfun exI[where x=False])
1323 lemma finfun_dom_update [simp]:
1324   "finfun_dom (f(\<^sup>f a := b)) = (finfun_dom f)(\<^sup>f a := (b \<noteq> finfun_default f))"
1325 unfolding finfun_dom_def finfun_update_def
1326 apply(simp add: finfun_default_update_const finfun_upd_apply finfun_dom_finfunI)
1327 apply(fold finfun_update.rep_eq)
1328 apply(simp add: finfun_upd_apply fun_eq_iff finfun_default_update_const)
1329 done
1331 lemma finfun_dom_update_code [code]:
1332   "finfun_dom (finfun_update_code f a b) = finfun_update_code (finfun_dom f) a (b \<noteq> finfun_default f)"
1333 by(simp)
1335 lemma finite_finfun_dom: "finite {x. (finfun_dom f)\<^sub>f x}"
1336 proof(induct f rule: finfun_weak_induct)
1337   case (const b)
1338   thus ?case
1339     by (cases "finite (UNIV :: 'a set) \<and> b \<noteq> undefined")
1340       (auto simp add: finfun_dom_const UNIV_def [symmetric] Set.empty_def [symmetric])
1341 next
1342   case (update f a b)
1343   have "{x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} =
1344     (if b = finfun_default f then {x. (finfun_dom f)\<^sub>f x} - {a} else insert a {x. (finfun_dom f)\<^sub>f x})"
1345     by (auto simp add: finfun_upd_apply split: split_if_asm)
1346   thus ?case using update by simp
1347 qed
1350 subsection {* The domain of a FinFun as a sorted list *}
1352 definition finfun_to_list :: "('a :: linorder) \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a list"
1353 where
1354   "finfun_to_list f = (THE xs. set xs = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs \<and> distinct xs)"
1356 lemma set_finfun_to_list [simp]: "set (finfun_to_list f) = {x. (finfun_dom f)\<^sub>f x}" (is ?thesis1)
1357   and sorted_finfun_to_list: "sorted (finfun_to_list f)" (is ?thesis2)
1358   and distinct_finfun_to_list: "distinct (finfun_to_list f)" (is ?thesis3)
1359 proof -
1360   have "?thesis1 \<and> ?thesis2 \<and> ?thesis3"
1361     unfolding finfun_to_list_def
1362     by(rule theI')(rule finite_sorted_distinct_unique finite_finfun_dom)+
1363   thus ?thesis1 ?thesis2 ?thesis3 by simp_all
1364 qed
1366 lemma finfun_const_False_conv_bot: "(\<lambda>\<^isup>f False)\<^sub>f = bot"
1367 by auto
1369 lemma finfun_const_True_conv_top: "(\<lambda>\<^isup>f True)\<^sub>f = top"
1370 by auto
1372 lemma finfun_to_list_const:
1373   "finfun_to_list ((\<lambda>\<^isup>f c) :: ('a :: {linorder} \<Rightarrow>\<^isub>f 'b)) =
1374   (if \<not> finite (UNIV :: 'a set) \<or> c = undefined then [] else THE xs. set xs = UNIV \<and> sorted xs \<and> distinct xs)"
1375 by(auto simp add: finfun_to_list_def finfun_const_False_conv_bot finfun_const_True_conv_top finfun_dom_const)
1377 lemma finfun_to_list_const_code [code]:
1378   "finfun_to_list ((\<lambda>\<^isup>f c) :: ('a :: {linorder, card_UNIV} \<Rightarrow>\<^isub>f 'b)) =
1379    (if card_UNIV (TYPE('a)) = 0 then [] else FinFun.code_abort (\<lambda>_. finfun_to_list ((\<lambda>\<^isup>f c) :: ('a \<Rightarrow>\<^isub>f 'b))))"
1380 unfolding card_UNIV_eq_0_infinite_UNIV
1383 lemma remove1_insort_insert_same:
1384   "x \<notin> set xs \<Longrightarrow> remove1 x (insort_insert x xs) = xs"
1385 by (metis insort_insert_insort remove1_insort)
1387 lemma finfun_dom_conv:
1388   "(finfun_dom f)\<^sub>f x \<longleftrightarrow> f\<^sub>f x \<noteq> finfun_default f"
1389 by(induct f rule: finfun_weak_induct)(auto simp add: finfun_dom_const finfun_default_const finfun_default_update_const finfun_upd_apply)
1391 lemma finfun_to_list_update:
1392   "finfun_to_list (f(\<^sup>f a := b)) =
1393   (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
1394 proof(subst finfun_to_list_def, rule the_equality)
1395   fix xs
1396   assume "set xs = {x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} \<and> sorted xs \<and> distinct xs"
1397   hence eq: "set xs = {x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x}"
1398     and [simp]: "sorted xs" "distinct xs" by simp_all
1399   show "xs = (if b = finfun_default f then remove1 a (finfun_to_list f) else insort_insert a (finfun_to_list f))"
1400   proof(cases "b = finfun_default f")
1401     case True [simp]
1402     show ?thesis
1403     proof(cases "(finfun_dom f)\<^sub>f a")
1404       case True
1405       have "finfun_to_list f = insort_insert a xs"
1406         unfolding finfun_to_list_def
1407       proof(rule the_equality)
1408         have "set (insort_insert a xs) = insert a (set xs)" by(simp add: set_insort_insert)
1409         also note eq also
1410         have "insert a {x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} = {x. (finfun_dom f)\<^sub>f x}" using True
1411           by(auto simp add: finfun_upd_apply split: split_if_asm)
1412         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)"
1415         fix xs'
1416         assume "set xs' = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs' \<and> distinct xs'"
1417         thus "xs' = insort_insert a xs" using 1 by(auto dest: sorted_distinct_set_unique)
1418       qed
1419       with eq True show ?thesis by(simp add: remove1_insort_insert_same)
1420     next
1421       case False
1422       hence "f\<^sub>f a = b" by(auto simp add: finfun_dom_conv)
1423       hence f: "f(\<^sup>f a := b) = f" by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
1424       from eq have "finfun_to_list f = xs" unfolding f finfun_to_list_def
1425         by(auto elim: sorted_distinct_set_unique intro!: the_equality)
1426       with eq False show ?thesis unfolding f by(simp add: remove1_idem)
1427     qed
1428   next
1429     case False
1430     show ?thesis
1431     proof(cases "(finfun_dom f)\<^sub>f a")
1432       case True
1433       have "finfun_to_list f = xs"
1434         unfolding finfun_to_list_def
1435       proof(rule the_equality)
1436         have "finfun_dom f = finfun_dom f(\<^sup>f a := b)" using False True
1437           by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
1438         with eq show 1: "set xs = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs \<and> distinct xs"
1439           by(simp del: finfun_dom_update)
1441         fix xs'
1442         assume "set xs' = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs' \<and> distinct xs'"
1443         thus "xs' = xs" using 1 by(auto elim: sorted_distinct_set_unique)
1444       qed
1445       thus ?thesis using False True eq by(simp add: insort_insert_triv)
1446     next
1447       case False
1448       have "finfun_to_list f = remove1 a xs"
1449         unfolding finfun_to_list_def
1450       proof(rule the_equality)
1451         have "set (remove1 a xs) = set xs - {a}" by simp
1452         also note eq also
1453         have "{x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} - {a} = {x. (finfun_dom f)\<^sub>f x}" using False
1454           by(auto simp add: finfun_upd_apply split: split_if_asm)
1455         finally show 1: "set (remove1 a xs) = {x. (finfun_dom f)\<^sub>f x} \<and> sorted (remove1 a xs) \<and> distinct (remove1 a xs)"
1458         fix xs'
1459         assume "set xs' = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs' \<and> distinct xs'"
1460         thus "xs' = remove1 a xs" using 1 by(blast intro: sorted_distinct_set_unique)
1461       qed
1462       thus ?thesis using False eq `b \<noteq> finfun_default f`
1463         by (simp add: insort_insert_insort insort_remove1)
1464     qed
1465   qed
1466 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)
1468 lemma finfun_to_list_update_code [code]:
1469   "finfun_to_list (finfun_update_code f a b) =
1470   (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"