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 ("\") where "\ = eSuc \" print_theorems primcorec eplus :: "enat \ enat \ enat" (infixl "\" 65) where "m \ n = (if is_zero m then n else eSuc (epred m \ n))" lemma eplus_inf: "\ \ x = \" 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 \ 'a stream \ 'a list" where "stake n (x ## xs) = (if n = 0 then [] else x # stake (n-1) xs)" primcorec even :: "'a stream \ 'a stream" where "even xs = shd xs ## even (stl (stl xs))" primcorec zip :: "'a stream \ 'a stream \ '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 \ nat stream \ nat stream" (infixl "\" 66) where "s \ t = (shd s + shd t) ## stl s \ stl t" corec fibA:: "nat stream" where "fibA = 0 ## ((1 ## fibA) \ fibA)" corec fibB:: "nat stream" where "fibB = (0 ## (1 ## fibB)) \ (0 ## fibB)" value [GHC] "stake 10 fibA" value [GHC] "stake 10 fibB" lemma fibA_sel[simp]: "shd fibA = 0" "stl fibA = (1 ## fibA) \ fibA" by (subst fibA.code; simp)+ lemma fibB_sel[simp]: "shd fibB = 0" "stl fibB = (1 ## fibB) \ 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)