Stream4.thy

(*
  SICP 3.5.2

  Isabele 2014
*)
theory Stream4 imports Main begin

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

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

(* integers-starting-from *)
primcorec nf2 :: "nat => nat stream" where
  "nf2 k = SCons k (nf2 (k + 1))"

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

(*
  (define integers (cons-stream 0 (add-streams ones integers)))
*)

(*
primcorec
  nf0 :: "nat stream"
where
  "nf0 = SCons 0 (sadd nf0 ones)"
*)

inductive_set
  nf :: "(nat * nat stream) set"
where
  "s = SCons k (sadd s ones) ==> (k, s) : nf"

lemma "(k, s) : nf & (k, t) : nf ==> s = t"
apply(coinduction arbitrary: k s t)
apply(auto)
apply (metis nf.cases stream.sel(1))
apply(rule_tac x="Suc k" in exI)
by (metis One_nat_def add_Suc comm_semiring_1_class.normalizing_semiring_rules(24) monoid_add_class.add.left_neutral nf.simps ones.simps(1) ones.simps(2) sadd.simps(1) sadd.simps(2) stream.exhaust stream.sel(1) stream.sel(2))

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

primcorec fs :: "(nat => 'a) => 'a stream" where
  "shd (fs f) = f 0" |
  "stl (fs f) = fs (%k. f (Suc k))"

lemma snth_fs: "fs (snth s) = s"
apply(coinduction arbitrary: s)
apply(auto)
done

lemma fs_snth0: "ALL f. snth (fs f) k = f k"
apply(induct_tac k)
apply(auto)
done

lemma fs_snth: "snth (fs f) = f"
apply(rule ext)
apply(rule fs_snth0[rule_format])
done

lemma fsI: "f = g ==> fs f = fs g"
by metis

lemma nf_fs: "(k, s) : nf ==> s = fs (%j. k + j)"
apply(coinduction arbitrary: k s)
apply(auto)
apply (metis nf.simps stream.sel(1))
apply(rule_tac x="Suc k" in exI)
apply(auto)
apply(rule fsI)
apply(rule ext)
apply(simp)
apply(erule nf.induct)
apply(auto)
by (metis One_nat_def add_Suc comm_semiring_1_class.normalizing_semiring_rules(24) monoid_add_class.add.left_neutral nf.simps ones.simps(1) ones.simps(2) sadd.simps(1) sadd.simps(2) stream.exhaust stream.sel(1) stream.sel(2))

lemma nf_snth: "(k, s) : nf ==> snth s j = k + j"
by (metis fs_snth nf_fs)

lemma "(k, s) : nf ==> s = nf2 k"
apply(coinduction arbitrary: k s)
apply(auto)
apply (metis fs.simps(1) monoid_add_class.add.right_neutral nf_fs)
apply(rule_tac x="Suc k" in exI)
apply(auto)
apply(erule nf.induct)
apply(auto)
by (metis One_nat_def add_Suc comm_semiring_1_class.normalizing_semiring_rules(24) monoid_add_class.add.left_neutral nf.simps ones.simps(1) ones.simps(2) sadd.simps(1) sadd.simps(2) stream.exhaust stream.sel(1) stream.sel(2))

lemma nf2_sadd: "nf2 k = SCons k (sadd (nf2 k) ones)"
apply(coinduction arbitrary: k)
apply(auto)
apply(rule_tac x="Suc k" in exI)
apply(auto)
by (metis Suc_eq_plus1 nf2.simps(1) nf2.simps(2) ones.simps(1) ones.simps(2) sadd.simps(1) sadd.simps(2) stream.exhaust stream.sel(1) stream.sel(2))

lemma "s = nf2 k ==> (k, s) : nf"
by (metis nf.intros nf2_sadd)

end