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 |
718 lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys" |
717 lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys" |
719 by (induct xs) auto |
718 by (induct xs) auto |
720 |
719 |
721 lemma map_map [simp]: "map f (map g xs) = map (f \<circ> g) xs" |
720 lemma map_map [simp]: "map f (map g xs) = map (f \<circ> g) xs" |
722 by (induct xs) auto |
721 by (induct xs) auto |
|
722 |
|
723 lemma map_comp_map[simp]: "((map f) o (map g)) = map(f o g)" |
|
724 apply(rule ext) |
|
725 apply(simp) |
|
726 done |
723 |
727 |
724 lemma rev_map: "rev (map f xs) = map f (rev xs)" |
728 lemma rev_map: "rev (map f xs) = map f (rev xs)" |
725 by (induct xs) auto |
729 by (induct xs) auto |
726 |
730 |
727 lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)" |
731 lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)" |
2264 lemma foldr_cong [fundef_cong, recdef_cong]: |
2268 lemma foldr_cong [fundef_cong, recdef_cong]: |
2265 "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] |
2269 "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] |
2266 ==> foldr f l a = foldr g k b" |
2270 ==> foldr f l a = foldr g k b" |
2267 by (induct k arbitrary: a b l) simp_all |
2271 by (induct k arbitrary: a b l) simp_all |
2268 |
2272 |
|
2273 lemma foldl_fun_comm: |
|
2274 assumes "\<And>x y s. f (f s x) y = f (f s y) x" |
|
2275 shows "f (foldl f s xs) x = foldl f (f s x) xs" |
|
2276 by (induct xs arbitrary: s) |
|
2277 (simp_all add: assms) |
|
2278 |
2269 lemma (in semigroup_add) foldl_assoc: |
2279 lemma (in semigroup_add) foldl_assoc: |
2270 shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)" |
2280 shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)" |
2271 by (induct zs arbitrary: y) (simp_all add:add_assoc) |
2281 by (induct zs arbitrary: y) (simp_all add:add_assoc) |
2272 |
2282 |
2273 lemma (in monoid_add) foldl_absorb0: |
2283 lemma (in monoid_add) foldl_absorb0: |
2274 shows "x + (foldl op+ 0 zs) = foldl op+ x zs" |
2284 shows "x + (foldl op+ 0 zs) = foldl op+ x zs" |
2275 by (induct zs) (simp_all add:foldl_assoc) |
2285 by (induct zs) (simp_all add:foldl_assoc) |
|
2286 |
|
2287 lemma foldl_rev: |
|
2288 assumes "\<And>x y s. f (f s x) y = f (f s y) x" |
|
2289 shows "foldl f s (rev xs) = foldl f s xs" |
|
2290 proof (induct xs arbitrary: s) |
|
2291 case Nil then show ?case by simp |
|
2292 next |
|
2293 case (Cons x xs) with assms show ?case by (simp add: foldl_fun_comm) |
|
2294 qed |
2276 |
2295 |
2277 |
2296 |
2278 text{* The ``First Duality Theorem'' in Bird \& Wadler: *} |
2297 text{* The ``First Duality Theorem'' in Bird \& Wadler: *} |
2279 |
2298 |
2280 lemma foldl_foldr1_lemma: |
2299 lemma foldl_foldr1_lemma: |
2339 |
2358 |
2340 lemma concat_conv_foldl: "concat xss = foldl (op @) [] xss" |
2359 lemma concat_conv_foldl: "concat xss = foldl (op @) [] xss" |
2341 by (simp add: foldl_conv_concat) |
2360 by (simp add: foldl_conv_concat) |
2342 |
2361 |
2343 text {* @{const Finite_Set.fold} and @{const foldl} *} |
2362 text {* @{const Finite_Set.fold} and @{const foldl} *} |
|
2363 |
|
2364 lemma (in fun_left_comm) fold_set_remdups: |
|
2365 "fold f y (set xs) = foldl (\<lambda>y x. f x y) y (remdups xs)" |
|
2366 by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb) |
2344 |
2367 |
2345 lemma (in fun_left_comm_idem) fold_set: |
2368 lemma (in fun_left_comm_idem) fold_set: |
2346 "fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs" |
2369 "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) |
2370 by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm) |
2348 |
2371 |
3435 context linorder |
3458 context linorder |
3436 begin |
3459 begin |
3437 |
3460 |
3438 lemma length_insert[simp] : "length (insort_key f x xs) = Suc (length xs)" |
3461 lemma length_insert[simp] : "length (insort_key f x xs) = Suc (length xs)" |
3439 by (induct xs, auto) |
3462 by (induct xs, auto) |
|
3463 |
|
3464 lemma insort_left_comm: |
|
3465 "insort x (insort y xs) = insort y (insort x xs)" |
|
3466 by (induct xs) auto |
|
3467 |
|
3468 lemma fun_left_comm_insort: |
|
3469 "fun_left_comm insort" |
|
3470 proof |
|
3471 qed (fact insort_left_comm) |
|
3472 |
|
3473 lemma sort_key_simps [simp]: |
|
3474 "sort_key f [] = []" |
|
3475 "sort_key f (x#xs) = insort_key f x (sort_key f xs)" |
|
3476 by (simp_all add: sort_key_def) |
|
3477 |
|
3478 lemma sort_foldl_insort: |
|
3479 "sort xs = foldl (\<lambda>ys x. insort x ys) [] xs" |
|
3480 by (simp add: sort_key_def foldr_foldl foldl_rev insort_left_comm) |
3440 |
3481 |
3441 lemma length_sort[simp]: "length (sort_key f xs) = length xs" |
3482 lemma length_sort[simp]: "length (sort_key f xs) = length xs" |
3442 by (induct xs, auto) |
3483 by (induct xs, auto) |
3443 |
3484 |
3444 lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x <= y))" |
3485 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 |
3839 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 |
3840 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 |
3841 sets to lists but one should convert in the other direction (via |
3801 @{const set}). *} |
3842 @{const set}). *} |
3802 |
3843 |
3803 |
|
3804 context linorder |
3844 context linorder |
3805 begin |
3845 begin |
3806 |
3846 |
3807 definition |
3847 definition sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where |
3808 sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where |
3848 "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" |
3849 |
3810 |
3850 lemma sorted_list_of_set_empty [simp]: |
3811 lemma sorted_list_of_set[simp]: "finite A \<Longrightarrow> |
3851 "sorted_list_of_set {} = []" |
3812 set(sorted_list_of_set A) = A & |
3852 by (simp add: sorted_list_of_set_def) |
3813 sorted(sorted_list_of_set A) & distinct(sorted_list_of_set A)" |
3853 |
3814 apply(simp add:sorted_list_of_set_def) |
3854 lemma sorted_list_of_set_insert [simp]: |
3815 apply(rule the1I2) |
3855 assumes "finite A" |
3816 apply(simp_all add: finite_sorted_distinct_unique) |
3856 shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))" |
3817 done |
3857 proof - |
3818 |
3858 interpret fun_left_comm insort by (fact fun_left_comm_insort) |
3819 lemma sorted_list_of_empty[simp]: "sorted_list_of_set {} = []" |
3859 with assms show ?thesis by (simp add: sorted_list_of_set_def fold_insert_remove) |
3820 unfolding sorted_list_of_set_def |
3860 qed |
3821 apply(subst the_equality[of _ "[]"]) |
3861 |
3822 apply simp_all |
3862 lemma sorted_list_of_set [simp]: |
3823 done |
3863 "finite A \<Longrightarrow> set (sorted_list_of_set A) = A \<and> sorted (sorted_list_of_set A) |
|
3864 \<and> distinct (sorted_list_of_set A)" |
|
3865 by (induct A rule: finite_induct) (simp_all add: set_insort sorted_insort distinct_insort) |
|
3866 |
|
3867 lemma sorted_list_of_set_sort_remdups: |
|
3868 "sorted_list_of_set (set xs) = sort (remdups xs)" |
|
3869 proof - |
|
3870 interpret fun_left_comm insort by (fact fun_left_comm_insort) |
|
3871 show ?thesis by (simp add: sort_foldl_insort sorted_list_of_set_def fold_set_remdups) |
|
3872 qed |
3824 |
3873 |
3825 end |
3874 end |
3826 |
3875 |
3827 |
3876 |
3828 subsubsection {* @{text lists}: the list-forming operator over sets *} |
3877 subsubsection {* @{text lists}: the list-forming operator over sets *} |