Stream.thy

(* Isabelle 2014 *)

theory Stream imports Main begin

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

coinductive_set
  sle :: "(('a::order) stream * 'a stream) set"
where
  sle: "shd s <= shd t &
        (shd s = shd t --> (stl s, stl t) : sle)
    ==> (s, t) : sle"

lemma "(s, t) : sle ==> (t, u) : sle ==> (s, u) : sle"
apply(rule_tac X="%s u. EX t. (s, t) : sle & (t, u) : sle" in sle.coinduct)
apply(auto)
apply (metis order_trans sle.cases)
by (metis antisym sle.simps)

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

lemma "(s1, s2) : sle ==> (t1, t2) : sle ==> (sadd s1 t1, sadd s2 t2) : sle"
apply(rule_tac X="%u1 u2. EX s1 s2 t1 t2. u1 = sadd s1 t1 & u2 = sadd s2 t2 & (s1, s2) : sle & (t1, t2) : sle" in sle.coinduct)
apply(auto)
apply (metis add_mono_thms_linordered_semiring(1) sle.cases)
by (metis add_le_cancel_left add_le_cancel_right antisym sle.cases)

end