1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Library/Fin_Fun.thy Tue Jun 02 15:53:34 2009 +0200
1.3 @@ -0,0 +1,1661 @@
1.4 +
1.5 +(* Author: Andreas Lochbihler, Uni Karlsruhe *)
1.6 +
1.7 +header {* Almost everywhere constant functions *}
1.8 +
1.9 +theory Fin_Fun
1.10 +imports Main Infinite_Set Enum
1.11 +begin
1.12 +
1.13 +text {*
1.14 + This theory defines functions which are constant except for finitely
1.15 + many points (FinFun) and introduces a type finfin along with a
1.16 + number of operators for them. The code generator is set up such that
1.17 + such functions can be represented as data in the generated code and
1.18 + all operators are executable.
1.19 +
1.20 + For details, see Formalising FinFuns - Generating Code for Functions as Data by A. Lochbihler in TPHOLs 2009.
1.21 +*}
1.22 +
1.23 +subsection {* Auxiliary definitions and lemmas *}
1.24 +
1.25 +(*FIXME move these to Finite_Set.thy*)
1.26 +lemma card_ge_0_finite:
1.27 + "card A > 0 \<Longrightarrow> finite A"
1.28 +by(rule ccontr, drule card_infinite, simp)
1.29 +
1.30 +lemma finite_UNIV_card_ge_0:
1.31 + "finite (UNIV :: 'a set) \<Longrightarrow> card (UNIV :: 'a set) > 0"
1.32 +by(rule ccontr) simp
1.33 +
1.34 +lemma card_eq_UNIV_imp_eq_UNIV:
1.35 + assumes fin: "finite (UNIV :: 'a set)"
1.36 + and card: "card A = card (UNIV :: 'a set)"
1.37 + shows "A = (UNIV :: 'a set)"
1.38 +apply -
1.39 + proof
1.40 + show "A \<subseteq> UNIV" by simp
1.41 + show "UNIV \<subseteq> A"
1.42 + proof
1.43 + fix x
1.44 + show "x \<in> A"
1.45 + proof(rule ccontr)
1.46 + assume "x \<notin> A"
1.47 + hence "A \<subset> UNIV" by auto
1.48 + from psubset_card_mono[OF fin this] card show False by simp
1.49 + qed
1.50 + qed
1.51 +qed
1.52 +
1.53 +lemma finite_fun_UNIVD2: assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
1.54 + shows "finite (UNIV :: 'b set)"
1.55 +proof -
1.56 + from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))"
1.57 + by(rule finite_imageI)
1.58 + moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary)"
1.59 + by(rule UNIV_eq_I) auto
1.60 + ultimately show "finite (UNIV :: 'b set)" by simp
1.61 +qed
1.62 +
1.63 +lemma finite_fun_UNIVD1: assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
1.64 + and card: "card (UNIV :: 'b set) \<noteq> Suc 0"
1.65 + shows "finite (UNIV :: 'a set)"
1.66 +proof -
1.67 + from fin have finb: "finite (UNIV :: 'b set)" by(rule finite_fun_UNIVD2)
1.68 + with card have "card (UNIV :: 'b set) \<ge> Suc (Suc 0)"
1.69 + by(cases "card (UNIV :: 'b set)")(auto simp add: card_eq_0_iff)
1.70 + then obtain n where "card (UNIV :: 'b set) = Suc (Suc n)" "n = card (UNIV :: 'b set) - 2" by(auto)
1.71 + then obtain b1 b2 where b1b2: "(b1 :: 'b) \<noteq> (b2 :: 'b)" by(auto simp add: card_Suc_eq)
1.72 + from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1))" by(rule finite_imageI)
1.73 + moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1)"
1.74 + proof(rule UNIV_eq_I)
1.75 + fix x :: 'a
1.76 + from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" by(simp add: inv_def)
1.77 + thus "x \<in> range (\<lambda>f\<Colon>'a \<Rightarrow> 'b. inv f b1)" by blast
1.78 + qed
1.79 + ultimately show "finite (UNIV :: 'a set)" by simp
1.80 +qed
1.81 +
1.82 +(*FIXME move to Map.thy*)
1.83 +lemma restrict_map_insert: "f |` (insert a A) = (f |` A)(a := f a)"
1.84 +by(auto simp add: restrict_map_def intro: ext)
1.85 +
1.86 +definition map_default :: "'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
1.87 +where "map_default b f a \<equiv> case f a of None \<Rightarrow> b | Some b' \<Rightarrow> b'"
1.88 +
1.89 +lemma map_default_delete [simp]:
1.90 + "map_default b (f(a := None)) = (map_default b f)(a := b)"
1.91 +by(simp add: map_default_def expand_fun_eq)
1.92 +
1.93 +lemma map_default_insert:
1.94 + "map_default b (f(a \<mapsto> b')) = (map_default b f)(a := b')"
1.95 +by(simp add: map_default_def expand_fun_eq)
1.96 +
1.97 +lemma map_default_empty [simp]: "map_default b empty = (\<lambda>a. b)"
1.98 +by(simp add: expand_fun_eq map_default_def)
1.99 +
1.100 +lemma map_default_inject:
1.101 + fixes g g' :: "'a \<rightharpoonup> 'b"
1.102 + assumes infin_eq: "\<not> finite (UNIV :: 'a set) \<or> b = b'"
1.103 + and fin: "finite (dom g)" and b: "b \<notin> ran g"
1.104 + and fin': "finite (dom g')" and b': "b' \<notin> ran g'"
1.105 + and eq': "map_default b g = map_default b' g'"
1.106 + shows "b = b'" "g = g'"
1.107 +proof -
1.108 + from infin_eq show bb': "b = b'"
1.109 + proof
1.110 + assume infin: "\<not> finite (UNIV :: 'a set)"
1.111 + from fin fin' have "finite (dom g \<union> dom g')" by auto
1.112 + with infin have "UNIV - (dom g \<union> dom g') \<noteq> {}" by(auto dest: finite_subset)
1.113 + then obtain a where a: "a \<notin> dom g \<union> dom g'" by auto
1.114 + hence "map_default b g a = b" "map_default b' g' a = b'" by(auto simp add: map_default_def)
1.115 + with eq' show "b = b'" by simp
1.116 + qed
1.117 +
1.118 + show "g = g'"
1.119 + proof
1.120 + fix x
1.121 + show "g x = g' x"
1.122 + proof(cases "g x")
1.123 + case None
1.124 + hence "map_default b g x = b" by(simp add: map_default_def)
1.125 + with bb' eq' have "map_default b' g' x = b'" by simp
1.126 + with b' have "g' x = None" by(simp add: map_default_def ran_def split: option.split_asm)
1.127 + with None show ?thesis by simp
1.128 + next
1.129 + case (Some c)
1.130 + with b have cb: "c \<noteq> b" by(auto simp add: ran_def)
1.131 + moreover from Some have "map_default b g x = c" by(simp add: map_default_def)
1.132 + with eq' have "map_default b' g' x = c" by simp
1.133 + ultimately have "g' x = Some c" using b' bb' by(auto simp add: map_default_def split: option.splits)
1.134 + with Some show ?thesis by simp
1.135 + qed
1.136 + qed
1.137 +qed
1.138 +
1.139 +subsection {* The finfun type *}
1.140 +
1.141 +typedef ('a,'b) finfun = "{f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}"
1.142 +apply(auto)
1.143 +apply(rule_tac x="\<lambda>x. arbitrary" in exI)
1.144 +apply(auto)
1.145 +done
1.146 +
1.147 +syntax
1.148 + "finfun" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ \<Rightarrow>\<^isub>f /_)" [22, 21] 21)
1.149 +
1.150 +lemma fun_upd_finfun: "y(a := b) \<in> finfun \<longleftrightarrow> y \<in> finfun"
1.151 +proof -
1.152 + { fix b'
1.153 + have "finite {a'. (y(a := b)) a' \<noteq> b'} = finite {a'. y a' \<noteq> b'}"
1.154 + proof(cases "b = b'")
1.155 + case True
1.156 + hence "{a'. (y(a := b)) a' \<noteq> b'} = {a'. y a' \<noteq> b'} - {a}" by auto
1.157 + thus ?thesis by simp
1.158 + next
1.159 + case False
1.160 + hence "{a'. (y(a := b)) a' \<noteq> b'} = insert a {a'. y a' \<noteq> b'}" by auto
1.161 + thus ?thesis by simp
1.162 + qed }
1.163 + thus ?thesis unfolding finfun_def by blast
1.164 +qed
1.165 +
1.166 +lemma const_finfun: "(\<lambda>x. a) \<in> finfun"
1.167 +by(auto simp add: finfun_def)
1.168 +
1.169 +lemma finfun_left_compose:
1.170 + assumes "y \<in> finfun"
1.171 + shows "g \<circ> y \<in> finfun"
1.172 +proof -
1.173 + from assms obtain b where "finite {a. y a \<noteq> b}"
1.174 + unfolding finfun_def by blast
1.175 + hence "finite {c. g (y c) \<noteq> g b}"
1.176 + proof(induct x\<equiv>"{a. y a \<noteq> b}" arbitrary: y)
1.177 + case empty
1.178 + hence "y = (\<lambda>a. b)" by(auto intro: ext)
1.179 + thus ?case by(simp)
1.180 + next
1.181 + case (insert x F)
1.182 + note IH = `\<And>y. F = {a. y a \<noteq> b} \<Longrightarrow> finite {c. g (y c) \<noteq> g b}`
1.183 + from `insert x F = {a. y a \<noteq> b}` `x \<notin> F`
1.184 + have F: "F = {a. (y(x := b)) a \<noteq> b}" by(auto)
1.185 + show ?case
1.186 + proof(cases "g (y x) = g b")
1.187 + case True
1.188 + hence "{c. g ((y(x := b)) c) \<noteq> g b} = {c. g (y c) \<noteq> g b}" by auto
1.189 + with IH[OF F] show ?thesis by simp
1.190 + next
1.191 + case False
1.192 + hence "{c. g (y c) \<noteq> g b} = insert x {c. g ((y(x := b)) c) \<noteq> g b}" by auto
1.193 + with IH[OF F] show ?thesis by(simp)
1.194 + qed
1.195 + qed
1.196 + thus ?thesis unfolding finfun_def by auto
1.197 +qed
1.198 +
1.199 +lemma assumes "y \<in> finfun"
1.200 + shows fst_finfun: "fst \<circ> y \<in> finfun"
1.201 + and snd_finfun: "snd \<circ> y \<in> finfun"
1.202 +proof -
1.203 + from assms obtain b c where bc: "finite {a. y a \<noteq> (b, c)}"
1.204 + unfolding finfun_def by auto
1.205 + have "{a. fst (y a) \<noteq> b} \<subseteq> {a. y a \<noteq> (b, c)}"
1.206 + and "{a. snd (y a) \<noteq> c} \<subseteq> {a. y a \<noteq> (b, c)}" by auto
1.207 + hence "finite {a. fst (y a) \<noteq> b}"
1.208 + and "finite {a. snd (y a) \<noteq> c}" using bc by(auto intro: finite_subset)
1.209 + thus "fst \<circ> y \<in> finfun" "snd \<circ> y \<in> finfun"
1.210 + unfolding finfun_def by auto
1.211 +qed
1.212 +
1.213 +lemma map_of_finfun: "map_of xs \<in> finfun"
1.214 +unfolding finfun_def
1.215 +by(induct xs)(auto simp add: Collect_neg_eq Collect_conj_eq Collect_imp_eq intro: finite_subset)
1.216 +
1.217 +lemma Diag_finfun: "(\<lambda>x. (f x, g x)) \<in> finfun \<longleftrightarrow> f \<in> finfun \<and> g \<in> finfun"
1.218 +by(auto intro: finite_subset simp add: Collect_neg_eq Collect_imp_eq Collect_conj_eq finfun_def)
1.219 +
1.220 +lemma finfun_right_compose:
1.221 + assumes g: "g \<in> finfun" and inj: "inj f"
1.222 + shows "g o f \<in> finfun"
1.223 +proof -
1.224 + from g obtain b where b: "finite {a. g a \<noteq> b}" unfolding finfun_def by blast
1.225 + moreover have "f ` {a. g (f a) \<noteq> b} \<subseteq> {a. g a \<noteq> b}" by auto
1.226 + moreover from inj have "inj_on f {a. g (f a) \<noteq> b}" by(rule subset_inj_on) blast
1.227 + ultimately have "finite {a. g (f a) \<noteq> b}"
1.228 + by(blast intro: finite_imageD[where f=f] finite_subset)
1.229 + thus ?thesis unfolding finfun_def by auto
1.230 +qed
1.231 +
1.232 +lemma finfun_curry:
1.233 + assumes fin: "f \<in> finfun"
1.234 + shows "curry f \<in> finfun" "curry f a \<in> finfun"
1.235 +proof -
1.236 + from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast
1.237 + moreover have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force)
1.238 + hence "{a. curry f a \<noteq> (\<lambda>b. c)} = fst ` {ab. f ab \<noteq> c}"
1.239 + by(auto simp add: curry_def expand_fun_eq)
1.240 + ultimately have "finite {a. curry f a \<noteq> (\<lambda>b. c)}" by simp
1.241 + thus "curry f \<in> finfun" unfolding finfun_def by blast
1.242 +
1.243 + have "snd ` {ab. f ab \<noteq> c} = {b. \<exists>a. f (a, b) \<noteq> c}" by(force)
1.244 + hence "{b. f (a, b) \<noteq> c} \<subseteq> snd ` {ab. f ab \<noteq> c}" by auto
1.245 + hence "finite {b. f (a, b) \<noteq> c}" by(rule finite_subset)(rule finite_imageI[OF c])
1.246 + thus "curry f a \<in> finfun" unfolding finfun_def by auto
1.247 +qed
1.248 +
1.249 +lemmas finfun_simp =
1.250 + fst_finfun snd_finfun Abs_finfun_inverse Rep_finfun_inverse Abs_finfun_inject Rep_finfun_inject Diag_finfun finfun_curry
1.251 +lemmas finfun_iff = const_finfun fun_upd_finfun Rep_finfun map_of_finfun
1.252 +lemmas finfun_intro = finfun_left_compose fst_finfun snd_finfun
1.253 +
1.254 +lemma Abs_finfun_inject_finite:
1.255 + fixes x y :: "'a \<Rightarrow> 'b"
1.256 + assumes fin: "finite (UNIV :: 'a set)"
1.257 + shows "Abs_finfun x = Abs_finfun y \<longleftrightarrow> x = y"
1.258 +proof
1.259 + assume "Abs_finfun x = Abs_finfun y"
1.260 + moreover have "x \<in> finfun" "y \<in> finfun" unfolding finfun_def
1.261 + by(auto intro: finite_subset[OF _ fin])
1.262 + ultimately show "x = y" by(simp add: Abs_finfun_inject)
1.263 +qed simp
1.264 +
1.265 +lemma Abs_finfun_inject_finite_class:
1.266 + fixes x y :: "('a :: finite) \<Rightarrow> 'b"
1.267 + shows "Abs_finfun x = Abs_finfun y \<longleftrightarrow> x = y"
1.268 +using finite_UNIV
1.269 +by(simp add: Abs_finfun_inject_finite)
1.270 +
1.271 +lemma Abs_finfun_inj_finite:
1.272 + assumes fin: "finite (UNIV :: 'a set)"
1.273 + shows "inj (Abs_finfun :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b)"
1.274 +proof(rule inj_onI)
1.275 + fix x y :: "'a \<Rightarrow> 'b"
1.276 + assume "Abs_finfun x = Abs_finfun y"
1.277 + moreover have "x \<in> finfun" "y \<in> finfun" unfolding finfun_def
1.278 + by(auto intro: finite_subset[OF _ fin])
1.279 + ultimately show "x = y" by(simp add: Abs_finfun_inject)
1.280 +qed
1.281 +
1.282 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1.283 +
1.284 +lemma Abs_finfun_inverse_finite:
1.285 + fixes x :: "'a \<Rightarrow> 'b"
1.286 + assumes fin: "finite (UNIV :: 'a set)"
1.287 + shows "Rep_finfun (Abs_finfun x) = x"
1.288 +proof -
1.289 + from fin have "x \<in> finfun"
1.290 + by(auto simp add: finfun_def intro: finite_subset)
1.291 + thus ?thesis by simp
1.292 +qed
1.293 +
1.294 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1.295 +
1.296 +lemma Abs_finfun_inverse_finite_class:
1.297 + fixes x :: "('a :: finite) \<Rightarrow> 'b"
1.298 + shows "Rep_finfun (Abs_finfun x) = x"
1.299 +using finite_UNIV by(simp add: Abs_finfun_inverse_finite)
1.300 +
1.301 +lemma finfun_eq_finite_UNIV: "finite (UNIV :: 'a set) \<Longrightarrow> (finfun :: ('a \<Rightarrow> 'b) set) = UNIV"
1.302 +unfolding finfun_def by(auto intro: finite_subset)
1.303 +
1.304 +lemma finfun_finite_UNIV_class: "finfun = (UNIV :: ('a :: finite \<Rightarrow> 'b) set)"
1.305 +by(simp add: finfun_eq_finite_UNIV)
1.306 +
1.307 +lemma map_default_in_finfun:
1.308 + assumes fin: "finite (dom f)"
1.309 + shows "map_default b f \<in> finfun"
1.310 +unfolding finfun_def
1.311 +proof(intro CollectI exI)
1.312 + from fin show "finite {a. map_default b f a \<noteq> b}"
1.313 + by(auto simp add: map_default_def dom_def Collect_conj_eq split: option.splits)
1.314 +qed
1.315 +
1.316 +lemma finfun_cases_map_default:
1.317 + obtains b g where "f = Abs_finfun (map_default b g)" "finite (dom g)" "b \<notin> ran g"
1.318 +proof -
1.319 + obtain y where f: "f = Abs_finfun y" and y: "y \<in> finfun" by(cases f)
1.320 + from y obtain b where b: "finite {a. y a \<noteq> b}" unfolding finfun_def by auto
1.321 + let ?g = "(\<lambda>a. if y a = b then None else Some (y a))"
1.322 + have "map_default b ?g = y" by(simp add: expand_fun_eq map_default_def)
1.323 + with f have "f = Abs_finfun (map_default b ?g)" by simp
1.324 + moreover from b have "finite (dom ?g)" by(auto simp add: dom_def)
1.325 + moreover have "b \<notin> ran ?g" by(auto simp add: ran_def)
1.326 + ultimately show ?thesis by(rule that)
1.327 +qed
1.328 +
1.329 +
1.330 +subsection {* Kernel functions for type @{typ "'a \<Rightarrow>\<^isub>f 'b"} *}
1.331 +
1.332 +definition finfun_const :: "'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("\<lambda>\<^isup>f/ _" [0] 1)
1.333 +where [code del]: "(\<lambda>\<^isup>f b) = Abs_finfun (\<lambda>x. b)"
1.334 +
1.335 +definition finfun_update :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("_'(\<^sup>f/ _ := _')" [1000,0,0] 1000)
1.336 +where [code del]: "f(\<^sup>fa := b) = Abs_finfun ((Rep_finfun f)(a := b))"
1.337 +
1.338 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1.339 +
1.340 +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.341 +by(simp add: finfun_update_def fun_upd_twist)
1.342 +
1.343 +lemma finfun_update_twice [simp]:
1.344 + "finfun_update (finfun_update f a b) a b' = finfun_update f a b'"
1.345 +by(simp add: finfun_update_def)
1.346 +
1.347 +lemma finfun_update_const_same: "(\<lambda>\<^isup>f b)(\<^sup>f a := b) = (\<lambda>\<^isup>f b)"
1.348 +by(simp add: finfun_update_def finfun_const_def expand_fun_eq)
1.349 +
1.350 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1.351 +
1.352 +subsection {* Code generator setup *}
1.353 +
1.354 +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)
1.355 +where [simp, code del]: "finfun_update_code = finfun_update"
1.356 +
1.357 +code_datatype finfun_const finfun_update_code
1.358 +
1.359 +lemma finfun_update_const_code [code]:
1.360 + "(\<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.361 +by(simp add: finfun_update_const_same)
1.362 +
1.363 +lemma finfun_update_update_code [code]:
1.364 + "(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.365 +by(simp add: finfun_update_twist)
1.366 +
1.367 +
1.368 +subsection {* Setup for quickcheck *}
1.369 +
1.370 +notation fcomp (infixl "o>" 60)
1.371 +notation scomp (infixl "o\<rightarrow>" 60)
1.372 +
1.373 +definition (in term_syntax) valtermify_finfun_const ::
1.374 + "'b\<Colon>typerep \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> ('a\<Colon>typerep \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Eval.term)" where
1.375 + "valtermify_finfun_const y = Code_Eval.valtermify finfun_const {\<cdot>} y"
1.376 +
1.377 +definition (in term_syntax) valtermify_finfun_update_code ::
1.378 + "'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
1.379 + "valtermify_finfun_update_code x y f = Code_Eval.valtermify finfun_update_code {\<cdot>} f {\<cdot>} x {\<cdot>} y"
1.380 +
1.381 +instantiation finfun :: (random, random) random
1.382 +begin
1.383 +
1.384 +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
1.385 + "random_finfun' 0 j = Quickcheck.collapse (Random.select_default 0
1.386 + (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))
1.387 + (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y))))"
1.388 + | "random_finfun' (Suc_code_numeral i) j = Quickcheck.collapse (Random.select_default i
1.389 + (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)))))
1.390 + (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y))))"
1.391 +
1.392 +definition
1.393 + "random i = random_finfun' i i"
1.394 +
1.395 +instance ..
1.396 +
1.397 +end
1.398 +
1.399 +lemma select_default_zero:
1.400 + "Random.select_default 0 y y = Random.select_default 0 x y"
1.401 + by (simp add: select_default_def)
1.402 +
1.403 +lemma random_finfun'_code [code]:
1.404 + "random_finfun' i j = Quickcheck.collapse (Random.select_default (i - 1)
1.405 + (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)))))
1.406 + (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y))))"
1.407 + apply (cases i rule: code_numeral.exhaust)
1.408 + apply (simp_all only: random_finfun'.simps code_numeral_zero_minus_one Suc_code_numeral_minus_one)
1.409 + apply (subst select_default_zero) apply (simp only:)
1.410 + done
1.411 +
1.412 +no_notation fcomp (infixl "o>" 60)
1.413 +no_notation scomp (infixl "o\<rightarrow>" 60)
1.414 +
1.415 +
1.416 +subsection {* @{text "finfun_update"} as instance of @{text "fun_left_comm"} *}
1.417 +
1.418 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1.419 +
1.420 +interpretation finfun_update: fun_left_comm "\<lambda>a f. f(\<^sup>f a :: 'a := b')"
1.421 +proof
1.422 + fix a' a :: 'a
1.423 + fix b
1.424 + have "(Rep_finfun b)(a := b', a' := b') = (Rep_finfun b)(a' := b', a := b')"
1.425 + by(cases "a = a'")(auto simp add: fun_upd_twist)
1.426 + thus "b(\<^sup>f a := b')(\<^sup>f a' := b') = b(\<^sup>f a' := b')(\<^sup>f a := b')"
1.427 + by(auto simp add: finfun_update_def fun_upd_twist)
1.428 +qed
1.429 +
1.430 +lemma fold_finfun_update_finite_univ:
1.431 + assumes fin: "finite (UNIV :: 'a set)"
1.432 + shows "fold (\<lambda>a f. f(\<^sup>f a := b')) (\<lambda>\<^isup>f b) (UNIV :: 'a set) = (\<lambda>\<^isup>f b')"
1.433 +proof -
1.434 + { fix A :: "'a set"
1.435 + from fin have "finite A" by(auto intro: finite_subset)
1.436 + 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)"
1.437 + proof(induct)
1.438 + case (insert x F)
1.439 + 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.440 + by(auto intro: ext)
1.441 + with insert show ?case
1.442 + by(simp add: finfun_const_def fun_upd_def)(simp add: finfun_update_def Abs_finfun_inverse_finite[OF fin] fun_upd_def)
1.443 + qed(simp add: finfun_const_def) }
1.444 + thus ?thesis by(simp add: finfun_const_def)
1.445 +qed
1.446 +
1.447 +
1.448 +subsection {* Default value for FinFuns *}
1.449 +
1.450 +definition finfun_default_aux :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"
1.451 +where [code del]: "finfun_default_aux f = (if finite (UNIV :: 'a set) then arbitrary else THE b. finite {a. f a \<noteq> b})"
1.452 +
1.453 +lemma finfun_default_aux_infinite:
1.454 + fixes f :: "'a \<Rightarrow> 'b"
1.455 + assumes infin: "infinite (UNIV :: 'a set)"
1.456 + and fin: "finite {a. f a \<noteq> b}"
1.457 + shows "finfun_default_aux f = b"
1.458 +proof -
1.459 + let ?B = "{a. f a \<noteq> b}"
1.460 + from fin have "(THE b. finite {a. f a \<noteq> b}) = b"
1.461 + proof(rule the_equality)
1.462 + fix b'
1.463 + assume "finite {a. f a \<noteq> b'}" (is "finite ?B'")
1.464 + with infin fin have "UNIV - (?B' \<union> ?B) \<noteq> {}" by(auto dest: finite_subset)
1.465 + then obtain a where a: "a \<notin> ?B' \<union> ?B" by auto
1.466 + thus "b' = b" by auto
1.467 + qed
1.468 + thus ?thesis using infin by(simp add: finfun_default_aux_def)
1.469 +qed
1.470 +
1.471 +
1.472 +lemma finite_finfun_default_aux:
1.473 + fixes f :: "'a \<Rightarrow> 'b"
1.474 + assumes fin: "f \<in> finfun"
1.475 + shows "finite {a. f a \<noteq> finfun_default_aux f}"
1.476 +proof(cases "finite (UNIV :: 'a set)")
1.477 + case True thus ?thesis using fin
1.478 + by(auto simp add: finfun_def finfun_default_aux_def intro: finite_subset)
1.479 +next
1.480 + case False
1.481 + from fin obtain b where b: "finite {a. f a \<noteq> b}" (is "finite ?B")
1.482 + unfolding finfun_def by blast
1.483 + with False show ?thesis by(simp add: finfun_default_aux_infinite)
1.484 +qed
1.485 +
1.486 +lemma finfun_default_aux_update_const:
1.487 + fixes f :: "'a \<Rightarrow> 'b"
1.488 + assumes fin: "f \<in> finfun"
1.489 + shows "finfun_default_aux (f(a := b)) = finfun_default_aux f"
1.490 +proof(cases "finite (UNIV :: 'a set)")
1.491 + case False
1.492 + from fin obtain b' where b': "finite {a. f a \<noteq> b'}" unfolding finfun_def by blast
1.493 + hence "finite {a'. (f(a := b)) a' \<noteq> b'}"
1.494 + proof(cases "b = b' \<and> f a \<noteq> b'")
1.495 + case True
1.496 + hence "{a. f a \<noteq> b'} = insert a {a'. (f(a := b)) a' \<noteq> b'}" by auto
1.497 + thus ?thesis using b' by simp
1.498 + next
1.499 + case False
1.500 + moreover
1.501 + { assume "b \<noteq> b'"
1.502 + hence "{a'. (f(a := b)) a' \<noteq> b'} = insert a {a. f a \<noteq> b'}" by auto
1.503 + hence ?thesis using b' by simp }
1.504 + moreover
1.505 + { assume "b = b'" "f a = b'"
1.506 + hence "{a'. (f(a := b)) a' \<noteq> b'} = {a. f a \<noteq> b'}" by auto
1.507 + hence ?thesis using b' by simp }
1.508 + ultimately show ?thesis by blast
1.509 + qed
1.510 + with False b' show ?thesis by(auto simp del: fun_upd_apply simp add: finfun_default_aux_infinite)
1.511 +next
1.512 + case True thus ?thesis by(simp add: finfun_default_aux_def)
1.513 +qed
1.514 +
1.515 +definition finfun_default :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'b"
1.516 + where [code del]: "finfun_default f = finfun_default_aux (Rep_finfun f)"
1.517 +
1.518 +lemma finite_finfun_default: "finite {a. Rep_finfun f a \<noteq> finfun_default f}"
1.519 +unfolding finfun_default_def by(simp add: finite_finfun_default_aux)
1.520 +
1.521 +lemma finfun_default_const: "finfun_default ((\<lambda>\<^isup>f b) :: 'a \<Rightarrow>\<^isub>f 'b) = (if finite (UNIV :: 'a set) then arbitrary else b)"
1.522 +apply(auto simp add: finfun_default_def finfun_const_def finfun_default_aux_infinite)
1.523 +apply(simp add: finfun_default_aux_def)
1.524 +done
1.525 +
1.526 +lemma finfun_default_update_const:
1.527 + "finfun_default (f(\<^sup>f a := b)) = finfun_default f"
1.528 +unfolding finfun_default_def finfun_update_def
1.529 +by(simp add: finfun_default_aux_update_const)
1.530 +
1.531 +subsection {* Recursion combinator and well-formedness conditions *}
1.532 +
1.533 +definition finfun_rec :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<Rightarrow> 'c"
1.534 +where [code del]:
1.535 + "finfun_rec cnst upd f \<equiv>
1.536 + let b = finfun_default f;
1.537 + g = THE g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g
1.538 + in fold (\<lambda>a. upd a (map_default b g a)) (cnst b) (dom g)"
1.539 +
1.540 +locale finfun_rec_wf_aux =
1.541 + fixes cnst :: "'b \<Rightarrow> 'c"
1.542 + and upd :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c"
1.543 + assumes upd_const_same: "upd a b (cnst b) = cnst b"
1.544 + and upd_commute: "a \<noteq> a' \<Longrightarrow> upd a b (upd a' b' c) = upd a' b' (upd a b c)"
1.545 + and upd_idemp: "b \<noteq> b' \<Longrightarrow> upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)"
1.546 +begin
1.547 +
1.548 +
1.549 +lemma upd_left_comm: "fun_left_comm (\<lambda>a. upd a (f a))"
1.550 +by(unfold_locales)(auto intro: upd_commute)
1.551 +
1.552 +lemma upd_upd_twice: "upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)"
1.553 +by(cases "b \<noteq> b'")(auto simp add: fun_upd_def upd_const_same upd_idemp)
1.554 +
1.555 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1.556 +
1.557 +lemma map_default_update_const:
1.558 + assumes fin: "finite (dom f)"
1.559 + and anf: "a \<notin> dom f"
1.560 + and fg: "f \<subseteq>\<^sub>m g"
1.561 + shows "upd a d (fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f)) =
1.562 + fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f)"
1.563 +proof -
1.564 + let ?upd = "\<lambda>a. upd a (map_default d g a)"
1.565 + let ?fr = "\<lambda>A. fold ?upd (cnst d) A"
1.566 + interpret gwf: fun_left_comm "?upd" by(rule upd_left_comm)
1.567 +
1.568 + from fin anf fg show ?thesis
1.569 + proof(induct A\<equiv>"dom f" arbitrary: f)
1.570 + case empty
1.571 + from `{} = dom f` have "f = empty" by(auto simp add: dom_def intro: ext)
1.572 + thus ?case by(simp add: finfun_const_def upd_const_same)
1.573 + next
1.574 + case (insert a' A)
1.575 + 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)`
1.576 + note fin = `finite A` note anf = `a \<notin> dom f` note a'nA = `a' \<notin> A`
1.577 + note domf = `insert a' A = dom f` note fg = `f \<subseteq>\<^sub>m g`
1.578 +
1.579 + from domf obtain b where b: "f a' = Some b" by auto
1.580 + let ?f' = "f(a' := None)"
1.581 + have "upd a d (?fr (insert a' A)) = upd a d (upd a' (map_default d g a') (?fr A))"
1.582 + by(subst gwf.fold_insert[OF fin a'nA]) rule
1.583 + also from b fg have "g a' = f a'" by(auto simp add: map_le_def intro: domI dest: bspec)
1.584 + hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def)
1.585 + also from anf domf have "a \<noteq> a'" by auto note upd_commute[OF this]
1.586 + 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.587 + note A also note IH[OF `a \<notin> dom ?f'` `?f' \<subseteq>\<^sub>m g` A]
1.588 + also have "upd a' (map_default d f a') (?fr (dom (f(a' := None)))) = ?fr (dom f)"
1.589 + unfolding domf[symmetric] gwf.fold_insert[OF fin a'nA] ga' unfolding A ..
1.590 + also have "insert a' (dom ?f') = dom f" using domf by auto
1.591 + finally show ?case .
1.592 + qed
1.593 +qed
1.594 +
1.595 +lemma map_default_update_twice:
1.596 + assumes fin: "finite (dom f)"
1.597 + and anf: "a \<notin> dom f"
1.598 + and fg: "f \<subseteq>\<^sub>m g"
1.599 + shows "upd a d'' (upd a d' (fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f))) =
1.600 + upd a d'' (fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f))"
1.601 +proof -
1.602 + let ?upd = "\<lambda>a. upd a (map_default d g a)"
1.603 + let ?fr = "\<lambda>A. fold ?upd (cnst d) A"
1.604 + interpret gwf: fun_left_comm "?upd" by(rule upd_left_comm)
1.605 +
1.606 + from fin anf fg show ?thesis
1.607 + proof(induct A\<equiv>"dom f" arbitrary: f)
1.608 + case empty
1.609 + from `{} = dom f` have "f = empty" by(auto simp add: dom_def intro: ext)
1.610 + thus ?case by(auto simp add: finfun_const_def finfun_update_def upd_upd_twice)
1.611 + next
1.612 + case (insert a' A)
1.613 + 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))`
1.614 + note fin = `finite A` note anf = `a \<notin> dom f` note a'nA = `a' \<notin> A`
1.615 + note domf = `insert a' A = dom f` note fg = `f \<subseteq>\<^sub>m g`
1.616 +
1.617 + from domf obtain b where b: "f a' = Some b" by auto
1.618 + let ?f' = "f(a' := None)"
1.619 + let ?b' = "case f a' of None \<Rightarrow> d | Some b \<Rightarrow> b"
1.620 + 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.621 + also note gwf.fold_insert[OF fin a'nA]
1.622 + also from b fg have "g a' = f a'" by(auto simp add: map_le_def intro: domI dest: bspec)
1.623 + hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def)
1.624 + also from anf domf have ana': "a \<noteq> a'" by auto note upd_commute[OF this]
1.625 + also note upd_commute[OF ana']
1.626 + 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.627 + note A also note IH[OF `a \<notin> dom ?f'` `?f' \<subseteq>\<^sub>m g` A]
1.628 + also note upd_commute[OF ana'[symmetric]] also note ga'[symmetric] also note A[symmetric]
1.629 + also note gwf.fold_insert[symmetric, OF fin a'nA] also note domf
1.630 + finally show ?case .
1.631 + qed
1.632 +qed
1.633 +
1.634 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1.635 +
1.636 +lemma map_default_eq_id [simp]: "map_default d ((\<lambda>a. Some (f a)) |` {a. f a \<noteq> d}) = f"
1.637 +by(auto simp add: map_default_def restrict_map_def intro: ext)
1.638 +
1.639 +lemma finite_rec_cong1:
1.640 + assumes f: "fun_left_comm f" and g: "fun_left_comm g"
1.641 + and fin: "finite A"
1.642 + and eq: "\<And>a. a \<in> A \<Longrightarrow> f a = g a"
1.643 + shows "fold f z A = fold g z A"
1.644 +proof -
1.645 + interpret f: fun_left_comm f by(rule f)
1.646 + interpret g: fun_left_comm g by(rule g)
1.647 + { fix B
1.648 + assume BsubA: "B \<subseteq> A"
1.649 + with fin have "finite B" by(blast intro: finite_subset)
1.650 + hence "B \<subseteq> A \<Longrightarrow> fold f z B = fold g z B"
1.651 + proof(induct)
1.652 + case empty thus ?case by simp
1.653 + next
1.654 + case (insert a B)
1.655 + note finB = `finite B` note anB = `a \<notin> B` note sub = `insert a B \<subseteq> A`
1.656 + note IH = `B \<subseteq> A \<Longrightarrow> fold f z B = fold g z B`
1.657 + from sub anB have BpsubA: "B \<subset> A" and BsubA: "B \<subseteq> A" and aA: "a \<in> A" by auto
1.658 + from IH[OF BsubA] eq[OF aA] finB anB
1.659 + show ?case by(auto)
1.660 + qed
1.661 + with BsubA have "fold f z B = fold g z B" by blast }
1.662 + thus ?thesis by blast
1.663 +qed
1.664 +
1.665 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1.666 +
1.667 +lemma finfun_rec_upd [simp]:
1.668 + "finfun_rec cnst upd (f(\<^sup>f a' := b')) = upd a' b' (finfun_rec cnst upd f)"
1.669 +proof -
1.670 + obtain b where b: "b = finfun_default f" by auto
1.671 + let ?the = "\<lambda>f g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g"
1.672 + obtain g where g: "g = The (?the f)" by blast
1.673 + obtain y where f: "f = Abs_finfun y" and y: "y \<in> finfun" by (cases f)
1.674 + from f y b have bfin: "finite {a. y a \<noteq> b}" by(simp add: finfun_default_def finite_finfun_default_aux)
1.675 +
1.676 + let ?g = "(\<lambda>a. Some (y a)) |` {a. y a \<noteq> b}"
1.677 + from bfin have fing: "finite (dom ?g)" by auto
1.678 + have bran: "b \<notin> ran ?g" by(auto simp add: ran_def restrict_map_def)
1.679 + have yg: "y = map_default b ?g" by simp
1.680 + have gg: "g = ?g" unfolding g
1.681 + proof(rule the_equality)
1.682 + from f y bfin show "?the f ?g"
1.683 + by(auto)(simp add: restrict_map_def ran_def split: split_if_asm)
1.684 + next
1.685 + fix g'
1.686 + assume "?the f g'"
1.687 + hence fin': "finite (dom g')" and ran': "b \<notin> ran g'"
1.688 + and eq: "Abs_finfun (map_default b ?g) = Abs_finfun (map_default b g')" using f yg by auto
1.689 + from fin' fing have "map_default b ?g \<in> finfun" "map_default b g' \<in> finfun" by(blast intro: map_default_in_finfun)+
1.690 + with eq have "map_default b ?g = map_default b g'" by simp
1.691 + with fing bran fin' ran' show "g' = ?g" by(rule map_default_inject[OF disjI2[OF refl], THEN sym])
1.692 + qed
1.693 +
1.694 + show ?thesis
1.695 + proof(cases "b' = b")
1.696 + case True
1.697 + note b'b = True
1.698 +
1.699 + let ?g' = "(\<lambda>a. Some ((y(a' := b)) a)) |` {a. (y(a' := b)) a \<noteq> b}"
1.700 + from bfin b'b have fing': "finite (dom ?g')"
1.701 + by(auto simp add: Collect_conj_eq Collect_imp_eq intro: finite_subset)
1.702 + have brang': "b \<notin> ran ?g'" by(auto simp add: ran_def restrict_map_def)
1.703 +
1.704 + let ?b' = "\<lambda>a. case ?g' a of None \<Rightarrow> b | Some b \<Rightarrow> b"
1.705 + let ?b = "map_default b ?g"
1.706 + from upd_left_comm upd_left_comm fing'
1.707 + have "fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g') = fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g')"
1.708 + by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b b map_default_def)
1.709 + also interpret gwf: fun_left_comm "\<lambda>a. upd a (?b a)" by(rule upd_left_comm)
1.710 + 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))"
1.711 + proof(cases "y a' = b")
1.712 + case True
1.713 + with b'b have g': "?g' = ?g" by(auto simp add: restrict_map_def intro: ext)
1.714 + from True have a'ndomg: "a' \<notin> dom ?g" by auto
1.715 + from f b'b b show ?thesis unfolding g'
1.716 + by(subst map_default_update_const[OF fing a'ndomg map_le_refl, symmetric]) simp
1.717 + next
1.718 + case False
1.719 + hence domg: "dom ?g = insert a' (dom ?g')" by auto
1.720 + from False b'b have a'ndomg': "a' \<notin> dom ?g'" by auto
1.721 + have "fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g')) =
1.722 + upd a' (?b a') (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'))"
1.723 + using fing' a'ndomg' unfolding b'b by(rule gwf.fold_insert)
1.724 + hence "upd a' b (fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g'))) =
1.725 + upd a' b (upd a' (?b a') (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g')))" by simp
1.726 + also from b'b have g'leg: "?g' \<subseteq>\<^sub>m ?g" by(auto simp add: restrict_map_def map_le_def)
1.727 + note map_default_update_twice[OF fing' a'ndomg' this, of b "?b a'" b]
1.728 + also note map_default_update_const[OF fing' a'ndomg' g'leg, of b]
1.729 + finally show ?thesis unfolding b'b domg[unfolded b'b] by(rule sym)
1.730 + qed
1.731 + also have "The (?the (f(\<^sup>f a' := b'))) = ?g'"
1.732 + proof(rule the_equality)
1.733 + from f y b b'b brang' fing' show "?the (f(\<^sup>f a' := b')) ?g'"
1.734 + by(auto simp del: fun_upd_apply simp add: finfun_update_def)
1.735 + next
1.736 + fix g'
1.737 + assume "?the (f(\<^sup>f a' := b')) g'"
1.738 + hence fin': "finite (dom g')" and ran': "b \<notin> ran g'"
1.739 + and eq: "f(\<^sup>f a' := b') = Abs_finfun (map_default b g')"
1.740 + by(auto simp del: fun_upd_apply)
1.741 + from fin' fing' have "map_default b g' \<in> finfun" "map_default b ?g' \<in> finfun"
1.742 + by(blast intro: map_default_in_finfun)+
1.743 + with eq f b'b b have "map_default b ?g' = map_default b g'"
1.744 + by(simp del: fun_upd_apply add: finfun_update_def)
1.745 + with fing' brang' fin' ran' show "g' = ?g'"
1.746 + by(rule map_default_inject[OF disjI2[OF refl], THEN sym])
1.747 + qed
1.748 + ultimately show ?thesis unfolding finfun_rec_def Let_def b gg[unfolded g b] using bfin b'b b
1.749 + by(simp only: finfun_default_update_const map_default_def)
1.750 + next
1.751 + case False
1.752 + note b'b = this
1.753 + let ?g' = "?g(a' \<mapsto> b')"
1.754 + let ?b' = "map_default b ?g'"
1.755 + let ?b = "map_default b ?g"
1.756 + from fing have fing': "finite (dom ?g')" by auto
1.757 + from bran b'b have bnrang': "b \<notin> ran ?g'" by(auto simp add: ran_def)
1.758 + have ffmg': "map_default b ?g' = y(a' := b')" by(auto intro: ext simp add: map_default_def restrict_map_def)
1.759 + 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.760 + have g': "The (?the (f(\<^sup>f a' := b'))) = ?g'"
1.761 + proof
1.762 + from fing' bnrang' f_Abs show "?the (f(\<^sup>f a' := b')) ?g'" by(auto simp add: finfun_update_def restrict_map_def)
1.763 + next
1.764 + fix g' assume "?the (f(\<^sup>f a' := b')) g'"
1.765 + hence f': "f(\<^sup>f a' := b') = Abs_finfun (map_default b g')"
1.766 + and fin': "finite (dom g')" and brang': "b \<notin> ran g'" by auto
1.767 + from fing' fin' have "map_default b ?g' \<in> finfun" "map_default b g' \<in> finfun"
1.768 + by(auto intro: map_default_in_finfun)
1.769 + with f' f_Abs have "map_default b g' = map_default b ?g'" by simp
1.770 + with fin' brang' fing' bnrang' show "g' = ?g'"
1.771 + by(rule map_default_inject[OF disjI2[OF refl]])
1.772 + qed
1.773 + 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.774 + by auto
1.775 + show ?thesis
1.776 + proof(cases "y a' = b")
1.777 + case True
1.778 + hence a'ndomg: "a' \<notin> dom ?g" by auto
1.779 + from f y b'b True have yff: "y = map_default b (?g' |` dom ?g)"
1.780 + by(auto simp add: restrict_map_def map_default_def intro!: ext)
1.781 + hence f': "f = Abs_finfun (map_default b (?g' |` dom ?g))" using f by simp
1.782 + interpret g'wf: fun_left_comm "\<lambda>a. upd a (?b' a)" by(rule upd_left_comm)
1.783 + from upd_left_comm upd_left_comm fing
1.784 + have "fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g) = fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g)"
1.785 + by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b True map_default_def)
1.786 + thus ?thesis unfolding finfun_rec_def Let_def finfun_default_update_const b[symmetric]
1.787 + unfolding g' g[symmetric] gg g'wf.fold_insert[OF fing a'ndomg, of "cnst b", folded dom]
1.788 + by -(rule arg_cong2[where f="upd a'"], simp_all add: map_default_def)
1.789 + next
1.790 + case False
1.791 + hence "insert a' (dom ?g) = dom ?g" by auto
1.792 + moreover {
1.793 + let ?g'' = "?g(a' := None)"
1.794 + let ?b'' = "map_default b ?g''"
1.795 + from False have domg: "dom ?g = insert a' (dom ?g'')" by auto
1.796 + from False have a'ndomg'': "a' \<notin> dom ?g''" by auto
1.797 + have fing'': "finite (dom ?g'')" by(rule finite_subset[OF _ fing]) auto
1.798 + have bnrang'': "b \<notin> ran ?g''" by(auto simp add: ran_def restrict_map_def)
1.799 + interpret gwf: fun_left_comm "\<lambda>a. upd a (?b a)" by(rule upd_left_comm)
1.800 + interpret g'wf: fun_left_comm "\<lambda>a. upd a (?b' a)" by(rule upd_left_comm)
1.801 + have "upd a' b' (fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g''))) =
1.802 + upd a' b' (upd a' (?b a') (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')))"
1.803 + unfolding gwf.fold_insert[OF fing'' a'ndomg''] f ..
1.804 + also have g''leg: "?g |` dom ?g'' \<subseteq>\<^sub>m ?g" by(auto simp add: map_le_def)
1.805 + have "dom (?g |` dom ?g'') = dom ?g''" by auto
1.806 + 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.807 + unfolded this, OF fing'' a'ndomg'' g''leg]
1.808 + also have b': "b' = ?b' a'" by(auto simp add: map_default_def)
1.809 + from upd_left_comm upd_left_comm fing''
1.810 + have "fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'') = fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g'')"
1.811 + by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b map_default_def)
1.812 + with b' have "upd a' b' (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')) =
1.813 + upd a' (?b' a') (fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g''))" by simp
1.814 + also note g'wf.fold_insert[OF fing'' a'ndomg'', symmetric]
1.815 + finally have "upd a' b' (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g)) =
1.816 + fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g)"
1.817 + unfolding domg . }
1.818 + ultimately have "fold (\<lambda>a. upd a (?b' a)) (cnst b) (insert a' (dom ?g)) =
1.819 + upd a' b' (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g))" by simp
1.820 + thus ?thesis unfolding finfun_rec_def Let_def finfun_default_update_const b[symmetric] g[symmetric] g' dom[symmetric]
1.821 + using b'b gg by(simp add: map_default_insert)
1.822 + qed
1.823 + qed
1.824 +qed
1.825 +
1.826 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1.827 +
1.828 +end
1.829 +
1.830 +locale finfun_rec_wf = finfun_rec_wf_aux +
1.831 + assumes const_update_all:
1.832 + "finite (UNIV :: 'a set) \<Longrightarrow> fold (\<lambda>a. upd a b') (cnst b) (UNIV :: 'a set) = cnst b'"
1.833 +begin
1.834 +
1.835 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1.836 +
1.837 +lemma finfun_rec_const [simp]:
1.838 + "finfun_rec cnst upd (\<lambda>\<^isup>f c) = cnst c"
1.839 +proof(cases "finite (UNIV :: 'a set)")
1.840 + case False
1.841 + hence "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = c" by(simp add: finfun_default_const)
1.842 + 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.843 + proof
1.844 + show "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c empty) \<and> finite (dom empty) \<and> c \<notin> ran empty"
1.845 + by(auto simp add: finfun_const_def)
1.846 + next
1.847 + fix g :: "'a \<rightharpoonup> 'b"
1.848 + assume "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g"
1.849 + 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.850 + from g map_default_in_finfun[OF fin, of c] have "map_default c g = (\<lambda>a. c)"
1.851 + by(simp add: finfun_const_def)
1.852 + moreover have "map_default c empty = (\<lambda>a. c)" by simp
1.853 + ultimately show "g = empty" by-(rule map_default_inject[OF disjI2[OF refl] fin ran], auto)
1.854 + qed
1.855 + ultimately show ?thesis by(simp add: finfun_rec_def)
1.856 +next
1.857 + case True
1.858 + hence default: "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = arbitrary" by(simp add: finfun_default_const)
1.859 + 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"
1.860 + show ?thesis
1.861 + proof(cases "c = arbitrary")
1.862 + case True
1.863 + have the: "The ?the = empty"
1.864 + proof
1.865 + from True show "?the empty" by(auto simp add: finfun_const_def)
1.866 + next
1.867 + fix g'
1.868 + assume "?the g'"
1.869 + hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default arbitrary g')"
1.870 + and fin: "finite (dom g')" and g: "arbitrary \<notin> ran g'" by simp_all
1.871 + from fin have "map_default arbitrary g' \<in> finfun" by(rule map_default_in_finfun)
1.872 + with fg have "map_default arbitrary g' = (\<lambda>a. c)"
1.873 + by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1])
1.874 + with True show "g' = empty"
1.875 + by -(rule map_default_inject(2)[OF _ fin g], auto)
1.876 + qed
1.877 + show ?thesis unfolding finfun_rec_def using `finite UNIV` True
1.878 + unfolding Let_def the default by(simp)
1.879 + next
1.880 + case False
1.881 + have the: "The ?the = (\<lambda>a :: 'a. Some c)"
1.882 + proof
1.883 + from False True show "?the (\<lambda>a :: 'a. Some c)"
1.884 + by(auto simp add: map_default_def_raw finfun_const_def dom_def ran_def)
1.885 + next
1.886 + fix g' :: "'a \<rightharpoonup> 'b"
1.887 + assume "?the g'"
1.888 + hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default arbitrary g')"
1.889 + and fin: "finite (dom g')" and g: "arbitrary \<notin> ran g'" by simp_all
1.890 + from fin have "map_default arbitrary g' \<in> finfun" by(rule map_default_in_finfun)
1.891 + with fg have "map_default arbitrary g' = (\<lambda>a. c)"
1.892 + by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1])
1.893 + with True False show "g' = (\<lambda>a::'a. Some c)"
1.894 + by -(rule map_default_inject(2)[OF _ fin g], auto simp add: dom_def ran_def map_default_def_raw)
1.895 + qed
1.896 + show ?thesis unfolding finfun_rec_def using True False
1.897 + unfolding Let_def the default by(simp add: dom_def map_default_def const_update_all)
1.898 + qed
1.899 +qed
1.900 +
1.901 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1.902 +
1.903 +end
1.904 +
1.905 +subsection {* Weak induction rule and case analysis for FinFuns *}
1.906 +
1.907 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1.908 +
1.909 +lemma finfun_weak_induct [consumes 0, case_names const update]:
1.910 + assumes const: "\<And>b. P (\<lambda>\<^isup>f b)"
1.911 + and update: "\<And>f a b. P f \<Longrightarrow> P (f(\<^sup>f a := b))"
1.912 + shows "P x"
1.913 +proof(induct x rule: Abs_finfun_induct)
1.914 + case (Abs_finfun y)
1.915 + then obtain b where "finite {a. y a \<noteq> b}" unfolding finfun_def by blast
1.916 + thus ?case using `y \<in> finfun`
1.917 + proof(induct x\<equiv>"{a. y a \<noteq> b}" arbitrary: y rule: finite_induct)
1.918 + case empty
1.919 + hence "\<And>a. y a = b" by blast
1.920 + hence "y = (\<lambda>a. b)" by(auto intro: ext)
1.921 + hence "Abs_finfun y = finfun_const b" unfolding finfun_const_def by simp
1.922 + thus ?case by(simp add: const)
1.923 + next
1.924 + case (insert a A)
1.925 + note IH = `\<And>y. \<lbrakk> y \<in> finfun; A = {a. y a \<noteq> b} \<rbrakk> \<Longrightarrow> P (Abs_finfun y)`
1.926 + note y = `y \<in> finfun`
1.927 + with `insert a A = {a. y a \<noteq> b}` `a \<notin> A`
1.928 + have "y(a := b) \<in> finfun" "A = {a'. (y(a := b)) a' \<noteq> b}" by auto
1.929 + from IH[OF this] have "P (finfun_update (Abs_finfun (y(a := b))) a (y a))" by(rule update)
1.930 + thus ?case using y unfolding finfun_update_def by simp
1.931 + qed
1.932 +qed
1.933 +
1.934 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1.935 +
1.936 +lemma finfun_exhaust_disj: "(\<exists>b. x = finfun_const b) \<or> (\<exists>f a b. x = finfun_update f a b)"
1.937 +by(induct x rule: finfun_weak_induct) blast+
1.938 +
1.939 +lemma finfun_exhaust:
1.940 + obtains b where "x = (\<lambda>\<^isup>f b)"
1.941 + | f a b where "x = f(\<^sup>f a := b)"
1.942 +by(atomize_elim)(rule finfun_exhaust_disj)
1.943 +
1.944 +lemma finfun_rec_unique:
1.945 + fixes f :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'c"
1.946 + assumes c: "\<And>c. f (\<lambda>\<^isup>f c) = cnst c"
1.947 + and u: "\<And>g a b. f (g(\<^sup>f a := b)) = upd g a b (f g)"
1.948 + and c': "\<And>c. f' (\<lambda>\<^isup>f c) = cnst c"
1.949 + and u': "\<And>g a b. f' (g(\<^sup>f a := b)) = upd g a b (f' g)"
1.950 + shows "f = f'"
1.951 +proof
1.952 + fix g :: "'a \<Rightarrow>\<^isub>f 'b"
1.953 + show "f g = f' g"
1.954 + by(induct g rule: finfun_weak_induct)(auto simp add: c u c' u')
1.955 +qed
1.956 +
1.957 +
1.958 +subsection {* Function application *}
1.959 +
1.960 +definition finfun_apply :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b" ("_\<^sub>f" [1000] 1000)
1.961 +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.962 +
1.963 +interpretation finfun_apply_aux: finfun_rec_wf_aux "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c"
1.964 +by(unfold_locales) auto
1.965 +
1.966 +interpretation finfun_apply: finfun_rec_wf "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c"
1.967 +proof(unfold_locales)
1.968 + fix b' b :: 'a
1.969 + assume fin: "finite (UNIV :: 'b set)"
1.970 + { fix A :: "'b set"
1.971 + interpret fun_left_comm "\<lambda>a'. If (a = a') b'" by(rule finfun_apply_aux.upd_left_comm)
1.972 + from fin have "finite A" by(auto intro: finite_subset)
1.973 + hence "fold (\<lambda>a'. If (a = a') b') b A = (if a \<in> A then b' else b)"
1.974 + by induct auto }
1.975 + from this[of UNIV] show "fold (\<lambda>a'. If (a = a') b') b UNIV = b'" by simp
1.976 +qed
1.977 +
1.978 +lemma finfun_const_apply [simp, code]: "(\<lambda>\<^isup>f b)\<^sub>f a = b"
1.979 +by(simp add: finfun_apply_def)
1.980 +
1.981 +lemma finfun_upd_apply: "f(\<^sup>fa := b)\<^sub>f a' = (if a = a' then b else f\<^sub>f a')"
1.982 + 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.983 +by(simp_all add: finfun_apply_def)
1.984 +
1.985 +lemma finfun_upd_apply_same [simp]:
1.986 + "f(\<^sup>fa := b)\<^sub>f a = b"
1.987 +by(simp add: finfun_upd_apply)
1.988 +
1.989 +lemma finfun_upd_apply_other [simp]:
1.990 + "a \<noteq> a' \<Longrightarrow> f(\<^sup>fa := b)\<^sub>f a' = f\<^sub>f a'"
1.991 +by(simp add: finfun_upd_apply)
1.992 +
1.993 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1.994 +
1.995 +lemma finfun_apply_Rep_finfun:
1.996 + "finfun_apply = Rep_finfun"
1.997 +proof(rule finfun_rec_unique)
1.998 + fix c show "Rep_finfun (\<lambda>\<^isup>f c) = (\<lambda>a. c)" by(auto simp add: finfun_const_def)
1.999 +next
1.1000 + 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.1001 + by(auto simp add: finfun_update_def fun_upd_finfun Abs_finfun_inverse Rep_finfun intro: ext)
1.1002 +qed(auto intro: ext)
1.1003 +
1.1004 +lemma finfun_ext: "(\<And>a. f\<^sub>f a = g\<^sub>f a) \<Longrightarrow> f = g"
1.1005 +by(auto simp add: finfun_apply_Rep_finfun Rep_finfun_inject[symmetric] simp del: Rep_finfun_inject intro: ext)
1.1006 +
1.1007 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1.1008 +
1.1009 +lemma expand_finfun_eq: "(f = g) = (f\<^sub>f = g\<^sub>f)"
1.1010 +by(auto intro: finfun_ext)
1.1011 +
1.1012 +lemma finfun_const_inject [simp]: "(\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b') \<equiv> b = b'"
1.1013 +by(simp add: expand_finfun_eq expand_fun_eq)
1.1014 +
1.1015 +lemma finfun_const_eq_update:
1.1016 + "((\<lambda>\<^isup>f b) = f(\<^sup>f a := b')) = (b = b' \<and> (\<forall>a'. a \<noteq> a' \<longrightarrow> f\<^sub>f a' = b))"
1.1017 +by(auto simp add: expand_finfun_eq expand_fun_eq finfun_upd_apply)
1.1018 +
1.1019 +subsection {* Function composition *}
1.1020 +
1.1021 +definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>\<^isub>f 'a \<Rightarrow> 'c \<Rightarrow>\<^isub>f 'b" (infixr "\<circ>\<^isub>f" 55)
1.1022 +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.1023 +
1.1024 +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.1025 +by(unfold_locales)(auto simp add: finfun_upd_apply intro: finfun_ext)
1.1026 +
1.1027 +interpretation finfun_comp: finfun_rec_wf "(\<lambda>b. (\<lambda>\<^isup>f g b))" "(\<lambda>a b c. c(\<^sup>f a := g b))"
1.1028 +proof
1.1029 + fix b' b :: 'a
1.1030 + assume fin: "finite (UNIV :: 'c set)"
1.1031 + { fix A :: "'c set"
1.1032 + from fin have "finite A" by(auto intro: finite_subset)
1.1033 + hence "fold (\<lambda>(a :: 'c) c. c(\<^sup>f a := g b')) (\<lambda>\<^isup>f g b) A =
1.1034 + Abs_finfun (\<lambda>a. if a \<in> A then g b' else g b)"
1.1035 + 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) }
1.1036 + 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')"
1.1037 + by(simp add: finfun_const_def)
1.1038 +qed
1.1039 +
1.1040 +lemma finfun_comp_const [simp, code]:
1.1041 + "g \<circ>\<^isub>f (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f g c)"
1.1042 +by(simp add: finfun_comp_def)
1.1043 +
1.1044 +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.1045 + 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.1046 +by(simp_all add: finfun_comp_def)
1.1047 +
1.1048 +lemma finfun_comp_apply [simp]:
1.1049 + "(g \<circ>\<^isub>f f)\<^sub>f = g \<circ> f\<^sub>f"
1.1050 +by(induct f rule: finfun_weak_induct)(auto simp add: finfun_upd_apply intro: ext)
1.1051 +
1.1052 +lemma finfun_comp_comp_collapse [simp]: "f \<circ>\<^isub>f g \<circ>\<^isub>f h = (f o g) \<circ>\<^isub>f h"
1.1053 +by(induct h rule: finfun_weak_induct) simp_all
1.1054 +
1.1055 +lemma finfun_comp_const1 [simp]: "(\<lambda>x. c) \<circ>\<^isub>f f = (\<lambda>\<^isup>f c)"
1.1056 +by(induct f rule: finfun_weak_induct)(auto intro: finfun_ext simp add: finfun_upd_apply)
1.1057 +
1.1058 +lemma finfun_comp_id1 [simp]: "(\<lambda>x. x) \<circ>\<^isub>f f = f" "id \<circ>\<^isub>f f = f"
1.1059 +by(induct f rule: finfun_weak_induct) auto
1.1060 +
1.1061 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1.1062 +
1.1063 +lemma finfun_comp_conv_comp: "g \<circ>\<^isub>f f = Abs_finfun (g \<circ> finfun_apply f)"
1.1064 +proof -
1.1065 + have "(\<lambda>f. g \<circ>\<^isub>f f) = (\<lambda>f. Abs_finfun (g \<circ> finfun_apply f))"
1.1066 + proof(rule finfun_rec_unique)
1.1067 + { fix c show "Abs_finfun (g \<circ> (\<lambda>\<^isup>f c)\<^sub>f) = (\<lambda>\<^isup>f g c)"
1.1068 + by(simp add: finfun_comp_def o_def)(simp add: finfun_const_def) }
1.1069 + { 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.1070 + proof -
1.1071 + obtain y where y: "y \<in> finfun" and g': "g' = Abs_finfun y" by(cases g')
1.1072 + moreover hence "(g \<circ> g'\<^sub>f) \<in> finfun" by(simp add: finfun_apply_Rep_finfun finfun_left_compose)
1.1073 + moreover have "g \<circ> y(a := b) = (g \<circ> y)(a := g b)" by(auto intro: ext)
1.1074 + ultimately show ?thesis by(simp add: finfun_comp_def finfun_update_def finfun_apply_Rep_finfun)
1.1075 + qed }
1.1076 + qed auto
1.1077 + thus ?thesis by(auto simp add: expand_fun_eq)
1.1078 +qed
1.1079 +
1.1080 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1.1081 +
1.1082 +
1.1083 +
1.1084 +definition finfun_comp2 :: "'b \<Rightarrow>\<^isub>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c" (infixr "\<^sub>f\<circ>" 55)
1.1085 +where [code del]: "finfun_comp2 g f = Abs_finfun (Rep_finfun g \<circ> f)"
1.1086 +
1.1087 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1.1088 +
1.1089 +lemma finfun_comp2_const [code, simp]: "finfun_comp2 (\<lambda>\<^isup>f c) f = (\<lambda>\<^isup>f c)"
1.1090 +by(simp add: finfun_comp2_def finfun_const_def comp_def)
1.1091 +
1.1092 +lemma finfun_comp2_update:
1.1093 + assumes inj: "inj f"
1.1094 + 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.1095 +proof(cases "b \<in> range f")
1.1096 + case True
1.1097 + 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.1098 + with inj True show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def finfun_right_compose)
1.1099 +next
1.1100 + case False
1.1101 + hence "(Rep_finfun g)(b := c) \<circ> f = Rep_finfun g \<circ> f" by(auto simp add: expand_fun_eq)
1.1102 + with False show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def)
1.1103 +qed
1.1104 +
1.1105 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1.1106 +
1.1107 +subsection {* A type class for computing the cardinality of a type's universe *}
1.1108 +
1.1109 +class card_UNIV =
1.1110 + fixes card_UNIV :: "'a itself \<Rightarrow> nat"
1.1111 + assumes card_UNIV: "card_UNIV x = card (UNIV :: 'a set)"
1.1112 +begin
1.1113 +
1.1114 +lemma card_UNIV_neq_0_finite_UNIV:
1.1115 + "card_UNIV x \<noteq> 0 \<longleftrightarrow> finite (UNIV :: 'a set)"
1.1116 +by(simp add: card_UNIV card_eq_0_iff)
1.1117 +
1.1118 +lemma card_UNIV_ge_0_finite_UNIV:
1.1119 + "card_UNIV x > 0 \<longleftrightarrow> finite (UNIV :: 'a set)"
1.1120 +by(auto simp add: card_UNIV intro: card_ge_0_finite finite_UNIV_card_ge_0)
1.1121 +
1.1122 +lemma card_UNIV_eq_0_infinite_UNIV:
1.1123 + "card_UNIV x = 0 \<longleftrightarrow> infinite (UNIV :: 'a set)"
1.1124 +by(simp add: card_UNIV card_eq_0_iff)
1.1125 +
1.1126 +definition is_list_UNIV :: "'a list \<Rightarrow> bool"
1.1127 +where "is_list_UNIV xs = (let c = card_UNIV (TYPE('a)) in if c = 0 then False else size (remdups xs) = c)"
1.1128 +
1.1129 +lemma is_list_UNIV_iff:
1.1130 + fixes xs :: "'a list"
1.1131 + shows "is_list_UNIV xs \<longleftrightarrow> set xs = UNIV"
1.1132 +proof
1.1133 + assume "is_list_UNIV xs"
1.1134 + hence c: "card_UNIV (TYPE('a)) > 0" and xs: "size (remdups xs) = card_UNIV (TYPE('a))"
1.1135 + unfolding is_list_UNIV_def by(simp_all add: Let_def split: split_if_asm)
1.1136 + from c have fin: "finite (UNIV :: 'a set)" by(auto simp add: card_UNIV_ge_0_finite_UNIV)
1.1137 + have "card (set (remdups xs)) = size (remdups xs)" by(subst distinct_card) auto
1.1138 + also note set_remdups
1.1139 + finally show "set xs = UNIV" using fin unfolding xs card_UNIV by-(rule card_eq_UNIV_imp_eq_UNIV)
1.1140 +next
1.1141 + assume xs: "set xs = UNIV"
1.1142 + from finite_set[of xs] have fin: "finite (UNIV :: 'a set)" unfolding xs .
1.1143 + hence "card_UNIV (TYPE ('a)) \<noteq> 0" unfolding card_UNIV_neq_0_finite_UNIV .
1.1144 + moreover have "size (remdups xs) = card (set (remdups xs))"
1.1145 + by(subst distinct_card) auto
1.1146 + ultimately show "is_list_UNIV xs" using xs by(simp add: is_list_UNIV_def Let_def card_UNIV)
1.1147 +qed
1.1148 +
1.1149 +lemma card_UNIV_eq_0_is_list_UNIV_False:
1.1150 + assumes cU0: "card_UNIV x = 0"
1.1151 + shows "is_list_UNIV = (\<lambda>xs. False)"
1.1152 +proof(rule ext)
1.1153 + fix xs :: "'a list"
1.1154 + from cU0 have "infinite (UNIV :: 'a set)"
1.1155 + by(auto simp only: card_UNIV_eq_0_infinite_UNIV)
1.1156 + moreover have "finite (set xs)" by(rule finite_set)
1.1157 + ultimately have "(UNIV :: 'a set) \<noteq> set xs" by(auto simp del: finite_set)
1.1158 + thus "is_list_UNIV xs = False" unfolding is_list_UNIV_iff by simp
1.1159 +qed
1.1160 +
1.1161 +end
1.1162 +
1.1163 +subsection {* Instantiations for @{text "card_UNIV"} *}
1.1164 +
1.1165 +subsubsection {* @{typ "nat"} *}
1.1166 +
1.1167 +instantiation nat :: card_UNIV begin
1.1168 +
1.1169 +definition card_UNIV_nat_def:
1.1170 + "card_UNIV_class.card_UNIV = (\<lambda>a :: nat itself. 0)"
1.1171 +
1.1172 +instance proof
1.1173 + fix x :: "nat itself"
1.1174 + show "card_UNIV x = card (UNIV :: nat set)"
1.1175 + unfolding card_UNIV_nat_def by simp
1.1176 +qed
1.1177 +
1.1178 +end
1.1179 +
1.1180 +subsubsection {* @{typ "int"} *}
1.1181 +
1.1182 +instantiation int :: card_UNIV begin
1.1183 +
1.1184 +definition card_UNIV_int_def:
1.1185 + "card_UNIV_class.card_UNIV = (\<lambda>a :: int itself. 0)"
1.1186 +
1.1187 +instance proof
1.1188 + fix x :: "int itself"
1.1189 + show "card_UNIV x = card (UNIV :: int set)"
1.1190 + unfolding card_UNIV_int_def by simp
1.1191 +qed
1.1192 +
1.1193 +end
1.1194 +
1.1195 +subsubsection {* @{typ "'a list"} *}
1.1196 +
1.1197 +instantiation list :: (type) card_UNIV begin
1.1198 +
1.1199 +definition card_UNIV_list_def:
1.1200 + "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a list itself. 0)"
1.1201 +
1.1202 +instance proof
1.1203 + fix x :: "'a list itself"
1.1204 + show "card_UNIV x = card (UNIV :: 'a list set)"
1.1205 + unfolding card_UNIV_list_def by(simp add: infinite_UNIV_listI)
1.1206 +qed
1.1207 +
1.1208 +end
1.1209 +
1.1210 +subsubsection {* @{typ "unit"} *}
1.1211 +
1.1212 +lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
1.1213 + unfolding UNIV_unit by simp
1.1214 +
1.1215 +instantiation unit :: card_UNIV begin
1.1216 +
1.1217 +definition card_UNIV_unit_def:
1.1218 + "card_UNIV_class.card_UNIV = (\<lambda>a :: unit itself. 1)"
1.1219 +
1.1220 +instance proof
1.1221 + fix x :: "unit itself"
1.1222 + show "card_UNIV x = card (UNIV :: unit set)"
1.1223 + by(simp add: card_UNIV_unit_def card_UNIV_unit)
1.1224 +qed
1.1225 +
1.1226 +end
1.1227 +
1.1228 +subsubsection {* @{typ "bool"} *}
1.1229 +
1.1230 +lemma card_UNIV_bool: "card (UNIV :: bool set) = 2"
1.1231 + unfolding UNIV_bool by simp
1.1232 +
1.1233 +instantiation bool :: card_UNIV begin
1.1234 +
1.1235 +definition card_UNIV_bool_def:
1.1236 + "card_UNIV_class.card_UNIV = (\<lambda>a :: bool itself. 2)"
1.1237 +
1.1238 +instance proof
1.1239 + fix x :: "bool itself"
1.1240 + show "card_UNIV x = card (UNIV :: bool set)"
1.1241 + by(simp add: card_UNIV_bool_def card_UNIV_bool)
1.1242 +qed
1.1243 +
1.1244 +end
1.1245 +
1.1246 +subsubsection {* @{typ "char"} *}
1.1247 +
1.1248 +lemma card_UNIV_char: "card (UNIV :: char set) = 256"
1.1249 +proof -
1.1250 + from enum_distinct
1.1251 + have "card (set (enum :: char list)) = length (enum :: char list)"
1.1252 + by -(rule distinct_card)
1.1253 + also have "set enum = (UNIV :: char set)" by auto
1.1254 + also note enum_char
1.1255 + finally show ?thesis by simp
1.1256 +qed
1.1257 +
1.1258 +instantiation char :: card_UNIV begin
1.1259 +
1.1260 +definition card_UNIV_char_def:
1.1261 + "card_UNIV_class.card_UNIV = (\<lambda>a :: char itself. 256)"
1.1262 +
1.1263 +instance proof
1.1264 + fix x :: "char itself"
1.1265 + show "card_UNIV x = card (UNIV :: char set)"
1.1266 + by(simp add: card_UNIV_char_def card_UNIV_char)
1.1267 +qed
1.1268 +
1.1269 +end
1.1270 +
1.1271 +subsubsection {* @{typ "'a \<times> 'b"} *}
1.1272 +
1.1273 +instantiation * :: (card_UNIV, card_UNIV) card_UNIV begin
1.1274 +
1.1275 +definition card_UNIV_product_def:
1.1276 + "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<times> 'b) itself. card_UNIV (TYPE('a)) * card_UNIV (TYPE('b)))"
1.1277 +
1.1278 +instance proof
1.1279 + fix x :: "('a \<times> 'b) itself"
1.1280 + show "card_UNIV x = card (UNIV :: ('a \<times> 'b) set)"
1.1281 + by(simp add: card_UNIV_product_def card_UNIV UNIV_Times_UNIV[symmetric] card_cartesian_product del: UNIV_Times_UNIV)
1.1282 +qed
1.1283 +
1.1284 +end
1.1285 +
1.1286 +subsubsection {* @{typ "'a + 'b"} *}
1.1287 +
1.1288 +instantiation "+" :: (card_UNIV, card_UNIV) card_UNIV begin
1.1289 +
1.1290 +definition card_UNIV_sum_def:
1.1291 + "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a + 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
1.1292 + in if ca \<noteq> 0 \<and> cb \<noteq> 0 then ca + cb else 0)"
1.1293 +
1.1294 +instance proof
1.1295 + fix x :: "('a + 'b) itself"
1.1296 + show "card_UNIV x = card (UNIV :: ('a + 'b) set)"
1.1297 + 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)
1.1298 +qed
1.1299 +
1.1300 +end
1.1301 +
1.1302 +subsubsection {* @{typ "'a \<Rightarrow> 'b"} *}
1.1303 +
1.1304 +instantiation "fun" :: (card_UNIV, card_UNIV) card_UNIV begin
1.1305 +
1.1306 +definition card_UNIV_fun_def:
1.1307 + "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<Rightarrow> 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
1.1308 + in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)"
1.1309 +
1.1310 +instance proof
1.1311 + fix x :: "('a \<Rightarrow> 'b) itself"
1.1312 +
1.1313 + { assume "0 < card (UNIV :: 'a set)"
1.1314 + and "0 < card (UNIV :: 'b set)"
1.1315 + hence fina: "finite (UNIV :: 'a set)" and finb: "finite (UNIV :: 'b set)"
1.1316 + by(simp_all only: card_ge_0_finite)
1.1317 + from finite_distinct_list[OF finb] obtain bs
1.1318 + where bs: "set bs = (UNIV :: 'b set)" and distb: "distinct bs" by blast
1.1319 + from finite_distinct_list[OF fina] obtain as
1.1320 + where as: "set as = (UNIV :: 'a set)" and dista: "distinct as" by blast
1.1321 + have cb: "card (UNIV :: 'b set) = length bs"
1.1322 + unfolding bs[symmetric] distinct_card[OF distb] ..
1.1323 + have ca: "card (UNIV :: 'a set) = length as"
1.1324 + unfolding as[symmetric] distinct_card[OF dista] ..
1.1325 + let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (n_lists (length as) bs)"
1.1326 + have "UNIV = set ?xs"
1.1327 + proof(rule UNIV_eq_I)
1.1328 + fix f :: "'a \<Rightarrow> 'b"
1.1329 + from as have "f = the \<circ> map_of (zip as (map f as))"
1.1330 + by(auto simp add: map_of_zip_map intro: ext)
1.1331 + thus "f \<in> set ?xs" using bs by(auto simp add: set_n_lists)
1.1332 + qed
1.1333 + moreover have "distinct ?xs" unfolding distinct_map
1.1334 + proof(intro conjI distinct_n_lists distb inj_onI)
1.1335 + fix xs ys :: "'b list"
1.1336 + assume xs: "xs \<in> set (n_lists (length as) bs)"
1.1337 + and ys: "ys \<in> set (n_lists (length as) bs)"
1.1338 + and eq: "the \<circ> map_of (zip as xs) = the \<circ> map_of (zip as ys)"
1.1339 + from xs ys have [simp]: "length xs = length as" "length ys = length as"
1.1340 + by(simp_all add: length_n_lists_elem)
1.1341 + have "map_of (zip as xs) = map_of (zip as ys)"
1.1342 + proof
1.1343 + fix x
1.1344 + from as bs have "\<exists>y. map_of (zip as xs) x = Some y" "\<exists>y. map_of (zip as ys) x = Some y"
1.1345 + by(simp_all add: map_of_zip_is_Some[symmetric])
1.1346 + with eq show "map_of (zip as xs) x = map_of (zip as ys) x"
1.1347 + by(auto dest: fun_cong[where x=x])
1.1348 + qed
1.1349 + with dista show "xs = ys" by(simp add: map_of_zip_inject)
1.1350 + qed
1.1351 + hence "card (set ?xs) = length ?xs" by(simp only: distinct_card)
1.1352 + moreover have "length ?xs = length bs ^ length as" by(simp add: length_n_lists)
1.1353 + ultimately have "card (UNIV :: ('a \<Rightarrow> 'b) set) = card (UNIV :: 'b set) ^ card (UNIV :: 'a set)"
1.1354 + using cb ca by simp }
1.1355 + moreover {
1.1356 + assume cb: "card (UNIV :: 'b set) = Suc 0"
1.1357 + then obtain b where b: "UNIV = {b :: 'b}" by(auto simp add: card_Suc_eq)
1.1358 + have eq: "UNIV = {\<lambda>x :: 'a. b ::'b}"
1.1359 + proof(rule UNIV_eq_I)
1.1360 + fix x :: "'a \<Rightarrow> 'b"
1.1361 + { fix y
1.1362 + have "x y \<in> UNIV" ..
1.1363 + hence "x y = b" unfolding b by simp }
1.1364 + thus "x \<in> {\<lambda>x. b}" by(auto intro: ext)
1.1365 + qed
1.1366 + have "card (UNIV :: ('a \<Rightarrow> 'b) set) = Suc 0" unfolding eq by simp }
1.1367 + ultimately show "card_UNIV x = card (UNIV :: ('a \<Rightarrow> 'b) set)"
1.1368 + unfolding card_UNIV_fun_def card_UNIV Let_def
1.1369 + by(auto simp del: One_nat_def)(auto simp add: card_eq_0_iff dest: finite_fun_UNIVD2 finite_fun_UNIVD1)
1.1370 +qed
1.1371 +
1.1372 +end
1.1373 +
1.1374 +subsubsection {* @{typ "'a option"} *}
1.1375 +
1.1376 +instantiation option :: (card_UNIV) card_UNIV
1.1377 +begin
1.1378 +
1.1379 +definition card_UNIV_option_def:
1.1380 + "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a option itself. let c = card_UNIV (TYPE('a))
1.1381 + in if c \<noteq> 0 then Suc c else 0)"
1.1382 +
1.1383 +instance proof
1.1384 + fix x :: "'a option itself"
1.1385 + show "card_UNIV x = card (UNIV :: 'a option set)"
1.1386 + unfolding UNIV_option_conv
1.1387 + by(auto simp add: card_UNIV_option_def card_UNIV card_eq_0_iff Let_def intro: inj_Some dest: finite_imageD)
1.1388 + (subst card_insert_disjoint, auto simp add: card_eq_0_iff card_image inj_Some intro: finite_imageI card_ge_0_finite)
1.1389 +qed
1.1390 +
1.1391 +end
1.1392 +
1.1393 +
1.1394 +subsection {* Universal quantification *}
1.1395 +
1.1396 +definition finfun_All_except :: "'a list \<Rightarrow> 'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
1.1397 +where [code del]: "finfun_All_except A P \<equiv> \<forall>a. a \<in> set A \<or> P\<^sub>f a"
1.1398 +
1.1399 +lemma finfun_All_except_const: "finfun_All_except A (\<lambda>\<^isup>f b) \<longleftrightarrow> b \<or> set A = UNIV"
1.1400 +by(auto simp add: finfun_All_except_def)
1.1401 +
1.1402 +lemma finfun_All_except_const_finfun_UNIV_code [code]:
1.1403 + "finfun_All_except A (\<lambda>\<^isup>f b) = (b \<or> is_list_UNIV A)"
1.1404 +by(simp add: finfun_All_except_const is_list_UNIV_iff)
1.1405 +
1.1406 +lemma finfun_All_except_update:
1.1407 + "finfun_All_except A f(\<^sup>f a := b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
1.1408 +by(fastsimp simp add: finfun_All_except_def finfun_upd_apply)
1.1409 +
1.1410 +lemma finfun_All_except_update_code [code]:
1.1411 + fixes a :: "'a :: card_UNIV"
1.1412 + 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.1413 +by(simp add: finfun_All_except_update)
1.1414 +
1.1415 +definition finfun_All :: "'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
1.1416 +where "finfun_All = finfun_All_except []"
1.1417 +
1.1418 +lemma finfun_All_const [simp]: "finfun_All (\<lambda>\<^isup>f b) = b"
1.1419 +by(simp add: finfun_All_def finfun_All_except_def)
1.1420 +
1.1421 +lemma finfun_All_update: "finfun_All f(\<^sup>f a := b) = (b \<and> finfun_All_except [a] f)"
1.1422 +by(simp add: finfun_All_def finfun_All_except_update)
1.1423 +
1.1424 +lemma finfun_All_All: "finfun_All P = All P\<^sub>f"
1.1425 +by(simp add: finfun_All_def finfun_All_except_def)
1.1426 +
1.1427 +
1.1428 +definition finfun_Ex :: "'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
1.1429 +where "finfun_Ex P = Not (finfun_All (Not \<circ>\<^isub>f P))"
1.1430 +
1.1431 +lemma finfun_Ex_Ex: "finfun_Ex P = Ex P\<^sub>f"
1.1432 +unfolding finfun_Ex_def finfun_All_All by simp
1.1433 +
1.1434 +lemma finfun_Ex_const [simp]: "finfun_Ex (\<lambda>\<^isup>f b) = b"
1.1435 +by(simp add: finfun_Ex_def)
1.1436 +
1.1437 +
1.1438 +subsection {* A diagonal operator for FinFuns *}
1.1439 +
1.1440 +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.1441 +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.1442 +
1.1443 +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.1444 +by(unfold_locales)(simp_all add: expand_finfun_eq expand_fun_eq finfun_upd_apply)
1.1445 +
1.1446 +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.1447 +proof
1.1448 + fix b' b :: 'a
1.1449 + assume fin: "finite (UNIV :: 'c set)"
1.1450 + { fix A :: "'c set"
1.1451 + interpret fun_left_comm "\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))" by(rule finfun_Diag_aux.upd_left_comm)
1.1452 + from fin have "finite A" by(auto intro: finite_subset)
1.1453 + hence "fold (\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))) (Pair b \<circ>\<^isub>f g) A =
1.1454 + Abs_finfun (\<lambda>a. (if a \<in> A then b' else b, g\<^sub>f a))"
1.1455 + by(induct)(simp_all add: finfun_const_def finfun_comp_conv_comp o_def,
1.1456 + auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite expand_fun_eq fin) }
1.1457 + 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"
1.1458 + by(simp add: finfun_const_def finfun_comp_conv_comp o_def)
1.1459 +qed
1.1460 +
1.1461 +lemma finfun_Diag_const1: "(\<lambda>\<^isup>f b, g)\<^sup>f = Pair b \<circ>\<^isub>f g"
1.1462 +by(simp add: finfun_Diag_def)
1.1463 +
1.1464 +text {*
1.1465 + 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.1466 +*}
1.1467 +
1.1468 +lemma finfun_Diag_const_code [code]:
1.1469 + "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))"
1.1470 + "(\<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))"
1.1471 +by(simp_all add: finfun_Diag_const1)
1.1472 +
1.1473 +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.1474 + 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.1475 +by(simp_all add: finfun_Diag_def)
1.1476 +
1.1477 +lemma finfun_Diag_const2: "(f, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>b. (b, c)) \<circ>\<^isub>f f"
1.1478 +by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
1.1479 +
1.1480 +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.1481 +by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
1.1482 +
1.1483 +lemma finfun_Diag_const_const [simp]: "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))"
1.1484 +by(simp add: finfun_Diag_const1)
1.1485 +
1.1486 +lemma finfun_Diag_const_update:
1.1487 + "(\<lambda>\<^isup>f b, g(\<^sup>f a := c))\<^sup>f = (\<lambda>\<^isup>f b, g)\<^sup>f(\<^sup>f a := (b, c))"
1.1488 +by(simp add: finfun_Diag_const1)
1.1489 +
1.1490 +lemma finfun_Diag_update_const:
1.1491 + "(f(\<^sup>f a := b), \<lambda>\<^isup>f c)\<^sup>f = (f, \<lambda>\<^isup>f c)\<^sup>f(\<^sup>f a := (b, c))"
1.1492 +by(simp add: finfun_Diag_def)
1.1493 +
1.1494 +lemma finfun_Diag_update_update:
1.1495 + "(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.1496 +by(auto simp add: finfun_Diag_update1 finfun_Diag_update2)
1.1497 +
1.1498 +lemma finfun_Diag_apply [simp]: "(f, g)\<^sup>f\<^sub>f = (\<lambda>x. (f\<^sub>f x, g\<^sub>f x))"
1.1499 +by(induct f rule: finfun_weak_induct)(auto simp add: finfun_Diag_const1 finfun_Diag_update1 finfun_upd_apply intro: ext)
1.1500 +
1.1501 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1.1502 +
1.1503 +lemma finfun_Diag_conv_Abs_finfun:
1.1504 + "(f, g)\<^sup>f = Abs_finfun ((\<lambda>x. (Rep_finfun f x, Rep_finfun g x)))"
1.1505 +proof -
1.1506 + 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.1507 + proof(rule finfun_rec_unique)
1.1508 + { 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.1509 + by(simp add: finfun_comp_conv_comp finfun_apply_Rep_finfun o_def finfun_const_def) }
1.1510 + { fix g' a b
1.1511 + show "Abs_finfun (\<lambda>x. (Rep_finfun g'(\<^sup>f a := b) x, Rep_finfun g x)) =
1.1512 + (Abs_finfun (\<lambda>x. (Rep_finfun g' x, Rep_finfun g x)))(\<^sup>f a := (b, g\<^sub>f a))"
1.1513 + by(auto simp add: finfun_update_def expand_fun_eq finfun_apply_Rep_finfun simp del: fun_upd_apply) simp }
1.1514 + qed(simp_all add: finfun_Diag_const1 finfun_Diag_update1)
1.1515 + thus ?thesis by(auto simp add: expand_fun_eq)
1.1516 +qed
1.1517 +
1.1518 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1.1519 +
1.1520 +lemma finfun_Diag_eq: "(f, g)\<^sup>f = (f', g')\<^sup>f \<longleftrightarrow> f = f' \<and> g = g'"
1.1521 +by(auto simp add: expand_finfun_eq expand_fun_eq)
1.1522 +
1.1523 +definition finfun_fst :: "'a \<Rightarrow>\<^isub>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b"
1.1524 +where [code]: "finfun_fst f = fst \<circ>\<^isub>f f"
1.1525 +
1.1526 +lemma finfun_fst_const: "finfun_fst (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f fst bc)"
1.1527 +by(simp add: finfun_fst_def)
1.1528 +
1.1529 +lemma finfun_fst_update: "finfun_fst (f(\<^sup>f a := bc)) = (finfun_fst f)(\<^sup>f a := fst bc)"
1.1530 + and finfun_fst_update_code: "finfun_fst (finfun_update_code f a bc) = (finfun_fst f)(\<^sup>f a := fst bc)"
1.1531 +by(simp_all add: finfun_fst_def)
1.1532 +
1.1533 +lemma finfun_fst_comp_conv: "finfun_fst (f \<circ>\<^isub>f g) = (fst \<circ> f) \<circ>\<^isub>f g"
1.1534 +by(simp add: finfun_fst_def)
1.1535 +
1.1536 +lemma finfun_fst_conv [simp]: "finfun_fst (f, g)\<^sup>f = f"
1.1537 +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.1538 +
1.1539 +lemma finfun_fst_conv_Abs_finfun: "finfun_fst = (\<lambda>f. Abs_finfun (fst o Rep_finfun f))"
1.1540 +by(simp add: finfun_fst_def_raw finfun_comp_conv_comp finfun_apply_Rep_finfun)
1.1541 +
1.1542 +
1.1543 +definition finfun_snd :: "'a \<Rightarrow>\<^isub>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c"
1.1544 +where [code]: "finfun_snd f = snd \<circ>\<^isub>f f"
1.1545 +
1.1546 +lemma finfun_snd_const: "finfun_snd (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f snd bc)"
1.1547 +by(simp add: finfun_snd_def)
1.1548 +
1.1549 +lemma finfun_snd_update: "finfun_snd (f(\<^sup>f a := bc)) = (finfun_snd f)(\<^sup>f a := snd bc)"
1.1550 + and finfun_snd_update_code [code]: "finfun_snd (finfun_update_code f a bc) = (finfun_snd f)(\<^sup>f a := snd bc)"
1.1551 +by(simp_all add: finfun_snd_def)
1.1552 +
1.1553 +lemma finfun_snd_comp_conv: "finfun_snd (f \<circ>\<^isub>f g) = (snd \<circ> f) \<circ>\<^isub>f g"
1.1554 +by(simp add: finfun_snd_def)
1.1555 +
1.1556 +lemma finfun_snd_conv [simp]: "finfun_snd (f, g)\<^sup>f = g"
1.1557 +apply(induct f rule: finfun_weak_induct)
1.1558 +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.1559 +done
1.1560 +
1.1561 +lemma finfun_snd_conv_Abs_finfun: "finfun_snd = (\<lambda>f. Abs_finfun (snd o Rep_finfun f))"
1.1562 +by(simp add: finfun_snd_def_raw finfun_comp_conv_comp finfun_apply_Rep_finfun)
1.1563 +
1.1564 +lemma finfun_Diag_collapse [simp]: "(finfun_fst f, finfun_snd f)\<^sup>f = f"
1.1565 +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.1566 +
1.1567 +subsection {* Currying for FinFuns *}
1.1568 +
1.1569 +definition finfun_curry :: "('a \<times> 'b) \<Rightarrow>\<^isub>f 'c \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b \<Rightarrow>\<^isub>f 'c"
1.1570 +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.1571 +
1.1572 +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.1573 +apply(unfold_locales)
1.1574 +apply(auto simp add: split_def finfun_update_twist finfun_upd_apply split_paired_all finfun_update_const_same)
1.1575 +done
1.1576 +
1.1577 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1.1578 +
1.1579 +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.1580 +proof(unfold_locales)
1.1581 + fix b' b :: 'b
1.1582 + assume fin: "finite (UNIV :: ('c \<times> 'a) set)"
1.1583 + hence fin1: "finite (UNIV :: 'c set)" and fin2: "finite (UNIV :: 'a set)"
1.1584 + unfolding UNIV_Times_UNIV[symmetric]
1.1585 + by(fastsimp dest: finite_cartesian_productD1 finite_cartesian_productD2)+
1.1586 + note [simp] = Abs_finfun_inverse_finite[OF fin] Abs_finfun_inverse_finite[OF fin1] Abs_finfun_inverse_finite[OF fin2]
1.1587 + { fix A :: "('c \<times> 'a) set"
1.1588 + 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'"
1.1589 + by(rule finfun_curry_aux.upd_left_comm)
1.1590 + from fin have "finite A" by(auto intro: finite_subset)
1.1591 + 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))"
1.1592 + 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.1593 + from this[of UNIV]
1.1594 + 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'"
1.1595 + by(simp add: finfun_const_def)
1.1596 +qed
1.1597 +
1.1598 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1.1599 +
1.1600 +lemma finfun_curry_const [simp, code]: "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
1.1601 +by(simp add: finfun_curry_def)
1.1602 +
1.1603 +lemma finfun_curry_update [simp]:
1.1604 + "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.1605 + and finfun_curry_update_code [code]:
1.1606 + "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))"
1.1607 +by(simp_all add: finfun_curry_def)
1.1608 +
1.1609 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1.1610 +
1.1611 +lemma finfun_Abs_finfun_curry: assumes fin: "f \<in> finfun"
1.1612 + shows "(\<lambda>a. Abs_finfun (curry f a)) \<in> finfun"
1.1613 +proof -
1.1614 + from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast
1.1615 + have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force)
1.1616 + hence "{a. curry f a \<noteq> (\<lambda>x. c)} = fst ` {ab. f ab \<noteq> c}"
1.1617 + by(auto simp add: curry_def expand_fun_eq)
1.1618 + with fin c have "finite {a. Abs_finfun (curry f a) \<noteq> (\<lambda>\<^isup>f c)}"
1.1619 + by(simp add: finfun_const_def finfun_curry)
1.1620 + thus ?thesis unfolding finfun_def by auto
1.1621 +qed
1.1622 +
1.1623 +lemma finfun_curry_conv_curry:
1.1624 + fixes f :: "('a \<times> 'b) \<Rightarrow>\<^isub>f 'c"
1.1625 + shows "finfun_curry f = Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun f) a))"
1.1626 +proof -
1.1627 + have "finfun_curry = (\<lambda>f :: ('a \<times> 'b) \<Rightarrow>\<^isub>f 'c. Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun f) a)))"
1.1628 + proof(rule finfun_rec_unique)
1.1629 + { fix c show "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)" by simp }
1.1630 + { 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.1631 + by(cases a) simp }
1.1632 + { 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.1633 + by(simp add: finfun_curry_def finfun_const_def curry_def) }
1.1634 + { fix g a b
1.1635 + show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (Rep_finfun g(\<^sup>f a := b)) aa)) =
1.1636 + (Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun g) a)))(\<^sup>f
1.1637 + fst a := ((Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun g) a)))\<^sub>f (fst a))(\<^sup>f snd a := b))"
1.1638 + 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.1639 + qed
1.1640 + thus ?thesis by(auto simp add: expand_fun_eq)
1.1641 +qed
1.1642 +
1.1643 +subsection {* Executable equality for FinFuns *}
1.1644 +
1.1645 +lemma eq_finfun_All_ext: "(f = g) \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>\<^isub>f (f, g)\<^sup>f)"
1.1646 +by(simp add: expand_finfun_eq expand_fun_eq finfun_All_All o_def)
1.1647 +
1.1648 +instantiation finfun :: ("{card_UNIV,eq}",eq) eq begin
1.1649 +definition eq_finfun_def: "eq_class.eq f g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>\<^isub>f (f, g)\<^sup>f)"
1.1650 +instance by(intro_classes)(simp add: eq_finfun_All_ext eq_finfun_def)
1.1651 +end
1.1652 +
1.1653 +subsection {* Operator that explicitly removes all redundant updates in the generated representations *}
1.1654 +
1.1655 +definition finfun_clearjunk :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b"
1.1656 +where [simp, code del]: "finfun_clearjunk = id"
1.1657 +
1.1658 +lemma finfun_clearjunk_const [code]: "finfun_clearjunk (\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b)"
1.1659 +by simp
1.1660 +
1.1661 +lemma finfun_clearjunk_update [code]: "finfun_clearjunk (finfun_update_code f a b) = f(\<^sup>f a := b)"
1.1662 +by simp
1.1663 +
1.1664 +end
1.1665 \ No newline at end of file
2.1 --- a/src/HOL/Library/Library.thy Tue Jun 02 15:53:07 2009 +0200
2.2 +++ b/src/HOL/Library/Library.thy Tue Jun 02 15:53:34 2009 +0200
2.3 @@ -22,6 +22,7 @@
2.4 Enum
2.5 Eval_Witness
2.6 Executable_Set
2.7 + Fin_Fun
2.8 Float
2.9 Formal_Power_Series
2.10 FrechetDeriv