src/HOL/Library/FinFun.thy
 author wenzelm Wed Jun 24 21:26:03 2015 +0200 (2015-06-24) changeset 60565 b7ee41f72add parent 60500 903bb1495239 child 60583 a645a0e6d790 permissions -rw-r--r--
clarified 'case' command;
```     1 (* Author: Andreas Lochbihler, Uni Karlsruhe *)
```
```     2
```
```     3 section \<open>Almost everywhere constant functions\<close>
```
```     4
```
```     5 theory FinFun
```
```     6 imports Cardinality
```
```     7 begin
```
```     8
```
```     9 text \<open>
```
```    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.
```
```    15
```
```    16   For details, see Formalising FinFuns - Generating Code for Functions as Data by A. Lochbihler in TPHOLs 2009.
```
```    17 \<close>
```
```    18
```
```    19
```
```    20 subsection \<open>The @{text "map_default"} operation\<close>
```
```    21
```
```    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'"
```
```    24
```
```    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)
```
```    28
```
```    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)
```
```    32
```
```    33 lemma map_default_empty [simp]: "map_default b empty = (\<lambda>a. b)"
```
```    34 by(simp add: fun_eq_iff map_default_def)
```
```    35
```
```    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'"
```
```    43 proof -
```
```    44   from infin_eq show bb': "b = b'"
```
```    45   proof
```
```    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
```
```    52   qed
```
```    53
```
```    54   show "g = g'"
```
```    55   proof
```
```    56     fix x
```
```    57     show "g x = g' x"
```
```    58     proof(cases "g x")
```
```    59       case None
```
```    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
```
```    64     next
```
```    65       case (Some c)
```
```    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
```
```    71     qed
```
```    72   qed
```
```    73 qed
```
```    74
```
```    75 subsection \<open>The finfun type\<close>
```
```    76
```
```    77 definition "finfun = {f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}"
```
```    78
```
```    79 typedef ('a,'b) finfun  ("(_ =>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set"
```
```    80   morphisms finfun_apply Abs_finfun
```
```    81 proof -
```
```    82   have "\<exists>f. finite {x. f x \<noteq> undefined}"
```
```    83   proof
```
```    84     show "finite {x. (\<lambda>y. undefined) x \<noteq> undefined}" by auto
```
```    85   qed
```
```    86   then show ?thesis unfolding finfun_def by auto
```
```    87 qed
```
```    88
```
```    89 type_notation finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
```
```    90
```
```    91 setup_lifting type_definition_finfun
```
```    92
```
```    93 lemma fun_upd_finfun: "y(a := b) \<in> finfun \<longleftrightarrow> y \<in> finfun"
```
```    94 proof -
```
```    95   { fix b'
```
```    96     have "finite {a'. (y(a := b)) a' \<noteq> b'} = finite {a'. y a' \<noteq> b'}"
```
```    97     proof(cases "b = b'")
```
```    98       case True
```
```    99       hence "{a'. (y(a := b)) a' \<noteq> b'} = {a'. y a' \<noteq> b'} - {a}" by auto
```
```   100       thus ?thesis by simp
```
```   101     next
```
```   102       case False
```
```   103       hence "{a'. (y(a := b)) a' \<noteq> b'} = insert a {a'. y a' \<noteq> b'}" by auto
```
```   104       thus ?thesis by simp
```
```   105     qed }
```
```   106   thus ?thesis unfolding finfun_def by blast
```
```   107 qed
```
```   108
```
```   109 lemma const_finfun: "(\<lambda>x. a) \<in> finfun"
```
```   110 by(auto simp add: finfun_def)
```
```   111
```
```   112 lemma finfun_left_compose:
```
```   113   assumes "y \<in> finfun"
```
```   114   shows "g \<circ> y \<in> finfun"
```
```   115 proof -
```
```   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)
```
```   120     case empty
```
```   121     hence "y = (\<lambda>a. b)" by(auto)
```
```   122     thus ?case by(simp)
```
```   123   next
```
```   124     case (insert x F)
```
```   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)
```
```   128     show ?case
```
```   129     proof(cases "g (y x) = g b")
```
```   130       case True
```
```   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
```
```   133     next
```
```   134       case False
```
```   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)
```
```   137     qed
```
```   138   qed
```
```   139   thus ?thesis unfolding finfun_def by auto
```
```   140 qed
```
```   141
```
```   142 lemma assumes "y \<in> finfun"
```
```   143   shows fst_finfun: "fst \<circ> y \<in> finfun"
```
```   144   and snd_finfun: "snd \<circ> y \<in> finfun"
```
```   145 proof -
```
```   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
```
```   154 qed
```
```   155
```
```   156 lemma map_of_finfun: "map_of xs \<in> finfun"
```
```   157 unfolding finfun_def
```
```   158 by(induct xs)(auto simp add: Collect_neg_eq Collect_conj_eq Collect_imp_eq intro: finite_subset)
```
```   159
```
```   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)
```
```   162
```
```   163 lemma finfun_right_compose:
```
```   164   assumes g: "g \<in> finfun" and inj: "inj f"
```
```   165   shows "g o f \<in> finfun"
```
```   166 proof -
```
```   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
```
```   173 qed
```
```   174
```
```   175 lemma finfun_curry:
```
```   176   assumes fin: "f \<in> finfun"
```
```   177   shows "curry f \<in> finfun" "curry f a \<in> finfun"
```
```   178 proof -
```
```   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
```
```   185
```
```   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
```
```   190 qed
```
```   191
```
```   192 bundle finfun =
```
```   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]
```
```   198
```
```   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"
```
```   203 proof
```
```   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)
```
```   208 qed simp
```
```   209
```
```   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"
```
```   213 using finite_UNIV
```
```   214 by(simp add: Abs_finfun_inject_finite)
```
```   215
```
```   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)"
```
```   219 proof(rule inj_onI)
```
```   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)
```
```   225 qed
```
```   226
```
```   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"
```
```   231   including finfun
```
```   232 proof -
```
```   233   from fin have "x \<in> finfun"
```
```   234     by(auto simp add: finfun_def intro: finite_subset)
```
```   235   thus ?thesis by simp
```
```   236 qed
```
```   237
```
```   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)
```
```   242
```
```   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)
```
```   245
```
```   246 lemma finfun_finite_UNIV_class: "finfun = (UNIV :: ('a :: finite \<Rightarrow> 'b) set)"
```
```   247 by(simp add: finfun_eq_finite_UNIV)
```
```   248
```
```   249 lemma map_default_in_finfun:
```
```   250   assumes fin: "finite (dom f)"
```
```   251   shows "map_default b f \<in> finfun"
```
```   252 unfolding finfun_def
```
```   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)
```
```   256 qed
```
```   257
```
```   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"
```
```   260 proof -
```
```   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)
```
```   269 qed
```
```   270
```
```   271
```
```   272 subsection \<open>Kernel functions for type @{typ "'a \<Rightarrow>f 'b"}\<close>
```
```   273
```
```   274 lift_definition finfun_const :: "'b \<Rightarrow> 'a \<Rightarrow>f 'b" ("K\$/ _" [0] 1)
```
```   275 is "\<lambda> b x. b" by (rule const_finfun)
```
```   276
```
```   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)
```
```   279
```
```   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)
```
```   282
```
```   283 lemma finfun_update_twice [simp]:
```
```   284   "f(a \$:= b)(a \$:= b') = f(a \$:= b')"
```
```   285 by transfer simp
```
```   286
```
```   287 lemma finfun_update_const_same: "(K\$ b)(a \$:= b) = (K\$ b)"
```
```   288 by transfer (simp add: fun_eq_iff)
```
```   289
```
```   290 subsection \<open>Code generator setup\<close>
```
```   291
```
```   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"
```
```   294
```
```   295 code_datatype finfun_const finfun_update_code
```
```   296
```
```   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)
```
```   300
```
```   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)
```
```   304
```
```   305
```
```   306 subsection \<open>Setup for quickcheck\<close>
```
```   307
```
```   308 quickcheck_generator finfun constructors: finfun_update_code, "finfun_const :: 'b \<Rightarrow> 'a \<Rightarrow>f 'b"
```
```   309
```
```   310 subsection \<open>@{text "finfun_update"} as instance of @{text "comp_fun_commute"}\<close>
```
```   311
```
```   312 interpretation finfun_update: comp_fun_commute "\<lambda>a f. f(a :: 'a \$:= b')"
```
```   313   including finfun
```
```   314 proof
```
```   315   fix a a' :: 'a
```
```   316   show "(\<lambda>f. f(a \$:= b')) \<circ> (\<lambda>f. f(a' \$:= b')) = (\<lambda>f. f(a' \$:= b')) \<circ> (\<lambda>f. f(a \$:= b'))"
```
```   317   proof
```
```   318     fix 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)
```
```   325   qed
```
```   326 qed
```
```   327
```
```   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')"
```
```   331 proof -
```
```   332   { fix A :: "'a set"
```
```   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)"
```
```   335     proof(induct)
```
```   336       case (insert x F)
```
```   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)"
```
```   338         by(auto)
```
```   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)
```
```   343 qed
```
```   344
```
```   345
```
```   346 subsection \<open>Default value for FinFuns\<close>
```
```   347
```
```   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})"
```
```   350
```
```   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"
```
```   356 proof -
```
```   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)
```
```   360     fix b'
```
```   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
```
```   365   qed
```
```   366   thus ?thesis using infin by(simp add: finfun_default_aux_def)
```
```   367 qed
```
```   368
```
```   369
```
```   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)
```
```   377 next
```
```   378   case False
```
```   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)
```
```   382 qed
```
```   383
```
```   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)")
```
```   389   case False
```
```   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'")
```
```   393     case True
```
```   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
```
```   396   next
```
```   397     case False
```
```   398     moreover
```
```   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 }
```
```   402     moreover
```
```   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
```
```   407   qed
```
```   408   with False b' show ?thesis by(auto simp del: fun_upd_apply simp add: finfun_default_aux_infinite)
```
```   409 next
```
```   410   case True thus ?thesis by(simp add: finfun_default_aux_def)
```
```   411 qed
```
```   412
```
```   413 lift_definition finfun_default :: "'a \<Rightarrow>f 'b \<Rightarrow> 'b"
```
```   414 is "finfun_default_aux" .
```
```   415
```
```   416 lemma finite_finfun_default: "finite {a. finfun_apply f a \<noteq> finfun_default f}"
```
```   417 by transfer (erule finite_finfun_default_aux)
```
```   418
```
```   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)
```
```   421
```
```   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)
```
```   425
```
```   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)
```
```   429
```
```   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)
```
```   433
```
```   434 subsection \<open>Recursion combinator and well-formedness conditions\<close>
```
```   435
```
```   436 definition finfun_rec :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow>f 'b) \<Rightarrow> 'c"
```
```   437 where [code del]:
```
```   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)"
```
```   442
```
```   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)"
```
```   449 begin
```
```   450
```
```   451
```
```   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)
```
```   454
```
```   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)
```
```   457
```
```   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)"
```
```   464 proof -
```
```   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)
```
```   468
```
```   469   from fin anf fg show ?thesis
```
```   470   proof(induct "dom f" arbitrary: f)
```
```   471     case empty
```
```   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)
```
```   474   next
```
```   475     case (insert a' A)
```
```   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>
```
```   479
```
```   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
```
```   492     finally show ?case .
```
```   493   qed
```
```   494 qed
```
```   495
```
```   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))"
```
```   502 proof -
```
```   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)
```
```   506
```
```   507   from fin anf fg show ?thesis
```
```   508   proof(induct "dom f" arbitrary: f)
```
```   509     case empty
```
```   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)
```
```   512   next
```
```   513     case (insert a' A)
```
```   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>
```
```   517
```
```   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
```
```   531     finally show ?case .
```
```   532   qed
```
```   533 qed
```
```   534
```
```   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)
```
```   537
```
```   538 lemma finite_rec_cong1:
```
```   539   assumes f: "comp_fun_commute f" and g: "comp_fun_commute g"
```
```   540   and fin: "finite A"
```
```   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"
```
```   543 proof -
```
```   544   interpret f: comp_fun_commute f by(rule f)
```
```   545   interpret g: comp_fun_commute g by(rule g)
```
```   546   { fix B
```
```   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"
```
```   550     proof(induct)
```
```   551       case empty thus ?case by simp
```
```   552     next
```
```   553       case (insert a B)
```
```   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
```
```   558       show ?case by(auto)
```
```   559     qed
```
```   560     with BsubA have "Finite_Set.fold f z B = Finite_Set.fold g z B" by blast }
```
```   561   thus ?thesis by blast
```
```   562 qed
```
```   563
```
```   564 lemma finfun_rec_upd [simp]:
```
```   565   "finfun_rec cnst upd (f(a' \$:= b')) = upd a' b' (finfun_rec cnst upd f)"
```
```   566   including finfun
```
```   567 proof -
```
```   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)
```
```   573
```
```   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)
```
```   582   next
```
```   583     fix g'
```
```   584     assume "?the f g'"
```
```   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])
```
```   590   qed
```
```   591
```
```   592   show ?thesis
```
```   593   proof(cases "b' = b")
```
```   594     case True
```
```   595     note b'b = True
```
```   596
```
```   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)
```
```   601
```
```   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")
```
```   610       case True
```
```   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
```
```   615     next
```
```   616       case False
```
```   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)
```
```   628     qed
```
```   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)
```
```   633     next
```
```   634       fix g'
```
```   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])
```
```   645     qed
```
```   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)
```
```   648   next
```
```   649     case False
```
```   650     note b'b = this
```
```   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)
```
```   662     next
```
```   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]])
```
```   671     qed
```
```   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}))"
```
```   673       by auto
```
```   674     show ?thesis
```
```   675     proof(cases "y a' = b")
```
```   676       case True
```
```   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)
```
```   688     next
```
```   689       case False
```
```   690       hence "insert a' (dom ?g) = dom ?g" by auto
```
```   691       moreover {
```
```   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)"
```
```   717           unfolding domg . }
```
```   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)
```
```   722     qed
```
```   723   qed
```
```   724 qed
```
```   725
```
```   726 end
```
```   727
```
```   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'"
```
```   731 begin
```
```   732
```
```   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)")
```
```   736   case False
```
```   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)
```
```   742   next
```
```   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)
```
```   750   qed
```
```   751   ultimately show ?thesis by(simp add: finfun_rec_def)
```
```   752 next
```
```   753   case True
```
```   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"
```
```   756   show ?thesis
```
```   757   proof(cases "c = undefined")
```
```   758     case True
```
```   759     have the: "The ?the = empty"
```
```   760     proof (rule the_equality)
```
```   761       from True show "?the empty" by(auto simp add: finfun_const_def)
```
```   762     next
```
```   763       fix g'
```
```   764       assume "?the g'"
```
```   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)
```
```   772     qed
```
```   773     show ?thesis unfolding finfun_rec_def using \<open>finite UNIV\<close> True
```
```   774       unfolding Let_def the default by(simp)
```
```   775   next
```
```   776     case False
```
```   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)
```
```   781     next
```
```   782       fix g' :: "'a \<rightharpoonup> 'b"
```
```   783       assume "?the g'"
```
```   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])
```
```   792     qed
```
```   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)
```
```   795   qed
```
```   796 qed
```
```   797
```
```   798 end
```
```   799
```
```   800 subsection \<open>Weak induction rule and case analysis for FinFuns\<close>
```
```   801
```
```   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))"
```
```   805   shows "P x"
```
```   806   including finfun
```
```   807 proof(induct x rule: Abs_finfun_induct)
```
```   808   case (Abs_finfun y)
```
```   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)
```
```   812     case empty
```
```   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)
```
```   817   next
```
```   818     case (insert a A)
```
```   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
```
```   825   qed
```
```   826 qed
```
```   827
```
```   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+
```
```   830
```
```   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)
```
```   835
```
```   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)"
```
```   842   shows "f = f'"
```
```   843 proof
```
```   844   fix g :: "'a \<Rightarrow>f 'b"
```
```   845   show "f g = f' g"
```
```   846     by(induct g rule: finfun_weak_induct)(auto simp add: c u c' u')
```
```   847 qed
```
```   848
```
```   849
```
```   850 subsection \<open>Function application\<close>
```
```   851
```
```   852 notation finfun_apply (infixl "\$" 999)
```
```   853
```
```   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
```
```   856
```
```   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)
```
```   859   fix b' b :: 'a
```
```   860   assume fin: "finite (UNIV :: 'b set)"
```
```   861   { fix A :: "'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)"
```
```   865       by induct auto }
```
```   866   from this[of UNIV] show "Finite_Set.fold (\<lambda>a'. If (a = a') b') b UNIV = b'" by simp
```
```   867 qed
```
```   868
```
```   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)
```
```   872 next
```
```   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)
```
```   875 qed auto
```
```   876
```
```   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)
```
```   880
```
```   881 lemma finfun_const_apply [simp, code]: "(K\$ b) \$ a = b"
```
```   882 by(simp add: finfun_apply_def)
```
```   883
```
```   884 lemma finfun_upd_apply_same [simp]:
```
```   885   "f(a \$:= b) \$ a = b"
```
```   886 by(simp add: finfun_upd_apply)
```
```   887
```
```   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)
```
```   891
```
```   892 lemma finfun_ext: "(\<And>a. f \$ a = g \$ a) \<Longrightarrow> f = g"
```
```   893 by(auto simp add: finfun_apply_inject[symmetric])
```
```   894
```
```   895 lemma expand_finfun_eq: "(f = g) = (op \$ f = op \$ g)"
```
```   896 by(auto intro: finfun_ext)
```
```   897
```
```   898 lemma finfun_upd_triv [simp]: "f(x \$:= f \$ x) = f"
```
```   899 by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
```
```   900
```
```   901 lemma finfun_const_inject [simp]: "(K\$ b) = (K\$ b') \<equiv> b = b'"
```
```   902 by(simp add: expand_finfun_eq fun_eq_iff)
```
```   903
```
```   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)
```
```   907
```
```   908 subsection \<open>Function composition\<close>
```
```   909
```
```   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"
```
```   912
```
```   913 notation (xsymbols) finfun_comp (infixr "\<circ>\$" 55)
```
```   914
```
```   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)
```
```   917
```
```   918 interpretation finfun_comp: finfun_rec_wf "(\<lambda>b. (K\$ g b))" "(\<lambda>a b c. c(a \$:= g b))"
```
```   919 proof
```
```   920   fix b' b :: 'a
```
```   921   assume fin: "finite (UNIV :: 'c set)"
```
```   922   { fix A :: "'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)
```
```   929 qed
```
```   930
```
```   931 lemma finfun_comp_const [simp, code]:
```
```   932   "g \<circ>\$ (K\$ c) = (K\$ g c)"
```
```   933 by(simp add: finfun_comp_def)
```
```   934
```
```   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)
```
```   939
```
```   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)
```
```   943
```
```   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
```
```   946
```
```   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)
```
```   949
```
```   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
```
```   952
```
```   953 lemma finfun_comp_conv_comp: "g \<circ>\$ f = Abs_finfun (g \<circ> op \$ f)"
```
```   954   including finfun
```
```   955 proof -
```
```   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)"
```
```   961       proof -
```
```   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)
```
```   966       qed }
```
```   967   qed auto
```
```   968   thus ?thesis by(auto simp add: fun_eq_iff)
```
```   969 qed
```
```   970
```
```   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)"
```
```   973
```
```   974 notation (xsymbol) finfun_comp2 (infixr "\$\<circ>" 55)
```
```   975
```
```   976 lemma finfun_comp2_const [code, simp]: "finfun_comp2 (K\$ c) f = (K\$ c)"
```
```   977   including finfun
```
```   978 by(simp add: finfun_comp2_def finfun_const_def comp_def)
```
```   979
```
```   980 lemma finfun_comp2_update:
```
```   981   includes finfun
```
```   982   assumes inj: "inj f"
```
```   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")
```
```   985   case True
```
```   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)
```
```   988 next
```
```   989   case False
```
```   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)
```
```   992 qed
```
```   993
```
```   994 subsection \<open>Universal quantification\<close>
```
```   995
```
```   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"
```
```   998
```
```   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)
```
```  1001
```
```  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)
```
```  1005
```
```  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)
```
```  1009
```
```  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)
```
```  1014
```
```  1015 definition finfun_All :: "'a \<Rightarrow>f bool \<Rightarrow> bool"
```
```  1016 where "finfun_All = finfun_All_except []"
```
```  1017
```
```  1018 lemma finfun_All_const [simp]: "finfun_All (K\$ b) = b"
```
```  1019 by(simp add: finfun_All_def finfun_All_except_def)
```
```  1020
```
```  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)
```
```  1023
```
```  1024 lemma finfun_All_All: "finfun_All P = All (op \$ P)"
```
```  1025 by(simp add: finfun_All_def finfun_All_except_def)
```
```  1026
```
```  1027
```
```  1028 definition finfun_Ex :: "'a \<Rightarrow>f bool \<Rightarrow> bool"
```
```  1029 where "finfun_Ex P = Not (finfun_All (Not \<circ>\$ P))"
```
```  1030
```
```  1031 lemma finfun_Ex_Ex: "finfun_Ex P = Ex (op \$ P)"
```
```  1032 unfolding finfun_Ex_def finfun_All_All by simp
```
```  1033
```
```  1034 lemma finfun_Ex_const [simp]: "finfun_Ex (K\$ b) = b"
```
```  1035 by(simp add: finfun_Ex_def)
```
```  1036
```
```  1037
```
```  1038 subsection \<open>A diagonal operator for FinFuns\<close>
```
```  1039
```
```  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"
```
```  1042
```
```  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)
```
```  1045
```
```  1046 interpretation finfun_Diag: finfun_rec_wf "\<lambda>b. Pair b \<circ>\$ g" "\<lambda>a b c. c(a \$:= (b, g \$ a))"
```
```  1047 proof
```
```  1048   fix b' b :: 'a
```
```  1049   assume fin: "finite (UNIV :: 'c set)"
```
```  1050   { fix A :: "'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)
```
```  1059 qed
```
```  1060
```
```  1061 lemma finfun_Diag_const1: "(\$K\$ b, g\$) = Pair b \<circ>\$ g"
```
```  1062 by(simp add: finfun_Diag_def)
```
```  1063
```
```  1064 text \<open>
```
```  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>\$"}.
```
```  1066 \<close>
```
```  1067
```
```  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)
```
```  1072
```
```  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)
```
```  1076
```
```  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)
```
```  1079
```
```  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)
```
```  1082
```
```  1083 lemma finfun_Diag_const_const [simp]: "(\$K\$ b, K\$ c\$) = (K\$ (b, c))"
```
```  1084 by(simp add: finfun_Diag_const1)
```
```  1085
```
```  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)
```
```  1089
```
```  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)
```
```  1093
```
```  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)
```
```  1097
```
```  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)
```
```  1100
```
```  1101 lemma finfun_Diag_conv_Abs_finfun:
```
```  1102   "(\$f, g\$) = Abs_finfun ((\<lambda>x. (f \$ x, g \$ x)))"
```
```  1103   including finfun
```
```  1104 proof -
```
```  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) }
```
```  1109     { fix g' a b
```
```  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)
```
```  1115 qed
```
```  1116
```
```  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)
```
```  1119
```
```  1120 definition finfun_fst :: "'a \<Rightarrow>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>f 'b"
```
```  1121 where [code]: "finfun_fst f = fst \<circ>\$ f"
```
```  1122
```
```  1123 lemma finfun_fst_const: "finfun_fst (K\$ bc) = (K\$ fst bc)"
```
```  1124 by(simp add: finfun_fst_def)
```
```  1125
```
```  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)
```
```  1129
```
```  1130 lemma finfun_fst_comp_conv: "finfun_fst (f \<circ>\$ g) = (fst \<circ> f) \<circ>\$ g"
```
```  1131 by(simp add: finfun_fst_def)
```
```  1132
```
```  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)
```
```  1135
```
```  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)
```
```  1138
```
```  1139
```
```  1140 definition finfun_snd :: "'a \<Rightarrow>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>f 'c"
```
```  1141 where [code]: "finfun_snd f = snd \<circ>\$ f"
```
```  1142
```
```  1143 lemma finfun_snd_const: "finfun_snd (K\$ bc) = (K\$ snd bc)"
```
```  1144 by(simp add: finfun_snd_def)
```
```  1145
```
```  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)
```
```  1149
```
```  1150 lemma finfun_snd_comp_conv: "finfun_snd (f \<circ>\$ g) = (snd \<circ> f) \<circ>\$ g"
```
```  1151 by(simp add: finfun_snd_def)
```
```  1152
```
```  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)
```
```  1156 done
```
```  1157
```
```  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)
```
```  1160
```
```  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)
```
```  1163
```
```  1164 subsection \<open>Currying for FinFuns\<close>
```
```  1165
```
```  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)))"
```
```  1168
```
```  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)
```
```  1172 done
```
```  1173
```
```  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)
```
```  1176   fix b' b :: 'b
```
```  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) }
```
```  1188   from this[of UNIV]
```
```  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)
```
```  1191 qed
```
```  1192
```
```  1193 lemma finfun_curry_const [simp, code]: "finfun_curry (K\$ c) = (K\$ K\$ c)"
```
```  1194 by(simp add: finfun_curry_def)
```
```  1195
```
```  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)
```
```  1201
```
```  1202 lemma finfun_Abs_finfun_curry: assumes fin: "f \<in> finfun"
```
```  1203   shows "(\<lambda>a. Abs_finfun (curry f a)) \<in> finfun"
```
```  1204   including finfun
```
```  1205 proof -
```
```  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
```
```  1213 qed
```
```  1214
```
```  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))"
```
```  1218   including finfun
```
```  1219 proof -
```
```  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
```
```  1223     fix f a
```
```  1224     show "finfun_curry (f(a \$:= c)) = (finfun_curry f)(fst a \$:= (finfun_curry f \$ (fst a))(snd a \$:= c))"
```
```  1225       by(cases a) simp
```
```  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)
```
```  1228     fix g b
```
```  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)
```
```  1233   qed
```
```  1234   thus ?thesis by(auto simp add: fun_eq_iff)
```
```  1235 qed
```
```  1236
```
```  1237 subsection \<open>Executable equality for FinFuns\<close>
```
```  1238
```
```  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)
```
```  1241
```
```  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)
```
```  1245 end
```
```  1246
```
```  1247 lemma [code nbe]:
```
```  1248   "HOL.equal (f :: _ \<Rightarrow>f _) f \<longleftrightarrow> True"
```
```  1249   by (fact equal_refl)
```
```  1250
```
```  1251 subsection \<open>An operator that explicitly removes all redundant updates in the generated representations\<close>
```
```  1252
```
```  1253 definition finfun_clearjunk :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow>f 'b"
```
```  1254 where [simp, code del]: "finfun_clearjunk = id"
```
```  1255
```
```  1256 lemma finfun_clearjunk_const [code]: "finfun_clearjunk (K\$ b) = (K\$ b)"
```
```  1257 by simp
```
```  1258
```
```  1259 lemma finfun_clearjunk_update [code]:
```
```  1260   "finfun_clearjunk (finfun_update_code f a b) = f(a \$:= b)"
```
```  1261 by simp
```
```  1262
```
```  1263 subsection \<open>The domain of a FinFun as a FinFun\<close>
```
```  1264
```
```  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)"
```
```  1267
```
```  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)
```
```  1272
```
```  1273 text \<open>
```
```  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.
```
```  1276 \<close>
```
```  1277
```
```  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)
```
```  1282
```
```  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])
```
```  1286
```
```  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)
```
```  1293 done
```
```  1294
```
```  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)"
```
```  1297 by(simp)
```
```  1298
```
```  1299 lemma finite_finfun_dom: "finite {x. finfun_dom f \$ x}"
```
```  1300 proof(induct f rule: finfun_weak_induct)
```
```  1301   case (const b)
```
```  1302   thus ?case
```
```  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])
```
```  1305 next
```
```  1306   case (update f a b)
```
```  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
```
```  1311 qed
```
```  1312
```
```  1313
```
```  1314 subsection \<open>The domain of a FinFun as a sorted list\<close>
```
```  1315
```
```  1316 definition finfun_to_list :: "('a :: linorder) \<Rightarrow>f 'b \<Rightarrow> 'a list"
```
```  1317 where
```
```  1318   "finfun_to_list f = (THE xs. set xs = {x. finfun_dom f \$ x} \<and> sorted xs \<and> distinct xs)"
```
```  1319
```
```  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 -
```
```  1324   have "?thesis1 \<and> ?thesis2 \<and> ?thesis3"
```
```  1325     unfolding finfun_to_list_def
```
```  1326     by(rule theI')(rule finite_sorted_distinct_unique finite_finfun_dom)+
```
```  1327   thus ?thesis1 ?thesis2 ?thesis3 by simp_all
```
```  1328 qed
```
```  1329
```
```  1330 lemma finfun_const_False_conv_bot: "op \$ (K\$ False) = bot"
```
```  1331 by auto
```
```  1332
```
```  1333 lemma finfun_const_True_conv_top: "op \$ (K\$ True) = top"
```
```  1334 by auto
```
```  1335
```
```  1336 lemma finfun_to_list_const:
```
```  1337   "finfun_to_list ((K\$ c) :: ('a :: {linorder} \<Rightarrow>f 'b)) =
```
```  1338   (if \<not> finite (UNIV :: 'a set) \<or> c = undefined then [] else THE xs. set xs = UNIV \<and> sorted xs \<and> distinct xs)"
```
```  1339 by(auto simp add: finfun_to_list_def finfun_const_False_conv_bot finfun_const_True_conv_top finfun_dom_const)
```
```  1340
```
```  1341 lemma finfun_to_list_const_code [code]:
```
```  1342   "finfun_to_list ((K\$ c) :: ('a :: {linorder, card_UNIV} \<Rightarrow>f 'b)) =
```
```  1343    (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))))"
```
```  1344 by(auto simp add: finfun_to_list_const card_UNIV card_eq_0_iff)
```
```  1345
```
```  1346 lemma remove1_insort_insert_same:
```
```  1347   "x \<notin> set xs \<Longrightarrow> remove1 x (insort_insert x xs) = xs"
```
```  1348 by (metis insort_insert_insort remove1_insort)
```
```  1349
```
```  1350 lemma finfun_dom_conv:
```
```  1351   "finfun_dom f \$ x \<longleftrightarrow> f \$ x \<noteq> finfun_default f"
```
```  1352 by(induct f rule: finfun_weak_induct)(auto simp add: finfun_dom_const finfun_default_const finfun_default_update_const finfun_upd_apply)
```
```  1353
```
```  1354 lemma finfun_to_list_update:
```
```  1355   "finfun_to_list (f(a \$:= b)) =
```
```  1356   (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
```
```  1357 proof(subst finfun_to_list_def, rule the_equality)
```
```  1358   fix xs
```
```  1359   assume "set xs = {x. finfun_dom f(a \$:= b) \$ x} \<and> sorted xs \<and> distinct xs"
```
```  1360   hence eq: "set xs = {x. finfun_dom f(a \$:= b) \$ x}"
```
```  1361     and [simp]: "sorted xs" "distinct xs" by simp_all
```
```  1362   show "xs = (if b = finfun_default f then remove1 a (finfun_to_list f) else insort_insert a (finfun_to_list f))"
```
```  1363   proof(cases "b = finfun_default f")
```
```  1364     case [simp]: True
```
```  1365     show ?thesis
```
```  1366     proof(cases "finfun_dom f \$ a")
```
```  1367       case True
```
```  1368       have "finfun_to_list f = insort_insert a xs"
```
```  1369         unfolding finfun_to_list_def
```
```  1370       proof(rule the_equality)
```
```  1371         have "set (insort_insert a xs) = insert a (set xs)" by(simp add: set_insort_insert)
```
```  1372         also note eq also
```
```  1373         have "insert a {x. finfun_dom f(a \$:= b) \$ x} = {x. finfun_dom f \$ x}" using True
```
```  1374           by(auto simp add: finfun_upd_apply split: split_if_asm)
```
```  1375         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)"
```
```  1376           by(simp add: sorted_insort_insert distinct_insort_insert)
```
```  1377
```
```  1378         fix xs'
```
```  1379         assume "set xs' = {x. finfun_dom f \$ x} \<and> sorted xs' \<and> distinct xs'"
```
```  1380         thus "xs' = insort_insert a xs" using 1 by(auto dest: sorted_distinct_set_unique)
```
```  1381       qed
```
```  1382       with eq True show ?thesis by(simp add: remove1_insort_insert_same)
```
```  1383     next
```
```  1384       case False
```
```  1385       hence "f \$ a = b" by(auto simp add: finfun_dom_conv)
```
```  1386       hence f: "f(a \$:= b) = f" by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
```
```  1387       from eq have "finfun_to_list f = xs" unfolding f finfun_to_list_def
```
```  1388         by(auto elim: sorted_distinct_set_unique intro!: the_equality)
```
```  1389       with eq False show ?thesis unfolding f by(simp add: remove1_idem)
```
```  1390     qed
```
```  1391   next
```
```  1392     case False
```
```  1393     show ?thesis
```
```  1394     proof(cases "finfun_dom f \$ a")
```
```  1395       case True
```
```  1396       have "finfun_to_list f = xs"
```
```  1397         unfolding finfun_to_list_def
```
```  1398       proof(rule the_equality)
```
```  1399         have "finfun_dom f = finfun_dom f(a \$:= b)" using False True
```
```  1400           by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
```
```  1401         with eq show 1: "set xs = {x. finfun_dom f \$ x} \<and> sorted xs \<and> distinct xs"
```
```  1402           by(simp del: finfun_dom_update)
```
```  1403
```
```  1404         fix xs'
```
```  1405         assume "set xs' = {x. finfun_dom f \$ x} \<and> sorted xs' \<and> distinct xs'"
```
```  1406         thus "xs' = xs" using 1 by(auto elim: sorted_distinct_set_unique)
```
```  1407       qed
```
```  1408       thus ?thesis using False True eq by(simp add: insort_insert_triv)
```
```  1409     next
```
```  1410       case False
```
```  1411       have "finfun_to_list f = remove1 a xs"
```
```  1412         unfolding finfun_to_list_def
```
```  1413       proof(rule the_equality)
```
```  1414         have "set (remove1 a xs) = set xs - {a}" by simp
```
```  1415         also note eq also
```
```  1416         have "{x. finfun_dom f(a \$:= b) \$ x} - {a} = {x. finfun_dom f \$ x}" using False
```
```  1417           by(auto simp add: finfun_upd_apply split: split_if_asm)
```
```  1418         finally show 1: "set (remove1 a xs) = {x. finfun_dom f \$ x} \<and> sorted (remove1 a xs) \<and> distinct (remove1 a xs)"
```
```  1419           by(simp add: sorted_remove1)
```
```  1420
```
```  1421         fix xs'
```
```  1422         assume "set xs' = {x. finfun_dom f \$ x} \<and> sorted xs' \<and> distinct xs'"
```
```  1423         thus "xs' = remove1 a xs" using 1 by(blast intro: sorted_distinct_set_unique)
```
```  1424       qed
```
```  1425       thus ?thesis using False eq \<open>b \<noteq> finfun_default f\<close>
```
```  1426         by (simp add: insort_insert_insort insort_remove1)
```
```  1427     qed
```
```  1428   qed
```
```  1429 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
```
```  1431 lemma finfun_to_list_update_code [code]:
```
```  1432   "finfun_to_list (finfun_update_code f a b) =
```
```  1433   (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
```
```  1434 by(simp add: finfun_to_list_update)
```
```  1435
```
```  1436 text \<open>More type class instantiations\<close>
```
```  1437
```
```  1438 lemma card_eq_1_iff: "card A = 1 \<longleftrightarrow> A \<noteq> {} \<and> (\<forall>x\<in>A. \<forall>y\<in>A. x = y)"
```
```  1439   (is "?lhs \<longleftrightarrow> ?rhs")
```
```  1440 proof
```
```  1441   assume ?lhs
```
```  1442   moreover {
```
```  1443     fix x y
```
```  1444     assume A: "x \<in> A" "y \<in> A" and neq: "x \<noteq> y"
```
```  1445     have "finite A" using \<open>?lhs\<close> by(simp add: card_ge_0_finite)
```
```  1446     from neq have "2 = card {x, y}" by simp
```
```  1447     also have "\<dots> \<le> card A" using A \<open>finite A\<close>
```
```  1448       by(auto intro: card_mono)
```
```  1449     finally have False using \<open>?lhs\<close> by simp }
```
```  1450   ultimately show ?rhs by auto
```
```  1451 next
```
```  1452   assume ?rhs
```
```  1453   hence "A = {THE x. x \<in> A}"
```
```  1454     by safe (auto intro: theI the_equality[symmetric])
```
```  1455   also have "card \<dots> = 1" by simp
```
```  1456   finally show ?lhs .
```
```  1457 qed
```
```  1458
```
```  1459 lemma card_UNIV_finfun:
```
```  1460   defines "F == finfun :: ('a \<Rightarrow> 'b) set"
```
```  1461   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)"
```
```  1462 proof(cases "0 < CARD('a) \<and> 0 < CARD('b) \<or> CARD('b) = 1")
```
```  1463   case True
```
```  1464   from True have "F = UNIV"
```
```  1465   proof
```
```  1466     assume b: "CARD('b) = 1"
```
```  1467     hence "\<forall>x :: 'b. x = undefined"
```
```  1468       by(auto simp add: card_eq_1_iff simp del: One_nat_def)
```
```  1469     thus ?thesis by(auto simp add: finfun_def F_def intro: exI[where x=undefined])
```
```  1470   qed(auto simp add: finfun_def card_gt_0_iff F_def intro: finite_subset[where B=UNIV])
```
```  1471   moreover have "CARD('a \<Rightarrow>f 'b) = card F"
```
```  1472     unfolding type_definition.Abs_image[OF type_definition_finfun, symmetric]
```
```  1473     by(auto intro!: card_image inj_onI simp add: Abs_finfun_inject F_def)
```
```  1474   ultimately show ?thesis by(simp add: card_fun)
```
```  1475 next
```
```  1476   case False
```
```  1477   hence infinite: "\<not> (finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set))"
```
```  1478     and b: "CARD('b) \<noteq> 1" by(simp_all add: card_eq_0_iff)
```
```  1479   from b obtain b1 b2 :: 'b where "b1 \<noteq> b2"
```
```  1480     by(auto simp add: card_eq_1_iff simp del: One_nat_def)
```
```  1481   let ?f = "\<lambda>a a' :: 'a. if a = a' then b1 else b2"
```
```  1482   from infinite have "\<not> finite (UNIV :: ('a \<Rightarrow>f 'b) set)"
```
```  1483   proof(rule contrapos_nn[OF _ conjI])
```
```  1484     assume finite: "finite (UNIV :: ('a \<Rightarrow>f 'b) set)"
```
```  1485     hence "finite F"
```
```  1486       unfolding type_definition.Abs_image[OF type_definition_finfun, symmetric] F_def
```
```  1487       by(rule finite_imageD)(auto intro: inj_onI simp add: Abs_finfun_inject)
```
```  1488     hence "finite (range ?f)"
```
```  1489       by(rule finite_subset[rotated 1])(auto simp add: F_def finfun_def \<open>b1 \<noteq> b2\<close> intro!: exI[where x=b2])
```
```  1490     thus "finite (UNIV :: 'a set)"
```
```  1491       by(rule finite_imageD)(auto intro: inj_onI simp add: fun_eq_iff \<open>b1 \<noteq> b2\<close> split: split_if_asm)
```
```  1492
```
```  1493     from finite have "finite (range (\<lambda>b. ((K\$ b) :: 'a \<Rightarrow>f 'b)))"
```
```  1494       by(rule finite_subset[rotated 1]) simp
```
```  1495     thus "finite (UNIV :: 'b set)"
```
```  1496       by(rule finite_imageD)(auto intro!: inj_onI)
```
```  1497   qed
```
```  1498   with False show ?thesis by auto
```
```  1499 qed
```
```  1500
```
```  1501 lemma finite_UNIV_finfun:
```
```  1502   "finite (UNIV :: ('a \<Rightarrow>f 'b) set) \<longleftrightarrow>
```
```  1503   (finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set) \<or> CARD('b) = 1)"
```
```  1504   (is "?lhs \<longleftrightarrow> ?rhs")
```
```  1505 proof -
```
```  1506   have "?lhs \<longleftrightarrow> CARD('a \<Rightarrow>f 'b) > 0" by(simp add: card_gt_0_iff)
```
```  1507   also have "\<dots> \<longleftrightarrow> CARD('a) > 0 \<and> CARD('b) > 0 \<or> CARD('b) = 1"
```
```  1508     by(simp add: card_UNIV_finfun)
```
```  1509   also have "\<dots> = ?rhs" by(simp add: card_gt_0_iff)
```
```  1510   finally show ?thesis .
```
```  1511 qed
```
```  1512
```
```  1513 instantiation finfun :: (finite_UNIV, card_UNIV) finite_UNIV begin
```
```  1514 definition "finite_UNIV = Phantom('a \<Rightarrow>f 'b)
```
```  1515   (let cb = of_phantom (card_UNIV :: 'b card_UNIV)
```
```  1516    in cb = 1 \<or> of_phantom (finite_UNIV :: 'a finite_UNIV) \<and> cb \<noteq> 0)"
```
```  1517 instance
```
```  1518   by intro_classes (auto simp add: finite_UNIV_finfun_def Let_def card_UNIV finite_UNIV finite_UNIV_finfun card_gt_0_iff)
```
```  1519 end
```
```  1520
```
```  1521 instantiation finfun :: (card_UNIV, card_UNIV) card_UNIV begin
```
```  1522 definition "card_UNIV = Phantom('a \<Rightarrow>f 'b)
```
```  1523   (let ca = of_phantom (card_UNIV :: 'a card_UNIV);
```
```  1524        cb = of_phantom (card_UNIV :: 'b card_UNIV)
```
```  1525    in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)"
```
```  1526 instance by intro_classes (simp add: card_UNIV_finfun_def card_UNIV Let_def card_UNIV_finfun)
```
```  1527 end
```
```  1528
```
```  1529 text \<open>Deactivate syntax again. Import theory @{text FinFun_Syntax} to reactivate it again\<close>
```
```  1530
```
```  1531 no_type_notation
```
```  1532   finfun ("(_ =>f /_)" [22, 21] 21)
```
```  1533
```
```  1534 no_type_notation (xsymbols)
```
```  1535   finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
```
```  1536
```
```  1537 no_notation
```
```  1538   finfun_const ("K\$/ _" [0] 1) and
```
```  1539   finfun_update ("_'(_ \$:= _')" [1000,0,0] 1000) and
```
```  1540   finfun_apply (infixl "\$" 999) and
```
```  1541   finfun_comp (infixr "o\$" 55) and
```
```  1542   finfun_comp2 (infixr "\$o" 55) and
```
```  1543   finfun_Diag ("(1'(\$_,/ _\$'))" [0, 0] 1000)
```
```  1544
```
```  1545 no_notation (xsymbols)
```
```  1546   finfun_comp (infixr "\<circ>\$" 55) and
```
```  1547   finfun_comp2 (infixr "\$\<circ>" 55)
```
```  1548
```
```  1549 end
```