src/HOL/Library/RBT_Set.thy
changeset 49758 718f10c8bbfc
parent 49757 73ab6d4a9236
child 49928 e3f0a92de280
     1.1 --- a/src/HOL/Library/RBT_Set.thy	Tue Oct 09 16:57:58 2012 +0200
     1.2 +++ b/src/HOL/Library/RBT_Set.thy	Tue Oct 09 16:58:36 2012 +0200
     1.3 @@ -187,9 +187,9 @@
     1.4  definition rbt_filter :: "('a :: linorder \<Rightarrow> bool) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'a set" where
     1.5    "rbt_filter P t = fold (\<lambda>k _ A'. if P k then Set.insert k A' else A') t {}"
     1.6  
     1.7 -lemma finite_filter_rbt_filter:
     1.8 -  "Finite_Set.filter P (Set t) = rbt_filter P t"
     1.9 -by (simp add: fold_keys_def Finite_Set.filter_def rbt_filter_def 
    1.10 +lemma Set_filter_rbt_filter:
    1.11 +  "Set.filter P (Set t) = rbt_filter P t"
    1.12 +by (simp add: fold_keys_def Set_filter_fold rbt_filter_def 
    1.13    finite_fold_fold_keys[OF comp_fun_commute_filter_fold])
    1.14  
    1.15  
    1.16 @@ -568,7 +568,7 @@
    1.17  
    1.18  lemma inter_Set [code]:
    1.19    "A \<inter> Set t = rbt_filter (\<lambda>k. k \<in> A) t"
    1.20 -by (simp add: inter_filter finite_filter_rbt_filter)
    1.21 +by (simp add: inter_Set_filter Set_filter_rbt_filter)
    1.22  
    1.23  lemma minus_Set [code]:
    1.24    "A - Set t = fold_keys Set.remove t A"
    1.25 @@ -604,7 +604,7 @@
    1.26  
    1.27  lemma filter_Set [code]:
    1.28    "Set.filter P (Set t) = (rbt_filter P t)"
    1.29 -by (auto simp add: project_filter finite_filter_rbt_filter)
    1.30 +by (auto simp add: Set_filter_rbt_filter)
    1.31  
    1.32  lemma image_Set [code]:
    1.33    "image f (Set t) = fold_keys (\<lambda>k A. Set.insert (f k) A) t {}"