1.1 --- a/src/HOL/Library/Dlist.thy	Wed May 19 10:17:05 2010 +0200
     1.2 +++ b/src/HOL/Library/Dlist.thy	Wed May 19 10:17:31 2010 +0200
     1.3 @@ -127,6 +127,16 @@
     1.4    by (simp add: filter_def)
     1.5  
     1.6  
     1.7 +text {* Explicit executable conversion *}
     1.8 +
     1.9 +definition dlist_of_list [simp]:
    1.10 +  "dlist_of_list = Dlist"
    1.11 +
    1.12 +lemma [code abstract]:
    1.13 +  "list_of_dlist (dlist_of_list xs) = remdups xs"
    1.14 +  by simp
    1.15 +
    1.16 +
    1.17  section {* Implementation of sets by distinct lists -- canonical! *}
    1.18  
    1.19  definition Set :: "'a dlist \<Rightarrow> 'a fset" where
    1.20 @@ -148,9 +158,6 @@
    1.21  declare forall_Set [code del]
    1.22  declare exists_Set [code del]
    1.23  declare card_Set [code del]
    1.24 -declare subfset_eq_forall [code del]
    1.25 -declare subfset_subfset_eq [code del]
    1.26 -declare eq_fset_subfset_eq [code del]
    1.27  declare inter_project [code del]
    1.28  declare subtract_remove [code del]
    1.29  declare union_insert [code del]
    1.30 @@ -173,6 +180,14 @@
    1.31    "Fset.member (Coset dxs) = Not \<circ> List.member (list_of_dlist dxs)"
    1.32    by (simp add: Coset_def member_set not_set_compl)
    1.33  
    1.34 +lemma Set_dlist_of_list [code]:
    1.35 +  "Fset.Set xs = Set (dlist_of_list xs)"
    1.36 +  by simp
    1.37 +
    1.38 +lemma Coset_dlist_of_list [code]:
    1.39 +  "Fset.Coset xs = Coset (dlist_of_list xs)"
    1.40 +  by simp
    1.41 +
    1.42  lemma is_empty_Set [code]:
    1.43    "Fset.is_empty (Set dxs) \<longleftrightarrow> null dxs"
    1.44    by (simp add: null_def null_empty member_set)