1.1 --- a/src/HOL/Library/Dlist_Cset.thy	Mon Jul 25 14:10:12 2011 +0200
     1.2 +++ b/src/HOL/Library/Dlist_Cset.thy	Mon Jul 25 16:55:48 2011 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  begin
     1.5  
     1.6  definition Set :: "'a dlist \<Rightarrow> 'a Cset.set" where
     1.7 -  "Set dxs = List_Cset.set (list_of_dlist dxs)"
     1.8 +  "Set dxs = Cset.set (list_of_dlist dxs)"
     1.9  
    1.10  definition Coset :: "'a dlist \<Rightarrow> 'a Cset.set" where
    1.11    "Coset dxs = List_Cset.coset (list_of_dlist dxs)"
    1.12 @@ -27,6 +27,9 @@
    1.13  declare forall_set [code del]
    1.14  declare exists_set [code del]
    1.15  declare card_set [code del]
    1.16 +declare List_Cset.single_set [code del]
    1.17 +declare List_Cset.bind_set [code del]
    1.18 +declare List_Cset.pred_of_cset_set [code del]
    1.19  declare inter_project [code del]
    1.20  declare subtract_remove [code del]
    1.21  declare union_insert [code del]
    1.22 @@ -50,7 +53,7 @@
    1.23    by (simp add: Coset_def member_set not_set_compl)
    1.24  
    1.25  lemma Set_dlist_of_list [code]:
    1.26 -  "List_Cset.set xs = Set (dlist_of_list xs)"
    1.27 +  "Cset.set xs = Set (dlist_of_list xs)"
    1.28    by (rule Cset.set_eqI) simp
    1.29  
    1.30  lemma Coset_dlist_of_list [code]:
    1.31 @@ -137,4 +140,16 @@
    1.32  
    1.33  end
    1.34  
    1.35 +declare Cset.single_code[code]
    1.36 +
    1.37 +lemma bind_set [code]:
    1.38 +  "Cset.bind (Dlist_Cset.Set xs) f = foldl (\<lambda>A x. sup A (f x)) Cset.empty (list_of_dlist xs)"
    1.39 +by(simp add: List_Cset.bind_set Dlist_Cset.Set_def)
    1.40 +hide_fact (open) bind_set
    1.41 +
    1.42 +lemma pred_of_cset_set [code]:
    1.43 +  "pred_of_cset (Dlist_Cset.Set xs) = foldr sup (map Predicate.single (list_of_dlist xs)) bot"
    1.44 +by(simp add: List_Cset.pred_of_cset_set Dlist_Cset.Set_def)
    1.45 +hide_fact (open) pred_of_cset_set
    1.46 +
    1.47  end