# HG changeset patch
# User haftmann
# Date 1274253636 -7200
# Node ID 1a4cc941171aa72f258da3f96aea24e1727319d6
# Parent  4ec5131c6f4604737928be82f4186b55e49b5a66
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets

diff -r 4ec5131c6f46 -r 1a4cc941171a src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Tue May 18 06:28:42 2010 -0700
+++ b/src/HOL/Library/Dlist.thy	Wed May 19 09:20:36 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)