src/HOL/HOLCF/Library/List_Predomain.thy

 (*  Title:      HOL/HOLCF/Library/List_Predomain.thy
     Author:     Brian Huffman
 *)
 
-section {* Predomain class instance for HOL list type *}
+section \<open>Predomain class instance for HOL list type\<close>
 
 theory List_Predomain
 imports List_Cpo Sum_Cpo
 begin
 
-subsection {* Strict list type *}
+subsection \<open>Strict list type\<close>
 
 domain 'a slist = SNil | SCons "'a" "'a slist"
 
-text {* Polymorphic map function for strict lists. *}
+text \<open>Polymorphic map function for strict lists.\<close>
 
-text {* FIXME: The domain package should generate this! *}
+text \<open>FIXME: The domain package should generate this!\<close>
 
 fixrec slist_map' :: "('a \<rightarrow> 'b) \<rightarrow> 'a slist \<rightarrow> 'b slist"
   where "slist_map'\<cdot>f\<cdot>SNil = SNil"
   | "\<lbrakk>x \<noteq> \<bottom>; xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow>
       slist_map'\<cdot>f\<cdot>(SCons\<cdot>x\<cdot>xs) = SCons\<cdot>(f\<cdot>x)\<cdot>(slist_map'\<cdot>f\<cdot>xs)"

 apply (subst slist_map'_ID [symmetric])
 apply (intro monofun_cfun below_refl)
 apply (simp add: cfun_below_iff ep_pair.e_p_below)
 done
 
-text {*
+text \<open>
   Types @{typ "'a list u"}. and @{typ "'a u slist"} are isomorphic.
-*}
+\<close>
 
 fixrec encode_list_u where
   "encode_list_u\<cdot>(up\<cdot>[]) = SNil" |
   "encode_list_u\<cdot>(up\<cdot>(x # xs)) = SCons\<cdot>(up\<cdot>x)\<cdot>(encode_list_u\<cdot>(up\<cdot>xs))"
 

 apply (induct y, simp, simp)
 apply (case_tac a, simp)
 apply (case_tac "decode_list_u\<cdot>y", simp, simp)
 done
 
-subsection {* Lists are a predomain *}
+subsection \<open>Lists are a predomain\<close>
 
 definition list_liftdefl :: "udom u defl \<rightarrow> udom u defl"
   where "list_liftdefl = (\<Lambda> a. udefl\<cdot>(slist_defl\<cdot>(u_liftdefl\<cdot>a)))"
 
 lemma cast_slist_defl: "cast\<cdot>(slist_defl\<cdot>a) = emb oo slist_map\<cdot>(cast\<cdot>a) oo prj"

     done
 qed
 
 end
 
-subsection {* Configuring domain package to work with list type *}
+subsection \<open>Configuring domain package to work with list type\<close>
 
 lemma liftdefl_list [domain_defl_simps]:
   "LIFTDEFL('a::predomain list) = list_liftdefl\<cdot>LIFTDEFL('a)"
 by (rule liftdefl_list_def)
 

 apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_liftdefl)
 apply (simp add: cfcomp1 encode_list_u_map)
 apply (simp add: slist_map'_slist_map' u_emb_bottom)
 done
 
-setup {*
+setup \<open>
   Domain_Take_Proofs.add_rec_type (@{type_name "list"}, [true])
-*}
+\<close>
 
 end