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]:

     2.1 --- a/src/HOL/ex/FinFunPred.thy	Tue May 29 15:31:58 2012 +0200
     2.2 +++ b/src/HOL/ex/FinFunPred.thy	Tue May 29 16:08:12 2012 +0200
     2.3 @@ -195,7 +195,7 @@
     2.4  
     2.5  lemma iso_finfun_eq [code_unfold]:
     2.6    "A\<^sub>f = B\<^sub>f \<longleftrightarrow> A = B"
     2.7 -by(simp add: expand_finfun_eq)
     2.8 +by(simp only: expand_finfun_eq)
     2.9  
    2.10  lemma iso_finfun_sup [code_unfold]:
    2.11    "sup A\<^sub>f B\<^sub>f = (sup A B)\<^sub>f"