1.1 --- a/src/HOL/Library/AssocList.thy Fri May 21 10:40:59 2010 +0200
1.2 +++ b/src/HOL/Library/AssocList.thy Fri May 21 15:28:25 2010 +0200
1.3 @@ -668,6 +668,10 @@
1.4 "Mapping.lookup (Mapping xs) = map_of xs"
1.5 by (simp add: Mapping_def)
1.6
1.7 +lemma keys_Mapping [simp, code]:
1.8 + "Mapping.keys (Mapping xs) = set (map fst xs)"
1.9 + by (simp add: keys_def dom_map_of_conv_image_fst)
1.10 +
1.11 lemma empty_Mapping [code]:
1.12 "Mapping.empty = Mapping []"
1.13 by (rule mapping_eqI) simp
1.14 @@ -684,13 +688,9 @@
1.15 "Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
1.16 by (rule mapping_eqI) (simp add: delete_conv')
1.17
1.18 -lemma keys_Mapping [code]:
1.19 - "Mapping.keys (Mapping xs) = set (map fst xs)"
1.20 - by (simp add: keys_def dom_map_of_conv_image_fst)
1.21 -
1.22 lemma ordered_keys_Mapping [code]:
1.23 "Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))"
1.24 - by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups)
1.25 + by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups) simp
1.26
1.27 lemma size_Mapping [code]:
1.28 "Mapping.size (Mapping xs) = length (remdups (map fst xs))"
1.29 @@ -704,4 +704,7 @@
1.30 "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
1.31 by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
1.32
1.33 +lemma [code, code del]:
1.34 + "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
1.35 +
1.36 end
2.1 --- a/src/HOL/Library/Efficient_Nat.thy Fri May 21 10:40:59 2010 +0200
2.2 +++ b/src/HOL/Library/Efficient_Nat.thy Fri May 21 15:28:25 2010 +0200
2.3 @@ -252,7 +252,7 @@
2.4 *}
2.5
2.6 code_include Haskell "Nat" {*
2.7 -newtype Nat = Nat Integer deriving (Show, Eq);
2.8 +newtype Nat = Nat Integer deriving (Eq, Show, Read);
2.9
2.10 instance Num Nat where {
2.11 fromInteger k = Nat (if k >= 0 then k else 0);
3.1 --- a/src/HOL/Library/Mapping.thy Fri May 21 10:40:59 2010 +0200
3.2 +++ b/src/HOL/Library/Mapping.thy Fri May 21 15:28:25 2010 +0200
3.3 @@ -6,6 +6,30 @@
3.4 imports Main
3.5 begin
3.6
3.7 +lemma remove1_idem: (*FIXME move to List.thy*)
3.8 + assumes "x \<notin> set xs"
3.9 + shows "remove1 x xs = xs"
3.10 + using assms by (induct xs) simp_all
3.11 +
3.12 +lemma remove1_insort [simp]:
3.13 + "remove1 x (insort x xs) = xs"
3.14 + by (induct xs) simp_all
3.15 +
3.16 +lemma sorted_list_of_set_remove:
3.17 + assumes "finite A"
3.18 + shows "sorted_list_of_set (A - {x}) = remove1 x (sorted_list_of_set A)"
3.19 +proof (cases "x \<in> A")
3.20 + case False with assms have "x \<notin> set (sorted_list_of_set A)" by simp
3.21 + with False show ?thesis by (simp add: remove1_idem)
3.22 +next
3.23 + case True then obtain B where A: "A = insert x B" by (rule Set.set_insert)
3.24 + with assms show ?thesis by simp
3.25 +qed
3.26 +
3.27 +lemma sorted_list_of_set_range [simp]:
3.28 + "sorted_list_of_set {m..<n} = [m..<n]"
3.29 + by (rule sorted_distinct_set_unique) simp_all
3.30 +
3.31 subsection {* Type definition and primitive operations *}
3.32
3.33 datatype ('a, 'b) mapping = Mapping "'a \<rightharpoonup> 'b"
3.34 @@ -29,19 +53,19 @@
3.35 "keys m = dom (lookup m)"
3.36
3.37 definition ordered_keys :: "('a\<Colon>linorder, 'b) mapping \<Rightarrow> 'a list" where
3.38 - "ordered_keys m = sorted_list_of_set (keys m)"
3.39 + "ordered_keys m = (if finite (keys m) then sorted_list_of_set (keys m) else [])"
3.40
3.41 definition is_empty :: "('a, 'b) mapping \<Rightarrow> bool" where
3.42 - "is_empty m \<longleftrightarrow> dom (lookup m) = {}"
3.43 + "is_empty m \<longleftrightarrow> keys m = {}"
3.44
3.45 definition size :: "('a, 'b) mapping \<Rightarrow> nat" where
3.46 - "size m = (if finite (dom (lookup m)) then card (dom (lookup m)) else 0)"
3.47 + "size m = (if finite (keys m) then card (keys m) else 0)"
3.48
3.49 definition replace :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
3.50 - "replace k v m = (if lookup m k = None then m else update k v m)"
3.51 + "replace k v m = (if k \<in> keys m then update k v m else m)"
3.52
3.53 definition default :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
3.54 - "default k v m = (if lookup m k = None then update k v m else m)"
3.55 + "default k v m = (if k \<in> keys m then m else update k v m)"
3.56
3.57 definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
3.58 "map_entry k f m = (case lookup m k of None \<Rightarrow> m
3.59 @@ -68,6 +92,10 @@
3.60 shows "m = n"
3.61 using assms by simp
3.62
3.63 +lemma keys_is_none_lookup [code_inline]:
3.64 + "k \<in> keys m \<longleftrightarrow> \<not> (Option.is_none (lookup m k))"
3.65 + by (auto simp add: keys_def is_none_def)
3.66 +
3.67 lemma lookup_empty [simp]:
3.68 "lookup empty = Map.empty"
3.69 by (simp add: empty_def)
3.70 @@ -111,42 +139,157 @@
3.71 by (rule mapping_eqI) simp
3.72
3.73 lemma replace_update:
3.74 - "k \<notin> dom (lookup m) \<Longrightarrow> replace k v m = m"
3.75 - "k \<in> dom (lookup m) \<Longrightarrow> replace k v m = update k v m"
3.76 - by (rule mapping_eqI, auto simp add: replace_def fun_upd_twist)+
3.77 + "k \<notin> keys m \<Longrightarrow> replace k v m = m"
3.78 + "k \<in> keys m \<Longrightarrow> replace k v m = update k v m"
3.79 + by (rule mapping_eqI) (auto simp add: replace_def fun_upd_twist)+
3.80
3.81 lemma size_empty [simp]:
3.82 "size empty = 0"
3.83 - by (simp add: size_def)
3.84 + by (simp add: size_def keys_def)
3.85
3.86 lemma size_update:
3.87 - "finite (dom (lookup m)) \<Longrightarrow> size (update k v m) =
3.88 - (if k \<in> dom (lookup m) then size m else Suc (size m))"
3.89 - by (auto simp add: size_def insert_dom)
3.90 + "finite (keys m) \<Longrightarrow> size (update k v m) =
3.91 + (if k \<in> keys m then size m else Suc (size m))"
3.92 + by (auto simp add: size_def insert_dom keys_def)
3.93
3.94 lemma size_delete:
3.95 - "size (delete k m) = (if k \<in> dom (lookup m) then size m - 1 else size m)"
3.96 - by (simp add: size_def)
3.97 + "size (delete k m) = (if k \<in> keys m then size m - 1 else size m)"
3.98 + by (simp add: size_def keys_def)
3.99
3.100 -lemma size_tabulate:
3.101 +lemma size_tabulate [simp]:
3.102 "size (tabulate ks f) = length (remdups ks)"
3.103 - by (simp add: size_def distinct_card [of "remdups ks", symmetric] comp_def)
3.104 + by (simp add: size_def distinct_card [of "remdups ks", symmetric] comp_def keys_def)
3.105
3.106 lemma bulkload_tabulate:
3.107 "bulkload xs = tabulate [0..<length xs] (nth xs)"
3.108 by (rule mapping_eqI) (simp add: expand_fun_eq)
3.109
3.110 -lemma keys_tabulate:
3.111 +lemma is_empty_empty: (*FIXME*)
3.112 + "is_empty m \<longleftrightarrow> m = Mapping Map.empty"
3.113 + by (cases m) (simp add: is_empty_def keys_def)
3.114 +
3.115 +lemma is_empty_empty' [simp]:
3.116 + "is_empty empty"
3.117 + by (simp add: is_empty_empty empty_def)
3.118 +
3.119 +lemma is_empty_update [simp]:
3.120 + "\<not> is_empty (update k v m)"
3.121 + by (cases m) (simp add: is_empty_empty)
3.122 +
3.123 +lemma is_empty_delete:
3.124 + "is_empty (delete k m) \<longleftrightarrow> is_empty m \<or> keys m = {k}"
3.125 + by (cases m) (auto simp add: is_empty_empty keys_def dom_eq_empty_conv [symmetric] simp del: dom_eq_empty_conv)
3.126 +
3.127 +lemma is_empty_replace [simp]:
3.128 + "is_empty (replace k v m) \<longleftrightarrow> is_empty m"
3.129 + by (auto simp add: replace_def) (simp add: is_empty_def)
3.130 +
3.131 +lemma is_empty_default [simp]:
3.132 + "\<not> is_empty (default k v m)"
3.133 + by (auto simp add: default_def) (simp add: is_empty_def)
3.134 +
3.135 +lemma is_empty_map_entry [simp]:
3.136 + "is_empty (map_entry k f m) \<longleftrightarrow> is_empty m"
3.137 + by (cases "lookup m k")
3.138 + (auto simp add: map_entry_def, simp add: is_empty_empty)
3.139 +
3.140 +lemma is_empty_map_default [simp]:
3.141 + "\<not> is_empty (map_default k v f m)"
3.142 + by (simp add: map_default_def)
3.143 +
3.144 +lemma keys_empty [simp]:
3.145 + "keys empty = {}"
3.146 + by (simp add: keys_def)
3.147 +
3.148 +lemma keys_update [simp]:
3.149 + "keys (update k v m) = insert k (keys m)"
3.150 + by (simp add: keys_def)
3.151 +
3.152 +lemma keys_delete [simp]:
3.153 + "keys (delete k m) = keys m - {k}"
3.154 + by (simp add: keys_def)
3.155 +
3.156 +lemma keys_replace [simp]:
3.157 + "keys (replace k v m) = keys m"
3.158 + by (auto simp add: keys_def replace_def)
3.159 +
3.160 +lemma keys_default [simp]:
3.161 + "keys (default k v m) = insert k (keys m)"
3.162 + by (auto simp add: keys_def default_def)
3.163 +
3.164 +lemma keys_map_entry [simp]:
3.165 + "keys (map_entry k f m) = keys m"
3.166 + by (auto simp add: keys_def)
3.167 +
3.168 +lemma keys_map_default [simp]:
3.169 + "keys (map_default k v f m) = insert k (keys m)"
3.170 + by (simp add: map_default_def)
3.171 +
3.172 +lemma keys_tabulate [simp]:
3.173 "keys (tabulate ks f) = set ks"
3.174 by (simp add: tabulate_def keys_def map_of_map_restrict o_def)
3.175
3.176 -lemma keys_bulkload:
3.177 +lemma keys_bulkload [simp]:
3.178 "keys (bulkload xs) = {0..<length xs}"
3.179 by (simp add: keys_tabulate bulkload_tabulate)
3.180
3.181 -lemma is_empty_empty:
3.182 - "is_empty m \<longleftrightarrow> m = Mapping Map.empty"
3.183 - by (cases m) (simp add: is_empty_def)
3.184 +lemma distinct_ordered_keys [simp]:
3.185 + "distinct (ordered_keys m)"
3.186 + by (simp add: ordered_keys_def)
3.187 +
3.188 +lemma ordered_keys_infinite [simp]:
3.189 + "\<not> finite (keys m) \<Longrightarrow> ordered_keys m = []"
3.190 + by (simp add: ordered_keys_def)
3.191 +
3.192 +lemma ordered_keys_empty [simp]:
3.193 + "ordered_keys empty = []"
3.194 + by (simp add: ordered_keys_def)
3.195 +
3.196 +lemma ordered_keys_update [simp]:
3.197 + "k \<in> keys m \<Longrightarrow> ordered_keys (update k v m) = ordered_keys m"
3.198 + "finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow> ordered_keys (update k v m) = insort k (ordered_keys m)"
3.199 + by (simp_all add: ordered_keys_def) (auto simp only: sorted_list_of_set_insert [symmetric] insert_absorb)
3.200 +
3.201 +lemma ordered_keys_delete [simp]:
3.202 + "ordered_keys (delete k m) = remove1 k (ordered_keys m)"
3.203 +proof (cases "finite (keys m)")
3.204 + case False then show ?thesis by simp
3.205 +next
3.206 + case True note fin = True
3.207 + show ?thesis
3.208 + proof (cases "k \<in> keys m")
3.209 + case False with fin have "k \<notin> set (sorted_list_of_set (keys m))" by simp
3.210 + with False show ?thesis by (simp add: ordered_keys_def remove1_idem)
3.211 + next
3.212 + case True with fin show ?thesis by (simp add: ordered_keys_def sorted_list_of_set_remove)
3.213 + qed
3.214 +qed
3.215 +
3.216 +lemma ordered_keys_replace [simp]:
3.217 + "ordered_keys (replace k v m) = ordered_keys m"
3.218 + by (simp add: replace_def)
3.219 +
3.220 +lemma ordered_keys_default [simp]:
3.221 + "k \<in> keys m \<Longrightarrow> ordered_keys (default k v m) = ordered_keys m"
3.222 + "finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow> ordered_keys (default k v m) = insort k (ordered_keys m)"
3.223 + by (simp_all add: default_def)
3.224 +
3.225 +lemma ordered_keys_map_entry [simp]:
3.226 + "ordered_keys (map_entry k f m) = ordered_keys m"
3.227 + by (simp add: ordered_keys_def)
3.228 +
3.229 +lemma ordered_keys_map_default [simp]:
3.230 + "k \<in> keys m \<Longrightarrow> ordered_keys (map_default k v f m) = ordered_keys m"
3.231 + "finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow> ordered_keys (map_default k v f m) = insort k (ordered_keys m)"
3.232 + by (simp_all add: map_default_def)
3.233 +
3.234 +lemma ordered_keys_tabulate [simp]:
3.235 + "ordered_keys (tabulate ks f) = sort (remdups ks)"
3.236 + by (simp add: ordered_keys_def sorted_list_of_set_sort_remdups)
3.237 +
3.238 +lemma ordered_keys_bulkload [simp]:
3.239 + "ordered_keys (bulkload ks) = [0..<length ks]"
3.240 + by (simp add: ordered_keys_def)
3.241
3.242
3.243 subsection {* Some technical code lemmas *}
4.1 --- a/src/HOL/Library/RBT.thy Fri May 21 10:40:59 2010 +0200
4.2 +++ b/src/HOL/Library/RBT.thy Fri May 21 15:28:25 2010 +0200
4.3 @@ -222,7 +222,8 @@
4.4 "Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
4.5 by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
4.6
4.7 -lemma [code, code del]: "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
4.8 +lemma [code, code del]:
4.9 + "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
4.10
4.11 lemma eq_Mapping [code]:
4.12 "HOL.eq (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"