1.1 --- a/src/HOL/BNF/Examples/Stream.thy	Wed Feb 06 17:57:21 2013 +0100
     1.2 +++ b/src/HOL/BNF/Examples/Stream.thy	Thu Feb 07 11:57:42 2013 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  imports "../BNF"
     1.5  begin
     1.6  
     1.7 -codata 'a stream = Stream (shd: 'a) (stl: "'a stream")
     1.8 +codata 'a stream = Stream (shd: 'a) (stl: "'a stream") (infixr "##" 65)
     1.9  
    1.10  (* TODO: Provide by the package*)
    1.11  theorem stream_set_induct:
    1.12 @@ -42,7 +42,7 @@
    1.13  
    1.14  primrec shift :: "'a list \<Rightarrow> 'a stream \<Rightarrow> 'a stream" (infixr "@-" 65) where
    1.15    "shift [] s = s"
    1.16 -| "shift (x # xs) s = Stream x (shift xs s)"
    1.17 +| "shift (x # xs) s = x ## shift xs s"
    1.18  
    1.19  lemma shift_append[simp]: "(xs @ ys) @- s = xs @- ys @- s"
    1.20  by (induct xs) auto
    1.21 @@ -71,10 +71,10 @@
    1.22    thus ?case using stream.unfold[of hd "\<lambda>xs. tl xs @ [hd xs]" u] by (auto simp: cycle_def)
    1.23  qed auto
    1.24  
    1.25 -lemma cycle_Cons: "cycle (x # xs) = Stream x (cycle (xs @ [x]))"
    1.26 -proof (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>x xs. s1 = cycle (x # xs) \<and> s2 = Stream x (cycle (xs @ [x]))"])
    1.27 +lemma cycle_Cons: "cycle (x # xs) = x ## cycle (xs @ [x])"
    1.28 +proof (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>x xs. s1 = cycle (x # xs) \<and> s2 = x ## cycle (xs @ [x])"])
    1.29    case (2 s1 s2)
    1.30 -  then obtain x xs where "s1 = cycle (x # xs) \<and> s2 = Stream x (cycle (xs @ [x]))" by blast
    1.31 +  then obtain x xs where "s1 = cycle (x # xs) \<and> s2 = x ## cycle (xs @ [x])" by blast
    1.32    thus ?case
    1.33      by (auto simp: cycle_def intro!: exI[of _ "hd (xs @ [x])"] exI[of _ "tl (xs @ [x])"] stream.unfold)
    1.34  qed auto
    1.35 @@ -83,7 +83,7 @@
    1.36    streams :: "'a set => 'a stream set"
    1.37    for A :: "'a set"
    1.38  where
    1.39 -  Stream[intro!, simp, no_atp]: "\<lbrakk>a \<in> A; s \<in> streams A\<rbrakk> \<Longrightarrow> Stream a s \<in> streams A"
    1.40 +  Stream[intro!, simp, no_atp]: "\<lbrakk>a \<in> A; s \<in> streams A\<rbrakk> \<Longrightarrow> a ## s \<in> streams A"
    1.41  
    1.42  lemma shift_streams: "\<lbrakk>w \<in> lists A; s \<in> streams A\<rbrakk> \<Longrightarrow> w @- s \<in> streams A"
    1.43  by (induct w) auto
    1.44 @@ -91,13 +91,13 @@
    1.45  lemma stream_set_streams:
    1.46    assumes "stream_set s \<subseteq> A"
    1.47    shows "s \<in> streams A"
    1.48 -proof (coinduct rule: streams.coinduct[of "\<lambda>s'. \<exists>a s. s' = Stream a s \<and> a \<in> A \<and> stream_set s \<subseteq> A"])
    1.49 +proof (coinduct rule: streams.coinduct[of "\<lambda>s'. \<exists>a s. s' = a ## s \<and> a \<in> A \<and> stream_set s \<subseteq> A"])
    1.50    case streams from assms show ?case by (cases s) auto
    1.51  next
    1.52 -  fix s' assume "\<exists>a s. s' = Stream a s \<and> a \<in> A \<and> stream_set s \<subseteq> A"
    1.53 +  fix s' assume "\<exists>a s. s' = a ## s \<and> a \<in> A \<and> stream_set s \<subseteq> A"
    1.54    then guess a s by (elim exE)
    1.55 -  with assms show "\<exists>a l. s' = Stream a l \<and>
    1.56 -    a \<in> A \<and> ((\<exists>a s. l = Stream a s \<and> a \<in> A \<and> stream_set s \<subseteq> A) \<or> l \<in> streams A)"
    1.57 +  with assms show "\<exists>a l. s' = a ## l \<and>
    1.58 +    a \<in> A \<and> ((\<exists>a s. l = a ## s \<and> a \<in> A \<and> stream_set s \<subseteq> A) \<or> l \<in> streams A)"
    1.59      by (cases s) auto
    1.60  qed
    1.61  
    1.62 @@ -105,17 +105,17 @@
    1.63  subsection {* flatten a stream of lists *}
    1.64  
    1.65  definition flat where
    1.66 -  "flat \<equiv> stream_unfold (hd o shd) (\<lambda>s. if tl (shd s) = [] then stl s else Stream (tl (shd s)) (stl s))"
    1.67 +  "flat \<equiv> stream_unfold (hd o shd) (\<lambda>s. if tl (shd s) = [] then stl s else tl (shd s) ## stl s)"
    1.68  
    1.69  lemma flat_simps[simp]:
    1.70    "shd (flat ws) = hd (shd ws)"
    1.71 -  "stl (flat ws) = flat (if tl (shd ws) = [] then stl ws else Stream (tl (shd ws)) (stl ws))"
    1.72 +  "stl (flat ws) = flat (if tl (shd ws) = [] then stl ws else tl (shd ws) ## stl ws)"
    1.73  unfolding flat_def by auto
    1.74  
    1.75 -lemma flat_Cons[simp]: "flat (Stream (x#xs) w) = Stream x (flat (if xs = [] then w else Stream xs w))"
    1.76 -unfolding flat_def using stream.unfold[of "hd o shd" _ "Stream (x#xs) w"] by auto
    1.77 +lemma flat_Cons[simp]: "flat ((x # xs) ## ws) = x ## flat (if xs = [] then ws else xs ## ws)"
    1.78 +unfolding flat_def using stream.unfold[of "hd o shd" _ "(x # xs) ## ws"] by auto
    1.79  
    1.80 -lemma flat_Stream[simp]: "xs \<noteq> [] \<Longrightarrow> flat (Stream xs ws) = xs @- flat ws"
    1.81 +lemma flat_Stream[simp]: "xs \<noteq> [] \<Longrightarrow> flat (xs ## ws) = xs @- flat ws"
    1.82  by (induct xs) auto
    1.83  
    1.84  lemma flat_unfold: "shd ws \<noteq> [] \<Longrightarrow> flat ws = shd ws @- flat (stl ws)"
    1.85 @@ -132,9 +132,9 @@
    1.86    "sdrop 0 s = s"
    1.87  | "sdrop (Suc n) s = sdrop n (stl s)"
    1.88  
    1.89 -primrec snth :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a" where
    1.90 -  "snth 0 s = shd s"
    1.91 -| "snth (Suc n) s = snth n (stl s)"
    1.92 +primrec snth :: "'a stream \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
    1.93 +  "s !! 0 = shd s"
    1.94 +| "s !! Suc n = stl s !! n"
    1.95  
    1.96  lemma stake_sdrop: "stake n s @- sdrop n s = s"
    1.97  by (induct n arbitrary: s) auto