use Set.filter instead of Finite_Set.filter, which is removed then
authorkuncar
Tue Oct 09 16:58:36 2012 +0200 (2012-10-09)
changeset 49758718f10c8bbfc
parent 49757 73ab6d4a9236
child 49759 ecf1d5d87e5e
use Set.filter instead of Finite_Set.filter, which is removed then
src/HOL/Finite_Set.thy
src/HOL/Library/RBT_Set.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Tue Oct 09 16:57:58 2012 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Oct 09 16:58:36 2012 +0200
     1.3 @@ -848,27 +848,24 @@
     1.4    then show ?thesis ..
     1.5  qed
     1.6  
     1.7 -definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" 
     1.8 -  where "filter P A = fold (\<lambda>x A'. if P x then Set.insert x A' else A') {} A"
     1.9 -
    1.10  lemma comp_fun_commute_filter_fold: "comp_fun_commute (\<lambda>x A'. if P x then Set.insert x A' else A')"
    1.11  proof - 
    1.12    interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
    1.13    show ?thesis by default (auto simp: fun_eq_iff)
    1.14  qed
    1.15  
    1.16 -lemma inter_filter:     
    1.17 -  assumes "finite B"
    1.18 -  shows "A \<inter> B = filter (\<lambda>x. x \<in> A) B"
    1.19 -using assms 
    1.20 -by (induct B) (auto simp: filter_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold])
    1.21 -
    1.22 -lemma project_filter:
    1.23 +lemma Set_filter_fold:
    1.24    assumes "finite A"
    1.25 -  shows "Set.filter P A = filter P A"
    1.26 +  shows "Set.filter P A = fold (\<lambda>x A'. if P x then Set.insert x A' else A') {} A"
    1.27  using assms
    1.28  by (induct A) 
    1.29 -  (auto simp add: filter_def Set.filter_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold])
    1.30 +  (auto simp add: Set.filter_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold])
    1.31 +
    1.32 +lemma inter_Set_filter:     
    1.33 +  assumes "finite B"
    1.34 +  shows "A \<inter> B = Set.filter (\<lambda>x. x \<in> A) B"
    1.35 +using assms 
    1.36 +by (induct B) (auto simp: Set.filter_def)
    1.37  
    1.38  lemma image_fold_insert:
    1.39    assumes "finite A"
    1.40 @@ -2457,7 +2454,7 @@
    1.41      by simp
    1.42  qed
    1.43  
    1.44 -hide_const (open) Finite_Set.fold Finite_Set.filter
    1.45 +hide_const (open) Finite_Set.fold
    1.46  
    1.47  end
    1.48  
     2.1 --- a/src/HOL/Library/RBT_Set.thy	Tue Oct 09 16:57:58 2012 +0200
     2.2 +++ b/src/HOL/Library/RBT_Set.thy	Tue Oct 09 16:58:36 2012 +0200
     2.3 @@ -187,9 +187,9 @@
     2.4  definition rbt_filter :: "('a :: linorder \<Rightarrow> bool) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'a set" where
     2.5    "rbt_filter P t = fold (\<lambda>k _ A'. if P k then Set.insert k A' else A') t {}"
     2.6  
     2.7 -lemma finite_filter_rbt_filter:
     2.8 -  "Finite_Set.filter P (Set t) = rbt_filter P t"
     2.9 -by (simp add: fold_keys_def Finite_Set.filter_def rbt_filter_def 
    2.10 +lemma Set_filter_rbt_filter:
    2.11 +  "Set.filter P (Set t) = rbt_filter P t"
    2.12 +by (simp add: fold_keys_def Set_filter_fold rbt_filter_def 
    2.13    finite_fold_fold_keys[OF comp_fun_commute_filter_fold])
    2.14  
    2.15  
    2.16 @@ -568,7 +568,7 @@
    2.17  
    2.18  lemma inter_Set [code]:
    2.19    "A \<inter> Set t = rbt_filter (\<lambda>k. k \<in> A) t"
    2.20 -by (simp add: inter_filter finite_filter_rbt_filter)
    2.21 +by (simp add: inter_Set_filter Set_filter_rbt_filter)
    2.22  
    2.23  lemma minus_Set [code]:
    2.24    "A - Set t = fold_keys Set.remove t A"
    2.25 @@ -604,7 +604,7 @@
    2.26  
    2.27  lemma filter_Set [code]:
    2.28    "Set.filter P (Set t) = (rbt_filter P t)"
    2.29 -by (auto simp add: project_filter finite_filter_rbt_filter)
    2.30 +by (auto simp add: Set_filter_rbt_filter)
    2.31  
    2.32  lemma image_Set [code]:
    2.33    "image f (Set t) = fold_keys (\<lambda>k A. Set.insert (f k) A) t {}"