# HG changeset patch # User Lars Hupel # Date 1473972065 -7200 # Node ID a6cd18af8bf941cae81c622a9f3e8e2f5fe6b1dc # Parent d588f684ccaf1e5a93175b31cd8e5b11f3644419 new type for finite maps; use it in HOL-Probability diff -r d588f684ccaf -r a6cd18af8bf9 src/HOL/Library/Finite_Map.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Finite_Map.thy Thu Sep 15 22:41:05 2016 +0200 @@ -0,0 +1,837 @@ +(* Title: HOL/Library/Finite_Map.thy + Author: Lars Hupel, TU München +*) + +section \Type of finite maps defined as a subtype of maps\ + +theory Finite_Map + imports FSet AList +begin + +subsection \Auxiliary constants and lemmas over @{type map}\ + +context includes lifting_syntax begin + +abbreviation rel_map :: "('b \ 'c \ bool) \ ('a \ 'b) \ ('a \ 'c) \ bool" where +"rel_map f \ op = ===> rel_option f" + +lemma map_empty_transfer[transfer_rule]: "rel_map A Map.empty Map.empty" +by transfer_prover + +lemma ran_transfer[transfer_rule]: "(rel_map A ===> rel_set A) ran ran" +proof + fix m n + assume "rel_map A m n" + show "rel_set A (ran m) (ran n)" + proof (rule rel_setI) + fix x + assume "x \ ran m" + then obtain a where "m a = Some x" + unfolding ran_def by auto + + have "rel_option A (m a) (n a)" + using \rel_map A m n\ + by (auto dest: rel_funD) + then obtain y where "n a = Some y" "A x y" + unfolding \m a = _\ + by cases auto + thus "\y \ ran n. A x y" + unfolding ran_def by blast + next + fix y + assume "y \ ran n" + then obtain a where "n a = Some y" + unfolding ran_def by auto + + have "rel_option A (m a) (n a)" + using \rel_map A m n\ + by (auto dest: rel_funD) + then obtain x where "m a = Some x" "A x y" + unfolding \n a = _\ + by cases auto + thus "\x \ ran m. A x y" + unfolding ran_def by blast + qed +qed + +lemma ran_alt_def: "ran m = (the \ m) ` dom m" +unfolding ran_def dom_def by force + +lemma dom_transfer[transfer_rule]: "(rel_map A ===> op =) dom dom" +proof + fix m n + assume "rel_map A m n" + have "m a \ None \ n a \ None" for a + proof - + from \rel_map A m n\ have "rel_option A (m a) (n a)" + unfolding rel_fun_def by auto + thus ?thesis + by cases auto + qed + thus "dom m = dom n" + by auto +qed + +definition map_upd :: "'a \ 'b \ ('a \ 'b) \ ('a \ 'b)" where +"map_upd k v m = m(k \ v)" + +lemma map_upd_transfer[transfer_rule]: + "(op = ===> A ===> rel_map A ===> rel_map A) map_upd map_upd" +unfolding map_upd_def[abs_def] +by transfer_prover + +definition map_filter :: "('a \ bool) \ ('a \ 'b) \ ('a \ 'b)" where +"map_filter P m = (\x. if P x then m x else None)" + +lemma map_filter_map_of[simp]: "map_filter P (map_of m) = map_of [(k, _) \ m. P k]" +proof + fix x + show "map_filter P (map_of m) x = map_of [(k, _) \ m. P k] x" + by (induct m) (auto simp: map_filter_def) +qed + +lemma map_filter_transfer[transfer_rule]: + "(op = ===> rel_map A ===> rel_map A) map_filter map_filter" +unfolding map_filter_def[abs_def] +by transfer_prover + +lemma map_filter_finite[intro]: + assumes "finite (dom m)" + shows "finite (dom (map_filter P m))" +proof - + have "dom (map_filter P m) = Set.filter P (dom m)" + unfolding map_filter_def Set.filter_def dom_def + by auto + thus ?thesis + using assms + by (simp add: Set.filter_def) +qed + +definition map_drop :: "'a \ ('a \ 'b) \ ('a \ 'b)" where +"map_drop a = map_filter (\a'. a' \ a)" + +lemma map_drop_transfer[transfer_rule]: + "(op = ===> rel_map A ===> rel_map A) map_drop map_drop" +unfolding map_drop_def[abs_def] +by transfer_prover + +definition map_drop_set :: "'a set \ ('a \ 'b) \ ('a \ 'b)" where +"map_drop_set A = map_filter (\a. a \ A)" + +lemma map_drop_set_transfer[transfer_rule]: + "(op = ===> rel_map A ===> rel_map A) map_drop_set map_drop_set" +unfolding map_drop_set_def[abs_def] +by transfer_prover + +definition map_restrict_set :: "'a set \ ('a \ 'b) \ ('a \ 'b)" where +"map_restrict_set A = map_filter (\a. a \ A)" + +lemma map_restrict_set_transfer[transfer_rule]: + "(op = ===> rel_map A ===> rel_map A) map_restrict_set map_restrict_set" +unfolding map_restrict_set_def[abs_def] +by transfer_prover + +lemma map_add_transfer[transfer_rule]: + "(rel_map A ===> rel_map A ===> rel_map A) op ++ op ++" +unfolding map_add_def[abs_def] +by transfer_prover + +definition map_pred :: "('a \ 'b \ bool) \ ('a \ 'b) \ bool" where +"map_pred P m \ (\x. case m x of None \ True | Some y \ P x y)" + +lemma map_pred_transfer[transfer_rule]: + "((op = ===> A ===> op =) ===> rel_map A ===> op =) map_pred map_pred" +unfolding map_pred_def[abs_def] +by transfer_prover + +definition rel_map_on_set :: "'a set \ ('b \ 'c \ bool) \ ('a \ 'b) \ ('a \ 'c) \ bool" where +"rel_map_on_set S P = eq_onp (\x. x \ S) ===> rel_option P" + +lemma map_of_transfer[transfer_rule]: + includes lifting_syntax + shows "(list_all2 (rel_prod op = A) ===> rel_map A) map_of map_of" +unfolding map_of_def by transfer_prover + +end + + +subsection \Abstract characterisation\ + +typedef ('a, 'b) fmap = "{m. finite (dom m)} :: ('a \ 'b) set" + morphisms fmlookup Abs_fmap +proof + show "Map.empty \ {m. finite (dom m)}" + by auto +qed + +setup_lifting type_definition_fmap + +lemma fmlookup_finite[intro, simp]: "finite (dom (fmlookup m))" +using fmap.fmlookup by auto + +lemma fmap_ext: + assumes "\x. fmlookup m x = fmlookup n x" + shows "m = n" +using assms +by transfer' auto + + +subsection \Operations\ + +context + includes fset.lifting +begin + +lift_definition fmran :: "('a, 'b) fmap \ 'b fset" + is ran + parametric ran_transfer +unfolding ran_alt_def by auto + +lemma fmranI: "fmlookup m x = Some y \ y |\| fmran m" by transfer' (auto simp: ran_def) + +lift_definition fmdom :: "('a, 'b) fmap \ 'a fset" + is dom + parametric dom_transfer +. + +lemma fmdom_notI: "fmlookup m x = None \ x |\| fmdom m" by transfer' auto +lemma fmdomI: "fmlookup m x = Some y \ x |\| fmdom m" by transfer' auto + +lift_definition fmdom' :: "('a, 'b) fmap \ 'a set" + is dom + parametric dom_transfer +. + +lemma fmdom'_notI: "fmlookup m x = None \ x \ fmdom' m" by transfer' auto +lemma fmdom'I: "fmlookup m x = Some y \ x \ fmdom' m" by transfer' auto + +lemma fmdom'_alt_def: "fmdom' = fset \ fmdom" +by transfer' force + +lemma fmlookup_dom_iff: "x |\| fmdom m \ (\a. fmlookup m x = Some a)" +by transfer' auto + +lift_definition fmempty :: "('a, 'b) fmap" + is Map.empty + parametric map_empty_transfer +by simp + +lemma fmempty_lookup[simp]: "fmlookup fmempty x = None" +by transfer' simp + +lemma fmdom_empty[simp]: "fmdom fmempty = {||}" by transfer' simp +lemma fmdom'_empty[simp]: "fmdom' fmempty = {}" by transfer' simp + +lift_definition fmupd :: "'a \ 'b \ ('a, 'b) fmap \ ('a, 'b) fmap" + is map_upd + parametric map_upd_transfer +unfolding map_upd_def[abs_def] +by simp + +lemma fmupd_lookup[simp]: "fmlookup (fmupd a b m) a' = (if a = a' then Some b else fmlookup m a')" +by transfer' (auto simp: map_upd_def) + +lemma fmdom_fmupd[simp]: "fmdom (fmupd a b m) = finsert a (fmdom m)" by transfer (simp add: map_upd_def) +lemma fmdom'_fmupd[simp]: "fmdom' (fmupd a b m) = insert a (fmdom' m)" by transfer (simp add: map_upd_def) + +lift_definition fmfilter :: "('a \ bool) \ ('a, 'b) fmap \ ('a, 'b) fmap" + is map_filter + parametric map_filter_transfer +by auto + +lemma fmdom_filter[simp]: "fmdom (fmfilter P m) = ffilter P (fmdom m)" +by transfer' (auto simp: map_filter_def Set.filter_def split: if_splits) + +lemma fmdom'_filter[simp]: "fmdom' (fmfilter P m) = Set.filter P (fmdom' m)" +by transfer' (auto simp: map_filter_def Set.filter_def split: if_splits) + +lemma fmlookup_filter[simp]: "fmlookup (fmfilter P m) x = (if P x then fmlookup m x else None)" +by transfer' (auto simp: map_filter_def) + +lemma fmfilter_empty[simp]: "fmfilter P fmempty = fmempty" +by transfer' (auto simp: map_filter_def) + +lemma fmfilter_true[simp]: "(\x. x |\| fmdom m \ P x) \ fmfilter P m = m" +apply transfer' +apply (rule ext) +apply (auto simp: map_filter_def) +apply (case_tac "m x") +apply simp +apply simp +apply (drule_tac m = m in domI) +apply auto +done + +lemma fmfilter_false[simp]: "(\x. x |\| fmdom m \ \ P x) \ fmfilter P m = fmempty" +apply transfer' +apply (rule ext) +apply (auto simp: map_filter_def) +done + +lemma fmfilter_comp[simp]: "fmfilter P (fmfilter Q m) = fmfilter (\x. P x \ Q x) m" +by transfer' (auto simp: map_filter_def) + +lemma fmfilter_comm: "fmfilter P (fmfilter Q m) = fmfilter Q (fmfilter P m)" +unfolding fmfilter_comp by meson + +lemma fmfilter_cong[cong]: + assumes "\x. x |\| fmdom m \ P x = Q x" + shows "fmfilter P m = fmfilter Q m" +using assms +apply transfer' +apply (rule ext) +apply (auto simp: map_filter_def split: if_splits) +apply (case_tac "m x") +apply simp +apply simp +apply (drule_tac m = m in domI) +apply auto +done + +lemma fmfilter_cong'[fundef_cong]: + assumes "\x. x \ fmdom' m \ P x = Q x" + shows "fmfilter P m = fmfilter Q m" +apply (rule fmfilter_cong) +using assms +unfolding fmdom'_alt_def fmember.rep_eq +by auto + +lemma fmfilter_upd[simp]: "fmfilter P (fmupd x y m) = (if P x then fmupd x y (fmfilter P m) else fmfilter P m)" +by transfer' (auto simp: map_upd_def map_filter_def) + +lift_definition fmdrop :: "'a \ ('a, 'b) fmap \ ('a, 'b) fmap" + is map_drop + parametric map_drop_transfer +unfolding map_drop_def by auto + +lemma fmdrop_lookup[simp]: "fmlookup (fmdrop a m) a = None" +by transfer' (auto simp: map_drop_def map_filter_def) + +lift_definition fmdrop_set :: "'a set \ ('a, 'b) fmap \ ('a, 'b) fmap" + is map_drop_set + parametric map_drop_set_transfer +unfolding map_drop_set_def by auto + +lift_definition fmdrop_fset :: "'a fset \ ('a, 'b) fmap \ ('a, 'b) fmap" + is map_drop_set + parametric map_drop_set_transfer +unfolding map_drop_set_def by auto + +lift_definition fmrestrict_set :: "'a set \ ('a, 'b) fmap \ ('a, 'b) fmap" + is map_restrict_set + parametric map_restrict_set_transfer +unfolding map_restrict_set_def by auto + +lemma fmrestrict_set_dom[simp]: "fmrestrict_set (fmdom' m) m = m" +apply transfer' +apply (auto simp: map_restrict_set_def map_filter_def) +apply (rule ext) +apply (auto split: if_splits) +by (metis option.collapse) + +lift_definition fmrestrict_fset :: "'a fset \ ('a, 'b) fmap \ ('a, 'b) fmap" + is map_restrict_set + parametric map_restrict_set_transfer +unfolding map_restrict_set_def by auto + +lemma fmrestrict_fset_dom[simp]: "fmrestrict_fset (fmdom m) m = m" +apply transfer' +apply (auto simp: map_restrict_set_def map_filter_def) +apply (rule ext) +apply (auto split: if_splits) +by (metis option.collapse) + +lemma fmfilter_alt_defs: + "fmdrop a = fmfilter (\a'. a' \ a)" + "fmdrop_set A = fmfilter (\a. a \ A)" + "fmdrop_fset B = fmfilter (\a. a |\| B)" + "fmrestrict_set A = fmfilter (\a. a \ A)" + "fmrestrict_fset B = fmfilter (\a. a |\| B)" +by (transfer'; simp add: map_drop_def map_drop_set_def map_restrict_set_def)+ + +lemma fmdom_drop[simp]: "fmdom (fmdrop a m) = fmdom m - {|a|}" unfolding fmfilter_alt_defs by auto +lemma fmdom'_drop[simp]: "fmdom' (fmdrop a m) = fmdom' m - {a}" unfolding fmfilter_alt_defs by auto +lemma fmdom'_drop_set[simp]: "fmdom' (fmdrop_set A m) = fmdom' m - A" unfolding fmfilter_alt_defs by auto +lemma fmdom_drop_fset[simp]: "fmdom (fmdrop_fset A m) = fmdom m - A" unfolding fmfilter_alt_defs by auto +lemma fmdom'_restrict_set: "fmdom' (fmrestrict_set A m) \ A" unfolding fmfilter_alt_defs by auto +lemma fmdom_restrict_fset: "fmdom (fmrestrict_fset A m) |\| A" unfolding fmfilter_alt_defs by auto + +lemma fmdom'_drop_fset[simp]: "fmdom' (fmdrop_fset A m) = fmdom' m - fset A" +unfolding fmfilter_alt_defs by transfer' (auto simp: map_filter_def split: if_splits) + +lemma fmdom'_restrict_fset: "fmdom' (fmrestrict_fset A m) \ fset A" +unfolding fmfilter_alt_defs by transfer' (auto simp: map_filter_def) + +lemma fmlookup_drop[simp]: + "fmlookup (fmdrop a m) x = (if x \ a then fmlookup m x else None)" +unfolding fmfilter_alt_defs by simp + +lemma fmlookup_drop_set[simp]: + "fmlookup (fmdrop_set A m) x = (if x \ A then fmlookup m x else None)" +unfolding fmfilter_alt_defs by simp + +lemma fmlookup_drop_fset[simp]: + "fmlookup (fmdrop_fset A m) x = (if x |\| A then fmlookup m x else None)" +unfolding fmfilter_alt_defs by simp + +lemma fmlookup_restrict_set[simp]: + "fmlookup (fmrestrict_set A m) x = (if x \ A then fmlookup m x else None)" +unfolding fmfilter_alt_defs by simp + +lemma fmlookup_restrict_fset[simp]: + "fmlookup (fmrestrict_fset A m) x = (if x |\| A then fmlookup m x else None)" +unfolding fmfilter_alt_defs by simp + +lemma fmdrop_empty[simp]: "fmdrop a fmempty = fmempty" + unfolding fmfilter_alt_defs by simp + +lemma fmdrop_set_empty[simp]: "fmdrop_set A fmempty = fmempty" + unfolding fmfilter_alt_defs by simp + +lemma fmdrop_fset_empty[simp]: "fmdrop_fset A fmempty = fmempty" + unfolding fmfilter_alt_defs by simp + +lemma fmrestrict_set_empty[simp]: "fmrestrict_set A fmempty = fmempty" + unfolding fmfilter_alt_defs by simp + +lemma fmrestrict_fset_empty[simp]: "fmrestrict_fset A fmempty = fmempty" + unfolding fmfilter_alt_defs by simp + +lemma fmdrop_set_single[simp]: "fmdrop_set {a} m = fmdrop a m" + unfolding fmfilter_alt_defs by simp + +lemma fmdrop_fset_single[simp]: "fmdrop_fset {|a|} m = fmdrop a m" + unfolding fmfilter_alt_defs by simp + +lemma fmrestrict_set_null[simp]: "fmrestrict_set {} m = fmempty" + unfolding fmfilter_alt_defs by simp + +lemma fmrestrict_fset_null[simp]: "fmrestrict_fset {||} m = fmempty" + unfolding fmfilter_alt_defs by simp + +lemma fmdrop_comm: "fmdrop a (fmdrop b m) = fmdrop b (fmdrop a m)" +unfolding fmfilter_alt_defs by (rule fmfilter_comm) + +lemma fmdrop_fmupd[simp]: "fmdrop x (fmupd x y m) = m" +oops + +lift_definition fmadd :: "('a, 'b) fmap \ ('a, 'b) fmap \ ('a, 'b) fmap" (infixl "++\<^sub>f" 100) + is map_add + parametric map_add_transfer +by simp + +lemma fmdom_add[simp]: "fmdom (m ++\<^sub>f n) = fmdom m |\| fmdom n" by transfer' auto +lemma fmdom'_add[simp]: "fmdom' (m ++\<^sub>f n) = fmdom' m \ fmdom' n" by transfer' auto + +lemma fmadd_drop_left_dom: "fmdrop_fset (fmdom n) m ++\<^sub>f n = m ++\<^sub>f n" +apply transfer' +unfolding map_add_def dom_def map_drop_set_def map_filter_def +by (rule ext) auto + +lemma fmadd_restrict_right_dom: "fmrestrict_fset (fmdom n) (m ++\<^sub>f n) = n" +apply transfer' +unfolding map_add_def dom_def map_restrict_set_def map_filter_def +by (rule ext) auto + +lemma fmfilter_add_distrib[simp]: "fmfilter P (m ++\<^sub>f n) = fmfilter P m ++\<^sub>f fmfilter P n" +by transfer' (auto simp: map_filter_def map_add_def) + +lemma fmdrop_add_distrib[simp]: "fmdrop a (m ++\<^sub>f n) = fmdrop a m ++\<^sub>f fmdrop a n" + unfolding fmfilter_alt_defs by simp + +lemma fmdrop_set_add_distrib[simp]: "fmdrop_set A (m ++\<^sub>f n) = fmdrop_set A m ++\<^sub>f fmdrop_set A n" + unfolding fmfilter_alt_defs by simp + +lemma fmdrop_fset_add_distrib[simp]: "fmdrop_fset A (m ++\<^sub>f n) = fmdrop_fset A m ++\<^sub>f fmdrop_fset A n" + unfolding fmfilter_alt_defs by simp + +lemma fmrestrict_set_add_distrib[simp]: + "fmrestrict_set A (m ++\<^sub>f n) = fmrestrict_set A m ++\<^sub>f fmrestrict_set A n" + unfolding fmfilter_alt_defs by simp + +lemma fmrestrict_fset_add_distrib[simp]: + "fmrestrict_fset A (m ++\<^sub>f n) = fmrestrict_fset A m ++\<^sub>f fmrestrict_fset A n" + unfolding fmfilter_alt_defs by simp + +lemma fmadd_empty[simp]: "fmempty ++\<^sub>f m = m" "m ++\<^sub>f fmempty = m" +by (transfer'; auto)+ + +lemma fmadd_idempotent[simp]: "m ++\<^sub>f m = m" +by transfer' (auto simp: map_add_def split: option.splits) + +lemma fmadd_assoc[simp]: "m ++\<^sub>f (n ++\<^sub>f p) = m ++\<^sub>f n ++\<^sub>f p" +by transfer' simp + +lemma fmlookup_add[simp]: + "fmlookup (m ++\<^sub>f n) x = (if x |\| fmdom n then fmlookup n x else fmlookup m x)" + by transfer' (auto simp: map_add_def split: option.splits) + +lift_definition fmpred :: "('a \ 'b \ bool) \ ('a, 'b) fmap \ bool" + is map_pred + parametric map_pred_transfer +. + +lemma fmpredI[intro]: + assumes "\x y. fmlookup m x = Some y \ P x y" + shows "fmpred P m" +using assms +by transfer' (auto simp: map_pred_def split: option.splits) + +lemma fmpredD[dest]: "fmpred P m \ fmlookup m x = Some y \ P x y" +by transfer' (auto simp: map_pred_def split: option.split_asm) + +lemma fmpred_iff: "fmpred P m \ (\x y. fmlookup m x = Some y \ P x y)" +by auto + +lemma fmpred_alt_def: "fmpred P m \ fBall (fmdom m) (\x. P x (the (fmlookup m x)))" +unfolding fmpred_iff +apply auto +apply (subst (asm) fmlookup_dom_iff) +apply simp +apply (erule_tac x = x in fBallE) +apply simp +by (simp add: fmlookup_dom_iff) + +lemma fmpred_empty[intro!, simp]: "fmpred P fmempty" +by auto + +lemma fmpred_upd[intro]: "fmpred P m \ P x y \ fmpred P (fmupd x y m)" +by transfer' (auto simp: map_pred_def map_upd_def) + +lemma fmpred_updD[dest]: "fmpred P (fmupd x y m) \ P x y" +by auto + +lemma fmpred_add[intro]: "fmpred P m \ fmpred P n \ fmpred P (m ++\<^sub>f n)" +by transfer' (auto simp: map_pred_def map_add_def split: option.splits) + +lemma fmpred_filter[intro]: "fmpred P m \ fmpred P (fmfilter Q m)" +by transfer' (auto simp: map_pred_def map_filter_def) + +lemma fmpred_drop[intro]: "fmpred P m \ fmpred P (fmdrop a m)" + by (auto simp: fmfilter_alt_defs) + +lemma fmpred_drop_set[intro]: "fmpred P m \ fmpred P (fmdrop_set A m)" + by (auto simp: fmfilter_alt_defs) + +lemma fmpred_drop_fset[intro]: "fmpred P m \ fmpred P (fmdrop_fset A m)" + by (auto simp: fmfilter_alt_defs) + +lemma fmpred_restrict_set[intro]: "fmpred P m \ fmpred P (fmrestrict_set A m)" + by (auto simp: fmfilter_alt_defs) + +lemma fmpred_restrict_fset[intro]: "fmpred P m \ fmpred P (fmrestrict_fset A m)" + by (auto simp: fmfilter_alt_defs) + +lemma fmpred_cases[consumes 1]: + assumes "fmpred P m" + obtains (none) "fmlookup m x = None" | (some) y where "fmlookup m x = Some y" "P x y" +using assms by auto + +lift_definition fmsubset :: "('a, 'b) fmap \ ('a, 'b) fmap \ bool" (infix "\\<^sub>f" 50) + is map_le +. + +lemma fmsubset_alt_def: "m \\<^sub>f n \ fmpred (\k v. fmlookup n k = Some v) m" +by transfer' (auto simp: map_pred_def map_le_def dom_def split: option.splits) + +lemma fmsubset_pred: "fmpred P m \ n \\<^sub>f m \ fmpred P n" +unfolding fmsubset_alt_def fmpred_iff +by auto + +lemma fmsubset_filter_mono: "m \\<^sub>f n \ fmfilter P m \\<^sub>f fmfilter P n" +unfolding fmsubset_alt_def fmpred_iff +by auto + +lemma fmsubset_drop_mono: "m \\<^sub>f n \ fmdrop a m \\<^sub>f fmdrop a n" +unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono) + +lemma fmsubset_drop_set_mono: "m \\<^sub>f n \ fmdrop_set A m \\<^sub>f fmdrop_set A n" +unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono) + +lemma fmsubset_drop_fset_mono: "m \\<^sub>f n \ fmdrop_fset A m \\<^sub>f fmdrop_fset A n" +unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono) + +lemma fmsubset_restrict_set_mono: "m \\<^sub>f n \ fmrestrict_set A m \\<^sub>f fmrestrict_set A n" +unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono) + +lemma fmsubset_restrict_fset_mono: "m \\<^sub>f n \ fmrestrict_fset A m \\<^sub>f fmrestrict_fset A n" +unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono) + +lift_definition fmap_of_list :: "('a \ 'b) list \ ('a, 'b) fmap" + is map_of + parametric map_of_transfer +by (rule finite_dom_map_of) + +lemma fmap_of_list_simps[simp]: + "fmap_of_list [] = fmempty" + "fmap_of_list ((k, v) # kvs) = fmupd k v (fmap_of_list kvs)" +by (transfer, simp add: map_upd_def)+ + +lemma fmap_of_list_app[simp]: "fmap_of_list (xs @ ys) = fmap_of_list ys ++\<^sub>f fmap_of_list xs" +by transfer' simp + +lemma fmupd_alt_def: "fmupd k v m = m ++\<^sub>f fmap_of_list [(k, v)]" +by transfer' (auto simp: map_upd_def) + +lemma fmpred_of_list[intro]: + assumes "\k v. (k, v) \ set xs \ P k v" + shows "fmpred P (fmap_of_list xs)" +using assms +by (induction xs) (transfer'; auto simp: map_pred_def)+ + +lemma fmap_of_list_SomeD: "fmlookup (fmap_of_list xs) k = Some v \ (k, v) \ set xs" +by transfer' (auto dest: map_of_SomeD) + +lift_definition fmrel_on_set :: "'a set \ ('b \ 'c \ bool) \ ('a, 'b) fmap \ ('a, 'c) fmap \ bool" + is rel_map_on_set +. + +lift_definition fmrel_on_fset :: "'a fset \ ('b \ 'c \ bool) \ ('a, 'b) fmap \ ('a, 'c) fmap \ bool" + is rel_map_on_set +. + +lemma fmrel_on_fset_alt_def: "fmrel_on_fset S P m n \ fBall S (\x. rel_option P (fmlookup m x) (fmlookup n x))" +by transfer' (auto simp: rel_map_on_set_def eq_onp_def rel_fun_def) + +lemma rel_map_on_fsetI[intro]: + assumes "\x. x |\| S \ rel_option P (fmlookup m x) (fmlookup n x)" + shows "fmrel_on_fset S P m n" +using assms +unfolding fmrel_on_fset_alt_def by auto + +lemma fmrel_on_fset_mono[mono]: "R \ Q \ fmrel_on_fset S R \ fmrel_on_fset S Q" +unfolding fmrel_on_fset_alt_def[abs_def] +apply (intro le_funI fBall_mono) +using option.rel_mono by auto + +lemma fmrel_on_fsetD: "x |\| S \ fmrel_on_fset S P m n \ rel_option P (fmlookup m x) (fmlookup n x)" +unfolding fmrel_on_fset_alt_def +by auto + +lemma fmrel_on_fsubset: "fmrel_on_fset S R m n \ T |\| S \ fmrel_on_fset T R m n" +unfolding fmrel_on_fset_alt_def +by auto + +end + + +subsection \BNF setup\ + +lift_bnf ('a, fmran': 'b) fmap [wits: Map.empty] + for map: fmmap + rel: fmrel + by auto + +context includes lifting_syntax begin + +lemma fmmap_transfer[transfer_rule]: + "(op = ===> pcr_fmap op = op = ===> pcr_fmap op = op =) (\f. op \ (map_option f)) fmmap" +apply (tactic \Local_Defs.unfold_tac @{context} [BNF_Def.bnf_of @{context} @{type_name fmap} |> the |> BNF_Def.map_def_of_bnf]\) +apply (rule rel_funI ext)+ +apply (auto simp: fmap.Abs_fmap_inverse fmap.pcr_cr_eq cr_fmap_def) +done + +lemma fmran'_transfer[transfer_rule]: + "(pcr_fmap op = op = ===> op =) (\x. UNION (range x) set_option) fmran'" +apply (tactic \Local_Defs.unfold_tac @{context} (BNF_Def.bnf_of @{context} @{type_name fmap} |> the |> BNF_Def.set_defs_of_bnf)\) +unfolding fmap.pcr_cr_eq cr_fmap_def +by fastforce + +lemma fmrel_transfer[transfer_rule]: + "(op = ===> pcr_fmap op = op = ===> pcr_fmap op = op = ===> op =) rel_map fmrel" +apply (tactic \Local_Defs.unfold_tac @{context} [BNF_Def.bnf_of @{context} @{type_name fmap} |> the |> BNF_Def.rel_def_of_bnf]\) +unfolding fmap.pcr_cr_eq cr_fmap_def vimage2p_def + by fastforce + +end + + +lemma fmran'_alt_def: "fmran' = fset \ fmran" +including fset.lifting +by transfer' (auto simp: ran_def fun_eq_iff) + +lemma fmran'I: "fmlookup m x = Some y \ y \ fmran' m" +by transfer' auto + +lemma fmrel_iff: "fmrel R m n \ (\x. rel_option R (fmlookup m x) (fmlookup n x))" +by transfer' (auto simp: rel_fun_def) + +lemma fmrelI[intro]: + assumes "\x. rel_option R (fmlookup m x) (fmlookup n x)" + shows "fmrel R m n" +using assms +by transfer' auto + +lemma fmempty_transfer[simp, intro, transfer_rule]: "fmrel P fmempty fmempty" +by transfer auto + +lemma fmrel_upd[intro]: "fmrel P m n \ P x y \ fmrel P (fmupd k x m) (fmupd k y n)" +by transfer' (auto simp: map_upd_def rel_fun_def) + +lemma fmrelD[dest]: "fmrel P m n \ rel_option P (fmlookup m x) (fmlookup n x)" +by transfer' (auto simp: rel_fun_def) + +lemma fmrel_addI[intro]: + assumes "fmrel P m n" "fmrel P a b" + shows "fmrel P (m ++\<^sub>f a) (n ++\<^sub>f b)" +using assms +apply transfer' +apply (auto simp: rel_fun_def map_add_def) +by (metis option.case_eq_if option.collapse option.rel_sel) + +lemma fmrel_cases[consumes 1]: + assumes "fmrel P m n" + obtains (none) "fmlookup m x = None" "fmlookup n x = None" + | (some) a b where "fmlookup m x = Some a" "fmlookup n x = Some b" "P a b" +proof - + from assms have "rel_option P (fmlookup m x) (fmlookup n x)" + by auto + thus thesis + using none some + by (cases rule: option.rel_cases) auto +qed + +lemma fmrel_filter[intro]: "fmrel P m n \ fmrel P (fmfilter Q m) (fmfilter Q n)" +unfolding fmrel_iff by auto + +lemma fmrel_drop[intro]: "fmrel P m n \ fmrel P (fmdrop a m) (fmdrop a n)" + unfolding fmfilter_alt_defs by blast + +lemma fmrel_drop_set[intro]: "fmrel P m n \ fmrel P (fmdrop_set A m) (fmdrop_set A n)" + unfolding fmfilter_alt_defs by blast + +lemma fmrel_drop_fset[intro]: "fmrel P m n \ fmrel P (fmdrop_fset A m) (fmdrop_fset A n)" + unfolding fmfilter_alt_defs by blast + +lemma fmrel_restrict_set[intro]: "fmrel P m n \ fmrel P (fmrestrict_set A m) (fmrestrict_set A n)" + unfolding fmfilter_alt_defs by blast + +lemma fmrel_restrict_fset[intro]: "fmrel P m n \ fmrel P (fmrestrict_fset A m) (fmrestrict_fset A n)" + unfolding fmfilter_alt_defs by blast + +lemma pred_fmap_fmpred[simp]: "pred_fmap P = fmpred (\_. P)" +unfolding fmap.pred_set fmran'_alt_def +including fset.lifting +apply transfer' +apply (rule ext) +apply (auto simp: map_pred_def ran_def split: option.splits dest: ) +done + +lemma pred_fmap_id[simp]: "pred_fmap id (fmmap f m) \ pred_fmap f m" +unfolding fmap.pred_set fmap.set_map +by simp + +lemma fmlookup_map[simp]: "fmlookup (fmmap f m) x = map_option f (fmlookup m x)" +apply (tactic \Local_Defs.unfold_tac @{context} [BNF_Def.bnf_of @{context} @{type_name fmap} |> the |> BNF_Def.map_def_of_bnf]\) +apply (auto simp: fmap.Abs_fmap_inverse) +done + +lemma fmpred_map[simp]: "fmpred P (fmmap f m) \ fmpred (\k v. P k (f v)) m" +unfolding fmpred_iff pred_fmap_def fmap.set_map +by auto + +lemma fmpred_id[simp]: "fmpred (\_. id) (fmmap f m) \ fmpred (\_. f) m" +by simp + +lemma fmmap_add[simp]: "fmmap f (m ++\<^sub>f n) = fmmap f m ++\<^sub>f fmmap f n" +by transfer' (auto simp: map_add_def fun_eq_iff split: option.splits) + +lemma fmmap_empty[simp]: "fmmap f fmempty = fmempty" +by transfer auto + +lemma fmdom_map[simp]: "fmdom (fmmap f m) = fmdom m" +including fset.lifting +by transfer' simp + +lemma fmdom'_map[simp]: "fmdom' (fmmap f m) = fmdom' m" +by transfer' simp + +lemma fmfilter_fmmap[simp]: "fmfilter P (fmmap f m) = fmmap f (fmfilter P m)" +by transfer' (auto simp: map_filter_def) + +lemma fmdrop_fmmap[simp]: "fmdrop a (fmmap f m) = fmmap f (fmdrop a m)" unfolding fmfilter_alt_defs by simp +lemma fmdrop_set_fmmap[simp]: "fmdrop_set A (fmmap f m) = fmmap f (fmdrop_set A m)" unfolding fmfilter_alt_defs by simp +lemma fmdrop_fset_fmmap[simp]: "fmdrop_fset A (fmmap f m) = fmmap f (fmdrop_fset A m)" unfolding fmfilter_alt_defs by simp +lemma fmrestrict_set_fmmap[simp]: "fmrestrict_set A (fmmap f m) = fmmap f (fmrestrict_set A m)" unfolding fmfilter_alt_defs by simp +lemma fmrestrict_fset_fmmap[simp]: "fmrestrict_fset A (fmmap f m) = fmmap f (fmrestrict_fset A m)" unfolding fmfilter_alt_defs by simp + +lemma fmmap_subset[intro]: "m \\<^sub>f n \ fmmap f m \\<^sub>f fmmap f n" +by transfer' (auto simp: map_le_def) + + +subsection \Code setup\ + +instantiation fmap :: (type, equal) equal begin + +definition "equal_fmap \ fmrel HOL.equal" + +instance proof + fix m n :: "('a, 'b) fmap" + have "fmrel op = m n \ (m = n)" + by transfer' (simp add: option.rel_eq rel_fun_eq) + thus "equal_class.equal m n \ (m = n)" + unfolding equal_fmap_def + by (simp add: equal_eq[abs_def]) +qed + +end + +lemma fBall_alt_def: "fBall S P \ (\x. x |\| S \ P x)" +by force + +lemma fmrel_code: + "fmrel R m n \ + fBall (fmdom m) (\x. rel_option R (fmlookup m x) (fmlookup n x)) \ + fBall (fmdom n) (\x. rel_option R (fmlookup m x) (fmlookup n x))" +unfolding fmrel_iff fmlookup_dom_iff fBall_alt_def +by (metis option.collapse option.rel_sel) + +lemmas fmap_generic_code = + fmrel_code + fmran'_alt_def + fmdom'_alt_def + fmfilter_alt_defs + pred_fmap_fmpred + fmsubset_alt_def + fmupd_alt_def + fmrel_on_fset_alt_def + fmpred_alt_def + + +code_datatype fmap_of_list +quickcheck_generator fmap constructors: fmap_of_list + +context includes fset.lifting begin + +lemma [code]: "fmlookup (fmap_of_list m) = map_of m" +by transfer simp + +lemma [code]: "fmempty = fmap_of_list []" +by transfer simp + +lemma [code]: "fmran (fmap_of_list m) = snd |`| fset_of_list (AList.clearjunk m)" +by transfer (auto simp: ran_map_of) + +lemma [code]: "fmdom (fmap_of_list m) = fst |`| fset_of_list m" +by transfer (auto simp: dom_map_of_conv_image_fst) + +lemma [code]: "fmfilter P (fmap_of_list m) = fmap_of_list (filter (\(k, _). P k) m)" +by transfer' auto + +lemma [code]: "fmap_of_list m ++\<^sub>f fmap_of_list n = fmap_of_list (AList.merge m n)" +by transfer (simp add: merge_conv') + +lemma [code]: "fmmap f (fmap_of_list m) = fmap_of_list (map (apsnd f) m)" +apply transfer +apply (subst map_of_map[symmetric]) +apply (auto simp: apsnd_def map_prod_def) +done + +end + +declare fmap_generic_code[code] + +lifting_update fmap.lifting +lifting_forget fmap.lifting + +end \ No newline at end of file diff -r d588f684ccaf -r a6cd18af8bf9 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Thu Sep 15 19:31:17 2016 +0200 +++ b/src/HOL/Library/Library.thy Thu Sep 15 22:41:05 2016 +0200 @@ -26,6 +26,7 @@ Extended_Nonnegative_Real Extended_Real FinFun + Finite_Map Float Formal_Power_Series Fraction_Field diff -r d588f684ccaf -r a6cd18af8bf9 src/HOL/Probability/Fin_Map.thy --- a/src/HOL/Probability/Fin_Map.thy Thu Sep 15 19:31:17 2016 +0200 +++ b/src/HOL/Probability/Fin_Map.thy Thu Sep 15 22:41:05 2016 +0200 @@ -5,29 +5,27 @@ section \Finite Maps\ theory Fin_Map -imports Finite_Product_Measure + imports Finite_Product_Measure "~~/src/HOL/Library/Finite_Map" begin -text \Auxiliary type that is instantiated to @{class polish_space}, needed for the proof of +text \The @{type fmap} type can be instantiated to @{class polish_space}, needed for the proof of projective limit. @{const extensional} functions are used for the representation in order to stay close to the developments of (finite) products @{const Pi\<^sub>E} and their sigma-algebra @{const Pi\<^sub>M}.\ -typedef ('i, 'a) finmap ("(_ \\<^sub>F /_)" [22, 21] 21) = - "{f::'i \ 'a option. finite (dom f)}" - by (auto intro!: exI[where x="\_. None"]) +type_notation fmap ("(_ \\<^sub>F /_)" [22, 21] 21) -setup_lifting type_definition_finmap +unbundle fmap.lifting subsection \Domain and Application\ -lift_definition domain::"('i, 'a) finmap \ 'i set" is dom . +lift_definition domain::"('i \\<^sub>F 'a) \ 'i set" is dom . lemma finite_domain[simp, intro]: "finite (domain P)" by transfer simp -lift_definition proj :: "('i, 'a) finmap \ 'i \ 'a" ("'((_)')\<^sub>F" [0] 1000) is +lift_definition proj :: "('i \\<^sub>F 'a) \ 'i \ 'a" ("'((_)')\<^sub>F" [0] 1000) is "\f x. if x \ dom f then the (f x) else undefined" . declare [[coercion proj]] @@ -48,7 +46,7 @@ subsection \Countable Finite Maps\ -instance finmap :: (countable, countable) countable +instance fmap :: (countable, countable) countable proof obtain mapper where mapper: "\fm :: 'a \\<^sub>F 'b. set (mapper fm) = domain fm" by (metis finite_list[OF finite_domain]) @@ -68,7 +66,7 @@ subsection \Constructor of Finite Maps\ -lift_definition finmap_of::"'i set \ ('i \ 'a) \ ('i, 'a) finmap" is +lift_definition finmap_of::"'i set \ ('i \ 'a) \ ('i \\<^sub>F 'a)" is "\I f x. if x \ I \ finite I then Some (f x) else None" by (simp add: dom_def) @@ -156,17 +154,17 @@ subsection \Topological Space of Finite Maps\ -instantiation finmap :: (type, topological_space) topological_space +instantiation fmap :: (type, topological_space) topological_space begin -definition open_finmap :: "('a \\<^sub>F 'b) set \ bool" where - [code del]: "open_finmap = generate_topology {Pi' a b|a b. \i\a. open (b i)}" +definition open_fmap :: "('a \\<^sub>F 'b) set \ bool" where + [code del]: "open_fmap = generate_topology {Pi' a b|a b. \i\a. open (b i)}" lemma open_Pi'I: "(\i. i \ I \ open (A i)) \ open (Pi' I A)" - by (auto intro: generate_topology.Basis simp: open_finmap_def) + by (auto intro: generate_topology.Basis simp: open_fmap_def) instance using topological_space_generate_topology - by intro_classes (auto simp: open_finmap_def class.topological_space_def) + by intro_classes (auto simp: open_fmap_def class.topological_space_def) end @@ -211,7 +209,7 @@ shows "continuous_on s (\x. (x)\<^sub>F i)" unfolding continuous_on_def by (safe intro!: tendsto_proj tendsto_ident_at) -instance finmap :: (type, first_countable_topology) first_countable_topology +instance fmap :: (type, first_countable_topology) first_countable_topology proof fix x::"'a\\<^sub>F'b" have "\i. \A. countable A \ (\a\A. x i \ a) \ (\a\A. open a) \ @@ -229,7 +227,7 @@ show "countable ?A" using A by (simp add: countable_PiE) next fix S::"('a \\<^sub>F 'b) set" assume "open S" "x \ S" - thus "\a\?A. a \ S" unfolding open_finmap_def + thus "\a\?A. a \ S" unfolding open_fmap_def proof (induct rule: generate_topology.induct) case UNIV thus ?case by (auto simp add: ex_in_conv PiE_eq_empty_iff A_notempty) next @@ -266,29 +264,29 @@ (* TODO: Product of uniform spaces and compatibility with metric_spaces! *) -instantiation finmap :: (type, metric_space) dist +instantiation fmap :: (type, metric_space) dist begin -definition dist_finmap where +definition dist_fmap where "dist P Q = Max (range (\i. dist ((P)\<^sub>F i) ((Q)\<^sub>F i))) + (if domain P = domain Q then 0 else 1)" instance .. end -instantiation finmap :: (type, metric_space) uniformity_dist +instantiation fmap :: (type, metric_space) uniformity_dist begin definition [code del]: - "(uniformity :: (('a, 'b) finmap \ ('a, 'b) finmap) filter) = + "(uniformity :: (('a, 'b) fmap \ ('a \\<^sub>F 'b)) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})" instance - by standard (rule uniformity_finmap_def) + by standard (rule uniformity_fmap_def) end -declare uniformity_Abort[where 'a="('a, 'b::metric_space) finmap", code] +declare uniformity_Abort[where 'a="('a \\<^sub>F 'b::metric_space)", code] -instantiation finmap :: (type, metric_space) metric_space +instantiation fmap :: (type, metric_space) metric_space begin lemma finite_proj_image': "x \ domain P \ finite ((P)\<^sub>F ` S)" @@ -308,14 +306,14 @@ lemma dist_le_1_imp_domain_eq: shows "dist P Q < 1 \ domain P = domain Q" - by (simp add: dist_finmap_def finite_proj_diag split: if_split_asm) + by (simp add: dist_fmap_def finite_proj_diag split: if_split_asm) lemma dist_proj: shows "dist ((x)\<^sub>F i) ((y)\<^sub>F i) \ dist x y" proof - have "dist (x i) (y i) \ Max (range (\i. dist (x i) (y i)))" by (simp add: Max_ge_iff finite_proj_diag) - also have "\ \ dist x y" by (simp add: dist_finmap_def) + also have "\ \ dist x y" by (simp add: dist_fmap_def) finally show ?thesis . qed @@ -326,7 +324,7 @@ shows "dist P Q < e" proof - have "dist P Q = Max (range (\i. dist (P i) (Q i)))" - using assms by (simp add: dist_finmap_def finite_proj_diag) + using assms by (simp add: dist_fmap_def finite_proj_diag) also have "\ < e" proof (subst Max_less_iff, safe) fix i @@ -343,7 +341,7 @@ proof assume "open S" thus ?od - unfolding open_finmap_def + unfolding open_fmap_def proof (induct rule: generate_topology.induct) case UNIV thus ?case by (auto intro: zero_less_one) next @@ -383,7 +381,7 @@ show "domain y = a" using d s \a \ {}\ by (auto simp: dist_le_1_imp_domain_eq a_dom) fix i assume i: "i \ a" hence "dist ((y)\<^sub>F i) ((x)\<^sub>F i) < es i" using d - by (auto simp: dist_finmap_def \a \ {}\ intro!: le_less_trans[OF dist_proj]) + by (auto simp: dist_fmap_def \a \ {}\ intro!: le_less_trans[OF dist_proj]) with i show "y i \ b i" by (rule in_b) qed next @@ -410,23 +408,23 @@ moreover assume "x \ (\' i\domain y. ball (y i) (e y))" hence "dist x y < e y" using e_pos \y \ S\ - by (auto simp: dist_finmap_def Pi'_iff finite_proj_diag dist_commute) + by (auto simp: dist_fmap_def Pi'_iff finite_proj_diag dist_commute) ultimately show "x \ S" by (rule e_in) qed also have "open \" - unfolding open_finmap_def + unfolding open_fmap_def by (intro generate_topology.UN) (auto intro: generate_topology.Basis) finally show "open S" . qed show "open S = (\x\S. \\<^sub>F (x', y) in uniformity. x' = x \ y \ S)" unfolding * eventually_uniformity_metric - by (simp del: split_paired_All add: dist_finmap_def dist_commute eq_commute) + by (simp del: split_paired_All add: dist_fmap_def dist_commute eq_commute) next fix P Q::"'a \\<^sub>F 'b" have Max_eq_iff: "\A m. finite A \ A \ {} \ (Max A = m) = (m \ A \ (\a\A. a \ m))" by (auto intro: Max_in Max_eqI) show "dist P Q = 0 \ P = Q" - by (auto simp: finmap_eq_iff dist_finmap_def Max_ge_iff finite_proj_diag Max_eq_iff + by (auto simp: finmap_eq_iff dist_fmap_def Max_ge_iff finite_proj_diag Max_eq_iff add_nonneg_eq_0_iff intro!: Max_eqI image_eqI[where x=undefined]) next @@ -435,14 +433,14 @@ let ?dpq = "?dists P Q" and ?dpr = "?dists P R" and ?dqr = "?dists Q R" let ?dom = "\P Q. (if domain P = domain Q then 0 else 1::real)" have "dist P Q = Max (range ?dpq) + ?dom P Q" - by (simp add: dist_finmap_def) + by (simp add: dist_fmap_def) also obtain t where "t \ range ?dpq" "t = Max (range ?dpq)" by (simp add: finite_proj_diag) then obtain i where "Max (range ?dpq) = ?dpq i" by auto also have "?dpq i \ ?dpr i + ?dqr i" by (rule dist_triangle2) also have "?dpr i \ Max (range ?dpr)" by (simp add: finite_proj_diag) also have "?dqr i \ Max (range ?dqr)" by (simp add: finite_proj_diag) also have "?dom P Q \ ?dom P R + ?dom Q R" by simp - finally show "dist P Q \ dist P R + dist Q R" by (simp add: dist_finmap_def ac_simps) + finally show "dist P Q \ dist P R + dist Q R" by (simp add: dist_fmap_def ac_simps) qed end @@ -468,10 +466,10 @@ ultimately show ?case by eventually_elim auto qed simp thus "eventually (\x. dist (f x) g < e) sequentially" - by eventually_elim (auto simp add: dist_finmap_def finite_proj_diag ind_f \0 < e\) + by eventually_elim (auto simp add: dist_fmap_def finite_proj_diag ind_f \0 < e\) qed -instance finmap :: (type, complete_space) complete_space +instance fmap :: (type, complete_space) complete_space proof fix P::"nat \ 'a \\<^sub>F 'b" assume "Cauchy P" @@ -483,7 +481,7 @@ define p where "p i n = P n i" for i n define q where "q i = lim (p i)" for i define Q where "Q = finmap_of d q" - have q: "\i. i \ d \ q i = Q i" by (auto simp add: Q_def Abs_finmap_inverse) + have q: "\i. i \ d \ q i = Q i" by (auto simp add: Q_def Abs_fmap_inverse) { fix i assume "i \ d" have "Cauchy (p i)" unfolding cauchy p_def @@ -520,7 +518,7 @@ proof (safe intro!: exI[where x="N"]) fix n assume "N \ n" hence dom: "domain (P n) = d" "domain Q = d" "domain (P n) = domain Q" - using dim by (simp_all add: N_def Q_def dim_def Abs_finmap_inverse) + using dim by (simp_all add: N_def Q_def dim_def Abs_fmap_inverse) show "dist (P n) Q < e" proof (rule dist_finmap_lessI[OF dom(3) \0 < e\]) fix i @@ -537,7 +535,7 @@ subsection \Second Countable Space of Finite Maps\ -instantiation finmap :: (countable, second_countable_topology) second_countable_topology +instantiation fmap :: (countable, second_countable_topology) second_countable_topology begin definition basis_proj::"'b set set" @@ -590,7 +588,7 @@ assume O': "open O'" "x \ O'" then obtain a where a: "x \ Pi' (domain x) a" "Pi' (domain x) a \ O'" "\i. i\domain x \ open (a i)" - unfolding open_finmap_def + unfolding open_fmap_def proof (atomize_elim, induct rule: generate_topology.induct) case (Int a b) let ?p="\a f. x \ Pi' (domain x) f \ Pi' (domain x) f \ a \ (\i. i \ domain x \ open (f i))" @@ -630,7 +628,7 @@ subsection \Polish Space of Finite Maps\ -instance finmap :: (countable, polish_space) polish_space proof qed +instance fmap :: (countable, polish_space) polish_space proof qed subsection \Product Measurable Space of Finite Maps\ diff -r d588f684ccaf -r a6cd18af8bf9 src/HOL/Probability/Projective_Limit.thy --- a/src/HOL/Probability/Projective_Limit.thy Thu Sep 15 19:31:17 2016 +0200 +++ b/src/HOL/Probability/Projective_Limit.thy Thu Sep 15 22:41:05 2016 +0200 @@ -455,8 +455,6 @@ hide_const (open) PiF hide_const (open) Pi\<^sub>F hide_const (open) Pi' -hide_const (open) Abs_finmap -hide_const (open) Rep_finmap hide_const (open) finmap_of hide_const (open) proj hide_const (open) domain @@ -477,7 +475,7 @@ product_prob_space "\_. borel::('a::polish_space) measure" I for I::"'i set" sublocale polish_product_prob_space \ P: polish_projective I "\J. PiM J (\_. borel::('a) measure)" -proof qed + .. lemma (in polish_product_prob_space) limP_eq_PiM: "lim = PiM I (\_. borel)" by (rule PiM_eq) (auto simp: emeasure_PiM emeasure_lim_emb) diff -r d588f684ccaf -r a6cd18af8bf9 src/HOL/ROOT --- a/src/HOL/ROOT Thu Sep 15 19:31:17 2016 +0200 +++ b/src/HOL/ROOT Thu Sep 15 22:41:05 2016 +0200 @@ -739,6 +739,7 @@ "~~/src/HOL/Library/Permutation" "~~/src/HOL/Library/Order_Continuity" "~~/src/HOL/Library/Diagonal_Subsequence" + "~~/src/HOL/Library/Finite_Map" theories Probability document_files "root.tex"