src/HOL/List.thy
changeset 46133 d9fe85d3d2cd
parent 46125 00cd193a48dc
child 46138 85f8d8a8c711
     1.1 --- a/src/HOL/List.thy	Fri Jan 06 10:19:49 2012 +0100
     1.2 +++ b/src/HOL/List.thy	Fri Jan 06 10:19:49 2012 +0100
     1.3 @@ -49,6 +49,10 @@
     1.4      "set [] = {}"
     1.5    | "set (x # xs) = insert x (set xs)"
     1.6  
     1.7 +definition
     1.8 +  coset :: "'a list \<Rightarrow> 'a set" where
     1.9 +  [simp]: "coset xs = - set xs"
    1.10 +
    1.11  primrec
    1.12    map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
    1.13      "map f [] = []"
    1.14 @@ -81,15 +85,18 @@
    1.15  syntax (HTML output)
    1.16    "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
    1.17  
    1.18 -primrec
    1.19 +primrec -- {* canonical argument order *}
    1.20 +  fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
    1.21 +    "fold f [] = id"
    1.22 +  | "fold f (x # xs) = fold f xs \<circ> f x"
    1.23 +
    1.24 +definition 
    1.25 +  foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
    1.26 +  [code_abbrev]: "foldr f xs = fold f (rev xs)"
    1.27 +
    1.28 +definition
    1.29    foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" where
    1.30 -    foldl_Nil: "foldl f a [] = a"
    1.31 -  | foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs"
    1.32 -
    1.33 -primrec
    1.34 -  foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
    1.35 -    "foldr f [] a = a"
    1.36 -  | "foldr f (x # xs) a = f x (foldr f xs a)"
    1.37 +  "foldl f s xs = fold (\<lambda>x s. f s x)  xs s"
    1.38  
    1.39  primrec
    1.40    concat:: "'a list list \<Rightarrow> 'a list" where
    1.41 @@ -236,8 +243,9 @@
    1.42  @{lemma "butlast [a,b,c,d] = [a,b,c]" by simp}\\
    1.43  @{lemma[source] "filter (\<lambda>n::nat. n<2) [0,2,1] = [0,1]" by simp}\\
    1.44  @{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" by simp}\\
    1.45 -@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\
    1.46 -@{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by simp}\\
    1.47 +@{lemma "fold f [a,b,c] x = f c (f b (f a x))" by simp}\\
    1.48 +@{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by (simp add: foldr_def)}\\
    1.49 +@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by (simp add: foldl_def)}\\
    1.50  @{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\
    1.51  @{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\
    1.52  @{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
    1.53 @@ -261,7 +269,7 @@
    1.54  @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def eval_nat_numeral)}\\
    1.55  @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\
    1.56  @{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}\\
    1.57 -@{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def)}
    1.58 +@{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def foldr_def)}
    1.59  \end{tabular}}
    1.60  \caption{Characteristic examples}
    1.61  \label{fig:Characteristic}
    1.62 @@ -298,11 +306,11 @@
    1.63    by simp_all
    1.64  
    1.65  primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
    1.66 -"insort_key f x [] = [x]" |
    1.67 -"insort_key f x (y#ys) = (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))"
    1.68 +  "insort_key f x [] = [x]" |
    1.69 +  "insort_key f x (y#ys) = (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))"
    1.70  
    1.71  definition sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where
    1.72 -"sort_key f xs = foldr (insort_key f) xs []"
    1.73 +  "sort_key f xs = foldr (insort_key f) xs []"
    1.74  
    1.75  definition insort_insert_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
    1.76    "insort_insert_key f x xs = (if f x \<in> f ` set xs then xs else insort_key f x xs)"
    1.77 @@ -470,6 +478,9 @@
    1.78  
    1.79  simproc_setup list_to_set_comprehension ("set xs") = {* K List_to_Set_Comprehension.simproc *}
    1.80  
    1.81 +code_datatype set coset
    1.82 +
    1.83 +hide_const (open) coset
    1.84  
    1.85  subsubsection {* @{const Nil} and @{const Cons} *}
    1.86  
    1.87 @@ -2368,159 +2379,81 @@
    1.88  by(auto simp add: set_zip list_all2_eq list_all2_conv_all_nth cong: conj_cong)
    1.89  
    1.90  
    1.91 -subsubsection {* @{text foldl} and @{text foldr} *}
    1.92 -
    1.93 -lemma foldl_append [simp]:
    1.94 -  "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
    1.95 -by (induct xs arbitrary: a) auto
    1.96 -
    1.97 -lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
    1.98 -by (induct xs) auto
    1.99 -
   1.100 -lemma foldr_map: "foldr g (map f xs) a = foldr (g o f) xs a"
   1.101 -by(induct xs) simp_all
   1.102 -
   1.103 -text{* For efficient code generation: avoid intermediate list. *}
   1.104 -lemma foldl_map[code_unfold]:
   1.105 -  "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
   1.106 -by(induct xs arbitrary:a) simp_all
   1.107 -
   1.108 -lemma foldl_apply:
   1.109 -  assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x \<circ> h = h \<circ> g x"
   1.110 -  shows "foldl (\<lambda>s x. f x s) (h s) xs = h (foldl (\<lambda>s x. g x s) s xs)"
   1.111 -  by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: fun_eq_iff)
   1.112 -
   1.113 -lemma foldl_cong [fundef_cong]:
   1.114 -  "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] 
   1.115 -  ==> foldl f a l = foldl g b k"
   1.116 -by (induct k arbitrary: a b l) simp_all
   1.117 -
   1.118 -lemma foldr_cong [fundef_cong]:
   1.119 -  "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] 
   1.120 -  ==> foldr f l a = foldr g k b"
   1.121 -by (induct k arbitrary: a b l) simp_all
   1.122 -
   1.123 -lemma foldl_fun_comm:
   1.124 -  assumes "\<And>x y s. f (f s x) y = f (f s y) x"
   1.125 -  shows "f (foldl f s xs) x = foldl f (f s x) xs"
   1.126 -  by (induct xs arbitrary: s)
   1.127 -    (simp_all add: assms)
   1.128 -
   1.129 -lemma (in semigroup_add) foldl_assoc:
   1.130 -shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"
   1.131 -by (induct zs arbitrary: y) (simp_all add:add_assoc)
   1.132 -
   1.133 -lemma (in monoid_add) foldl_absorb0:
   1.134 -shows "x + (foldl op+ 0 zs) = foldl op+ x zs"
   1.135 -by (induct zs) (simp_all add:foldl_assoc)
   1.136 -
   1.137 -lemma foldl_rev:
   1.138 -  assumes "\<And>x y s. f (f s x) y = f (f s y) x"
   1.139 -  shows "foldl f s (rev xs) = foldl f s xs"
   1.140 -proof (induct xs arbitrary: s)
   1.141 -  case Nil then show ?case by simp
   1.142 -next
   1.143 -  case (Cons x xs) with assms show ?case by (simp add: foldl_fun_comm)
   1.144 -qed
   1.145 -
   1.146 -lemma rev_foldl_cons [code]:
   1.147 -  "rev xs = foldl (\<lambda>xs x. x # xs) [] xs"
   1.148 -proof (induct xs)
   1.149 -  case Nil then show ?case by simp
   1.150 -next
   1.151 -  case Cons
   1.152 -  {
   1.153 -    fix x xs ys
   1.154 -    have "foldl (\<lambda>xs x. x # xs) ys xs @ [x]
   1.155 -      = foldl (\<lambda>xs x. x # xs) (ys @ [x]) xs"
   1.156 -    by (induct xs arbitrary: ys) auto
   1.157 -  }
   1.158 -  note aux = this
   1.159 -  show ?case by (induct xs) (auto simp add: Cons aux)
   1.160 +subsubsection {* @{const fold} with canonical argument order *}
   1.161 +
   1.162 +lemma fold_remove1_split:
   1.163 +  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"
   1.164 +    and x: "x \<in> set xs"
   1.165 +  shows "fold f xs = fold f (remove1 x xs) \<circ> f x"
   1.166 +  using assms by (induct xs) (auto simp add: o_assoc [symmetric])
   1.167 +
   1.168 +lemma fold_cong [fundef_cong]:
   1.169 +  "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)
   1.170 +    \<Longrightarrow> fold f xs a = fold g ys b"
   1.171 +  by (induct ys arbitrary: a b xs) simp_all
   1.172 +
   1.173 +lemma fold_id:
   1.174 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = id"
   1.175 +  shows "fold f xs = id"
   1.176 +  using assms by (induct xs) simp_all
   1.177 +
   1.178 +lemma fold_commute:
   1.179 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
   1.180 +  shows "h \<circ> fold g xs = fold f xs \<circ> h"
   1.181 +  using assms by (induct xs) (simp_all add: fun_eq_iff)
   1.182 +
   1.183 +lemma fold_commute_apply:
   1.184 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
   1.185 +  shows "h (fold g xs s) = fold f xs (h s)"
   1.186 +proof -
   1.187 +  from assms have "h \<circ> fold g xs = fold f xs \<circ> h" by (rule fold_commute)
   1.188 +  then show ?thesis by (simp add: fun_eq_iff)
   1.189  qed
   1.190  
   1.191 -
   1.192 -text{* The ``Third Duality Theorem'' in Bird \& Wadler: *}
   1.193 -
   1.194 -lemma foldr_foldl:
   1.195 -  "foldr f xs a = foldl (%x y. f y x) a (rev xs)"
   1.196 -  by (induct xs) auto
   1.197 -
   1.198 -lemma foldl_foldr:
   1.199 -  "foldl f a xs = foldr (%x y. f y x) (rev xs) a"
   1.200 -  by (simp add: foldr_foldl [of "%x y. f y x" "rev xs"])
   1.201 -
   1.202 -
   1.203 -text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
   1.204 -
   1.205 -lemma (in monoid_add) foldl_foldr1_lemma:
   1.206 -  "foldl op + a xs = a + foldr op + xs 0"
   1.207 -  by (induct xs arbitrary: a) (auto simp: add_assoc)
   1.208 -
   1.209 -corollary (in monoid_add) foldl_foldr1:
   1.210 -  "foldl op + 0 xs = foldr op + xs 0"
   1.211 -  by (simp add: foldl_foldr1_lemma)
   1.212 -
   1.213 -lemma (in ab_semigroup_add) foldr_conv_foldl:
   1.214 -  "foldr op + xs a = foldl op + a xs"
   1.215 -  by (induct xs) (simp_all add: foldl_assoc add.commute)
   1.216 -
   1.217 -text {*
   1.218 -Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more
   1.219 -difficult to use because it requires an additional transitivity step.
   1.220 -*}
   1.221 -
   1.222 -lemma start_le_sum: "(m::nat) <= n ==> m <= foldl (op +) n ns"
   1.223 -by (induct ns arbitrary: n) auto
   1.224 -
   1.225 -lemma elem_le_sum: "(n::nat) : set ns ==> n <= foldl (op +) 0 ns"
   1.226 -by (force intro: start_le_sum simp add: in_set_conv_decomp)
   1.227 -
   1.228 -lemma sum_eq_0_conv [iff]:
   1.229 -  "(foldl (op +) (m::nat) ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))"
   1.230 -by (induct ns arbitrary: m) auto
   1.231 -
   1.232 -lemma foldr_invariant: 
   1.233 -  "\<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)"
   1.234 -  by (induct xs, simp_all)
   1.235 -
   1.236 -lemma foldl_invariant: 
   1.237 -  "\<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)"
   1.238 -  by (induct xs arbitrary: x, simp_all)
   1.239 -
   1.240 -lemma foldl_weak_invariant:
   1.241 -  assumes "P s"
   1.242 -    and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f s x)"
   1.243 -  shows "P (foldl f s xs)"
   1.244 +lemma fold_invariant: 
   1.245 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s"
   1.246 +    and "\<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
   1.247 +  shows "P (fold f xs s)"
   1.248    using assms by (induct xs arbitrary: s) simp_all
   1.249  
   1.250 -text {* @{const foldl} and @{const concat} *}
   1.251 -
   1.252 -lemma foldl_conv_concat:
   1.253 -  "foldl (op @) xs xss = xs @ concat xss"
   1.254 -proof (induct xss arbitrary: xs)
   1.255 -  case Nil show ?case by simp
   1.256 -next
   1.257 -  interpret monoid_add "op @" "[]" proof qed simp_all
   1.258 -  case Cons then show ?case by (simp add: foldl_absorb0)
   1.259 -qed
   1.260 -
   1.261 -lemma concat_conv_foldl: "concat xss = foldl (op @) [] xss"
   1.262 -  by (simp add: foldl_conv_concat)
   1.263 -
   1.264 -text {* @{const Finite_Set.fold} and @{const foldl} *}
   1.265 -
   1.266 -lemma (in comp_fun_commute) fold_set_remdups:
   1.267 -  "Finite_Set.fold f y (set xs) = foldl (\<lambda>y x. f x y) y (remdups xs)"
   1.268 +lemma fold_append [simp]:
   1.269 +  "fold f (xs @ ys) = fold f ys \<circ> fold f xs"
   1.270 +  by (induct xs) simp_all
   1.271 +
   1.272 +lemma fold_map [code_unfold]:
   1.273 +  "fold g (map f xs) = fold (g o f) xs"
   1.274 +  by (induct xs) simp_all
   1.275 +
   1.276 +lemma fold_rev:
   1.277 +  assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
   1.278 +  shows "fold f (rev xs) = fold f xs"
   1.279 +using assms by (induct xs) (simp_all add: fold_commute_apply fun_eq_iff)
   1.280 +
   1.281 +lemma fold_Cons_rev:
   1.282 +  "fold Cons xs = append (rev xs)"
   1.283 +  by (induct xs) simp_all
   1.284 +
   1.285 +lemma rev_conv_fold [code]:
   1.286 +  "rev xs = fold Cons xs []"
   1.287 +  by (simp add: fold_Cons_rev)
   1.288 +
   1.289 +lemma fold_append_concat_rev:
   1.290 +  "fold append xss = append (concat (rev xss))"
   1.291 +  by (induct xss) simp_all
   1.292 +
   1.293 +text {* @{const Finite_Set.fold} and @{const fold} *}
   1.294 +
   1.295 +lemma (in comp_fun_commute) fold_set_fold_remdups:
   1.296 +  "Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
   1.297    by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
   1.298  
   1.299 -lemma (in comp_fun_idem) fold_set:
   1.300 -  "Finite_Set.fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"
   1.301 +lemma (in comp_fun_idem) fold_set_fold:
   1.302 +  "Finite_Set.fold f y (set xs) = fold f xs y"
   1.303    by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
   1.304  
   1.305 -lemma (in ab_semigroup_idem_mult) fold1_set:
   1.306 +lemma (in ab_semigroup_idem_mult) fold1_set_fold:
   1.307    assumes "xs \<noteq> []"
   1.308 -  shows "fold1 times (set xs) = foldl times (hd xs) (tl xs)"
   1.309 +  shows "Finite_Set.fold1 times (set xs) = fold times (tl xs) (hd xs)"
   1.310  proof -
   1.311    interpret comp_fun_idem times by (fact comp_fun_idem)
   1.312    from assms obtain y ys where xs: "xs = y # ys"
   1.313 @@ -2532,10 +2465,160 @@
   1.314      case False
   1.315      then have "fold1 times (insert y (set ys)) = Finite_Set.fold times y (set ys)"
   1.316        by (simp only: finite_set fold1_eq_fold_idem)
   1.317 -    with xs show ?thesis by (simp add: fold_set mult_commute)
   1.318 +    with xs show ?thesis by (simp add: fold_set_fold mult_commute)
   1.319    qed
   1.320  qed
   1.321  
   1.322 +lemma (in lattice) Inf_fin_set_fold:
   1.323 +  "Inf_fin (set (x # xs)) = fold inf xs x"
   1.324 +proof -
   1.325 +  interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   1.326 +    by (fact ab_semigroup_idem_mult_inf)
   1.327 +  show ?thesis
   1.328 +    by (simp add: Inf_fin_def fold1_set_fold del: set.simps)
   1.329 +qed
   1.330 +
   1.331 +lemma (in lattice) Sup_fin_set_fold:
   1.332 +  "Sup_fin (set (x # xs)) = fold sup xs x"
   1.333 +proof -
   1.334 +  interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   1.335 +    by (fact ab_semigroup_idem_mult_sup)
   1.336 +  show ?thesis
   1.337 +    by (simp add: Sup_fin_def fold1_set_fold del: set.simps)
   1.338 +qed
   1.339 +
   1.340 +lemma (in linorder) Min_fin_set_fold:
   1.341 +  "Min (set (x # xs)) = fold min xs x"
   1.342 +proof -
   1.343 +  interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   1.344 +    by (fact ab_semigroup_idem_mult_min)
   1.345 +  show ?thesis
   1.346 +    by (simp add: Min_def fold1_set_fold del: set.simps)
   1.347 +qed
   1.348 +
   1.349 +lemma (in linorder) Max_fin_set_fold:
   1.350 +  "Max (set (x # xs)) = fold max xs x"
   1.351 +proof -
   1.352 +  interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   1.353 +    by (fact ab_semigroup_idem_mult_max)
   1.354 +  show ?thesis
   1.355 +    by (simp add: Max_def fold1_set_fold del: set.simps)
   1.356 +qed
   1.357 +
   1.358 +lemma (in complete_lattice) Inf_set_fold:
   1.359 +  "Inf (set xs) = fold inf xs top"
   1.360 +proof -
   1.361 +  interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   1.362 +    by (fact comp_fun_idem_inf)
   1.363 +  show ?thesis by (simp add: Inf_fold_inf fold_set_fold inf_commute)
   1.364 +qed
   1.365 +
   1.366 +lemma (in complete_lattice) Sup_set_fold:
   1.367 +  "Sup (set xs) = fold sup xs bot"
   1.368 +proof -
   1.369 +  interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   1.370 +    by (fact comp_fun_idem_sup)
   1.371 +  show ?thesis by (simp add: Sup_fold_sup fold_set_fold sup_commute)
   1.372 +qed
   1.373 +
   1.374 +lemma (in complete_lattice) INF_set_fold:
   1.375 +  "INFI (set xs) f = fold (inf \<circ> f) xs top"
   1.376 +  unfolding INF_def set_map [symmetric] Inf_set_fold fold_map ..
   1.377 +
   1.378 +lemma (in complete_lattice) SUP_set_fold:
   1.379 +  "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
   1.380 +  unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..
   1.381 +
   1.382 +
   1.383 +subsubsection {* Fold variants: @{const foldr} and @{const foldl} *}
   1.384 +
   1.385 +text {* Correspondence *}
   1.386 +
   1.387 +lemma foldr_foldl: -- {* The ``Third Duality Theorem'' in Bird \& Wadler: *}
   1.388 +  "foldr f xs a = foldl (\<lambda>x y. f y x) a (rev xs)"
   1.389 +  by (simp add: foldr_def foldl_def)
   1.390 +
   1.391 +lemma foldl_foldr:
   1.392 +  "foldl f a xs = foldr (\<lambda>x y. f y x) (rev xs) a"
   1.393 +  by (simp add: foldr_def foldl_def)
   1.394 +
   1.395 +lemma foldr_fold:
   1.396 +  assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
   1.397 +  shows "foldr f xs = fold f xs"
   1.398 +  using assms unfolding foldr_def by (rule fold_rev)
   1.399 +
   1.400 +lemma
   1.401 +  foldr_Nil [code, simp]: "foldr f [] = id"
   1.402 +  and foldr_Cons [code, simp]: "foldr f (x # xs) = f x \<circ> foldr f xs"
   1.403 +  by (simp_all add: foldr_def)
   1.404 +
   1.405 +lemma
   1.406 +  foldl_Nil [simp]: "foldl f a [] = a"
   1.407 +  and foldl_Cons [simp]: "foldl f a (x # xs) = foldl f (f a x) xs"
   1.408 +  by (simp_all add: foldl_def)
   1.409 +
   1.410 +lemma foldr_cong [fundef_cong]:
   1.411 +  "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"
   1.412 +  by (auto simp add: foldr_def intro!: fold_cong)
   1.413 +
   1.414 +lemma foldl_cong [fundef_cong]:
   1.415 +  "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"
   1.416 +  by (auto simp add: foldl_def intro!: fold_cong)
   1.417 +
   1.418 +lemma foldr_append [simp]:
   1.419 +  "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
   1.420 +  by (simp add: foldr_def)
   1.421 +
   1.422 +lemma foldl_append [simp]:
   1.423 +  "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
   1.424 +  by (simp add: foldl_def)
   1.425 +
   1.426 +lemma foldr_map [code_unfold]:
   1.427 +  "foldr g (map f xs) a = foldr (g o f) xs a"
   1.428 +  by (simp add: foldr_def fold_map rev_map)
   1.429 +
   1.430 +lemma foldl_map [code_unfold]:
   1.431 +  "foldl g a (map f xs) = foldl (\<lambda>a x. g a (f x)) a xs"
   1.432 +  by (simp add: foldl_def fold_map comp_def)
   1.433 +
   1.434 +text {* Executing operations in terms of @{const foldr} -- tail-recursive! *}
   1.435 +
   1.436 +lemma concat_conv_foldr [code]:
   1.437 +  "concat xss = foldr append xss []"
   1.438 +  by (simp add: fold_append_concat_rev foldr_def)
   1.439 +
   1.440 +lemma (in lattice) Inf_fin_set_foldr [code]:
   1.441 +  "Inf_fin (set (x # xs)) = foldr inf xs x"
   1.442 +  by (simp add: Inf_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
   1.443 +
   1.444 +lemma (in lattice) Sup_fin_set_foldr [code]:
   1.445 +  "Sup_fin (set (x # xs)) = foldr sup xs x"
   1.446 +  by (simp add: Sup_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
   1.447 +
   1.448 +lemma (in linorder) Min_fin_set_foldr [code]:
   1.449 +  "Min (set (x # xs)) = foldr min xs x"
   1.450 +  by (simp add: Min_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
   1.451 +
   1.452 +lemma (in linorder) Max_fin_set_foldr [code]:
   1.453 +  "Max (set (x # xs)) = foldr max xs x"
   1.454 +  by (simp add: Max_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
   1.455 +
   1.456 +lemma (in complete_lattice) Inf_set_foldr:
   1.457 +  "Inf (set xs) = foldr inf xs top"
   1.458 +  by (simp add: Inf_set_fold ac_simps foldr_fold fun_eq_iff)
   1.459 +
   1.460 +lemma (in complete_lattice) Sup_set_foldr:
   1.461 +  "Sup (set xs) = foldr sup xs bot"
   1.462 +  by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff)
   1.463 +
   1.464 +lemma (in complete_lattice) INF_set_foldr [code]:
   1.465 +  "INFI (set xs) f = foldr (inf \<circ> f) xs top"
   1.466 +  by (simp only: INF_def Inf_set_foldr foldr_map set_map [symmetric])
   1.467 +
   1.468 +lemma (in complete_lattice) SUP_set_foldr [code]:
   1.469 +  "SUPR (set xs) f = foldr (sup \<circ> f) xs bot"
   1.470 +  by (simp only: SUP_def Sup_set_foldr foldr_map set_map [symmetric])
   1.471 +
   1.472  
   1.473  subsubsection {* @{text upt} *}
   1.474  
   1.475 @@ -2940,16 +3023,11 @@
   1.476  "distinct (a # b # xs) \<longleftrightarrow> (a \<noteq> b \<and> distinct (a # xs) \<and> distinct (b # xs))"
   1.477  by (metis distinct.simps(2) hd.simps hd_in_set list.simps(2) set_ConsD set_rev_mp set_subset_Cons)
   1.478  
   1.479 -
   1.480  subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
   1.481  
   1.482 -lemma (in monoid_add) listsum_foldl [code]:
   1.483 -  "listsum = foldl (op +) 0"
   1.484 -  by (simp add: listsum_def foldl_foldr1 fun_eq_iff)
   1.485 -
   1.486  lemma (in monoid_add) listsum_simps [simp]:
   1.487    "listsum [] = 0"
   1.488 -  "listsum (x#xs) = x + listsum xs"
   1.489 +  "listsum (x # xs) = x + listsum xs"
   1.490    by (simp_all add: listsum_def)
   1.491  
   1.492  lemma (in monoid_add) listsum_append [simp]:
   1.493 @@ -2958,7 +3036,60 @@
   1.494  
   1.495  lemma (in comm_monoid_add) listsum_rev [simp]:
   1.496    "listsum (rev xs) = listsum xs"
   1.497 -  by (simp add: listsum_def [of "rev xs"]) (simp add: listsum_foldl foldr_foldl add.commute)
   1.498 +  by (simp add: listsum_def foldr_def fold_rev fun_eq_iff add_ac)
   1.499 +
   1.500 +lemma (in monoid_add) fold_plus_listsum_rev:
   1.501 +  "fold plus xs = plus (listsum (rev xs))"
   1.502 +proof
   1.503 +  fix x
   1.504 +  have "fold plus xs x = fold plus xs (x + 0)" by simp
   1.505 +  also have "\<dots> = fold plus (x # xs) 0" by simp
   1.506 +  also have "\<dots> = foldr plus (rev xs @ [x]) 0" by (simp add: foldr_def)
   1.507 +  also have "\<dots> = listsum (rev xs @ [x])" by (simp add: listsum_def)
   1.508 +  also have "\<dots> = listsum (rev xs) + listsum [x]" by simp
   1.509 +  finally show "fold plus xs x = listsum (rev xs) + x" by simp
   1.510 +qed
   1.511 +
   1.512 +lemma (in semigroup_add) foldl_assoc:
   1.513 +  "foldl plus (x + y) zs = x + foldl plus y zs"
   1.514 +  by (simp add: foldl_def fold_commute_apply [symmetric] fun_eq_iff add_assoc)
   1.515 +
   1.516 +lemma (in ab_semigroup_add) foldr_conv_foldl:
   1.517 +  "foldr plus xs a = foldl plus a xs"
   1.518 +  by (simp add: foldl_def foldr_fold fun_eq_iff add_ac)
   1.519 +
   1.520 +text {*
   1.521 +  Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more
   1.522 +  difficult to use because it requires an additional transitivity step.
   1.523 +*}
   1.524 +
   1.525 +lemma start_le_sum:
   1.526 +  fixes m n :: nat
   1.527 +  shows "m \<le> n \<Longrightarrow> m \<le> foldl plus n ns"
   1.528 +  by (simp add: foldl_def add_commute fold_plus_listsum_rev)
   1.529 +
   1.530 +lemma elem_le_sum:
   1.531 +  fixes m n :: nat 
   1.532 +  shows "n \<in> set ns \<Longrightarrow> n \<le> foldl plus 0 ns"
   1.533 +  by (force intro: start_le_sum simp add: in_set_conv_decomp)
   1.534 +
   1.535 +lemma sum_eq_0_conv [iff]:
   1.536 +  fixes m :: nat
   1.537 +  shows "foldl plus m ns = 0 \<longleftrightarrow> m = 0 \<and> (\<forall>n \<in> set ns. n = 0)"
   1.538 +  by (induct ns arbitrary: m) auto
   1.539 +
   1.540 +text{* Some syntactic sugar for summing a function over a list: *}
   1.541 +
   1.542 +syntax
   1.543 +  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
   1.544 +syntax (xsymbols)
   1.545 +  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
   1.546 +syntax (HTML output)
   1.547 +  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
   1.548 +
   1.549 +translations -- {* Beware of argument permutation! *}
   1.550 +  "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
   1.551 +  "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
   1.552  
   1.553  lemma (in comm_monoid_add) listsum_map_remove1:
   1.554    "x \<in> set xs \<Longrightarrow> listsum (map f xs) = f x + listsum (map f (remove1 x xs))"
   1.555 @@ -2983,7 +3114,7 @@
   1.556  
   1.557  lemma listsum_eq_0_nat_iff_nat [simp]:
   1.558    "listsum ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
   1.559 -  by (simp add: listsum_foldl)
   1.560 +  by (simp add: listsum_def foldr_conv_foldl)
   1.561  
   1.562  lemma elem_le_listsum_nat:
   1.563    "k < size ns \<Longrightarrow> ns ! k \<le> listsum (ns::nat list)"
   1.564 @@ -3000,19 +3131,6 @@
   1.565  apply arith
   1.566  done
   1.567  
   1.568 -text{* Some syntactic sugar for summing a function over a list: *}
   1.569 -
   1.570 -syntax
   1.571 -  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
   1.572 -syntax (xsymbols)
   1.573 -  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
   1.574 -syntax (HTML output)
   1.575 -  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
   1.576 -
   1.577 -translations -- {* Beware of argument permutation! *}
   1.578 -  "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
   1.579 -  "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
   1.580 -
   1.581  lemma (in monoid_add) listsum_triv:
   1.582    "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
   1.583    by (induct xs) (simp_all add: left_distrib)
   1.584 @@ -3819,9 +3937,26 @@
   1.585    "sort_key f (x#xs) = insort_key f x (sort_key f xs)"
   1.586    by (simp_all add: sort_key_def)
   1.587  
   1.588 -lemma sort_foldl_insort:
   1.589 -  "sort xs = foldl (\<lambda>ys x. insort x ys) [] xs"
   1.590 -  by (simp add: sort_key_def foldr_foldl foldl_rev insort_left_comm)
   1.591 +lemma (in linorder) sort_key_conv_fold:
   1.592 +  assumes "inj_on f (set xs)"
   1.593 +  shows "sort_key f xs = fold (insort_key f) xs []"
   1.594 +proof -
   1.595 +  have "fold (insort_key f) (rev xs) = fold (insort_key f) xs"
   1.596 +  proof (rule fold_rev, rule ext)
   1.597 +    fix zs
   1.598 +    fix x y
   1.599 +    assume "x \<in> set xs" "y \<in> set xs"
   1.600 +    with assms have *: "f y = f x \<Longrightarrow> y = x" by (auto dest: inj_onD)
   1.601 +    have **: "x = y \<longleftrightarrow> y = x" by auto
   1.602 +    show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs"
   1.603 +      by (induct zs) (auto intro: * simp add: **)
   1.604 +  qed
   1.605 +  then show ?thesis by (simp add: sort_key_def foldr_def)
   1.606 +qed
   1.607 +
   1.608 +lemma (in linorder) sort_conv_fold:
   1.609 +  "sort xs = fold insort xs []"
   1.610 +  by (rule sort_key_conv_fold) simp
   1.611  
   1.612  lemma length_sort[simp]: "length (sort_key f xs) = length xs"
   1.613  by (induct xs, auto)
   1.614 @@ -4312,7 +4447,7 @@
   1.615    "sorted_list_of_set (set xs) = sort (remdups xs)"
   1.616  proof -
   1.617    interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
   1.618 -  show ?thesis by (simp add: sort_foldl_insort sorted_list_of_set_def fold_set_remdups)
   1.619 +  show ?thesis by (simp add: sorted_list_of_set_def sort_conv_fold fold_set_fold_remdups)
   1.620  qed
   1.621  
   1.622  lemma sorted_list_of_set_remove: