# HG changeset patch # User Lukas Stevens # Date 1629369066 -7200 # Node ID 8e2355ddce1b1576eba32c05629e7f8345de0687 # Parent ecf80e37ed1ae7f38fc4ef66e450cecac87a18aa add/rename some theorems about Map(pings) diff -r ecf80e37ed1a -r 8e2355ddce1b src/HOL/Library/AList.thy --- a/src/HOL/Library/AList.thy Wed Aug 18 23:04:58 2021 +0200 +++ b/src/HOL/Library/AList.thy Thu Aug 19 12:31:06 2021 +0200 @@ -424,7 +424,7 @@ qed lemma graph_map_of: "Map.graph (map_of al) = set (clearjunk al)" - by (metis distinct_clearjunk graph_map_of_if_distinct_ran map_of_clearjunk) + by (metis distinct_clearjunk graph_map_of_if_distinct_dom map_of_clearjunk) lemma clearjunk_update: "clearjunk (update k v al) = update k v (clearjunk al)" by (induct al rule: clearjunk.induct) (simp_all add: delete_update) diff -r ecf80e37ed1a -r 8e2355ddce1b src/HOL/Library/Mapping.thy --- a/src/HOL/Library/Mapping.thy Wed Aug 18 23:04:58 2021 +0200 +++ b/src/HOL/Library/Mapping.thy Thu Aug 19 12:31:06 2021 +0200 @@ -284,16 +284,22 @@ qed qed -lemma lookup_update: "lookup (update k v m) k = Some v" +lemma lookup_update[simp]: "lookup (update k v m) k = Some v" + by transfer simp + +lemma lookup_update_neq[simp]: "k \ k' \ lookup (update k v m) k' = lookup m k'" by transfer simp -lemma lookup_update_neq: "k \ k' \ lookup (update k v m) k' = lookup m k'" +lemma lookup_update': "lookup (update k v m) k' = (if k = k' then Some v else lookup m k')" by transfer simp -lemma lookup_update': "Mapping.lookup (update k v m) k' = (if k = k' then Some v else lookup m k')" - by (auto simp: lookup_update lookup_update_neq) +lemma lookup_empty[simp]: "lookup empty k = None" + by transfer simp -lemma lookup_empty: "lookup empty k = None" +lemma lookup_delete[simp]: "lookup (delete k m) k = None" + by transfer simp + +lemma lookup_delete_neq[simp]: "k \ k' \ lookup (delete k m) k' = lookup m k'" by transfer simp lemma lookup_filter: @@ -310,11 +316,11 @@ by (simp add: lookup_default_def lookup_empty) lemma lookup_default_update: "lookup_default d (update k v m) k = v" - by (simp add: lookup_default_def lookup_update) + by (simp add: lookup_default_def) lemma lookup_default_update_neq: "k \ k' \ lookup_default d (update k v m) k' = lookup_default d m k'" - by (simp add: lookup_default_def lookup_update_neq) + by (simp add: lookup_default_def) lemma lookup_default_update': "lookup_default d (update k v m) k' = (if k = k' then v else lookup_default d m k')" @@ -398,7 +404,7 @@ shows "Mapping.lookup (Mapping.tabulate xs f) x = (if x \ set xs then Some (f x) else None)" using assms by transfer (auto simp: map_of_eq_None_iff o_def dest!: map_of_SomeD) -lemma lookup_of_alist: "Mapping.lookup (Mapping.of_alist xs) k = map_of xs k" +lemma lookup_of_alist: "lookup (of_alist xs) k = map_of xs k" by transfer simp_all lemma keys_is_none_rep [code_unfold]: "k \ keys m \ \ (Option.is_none (lookup m k))" @@ -420,6 +426,10 @@ lemma delete_empty [simp]: "delete k empty = empty" by transfer simp +lemma Mapping_delete_if_notin_keys[simp]: + "k \ keys m \ delete k m = m" + by transfer simp + lemma replace_update: "k \ keys m \ replace k v m = m" "k \ keys m \ replace k v m = update k v m" @@ -487,9 +497,6 @@ lemma in_keysD: "k \ keys m \ \v. lookup m k = Some v" by transfer (fact domD) -lemma in_entriesI: "lookup m k = Some v \ (k, v) \ entries m" - by transfer (fact in_graphI) - lemma keys_update [simp]: "keys (update k v m) = insert k (keys m)" by transfer simp @@ -527,6 +534,14 @@ lemma keys_bulkload [simp]: "keys (bulkload xs) = {0.. set (Mapping.ordered_keys m) = Mapping.keys m" + unfolding ordered_keys_def by transfer auto + lemma distinct_ordered_keys [simp]: "distinct (ordered_keys m)" by (simp add: ordered_keys_def) @@ -536,6 +551,9 @@ lemma ordered_keys_empty [simp]: "ordered_keys empty = []" by (simp add: ordered_keys_def) +lemma sorted_ordered_keys[simp]: "sorted (ordered_keys m)" + unfolding ordered_keys_def by simp + lemma ordered_keys_update [simp]: "k \ keys m \ ordered_keys (update k v m) = ordered_keys m" "finite (keys m) \ k \ keys m \ @@ -806,42 +824,43 @@ qed simp qed simp +lemma entries_empty[simp]: "entries empty = {}" + by transfer (fact graph_empty) + lemma entries_lookup: "entries m = Map.graph (lookup m)" by transfer rule -lemma entries_empty[simp]: "entries empty = {}" - by transfer (fact graph_empty) +lemma in_entriesI: "lookup m k = Some v \ (k, v) \ entries m" + by transfer (fact in_graphI) + +lemma in_entriesD: "(k, v) \ entries m \ lookup m k = Some v" + by transfer (fact in_graphD) + +lemma fst_image_entries_eq_keys[simp]: "fst ` Mapping.entries m = Mapping.keys m" + by transfer (fact fst_graph_eq_dom) lemma finite_entries_iff_finite_keys[simp]: "finite (entries m) = finite (keys m)" by transfer (fact finite_graph_iff_finite_dom) -lemma entries_update[simp]: +lemma entries_update: "entries (update k v m) = insert (k, v) (entries (delete k m))" by transfer (fact graph_map_upd) -lemma Mapping_delete_if_notin_keys[simp]: - "k \ Mapping.keys m \ delete k m = m" - by transfer simp - lemma entries_delete: "entries (delete k m) = {e \ entries m. fst e \ k}" by transfer (fact graph_fun_upd_None) lemma entries_of_alist[simp]: "distinct (List.map fst xs) \ entries (of_alist xs) = set xs" - by transfer (fact graph_map_of_if_distinct_ran) + by transfer (fact graph_map_of_if_distinct_dom) lemma entries_keysD: "x \ entries m \ fst x \ keys m" by transfer (fact graph_domD) -lemma finite_keys_entries[simp]: - "finite (keys (update k v m)) = finite (keys m)" - by transfer simp - lemma set_ordered_entries[simp]: - "finite (Mapping.keys m) \ set (ordered_entries m) = entries m" + "finite (keys m) \ set (ordered_entries m) = entries m" unfolding ordered_entries_def by transfer (auto simp: folding_Map_graph.set_sorted_key_list_of_set[OF subset_refl]) @@ -884,6 +903,22 @@ "ordered_entries (delete k m) = AList.delete k (ordered_entries m)" unfolding ordered_entries_def by transfer auto +lemma map_fst_ordered_entries[simp]: + "List.map fst (ordered_entries m) = ordered_keys m" +proof(cases "finite (Mapping.keys m)") + case True + then have "set (List.map fst (Mapping.ordered_entries m)) = set (Mapping.ordered_keys m)" + unfolding ordered_entries_def ordered_keys_def + by (transfer) (simp add: folding_Map_graph.set_sorted_key_list_of_set[OF subset_refl] fst_graph_eq_dom) + with True show "List.map fst (Mapping.ordered_entries m) = Mapping.ordered_keys m" + by (metis distinct_ordered_entries ordered_keys_def sorted_list_of_set.idem_if_sorted_distinct + sorted_list_of_set.set_sorted_key_list_of_set sorted_ordered_entries) +next + case False + then show ?thesis + unfolding ordered_entries_def ordered_keys_def by simp +qed + lemma fold_empty[simp]: "fold f empty a = a" unfolding fold_def by simp @@ -908,7 +943,9 @@ unfolding ordered_entries_def by transfer (fastforce simp: folding_Map_graph.set_sorted_key_list_of_set[OF order_refl] dest: graph_domD) - from insort_key_is_snoc_if_sorted_and_distinct[OF _ _ this] k_notin_entries show ?thesis + from insort_key_is_snoc_if_sorted_and_distinct[OF _ _ this] k_notin_entries \finite (keys m)\ + show ?thesis + using sorted_ordered_keys unfolding insort_insert_key_def by auto qed finally show ?thesis unfolding fold_def by simp diff -r ecf80e37ed1a -r 8e2355ddce1b src/HOL/Library/RBT_Mapping.thy --- a/src/HOL/Library/RBT_Mapping.thy Wed Aug 18 23:04:58 2021 +0200 +++ b/src/HOL/Library/RBT_Mapping.thy Thu Aug 19 12:31:06 2021 +0200 @@ -58,7 +58,7 @@ by (transfer fixing: t) (auto simp add: lookup_keys intro: sorted_distinct_set_unique) lemma Map_graph_lookup: "Map.graph (RBT.lookup t) = set (RBT.entries t)" - by (metis RBT.distinct_entries RBT.map_of_entries graph_map_of_if_distinct_ran) + by (metis RBT.distinct_entries RBT.map_of_entries graph_map_of_if_distinct_dom) lemma entries_Mapping [code]: "Mapping.entries (Mapping t) = set (RBT.entries t)" by (transfer fixing: t) (fact Map_graph_lookup) diff -r ecf80e37ed1a -r 8e2355ddce1b src/HOL/Map.thy --- a/src/HOL/Map.thy Wed Aug 18 23:04:58 2021 +0200 +++ b/src/HOL/Map.thy Thu Aug 19 12:31:06 2021 +0200 @@ -765,7 +765,7 @@ unfolding graph_eq_to_snd_dom finite_dom_map_of using finite_dom_map_of by blast -lemma graph_map_of_if_distinct_ran: "distinct (map fst al) \ graph (map_of al) = set al" +lemma graph_map_of_if_distinct_dom: "distinct (map fst al) \ graph (map_of al) = set al" unfolding graph_def by auto lemma finite_graph_iff_finite_dom[simp]: "finite (graph m) = finite (dom m)"