src/HOL/HOLCF/IOA/meta_theory/Seq.thy

 (*  Title:      HOL/HOLCF/IOA/meta_theory/Seq.thy
     Author:     Olaf Müller
 *)
 
-section {* Partial, Finite and Infinite Sequences (lazy lists), modeled as domain *}
+section \<open>Partial, Finite and Infinite Sequences (lazy lists), modeled as domain\<close>
 
 theory Seq
 imports "../../HOLCF"
 begin
 

   Infinite :: "'a seq => bool"
 where
   "Infinite x == ~(seq_finite x)"
 
 
-subsection {* recursive equations of operators *}
-
-subsubsection {* smap *}
+subsection \<open>recursive equations of operators\<close>
+
+subsubsection \<open>smap\<close>
 
 fixrec
   smap :: "('a -> 'b) -> 'a seq -> 'b seq"
 where
   smap_nil: "smap$f$nil=nil"
 | smap_cons: "[|x~=UU|] ==> smap$f$(x##xs)= (f$x)##smap$f$xs"
 
 lemma smap_UU [simp]: "smap$f$UU=UU"
 by fixrec_simp
 
-subsubsection {* sfilter *}
+subsubsection \<open>sfilter\<close>
 
 fixrec
    sfilter :: "('a -> tr) -> 'a seq -> 'a seq"
 where
   sfilter_nil: "sfilter$P$nil=nil"

               (If P$x then x##(sfilter$P$xs) else sfilter$P$xs)"
 
 lemma sfilter_UU [simp]: "sfilter$P$UU=UU"
 by fixrec_simp
 
-subsubsection {* sforall2 *}
+subsubsection \<open>sforall2\<close>
 
 fixrec
   sforall2 :: "('a -> tr) -> 'a seq -> tr"
 where
   sforall2_nil: "sforall2$P$nil=TT"

 by fixrec_simp
 
 definition
   sforall_def: "sforall P t == (sforall2$P$t ~=FF)"
 
-subsubsection {* stakewhile *}
+subsubsection \<open>stakewhile\<close>
 
 fixrec
   stakewhile :: "('a -> tr)  -> 'a seq -> 'a seq"
 where
   stakewhile_nil: "stakewhile$P$nil=nil"

               (If P$x then x##(stakewhile$P$xs) else nil)"
 
 lemma stakewhile_UU [simp]: "stakewhile$P$UU=UU"
 by fixrec_simp
 
-subsubsection {* sdropwhile *}
+subsubsection \<open>sdropwhile\<close>
 
 fixrec
   sdropwhile :: "('a -> tr) -> 'a seq -> 'a seq"
 where
   sdropwhile_nil: "sdropwhile$P$nil=nil"

               (If P$x then sdropwhile$P$xs else x##xs)"
 
 lemma sdropwhile_UU [simp]: "sdropwhile$P$UU=UU"
 by fixrec_simp
 
-subsubsection {* slast *}
+subsubsection \<open>slast\<close>
 
 fixrec
   slast :: "'a seq -> 'a"
 where
   slast_nil: "slast$nil=UU"

     "x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs)"
 
 lemma slast_UU [simp]: "slast$UU=UU"
 by fixrec_simp
 
-subsubsection {* sconc *}
+subsubsection \<open>sconc\<close>
 
 fixrec
   sconc :: "'a seq -> 'a seq -> 'a seq"
 where
   sconc_nil: "sconc$nil$y = y"

 apply simp_all
 done
 
 declare sconc_cons' [simp del]
 
-subsubsection {* sflat *}
+subsubsection \<open>sflat\<close>
 
 fixrec
   sflat :: "('a seq) seq -> 'a seq"
 where
   sflat_nil: "sflat$nil=nil"

 lemma sflat_cons [simp]: "sflat$(x##xs)= x@@(sflat$xs)"
 by (cases "x=UU", simp_all)
 
 declare sflat_cons' [simp del]
 
-subsubsection {* szip *}
+subsubsection \<open>szip\<close>
 
 fixrec
   szip :: "'a seq -> 'b seq -> ('a*'b) seq"
 where
   szip_nil: "szip$nil$y=nil"