src/HOL/Library/FinFun.thy
changeset 48028 a5377f6d9f14
child 48029 9d9c9069abbc
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/FinFun.thy	Tue May 29 15:31:58 2012 +0200
     1.3 @@ -0,0 +1,1473 @@
     1.4 +(* Author: Andreas Lochbihler, Uni Karlsruhe *)
     1.5 +
     1.6 +header {* Almost everywhere constant functions *}
     1.7 +
     1.8 +theory FinFun
     1.9 +imports Card_Univ
    1.10 +begin
    1.11 +
    1.12 +text {*
    1.13 +  This theory defines functions which are constant except for finitely
    1.14 +  many points (FinFun) and introduces a type finfin along with a
    1.15 +  number of operators for them. The code generator is set up such that
    1.16 +  such functions can be represented as data in the generated code and
    1.17 +  all operators are executable.
    1.18 +
    1.19 +  For details, see Formalising FinFuns - Generating Code for Functions as Data by A. Lochbihler in TPHOLs 2009.
    1.20 +*}
    1.21 +
    1.22 +
    1.23 +definition "code_abort" :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.24 +where [simp, code del]: "code_abort f = f ()"
    1.25 +
    1.26 +code_abort "code_abort"
    1.27 +
    1.28 +hide_const (open) "code_abort"
    1.29 +
    1.30 +subsection {* The @{text "map_default"} operation *}
    1.31 +
    1.32 +definition map_default :: "'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.33 +where "map_default b f a \<equiv> case f a of None \<Rightarrow> b | Some b' \<Rightarrow> b'"
    1.34 +
    1.35 +lemma map_default_delete [simp]:
    1.36 +  "map_default b (f(a := None)) = (map_default b f)(a := b)"
    1.37 +by(simp add: map_default_def fun_eq_iff)
    1.38 +
    1.39 +lemma map_default_insert:
    1.40 +  "map_default b (f(a \<mapsto> b')) = (map_default b f)(a := b')"
    1.41 +by(simp add: map_default_def fun_eq_iff)
    1.42 +
    1.43 +lemma map_default_empty [simp]: "map_default b empty = (\<lambda>a. b)"
    1.44 +by(simp add: fun_eq_iff map_default_def)
    1.45 +
    1.46 +lemma map_default_inject:
    1.47 +  fixes g g' :: "'a \<rightharpoonup> 'b"
    1.48 +  assumes infin_eq: "\<not> finite (UNIV :: 'a set) \<or> b = b'"
    1.49 +  and fin: "finite (dom g)" and b: "b \<notin> ran g"
    1.50 +  and fin': "finite (dom g')" and b': "b' \<notin> ran g'"
    1.51 +  and eq': "map_default b g = map_default b' g'"
    1.52 +  shows "b = b'" "g = g'"
    1.53 +proof -
    1.54 +  from infin_eq show bb': "b = b'"
    1.55 +  proof
    1.56 +    assume infin: "\<not> finite (UNIV :: 'a set)"
    1.57 +    from fin fin' have "finite (dom g \<union> dom g')" by auto
    1.58 +    with infin have "UNIV - (dom g \<union> dom g') \<noteq> {}" by(auto dest: finite_subset)
    1.59 +    then obtain a where a: "a \<notin> dom g \<union> dom g'" by auto
    1.60 +    hence "map_default b g a = b" "map_default b' g' a = b'" by(auto simp add: map_default_def)
    1.61 +    with eq' show "b = b'" by simp
    1.62 +  qed
    1.63 +
    1.64 +  show "g = g'"
    1.65 +  proof
    1.66 +    fix x
    1.67 +    show "g x = g' x"
    1.68 +    proof(cases "g x")
    1.69 +      case None
    1.70 +      hence "map_default b g x = b" by(simp add: map_default_def)
    1.71 +      with bb' eq' have "map_default b' g' x = b'" by simp
    1.72 +      with b' have "g' x = None" by(simp add: map_default_def ran_def split: option.split_asm)
    1.73 +      with None show ?thesis by simp
    1.74 +    next
    1.75 +      case (Some c)
    1.76 +      with b have cb: "c \<noteq> b" by(auto simp add: ran_def)
    1.77 +      moreover from Some have "map_default b g x = c" by(simp add: map_default_def)
    1.78 +      with eq' have "map_default b' g' x = c" by simp
    1.79 +      ultimately have "g' x = Some c" using b' bb' by(auto simp add: map_default_def split: option.splits)
    1.80 +      with Some show ?thesis by simp
    1.81 +    qed
    1.82 +  qed
    1.83 +qed
    1.84 +
    1.85 +subsection {* The finfun type *}
    1.86 +
    1.87 +definition "finfun = {f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}"
    1.88 +
    1.89 +typedef (open) ('a,'b) finfun  ("(_ \<Rightarrow>\<^isub>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set"
    1.90 +proof -
    1.91 +  have "\<exists>f. finite {x. f x \<noteq> undefined}"
    1.92 +  proof
    1.93 +    show "finite {x. (\<lambda>y. undefined) x \<noteq> undefined}" by auto
    1.94 +  qed
    1.95 +  then show ?thesis unfolding finfun_def by auto
    1.96 +qed
    1.97 +
    1.98 +setup_lifting type_definition_finfun
    1.99 +
   1.100 +lemma fun_upd_finfun: "y(a := b) \<in> finfun \<longleftrightarrow> y \<in> finfun"
   1.101 +proof -
   1.102 +  { fix b'
   1.103 +    have "finite {a'. (y(a := b)) a' \<noteq> b'} = finite {a'. y a' \<noteq> b'}"
   1.104 +    proof(cases "b = b'")
   1.105 +      case True
   1.106 +      hence "{a'. (y(a := b)) a' \<noteq> b'} = {a'. y a' \<noteq> b'} - {a}" by auto
   1.107 +      thus ?thesis by simp
   1.108 +    next
   1.109 +      case False
   1.110 +      hence "{a'. (y(a := b)) a' \<noteq> b'} = insert a {a'. y a' \<noteq> b'}" by auto
   1.111 +      thus ?thesis by simp
   1.112 +    qed }
   1.113 +  thus ?thesis unfolding finfun_def by blast
   1.114 +qed
   1.115 +
   1.116 +lemma const_finfun: "(\<lambda>x. a) \<in> finfun"
   1.117 +by(auto simp add: finfun_def)
   1.118 +
   1.119 +lemma finfun_left_compose:
   1.120 +  assumes "y \<in> finfun"
   1.121 +  shows "g \<circ> y \<in> finfun"
   1.122 +proof -
   1.123 +  from assms obtain b where "finite {a. y a \<noteq> b}"
   1.124 +    unfolding finfun_def by blast
   1.125 +  hence "finite {c. g (y c) \<noteq> g b}"
   1.126 +  proof(induct "{a. y a \<noteq> b}" arbitrary: y)
   1.127 +    case empty
   1.128 +    hence "y = (\<lambda>a. b)" by(auto intro: ext)
   1.129 +    thus ?case by(simp)
   1.130 +  next
   1.131 +    case (insert x F)
   1.132 +    note IH = `\<And>y. F = {a. y a \<noteq> b} \<Longrightarrow> finite {c. g (y c) \<noteq> g b}`
   1.133 +    from `insert x F = {a. y a \<noteq> b}` `x \<notin> F`
   1.134 +    have F: "F = {a. (y(x := b)) a \<noteq> b}" by(auto)
   1.135 +    show ?case
   1.136 +    proof(cases "g (y x) = g b")
   1.137 +      case True
   1.138 +      hence "{c. g ((y(x := b)) c) \<noteq> g b} = {c. g (y c) \<noteq> g b}" by auto
   1.139 +      with IH[OF F] show ?thesis by simp
   1.140 +    next
   1.141 +      case False
   1.142 +      hence "{c. g (y c) \<noteq> g b} = insert x {c. g ((y(x := b)) c) \<noteq> g b}" by auto
   1.143 +      with IH[OF F] show ?thesis by(simp)
   1.144 +    qed
   1.145 +  qed
   1.146 +  thus ?thesis unfolding finfun_def by auto
   1.147 +qed
   1.148 +
   1.149 +lemma assumes "y \<in> finfun"
   1.150 +  shows fst_finfun: "fst \<circ> y \<in> finfun"
   1.151 +  and snd_finfun: "snd \<circ> y \<in> finfun"
   1.152 +proof -
   1.153 +  from assms obtain b c where bc: "finite {a. y a \<noteq> (b, c)}"
   1.154 +    unfolding finfun_def by auto
   1.155 +  have "{a. fst (y a) \<noteq> b} \<subseteq> {a. y a \<noteq> (b, c)}"
   1.156 +    and "{a. snd (y a) \<noteq> c} \<subseteq> {a. y a \<noteq> (b, c)}" by auto
   1.157 +  hence "finite {a. fst (y a) \<noteq> b}" 
   1.158 +    and "finite {a. snd (y a) \<noteq> c}" using bc by(auto intro: finite_subset)
   1.159 +  thus "fst \<circ> y \<in> finfun" "snd \<circ> y \<in> finfun"
   1.160 +    unfolding finfun_def by auto
   1.161 +qed
   1.162 +
   1.163 +lemma map_of_finfun: "map_of xs \<in> finfun"
   1.164 +unfolding finfun_def
   1.165 +by(induct xs)(auto simp add: Collect_neg_eq Collect_conj_eq Collect_imp_eq intro: finite_subset)
   1.166 +
   1.167 +lemma Diag_finfun: "(\<lambda>x. (f x, g x)) \<in> finfun \<longleftrightarrow> f \<in> finfun \<and> g \<in> finfun"
   1.168 +by(auto intro: finite_subset simp add: Collect_neg_eq Collect_imp_eq Collect_conj_eq finfun_def)
   1.169 +
   1.170 +lemma finfun_right_compose:
   1.171 +  assumes g: "g \<in> finfun" and inj: "inj f"
   1.172 +  shows "g o f \<in> finfun"
   1.173 +proof -
   1.174 +  from g obtain b where b: "finite {a. g a \<noteq> b}" unfolding finfun_def by blast
   1.175 +  moreover have "f ` {a. g (f a) \<noteq> b} \<subseteq> {a. g a \<noteq> b}" by auto
   1.176 +  moreover from inj have "inj_on f {a.  g (f a) \<noteq> b}" by(rule subset_inj_on) blast
   1.177 +  ultimately have "finite {a. g (f a) \<noteq> b}"
   1.178 +    by(blast intro: finite_imageD[where f=f] finite_subset)
   1.179 +  thus ?thesis unfolding finfun_def by auto
   1.180 +qed
   1.181 +
   1.182 +lemma finfun_curry:
   1.183 +  assumes fin: "f \<in> finfun"
   1.184 +  shows "curry f \<in> finfun" "curry f a \<in> finfun"
   1.185 +proof -
   1.186 +  from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast
   1.187 +  moreover have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force)
   1.188 +  hence "{a. curry f a \<noteq> (\<lambda>b. c)} = fst ` {ab. f ab \<noteq> c}"
   1.189 +    by(auto simp add: curry_def fun_eq_iff)
   1.190 +  ultimately have "finite {a. curry f a \<noteq> (\<lambda>b. c)}" by simp
   1.191 +  thus "curry f \<in> finfun" unfolding finfun_def by blast
   1.192 +  
   1.193 +  have "snd ` {ab. f ab \<noteq> c} = {b. \<exists>a. f (a, b) \<noteq> c}" by(force)
   1.194 +  hence "{b. f (a, b) \<noteq> c} \<subseteq> snd ` {ab. f ab \<noteq> c}" by auto
   1.195 +  hence "finite {b. f (a, b) \<noteq> c}" by(rule finite_subset)(rule finite_imageI[OF c])
   1.196 +  thus "curry f a \<in> finfun" unfolding finfun_def by auto
   1.197 +qed
   1.198 +
   1.199 +lemmas finfun_simp = 
   1.200 +  fst_finfun snd_finfun Abs_finfun_inverse Rep_finfun_inverse Abs_finfun_inject Rep_finfun_inject Diag_finfun finfun_curry
   1.201 +lemmas finfun_iff = const_finfun fun_upd_finfun Rep_finfun map_of_finfun
   1.202 +lemmas finfun_intro = finfun_left_compose fst_finfun snd_finfun
   1.203 +
   1.204 +lemma Abs_finfun_inject_finite:
   1.205 +  fixes x y :: "'a \<Rightarrow> 'b"
   1.206 +  assumes fin: "finite (UNIV :: 'a set)"
   1.207 +  shows "Abs_finfun x = Abs_finfun y \<longleftrightarrow> x = y"
   1.208 +proof
   1.209 +  assume "Abs_finfun x = Abs_finfun y"
   1.210 +  moreover have "x \<in> finfun" "y \<in> finfun" unfolding finfun_def
   1.211 +    by(auto intro: finite_subset[OF _ fin])
   1.212 +  ultimately show "x = y" by(simp add: Abs_finfun_inject)
   1.213 +qed simp
   1.214 +
   1.215 +lemma Abs_finfun_inject_finite_class:
   1.216 +  fixes x y :: "('a :: finite) \<Rightarrow> 'b"
   1.217 +  shows "Abs_finfun x = Abs_finfun y \<longleftrightarrow> x = y"
   1.218 +using finite_UNIV
   1.219 +by(simp add: Abs_finfun_inject_finite)
   1.220 +
   1.221 +lemma Abs_finfun_inj_finite:
   1.222 +  assumes fin: "finite (UNIV :: 'a set)"
   1.223 +  shows "inj (Abs_finfun :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b)"
   1.224 +proof(rule inj_onI)
   1.225 +  fix x y :: "'a \<Rightarrow> 'b"
   1.226 +  assume "Abs_finfun x = Abs_finfun y"
   1.227 +  moreover have "x \<in> finfun" "y \<in> finfun" unfolding finfun_def
   1.228 +    by(auto intro: finite_subset[OF _ fin])
   1.229 +  ultimately show "x = y" by(simp add: Abs_finfun_inject)
   1.230 +qed
   1.231 +
   1.232 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
   1.233 +
   1.234 +lemma Abs_finfun_inverse_finite:
   1.235 +  fixes x :: "'a \<Rightarrow> 'b"
   1.236 +  assumes fin: "finite (UNIV :: 'a set)"
   1.237 +  shows "Rep_finfun (Abs_finfun x) = x"
   1.238 +proof -
   1.239 +  from fin have "x \<in> finfun"
   1.240 +    by(auto simp add: finfun_def intro: finite_subset)
   1.241 +  thus ?thesis by simp
   1.242 +qed
   1.243 +
   1.244 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
   1.245 +
   1.246 +lemma Abs_finfun_inverse_finite_class:
   1.247 +  fixes x :: "('a :: finite) \<Rightarrow> 'b"
   1.248 +  shows "Rep_finfun (Abs_finfun x) = x"
   1.249 +using finite_UNIV by(simp add: Abs_finfun_inverse_finite)
   1.250 +
   1.251 +lemma finfun_eq_finite_UNIV: "finite (UNIV :: 'a set) \<Longrightarrow> (finfun :: ('a \<Rightarrow> 'b) set) = UNIV"
   1.252 +unfolding finfun_def by(auto intro: finite_subset)
   1.253 +
   1.254 +lemma finfun_finite_UNIV_class: "finfun = (UNIV :: ('a :: finite \<Rightarrow> 'b) set)"
   1.255 +by(simp add: finfun_eq_finite_UNIV)
   1.256 +
   1.257 +lemma map_default_in_finfun:
   1.258 +  assumes fin: "finite (dom f)"
   1.259 +  shows "map_default b f \<in> finfun"
   1.260 +unfolding finfun_def
   1.261 +proof(intro CollectI exI)
   1.262 +  from fin show "finite {a. map_default b f a \<noteq> b}"
   1.263 +    by(auto simp add: map_default_def dom_def Collect_conj_eq split: option.splits)
   1.264 +qed
   1.265 +
   1.266 +lemma finfun_cases_map_default:
   1.267 +  obtains b g where "f = Abs_finfun (map_default b g)" "finite (dom g)" "b \<notin> ran g"
   1.268 +proof -
   1.269 +  obtain y where f: "f = Abs_finfun y" and y: "y \<in> finfun" by(cases f)
   1.270 +  from y obtain b where b: "finite {a. y a \<noteq> b}" unfolding finfun_def by auto
   1.271 +  let ?g = "(\<lambda>a. if y a = b then None else Some (y a))"
   1.272 +  have "map_default b ?g = y" by(simp add: fun_eq_iff map_default_def)
   1.273 +  with f have "f = Abs_finfun (map_default b ?g)" by simp
   1.274 +  moreover from b have "finite (dom ?g)" by(auto simp add: dom_def)
   1.275 +  moreover have "b \<notin> ran ?g" by(auto simp add: ran_def)
   1.276 +  ultimately show ?thesis by(rule that)
   1.277 +qed
   1.278 +
   1.279 +
   1.280 +subsection {* Kernel functions for type @{typ "'a \<Rightarrow>\<^isub>f 'b"} *}
   1.281 +
   1.282 +lift_definition finfun_const :: "'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("\<lambda>\<^isup>f/ _" [0] 1)
   1.283 +is "\<lambda> b x. b" by (rule const_finfun)
   1.284 +
   1.285 +lift_definition finfun_update :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("_'(\<^sup>f/ _ := _')" [1000,0,0] 1000) is "fun_upd" by (simp add: fun_upd_finfun)
   1.286 +
   1.287 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
   1.288 +
   1.289 +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)"
   1.290 +by transfer (simp add: fun_upd_twist)
   1.291 +
   1.292 +lemma finfun_update_twice [simp]:
   1.293 +  "finfun_update (finfun_update f a b) a b' = finfun_update f a b'"
   1.294 +by transfer simp
   1.295 +
   1.296 +lemma finfun_update_const_same: "(\<lambda>\<^isup>f b)(\<^sup>f a := b) = (\<lambda>\<^isup>f b)"
   1.297 +by transfer (simp add: fun_eq_iff)
   1.298 +
   1.299 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
   1.300 +
   1.301 +subsection {* Code generator setup *}
   1.302 +
   1.303 +definition finfun_update_code :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("_'(\<^sup>fc/ _ := _')" [1000,0,0] 1000)
   1.304 +where [simp, code del]: "finfun_update_code = finfun_update"
   1.305 +
   1.306 +code_datatype finfun_const finfun_update_code
   1.307 +
   1.308 +lemma finfun_update_const_code [code]:
   1.309 +  "(\<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')"
   1.310 +by(simp add: finfun_update_const_same)
   1.311 +
   1.312 +lemma finfun_update_update_code [code]:
   1.313 +  "(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)"
   1.314 +by(simp add: finfun_update_twist)
   1.315 +
   1.316 +
   1.317 +subsection {* Setup for quickcheck *}
   1.318 +
   1.319 +quickcheck_generator finfun constructors: finfun_update_code, "finfun_const :: 'b => 'a \<Rightarrow>\<^isub>f 'b"
   1.320 +
   1.321 +subsection {* @{text "finfun_update"} as instance of @{text "comp_fun_commute"} *}
   1.322 +
   1.323 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
   1.324 +
   1.325 +interpretation finfun_update: comp_fun_commute "\<lambda>a f. f(\<^sup>f a :: 'a := b')"
   1.326 +proof
   1.327 +  fix a a' :: 'a
   1.328 +  show "(\<lambda>f. f(\<^sup>f a := b')) \<circ> (\<lambda>f. f(\<^sup>f a' := b')) = (\<lambda>f. f(\<^sup>f a' := b')) \<circ> (\<lambda>f. f(\<^sup>f a := b'))"
   1.329 +  proof
   1.330 +    fix b
   1.331 +    have "(Rep_finfun b)(a := b', a' := b') = (Rep_finfun b)(a' := b', a := b')"
   1.332 +      by(cases "a = a'")(auto simp add: fun_upd_twist)
   1.333 +    then have "b(\<^sup>f a := b')(\<^sup>f a' := b') = b(\<^sup>f a' := b')(\<^sup>f a := b')"
   1.334 +      by(auto simp add: finfun_update_def fun_upd_twist)
   1.335 +    then show "((\<lambda>f. f(\<^sup>f a := b')) \<circ> (\<lambda>f. f(\<^sup>f a' := b'))) b = ((\<lambda>f. f(\<^sup>f a' := b')) \<circ> (\<lambda>f. f(\<^sup>f a := b'))) b"
   1.336 +      by (simp add: fun_eq_iff)
   1.337 +  qed
   1.338 +qed
   1.339 +
   1.340 +lemma fold_finfun_update_finite_univ:
   1.341 +  assumes fin: "finite (UNIV :: 'a set)"
   1.342 +  shows "Finite_Set.fold (\<lambda>a f. f(\<^sup>f a := b')) (\<lambda>\<^isup>f b) (UNIV :: 'a set) = (\<lambda>\<^isup>f b')"
   1.343 +proof -
   1.344 +  { fix A :: "'a set"
   1.345 +    from fin have "finite A" by(auto intro: finite_subset)
   1.346 +    hence "Finite_Set.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)"
   1.347 +    proof(induct)
   1.348 +      case (insert x F)
   1.349 +      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)"
   1.350 +        by(auto intro: ext)
   1.351 +      with insert show ?case
   1.352 +        by(simp add: finfun_const_def fun_upd_def)(simp add: finfun_update_def Abs_finfun_inverse_finite[OF fin] fun_upd_def)
   1.353 +    qed(simp add: finfun_const_def) }
   1.354 +  thus ?thesis by(simp add: finfun_const_def)
   1.355 +qed
   1.356 +
   1.357 +
   1.358 +subsection {* Default value for FinFuns *}
   1.359 +
   1.360 +definition finfun_default_aux :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"
   1.361 +where [code del]: "finfun_default_aux f = (if finite (UNIV :: 'a set) then undefined else THE b. finite {a. f a \<noteq> b})"
   1.362 +
   1.363 +lemma finfun_default_aux_infinite:
   1.364 +  fixes f :: "'a \<Rightarrow> 'b"
   1.365 +  assumes infin: "\<not> finite (UNIV :: 'a set)"
   1.366 +  and fin: "finite {a. f a \<noteq> b}"
   1.367 +  shows "finfun_default_aux f = b"
   1.368 +proof -
   1.369 +  let ?B = "{a. f a \<noteq> b}"
   1.370 +  from fin have "(THE b. finite {a. f a \<noteq> b}) = b"
   1.371 +  proof(rule the_equality)
   1.372 +    fix b'
   1.373 +    assume "finite {a. f a \<noteq> b'}" (is "finite ?B'")
   1.374 +    with infin fin have "UNIV - (?B' \<union> ?B) \<noteq> {}" by(auto dest: finite_subset)
   1.375 +    then obtain a where a: "a \<notin> ?B' \<union> ?B" by auto
   1.376 +    thus "b' = b" by auto
   1.377 +  qed
   1.378 +  thus ?thesis using infin by(simp add: finfun_default_aux_def)
   1.379 +qed
   1.380 +
   1.381 +
   1.382 +lemma finite_finfun_default_aux:
   1.383 +  fixes f :: "'a \<Rightarrow> 'b"
   1.384 +  assumes fin: "f \<in> finfun"
   1.385 +  shows "finite {a. f a \<noteq> finfun_default_aux f}"
   1.386 +proof(cases "finite (UNIV :: 'a set)")
   1.387 +  case True thus ?thesis using fin
   1.388 +    by(auto simp add: finfun_def finfun_default_aux_def intro: finite_subset)
   1.389 +next
   1.390 +  case False
   1.391 +  from fin obtain b where b: "finite {a. f a \<noteq> b}" (is "finite ?B")
   1.392 +    unfolding finfun_def by blast
   1.393 +  with False show ?thesis by(simp add: finfun_default_aux_infinite)
   1.394 +qed
   1.395 +
   1.396 +lemma finfun_default_aux_update_const:
   1.397 +  fixes f :: "'a \<Rightarrow> 'b"
   1.398 +  assumes fin: "f \<in> finfun"
   1.399 +  shows "finfun_default_aux (f(a := b)) = finfun_default_aux f"
   1.400 +proof(cases "finite (UNIV :: 'a set)")
   1.401 +  case False
   1.402 +  from fin obtain b' where b': "finite {a. f a \<noteq> b'}" unfolding finfun_def by blast
   1.403 +  hence "finite {a'. (f(a := b)) a' \<noteq> b'}"
   1.404 +  proof(cases "b = b' \<and> f a \<noteq> b'") 
   1.405 +    case True
   1.406 +    hence "{a. f a \<noteq> b'} = insert a {a'. (f(a := b)) a' \<noteq> b'}" by auto
   1.407 +    thus ?thesis using b' by simp
   1.408 +  next
   1.409 +    case False
   1.410 +    moreover
   1.411 +    { assume "b \<noteq> b'"
   1.412 +      hence "{a'. (f(a := b)) a' \<noteq> b'} = insert a {a. f a \<noteq> b'}" by auto
   1.413 +      hence ?thesis using b' by simp }
   1.414 +    moreover
   1.415 +    { assume "b = b'" "f a = b'"
   1.416 +      hence "{a'. (f(a := b)) a' \<noteq> b'} = {a. f a \<noteq> b'}" by auto
   1.417 +      hence ?thesis using b' by simp }
   1.418 +    ultimately show ?thesis by blast
   1.419 +  qed
   1.420 +  with False b' show ?thesis by(auto simp del: fun_upd_apply simp add: finfun_default_aux_infinite)
   1.421 +next
   1.422 +  case True thus ?thesis by(simp add: finfun_default_aux_def)
   1.423 +qed
   1.424 +
   1.425 +lift_definition finfun_default :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'b"
   1.426 +is "finfun_default_aux" ..
   1.427 +
   1.428 +lemma finite_finfun_default: "finite {a. Rep_finfun f a \<noteq> finfun_default f}"
   1.429 +apply transfer apply (erule finite_finfun_default_aux)
   1.430 +unfolding Rel_def fun_rel_def cr_finfun_def by simp
   1.431 +
   1.432 +lemma finfun_default_const: "finfun_default ((\<lambda>\<^isup>f b) :: 'a \<Rightarrow>\<^isub>f 'b) = (if finite (UNIV :: 'a set) then undefined else b)"
   1.433 +apply(transfer)
   1.434 +apply(auto simp add: finfun_default_aux_infinite)
   1.435 +apply(simp add: finfun_default_aux_def)
   1.436 +done
   1.437 +
   1.438 +lemma finfun_default_update_const:
   1.439 +  "finfun_default (f(\<^sup>f a := b)) = finfun_default f"
   1.440 +by transfer (simp add: finfun_default_aux_update_const)
   1.441 +
   1.442 +lemma finfun_default_const_code [code]:
   1.443 +  "finfun_default ((\<lambda>\<^isup>f c) :: ('a :: card_UNIV) \<Rightarrow>\<^isub>f 'b) = (if card_UNIV (TYPE('a)) = 0 then c else undefined)"
   1.444 +by(simp add: finfun_default_const card_UNIV_eq_0_infinite_UNIV)
   1.445 +
   1.446 +lemma finfun_default_update_code [code]:
   1.447 +  "finfun_default (finfun_update_code f a b) = finfun_default f"
   1.448 +by(simp add: finfun_default_update_const)
   1.449 +
   1.450 +subsection {* Recursion combinator and well-formedness conditions *}
   1.451 +
   1.452 +definition finfun_rec :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<Rightarrow> 'c"
   1.453 +where [code del]:
   1.454 +  "finfun_rec cnst upd f \<equiv>
   1.455 +   let b = finfun_default f;
   1.456 +       g = THE g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g
   1.457 +   in Finite_Set.fold (\<lambda>a. upd a (map_default b g a)) (cnst b) (dom g)"
   1.458 +
   1.459 +locale finfun_rec_wf_aux =
   1.460 +  fixes cnst :: "'b \<Rightarrow> 'c"
   1.461 +  and upd :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c"
   1.462 +  assumes upd_const_same: "upd a b (cnst b) = cnst b"
   1.463 +  and upd_commute: "a \<noteq> a' \<Longrightarrow> upd a b (upd a' b' c) = upd a' b' (upd a b c)"
   1.464 +  and upd_idemp: "b \<noteq> b' \<Longrightarrow> upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)"
   1.465 +begin
   1.466 +
   1.467 +
   1.468 +lemma upd_left_comm: "comp_fun_commute (\<lambda>a. upd a (f a))"
   1.469 +by(unfold_locales)(auto intro: upd_commute simp add: fun_eq_iff)
   1.470 +
   1.471 +lemma upd_upd_twice: "upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)"
   1.472 +by(cases "b \<noteq> b'")(auto simp add: fun_upd_def upd_const_same upd_idemp)
   1.473 +
   1.474 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
   1.475 +
   1.476 +lemma map_default_update_const:
   1.477 +  assumes fin: "finite (dom f)"
   1.478 +  and anf: "a \<notin> dom f"
   1.479 +  and fg: "f \<subseteq>\<^sub>m g"
   1.480 +  shows "upd a d  (Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f)) =
   1.481 +         Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f)"
   1.482 +proof -
   1.483 +  let ?upd = "\<lambda>a. upd a (map_default d g a)"
   1.484 +  let ?fr = "\<lambda>A. Finite_Set.fold ?upd (cnst d) A"
   1.485 +  interpret gwf: comp_fun_commute "?upd" by(rule upd_left_comm)
   1.486 +  
   1.487 +  from fin anf fg show ?thesis
   1.488 +  proof(induct "dom f" arbitrary: f)
   1.489 +    case empty
   1.490 +    from `{} = dom f` have "f = empty" by(auto simp add: dom_def intro: ext)
   1.491 +    thus ?case by(simp add: finfun_const_def upd_const_same)
   1.492 +  next
   1.493 +    case (insert a' A)
   1.494 +    note IH = `\<And>f.  \<lbrakk> A = dom f; a \<notin> dom f; f \<subseteq>\<^sub>m g \<rbrakk> \<Longrightarrow> upd a d (?fr (dom f)) = ?fr (dom f)`
   1.495 +    note fin = `finite A` note anf = `a \<notin> dom f` note a'nA = `a' \<notin> A`
   1.496 +    note domf = `insert a' A = dom f` note fg = `f \<subseteq>\<^sub>m g`
   1.497 +    
   1.498 +    from domf obtain b where b: "f a' = Some b" by auto
   1.499 +    let ?f' = "f(a' := None)"
   1.500 +    have "upd a d (?fr (insert a' A)) = upd a d (upd a' (map_default d g a') (?fr A))"
   1.501 +      by(subst gwf.fold_insert[OF fin a'nA]) rule
   1.502 +    also from b fg have "g a' = f a'" by(auto simp add: map_le_def intro: domI dest: bspec)
   1.503 +    hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def)
   1.504 +    also from anf domf have "a \<noteq> a'" by auto note upd_commute[OF this]
   1.505 +    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)
   1.506 +    note A also note IH[OF A `a \<notin> dom ?f'` `?f' \<subseteq>\<^sub>m g`]
   1.507 +    also have "upd a' (map_default d f a') (?fr (dom (f(a' := None)))) = ?fr (dom f)"
   1.508 +      unfolding domf[symmetric] gwf.fold_insert[OF fin a'nA] ga' unfolding A ..
   1.509 +    also have "insert a' (dom ?f') = dom f" using domf by auto
   1.510 +    finally show ?case .
   1.511 +  qed
   1.512 +qed
   1.513 +
   1.514 +lemma map_default_update_twice:
   1.515 +  assumes fin: "finite (dom f)"
   1.516 +  and anf: "a \<notin> dom f"
   1.517 +  and fg: "f \<subseteq>\<^sub>m g"
   1.518 +  shows "upd a d'' (upd a d' (Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f))) =
   1.519 +         upd a d'' (Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f))"
   1.520 +proof -
   1.521 +  let ?upd = "\<lambda>a. upd a (map_default d g a)"
   1.522 +  let ?fr = "\<lambda>A. Finite_Set.fold ?upd (cnst d) A"
   1.523 +  interpret gwf: comp_fun_commute "?upd" by(rule upd_left_comm)
   1.524 +  
   1.525 +  from fin anf fg show ?thesis
   1.526 +  proof(induct "dom f" arbitrary: f)
   1.527 +    case empty
   1.528 +    from `{} = dom f` have "f = empty" by(auto simp add: dom_def intro: ext)
   1.529 +    thus ?case by(auto simp add: finfun_const_def finfun_update_def upd_upd_twice)
   1.530 +  next
   1.531 +    case (insert a' A)
   1.532 +    note IH = `\<And>f. \<lbrakk>A = dom f; a \<notin> dom f; f \<subseteq>\<^sub>m g\<rbrakk> \<Longrightarrow> upd a d'' (upd a d' (?fr (dom f))) = upd a d'' (?fr (dom f))`
   1.533 +    note fin = `finite A` note anf = `a \<notin> dom f` note a'nA = `a' \<notin> A`
   1.534 +    note domf = `insert a' A = dom f` note fg = `f \<subseteq>\<^sub>m g`
   1.535 +    
   1.536 +    from domf obtain b where b: "f a' = Some b" by auto
   1.537 +    let ?f' = "f(a' := None)"
   1.538 +    let ?b' = "case f a' of None \<Rightarrow> d | Some b \<Rightarrow> b"
   1.539 +    from domf have "upd a d'' (upd a d' (?fr (dom f))) = upd a d'' (upd a d' (?fr (insert a' A)))" by simp
   1.540 +    also note gwf.fold_insert[OF fin a'nA]
   1.541 +    also from b fg have "g a' = f a'" by(auto simp add: map_le_def intro: domI dest: bspec)
   1.542 +    hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def)
   1.543 +    also from anf domf have ana': "a \<noteq> a'" by auto note upd_commute[OF this]
   1.544 +    also note upd_commute[OF ana']
   1.545 +    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)
   1.546 +    note A also note IH[OF A `a \<notin> dom ?f'` `?f' \<subseteq>\<^sub>m g`]
   1.547 +    also note upd_commute[OF ana'[symmetric]] also note ga'[symmetric] also note A[symmetric]
   1.548 +    also note gwf.fold_insert[symmetric, OF fin a'nA] also note domf
   1.549 +    finally show ?case .
   1.550 +  qed
   1.551 +qed
   1.552 +
   1.553 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
   1.554 +
   1.555 +lemma map_default_eq_id [simp]: "map_default d ((\<lambda>a. Some (f a)) |` {a. f a \<noteq> d}) = f"
   1.556 +by(auto simp add: map_default_def restrict_map_def intro: ext)
   1.557 +
   1.558 +lemma finite_rec_cong1:
   1.559 +  assumes f: "comp_fun_commute f" and g: "comp_fun_commute g"
   1.560 +  and fin: "finite A"
   1.561 +  and eq: "\<And>a. a \<in> A \<Longrightarrow> f a = g a"
   1.562 +  shows "Finite_Set.fold f z A = Finite_Set.fold g z A"
   1.563 +proof -
   1.564 +  interpret f: comp_fun_commute f by(rule f)
   1.565 +  interpret g: comp_fun_commute g by(rule g)
   1.566 +  { fix B
   1.567 +    assume BsubA: "B \<subseteq> A"
   1.568 +    with fin have "finite B" by(blast intro: finite_subset)
   1.569 +    hence "B \<subseteq> A \<Longrightarrow> Finite_Set.fold f z B = Finite_Set.fold g z B"
   1.570 +    proof(induct)
   1.571 +      case empty thus ?case by simp
   1.572 +    next
   1.573 +      case (insert a B)
   1.574 +      note finB = `finite B` note anB = `a \<notin> B` note sub = `insert a B \<subseteq> A`
   1.575 +      note IH = `B \<subseteq> A \<Longrightarrow> Finite_Set.fold f z B = Finite_Set.fold g z B`
   1.576 +      from sub anB have BpsubA: "B \<subset> A" and BsubA: "B \<subseteq> A" and aA: "a \<in> A" by auto
   1.577 +      from IH[OF BsubA] eq[OF aA] finB anB
   1.578 +      show ?case by(auto)
   1.579 +    qed
   1.580 +    with BsubA have "Finite_Set.fold f z B = Finite_Set.fold g z B" by blast }
   1.581 +  thus ?thesis by blast
   1.582 +qed
   1.583 +
   1.584 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
   1.585 +
   1.586 +lemma finfun_rec_upd [simp]:
   1.587 +  "finfun_rec cnst upd (f(\<^sup>f a' := b')) = upd a' b' (finfun_rec cnst upd f)"
   1.588 +proof -
   1.589 +  obtain b where b: "b = finfun_default f" by auto
   1.590 +  let ?the = "\<lambda>f g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g"
   1.591 +  obtain g where g: "g = The (?the f)" by blast
   1.592 +  obtain y where f: "f = Abs_finfun y" and y: "y \<in> finfun" by (cases f)
   1.593 +  from f y b have bfin: "finite {a. y a \<noteq> b}" by(simp add: finfun_default_def finite_finfun_default_aux)
   1.594 +
   1.595 +  let ?g = "(\<lambda>a. Some (y a)) |` {a. y a \<noteq> b}"
   1.596 +  from bfin have fing: "finite (dom ?g)" by auto
   1.597 +  have bran: "b \<notin> ran ?g" by(auto simp add: ran_def restrict_map_def)
   1.598 +  have yg: "y = map_default b ?g" by simp
   1.599 +  have gg: "g = ?g" unfolding g
   1.600 +  proof(rule the_equality)
   1.601 +    from f y bfin show "?the f ?g"
   1.602 +      by(auto)(simp add: restrict_map_def ran_def split: split_if_asm)
   1.603 +  next
   1.604 +    fix g'
   1.605 +    assume "?the f g'"
   1.606 +    hence fin': "finite (dom g')" and ran': "b \<notin> ran g'"
   1.607 +      and eq: "Abs_finfun (map_default b ?g) = Abs_finfun (map_default b g')" using f yg by auto
   1.608 +    from fin' fing have "map_default b ?g \<in> finfun" "map_default b g' \<in> finfun" by(blast intro: map_default_in_finfun)+
   1.609 +    with eq have "map_default b ?g = map_default b g'" by simp
   1.610 +    with fing bran fin' ran' show "g' = ?g" by(rule map_default_inject[OF disjI2[OF refl], THEN sym])
   1.611 +  qed
   1.612 +
   1.613 +  show ?thesis
   1.614 +  proof(cases "b' = b")
   1.615 +    case True
   1.616 +    note b'b = True
   1.617 +
   1.618 +    let ?g' = "(\<lambda>a. Some ((y(a' := b)) a)) |` {a. (y(a' := b)) a \<noteq> b}"
   1.619 +    from bfin b'b have fing': "finite (dom ?g')"
   1.620 +      by(auto simp add: Collect_conj_eq Collect_imp_eq intro: finite_subset)
   1.621 +    have brang': "b \<notin> ran ?g'" by(auto simp add: ran_def restrict_map_def)
   1.622 +
   1.623 +    let ?b' = "\<lambda>a. case ?g' a of None \<Rightarrow> b | Some b \<Rightarrow> b"
   1.624 +    let ?b = "map_default b ?g"
   1.625 +    from upd_left_comm upd_left_comm fing'
   1.626 +    have "Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g') = Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g')"
   1.627 +      by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b b map_default_def)
   1.628 +    also interpret gwf: comp_fun_commute "\<lambda>a. upd a (?b a)" by(rule upd_left_comm)
   1.629 +    have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g') = upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g))"
   1.630 +    proof(cases "y a' = b")
   1.631 +      case True
   1.632 +      with b'b have g': "?g' = ?g" by(auto simp add: restrict_map_def intro: ext)
   1.633 +      from True have a'ndomg: "a' \<notin> dom ?g" by auto
   1.634 +      from f b'b b show ?thesis unfolding g'
   1.635 +        by(subst map_default_update_const[OF fing a'ndomg map_le_refl, symmetric]) simp
   1.636 +    next
   1.637 +      case False
   1.638 +      hence domg: "dom ?g = insert a' (dom ?g')" by auto
   1.639 +      from False b'b have a'ndomg': "a' \<notin> dom ?g'" by auto
   1.640 +      have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g')) = 
   1.641 +            upd a' (?b a') (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'))"
   1.642 +        using fing' a'ndomg' unfolding b'b by(rule gwf.fold_insert)
   1.643 +      hence "upd a' b (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g'))) =
   1.644 +             upd a' b (upd a' (?b a') (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g')))" by simp
   1.645 +      also from b'b have g'leg: "?g' \<subseteq>\<^sub>m ?g" by(auto simp add: restrict_map_def map_le_def)
   1.646 +      note map_default_update_twice[OF fing' a'ndomg' this, of b "?b a'" b]
   1.647 +      also note map_default_update_const[OF fing' a'ndomg' g'leg, of b]
   1.648 +      finally show ?thesis unfolding b'b domg[unfolded b'b] by(rule sym)
   1.649 +    qed
   1.650 +    also have "The (?the (f(\<^sup>f a' := b'))) = ?g'"
   1.651 +    proof(rule the_equality)
   1.652 +      from f y b b'b brang' fing' show "?the (f(\<^sup>f a' := b')) ?g'"
   1.653 +        by(auto simp del: fun_upd_apply simp add: finfun_update_def)
   1.654 +    next
   1.655 +      fix g'
   1.656 +      assume "?the (f(\<^sup>f a' := b')) g'"
   1.657 +      hence fin': "finite (dom g')" and ran': "b \<notin> ran g'"
   1.658 +        and eq: "f(\<^sup>f a' := b') = Abs_finfun (map_default b g')" 
   1.659 +        by(auto simp del: fun_upd_apply)
   1.660 +      from fin' fing' have "map_default b g' \<in> finfun" "map_default b ?g' \<in> finfun"
   1.661 +        by(blast intro: map_default_in_finfun)+
   1.662 +      with eq f b'b b have "map_default b ?g' = map_default b g'"
   1.663 +        by(simp del: fun_upd_apply add: finfun_update_def)
   1.664 +      with fing' brang' fin' ran' show "g' = ?g'"
   1.665 +        by(rule map_default_inject[OF disjI2[OF refl], THEN sym])
   1.666 +    qed
   1.667 +    ultimately show ?thesis unfolding finfun_rec_def Let_def b gg[unfolded g b] using bfin b'b b
   1.668 +      by(simp only: finfun_default_update_const map_default_def)
   1.669 +  next
   1.670 +    case False
   1.671 +    note b'b = this
   1.672 +    let ?g' = "?g(a' \<mapsto> b')"
   1.673 +    let ?b' = "map_default b ?g'"
   1.674 +    let ?b = "map_default b ?g"
   1.675 +    from fing have fing': "finite (dom ?g')" by auto
   1.676 +    from bran b'b have bnrang': "b \<notin> ran ?g'" by(auto simp add: ran_def)
   1.677 +    have ffmg': "map_default b ?g' = y(a' := b')" by(auto intro: ext simp add: map_default_def restrict_map_def)
   1.678 +    with f y have f_Abs: "f(\<^sup>f a' := b') = Abs_finfun (map_default b ?g')" by(auto simp add: finfun_update_def)
   1.679 +    have g': "The (?the (f(\<^sup>f a' := b'))) = ?g'"
   1.680 +    proof (rule the_equality)
   1.681 +      from fing' bnrang' f_Abs show "?the (f(\<^sup>f a' := b')) ?g'" by(auto simp add: finfun_update_def restrict_map_def)
   1.682 +    next
   1.683 +      fix g' assume "?the (f(\<^sup>f a' := b')) g'"
   1.684 +      hence f': "f(\<^sup>f a' := b') = Abs_finfun (map_default b g')"
   1.685 +        and fin': "finite (dom g')" and brang': "b \<notin> ran g'" by auto
   1.686 +      from fing' fin' have "map_default b ?g' \<in> finfun" "map_default b g' \<in> finfun"
   1.687 +        by(auto intro: map_default_in_finfun)
   1.688 +      with f' f_Abs have "map_default b g' = map_default b ?g'" by simp
   1.689 +      with fin' brang' fing' bnrang' show "g' = ?g'"
   1.690 +        by(rule map_default_inject[OF disjI2[OF refl]])
   1.691 +    qed
   1.692 +    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}))"
   1.693 +      by auto
   1.694 +    show ?thesis
   1.695 +    proof(cases "y a' = b")
   1.696 +      case True
   1.697 +      hence a'ndomg: "a' \<notin> dom ?g" by auto
   1.698 +      from f y b'b True have yff: "y = map_default b (?g' |` dom ?g)"
   1.699 +        by(auto simp add: restrict_map_def map_default_def intro!: ext)
   1.700 +      hence f': "f = Abs_finfun (map_default b (?g' |` dom ?g))" using f by simp
   1.701 +      interpret g'wf: comp_fun_commute "\<lambda>a. upd a (?b' a)" by(rule upd_left_comm)
   1.702 +      from upd_left_comm upd_left_comm fing
   1.703 +      have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g) = Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g)"
   1.704 +        by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b True map_default_def)
   1.705 +      thus ?thesis unfolding finfun_rec_def Let_def finfun_default_update_const b[symmetric]
   1.706 +        unfolding g' g[symmetric] gg g'wf.fold_insert[OF fing a'ndomg, of "cnst b", folded dom]
   1.707 +        by -(rule arg_cong2[where f="upd a'"], simp_all add: map_default_def)
   1.708 +    next
   1.709 +      case False
   1.710 +      hence "insert a' (dom ?g) = dom ?g" by auto
   1.711 +      moreover {
   1.712 +        let ?g'' = "?g(a' := None)"
   1.713 +        let ?b'' = "map_default b ?g''"
   1.714 +        from False have domg: "dom ?g = insert a' (dom ?g'')" by auto
   1.715 +        from False have a'ndomg'': "a' \<notin> dom ?g''" by auto
   1.716 +        have fing'': "finite (dom ?g'')" by(rule finite_subset[OF _ fing]) auto
   1.717 +        have bnrang'': "b \<notin> ran ?g''" by(auto simp add: ran_def restrict_map_def)
   1.718 +        interpret gwf: comp_fun_commute "\<lambda>a. upd a (?b a)" by(rule upd_left_comm)
   1.719 +        interpret g'wf: comp_fun_commute "\<lambda>a. upd a (?b' a)" by(rule upd_left_comm)
   1.720 +        have "upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g''))) =
   1.721 +              upd a' b' (upd a' (?b a') (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')))"
   1.722 +          unfolding gwf.fold_insert[OF fing'' a'ndomg''] f ..
   1.723 +        also have g''leg: "?g |` dom ?g'' \<subseteq>\<^sub>m ?g" by(auto simp add: map_le_def)
   1.724 +        have "dom (?g |` dom ?g'') = dom ?g''" by auto
   1.725 +        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",
   1.726 +                                     unfolded this, OF fing'' a'ndomg'' g''leg]
   1.727 +        also have b': "b' = ?b' a'" by(auto simp add: map_default_def)
   1.728 +        from upd_left_comm upd_left_comm fing''
   1.729 +        have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'') = Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g'')"
   1.730 +          by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b map_default_def)
   1.731 +        with b' have "upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')) =
   1.732 +                     upd a' (?b' a') (Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g''))" by simp
   1.733 +        also note g'wf.fold_insert[OF fing'' a'ndomg'', symmetric]
   1.734 +        finally have "upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g)) =
   1.735 +                   Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g)"
   1.736 +          unfolding domg . }
   1.737 +      ultimately have "Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (insert a' (dom ?g)) =
   1.738 +                    upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g))" by simp
   1.739 +      thus ?thesis unfolding finfun_rec_def Let_def finfun_default_update_const b[symmetric] g[symmetric] g' dom[symmetric]
   1.740 +        using b'b gg by(simp add: map_default_insert)
   1.741 +    qed
   1.742 +  qed
   1.743 +qed
   1.744 +
   1.745 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
   1.746 +
   1.747 +end
   1.748 +
   1.749 +locale finfun_rec_wf = finfun_rec_wf_aux + 
   1.750 +  assumes const_update_all:
   1.751 +  "finite (UNIV :: 'a set) \<Longrightarrow> Finite_Set.fold (\<lambda>a. upd a b') (cnst b) (UNIV :: 'a set) = cnst b'"
   1.752 +begin
   1.753 +
   1.754 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
   1.755 +
   1.756 +lemma finfun_rec_const [simp]:
   1.757 +  "finfun_rec cnst upd (\<lambda>\<^isup>f c) = cnst c"
   1.758 +proof(cases "finite (UNIV :: 'a set)")
   1.759 +  case False
   1.760 +  hence "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = c" by(simp add: finfun_default_const)
   1.761 +  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"
   1.762 +  proof (rule the_equality)
   1.763 +    show "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c empty) \<and> finite (dom empty) \<and> c \<notin> ran empty"
   1.764 +      by(auto simp add: finfun_const_def)
   1.765 +  next
   1.766 +    fix g :: "'a \<rightharpoonup> 'b"
   1.767 +    assume "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g"
   1.768 +    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+
   1.769 +    from g map_default_in_finfun[OF fin, of c] have "map_default c g = (\<lambda>a. c)"
   1.770 +      by(simp add: finfun_const_def)
   1.771 +    moreover have "map_default c empty = (\<lambda>a. c)" by simp
   1.772 +    ultimately show "g = empty" by-(rule map_default_inject[OF disjI2[OF refl] fin ran], auto)
   1.773 +  qed
   1.774 +  ultimately show ?thesis by(simp add: finfun_rec_def)
   1.775 +next
   1.776 +  case True
   1.777 +  hence default: "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = undefined" by(simp add: finfun_default_const)
   1.778 +  let ?the = "\<lambda>g :: 'a \<rightharpoonup> 'b. (\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g) \<and> finite (dom g) \<and> undefined \<notin> ran g"
   1.779 +  show ?thesis
   1.780 +  proof(cases "c = undefined")
   1.781 +    case True
   1.782 +    have the: "The ?the = empty"
   1.783 +    proof (rule the_equality)
   1.784 +      from True show "?the empty" by(auto simp add: finfun_const_def)
   1.785 +    next
   1.786 +      fix g'
   1.787 +      assume "?the g'"
   1.788 +      hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g')"
   1.789 +        and fin: "finite (dom g')" and g: "undefined \<notin> ran g'" by simp_all
   1.790 +      from fin have "map_default undefined g' \<in> finfun" by(rule map_default_in_finfun)
   1.791 +      with fg have "map_default undefined g' = (\<lambda>a. c)"
   1.792 +        by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1])
   1.793 +      with True show "g' = empty"
   1.794 +        by -(rule map_default_inject(2)[OF _ fin g], auto)
   1.795 +    qed
   1.796 +    show ?thesis unfolding finfun_rec_def using `finite UNIV` True
   1.797 +      unfolding Let_def the default by(simp)
   1.798 +  next
   1.799 +    case False
   1.800 +    have the: "The ?the = (\<lambda>a :: 'a. Some c)"
   1.801 +    proof (rule the_equality)
   1.802 +      from False True show "?the (\<lambda>a :: 'a. Some c)"
   1.803 +        by(auto simp add: map_default_def [abs_def] finfun_const_def dom_def ran_def)
   1.804 +    next
   1.805 +      fix g' :: "'a \<rightharpoonup> 'b"
   1.806 +      assume "?the g'"
   1.807 +      hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g')"
   1.808 +        and fin: "finite (dom g')" and g: "undefined \<notin> ran g'" by simp_all
   1.809 +      from fin have "map_default undefined g' \<in> finfun" by(rule map_default_in_finfun)
   1.810 +      with fg have "map_default undefined g' = (\<lambda>a. c)"
   1.811 +        by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1])
   1.812 +      with True False show "g' = (\<lambda>a::'a. Some c)"
   1.813 +        by - (rule map_default_inject(2)[OF _ fin g],
   1.814 +          auto simp add: dom_def ran_def map_default_def [abs_def])
   1.815 +    qed
   1.816 +    show ?thesis unfolding finfun_rec_def using True False
   1.817 +      unfolding Let_def the default by(simp add: dom_def map_default_def const_update_all)
   1.818 +  qed
   1.819 +qed
   1.820 +
   1.821 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
   1.822 +
   1.823 +end
   1.824 +
   1.825 +subsection {* Weak induction rule and case analysis for FinFuns *}
   1.826 +
   1.827 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
   1.828 +
   1.829 +lemma finfun_weak_induct [consumes 0, case_names const update]:
   1.830 +  assumes const: "\<And>b. P (\<lambda>\<^isup>f b)"
   1.831 +  and update: "\<And>f a b. P f \<Longrightarrow> P (f(\<^sup>f a := b))"
   1.832 +  shows "P x"
   1.833 +proof(induct x rule: Abs_finfun_induct)
   1.834 +  case (Abs_finfun y)
   1.835 +  then obtain b where "finite {a. y a \<noteq> b}" unfolding finfun_def by blast
   1.836 +  thus ?case using `y \<in> finfun`
   1.837 +  proof(induct "{a. y a \<noteq> b}" arbitrary: y rule: finite_induct)
   1.838 +    case empty
   1.839 +    hence "\<And>a. y a = b" by blast
   1.840 +    hence "y = (\<lambda>a. b)" by(auto intro: ext)
   1.841 +    hence "Abs_finfun y = finfun_const b" unfolding finfun_const_def by simp
   1.842 +    thus ?case by(simp add: const)
   1.843 +  next
   1.844 +    case (insert a A)
   1.845 +    note IH = `\<And>y. \<lbrakk> A = {a. y a \<noteq> b}; y \<in> finfun  \<rbrakk> \<Longrightarrow> P (Abs_finfun y)`
   1.846 +    note y = `y \<in> finfun`
   1.847 +    with `insert a A = {a. y a \<noteq> b}` `a \<notin> A`
   1.848 +    have "A = {a'. (y(a := b)) a' \<noteq> b}" "y(a := b) \<in> finfun" by auto
   1.849 +    from IH[OF this] have "P (finfun_update (Abs_finfun (y(a := b))) a (y a))" by(rule update)
   1.850 +    thus ?case using y unfolding finfun_update_def by simp
   1.851 +  qed
   1.852 +qed
   1.853 +
   1.854 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
   1.855 +
   1.856 +lemma finfun_exhaust_disj: "(\<exists>b. x = finfun_const b) \<or> (\<exists>f a b. x = finfun_update f a b)"
   1.857 +by(induct x rule: finfun_weak_induct) blast+
   1.858 +
   1.859 +lemma finfun_exhaust:
   1.860 +  obtains b where "x = (\<lambda>\<^isup>f b)"
   1.861 +        | f a b where "x = f(\<^sup>f a := b)"
   1.862 +by(atomize_elim)(rule finfun_exhaust_disj)
   1.863 +
   1.864 +lemma finfun_rec_unique:
   1.865 +  fixes f :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'c"
   1.866 +  assumes c: "\<And>c. f (\<lambda>\<^isup>f c) = cnst c"
   1.867 +  and u: "\<And>g a b. f (g(\<^sup>f a := b)) = upd g a b (f g)"
   1.868 +  and c': "\<And>c. f' (\<lambda>\<^isup>f c) = cnst c"
   1.869 +  and u': "\<And>g a b. f' (g(\<^sup>f a := b)) = upd g a b (f' g)"
   1.870 +  shows "f = f'"
   1.871 +proof
   1.872 +  fix g :: "'a \<Rightarrow>\<^isub>f 'b"
   1.873 +  show "f g = f' g"
   1.874 +    by(induct g rule: finfun_weak_induct)(auto simp add: c u c' u')
   1.875 +qed
   1.876 +
   1.877 +
   1.878 +subsection {* Function application *}
   1.879 +
   1.880 +definition finfun_apply :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b" ("_\<^sub>f" [1000] 1000)
   1.881 +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)"
   1.882 +
   1.883 +interpretation finfun_apply_aux: finfun_rec_wf_aux "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c"
   1.884 +by(unfold_locales) auto
   1.885 +
   1.886 +interpretation finfun_apply: finfun_rec_wf "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c"
   1.887 +proof(unfold_locales)
   1.888 +  fix b' b :: 'a
   1.889 +  assume fin: "finite (UNIV :: 'b set)"
   1.890 +  { fix A :: "'b set"
   1.891 +    interpret comp_fun_commute "\<lambda>a'. If (a = a') b'" by(rule finfun_apply_aux.upd_left_comm)
   1.892 +    from fin have "finite A" by(auto intro: finite_subset)
   1.893 +    hence "Finite_Set.fold (\<lambda>a'. If (a = a') b') b A = (if a \<in> A then b' else b)"
   1.894 +      by induct auto }
   1.895 +  from this[of UNIV] show "Finite_Set.fold (\<lambda>a'. If (a = a') b') b UNIV = b'" by simp
   1.896 +qed
   1.897 +
   1.898 +lemma finfun_const_apply [simp, code]: "(\<lambda>\<^isup>f b)\<^sub>f a = b"
   1.899 +by(simp add: finfun_apply_def)
   1.900 +
   1.901 +lemma finfun_upd_apply: "f(\<^sup>fa := b)\<^sub>f a' = (if a = a' then b else f\<^sub>f a')"
   1.902 +  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')"
   1.903 +by(simp_all add: finfun_apply_def)
   1.904 +
   1.905 +lemma finfun_upd_apply_same [simp]:
   1.906 +  "f(\<^sup>fa := b)\<^sub>f a = b"
   1.907 +by(simp add: finfun_upd_apply)
   1.908 +
   1.909 +lemma finfun_upd_apply_other [simp]:
   1.910 +  "a \<noteq> a' \<Longrightarrow> f(\<^sup>fa := b)\<^sub>f a' = f\<^sub>f a'"
   1.911 +by(simp add: finfun_upd_apply)
   1.912 +
   1.913 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
   1.914 +
   1.915 +lemma finfun_apply_Rep_finfun:
   1.916 +  "finfun_apply = Rep_finfun"
   1.917 +proof(rule finfun_rec_unique)
   1.918 +  fix c show "Rep_finfun (\<lambda>\<^isup>f c) = (\<lambda>a. c)" by(auto simp add: finfun_const_def)
   1.919 +next
   1.920 +  fix g a b show "Rep_finfun g(\<^sup>f a := b) = (\<lambda>c. if c = a then b else Rep_finfun g c)"
   1.921 +    by(auto simp add: finfun_update_def fun_upd_finfun Abs_finfun_inverse Rep_finfun intro: ext)
   1.922 +qed(auto intro: ext)
   1.923 +
   1.924 +lemma finfun_ext: "(\<And>a. f\<^sub>f a = g\<^sub>f a) \<Longrightarrow> f = g"
   1.925 +by(auto simp add: finfun_apply_Rep_finfun Rep_finfun_inject[symmetric] simp del: Rep_finfun_inject intro: ext)
   1.926 +
   1.927 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
   1.928 +
   1.929 +lemma expand_finfun_eq: "(f = g) = (f\<^sub>f = g\<^sub>f)"
   1.930 +by(auto intro: finfun_ext)
   1.931 +
   1.932 +lemma finfun_const_inject [simp]: "(\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b') \<equiv> b = b'"
   1.933 +by(simp add: expand_finfun_eq fun_eq_iff)
   1.934 +
   1.935 +lemma finfun_const_eq_update:
   1.936 +  "((\<lambda>\<^isup>f b) = f(\<^sup>f a := b')) = (b = b' \<and> (\<forall>a'. a \<noteq> a' \<longrightarrow> f\<^sub>f a' = b))"
   1.937 +by(auto simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
   1.938 +
   1.939 +subsection {* Function composition *}
   1.940 +
   1.941 +definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>\<^isub>f 'a \<Rightarrow> 'c \<Rightarrow>\<^isub>f 'b" (infixr "\<circ>\<^isub>f" 55)
   1.942 +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"
   1.943 +
   1.944 +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))"
   1.945 +by(unfold_locales)(auto simp add: finfun_upd_apply intro: finfun_ext)
   1.946 +
   1.947 +interpretation finfun_comp: finfun_rec_wf "(\<lambda>b. (\<lambda>\<^isup>f g b))" "(\<lambda>a b c. c(\<^sup>f a := g b))"
   1.948 +proof
   1.949 +  fix b' b :: 'a
   1.950 +  assume fin: "finite (UNIV :: 'c set)"
   1.951 +  { fix A :: "'c set"
   1.952 +    from fin have "finite A" by(auto intro: finite_subset)
   1.953 +    hence "Finite_Set.fold (\<lambda>(a :: 'c) c. c(\<^sup>f a := g b')) (\<lambda>\<^isup>f g b) A =
   1.954 +      Abs_finfun (\<lambda>a. if a \<in> A then g b' else g b)"
   1.955 +      by induct (simp_all add: finfun_const_def, auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite fun_eq_iff fin) }
   1.956 +  from this[of UNIV] show "Finite_Set.fold (\<lambda>(a :: 'c) c. c(\<^sup>f a := g b')) (\<lambda>\<^isup>f g b) UNIV = (\<lambda>\<^isup>f g b')"
   1.957 +    by(simp add: finfun_const_def)
   1.958 +qed
   1.959 +
   1.960 +lemma finfun_comp_const [simp, code]:
   1.961 +  "g \<circ>\<^isub>f (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f g c)"
   1.962 +by(simp add: finfun_comp_def)
   1.963 +
   1.964 +lemma finfun_comp_update [simp]: "g \<circ>\<^isub>f (f(\<^sup>f a := b)) = (g \<circ>\<^isub>f f)(\<^sup>f a := g b)"
   1.965 +  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)"
   1.966 +by(simp_all add: finfun_comp_def)
   1.967 +
   1.968 +lemma finfun_comp_apply [simp]:
   1.969 +  "(g \<circ>\<^isub>f f)\<^sub>f = g \<circ> f\<^sub>f"
   1.970 +by(induct f rule: finfun_weak_induct)(auto simp add: finfun_upd_apply intro: ext)
   1.971 +
   1.972 +lemma finfun_comp_comp_collapse [simp]: "f \<circ>\<^isub>f g \<circ>\<^isub>f h = (f o g) \<circ>\<^isub>f h"
   1.973 +by(induct h rule: finfun_weak_induct) simp_all
   1.974 +
   1.975 +lemma finfun_comp_const1 [simp]: "(\<lambda>x. c) \<circ>\<^isub>f f = (\<lambda>\<^isup>f c)"
   1.976 +by(induct f rule: finfun_weak_induct)(auto intro: finfun_ext simp add: finfun_upd_apply)
   1.977 +
   1.978 +lemma finfun_comp_id1 [simp]: "(\<lambda>x. x) \<circ>\<^isub>f f = f" "id \<circ>\<^isub>f f = f"
   1.979 +by(induct f rule: finfun_weak_induct) auto
   1.980 +
   1.981 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
   1.982 +
   1.983 +lemma finfun_comp_conv_comp: "g \<circ>\<^isub>f f = Abs_finfun (g \<circ> finfun_apply f)"
   1.984 +proof -
   1.985 +  have "(\<lambda>f. g \<circ>\<^isub>f f) = (\<lambda>f. Abs_finfun (g \<circ> finfun_apply f))"
   1.986 +  proof(rule finfun_rec_unique)
   1.987 +    { fix c show "Abs_finfun (g \<circ> (\<lambda>\<^isup>f c)\<^sub>f) = (\<lambda>\<^isup>f g c)"
   1.988 +        by(simp add: finfun_comp_def o_def)(simp add: finfun_const_def) }
   1.989 +    { 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)"
   1.990 +      proof -
   1.991 +        obtain y where y: "y \<in> finfun" and g': "g' = Abs_finfun y" by(cases g')
   1.992 +        moreover hence "(g \<circ> g'\<^sub>f) \<in> finfun" by(simp add: finfun_apply_Rep_finfun finfun_left_compose)
   1.993 +        moreover have "g \<circ> y(a := b) = (g \<circ> y)(a := g b)" by(auto intro: ext)
   1.994 +        ultimately show ?thesis by(simp add: finfun_comp_def finfun_update_def finfun_apply_Rep_finfun)
   1.995 +      qed }
   1.996 +  qed auto
   1.997 +  thus ?thesis by(auto simp add: fun_eq_iff)
   1.998 +qed
   1.999 +
  1.1000 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
  1.1001 +
  1.1002 +definition finfun_comp2 :: "'b \<Rightarrow>\<^isub>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c" (infixr "\<^sub>f\<circ>" 55)
  1.1003 +where [code del]: "finfun_comp2 g f = Abs_finfun (Rep_finfun g \<circ> f)"
  1.1004 +
  1.1005 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
  1.1006 +
  1.1007 +lemma finfun_comp2_const [code, simp]: "finfun_comp2 (\<lambda>\<^isup>f c) f = (\<lambda>\<^isup>f c)"
  1.1008 +by(simp add: finfun_comp2_def finfun_const_def comp_def)
  1.1009 +
  1.1010 +lemma finfun_comp2_update:
  1.1011 +  assumes inj: "inj f"
  1.1012 +  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)"
  1.1013 +proof(cases "b \<in> range f")
  1.1014 +  case True
  1.1015 +  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)
  1.1016 +  with inj True show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def finfun_right_compose)
  1.1017 +next
  1.1018 +  case False
  1.1019 +  hence "(Rep_finfun g)(b := c) \<circ> f = Rep_finfun g \<circ> f" by(auto simp add: fun_eq_iff)
  1.1020 +  with False show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def)
  1.1021 +qed
  1.1022 +
  1.1023 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
  1.1024 +
  1.1025 +
  1.1026 +
  1.1027 +subsection {* Universal quantification *}
  1.1028 +
  1.1029 +definition finfun_All_except :: "'a list \<Rightarrow> 'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
  1.1030 +where [code del]: "finfun_All_except A P \<equiv> \<forall>a. a \<in> set A \<or> P\<^sub>f a"
  1.1031 +
  1.1032 +lemma finfun_All_except_const: "finfun_All_except A (\<lambda>\<^isup>f b) \<longleftrightarrow> b \<or> set A = UNIV"
  1.1033 +by(auto simp add: finfun_All_except_def)
  1.1034 +
  1.1035 +lemma finfun_All_except_const_finfun_UNIV_code [code]:
  1.1036 +  "finfun_All_except A (\<lambda>\<^isup>f b) = (b \<or> is_list_UNIV A)"
  1.1037 +by(simp add: finfun_All_except_const is_list_UNIV_iff)
  1.1038 +
  1.1039 +lemma finfun_All_except_update: 
  1.1040 +  "finfun_All_except A f(\<^sup>f a := b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
  1.1041 +by(fastforce simp add: finfun_All_except_def finfun_upd_apply)
  1.1042 +
  1.1043 +lemma finfun_All_except_update_code [code]:
  1.1044 +  fixes a :: "'a :: card_UNIV"
  1.1045 +  shows "finfun_All_except A (finfun_update_code f a b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
  1.1046 +by(simp add: finfun_All_except_update)
  1.1047 +
  1.1048 +definition finfun_All :: "'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
  1.1049 +where "finfun_All = finfun_All_except []"
  1.1050 +
  1.1051 +lemma finfun_All_const [simp]: "finfun_All (\<lambda>\<^isup>f b) = b"
  1.1052 +by(simp add: finfun_All_def finfun_All_except_def)
  1.1053 +
  1.1054 +lemma finfun_All_update: "finfun_All f(\<^sup>f a := b) = (b \<and> finfun_All_except [a] f)"
  1.1055 +by(simp add: finfun_All_def finfun_All_except_update)
  1.1056 +
  1.1057 +lemma finfun_All_All: "finfun_All P = All P\<^sub>f"
  1.1058 +by(simp add: finfun_All_def finfun_All_except_def)
  1.1059 +
  1.1060 +
  1.1061 +definition finfun_Ex :: "'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
  1.1062 +where "finfun_Ex P = Not (finfun_All (Not \<circ>\<^isub>f P))"
  1.1063 +
  1.1064 +lemma finfun_Ex_Ex: "finfun_Ex P = Ex P\<^sub>f"
  1.1065 +unfolding finfun_Ex_def finfun_All_All by simp
  1.1066 +
  1.1067 +lemma finfun_Ex_const [simp]: "finfun_Ex (\<lambda>\<^isup>f b) = b"
  1.1068 +by(simp add: finfun_Ex_def)
  1.1069 +
  1.1070 +
  1.1071 +subsection {* A diagonal operator for FinFuns *}
  1.1072 +
  1.1073 +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)
  1.1074 +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"
  1.1075 +
  1.1076 +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))"
  1.1077 +by(unfold_locales)(simp_all add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
  1.1078 +
  1.1079 +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))"
  1.1080 +proof
  1.1081 +  fix b' b :: 'a
  1.1082 +  assume fin: "finite (UNIV :: 'c set)"
  1.1083 +  { fix A :: "'c set"
  1.1084 +    interpret comp_fun_commute "\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))" by(rule finfun_Diag_aux.upd_left_comm)
  1.1085 +    from fin have "finite A" by(auto intro: finite_subset)
  1.1086 +    hence "Finite_Set.fold (\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))) (Pair b \<circ>\<^isub>f g) A =
  1.1087 +      Abs_finfun (\<lambda>a. (if a \<in> A then b' else b, g\<^sub>f a))"
  1.1088 +      by(induct)(simp_all add: finfun_const_def finfun_comp_conv_comp o_def,
  1.1089 +                 auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite fun_eq_iff fin) }
  1.1090 +  from this[of UNIV] show "Finite_Set.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"
  1.1091 +    by(simp add: finfun_const_def finfun_comp_conv_comp o_def)
  1.1092 +qed
  1.1093 +
  1.1094 +lemma finfun_Diag_const1: "(\<lambda>\<^isup>f b, g)\<^sup>f = Pair b \<circ>\<^isub>f g"
  1.1095 +by(simp add: finfun_Diag_def)
  1.1096 +
  1.1097 +text {*
  1.1098 +  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"}.
  1.1099 +*}
  1.1100 +
  1.1101 +lemma finfun_Diag_const_code [code]:
  1.1102 +  "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))"
  1.1103 +  "(\<lambda>\<^isup>f b, g(\<^sup>fc a := c))\<^sup>f = (\<lambda>\<^isup>f b, g)\<^sup>f(\<^sup>fc a := (b, c))"
  1.1104 +by(simp_all add: finfun_Diag_const1)
  1.1105 +
  1.1106 +lemma finfun_Diag_update1: "(f(\<^sup>f a := b), g)\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (b, g\<^sub>f a))"
  1.1107 +  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))"
  1.1108 +by(simp_all add: finfun_Diag_def)
  1.1109 +
  1.1110 +lemma finfun_Diag_const2: "(f, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>b. (b, c)) \<circ>\<^isub>f f"
  1.1111 +by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
  1.1112 +
  1.1113 +lemma finfun_Diag_update2: "(f, g(\<^sup>f a := c))\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (f\<^sub>f a, c))"
  1.1114 +by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
  1.1115 +
  1.1116 +lemma finfun_Diag_const_const [simp]: "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))"
  1.1117 +by(simp add: finfun_Diag_const1)
  1.1118 +
  1.1119 +lemma finfun_Diag_const_update:
  1.1120 +  "(\<lambda>\<^isup>f b, g(\<^sup>f a := c))\<^sup>f = (\<lambda>\<^isup>f b, g)\<^sup>f(\<^sup>f a := (b, c))"
  1.1121 +by(simp add: finfun_Diag_const1)
  1.1122 +
  1.1123 +lemma finfun_Diag_update_const:
  1.1124 +  "(f(\<^sup>f a := b), \<lambda>\<^isup>f c)\<^sup>f = (f, \<lambda>\<^isup>f c)\<^sup>f(\<^sup>f a := (b, c))"
  1.1125 +by(simp add: finfun_Diag_def)
  1.1126 +
  1.1127 +lemma finfun_Diag_update_update:
  1.1128 +  "(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)))"
  1.1129 +by(auto simp add: finfun_Diag_update1 finfun_Diag_update2)
  1.1130 +
  1.1131 +lemma finfun_Diag_apply [simp]: "(f, g)\<^sup>f\<^sub>f = (\<lambda>x. (f\<^sub>f x, g\<^sub>f x))"
  1.1132 +by(induct f rule: finfun_weak_induct)(auto simp add: finfun_Diag_const1 finfun_Diag_update1 finfun_upd_apply intro: ext)
  1.1133 +
  1.1134 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
  1.1135 +
  1.1136 +lemma finfun_Diag_conv_Abs_finfun:
  1.1137 +  "(f, g)\<^sup>f = Abs_finfun ((\<lambda>x. (Rep_finfun f x, Rep_finfun g x)))"
  1.1138 +proof -
  1.1139 +  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))))"
  1.1140 +  proof(rule finfun_rec_unique)
  1.1141 +    { fix c show "Abs_finfun (\<lambda>x. (Rep_finfun (\<lambda>\<^isup>f c) x, Rep_finfun g x)) = Pair c \<circ>\<^isub>f g"
  1.1142 +        by(simp add: finfun_comp_conv_comp finfun_apply_Rep_finfun o_def finfun_const_def) }
  1.1143 +    { fix g' a b
  1.1144 +      show "Abs_finfun (\<lambda>x. (Rep_finfun g'(\<^sup>f a := b) x, Rep_finfun g x)) =
  1.1145 +            (Abs_finfun (\<lambda>x. (Rep_finfun g' x, Rep_finfun g x)))(\<^sup>f a := (b, g\<^sub>f a))"
  1.1146 +        by(auto simp add: finfun_update_def fun_eq_iff finfun_apply_Rep_finfun simp del: fun_upd_apply) simp }
  1.1147 +  qed(simp_all add: finfun_Diag_const1 finfun_Diag_update1)
  1.1148 +  thus ?thesis by(auto simp add: fun_eq_iff)
  1.1149 +qed
  1.1150 +
  1.1151 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
  1.1152 +
  1.1153 +lemma finfun_Diag_eq: "(f, g)\<^sup>f = (f', g')\<^sup>f \<longleftrightarrow> f = f' \<and> g = g'"
  1.1154 +by(auto simp add: expand_finfun_eq fun_eq_iff)
  1.1155 +
  1.1156 +definition finfun_fst :: "'a \<Rightarrow>\<^isub>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b"
  1.1157 +where [code]: "finfun_fst f = fst \<circ>\<^isub>f f"
  1.1158 +
  1.1159 +lemma finfun_fst_const: "finfun_fst (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f fst bc)"
  1.1160 +by(simp add: finfun_fst_def)
  1.1161 +
  1.1162 +lemma finfun_fst_update: "finfun_fst (f(\<^sup>f a := bc)) = (finfun_fst f)(\<^sup>f a := fst bc)"
  1.1163 +  and finfun_fst_update_code: "finfun_fst (finfun_update_code f a bc) = (finfun_fst f)(\<^sup>f a := fst bc)"
  1.1164 +by(simp_all add: finfun_fst_def)
  1.1165 +
  1.1166 +lemma finfun_fst_comp_conv: "finfun_fst (f \<circ>\<^isub>f g) = (fst \<circ> f) \<circ>\<^isub>f g"
  1.1167 +by(simp add: finfun_fst_def)
  1.1168 +
  1.1169 +lemma finfun_fst_conv [simp]: "finfun_fst (f, g)\<^sup>f = f"
  1.1170 +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)
  1.1171 +
  1.1172 +lemma finfun_fst_conv_Abs_finfun: "finfun_fst = (\<lambda>f. Abs_finfun (fst o Rep_finfun f))"
  1.1173 +by(simp add: finfun_fst_def [abs_def] finfun_comp_conv_comp finfun_apply_Rep_finfun)
  1.1174 +
  1.1175 +
  1.1176 +definition finfun_snd :: "'a \<Rightarrow>\<^isub>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c"
  1.1177 +where [code]: "finfun_snd f = snd \<circ>\<^isub>f f"
  1.1178 +
  1.1179 +lemma finfun_snd_const: "finfun_snd (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f snd bc)"
  1.1180 +by(simp add: finfun_snd_def)
  1.1181 +
  1.1182 +lemma finfun_snd_update: "finfun_snd (f(\<^sup>f a := bc)) = (finfun_snd f)(\<^sup>f a := snd bc)"
  1.1183 +  and finfun_snd_update_code [code]: "finfun_snd (finfun_update_code f a bc) = (finfun_snd f)(\<^sup>f a := snd bc)"
  1.1184 +by(simp_all add: finfun_snd_def)
  1.1185 +
  1.1186 +lemma finfun_snd_comp_conv: "finfun_snd (f \<circ>\<^isub>f g) = (snd \<circ> f) \<circ>\<^isub>f g"
  1.1187 +by(simp add: finfun_snd_def)
  1.1188 +
  1.1189 +lemma finfun_snd_conv [simp]: "finfun_snd (f, g)\<^sup>f = g"
  1.1190 +apply(induct f rule: finfun_weak_induct)
  1.1191 +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)
  1.1192 +done
  1.1193 +
  1.1194 +lemma finfun_snd_conv_Abs_finfun: "finfun_snd = (\<lambda>f. Abs_finfun (snd o Rep_finfun f))"
  1.1195 +by(simp add: finfun_snd_def [abs_def] finfun_comp_conv_comp finfun_apply_Rep_finfun)
  1.1196 +
  1.1197 +lemma finfun_Diag_collapse [simp]: "(finfun_fst f, finfun_snd f)\<^sup>f = f"
  1.1198 +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)
  1.1199 +
  1.1200 +subsection {* Currying for FinFuns *}
  1.1201 +
  1.1202 +definition finfun_curry :: "('a \<times> 'b) \<Rightarrow>\<^isub>f 'c \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b \<Rightarrow>\<^isub>f 'c"
  1.1203 +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)))"
  1.1204 +
  1.1205 +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))"
  1.1206 +apply(unfold_locales)
  1.1207 +apply(auto simp add: split_def finfun_update_twist finfun_upd_apply split_paired_all finfun_update_const_same)
  1.1208 +done
  1.1209 +
  1.1210 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
  1.1211 +
  1.1212 +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))"
  1.1213 +proof(unfold_locales)
  1.1214 +  fix b' b :: 'b
  1.1215 +  assume fin: "finite (UNIV :: ('c \<times> 'a) set)"
  1.1216 +  hence fin1: "finite (UNIV :: 'c set)" and fin2: "finite (UNIV :: 'a set)"
  1.1217 +    unfolding UNIV_Times_UNIV[symmetric]
  1.1218 +    by(fastforce dest: finite_cartesian_productD1 finite_cartesian_productD2)+
  1.1219 +  note [simp] = Abs_finfun_inverse_finite[OF fin] Abs_finfun_inverse_finite[OF fin1] Abs_finfun_inverse_finite[OF fin2]
  1.1220 +  { fix A :: "('c \<times> 'a) set"
  1.1221 +    interpret comp_fun_commute "\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))) a b'"
  1.1222 +      by(rule finfun_curry_aux.upd_left_comm)
  1.1223 +    from fin have "finite A" by(auto intro: finite_subset)
  1.1224 +    hence "Finite_Set.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))"
  1.1225 +      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) }
  1.1226 +  from this[of UNIV]
  1.1227 +  show "Finite_Set.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'"
  1.1228 +    by(simp add: finfun_const_def)
  1.1229 +qed
  1.1230 +
  1.1231 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
  1.1232 +
  1.1233 +lemma finfun_curry_const [simp, code]: "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
  1.1234 +by(simp add: finfun_curry_def)
  1.1235 +
  1.1236 +lemma finfun_curry_update [simp]:
  1.1237 +  "finfun_curry (f(\<^sup>f (a, b) := c)) = (finfun_curry f)(\<^sup>f a := ((finfun_curry f)\<^sub>f a)(\<^sup>f b := c))"
  1.1238 +  and finfun_curry_update_code [code]:
  1.1239 +  "finfun_curry (f(\<^sup>fc (a, b) := c)) = (finfun_curry f)(\<^sup>f a := ((finfun_curry f)\<^sub>f a)(\<^sup>f b := c))"
  1.1240 +by(simp_all add: finfun_curry_def)
  1.1241 +
  1.1242 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
  1.1243 +
  1.1244 +lemma finfun_Abs_finfun_curry: assumes fin: "f \<in> finfun"
  1.1245 +  shows "(\<lambda>a. Abs_finfun (curry f a)) \<in> finfun"
  1.1246 +proof -
  1.1247 +  from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast
  1.1248 +  have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force)
  1.1249 +  hence "{a. curry f a \<noteq> (\<lambda>x. c)} = fst ` {ab. f ab \<noteq> c}"
  1.1250 +    by(auto simp add: curry_def fun_eq_iff)
  1.1251 +  with fin c have "finite {a.  Abs_finfun (curry f a) \<noteq> (\<lambda>\<^isup>f c)}"
  1.1252 +    by(simp add: finfun_const_def finfun_curry)
  1.1253 +  thus ?thesis unfolding finfun_def by auto
  1.1254 +qed
  1.1255 +
  1.1256 +lemma finfun_curry_conv_curry:
  1.1257 +  fixes f :: "('a \<times> 'b) \<Rightarrow>\<^isub>f 'c"
  1.1258 +  shows "finfun_curry f = Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun f) a))"
  1.1259 +proof -
  1.1260 +  have "finfun_curry = (\<lambda>f :: ('a \<times> 'b) \<Rightarrow>\<^isub>f 'c. Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun f) a)))"
  1.1261 +  proof(rule finfun_rec_unique)
  1.1262 +    { fix c show "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)" by simp }
  1.1263 +    { 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))"
  1.1264 +        by(cases a) simp }
  1.1265 +    { fix c show "Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun (\<lambda>\<^isup>f c)) a)) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
  1.1266 +        by(simp add: finfun_curry_def finfun_const_def curry_def) }
  1.1267 +    { fix g a b
  1.1268 +      show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (Rep_finfun g(\<^sup>f a := b)) aa)) =
  1.1269 +       (Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun g) a)))(\<^sup>f
  1.1270 +       fst a := ((Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun g) a)))\<^sub>f (fst a))(\<^sup>f snd a := b))"
  1.1271 +        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) }
  1.1272 +  qed
  1.1273 +  thus ?thesis by(auto simp add: fun_eq_iff)
  1.1274 +qed
  1.1275 +
  1.1276 +subsection {* Executable equality for FinFuns *}
  1.1277 +
  1.1278 +lemma eq_finfun_All_ext: "(f = g) \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>\<^isub>f (f, g)\<^sup>f)"
  1.1279 +by(simp add: expand_finfun_eq fun_eq_iff finfun_All_All o_def)
  1.1280 +
  1.1281 +instantiation finfun :: ("{card_UNIV,equal}",equal) equal begin
  1.1282 +definition eq_finfun_def [code]: "HOL.equal f g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>\<^isub>f (f, g)\<^sup>f)"
  1.1283 +instance by(intro_classes)(simp add: eq_finfun_All_ext eq_finfun_def)
  1.1284 +end
  1.1285 +
  1.1286 +lemma [code nbe]:
  1.1287 +  "HOL.equal (f :: _ \<Rightarrow>\<^isub>f _) f \<longleftrightarrow> True"
  1.1288 +  by (fact equal_refl)
  1.1289 +
  1.1290 +subsection {* An operator that explicitly removes all redundant updates in the generated representations *}
  1.1291 +
  1.1292 +definition finfun_clearjunk :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b"
  1.1293 +where [simp, code del]: "finfun_clearjunk = id"
  1.1294 +
  1.1295 +lemma finfun_clearjunk_const [code]: "finfun_clearjunk (\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b)"
  1.1296 +by simp
  1.1297 +
  1.1298 +lemma finfun_clearjunk_update [code]: "finfun_clearjunk (finfun_update_code f a b) = f(\<^sup>f a := b)"
  1.1299 +by simp
  1.1300 +
  1.1301 +subsection {* The domain of a FinFun as a FinFun *}
  1.1302 +
  1.1303 +definition finfun_dom :: "('a \<Rightarrow>\<^isub>f 'b) \<Rightarrow> ('a \<Rightarrow>\<^isub>f bool)"
  1.1304 +where [code del]: "finfun_dom f = Abs_finfun (\<lambda>a. f\<^sub>f a \<noteq> finfun_default f)"
  1.1305 +
  1.1306 +lemma finfun_dom_const:
  1.1307 +  "finfun_dom ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = (\<lambda>\<^isup>f finite (UNIV :: 'a set) \<and> c \<noteq> undefined)"
  1.1308 +unfolding finfun_dom_def finfun_default_const
  1.1309 +by(auto)(simp_all add: finfun_const_def)
  1.1310 +
  1.1311 +text {*
  1.1312 +  @{term "finfun_dom" } raises an exception when called on a FinFun whose domain is a finite type. 
  1.1313 +  For such FinFuns, the default value (and as such the domain) is undefined.
  1.1314 +*}
  1.1315 +
  1.1316 +lemma finfun_dom_const_code [code]:
  1.1317 +  "finfun_dom ((\<lambda>\<^isup>f c) :: ('a :: card_UNIV) \<Rightarrow>\<^isub>f 'b) = 
  1.1318 +   (if card_UNIV (TYPE('a)) = 0 then (\<lambda>\<^isup>f False) else FinFun.code_abort (\<lambda>_. finfun_dom (\<lambda>\<^isup>f c)))"
  1.1319 +unfolding card_UNIV_eq_0_infinite_UNIV
  1.1320 +by(simp add: finfun_dom_const)
  1.1321 +
  1.1322 +lemma finfun_dom_finfunI: "(\<lambda>a. f\<^sub>f a \<noteq> finfun_default f) \<in> finfun"
  1.1323 +using finite_finfun_default[of f]
  1.1324 +by(simp add: finfun_def finfun_apply_Rep_finfun exI[where x=False])
  1.1325 +
  1.1326 +lemma finfun_dom_update [simp]:
  1.1327 +  "finfun_dom (f(\<^sup>f a := b)) = (finfun_dom f)(\<^sup>f a := (b \<noteq> finfun_default f))"
  1.1328 +unfolding finfun_dom_def finfun_update_def
  1.1329 +apply(simp add: finfun_default_update_const finfun_upd_apply finfun_dom_finfunI)
  1.1330 +apply(fold finfun_update.rep_eq)
  1.1331 +apply(simp add: finfun_upd_apply fun_eq_iff finfun_default_update_const)
  1.1332 +done
  1.1333 +
  1.1334 +lemma finfun_dom_update_code [code]:
  1.1335 +  "finfun_dom (finfun_update_code f a b) = finfun_update_code (finfun_dom f) a (b \<noteq> finfun_default f)"
  1.1336 +by(simp)
  1.1337 +
  1.1338 +lemma finite_finfun_dom: "finite {x. (finfun_dom f)\<^sub>f x}"
  1.1339 +proof(induct f rule: finfun_weak_induct)
  1.1340 +  case (const b)
  1.1341 +  thus ?case
  1.1342 +    by (cases "finite (UNIV :: 'a set) \<and> b \<noteq> undefined")
  1.1343 +      (auto simp add: finfun_dom_const UNIV_def [symmetric] Set.empty_def [symmetric])
  1.1344 +next
  1.1345 +  case (update f a b)
  1.1346 +  have "{x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} =
  1.1347 +    (if b = finfun_default f then {x. (finfun_dom f)\<^sub>f x} - {a} else insert a {x. (finfun_dom f)\<^sub>f x})"
  1.1348 +    by (auto simp add: finfun_upd_apply split: split_if_asm)
  1.1349 +  thus ?case using update by simp
  1.1350 +qed
  1.1351 +
  1.1352 +
  1.1353 +subsection {* The domain of a FinFun as a sorted list *}
  1.1354 +
  1.1355 +definition finfun_to_list :: "('a :: linorder) \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a list"
  1.1356 +where
  1.1357 +  "finfun_to_list f = (THE xs. set xs = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs \<and> distinct xs)"
  1.1358 +
  1.1359 +lemma set_finfun_to_list [simp]: "set (finfun_to_list f) = {x. (finfun_dom f)\<^sub>f x}" (is ?thesis1)
  1.1360 +  and sorted_finfun_to_list: "sorted (finfun_to_list f)" (is ?thesis2)
  1.1361 +  and distinct_finfun_to_list: "distinct (finfun_to_list f)" (is ?thesis3)
  1.1362 +proof -
  1.1363 +  have "?thesis1 \<and> ?thesis2 \<and> ?thesis3"
  1.1364 +    unfolding finfun_to_list_def
  1.1365 +    by(rule theI')(rule finite_sorted_distinct_unique finite_finfun_dom)+
  1.1366 +  thus ?thesis1 ?thesis2 ?thesis3 by simp_all
  1.1367 +qed
  1.1368 +
  1.1369 +lemma finfun_const_False_conv_bot: "(\<lambda>\<^isup>f False)\<^sub>f = bot"
  1.1370 +by auto
  1.1371 +
  1.1372 +lemma finfun_const_True_conv_top: "(\<lambda>\<^isup>f True)\<^sub>f = top"
  1.1373 +by auto
  1.1374 +
  1.1375 +lemma finfun_to_list_const:
  1.1376 +  "finfun_to_list ((\<lambda>\<^isup>f c) :: ('a :: {linorder} \<Rightarrow>\<^isub>f 'b)) = 
  1.1377 +  (if \<not> finite (UNIV :: 'a set) \<or> c = undefined then [] else THE xs. set xs = UNIV \<and> sorted xs \<and> distinct xs)"
  1.1378 +by(auto simp add: finfun_to_list_def finfun_const_False_conv_bot finfun_const_True_conv_top finfun_dom_const)
  1.1379 +
  1.1380 +lemma finfun_to_list_const_code [code]:
  1.1381 +  "finfun_to_list ((\<lambda>\<^isup>f c) :: ('a :: {linorder, card_UNIV} \<Rightarrow>\<^isub>f 'b)) =
  1.1382 +   (if card_UNIV (TYPE('a)) = 0 then [] else FinFun.code_abort (\<lambda>_. finfun_to_list ((\<lambda>\<^isup>f c) :: ('a \<Rightarrow>\<^isub>f 'b))))"
  1.1383 +unfolding card_UNIV_eq_0_infinite_UNIV
  1.1384 +by(auto simp add: finfun_to_list_const)
  1.1385 +
  1.1386 +lemma remove1_insort_insert_same:
  1.1387 +  "x \<notin> set xs \<Longrightarrow> remove1 x (insort_insert x xs) = xs"
  1.1388 +by (metis insort_insert_insort remove1_insort)
  1.1389 +
  1.1390 +lemma finfun_dom_conv:
  1.1391 +  "(finfun_dom f)\<^sub>f x \<longleftrightarrow> f\<^sub>f x \<noteq> finfun_default f"
  1.1392 +by(induct f rule: finfun_weak_induct)(auto simp add: finfun_dom_const finfun_default_const finfun_default_update_const finfun_upd_apply)
  1.1393 +
  1.1394 +lemma finfun_to_list_update:
  1.1395 +  "finfun_to_list (f(\<^sup>f a := b)) = 
  1.1396 +  (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
  1.1397 +proof(subst finfun_to_list_def, rule the_equality)
  1.1398 +  fix xs
  1.1399 +  assume "set xs = {x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} \<and> sorted xs \<and> distinct xs"
  1.1400 +  hence eq: "set xs = {x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x}"
  1.1401 +    and [simp]: "sorted xs" "distinct xs" by simp_all
  1.1402 +  show "xs = (if b = finfun_default f then remove1 a (finfun_to_list f) else insort_insert a (finfun_to_list f))"
  1.1403 +  proof(cases "b = finfun_default f")
  1.1404 +    case True [simp]
  1.1405 +    show ?thesis
  1.1406 +    proof(cases "(finfun_dom f)\<^sub>f a")
  1.1407 +      case True
  1.1408 +      have "finfun_to_list f = insort_insert a xs"
  1.1409 +        unfolding finfun_to_list_def
  1.1410 +      proof(rule the_equality)
  1.1411 +        have "set (insort_insert a xs) = insert a (set xs)" by(simp add: set_insort_insert)
  1.1412 +        also note eq also
  1.1413 +        have "insert a {x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} = {x. (finfun_dom f)\<^sub>f x}" using True
  1.1414 +          by(auto simp add: finfun_upd_apply split: split_if_asm)
  1.1415 +        finally show 1: "set (insort_insert a xs) = {x. (finfun_dom f)\<^sub>f x} \<and> sorted (insort_insert a xs) \<and> distinct (insort_insert a xs)"
  1.1416 +          by(simp add: sorted_insort_insert distinct_insort_insert)
  1.1417 +
  1.1418 +        fix xs'
  1.1419 +        assume "set xs' = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs' \<and> distinct xs'"
  1.1420 +        thus "xs' = insort_insert a xs" using 1 by(auto dest: sorted_distinct_set_unique)
  1.1421 +      qed
  1.1422 +      with eq True show ?thesis by(simp add: remove1_insort_insert_same)
  1.1423 +    next
  1.1424 +      case False
  1.1425 +      hence "f\<^sub>f a = b" by(auto simp add: finfun_dom_conv)
  1.1426 +      hence f: "f(\<^sup>f a := b) = f" by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
  1.1427 +      from eq have "finfun_to_list f = xs" unfolding f finfun_to_list_def
  1.1428 +        by(auto elim: sorted_distinct_set_unique intro!: the_equality)
  1.1429 +      with eq False show ?thesis unfolding f by(simp add: remove1_idem)
  1.1430 +    qed
  1.1431 +  next
  1.1432 +    case False
  1.1433 +    show ?thesis
  1.1434 +    proof(cases "(finfun_dom f)\<^sub>f a")
  1.1435 +      case True
  1.1436 +      have "finfun_to_list f = xs"
  1.1437 +        unfolding finfun_to_list_def
  1.1438 +      proof(rule the_equality)
  1.1439 +        have "finfun_dom f = finfun_dom f(\<^sup>f a := b)" using False True
  1.1440 +          by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
  1.1441 +        with eq show 1: "set xs = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs \<and> distinct xs"
  1.1442 +          by(simp del: finfun_dom_update)
  1.1443 +        
  1.1444 +        fix xs'
  1.1445 +        assume "set xs' = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs' \<and> distinct xs'"
  1.1446 +        thus "xs' = xs" using 1 by(auto elim: sorted_distinct_set_unique)
  1.1447 +      qed
  1.1448 +      thus ?thesis using False True eq by(simp add: insort_insert_triv)
  1.1449 +    next
  1.1450 +      case False
  1.1451 +      have "finfun_to_list f = remove1 a xs"
  1.1452 +        unfolding finfun_to_list_def
  1.1453 +      proof(rule the_equality)
  1.1454 +        have "set (remove1 a xs) = set xs - {a}" by simp
  1.1455 +        also note eq also
  1.1456 +        have "{x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} - {a} = {x. (finfun_dom f)\<^sub>f x}" using False
  1.1457 +          by(auto simp add: finfun_upd_apply split: split_if_asm)
  1.1458 +        finally show 1: "set (remove1 a xs) = {x. (finfun_dom f)\<^sub>f x} \<and> sorted (remove1 a xs) \<and> distinct (remove1 a xs)"
  1.1459 +          by(simp add: sorted_remove1)
  1.1460 +        
  1.1461 +        fix xs'
  1.1462 +        assume "set xs' = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs' \<and> distinct xs'"
  1.1463 +        thus "xs' = remove1 a xs" using 1 by(blast intro: sorted_distinct_set_unique)
  1.1464 +      qed
  1.1465 +      thus ?thesis using False eq `b \<noteq> finfun_default f` 
  1.1466 +        by (simp add: insort_insert_insort insort_remove1)
  1.1467 +    qed
  1.1468 +  qed
  1.1469 +qed (auto simp add: distinct_finfun_to_list sorted_finfun_to_list sorted_remove1 set_insort_insert sorted_insort_insert distinct_insort_insert finfun_upd_apply split: split_if_asm)
  1.1470 +
  1.1471 +lemma finfun_to_list_update_code [code]:
  1.1472 +  "finfun_to_list (finfun_update_code f a b) = 
  1.1473 +  (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
  1.1474 +by(simp add: finfun_to_list_update)
  1.1475 +
  1.1476 +end