--- a/src/HOL/Finite_Set.thy Tue Oct 09 16:57:58 2012 +0200
+++ b/src/HOL/Finite_Set.thy Tue Oct 09 16:58:36 2012 +0200
@@ -848,27 +848,24 @@
then show ?thesis ..
qed
-definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"
- where "filter P A = fold (\<lambda>x A'. if P x then Set.insert x A' else A') {} A"
-
lemma comp_fun_commute_filter_fold: "comp_fun_commute (\<lambda>x A'. if P x then Set.insert x A' else A')"
proof -
interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
show ?thesis by default (auto simp: fun_eq_iff)
qed
-lemma inter_filter:
- assumes "finite B"
- shows "A \<inter> B = filter (\<lambda>x. x \<in> A) B"
-using assms
-by (induct B) (auto simp: filter_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold])
-
-lemma project_filter:
+lemma Set_filter_fold:
assumes "finite A"
- shows "Set.filter P A = filter P A"
+ shows "Set.filter P A = fold (\<lambda>x A'. if P x then Set.insert x A' else A') {} A"
using assms
by (induct A)
- (auto simp add: filter_def Set.filter_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold])
+ (auto simp add: Set.filter_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold])
+
+lemma inter_Set_filter:
+ assumes "finite B"
+ shows "A \<inter> B = Set.filter (\<lambda>x. x \<in> A) B"
+using assms
+by (induct B) (auto simp: Set.filter_def)
lemma image_fold_insert:
assumes "finite A"
@@ -2457,7 +2454,7 @@
by simp
qed
-hide_const (open) Finite_Set.fold Finite_Set.filter
+hide_const (open) Finite_Set.fold
end
--- a/src/HOL/Library/RBT_Set.thy Tue Oct 09 16:57:58 2012 +0200
+++ b/src/HOL/Library/RBT_Set.thy Tue Oct 09 16:58:36 2012 +0200
@@ -187,9 +187,9 @@
definition rbt_filter :: "('a :: linorder \<Rightarrow> bool) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'a set" where
"rbt_filter P t = fold (\<lambda>k _ A'. if P k then Set.insert k A' else A') t {}"
-lemma finite_filter_rbt_filter:
- "Finite_Set.filter P (Set t) = rbt_filter P t"
-by (simp add: fold_keys_def Finite_Set.filter_def rbt_filter_def
+lemma Set_filter_rbt_filter:
+ "Set.filter P (Set t) = rbt_filter P t"
+by (simp add: fold_keys_def Set_filter_fold rbt_filter_def
finite_fold_fold_keys[OF comp_fun_commute_filter_fold])
@@ -568,7 +568,7 @@
lemma inter_Set [code]:
"A \<inter> Set t = rbt_filter (\<lambda>k. k \<in> A) t"
-by (simp add: inter_filter finite_filter_rbt_filter)
+by (simp add: inter_Set_filter Set_filter_rbt_filter)
lemma minus_Set [code]:
"A - Set t = fold_keys Set.remove t A"
@@ -604,7 +604,7 @@
lemma filter_Set [code]:
"Set.filter P (Set t) = (rbt_filter P t)"
-by (auto simp add: project_filter finite_filter_rbt_filter)
+by (auto simp add: Set_filter_rbt_filter)
lemma image_Set [code]:
"image f (Set t) = fold_keys (\<lambda>k A. Set.insert (f k) A) t {}"