author | traytel |
Wed, 02 Oct 2013 13:29:04 +0200 | |
changeset 54027 | e5853a648b59 |
parent 52992 | abd760a19e22 |
child 54490 | 930409d43211 |
permissions | -rw-r--r-- |
50530 | 1 |
(* Title: HOL/BNF/Examples/Koenig.thy |
50517 | 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 |
|
50518 | 12 |
imports TreeFI Stream |
50517 | 13 |
begin |
14 |
||
15 |
(* selectors for streams *) |
|
16 |
lemma shd_def': "shd as = fst (stream_dtor as)" |
|
52992 | 17 |
apply (case_tac as) |
18 |
apply (auto simp add: shd_def) |
|
19 |
by (simp add: Stream_def stream.dtor_ctor) |
|
50517 | 20 |
|
21 |
lemma stl_def': "stl as = snd (stream_dtor as)" |
|
52992 | 22 |
apply (case_tac as) |
23 |
apply (auto simp add: stl_def) |
|
24 |
by (simp add: Stream_def stream.dtor_ctor) |
|
50517 | 25 |
|
26 |
(* infinite trees: *) |
|
27 |
coinductive infiniteTr where |
|
28 |
"\<lbrakk>tr' \<in> listF_set (sub tr); infiniteTr tr'\<rbrakk> \<Longrightarrow> infiniteTr tr" |
|
29 |
||
30 |
lemma infiniteTr_strong_coind[consumes 1, case_names sub]: |
|
31 |
assumes *: "phi tr" and |
|
32 |
**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr' \<or> infiniteTr tr'" |
|
33 |
shows "infiniteTr tr" |
|
34 |
using assms by (elim infiniteTr.coinduct) blast |
|
35 |
||
36 |
lemma infiniteTr_coind[consumes 1, case_names sub, induct pred: infiniteTr]: |
|
37 |
assumes *: "phi tr" and |
|
38 |
**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr'" |
|
39 |
shows "infiniteTr tr" |
|
40 |
using assms by (elim infiniteTr.coinduct) blast |
|
41 |
||
42 |
lemma infiniteTr_sub[simp]: |
|
43 |
"infiniteTr tr \<Longrightarrow> (\<exists> tr' \<in> listF_set (sub tr). infiniteTr tr')" |
|
44 |
by (erule infiniteTr.cases) blast |
|
45 |
||
54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
52992
diff
changeset
|
46 |
primcorec konigPath where |
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
52992
diff
changeset
|
47 |
"shd (konigPath t) = lab t" |
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
52992
diff
changeset
|
48 |
| "stl (konigPath t) = konigPath (SOME tr. tr \<in> listF_set (sub t) \<and> infiniteTr tr)" |
50517 | 49 |
|
50 |
(* proper paths in trees: *) |
|
51 |
coinductive properPath where |
|
52 |
"\<lbrakk>shd as = lab tr; tr' \<in> listF_set (sub tr); properPath (stl as) tr'\<rbrakk> \<Longrightarrow> |
|
53 |
properPath as tr" |
|
54 |
||
55 |
lemma properPath_strong_coind[consumes 1, case_names shd_lab sub]: |
|
56 |
assumes *: "phi as tr" and |
|
57 |
**: "\<And> as tr. phi as tr \<Longrightarrow> shd as = lab tr" and |
|
58 |
***: "\<And> as tr. |
|
59 |
phi as tr \<Longrightarrow> |
|
60 |
\<exists> tr' \<in> listF_set (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'" |
|
61 |
shows "properPath as tr" |
|
62 |
using assms by (elim properPath.coinduct) blast |
|
63 |
||
64 |
lemma properPath_coind[consumes 1, case_names shd_lab sub, induct pred: properPath]: |
|
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'" |
|
70 |
shows "properPath as tr" |
|
71 |
using properPath_strong_coind[of phi, OF * **] *** by blast |
|
72 |
||
73 |
lemma properPath_shd_lab: |
|
74 |
"properPath as tr \<Longrightarrow> shd as = lab tr" |
|
75 |
by (erule properPath.cases) blast |
|
76 |
||
77 |
lemma properPath_sub: |
|
78 |
"properPath as tr \<Longrightarrow> |
|
79 |
\<exists> tr' \<in> listF_set (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'" |
|
80 |
by (erule properPath.cases) blast |
|
81 |
||
82 |
(* prove the following by coinduction *) |
|
83 |
theorem Konig: |
|
84 |
assumes "infiniteTr tr" |
|
85 |
shows "properPath (konigPath tr) tr" |
|
86 |
proof- |
|
87 |
{fix as |
|
88 |
assume "infiniteTr tr \<and> as = konigPath tr" hence "properPath as tr" |
|
54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
52992
diff
changeset
|
89 |
proof (coinduction arbitrary: tr as rule: properPath_coind) |
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
52992
diff
changeset
|
90 |
case (sub tr as) |
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
52992
diff
changeset
|
91 |
let ?t = "SOME t'. t' \<in> listF_set (sub tr) \<and> infiniteTr t'" |
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
52992
diff
changeset
|
92 |
from sub have "\<exists>t' \<in> listF_set (sub tr). infiniteTr t'" by simp |
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
52992
diff
changeset
|
93 |
then have "\<exists>t'. t' \<in> listF_set (sub tr) \<and> infiniteTr t'" by blast |
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
52992
diff
changeset
|
94 |
then have "?t \<in> listF_set (sub tr) \<and> infiniteTr ?t" by (rule someI_ex) |
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
52992
diff
changeset
|
95 |
moreover have "stl (konigPath tr) = konigPath ?t" by simp |
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
52992
diff
changeset
|
96 |
ultimately show ?case using sub by blast |
50517 | 97 |
qed simp |
98 |
} |
|
99 |
thus ?thesis using assms by blast |
|
100 |
qed |
|
101 |
||
102 |
(* some more stream theorems *) |
|
103 |
||
54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
52992
diff
changeset
|
104 |
primcorec plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where |
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
52992
diff
changeset
|
105 |
"shd (plus xs ys) = shd xs + shd ys" |
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
52992
diff
changeset
|
106 |
| "stl (plus xs ys) = plus (stl xs) (stl ys)" |
50517 | 107 |
|
108 |
definition scalar :: "nat \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<cdot>" 68) where |
|
51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
50530
diff
changeset
|
109 |
[simp]: "scalar n = smap (\<lambda>x. n * x)" |
50517 | 110 |
|
54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
52992
diff
changeset
|
111 |
primcorec ones :: "nat stream" where "ones = 1 ## ones" |
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
52992
diff
changeset
|
112 |
primcorec twos :: "nat stream" where "twos = 2 ## twos" |
50517 | 113 |
definition ns :: "nat \<Rightarrow> nat stream" where [simp]: "ns n = scalar n ones" |
114 |
||
115 |
lemma "ones \<oplus> ones = twos" |
|
54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
52992
diff
changeset
|
116 |
by coinduction simp |
50517 | 117 |
|
118 |
lemma "n \<cdot> twos = ns (2 * n)" |
|
54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
52992
diff
changeset
|
119 |
by coinduction simp |
50517 | 120 |
|
121 |
lemma prod_scalar: "(n * m) \<cdot> xs = n \<cdot> m \<cdot> xs" |
|
54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
52992
diff
changeset
|
122 |
by (coinduction arbitrary: xs) auto |
50517 | 123 |
|
124 |
lemma scalar_plus: "n \<cdot> (xs \<oplus> ys) = n \<cdot> xs \<oplus> n \<cdot> ys" |
|
54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
52992
diff
changeset
|
125 |
by (coinduction arbitrary: xs ys) (auto simp: add_mult_distrib2) |
50517 | 126 |
|
127 |
lemma plus_comm: "xs \<oplus> ys = ys \<oplus> xs" |
|
54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
52992
diff
changeset
|
128 |
by (coinduction arbitrary: xs ys) auto |
50517 | 129 |
|
130 |
lemma plus_assoc: "(xs \<oplus> ys) \<oplus> zs = xs \<oplus> ys \<oplus> zs" |
|
54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
52992
diff
changeset
|
131 |
by (coinduction arbitrary: xs ys zs) auto |
50517 | 132 |
|
133 |
end |