--- 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.
--- 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} *}
--- 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
+
--- 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 *)