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