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