1.1 --- a/src/HOL/Library/FinFun.thy Tue May 29 15:31:58 2012 +0200
1.2 +++ b/src/HOL/Library/FinFun.thy Tue May 29 16:08:12 2012 +0200
1.3 @@ -84,6 +84,7 @@
1.4 definition "finfun = {f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}"
1.5
1.6 typedef (open) ('a,'b) finfun ("(_ \<Rightarrow>\<^isub>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set"
1.7 + morphisms finfun_apply Abs_finfun
1.8 proof -
1.9 have "\<exists>f. finite {x. f x \<noteq> undefined}"
1.10 proof
1.11 @@ -194,8 +195,8 @@
1.12 qed
1.13
1.14 lemmas finfun_simp =
1.15 - fst_finfun snd_finfun Abs_finfun_inverse Rep_finfun_inverse Abs_finfun_inject Rep_finfun_inject Diag_finfun finfun_curry
1.16 -lemmas finfun_iff = const_finfun fun_upd_finfun Rep_finfun map_of_finfun
1.17 + fst_finfun snd_finfun Abs_finfun_inverse finfun_apply_inverse Abs_finfun_inject finfun_apply_inject Diag_finfun finfun_curry
1.18 +lemmas finfun_iff = const_finfun fun_upd_finfun finfun_apply map_of_finfun
1.19 lemmas finfun_intro = finfun_left_compose fst_finfun snd_finfun
1.20
1.21 lemma Abs_finfun_inject_finite:
1.22 @@ -231,7 +232,7 @@
1.23 lemma Abs_finfun_inverse_finite:
1.24 fixes x :: "'a \<Rightarrow> 'b"
1.25 assumes fin: "finite (UNIV :: 'a set)"
1.26 - shows "Rep_finfun (Abs_finfun x) = x"
1.27 + shows "finfun_apply (Abs_finfun x) = x"
1.28 proof -
1.29 from fin have "x \<in> finfun"
1.30 by(auto simp add: finfun_def intro: finite_subset)
1.31 @@ -242,7 +243,7 @@
1.32
1.33 lemma Abs_finfun_inverse_finite_class:
1.34 fixes x :: "('a :: finite) \<Rightarrow> 'b"
1.35 - shows "Rep_finfun (Abs_finfun x) = x"
1.36 + shows "finfun_apply (Abs_finfun x) = x"
1.37 using finite_UNIV by(simp add: Abs_finfun_inverse_finite)
1.38
1.39 lemma finfun_eq_finite_UNIV: "finite (UNIV :: 'a set) \<Longrightarrow> (finfun :: ('a \<Rightarrow> 'b) set) = UNIV"
1.40 @@ -325,7 +326,7 @@
1.41 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.42 proof
1.43 fix b
1.44 - have "(Rep_finfun b)(a := b', a' := b') = (Rep_finfun b)(a' := b', a := b')"
1.45 + have "(finfun_apply b)(a := b', a' := b') = (finfun_apply b)(a' := b', a := b')"
1.46 by(cases "a = a'")(auto simp add: fun_upd_twist)
1.47 then have "b(\<^sup>f a := b')(\<^sup>f a' := b') = b(\<^sup>f a' := b')(\<^sup>f a := b')"
1.48 by(auto simp add: finfun_update_def fun_upd_twist)
1.49 @@ -422,7 +423,7 @@
1.50 lift_definition finfun_default :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'b"
1.51 is "finfun_default_aux" ..
1.52
1.53 -lemma finite_finfun_default: "finite {a. Rep_finfun f a \<noteq> finfun_default f}"
1.54 +lemma finite_finfun_default: "finite {a. finfun_apply f a \<noteq> finfun_default f}"
1.55 apply transfer apply (erule finite_finfun_default_aux)
1.56 unfolding Rel_def fun_rel_def cr_finfun_def by simp
1.57
1.58 @@ -874,8 +875,7 @@
1.59
1.60 subsection {* Function application *}
1.61
1.62 -definition finfun_apply :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b" ("_\<^sub>f" [1000] 1000)
1.63 -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.64 +notation finfun_apply ("_\<^sub>f" [1000] 1000)
1.65
1.66 interpretation finfun_apply_aux: finfun_rec_wf_aux "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c"
1.67 by(unfold_locales) auto
1.68 @@ -892,13 +892,21 @@
1.69 from this[of UNIV] show "Finite_Set.fold (\<lambda>a'. If (a = a') b') b UNIV = b'" by simp
1.70 qed
1.71
1.72 -lemma finfun_const_apply [simp, code]: "(\<lambda>\<^isup>f b)\<^sub>f a = b"
1.73 -by(simp add: finfun_apply_def)
1.74 +lemma finfun_apply_def: "finfun_apply = (\<lambda>f a. finfun_rec (\<lambda>b. b) (\<lambda>a' b c. if (a = a') then b else c) f)"
1.75 +proof(rule finfun_rec_unique)
1.76 + fix c show "finfun_apply (\<lambda>\<^isup>f c) = (\<lambda>a. c)" by(simp add: finfun_const.rep_eq)
1.77 +next
1.78 + fix g a b show "finfun_apply g(\<^sup>f a := b) = (\<lambda>c. if c = a then b else finfun_apply g c)"
1.79 + by(auto simp add: finfun_update_def fun_upd_finfun Abs_finfun_inverse finfun_apply)
1.80 +qed auto
1.81
1.82 lemma finfun_upd_apply: "f(\<^sup>fa := b)\<^sub>f a' = (if a = a' then b else f\<^sub>f a')"
1.83 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.84 by(simp_all add: finfun_apply_def)
1.85
1.86 +lemma finfun_const_apply [simp, code]: "(\<lambda>\<^isup>f b)\<^sub>f a = b"
1.87 +by(simp add: finfun_apply_def)
1.88 +
1.89 lemma finfun_upd_apply_same [simp]:
1.90 "f(\<^sup>fa := b)\<^sub>f a = b"
1.91 by(simp add: finfun_upd_apply)
1.92 @@ -909,17 +917,8 @@
1.93
1.94 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1.95
1.96 -lemma finfun_apply_Rep_finfun:
1.97 - "finfun_apply = Rep_finfun"
1.98 -proof(rule finfun_rec_unique)
1.99 - fix c show "Rep_finfun (\<lambda>\<^isup>f c) = (\<lambda>a. c)" by(auto simp add: finfun_const_def)
1.100 -next
1.101 - 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.102 - by(auto simp add: finfun_update_def fun_upd_finfun Abs_finfun_inverse Rep_finfun intro: ext)
1.103 -qed(auto intro: ext)
1.104 -
1.105 lemma finfun_ext: "(\<And>a. f\<^sub>f a = g\<^sub>f a) \<Longrightarrow> f = g"
1.106 -by(auto simp add: finfun_apply_Rep_finfun Rep_finfun_inject[symmetric] simp del: Rep_finfun_inject intro: ext)
1.107 +by(auto simp add: finfun_apply_inject[symmetric] simp del: finfun_apply_inject)
1.108
1.109 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1.110
1.111 @@ -986,9 +985,9 @@
1.112 { 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.113 proof -
1.114 obtain y where y: "y \<in> finfun" and g': "g' = Abs_finfun y" by(cases g')
1.115 - moreover hence "(g \<circ> g'\<^sub>f) \<in> finfun" by(simp add: finfun_apply_Rep_finfun finfun_left_compose)
1.116 + moreover hence "(g \<circ> g'\<^sub>f) \<in> finfun" by(simp add: finfun_left_compose)
1.117 moreover have "g \<circ> y(a := b) = (g \<circ> y)(a := g b)" by(auto intro: ext)
1.118 - ultimately show ?thesis by(simp add: finfun_comp_def finfun_update_def finfun_apply_Rep_finfun)
1.119 + ultimately show ?thesis by(simp add: finfun_comp_def finfun_update_def)
1.120 qed }
1.121 qed auto
1.122 thus ?thesis by(auto simp add: fun_eq_iff)
1.123 @@ -997,7 +996,7 @@
1.124 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1.125
1.126 definition finfun_comp2 :: "'b \<Rightarrow>\<^isub>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c" (infixr "\<^sub>f\<circ>" 55)
1.127 -where [code del]: "finfun_comp2 g f = Abs_finfun (Rep_finfun g \<circ> f)"
1.128 +where [code del]: "finfun_comp2 g f = Abs_finfun (finfun_apply g \<circ> f)"
1.129
1.130 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1.131
1.132 @@ -1009,18 +1008,17 @@
1.133 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.134 proof(cases "b \<in> range f")
1.135 case True
1.136 - 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.137 + from inj have "\<And>x. (finfun_apply g)(f x := c) \<circ> f = (finfun_apply g \<circ> f)(x := c)" by(auto intro!: ext dest: injD)
1.138 with inj True show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def finfun_right_compose)
1.139 next
1.140 case False
1.141 - hence "(Rep_finfun g)(b := c) \<circ> f = Rep_finfun g \<circ> f" by(auto simp add: fun_eq_iff)
1.142 + hence "(finfun_apply g)(b := c) \<circ> f = finfun_apply g \<circ> f" by(auto simp add: fun_eq_iff)
1.143 with False show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def)
1.144 qed
1.145
1.146 declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
1.147
1.148
1.149 -
1.150 subsection {* Universal quantification *}
1.151
1.152 definition finfun_All_except :: "'a list \<Rightarrow> 'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
1.153 @@ -1131,16 +1129,16 @@
1.154 declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
1.155
1.156 lemma finfun_Diag_conv_Abs_finfun:
1.157 - "(f, g)\<^sup>f = Abs_finfun ((\<lambda>x. (Rep_finfun f x, Rep_finfun g x)))"
1.158 + "(f, g)\<^sup>f = Abs_finfun ((\<lambda>x. (finfun_apply f x, finfun_apply g x)))"
1.159 proof -
1.160 - 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.161 + have "(\<lambda>f :: 'a \<Rightarrow>\<^isub>f 'b. (f, g)\<^sup>f) = (\<lambda>f. Abs_finfun ((\<lambda>x. (finfun_apply f x, finfun_apply g x))))"
1.162 proof(rule finfun_rec_unique)
1.163 - { 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.164 - by(simp add: finfun_comp_conv_comp finfun_apply_Rep_finfun o_def finfun_const_def) }
1.165 + { fix c show "Abs_finfun (\<lambda>x. (finfun_apply (\<lambda>\<^isup>f c) x, finfun_apply g x)) = Pair c \<circ>\<^isub>f g"
1.166 + by(simp add: finfun_comp_conv_comp o_def finfun_const_def) }
1.167 { fix g' a b
1.168 - show "Abs_finfun (\<lambda>x. (Rep_finfun g'(\<^sup>f a := b) x, Rep_finfun g x)) =
1.169 - (Abs_finfun (\<lambda>x. (Rep_finfun g' x, Rep_finfun g x)))(\<^sup>f a := (b, g\<^sub>f a))"
1.170 - by(auto simp add: finfun_update_def fun_eq_iff finfun_apply_Rep_finfun simp del: fun_upd_apply) simp }
1.171 + show "Abs_finfun (\<lambda>x. (finfun_apply g'(\<^sup>f a := b) x, finfun_apply g x)) =
1.172 + (Abs_finfun (\<lambda>x. (finfun_apply g' x, finfun_apply g x)))(\<^sup>f a := (b, g\<^sub>f a))"
1.173 + by(auto simp add: finfun_update_def fun_eq_iff simp del: fun_upd_apply) simp }
1.174 qed(simp_all add: finfun_Diag_const1 finfun_Diag_update1)
1.175 thus ?thesis by(auto simp add: fun_eq_iff)
1.176 qed
1.177 @@ -1166,8 +1164,8 @@
1.178 lemma finfun_fst_conv [simp]: "finfun_fst (f, g)\<^sup>f = f"
1.179 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.180
1.181 -lemma finfun_fst_conv_Abs_finfun: "finfun_fst = (\<lambda>f. Abs_finfun (fst o Rep_finfun f))"
1.182 -by(simp add: finfun_fst_def [abs_def] finfun_comp_conv_comp finfun_apply_Rep_finfun)
1.183 +lemma finfun_fst_conv_Abs_finfun: "finfun_fst = (\<lambda>f. Abs_finfun (fst o finfun_apply f))"
1.184 +by(simp add: finfun_fst_def [abs_def] finfun_comp_conv_comp)
1.185
1.186
1.187 definition finfun_snd :: "'a \<Rightarrow>\<^isub>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c"
1.188 @@ -1188,8 +1186,8 @@
1.189 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.190 done
1.191
1.192 -lemma finfun_snd_conv_Abs_finfun: "finfun_snd = (\<lambda>f. Abs_finfun (snd o Rep_finfun f))"
1.193 -by(simp add: finfun_snd_def [abs_def] finfun_comp_conv_comp finfun_apply_Rep_finfun)
1.194 +lemma finfun_snd_conv_Abs_finfun: "finfun_snd = (\<lambda>f. Abs_finfun (snd o finfun_apply f))"
1.195 +by(simp add: finfun_snd_def [abs_def] finfun_comp_conv_comp)
1.196
1.197 lemma finfun_Diag_collapse [simp]: "(finfun_fst f, finfun_snd f)\<^sup>f = f"
1.198 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.199 @@ -1219,7 +1217,7 @@
1.200 by(rule finfun_curry_aux.upd_left_comm)
1.201 from fin have "finite A" by(auto intro: finite_subset)
1.202 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.203 - 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.204 + by induct (simp_all, auto simp add: finfun_update_def finfun_const_def split_def intro!: arg_cong[where f="Abs_finfun"] ext) }
1.205 from this[of UNIV]
1.206 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.207 by(simp add: finfun_const_def)
1.208 @@ -1252,20 +1250,20 @@
1.209
1.210 lemma finfun_curry_conv_curry:
1.211 fixes f :: "('a \<times> 'b) \<Rightarrow>\<^isub>f 'c"
1.212 - shows "finfun_curry f = Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun f) a))"
1.213 + shows "finfun_curry f = Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply f) a))"
1.214 proof -
1.215 - have "finfun_curry = (\<lambda>f :: ('a \<times> 'b) \<Rightarrow>\<^isub>f 'c. Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun f) a)))"
1.216 + have "finfun_curry = (\<lambda>f :: ('a \<times> 'b) \<Rightarrow>\<^isub>f 'c. Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply f) a)))"
1.217 proof(rule finfun_rec_unique)
1.218 { fix c show "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)" by simp }
1.219 { 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.220 by(cases a) simp }
1.221 - { 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.222 + { fix c show "Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply (\<lambda>\<^isup>f c)) a)) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
1.223 by(simp add: finfun_curry_def finfun_const_def curry_def) }
1.224 { fix g a b
1.225 - show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (Rep_finfun g(\<^sup>f a := b)) aa)) =
1.226 - (Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun g) a)))(\<^sup>f
1.227 - fst a := ((Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun g) a)))\<^sub>f (fst a))(\<^sup>f snd a := b))"
1.228 - 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.229 + show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (finfun_apply g(\<^sup>f a := b)) aa)) =
1.230 + (Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply g) a)))(\<^sup>f
1.231 + fst a := ((Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply g) a)))\<^sub>f (fst a))(\<^sup>f snd a := b))"
1.232 + by(cases a)(auto intro!: ext arg_cong[where f=Abs_finfun] simp add: finfun_curry_def finfun_update_def finfun_curry finfun_Abs_finfun_curry) }
1.233 qed
1.234 thus ?thesis by(auto simp add: fun_eq_iff)
1.235 qed
1.236 @@ -1318,14 +1316,14 @@
1.237
1.238 lemma finfun_dom_finfunI: "(\<lambda>a. f\<^sub>f a \<noteq> finfun_default f) \<in> finfun"
1.239 using finite_finfun_default[of f]
1.240 -by(simp add: finfun_def finfun_apply_Rep_finfun exI[where x=False])
1.241 +by(simp add: finfun_def exI[where x=False])
1.242
1.243 lemma finfun_dom_update [simp]:
1.244 "finfun_dom (f(\<^sup>f a := b)) = (finfun_dom f)(\<^sup>f a := (b \<noteq> finfun_default f))"
1.245 unfolding finfun_dom_def finfun_update_def
1.246 -apply(simp add: finfun_default_update_const finfun_upd_apply finfun_dom_finfunI)
1.247 +apply(simp add: finfun_default_update_const fun_upd_apply finfun_dom_finfunI)
1.248 apply(fold finfun_update.rep_eq)
1.249 -apply(simp add: finfun_upd_apply fun_eq_iff finfun_default_update_const)
1.250 +apply(simp add: finfun_upd_apply fun_eq_iff fun_upd_def finfun_default_update_const)
1.251 done
1.252
1.253 lemma finfun_dom_update_code [code]: