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