new type for finite maps; use it in HOL-Probability
authorLars Hupel <lars.hupel@mytum.de>
Thu Sep 15 22:41:05 2016 +0200 (2016-09-15)
changeset 63885a6cd18af8bf9
parent 63884 d588f684ccaf
child 63886 685fb01256af
child 63887 2d9c12eba726
new type for finite maps; use it in HOL-Probability
src/HOL/Library/Finite_Map.thy
src/HOL/Library/Library.thy
src/HOL/Probability/Fin_Map.thy
src/HOL/Probability/Projective_Limit.thy
src/HOL/ROOT
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Finite_Map.thy	Thu Sep 15 22:41:05 2016 +0200
     1.3 @@ -0,0 +1,837 @@
     1.4 +(*  Title:      HOL/Library/Finite_Map.thy
     1.5 +    Author:     Lars Hupel, TU M√ľnchen
     1.6 +*)
     1.7 +
     1.8 +section \<open>Type of finite maps defined as a subtype of maps\<close>
     1.9 +
    1.10 +theory Finite_Map
    1.11 +  imports FSet AList
    1.12 +begin
    1.13 +
    1.14 +subsection \<open>Auxiliary constants and lemmas over @{type map}\<close>
    1.15 +
    1.16 +context includes lifting_syntax begin
    1.17 +
    1.18 +abbreviation rel_map :: "('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'c) \<Rightarrow> bool" where
    1.19 +"rel_map f \<equiv> op = ===> rel_option f"
    1.20 +
    1.21 +lemma map_empty_transfer[transfer_rule]: "rel_map A Map.empty Map.empty"
    1.22 +by transfer_prover
    1.23 +
    1.24 +lemma ran_transfer[transfer_rule]: "(rel_map A ===> rel_set A) ran ran"
    1.25 +proof
    1.26 +  fix m n
    1.27 +  assume "rel_map A m n"
    1.28 +  show "rel_set A (ran m) (ran n)"
    1.29 +    proof (rule rel_setI)
    1.30 +      fix x
    1.31 +      assume "x \<in> ran m"
    1.32 +      then obtain a where "m a = Some x"
    1.33 +        unfolding ran_def by auto
    1.34 +
    1.35 +      have "rel_option A (m a) (n a)"
    1.36 +        using \<open>rel_map A m n\<close>
    1.37 +        by (auto dest: rel_funD)
    1.38 +      then obtain y where "n a = Some y" "A x y"
    1.39 +        unfolding \<open>m a = _\<close>
    1.40 +        by cases auto
    1.41 +      thus "\<exists>y \<in> ran n. A x y"
    1.42 +        unfolding ran_def by blast
    1.43 +    next
    1.44 +      fix y
    1.45 +      assume "y \<in> ran n"
    1.46 +      then obtain a where "n a = Some y"
    1.47 +        unfolding ran_def by auto
    1.48 +
    1.49 +      have "rel_option A (m a) (n a)"
    1.50 +        using \<open>rel_map A m n\<close>
    1.51 +        by (auto dest: rel_funD)
    1.52 +      then obtain x where "m a = Some x" "A x y"
    1.53 +        unfolding \<open>n a = _\<close>
    1.54 +        by cases auto
    1.55 +      thus "\<exists>x \<in> ran m. A x y"
    1.56 +        unfolding ran_def by blast
    1.57 +    qed
    1.58 +qed
    1.59 +
    1.60 +lemma ran_alt_def: "ran m = (the \<circ> m) ` dom m"
    1.61 +unfolding ran_def dom_def by force
    1.62 +
    1.63 +lemma dom_transfer[transfer_rule]: "(rel_map A ===> op =) dom dom"
    1.64 +proof
    1.65 +  fix m n
    1.66 +  assume "rel_map A m n"
    1.67 +  have "m a \<noteq> None \<longleftrightarrow> n a \<noteq> None" for a
    1.68 +    proof -
    1.69 +      from \<open>rel_map A m n\<close> have "rel_option A (m a) (n a)"
    1.70 +        unfolding rel_fun_def by auto
    1.71 +      thus ?thesis
    1.72 +        by cases auto
    1.73 +    qed
    1.74 +  thus "dom m = dom n"
    1.75 +    by auto
    1.76 +qed
    1.77 +
    1.78 +definition map_upd :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
    1.79 +"map_upd k v m = m(k \<mapsto> v)"
    1.80 +
    1.81 +lemma map_upd_transfer[transfer_rule]:
    1.82 +  "(op = ===> A ===> rel_map A ===> rel_map A) map_upd map_upd"
    1.83 +unfolding map_upd_def[abs_def]
    1.84 +by transfer_prover
    1.85 +
    1.86 +definition map_filter :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
    1.87 +"map_filter P m = (\<lambda>x. if P x then m x else None)"
    1.88 +
    1.89 +lemma map_filter_map_of[simp]: "map_filter P (map_of m) = map_of [(k, _) \<leftarrow> m. P k]"
    1.90 +proof
    1.91 +  fix x
    1.92 +  show "map_filter P (map_of m) x = map_of [(k, _) \<leftarrow> m. P k] x"
    1.93 +    by (induct m) (auto simp: map_filter_def)
    1.94 +qed
    1.95 +
    1.96 +lemma map_filter_transfer[transfer_rule]:
    1.97 +  "(op = ===> rel_map A ===> rel_map A) map_filter map_filter"
    1.98 +unfolding map_filter_def[abs_def]
    1.99 +by transfer_prover
   1.100 +
   1.101 +lemma map_filter_finite[intro]:
   1.102 +  assumes "finite (dom m)"
   1.103 +  shows "finite (dom (map_filter P m))"
   1.104 +proof -
   1.105 +  have "dom (map_filter P m) = Set.filter P (dom m)"
   1.106 +    unfolding map_filter_def Set.filter_def dom_def
   1.107 +    by auto
   1.108 +  thus ?thesis
   1.109 +    using assms
   1.110 +    by (simp add: Set.filter_def)
   1.111 +qed
   1.112 +
   1.113 +definition map_drop :: "'a \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
   1.114 +"map_drop a = map_filter (\<lambda>a'. a' \<noteq> a)"
   1.115 +
   1.116 +lemma map_drop_transfer[transfer_rule]:
   1.117 +  "(op = ===> rel_map A ===> rel_map A) map_drop map_drop"
   1.118 +unfolding map_drop_def[abs_def]
   1.119 +by transfer_prover
   1.120 +
   1.121 +definition map_drop_set :: "'a set \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
   1.122 +"map_drop_set A = map_filter (\<lambda>a. a \<notin> A)"
   1.123 +
   1.124 +lemma map_drop_set_transfer[transfer_rule]:
   1.125 +  "(op = ===> rel_map A ===> rel_map A) map_drop_set map_drop_set"
   1.126 +unfolding map_drop_set_def[abs_def]
   1.127 +by transfer_prover
   1.128 +
   1.129 +definition map_restrict_set :: "'a set \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
   1.130 +"map_restrict_set A = map_filter (\<lambda>a. a \<in> A)"
   1.131 +
   1.132 +lemma map_restrict_set_transfer[transfer_rule]:
   1.133 +  "(op = ===> rel_map A ===> rel_map A) map_restrict_set map_restrict_set"
   1.134 +unfolding map_restrict_set_def[abs_def]
   1.135 +by transfer_prover
   1.136 +
   1.137 +lemma map_add_transfer[transfer_rule]:
   1.138 +  "(rel_map A ===> rel_map A ===> rel_map A) op ++ op ++"
   1.139 +unfolding map_add_def[abs_def]
   1.140 +by transfer_prover
   1.141 +
   1.142 +definition map_pred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> bool" where
   1.143 +"map_pred P m \<longleftrightarrow> (\<forall>x. case m x of None \<Rightarrow> True | Some y \<Rightarrow> P x y)"
   1.144 +
   1.145 +lemma map_pred_transfer[transfer_rule]:
   1.146 +  "((op = ===> A ===> op =) ===> rel_map A ===> op =) map_pred map_pred"
   1.147 +unfolding map_pred_def[abs_def]
   1.148 +by transfer_prover
   1.149 +
   1.150 +definition rel_map_on_set :: "'a set \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'c) \<Rightarrow> bool" where
   1.151 +"rel_map_on_set S P = eq_onp (\<lambda>x. x \<in> S) ===> rel_option P"
   1.152 +  
   1.153 +lemma map_of_transfer[transfer_rule]:
   1.154 +  includes lifting_syntax
   1.155 +  shows "(list_all2 (rel_prod op = A) ===> rel_map A) map_of map_of"
   1.156 +unfolding map_of_def by transfer_prover
   1.157 +  
   1.158 +end
   1.159 +
   1.160 +
   1.161 +subsection \<open>Abstract characterisation\<close>
   1.162 +
   1.163 +typedef ('a, 'b) fmap = "{m. finite (dom m)} :: ('a \<rightharpoonup> 'b) set"
   1.164 +  morphisms fmlookup Abs_fmap
   1.165 +proof
   1.166 +  show "Map.empty \<in> {m. finite (dom m)}"
   1.167 +    by auto
   1.168 +qed
   1.169 +
   1.170 +setup_lifting type_definition_fmap
   1.171 +
   1.172 +lemma fmlookup_finite[intro, simp]: "finite (dom (fmlookup m))"
   1.173 +using fmap.fmlookup by auto
   1.174 +
   1.175 +lemma fmap_ext:
   1.176 +  assumes "\<And>x. fmlookup m x = fmlookup n x"
   1.177 +  shows "m = n"
   1.178 +using assms
   1.179 +by transfer' auto
   1.180 +
   1.181 +
   1.182 +subsection \<open>Operations\<close>
   1.183 +
   1.184 +context
   1.185 +  includes fset.lifting
   1.186 +begin
   1.187 +
   1.188 +lift_definition fmran :: "('a, 'b) fmap \<Rightarrow> 'b fset"
   1.189 +  is ran
   1.190 +  parametric ran_transfer
   1.191 +unfolding ran_alt_def by auto
   1.192 +
   1.193 +lemma fmranI: "fmlookup m x = Some y \<Longrightarrow> y |\<in>| fmran m" by transfer' (auto simp: ran_def)
   1.194 +
   1.195 +lift_definition fmdom :: "('a, 'b) fmap \<Rightarrow> 'a fset"
   1.196 +  is dom
   1.197 +  parametric dom_transfer
   1.198 +.
   1.199 +
   1.200 +lemma fmdom_notI: "fmlookup m x = None \<Longrightarrow> x |\<notin>| fmdom m" by transfer' auto
   1.201 +lemma fmdomI: "fmlookup m x = Some y \<Longrightarrow> x |\<in>| fmdom m" by transfer' auto
   1.202 +
   1.203 +lift_definition fmdom' :: "('a, 'b) fmap \<Rightarrow> 'a set"
   1.204 +  is dom
   1.205 +  parametric dom_transfer
   1.206 +.
   1.207 +
   1.208 +lemma fmdom'_notI: "fmlookup m x = None \<Longrightarrow> x \<notin> fmdom' m" by transfer' auto
   1.209 +lemma fmdom'I: "fmlookup m x = Some y \<Longrightarrow> x \<in> fmdom' m" by transfer' auto
   1.210 +
   1.211 +lemma fmdom'_alt_def: "fmdom' = fset \<circ> fmdom"
   1.212 +by transfer' force
   1.213 +
   1.214 +lemma fmlookup_dom_iff: "x |\<in>| fmdom m \<longleftrightarrow> (\<exists>a. fmlookup m x = Some a)"
   1.215 +by transfer' auto
   1.216 +
   1.217 +lift_definition fmempty :: "('a, 'b) fmap"
   1.218 +  is Map.empty
   1.219 +  parametric map_empty_transfer
   1.220 +by simp
   1.221 +
   1.222 +lemma fmempty_lookup[simp]: "fmlookup fmempty x = None"
   1.223 +by transfer' simp
   1.224 +
   1.225 +lemma fmdom_empty[simp]: "fmdom fmempty = {||}" by transfer' simp
   1.226 +lemma fmdom'_empty[simp]: "fmdom' fmempty = {}" by transfer' simp
   1.227 +
   1.228 +lift_definition fmupd :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
   1.229 +  is map_upd
   1.230 +  parametric map_upd_transfer
   1.231 +unfolding map_upd_def[abs_def]
   1.232 +by simp
   1.233 +
   1.234 +lemma fmupd_lookup[simp]: "fmlookup (fmupd a b m) a' = (if a = a' then Some b else fmlookup m a')"
   1.235 +by transfer' (auto simp: map_upd_def)
   1.236 +
   1.237 +lemma fmdom_fmupd[simp]: "fmdom (fmupd a b m) = finsert a (fmdom m)" by transfer (simp add: map_upd_def)
   1.238 +lemma fmdom'_fmupd[simp]: "fmdom' (fmupd a b m) = insert a (fmdom' m)" by transfer (simp add: map_upd_def)
   1.239 +
   1.240 +lift_definition fmfilter :: "('a \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
   1.241 +  is map_filter
   1.242 +  parametric map_filter_transfer
   1.243 +by auto
   1.244 +
   1.245 +lemma fmdom_filter[simp]: "fmdom (fmfilter P m) = ffilter P (fmdom m)"
   1.246 +by transfer' (auto simp: map_filter_def Set.filter_def split: if_splits)
   1.247 +
   1.248 +lemma fmdom'_filter[simp]: "fmdom' (fmfilter P m) = Set.filter P (fmdom' m)"
   1.249 +by transfer' (auto simp: map_filter_def Set.filter_def split: if_splits)
   1.250 +
   1.251 +lemma fmlookup_filter[simp]: "fmlookup (fmfilter P m) x = (if P x then fmlookup m x else None)"
   1.252 +by transfer' (auto simp: map_filter_def)
   1.253 +
   1.254 +lemma fmfilter_empty[simp]: "fmfilter P fmempty = fmempty"
   1.255 +by transfer' (auto simp: map_filter_def)
   1.256 +
   1.257 +lemma fmfilter_true[simp]: "(\<And>x. x |\<in>| fmdom m \<Longrightarrow> P x) \<Longrightarrow> fmfilter P m = m"
   1.258 +apply transfer'
   1.259 +apply (rule ext)
   1.260 +apply (auto simp: map_filter_def)
   1.261 +apply (case_tac "m x")
   1.262 +apply simp
   1.263 +apply simp
   1.264 +apply (drule_tac m = m in domI)
   1.265 +apply auto
   1.266 +done
   1.267 +
   1.268 +lemma fmfilter_false[simp]: "(\<And>x. x |\<in>| fmdom m \<Longrightarrow> \<not> P x) \<Longrightarrow> fmfilter P m = fmempty"
   1.269 +apply transfer'
   1.270 +apply (rule ext)
   1.271 +apply (auto simp: map_filter_def)
   1.272 +done
   1.273 +
   1.274 +lemma fmfilter_comp[simp]: "fmfilter P (fmfilter Q m) = fmfilter (\<lambda>x. P x \<and> Q x) m"
   1.275 +by transfer' (auto simp: map_filter_def)
   1.276 +
   1.277 +lemma fmfilter_comm: "fmfilter P (fmfilter Q m) = fmfilter Q (fmfilter P m)"
   1.278 +unfolding fmfilter_comp by meson
   1.279 +
   1.280 +lemma fmfilter_cong[cong]:
   1.281 +  assumes "\<And>x. x |\<in>| fmdom m \<Longrightarrow> P x = Q x"
   1.282 +  shows "fmfilter P m = fmfilter Q m"
   1.283 +using assms
   1.284 +apply transfer'
   1.285 +apply (rule ext)
   1.286 +apply (auto simp: map_filter_def split: if_splits)
   1.287 +apply (case_tac "m x")
   1.288 +apply simp
   1.289 +apply simp
   1.290 +apply (drule_tac m = m in domI)
   1.291 +apply auto
   1.292 +done
   1.293 +
   1.294 +lemma fmfilter_cong'[fundef_cong]:
   1.295 +  assumes "\<And>x. x \<in> fmdom' m \<Longrightarrow> P x = Q x"
   1.296 +  shows "fmfilter P m = fmfilter Q m"
   1.297 +apply (rule fmfilter_cong)
   1.298 +using assms
   1.299 +unfolding fmdom'_alt_def fmember.rep_eq
   1.300 +by auto
   1.301 +
   1.302 +lemma fmfilter_upd[simp]: "fmfilter P (fmupd x y m) = (if P x then fmupd x y (fmfilter P m) else fmfilter P m)"
   1.303 +by transfer' (auto simp: map_upd_def map_filter_def)
   1.304 +
   1.305 +lift_definition fmdrop :: "'a \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
   1.306 +  is map_drop
   1.307 +  parametric map_drop_transfer
   1.308 +unfolding map_drop_def by auto
   1.309 +
   1.310 +lemma fmdrop_lookup[simp]: "fmlookup (fmdrop a m) a = None"
   1.311 +by transfer' (auto simp: map_drop_def map_filter_def)
   1.312 +
   1.313 +lift_definition fmdrop_set :: "'a set \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
   1.314 +  is map_drop_set
   1.315 +  parametric map_drop_set_transfer
   1.316 +unfolding map_drop_set_def by auto
   1.317 +
   1.318 +lift_definition fmdrop_fset :: "'a fset \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
   1.319 +  is map_drop_set
   1.320 +  parametric map_drop_set_transfer
   1.321 +unfolding map_drop_set_def by auto
   1.322 +
   1.323 +lift_definition fmrestrict_set :: "'a set \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
   1.324 +  is map_restrict_set
   1.325 +  parametric map_restrict_set_transfer
   1.326 +unfolding map_restrict_set_def by auto
   1.327 +
   1.328 +lemma fmrestrict_set_dom[simp]: "fmrestrict_set (fmdom' m) m = m"
   1.329 +apply transfer'
   1.330 +apply (auto simp: map_restrict_set_def map_filter_def)
   1.331 +apply (rule ext)
   1.332 +apply (auto split: if_splits)
   1.333 +by (metis option.collapse)
   1.334 +
   1.335 +lift_definition fmrestrict_fset :: "'a fset \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
   1.336 +  is map_restrict_set
   1.337 +  parametric map_restrict_set_transfer
   1.338 +unfolding map_restrict_set_def by auto
   1.339 +
   1.340 +lemma fmrestrict_fset_dom[simp]: "fmrestrict_fset (fmdom m) m = m"
   1.341 +apply transfer'
   1.342 +apply (auto simp: map_restrict_set_def map_filter_def)
   1.343 +apply (rule ext)
   1.344 +apply (auto split: if_splits)
   1.345 +by (metis option.collapse)
   1.346 +
   1.347 +lemma fmfilter_alt_defs:
   1.348 +  "fmdrop a = fmfilter (\<lambda>a'. a' \<noteq> a)"
   1.349 +  "fmdrop_set A = fmfilter (\<lambda>a. a \<notin> A)"
   1.350 +  "fmdrop_fset B = fmfilter (\<lambda>a. a |\<notin>| B)"
   1.351 +  "fmrestrict_set A = fmfilter (\<lambda>a. a \<in> A)"
   1.352 +  "fmrestrict_fset B = fmfilter (\<lambda>a. a |\<in>| B)"
   1.353 +by (transfer'; simp add: map_drop_def map_drop_set_def map_restrict_set_def)+
   1.354 +
   1.355 +lemma fmdom_drop[simp]: "fmdom (fmdrop a m) = fmdom m - {|a|}" unfolding fmfilter_alt_defs by auto
   1.356 +lemma fmdom'_drop[simp]: "fmdom' (fmdrop a m) = fmdom' m - {a}" unfolding fmfilter_alt_defs by auto
   1.357 +lemma fmdom'_drop_set[simp]: "fmdom' (fmdrop_set A m) = fmdom' m - A" unfolding fmfilter_alt_defs by auto
   1.358 +lemma fmdom_drop_fset[simp]: "fmdom (fmdrop_fset A m) = fmdom m - A" unfolding fmfilter_alt_defs by auto
   1.359 +lemma fmdom'_restrict_set: "fmdom' (fmrestrict_set A m) \<subseteq> A" unfolding fmfilter_alt_defs by auto
   1.360 +lemma fmdom_restrict_fset: "fmdom (fmrestrict_fset A m) |\<subseteq>| A" unfolding fmfilter_alt_defs by auto
   1.361 +
   1.362 +lemma fmdom'_drop_fset[simp]: "fmdom' (fmdrop_fset A m) = fmdom' m - fset A"
   1.363 +unfolding fmfilter_alt_defs by transfer' (auto simp: map_filter_def split: if_splits)
   1.364 +
   1.365 +lemma fmdom'_restrict_fset: "fmdom' (fmrestrict_fset A m) \<subseteq> fset A"
   1.366 +unfolding fmfilter_alt_defs by transfer' (auto simp: map_filter_def)
   1.367 +
   1.368 +lemma fmlookup_drop[simp]:
   1.369 +  "fmlookup (fmdrop a m) x = (if x \<noteq> a then fmlookup m x else None)"
   1.370 +unfolding fmfilter_alt_defs by simp
   1.371 +
   1.372 +lemma fmlookup_drop_set[simp]:
   1.373 +  "fmlookup (fmdrop_set A m) x = (if x \<notin> A then fmlookup m x else None)"
   1.374 +unfolding fmfilter_alt_defs by simp
   1.375 +
   1.376 +lemma fmlookup_drop_fset[simp]:
   1.377 +  "fmlookup (fmdrop_fset A m) x = (if x |\<notin>| A then fmlookup m x else None)"
   1.378 +unfolding fmfilter_alt_defs by simp
   1.379 +
   1.380 +lemma fmlookup_restrict_set[simp]:
   1.381 +  "fmlookup (fmrestrict_set A m) x = (if x \<in> A then fmlookup m x else None)"
   1.382 +unfolding fmfilter_alt_defs by simp
   1.383 +
   1.384 +lemma fmlookup_restrict_fset[simp]:
   1.385 +  "fmlookup (fmrestrict_fset A m) x = (if x |\<in>| A then fmlookup m x else None)"
   1.386 +unfolding fmfilter_alt_defs by simp
   1.387 +
   1.388 +lemma fmdrop_empty[simp]: "fmdrop a fmempty = fmempty"
   1.389 +  unfolding fmfilter_alt_defs by simp
   1.390 +
   1.391 +lemma fmdrop_set_empty[simp]: "fmdrop_set A fmempty = fmempty"
   1.392 +  unfolding fmfilter_alt_defs by simp
   1.393 +
   1.394 +lemma fmdrop_fset_empty[simp]: "fmdrop_fset A fmempty = fmempty"
   1.395 +  unfolding fmfilter_alt_defs by simp
   1.396 +
   1.397 +lemma fmrestrict_set_empty[simp]: "fmrestrict_set A fmempty = fmempty"
   1.398 +  unfolding fmfilter_alt_defs by simp
   1.399 +
   1.400 +lemma fmrestrict_fset_empty[simp]: "fmrestrict_fset A fmempty = fmempty"
   1.401 +  unfolding fmfilter_alt_defs by simp
   1.402 +
   1.403 +lemma fmdrop_set_single[simp]: "fmdrop_set {a} m = fmdrop a m"
   1.404 +  unfolding fmfilter_alt_defs by simp
   1.405 +
   1.406 +lemma fmdrop_fset_single[simp]: "fmdrop_fset {|a|} m = fmdrop a m"
   1.407 +  unfolding fmfilter_alt_defs by simp
   1.408 +
   1.409 +lemma fmrestrict_set_null[simp]: "fmrestrict_set {} m = fmempty"
   1.410 +  unfolding fmfilter_alt_defs by simp
   1.411 +
   1.412 +lemma fmrestrict_fset_null[simp]: "fmrestrict_fset {||} m = fmempty"
   1.413 +  unfolding fmfilter_alt_defs by simp
   1.414 +
   1.415 +lemma fmdrop_comm: "fmdrop a (fmdrop b m) = fmdrop b (fmdrop a m)"
   1.416 +unfolding fmfilter_alt_defs by (rule fmfilter_comm)
   1.417 +
   1.418 +lemma fmdrop_fmupd[simp]: "fmdrop x (fmupd x y m) = m"
   1.419 +oops
   1.420 +
   1.421 +lift_definition fmadd :: "('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap" (infixl "++\<^sub>f" 100)
   1.422 +  is map_add
   1.423 +  parametric map_add_transfer
   1.424 +by simp
   1.425 +
   1.426 +lemma fmdom_add[simp]: "fmdom (m ++\<^sub>f n) = fmdom m |\<union>| fmdom n" by transfer' auto
   1.427 +lemma fmdom'_add[simp]: "fmdom' (m ++\<^sub>f n) = fmdom' m \<union> fmdom' n" by transfer' auto
   1.428 +
   1.429 +lemma fmadd_drop_left_dom: "fmdrop_fset (fmdom n) m ++\<^sub>f n = m ++\<^sub>f n"
   1.430 +apply transfer'
   1.431 +unfolding map_add_def dom_def map_drop_set_def map_filter_def
   1.432 +by (rule ext) auto
   1.433 +
   1.434 +lemma fmadd_restrict_right_dom: "fmrestrict_fset (fmdom n) (m ++\<^sub>f n) = n"
   1.435 +apply transfer'
   1.436 +unfolding map_add_def dom_def map_restrict_set_def map_filter_def
   1.437 +by (rule ext) auto
   1.438 +
   1.439 +lemma fmfilter_add_distrib[simp]: "fmfilter P (m ++\<^sub>f n) = fmfilter P m ++\<^sub>f fmfilter P n"
   1.440 +by transfer' (auto simp: map_filter_def map_add_def)
   1.441 +
   1.442 +lemma fmdrop_add_distrib[simp]: "fmdrop a (m ++\<^sub>f n) = fmdrop a m ++\<^sub>f fmdrop a n"
   1.443 +  unfolding fmfilter_alt_defs by simp
   1.444 +
   1.445 +lemma fmdrop_set_add_distrib[simp]: "fmdrop_set A (m ++\<^sub>f n) = fmdrop_set A m ++\<^sub>f fmdrop_set A n"
   1.446 +  unfolding fmfilter_alt_defs by simp
   1.447 +
   1.448 +lemma fmdrop_fset_add_distrib[simp]: "fmdrop_fset A (m ++\<^sub>f n) = fmdrop_fset A m ++\<^sub>f fmdrop_fset A n"
   1.449 +  unfolding fmfilter_alt_defs by simp
   1.450 +
   1.451 +lemma fmrestrict_set_add_distrib[simp]:
   1.452 +  "fmrestrict_set A (m ++\<^sub>f n) = fmrestrict_set A m ++\<^sub>f fmrestrict_set A n"
   1.453 +  unfolding fmfilter_alt_defs by simp
   1.454 +
   1.455 +lemma fmrestrict_fset_add_distrib[simp]:
   1.456 +  "fmrestrict_fset A (m ++\<^sub>f n) = fmrestrict_fset A m ++\<^sub>f fmrestrict_fset A n"
   1.457 +  unfolding fmfilter_alt_defs by simp
   1.458 +
   1.459 +lemma fmadd_empty[simp]: "fmempty ++\<^sub>f m = m" "m ++\<^sub>f fmempty = m"
   1.460 +by (transfer'; auto)+
   1.461 +
   1.462 +lemma fmadd_idempotent[simp]: "m ++\<^sub>f m = m"
   1.463 +by transfer' (auto simp: map_add_def split: option.splits)
   1.464 +
   1.465 +lemma fmadd_assoc[simp]: "m ++\<^sub>f (n ++\<^sub>f p) = m ++\<^sub>f n ++\<^sub>f p"
   1.466 +by transfer' simp
   1.467 +
   1.468 +lemma fmlookup_add[simp]:
   1.469 +  "fmlookup (m ++\<^sub>f n) x = (if x |\<in>| fmdom n then fmlookup n x else fmlookup m x)"
   1.470 +  by transfer' (auto simp: map_add_def split: option.splits)
   1.471 +
   1.472 +lift_definition fmpred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> bool"
   1.473 +  is map_pred
   1.474 +  parametric map_pred_transfer
   1.475 +.
   1.476 +
   1.477 +lemma fmpredI[intro]:
   1.478 +  assumes "\<And>x y. fmlookup m x = Some y \<Longrightarrow> P x y"
   1.479 +  shows "fmpred P m"
   1.480 +using assms
   1.481 +by transfer' (auto simp: map_pred_def split: option.splits)
   1.482 +
   1.483 +lemma fmpredD[dest]: "fmpred P m \<Longrightarrow> fmlookup m x = Some y \<Longrightarrow> P x y" 
   1.484 +by transfer' (auto simp: map_pred_def split: option.split_asm)
   1.485 +
   1.486 +lemma fmpred_iff: "fmpred P m \<longleftrightarrow> (\<forall>x y. fmlookup m x = Some y \<longrightarrow> P x y)"
   1.487 +by auto
   1.488 +
   1.489 +lemma fmpred_alt_def: "fmpred P m \<longleftrightarrow> fBall (fmdom m) (\<lambda>x. P x (the (fmlookup m x)))"
   1.490 +unfolding fmpred_iff
   1.491 +apply auto
   1.492 +apply (subst (asm) fmlookup_dom_iff)
   1.493 +apply simp
   1.494 +apply (erule_tac x = x in fBallE)
   1.495 +apply simp
   1.496 +by (simp add: fmlookup_dom_iff)
   1.497 +
   1.498 +lemma fmpred_empty[intro!, simp]: "fmpred P fmempty"
   1.499 +by auto
   1.500 +
   1.501 +lemma fmpred_upd[intro]: "fmpred P m \<Longrightarrow> P x y \<Longrightarrow> fmpred P (fmupd x y m)"
   1.502 +by transfer' (auto simp: map_pred_def map_upd_def)
   1.503 +
   1.504 +lemma fmpred_updD[dest]: "fmpred P (fmupd x y m) \<Longrightarrow> P x y"
   1.505 +by auto
   1.506 +
   1.507 +lemma fmpred_add[intro]: "fmpred P m \<Longrightarrow> fmpred P n \<Longrightarrow> fmpred P (m ++\<^sub>f n)"
   1.508 +by transfer' (auto simp: map_pred_def map_add_def split: option.splits)
   1.509 +
   1.510 +lemma fmpred_filter[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmfilter Q m)"
   1.511 +by transfer' (auto simp: map_pred_def map_filter_def)
   1.512 +
   1.513 +lemma fmpred_drop[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop a m)"
   1.514 +  by (auto simp: fmfilter_alt_defs)
   1.515 +
   1.516 +lemma fmpred_drop_set[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop_set A m)"
   1.517 +  by (auto simp: fmfilter_alt_defs)
   1.518 +
   1.519 +lemma fmpred_drop_fset[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop_fset A m)"
   1.520 +  by (auto simp: fmfilter_alt_defs)
   1.521 +
   1.522 +lemma fmpred_restrict_set[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmrestrict_set A m)"
   1.523 +  by (auto simp: fmfilter_alt_defs)
   1.524 +
   1.525 +lemma fmpred_restrict_fset[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmrestrict_fset A m)"
   1.526 +  by (auto simp: fmfilter_alt_defs)
   1.527 +
   1.528 +lemma fmpred_cases[consumes 1]:
   1.529 +  assumes "fmpred P m"
   1.530 +  obtains (none) "fmlookup m x = None" | (some) y where "fmlookup m x = Some y" "P x y"
   1.531 +using assms by auto
   1.532 +
   1.533 +lift_definition fmsubset :: "('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap \<Rightarrow> bool" (infix "\<subseteq>\<^sub>f" 50)
   1.534 +  is map_le
   1.535 +.
   1.536 +
   1.537 +lemma fmsubset_alt_def: "m \<subseteq>\<^sub>f n \<longleftrightarrow> fmpred (\<lambda>k v. fmlookup n k = Some v) m"
   1.538 +by transfer' (auto simp: map_pred_def map_le_def dom_def split: option.splits)
   1.539 +
   1.540 +lemma fmsubset_pred: "fmpred P m \<Longrightarrow> n \<subseteq>\<^sub>f m \<Longrightarrow> fmpred P n"
   1.541 +unfolding fmsubset_alt_def fmpred_iff
   1.542 +by auto
   1.543 +
   1.544 +lemma fmsubset_filter_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmfilter P m \<subseteq>\<^sub>f fmfilter P n"
   1.545 +unfolding fmsubset_alt_def fmpred_iff
   1.546 +by auto
   1.547 +
   1.548 +lemma fmsubset_drop_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmdrop a m \<subseteq>\<^sub>f fmdrop a n"
   1.549 +unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
   1.550 +
   1.551 +lemma fmsubset_drop_set_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmdrop_set A m \<subseteq>\<^sub>f fmdrop_set A n"
   1.552 +unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
   1.553 +
   1.554 +lemma fmsubset_drop_fset_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmdrop_fset A m \<subseteq>\<^sub>f fmdrop_fset A n"
   1.555 +unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
   1.556 +
   1.557 +lemma fmsubset_restrict_set_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmrestrict_set A m \<subseteq>\<^sub>f fmrestrict_set A n"
   1.558 +unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
   1.559 +
   1.560 +lemma fmsubset_restrict_fset_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmrestrict_fset A m \<subseteq>\<^sub>f fmrestrict_fset A n"
   1.561 +unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
   1.562 +
   1.563 +lift_definition fmap_of_list :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) fmap"
   1.564 +  is map_of
   1.565 +  parametric map_of_transfer
   1.566 +by (rule finite_dom_map_of)
   1.567 +
   1.568 +lemma fmap_of_list_simps[simp]:
   1.569 +  "fmap_of_list [] = fmempty"
   1.570 +  "fmap_of_list ((k, v) # kvs) = fmupd k v (fmap_of_list kvs)"
   1.571 +by (transfer, simp add: map_upd_def)+
   1.572 +
   1.573 +lemma fmap_of_list_app[simp]: "fmap_of_list (xs @ ys) = fmap_of_list ys ++\<^sub>f fmap_of_list xs"
   1.574 +by transfer' simp
   1.575 +
   1.576 +lemma fmupd_alt_def: "fmupd k v m = m ++\<^sub>f fmap_of_list [(k, v)]"
   1.577 +by transfer' (auto simp: map_upd_def)
   1.578 +
   1.579 +lemma fmpred_of_list[intro]:
   1.580 +  assumes "\<And>k v. (k, v) \<in> set xs \<Longrightarrow> P k v"
   1.581 +  shows "fmpred P (fmap_of_list xs)"
   1.582 +using assms
   1.583 +by (induction xs) (transfer'; auto simp: map_pred_def)+
   1.584 +
   1.585 +lemma fmap_of_list_SomeD: "fmlookup (fmap_of_list xs) k = Some v \<Longrightarrow> (k, v) \<in> set xs"
   1.586 +by transfer' (auto dest: map_of_SomeD)
   1.587 +
   1.588 +lift_definition fmrel_on_set :: "'a set \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'c) fmap \<Rightarrow> bool"
   1.589 +  is rel_map_on_set
   1.590 +.
   1.591 +
   1.592 +lift_definition fmrel_on_fset :: "'a fset \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'c) fmap \<Rightarrow> bool"
   1.593 +  is rel_map_on_set
   1.594 +.
   1.595 +
   1.596 +lemma fmrel_on_fset_alt_def: "fmrel_on_fset S P m n \<longleftrightarrow> fBall S (\<lambda>x. rel_option P (fmlookup m x) (fmlookup n x))"
   1.597 +by transfer' (auto simp: rel_map_on_set_def eq_onp_def rel_fun_def)
   1.598 +
   1.599 +lemma rel_map_on_fsetI[intro]:
   1.600 +  assumes "\<And>x. x |\<in>| S \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
   1.601 +  shows "fmrel_on_fset S P m n"
   1.602 +using assms
   1.603 +unfolding fmrel_on_fset_alt_def by auto
   1.604 +
   1.605 +lemma fmrel_on_fset_mono[mono]: "R \<le> Q \<Longrightarrow> fmrel_on_fset S R \<le> fmrel_on_fset S Q"
   1.606 +unfolding fmrel_on_fset_alt_def[abs_def]
   1.607 +apply (intro le_funI fBall_mono)
   1.608 +using option.rel_mono by auto
   1.609 +
   1.610 +lemma fmrel_on_fsetD: "x |\<in>| S \<Longrightarrow> fmrel_on_fset S P m n \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
   1.611 +unfolding fmrel_on_fset_alt_def
   1.612 +by auto
   1.613 +
   1.614 +lemma fmrel_on_fsubset: "fmrel_on_fset S R m n \<Longrightarrow> T |\<subseteq>| S \<Longrightarrow> fmrel_on_fset T R m n"
   1.615 +unfolding fmrel_on_fset_alt_def
   1.616 +by auto
   1.617 +
   1.618 +end
   1.619 +
   1.620 +
   1.621 +subsection \<open>BNF setup\<close>
   1.622 +
   1.623 +lift_bnf ('a, fmran': 'b) fmap [wits: Map.empty]
   1.624 +  for map: fmmap
   1.625 +      rel: fmrel
   1.626 +  by auto
   1.627 +
   1.628 +context includes lifting_syntax begin
   1.629 +
   1.630 +lemma fmmap_transfer[transfer_rule]:
   1.631 +  "(op = ===> pcr_fmap op = op = ===> pcr_fmap op = op =) (\<lambda>f. op \<circ> (map_option f)) fmmap"
   1.632 +apply (tactic \<open>Local_Defs.unfold_tac @{context} [BNF_Def.bnf_of @{context} @{type_name fmap} |> the |> BNF_Def.map_def_of_bnf]\<close>)
   1.633 +apply (rule rel_funI ext)+
   1.634 +apply (auto simp: fmap.Abs_fmap_inverse fmap.pcr_cr_eq cr_fmap_def)
   1.635 +done
   1.636 +
   1.637 +lemma fmran'_transfer[transfer_rule]:
   1.638 +  "(pcr_fmap op = op = ===> op =) (\<lambda>x. UNION (range x) set_option) fmran'"
   1.639 +apply (tactic \<open>Local_Defs.unfold_tac @{context} (BNF_Def.bnf_of @{context} @{type_name fmap} |> the |> BNF_Def.set_defs_of_bnf)\<close>)
   1.640 +unfolding fmap.pcr_cr_eq cr_fmap_def
   1.641 +by fastforce
   1.642 +
   1.643 +lemma fmrel_transfer[transfer_rule]:
   1.644 +  "(op = ===> pcr_fmap op = op = ===> pcr_fmap op = op = ===> op =) rel_map fmrel"
   1.645 +apply (tactic \<open>Local_Defs.unfold_tac @{context} [BNF_Def.bnf_of @{context} @{type_name fmap} |> the |> BNF_Def.rel_def_of_bnf]\<close>)
   1.646 +unfolding fmap.pcr_cr_eq cr_fmap_def vimage2p_def
   1.647 +  by fastforce
   1.648 +
   1.649 +end
   1.650 +
   1.651 +
   1.652 +lemma fmran'_alt_def: "fmran' = fset \<circ> fmran"
   1.653 +including fset.lifting
   1.654 +by transfer' (auto simp: ran_def fun_eq_iff)
   1.655 +
   1.656 +lemma fmran'I: "fmlookup m x = Some y \<Longrightarrow> y \<in> fmran' m"
   1.657 +by transfer' auto
   1.658 +
   1.659 +lemma fmrel_iff: "fmrel R m n \<longleftrightarrow> (\<forall>x. rel_option R (fmlookup m x) (fmlookup n x))"
   1.660 +by transfer' (auto simp: rel_fun_def)
   1.661 +
   1.662 +lemma fmrelI[intro]:
   1.663 +  assumes "\<And>x. rel_option R (fmlookup m x) (fmlookup n x)"
   1.664 +  shows "fmrel R m n"
   1.665 +using assms
   1.666 +by transfer' auto
   1.667 +
   1.668 +lemma fmempty_transfer[simp, intro, transfer_rule]: "fmrel P fmempty fmempty"
   1.669 +by transfer auto
   1.670 +
   1.671 +lemma fmrel_upd[intro]: "fmrel P m n \<Longrightarrow> P x y \<Longrightarrow> fmrel P (fmupd k x m) (fmupd k y n)"
   1.672 +by transfer' (auto simp: map_upd_def rel_fun_def)
   1.673 +
   1.674 +lemma fmrelD[dest]: "fmrel P m n \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
   1.675 +by transfer' (auto simp: rel_fun_def)
   1.676 +
   1.677 +lemma fmrel_addI[intro]:
   1.678 +  assumes "fmrel P m n" "fmrel P a b"
   1.679 +  shows "fmrel P (m ++\<^sub>f a) (n ++\<^sub>f b)"
   1.680 +using assms
   1.681 +apply transfer'
   1.682 +apply (auto simp: rel_fun_def map_add_def)
   1.683 +by (metis option.case_eq_if option.collapse option.rel_sel)
   1.684 +
   1.685 +lemma fmrel_cases[consumes 1]:
   1.686 +  assumes "fmrel P m n"
   1.687 +  obtains (none) "fmlookup m x = None" "fmlookup n x = None"
   1.688 +        | (some) a b where "fmlookup m x = Some a" "fmlookup n x = Some b" "P a b"
   1.689 +proof -
   1.690 +  from assms have "rel_option P (fmlookup m x) (fmlookup n x)"
   1.691 +    by auto
   1.692 +  thus thesis
   1.693 +    using none some
   1.694 +    by (cases rule: option.rel_cases) auto
   1.695 +qed
   1.696 +
   1.697 +lemma fmrel_filter[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmfilter Q m) (fmfilter Q n)"
   1.698 +unfolding fmrel_iff by auto
   1.699 +
   1.700 +lemma fmrel_drop[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop a m) (fmdrop a n)"
   1.701 +  unfolding fmfilter_alt_defs by blast
   1.702 +
   1.703 +lemma fmrel_drop_set[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop_set A m) (fmdrop_set A n)"
   1.704 +  unfolding fmfilter_alt_defs by blast
   1.705 +
   1.706 +lemma fmrel_drop_fset[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop_fset A m) (fmdrop_fset A n)"
   1.707 +  unfolding fmfilter_alt_defs by blast
   1.708 +
   1.709 +lemma fmrel_restrict_set[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmrestrict_set A m) (fmrestrict_set A n)"
   1.710 +  unfolding fmfilter_alt_defs by blast
   1.711 +
   1.712 +lemma fmrel_restrict_fset[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmrestrict_fset A m) (fmrestrict_fset A n)"
   1.713 +  unfolding fmfilter_alt_defs by blast
   1.714 +
   1.715 +lemma pred_fmap_fmpred[simp]: "pred_fmap P = fmpred (\<lambda>_. P)"
   1.716 +unfolding fmap.pred_set fmran'_alt_def
   1.717 +including fset.lifting
   1.718 +apply transfer'
   1.719 +apply (rule ext)
   1.720 +apply (auto simp: map_pred_def ran_def split: option.splits dest: )
   1.721 +done
   1.722 +
   1.723 +lemma pred_fmap_id[simp]: "pred_fmap id (fmmap f m) \<longleftrightarrow> pred_fmap f m"
   1.724 +unfolding fmap.pred_set fmap.set_map
   1.725 +by simp
   1.726 +
   1.727 +lemma fmlookup_map[simp]: "fmlookup (fmmap f m) x = map_option f (fmlookup m x)"
   1.728 +apply (tactic \<open>Local_Defs.unfold_tac @{context} [BNF_Def.bnf_of @{context} @{type_name fmap} |> the |> BNF_Def.map_def_of_bnf]\<close>)
   1.729 +apply (auto simp: fmap.Abs_fmap_inverse)
   1.730 +done
   1.731 +
   1.732 +lemma fmpred_map[simp]: "fmpred P (fmmap f m) \<longleftrightarrow> fmpred (\<lambda>k v. P k (f v)) m"
   1.733 +unfolding fmpred_iff pred_fmap_def fmap.set_map
   1.734 +by auto
   1.735 +
   1.736 +lemma fmpred_id[simp]: "fmpred (\<lambda>_. id) (fmmap f m) \<longleftrightarrow> fmpred (\<lambda>_. f) m"
   1.737 +by simp
   1.738 +
   1.739 +lemma fmmap_add[simp]: "fmmap f (m ++\<^sub>f n) = fmmap f m ++\<^sub>f fmmap f n"
   1.740 +by transfer' (auto simp: map_add_def fun_eq_iff split: option.splits)
   1.741 +
   1.742 +lemma fmmap_empty[simp]: "fmmap f fmempty = fmempty"
   1.743 +by transfer auto
   1.744 +
   1.745 +lemma fmdom_map[simp]: "fmdom (fmmap f m) = fmdom m"
   1.746 +including fset.lifting
   1.747 +by transfer' simp
   1.748 +
   1.749 +lemma fmdom'_map[simp]: "fmdom' (fmmap f m) = fmdom' m"
   1.750 +by transfer' simp
   1.751 +
   1.752 +lemma fmfilter_fmmap[simp]: "fmfilter P (fmmap f m) = fmmap f (fmfilter P m)"
   1.753 +by transfer' (auto simp: map_filter_def)
   1.754 +
   1.755 +lemma fmdrop_fmmap[simp]: "fmdrop a (fmmap f m) = fmmap f (fmdrop a m)" unfolding fmfilter_alt_defs by simp
   1.756 +lemma fmdrop_set_fmmap[simp]: "fmdrop_set A (fmmap f m) = fmmap f (fmdrop_set A m)" unfolding fmfilter_alt_defs by simp
   1.757 +lemma fmdrop_fset_fmmap[simp]: "fmdrop_fset A (fmmap f m) = fmmap f (fmdrop_fset A m)" unfolding fmfilter_alt_defs by simp
   1.758 +lemma fmrestrict_set_fmmap[simp]: "fmrestrict_set A (fmmap f m) = fmmap f (fmrestrict_set A m)" unfolding fmfilter_alt_defs by simp
   1.759 +lemma fmrestrict_fset_fmmap[simp]: "fmrestrict_fset A (fmmap f m) = fmmap f (fmrestrict_fset A m)" unfolding fmfilter_alt_defs by simp
   1.760 +
   1.761 +lemma fmmap_subset[intro]: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmmap f m \<subseteq>\<^sub>f fmmap f n"
   1.762 +by transfer' (auto simp: map_le_def)
   1.763 +
   1.764 +
   1.765 +subsection \<open>Code setup\<close>
   1.766 +
   1.767 +instantiation fmap :: (type, equal) equal begin
   1.768 +
   1.769 +definition "equal_fmap \<equiv> fmrel HOL.equal"
   1.770 +
   1.771 +instance proof
   1.772 +  fix m n :: "('a, 'b) fmap"
   1.773 +  have "fmrel op = m n \<longleftrightarrow> (m = n)"
   1.774 +    by transfer' (simp add: option.rel_eq rel_fun_eq)
   1.775 +  thus "equal_class.equal m n \<longleftrightarrow> (m = n)"
   1.776 +    unfolding equal_fmap_def
   1.777 +    by (simp add: equal_eq[abs_def])
   1.778 +qed
   1.779 +
   1.780 +end
   1.781 +
   1.782 +lemma fBall_alt_def: "fBall S P \<longleftrightarrow> (\<forall>x. x |\<in>| S \<longrightarrow> P x)"
   1.783 +by force
   1.784 +
   1.785 +lemma fmrel_code:
   1.786 +  "fmrel R m n \<longleftrightarrow>
   1.787 +    fBall (fmdom m) (\<lambda>x. rel_option R (fmlookup m x) (fmlookup n x)) \<and>
   1.788 +    fBall (fmdom n) (\<lambda>x. rel_option R (fmlookup m x) (fmlookup n x))"
   1.789 +unfolding fmrel_iff fmlookup_dom_iff fBall_alt_def
   1.790 +by (metis option.collapse option.rel_sel)
   1.791 +
   1.792 +lemmas fmap_generic_code =
   1.793 +  fmrel_code
   1.794 +  fmran'_alt_def
   1.795 +  fmdom'_alt_def
   1.796 +  fmfilter_alt_defs
   1.797 +  pred_fmap_fmpred
   1.798 +  fmsubset_alt_def
   1.799 +  fmupd_alt_def
   1.800 +  fmrel_on_fset_alt_def
   1.801 +  fmpred_alt_def
   1.802 +
   1.803 +
   1.804 +code_datatype fmap_of_list
   1.805 +quickcheck_generator fmap constructors: fmap_of_list
   1.806 +
   1.807 +context includes fset.lifting begin
   1.808 +
   1.809 +lemma [code]: "fmlookup (fmap_of_list m) = map_of m"
   1.810 +by transfer simp
   1.811 +
   1.812 +lemma [code]: "fmempty = fmap_of_list []"
   1.813 +by transfer simp
   1.814 +
   1.815 +lemma [code]: "fmran (fmap_of_list m) = snd |`| fset_of_list (AList.clearjunk m)"
   1.816 +by transfer (auto simp: ran_map_of)
   1.817 +
   1.818 +lemma [code]: "fmdom (fmap_of_list m) = fst |`| fset_of_list m"
   1.819 +by transfer (auto simp: dom_map_of_conv_image_fst)
   1.820 +
   1.821 +lemma [code]: "fmfilter P (fmap_of_list m) = fmap_of_list (filter (\<lambda>(k, _). P k) m)"
   1.822 +by transfer' auto
   1.823 +
   1.824 +lemma [code]: "fmap_of_list m ++\<^sub>f fmap_of_list n = fmap_of_list (AList.merge m n)"
   1.825 +by transfer (simp add: merge_conv')
   1.826 +
   1.827 +lemma [code]: "fmmap f (fmap_of_list m) = fmap_of_list (map (apsnd f) m)"
   1.828 +apply transfer
   1.829 +apply (subst map_of_map[symmetric])
   1.830 +apply (auto simp: apsnd_def map_prod_def)
   1.831 +done
   1.832 +
   1.833 +end
   1.834 +
   1.835 +declare fmap_generic_code[code]
   1.836 +
   1.837 +lifting_update fmap.lifting
   1.838 +lifting_forget fmap.lifting
   1.839 +
   1.840 +end
   1.841 \ No newline at end of file
     2.1 --- a/src/HOL/Library/Library.thy	Thu Sep 15 19:31:17 2016 +0200
     2.2 +++ b/src/HOL/Library/Library.thy	Thu Sep 15 22:41:05 2016 +0200
     2.3 @@ -26,6 +26,7 @@
     2.4    Extended_Nonnegative_Real
     2.5    Extended_Real
     2.6    FinFun
     2.7 +  Finite_Map
     2.8    Float
     2.9    Formal_Power_Series
    2.10    Fraction_Field
     3.1 --- a/src/HOL/Probability/Fin_Map.thy	Thu Sep 15 19:31:17 2016 +0200
     3.2 +++ b/src/HOL/Probability/Fin_Map.thy	Thu Sep 15 22:41:05 2016 +0200
     3.3 @@ -5,29 +5,27 @@
     3.4  section \<open>Finite Maps\<close>
     3.5  
     3.6  theory Fin_Map
     3.7 -imports Finite_Product_Measure
     3.8 +  imports Finite_Product_Measure "~~/src/HOL/Library/Finite_Map"
     3.9  begin
    3.10  
    3.11 -text \<open>Auxiliary type that is instantiated to @{class polish_space}, needed for the proof of
    3.12 +text \<open>The @{type fmap} type can be instantiated to @{class polish_space}, needed for the proof of
    3.13    projective limit. @{const extensional} functions are used for the representation in order to
    3.14    stay close to the developments of (finite) products @{const Pi\<^sub>E} and their sigma-algebra
    3.15    @{const Pi\<^sub>M}.\<close>
    3.16  
    3.17 -typedef ('i, 'a) finmap ("(_ \<Rightarrow>\<^sub>F /_)" [22, 21] 21) =
    3.18 -  "{f::'i \<Rightarrow> 'a option. finite (dom f)}"
    3.19 -  by (auto intro!: exI[where x="\<lambda>_. None"])
    3.20 +type_notation fmap ("(_ \<Rightarrow>\<^sub>F /_)" [22, 21] 21)
    3.21  
    3.22 -setup_lifting type_definition_finmap
    3.23 +unbundle fmap.lifting
    3.24  
    3.25  
    3.26  subsection \<open>Domain and Application\<close>
    3.27  
    3.28 -lift_definition domain::"('i, 'a) finmap \<Rightarrow> 'i set" is dom .
    3.29 +lift_definition domain::"('i \<Rightarrow>\<^sub>F 'a) \<Rightarrow> 'i set" is dom .
    3.30  
    3.31  lemma finite_domain[simp, intro]: "finite (domain P)"
    3.32    by transfer simp
    3.33  
    3.34 -lift_definition proj :: "('i, 'a) finmap \<Rightarrow> 'i \<Rightarrow> 'a" ("'((_)')\<^sub>F" [0] 1000) is
    3.35 +lift_definition proj :: "('i \<Rightarrow>\<^sub>F 'a) \<Rightarrow> 'i \<Rightarrow> 'a" ("'((_)')\<^sub>F" [0] 1000) is
    3.36    "\<lambda>f x. if x \<in> dom f then the (f x) else undefined" .
    3.37  
    3.38  declare [[coercion proj]]
    3.39 @@ -48,7 +46,7 @@
    3.40  
    3.41  subsection \<open>Countable Finite Maps\<close>
    3.42  
    3.43 -instance finmap :: (countable, countable) countable
    3.44 +instance fmap :: (countable, countable) countable
    3.45  proof
    3.46    obtain mapper where mapper: "\<And>fm :: 'a \<Rightarrow>\<^sub>F 'b. set (mapper fm) = domain fm"
    3.47      by (metis finite_list[OF finite_domain])
    3.48 @@ -68,7 +66,7 @@
    3.49  
    3.50  subsection \<open>Constructor of Finite Maps\<close>
    3.51  
    3.52 -lift_definition finmap_of::"'i set \<Rightarrow> ('i \<Rightarrow> 'a) \<Rightarrow> ('i, 'a) finmap" is
    3.53 +lift_definition finmap_of::"'i set \<Rightarrow> ('i \<Rightarrow> 'a) \<Rightarrow> ('i \<Rightarrow>\<^sub>F 'a)" is
    3.54    "\<lambda>I f x. if x \<in> I \<and> finite I then Some (f x) else None"
    3.55    by (simp add: dom_def)
    3.56  
    3.57 @@ -156,17 +154,17 @@
    3.58  
    3.59  subsection \<open>Topological Space of Finite Maps\<close>
    3.60  
    3.61 -instantiation finmap :: (type, topological_space) topological_space
    3.62 +instantiation fmap :: (type, topological_space) topological_space
    3.63  begin
    3.64  
    3.65 -definition open_finmap :: "('a \<Rightarrow>\<^sub>F 'b) set \<Rightarrow> bool" where
    3.66 -   [code del]: "open_finmap = generate_topology {Pi' a b|a b. \<forall>i\<in>a. open (b i)}"
    3.67 +definition open_fmap :: "('a \<Rightarrow>\<^sub>F 'b) set \<Rightarrow> bool" where
    3.68 +   [code del]: "open_fmap = generate_topology {Pi' a b|a b. \<forall>i\<in>a. open (b i)}"
    3.69  
    3.70  lemma open_Pi'I: "(\<And>i. i \<in> I \<Longrightarrow> open (A i)) \<Longrightarrow> open (Pi' I A)"
    3.71 -  by (auto intro: generate_topology.Basis simp: open_finmap_def)
    3.72 +  by (auto intro: generate_topology.Basis simp: open_fmap_def)
    3.73  
    3.74  instance using topological_space_generate_topology
    3.75 -  by intro_classes (auto simp: open_finmap_def class.topological_space_def)
    3.76 +  by intro_classes (auto simp: open_fmap_def class.topological_space_def)
    3.77  
    3.78  end
    3.79  
    3.80 @@ -211,7 +209,7 @@
    3.81    shows "continuous_on s (\<lambda>x. (x)\<^sub>F i)"
    3.82    unfolding continuous_on_def by (safe intro!: tendsto_proj tendsto_ident_at)
    3.83  
    3.84 -instance finmap :: (type, first_countable_topology) first_countable_topology
    3.85 +instance fmap :: (type, first_countable_topology) first_countable_topology
    3.86  proof
    3.87    fix x::"'a\<Rightarrow>\<^sub>F'b"
    3.88    have "\<forall>i. \<exists>A. countable A \<and> (\<forall>a\<in>A. x i \<in> a) \<and> (\<forall>a\<in>A. open a) \<and>
    3.89 @@ -229,7 +227,7 @@
    3.90      show "countable ?A" using A by (simp add: countable_PiE)
    3.91    next
    3.92      fix S::"('a \<Rightarrow>\<^sub>F 'b) set" assume "open S" "x \<in> S"
    3.93 -    thus "\<exists>a\<in>?A. a \<subseteq> S" unfolding open_finmap_def
    3.94 +    thus "\<exists>a\<in>?A. a \<subseteq> S" unfolding open_fmap_def
    3.95      proof (induct rule: generate_topology.induct)
    3.96        case UNIV thus ?case by (auto simp add: ex_in_conv PiE_eq_empty_iff A_notempty)
    3.97      next
    3.98 @@ -266,29 +264,29 @@
    3.99  
   3.100  (* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
   3.101  
   3.102 -instantiation finmap :: (type, metric_space) dist
   3.103 +instantiation fmap :: (type, metric_space) dist
   3.104  begin
   3.105  
   3.106 -definition dist_finmap where
   3.107 +definition dist_fmap where
   3.108    "dist P Q = Max (range (\<lambda>i. dist ((P)\<^sub>F i) ((Q)\<^sub>F i))) + (if domain P = domain Q then 0 else 1)"
   3.109  
   3.110  instance ..
   3.111  end
   3.112  
   3.113 -instantiation finmap :: (type, metric_space) uniformity_dist
   3.114 +instantiation fmap :: (type, metric_space) uniformity_dist
   3.115  begin
   3.116  
   3.117  definition [code del]:
   3.118 -  "(uniformity :: (('a, 'b) finmap \<times> ('a, 'b) finmap) filter) =
   3.119 +  "(uniformity :: (('a, 'b) fmap \<times> ('a \<Rightarrow>\<^sub>F 'b)) filter) =
   3.120      (INF e:{0 <..}. principal {(x, y). dist x y < e})"
   3.121  
   3.122  instance
   3.123 -  by standard (rule uniformity_finmap_def)
   3.124 +  by standard (rule uniformity_fmap_def)
   3.125  end
   3.126  
   3.127 -declare uniformity_Abort[where 'a="('a, 'b::metric_space) finmap", code]
   3.128 +declare uniformity_Abort[where 'a="('a \<Rightarrow>\<^sub>F 'b::metric_space)", code]
   3.129  
   3.130 -instantiation finmap :: (type, metric_space) metric_space
   3.131 +instantiation fmap :: (type, metric_space) metric_space
   3.132  begin
   3.133  
   3.134  lemma finite_proj_image': "x \<notin> domain P \<Longrightarrow> finite ((P)\<^sub>F ` S)"
   3.135 @@ -308,14 +306,14 @@
   3.136  
   3.137  lemma dist_le_1_imp_domain_eq:
   3.138    shows "dist P Q < 1 \<Longrightarrow> domain P = domain Q"
   3.139 -  by (simp add: dist_finmap_def finite_proj_diag split: if_split_asm)
   3.140 +  by (simp add: dist_fmap_def finite_proj_diag split: if_split_asm)
   3.141  
   3.142  lemma dist_proj:
   3.143    shows "dist ((x)\<^sub>F i) ((y)\<^sub>F i) \<le> dist x y"
   3.144  proof -
   3.145    have "dist (x i) (y i) \<le> Max (range (\<lambda>i. dist (x i) (y i)))"
   3.146      by (simp add: Max_ge_iff finite_proj_diag)
   3.147 -  also have "\<dots> \<le> dist x y" by (simp add: dist_finmap_def)
   3.148 +  also have "\<dots> \<le> dist x y" by (simp add: dist_fmap_def)
   3.149    finally show ?thesis .
   3.150  qed
   3.151  
   3.152 @@ -326,7 +324,7 @@
   3.153    shows "dist P Q < e"
   3.154  proof -
   3.155    have "dist P Q = Max (range (\<lambda>i. dist (P i) (Q i)))"
   3.156 -    using assms by (simp add: dist_finmap_def finite_proj_diag)
   3.157 +    using assms by (simp add: dist_fmap_def finite_proj_diag)
   3.158    also have "\<dots> < e"
   3.159    proof (subst Max_less_iff, safe)
   3.160      fix i
   3.161 @@ -343,7 +341,7 @@
   3.162    proof
   3.163      assume "open S"
   3.164      thus ?od
   3.165 -      unfolding open_finmap_def
   3.166 +      unfolding open_fmap_def
   3.167      proof (induct rule: generate_topology.induct)
   3.168        case UNIV thus ?case by (auto intro: zero_less_one)
   3.169      next
   3.170 @@ -383,7 +381,7 @@
   3.171              show "domain y = a" using d s \<open>a \<noteq> {}\<close> by (auto simp: dist_le_1_imp_domain_eq a_dom)
   3.172              fix i assume i: "i \<in> a"
   3.173              hence "dist ((y)\<^sub>F i) ((x)\<^sub>F i) < es i" using d
   3.174 -              by (auto simp: dist_finmap_def \<open>a \<noteq> {}\<close> intro!: le_less_trans[OF dist_proj])
   3.175 +              by (auto simp: dist_fmap_def \<open>a \<noteq> {}\<close> intro!: le_less_trans[OF dist_proj])
   3.176              with i show "y i \<in> b i" by (rule in_b)
   3.177            qed
   3.178          next
   3.179 @@ -410,23 +408,23 @@
   3.180        moreover
   3.181        assume "x \<in> (\<Pi>' i\<in>domain y. ball (y i) (e y))"
   3.182        hence "dist x y < e y" using e_pos \<open>y \<in> S\<close>
   3.183 -        by (auto simp: dist_finmap_def Pi'_iff finite_proj_diag dist_commute)
   3.184 +        by (auto simp: dist_fmap_def Pi'_iff finite_proj_diag dist_commute)
   3.185        ultimately show "x \<in> S" by (rule e_in)
   3.186      qed
   3.187      also have "open \<dots>"
   3.188 -      unfolding open_finmap_def
   3.189 +      unfolding open_fmap_def
   3.190        by (intro generate_topology.UN) (auto intro: generate_topology.Basis)
   3.191      finally show "open S" .
   3.192    qed
   3.193    show "open S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
   3.194      unfolding * eventually_uniformity_metric
   3.195 -    by (simp del: split_paired_All add: dist_finmap_def dist_commute eq_commute)
   3.196 +    by (simp del: split_paired_All add: dist_fmap_def dist_commute eq_commute)
   3.197  next
   3.198    fix P Q::"'a \<Rightarrow>\<^sub>F 'b"
   3.199    have Max_eq_iff: "\<And>A m. finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> (Max A = m) = (m \<in> A \<and> (\<forall>a\<in>A. a \<le> m))"
   3.200      by (auto intro: Max_in Max_eqI)
   3.201    show "dist P Q = 0 \<longleftrightarrow> P = Q"
   3.202 -    by (auto simp: finmap_eq_iff dist_finmap_def Max_ge_iff finite_proj_diag Max_eq_iff
   3.203 +    by (auto simp: finmap_eq_iff dist_fmap_def Max_ge_iff finite_proj_diag Max_eq_iff
   3.204          add_nonneg_eq_0_iff
   3.205        intro!: Max_eqI image_eqI[where x=undefined])
   3.206  next
   3.207 @@ -435,14 +433,14 @@
   3.208    let ?dpq = "?dists P Q" and ?dpr = "?dists P R" and ?dqr = "?dists Q R"
   3.209    let ?dom = "\<lambda>P Q. (if domain P = domain Q then 0 else 1::real)"
   3.210    have "dist P Q = Max (range ?dpq) + ?dom P Q"
   3.211 -    by (simp add: dist_finmap_def)
   3.212 +    by (simp add: dist_fmap_def)
   3.213    also obtain t where "t \<in> range ?dpq" "t = Max (range ?dpq)" by (simp add: finite_proj_diag)
   3.214    then obtain i where "Max (range ?dpq) = ?dpq i" by auto
   3.215    also have "?dpq i \<le> ?dpr i + ?dqr i" by (rule dist_triangle2)
   3.216    also have "?dpr i \<le> Max (range ?dpr)" by (simp add: finite_proj_diag)
   3.217    also have "?dqr i \<le> Max (range ?dqr)" by (simp add: finite_proj_diag)
   3.218    also have "?dom P Q \<le> ?dom P R + ?dom Q R" by simp
   3.219 -  finally show "dist P Q \<le> dist P R + dist Q R" by (simp add: dist_finmap_def ac_simps)
   3.220 +  finally show "dist P Q \<le> dist P R + dist Q R" by (simp add: dist_fmap_def ac_simps)
   3.221  qed
   3.222  
   3.223  end
   3.224 @@ -468,10 +466,10 @@
   3.225      ultimately show ?case by eventually_elim auto
   3.226    qed simp
   3.227    thus "eventually (\<lambda>x. dist (f x) g < e) sequentially"
   3.228 -    by eventually_elim (auto simp add: dist_finmap_def finite_proj_diag ind_f \<open>0 < e\<close>)
   3.229 +    by eventually_elim (auto simp add: dist_fmap_def finite_proj_diag ind_f \<open>0 < e\<close>)
   3.230  qed
   3.231  
   3.232 -instance finmap :: (type, complete_space) complete_space
   3.233 +instance fmap :: (type, complete_space) complete_space
   3.234  proof
   3.235    fix P::"nat \<Rightarrow> 'a \<Rightarrow>\<^sub>F 'b"
   3.236    assume "Cauchy P"
   3.237 @@ -483,7 +481,7 @@
   3.238    define p where "p i n = P n i" for i n
   3.239    define q where "q i = lim (p i)" for i
   3.240    define Q where "Q = finmap_of d q"
   3.241 -  have q: "\<And>i. i \<in> d \<Longrightarrow> q i = Q i" by (auto simp add: Q_def Abs_finmap_inverse)
   3.242 +  have q: "\<And>i. i \<in> d \<Longrightarrow> q i = Q i" by (auto simp add: Q_def Abs_fmap_inverse)
   3.243    {
   3.244      fix i assume "i \<in> d"
   3.245      have "Cauchy (p i)" unfolding cauchy p_def
   3.246 @@ -520,7 +518,7 @@
   3.247      proof (safe intro!: exI[where x="N"])
   3.248        fix n assume "N \<le> n"
   3.249        hence dom: "domain (P n) = d" "domain Q = d" "domain (P n) = domain Q"
   3.250 -        using dim by (simp_all add: N_def Q_def dim_def Abs_finmap_inverse)
   3.251 +        using dim by (simp_all add: N_def Q_def dim_def Abs_fmap_inverse)
   3.252        show "dist (P n) Q < e"
   3.253        proof (rule dist_finmap_lessI[OF dom(3) \<open>0 < e\<close>])
   3.254          fix i
   3.255 @@ -537,7 +535,7 @@
   3.256  
   3.257  subsection \<open>Second Countable Space of Finite Maps\<close>
   3.258  
   3.259 -instantiation finmap :: (countable, second_countable_topology) second_countable_topology
   3.260 +instantiation fmap :: (countable, second_countable_topology) second_countable_topology
   3.261  begin
   3.262  
   3.263  definition basis_proj::"'b set set"
   3.264 @@ -590,7 +588,7 @@
   3.265    assume O': "open O'" "x \<in> O'"
   3.266    then obtain a where a:
   3.267      "x \<in> Pi' (domain x) a" "Pi' (domain x) a \<subseteq> O'" "\<And>i. i\<in>domain x \<Longrightarrow> open (a i)"
   3.268 -    unfolding open_finmap_def
   3.269 +    unfolding open_fmap_def
   3.270    proof (atomize_elim, induct rule: generate_topology.induct)
   3.271      case (Int a b)
   3.272      let ?p="\<lambda>a f. x \<in> Pi' (domain x) f \<and> Pi' (domain x) f \<subseteq> a \<and> (\<forall>i. i \<in> domain x \<longrightarrow> open (f i))"
   3.273 @@ -630,7 +628,7 @@
   3.274  
   3.275  subsection \<open>Polish Space of Finite Maps\<close>
   3.276  
   3.277 -instance finmap :: (countable, polish_space) polish_space proof qed
   3.278 +instance fmap :: (countable, polish_space) polish_space proof qed
   3.279  
   3.280  
   3.281  subsection \<open>Product Measurable Space of Finite Maps\<close>
     4.1 --- a/src/HOL/Probability/Projective_Limit.thy	Thu Sep 15 19:31:17 2016 +0200
     4.2 +++ b/src/HOL/Probability/Projective_Limit.thy	Thu Sep 15 22:41:05 2016 +0200
     4.3 @@ -455,8 +455,6 @@
     4.4  hide_const (open) PiF
     4.5  hide_const (open) Pi\<^sub>F
     4.6  hide_const (open) Pi'
     4.7 -hide_const (open) Abs_finmap
     4.8 -hide_const (open) Rep_finmap
     4.9  hide_const (open) finmap_of
    4.10  hide_const (open) proj
    4.11  hide_const (open) domain
    4.12 @@ -477,7 +475,7 @@
    4.13    product_prob_space "\<lambda>_. borel::('a::polish_space) measure" I for I::"'i set"
    4.14  
    4.15  sublocale polish_product_prob_space \<subseteq> P: polish_projective I "\<lambda>J. PiM J (\<lambda>_. borel::('a) measure)"
    4.16 -proof qed
    4.17 +  ..
    4.18  
    4.19  lemma (in polish_product_prob_space) limP_eq_PiM: "lim = PiM I (\<lambda>_. borel)"
    4.20    by (rule PiM_eq) (auto simp: emeasure_PiM emeasure_lim_emb)
     5.1 --- a/src/HOL/ROOT	Thu Sep 15 19:31:17 2016 +0200
     5.2 +++ b/src/HOL/ROOT	Thu Sep 15 22:41:05 2016 +0200
     5.3 @@ -739,6 +739,7 @@
     5.4      "~~/src/HOL/Library/Permutation"
     5.5      "~~/src/HOL/Library/Order_Continuity"
     5.6      "~~/src/HOL/Library/Diagonal_Subsequence"
     5.7 +    "~~/src/HOL/Library/Finite_Map"
     5.8    theories
     5.9      Probability
    5.10    document_files "root.tex"