src/HOL/BNF/Examples/Stream.thy
changeset 51352 fdecc2cd5649
parent 51141 cc7423ce6774
child 51353 ae707530c359
     1.1 --- a/src/HOL/BNF/Examples/Stream.thy	Tue Mar 05 15:43:22 2013 +0100
     1.2 +++ b/src/HOL/BNF/Examples/Stream.thy	Tue Mar 05 17:10:49 2013 +0100
     1.3 @@ -63,6 +63,9 @@
     1.4  lemma stream_set_shift[simp]: "stream_set (xs @- s) = set xs \<union> stream_set s"
     1.5    by (induct xs) auto
     1.6  
     1.7 +lemma shift_left_inj[simp]: "xs @- s1 = xs @- s2 \<longleftrightarrow> s1 = s2"
     1.8 +  by (induct xs) auto
     1.9 +
    1.10  
    1.11  subsection {* set of streams with elements in some fixes set *}
    1.12  
    1.13 @@ -89,26 +92,6 @@
    1.14  qed
    1.15  
    1.16  
    1.17 -subsection {* flatten a stream of lists *}
    1.18 -
    1.19 -definition flat where
    1.20 -  "flat \<equiv> stream_unfold (hd o shd) (\<lambda>s. if tl (shd s) = [] then stl s else tl (shd s) ## stl s)"
    1.21 -
    1.22 -lemma flat_simps[simp]:
    1.23 -  "shd (flat ws) = hd (shd ws)"
    1.24 -  "stl (flat ws) = flat (if tl (shd ws) = [] then stl ws else tl (shd ws) ## stl ws)"
    1.25 -  unfolding flat_def by auto
    1.26 -
    1.27 -lemma flat_Cons[simp]: "flat ((x # xs) ## ws) = x ## flat (if xs = [] then ws else xs ## ws)"
    1.28 -  unfolding flat_def using stream.unfold[of "hd o shd" _ "(x # xs) ## ws"] by auto
    1.29 -
    1.30 -lemma flat_Stream[simp]: "xs \<noteq> [] \<Longrightarrow> flat (xs ## ws) = xs @- flat ws"
    1.31 -  by (induct xs) auto
    1.32 -
    1.33 -lemma flat_unfold: "shd ws \<noteq> [] \<Longrightarrow> flat ws = shd ws @- flat (stl ws)"
    1.34 -  by (cases ws) auto
    1.35 -
    1.36 -
    1.37  subsection {* nth, take, drop for streams *}
    1.38  
    1.39  primrec snth :: "'a stream \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
    1.40 @@ -159,6 +142,9 @@
    1.41  lemma sdrop_stream_map[simp]: "sdrop n (stream_map f s) = stream_map f (sdrop n s)"
    1.42    by (induct n arbitrary: s) auto
    1.43  
    1.44 +lemma sdrop_stl: "sdrop n (stl s) = stl (sdrop n s)"
    1.45 +  by (induct n) auto
    1.46 +
    1.47  lemma stake_sdrop: "stake n s @- sdrop n s = s"
    1.48    by (induct n arbitrary: s) auto
    1.49  
    1.50 @@ -201,6 +187,62 @@
    1.51    unfolding stream_all_iff list_all_iff by auto
    1.52  
    1.53  
    1.54 +subsection {* flatten a stream of lists *}
    1.55 +
    1.56 +definition flat where
    1.57 +  "flat \<equiv> stream_unfold (hd o shd) (\<lambda>s. if tl (shd s) = [] then stl s else tl (shd s) ## stl s)"
    1.58 +
    1.59 +lemma flat_simps[simp]:
    1.60 +  "shd (flat ws) = hd (shd ws)"
    1.61 +  "stl (flat ws) = flat (if tl (shd ws) = [] then stl ws else tl (shd ws) ## stl ws)"
    1.62 +  unfolding flat_def by auto
    1.63 +
    1.64 +lemma flat_Cons[simp]: "flat ((x # xs) ## ws) = x ## flat (if xs = [] then ws else xs ## ws)"
    1.65 +  unfolding flat_def using stream.unfold[of "hd o shd" _ "(x # xs) ## ws"] by auto
    1.66 +
    1.67 +lemma flat_Stream[simp]: "xs \<noteq> [] \<Longrightarrow> flat (xs ## ws) = xs @- flat ws"
    1.68 +  by (induct xs) auto
    1.69 +
    1.70 +lemma flat_unfold: "shd ws \<noteq> [] \<Longrightarrow> flat ws = shd ws @- flat (stl ws)"
    1.71 +  by (cases ws) auto
    1.72 +
    1.73 +lemma flat_snth: "\<forall>xs \<in> stream_set s. xs \<noteq> [] \<Longrightarrow> flat s !! n = (if n < length (shd s) then 
    1.74 +  shd s ! n else flat (stl s) !! (n - length (shd s)))"
    1.75 +  by (metis flat_unfold not_less shd_stream_set shift_snth_ge shift_snth_less)
    1.76 +
    1.77 +lemma stream_set_flat[simp]: "\<forall>xs \<in> stream_set s. xs \<noteq> [] \<Longrightarrow> 
    1.78 +  stream_set (flat s) = (\<Union>xs \<in> stream_set s. set xs)" (is "?P \<Longrightarrow> ?L = ?R")
    1.79 +proof safe
    1.80 +  fix x assume ?P "x : ?L"
    1.81 +  then obtain m where "x = flat s !! m" by (metis image_iff stream_set_range)
    1.82 +  with `?P` obtain n m' where "x = s !! n ! m'" "m' < length (s !! n)"
    1.83 +  proof (atomize_elim, induct m arbitrary: s rule: less_induct)
    1.84 +    case (less y)
    1.85 +    thus ?case
    1.86 +    proof (cases "y < length (shd s)")
    1.87 +      case True thus ?thesis by (metis flat_snth less(2,3) snth.simps(1))
    1.88 +    next
    1.89 +      case False
    1.90 +      hence "x = flat (stl s) !! (y - length (shd s))" by (metis less(2,3) flat_snth)
    1.91 +      moreover
    1.92 +      { from less(2) have "length (shd s) > 0" by (cases s) simp_all
    1.93 +        moreover with False have "y > 0" by (cases y) simp_all
    1.94 +        ultimately have "y - length (shd s) < y" by simp
    1.95 +      }
    1.96 +      moreover have "\<forall>xs \<in> stream_set (stl s). xs \<noteq> []" using less(2) by (cases s) auto
    1.97 +      ultimately have "\<exists>n m'. x = stl s !! n ! m' \<and> m' < length (stl s !! n)" by (intro less(1)) auto
    1.98 +      thus ?thesis by (metis snth.simps(2))
    1.99 +    qed
   1.100 +  qed
   1.101 +  thus "x \<in> ?R" by (auto simp: stream_set_range dest!: nth_mem)
   1.102 +next
   1.103 +  fix x xs assume "xs \<in> stream_set s" ?P "x \<in> set xs" thus "x \<in> ?L"
   1.104 +    by (induct rule: stream_set_induct1)
   1.105 +      (metis UnI1 flat_unfold shift.simps(1) stream_set_shift,
   1.106 +       metis UnI2 flat_unfold shd_stream_set stl_stream_set stream_set_shift)
   1.107 +qed
   1.108 +
   1.109 +
   1.110  subsection {* recurring stream out of a list *}
   1.111  
   1.112  definition cycle :: "'a list \<Rightarrow> 'a stream" where
   1.113 @@ -307,6 +349,18 @@
   1.114  lemma sdrop_fromN[simp]: "sdrop m (fromN n) = fromN (n + m)"
   1.115    unfolding fromN_def by (induct m arbitrary: n) auto
   1.116  
   1.117 +lemma stream_set_fromN[simp]: "stream_set (fromN n) = {n ..}" (is "?L = ?R")
   1.118 +proof safe
   1.119 +  fix m assume "m : ?L"
   1.120 +  moreover
   1.121 +  { fix s assume "m \<in> stream_set s" "\<exists>n'\<ge>n. s = fromN n'"
   1.122 +    hence "n \<le> m" by (induct arbitrary: n rule: stream_set_induct1) fastforce+
   1.123 +  }
   1.124 +  ultimately show "n \<le> m" by blast
   1.125 +next
   1.126 +  fix m assume "n \<le> m" thus "m \<in> ?L" by (metis le_iff_add snth_fromN snth_stream_set)
   1.127 +qed
   1.128 +
   1.129  abbreviation "nats \<equiv> fromN 0"
   1.130  
   1.131