1.1 --- a/src/HOL/BNF/Examples/Stream.thy	Wed Dec 11 20:57:47 2013 +0100
     1.2 +++ b/src/HOL/BNF/Examples/Stream.thy	Wed Dec 11 17:30:51 2013 +0100
     1.3 @@ -13,24 +13,13 @@
     1.4  begin
     1.5  
     1.6  codatatype (sset: 'a) stream (map: smap rel: stream_all2) =
     1.7 -  Stream (shd: 'a) (stl: "'a stream") (infixr "##" 65)
     1.8 -
     1.9 -code_datatype Stream
    1.10 -
    1.11 -lemma stream_case_cert:
    1.12 -  assumes "CASE \<equiv> case_stream c"
    1.13 -  shows "CASE (a ## s) \<equiv> c a s"
    1.14 -  using assms by simp_all
    1.15 -
    1.16 -setup {*
    1.17 -  Code.add_case @{thm stream_case_cert}
    1.18 -*}
    1.19 +  SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
    1.20  
    1.21  (*for code generation only*)
    1.22  definition smember :: "'a \<Rightarrow> 'a stream \<Rightarrow> bool" where
    1.23    [code_abbrev]: "smember x s \<longleftrightarrow> x \<in> sset s"
    1.24  
    1.25 -lemma smember_code[code, simp]: "smember x (Stream y s) = (if x = y then True else smember x s)"
    1.26 +lemma smember_code[code, simp]: "smember x (y ## s) = (if x = y then True else smember x s)"
    1.27    unfolding smember_def by auto
    1.28  
    1.29  hide_const (open) smember
    1.30 @@ -41,8 +30,8 @@
    1.31      \<forall>y \<in> sset s. P y s"
    1.32    apply (rule stream.dtor_set_induct)
    1.33    apply (auto simp add: shd_def stl_def fsts_def snds_def split_beta)
    1.34 -  apply (metis Stream_def fst_conv stream.case stream.dtor_ctor stream.exhaust)
    1.35 -  by (metis Stream_def sndI stl_def stream.collapse stream.dtor_ctor)
    1.36 +  apply (metis SCons_def fst_conv stream.case stream.dtor_ctor stream.exhaust)
    1.37 +  by (metis SCons_def sndI stl_def stream.collapse stream.dtor_ctor)
    1.38  
    1.39  lemma smap_simps[simp]:
    1.40    "shd (smap f s) = f (shd s)" "stl (smap f s) = smap f (stl s)"
    1.41 @@ -223,8 +212,8 @@
    1.42  partial_function (tailrec) sdrop_while :: "('a \<Rightarrow> bool) \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where 
    1.43    "sdrop_while P s = (if P (shd s) then sdrop_while P (stl s) else s)"
    1.44  
    1.45 -lemma sdrop_while_Stream[code]:
    1.46 -  "sdrop_while P (Stream a s) = (if P a then sdrop_while P s else Stream a s)"
    1.47 +lemma sdrop_while_SCons[code]:
    1.48 +  "sdrop_while P (a ## s) = (if P a then sdrop_while P s else a ## s)"
    1.49    by (subst sdrop_while.simps) simp
    1.50  
    1.51  lemma sdrop_while_sdrop_LEAST:
    1.52 @@ -249,9 +238,9 @@
    1.53  
    1.54  lemma sfilter_Stream: "sfilter P (x ## s) = (if P x then x ## sfilter P s else sfilter P s)"
    1.55  proof (cases "P x")
    1.56 -  case True thus ?thesis by (subst sfilter.ctr) (simp add: sdrop_while_Stream)
    1.57 +  case True thus ?thesis by (subst sfilter.ctr) (simp add: sdrop_while_SCons)
    1.58  next
    1.59 -  case False thus ?thesis by (subst (1 2) sfilter.ctr) (simp add: sdrop_while_Stream)
    1.60 +  case False thus ?thesis by (subst (1 2) sfilter.ctr) (simp add: sdrop_while_SCons)
    1.61  qed
    1.62  
    1.63  
    1.64 @@ -274,6 +263,7 @@
    1.65  primcorec cycle :: "'a list \<Rightarrow> 'a stream" where
    1.66    "shd (cycle xs) = hd xs"
    1.67  | "stl (cycle xs) = cycle (tl xs @ [hd xs])"
    1.68 +
    1.69  lemma cycle_decomp: "u \<noteq> [] \<Longrightarrow> cycle u = u @- cycle u"
    1.70  proof (coinduction arbitrary: u)
    1.71    case Eq_stream then show ?case using stream.collapse[of "cycle u"]
    1.72 @@ -371,7 +361,7 @@
    1.73  abbreviation "nats \<equiv> fromN 0"
    1.74  
    1.75  lemma sset_fromN[simp]: "sset (fromN n) = {n ..}"
    1.76 -  by (auto simp add: sset_siterate) arith
    1.77 +  by (auto simp add: sset_siterate le_iff_add)
    1.78  
    1.79  
    1.80  subsection {* flatten a stream of lists *}
    1.81 @@ -512,7 +502,7 @@
    1.82    "shd (szip s1 s2) = (shd s1, shd s2)"
    1.83  | "stl (szip s1 s2) = szip (stl s1) (stl s2)"
    1.84  
    1.85 -lemma szip_unfold[code]: "szip (Stream a s1) (Stream b s2) = Stream (a, b) (szip s1 s2)"
    1.86 +lemma szip_unfold[code]: "szip (a ## s1) (b ## s2) = (a, b) ## (szip s1 s2)"
    1.87    by (subst szip.ctr) simp
    1.88  
    1.89  lemma snth_szip[simp]: "szip s1 s2 !! n = (s1 !! n, s2 !! n)"
    1.90 @@ -526,7 +516,7 @@
    1.91  | "stl (smap2 f s1 s2) = smap2 f (stl s1) (stl s2)"
    1.92  
    1.93  lemma smap2_unfold[code]:
    1.94 -  "smap2 f (Stream a s1) (Stream b s2) = Stream (f a b) (smap2 f s1 s2)"
    1.95 +  "smap2 f (a ## s1) (b ## s2) = f a b ## (smap2 f s1 s2)"
    1.96    by (subst smap2.ctr) simp
    1.97  
    1.98  lemma smap2_szip: