# Theory Koenig

theory Koenig
imports TreeFI Stream
```(*  Title:      HOL/Datatype_Examples/Koenig.thy
Author:     Dmitriy Traytel, TU Muenchen
Author:     Andrei Popescu, TU Muenchen

Koenig's lemma.
*)

section ‹Koenig's Lemma›

theory Koenig
imports TreeFI "HOL-Library.Stream"
begin

(* infinite trees: *)
coinductive infiniteTr where
"⟦tr' ∈ set (sub tr); infiniteTr tr'⟧ ⟹ infiniteTr tr"

lemma infiniteTr_strong_coind[consumes 1, case_names sub]:
assumes *: "phi tr" and
**: "⋀ tr. phi tr ⟹ ∃ tr' ∈ set (sub tr). phi tr' ∨ infiniteTr tr'"
shows "infiniteTr tr"
using assms by (elim infiniteTr.coinduct) blast

lemma infiniteTr_coind[consumes 1, case_names sub, induct pred: infiniteTr]:
assumes *: "phi tr" and
**: "⋀ tr. phi tr ⟹ ∃ tr' ∈ set (sub tr). phi tr'"
shows "infiniteTr tr"
using assms by (elim infiniteTr.coinduct) blast

lemma infiniteTr_sub[simp]:
"infiniteTr tr ⟹ (∃ tr' ∈ set (sub tr). infiniteTr tr')"
by (erule infiniteTr.cases) blast

primcorec konigPath where
"shd (konigPath t) = lab t"
| "stl (konigPath t) = konigPath (SOME tr. tr ∈ set (sub t) ∧ infiniteTr tr)"

(* proper paths in trees: *)
coinductive properPath where
"⟦shd as = lab tr; tr' ∈ set (sub tr); properPath (stl as) tr'⟧ ⟹
properPath as tr"

lemma properPath_strong_coind[consumes 1, case_names shd_lab sub]:
assumes *: "phi as tr" and
**: "⋀ as tr. phi as tr ⟹ shd as = lab tr" and
***: "⋀ as tr.
phi as tr ⟹
∃ tr' ∈ set (sub tr). phi (stl as) tr' ∨ properPath (stl as) tr'"
shows "properPath as tr"
using assms by (elim properPath.coinduct) blast

lemma properPath_coind[consumes 1, case_names shd_lab sub, induct pred: properPath]:
assumes *: "phi as tr" and
**: "⋀ as tr. phi as tr ⟹ shd as = lab tr" and
***: "⋀ as tr.
phi as tr ⟹
∃ tr' ∈ set (sub tr). phi (stl as) tr'"
shows "properPath as tr"
using properPath_strong_coind[of phi, OF * **] *** by blast

lemma properPath_shd_lab:
"properPath as tr ⟹ shd as = lab tr"
by (erule properPath.cases) blast

lemma properPath_sub:
"properPath as tr ⟹
∃ tr' ∈ set (sub tr). phi (stl as) tr' ∨ properPath (stl as) tr'"
by (erule properPath.cases) blast

(* prove the following by coinduction *)
theorem Konig:
assumes "infiniteTr tr"
shows "properPath (konigPath tr) tr"
proof-
{fix as
assume "infiniteTr tr ∧ as = konigPath tr" hence "properPath as tr"
proof (coinduction arbitrary: tr as rule: properPath_coind)
case (sub tr as)
let ?t = "SOME t'. t' ∈ set (sub tr) ∧ infiniteTr t'"
from sub have "∃t' ∈ set (sub tr). infiniteTr t'" by simp
then have "∃t'. t' ∈ set (sub tr) ∧ infiniteTr t'" by blast
then have "?t ∈ set (sub tr) ∧ infiniteTr ?t" by (rule someI_ex)
moreover have "stl (konigPath tr) = konigPath ?t" by simp
ultimately show ?case using sub by blast
qed simp
}
thus ?thesis using assms by blast
qed

(* some more stream theorems *)

primcorec plus :: "nat stream ⇒ nat stream ⇒ nat stream" (infixr "⊕" 66) where
"shd (plus xs ys) = shd xs + shd ys"
| "stl (plus xs ys) = plus (stl xs) (stl ys)"

definition scalar :: "nat ⇒ nat stream ⇒ nat stream" (infixr "⋅" 68) where
[simp]: "scalar n = smap (λx. n * x)"

primcorec ones :: "nat stream" where "ones = 1 ## ones"
primcorec twos :: "nat stream" where "twos = 2 ## twos"
definition ns :: "nat ⇒ nat stream" where [simp]: "ns n = scalar n ones"

lemma "ones ⊕ ones = twos"
by coinduction simp

lemma "n ⋅ twos = ns (2 * n)"
by coinduction simp

lemma prod_scalar: "(n * m) ⋅ xs = n ⋅ m ⋅ xs"
by (coinduction arbitrary: xs) auto

lemma scalar_plus: "n ⋅ (xs ⊕ ys) = n ⋅ xs ⊕ n ⋅ ys"
by (coinduction arbitrary: xs ys) (auto simp: add_mult_distrib2)

lemma plus_comm: "xs ⊕ ys = ys ⊕ xs"
by (coinduction arbitrary: xs ys) auto

lemma plus_assoc: "(xs ⊕ ys) ⊕ zs = xs ⊕ ys ⊕ zs"
by (coinduction arbitrary: xs ys zs) auto

end
```