# HG changeset patch
# User haftmann
# Date 1285680105 -7200
# Node ID 38852e989efaf8ead18d8d5b1d0638a532ae4620
# Parent  1c46d4f8afd2b978da1ed63777623ed73763a6c0
lemma listsum_conv_fold

diff -r 1c46d4f8afd2 -r 38852e989efa src/HOL/Library/More_List.thy
--- a/src/HOL/Library/More_List.thy	Tue Sep 28 13:44:06 2010 +0200
+++ b/src/HOL/Library/More_List.thy	Tue Sep 28 15:21:45 2010 +0200
@@ -16,7 +16,6 @@
 declare (in linorder) Max_fin_set_fold [code_unfold del]
 declare (in complete_lattice) Inf_set_fold [code_unfold del]
 declare (in complete_lattice) Sup_set_fold [code_unfold del]
-declare rev_foldl_cons [code del]
 
 text {* Fold combinator with canonical argument order *}
 
@@ -101,11 +100,11 @@
   "fold plus xs = plus (listsum (rev xs))"
   by (induct xs) (simp_all add: add.assoc)
 
-lemma listsum_conv_foldr [code]:
-  "listsum xs = foldr plus xs 0"
-  by (fact listsum_foldr)
+lemma (in monoid_add) listsum_conv_fold [code]:
+  "listsum xs = fold (\<lambda>x y. y + x) xs 0"
+  by (auto simp add: listsum_foldl foldl_fold fun_eq_iff)
 
-lemma sort_key_conv_fold:
+lemma (in linorder) sort_key_conv_fold:
   assumes "inj_on f (set xs)"
   shows "sort_key f xs = fold (insort_key f) xs []"
 proof -
@@ -115,13 +114,14 @@
     fix x y
     assume "x \<in> set xs" "y \<in> set xs"
     with assms have *: "f y = f x \<Longrightarrow> y = x" by (auto dest: inj_onD)
+    have **: "x = y \<longleftrightarrow> y = x" by auto
     show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs"
-      by (induct zs) (auto dest: *)
+      by (induct zs) (auto intro: * simp add: **)
   qed
   then show ?thesis by (simp add: sort_key_def foldr_fold_rev)
 qed
 
-lemma sort_conv_fold:
+lemma (in linorder) sort_conv_fold:
   "sort xs = fold insort xs []"
   by (rule sort_key_conv_fold) simp