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