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