# HG changeset patch # User Lars Hupel # Date 1535222649 -7200 # Node ID db97c1ed115e0f8a249e151d0541878239761f4b # Parent 3974935e0252d0bf411d5f9d7bc960218025706a material on finite maps diff -r 3974935e0252 -r db97c1ed115e src/HOL/Library/Finite_Map.thy --- a/src/HOL/Library/Finite_Map.thy Fri Aug 24 20:22:14 2018 +0000 +++ b/src/HOL/Library/Finite_Map.thy Sat Aug 25 20:44:09 2018 +0200 @@ -134,6 +134,15 @@ thus "x = y" .. qed +lemma dom_comp: "dom (m \\<^sub>m n) \ dom n" +unfolding map_comp_def dom_def +by (auto split: option.splits) + +lemma dom_comp_finite: "finite (dom n) \ finite (dom (map_comp m n))" +by (metis finite_subset dom_comp) + +parametric_constant map_comp_transfer[transfer_rule]: map_comp_def + end @@ -651,6 +660,82 @@ unfolding fmrel_on_fset_alt_def by auto +lift_definition fmimage :: "('a, 'b) fmap \ 'a fset \ 'b fset" is "\m S. {b|a b. m a = Some b \ a \ S}" +subgoal for m S + apply (rule finite_subset[where B = "ran m"]) + apply (auto simp: ran_def)[] + by (rule finite_ran) +done + +lemma fmimage_alt_def: "fmimage m S = fmran (fmrestrict_fset S m)" +by transfer' (auto simp: ran_def map_restrict_set_def map_filter_def) + +lemma fmimage_empty[simp]: "fmimage m fempty = fempty" +by transfer' auto + +lemma fmimage_subset_ran[simp]: "fmimage m S |\| fmran m" +by transfer' (auto simp: ran_def) + +lemma fmimage_dom[simp]: "fmimage m (fmdom m) = fmran m" +by transfer' (auto simp: ran_def) + +lemma fmimage_inter: "fmimage m (A |\| B) |\| fmimage m A |\| fmimage m B" +by transfer' auto + +lemma fimage_inter_dom[simp]: + "fmimage m (fmdom m |\| A) = fmimage m A" + "fmimage m (A |\| fmdom m) = fmimage m A" +by (transfer'; auto)+ + +lemma fmimage_union[simp]: "fmimage m (A |\| B) = fmimage m A |\| fmimage m B" +by transfer' auto + +lemma fmimage_Union[simp]: "fmimage m (ffUnion A) = ffUnion (fmimage m |`| A)" +by transfer' auto + +lemma fmimage_filter[simp]: "fmimage (fmfilter P m) A = fmimage m (ffilter P A)" +by transfer' (auto simp: map_filter_def) + +lemma fmimage_drop[simp]: "fmimage (fmdrop a m) A = fmimage m (A - {|a|})" +by transfer' (auto simp: map_filter_def map_drop_def) + +lemma fmimage_drop_fset[simp]: "fmimage (fmdrop_fset B m) A = fmimage m (A - B)" +by transfer' (auto simp: map_filter_def map_drop_set_def) + +lemma fmimage_restrict_fset[simp]: "fmimage (fmrestrict_fset B m) A = fmimage m (A |\| B)" +by transfer' (auto simp: map_filter_def map_restrict_set_def) + +lemma fmfilter_ran[simp]: "fmran (fmfilter P m) = fmimage m (ffilter P (fmdom m))" +by transfer' (auto simp: ran_def map_filter_def) + +lemma fmran_drop[simp]: "fmran (fmdrop a m) = fmimage m (fmdom m - {|a|})" +by transfer' (auto simp: ran_def map_drop_def map_filter_def) + +lemma fmran_drop_fset[simp]: "fmran (fmdrop_fset A m) = fmimage m (fmdom m - A)" +by transfer' (auto simp: ran_def map_drop_set_def map_filter_def) + +lemma fmran_restrict_fset: "fmran (fmrestrict_fset A m) = fmimage m (fmdom m |\| A)" +by transfer' (auto simp: ran_def map_restrict_set_def map_filter_def) + +lemma fmlookup_image_iff: "y |\| fmimage m A \ (\x. fmlookup m x = Some y \ x |\| A)" +by transfer' (auto simp: ran_def) + +lemma fmimageI: "fmlookup m x = Some y \ x |\| A \ y |\| fmimage m A" +by (auto simp: fmlookup_image_iff) + +lemma fmimageE[elim]: + assumes "y |\| fmimage m A" + obtains x where "fmlookup m x = Some y" "x |\| A" +using assms by (auto simp: fmlookup_image_iff) + +lift_definition fmcomp :: "('b, 'c) fmap \ ('a, 'b) fmap \ ('a, 'c) fmap" (infixl "\\<^sub>f" 55) + is map_comp + parametric map_comp_transfer +by (rule dom_comp_finite) + +lemma fmlookup_comp[simp]: "fmlookup (m \\<^sub>f n) x = Option.bind (fmlookup n x) (fmlookup m)" +by transfer' (auto simp: map_comp_def split: option.splits) + end @@ -963,12 +1048,12 @@ lemma list_all_sorted_list[simp]: "list_all P (sorted_list_of_fmap m) = fmpred (curry P) m" unfolding sorted_list_of_fmap_def curry_def list.pred_map apply (auto simp: list_all_iff) -including fmap.lifting fset.lifting +including fset.lifting by (transfer; auto simp: dom_def map_pred_def split: option.splits)+ lemma map_of_sorted_list[simp]: "map_of (sorted_list_of_fmap m) = fmlookup m" unfolding sorted_list_of_fmap_def -including fmap.lifting fset.lifting +including fset.lifting by transfer (simp add: map_of_map_keys) @@ -999,11 +1084,10 @@ lifting_update fmap.lifting -lemma fmap_exhaust[case_names fmempty fmupd, cases type: fmap]: - assumes fmempty: "m = fmempty \ P" - assumes fmupd: "\x y m'. m = fmupd x y m' \ x |\| fmdom m' \ P" - shows "P" -using assms including fmap.lifting fset.lifting +lemma fmap_exhaust[cases type: fmap]: + obtains (fmempty) "m = fmempty" + | (fmupd) x y m' where "m = fmupd x y m'" "x |\| fmdom m'" +using that including fmap.lifting fset.lifting proof transfer fix m P assume "finite (dom m)" @@ -1139,11 +1223,28 @@ apply (auto simp: apsnd_def map_prod_def) done -lemma fmmap_keys_of_list[code]: "fmmap_keys f (fmap_of_list m) = fmap_of_list (map (\(a, b). (a, f a b)) m)" +lemma fmmap_keys_of_list[code]: + "fmmap_keys f (fmap_of_list m) = fmap_of_list (map (\(a, b). (a, f a b)) m)" apply transfer subgoal for f m by (induction m) (auto simp: apsnd_def map_prod_def fun_eq_iff) done +lemma fmimage_of_list[code]: + "fmimage (fmap_of_list m) A = fset_of_list (map snd (filter (\(k, _). k |\| A) (AList.clearjunk m)))" +apply (subst fmimage_alt_def) +apply (subst fmfilter_alt_defs) +apply (subst fmfilter_of_list) +apply (subst fmran_of_list) +apply transfer' +apply (subst AList.restrict_eq[symmetric]) +apply (subst clearjunk_restrict) +apply (subst AList.restrict_eq) +by auto + +lemma fmcomp_list[code]: + "fmap_of_list m \\<^sub>f fmap_of_list n = fmap_of_list (AList.compose n m)" +by (rule fmap_ext) (simp add: fmlookup_of_list compose_conv map_comp_def split: option.splits) + end