src/HOL/Library/FinFun.thy
changeset 48030 ac43c8a7dcb5
parent 48029 9d9c9069abbc
child 48031 bbf95f3595ab
     1.1 --- a/src/HOL/Library/FinFun.thy	Tue May 29 16:08:12 2012 +0200
     1.2 +++ b/src/HOL/Library/FinFun.thy	Tue May 29 16:41:00 2012 +0200
     1.3 @@ -194,10 +194,12 @@
     1.4    thus "curry f a \<in> finfun" unfolding finfun_def by auto
     1.5  qed
     1.6  
     1.7 -lemmas finfun_simp = 
     1.8 -  fst_finfun snd_finfun Abs_finfun_inverse finfun_apply_inverse Abs_finfun_inject finfun_apply_inject Diag_finfun finfun_curry
     1.9 -lemmas finfun_iff = const_finfun fun_upd_finfun finfun_apply map_of_finfun
    1.10 -lemmas finfun_intro = finfun_left_compose fst_finfun snd_finfun
    1.11 +bundle finfun =
    1.12 +  fst_finfun[simp] snd_finfun[simp] Abs_finfun_inverse[simp] 
    1.13 +  finfun_apply_inverse[simp] Abs_finfun_inject[simp] finfun_apply_inject[simp]
    1.14 +  Diag_finfun[simp] finfun_curry[simp]
    1.15 +  const_finfun[iff] fun_upd_finfun[iff] finfun_apply[iff] map_of_finfun[iff]
    1.16 +  finfun_left_compose[intro] fst_finfun[intro] snd_finfun[intro]
    1.17  
    1.18  lemma Abs_finfun_inject_finite:
    1.19    fixes x y :: "'a \<Rightarrow> 'b"
    1.20 @@ -227,20 +229,17 @@
    1.21    ultimately show "x = y" by(simp add: Abs_finfun_inject)
    1.22  qed
    1.23  
    1.24 -declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
    1.25 -
    1.26  lemma Abs_finfun_inverse_finite:
    1.27    fixes x :: "'a \<Rightarrow> 'b"
    1.28    assumes fin: "finite (UNIV :: 'a set)"
    1.29    shows "finfun_apply (Abs_finfun x) = x"
    1.30 +  including finfun
    1.31  proof -
    1.32    from fin have "x \<in> finfun"
    1.33      by(auto simp add: finfun_def intro: finite_subset)
    1.34    thus ?thesis by simp
    1.35  qed
    1.36  
    1.37 -declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
    1.38 -
    1.39  lemma Abs_finfun_inverse_finite_class:
    1.40    fixes x :: "('a :: finite) \<Rightarrow> 'b"
    1.41    shows "finfun_apply (Abs_finfun x) = x"
    1.42 @@ -282,8 +281,6 @@
    1.43  
    1.44  lift_definition finfun_update :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("_'(\<^sup>f/ _ := _')" [1000,0,0] 1000) is "fun_upd" by (simp add: fun_upd_finfun)
    1.45  
    1.46 -declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
    1.47 -
    1.48  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.49  by transfer (simp add: fun_upd_twist)
    1.50  
    1.51 @@ -294,8 +291,6 @@
    1.52  lemma finfun_update_const_same: "(\<lambda>\<^isup>f b)(\<^sup>f a := b) = (\<lambda>\<^isup>f b)"
    1.53  by transfer (simp add: fun_eq_iff)
    1.54  
    1.55 -declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
    1.56 -
    1.57  subsection {* Code generator setup *}
    1.58  
    1.59  definition finfun_update_code :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("_'(\<^sup>fc/ _ := _')" [1000,0,0] 1000)
    1.60 @@ -318,9 +313,8 @@
    1.61  
    1.62  subsection {* @{text "finfun_update"} as instance of @{text "comp_fun_commute"} *}
    1.63  
    1.64 -declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
    1.65 -
    1.66  interpretation finfun_update: comp_fun_commute "\<lambda>a f. f(\<^sup>f a :: 'a := b')"
    1.67 +  including finfun
    1.68  proof
    1.69    fix a a' :: 'a
    1.70    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.71 @@ -469,8 +463,6 @@
    1.72  lemma upd_upd_twice: "upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)"
    1.73  by(cases "b \<noteq> b'")(auto simp add: fun_upd_def upd_const_same upd_idemp)
    1.74  
    1.75 -declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
    1.76 -
    1.77  lemma map_default_update_const:
    1.78    assumes fin: "finite (dom f)"
    1.79    and anf: "a \<notin> dom f"
    1.80 @@ -548,8 +540,6 @@
    1.81    qed
    1.82  qed
    1.83  
    1.84 -declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
    1.85 -
    1.86  lemma map_default_eq_id [simp]: "map_default d ((\<lambda>a. Some (f a)) |` {a. f a \<noteq> d}) = f"
    1.87  by(auto simp add: map_default_def restrict_map_def intro: ext)
    1.88  
    1.89 @@ -579,10 +569,9 @@
    1.90    thus ?thesis by blast
    1.91  qed
    1.92  
    1.93 -declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
    1.94 -
    1.95  lemma finfun_rec_upd [simp]:
    1.96    "finfun_rec cnst upd (f(\<^sup>f a' := b')) = upd a' b' (finfun_rec cnst upd f)"
    1.97 +  including finfun
    1.98  proof -
    1.99    obtain b where b: "b = finfun_default f" by auto
   1.100    let ?the = "\<lambda>f g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g"
   1.101 @@ -740,8 +729,6 @@
   1.102    qed
   1.103  qed
   1.104  
   1.105 -declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
   1.106 -
   1.107  end
   1.108  
   1.109  locale finfun_rec_wf = finfun_rec_wf_aux + 
   1.110 @@ -749,9 +736,7 @@
   1.111    "finite (UNIV :: 'a set) \<Longrightarrow> Finite_Set.fold (\<lambda>a. upd a b') (cnst b) (UNIV :: 'a set) = cnst b'"
   1.112  begin
   1.113  
   1.114 -declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
   1.115 -
   1.116 -lemma finfun_rec_const [simp]:
   1.117 +lemma finfun_rec_const [simp]: includes finfun shows
   1.118    "finfun_rec cnst upd (\<lambda>\<^isup>f c) = cnst c"
   1.119  proof(cases "finite (UNIV :: 'a set)")
   1.120    case False
   1.121 @@ -787,7 +772,7 @@
   1.122          and fin: "finite (dom g')" and g: "undefined \<notin> ran g'" by simp_all
   1.123        from fin have "map_default undefined g' \<in> finfun" by(rule map_default_in_finfun)
   1.124        with fg have "map_default undefined g' = (\<lambda>a. c)"
   1.125 -        by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1])
   1.126 +        by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1, symmetric])
   1.127        with True show "g' = empty"
   1.128          by -(rule map_default_inject(2)[OF _ fin g], auto)
   1.129      qed
   1.130 @@ -816,18 +801,15 @@
   1.131    qed
   1.132  qed
   1.133  
   1.134 -declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
   1.135 -
   1.136  end
   1.137  
   1.138  subsection {* Weak induction rule and case analysis for FinFuns *}
   1.139  
   1.140 -declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
   1.141 -
   1.142  lemma finfun_weak_induct [consumes 0, case_names const update]:
   1.143    assumes const: "\<And>b. P (\<lambda>\<^isup>f b)"
   1.144    and update: "\<And>f a b. P f \<Longrightarrow> P (f(\<^sup>f a := b))"
   1.145    shows "P x"
   1.146 +  including finfun
   1.147  proof(induct x rule: Abs_finfun_induct)
   1.148    case (Abs_finfun y)
   1.149    then obtain b where "finite {a. y a \<noteq> b}" unfolding finfun_def by blast
   1.150 @@ -849,8 +831,6 @@
   1.151    qed
   1.152  qed
   1.153  
   1.154 -declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
   1.155 -
   1.156  lemma finfun_exhaust_disj: "(\<exists>b. x = finfun_const b) \<or> (\<exists>f a b. x = finfun_update f a b)"
   1.157  by(induct x rule: finfun_weak_induct) blast+
   1.158  
   1.159 @@ -915,13 +895,9 @@
   1.160    "a \<noteq> a' \<Longrightarrow> f(\<^sup>fa := b)\<^sub>f a' = f\<^sub>f a'"
   1.161  by(simp add: finfun_upd_apply)
   1.162  
   1.163 -declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
   1.164 -
   1.165  lemma finfun_ext: "(\<And>a. f\<^sub>f a = g\<^sub>f a) \<Longrightarrow> f = g"
   1.166  by(auto simp add: finfun_apply_inject[symmetric] simp del: finfun_apply_inject)
   1.167  
   1.168 -declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
   1.169 -
   1.170  lemma expand_finfun_eq: "(f = g) = (f\<^sub>f = g\<^sub>f)"
   1.171  by(auto intro: finfun_ext)
   1.172  
   1.173 @@ -974,9 +950,8 @@
   1.174  lemma finfun_comp_id1 [simp]: "(\<lambda>x. x) \<circ>\<^isub>f f = f" "id \<circ>\<^isub>f f = f"
   1.175  by(induct f rule: finfun_weak_induct) auto
   1.176  
   1.177 -declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
   1.178 -
   1.179  lemma finfun_comp_conv_comp: "g \<circ>\<^isub>f f = Abs_finfun (g \<circ> finfun_apply f)"
   1.180 +  including finfun
   1.181  proof -
   1.182    have "(\<lambda>f. g \<circ>\<^isub>f f) = (\<lambda>f. Abs_finfun (g \<circ> finfun_apply f))"
   1.183    proof(rule finfun_rec_unique)
   1.184 @@ -993,17 +968,15 @@
   1.185    thus ?thesis by(auto simp add: fun_eq_iff)
   1.186  qed
   1.187  
   1.188 -declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
   1.189 -
   1.190  definition finfun_comp2 :: "'b \<Rightarrow>\<^isub>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c" (infixr "\<^sub>f\<circ>" 55)
   1.191  where [code del]: "finfun_comp2 g f = Abs_finfun (finfun_apply g \<circ> f)"
   1.192  
   1.193 -declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
   1.194 -
   1.195  lemma finfun_comp2_const [code, simp]: "finfun_comp2 (\<lambda>\<^isup>f c) f = (\<lambda>\<^isup>f c)"
   1.196 +  including finfun
   1.197  by(simp add: finfun_comp2_def finfun_const_def comp_def)
   1.198  
   1.199  lemma finfun_comp2_update:
   1.200 +  includes finfun
   1.201    assumes inj: "inj f"
   1.202    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.203  proof(cases "b \<in> range f")
   1.204 @@ -1016,9 +989,6 @@
   1.205    with False show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def)
   1.206  qed
   1.207  
   1.208 -declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
   1.209 -
   1.210 -
   1.211  subsection {* Universal quantification *}
   1.212  
   1.213  definition finfun_All_except :: "'a list \<Rightarrow> 'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
   1.214 @@ -1126,10 +1096,9 @@
   1.215  lemma finfun_Diag_apply [simp]: "(f, g)\<^sup>f\<^sub>f = (\<lambda>x. (f\<^sub>f x, g\<^sub>f x))"
   1.216  by(induct f rule: finfun_weak_induct)(auto simp add: finfun_Diag_const1 finfun_Diag_update1 finfun_upd_apply intro: ext)
   1.217  
   1.218 -declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
   1.219 -
   1.220  lemma finfun_Diag_conv_Abs_finfun:
   1.221    "(f, g)\<^sup>f = Abs_finfun ((\<lambda>x. (finfun_apply f x, finfun_apply g x)))"
   1.222 +  including finfun
   1.223  proof -
   1.224    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.225    proof(rule finfun_rec_unique)
   1.226 @@ -1143,8 +1112,6 @@
   1.227    thus ?thesis by(auto simp add: fun_eq_iff)
   1.228  qed
   1.229  
   1.230 -declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
   1.231 -
   1.232  lemma finfun_Diag_eq: "(f, g)\<^sup>f = (f', g')\<^sup>f \<longleftrightarrow> f = f' \<and> g = g'"
   1.233  by(auto simp add: expand_finfun_eq fun_eq_iff)
   1.234  
   1.235 @@ -1202,8 +1169,6 @@
   1.236  apply(auto simp add: split_def finfun_update_twist finfun_upd_apply split_paired_all finfun_update_const_same)
   1.237  done
   1.238  
   1.239 -declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
   1.240 -
   1.241  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.242  proof(unfold_locales)
   1.243    fix b' b :: 'b
   1.244 @@ -1223,8 +1188,6 @@
   1.245      by(simp add: finfun_const_def)
   1.246  qed
   1.247  
   1.248 -declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
   1.249 -
   1.250  lemma finfun_curry_const [simp, code]: "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
   1.251  by(simp add: finfun_curry_def)
   1.252  
   1.253 @@ -1234,10 +1197,9 @@
   1.254    "finfun_curry (f(\<^sup>fc (a, b) := c)) = (finfun_curry f)(\<^sup>f a := ((finfun_curry f)\<^sub>f a)(\<^sup>f b := c))"
   1.255  by(simp_all add: finfun_curry_def)
   1.256  
   1.257 -declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
   1.258 -
   1.259  lemma finfun_Abs_finfun_curry: assumes fin: "f \<in> finfun"
   1.260    shows "(\<lambda>a. Abs_finfun (curry f a)) \<in> finfun"
   1.261 +  including finfun
   1.262  proof -
   1.263    from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast
   1.264    have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force)
   1.265 @@ -1251,6 +1213,7 @@
   1.266  lemma finfun_curry_conv_curry:
   1.267    fixes f :: "('a \<times> 'b) \<Rightarrow>\<^isub>f 'c"
   1.268    shows "finfun_curry f = Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply f) a))"
   1.269 +  including finfun
   1.270  proof -
   1.271    have "finfun_curry = (\<lambda>f :: ('a \<times> 'b) \<Rightarrow>\<^isub>f 'c. Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply f) a)))"
   1.272    proof(rule finfun_rec_unique)
   1.273 @@ -1320,7 +1283,7 @@
   1.274  
   1.275  lemma finfun_dom_update [simp]:
   1.276    "finfun_dom (f(\<^sup>f a := b)) = (finfun_dom f)(\<^sup>f a := (b \<noteq> finfun_default f))"
   1.277 -unfolding finfun_dom_def finfun_update_def
   1.278 +including finfun unfolding finfun_dom_def finfun_update_def
   1.279  apply(simp add: finfun_default_update_const fun_upd_apply finfun_dom_finfunI)
   1.280  apply(fold finfun_update.rep_eq)
   1.281  apply(simp add: finfun_upd_apply fun_eq_iff fun_upd_def finfun_default_update_const)