Stream3.thy

theory Stream3 imports Main begin

codatatype 'a stream = SCons (shd:'a) (stl:"'a stream")

primcorec
  sadd :: "nat stream => nat stream => nat stream"
where
  "sadd s t = SCons (shd s + shd t) (sadd (stl s) (stl t))"

primcorec zeros :: "nat stream" where
  "zeros = SCons 0 zeros"

primcorec ones :: "nat stream" where
  "ones = SCons 1 ones"

lemma "sadd zeros ones = ones"
apply(coinduction)
apply(auto)
done

primcorec nf :: "nat => nat stream" where
  "nf k = SCons k (nf (k + 1))"

fun snth :: "nat => nat stream => nat" where
  "snth 0 s = shd s" |
  "snth (Suc k) s = snth k (stl s)"

lemma "snth k (nf j) = k + j"
apply(induction k arbitrary: j)
apply(auto)
done

lemma "sadd (nf k) ones = nf (Suc k)"
apply(coinduction arbitrary: k)
apply(auto)
done

end