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