# HG changeset patch
# User haftmann
# Date 1274257051 -7200
# Node ID 10aa84e6dd6607ae39f00000da613e37b04cc670
# Parent  e922a5124428c610a9ed62f678f9f97c2073ed46# Parent  684d9dbd3dfc3a1bec005ff3a8e11925732d47dc
merged

diff -r e922a5124428 -r 10aa84e6dd66 src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Wed May 19 10:17:05 2010 +0200
+++ b/src/HOL/Library/Dlist.thy	Wed May 19 10:17:31 2010 +0200
@@ -127,6 +127,16 @@
   by (simp add: filter_def)
 
 
+text {* Explicit executable conversion *}
+
+definition dlist_of_list [simp]:
+  "dlist_of_list = Dlist"
+
+lemma [code abstract]:
+  "list_of_dlist (dlist_of_list xs) = remdups xs"
+  by simp
+
+
 section {* Implementation of sets by distinct lists -- canonical! *}
 
 definition Set :: "'a dlist \<Rightarrow> 'a fset" where
@@ -148,9 +158,6 @@
 declare forall_Set [code del]
 declare exists_Set [code del]
 declare card_Set [code del]
-declare subfset_eq_forall [code del]
-declare subfset_subfset_eq [code del]
-declare eq_fset_subfset_eq [code del]
 declare inter_project [code del]
 declare subtract_remove [code del]
 declare union_insert [code del]
@@ -173,6 +180,14 @@
   "Fset.member (Coset dxs) = Not \<circ> List.member (list_of_dlist dxs)"
   by (simp add: Coset_def member_set not_set_compl)
 
+lemma Set_dlist_of_list [code]:
+  "Fset.Set xs = Set (dlist_of_list xs)"
+  by simp
+
+lemma Coset_dlist_of_list [code]:
+  "Fset.Coset xs = Coset (dlist_of_list xs)"
+  by simp
+
 lemma is_empty_Set [code]:
   "Fset.is_empty (Set dxs) \<longleftrightarrow> null dxs"
   by (simp add: null_def null_empty member_set)