more lemmas about sort(_key)
authorhaftmann
Wed Feb 17 16:49:38 2010 +0100 (2010-02-17)
changeset 351955163c2d00904
parent 35194 a6c573d13385
child 35196 6eab566aa609
more lemmas about sort(_key)
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Wed Feb 17 16:49:37 2010 +0100
     1.2 +++ b/src/HOL/List.thy	Wed Feb 17 16:49:38 2010 +0100
     1.3 @@ -284,9 +284,8 @@
     1.4  "insort_key f x [] = [x]" |
     1.5  "insort_key f x (y#ys) = (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))"
     1.6  
     1.7 -primrec sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where
     1.8 -"sort_key f [] = []" |
     1.9 -"sort_key f (x#xs) = insort_key f x (sort_key f xs)"
    1.10 +definition sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where
    1.11 +"sort_key f xs = foldr (insort_key f) xs []"
    1.12  
    1.13  abbreviation "sort \<equiv> sort_key (\<lambda>x. x)"
    1.14  abbreviation "insort \<equiv> insort_key (\<lambda>x. x)"
    1.15 @@ -2266,6 +2265,12 @@
    1.16    ==> foldr f l a = foldr g k b"
    1.17  by (induct k arbitrary: a b l) simp_all
    1.18  
    1.19 +lemma foldl_fun_comm:
    1.20 +  assumes "\<And>x y s. f (f s x) y = f (f s y) x"
    1.21 +  shows "f (foldl f s xs) x = foldl f (f s x) xs"
    1.22 +  by (induct xs arbitrary: s)
    1.23 +    (simp_all add: assms)
    1.24 +
    1.25  lemma (in semigroup_add) foldl_assoc:
    1.26  shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"
    1.27  by (induct zs arbitrary: y) (simp_all add:add_assoc)
    1.28 @@ -2274,6 +2279,15 @@
    1.29  shows "x + (foldl op+ 0 zs) = foldl op+ x zs"
    1.30  by (induct zs) (simp_all add:foldl_assoc)
    1.31  
    1.32 +lemma foldl_rev:
    1.33 +  assumes "\<And>x y s. f (f s x) y = f (f s y) x"
    1.34 +  shows "foldl f s (rev xs) = foldl f s xs"
    1.35 +proof (induct xs arbitrary: s)
    1.36 +  case Nil then show ?case by simp
    1.37 +next
    1.38 +  case (Cons x xs) with assms show ?case by (simp add: foldl_fun_comm)
    1.39 +qed
    1.40 +
    1.41  
    1.42  text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
    1.43  
    1.44 @@ -2342,6 +2356,10 @@
    1.45  
    1.46  text {* @{const Finite_Set.fold} and @{const foldl} *}
    1.47  
    1.48 +lemma (in fun_left_comm) fold_set_remdups:
    1.49 +  "fold f y (set xs) = foldl (\<lambda>y x. f x y) y (remdups xs)"
    1.50 +  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
    1.51 +
    1.52  lemma (in fun_left_comm_idem) fold_set:
    1.53    "fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"
    1.54    by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
    1.55 @@ -3438,6 +3456,24 @@
    1.56  lemma length_insert[simp] : "length (insort_key f x xs) = Suc (length xs)"
    1.57  by (induct xs, auto)
    1.58  
    1.59 +lemma insort_left_comm:
    1.60 +  "insort x (insort y xs) = insort y (insort x xs)"
    1.61 +  by (induct xs) auto
    1.62 +
    1.63 +lemma fun_left_comm_insort:
    1.64 +  "fun_left_comm insort"
    1.65 +proof
    1.66 +qed (fact insort_left_comm)
    1.67 +
    1.68 +lemma sort_key_simps [simp]:
    1.69 +  "sort_key f [] = []"
    1.70 +  "sort_key f (x#xs) = insort_key f x (sort_key f xs)"
    1.71 +  by (simp_all add: sort_key_def)
    1.72 +
    1.73 +lemma sort_foldl_insort:
    1.74 +  "sort xs = foldl (\<lambda>ys x. insort x ys) [] xs"
    1.75 +  by (simp add: sort_key_def foldr_foldl foldl_rev insort_left_comm)
    1.76 +
    1.77  lemma length_sort[simp]: "length (sort_key f xs) = length xs"
    1.78  by (induct xs, auto)
    1.79  
    1.80 @@ -3800,27 +3836,35 @@
    1.81  sets to lists but one should convert in the other direction (via
    1.82  @{const set}). *}
    1.83  
    1.84 -
    1.85  context linorder
    1.86  begin
    1.87  
    1.88 -definition
    1.89 - sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
    1.90 - [code del]: "sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs"
    1.91 -
    1.92 -lemma sorted_list_of_set[simp]: "finite A \<Longrightarrow>
    1.93 -  set(sorted_list_of_set A) = A &
    1.94 -  sorted(sorted_list_of_set A) & distinct(sorted_list_of_set A)"
    1.95 -apply(simp add:sorted_list_of_set_def)
    1.96 -apply(rule the1I2)
    1.97 - apply(simp_all add: finite_sorted_distinct_unique)
    1.98 -done
    1.99 -
   1.100 -lemma sorted_list_of_empty[simp]: "sorted_list_of_set {} = []"
   1.101 -unfolding sorted_list_of_set_def
   1.102 -apply(subst the_equality[of _ "[]"])
   1.103 -apply simp_all
   1.104 -done
   1.105 +definition sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
   1.106 +  "sorted_list_of_set = Finite_Set.fold insort []"
   1.107 +
   1.108 +lemma sorted_list_of_set_empty [simp]:
   1.109 +  "sorted_list_of_set {} = []"
   1.110 +  by (simp add: sorted_list_of_set_def)
   1.111 +
   1.112 +lemma sorted_list_of_set_insert [simp]:
   1.113 +  assumes "finite A"
   1.114 +  shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
   1.115 +proof -
   1.116 +  interpret fun_left_comm insort by (fact fun_left_comm_insort)
   1.117 +  with assms show ?thesis by (simp add: sorted_list_of_set_def fold_insert_remove)
   1.118 +qed
   1.119 +
   1.120 +lemma sorted_list_of_set [simp]:
   1.121 +  "finite A \<Longrightarrow> set (sorted_list_of_set A) = A \<and> sorted (sorted_list_of_set A) 
   1.122 +    \<and> distinct (sorted_list_of_set A)"
   1.123 +  by (induct A rule: finite_induct) (simp_all add: set_insort sorted_insort distinct_insort)
   1.124 +
   1.125 +lemma sorted_list_of_set_sort_remdups:
   1.126 +  "sorted_list_of_set (set xs) = sort (remdups xs)"
   1.127 +proof -
   1.128 +  interpret fun_left_comm insort by (fact fun_left_comm_insort)
   1.129 +  show ?thesis by (simp add: sort_foldl_insort sorted_list_of_set_def fold_set_remdups)
   1.130 +qed
   1.131  
   1.132  end
   1.133