src/HOL/Datatype_Examples/Koenig.thy
 author blanchet Thu Sep 11 19:26:59 2014 +0200 (2014-09-11) changeset 58309 a09ec6daaa19 parent 57634 src/HOL/BNF_Examples/Koenig.thy@efc00b9b8680 child 58607 1f90ea1b4010 permissions -rw-r--r--
renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
```     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 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
```