theory Coinduction
  imports 
    "~~/src/HOL/Library/BNF_Corec"
    "~~/src/HOL/Library/Code_Test"
begin

codatatype 'a llist = lnull: LNil | LCons (lhd: 'a) (ltl: "'a llist")
print_theorems

primcorec test :: "nat llist" where "test = LCons 0 (LCons 1 LNil)"
primcorec zeros :: "nat llist" where "zeros = LCons 0 zeros"

value "lhd test"
value "ltl test"


codatatype enat = is_zero: Zero | eSuc (epred: enat)
print_theorems


primcorec infty :: enat ("\<infinity>") where "\<infinity> = eSuc \<infinity>"
print_theorems

primcorec eplus :: "enat \<Rightarrow> enat \<Rightarrow> enat" (infixl "\<oplus>" 65)
  where "m \<oplus> n = (if is_zero m then n else eSuc (epred m \<oplus> n))"

lemma eplus_inf: "\<infinity> \<oplus> x = \<infinity>"
  apply (coinduction arbitrary: x)
  apply (rule conjI)
  subgoal by simp
  apply simp
  apply auto
  done


codatatype 'a stream = SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
print_theorems

corec one_twos :: "nat stream" where "one_twos = SCons 1 (SCons 2 one_twos)"

fun stake :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a list" 
  where "stake n (x ## xs) = (if n = 0 then [] else x # stake (n-1) xs)"

primcorec even :: "'a stream \<Rightarrow> 'a stream" 
  where "even xs = shd xs ## even (stl (stl xs))"

primcorec  zip :: "'a stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream"
  where "zip xs ys = shd xs ## zip ys (stl xs)"


value [GHC] "stake 3 (even one_twos)"
value [GHC] "stake 9 (zip one_twos one_twos)"

lemma zip_shd[simp]: "shd (zip x y) = shd x" by auto

lemma zip_stl[simp]: "stl (zip x y) = zip y (stl x)" by auto

lemma "even (zip xs ys) = xs" (*by (coinduction arbitrary: xs ys) auto*)
  apply (coinduction arbitrary: xs ys rule: stream.coinduct)
  apply (rule conjI)
  apply auto
  done

corec (friend) pls :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixl "\<Oplus>" 66) where
  "s \<Oplus> t = (shd s + shd t) ## stl s \<Oplus> stl t"

corec fibA:: "nat stream" where "fibA = 0 ## ((1 ## fibA) \<Oplus> fibA)"

corec fibB:: "nat stream" where "fibB = (0 ## (1 ## fibB)) \<Oplus> (0 ## fibB)"

value [GHC] "stake 10 fibA"
value [GHC] "stake 10 fibB"


lemma fibA_sel[simp]:
  "shd fibA = 0"
  "stl fibA = (1 ## fibA) \<Oplus> fibA"
  by (subst fibA.code; simp)+

lemma fibB_sel[simp]:
  "shd fibB = 0"
  "stl fibB = (1 ## fibB) \<Oplus> fibB"
  by (subst fibB.code; subst pls.code;  simp)+

lemma "fibA = fibB" (*by (coinduction rule: stream.coinduct_upto) 
(auto intro: stream.cong_intros)*)
  apply (coinduction rule: stream.coinduct_upto)
  apply (rule conjI)
  subgoal by simp
  apply (auto intro: stream.cong_intros)