src/HOL/Datatype_Examples/Koenig.thy
author hoelzl
Tue Oct 07 10:48:29 2014 +0200 (2014-10-07)
changeset 58607 1f90ea1b4010
parent 58309 a09ec6daaa19
child 58889 5b7a9633cfa8
permissions -rw-r--r--
move Stream theory from Datatype_Examples to Library
     1 (*  Title:      HOL/Datatype_Examples/Koenig.thy
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Author:     Andrei Popescu, TU Muenchen
     4     Copyright   2012
     5 
     6 Koenig's lemma.
     7 *)
     8 
     9 header {* Koenig's Lemma *}
    10 
    11 theory Koenig
    12 imports TreeFI "~~/src/HOL/Library/Stream"
    13 begin
    14 
    15 (* infinite trees: *)
    16 coinductive infiniteTr where
    17 "\<lbrakk>tr' \<in> set (sub tr); infiniteTr tr'\<rbrakk> \<Longrightarrow> infiniteTr tr"
    18 
    19 lemma infiniteTr_strong_coind[consumes 1, case_names sub]:
    20 assumes *: "phi tr" and
    21 **: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> set (sub tr). phi tr' \<or> infiniteTr tr'"
    22 shows "infiniteTr tr"
    23 using assms by (elim infiniteTr.coinduct) blast
    24 
    25 lemma infiniteTr_coind[consumes 1, case_names sub, induct pred: infiniteTr]:
    26 assumes *: "phi tr" and
    27 **: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> set (sub tr). phi tr'"
    28 shows "infiniteTr tr"
    29 using assms by (elim infiniteTr.coinduct) blast
    30 
    31 lemma infiniteTr_sub[simp]:
    32 "infiniteTr tr \<Longrightarrow> (\<exists> tr' \<in> set (sub tr). infiniteTr tr')"
    33 by (erule infiniteTr.cases) blast
    34 
    35 primcorec konigPath where
    36   "shd (konigPath t) = lab t"
    37 | "stl (konigPath t) = konigPath (SOME tr. tr \<in> set (sub t) \<and> infiniteTr tr)"
    38 
    39 (* proper paths in trees: *)
    40 coinductive properPath where
    41 "\<lbrakk>shd as = lab tr; tr' \<in> set (sub tr); properPath (stl as) tr'\<rbrakk> \<Longrightarrow>
    42  properPath as tr"
    43 
    44 lemma properPath_strong_coind[consumes 1, case_names shd_lab sub]:
    45 assumes *: "phi as tr" and
    46 **: "\<And> as tr. phi as tr \<Longrightarrow> shd as = lab tr" and
    47 ***: "\<And> as tr.
    48          phi as tr \<Longrightarrow>
    49          \<exists> tr' \<in> set (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'"
    50 shows "properPath as tr"
    51 using assms by (elim properPath.coinduct) blast
    52 
    53 lemma properPath_coind[consumes 1, case_names shd_lab sub, induct pred: properPath]:
    54 assumes *: "phi as tr" and
    55 **: "\<And> as tr. phi as tr \<Longrightarrow> shd as = lab tr" and
    56 ***: "\<And> as tr.
    57          phi as tr \<Longrightarrow>
    58          \<exists> tr' \<in> set (sub tr). phi (stl as) tr'"
    59 shows "properPath as tr"
    60 using properPath_strong_coind[of phi, OF * **] *** by blast
    61 
    62 lemma properPath_shd_lab:
    63 "properPath as tr \<Longrightarrow> shd as = lab tr"
    64 by (erule properPath.cases) blast
    65 
    66 lemma properPath_sub:
    67 "properPath as tr \<Longrightarrow>
    68  \<exists> tr' \<in> set (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'"
    69 by (erule properPath.cases) blast
    70 
    71 (* prove the following by coinduction *)
    72 theorem Konig:
    73   assumes "infiniteTr tr"
    74   shows "properPath (konigPath tr) tr"
    75 proof-
    76   {fix as
    77    assume "infiniteTr tr \<and> as = konigPath tr" hence "properPath as tr"
    78    proof (coinduction arbitrary: tr as rule: properPath_coind)
    79      case (sub tr as)
    80      let ?t = "SOME t'. t' \<in> set (sub tr) \<and> infiniteTr t'"
    81      from sub have "\<exists>t' \<in> set (sub tr). infiniteTr t'" by simp
    82      then have "\<exists>t'. t' \<in> set (sub tr) \<and> infiniteTr t'" by blast
    83      then have "?t \<in> set (sub tr) \<and> infiniteTr ?t" by (rule someI_ex)
    84      moreover have "stl (konigPath tr) = konigPath ?t" by simp
    85      ultimately show ?case using sub by blast
    86    qed simp
    87   }
    88   thus ?thesis using assms by blast
    89 qed
    90 
    91 (* some more stream theorems *)
    92 
    93 primcorec plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where
    94   "shd (plus xs ys) = shd xs + shd ys"
    95 | "stl (plus xs ys) = plus (stl xs) (stl ys)"
    96 
    97 definition scalar :: "nat \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<cdot>" 68) where
    98   [simp]: "scalar n = smap (\<lambda>x. n * x)"
    99 
   100 primcorec ones :: "nat stream" where "ones = 1 ## ones"
   101 primcorec twos :: "nat stream" where "twos = 2 ## twos"
   102 definition ns :: "nat \<Rightarrow> nat stream" where [simp]: "ns n = scalar n ones"
   103 
   104 lemma "ones \<oplus> ones = twos"
   105   by coinduction simp
   106 
   107 lemma "n \<cdot> twos = ns (2 * n)"
   108   by coinduction simp
   109 
   110 lemma prod_scalar: "(n * m) \<cdot> xs = n \<cdot> m \<cdot> xs"
   111   by (coinduction arbitrary: xs) auto
   112 
   113 lemma scalar_plus: "n \<cdot> (xs \<oplus> ys) = n \<cdot> xs \<oplus> n \<cdot> ys"
   114   by (coinduction arbitrary: xs ys) (auto simp: add_mult_distrib2)
   115 
   116 lemma plus_comm: "xs \<oplus> ys = ys \<oplus> xs"
   117   by (coinduction arbitrary: xs ys) auto
   118 
   119 lemma plus_assoc: "(xs \<oplus> ys) \<oplus> zs = xs \<oplus> ys \<oplus> zs"
   120   by (coinduction arbitrary: xs ys zs) auto
   121 
   122 end