src/HOL/Datatype_Examples/Koenig.thy
changeset 58309 a09ec6daaa19
parent 57634 efc00b9b8680
child 58607 1f90ea1b4010
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Datatype_Examples/Koenig.thy	Thu Sep 11 19:26:59 2014 +0200
     1.3 @@ -0,0 +1,122 @@
     1.4 +(*  Title:      HOL/Datatype_Examples/Koenig.thy
     1.5 +    Author:     Dmitriy Traytel, TU Muenchen
     1.6 +    Author:     Andrei Popescu, TU Muenchen
     1.7 +    Copyright   2012
     1.8 +
     1.9 +Koenig's lemma.
    1.10 +*)
    1.11 +
    1.12 +header {* Koenig's Lemma *}
    1.13 +
    1.14 +theory Koenig
    1.15 +imports TreeFI Stream
    1.16 +begin
    1.17 +
    1.18 +(* infinite trees: *)
    1.19 +coinductive infiniteTr where
    1.20 +"\<lbrakk>tr' \<in> set (sub tr); infiniteTr tr'\<rbrakk> \<Longrightarrow> infiniteTr tr"
    1.21 +
    1.22 +lemma infiniteTr_strong_coind[consumes 1, case_names sub]:
    1.23 +assumes *: "phi tr" and
    1.24 +**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> set (sub tr). phi tr' \<or> infiniteTr tr'"
    1.25 +shows "infiniteTr tr"
    1.26 +using assms by (elim infiniteTr.coinduct) blast
    1.27 +
    1.28 +lemma infiniteTr_coind[consumes 1, case_names sub, induct pred: infiniteTr]:
    1.29 +assumes *: "phi tr" and
    1.30 +**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> set (sub tr). phi tr'"
    1.31 +shows "infiniteTr tr"
    1.32 +using assms by (elim infiniteTr.coinduct) blast
    1.33 +
    1.34 +lemma infiniteTr_sub[simp]:
    1.35 +"infiniteTr tr \<Longrightarrow> (\<exists> tr' \<in> set (sub tr). infiniteTr tr')"
    1.36 +by (erule infiniteTr.cases) blast
    1.37 +
    1.38 +primcorec konigPath where
    1.39 +  "shd (konigPath t) = lab t"
    1.40 +| "stl (konigPath t) = konigPath (SOME tr. tr \<in> set (sub t) \<and> infiniteTr tr)"
    1.41 +
    1.42 +(* proper paths in trees: *)
    1.43 +coinductive properPath where
    1.44 +"\<lbrakk>shd as = lab tr; tr' \<in> set (sub tr); properPath (stl as) tr'\<rbrakk> \<Longrightarrow>
    1.45 + properPath as tr"
    1.46 +
    1.47 +lemma properPath_strong_coind[consumes 1, case_names shd_lab sub]:
    1.48 +assumes *: "phi as tr" and
    1.49 +**: "\<And> as tr. phi as tr \<Longrightarrow> shd as = lab tr" and
    1.50 +***: "\<And> as tr.
    1.51 +         phi as tr \<Longrightarrow>
    1.52 +         \<exists> tr' \<in> set (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'"
    1.53 +shows "properPath as tr"
    1.54 +using assms by (elim properPath.coinduct) blast
    1.55 +
    1.56 +lemma properPath_coind[consumes 1, case_names shd_lab sub, induct pred: properPath]:
    1.57 +assumes *: "phi as tr" and
    1.58 +**: "\<And> as tr. phi as tr \<Longrightarrow> shd as = lab tr" and
    1.59 +***: "\<And> as tr.
    1.60 +         phi as tr \<Longrightarrow>
    1.61 +         \<exists> tr' \<in> set (sub tr). phi (stl as) tr'"
    1.62 +shows "properPath as tr"
    1.63 +using properPath_strong_coind[of phi, OF * **] *** by blast
    1.64 +
    1.65 +lemma properPath_shd_lab:
    1.66 +"properPath as tr \<Longrightarrow> shd as = lab tr"
    1.67 +by (erule properPath.cases) blast
    1.68 +
    1.69 +lemma properPath_sub:
    1.70 +"properPath as tr \<Longrightarrow>
    1.71 + \<exists> tr' \<in> set (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'"
    1.72 +by (erule properPath.cases) blast
    1.73 +
    1.74 +(* prove the following by coinduction *)
    1.75 +theorem Konig:
    1.76 +  assumes "infiniteTr tr"
    1.77 +  shows "properPath (konigPath tr) tr"
    1.78 +proof-
    1.79 +  {fix as
    1.80 +   assume "infiniteTr tr \<and> as = konigPath tr" hence "properPath as tr"
    1.81 +   proof (coinduction arbitrary: tr as rule: properPath_coind)
    1.82 +     case (sub tr as)
    1.83 +     let ?t = "SOME t'. t' \<in> set (sub tr) \<and> infiniteTr t'"
    1.84 +     from sub have "\<exists>t' \<in> set (sub tr). infiniteTr t'" by simp
    1.85 +     then have "\<exists>t'. t' \<in> set (sub tr) \<and> infiniteTr t'" by blast
    1.86 +     then have "?t \<in> set (sub tr) \<and> infiniteTr ?t" by (rule someI_ex)
    1.87 +     moreover have "stl (konigPath tr) = konigPath ?t" by simp
    1.88 +     ultimately show ?case using sub by blast
    1.89 +   qed simp
    1.90 +  }
    1.91 +  thus ?thesis using assms by blast
    1.92 +qed
    1.93 +
    1.94 +(* some more stream theorems *)
    1.95 +
    1.96 +primcorec plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where
    1.97 +  "shd (plus xs ys) = shd xs + shd ys"
    1.98 +| "stl (plus xs ys) = plus (stl xs) (stl ys)"
    1.99 +
   1.100 +definition scalar :: "nat \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<cdot>" 68) where
   1.101 +  [simp]: "scalar n = smap (\<lambda>x. n * x)"
   1.102 +
   1.103 +primcorec ones :: "nat stream" where "ones = 1 ## ones"
   1.104 +primcorec twos :: "nat stream" where "twos = 2 ## twos"
   1.105 +definition ns :: "nat \<Rightarrow> nat stream" where [simp]: "ns n = scalar n ones"
   1.106 +
   1.107 +lemma "ones \<oplus> ones = twos"
   1.108 +  by coinduction simp
   1.109 +
   1.110 +lemma "n \<cdot> twos = ns (2 * n)"
   1.111 +  by coinduction simp
   1.112 +
   1.113 +lemma prod_scalar: "(n * m) \<cdot> xs = n \<cdot> m \<cdot> xs"
   1.114 +  by (coinduction arbitrary: xs) auto
   1.115 +
   1.116 +lemma scalar_plus: "n \<cdot> (xs \<oplus> ys) = n \<cdot> xs \<oplus> n \<cdot> ys"
   1.117 +  by (coinduction arbitrary: xs ys) (auto simp: add_mult_distrib2)
   1.118 +
   1.119 +lemma plus_comm: "xs \<oplus> ys = ys \<oplus> xs"
   1.120 +  by (coinduction arbitrary: xs ys) auto
   1.121 +
   1.122 +lemma plus_assoc: "(xs \<oplus> ys) \<oplus> zs = xs \<oplus> ys \<oplus> zs"
   1.123 +  by (coinduction arbitrary: xs ys zs) auto
   1.124 +
   1.125 +end