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