# HG changeset patch
# User kuncar
# Date 1349794716 -7200
# Node ID 718f10c8bbfcd40dc9314dec017b82300c62f465
# Parent  73ab6d4a9236fc44fb920a1562cd506ac0195223
use Set.filter instead of Finite_Set.filter, which is removed then

diff -r 73ab6d4a9236 -r 718f10c8bbfc src/HOL/Finite_Set.thy
--- 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
 
diff -r 73ab6d4a9236 -r 718f10c8bbfc src/HOL/Library/RBT_Set.thy
--- 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 {}"