# HG changeset patch
# User haftmann
# Date 1333733031 -7200
# Node ID b72fa7bf9a10ce2acf17244497ba88e55d51df8d
# Parent  07bcf80391d06fc03e7729f04eb44c499b71b19a
abandoned almost redundant *_foldr lemmas

diff -r 07bcf80391d0 -r b72fa7bf9a10 NEWS
--- a/NEWS	Fri Apr 06 19:18:00 2012 +0200
+++ b/NEWS	Fri Apr 06 19:23:51 2012 +0200
@@ -226,7 +226,14 @@
 INCOMPATIBILITY.  For the common phrases "%xs. List.foldr plus xs 0"
 and "List.foldl plus 0", prefer "List.listsum".  Otherwise it can
 be useful to boil down "List.foldr" and "List.foldl" to "List.fold"
-by unfolding "foldr_conv_fold" and "foldl_conv_fold".  
+by unfolding "foldr_conv_fold" and "foldl_conv_fold".
+
+* Dropped lemmas minus_set_foldr, union_set_foldr, union_coset_foldr,
+inter_coset_foldr, Inf_fin_set_foldr, Sup_fin_set_foldr,
+Min_fin_set_foldr, Max_fin_set_foldr, Inf_set_foldr, Sup_set_foldr,
+INF_set_foldr, SUP_set_foldr.  INCOMPATIBILITY.  Prefer corresponding
+lemmas over fold rather than foldr, or make use of lemmas
+fold_conv_foldr and fold_rev.
 
 * Congruence rules Option.map_cong and Option.bind_cong for recursion
 through option types.
diff -r 07bcf80391d0 -r b72fa7bf9a10 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Apr 06 19:18:00 2012 +0200
+++ b/src/HOL/List.thy	Fri Apr 06 19:23:51 2012 +0200
@@ -2641,58 +2641,6 @@
   "concat xss = foldr append xss []"
   by (simp add: fold_append_concat_rev foldr_conv_fold)
 
-lemma minus_set_foldr:
-  "A - set xs = foldr Set.remove xs A"
-proof -
-  have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y"
-    by (auto simp add: remove_def)
-  then show ?thesis by (simp add: minus_set_fold foldr_fold)
-qed
-
-lemma union_set_foldr:
-  "set xs \<union> A = foldr Set.insert xs A"
-proof -
-  have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
-    by auto
-  then show ?thesis by (simp add: union_set_fold foldr_fold)
-qed
-
-lemma inter_coset_foldr:
-  "A \<inter> List.coset xs = foldr Set.remove xs A"
-  by (simp add: Diff_eq [symmetric] minus_set_foldr)
-
-lemma (in lattice) Inf_fin_set_foldr:
-  "Inf_fin (set (x # xs)) = foldr inf xs x"
-  by (simp add: Inf_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
-
-lemma (in lattice) Sup_fin_set_foldr:
-  "Sup_fin (set (x # xs)) = foldr sup xs x"
-  by (simp add: Sup_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
-
-lemma (in linorder) Min_fin_set_foldr:
-  "Min (set (x # xs)) = foldr min xs x"
-  by (simp add: Min_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
-
-lemma (in linorder) Max_fin_set_foldr:
-  "Max (set (x # xs)) = foldr max xs x"
-  by (simp add: Max_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
-
-lemma (in complete_lattice) Inf_set_foldr:
-  "Inf (set xs) = foldr inf xs top"
-  by (simp add: Inf_set_fold ac_simps foldr_fold fun_eq_iff)
-
-lemma (in complete_lattice) Sup_set_foldr:
-  "Sup (set xs) = foldr sup xs bot"
-  by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff)
-
-lemma (in complete_lattice) INF_set_foldr:
-  "INFI (set xs) f = foldr (inf \<circ> f) xs top"
-  by (simp only: INF_def Inf_set_foldr foldr_map set_map [symmetric])
-
-lemma (in complete_lattice) SUP_set_foldr:
-  "SUPR (set xs) f = foldr (sup \<circ> f) xs bot"
-  by (simp only: SUP_def Sup_set_foldr foldr_map set_map [symmetric])
-
 
 subsubsection {* @{text upt} *}
 
diff -r 07bcf80391d0 -r b72fa7bf9a10 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Fri Apr 06 19:18:00 2012 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Fri Apr 06 19:23:51 2012 +0200
@@ -408,7 +408,7 @@
 
 lemma [code]:
   "unstables r step ss = 
-   foldr (\<lambda>p A. if \<not>stable r step ss p then insert p A else A) [0..<size ss] {}"
+   fold (\<lambda>p A. if \<not>stable r step ss p then insert p A else A) [0..<size ss] {}"
 proof -
   have "unstables r step ss = (UN p:{..<size ss}. if \<not>stable r step ss p then {p} else {})"
     apply (unfold unstables_def)
@@ -425,7 +425,7 @@
     apply simp+
     done
   also have "\<And>f. (UN p:{..<size ss}. f p) = Union (set (map f [0..<size ss]))" by auto
-  also note Sup_set_foldr also note foldr_map
+  also note Sup_set_fold also note fold_map
   also have "op \<union> \<circ> (\<lambda>p. if \<not> stable r step ss p then {p} else {}) = 
             (\<lambda>p A. if \<not>stable r step ss p then insert p A else A)"
     by(auto simp add: fun_eq_iff)
@@ -486,3 +486,4 @@
 *}
 
 end
+
diff -r 07bcf80391d0 -r b72fa7bf9a10 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Fri Apr 06 19:18:00 2012 +0200
+++ b/src/HOL/Predicate.thy	Fri Apr 06 19:23:51 2012 +0200
@@ -702,7 +702,8 @@
 
 text {* Misc *}
 
-declare Inf_set_foldr [where 'a = "'a Predicate.pred", code] Sup_set_foldr [where 'a = "'a Predicate.pred", code]
+declare Inf_set_fold [where 'a = "'a Predicate.pred", code]
+declare Sup_set_fold [where 'a = "'a Predicate.pred", code]
 
 (* FIXME: better implement conversion by bisection *)