234 @{lemma "tl [a,b,c,d] = [b,c,d]" by simp}\\ |
241 @{lemma "tl [a,b,c,d] = [b,c,d]" by simp}\\ |
235 @{lemma "last [a,b,c,d] = d" by simp}\\ |
242 @{lemma "last [a,b,c,d] = d" by simp}\\ |
236 @{lemma "butlast [a,b,c,d] = [a,b,c]" by simp}\\ |
243 @{lemma "butlast [a,b,c,d] = [a,b,c]" by simp}\\ |
237 @{lemma[source] "filter (\<lambda>n::nat. n<2) [0,2,1] = [0,1]" by simp}\\ |
244 @{lemma[source] "filter (\<lambda>n::nat. n<2) [0,2,1] = [0,1]" by simp}\\ |
238 @{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" by simp}\\ |
245 @{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" by simp}\\ |
239 @{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\ |
246 @{lemma "fold f [a,b,c] x = f c (f b (f a x))" by simp}\\ |
240 @{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by simp}\\ |
247 @{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by (simp add: foldr_def)}\\ |
|
248 @{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by (simp add: foldl_def)}\\ |
241 @{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\ |
249 @{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\ |
242 @{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\ |
250 @{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\ |
243 @{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\ |
251 @{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\ |
244 @{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\ |
252 @{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\ |
245 @{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\ |
253 @{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\ |
259 @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\ |
267 @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\ |
260 @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by (simp add:rotate1_def)}\\ |
268 @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by (simp add:rotate1_def)}\\ |
261 @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def eval_nat_numeral)}\\ |
269 @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def eval_nat_numeral)}\\ |
262 @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\ |
270 @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\ |
263 @{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}\\ |
271 @{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}\\ |
264 @{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def)} |
272 @{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def foldr_def)} |
265 \end{tabular}} |
273 \end{tabular}} |
266 \caption{Characteristic examples} |
274 \caption{Characteristic examples} |
267 \label{fig:Characteristic} |
275 \label{fig:Characteristic} |
268 \end{figure} |
276 \end{figure} |
269 Figure~\ref{fig:Characteristic} shows characteristic examples |
277 Figure~\ref{fig:Characteristic} shows characteristic examples |
2366 lemma list_eq_iff_zip_eq: |
2377 lemma list_eq_iff_zip_eq: |
2367 "xs = ys \<longleftrightarrow> length xs = length ys \<and> (\<forall>(x,y) \<in> set (zip xs ys). x = y)" |
2378 "xs = ys \<longleftrightarrow> length xs = length ys \<and> (\<forall>(x,y) \<in> set (zip xs ys). x = y)" |
2368 by(auto simp add: set_zip list_all2_eq list_all2_conv_all_nth cong: conj_cong) |
2379 by(auto simp add: set_zip list_all2_eq list_all2_conv_all_nth cong: conj_cong) |
2369 |
2380 |
2370 |
2381 |
2371 subsubsection {* @{text foldl} and @{text foldr} *} |
2382 subsubsection {* @{const fold} with canonical argument order *} |
2372 |
2383 |
2373 lemma foldl_append [simp]: |
2384 lemma fold_remove1_split: |
2374 "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys" |
2385 assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" |
2375 by (induct xs arbitrary: a) auto |
2386 and x: "x \<in> set xs" |
2376 |
2387 shows "fold f xs = fold f (remove1 x xs) \<circ> f x" |
2377 lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)" |
2388 using assms by (induct xs) (auto simp add: o_assoc [symmetric]) |
2378 by (induct xs) auto |
2389 |
2379 |
2390 lemma fold_cong [fundef_cong]: |
2380 lemma foldr_map: "foldr g (map f xs) a = foldr (g o f) xs a" |
2391 "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x) |
2381 by(induct xs) simp_all |
2392 \<Longrightarrow> fold f xs a = fold g ys b" |
2382 |
2393 by (induct ys arbitrary: a b xs) simp_all |
2383 text{* For efficient code generation: avoid intermediate list. *} |
2394 |
2384 lemma foldl_map[code_unfold]: |
2395 lemma fold_id: |
2385 "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs" |
2396 assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = id" |
2386 by(induct xs arbitrary:a) simp_all |
2397 shows "fold f xs = id" |
2387 |
2398 using assms by (induct xs) simp_all |
2388 lemma foldl_apply: |
2399 |
2389 assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x \<circ> h = h \<circ> g x" |
2400 lemma fold_commute: |
2390 shows "foldl (\<lambda>s x. f x s) (h s) xs = h (foldl (\<lambda>s x. g x s) s xs)" |
2401 assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h" |
2391 by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: fun_eq_iff) |
2402 shows "h \<circ> fold g xs = fold f xs \<circ> h" |
2392 |
2403 using assms by (induct xs) (simp_all add: fun_eq_iff) |
2393 lemma foldl_cong [fundef_cong]: |
2404 |
2394 "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] |
2405 lemma fold_commute_apply: |
2395 ==> foldl f a l = foldl g b k" |
2406 assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h" |
2396 by (induct k arbitrary: a b l) simp_all |
2407 shows "h (fold g xs s) = fold f xs (h s)" |
2397 |
2408 proof - |
2398 lemma foldr_cong [fundef_cong]: |
2409 from assms have "h \<circ> fold g xs = fold f xs \<circ> h" by (rule fold_commute) |
2399 "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] |
2410 then show ?thesis by (simp add: fun_eq_iff) |
2400 ==> foldr f l a = foldr g k b" |
2411 qed |
2401 by (induct k arbitrary: a b l) simp_all |
2412 |
2402 |
2413 lemma fold_invariant: |
2403 lemma foldl_fun_comm: |
2414 assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s" |
2404 assumes "\<And>x y s. f (f s x) y = f (f s y) x" |
2415 and "\<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s)" |
2405 shows "f (foldl f s xs) x = foldl f (f s x) xs" |
2416 shows "P (fold f xs s)" |
2406 by (induct xs arbitrary: s) |
|
2407 (simp_all add: assms) |
|
2408 |
|
2409 lemma (in semigroup_add) foldl_assoc: |
|
2410 shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)" |
|
2411 by (induct zs arbitrary: y) (simp_all add:add_assoc) |
|
2412 |
|
2413 lemma (in monoid_add) foldl_absorb0: |
|
2414 shows "x + (foldl op+ 0 zs) = foldl op+ x zs" |
|
2415 by (induct zs) (simp_all add:foldl_assoc) |
|
2416 |
|
2417 lemma foldl_rev: |
|
2418 assumes "\<And>x y s. f (f s x) y = f (f s y) x" |
|
2419 shows "foldl f s (rev xs) = foldl f s xs" |
|
2420 proof (induct xs arbitrary: s) |
|
2421 case Nil then show ?case by simp |
|
2422 next |
|
2423 case (Cons x xs) with assms show ?case by (simp add: foldl_fun_comm) |
|
2424 qed |
|
2425 |
|
2426 lemma rev_foldl_cons [code]: |
|
2427 "rev xs = foldl (\<lambda>xs x. x # xs) [] xs" |
|
2428 proof (induct xs) |
|
2429 case Nil then show ?case by simp |
|
2430 next |
|
2431 case Cons |
|
2432 { |
|
2433 fix x xs ys |
|
2434 have "foldl (\<lambda>xs x. x # xs) ys xs @ [x] |
|
2435 = foldl (\<lambda>xs x. x # xs) (ys @ [x]) xs" |
|
2436 by (induct xs arbitrary: ys) auto |
|
2437 } |
|
2438 note aux = this |
|
2439 show ?case by (induct xs) (auto simp add: Cons aux) |
|
2440 qed |
|
2441 |
|
2442 |
|
2443 text{* The ``Third Duality Theorem'' in Bird \& Wadler: *} |
|
2444 |
|
2445 lemma foldr_foldl: |
|
2446 "foldr f xs a = foldl (%x y. f y x) a (rev xs)" |
|
2447 by (induct xs) auto |
|
2448 |
|
2449 lemma foldl_foldr: |
|
2450 "foldl f a xs = foldr (%x y. f y x) (rev xs) a" |
|
2451 by (simp add: foldr_foldl [of "%x y. f y x" "rev xs"]) |
|
2452 |
|
2453 |
|
2454 text{* The ``First Duality Theorem'' in Bird \& Wadler: *} |
|
2455 |
|
2456 lemma (in monoid_add) foldl_foldr1_lemma: |
|
2457 "foldl op + a xs = a + foldr op + xs 0" |
|
2458 by (induct xs arbitrary: a) (auto simp: add_assoc) |
|
2459 |
|
2460 corollary (in monoid_add) foldl_foldr1: |
|
2461 "foldl op + 0 xs = foldr op + xs 0" |
|
2462 by (simp add: foldl_foldr1_lemma) |
|
2463 |
|
2464 lemma (in ab_semigroup_add) foldr_conv_foldl: |
|
2465 "foldr op + xs a = foldl op + a xs" |
|
2466 by (induct xs) (simp_all add: foldl_assoc add.commute) |
|
2467 |
|
2468 text {* |
|
2469 Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more |
|
2470 difficult to use because it requires an additional transitivity step. |
|
2471 *} |
|
2472 |
|
2473 lemma start_le_sum: "(m::nat) <= n ==> m <= foldl (op +) n ns" |
|
2474 by (induct ns arbitrary: n) auto |
|
2475 |
|
2476 lemma elem_le_sum: "(n::nat) : set ns ==> n <= foldl (op +) 0 ns" |
|
2477 by (force intro: start_le_sum simp add: in_set_conv_decomp) |
|
2478 |
|
2479 lemma sum_eq_0_conv [iff]: |
|
2480 "(foldl (op +) (m::nat) ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))" |
|
2481 by (induct ns arbitrary: m) auto |
|
2482 |
|
2483 lemma foldr_invariant: |
|
2484 "\<lbrakk>Q x ; \<forall> x\<in> set xs. P x; \<forall> x y. P x \<and> Q y \<longrightarrow> Q (f x y) \<rbrakk> \<Longrightarrow> Q (foldr f xs x)" |
|
2485 by (induct xs, simp_all) |
|
2486 |
|
2487 lemma foldl_invariant: |
|
2488 "\<lbrakk>Q x ; \<forall> x\<in> set xs. P x; \<forall> x y. P x \<and> Q y \<longrightarrow> Q (f y x) \<rbrakk> \<Longrightarrow> Q (foldl f x xs)" |
|
2489 by (induct xs arbitrary: x, simp_all) |
|
2490 |
|
2491 lemma foldl_weak_invariant: |
|
2492 assumes "P s" |
|
2493 and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f s x)" |
|
2494 shows "P (foldl f s xs)" |
|
2495 using assms by (induct xs arbitrary: s) simp_all |
2417 using assms by (induct xs arbitrary: s) simp_all |
2496 |
2418 |
2497 text {* @{const foldl} and @{const concat} *} |
2419 lemma fold_append [simp]: |
2498 |
2420 "fold f (xs @ ys) = fold f ys \<circ> fold f xs" |
2499 lemma foldl_conv_concat: |
2421 by (induct xs) simp_all |
2500 "foldl (op @) xs xss = xs @ concat xss" |
2422 |
2501 proof (induct xss arbitrary: xs) |
2423 lemma fold_map [code_unfold]: |
2502 case Nil show ?case by simp |
2424 "fold g (map f xs) = fold (g o f) xs" |
2503 next |
2425 by (induct xs) simp_all |
2504 interpret monoid_add "op @" "[]" proof qed simp_all |
2426 |
2505 case Cons then show ?case by (simp add: foldl_absorb0) |
2427 lemma fold_rev: |
2506 qed |
2428 assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y" |
2507 |
2429 shows "fold f (rev xs) = fold f xs" |
2508 lemma concat_conv_foldl: "concat xss = foldl (op @) [] xss" |
2430 using assms by (induct xs) (simp_all add: fold_commute_apply fun_eq_iff) |
2509 by (simp add: foldl_conv_concat) |
2431 |
2510 |
2432 lemma fold_Cons_rev: |
2511 text {* @{const Finite_Set.fold} and @{const foldl} *} |
2433 "fold Cons xs = append (rev xs)" |
2512 |
2434 by (induct xs) simp_all |
2513 lemma (in comp_fun_commute) fold_set_remdups: |
2435 |
2514 "Finite_Set.fold f y (set xs) = foldl (\<lambda>y x. f x y) y (remdups xs)" |
2436 lemma rev_conv_fold [code]: |
|
2437 "rev xs = fold Cons xs []" |
|
2438 by (simp add: fold_Cons_rev) |
|
2439 |
|
2440 lemma fold_append_concat_rev: |
|
2441 "fold append xss = append (concat (rev xss))" |
|
2442 by (induct xss) simp_all |
|
2443 |
|
2444 text {* @{const Finite_Set.fold} and @{const fold} *} |
|
2445 |
|
2446 lemma (in comp_fun_commute) fold_set_fold_remdups: |
|
2447 "Finite_Set.fold f y (set xs) = fold f (remdups xs) y" |
2515 by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb) |
2448 by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb) |
2516 |
2449 |
2517 lemma (in comp_fun_idem) fold_set: |
2450 lemma (in comp_fun_idem) fold_set_fold: |
2518 "Finite_Set.fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs" |
2451 "Finite_Set.fold f y (set xs) = fold f xs y" |
2519 by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm) |
2452 by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm) |
2520 |
2453 |
2521 lemma (in ab_semigroup_idem_mult) fold1_set: |
2454 lemma (in ab_semigroup_idem_mult) fold1_set_fold: |
2522 assumes "xs \<noteq> []" |
2455 assumes "xs \<noteq> []" |
2523 shows "fold1 times (set xs) = foldl times (hd xs) (tl xs)" |
2456 shows "Finite_Set.fold1 times (set xs) = fold times (tl xs) (hd xs)" |
2524 proof - |
2457 proof - |
2525 interpret comp_fun_idem times by (fact comp_fun_idem) |
2458 interpret comp_fun_idem times by (fact comp_fun_idem) |
2526 from assms obtain y ys where xs: "xs = y # ys" |
2459 from assms obtain y ys where xs: "xs = y # ys" |
2527 by (cases xs) auto |
2460 by (cases xs) auto |
2528 show ?thesis |
2461 show ?thesis |
2530 case True with xs show ?thesis by simp |
2463 case True with xs show ?thesis by simp |
2531 next |
2464 next |
2532 case False |
2465 case False |
2533 then have "fold1 times (insert y (set ys)) = Finite_Set.fold times y (set ys)" |
2466 then have "fold1 times (insert y (set ys)) = Finite_Set.fold times y (set ys)" |
2534 by (simp only: finite_set fold1_eq_fold_idem) |
2467 by (simp only: finite_set fold1_eq_fold_idem) |
2535 with xs show ?thesis by (simp add: fold_set mult_commute) |
2468 with xs show ?thesis by (simp add: fold_set_fold mult_commute) |
2536 qed |
2469 qed |
2537 qed |
2470 qed |
|
2471 |
|
2472 lemma (in lattice) Inf_fin_set_fold: |
|
2473 "Inf_fin (set (x # xs)) = fold inf xs x" |
|
2474 proof - |
|
2475 interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
2476 by (fact ab_semigroup_idem_mult_inf) |
|
2477 show ?thesis |
|
2478 by (simp add: Inf_fin_def fold1_set_fold del: set.simps) |
|
2479 qed |
|
2480 |
|
2481 lemma (in lattice) Sup_fin_set_fold: |
|
2482 "Sup_fin (set (x # xs)) = fold sup xs x" |
|
2483 proof - |
|
2484 interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
2485 by (fact ab_semigroup_idem_mult_sup) |
|
2486 show ?thesis |
|
2487 by (simp add: Sup_fin_def fold1_set_fold del: set.simps) |
|
2488 qed |
|
2489 |
|
2490 lemma (in linorder) Min_fin_set_fold: |
|
2491 "Min (set (x # xs)) = fold min xs x" |
|
2492 proof - |
|
2493 interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
2494 by (fact ab_semigroup_idem_mult_min) |
|
2495 show ?thesis |
|
2496 by (simp add: Min_def fold1_set_fold del: set.simps) |
|
2497 qed |
|
2498 |
|
2499 lemma (in linorder) Max_fin_set_fold: |
|
2500 "Max (set (x # xs)) = fold max xs x" |
|
2501 proof - |
|
2502 interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
2503 by (fact ab_semigroup_idem_mult_max) |
|
2504 show ?thesis |
|
2505 by (simp add: Max_def fold1_set_fold del: set.simps) |
|
2506 qed |
|
2507 |
|
2508 lemma (in complete_lattice) Inf_set_fold: |
|
2509 "Inf (set xs) = fold inf xs top" |
|
2510 proof - |
|
2511 interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
2512 by (fact comp_fun_idem_inf) |
|
2513 show ?thesis by (simp add: Inf_fold_inf fold_set_fold inf_commute) |
|
2514 qed |
|
2515 |
|
2516 lemma (in complete_lattice) Sup_set_fold: |
|
2517 "Sup (set xs) = fold sup xs bot" |
|
2518 proof - |
|
2519 interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
2520 by (fact comp_fun_idem_sup) |
|
2521 show ?thesis by (simp add: Sup_fold_sup fold_set_fold sup_commute) |
|
2522 qed |
|
2523 |
|
2524 lemma (in complete_lattice) INF_set_fold: |
|
2525 "INFI (set xs) f = fold (inf \<circ> f) xs top" |
|
2526 unfolding INF_def set_map [symmetric] Inf_set_fold fold_map .. |
|
2527 |
|
2528 lemma (in complete_lattice) SUP_set_fold: |
|
2529 "SUPR (set xs) f = fold (sup \<circ> f) xs bot" |
|
2530 unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map .. |
|
2531 |
|
2532 |
|
2533 subsubsection {* Fold variants: @{const foldr} and @{const foldl} *} |
|
2534 |
|
2535 text {* Correspondence *} |
|
2536 |
|
2537 lemma foldr_foldl: -- {* The ``Third Duality Theorem'' in Bird \& Wadler: *} |
|
2538 "foldr f xs a = foldl (\<lambda>x y. f y x) a (rev xs)" |
|
2539 by (simp add: foldr_def foldl_def) |
|
2540 |
|
2541 lemma foldl_foldr: |
|
2542 "foldl f a xs = foldr (\<lambda>x y. f y x) (rev xs) a" |
|
2543 by (simp add: foldr_def foldl_def) |
|
2544 |
|
2545 lemma foldr_fold: |
|
2546 assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y" |
|
2547 shows "foldr f xs = fold f xs" |
|
2548 using assms unfolding foldr_def by (rule fold_rev) |
|
2549 |
|
2550 lemma |
|
2551 foldr_Nil [code, simp]: "foldr f [] = id" |
|
2552 and foldr_Cons [code, simp]: "foldr f (x # xs) = f x \<circ> foldr f xs" |
|
2553 by (simp_all add: foldr_def) |
|
2554 |
|
2555 lemma |
|
2556 foldl_Nil [simp]: "foldl f a [] = a" |
|
2557 and foldl_Cons [simp]: "foldl f a (x # xs) = foldl f (f a x) xs" |
|
2558 by (simp_all add: foldl_def) |
|
2559 |
|
2560 lemma foldr_cong [fundef_cong]: |
|
2561 "a = b \<Longrightarrow> l = k \<Longrightarrow> (\<And>a x. x \<in> set l \<Longrightarrow> f x a = g x a) \<Longrightarrow> foldr f l a = foldr g k b" |
|
2562 by (auto simp add: foldr_def intro!: fold_cong) |
|
2563 |
|
2564 lemma foldl_cong [fundef_cong]: |
|
2565 "a = b \<Longrightarrow> l = k \<Longrightarrow> (\<And>a x. x \<in> set l \<Longrightarrow> f a x = g a x) \<Longrightarrow> foldl f a l = foldl g b k" |
|
2566 by (auto simp add: foldl_def intro!: fold_cong) |
|
2567 |
|
2568 lemma foldr_append [simp]: |
|
2569 "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)" |
|
2570 by (simp add: foldr_def) |
|
2571 |
|
2572 lemma foldl_append [simp]: |
|
2573 "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys" |
|
2574 by (simp add: foldl_def) |
|
2575 |
|
2576 lemma foldr_map [code_unfold]: |
|
2577 "foldr g (map f xs) a = foldr (g o f) xs a" |
|
2578 by (simp add: foldr_def fold_map rev_map) |
|
2579 |
|
2580 lemma foldl_map [code_unfold]: |
|
2581 "foldl g a (map f xs) = foldl (\<lambda>a x. g a (f x)) a xs" |
|
2582 by (simp add: foldl_def fold_map comp_def) |
|
2583 |
|
2584 text {* Executing operations in terms of @{const foldr} -- tail-recursive! *} |
|
2585 |
|
2586 lemma concat_conv_foldr [code]: |
|
2587 "concat xss = foldr append xss []" |
|
2588 by (simp add: fold_append_concat_rev foldr_def) |
|
2589 |
|
2590 lemma (in lattice) Inf_fin_set_foldr [code]: |
|
2591 "Inf_fin (set (x # xs)) = foldr inf xs x" |
|
2592 by (simp add: Inf_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) |
|
2593 |
|
2594 lemma (in lattice) Sup_fin_set_foldr [code]: |
|
2595 "Sup_fin (set (x # xs)) = foldr sup xs x" |
|
2596 by (simp add: Sup_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) |
|
2597 |
|
2598 lemma (in linorder) Min_fin_set_foldr [code]: |
|
2599 "Min (set (x # xs)) = foldr min xs x" |
|
2600 by (simp add: Min_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) |
|
2601 |
|
2602 lemma (in linorder) Max_fin_set_foldr [code]: |
|
2603 "Max (set (x # xs)) = foldr max xs x" |
|
2604 by (simp add: Max_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) |
|
2605 |
|
2606 lemma (in complete_lattice) Inf_set_foldr: |
|
2607 "Inf (set xs) = foldr inf xs top" |
|
2608 by (simp add: Inf_set_fold ac_simps foldr_fold fun_eq_iff) |
|
2609 |
|
2610 lemma (in complete_lattice) Sup_set_foldr: |
|
2611 "Sup (set xs) = foldr sup xs bot" |
|
2612 by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff) |
|
2613 |
|
2614 lemma (in complete_lattice) INF_set_foldr [code]: |
|
2615 "INFI (set xs) f = foldr (inf \<circ> f) xs top" |
|
2616 by (simp only: INF_def Inf_set_foldr foldr_map set_map [symmetric]) |
|
2617 |
|
2618 lemma (in complete_lattice) SUP_set_foldr [code]: |
|
2619 "SUPR (set xs) f = foldr (sup \<circ> f) xs bot" |
|
2620 by (simp only: SUP_def Sup_set_foldr foldr_map set_map [symmetric]) |
2538 |
2621 |
2539 |
2622 |
2540 subsubsection {* @{text upt} *} |
2623 subsubsection {* @{text upt} *} |
2541 |
2624 |
2542 lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])" |
2625 lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])" |
2938 |
3021 |
2939 lemma distinct_length_2_or_more: |
3022 lemma distinct_length_2_or_more: |
2940 "distinct (a # b # xs) \<longleftrightarrow> (a \<noteq> b \<and> distinct (a # xs) \<and> distinct (b # xs))" |
3023 "distinct (a # b # xs) \<longleftrightarrow> (a \<noteq> b \<and> distinct (a # xs) \<and> distinct (b # xs))" |
2941 by (metis distinct.simps(2) hd.simps hd_in_set list.simps(2) set_ConsD set_rev_mp set_subset_Cons) |
3024 by (metis distinct.simps(2) hd.simps hd_in_set list.simps(2) set_ConsD set_rev_mp set_subset_Cons) |
2942 |
3025 |
2943 |
|
2944 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*} |
3026 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*} |
2945 |
|
2946 lemma (in monoid_add) listsum_foldl [code]: |
|
2947 "listsum = foldl (op +) 0" |
|
2948 by (simp add: listsum_def foldl_foldr1 fun_eq_iff) |
|
2949 |
3027 |
2950 lemma (in monoid_add) listsum_simps [simp]: |
3028 lemma (in monoid_add) listsum_simps [simp]: |
2951 "listsum [] = 0" |
3029 "listsum [] = 0" |
2952 "listsum (x#xs) = x + listsum xs" |
3030 "listsum (x # xs) = x + listsum xs" |
2953 by (simp_all add: listsum_def) |
3031 by (simp_all add: listsum_def) |
2954 |
3032 |
2955 lemma (in monoid_add) listsum_append [simp]: |
3033 lemma (in monoid_add) listsum_append [simp]: |
2956 "listsum (xs @ ys) = listsum xs + listsum ys" |
3034 "listsum (xs @ ys) = listsum xs + listsum ys" |
2957 by (induct xs) (simp_all add: add.assoc) |
3035 by (induct xs) (simp_all add: add.assoc) |
2958 |
3036 |
2959 lemma (in comm_monoid_add) listsum_rev [simp]: |
3037 lemma (in comm_monoid_add) listsum_rev [simp]: |
2960 "listsum (rev xs) = listsum xs" |
3038 "listsum (rev xs) = listsum xs" |
2961 by (simp add: listsum_def [of "rev xs"]) (simp add: listsum_foldl foldr_foldl add.commute) |
3039 by (simp add: listsum_def foldr_def fold_rev fun_eq_iff add_ac) |
|
3040 |
|
3041 lemma (in monoid_add) fold_plus_listsum_rev: |
|
3042 "fold plus xs = plus (listsum (rev xs))" |
|
3043 proof |
|
3044 fix x |
|
3045 have "fold plus xs x = fold plus xs (x + 0)" by simp |
|
3046 also have "\<dots> = fold plus (x # xs) 0" by simp |
|
3047 also have "\<dots> = foldr plus (rev xs @ [x]) 0" by (simp add: foldr_def) |
|
3048 also have "\<dots> = listsum (rev xs @ [x])" by (simp add: listsum_def) |
|
3049 also have "\<dots> = listsum (rev xs) + listsum [x]" by simp |
|
3050 finally show "fold plus xs x = listsum (rev xs) + x" by simp |
|
3051 qed |
|
3052 |
|
3053 lemma (in semigroup_add) foldl_assoc: |
|
3054 "foldl plus (x + y) zs = x + foldl plus y zs" |
|
3055 by (simp add: foldl_def fold_commute_apply [symmetric] fun_eq_iff add_assoc) |
|
3056 |
|
3057 lemma (in ab_semigroup_add) foldr_conv_foldl: |
|
3058 "foldr plus xs a = foldl plus a xs" |
|
3059 by (simp add: foldl_def foldr_fold fun_eq_iff add_ac) |
|
3060 |
|
3061 text {* |
|
3062 Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more |
|
3063 difficult to use because it requires an additional transitivity step. |
|
3064 *} |
|
3065 |
|
3066 lemma start_le_sum: |
|
3067 fixes m n :: nat |
|
3068 shows "m \<le> n \<Longrightarrow> m \<le> foldl plus n ns" |
|
3069 by (simp add: foldl_def add_commute fold_plus_listsum_rev) |
|
3070 |
|
3071 lemma elem_le_sum: |
|
3072 fixes m n :: nat |
|
3073 shows "n \<in> set ns \<Longrightarrow> n \<le> foldl plus 0 ns" |
|
3074 by (force intro: start_le_sum simp add: in_set_conv_decomp) |
|
3075 |
|
3076 lemma sum_eq_0_conv [iff]: |
|
3077 fixes m :: nat |
|
3078 shows "foldl plus m ns = 0 \<longleftrightarrow> m = 0 \<and> (\<forall>n \<in> set ns. n = 0)" |
|
3079 by (induct ns arbitrary: m) auto |
|
3080 |
|
3081 text{* Some syntactic sugar for summing a function over a list: *} |
|
3082 |
|
3083 syntax |
|
3084 "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10) |
|
3085 syntax (xsymbols) |
|
3086 "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10) |
|
3087 syntax (HTML output) |
|
3088 "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10) |
|
3089 |
|
3090 translations -- {* Beware of argument permutation! *} |
|
3091 "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)" |
|
3092 "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)" |
2962 |
3093 |
2963 lemma (in comm_monoid_add) listsum_map_remove1: |
3094 lemma (in comm_monoid_add) listsum_map_remove1: |
2964 "x \<in> set xs \<Longrightarrow> listsum (map f xs) = f x + listsum (map f (remove1 x xs))" |
3095 "x \<in> set xs \<Longrightarrow> listsum (map f xs) = f x + listsum (map f (remove1 x xs))" |
2965 by (induct xs) (auto simp add: ac_simps) |
3096 by (induct xs) (auto simp add: ac_simps) |
2966 |
3097 |