src/HOL/BNF/Examples/Koenig.thy
author traytel
Thu Dec 13 15:36:08 2012 +0100 (2012-12-13)
changeset 50517 8f6c11103820
child 50518 d4fdda801e19
permissions -rw-r--r--
renamed theory
     1 (*  Title:      HOL/BNF/Examples/Stream.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
    13 begin
    14 
    15 codata 'a stream = Stream (shd: 'a) (stl: "'a stream")
    16 
    17 (* selectors for streams *)
    18 lemma shd_def': "shd as = fst (stream_dtor as)"
    19 unfolding shd_def stream_case_def fst_def by (rule refl)
    20 
    21 lemma stl_def': "stl as = snd (stream_dtor as)"
    22 unfolding stl_def stream_case_def snd_def by (rule refl)
    23 
    24 lemma unfold_pair_fun_shd[simp]: "shd (stream_dtor_unfold (f \<odot> g) t) = f t"
    25 unfolding shd_def' pair_fun_def stream.dtor_unfold by simp
    26 
    27 lemma unfold_pair_fun_stl[simp]: "stl (stream_dtor_unfold (f \<odot> g) t) =
    28  stream_dtor_unfold (f \<odot> g) (g t)"
    29 unfolding stl_def' pair_fun_def stream.dtor_unfold by simp
    30 
    31 (* infinite trees: *)
    32 coinductive infiniteTr where
    33 "\<lbrakk>tr' \<in> listF_set (sub tr); infiniteTr tr'\<rbrakk> \<Longrightarrow> infiniteTr tr"
    34 
    35 lemma infiniteTr_strong_coind[consumes 1, case_names sub]:
    36 assumes *: "phi tr" and
    37 **: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr' \<or> infiniteTr tr'"
    38 shows "infiniteTr tr"
    39 using assms by (elim infiniteTr.coinduct) blast
    40 
    41 lemma infiniteTr_coind[consumes 1, case_names sub, induct pred: infiniteTr]:
    42 assumes *: "phi tr" and
    43 **: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr'"
    44 shows "infiniteTr tr"
    45 using assms by (elim infiniteTr.coinduct) blast
    46 
    47 lemma infiniteTr_sub[simp]:
    48 "infiniteTr tr \<Longrightarrow> (\<exists> tr' \<in> listF_set (sub tr). infiniteTr tr')"
    49 by (erule infiniteTr.cases) blast
    50 
    51 definition "konigPath \<equiv> stream_dtor_unfold
    52   (lab \<odot> (\<lambda>tr. SOME tr'. tr' \<in> listF_set (sub tr) \<and> infiniteTr tr'))"
    53 
    54 lemma konigPath_simps[simp]:
    55 "shd (konigPath t) = lab t"
    56 "stl (konigPath t) = konigPath (SOME tr. tr \<in> listF_set (sub t) \<and> infiniteTr tr)"
    57 unfolding konigPath_def by simp+
    58 
    59 (* proper paths in trees: *)
    60 coinductive properPath where
    61 "\<lbrakk>shd as = lab tr; tr' \<in> listF_set (sub tr); properPath (stl as) tr'\<rbrakk> \<Longrightarrow>
    62  properPath as tr"
    63 
    64 lemma properPath_strong_coind[consumes 1, case_names shd_lab sub]:
    65 assumes *: "phi as tr" and
    66 **: "\<And> as tr. phi as tr \<Longrightarrow> shd as = lab tr" and
    67 ***: "\<And> as tr.
    68          phi as tr \<Longrightarrow>
    69          \<exists> tr' \<in> listF_set (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'"
    70 shows "properPath as tr"
    71 using assms by (elim properPath.coinduct) blast
    72 
    73 lemma properPath_coind[consumes 1, case_names shd_lab sub, induct pred: properPath]:
    74 assumes *: "phi as tr" and
    75 **: "\<And> as tr. phi as tr \<Longrightarrow> shd as = lab tr" and
    76 ***: "\<And> as tr.
    77          phi as tr \<Longrightarrow>
    78          \<exists> tr' \<in> listF_set (sub tr). phi (stl as) tr'"
    79 shows "properPath as tr"
    80 using properPath_strong_coind[of phi, OF * **] *** by blast
    81 
    82 lemma properPath_shd_lab:
    83 "properPath as tr \<Longrightarrow> shd as = lab tr"
    84 by (erule properPath.cases) blast
    85 
    86 lemma properPath_sub:
    87 "properPath as tr \<Longrightarrow>
    88  \<exists> tr' \<in> listF_set (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'"
    89 by (erule properPath.cases) blast
    90 
    91 (* prove the following by coinduction *)
    92 theorem Konig:
    93   assumes "infiniteTr tr"
    94   shows "properPath (konigPath tr) tr"
    95 proof-
    96   {fix as
    97    assume "infiniteTr tr \<and> as = konigPath tr" hence "properPath as tr"
    98    proof (induct rule: properPath_coind, safe)
    99      fix t
   100      let ?t = "SOME t'. t' \<in> listF_set (sub t) \<and> infiniteTr t'"
   101      assume "infiniteTr t"
   102      hence "\<exists>t' \<in> listF_set (sub t). infiniteTr t'" by simp
   103      hence "\<exists>t'. t' \<in> listF_set (sub t) \<and> infiniteTr t'" by blast
   104      hence "?t \<in> listF_set (sub t) \<and> infiniteTr ?t" by (elim someI_ex)
   105      moreover have "stl (konigPath t) = konigPath ?t" by simp
   106      ultimately show "\<exists>t' \<in> listF_set (sub t).
   107              infiniteTr t' \<and> stl (konigPath t) = konigPath t'" by blast
   108    qed simp
   109   }
   110   thus ?thesis using assms by blast
   111 qed
   112 
   113 (* some more stream theorems *)
   114 
   115 lemma stream_map[simp]: "stream_map f = stream_dtor_unfold (f o shd \<odot> stl)"
   116 unfolding stream_map_def pair_fun_def shd_def'[abs_def] stl_def'[abs_def]
   117   map_pair_def o_def prod_case_beta by simp
   118 
   119 definition plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where
   120   [simp]: "plus xs ys =
   121     stream_dtor_unfold ((%(xs, ys). shd xs + shd ys) \<odot> (%(xs, ys). (stl xs, stl ys))) (xs, ys)"
   122 
   123 definition scalar :: "nat \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<cdot>" 68) where
   124   [simp]: "scalar n = stream_map (\<lambda>x. n * x)"
   125 
   126 definition ones :: "nat stream" where [simp]: "ones = stream_dtor_unfold ((%x. 1) \<odot> id) ()"
   127 definition twos :: "nat stream" where [simp]: "twos = stream_dtor_unfold ((%x. 2) \<odot> id) ()"
   128 definition ns :: "nat \<Rightarrow> nat stream" where [simp]: "ns n = scalar n ones"
   129 
   130 lemma "ones \<oplus> ones = twos"
   131 by (rule stream.coinduct[of "%x1 x2. \<exists>x. x1 = ones \<oplus> ones \<and> x2 = twos"]) auto
   132 
   133 lemma "n \<cdot> twos = ns (2 * n)"
   134 by (rule stream.coinduct[of "%x1 x2. \<exists>n. x1 = n \<cdot> twos \<and> x2 = ns (2 * n)"]) force+
   135 
   136 lemma prod_scalar: "(n * m) \<cdot> xs = n \<cdot> m \<cdot> xs"
   137 by (rule stream.coinduct[of "%x1 x2. \<exists>n m xs. x1 = (n * m) \<cdot> xs \<and> x2 = n \<cdot> m \<cdot> xs"]) force+
   138 
   139 lemma scalar_plus: "n \<cdot> (xs \<oplus> ys) = n \<cdot> xs \<oplus> n \<cdot> ys"
   140 by (rule stream.coinduct[of "%x1 x2. \<exists>n xs ys. x1 = n \<cdot> (xs \<oplus> ys) \<and> x2 = n \<cdot> xs \<oplus> n \<cdot> ys"])
   141    (force simp: add_mult_distrib2)+
   142 
   143 lemma plus_comm: "xs \<oplus> ys = ys \<oplus> xs"
   144 by (rule stream.coinduct[of "%x1 x2. \<exists>xs ys. x1 = xs \<oplus> ys \<and> x2 = ys \<oplus> xs"]) force+
   145 
   146 lemma plus_assoc: "(xs \<oplus> ys) \<oplus> zs = xs \<oplus> ys \<oplus> zs"
   147 by (rule stream.coinduct[of "%x1 x2. \<exists>xs ys zs. x1 = (xs \<oplus> ys) \<oplus> zs \<and> x2 = xs \<oplus> ys \<oplus> zs"]) force+
   148 
   149 end