src/HOL/List.thy
 changeset 35195 5163c2d00904 parent 35115 446c5063e4fd child 35208 2b9bce05e84b
equal 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 `
`  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 *}`