src/HOL/Library/Fin_Fun.thy
 author huffman Thu Jun 11 09:03:24 2009 -0700 (2009-06-11) changeset 31563 ded2364d14d4 parent 31486 bee3b47e1516 child 31633 ea47e2b63588 permissions -rw-r--r--
cleaned up some proofs
```     1
```
```     2 (* Author: Andreas Lochbihler, Uni Karlsruhe *)
```
```     3
```
```     4 header {* Almost everywhere constant functions *}
```
```     5
```
```     6 theory Fin_Fun
```
```     7 imports Main Infinite_Set Enum
```
```     8 begin
```
```     9
```
```    10 text {*
```
```    11   This theory defines functions which are constant except for finitely
```
```    12   many points (FinFun) and introduces a type finfin along with a
```
```    13   number of operators for them. The code generator is set up such that
```
```    14   such functions can be represented as data in the generated code and
```
```    15   all operators are executable.
```
```    16
```
```    17   For details, see Formalising FinFuns - Generating Code for Functions as Data by A. Lochbihler in TPHOLs 2009.
```
```    18 *}
```
```    19
```
```    20
```
```    21 subsection {* The @{text "map_default"} operation *}
```
```    22
```
```    23 definition map_default :: "'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
```
```    24 where "map_default b f a \<equiv> case f a of None \<Rightarrow> b | Some b' \<Rightarrow> b'"
```
```    25
```
```    26 lemma map_default_delete [simp]:
```
```    27   "map_default b (f(a := None)) = (map_default b f)(a := b)"
```
```    28 by(simp add: map_default_def expand_fun_eq)
```
```    29
```
```    30 lemma map_default_insert:
```
```    31   "map_default b (f(a \<mapsto> b')) = (map_default b f)(a := b')"
```
```    32 by(simp add: map_default_def expand_fun_eq)
```
```    33
```
```    34 lemma map_default_empty [simp]: "map_default b empty = (\<lambda>a. b)"
```
```    35 by(simp add: expand_fun_eq map_default_def)
```
```    36
```
```    37 lemma map_default_inject:
```
```    38   fixes g g' :: "'a \<rightharpoonup> 'b"
```
```    39   assumes infin_eq: "\<not> finite (UNIV :: 'a set) \<or> b = b'"
```
```    40   and fin: "finite (dom g)" and b: "b \<notin> ran g"
```
```    41   and fin': "finite (dom g')" and b': "b' \<notin> ran g'"
```
```    42   and eq': "map_default b g = map_default b' g'"
```
```    43   shows "b = b'" "g = g'"
```
```    44 proof -
```
```    45   from infin_eq show bb': "b = b'"
```
```    46   proof
```
```    47     assume infin: "\<not> finite (UNIV :: 'a set)"
```
```    48     from fin fin' have "finite (dom g \<union> dom g')" by auto
```
```    49     with infin have "UNIV - (dom g \<union> dom g') \<noteq> {}" by(auto dest: finite_subset)
```
```    50     then obtain a where a: "a \<notin> dom g \<union> dom g'" by auto
```
```    51     hence "map_default b g a = b" "map_default b' g' a = b'" by(auto simp add: map_default_def)
```
```    52     with eq' show "b = b'" by simp
```
```    53   qed
```
```    54
```
```    55   show "g = g'"
```
```    56   proof
```
```    57     fix x
```
```    58     show "g x = g' x"
```
```    59     proof(cases "g x")
```
```    60       case None
```
```    61       hence "map_default b g x = b" by(simp add: map_default_def)
```
```    62       with bb' eq' have "map_default b' g' x = b'" by simp
```
```    63       with b' have "g' x = None" by(simp add: map_default_def ran_def split: option.split_asm)
```
```    64       with None show ?thesis by simp
```
```    65     next
```
```    66       case (Some c)
```
```    67       with b have cb: "c \<noteq> b" by(auto simp add: ran_def)
```
```    68       moreover from Some have "map_default b g x = c" by(simp add: map_default_def)
```
```    69       with eq' have "map_default b' g' x = c" by simp
```
```    70       ultimately have "g' x = Some c" using b' bb' by(auto simp add: map_default_def split: option.splits)
```
```    71       with Some show ?thesis by simp
```
```    72     qed
```
```    73   qed
```
```    74 qed
```
```    75
```
```    76 subsection {* The finfun type *}
```
```    77
```
```    78 typedef ('a,'b) finfun = "{f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}"
```
```    79 apply(auto)
```
```    80 apply(rule_tac x="\<lambda>x. arbitrary" in exI)
```
```    81 apply(auto)
```
```    82 done
```
```    83
```
```    84 syntax
```
```    85   "finfun"      :: "type \<Rightarrow> type \<Rightarrow> type"         ("(_ \<Rightarrow>\<^isub>f /_)" [22, 21] 21)
```
```    86
```
```    87 lemma fun_upd_finfun: "y(a := b) \<in> finfun \<longleftrightarrow> y \<in> finfun"
```
```    88 proof -
```
```    89   { fix b'
```
```    90     have "finite {a'. (y(a := b)) a' \<noteq> b'} = finite {a'. y a' \<noteq> b'}"
```
```    91     proof(cases "b = b'")
```
```    92       case True
```
```    93       hence "{a'. (y(a := b)) a' \<noteq> b'} = {a'. y a' \<noteq> b'} - {a}" by auto
```
```    94       thus ?thesis by simp
```
```    95     next
```
```    96       case False
```
```    97       hence "{a'. (y(a := b)) a' \<noteq> b'} = insert a {a'. y a' \<noteq> b'}" by auto
```
```    98       thus ?thesis by simp
```
```    99     qed }
```
```   100   thus ?thesis unfolding finfun_def by blast
```
```   101 qed
```
```   102
```
```   103 lemma const_finfun: "(\<lambda>x. a) \<in> finfun"
```
```   104 by(auto simp add: finfun_def)
```
```   105
```
```   106 lemma finfun_left_compose:
```
```   107   assumes "y \<in> finfun"
```
```   108   shows "g \<circ> y \<in> finfun"
```
```   109 proof -
```
```   110   from assms obtain b where "finite {a. y a \<noteq> b}"
```
```   111     unfolding finfun_def by blast
```
```   112   hence "finite {c. g (y c) \<noteq> g b}"
```
```   113   proof(induct x\<equiv>"{a. y a \<noteq> b}" arbitrary: y)
```
```   114     case empty
```
```   115     hence "y = (\<lambda>a. b)" by(auto intro: ext)
```
```   116     thus ?case by(simp)
```
```   117   next
```
```   118     case (insert x F)
```
```   119     note IH = `\<And>y. F = {a. y a \<noteq> b} \<Longrightarrow> finite {c. g (y c) \<noteq> g b}`
```
```   120     from `insert x F = {a. y a \<noteq> b}` `x \<notin> F`
```
```   121     have F: "F = {a. (y(x := b)) a \<noteq> b}" by(auto)
```
```   122     show ?case
```
```   123     proof(cases "g (y x) = g b")
```
```   124       case True
```
```   125       hence "{c. g ((y(x := b)) c) \<noteq> g b} = {c. g (y c) \<noteq> g b}" by auto
```
```   126       with IH[OF F] show ?thesis by simp
```
```   127     next
```
```   128       case False
```
```   129       hence "{c. g (y c) \<noteq> g b} = insert x {c. g ((y(x := b)) c) \<noteq> g b}" by auto
```
```   130       with IH[OF F] show ?thesis by(simp)
```
```   131     qed
```
```   132   qed
```
```   133   thus ?thesis unfolding finfun_def by auto
```
```   134 qed
```
```   135
```
```   136 lemma assumes "y \<in> finfun"
```
```   137   shows fst_finfun: "fst \<circ> y \<in> finfun"
```
```   138   and snd_finfun: "snd \<circ> y \<in> finfun"
```
```   139 proof -
```
```   140   from assms obtain b c where bc: "finite {a. y a \<noteq> (b, c)}"
```
```   141     unfolding finfun_def by auto
```
```   142   have "{a. fst (y a) \<noteq> b} \<subseteq> {a. y a \<noteq> (b, c)}"
```
```   143     and "{a. snd (y a) \<noteq> c} \<subseteq> {a. y a \<noteq> (b, c)}" by auto
```
```   144   hence "finite {a. fst (y a) \<noteq> b}"
```
```   145     and "finite {a. snd (y a) \<noteq> c}" using bc by(auto intro: finite_subset)
```
```   146   thus "fst \<circ> y \<in> finfun" "snd \<circ> y \<in> finfun"
```
```   147     unfolding finfun_def by auto
```
```   148 qed
```
```   149
```
```   150 lemma map_of_finfun: "map_of xs \<in> finfun"
```
```   151 unfolding finfun_def
```
```   152 by(induct xs)(auto simp add: Collect_neg_eq Collect_conj_eq Collect_imp_eq intro: finite_subset)
```
```   153
```
```   154 lemma Diag_finfun: "(\<lambda>x. (f x, g x)) \<in> finfun \<longleftrightarrow> f \<in> finfun \<and> g \<in> finfun"
```
```   155 by(auto intro: finite_subset simp add: Collect_neg_eq Collect_imp_eq Collect_conj_eq finfun_def)
```
```   156
```
```   157 lemma finfun_right_compose:
```
```   158   assumes g: "g \<in> finfun" and inj: "inj f"
```
```   159   shows "g o f \<in> finfun"
```
```   160 proof -
```
```   161   from g obtain b where b: "finite {a. g a \<noteq> b}" unfolding finfun_def by blast
```
```   162   moreover have "f ` {a. g (f a) \<noteq> b} \<subseteq> {a. g a \<noteq> b}" by auto
```
```   163   moreover from inj have "inj_on f {a.  g (f a) \<noteq> b}" by(rule subset_inj_on) blast
```
```   164   ultimately have "finite {a. g (f a) \<noteq> b}"
```
```   165     by(blast intro: finite_imageD[where f=f] finite_subset)
```
```   166   thus ?thesis unfolding finfun_def by auto
```
```   167 qed
```
```   168
```
```   169 lemma finfun_curry:
```
```   170   assumes fin: "f \<in> finfun"
```
```   171   shows "curry f \<in> finfun" "curry f a \<in> finfun"
```
```   172 proof -
```
```   173   from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast
```
```   174   moreover have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force)
```
```   175   hence "{a. curry f a \<noteq> (\<lambda>b. c)} = fst ` {ab. f ab \<noteq> c}"
```
```   176     by(auto simp add: curry_def expand_fun_eq)
```
```   177   ultimately have "finite {a. curry f a \<noteq> (\<lambda>b. c)}" by simp
```
```   178   thus "curry f \<in> finfun" unfolding finfun_def by blast
```
```   179
```
```   180   have "snd ` {ab. f ab \<noteq> c} = {b. \<exists>a. f (a, b) \<noteq> c}" by(force)
```
```   181   hence "{b. f (a, b) \<noteq> c} \<subseteq> snd ` {ab. f ab \<noteq> c}" by auto
```
```   182   hence "finite {b. f (a, b) \<noteq> c}" by(rule finite_subset)(rule finite_imageI[OF c])
```
```   183   thus "curry f a \<in> finfun" unfolding finfun_def by auto
```
```   184 qed
```
```   185
```
```   186 lemmas finfun_simp =
```
```   187   fst_finfun snd_finfun Abs_finfun_inverse Rep_finfun_inverse Abs_finfun_inject Rep_finfun_inject Diag_finfun finfun_curry
```
```   188 lemmas finfun_iff = const_finfun fun_upd_finfun Rep_finfun map_of_finfun
```
```   189 lemmas finfun_intro = finfun_left_compose fst_finfun snd_finfun
```
```   190
```
```   191 lemma Abs_finfun_inject_finite:
```
```   192   fixes x y :: "'a \<Rightarrow> 'b"
```
```   193   assumes fin: "finite (UNIV :: 'a set)"
```
```   194   shows "Abs_finfun x = Abs_finfun y \<longleftrightarrow> x = y"
```
```   195 proof
```
```   196   assume "Abs_finfun x = Abs_finfun y"
```
```   197   moreover have "x \<in> finfun" "y \<in> finfun" unfolding finfun_def
```
```   198     by(auto intro: finite_subset[OF _ fin])
```
```   199   ultimately show "x = y" by(simp add: Abs_finfun_inject)
```
```   200 qed simp
```
```   201
```
```   202 lemma Abs_finfun_inject_finite_class:
```
```   203   fixes x y :: "('a :: finite) \<Rightarrow> 'b"
```
```   204   shows "Abs_finfun x = Abs_finfun y \<longleftrightarrow> x = y"
```
```   205 using finite_UNIV
```
```   206 by(simp add: Abs_finfun_inject_finite)
```
```   207
```
```   208 lemma Abs_finfun_inj_finite:
```
```   209   assumes fin: "finite (UNIV :: 'a set)"
```
```   210   shows "inj (Abs_finfun :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b)"
```
```   211 proof(rule inj_onI)
```
```   212   fix x y :: "'a \<Rightarrow> 'b"
```
```   213   assume "Abs_finfun x = Abs_finfun y"
```
```   214   moreover have "x \<in> finfun" "y \<in> finfun" unfolding finfun_def
```
```   215     by(auto intro: finite_subset[OF _ fin])
```
```   216   ultimately show "x = y" by(simp add: Abs_finfun_inject)
```
```   217 qed
```
```   218
```
```   219 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
```
```   220
```
```   221 lemma Abs_finfun_inverse_finite:
```
```   222   fixes x :: "'a \<Rightarrow> 'b"
```
```   223   assumes fin: "finite (UNIV :: 'a set)"
```
```   224   shows "Rep_finfun (Abs_finfun x) = x"
```
```   225 proof -
```
```   226   from fin have "x \<in> finfun"
```
```   227     by(auto simp add: finfun_def intro: finite_subset)
```
```   228   thus ?thesis by simp
```
```   229 qed
```
```   230
```
```   231 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
```
```   232
```
```   233 lemma Abs_finfun_inverse_finite_class:
```
```   234   fixes x :: "('a :: finite) \<Rightarrow> 'b"
```
```   235   shows "Rep_finfun (Abs_finfun x) = x"
```
```   236 using finite_UNIV by(simp add: Abs_finfun_inverse_finite)
```
```   237
```
```   238 lemma finfun_eq_finite_UNIV: "finite (UNIV :: 'a set) \<Longrightarrow> (finfun :: ('a \<Rightarrow> 'b) set) = UNIV"
```
```   239 unfolding finfun_def by(auto intro: finite_subset)
```
```   240
```
```   241 lemma finfun_finite_UNIV_class: "finfun = (UNIV :: ('a :: finite \<Rightarrow> 'b) set)"
```
```   242 by(simp add: finfun_eq_finite_UNIV)
```
```   243
```
```   244 lemma map_default_in_finfun:
```
```   245   assumes fin: "finite (dom f)"
```
```   246   shows "map_default b f \<in> finfun"
```
```   247 unfolding finfun_def
```
```   248 proof(intro CollectI exI)
```
```   249   from fin show "finite {a. map_default b f a \<noteq> b}"
```
```   250     by(auto simp add: map_default_def dom_def Collect_conj_eq split: option.splits)
```
```   251 qed
```
```   252
```
```   253 lemma finfun_cases_map_default:
```
```   254   obtains b g where "f = Abs_finfun (map_default b g)" "finite (dom g)" "b \<notin> ran g"
```
```   255 proof -
```
```   256   obtain y where f: "f = Abs_finfun y" and y: "y \<in> finfun" by(cases f)
```
```   257   from y obtain b where b: "finite {a. y a \<noteq> b}" unfolding finfun_def by auto
```
```   258   let ?g = "(\<lambda>a. if y a = b then None else Some (y a))"
```
```   259   have "map_default b ?g = y" by(simp add: expand_fun_eq map_default_def)
```
```   260   with f have "f = Abs_finfun (map_default b ?g)" by simp
```
```   261   moreover from b have "finite (dom ?g)" by(auto simp add: dom_def)
```
```   262   moreover have "b \<notin> ran ?g" by(auto simp add: ran_def)
```
```   263   ultimately show ?thesis by(rule that)
```
```   264 qed
```
```   265
```
```   266
```
```   267 subsection {* Kernel functions for type @{typ "'a \<Rightarrow>\<^isub>f 'b"} *}
```
```   268
```
```   269 definition finfun_const :: "'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("\<lambda>\<^isup>f/ _" [0] 1)
```
```   270 where [code del]: "(\<lambda>\<^isup>f b) = Abs_finfun (\<lambda>x. b)"
```
```   271
```
```   272 definition finfun_update :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("_'(\<^sup>f/ _ := _')" [1000,0,0] 1000)
```
```   273 where [code del]: "f(\<^sup>fa := b) = Abs_finfun ((Rep_finfun f)(a := b))"
```
```   274
```
```   275 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
```
```   276
```
```   277 lemma finfun_update_twist: "a \<noteq> a' \<Longrightarrow> f(\<^sup>f a := b)(\<^sup>f a' := b') = f(\<^sup>f a' := b')(\<^sup>f a := b)"
```
```   278 by(simp add: finfun_update_def fun_upd_twist)
```
```   279
```
```   280 lemma finfun_update_twice [simp]:
```
```   281   "finfun_update (finfun_update f a b) a b' = finfun_update f a b'"
```
```   282 by(simp add: finfun_update_def)
```
```   283
```
```   284 lemma finfun_update_const_same: "(\<lambda>\<^isup>f b)(\<^sup>f a := b) = (\<lambda>\<^isup>f b)"
```
```   285 by(simp add: finfun_update_def finfun_const_def expand_fun_eq)
```
```   286
```
```   287 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
```
```   288
```
```   289 subsection {* Code generator setup *}
```
```   290
```
```   291 definition finfun_update_code :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("_'(\<^sup>f\<^sup>c/ _ := _')" [1000,0,0] 1000)
```
```   292 where [simp, code del]: "finfun_update_code = finfun_update"
```
```   293
```
```   294 code_datatype finfun_const finfun_update_code
```
```   295
```
```   296 lemma finfun_update_const_code [code]:
```
```   297   "(\<lambda>\<^isup>f b)(\<^sup>f a := b') = (if b = b' then (\<lambda>\<^isup>f b) else finfun_update_code (\<lambda>\<^isup>f b) a b')"
```
```   298 by(simp add: finfun_update_const_same)
```
```   299
```
```   300 lemma finfun_update_update_code [code]:
```
```   301   "(finfun_update_code f a b)(\<^sup>f a' := b') = (if a = a' then f(\<^sup>f a := b') else finfun_update_code (f(\<^sup>f a' := b')) a b)"
```
```   302 by(simp add: finfun_update_twist)
```
```   303
```
```   304
```
```   305 subsection {* Setup for quickcheck *}
```
```   306
```
```   307 notation fcomp (infixl "o>" 60)
```
```   308 notation scomp (infixl "o\<rightarrow>" 60)
```
```   309
```
```   310 definition (in term_syntax) valtermify_finfun_const ::
```
```   311   "'b\<Colon>typerep \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> ('a\<Colon>typerep \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Eval.term)" where
```
```   312   "valtermify_finfun_const y = Code_Eval.valtermify finfun_const {\<cdot>} y"
```
```   313
```
```   314 definition (in term_syntax) valtermify_finfun_update_code ::
```
```   315   "'a\<Colon>typerep \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> 'b\<Colon>typerep \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Eval.term)" where
```
```   316   "valtermify_finfun_update_code x y f = Code_Eval.valtermify finfun_update_code {\<cdot>} f {\<cdot>} x {\<cdot>} y"
```
```   317
```
```   318 instantiation finfun :: (random, random) random
```
```   319 begin
```
```   320
```
```   321 primrec random_finfun' :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
```
```   322     "random_finfun' 0 j = Quickcheck.collapse (Random.select_default 0
```
```   323        (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))
```
```   324        (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y))))"
```
```   325   | "random_finfun' (Suc_code_numeral i) j = Quickcheck.collapse (Random.select_default i
```
```   326        (random j o\<rightarrow> (\<lambda>x. random j o\<rightarrow> (\<lambda>y. random_finfun' i j o\<rightarrow> (\<lambda>f. Pair (valtermify_finfun_update_code x y f)))))
```
```   327        (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y))))"
```
```   328
```
```   329 definition
```
```   330   "random i = random_finfun' i i"
```
```   331
```
```   332 instance ..
```
```   333
```
```   334 end
```
```   335
```
```   336 lemma select_default_zero:
```
```   337   "Random.select_default 0 y y = Random.select_default 0 x y"
```
```   338   by (simp add: select_default_def)
```
```   339
```
```   340 lemma random_finfun'_code [code]:
```
```   341   "random_finfun' i j = Quickcheck.collapse (Random.select_default (i - 1)
```
```   342     (random j o\<rightarrow> (\<lambda>x. random j o\<rightarrow> (\<lambda>y. random_finfun' (i - 1) j o\<rightarrow> (\<lambda>f. Pair (valtermify_finfun_update_code x y f)))))
```
```   343     (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y))))"
```
```   344   apply (cases i rule: code_numeral.exhaust)
```
```   345   apply (simp_all only: random_finfun'.simps code_numeral_zero_minus_one Suc_code_numeral_minus_one)
```
```   346   apply (subst select_default_zero) apply (simp only:)
```
```   347   done
```
```   348
```
```   349 no_notation fcomp (infixl "o>" 60)
```
```   350 no_notation scomp (infixl "o\<rightarrow>" 60)
```
```   351
```
```   352
```
```   353 subsection {* @{text "finfun_update"} as instance of @{text "fun_left_comm"} *}
```
```   354
```
```   355 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
```
```   356
```
```   357 interpretation finfun_update: fun_left_comm "\<lambda>a f. f(\<^sup>f a :: 'a := b')"
```
```   358 proof
```
```   359   fix a' a :: 'a
```
```   360   fix b
```
```   361   have "(Rep_finfun b)(a := b', a' := b') = (Rep_finfun b)(a' := b', a := b')"
```
```   362     by(cases "a = a'")(auto simp add: fun_upd_twist)
```
```   363   thus "b(\<^sup>f a := b')(\<^sup>f a' := b') = b(\<^sup>f a' := b')(\<^sup>f a := b')"
```
```   364     by(auto simp add: finfun_update_def fun_upd_twist)
```
```   365 qed
```
```   366
```
```   367 lemma fold_finfun_update_finite_univ:
```
```   368   assumes fin: "finite (UNIV :: 'a set)"
```
```   369   shows "fold (\<lambda>a f. f(\<^sup>f a := b')) (\<lambda>\<^isup>f b) (UNIV :: 'a set) = (\<lambda>\<^isup>f b')"
```
```   370 proof -
```
```   371   { fix A :: "'a set"
```
```   372     from fin have "finite A" by(auto intro: finite_subset)
```
```   373     hence "fold (\<lambda>a f. f(\<^sup>f a := b')) (\<lambda>\<^isup>f b) A = Abs_finfun (\<lambda>a. if a \<in> A then b' else b)"
```
```   374     proof(induct)
```
```   375       case (insert x F)
```
```   376       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)"
```
```   377         by(auto intro: ext)
```
```   378       with insert show ?case
```
```   379         by(simp add: finfun_const_def fun_upd_def)(simp add: finfun_update_def Abs_finfun_inverse_finite[OF fin] fun_upd_def)
```
```   380     qed(simp add: finfun_const_def) }
```
```   381   thus ?thesis by(simp add: finfun_const_def)
```
```   382 qed
```
```   383
```
```   384
```
```   385 subsection {* Default value for FinFuns *}
```
```   386
```
```   387 definition finfun_default_aux :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"
```
```   388 where [code del]: "finfun_default_aux f = (if finite (UNIV :: 'a set) then arbitrary else THE b. finite {a. f a \<noteq> b})"
```
```   389
```
```   390 lemma finfun_default_aux_infinite:
```
```   391   fixes f :: "'a \<Rightarrow> 'b"
```
```   392   assumes infin: "infinite (UNIV :: 'a set)"
```
```   393   and fin: "finite {a. f a \<noteq> b}"
```
```   394   shows "finfun_default_aux f = b"
```
```   395 proof -
```
```   396   let ?B = "{a. f a \<noteq> b}"
```
```   397   from fin have "(THE b. finite {a. f a \<noteq> b}) = b"
```
```   398   proof(rule the_equality)
```
```   399     fix b'
```
```   400     assume "finite {a. f a \<noteq> b'}" (is "finite ?B'")
```
```   401     with infin fin have "UNIV - (?B' \<union> ?B) \<noteq> {}" by(auto dest: finite_subset)
```
```   402     then obtain a where a: "a \<notin> ?B' \<union> ?B" by auto
```
```   403     thus "b' = b" by auto
```
```   404   qed
```
```   405   thus ?thesis using infin by(simp add: finfun_default_aux_def)
```
```   406 qed
```
```   407
```
```   408
```
```   409 lemma finite_finfun_default_aux:
```
```   410   fixes f :: "'a \<Rightarrow> 'b"
```
```   411   assumes fin: "f \<in> finfun"
```
```   412   shows "finite {a. f a \<noteq> finfun_default_aux f}"
```
```   413 proof(cases "finite (UNIV :: 'a set)")
```
```   414   case True thus ?thesis using fin
```
```   415     by(auto simp add: finfun_def finfun_default_aux_def intro: finite_subset)
```
```   416 next
```
```   417   case False
```
```   418   from fin obtain b where b: "finite {a. f a \<noteq> b}" (is "finite ?B")
```
```   419     unfolding finfun_def by blast
```
```   420   with False show ?thesis by(simp add: finfun_default_aux_infinite)
```
```   421 qed
```
```   422
```
```   423 lemma finfun_default_aux_update_const:
```
```   424   fixes f :: "'a \<Rightarrow> 'b"
```
```   425   assumes fin: "f \<in> finfun"
```
```   426   shows "finfun_default_aux (f(a := b)) = finfun_default_aux f"
```
```   427 proof(cases "finite (UNIV :: 'a set)")
```
```   428   case False
```
```   429   from fin obtain b' where b': "finite {a. f a \<noteq> b'}" unfolding finfun_def by blast
```
```   430   hence "finite {a'. (f(a := b)) a' \<noteq> b'}"
```
```   431   proof(cases "b = b' \<and> f a \<noteq> b'")
```
```   432     case True
```
```   433     hence "{a. f a \<noteq> b'} = insert a {a'. (f(a := b)) a' \<noteq> b'}" by auto
```
```   434     thus ?thesis using b' by simp
```
```   435   next
```
```   436     case False
```
```   437     moreover
```
```   438     { assume "b \<noteq> b'"
```
```   439       hence "{a'. (f(a := b)) a' \<noteq> b'} = insert a {a. f a \<noteq> b'}" by auto
```
```   440       hence ?thesis using b' by simp }
```
```   441     moreover
```
```   442     { assume "b = b'" "f a = b'"
```
```   443       hence "{a'. (f(a := b)) a' \<noteq> b'} = {a. f a \<noteq> b'}" by auto
```
```   444       hence ?thesis using b' by simp }
```
```   445     ultimately show ?thesis by blast
```
```   446   qed
```
```   447   with False b' show ?thesis by(auto simp del: fun_upd_apply simp add: finfun_default_aux_infinite)
```
```   448 next
```
```   449   case True thus ?thesis by(simp add: finfun_default_aux_def)
```
```   450 qed
```
```   451
```
```   452 definition finfun_default :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'b"
```
```   453   where [code del]: "finfun_default f = finfun_default_aux (Rep_finfun f)"
```
```   454
```
```   455 lemma finite_finfun_default: "finite {a. Rep_finfun f a \<noteq> finfun_default f}"
```
```   456 unfolding finfun_default_def by(simp add: finite_finfun_default_aux)
```
```   457
```
```   458 lemma finfun_default_const: "finfun_default ((\<lambda>\<^isup>f b) :: 'a \<Rightarrow>\<^isub>f 'b) = (if finite (UNIV :: 'a set) then arbitrary else b)"
```
```   459 apply(auto simp add: finfun_default_def finfun_const_def finfun_default_aux_infinite)
```
```   460 apply(simp add: finfun_default_aux_def)
```
```   461 done
```
```   462
```
```   463 lemma finfun_default_update_const:
```
```   464   "finfun_default (f(\<^sup>f a := b)) = finfun_default f"
```
```   465 unfolding finfun_default_def finfun_update_def
```
```   466 by(simp add: finfun_default_aux_update_const)
```
```   467
```
```   468 subsection {* Recursion combinator and well-formedness conditions *}
```
```   469
```
```   470 definition finfun_rec :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<Rightarrow> 'c"
```
```   471 where [code del]:
```
```   472   "finfun_rec cnst upd f \<equiv>
```
```   473    let b = finfun_default f;
```
```   474        g = THE g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g
```
```   475    in fold (\<lambda>a. upd a (map_default b g a)) (cnst b) (dom g)"
```
```   476
```
```   477 locale finfun_rec_wf_aux =
```
```   478   fixes cnst :: "'b \<Rightarrow> 'c"
```
```   479   and upd :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c"
```
```   480   assumes upd_const_same: "upd a b (cnst b) = cnst b"
```
```   481   and upd_commute: "a \<noteq> a' \<Longrightarrow> upd a b (upd a' b' c) = upd a' b' (upd a b c)"
```
```   482   and upd_idemp: "b \<noteq> b' \<Longrightarrow> upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)"
```
```   483 begin
```
```   484
```
```   485
```
```   486 lemma upd_left_comm: "fun_left_comm (\<lambda>a. upd a (f a))"
```
```   487 by(unfold_locales)(auto intro: upd_commute)
```
```   488
```
```   489 lemma upd_upd_twice: "upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)"
```
```   490 by(cases "b \<noteq> b'")(auto simp add: fun_upd_def upd_const_same upd_idemp)
```
```   491
```
```   492 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
```
```   493
```
```   494 lemma map_default_update_const:
```
```   495   assumes fin: "finite (dom f)"
```
```   496   and anf: "a \<notin> dom f"
```
```   497   and fg: "f \<subseteq>\<^sub>m g"
```
```   498   shows "upd a d  (fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f)) =
```
```   499          fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f)"
```
```   500 proof -
```
```   501   let ?upd = "\<lambda>a. upd a (map_default d g a)"
```
```   502   let ?fr = "\<lambda>A. fold ?upd (cnst d) A"
```
```   503   interpret gwf: fun_left_comm "?upd" by(rule upd_left_comm)
```
```   504
```
```   505   from fin anf fg show ?thesis
```
```   506   proof(induct A\<equiv>"dom f" arbitrary: f)
```
```   507     case empty
```
```   508     from `{} = dom f` have "f = empty" by(auto simp add: dom_def intro: ext)
```
```   509     thus ?case by(simp add: finfun_const_def upd_const_same)
```
```   510   next
```
```   511     case (insert a' A)
```
```   512     note IH = `\<And>f.  \<lbrakk> a \<notin> dom f; f \<subseteq>\<^sub>m g; A = dom f\<rbrakk> \<Longrightarrow> upd a d (?fr (dom f)) = ?fr (dom f)`
```
```   513     note fin = `finite A` note anf = `a \<notin> dom f` note a'nA = `a' \<notin> A`
```
```   514     note domf = `insert a' A = dom f` note fg = `f \<subseteq>\<^sub>m g`
```
```   515
```
```   516     from domf obtain b where b: "f a' = Some b" by auto
```
```   517     let ?f' = "f(a' := None)"
```
```   518     have "upd a d (?fr (insert a' A)) = upd a d (upd a' (map_default d g a') (?fr A))"
```
```   519       by(subst gwf.fold_insert[OF fin a'nA]) rule
```
```   520     also from b fg have "g a' = f a'" by(auto simp add: map_le_def intro: domI dest: bspec)
```
```   521     hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def)
```
```   522     also from anf domf have "a \<noteq> a'" by auto note upd_commute[OF this]
```
```   523     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)
```
```   524     note A also note IH[OF `a \<notin> dom ?f'` `?f' \<subseteq>\<^sub>m g` A]
```
```   525     also have "upd a' (map_default d f a') (?fr (dom (f(a' := None)))) = ?fr (dom f)"
```
```   526       unfolding domf[symmetric] gwf.fold_insert[OF fin a'nA] ga' unfolding A ..
```
```   527     also have "insert a' (dom ?f') = dom f" using domf by auto
```
```   528     finally show ?case .
```
```   529   qed
```
```   530 qed
```
```   531
```
```   532 lemma map_default_update_twice:
```
```   533   assumes fin: "finite (dom f)"
```
```   534   and anf: "a \<notin> dom f"
```
```   535   and fg: "f \<subseteq>\<^sub>m g"
```
```   536   shows "upd a d'' (upd a d' (fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f))) =
```
```   537          upd a d'' (fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f))"
```
```   538 proof -
```
```   539   let ?upd = "\<lambda>a. upd a (map_default d g a)"
```
```   540   let ?fr = "\<lambda>A. fold ?upd (cnst d) A"
```
```   541   interpret gwf: fun_left_comm "?upd" by(rule upd_left_comm)
```
```   542
```
```   543   from fin anf fg show ?thesis
```
```   544   proof(induct A\<equiv>"dom f" arbitrary: f)
```
```   545     case empty
```
```   546     from `{} = dom f` have "f = empty" by(auto simp add: dom_def intro: ext)
```
```   547     thus ?case by(auto simp add: finfun_const_def finfun_update_def upd_upd_twice)
```
```   548   next
```
```   549     case (insert a' A)
```
```   550     note IH = `\<And>f. \<lbrakk>a \<notin> dom f; f \<subseteq>\<^sub>m g; A = dom f\<rbrakk> \<Longrightarrow> upd a d'' (upd a d' (?fr (dom f))) = upd a d'' (?fr (dom f))`
```
```   551     note fin = `finite A` note anf = `a \<notin> dom f` note a'nA = `a' \<notin> A`
```
```   552     note domf = `insert a' A = dom f` note fg = `f \<subseteq>\<^sub>m g`
```
```   553
```
```   554     from domf obtain b where b: "f a' = Some b" by auto
```
```   555     let ?f' = "f(a' := None)"
```
```   556     let ?b' = "case f a' of None \<Rightarrow> d | Some b \<Rightarrow> b"
```
```   557     from domf have "upd a d'' (upd a d' (?fr (dom f))) = upd a d'' (upd a d' (?fr (insert a' A)))" by simp
```
```   558     also note gwf.fold_insert[OF fin a'nA]
```
```   559     also from b fg have "g a' = f a'" by(auto simp add: map_le_def intro: domI dest: bspec)
```
```   560     hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def)
```
```   561     also from anf domf have ana': "a \<noteq> a'" by auto note upd_commute[OF this]
```
```   562     also note upd_commute[OF ana']
```
```   563     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)
```
```   564     note A also note IH[OF `a \<notin> dom ?f'` `?f' \<subseteq>\<^sub>m g` A]
```
```   565     also note upd_commute[OF ana'[symmetric]] also note ga'[symmetric] also note A[symmetric]
```
```   566     also note gwf.fold_insert[symmetric, OF fin a'nA] also note domf
```
```   567     finally show ?case .
```
```   568   qed
```
```   569 qed
```
```   570
```
```   571 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
```
```   572
```
```   573 lemma map_default_eq_id [simp]: "map_default d ((\<lambda>a. Some (f a)) |` {a. f a \<noteq> d}) = f"
```
```   574 by(auto simp add: map_default_def restrict_map_def intro: ext)
```
```   575
```
```   576 lemma finite_rec_cong1:
```
```   577   assumes f: "fun_left_comm f" and g: "fun_left_comm g"
```
```   578   and fin: "finite A"
```
```   579   and eq: "\<And>a. a \<in> A \<Longrightarrow> f a = g a"
```
```   580   shows "fold f z A = fold g z A"
```
```   581 proof -
```
```   582   interpret f: fun_left_comm f by(rule f)
```
```   583   interpret g: fun_left_comm g by(rule g)
```
```   584   { fix B
```
```   585     assume BsubA: "B \<subseteq> A"
```
```   586     with fin have "finite B" by(blast intro: finite_subset)
```
```   587     hence "B \<subseteq> A \<Longrightarrow> fold f z B = fold g z B"
```
```   588     proof(induct)
```
```   589       case empty thus ?case by simp
```
```   590     next
```
```   591       case (insert a B)
```
```   592       note finB = `finite B` note anB = `a \<notin> B` note sub = `insert a B \<subseteq> A`
```
```   593       note IH = `B \<subseteq> A \<Longrightarrow> fold f z B = fold g z B`
```
```   594       from sub anB have BpsubA: "B \<subset> A" and BsubA: "B \<subseteq> A" and aA: "a \<in> A" by auto
```
```   595       from IH[OF BsubA] eq[OF aA] finB anB
```
```   596       show ?case by(auto)
```
```   597     qed
```
```   598     with BsubA have "fold f z B = fold g z B" by blast }
```
```   599   thus ?thesis by blast
```
```   600 qed
```
```   601
```
```   602 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
```
```   603
```
```   604 lemma finfun_rec_upd [simp]:
```
```   605   "finfun_rec cnst upd (f(\<^sup>f a' := b')) = upd a' b' (finfun_rec cnst upd f)"
```
```   606 proof -
```
```   607   obtain b where b: "b = finfun_default f" by auto
```
```   608   let ?the = "\<lambda>f g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g"
```
```   609   obtain g where g: "g = The (?the f)" by blast
```
```   610   obtain y where f: "f = Abs_finfun y" and y: "y \<in> finfun" by (cases f)
```
```   611   from f y b have bfin: "finite {a. y a \<noteq> b}" by(simp add: finfun_default_def finite_finfun_default_aux)
```
```   612
```
```   613   let ?g = "(\<lambda>a. Some (y a)) |` {a. y a \<noteq> b}"
```
```   614   from bfin have fing: "finite (dom ?g)" by auto
```
```   615   have bran: "b \<notin> ran ?g" by(auto simp add: ran_def restrict_map_def)
```
```   616   have yg: "y = map_default b ?g" by simp
```
```   617   have gg: "g = ?g" unfolding g
```
```   618   proof(rule the_equality)
```
```   619     from f y bfin show "?the f ?g"
```
```   620       by(auto)(simp add: restrict_map_def ran_def split: split_if_asm)
```
```   621   next
```
```   622     fix g'
```
```   623     assume "?the f g'"
```
```   624     hence fin': "finite (dom g')" and ran': "b \<notin> ran g'"
```
```   625       and eq: "Abs_finfun (map_default b ?g) = Abs_finfun (map_default b g')" using f yg by auto
```
```   626     from fin' fing have "map_default b ?g \<in> finfun" "map_default b g' \<in> finfun" by(blast intro: map_default_in_finfun)+
```
```   627     with eq have "map_default b ?g = map_default b g'" by simp
```
```   628     with fing bran fin' ran' show "g' = ?g" by(rule map_default_inject[OF disjI2[OF refl], THEN sym])
```
```   629   qed
```
```   630
```
```   631   show ?thesis
```
```   632   proof(cases "b' = b")
```
```   633     case True
```
```   634     note b'b = True
```
```   635
```
```   636     let ?g' = "(\<lambda>a. Some ((y(a' := b)) a)) |` {a. (y(a' := b)) a \<noteq> b}"
```
```   637     from bfin b'b have fing': "finite (dom ?g')"
```
```   638       by(auto simp add: Collect_conj_eq Collect_imp_eq intro: finite_subset)
```
```   639     have brang': "b \<notin> ran ?g'" by(auto simp add: ran_def restrict_map_def)
```
```   640
```
```   641     let ?b' = "\<lambda>a. case ?g' a of None \<Rightarrow> b | Some b \<Rightarrow> b"
```
```   642     let ?b = "map_default b ?g"
```
```   643     from upd_left_comm upd_left_comm fing'
```
```   644     have "fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g') = fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g')"
```
```   645       by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b b map_default_def)
```
```   646     also interpret gwf: fun_left_comm "\<lambda>a. upd a (?b a)" by(rule upd_left_comm)
```
```   647     have "fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g') = upd a' b' (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g))"
```
```   648     proof(cases "y a' = b")
```
```   649       case True
```
```   650       with b'b have g': "?g' = ?g" by(auto simp add: restrict_map_def intro: ext)
```
```   651       from True have a'ndomg: "a' \<notin> dom ?g" by auto
```
```   652       from f b'b b show ?thesis unfolding g'
```
```   653         by(subst map_default_update_const[OF fing a'ndomg map_le_refl, symmetric]) simp
```
```   654     next
```
```   655       case False
```
```   656       hence domg: "dom ?g = insert a' (dom ?g')" by auto
```
```   657       from False b'b have a'ndomg': "a' \<notin> dom ?g'" by auto
```
```   658       have "fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g')) =
```
```   659             upd a' (?b a') (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'))"
```
```   660         using fing' a'ndomg' unfolding b'b by(rule gwf.fold_insert)
```
```   661       hence "upd a' b (fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g'))) =
```
```   662              upd a' b (upd a' (?b a') (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g')))" by simp
```
```   663       also from b'b have g'leg: "?g' \<subseteq>\<^sub>m ?g" by(auto simp add: restrict_map_def map_le_def)
```
```   664       note map_default_update_twice[OF fing' a'ndomg' this, of b "?b a'" b]
```
```   665       also note map_default_update_const[OF fing' a'ndomg' g'leg, of b]
```
```   666       finally show ?thesis unfolding b'b domg[unfolded b'b] by(rule sym)
```
```   667     qed
```
```   668     also have "The (?the (f(\<^sup>f a' := b'))) = ?g'"
```
```   669     proof(rule the_equality)
```
```   670       from f y b b'b brang' fing' show "?the (f(\<^sup>f a' := b')) ?g'"
```
```   671         by(auto simp del: fun_upd_apply simp add: finfun_update_def)
```
```   672     next
```
```   673       fix g'
```
```   674       assume "?the (f(\<^sup>f a' := b')) g'"
```
```   675       hence fin': "finite (dom g')" and ran': "b \<notin> ran g'"
```
```   676         and eq: "f(\<^sup>f a' := b') = Abs_finfun (map_default b g')"
```
```   677         by(auto simp del: fun_upd_apply)
```
```   678       from fin' fing' have "map_default b g' \<in> finfun" "map_default b ?g' \<in> finfun"
```
```   679         by(blast intro: map_default_in_finfun)+
```
```   680       with eq f b'b b have "map_default b ?g' = map_default b g'"
```
```   681         by(simp del: fun_upd_apply add: finfun_update_def)
```
```   682       with fing' brang' fin' ran' show "g' = ?g'"
```
```   683         by(rule map_default_inject[OF disjI2[OF refl], THEN sym])
```
```   684     qed
```
```   685     ultimately show ?thesis unfolding finfun_rec_def Let_def b gg[unfolded g b] using bfin b'b b
```
```   686       by(simp only: finfun_default_update_const map_default_def)
```
```   687   next
```
```   688     case False
```
```   689     note b'b = this
```
```   690     let ?g' = "?g(a' \<mapsto> b')"
```
```   691     let ?b' = "map_default b ?g'"
```
```   692     let ?b = "map_default b ?g"
```
```   693     from fing have fing': "finite (dom ?g')" by auto
```
```   694     from bran b'b have bnrang': "b \<notin> ran ?g'" by(auto simp add: ran_def)
```
```   695     have ffmg': "map_default b ?g' = y(a' := b')" by(auto intro: ext simp add: map_default_def restrict_map_def)
```
```   696     with f y have f_Abs: "f(\<^sup>f a' := b') = Abs_finfun (map_default b ?g')" by(auto simp add: finfun_update_def)
```
```   697     have g': "The (?the (f(\<^sup>f a' := b'))) = ?g'"
```
```   698     proof
```
```   699       from fing' bnrang' f_Abs show "?the (f(\<^sup>f a' := b')) ?g'" by(auto simp add: finfun_update_def restrict_map_def)
```
```   700     next
```
```   701       fix g' assume "?the (f(\<^sup>f a' := b')) g'"
```
```   702       hence f': "f(\<^sup>f a' := b') = Abs_finfun (map_default b g')"
```
```   703         and fin': "finite (dom g')" and brang': "b \<notin> ran g'" by auto
```
```   704       from fing' fin' have "map_default b ?g' \<in> finfun" "map_default b g' \<in> finfun"
```
```   705         by(auto intro: map_default_in_finfun)
```
```   706       with f' f_Abs have "map_default b g' = map_default b ?g'" by simp
```
```   707       with fin' brang' fing' bnrang' show "g' = ?g'"
```
```   708         by(rule map_default_inject[OF disjI2[OF refl]])
```
```   709     qed
```
```   710     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}))"
```
```   711       by auto
```
```   712     show ?thesis
```
```   713     proof(cases "y a' = b")
```
```   714       case True
```
```   715       hence a'ndomg: "a' \<notin> dom ?g" by auto
```
```   716       from f y b'b True have yff: "y = map_default b (?g' |` dom ?g)"
```
```   717         by(auto simp add: restrict_map_def map_default_def intro!: ext)
```
```   718       hence f': "f = Abs_finfun (map_default b (?g' |` dom ?g))" using f by simp
```
```   719       interpret g'wf: fun_left_comm "\<lambda>a. upd a (?b' a)" by(rule upd_left_comm)
```
```   720       from upd_left_comm upd_left_comm fing
```
```   721       have "fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g) = fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g)"
```
```   722         by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b True map_default_def)
```
```   723       thus ?thesis unfolding finfun_rec_def Let_def finfun_default_update_const b[symmetric]
```
```   724         unfolding g' g[symmetric] gg g'wf.fold_insert[OF fing a'ndomg, of "cnst b", folded dom]
```
```   725         by -(rule arg_cong2[where f="upd a'"], simp_all add: map_default_def)
```
```   726     next
```
```   727       case False
```
```   728       hence "insert a' (dom ?g) = dom ?g" by auto
```
```   729       moreover {
```
```   730         let ?g'' = "?g(a' := None)"
```
```   731         let ?b'' = "map_default b ?g''"
```
```   732         from False have domg: "dom ?g = insert a' (dom ?g'')" by auto
```
```   733         from False have a'ndomg'': "a' \<notin> dom ?g''" by auto
```
```   734         have fing'': "finite (dom ?g'')" by(rule finite_subset[OF _ fing]) auto
```
```   735         have bnrang'': "b \<notin> ran ?g''" by(auto simp add: ran_def restrict_map_def)
```
```   736         interpret gwf: fun_left_comm "\<lambda>a. upd a (?b a)" by(rule upd_left_comm)
```
```   737         interpret g'wf: fun_left_comm "\<lambda>a. upd a (?b' a)" by(rule upd_left_comm)
```
```   738         have "upd a' b' (fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g''))) =
```
```   739               upd a' b' (upd a' (?b a') (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')))"
```
```   740           unfolding gwf.fold_insert[OF fing'' a'ndomg''] f ..
```
```   741         also have g''leg: "?g |` dom ?g'' \<subseteq>\<^sub>m ?g" by(auto simp add: map_le_def)
```
```   742         have "dom (?g |` dom ?g'') = dom ?g''" by auto
```
```   743         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",
```
```   744                                      unfolded this, OF fing'' a'ndomg'' g''leg]
```
```   745         also have b': "b' = ?b' a'" by(auto simp add: map_default_def)
```
```   746         from upd_left_comm upd_left_comm fing''
```
```   747         have "fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'') = fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g'')"
```
```   748           by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b map_default_def)
```
```   749         with b' have "upd a' b' (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')) =
```
```   750                      upd a' (?b' a') (fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g''))" by simp
```
```   751         also note g'wf.fold_insert[OF fing'' a'ndomg'', symmetric]
```
```   752         finally have "upd a' b' (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g)) =
```
```   753                    fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g)"
```
```   754           unfolding domg . }
```
```   755       ultimately have "fold (\<lambda>a. upd a (?b' a)) (cnst b) (insert a' (dom ?g)) =
```
```   756                     upd a' b' (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g))" by simp
```
```   757       thus ?thesis unfolding finfun_rec_def Let_def finfun_default_update_const b[symmetric] g[symmetric] g' dom[symmetric]
```
```   758         using b'b gg by(simp add: map_default_insert)
```
```   759     qed
```
```   760   qed
```
```   761 qed
```
```   762
```
```   763 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
```
```   764
```
```   765 end
```
```   766
```
```   767 locale finfun_rec_wf = finfun_rec_wf_aux +
```
```   768   assumes const_update_all:
```
```   769   "finite (UNIV :: 'a set) \<Longrightarrow> fold (\<lambda>a. upd a b') (cnst b) (UNIV :: 'a set) = cnst b'"
```
```   770 begin
```
```   771
```
```   772 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
```
```   773
```
```   774 lemma finfun_rec_const [simp]:
```
```   775   "finfun_rec cnst upd (\<lambda>\<^isup>f c) = cnst c"
```
```   776 proof(cases "finite (UNIV :: 'a set)")
```
```   777   case False
```
```   778   hence "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = c" by(simp add: finfun_default_const)
```
```   779   moreover have "(THE g :: 'a \<rightharpoonup> 'b. (\<lambda>\<^isup>f c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g) = empty"
```
```   780   proof
```
```   781     show "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c empty) \<and> finite (dom empty) \<and> c \<notin> ran empty"
```
```   782       by(auto simp add: finfun_const_def)
```
```   783   next
```
```   784     fix g :: "'a \<rightharpoonup> 'b"
```
```   785     assume "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g"
```
```   786     hence g: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c g)" and fin: "finite (dom g)" and ran: "c \<notin> ran g" by blast+
```
```   787     from g map_default_in_finfun[OF fin, of c] have "map_default c g = (\<lambda>a. c)"
```
```   788       by(simp add: finfun_const_def)
```
```   789     moreover have "map_default c empty = (\<lambda>a. c)" by simp
```
```   790     ultimately show "g = empty" by-(rule map_default_inject[OF disjI2[OF refl] fin ran], auto)
```
```   791   qed
```
```   792   ultimately show ?thesis by(simp add: finfun_rec_def)
```
```   793 next
```
```   794   case True
```
```   795   hence default: "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = arbitrary" by(simp add: finfun_default_const)
```
```   796   let ?the = "\<lambda>g :: 'a \<rightharpoonup> 'b. (\<lambda>\<^isup>f c) = Abs_finfun (map_default arbitrary g) \<and> finite (dom g) \<and> arbitrary \<notin> ran g"
```
```   797   show ?thesis
```
```   798   proof(cases "c = arbitrary")
```
```   799     case True
```
```   800     have the: "The ?the = empty"
```
```   801     proof
```
```   802       from True show "?the empty" by(auto simp add: finfun_const_def)
```
```   803     next
```
```   804       fix g'
```
```   805       assume "?the g'"
```
```   806       hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default arbitrary g')"
```
```   807         and fin: "finite (dom g')" and g: "arbitrary \<notin> ran g'" by simp_all
```
```   808       from fin have "map_default arbitrary g' \<in> finfun" by(rule map_default_in_finfun)
```
```   809       with fg have "map_default arbitrary g' = (\<lambda>a. c)"
```
```   810         by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1])
```
```   811       with True show "g' = empty"
```
```   812         by -(rule map_default_inject(2)[OF _ fin g], auto)
```
```   813     qed
```
```   814     show ?thesis unfolding finfun_rec_def using `finite UNIV` True
```
```   815       unfolding Let_def the default by(simp)
```
```   816   next
```
```   817     case False
```
```   818     have the: "The ?the = (\<lambda>a :: 'a. Some c)"
```
```   819     proof
```
```   820       from False True show "?the (\<lambda>a :: 'a. Some c)"
```
```   821         by(auto simp add: map_default_def_raw finfun_const_def dom_def ran_def)
```
```   822     next
```
```   823       fix g' :: "'a \<rightharpoonup> 'b"
```
```   824       assume "?the g'"
```
```   825       hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default arbitrary g')"
```
```   826         and fin: "finite (dom g')" and g: "arbitrary \<notin> ran g'" by simp_all
```
```   827       from fin have "map_default arbitrary g' \<in> finfun" by(rule map_default_in_finfun)
```
```   828       with fg have "map_default arbitrary g' = (\<lambda>a. c)"
```
```   829         by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1])
```
```   830       with True False show "g' = (\<lambda>a::'a. Some c)"
```
```   831         by -(rule map_default_inject(2)[OF _ fin g], auto simp add: dom_def ran_def map_default_def_raw)
```
```   832     qed
```
```   833     show ?thesis unfolding finfun_rec_def using True False
```
```   834       unfolding Let_def the default by(simp add: dom_def map_default_def const_update_all)
```
```   835   qed
```
```   836 qed
```
```   837
```
```   838 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
```
```   839
```
```   840 end
```
```   841
```
```   842 subsection {* Weak induction rule and case analysis for FinFuns *}
```
```   843
```
```   844 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
```
```   845
```
```   846 lemma finfun_weak_induct [consumes 0, case_names const update]:
```
```   847   assumes const: "\<And>b. P (\<lambda>\<^isup>f b)"
```
```   848   and update: "\<And>f a b. P f \<Longrightarrow> P (f(\<^sup>f a := b))"
```
```   849   shows "P x"
```
```   850 proof(induct x rule: Abs_finfun_induct)
```
```   851   case (Abs_finfun y)
```
```   852   then obtain b where "finite {a. y a \<noteq> b}" unfolding finfun_def by blast
```
```   853   thus ?case using `y \<in> finfun`
```
```   854   proof(induct x\<equiv>"{a. y a \<noteq> b}" arbitrary: y rule: finite_induct)
```
```   855     case empty
```
```   856     hence "\<And>a. y a = b" by blast
```
```   857     hence "y = (\<lambda>a. b)" by(auto intro: ext)
```
```   858     hence "Abs_finfun y = finfun_const b" unfolding finfun_const_def by simp
```
```   859     thus ?case by(simp add: const)
```
```   860   next
```
```   861     case (insert a A)
```
```   862     note IH = `\<And>y. \<lbrakk> y \<in> finfun; A = {a. y a \<noteq> b} \<rbrakk> \<Longrightarrow> P (Abs_finfun y)`
```
```   863     note y = `y \<in> finfun`
```
```   864     with `insert a A = {a. y a \<noteq> b}` `a \<notin> A`
```
```   865     have "y(a := b) \<in> finfun" "A = {a'. (y(a := b)) a' \<noteq> b}" by auto
```
```   866     from IH[OF this] have "P (finfun_update (Abs_finfun (y(a := b))) a (y a))" by(rule update)
```
```   867     thus ?case using y unfolding finfun_update_def by simp
```
```   868   qed
```
```   869 qed
```
```   870
```
```   871 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
```
```   872
```
```   873 lemma finfun_exhaust_disj: "(\<exists>b. x = finfun_const b) \<or> (\<exists>f a b. x = finfun_update f a b)"
```
```   874 by(induct x rule: finfun_weak_induct) blast+
```
```   875
```
```   876 lemma finfun_exhaust:
```
```   877   obtains b where "x = (\<lambda>\<^isup>f b)"
```
```   878         | f a b where "x = f(\<^sup>f a := b)"
```
```   879 by(atomize_elim)(rule finfun_exhaust_disj)
```
```   880
```
```   881 lemma finfun_rec_unique:
```
```   882   fixes f :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'c"
```
```   883   assumes c: "\<And>c. f (\<lambda>\<^isup>f c) = cnst c"
```
```   884   and u: "\<And>g a b. f (g(\<^sup>f a := b)) = upd g a b (f g)"
```
```   885   and c': "\<And>c. f' (\<lambda>\<^isup>f c) = cnst c"
```
```   886   and u': "\<And>g a b. f' (g(\<^sup>f a := b)) = upd g a b (f' g)"
```
```   887   shows "f = f'"
```
```   888 proof
```
```   889   fix g :: "'a \<Rightarrow>\<^isub>f 'b"
```
```   890   show "f g = f' g"
```
```   891     by(induct g rule: finfun_weak_induct)(auto simp add: c u c' u')
```
```   892 qed
```
```   893
```
```   894
```
```   895 subsection {* Function application *}
```
```   896
```
```   897 definition finfun_apply :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b" ("_\<^sub>f" [1000] 1000)
```
```   898 where [code del]: "finfun_apply = (\<lambda>f a. finfun_rec (\<lambda>b. b) (\<lambda>a' b c. if (a = a') then b else c) f)"
```
```   899
```
```   900 interpretation finfun_apply_aux: finfun_rec_wf_aux "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c"
```
```   901 by(unfold_locales) auto
```
```   902
```
```   903 interpretation finfun_apply: finfun_rec_wf "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c"
```
```   904 proof(unfold_locales)
```
```   905   fix b' b :: 'a
```
```   906   assume fin: "finite (UNIV :: 'b set)"
```
```   907   { fix A :: "'b set"
```
```   908     interpret fun_left_comm "\<lambda>a'. If (a = a') b'" by(rule finfun_apply_aux.upd_left_comm)
```
```   909     from fin have "finite A" by(auto intro: finite_subset)
```
```   910     hence "fold (\<lambda>a'. If (a = a') b') b A = (if a \<in> A then b' else b)"
```
```   911       by induct auto }
```
```   912   from this[of UNIV] show "fold (\<lambda>a'. If (a = a') b') b UNIV = b'" by simp
```
```   913 qed
```
```   914
```
```   915 lemma finfun_const_apply [simp, code]: "(\<lambda>\<^isup>f b)\<^sub>f a = b"
```
```   916 by(simp add: finfun_apply_def)
```
```   917
```
```   918 lemma finfun_upd_apply: "f(\<^sup>fa := b)\<^sub>f a' = (if a = a' then b else f\<^sub>f a')"
```
```   919   and finfun_upd_apply_code [code]: "(finfun_update_code f a b)\<^sub>f a' = (if a = a' then b else f\<^sub>f a')"
```
```   920 by(simp_all add: finfun_apply_def)
```
```   921
```
```   922 lemma finfun_upd_apply_same [simp]:
```
```   923   "f(\<^sup>fa := b)\<^sub>f a = b"
```
```   924 by(simp add: finfun_upd_apply)
```
```   925
```
```   926 lemma finfun_upd_apply_other [simp]:
```
```   927   "a \<noteq> a' \<Longrightarrow> f(\<^sup>fa := b)\<^sub>f a' = f\<^sub>f a'"
```
```   928 by(simp add: finfun_upd_apply)
```
```   929
```
```   930 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
```
```   931
```
```   932 lemma finfun_apply_Rep_finfun:
```
```   933   "finfun_apply = Rep_finfun"
```
```   934 proof(rule finfun_rec_unique)
```
```   935   fix c show "Rep_finfun (\<lambda>\<^isup>f c) = (\<lambda>a. c)" by(auto simp add: finfun_const_def)
```
```   936 next
```
```   937   fix g a b show "Rep_finfun g(\<^sup>f a := b) = (\<lambda>c. if c = a then b else Rep_finfun g c)"
```
```   938     by(auto simp add: finfun_update_def fun_upd_finfun Abs_finfun_inverse Rep_finfun intro: ext)
```
```   939 qed(auto intro: ext)
```
```   940
```
```   941 lemma finfun_ext: "(\<And>a. f\<^sub>f a = g\<^sub>f a) \<Longrightarrow> f = g"
```
```   942 by(auto simp add: finfun_apply_Rep_finfun Rep_finfun_inject[symmetric] simp del: Rep_finfun_inject intro: ext)
```
```   943
```
```   944 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
```
```   945
```
```   946 lemma expand_finfun_eq: "(f = g) = (f\<^sub>f = g\<^sub>f)"
```
```   947 by(auto intro: finfun_ext)
```
```   948
```
```   949 lemma finfun_const_inject [simp]: "(\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b') \<equiv> b = b'"
```
```   950 by(simp add: expand_finfun_eq expand_fun_eq)
```
```   951
```
```   952 lemma finfun_const_eq_update:
```
```   953   "((\<lambda>\<^isup>f b) = f(\<^sup>f a := b')) = (b = b' \<and> (\<forall>a'. a \<noteq> a' \<longrightarrow> f\<^sub>f a' = b))"
```
```   954 by(auto simp add: expand_finfun_eq expand_fun_eq finfun_upd_apply)
```
```   955
```
```   956 subsection {* Function composition *}
```
```   957
```
```   958 definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>\<^isub>f 'a \<Rightarrow> 'c \<Rightarrow>\<^isub>f 'b" (infixr "\<circ>\<^isub>f" 55)
```
```   959 where [code del]: "g \<circ>\<^isub>f f  = finfun_rec (\<lambda>b. (\<lambda>\<^isup>f g b)) (\<lambda>a b c. c(\<^sup>f a := g b)) f"
```
```   960
```
```   961 interpretation finfun_comp_aux: finfun_rec_wf_aux "(\<lambda>b. (\<lambda>\<^isup>f g b))" "(\<lambda>a b c. c(\<^sup>f a := g b))"
```
```   962 by(unfold_locales)(auto simp add: finfun_upd_apply intro: finfun_ext)
```
```   963
```
```   964 interpretation finfun_comp: finfun_rec_wf "(\<lambda>b. (\<lambda>\<^isup>f g b))" "(\<lambda>a b c. c(\<^sup>f a := g b))"
```
```   965 proof
```
```   966   fix b' b :: 'a
```
```   967   assume fin: "finite (UNIV :: 'c set)"
```
```   968   { fix A :: "'c set"
```
```   969     from fin have "finite A" by(auto intro: finite_subset)
```
```   970     hence "fold (\<lambda>(a :: 'c) c. c(\<^sup>f a := g b')) (\<lambda>\<^isup>f g b) A =
```
```   971       Abs_finfun (\<lambda>a. if a \<in> A then g b' else g b)"
```
```   972       by induct (simp_all add: finfun_const_def, auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite expand_fun_eq fin) }
```
```   973   from this[of UNIV] show "fold (\<lambda>(a :: 'c) c. c(\<^sup>f a := g b')) (\<lambda>\<^isup>f g b) UNIV = (\<lambda>\<^isup>f g b')"
```
```   974     by(simp add: finfun_const_def)
```
```   975 qed
```
```   976
```
```   977 lemma finfun_comp_const [simp, code]:
```
```   978   "g \<circ>\<^isub>f (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f g c)"
```
```   979 by(simp add: finfun_comp_def)
```
```   980
```
```   981 lemma finfun_comp_update [simp]: "g \<circ>\<^isub>f (f(\<^sup>f a := b)) = (g \<circ>\<^isub>f f)(\<^sup>f a := g b)"
```
```   982   and finfun_comp_update_code [code]: "g \<circ>\<^isub>f (finfun_update_code f a b) = finfun_update_code (g \<circ>\<^isub>f f) a (g b)"
```
```   983 by(simp_all add: finfun_comp_def)
```
```   984
```
```   985 lemma finfun_comp_apply [simp]:
```
```   986   "(g \<circ>\<^isub>f f)\<^sub>f = g \<circ> f\<^sub>f"
```
```   987 by(induct f rule: finfun_weak_induct)(auto simp add: finfun_upd_apply intro: ext)
```
```   988
```
```   989 lemma finfun_comp_comp_collapse [simp]: "f \<circ>\<^isub>f g \<circ>\<^isub>f h = (f o g) \<circ>\<^isub>f h"
```
```   990 by(induct h rule: finfun_weak_induct) simp_all
```
```   991
```
```   992 lemma finfun_comp_const1 [simp]: "(\<lambda>x. c) \<circ>\<^isub>f f = (\<lambda>\<^isup>f c)"
```
```   993 by(induct f rule: finfun_weak_induct)(auto intro: finfun_ext simp add: finfun_upd_apply)
```
```   994
```
```   995 lemma finfun_comp_id1 [simp]: "(\<lambda>x. x) \<circ>\<^isub>f f = f" "id \<circ>\<^isub>f f = f"
```
```   996 by(induct f rule: finfun_weak_induct) auto
```
```   997
```
```   998 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
```
```   999
```
```  1000 lemma finfun_comp_conv_comp: "g \<circ>\<^isub>f f = Abs_finfun (g \<circ> finfun_apply f)"
```
```  1001 proof -
```
```  1002   have "(\<lambda>f. g \<circ>\<^isub>f f) = (\<lambda>f. Abs_finfun (g \<circ> finfun_apply f))"
```
```  1003   proof(rule finfun_rec_unique)
```
```  1004     { fix c show "Abs_finfun (g \<circ> (\<lambda>\<^isup>f c)\<^sub>f) = (\<lambda>\<^isup>f g c)"
```
```  1005         by(simp add: finfun_comp_def o_def)(simp add: finfun_const_def) }
```
```  1006     { fix g' a b show "Abs_finfun (g \<circ> g'(\<^sup>f a := b)\<^sub>f) = (Abs_finfun (g \<circ> g'\<^sub>f))(\<^sup>f a := g b)"
```
```  1007       proof -
```
```  1008         obtain y where y: "y \<in> finfun" and g': "g' = Abs_finfun y" by(cases g')
```
```  1009         moreover hence "(g \<circ> g'\<^sub>f) \<in> finfun" by(simp add: finfun_apply_Rep_finfun finfun_left_compose)
```
```  1010         moreover have "g \<circ> y(a := b) = (g \<circ> y)(a := g b)" by(auto intro: ext)
```
```  1011         ultimately show ?thesis by(simp add: finfun_comp_def finfun_update_def finfun_apply_Rep_finfun)
```
```  1012       qed }
```
```  1013   qed auto
```
```  1014   thus ?thesis by(auto simp add: expand_fun_eq)
```
```  1015 qed
```
```  1016
```
```  1017 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
```
```  1018
```
```  1019
```
```  1020
```
```  1021 definition finfun_comp2 :: "'b \<Rightarrow>\<^isub>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c" (infixr "\<^sub>f\<circ>" 55)
```
```  1022 where [code del]: "finfun_comp2 g f = Abs_finfun (Rep_finfun g \<circ> f)"
```
```  1023
```
```  1024 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
```
```  1025
```
```  1026 lemma finfun_comp2_const [code, simp]: "finfun_comp2 (\<lambda>\<^isup>f c) f = (\<lambda>\<^isup>f c)"
```
```  1027 by(simp add: finfun_comp2_def finfun_const_def comp_def)
```
```  1028
```
```  1029 lemma finfun_comp2_update:
```
```  1030   assumes inj: "inj f"
```
```  1031   shows "finfun_comp2 (g(\<^sup>f b := c)) f = (if b \<in> range f then (finfun_comp2 g f)(\<^sup>f inv f b := c) else finfun_comp2 g f)"
```
```  1032 proof(cases "b \<in> range f")
```
```  1033   case True
```
```  1034   from inj have "\<And>x. (Rep_finfun g)(f x := c) \<circ> f = (Rep_finfun g \<circ> f)(x := c)" by(auto intro!: ext dest: injD)
```
```  1035   with inj True show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def finfun_right_compose)
```
```  1036 next
```
```  1037   case False
```
```  1038   hence "(Rep_finfun g)(b := c) \<circ> f = Rep_finfun g \<circ> f" by(auto simp add: expand_fun_eq)
```
```  1039   with False show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def)
```
```  1040 qed
```
```  1041
```
```  1042 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
```
```  1043
```
```  1044 subsection {* A type class for computing the cardinality of a type's universe *}
```
```  1045
```
```  1046 class card_UNIV =
```
```  1047   fixes card_UNIV :: "'a itself \<Rightarrow> nat"
```
```  1048   assumes card_UNIV: "card_UNIV x = card (UNIV :: 'a set)"
```
```  1049 begin
```
```  1050
```
```  1051 lemma card_UNIV_neq_0_finite_UNIV:
```
```  1052   "card_UNIV x \<noteq> 0 \<longleftrightarrow> finite (UNIV :: 'a set)"
```
```  1053 by(simp add: card_UNIV card_eq_0_iff)
```
```  1054
```
```  1055 lemma card_UNIV_ge_0_finite_UNIV:
```
```  1056   "card_UNIV x > 0 \<longleftrightarrow> finite (UNIV :: 'a set)"
```
```  1057 by(auto simp add: card_UNIV intro: card_ge_0_finite finite_UNIV_card_ge_0)
```
```  1058
```
```  1059 lemma card_UNIV_eq_0_infinite_UNIV:
```
```  1060   "card_UNIV x = 0 \<longleftrightarrow> infinite (UNIV :: 'a set)"
```
```  1061 by(simp add: card_UNIV card_eq_0_iff)
```
```  1062
```
```  1063 definition is_list_UNIV :: "'a list \<Rightarrow> bool"
```
```  1064 where "is_list_UNIV xs = (let c = card_UNIV (TYPE('a)) in if c = 0 then False else size (remdups xs) = c)"
```
```  1065
```
```  1066 lemma is_list_UNIV_iff:
```
```  1067   fixes xs :: "'a list"
```
```  1068   shows "is_list_UNIV xs \<longleftrightarrow> set xs = UNIV"
```
```  1069 proof
```
```  1070   assume "is_list_UNIV xs"
```
```  1071   hence c: "card_UNIV (TYPE('a)) > 0" and xs: "size (remdups xs) = card_UNIV (TYPE('a))"
```
```  1072     unfolding is_list_UNIV_def by(simp_all add: Let_def split: split_if_asm)
```
```  1073   from c have fin: "finite (UNIV :: 'a set)" by(auto simp add: card_UNIV_ge_0_finite_UNIV)
```
```  1074   have "card (set (remdups xs)) = size (remdups xs)" by(subst distinct_card) auto
```
```  1075   also note set_remdups
```
```  1076   finally show "set xs = UNIV" using fin unfolding xs card_UNIV by-(rule card_eq_UNIV_imp_eq_UNIV)
```
```  1077 next
```
```  1078   assume xs: "set xs = UNIV"
```
```  1079   from finite_set[of xs] have fin: "finite (UNIV :: 'a set)" unfolding xs .
```
```  1080   hence "card_UNIV (TYPE ('a)) \<noteq> 0" unfolding card_UNIV_neq_0_finite_UNIV .
```
```  1081   moreover have "size (remdups xs) = card (set (remdups xs))"
```
```  1082     by(subst distinct_card) auto
```
```  1083   ultimately show "is_list_UNIV xs" using xs by(simp add: is_list_UNIV_def Let_def card_UNIV)
```
```  1084 qed
```
```  1085
```
```  1086 lemma card_UNIV_eq_0_is_list_UNIV_False:
```
```  1087   assumes cU0: "card_UNIV x = 0"
```
```  1088   shows "is_list_UNIV = (\<lambda>xs. False)"
```
```  1089 proof(rule ext)
```
```  1090   fix xs :: "'a list"
```
```  1091   from cU0 have "infinite (UNIV :: 'a set)"
```
```  1092     by(auto simp only: card_UNIV_eq_0_infinite_UNIV)
```
```  1093   moreover have "finite (set xs)" by(rule finite_set)
```
```  1094   ultimately have "(UNIV :: 'a set) \<noteq> set xs" by(auto simp del: finite_set)
```
```  1095   thus "is_list_UNIV xs = False" unfolding is_list_UNIV_iff by simp
```
```  1096 qed
```
```  1097
```
```  1098 end
```
```  1099
```
```  1100 subsection {* Instantiations for @{text "card_UNIV"} *}
```
```  1101
```
```  1102 subsubsection {* @{typ "nat"} *}
```
```  1103
```
```  1104 instantiation nat :: card_UNIV begin
```
```  1105
```
```  1106 definition card_UNIV_nat_def:
```
```  1107   "card_UNIV_class.card_UNIV = (\<lambda>a :: nat itself. 0)"
```
```  1108
```
```  1109 instance proof
```
```  1110   fix x :: "nat itself"
```
```  1111   show "card_UNIV x = card (UNIV :: nat set)"
```
```  1112     unfolding card_UNIV_nat_def by simp
```
```  1113 qed
```
```  1114
```
```  1115 end
```
```  1116
```
```  1117 subsubsection {* @{typ "int"} *}
```
```  1118
```
```  1119 instantiation int :: card_UNIV begin
```
```  1120
```
```  1121 definition card_UNIV_int_def:
```
```  1122   "card_UNIV_class.card_UNIV = (\<lambda>a :: int itself. 0)"
```
```  1123
```
```  1124 instance proof
```
```  1125   fix x :: "int itself"
```
```  1126   show "card_UNIV x = card (UNIV :: int set)"
```
```  1127     unfolding card_UNIV_int_def by simp
```
```  1128 qed
```
```  1129
```
```  1130 end
```
```  1131
```
```  1132 subsubsection {* @{typ "'a list"} *}
```
```  1133
```
```  1134 instantiation list :: (type) card_UNIV begin
```
```  1135
```
```  1136 definition card_UNIV_list_def:
```
```  1137   "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a list itself. 0)"
```
```  1138
```
```  1139 instance proof
```
```  1140   fix x :: "'a list itself"
```
```  1141   show "card_UNIV x = card (UNIV :: 'a list set)"
```
```  1142     unfolding card_UNIV_list_def by(simp add: infinite_UNIV_listI)
```
```  1143 qed
```
```  1144
```
```  1145 end
```
```  1146
```
```  1147 subsubsection {* @{typ "unit"} *}
```
```  1148
```
```  1149 lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
```
```  1150   unfolding UNIV_unit by simp
```
```  1151
```
```  1152 instantiation unit :: card_UNIV begin
```
```  1153
```
```  1154 definition card_UNIV_unit_def:
```
```  1155   "card_UNIV_class.card_UNIV = (\<lambda>a :: unit itself. 1)"
```
```  1156
```
```  1157 instance proof
```
```  1158   fix x :: "unit itself"
```
```  1159   show "card_UNIV x = card (UNIV :: unit set)"
```
```  1160     by(simp add: card_UNIV_unit_def card_UNIV_unit)
```
```  1161 qed
```
```  1162
```
```  1163 end
```
```  1164
```
```  1165 subsubsection {* @{typ "bool"} *}
```
```  1166
```
```  1167 lemma card_UNIV_bool: "card (UNIV :: bool set) = 2"
```
```  1168   unfolding UNIV_bool by simp
```
```  1169
```
```  1170 instantiation bool :: card_UNIV begin
```
```  1171
```
```  1172 definition card_UNIV_bool_def:
```
```  1173   "card_UNIV_class.card_UNIV = (\<lambda>a :: bool itself. 2)"
```
```  1174
```
```  1175 instance proof
```
```  1176   fix x :: "bool itself"
```
```  1177   show "card_UNIV x = card (UNIV :: bool set)"
```
```  1178     by(simp add: card_UNIV_bool_def card_UNIV_bool)
```
```  1179 qed
```
```  1180
```
```  1181 end
```
```  1182
```
```  1183 subsubsection {* @{typ "char"} *}
```
```  1184
```
```  1185 lemma card_UNIV_char: "card (UNIV :: char set) = 256"
```
```  1186 proof -
```
```  1187   from enum_distinct
```
```  1188   have "card (set (enum :: char list)) = length (enum :: char list)"
```
```  1189     by - (rule distinct_card)
```
```  1190   also have "set enum = (UNIV :: char set)" by auto
```
```  1191   also note enum_chars
```
```  1192   finally show ?thesis by (simp add: chars_def)
```
```  1193 qed
```
```  1194
```
```  1195 instantiation char :: card_UNIV begin
```
```  1196
```
```  1197 definition card_UNIV_char_def:
```
```  1198   "card_UNIV_class.card_UNIV = (\<lambda>a :: char itself. 256)"
```
```  1199
```
```  1200 instance proof
```
```  1201   fix x :: "char itself"
```
```  1202   show "card_UNIV x = card (UNIV :: char set)"
```
```  1203     by(simp add: card_UNIV_char_def card_UNIV_char)
```
```  1204 qed
```
```  1205
```
```  1206 end
```
```  1207
```
```  1208 subsubsection {* @{typ "'a \<times> 'b"} *}
```
```  1209
```
```  1210 instantiation * :: (card_UNIV, card_UNIV) card_UNIV begin
```
```  1211
```
```  1212 definition card_UNIV_product_def:
```
```  1213   "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<times> 'b) itself. card_UNIV (TYPE('a)) * card_UNIV (TYPE('b)))"
```
```  1214
```
```  1215 instance proof
```
```  1216   fix x :: "('a \<times> 'b) itself"
```
```  1217   show "card_UNIV x = card (UNIV :: ('a \<times> 'b) set)"
```
```  1218     by(simp add: card_UNIV_product_def card_UNIV UNIV_Times_UNIV[symmetric] card_cartesian_product del: UNIV_Times_UNIV)
```
```  1219 qed
```
```  1220
```
```  1221 end
```
```  1222
```
```  1223 subsubsection {* @{typ "'a + 'b"} *}
```
```  1224
```
```  1225 instantiation "+" :: (card_UNIV, card_UNIV) card_UNIV begin
```
```  1226
```
```  1227 definition card_UNIV_sum_def:
```
```  1228   "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a + 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
```
```  1229                            in if ca \<noteq> 0 \<and> cb \<noteq> 0 then ca + cb else 0)"
```
```  1230
```
```  1231 instance proof
```
```  1232   fix x :: "('a + 'b) itself"
```
```  1233   show "card_UNIV x = card (UNIV :: ('a + 'b) set)"
```
```  1234     by (auto simp add: card_UNIV_sum_def card_UNIV card_eq_0_iff UNIV_Plus_UNIV[symmetric] finite_Plus_iff Let_def card_Plus simp del: UNIV_Plus_UNIV dest!: card_ge_0_finite)
```
```  1235 qed
```
```  1236
```
```  1237 end
```
```  1238
```
```  1239 subsubsection {* @{typ "'a \<Rightarrow> 'b"} *}
```
```  1240
```
```  1241 instantiation "fun" :: (card_UNIV, card_UNIV) card_UNIV begin
```
```  1242
```
```  1243 definition card_UNIV_fun_def:
```
```  1244   "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<Rightarrow> 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
```
```  1245                            in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)"
```
```  1246
```
```  1247 instance proof
```
```  1248   fix x :: "('a \<Rightarrow> 'b) itself"
```
```  1249
```
```  1250   { assume "0 < card (UNIV :: 'a set)"
```
```  1251     and "0 < card (UNIV :: 'b set)"
```
```  1252     hence fina: "finite (UNIV :: 'a set)" and finb: "finite (UNIV :: 'b set)"
```
```  1253       by(simp_all only: card_ge_0_finite)
```
```  1254     from finite_distinct_list[OF finb] obtain bs
```
```  1255       where bs: "set bs = (UNIV :: 'b set)" and distb: "distinct bs" by blast
```
```  1256     from finite_distinct_list[OF fina] obtain as
```
```  1257       where as: "set as = (UNIV :: 'a set)" and dista: "distinct as" by blast
```
```  1258     have cb: "card (UNIV :: 'b set) = length bs"
```
```  1259       unfolding bs[symmetric] distinct_card[OF distb] ..
```
```  1260     have ca: "card (UNIV :: 'a set) = length as"
```
```  1261       unfolding as[symmetric] distinct_card[OF dista] ..
```
```  1262     let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (n_lists (length as) bs)"
```
```  1263     have "UNIV = set ?xs"
```
```  1264     proof(rule UNIV_eq_I)
```
```  1265       fix f :: "'a \<Rightarrow> 'b"
```
```  1266       from as have "f = the \<circ> map_of (zip as (map f as))"
```
```  1267         by(auto simp add: map_of_zip_map intro: ext)
```
```  1268       thus "f \<in> set ?xs" using bs by(auto simp add: set_n_lists)
```
```  1269     qed
```
```  1270     moreover have "distinct ?xs" unfolding distinct_map
```
```  1271     proof(intro conjI distinct_n_lists distb inj_onI)
```
```  1272       fix xs ys :: "'b list"
```
```  1273       assume xs: "xs \<in> set (n_lists (length as) bs)"
```
```  1274         and ys: "ys \<in> set (n_lists (length as) bs)"
```
```  1275         and eq: "the \<circ> map_of (zip as xs) = the \<circ> map_of (zip as ys)"
```
```  1276       from xs ys have [simp]: "length xs = length as" "length ys = length as"
```
```  1277         by(simp_all add: length_n_lists_elem)
```
```  1278       have "map_of (zip as xs) = map_of (zip as ys)"
```
```  1279       proof
```
```  1280         fix x
```
```  1281         from as bs have "\<exists>y. map_of (zip as xs) x = Some y" "\<exists>y. map_of (zip as ys) x = Some y"
```
```  1282           by(simp_all add: map_of_zip_is_Some[symmetric])
```
```  1283         with eq show "map_of (zip as xs) x = map_of (zip as ys) x"
```
```  1284           by(auto dest: fun_cong[where x=x])
```
```  1285       qed
```
```  1286       with dista show "xs = ys" by(simp add: map_of_zip_inject)
```
```  1287     qed
```
```  1288     hence "card (set ?xs) = length ?xs" by(simp only: distinct_card)
```
```  1289     moreover have "length ?xs = length bs ^ length as" by(simp add: length_n_lists)
```
```  1290     ultimately have "card (UNIV :: ('a \<Rightarrow> 'b) set) = card (UNIV :: 'b set) ^ card (UNIV :: 'a set)"
```
```  1291       using cb ca by simp }
```
```  1292   moreover {
```
```  1293     assume cb: "card (UNIV :: 'b set) = Suc 0"
```
```  1294     then obtain b where b: "UNIV = {b :: 'b}" by(auto simp add: card_Suc_eq)
```
```  1295     have eq: "UNIV = {\<lambda>x :: 'a. b ::'b}"
```
```  1296     proof(rule UNIV_eq_I)
```
```  1297       fix x :: "'a \<Rightarrow> 'b"
```
```  1298       { fix y
```
```  1299         have "x y \<in> UNIV" ..
```
```  1300         hence "x y = b" unfolding b by simp }
```
```  1301       thus "x \<in> {\<lambda>x. b}" by(auto intro: ext)
```
```  1302     qed
```
```  1303     have "card (UNIV :: ('a \<Rightarrow> 'b) set) = Suc 0" unfolding eq by simp }
```
```  1304   ultimately show "card_UNIV x = card (UNIV :: ('a \<Rightarrow> 'b) set)"
```
```  1305     unfolding card_UNIV_fun_def card_UNIV Let_def
```
```  1306     by(auto simp del: One_nat_def)(auto simp add: card_eq_0_iff dest: finite_fun_UNIVD2 finite_fun_UNIVD1)
```
```  1307 qed
```
```  1308
```
```  1309 end
```
```  1310
```
```  1311 subsubsection {* @{typ "'a option"} *}
```
```  1312
```
```  1313 instantiation option :: (card_UNIV) card_UNIV
```
```  1314 begin
```
```  1315
```
```  1316 definition card_UNIV_option_def:
```
```  1317   "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a option itself. let c = card_UNIV (TYPE('a))
```
```  1318                            in if c \<noteq> 0 then Suc c else 0)"
```
```  1319
```
```  1320 instance proof
```
```  1321   fix x :: "'a option itself"
```
```  1322   show "card_UNIV x = card (UNIV :: 'a option set)"
```
```  1323     unfolding UNIV_option_conv
```
```  1324     by(auto simp add: card_UNIV_option_def card_UNIV card_eq_0_iff Let_def intro: inj_Some dest: finite_imageD)
```
```  1325       (subst card_insert_disjoint, auto simp add: card_eq_0_iff card_image inj_Some intro: finite_imageI card_ge_0_finite)
```
```  1326 qed
```
```  1327
```
```  1328 end
```
```  1329
```
```  1330
```
```  1331 subsection {* Universal quantification *}
```
```  1332
```
```  1333 definition finfun_All_except :: "'a list \<Rightarrow> 'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
```
```  1334 where [code del]: "finfun_All_except A P \<equiv> \<forall>a. a \<in> set A \<or> P\<^sub>f a"
```
```  1335
```
```  1336 lemma finfun_All_except_const: "finfun_All_except A (\<lambda>\<^isup>f b) \<longleftrightarrow> b \<or> set A = UNIV"
```
```  1337 by(auto simp add: finfun_All_except_def)
```
```  1338
```
```  1339 lemma finfun_All_except_const_finfun_UNIV_code [code]:
```
```  1340   "finfun_All_except A (\<lambda>\<^isup>f b) = (b \<or> is_list_UNIV A)"
```
```  1341 by(simp add: finfun_All_except_const is_list_UNIV_iff)
```
```  1342
```
```  1343 lemma finfun_All_except_update:
```
```  1344   "finfun_All_except A f(\<^sup>f a := b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
```
```  1345 by(fastsimp simp add: finfun_All_except_def finfun_upd_apply)
```
```  1346
```
```  1347 lemma finfun_All_except_update_code [code]:
```
```  1348   fixes a :: "'a :: card_UNIV"
```
```  1349   shows "finfun_All_except A (finfun_update_code f a b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
```
```  1350 by(simp add: finfun_All_except_update)
```
```  1351
```
```  1352 definition finfun_All :: "'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
```
```  1353 where "finfun_All = finfun_All_except []"
```
```  1354
```
```  1355 lemma finfun_All_const [simp]: "finfun_All (\<lambda>\<^isup>f b) = b"
```
```  1356 by(simp add: finfun_All_def finfun_All_except_def)
```
```  1357
```
```  1358 lemma finfun_All_update: "finfun_All f(\<^sup>f a := b) = (b \<and> finfun_All_except [a] f)"
```
```  1359 by(simp add: finfun_All_def finfun_All_except_update)
```
```  1360
```
```  1361 lemma finfun_All_All: "finfun_All P = All P\<^sub>f"
```
```  1362 by(simp add: finfun_All_def finfun_All_except_def)
```
```  1363
```
```  1364
```
```  1365 definition finfun_Ex :: "'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
```
```  1366 where "finfun_Ex P = Not (finfun_All (Not \<circ>\<^isub>f P))"
```
```  1367
```
```  1368 lemma finfun_Ex_Ex: "finfun_Ex P = Ex P\<^sub>f"
```
```  1369 unfolding finfun_Ex_def finfun_All_All by simp
```
```  1370
```
```  1371 lemma finfun_Ex_const [simp]: "finfun_Ex (\<lambda>\<^isup>f b) = b"
```
```  1372 by(simp add: finfun_Ex_def)
```
```  1373
```
```  1374
```
```  1375 subsection {* A diagonal operator for FinFuns *}
```
```  1376
```
```  1377 definition finfun_Diag :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c \<Rightarrow> 'a \<Rightarrow>\<^isub>f ('b \<times> 'c)" ("(1'(_,/ _')\<^sup>f)" [0, 0] 1000)
```
```  1378 where [code del]: "finfun_Diag f g = finfun_rec (\<lambda>b. Pair b \<circ>\<^isub>f g) (\<lambda>a b c. c(\<^sup>f a := (b, g\<^sub>f a))) f"
```
```  1379
```
```  1380 interpretation finfun_Diag_aux: finfun_rec_wf_aux "\<lambda>b. Pair b \<circ>\<^isub>f g" "\<lambda>a b c. c(\<^sup>f a := (b, g\<^sub>f a))"
```
```  1381 by(unfold_locales)(simp_all add: expand_finfun_eq expand_fun_eq finfun_upd_apply)
```
```  1382
```
```  1383 interpretation finfun_Diag: finfun_rec_wf "\<lambda>b. Pair b \<circ>\<^isub>f g" "\<lambda>a b c. c(\<^sup>f a := (b, g\<^sub>f a))"
```
```  1384 proof
```
```  1385   fix b' b :: 'a
```
```  1386   assume fin: "finite (UNIV :: 'c set)"
```
```  1387   { fix A :: "'c set"
```
```  1388     interpret fun_left_comm "\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))" by(rule finfun_Diag_aux.upd_left_comm)
```
```  1389     from fin have "finite A" by(auto intro: finite_subset)
```
```  1390     hence "fold (\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))) (Pair b \<circ>\<^isub>f g) A =
```
```  1391       Abs_finfun (\<lambda>a. (if a \<in> A then b' else b, g\<^sub>f a))"
```
```  1392       by(induct)(simp_all add: finfun_const_def finfun_comp_conv_comp o_def,
```
```  1393                  auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite expand_fun_eq fin) }
```
```  1394   from this[of UNIV] show "fold (\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))) (Pair b \<circ>\<^isub>f g) UNIV = Pair b' \<circ>\<^isub>f g"
```
```  1395     by(simp add: finfun_const_def finfun_comp_conv_comp o_def)
```
```  1396 qed
```
```  1397
```
```  1398 lemma finfun_Diag_const1: "(\<lambda>\<^isup>f b, g)\<^sup>f = Pair b \<circ>\<^isub>f g"
```
```  1399 by(simp add: finfun_Diag_def)
```
```  1400
```
```  1401 text {*
```
```  1402   Do not use @{thm finfun_Diag_const1} for the code generator because @{term "Pair b"} is injective, i.e. if @{term g} is free of redundant updates, there is no need to check for redundant updates as is done for @{text "\<circ>\<^isub>f"}.
```
```  1403 *}
```
```  1404
```
```  1405 lemma finfun_Diag_const_code [code]:
```
```  1406   "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))"
```
```  1407   "(\<lambda>\<^isup>f b, g(\<^sup>f\<^sup>c a := c))\<^sup>f = (\<lambda>\<^isup>f b, g)\<^sup>f(\<^sup>f\<^sup>c a := (b, c))"
```
```  1408 by(simp_all add: finfun_Diag_const1)
```
```  1409
```
```  1410 lemma finfun_Diag_update1: "(f(\<^sup>f a := b), g)\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (b, g\<^sub>f a))"
```
```  1411   and finfun_Diag_update1_code [code]: "(finfun_update_code f a b, g)\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (b, g\<^sub>f a))"
```
```  1412 by(simp_all add: finfun_Diag_def)
```
```  1413
```
```  1414 lemma finfun_Diag_const2: "(f, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>b. (b, c)) \<circ>\<^isub>f f"
```
```  1415 by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
```
```  1416
```
```  1417 lemma finfun_Diag_update2: "(f, g(\<^sup>f a := c))\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (f\<^sub>f a, c))"
```
```  1418 by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
```
```  1419
```
```  1420 lemma finfun_Diag_const_const [simp]: "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))"
```
```  1421 by(simp add: finfun_Diag_const1)
```
```  1422
```
```  1423 lemma finfun_Diag_const_update:
```
```  1424   "(\<lambda>\<^isup>f b, g(\<^sup>f a := c))\<^sup>f = (\<lambda>\<^isup>f b, g)\<^sup>f(\<^sup>f a := (b, c))"
```
```  1425 by(simp add: finfun_Diag_const1)
```
```  1426
```
```  1427 lemma finfun_Diag_update_const:
```
```  1428   "(f(\<^sup>f a := b), \<lambda>\<^isup>f c)\<^sup>f = (f, \<lambda>\<^isup>f c)\<^sup>f(\<^sup>f a := (b, c))"
```
```  1429 by(simp add: finfun_Diag_def)
```
```  1430
```
```  1431 lemma finfun_Diag_update_update:
```
```  1432   "(f(\<^sup>f a := b), g(\<^sup>f a' := c))\<^sup>f = (if a = a' then (f, g)\<^sup>f(\<^sup>f a := (b, c)) else (f, g)\<^sup>f(\<^sup>f a := (b, g\<^sub>f a))(\<^sup>f a' := (f\<^sub>f a', c)))"
```
```  1433 by(auto simp add: finfun_Diag_update1 finfun_Diag_update2)
```
```  1434
```
```  1435 lemma finfun_Diag_apply [simp]: "(f, g)\<^sup>f\<^sub>f = (\<lambda>x. (f\<^sub>f x, g\<^sub>f x))"
```
```  1436 by(induct f rule: finfun_weak_induct)(auto simp add: finfun_Diag_const1 finfun_Diag_update1 finfun_upd_apply intro: ext)
```
```  1437
```
```  1438 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
```
```  1439
```
```  1440 lemma finfun_Diag_conv_Abs_finfun:
```
```  1441   "(f, g)\<^sup>f = Abs_finfun ((\<lambda>x. (Rep_finfun f x, Rep_finfun g x)))"
```
```  1442 proof -
```
```  1443   have "(\<lambda>f :: 'a \<Rightarrow>\<^isub>f 'b. (f, g)\<^sup>f) = (\<lambda>f. Abs_finfun ((\<lambda>x. (Rep_finfun f x, Rep_finfun g x))))"
```
```  1444   proof(rule finfun_rec_unique)
```
```  1445     { fix c show "Abs_finfun (\<lambda>x. (Rep_finfun (\<lambda>\<^isup>f c) x, Rep_finfun g x)) = Pair c \<circ>\<^isub>f g"
```
```  1446         by(simp add: finfun_comp_conv_comp finfun_apply_Rep_finfun o_def finfun_const_def) }
```
```  1447     { fix g' a b
```
```  1448       show "Abs_finfun (\<lambda>x. (Rep_finfun g'(\<^sup>f a := b) x, Rep_finfun g x)) =
```
```  1449             (Abs_finfun (\<lambda>x. (Rep_finfun g' x, Rep_finfun g x)))(\<^sup>f a := (b, g\<^sub>f a))"
```
```  1450         by(auto simp add: finfun_update_def expand_fun_eq finfun_apply_Rep_finfun simp del: fun_upd_apply) simp }
```
```  1451   qed(simp_all add: finfun_Diag_const1 finfun_Diag_update1)
```
```  1452   thus ?thesis by(auto simp add: expand_fun_eq)
```
```  1453 qed
```
```  1454
```
```  1455 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
```
```  1456
```
```  1457 lemma finfun_Diag_eq: "(f, g)\<^sup>f = (f', g')\<^sup>f \<longleftrightarrow> f = f' \<and> g = g'"
```
```  1458 by(auto simp add: expand_finfun_eq expand_fun_eq)
```
```  1459
```
```  1460 definition finfun_fst :: "'a \<Rightarrow>\<^isub>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b"
```
```  1461 where [code]: "finfun_fst f = fst \<circ>\<^isub>f f"
```
```  1462
```
```  1463 lemma finfun_fst_const: "finfun_fst (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f fst bc)"
```
```  1464 by(simp add: finfun_fst_def)
```
```  1465
```
```  1466 lemma finfun_fst_update: "finfun_fst (f(\<^sup>f a := bc)) = (finfun_fst f)(\<^sup>f a := fst bc)"
```
```  1467   and finfun_fst_update_code: "finfun_fst (finfun_update_code f a bc) = (finfun_fst f)(\<^sup>f a := fst bc)"
```
```  1468 by(simp_all add: finfun_fst_def)
```
```  1469
```
```  1470 lemma finfun_fst_comp_conv: "finfun_fst (f \<circ>\<^isub>f g) = (fst \<circ> f) \<circ>\<^isub>f g"
```
```  1471 by(simp add: finfun_fst_def)
```
```  1472
```
```  1473 lemma finfun_fst_conv [simp]: "finfun_fst (f, g)\<^sup>f = f"
```
```  1474 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)
```
```  1475
```
```  1476 lemma finfun_fst_conv_Abs_finfun: "finfun_fst = (\<lambda>f. Abs_finfun (fst o Rep_finfun f))"
```
```  1477 by(simp add: finfun_fst_def_raw finfun_comp_conv_comp finfun_apply_Rep_finfun)
```
```  1478
```
```  1479
```
```  1480 definition finfun_snd :: "'a \<Rightarrow>\<^isub>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c"
```
```  1481 where [code]: "finfun_snd f = snd \<circ>\<^isub>f f"
```
```  1482
```
```  1483 lemma finfun_snd_const: "finfun_snd (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f snd bc)"
```
```  1484 by(simp add: finfun_snd_def)
```
```  1485
```
```  1486 lemma finfun_snd_update: "finfun_snd (f(\<^sup>f a := bc)) = (finfun_snd f)(\<^sup>f a := snd bc)"
```
```  1487   and finfun_snd_update_code [code]: "finfun_snd (finfun_update_code f a bc) = (finfun_snd f)(\<^sup>f a := snd bc)"
```
```  1488 by(simp_all add: finfun_snd_def)
```
```  1489
```
```  1490 lemma finfun_snd_comp_conv: "finfun_snd (f \<circ>\<^isub>f g) = (snd \<circ> f) \<circ>\<^isub>f g"
```
```  1491 by(simp add: finfun_snd_def)
```
```  1492
```
```  1493 lemma finfun_snd_conv [simp]: "finfun_snd (f, g)\<^sup>f = g"
```
```  1494 apply(induct f rule: finfun_weak_induct)
```
```  1495 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)
```
```  1496 done
```
```  1497
```
```  1498 lemma finfun_snd_conv_Abs_finfun: "finfun_snd = (\<lambda>f. Abs_finfun (snd o Rep_finfun f))"
```
```  1499 by(simp add: finfun_snd_def_raw finfun_comp_conv_comp finfun_apply_Rep_finfun)
```
```  1500
```
```  1501 lemma finfun_Diag_collapse [simp]: "(finfun_fst f, finfun_snd f)\<^sup>f = f"
```
```  1502 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)
```
```  1503
```
```  1504 subsection {* Currying for FinFuns *}
```
```  1505
```
```  1506 definition finfun_curry :: "('a \<times> 'b) \<Rightarrow>\<^isub>f 'c \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b \<Rightarrow>\<^isub>f 'c"
```
```  1507 where [code del]: "finfun_curry = finfun_rec (finfun_const \<circ> finfun_const) (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c)))"
```
```  1508
```
```  1509 interpretation finfun_curry_aux: finfun_rec_wf_aux "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))"
```
```  1510 apply(unfold_locales)
```
```  1511 apply(auto simp add: split_def finfun_update_twist finfun_upd_apply split_paired_all finfun_update_const_same)
```
```  1512 done
```
```  1513
```
```  1514 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
```
```  1515
```
```  1516 interpretation finfun_curry: finfun_rec_wf "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))"
```
```  1517 proof(unfold_locales)
```
```  1518   fix b' b :: 'b
```
```  1519   assume fin: "finite (UNIV :: ('c \<times> 'a) set)"
```
```  1520   hence fin1: "finite (UNIV :: 'c set)" and fin2: "finite (UNIV :: 'a set)"
```
```  1521     unfolding UNIV_Times_UNIV[symmetric]
```
```  1522     by(fastsimp dest: finite_cartesian_productD1 finite_cartesian_productD2)+
```
```  1523   note [simp] = Abs_finfun_inverse_finite[OF fin] Abs_finfun_inverse_finite[OF fin1] Abs_finfun_inverse_finite[OF fin2]
```
```  1524   { fix A :: "('c \<times> 'a) set"
```
```  1525     interpret fun_left_comm "\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))) a b'"
```
```  1526       by(rule finfun_curry_aux.upd_left_comm)
```
```  1527     from fin have "finite A" by(auto intro: finite_subset)
```
```  1528     hence "fold (\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))) a b') ((finfun_const \<circ> finfun_const) b) A = Abs_finfun (\<lambda>a. Abs_finfun (\<lambda>b''. if (a, b'') \<in> A then b' else b))"
```
```  1529       by induct (simp_all, auto simp add: finfun_update_def finfun_const_def split_def finfun_apply_Rep_finfun intro!: arg_cong[where f="Abs_finfun"] ext) }
```
```  1530   from this[of UNIV]
```
```  1531   show "fold (\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))) a b') ((finfun_const \<circ> finfun_const) b) UNIV = (finfun_const \<circ> finfun_const) b'"
```
```  1532     by(simp add: finfun_const_def)
```
```  1533 qed
```
```  1534
```
```  1535 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
```
```  1536
```
```  1537 lemma finfun_curry_const [simp, code]: "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
```
```  1538 by(simp add: finfun_curry_def)
```
```  1539
```
```  1540 lemma finfun_curry_update [simp]:
```
```  1541   "finfun_curry (f(\<^sup>f (a, b) := c)) = (finfun_curry f)(\<^sup>f a := ((finfun_curry f)\<^sub>f a)(\<^sup>f b := c))"
```
```  1542   and finfun_curry_update_code [code]:
```
```  1543   "finfun_curry (f(\<^sup>f\<^sup>c (a, b) := c)) = (finfun_curry f)(\<^sup>f a := ((finfun_curry f)\<^sub>f a)(\<^sup>f b := c))"
```
```  1544 by(simp_all add: finfun_curry_def)
```
```  1545
```
```  1546 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
```
```  1547
```
```  1548 lemma finfun_Abs_finfun_curry: assumes fin: "f \<in> finfun"
```
```  1549   shows "(\<lambda>a. Abs_finfun (curry f a)) \<in> finfun"
```
```  1550 proof -
```
```  1551   from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast
```
```  1552   have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force)
```
```  1553   hence "{a. curry f a \<noteq> (\<lambda>x. c)} = fst ` {ab. f ab \<noteq> c}"
```
```  1554     by(auto simp add: curry_def expand_fun_eq)
```
```  1555   with fin c have "finite {a.  Abs_finfun (curry f a) \<noteq> (\<lambda>\<^isup>f c)}"
```
```  1556     by(simp add: finfun_const_def finfun_curry)
```
```  1557   thus ?thesis unfolding finfun_def by auto
```
```  1558 qed
```
```  1559
```
```  1560 lemma finfun_curry_conv_curry:
```
```  1561   fixes f :: "('a \<times> 'b) \<Rightarrow>\<^isub>f 'c"
```
```  1562   shows "finfun_curry f = Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun f) a))"
```
```  1563 proof -
```
```  1564   have "finfun_curry = (\<lambda>f :: ('a \<times> 'b) \<Rightarrow>\<^isub>f 'c. Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun f) a)))"
```
```  1565   proof(rule finfun_rec_unique)
```
```  1566     { fix c show "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)" by simp }
```
```  1567     { fix f a c show "finfun_curry (f(\<^sup>f a := c)) = (finfun_curry f)(\<^sup>f fst a := ((finfun_curry f)\<^sub>f (fst a))(\<^sup>f snd a := c))"
```
```  1568         by(cases a) simp }
```
```  1569     { fix c show "Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun (\<lambda>\<^isup>f c)) a)) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
```
```  1570         by(simp add: finfun_curry_def finfun_const_def curry_def) }
```
```  1571     { fix g a b
```
```  1572       show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (Rep_finfun g(\<^sup>f a := b)) aa)) =
```
```  1573        (Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun g) a)))(\<^sup>f
```
```  1574        fst a := ((Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun g) a)))\<^sub>f (fst a))(\<^sup>f snd a := b))"
```
```  1575         by(cases a)(auto intro!: ext arg_cong[where f=Abs_finfun] simp add: finfun_curry_def finfun_update_def finfun_apply_Rep_finfun finfun_curry finfun_Abs_finfun_curry) }
```
```  1576   qed
```
```  1577   thus ?thesis by(auto simp add: expand_fun_eq)
```
```  1578 qed
```
```  1579
```
```  1580 subsection {* Executable equality for FinFuns *}
```
```  1581
```
```  1582 lemma eq_finfun_All_ext: "(f = g) \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>\<^isub>f (f, g)\<^sup>f)"
```
```  1583 by(simp add: expand_finfun_eq expand_fun_eq finfun_All_All o_def)
```
```  1584
```
```  1585 instantiation finfun :: ("{card_UNIV,eq}",eq) eq begin
```
```  1586 definition eq_finfun_def: "eq_class.eq f g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>\<^isub>f (f, g)\<^sup>f)"
```
```  1587 instance by(intro_classes)(simp add: eq_finfun_All_ext eq_finfun_def)
```
```  1588 end
```
```  1589
```
```  1590 subsection {* Operator that explicitly removes all redundant updates in the generated representations *}
```
```  1591
```
```  1592 definition finfun_clearjunk :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b"
```
```  1593 where [simp, code del]: "finfun_clearjunk = id"
```
```  1594
```
```  1595 lemma finfun_clearjunk_const [code]: "finfun_clearjunk (\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b)"
```
```  1596 by simp
```
```  1597
```
```  1598 lemma finfun_clearjunk_update [code]: "finfun_clearjunk (finfun_update_code f a b) = f(\<^sup>f a := b)"
```
```  1599 by simp
```
```  1600
```
`  1601 end`