src/HOL/Quotient_Examples/DList.thy

 
 Based on typedef version "Library/Dlist" by Florian Haftmann
 and theory morphism version by Maksym Bortin
 *)
 
-section {* Lists with distinct elements *}
+section \<open>Lists with distinct elements\<close>
 
 theory DList
 imports "~~/src/HOL/Library/Quotient_List"
 begin
 
-text {* Some facts about lists *}
+text \<open>Some facts about lists\<close>
 
 lemma remdups_removeAll_commute[simp]:
   "remdups (removeAll x l) = removeAll x (remdups l)"
   by (induct l) auto
 

   using assms
   unfolding fun_eq_iff List.member_def
   by (induct xa ya rule: list_induct2')
      (metis remdups_nil_noteq_cons set_remdups)+
 
-text {* Setting up the quotient type *}
+text \<open>Setting up the quotient type\<close>
 
 definition
   dlist_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
 where
   [simp]: "dlist_eq xs ys \<longleftrightarrow> remdups xs = remdups ys"

 
 quotient_type
   'a dlist = "'a list" / "dlist_eq"
   by (rule dlist_eq_equivp)
 
-text {* respectfulness and constant definitions *}
+text \<open>respectfulness and constant definitions\<close>
 
 definition [simp]: "card_remdups = length \<circ> remdups"
 definition [simp]: "foldr_remdups f xs e = foldr f (remdups xs) e"
 
 quotient_definition empty where "empty :: 'a dlist"

   is "List.filter" by (metis dlist_eq_def remdups_filter)
 
 quotient_definition "list_of_dlist :: 'a dlist \<Rightarrow> 'a list"
   is "remdups" by simp
 
-text {* lifted theorems *}
+text \<open>lifted theorems\<close>
 
 lemma dlist_member_insert:
   "member dl x \<Longrightarrow> insert x dl = dl"
   by descending (simp add: List.member_def)