--- a/src/HOL/Library/Mapping.thy Fri May 21 15:22:36 2010 +0200
+++ b/src/HOL/Library/Mapping.thy Fri May 21 15:22:37 2010 +0200
@@ -6,6 +6,30 @@
imports Main
begin
+lemma remove1_idem: (*FIXME move to List.thy*)
+ assumes "x \<notin> set xs"
+ shows "remove1 x xs = xs"
+ using assms by (induct xs) simp_all
+
+lemma remove1_insort [simp]:
+ "remove1 x (insort x xs) = xs"
+ by (induct xs) simp_all
+
+lemma sorted_list_of_set_remove:
+ assumes "finite A"
+ shows "sorted_list_of_set (A - {x}) = remove1 x (sorted_list_of_set A)"
+proof (cases "x \<in> A")
+ case False with assms have "x \<notin> set (sorted_list_of_set A)" by simp
+ with False show ?thesis by (simp add: remove1_idem)
+next
+ case True then obtain B where A: "A = insert x B" by (rule Set.set_insert)
+ with assms show ?thesis by simp
+qed
+
+lemma sorted_list_of_set_range [simp]:
+ "sorted_list_of_set {m..<n} = [m..<n]"
+ by (rule sorted_distinct_set_unique) simp_all
+
subsection {* Type definition and primitive operations *}
datatype ('a, 'b) mapping = Mapping "'a \<rightharpoonup> 'b"
@@ -29,19 +53,19 @@
"keys m = dom (lookup m)"
definition ordered_keys :: "('a\<Colon>linorder, 'b) mapping \<Rightarrow> 'a list" where
- "ordered_keys m = sorted_list_of_set (keys m)"
+ "ordered_keys m = (if finite (keys m) then sorted_list_of_set (keys m) else [])"
definition is_empty :: "('a, 'b) mapping \<Rightarrow> bool" where
- "is_empty m \<longleftrightarrow> dom (lookup m) = {}"
+ "is_empty m \<longleftrightarrow> keys m = {}"
definition size :: "('a, 'b) mapping \<Rightarrow> nat" where
- "size m = (if finite (dom (lookup m)) then card (dom (lookup m)) else 0)"
+ "size m = (if finite (keys m) then card (keys m) else 0)"
definition replace :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
- "replace k v m = (if lookup m k = None then m else update k v m)"
+ "replace k v m = (if k \<in> keys m then update k v m else m)"
definition default :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
- "default k v m = (if lookup m k = None then update k v m else m)"
+ "default k v m = (if k \<in> keys m then m else update k v m)"
definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
"map_entry k f m = (case lookup m k of None \<Rightarrow> m
@@ -68,6 +92,10 @@
shows "m = n"
using assms by simp
+lemma keys_is_none_lookup [code_inline]:
+ "k \<in> keys m \<longleftrightarrow> \<not> (Option.is_none (lookup m k))"
+ by (auto simp add: keys_def is_none_def)
+
lemma lookup_empty [simp]:
"lookup empty = Map.empty"
by (simp add: empty_def)
@@ -111,42 +139,157 @@
by (rule mapping_eqI) simp
lemma replace_update:
- "k \<notin> dom (lookup m) \<Longrightarrow> replace k v m = m"
- "k \<in> dom (lookup m) \<Longrightarrow> replace k v m = update k v m"
- by (rule mapping_eqI, auto simp add: replace_def fun_upd_twist)+
+ "k \<notin> keys m \<Longrightarrow> replace k v m = m"
+ "k \<in> keys m \<Longrightarrow> replace k v m = update k v m"
+ by (rule mapping_eqI) (auto simp add: replace_def fun_upd_twist)+
lemma size_empty [simp]:
"size empty = 0"
- by (simp add: size_def)
+ by (simp add: size_def keys_def)
lemma size_update:
- "finite (dom (lookup m)) \<Longrightarrow> size (update k v m) =
- (if k \<in> dom (lookup m) then size m else Suc (size m))"
- by (auto simp add: size_def insert_dom)
+ "finite (keys m) \<Longrightarrow> size (update k v m) =
+ (if k \<in> keys m then size m else Suc (size m))"
+ by (auto simp add: size_def insert_dom keys_def)
lemma size_delete:
- "size (delete k m) = (if k \<in> dom (lookup m) then size m - 1 else size m)"
- by (simp add: size_def)
+ "size (delete k m) = (if k \<in> keys m then size m - 1 else size m)"
+ by (simp add: size_def keys_def)
-lemma size_tabulate:
+lemma size_tabulate [simp]:
"size (tabulate ks f) = length (remdups ks)"
- by (simp add: size_def distinct_card [of "remdups ks", symmetric] comp_def)
+ by (simp add: size_def distinct_card [of "remdups ks", symmetric] comp_def keys_def)
lemma bulkload_tabulate:
"bulkload xs = tabulate [0..<length xs] (nth xs)"
by (rule mapping_eqI) (simp add: expand_fun_eq)
-lemma keys_tabulate:
+lemma is_empty_empty: (*FIXME*)
+ "is_empty m \<longleftrightarrow> m = Mapping Map.empty"
+ by (cases m) (simp add: is_empty_def keys_def)
+
+lemma is_empty_empty' [simp]:
+ "is_empty empty"
+ by (simp add: is_empty_empty empty_def)
+
+lemma is_empty_update [simp]:
+ "\<not> is_empty (update k v m)"
+ by (cases m) (simp add: is_empty_empty)
+
+lemma is_empty_delete:
+ "is_empty (delete k m) \<longleftrightarrow> is_empty m \<or> keys m = {k}"
+ by (cases m) (auto simp add: is_empty_empty keys_def dom_eq_empty_conv [symmetric] simp del: dom_eq_empty_conv)
+
+lemma is_empty_replace [simp]:
+ "is_empty (replace k v m) \<longleftrightarrow> is_empty m"
+ by (auto simp add: replace_def) (simp add: is_empty_def)
+
+lemma is_empty_default [simp]:
+ "\<not> is_empty (default k v m)"
+ by (auto simp add: default_def) (simp add: is_empty_def)
+
+lemma is_empty_map_entry [simp]:
+ "is_empty (map_entry k f m) \<longleftrightarrow> is_empty m"
+ by (cases "lookup m k")
+ (auto simp add: map_entry_def, simp add: is_empty_empty)
+
+lemma is_empty_map_default [simp]:
+ "\<not> is_empty (map_default k v f m)"
+ by (simp add: map_default_def)
+
+lemma keys_empty [simp]:
+ "keys empty = {}"
+ by (simp add: keys_def)
+
+lemma keys_update [simp]:
+ "keys (update k v m) = insert k (keys m)"
+ by (simp add: keys_def)
+
+lemma keys_delete [simp]:
+ "keys (delete k m) = keys m - {k}"
+ by (simp add: keys_def)
+
+lemma keys_replace [simp]:
+ "keys (replace k v m) = keys m"
+ by (auto simp add: keys_def replace_def)
+
+lemma keys_default [simp]:
+ "keys (default k v m) = insert k (keys m)"
+ by (auto simp add: keys_def default_def)
+
+lemma keys_map_entry [simp]:
+ "keys (map_entry k f m) = keys m"
+ by (auto simp add: keys_def)
+
+lemma keys_map_default [simp]:
+ "keys (map_default k v f m) = insert k (keys m)"
+ by (simp add: map_default_def)
+
+lemma keys_tabulate [simp]:
"keys (tabulate ks f) = set ks"
by (simp add: tabulate_def keys_def map_of_map_restrict o_def)
-lemma keys_bulkload:
+lemma keys_bulkload [simp]:
"keys (bulkload xs) = {0..<length xs}"
by (simp add: keys_tabulate bulkload_tabulate)
-lemma is_empty_empty:
- "is_empty m \<longleftrightarrow> m = Mapping Map.empty"
- by (cases m) (simp add: is_empty_def)
+lemma distinct_ordered_keys [simp]:
+ "distinct (ordered_keys m)"
+ by (simp add: ordered_keys_def)
+
+lemma ordered_keys_infinite [simp]:
+ "\<not> finite (keys m) \<Longrightarrow> ordered_keys m = []"
+ by (simp add: ordered_keys_def)
+
+lemma ordered_keys_empty [simp]:
+ "ordered_keys empty = []"
+ by (simp add: ordered_keys_def)
+
+lemma ordered_keys_update [simp]:
+ "k \<in> keys m \<Longrightarrow> ordered_keys (update k v m) = ordered_keys m"
+ "finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow> ordered_keys (update k v m) = insort k (ordered_keys m)"
+ by (simp_all add: ordered_keys_def) (auto simp only: sorted_list_of_set_insert [symmetric] insert_absorb)
+
+lemma ordered_keys_delete [simp]:
+ "ordered_keys (delete k m) = remove1 k (ordered_keys m)"
+proof (cases "finite (keys m)")
+ case False then show ?thesis by simp
+next
+ case True note fin = True
+ show ?thesis
+ proof (cases "k \<in> keys m")
+ case False with fin have "k \<notin> set (sorted_list_of_set (keys m))" by simp
+ with False show ?thesis by (simp add: ordered_keys_def remove1_idem)
+ next
+ case True with fin show ?thesis by (simp add: ordered_keys_def sorted_list_of_set_remove)
+ qed
+qed
+
+lemma ordered_keys_replace [simp]:
+ "ordered_keys (replace k v m) = ordered_keys m"
+ by (simp add: replace_def)
+
+lemma ordered_keys_default [simp]:
+ "k \<in> keys m \<Longrightarrow> ordered_keys (default k v m) = ordered_keys m"
+ "finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow> ordered_keys (default k v m) = insort k (ordered_keys m)"
+ by (simp_all add: default_def)
+
+lemma ordered_keys_map_entry [simp]:
+ "ordered_keys (map_entry k f m) = ordered_keys m"
+ by (simp add: ordered_keys_def)
+
+lemma ordered_keys_map_default [simp]:
+ "k \<in> keys m \<Longrightarrow> ordered_keys (map_default k v f m) = ordered_keys m"
+ "finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow> ordered_keys (map_default k v f m) = insort k (ordered_keys m)"
+ by (simp_all add: map_default_def)
+
+lemma ordered_keys_tabulate [simp]:
+ "ordered_keys (tabulate ks f) = sort (remdups ks)"
+ by (simp add: ordered_keys_def sorted_list_of_set_sort_remdups)
+
+lemma ordered_keys_bulkload [simp]:
+ "ordered_keys (bulkload ks) = [0..<length ks]"
+ by (simp add: ordered_keys_def)
subsection {* Some technical code lemmas *}