merged
authorhaftmann
Thu, 18 Feb 2010 08:17:24 +0100
changeset 35197 5c5457a7be85
parent 35193 3979b0729802 (current diff)
parent 35196 6eab566aa609 (diff)
child 35198 f95c6440c1c7
child 35208 2b9bce05e84b
child 35219 15a5f213ef5b
merged
--- a/src/HOL/Library/AssocList.thy	Wed Feb 17 22:32:05 2010 +0100
+++ b/src/HOL/Library/AssocList.thy	Thu Feb 18 08:17:24 2010 +0100
@@ -688,6 +688,10 @@
   "Mapping.keys (AList xs) = set (map fst xs)"
   by (simp add: keys_def dom_map_of_conv_image_fst)
 
+lemma ordered_keys_AList [code]:
+  "Mapping.ordered_keys (AList xs) = sort (remdups (map fst xs))"
+  by (simp only: ordered_keys_def keys_AList sorted_list_of_set_sort_remdups)
+
 lemma size_AList [code]:
   "Mapping.size (AList xs) = length (remdups (map fst xs))"
   by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst)
--- a/src/HOL/Library/Mapping.thy	Wed Feb 17 22:32:05 2010 +0100
+++ b/src/HOL/Library/Mapping.thy	Thu Feb 18 08:17:24 2010 +0100
@@ -28,6 +28,9 @@
 definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set" where
   "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)"
+
 definition is_empty :: "('a, 'b) mapping \<Rightarrow> bool" where
   "is_empty m \<longleftrightarrow> dom (lookup m) = {}"
 
@@ -139,6 +142,6 @@
   by (cases m) simp
 
 
-hide (open) const empty is_empty lookup update delete keys size replace tabulate bulkload
+hide (open) const empty is_empty lookup update delete ordered_keys keys size replace tabulate bulkload
 
 end
\ No newline at end of file
--- a/src/HOL/Library/Tree.thy	Wed Feb 17 22:32:05 2010 +0100
+++ b/src/HOL/Library/Tree.thy	Thu Feb 18 08:17:24 2010 +0100
@@ -124,6 +124,9 @@
   "Mapping.update k v (Tree t) = Tree (update k v t)"
   by (simp add: Tree_def lookup_update)
 
+lemma [code, code del]:
+  "Mapping.ordered_keys = Mapping.ordered_keys " ..
+
 lemma keys_Tree [code]:
   "Mapping.keys (Tree t) = set (filter (\<lambda>k. lookup t k \<noteq> None) (remdups (keys t)))"
   by (simp add: Mapping.keys_def lookup_Tree dom_lookup)
--- a/src/HOL/List.thy	Wed Feb 17 22:32:05 2010 +0100
+++ b/src/HOL/List.thy	Thu Feb 18 08:17:24 2010 +0100
@@ -284,9 +284,8 @@
 "insort_key f x [] = [x]" |
 "insort_key f x (y#ys) = (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))"
 
-primrec sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where
-"sort_key f [] = []" |
-"sort_key f (x#xs) = insort_key f x (sort_key f xs)"
+definition sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where
+"sort_key f xs = foldr (insort_key f) xs []"
 
 abbreviation "sort \<equiv> sort_key (\<lambda>x. x)"
 abbreviation "insort \<equiv> insort_key (\<lambda>x. x)"
@@ -2266,6 +2265,12 @@
   ==> foldr f l a = foldr g k b"
 by (induct k arbitrary: a b l) simp_all
 
+lemma foldl_fun_comm:
+  assumes "\<And>x y s. f (f s x) y = f (f s y) x"
+  shows "f (foldl f s xs) x = foldl f (f s x) xs"
+  by (induct xs arbitrary: s)
+    (simp_all add: assms)
+
 lemma (in semigroup_add) foldl_assoc:
 shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"
 by (induct zs arbitrary: y) (simp_all add:add_assoc)
@@ -2274,6 +2279,15 @@
 shows "x + (foldl op+ 0 zs) = foldl op+ x zs"
 by (induct zs) (simp_all add:foldl_assoc)
 
+lemma foldl_rev:
+  assumes "\<And>x y s. f (f s x) y = f (f s y) x"
+  shows "foldl f s (rev xs) = foldl f s xs"
+proof (induct xs arbitrary: s)
+  case Nil then show ?case by simp
+next
+  case (Cons x xs) with assms show ?case by (simp add: foldl_fun_comm)
+qed
+
 
 text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
 
@@ -2342,6 +2356,10 @@
 
 text {* @{const Finite_Set.fold} and @{const foldl} *}
 
+lemma (in fun_left_comm) fold_set_remdups:
+  "fold f y (set xs) = foldl (\<lambda>y x. f x y) y (remdups xs)"
+  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
+
 lemma (in fun_left_comm_idem) fold_set:
   "fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"
   by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
@@ -3438,6 +3456,24 @@
 lemma length_insert[simp] : "length (insort_key f x xs) = Suc (length xs)"
 by (induct xs, auto)
 
+lemma insort_left_comm:
+  "insort x (insort y xs) = insort y (insort x xs)"
+  by (induct xs) auto
+
+lemma fun_left_comm_insort:
+  "fun_left_comm insort"
+proof
+qed (fact insort_left_comm)
+
+lemma sort_key_simps [simp]:
+  "sort_key f [] = []"
+  "sort_key f (x#xs) = insort_key f x (sort_key f xs)"
+  by (simp_all add: sort_key_def)
+
+lemma sort_foldl_insort:
+  "sort xs = foldl (\<lambda>ys x. insort x ys) [] xs"
+  by (simp add: sort_key_def foldr_foldl foldl_rev insort_left_comm)
+
 lemma length_sort[simp]: "length (sort_key f xs) = length xs"
 by (induct xs, auto)
 
@@ -3800,27 +3836,35 @@
 sets to lists but one should convert in the other direction (via
 @{const set}). *}
 
-
 context linorder
 begin
 
-definition
- sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
- [code del]: "sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs"
-
-lemma sorted_list_of_set[simp]: "finite A \<Longrightarrow>
-  set(sorted_list_of_set A) = A &
-  sorted(sorted_list_of_set A) & distinct(sorted_list_of_set A)"
-apply(simp add:sorted_list_of_set_def)
-apply(rule the1I2)
- apply(simp_all add: finite_sorted_distinct_unique)
-done
-
-lemma sorted_list_of_empty[simp]: "sorted_list_of_set {} = []"
-unfolding sorted_list_of_set_def
-apply(subst the_equality[of _ "[]"])
-apply simp_all
-done
+definition sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
+  "sorted_list_of_set = Finite_Set.fold insort []"
+
+lemma sorted_list_of_set_empty [simp]:
+  "sorted_list_of_set {} = []"
+  by (simp add: sorted_list_of_set_def)
+
+lemma sorted_list_of_set_insert [simp]:
+  assumes "finite A"
+  shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
+proof -
+  interpret fun_left_comm insort by (fact fun_left_comm_insort)
+  with assms show ?thesis by (simp add: sorted_list_of_set_def fold_insert_remove)
+qed
+
+lemma sorted_list_of_set [simp]:
+  "finite A \<Longrightarrow> set (sorted_list_of_set A) = A \<and> sorted (sorted_list_of_set A) 
+    \<and> distinct (sorted_list_of_set A)"
+  by (induct A rule: finite_induct) (simp_all add: set_insort sorted_insort distinct_insort)
+
+lemma sorted_list_of_set_sort_remdups:
+  "sorted_list_of_set (set xs) = sort (remdups xs)"
+proof -
+  interpret fun_left_comm insort by (fact fun_left_comm_insort)
+  show ?thesis by (simp add: sort_foldl_insort sorted_list_of_set_def fold_set_remdups)
+qed
 
 end