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