448 lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" |
448 lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" |
449 by (induct xs) auto |
449 by (induct xs) auto |
450 |
450 |
451 lemma append_Nil2 [simp]: "xs @ [] = xs" |
451 lemma append_Nil2 [simp]: "xs @ [] = xs" |
452 by (induct xs) auto |
452 by (induct xs) auto |
|
453 |
|
454 interpretation semigroup_append: semigroup_add ["op @"] |
|
455 by unfold_locales simp |
|
456 interpretation monoid_append: monoid_add ["[]" "op @"] |
|
457 by unfold_locales (simp+) |
453 |
458 |
454 lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])" |
459 lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])" |
455 by (induct xs) auto |
460 by (induct xs) auto |
456 |
461 |
457 lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])" |
462 lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])" |
1736 by (induct xs) auto |
1741 by (induct xs) auto |
1737 |
1742 |
1738 lemma foldr_map: "foldr g (map f xs) a = foldr (g o f) xs a" |
1743 lemma foldr_map: "foldr g (map f xs) a = foldr (g o f) xs a" |
1739 by(induct xs) simp_all |
1744 by(induct xs) simp_all |
1740 |
1745 |
1741 lemma foldl_map: "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs" |
1746 text{* For efficient code generation: avoid intermediate list. *} |
|
1747 lemma foldl_map[code unfold]: |
|
1748 "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs" |
1742 by(induct xs arbitrary:a) simp_all |
1749 by(induct xs arbitrary:a) simp_all |
1743 |
1750 |
1744 lemma foldl_cong [fundef_cong, recdef_cong]: |
1751 lemma foldl_cong [fundef_cong, recdef_cong]: |
1745 "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] |
1752 "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] |
1746 ==> foldl f a l = foldl g b k" |
1753 ==> foldl f a l = foldl g b k" |
1749 lemma foldr_cong [fundef_cong, recdef_cong]: |
1756 lemma foldr_cong [fundef_cong, recdef_cong]: |
1750 "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] |
1757 "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] |
1751 ==> foldr f l a = foldr g k b" |
1758 ==> foldr f l a = foldr g k b" |
1752 by (induct k arbitrary: a b l) simp_all |
1759 by (induct k arbitrary: a b l) simp_all |
1753 |
1760 |
|
1761 lemma (in semigroup_add) foldl_assoc: |
|
1762 shows "foldl op\<^loc>+ (x\<^loc>+y) zs = x \<^loc>+ (foldl op\<^loc>+ y zs)" |
|
1763 by (induct zs arbitrary: y) (simp_all add:add_assoc) |
|
1764 |
|
1765 lemma (in monoid_add) foldl_absorb0: |
|
1766 shows "x \<^loc>+ (foldl op\<^loc>+ \<^loc>0 zs) = foldl op\<^loc>+ x zs" |
|
1767 by (induct zs) (simp_all add:foldl_assoc) |
|
1768 |
|
1769 |
1754 text{* The ``First Duality Theorem'' in Bird \& Wadler: *} |
1770 text{* The ``First Duality Theorem'' in Bird \& Wadler: *} |
1755 |
1771 |
1756 lemma foldl_foldr1_lemma: |
1772 lemma foldl_foldr1_lemma: |
1757 "foldl op + a xs = a + foldr op + xs (0\<Colon>'a::monoid_add)" |
1773 "foldl op + a xs = a + foldr op + xs (0\<Colon>'a::monoid_add)" |
1758 by (induct xs arbitrary: a) (auto simp:add_assoc) |
1774 by (induct xs arbitrary: a) (auto simp:add_assoc) |
1783 |
1799 |
1784 lemma sum_eq_0_conv [iff]: |
1800 lemma sum_eq_0_conv [iff]: |
1785 "!!m::nat. (foldl (op +) m ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))" |
1801 "!!m::nat. (foldl (op +) m ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))" |
1786 by (induct ns) auto |
1802 by (induct ns) auto |
1787 |
1803 |
|
1804 text{* @{const foldl} and @{text concat} *} |
|
1805 |
|
1806 lemma concat_conv_foldl: "concat xss = foldl op@ [] xss" |
|
1807 by (induct xss) (simp_all add:monoid_append.foldl_absorb0) |
|
1808 |
|
1809 lemma foldl_conv_concat: |
|
1810 "foldl (op @) xs xxs = xs @ (concat xxs)" |
|
1811 by(simp add:concat_conv_foldl monoid_append.foldl_absorb0) |
|
1812 |
1788 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*} |
1813 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*} |
|
1814 |
|
1815 lemma listsum_append[simp]: "listsum (xs @ ys) = listsum xs + listsum ys" |
|
1816 by (induct xs) (simp_all add:add_assoc) |
|
1817 |
|
1818 lemma listsum_rev[simp]: |
|
1819 fixes xs :: "'a::comm_monoid_add list" |
|
1820 shows "listsum (rev xs) = listsum xs" |
|
1821 by (induct xs) (simp_all add:add_ac) |
1789 |
1822 |
1790 lemma listsum_foldr: |
1823 lemma listsum_foldr: |
1791 "listsum xs = foldr (op +) xs 0" |
1824 "listsum xs = foldr (op +) xs 0" |
1792 by(induct xs) auto |
1825 by(induct xs) auto |
1793 |
1826 |
1794 (* for efficient code generation *) |
1827 text{* For efficient code generation --- |
1795 lemma listsum[code]: "listsum xs = foldl (op +) 0 xs" |
1828 @{const listsum} is not tail recursive but @{const foldl} is. *} |
|
1829 lemma listsum[code unfold]: "listsum xs = foldl (op +) 0 xs" |
1796 by(simp add:listsum_foldr foldl_foldr1) |
1830 by(simp add:listsum_foldr foldl_foldr1) |
|
1831 |
1797 |
1832 |
1798 text{* Some syntactic sugar for summing a function over a list: *} |
1833 text{* Some syntactic sugar for summing a function over a list: *} |
1799 |
1834 |
1800 syntax |
1835 syntax |
1801 "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10) |
1836 "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10) |
2988 |
3023 |
2989 lemma map_filter_conv [simp]: |
3024 lemma map_filter_conv [simp]: |
2990 "map_filter f P xs = map f (filter P xs)" |
3025 "map_filter f P xs = map f (filter P xs)" |
2991 by (induct xs) auto |
3026 by (induct xs) auto |
2992 |
3027 |
2993 lemma [code inline]: "listsum (map f xs) = foldl (%n x. n + f x) 0 xs" |
3028 |
2994 by (simp add: listsum_foldr foldl_map [symmetric] foldl_foldr1) |
3029 text {* Code for bounded quantification and summation over nats. *} |
2995 |
|
2996 |
|
2997 text {* Code for bounded quantification over nats. *} |
|
2998 |
3030 |
2999 lemma atMost_upto [code unfold]: |
3031 lemma atMost_upto [code unfold]: |
3000 "{..n} = set [0..n]" |
3032 "{..n} = set [0..n]" |
3001 by auto |
3033 by auto |
3002 |
3034 |
3003 lemma atLeast_upt [code unfold]: |
3035 lemma atLeast_upt [code unfold]: |
3004 "{..<n} = set [0..<n]" |
3036 "{..<n} = set [0..<n]" |
3005 by auto |
3037 by auto |
3006 |
3038 |
3007 lemma greaterThanLessThan_upd [code unfold]: |
3039 lemma greaterThanLessThan_upt [code unfold]: |
3008 "{n<..<m} = set [Suc n..<m]" |
3040 "{n<..<m} = set [Suc n..<m]" |
3009 by auto |
3041 by auto |
3010 |
3042 |
3011 lemma atLeastLessThan_upd [code unfold]: |
3043 lemma atLeastLessThan_upt [code unfold]: |
3012 "{n..<m} = set [n..<m]" |
3044 "{n..<m} = set [n..<m]" |
3013 by auto |
3045 by auto |
3014 |
3046 |
3015 lemma greaterThanAtMost_upto [code unfold]: |
3047 lemma greaterThanAtMost_upto [code unfold]: |
3016 "{n<..m} = set [Suc n..m]" |
3048 "{n<..m} = set [Suc n..m]" |
3034 |
3066 |
3035 lemma ex_nat_less [code unfold]: |
3067 lemma ex_nat_less [code unfold]: |
3036 "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)" |
3068 "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)" |
3037 by auto |
3069 by auto |
3038 |
3070 |
3039 lemma foldl_append_append: "\<And> ss ss'. foldl (op @) (ss@ss') xs = ss@(foldl (op @) ss' xs)" |
3071 lemma setsum_set_upt_conv_listsum[code unfold]: |
3040 by (induct xs, simp_all) |
3072 "setsum f (set[k..<n]) = listsum (map f [k..<n])" |
3041 |
3073 apply(subst atLeastLessThan_upt[symmetric]) |
|
3074 by (induct n) simp_all |
|
3075 |
|
3076 |
|
3077 (* FIXME Amine *) |
|
3078 |
|
3079 (* is now available as thm semigroup_append.foldl_assoc *) |
|
3080 lemma foldl_append_append: "foldl (op @) (ss@ss') xs = ss@(foldl (op @) ss' xs)" |
|
3081 by (induct xs arbitrary: ss ss', simp_all) |
|
3082 |
|
3083 (* now superfluous *) |
|
3084 lemma foldl_append_map_set: |
|
3085 "set (foldl (op @) ss (map f xs)) = set ss \<union> UNION (set xs) (\<lambda>x. set (f x))" |
|
3086 by(simp add:foldl_conv_concat) |
|
3087 (* |
3042 lemma foldl_append_map_set: "\<And> ss. set (foldl (op @) ss (map f xs)) = set ss \<union> UNION (set xs) (\<lambda>x. set (f x))" |
3088 lemma foldl_append_map_set: "\<And> ss. set (foldl (op @) ss (map f xs)) = set ss \<union> UNION (set xs) (\<lambda>x. set (f x))" |
3043 proof(induct xs) |
3089 proof(induct xs) |
3044 case Nil thus ?case by simp |
3090 case Nil thus ?case by simp |
3045 next |
3091 next |
3046 case (Cons x xs ss) |
3092 case (Cons x xs ss) |
3050 also have "\<dots>= set ss \<union> set (f x) \<union> UNION (set xs) (\<lambda>x. set (f x))" by simp |
3096 also have "\<dots>= set ss \<union> set (f x) \<union> UNION (set xs) (\<lambda>x. set (f x))" by simp |
3051 also have "\<dots> = set ss \<union> UNION (set (x#xs)) (\<lambda>x. set (f x))" |
3097 also have "\<dots> = set ss \<union> UNION (set (x#xs)) (\<lambda>x. set (f x))" |
3052 by (simp add: Un_assoc) |
3098 by (simp add: Un_assoc) |
3053 finally show ?case by simp |
3099 finally show ?case by simp |
3054 qed |
3100 qed |
3055 |
3101 *) |
|
3102 |
|
3103 (* also superfluous *) |
3056 lemma foldl_append_map_Nil_set: |
3104 lemma foldl_append_map_Nil_set: |
3057 "set (foldl (op @) [] (map f xs)) = UNION (set xs) (\<lambda>x. set (f x))" |
3105 "set (foldl (op @) [] (map f xs)) = UNION (set xs) (\<lambda>x. set (f x))" |
|
3106 by(simp add:foldl_conv_concat) |
|
3107 (* |
3058 using foldl_append_map_set[where ss="[]" and xs="xs" and f="f"] by simp |
3108 using foldl_append_map_set[where ss="[]" and xs="xs" and f="f"] by simp |
3059 |
3109 *) |
3060 |
3110 |
3061 subsubsection {* List partitioning *} |
3111 subsubsection {* List partitioning *} |
3062 |
3112 |
3063 consts |
3113 consts |
3064 partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> 'a list \<times> 'a list" |
3114 partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> 'a list \<times> 'a list" |