10 |
10 |
11 theory Koenig |
11 theory Koenig |
12 imports TreeFI Stream |
12 imports TreeFI Stream |
13 begin |
13 begin |
14 |
14 |
15 (* selectors for streams *) |
|
16 lemma shd_def': "shd as = fst (stream_dtor as)" |
|
17 apply (case_tac as) |
|
18 apply (auto simp add: shd_def) |
|
19 by (simp add: Stream_def stream.dtor_ctor) |
|
20 |
|
21 lemma stl_def': "stl as = snd (stream_dtor as)" |
|
22 apply (case_tac as) |
|
23 apply (auto simp add: stl_def) |
|
24 by (simp add: Stream_def stream.dtor_ctor) |
|
25 |
|
26 (* infinite trees: *) |
15 (* infinite trees: *) |
27 coinductive infiniteTr where |
16 coinductive infiniteTr where |
28 "\<lbrakk>tr' \<in> listF_set (sub tr); infiniteTr tr'\<rbrakk> \<Longrightarrow> infiniteTr tr" |
17 "\<lbrakk>tr' \<in> set_listF (sub tr); infiniteTr tr'\<rbrakk> \<Longrightarrow> infiniteTr tr" |
29 |
18 |
30 lemma infiniteTr_strong_coind[consumes 1, case_names sub]: |
19 lemma infiniteTr_strong_coind[consumes 1, case_names sub]: |
31 assumes *: "phi tr" and |
20 assumes *: "phi tr" and |
32 **: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr' \<or> infiniteTr tr'" |
21 **: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> set_listF (sub tr). phi tr' \<or> infiniteTr tr'" |
33 shows "infiniteTr tr" |
22 shows "infiniteTr tr" |
34 using assms by (elim infiniteTr.coinduct) blast |
23 using assms by (elim infiniteTr.coinduct) blast |
35 |
24 |
36 lemma infiniteTr_coind[consumes 1, case_names sub, induct pred: infiniteTr]: |
25 lemma infiniteTr_coind[consumes 1, case_names sub, induct pred: infiniteTr]: |
37 assumes *: "phi tr" and |
26 assumes *: "phi tr" and |
38 **: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr'" |
27 **: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> set_listF (sub tr). phi tr'" |
39 shows "infiniteTr tr" |
28 shows "infiniteTr tr" |
40 using assms by (elim infiniteTr.coinduct) blast |
29 using assms by (elim infiniteTr.coinduct) blast |
41 |
30 |
42 lemma infiniteTr_sub[simp]: |
31 lemma infiniteTr_sub[simp]: |
43 "infiniteTr tr \<Longrightarrow> (\<exists> tr' \<in> listF_set (sub tr). infiniteTr tr')" |
32 "infiniteTr tr \<Longrightarrow> (\<exists> tr' \<in> set_listF (sub tr). infiniteTr tr')" |
44 by (erule infiniteTr.cases) blast |
33 by (erule infiniteTr.cases) blast |
45 |
34 |
46 primcorec konigPath where |
35 primcorec konigPath where |
47 "shd (konigPath t) = lab t" |
36 "shd (konigPath t) = lab t" |
48 | "stl (konigPath t) = konigPath (SOME tr. tr \<in> listF_set (sub t) \<and> infiniteTr tr)" |
37 | "stl (konigPath t) = konigPath (SOME tr. tr \<in> set_listF (sub t) \<and> infiniteTr tr)" |
49 |
38 |
50 (* proper paths in trees: *) |
39 (* proper paths in trees: *) |
51 coinductive properPath where |
40 coinductive properPath where |
52 "\<lbrakk>shd as = lab tr; tr' \<in> listF_set (sub tr); properPath (stl as) tr'\<rbrakk> \<Longrightarrow> |
41 "\<lbrakk>shd as = lab tr; tr' \<in> set_listF (sub tr); properPath (stl as) tr'\<rbrakk> \<Longrightarrow> |
53 properPath as tr" |
42 properPath as tr" |
54 |
43 |
55 lemma properPath_strong_coind[consumes 1, case_names shd_lab sub]: |
44 lemma properPath_strong_coind[consumes 1, case_names shd_lab sub]: |
56 assumes *: "phi as tr" and |
45 assumes *: "phi as tr" and |
57 **: "\<And> as tr. phi as tr \<Longrightarrow> shd as = lab tr" and |
46 **: "\<And> as tr. phi as tr \<Longrightarrow> shd as = lab tr" and |
58 ***: "\<And> as tr. |
47 ***: "\<And> as tr. |
59 phi as tr \<Longrightarrow> |
48 phi as tr \<Longrightarrow> |
60 \<exists> tr' \<in> listF_set (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'" |
49 \<exists> tr' \<in> set_listF (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'" |
61 shows "properPath as tr" |
50 shows "properPath as tr" |
62 using assms by (elim properPath.coinduct) blast |
51 using assms by (elim properPath.coinduct) blast |
63 |
52 |
64 lemma properPath_coind[consumes 1, case_names shd_lab sub, induct pred: properPath]: |
53 lemma properPath_coind[consumes 1, case_names shd_lab sub, induct pred: properPath]: |
65 assumes *: "phi as tr" and |
54 assumes *: "phi as tr" and |
66 **: "\<And> as tr. phi as tr \<Longrightarrow> shd as = lab tr" and |
55 **: "\<And> as tr. phi as tr \<Longrightarrow> shd as = lab tr" and |
67 ***: "\<And> as tr. |
56 ***: "\<And> as tr. |
68 phi as tr \<Longrightarrow> |
57 phi as tr \<Longrightarrow> |
69 \<exists> tr' \<in> listF_set (sub tr). phi (stl as) tr'" |
58 \<exists> tr' \<in> set_listF (sub tr). phi (stl as) tr'" |
70 shows "properPath as tr" |
59 shows "properPath as tr" |
71 using properPath_strong_coind[of phi, OF * **] *** by blast |
60 using properPath_strong_coind[of phi, OF * **] *** by blast |
72 |
61 |
73 lemma properPath_shd_lab: |
62 lemma properPath_shd_lab: |
74 "properPath as tr \<Longrightarrow> shd as = lab tr" |
63 "properPath as tr \<Longrightarrow> shd as = lab tr" |
75 by (erule properPath.cases) blast |
64 by (erule properPath.cases) blast |
76 |
65 |
77 lemma properPath_sub: |
66 lemma properPath_sub: |
78 "properPath as tr \<Longrightarrow> |
67 "properPath as tr \<Longrightarrow> |
79 \<exists> tr' \<in> listF_set (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'" |
68 \<exists> tr' \<in> set_listF (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'" |
80 by (erule properPath.cases) blast |
69 by (erule properPath.cases) blast |
81 |
70 |
82 (* prove the following by coinduction *) |
71 (* prove the following by coinduction *) |
83 theorem Konig: |
72 theorem Konig: |
84 assumes "infiniteTr tr" |
73 assumes "infiniteTr tr" |
86 proof- |
75 proof- |
87 {fix as |
76 {fix as |
88 assume "infiniteTr tr \<and> as = konigPath tr" hence "properPath as tr" |
77 assume "infiniteTr tr \<and> as = konigPath tr" hence "properPath as tr" |
89 proof (coinduction arbitrary: tr as rule: properPath_coind) |
78 proof (coinduction arbitrary: tr as rule: properPath_coind) |
90 case (sub tr as) |
79 case (sub tr as) |
91 let ?t = "SOME t'. t' \<in> listF_set (sub tr) \<and> infiniteTr t'" |
80 let ?t = "SOME t'. t' \<in> set_listF (sub tr) \<and> infiniteTr t'" |
92 from sub have "\<exists>t' \<in> listF_set (sub tr). infiniteTr t'" by simp |
81 from sub have "\<exists>t' \<in> set_listF (sub tr). infiniteTr t'" by simp |
93 then have "\<exists>t'. t' \<in> listF_set (sub tr) \<and> infiniteTr t'" by blast |
82 then have "\<exists>t'. t' \<in> set_listF (sub tr) \<and> infiniteTr t'" by blast |
94 then have "?t \<in> listF_set (sub tr) \<and> infiniteTr ?t" by (rule someI_ex) |
83 then have "?t \<in> set_listF (sub tr) \<and> infiniteTr ?t" by (rule someI_ex) |
95 moreover have "stl (konigPath tr) = konigPath ?t" by simp |
84 moreover have "stl (konigPath tr) = konigPath ?t" by simp |
96 ultimately show ?case using sub by blast |
85 ultimately show ?case using sub by blast |
97 qed simp |
86 qed simp |
98 } |
87 } |
99 thus ?thesis using assms by blast |
88 thus ?thesis using assms by blast |