src/HOL/Library/Dlist.thy

 (* Author: Florian Haftmann, TU Muenchen *)
 
 header {* Lists with elements distinct as canonical example for datatype invariants *}
 
 theory Dlist
-imports Main More_List Fset
+imports Main Fset
 begin
 
 section {* The type of distinct lists *}
 
 typedef (open) 'a dlist = "{xs::'a list. distinct xs}"

 declare Infimum_inf [code del]
 declare Supremum_sup [code del]
 
 lemma Set_Dlist [simp]:
   "Set (Dlist xs) = Fset (set xs)"
-  by (simp add: Set_def Fset.Set_def)
+  by (rule fset_eqI) (simp add: Set_def)
 
 lemma Coset_Dlist [simp]:
   "Coset (Dlist xs) = Fset (- set xs)"
-  by (simp add: Coset_def Fset.Coset_def)
+  by (rule fset_eqI) (simp add: Coset_def)
 
 lemma member_Set [simp]:
   "Fset.member (Set dxs) = List.member (list_of_dlist dxs)"
   by (simp add: Set_def member_set)
 

   "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
+  by (rule fset_eqI) simp
 
 lemma Coset_dlist_of_list [code]:
   "Fset.Coset xs = Coset (dlist_of_list xs)"
-  by simp
+  by (rule fset_eqI) simp
 
 lemma is_empty_Set [code]:
   "Fset.is_empty (Set dxs) \<longleftrightarrow> null dxs"
   by (simp add: null_def null_empty member_set)
 

   by (simp_all add: member_def)
 
 lemma compl_code [code]:
   "- Set dxs = Coset dxs"
   "- Coset dxs = Set dxs"
-  by (simp_all add: not_set_compl member_set)
+  by (rule fset_eqI, simp add: member_set not_set_compl)+
 
 lemma map_code [code]:
   "Fset.map f (Set dxs) = Set (map f dxs)"
-  by (simp add: member_set)
+  by (rule fset_eqI) (simp add: member_set)
   
 lemma filter_code [code]:
   "Fset.filter f (Set dxs) = Set (filter f dxs)"
-  by (simp add: member_set)
+  by (rule fset_eqI) (simp add: member_set)
 
 lemma forall_Set [code]:
   "Fset.forall P (Set xs) \<longleftrightarrow> list_all P (list_of_dlist xs)"
   by (simp add: member_set list_all_iff)