Theory Koenig

(*  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