(* Title: HOL/Datatype_Examples/Koenig.thy Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen Copyright 2012 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