# HG changeset patch # User Lars Hupel # Date 1499785897 -7200 # Node ID 0820c83683203fa81cdef956387c0389c6c2b8d2 # Parent e4b98cad5ab4766a4a84f8c8b2ebea02e85e6241 more material on fmaps diff -r e4b98cad5ab4 -r 0820c8368320 src/HOL/Library/Finite_Map.thy --- a/src/HOL/Library/Finite_Map.thy Tue Jul 11 16:12:36 2017 +0200 +++ b/src/HOL/Library/Finite_Map.thy Tue Jul 11 17:11:37 2017 +0200 @@ -244,6 +244,7 @@ lemma fmdom_empty[simp]: "fmdom fmempty = {||}" by transfer' simp lemma fmdom'_empty[simp]: "fmdom' fmempty = {}" by transfer' simp +lemma fmran_empty[simp]: "fmran fmempty = fempty" by transfer' (auto simp: ran_def map_filter_def) lift_definition fmupd :: "'a \ 'b \ ('a, 'b) fmap \ ('a, 'b) fmap" is map_upd @@ -407,6 +408,12 @@ lemma fmrestrict_fset_empty[simp]: "fmrestrict_fset A fmempty = fmempty" unfolding fmfilter_alt_defs by simp +lemma fmdrop_set_null[simp]: "fmdrop_set {} m = m" + by (rule fmap_ext) auto + +lemma fmdrop_fset_null[simp]: "fmdrop_fset {||} m = m" + by (rule fmap_ext) auto + lemma fmdrop_set_single[simp]: "fmdrop_set {a} m = fmdrop a m" unfolding fmfilter_alt_defs by simp @@ -422,6 +429,12 @@ lemma fmdrop_comm: "fmdrop a (fmdrop b m) = fmdrop b (fmdrop a m)" unfolding fmfilter_alt_defs by (rule fmfilter_comm) +lemma fmdrop_set_insert[simp]: "fmdrop_set (insert x S) m = fmdrop x (fmdrop_set S m)" +by (rule fmap_ext) auto + +lemma fmdrop_fset_insert[simp]: "fmdrop_fset (finsert x S) m = fmdrop x (fmdrop_fset S m)" +by (rule fmap_ext) auto + lift_definition fmadd :: "('a, 'b) fmap \ ('a, 'b) fmap \ ('a, 'b) fmap" (infixl "++\<^sub>f" 100) is map_add parametric map_add_transfer @@ -469,6 +482,9 @@ lemma fmadd_assoc[simp]: "m ++\<^sub>f (n ++\<^sub>f p) = m ++\<^sub>f n ++\<^sub>f p" by transfer' simp +lemma fmadd_fmupd[simp]: "m ++\<^sub>f fmupd a b n = fmupd a b (m ++\<^sub>f n)" +by (rule fmap_ext) simp + lift_definition fmpred :: "('a \ 'b \ bool) \ ('a, 'b) fmap \ bool" is map_pred parametric map_pred_transfer @@ -584,6 +600,12 @@ lemma fmap_of_list_SomeD: "fmlookup (fmap_of_list xs) k = Some v \ (k, v) \ set xs" by transfer' (auto dest: map_of_SomeD) +lemma fmdom_fmap_of_list[simp]: "fmdom (fmap_of_list xs) = fset_of_list (map fst xs)" +apply transfer' +apply (subst dom_map_of_conv_image_fst) +apply auto +done + lift_definition fmrel_on_set :: "'a set \ ('b \ 'c \ bool) \ ('a, 'b) fmap \ ('a, 'c) fmap \ bool" is rel_map_on_set . @@ -640,6 +662,7 @@ end \ +declare fmap.pred_mono[mono] context includes lifting_syntax begin @@ -682,9 +705,6 @@ 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) @@ -764,6 +784,13 @@ lemma fmdom'_map[simp]: "fmdom' (fmmap f m) = fmdom' m" by transfer' simp +lemma fmran_fmmap[simp]: "fmran (fmmap f m) = f |`| fmran m" +including fset.lifting +by transfer' (auto simp: ran_def) + +lemma fmran'_fmmap[simp]: "fmran' (fmmap f m) = f ` fmran' m" +by transfer' (auto simp: ran_def) + lemma fmfilter_fmmap[simp]: "fmfilter P (fmmap f m) = fmmap f (fmfilter P m)" by transfer' (auto simp: map_filter_def) @@ -777,6 +804,62 @@ by transfer' (auto simp: map_le_def) +subsection \Additional operations\ + +lift_definition fmmap_keys :: "('a \ 'b \ 'c) \ ('a, 'b) fmap \ ('a, 'c) fmap" is + "\f m a. map_option (f a) (m a)" +unfolding dom_def +by simp + +lemma fmpred_fmmap_keys[simp]: "fmpred P (fmmap_keys f m) = fmpred (\a b. P a (f a b)) m" +by transfer' (auto simp: map_pred_def split: option.splits) + +lemma fmdom_fmmap_keys[simp]: "fmdom (fmmap_keys f m) = fmdom m" +including fset.lifting +by transfer' auto + +lemma fmlookup_fmmap_keys[simp]: "fmlookup (fmmap_keys f m) x = map_option (f x) (fmlookup m x)" +by transfer' simp + +lemma fmfilter_fmmap_keys[simp]: "fmfilter P (fmmap_keys f m) = fmmap_keys f (fmfilter P m)" +by transfer' (auto simp: map_filter_def) + +lemma fmdrop_fmmap_keys[simp]: "fmdrop a (fmmap_keys f m) = fmmap_keys f (fmdrop a m)" +unfolding fmfilter_alt_defs by simp + +lemma fmdrop_set_fmmap_keys[simp]: "fmdrop_set A (fmmap_keys f m) = fmmap_keys f (fmdrop_set A m)" +unfolding fmfilter_alt_defs by simp + +lemma fmdrop_fset_fmmap_keys[simp]: "fmdrop_fset A (fmmap_keys f m) = fmmap_keys f (fmdrop_fset A m)" +unfolding fmfilter_alt_defs by simp + +lemma fmrestrict_set_fmmap_keys[simp]: "fmrestrict_set A (fmmap_keys f m) = fmmap_keys f (fmrestrict_set A m)" +unfolding fmfilter_alt_defs by simp + +lemma fmrestrict_fset_fmmap_keys[simp]: "fmrestrict_fset A (fmmap_keys f m) = fmmap_keys f (fmrestrict_fset A m)" +unfolding fmfilter_alt_defs by simp + +lemma fmmap_keys_subset[intro]: "m \\<^sub>f n \ fmmap_keys f m \\<^sub>f fmmap_keys f n" +by transfer' (auto simp: map_le_def dom_def) + + +subsection \Lifting/transfer setup\ + +context includes lifting_syntax begin + +lemma fmempty_transfer[simp, intro, transfer_rule]: "fmrel P fmempty fmempty" +by transfer auto + +lemma fmadd_transfer[transfer_rule]: + "(fmrel P ===> fmrel P ===> fmrel P) fmadd fmadd" + by (intro fmrel_addI rel_funI) + +lemma fmupd_transfer[transfer_rule]: + "(op = ===> P ===> fmrel P ===> fmrel P) fmupd fmupd" + by auto + +end + subsection \Code setup\ instantiation fmap :: (type, equal) equal begin @@ -821,30 +904,35 @@ context includes fset.lifting begin -lemma [code]: "fmlookup (fmap_of_list m) = map_of m" +lemma fmlookup_of_list[code]: "fmlookup (fmap_of_list m) = map_of m" by transfer simp -lemma [code]: "fmempty = fmap_of_list []" +lemma fmempty_of_list[code]: "fmempty = fmap_of_list []" by transfer simp -lemma [code]: "fmran (fmap_of_list m) = snd |`| fset_of_list (AList.clearjunk m)" +lemma fmran_of_list[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" +lemma fmdom_of_list[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)" +lemma fmfilter_of_list[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)" +lemma fmadd_of_list[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)" +lemma fmmap_of_list[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 +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 + end declare fmap_generic_code[code]