src/HOL/Library/FinFun.thy
author wenzelm
Fri Oct 12 18:58:20 2012 +0200 (2012-10-12)
changeset 49834 b27bbb021df1
parent 48100 0122ba071e1a
child 51124 8fd094d5b7b7
permissions -rw-r--r--
discontinued obsolete typedef (open) syntax;
     1 (* Author: Andreas Lochbihler, Uni Karlsruhe *)
     2 
     3 header {* Almost everywhere constant functions *}
     4 
     5 theory FinFun
     6 imports Cardinality
     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 ('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('a) = 0 then c else undefined)"
   439 by(simp add: finfun_default_const)
   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_upd_triv [simp]: "f(x $:= f $ x) = f"
   910 by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
   911 
   912 lemma finfun_const_inject [simp]: "(K$ b) = (K$ b') \<equiv> b = b'"
   913 by(simp add: expand_finfun_eq fun_eq_iff)
   914 
   915 lemma finfun_const_eq_update:
   916   "((K$ b) = f(a $:= b')) = (b = b' \<and> (\<forall>a'. a \<noteq> a' \<longrightarrow> f $ a' = b))"
   917 by(auto simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
   918 
   919 subsection {* Function composition *}
   920 
   921 definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>f 'a \<Rightarrow> 'c \<Rightarrow>f 'b" (infixr "o$" 55)
   922 where [code del]: "g o$ f  = finfun_rec (\<lambda>b. (K$ g b)) (\<lambda>a b c. c(a $:= g b)) f"
   923 
   924 notation (xsymbols) finfun_comp (infixr "\<circ>$" 55)
   925 
   926 interpretation finfun_comp_aux: finfun_rec_wf_aux "(\<lambda>b. (K$ g b))" "(\<lambda>a b c. c(a $:= g b))"
   927 by(unfold_locales)(auto simp add: finfun_upd_apply intro: finfun_ext)
   928 
   929 interpretation finfun_comp: finfun_rec_wf "(\<lambda>b. (K$ g b))" "(\<lambda>a b c. c(a $:= g b))"
   930 proof
   931   fix b' b :: 'a
   932   assume fin: "finite (UNIV :: 'c set)"
   933   { fix A :: "'c set"
   934     from fin have "finite A" by(auto intro: finite_subset)
   935     hence "Finite_Set.fold (\<lambda>(a :: 'c) c. c(a $:= g b')) (K$ g b) A =
   936       Abs_finfun (\<lambda>a. if a \<in> A then g b' else g b)"
   937       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) }
   938   from this[of UNIV] show "Finite_Set.fold (\<lambda>(a :: 'c) c. c(a $:= g b')) (K$ g b) UNIV = (K$ g b')"
   939     by(simp add: finfun_const_def)
   940 qed
   941 
   942 lemma finfun_comp_const [simp, code]:
   943   "g \<circ>$ (K$ c) = (K$ g c)"
   944 by(simp add: finfun_comp_def)
   945 
   946 lemma finfun_comp_update [simp]: "g \<circ>$ (f(a $:= b)) = (g \<circ>$ f)(a $:= g b)"
   947   and finfun_comp_update_code [code]: 
   948   "g \<circ>$ (finfun_update_code f a b) = finfun_update_code (g \<circ>$ f) a (g b)"
   949 by(simp_all add: finfun_comp_def)
   950 
   951 lemma finfun_comp_apply [simp]:
   952   "op $ (g \<circ>$ f) = g \<circ> op $ f"
   953 by(induct f rule: finfun_weak_induct)(auto simp add: finfun_upd_apply)
   954 
   955 lemma finfun_comp_comp_collapse [simp]: "f \<circ>$ g \<circ>$ h = (f \<circ> g) \<circ>$ h"
   956 by(induct h rule: finfun_weak_induct) simp_all
   957 
   958 lemma finfun_comp_const1 [simp]: "(\<lambda>x. c) \<circ>$ f = (K$ c)"
   959 by(induct f rule: finfun_weak_induct)(auto intro: finfun_ext simp add: finfun_upd_apply)
   960 
   961 lemma finfun_comp_id1 [simp]: "(\<lambda>x. x) \<circ>$ f = f" "id \<circ>$ f = f"
   962 by(induct f rule: finfun_weak_induct) auto
   963 
   964 lemma finfun_comp_conv_comp: "g \<circ>$ f = Abs_finfun (g \<circ> op $ f)"
   965   including finfun
   966 proof -
   967   have "(\<lambda>f. g \<circ>$ f) = (\<lambda>f. Abs_finfun (g \<circ> op $ f))"
   968   proof(rule finfun_rec_unique)
   969     { fix c show "Abs_finfun (g \<circ> op $ (K$ c)) = (K$ g c)"
   970         by(simp add: finfun_comp_def o_def)(simp add: finfun_const_def) }
   971     { fix g' a b show "Abs_finfun (g \<circ> op $ g'(a $:= b)) = (Abs_finfun (g \<circ> op $ g'))(a $:= g b)"
   972       proof -
   973         obtain y where y: "y \<in> finfun" and g': "g' = Abs_finfun y" by(cases g')
   974         moreover hence "(g \<circ> op $ g') \<in> finfun" by(simp add: finfun_left_compose)
   975         moreover have "g \<circ> y(a := b) = (g \<circ> y)(a := g b)" by(auto)
   976         ultimately show ?thesis by(simp add: finfun_comp_def finfun_update_def)
   977       qed }
   978   qed auto
   979   thus ?thesis by(auto simp add: fun_eq_iff)
   980 qed
   981 
   982 definition finfun_comp2 :: "'b \<Rightarrow>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>f 'c" (infixr "$o" 55)
   983 where [code del]: "g $o f = Abs_finfun (op $ g \<circ> f)"
   984 
   985 notation (xsymbol) finfun_comp2 (infixr "$\<circ>" 55)
   986 
   987 lemma finfun_comp2_const [code, simp]: "finfun_comp2 (K$ c) f = (K$ c)"
   988   including finfun
   989 by(simp add: finfun_comp2_def finfun_const_def comp_def)
   990 
   991 lemma finfun_comp2_update:
   992   includes finfun
   993   assumes inj: "inj f"
   994   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)"
   995 proof(cases "b \<in> range f")
   996   case True
   997   from inj have "\<And>x. (op $ g)(f x := c) \<circ> f = (op $ g \<circ> f)(x := c)" by(auto intro!: ext dest: injD)
   998   with inj True show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def finfun_right_compose)
   999 next
  1000   case False
  1001   hence "(op $ g)(b := c) \<circ> f = op $ g \<circ> f" by(auto simp add: fun_eq_iff)
  1002   with False show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def)
  1003 qed
  1004 
  1005 subsection {* Universal quantification *}
  1006 
  1007 definition finfun_All_except :: "'a list \<Rightarrow> 'a \<Rightarrow>f bool \<Rightarrow> bool"
  1008 where [code del]: "finfun_All_except A P \<equiv> \<forall>a. a \<in> set A \<or> P $ a"
  1009 
  1010 lemma finfun_All_except_const: "finfun_All_except A (K$ b) \<longleftrightarrow> b \<or> set A = UNIV"
  1011 by(auto simp add: finfun_All_except_def)
  1012 
  1013 lemma finfun_All_except_const_finfun_UNIV_code [code]:
  1014   "finfun_All_except A (K$ b) = (b \<or> is_list_UNIV A)"
  1015 by(simp add: finfun_All_except_const is_list_UNIV_iff)
  1016 
  1017 lemma finfun_All_except_update:
  1018   "finfun_All_except A f(a $:= b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
  1019 by(fastforce simp add: finfun_All_except_def finfun_upd_apply)
  1020 
  1021 lemma finfun_All_except_update_code [code]:
  1022   fixes a :: "'a :: card_UNIV"
  1023   shows "finfun_All_except A (finfun_update_code f a b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
  1024 by(simp add: finfun_All_except_update)
  1025 
  1026 definition finfun_All :: "'a \<Rightarrow>f bool \<Rightarrow> bool"
  1027 where "finfun_All = finfun_All_except []"
  1028 
  1029 lemma finfun_All_const [simp]: "finfun_All (K$ b) = b"
  1030 by(simp add: finfun_All_def finfun_All_except_def)
  1031 
  1032 lemma finfun_All_update: "finfun_All f(a $:= b) = (b \<and> finfun_All_except [a] f)"
  1033 by(simp add: finfun_All_def finfun_All_except_update)
  1034 
  1035 lemma finfun_All_All: "finfun_All P = All (op $ P)"
  1036 by(simp add: finfun_All_def finfun_All_except_def)
  1037 
  1038 
  1039 definition finfun_Ex :: "'a \<Rightarrow>f bool \<Rightarrow> bool"
  1040 where "finfun_Ex P = Not (finfun_All (Not \<circ>$ P))"
  1041 
  1042 lemma finfun_Ex_Ex: "finfun_Ex P = Ex (op $ P)"
  1043 unfolding finfun_Ex_def finfun_All_All by simp
  1044 
  1045 lemma finfun_Ex_const [simp]: "finfun_Ex (K$ b) = b"
  1046 by(simp add: finfun_Ex_def)
  1047 
  1048 
  1049 subsection {* A diagonal operator for FinFuns *}
  1050 
  1051 definition finfun_Diag :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow>f 'c \<Rightarrow> 'a \<Rightarrow>f ('b \<times> 'c)" ("(1'($_,/ _$'))" [0, 0] 1000)
  1052 where [code del]: "($f, g$) = finfun_rec (\<lambda>b. Pair b \<circ>$ g) (\<lambda>a b c. c(a $:= (b, g $ a))) f"
  1053 
  1054 interpretation finfun_Diag_aux: finfun_rec_wf_aux "\<lambda>b. Pair b \<circ>$ g" "\<lambda>a b c. c(a $:= (b, g $ a))"
  1055 by(unfold_locales)(simp_all add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
  1056 
  1057 interpretation finfun_Diag: finfun_rec_wf "\<lambda>b. Pair b \<circ>$ g" "\<lambda>a b c. c(a $:= (b, g $ a))"
  1058 proof
  1059   fix b' b :: 'a
  1060   assume fin: "finite (UNIV :: 'c set)"
  1061   { fix A :: "'c set"
  1062     interpret comp_fun_commute "\<lambda>a c. c(a $:= (b', g $ a))" by(rule finfun_Diag_aux.upd_left_comm)
  1063     from fin have "finite A" by(auto intro: finite_subset)
  1064     hence "Finite_Set.fold (\<lambda>a c. c(a $:= (b', g $ a))) (Pair b \<circ>$ g) A =
  1065       Abs_finfun (\<lambda>a. (if a \<in> A then b' else b, g $ a))"
  1066       by(induct)(simp_all add: finfun_const_def finfun_comp_conv_comp o_def,
  1067                  auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite fun_eq_iff fin) }
  1068   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"
  1069     by(simp add: finfun_const_def finfun_comp_conv_comp o_def)
  1070 qed
  1071 
  1072 lemma finfun_Diag_const1: "($K$ b, g$) = Pair b \<circ>$ g"
  1073 by(simp add: finfun_Diag_def)
  1074 
  1075 text {*
  1076   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 @{term "op \<circ>$"}.
  1077 *}
  1078 
  1079 lemma finfun_Diag_const_code [code]:
  1080   "($K$ b, K$ c$) = (K$ (b, c))"
  1081   "($K$ b, finfun_update_code g a c$) = finfun_update_code ($K$ b, g$) a (b, c)"
  1082 by(simp_all add: finfun_Diag_const1)
  1083 
  1084 lemma finfun_Diag_update1: "($f(a $:= b), g$) = ($f, g$)(a $:= (b, g $ a))"
  1085   and finfun_Diag_update1_code [code]: "($finfun_update_code f a b, g$) = ($f, g$)(a $:= (b, g $ a))"
  1086 by(simp_all add: finfun_Diag_def)
  1087 
  1088 lemma finfun_Diag_const2: "($f, K$ c$) = (\<lambda>b. (b, c)) \<circ>$ f"
  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_update2: "($f, g(a $:= c)$) = ($f, g$)(a $:= (f $ a, c))"
  1092 by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
  1093 
  1094 lemma finfun_Diag_const_const [simp]: "($K$ b, K$ c$) = (K$ (b, c))"
  1095 by(simp add: finfun_Diag_const1)
  1096 
  1097 lemma finfun_Diag_const_update:
  1098   "($K$ b, g(a $:= c)$) = ($K$ b, g$)(a $:= (b, c))"
  1099 by(simp add: finfun_Diag_const1)
  1100 
  1101 lemma finfun_Diag_update_const:
  1102   "($f(a $:= b), K$ c$) = ($f, K$ c$)(a $:= (b, c))"
  1103 by(simp add: finfun_Diag_def)
  1104 
  1105 lemma finfun_Diag_update_update:
  1106   "($f(a $:= b), g(a' $:= c)$) = (if a = a' then ($f, g$)(a $:= (b, c)) else ($f, g$)(a $:= (b, g $ a))(a' $:= (f $ a', c)))"
  1107 by(auto simp add: finfun_Diag_update1 finfun_Diag_update2)
  1108 
  1109 lemma finfun_Diag_apply [simp]: "op $ ($f, g$) = (\<lambda>x. (f $ x, g $ x))"
  1110 by(induct f rule: finfun_weak_induct)(auto simp add: finfun_Diag_const1 finfun_Diag_update1 finfun_upd_apply)
  1111 
  1112 lemma finfun_Diag_conv_Abs_finfun:
  1113   "($f, g$) = Abs_finfun ((\<lambda>x. (f $ x, g $ x)))"
  1114   including finfun
  1115 proof -
  1116   have "(\<lambda>f :: 'a \<Rightarrow>f 'b. ($f, g$)) = (\<lambda>f. Abs_finfun ((\<lambda>x. (f $ x, g $ x))))"
  1117   proof(rule finfun_rec_unique)
  1118     { fix c show "Abs_finfun (\<lambda>x. ((K$ c) $ x, g $ x)) = Pair c \<circ>$ g"
  1119         by(simp add: finfun_comp_conv_comp o_def finfun_const_def) }
  1120     { fix g' a b
  1121       show "Abs_finfun (\<lambda>x. (g'(a $:= b) $ x, g $ x)) =
  1122             (Abs_finfun (\<lambda>x. (g' $ x, g $ x)))(a $:= (b, g $ a))"
  1123         by(auto simp add: finfun_update_def fun_eq_iff simp del: fun_upd_apply) simp }
  1124   qed(simp_all add: finfun_Diag_const1 finfun_Diag_update1)
  1125   thus ?thesis by(auto simp add: fun_eq_iff)
  1126 qed
  1127 
  1128 lemma finfun_Diag_eq: "($f, g$) = ($f', g'$) \<longleftrightarrow> f = f' \<and> g = g'"
  1129 by(auto simp add: expand_finfun_eq fun_eq_iff)
  1130 
  1131 definition finfun_fst :: "'a \<Rightarrow>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>f 'b"
  1132 where [code]: "finfun_fst f = fst \<circ>$ f"
  1133 
  1134 lemma finfun_fst_const: "finfun_fst (K$ bc) = (K$ fst bc)"
  1135 by(simp add: finfun_fst_def)
  1136 
  1137 lemma finfun_fst_update: "finfun_fst (f(a $:= bc)) = (finfun_fst f)(a $:= fst bc)"
  1138   and finfun_fst_update_code: "finfun_fst (finfun_update_code f a bc) = (finfun_fst f)(a $:= fst bc)"
  1139 by(simp_all add: finfun_fst_def)
  1140 
  1141 lemma finfun_fst_comp_conv: "finfun_fst (f \<circ>$ g) = (fst \<circ> f) \<circ>$ g"
  1142 by(simp add: finfun_fst_def)
  1143 
  1144 lemma finfun_fst_conv [simp]: "finfun_fst ($f, g$) = f"
  1145 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)
  1146 
  1147 lemma finfun_fst_conv_Abs_finfun: "finfun_fst = (\<lambda>f. Abs_finfun (fst \<circ> op $ f))"
  1148 by(simp add: finfun_fst_def [abs_def] finfun_comp_conv_comp)
  1149 
  1150 
  1151 definition finfun_snd :: "'a \<Rightarrow>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>f 'c"
  1152 where [code]: "finfun_snd f = snd \<circ>$ f"
  1153 
  1154 lemma finfun_snd_const: "finfun_snd (K$ bc) = (K$ snd bc)"
  1155 by(simp add: finfun_snd_def)
  1156 
  1157 lemma finfun_snd_update: "finfun_snd (f(a $:= bc)) = (finfun_snd f)(a $:= snd bc)"
  1158   and finfun_snd_update_code [code]: "finfun_snd (finfun_update_code f a bc) = (finfun_snd f)(a $:= snd bc)"
  1159 by(simp_all add: finfun_snd_def)
  1160 
  1161 lemma finfun_snd_comp_conv: "finfun_snd (f \<circ>$ g) = (snd \<circ> f) \<circ>$ g"
  1162 by(simp add: finfun_snd_def)
  1163 
  1164 lemma finfun_snd_conv [simp]: "finfun_snd ($f, g$) = g"
  1165 apply(induct f rule: finfun_weak_induct)
  1166 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)
  1167 done
  1168 
  1169 lemma finfun_snd_conv_Abs_finfun: "finfun_snd = (\<lambda>f. Abs_finfun (snd \<circ> op $ f))"
  1170 by(simp add: finfun_snd_def [abs_def] finfun_comp_conv_comp)
  1171 
  1172 lemma finfun_Diag_collapse [simp]: "($finfun_fst f, finfun_snd f$) = f"
  1173 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)
  1174 
  1175 subsection {* Currying for FinFuns *}
  1176 
  1177 definition finfun_curry :: "('a \<times> 'b) \<Rightarrow>f 'c \<Rightarrow> 'a \<Rightarrow>f 'b \<Rightarrow>f 'c"
  1178 where [code del]: "finfun_curry = finfun_rec (finfun_const \<circ> finfun_const) (\<lambda>(a, b) c f. f(a $:= (f $ a)(b $:= c)))"
  1179 
  1180 interpretation finfun_curry_aux: finfun_rec_wf_aux "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(a $:= (f $ a)(b $:= c))"
  1181 apply(unfold_locales)
  1182 apply(auto simp add: split_def finfun_update_twist finfun_upd_apply split_paired_all finfun_update_const_same)
  1183 done
  1184 
  1185 interpretation finfun_curry: finfun_rec_wf "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(a $:= (f $ a)(b $:= c))"
  1186 proof(unfold_locales)
  1187   fix b' b :: 'b
  1188   assume fin: "finite (UNIV :: ('c \<times> 'a) set)"
  1189   hence fin1: "finite (UNIV :: 'c set)" and fin2: "finite (UNIV :: 'a set)"
  1190     unfolding UNIV_Times_UNIV[symmetric]
  1191     by(fastforce dest: finite_cartesian_productD1 finite_cartesian_productD2)+
  1192   note [simp] = Abs_finfun_inverse_finite[OF fin] Abs_finfun_inverse_finite[OF fin1] Abs_finfun_inverse_finite[OF fin2]
  1193   { fix A :: "('c \<times> 'a) set"
  1194     interpret comp_fun_commute "\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(a $:= (f $ a)(b $:= c))) a b'"
  1195       by(rule finfun_curry_aux.upd_left_comm)
  1196     from fin have "finite A" by(auto intro: finite_subset)
  1197     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))"
  1198       by induct (simp_all, auto simp add: finfun_update_def finfun_const_def split_def intro!: arg_cong[where f="Abs_finfun"] ext) }
  1199   from this[of UNIV]
  1200   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'"
  1201     by(simp add: finfun_const_def)
  1202 qed
  1203 
  1204 lemma finfun_curry_const [simp, code]: "finfun_curry (K$ c) = (K$ K$ c)"
  1205 by(simp add: finfun_curry_def)
  1206 
  1207 lemma finfun_curry_update [simp]:
  1208   "finfun_curry (f((a, b) $:= c)) = (finfun_curry f)(a $:= (finfun_curry f $ a)(b $:= c))"
  1209   and finfun_curry_update_code [code]:
  1210   "finfun_curry (finfun_update_code f (a, b) c) = (finfun_curry f)(a $:= (finfun_curry f $ a)(b $:= c))"
  1211 by(simp_all add: finfun_curry_def)
  1212 
  1213 lemma finfun_Abs_finfun_curry: assumes fin: "f \<in> finfun"
  1214   shows "(\<lambda>a. Abs_finfun (curry f a)) \<in> finfun"
  1215   including finfun
  1216 proof -
  1217   from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast
  1218   have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force)
  1219   hence "{a. curry f a \<noteq> (\<lambda>x. c)} = fst ` {ab. f ab \<noteq> c}"
  1220     by(auto simp add: curry_def fun_eq_iff)
  1221   with fin c have "finite {a.  Abs_finfun (curry f a) \<noteq> (K$ c)}"
  1222     by(simp add: finfun_const_def finfun_curry)
  1223   thus ?thesis unfolding finfun_def by auto
  1224 qed
  1225 
  1226 lemma finfun_curry_conv_curry:
  1227   fixes f :: "('a \<times> 'b) \<Rightarrow>f 'c"
  1228   shows "finfun_curry f = Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply f) a))"
  1229   including finfun
  1230 proof -
  1231   have "finfun_curry = (\<lambda>f :: ('a \<times> 'b) \<Rightarrow>f 'c. Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply f) a)))"
  1232   proof(rule finfun_rec_unique)
  1233     fix c show "finfun_curry (K$ c) = (K$ K$ c)" by simp
  1234     fix f a
  1235     show "finfun_curry (f(a $:= c)) = (finfun_curry f)(fst a $:= (finfun_curry f $ (fst a))(snd a $:= c))"
  1236       by(cases a) simp
  1237     show "Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply (K$ c)) a)) = (K$ K$ c)"
  1238       by(simp add: finfun_curry_def finfun_const_def curry_def)
  1239     fix g b
  1240     show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (op $ g(a $:= b)) aa)) =
  1241       (Abs_finfun (\<lambda>a. Abs_finfun (curry (op $ g) a)))(
  1242       fst a $:= ((Abs_finfun (\<lambda>a. Abs_finfun (curry (op $ g) a))) $ (fst a))(snd a $:= b))"
  1243       by(cases a)(auto intro!: ext arg_cong[where f=Abs_finfun] simp add: finfun_curry_def finfun_update_def finfun_Abs_finfun_curry)
  1244   qed
  1245   thus ?thesis by(auto simp add: fun_eq_iff)
  1246 qed
  1247 
  1248 subsection {* Executable equality for FinFuns *}
  1249 
  1250 lemma eq_finfun_All_ext: "(f = g) \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>$ ($f, g$))"
  1251 by(simp add: expand_finfun_eq fun_eq_iff finfun_All_All o_def)
  1252 
  1253 instantiation finfun :: ("{card_UNIV,equal}",equal) equal begin
  1254 definition eq_finfun_def [code]: "HOL.equal f g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>$ ($f, g$))"
  1255 instance by(intro_classes)(simp add: eq_finfun_All_ext eq_finfun_def)
  1256 end
  1257 
  1258 lemma [code nbe]:
  1259   "HOL.equal (f :: _ \<Rightarrow>f _) f \<longleftrightarrow> True"
  1260   by (fact equal_refl)
  1261 
  1262 subsection {* An operator that explicitly removes all redundant updates in the generated representations *}
  1263 
  1264 definition finfun_clearjunk :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow>f 'b"
  1265 where [simp, code del]: "finfun_clearjunk = id"
  1266 
  1267 lemma finfun_clearjunk_const [code]: "finfun_clearjunk (K$ b) = (K$ b)"
  1268 by simp
  1269 
  1270 lemma finfun_clearjunk_update [code]: 
  1271   "finfun_clearjunk (finfun_update_code f a b) = f(a $:= b)"
  1272 by simp
  1273 
  1274 subsection {* The domain of a FinFun as a FinFun *}
  1275 
  1276 definition finfun_dom :: "('a \<Rightarrow>f 'b) \<Rightarrow> ('a \<Rightarrow>f bool)"
  1277 where [code del]: "finfun_dom f = Abs_finfun (\<lambda>a. f $ a \<noteq> finfun_default f)"
  1278 
  1279 lemma finfun_dom_const:
  1280   "finfun_dom ((K$ c) :: 'a \<Rightarrow>f 'b) = (K$ finite (UNIV :: 'a set) \<and> c \<noteq> undefined)"
  1281 unfolding finfun_dom_def finfun_default_const
  1282 by(auto)(simp_all add: finfun_const_def)
  1283 
  1284 text {*
  1285   @{term "finfun_dom" } raises an exception when called on a FinFun whose domain is a finite type. 
  1286   For such FinFuns, the default value (and as such the domain) is undefined.
  1287 *}
  1288 
  1289 lemma finfun_dom_const_code [code]:
  1290   "finfun_dom ((K$ c) :: ('a :: card_UNIV) \<Rightarrow>f 'b) = 
  1291    (if CARD('a) = 0 then (K$ False) else FinFun.code_abort (\<lambda>_. finfun_dom (K$ c)))"
  1292 by(simp add: finfun_dom_const card_UNIV card_eq_0_iff)
  1293 
  1294 lemma finfun_dom_finfunI: "(\<lambda>a. f $ a \<noteq> finfun_default f) \<in> finfun"
  1295 using finite_finfun_default[of f]
  1296 by(simp add: finfun_def exI[where x=False])
  1297 
  1298 lemma finfun_dom_update [simp]:
  1299   "finfun_dom (f(a $:= b)) = (finfun_dom f)(a $:= (b \<noteq> finfun_default f))"
  1300 including finfun unfolding finfun_dom_def finfun_update_def
  1301 apply(simp add: finfun_default_update_const fun_upd_apply finfun_dom_finfunI)
  1302 apply(fold finfun_update.rep_eq)
  1303 apply(simp add: finfun_upd_apply fun_eq_iff fun_upd_def finfun_default_update_const)
  1304 done
  1305 
  1306 lemma finfun_dom_update_code [code]:
  1307   "finfun_dom (finfun_update_code f a b) = finfun_update_code (finfun_dom f) a (b \<noteq> finfun_default f)"
  1308 by(simp)
  1309 
  1310 lemma finite_finfun_dom: "finite {x. finfun_dom f $ x}"
  1311 proof(induct f rule: finfun_weak_induct)
  1312   case (const b)
  1313   thus ?case
  1314     by (cases "finite (UNIV :: 'a set) \<and> b \<noteq> undefined")
  1315       (auto simp add: finfun_dom_const UNIV_def [symmetric] Set.empty_def [symmetric])
  1316 next
  1317   case (update f a b)
  1318   have "{x. finfun_dom f(a $:= b) $ x} =
  1319     (if b = finfun_default f then {x. finfun_dom f $ x} - {a} else insert a {x. finfun_dom f $ x})"
  1320     by (auto simp add: finfun_upd_apply split: split_if_asm)
  1321   thus ?case using update by simp
  1322 qed
  1323 
  1324 
  1325 subsection {* The domain of a FinFun as a sorted list *}
  1326 
  1327 definition finfun_to_list :: "('a :: linorder) \<Rightarrow>f 'b \<Rightarrow> 'a list"
  1328 where
  1329   "finfun_to_list f = (THE xs. set xs = {x. finfun_dom f $ x} \<and> sorted xs \<and> distinct xs)"
  1330 
  1331 lemma set_finfun_to_list [simp]: "set (finfun_to_list f) = {x. finfun_dom f $ x}" (is ?thesis1)
  1332   and sorted_finfun_to_list: "sorted (finfun_to_list f)" (is ?thesis2)
  1333   and distinct_finfun_to_list: "distinct (finfun_to_list f)" (is ?thesis3)
  1334 proof -
  1335   have "?thesis1 \<and> ?thesis2 \<and> ?thesis3"
  1336     unfolding finfun_to_list_def
  1337     by(rule theI')(rule finite_sorted_distinct_unique finite_finfun_dom)+
  1338   thus ?thesis1 ?thesis2 ?thesis3 by simp_all
  1339 qed
  1340 
  1341 lemma finfun_const_False_conv_bot: "op $ (K$ False) = bot"
  1342 by auto
  1343 
  1344 lemma finfun_const_True_conv_top: "op $ (K$ True) = top"
  1345 by auto
  1346 
  1347 lemma finfun_to_list_const:
  1348   "finfun_to_list ((K$ c) :: ('a :: {linorder} \<Rightarrow>f 'b)) = 
  1349   (if \<not> finite (UNIV :: 'a set) \<or> c = undefined then [] else THE xs. set xs = UNIV \<and> sorted xs \<and> distinct xs)"
  1350 by(auto simp add: finfun_to_list_def finfun_const_False_conv_bot finfun_const_True_conv_top finfun_dom_const)
  1351 
  1352 lemma finfun_to_list_const_code [code]:
  1353   "finfun_to_list ((K$ c) :: ('a :: {linorder, card_UNIV} \<Rightarrow>f 'b)) =
  1354    (if CARD('a) = 0 then [] else FinFun.code_abort (\<lambda>_. finfun_to_list ((K$ c) :: ('a \<Rightarrow>f 'b))))"
  1355 by(auto simp add: finfun_to_list_const card_UNIV card_eq_0_iff)
  1356 
  1357 lemma remove1_insort_insert_same:
  1358   "x \<notin> set xs \<Longrightarrow> remove1 x (insort_insert x xs) = xs"
  1359 by (metis insort_insert_insort remove1_insort)
  1360 
  1361 lemma finfun_dom_conv:
  1362   "finfun_dom f $ x \<longleftrightarrow> f $ x \<noteq> finfun_default f"
  1363 by(induct f rule: finfun_weak_induct)(auto simp add: finfun_dom_const finfun_default_const finfun_default_update_const finfun_upd_apply)
  1364 
  1365 lemma finfun_to_list_update:
  1366   "finfun_to_list (f(a $:= b)) = 
  1367   (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
  1368 proof(subst finfun_to_list_def, rule the_equality)
  1369   fix xs
  1370   assume "set xs = {x. finfun_dom f(a $:= b) $ x} \<and> sorted xs \<and> distinct xs"
  1371   hence eq: "set xs = {x. finfun_dom f(a $:= b) $ x}"
  1372     and [simp]: "sorted xs" "distinct xs" by simp_all
  1373   show "xs = (if b = finfun_default f then remove1 a (finfun_to_list f) else insort_insert a (finfun_to_list f))"
  1374   proof(cases "b = finfun_default f")
  1375     case True [simp]
  1376     show ?thesis
  1377     proof(cases "finfun_dom f $ a")
  1378       case True
  1379       have "finfun_to_list f = insort_insert a xs"
  1380         unfolding finfun_to_list_def
  1381       proof(rule the_equality)
  1382         have "set (insort_insert a xs) = insert a (set xs)" by(simp add: set_insort_insert)
  1383         also note eq also
  1384         have "insert a {x. finfun_dom f(a $:= b) $ x} = {x. finfun_dom f $ x}" using True
  1385           by(auto simp add: finfun_upd_apply split: split_if_asm)
  1386         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)"
  1387           by(simp add: sorted_insort_insert distinct_insort_insert)
  1388 
  1389         fix xs'
  1390         assume "set xs' = {x. finfun_dom f $ x} \<and> sorted xs' \<and> distinct xs'"
  1391         thus "xs' = insort_insert a xs" using 1 by(auto dest: sorted_distinct_set_unique)
  1392       qed
  1393       with eq True show ?thesis by(simp add: remove1_insort_insert_same)
  1394     next
  1395       case False
  1396       hence "f $ a = b" by(auto simp add: finfun_dom_conv)
  1397       hence f: "f(a $:= b) = f" by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
  1398       from eq have "finfun_to_list f = xs" unfolding f finfun_to_list_def
  1399         by(auto elim: sorted_distinct_set_unique intro!: the_equality)
  1400       with eq False show ?thesis unfolding f by(simp add: remove1_idem)
  1401     qed
  1402   next
  1403     case False
  1404     show ?thesis
  1405     proof(cases "finfun_dom f $ a")
  1406       case True
  1407       have "finfun_to_list f = xs"
  1408         unfolding finfun_to_list_def
  1409       proof(rule the_equality)
  1410         have "finfun_dom f = finfun_dom f(a $:= b)" using False True
  1411           by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
  1412         with eq show 1: "set xs = {x. finfun_dom f $ x} \<and> sorted xs \<and> distinct xs"
  1413           by(simp del: finfun_dom_update)
  1414         
  1415         fix xs'
  1416         assume "set xs' = {x. finfun_dom f $ x} \<and> sorted xs' \<and> distinct xs'"
  1417         thus "xs' = xs" using 1 by(auto elim: sorted_distinct_set_unique)
  1418       qed
  1419       thus ?thesis using False True eq by(simp add: insort_insert_triv)
  1420     next
  1421       case False
  1422       have "finfun_to_list f = remove1 a xs"
  1423         unfolding finfun_to_list_def
  1424       proof(rule the_equality)
  1425         have "set (remove1 a xs) = set xs - {a}" by simp
  1426         also note eq also
  1427         have "{x. finfun_dom f(a $:= b) $ x} - {a} = {x. finfun_dom f $ x}" using False
  1428           by(auto simp add: finfun_upd_apply split: split_if_asm)
  1429         finally show 1: "set (remove1 a xs) = {x. finfun_dom f $ x} \<and> sorted (remove1 a xs) \<and> distinct (remove1 a xs)"
  1430           by(simp add: sorted_remove1)
  1431         
  1432         fix xs'
  1433         assume "set xs' = {x. finfun_dom f $ x} \<and> sorted xs' \<and> distinct xs'"
  1434         thus "xs' = remove1 a xs" using 1 by(blast intro: sorted_distinct_set_unique)
  1435       qed
  1436       thus ?thesis using False eq `b \<noteq> finfun_default f` 
  1437         by (simp add: insort_insert_insort insort_remove1)
  1438     qed
  1439   qed
  1440 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)
  1441 
  1442 lemma finfun_to_list_update_code [code]:
  1443   "finfun_to_list (finfun_update_code f a b) = 
  1444   (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
  1445 by(simp add: finfun_to_list_update)
  1446 
  1447 text {* Deactivate syntax again. Import theory @{text FinFun_Syntax} to reactivate it again *}
  1448 
  1449 no_type_notation
  1450   finfun ("(_ =>f /_)" [22, 21] 21)
  1451 
  1452 no_type_notation (xsymbols)
  1453   finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
  1454 
  1455 no_notation
  1456   finfun_const ("K$/ _" [0] 1) and
  1457   finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and
  1458   finfun_apply (infixl "$" 999) and
  1459   finfun_comp (infixr "o$" 55) and
  1460   finfun_comp2 (infixr "$o" 55) and
  1461   finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000)
  1462 
  1463 no_notation (xsymbols) 
  1464   finfun_comp (infixr "\<circ>$" 55) and
  1465   finfun_comp2 (infixr "$\<circ>" 55)
  1466 
  1467 end