src/HOL/Library/RBT_Set.thy
changeset 49757 73ab6d4a9236
parent 48623 bea613f2543d
child 49758 718f10c8bbfc
equal deleted inserted replaced
49746:5073cb632b6c 49757:73ab6d4a9236
    47 
    47 
    48 lemma [code, code del]:
    48 lemma [code, code del]:
    49   "UNIV = UNIV" ..
    49   "UNIV = UNIV" ..
    50 
    50 
    51 lemma [code, code del]:
    51 lemma [code, code del]:
    52   "Set.project = Set.project" ..
    52   "Set.filter = Set.filter" ..
    53 
    53 
    54 lemma [code, code del]:
    54 lemma [code, code del]:
    55   "image = image" ..
    55   "image = image" ..
    56 
    56 
    57 lemma [code, code del]:
    57 lemma [code, code del]:
   600 
   600 
   601 lemma minus_Coset [code]:
   601 lemma minus_Coset [code]:
   602   "A - Coset t = rbt_filter (\<lambda>k. k \<in> A) t"
   602   "A - Coset t = rbt_filter (\<lambda>k. k \<in> A) t"
   603 by (simp add: inter_Set[simplified Int_commute])
   603 by (simp add: inter_Set[simplified Int_commute])
   604 
   604 
   605 lemma project_Set [code]:
   605 lemma filter_Set [code]:
   606   "Set.project P (Set t) = (rbt_filter P t)"
   606   "Set.filter P (Set t) = (rbt_filter P t)"
   607 by (auto simp add: project_filter finite_filter_rbt_filter)
   607 by (auto simp add: project_filter finite_filter_rbt_filter)
   608 
   608 
   609 lemma image_Set [code]:
   609 lemma image_Set [code]:
   610   "image f (Set t) = fold_keys (\<lambda>k A. Set.insert (f k) A) t {}"
   610   "image f (Set t) = fold_keys (\<lambda>k A. Set.insert (f k) A) t {}"
   611 proof -
   611 proof -