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