src/HOL/List.thy
changeset 35195 5163c2d00904
parent 35115 446c5063e4fd
child 35208 2b9bce05e84b
equal deleted inserted replaced
35194:a6c573d13385 35195:5163c2d00904
   282 
   282 
   283 primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
   283 primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
   284 "insort_key f x [] = [x]" |
   284 "insort_key f x [] = [x]" |
   285 "insort_key f x (y#ys) = (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))"
   285 "insort_key f x (y#ys) = (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))"
   286 
   286 
   287 primrec sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where
   287 definition sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where
   288 "sort_key f [] = []" |
   288 "sort_key f xs = foldr (insort_key f) xs []"
   289 "sort_key f (x#xs) = insort_key f x (sort_key f xs)"
       
   290 
   289 
   291 abbreviation "sort \<equiv> sort_key (\<lambda>x. x)"
   290 abbreviation "sort \<equiv> sort_key (\<lambda>x. x)"
   292 abbreviation "insort \<equiv> insort_key (\<lambda>x. x)"
   291 abbreviation "insort \<equiv> insort_key (\<lambda>x. x)"
   293 
   292 
   294 end
   293 end
  2264 lemma foldr_cong [fundef_cong, recdef_cong]:
  2263 lemma foldr_cong [fundef_cong, recdef_cong]:
  2265   "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] 
  2264   "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] 
  2266   ==> foldr f l a = foldr g k b"
  2265   ==> foldr f l a = foldr g k b"
  2267 by (induct k arbitrary: a b l) simp_all
  2266 by (induct k arbitrary: a b l) simp_all
  2268 
  2267 
       
  2268 lemma foldl_fun_comm:
       
  2269   assumes "\<And>x y s. f (f s x) y = f (f s y) x"
       
  2270   shows "f (foldl f s xs) x = foldl f (f s x) xs"
       
  2271   by (induct xs arbitrary: s)
       
  2272     (simp_all add: assms)
       
  2273 
  2269 lemma (in semigroup_add) foldl_assoc:
  2274 lemma (in semigroup_add) foldl_assoc:
  2270 shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"
  2275 shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"
  2271 by (induct zs arbitrary: y) (simp_all add:add_assoc)
  2276 by (induct zs arbitrary: y) (simp_all add:add_assoc)
  2272 
  2277 
  2273 lemma (in monoid_add) foldl_absorb0:
  2278 lemma (in monoid_add) foldl_absorb0:
  2274 shows "x + (foldl op+ 0 zs) = foldl op+ x zs"
  2279 shows "x + (foldl op+ 0 zs) = foldl op+ x zs"
  2275 by (induct zs) (simp_all add:foldl_assoc)
  2280 by (induct zs) (simp_all add:foldl_assoc)
       
  2281 
       
  2282 lemma foldl_rev:
       
  2283   assumes "\<And>x y s. f (f s x) y = f (f s y) x"
       
  2284   shows "foldl f s (rev xs) = foldl f s xs"
       
  2285 proof (induct xs arbitrary: s)
       
  2286   case Nil then show ?case by simp
       
  2287 next
       
  2288   case (Cons x xs) with assms show ?case by (simp add: foldl_fun_comm)
       
  2289 qed
  2276 
  2290 
  2277 
  2291 
  2278 text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
  2292 text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
  2279 
  2293 
  2280 lemma foldl_foldr1_lemma:
  2294 lemma foldl_foldr1_lemma:
  2339 
  2353 
  2340 lemma concat_conv_foldl: "concat xss = foldl (op @) [] xss"
  2354 lemma concat_conv_foldl: "concat xss = foldl (op @) [] xss"
  2341   by (simp add: foldl_conv_concat)
  2355   by (simp add: foldl_conv_concat)
  2342 
  2356 
  2343 text {* @{const Finite_Set.fold} and @{const foldl} *}
  2357 text {* @{const Finite_Set.fold} and @{const foldl} *}
       
  2358 
       
  2359 lemma (in fun_left_comm) fold_set_remdups:
       
  2360   "fold f y (set xs) = foldl (\<lambda>y x. f x y) y (remdups xs)"
       
  2361   by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
  2344 
  2362 
  2345 lemma (in fun_left_comm_idem) fold_set:
  2363 lemma (in fun_left_comm_idem) fold_set:
  2346   "fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"
  2364   "fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"
  2347   by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
  2365   by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
  2348 
  2366 
  3435 context linorder
  3453 context linorder
  3436 begin
  3454 begin
  3437 
  3455 
  3438 lemma length_insert[simp] : "length (insort_key f x xs) = Suc (length xs)"
  3456 lemma length_insert[simp] : "length (insort_key f x xs) = Suc (length xs)"
  3439 by (induct xs, auto)
  3457 by (induct xs, auto)
       
  3458 
       
  3459 lemma insort_left_comm:
       
  3460   "insort x (insort y xs) = insort y (insort x xs)"
       
  3461   by (induct xs) auto
       
  3462 
       
  3463 lemma fun_left_comm_insort:
       
  3464   "fun_left_comm insort"
       
  3465 proof
       
  3466 qed (fact insort_left_comm)
       
  3467 
       
  3468 lemma sort_key_simps [simp]:
       
  3469   "sort_key f [] = []"
       
  3470   "sort_key f (x#xs) = insort_key f x (sort_key f xs)"
       
  3471   by (simp_all add: sort_key_def)
       
  3472 
       
  3473 lemma sort_foldl_insort:
       
  3474   "sort xs = foldl (\<lambda>ys x. insort x ys) [] xs"
       
  3475   by (simp add: sort_key_def foldr_foldl foldl_rev insort_left_comm)
  3440 
  3476 
  3441 lemma length_sort[simp]: "length (sort_key f xs) = length xs"
  3477 lemma length_sort[simp]: "length (sort_key f xs) = length xs"
  3442 by (induct xs, auto)
  3478 by (induct xs, auto)
  3443 
  3479 
  3444 lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x <= y))"
  3480 lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x <= y))"
  3798 text{* This function maps (finite) linearly ordered sets to sorted
  3834 text{* This function maps (finite) linearly ordered sets to sorted
  3799 lists. Warning: in most cases it is not a good idea to convert from
  3835 lists. Warning: in most cases it is not a good idea to convert from
  3800 sets to lists but one should convert in the other direction (via
  3836 sets to lists but one should convert in the other direction (via
  3801 @{const set}). *}
  3837 @{const set}). *}
  3802 
  3838 
  3803 
       
  3804 context linorder
  3839 context linorder
  3805 begin
  3840 begin
  3806 
  3841 
  3807 definition
  3842 definition sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
  3808  sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
  3843   "sorted_list_of_set = Finite_Set.fold insort []"
  3809  [code del]: "sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs"
  3844 
  3810 
  3845 lemma sorted_list_of_set_empty [simp]:
  3811 lemma sorted_list_of_set[simp]: "finite A \<Longrightarrow>
  3846   "sorted_list_of_set {} = []"
  3812   set(sorted_list_of_set A) = A &
  3847   by (simp add: sorted_list_of_set_def)
  3813   sorted(sorted_list_of_set A) & distinct(sorted_list_of_set A)"
  3848 
  3814 apply(simp add:sorted_list_of_set_def)
  3849 lemma sorted_list_of_set_insert [simp]:
  3815 apply(rule the1I2)
  3850   assumes "finite A"
  3816  apply(simp_all add: finite_sorted_distinct_unique)
  3851   shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
  3817 done
  3852 proof -
  3818 
  3853   interpret fun_left_comm insort by (fact fun_left_comm_insort)
  3819 lemma sorted_list_of_empty[simp]: "sorted_list_of_set {} = []"
  3854   with assms show ?thesis by (simp add: sorted_list_of_set_def fold_insert_remove)
  3820 unfolding sorted_list_of_set_def
  3855 qed
  3821 apply(subst the_equality[of _ "[]"])
  3856 
  3822 apply simp_all
  3857 lemma sorted_list_of_set [simp]:
  3823 done
  3858   "finite A \<Longrightarrow> set (sorted_list_of_set A) = A \<and> sorted (sorted_list_of_set A) 
       
  3859     \<and> distinct (sorted_list_of_set A)"
       
  3860   by (induct A rule: finite_induct) (simp_all add: set_insort sorted_insort distinct_insort)
       
  3861 
       
  3862 lemma sorted_list_of_set_sort_remdups:
       
  3863   "sorted_list_of_set (set xs) = sort (remdups xs)"
       
  3864 proof -
       
  3865   interpret fun_left_comm insort by (fact fun_left_comm_insort)
       
  3866   show ?thesis by (simp add: sort_foldl_insort sorted_list_of_set_def fold_set_remdups)
       
  3867 qed
  3824 
  3868 
  3825 end
  3869 end
  3826 
  3870 
  3827 
  3871 
  3828 subsubsection {* @{text lists}: the list-forming operator over sets *}
  3872 subsubsection {* @{text lists}: the list-forming operator over sets *}