1.1 --- a/src/HOL/BNF/Examples/Stream.thy	Mon Nov 18 17:14:01 2013 +0100
     1.2 +++ b/src/HOL/BNF/Examples/Stream.thy	Mon Nov 18 17:15:01 2013 +0100
     1.3 @@ -319,62 +319,60 @@
     1.4    by (induct n arbitrary: u) (auto simp: rotate1_rotate_swap rotate1_hd_tl rotate_conv_mod[symmetric])
     1.5  
     1.6  
     1.7 +subsection {* iterated application of a function *}
     1.8 +
     1.9 +primcorec siterate where
    1.10 +  "shd (siterate f x) = x"
    1.11 +| "stl (siterate f x) = siterate f (f x)"
    1.12 +
    1.13 +lemma stake_Suc: "stake (Suc n) s = stake n s @ [s !! n]"
    1.14 +  by (induct n arbitrary: s) auto
    1.15 +
    1.16 +lemma snth_siterate[simp]: "siterate f x !! n = (f^^n) x"
    1.17 +  by (induct n arbitrary: x) (auto simp: funpow_swap1)
    1.18 +
    1.19 +lemma sdrop_siterate[simp]: "sdrop n (siterate f x) = siterate f ((f^^n) x)"
    1.20 +  by (induct n arbitrary: x) (auto simp: funpow_swap1)
    1.21 +
    1.22 +lemma stake_siterate[simp]: "stake n (siterate f x) = map (\<lambda>n. (f^^n) x) [0 ..< n]"
    1.23 +  by (induct n arbitrary: x) (auto simp del: stake.simps(2) simp: stake_Suc)
    1.24 +
    1.25 +lemma sset_siterate: "sset (siterate f x) = {(f^^n) x | n. True}"
    1.26 +  by (auto simp: sset_range)
    1.27 +
    1.28 +lemma smap_siterate: "smap f (siterate f x) = siterate f (f x)"
    1.29 +  by (coinduction arbitrary: x) auto
    1.30 +
    1.31 +
    1.32  subsection {* stream repeating a single element *}
    1.33  
    1.34 -primcorec same where
    1.35 -  "shd (same x) = x"
    1.36 -| "stl (same x) = same x"
    1.37 +abbreviation "sconst \<equiv> siterate id"
    1.38  
    1.39 -lemma snth_same[simp]: "same x !! n = x"
    1.40 -  unfolding same_def by (induct n) auto
    1.41 +lemma shift_replicate_sconst[simp]: "replicate n x @- sconst x = sconst x"
    1.42 +  by (subst (3) stake_sdrop[symmetric]) (simp add: map_replicate_trivial)
    1.43  
    1.44 -lemma stake_same[simp]: "stake n (same x) = replicate n x"
    1.45 -  unfolding same_def by (induct n) (auto simp: upt_rec)
    1.46 +lemma stream_all_same[simp]: "sset (sconst x) = {x}"
    1.47 +  by (simp add: sset_siterate)
    1.48  
    1.49 -lemma sdrop_same[simp]: "sdrop n (same x) = same x"
    1.50 -  unfolding same_def by (induct n) auto
    1.51 +lemma same_cycle: "sconst x = cycle [x]"
    1.52 +  by coinduction auto
    1.53  
    1.54 -lemma shift_replicate_same[simp]: "replicate n x @- same x = same x"
    1.55 -  by (metis sdrop_same stake_same stake_sdrop)
    1.56 +lemma smap_sconst: "smap f (sconst x) = sconst (f x)"
    1.57 +  by coinduction auto
    1.58  
    1.59 -lemma stream_all_same[simp]: "stream_all P (same x) \<longleftrightarrow> P x"
    1.60 -  unfolding stream_all_def by auto
    1.61 -
    1.62 -lemma same_cycle: "same x = cycle [x]"
    1.63 -  by coinduction auto
    1.64 +lemma sconst_streams: "x \<in> A \<Longrightarrow> sconst x \<in> streams A"
    1.65 +  by (simp add: streams_iff_sset)
    1.66  
    1.67  
    1.68  subsection {* stream of natural numbers *}
    1.69  
    1.70 -primcorec fromN :: "nat \<Rightarrow> nat stream" where
    1.71 -  "fromN n = n ## fromN (n + 1)"
    1.72 -
    1.73 -lemma snth_fromN[simp]: "fromN n !! m = n + m"
    1.74 -  unfolding fromN_def by (induct m arbitrary: n) auto
    1.75 -
    1.76 -lemma stake_fromN[simp]: "stake m (fromN n) = [n ..< m + n]"
    1.77 -  unfolding fromN_def by (induct m arbitrary: n) (auto simp: upt_rec)
    1.78 -
    1.79 -lemma sdrop_fromN[simp]: "sdrop m (fromN n) = fromN (n + m)"
    1.80 -  unfolding fromN_def by (induct m arbitrary: n) auto
    1.81 -
    1.82 -lemma sset_fromN[simp]: "sset (fromN n) = {n ..}" (is "?L = ?R")
    1.83 -proof safe
    1.84 -  fix m assume "m \<in> ?L"
    1.85 -  moreover
    1.86 -  { fix s assume "m \<in> sset s" "\<exists>n'\<ge>n. s = fromN n'"
    1.87 -    hence "n \<le> m"  by (induct arbitrary: n rule: sset_induct1) fastforce+
    1.88 -  }
    1.89 -  ultimately show "n \<le> m" by auto
    1.90 -next
    1.91 -  fix m assume "n \<le> m" thus "m \<in> ?L" by (metis le_iff_add snth_fromN snth_sset)
    1.92 -qed
    1.93 -
    1.94 -lemma fromN_Suc_eq_smap: "fromN (Suc n) = smap Suc (fromN n)"
    1.95 -  by (coinduction arbitrary: n) auto
    1.96 +abbreviation "fromN \<equiv> siterate Suc"
    1.97  
    1.98  abbreviation "nats \<equiv> fromN 0"
    1.99  
   1.100 +lemma sset_fromN[simp]: "sset (fromN n) = {n ..}"
   1.101 +  by (auto simp add: sset_siterate) arith
   1.102 +
   1.103  
   1.104  subsection {* flatten a stream of lists *}
   1.105  
   1.106 @@ -535,26 +533,4 @@
   1.107    "smap2 f s1 s2 = smap (split f) (szip s1 s2)"
   1.108    by (coinduction arbitrary: s1 s2) auto
   1.109  
   1.110 -
   1.111 -subsection {* iterated application of a function *}
   1.112 -
   1.113 -primcorec siterate where
   1.114 -  "shd (siterate f x) = x"
   1.115 -| "stl (siterate f x) = siterate f (f x)"
   1.116 -
   1.117 -lemma stake_Suc: "stake (Suc n) s = stake n s @ [s !! n]"
   1.118 -  by (induct n arbitrary: s) auto
   1.119 -
   1.120 -lemma snth_siterate[simp]: "siterate f x !! n = (f^^n) x"
   1.121 -  by (induct n arbitrary: x) (auto simp: funpow_swap1)
   1.122 -
   1.123 -lemma sdrop_siterate[simp]: "sdrop n (siterate f x) = siterate f ((f^^n) x)"
   1.124 -  by (induct n arbitrary: x) (auto simp: funpow_swap1)
   1.125 -
   1.126 -lemma stake_siterate[simp]: "stake n (siterate f x) = map (\<lambda>n. (f^^n) x) [0 ..< n]"
   1.127 -  by (induct n arbitrary: x) (auto simp del: stake.simps(2) simp: stake_Suc)
   1.128 -
   1.129 -lemma sset_siterate: "sset (siterate f x) = {(f^^n) x | n. True}"
   1.130 -  by (auto simp: sset_range)
   1.131 -
   1.132  end