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