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