theory Termin10 imports Main begin section \Coinduction\ inductive rtc :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" for r :: "'a \ 'a \ bool" where refl: "rtc r x x" | trans: "r x y \ rtc r y z \ rtc r x z" coinductive cortc :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" for r :: "'a \ 'a \ bool" where refl: "cortc r x x" | trans: "r x y \ cortc r y z \ cortc r x z" thm rtc.induct cortc.coinduct datatype a = A | B | C | D fun r :: "a \ a \ bool" where "r A B = True" | "r B D = True" | "r C C = True" | "r x y = False" lemma "cortc r C A" (* apply (coinduct rule: cortc.coinduct [where X="\x y. x=C \ y=A"]) *) apply (coinduction rule: cortc.coinduct) apply clarsimp apply (rule exI[where x = C]) by clarsimp locale my_nat = fixes \ :: 'a and succ :: "'a \ 'a" begin inductive inat :: "'a \ bool" where "inat \" | "inat x \ inat (succ x)" coinductive cnat :: "'a \ bool" where "cnat \" | "cnat x \ cnat (succ x)" thm inat.induct cnat.coinduct lemma "inat x \ cnat x" by (induction rule: inat.induct) (auto intro: cnat.intros) lemma "inat x \ cnat x" apply (coinduct rule: cnat.coinduct [where X=inat]) apply assumption apply (thin_tac "inat x") apply (erule inat.cases) apply simp apply (rule disjI2) apply (rule_tac x="xa" in exI) apply simp done (* by (coinduction arbitrary: x rule: cnat.coinduct) (auto elim: inat.cases) *) end subsection \Codatatypes\ codatatype 'a llist = lnull: LNil | lnot_null: LCons (lhd: 'a) (ltl: "'a llist") where "ltl LNil = LNil" thm llist.disc thm llist.sel thm list.rel_induct thm list.rel_induct [where R="op =" and Q="\x y. x=y \ P x" for P, unfolded list.rel_eq, simplified] thm list.rel_induct llist.rel_coinduct thm llist.rel_coinduct llist.coinduct thm llist.coinduct_strong primcorec literate :: "('a \ 'a) \ 'a \ 'a llist" where "literate f s = LCons s (literate f (f s))" export_code literate in Haskell lemma map_literate: "map_llist f (literate f s) = literate f (f s)" (* apply (coinduction arbitrary: s) *) apply (coinduct rule: llist.coinduct [where R="\l1 l2. (l1,l2) \ {(l1,l2). \s. l1 = map_llist f (literate f s) \ l2 = literate f (f s)}"]) by (auto simp: llist.map_sel) (* apply (subst llist.map_sel(1)) apply simp apply simp apply (rule_tac x="f s" in exI) apply simp apply (subst llist.map_sel(2)) apply simp apply simp done *) text \Discriminator view\ primcorec literate2 :: "('a \ 'a) \ 'a \ 'a llist" where "\ lnull (literate2 f s)" | "lhd (literate2 f s) = s" | "ltl (literate2 f s) = literate2 f (f s)" print_theorems text \Constructor view\ primcorec until :: "('a \ bool) \ ('a \ 'a) \ 'a \ 'a llist" where "P s \ until P f s = LNil" | "\ P s \ until P f s = LCons s (until P f (f s))" print_theorems export_code until in Haskell inductive finite :: "'a llist \ bool" where "finite LNil" | "finite l \ finite (LCons x l)" coinductive infinite :: "'a llist \ bool" where "infinite l \ infinite (LCons x l)" lemma "\ finite l \ infinite l" proof show "\ finite l \ infinite l" apply (coinduction arbitrary: l rule: infinite.coinduct) apply clarsimp by (case_tac l; auto intro: finite.intros) next have "finite l \ \ infinite l" by (induction rule: finite.induct) (auto elim: infinite.cases) then show "infinite l \ \ finite l" by blast qed subsection \Languages as Infinte Tries\ codatatype 'a lang = Lang (\: bool) (\: "'a \ 'a lang") primrec "in" :: "'a list \ 'a lang \ bool" (infix "\" 65) where "[] \ L = \ L" | "(x # w) \ L = w \ \ L x" definition out :: "'a lang \ 'a list set" where "out L = {w. w \ L}" primcorec empty :: "'a lang" ("\") where "\ = Lang False (\x. \)" primcorec \ :: "'a lang" where "\ = Lang True (\x. \)" primcorec A :: "'a \ 'a lang" where "\ (A a) = False" | "\ (A a) = (\x. if a = x then \ else \)" primcorec union :: "'a lang \ 'a lang \ 'a lang" (infixl "\" 65) where "\ (L \ K) = (\ L \ \ K)" | "\ (L \ K) = (\x. \ L x \ \ K x)" primcorec intersect :: "'a lang \ 'a lang \ 'a lang" (infixl "\\<^sub>L" 65) where "\ (L \\<^sub>L K) = (\ L \ \ K)" | "\ (L \\<^sub>L K) = (\x. \ L x \\<^sub>L \ K x)" primcorec negation :: "'a lang \ 'a lang" ("\\<^sub>L _" [40] 40) where "\ (\\<^sub>L L) = (\ \ L)" | "\ (\\<^sub>L L) = (\x. \\<^sub>L \ L x)" theorem "\ \ L = L" (* by (coinduction arbitrary: L) auto *) proof (rule lang.coinduct [unfolded rel_fun_def, simplified]) def R \ "\(L\<^sub>1::'a lang) L\<^sub>2. \K. L\<^sub>1 = \ \ K \ L\<^sub>2 = K" show "R (\ \ L) L" unfolding R_def by simp fix L\<^sub>1 L\<^sub>2 assume "R L\<^sub>1 L\<^sub>2" then obtain K where "L\<^sub>1 = \ \ K" and "L\<^sub>2 = K" unfolding R_def by simp then show "\ L\<^sub>1 = \ L\<^sub>2 \ (\x. R (\ L\<^sub>1 x) (\ L\<^sub>2 x))" unfolding R_def by simp qed section \Data refinement\ codatatype 'a stream = SCons (shd: 'a) (stl: "'a stream") primcorec siterate :: "('a \ 'a) \ 'a \ 'a stream" where "siterate f a = SCons a (siterate f (f a))" fun nths :: "nat \ 'a stream \ 'a" where "nths 0 s = shd s" | "nths (Suc n) s = nths n (stl s)" primcorec fromIdx :: "(nat \ 'a) \ 'a stream" where "shd (fromIdx f) = f 0" | "stl (fromIdx f) = fromIdx (\ n. f (Suc n))" print_theorems export_code siterate nths fromIdx map_stream in Haskell code_datatype fromIdx declare fromIdx.sel[code] lemma SCons_fromIdx[code]: "SCons x (fromIdx f) = fromIdx (\n. if n = 0 then x else f (n - 1))" by (subst (2) fromIdx.ctr) auto lemma map_stream_fromIdx[code]: "map_stream f (fromIdx g) = fromIdx (f \ g)" apply (coinduction arbitrary: g) apply (auto simp add: stream.map_sel) apply (rule_tac x = "\n . g (Suc n)" in exI) apply (auto simp add: comp_def) done export_code siterate nths fromIdx map_stream in Haskell declare SCons_fromIdx[code del] lemma siterate_fromIdx[code]: "siterate f a = fromIdx (\n . (f^^n) a)" apply (coinduction arbitrary: a) apply auto apply (rule_tac x = "f a" in exI) apply (auto simp add: funpow_swap1) done lemma nths_fromIdx[code]: "nths n (fromIdx f) = f n" by (induction n arbitrary: f) auto export_code siterate nths fromIdx map_stream in Haskell end