10 |
10 |
11 theory Stream |
11 theory Stream |
12 imports TreeFI |
12 imports TreeFI |
13 begin |
13 begin |
14 |
14 |
15 hide_const (open) Quotient_Product.prod_pred |
15 hide_const (open) Quotient_Product.prod_rel |
16 hide_fact (open) Quotient_Product.prod_pred_def |
16 hide_fact (open) Quotient_Product.prod_rel_def |
17 |
17 |
18 codata_raw stream: 's = "'a \<times> 's" |
18 codata_raw stream: 's = "'a \<times> 's" |
19 |
19 |
20 (* selectors for streams *) |
20 (* selectors for streams *) |
21 definition "hdd as \<equiv> fst (stream_unf as)" |
21 definition "hdd as \<equiv> fst (stream_dtor as)" |
22 definition "tll as \<equiv> snd (stream_unf as)" |
22 definition "tll as \<equiv> snd (stream_dtor as)" |
23 |
23 |
24 lemma coiter_pair_fun_hdd[simp]: "hdd (stream_unf_coiter (f \<odot> g) t) = f t" |
24 lemma unfold_pair_fun_hdd[simp]: "hdd (stream_dtor_unfold (f \<odot> g) t) = f t" |
25 unfolding hdd_def pair_fun_def stream.unf_coiters by simp |
25 unfolding hdd_def pair_fun_def stream.dtor_unfolds by simp |
26 |
26 |
27 lemma coiter_pair_fun_tll[simp]: "tll (stream_unf_coiter (f \<odot> g) t) = |
27 lemma unfold_pair_fun_tll[simp]: "tll (stream_dtor_unfold (f \<odot> g) t) = |
28 stream_unf_coiter (f \<odot> g) (g t)" |
28 stream_dtor_unfold (f \<odot> g) (g t)" |
29 unfolding tll_def pair_fun_def stream.unf_coiters by simp |
29 unfolding tll_def pair_fun_def stream.dtor_unfolds by simp |
30 |
30 |
31 (* infinite trees: *) |
31 (* infinite trees: *) |
32 coinductive infiniteTr where |
32 coinductive infiniteTr where |
33 "\<lbrakk>tr' \<in> listF_set (sub tr); infiniteTr tr'\<rbrakk> \<Longrightarrow> infiniteTr tr" |
33 "\<lbrakk>tr' \<in> listF_set (sub tr); infiniteTr tr'\<rbrakk> \<Longrightarrow> infiniteTr tr" |
34 |
34 |
35 lemma infiniteTr_coind_upto[consumes 1, case_names sub]: |
35 lemma infiniteTr_strong_coind[consumes 1, case_names sub]: |
36 assumes *: "phi tr" and |
36 assumes *: "phi tr" and |
37 **: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr' \<or> infiniteTr tr'" |
37 **: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr' \<or> infiniteTr tr'" |
38 shows "infiniteTr tr" |
38 shows "infiniteTr tr" |
39 using assms by (elim infiniteTr.coinduct) blast |
39 using assms by (elim infiniteTr.coinduct) blast |
40 |
40 |
46 |
46 |
47 lemma infiniteTr_sub[simp]: |
47 lemma infiniteTr_sub[simp]: |
48 "infiniteTr tr \<Longrightarrow> (\<exists> tr' \<in> listF_set (sub tr). infiniteTr tr')" |
48 "infiniteTr tr \<Longrightarrow> (\<exists> tr' \<in> listF_set (sub tr). infiniteTr tr')" |
49 by (erule infiniteTr.cases) blast |
49 by (erule infiniteTr.cases) blast |
50 |
50 |
51 definition "konigPath \<equiv> stream_unf_coiter |
51 definition "konigPath \<equiv> stream_dtor_unfold |
52 (lab \<odot> (\<lambda>tr. SOME tr'. tr' \<in> listF_set (sub tr) \<and> infiniteTr tr'))" |
52 (lab \<odot> (\<lambda>tr. SOME tr'. tr' \<in> listF_set (sub tr) \<and> infiniteTr tr'))" |
53 |
53 |
54 lemma hdd_simps1[simp]: "hdd (konigPath t) = lab t" |
54 lemma hdd_simps1[simp]: "hdd (konigPath t) = lab t" |
55 unfolding konigPath_def by simp |
55 unfolding konigPath_def by simp |
56 |
56 |
61 (* proper paths in trees: *) |
61 (* proper paths in trees: *) |
62 coinductive properPath where |
62 coinductive properPath where |
63 "\<lbrakk>hdd as = lab tr; tr' \<in> listF_set (sub tr); properPath (tll as) tr'\<rbrakk> \<Longrightarrow> |
63 "\<lbrakk>hdd as = lab tr; tr' \<in> listF_set (sub tr); properPath (tll as) tr'\<rbrakk> \<Longrightarrow> |
64 properPath as tr" |
64 properPath as tr" |
65 |
65 |
66 lemma properPath_coind_upto[consumes 1, case_names hdd_lab sub]: |
66 lemma properPath_strong_coind[consumes 1, case_names hdd_lab sub]: |
67 assumes *: "phi as tr" and |
67 assumes *: "phi as tr" and |
68 **: "\<And> as tr. phi as tr \<Longrightarrow> hdd as = lab tr" and |
68 **: "\<And> as tr. phi as tr \<Longrightarrow> hdd as = lab tr" and |
69 ***: "\<And> as tr. |
69 ***: "\<And> as tr. |
70 phi as tr \<Longrightarrow> |
70 phi as tr \<Longrightarrow> |
71 \<exists> tr' \<in> listF_set (sub tr). phi (tll as) tr' \<or> properPath (tll as) tr'" |
71 \<exists> tr' \<in> listF_set (sub tr). phi (tll as) tr' \<or> properPath (tll as) tr'" |
77 **: "\<And> as tr. phi as tr \<Longrightarrow> hdd as = lab tr" and |
77 **: "\<And> as tr. phi as tr \<Longrightarrow> hdd as = lab tr" and |
78 ***: "\<And> as tr. |
78 ***: "\<And> as tr. |
79 phi as tr \<Longrightarrow> |
79 phi as tr \<Longrightarrow> |
80 \<exists> tr' \<in> listF_set (sub tr). phi (tll as) tr'" |
80 \<exists> tr' \<in> listF_set (sub tr). phi (tll as) tr'" |
81 shows "properPath as tr" |
81 shows "properPath as tr" |
82 using properPath_coind_upto[of phi, OF * **] *** by blast |
82 using properPath_strong_coind[of phi, OF * **] *** by blast |
83 |
83 |
84 lemma properPath_hdd_lab: |
84 lemma properPath_hdd_lab: |
85 "properPath as tr \<Longrightarrow> hdd as = lab tr" |
85 "properPath as tr \<Longrightarrow> hdd as = lab tr" |
86 by (erule properPath.cases) blast |
86 by (erule properPath.cases) blast |
87 |
87 |
112 thus ?thesis using assms by blast |
112 thus ?thesis using assms by blast |
113 qed |
113 qed |
114 |
114 |
115 (* some more stream theorems *) |
115 (* some more stream theorems *) |
116 |
116 |
117 lemma stream_map[simp]: "stream_map f = stream_unf_coiter (f o hdd \<odot> tll)" |
117 lemma stream_map[simp]: "stream_map f = stream_dtor_unfold (f o hdd \<odot> tll)" |
118 unfolding stream_map_def pair_fun_def hdd_def[abs_def] tll_def[abs_def] |
118 unfolding stream_map_def pair_fun_def hdd_def[abs_def] tll_def[abs_def] |
119 map_pair_def o_def prod_case_beta by simp |
119 map_pair_def o_def prod_case_beta by simp |
120 |
120 |
121 lemma prod_pred[simp]: "prod_pred \<phi>1 \<phi>2 a b = (\<phi>1 (fst a) (fst b) \<and> \<phi>2 (snd a) (snd b))" |
121 lemma prod_rel[simp]: "prod_rel \<phi>1 \<phi>2 a b = (\<phi>1 (fst a) (fst b) \<and> \<phi>2 (snd a) (snd b))" |
122 unfolding prod_pred_def by auto |
122 unfolding prod_rel_def by auto |
123 |
123 |
124 lemmas stream_coind = mp[OF stream.pred_coinduct, unfolded prod_pred[abs_def], |
124 lemmas stream_coind = |
125 folded hdd_def tll_def] |
125 mp[OF stream.rel_coinduct, unfolded prod_rel[abs_def], folded hdd_def tll_def] |
126 |
126 |
127 definition plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where |
127 definition plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where |
128 [simp]: "plus xs ys = |
128 [simp]: "plus xs ys = |
129 stream_unf_coiter ((%(xs, ys). hdd xs + hdd ys) \<odot> (%(xs, ys). (tll xs, tll ys))) (xs, ys)" |
129 stream_dtor_unfold ((%(xs, ys). hdd xs + hdd ys) \<odot> (%(xs, ys). (tll xs, tll ys))) (xs, ys)" |
130 |
130 |
131 definition scalar :: "nat \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<cdot>" 68) where |
131 definition scalar :: "nat \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<cdot>" 68) where |
132 [simp]: "scalar n = stream_map (\<lambda>x. n * x)" |
132 [simp]: "scalar n = stream_map (\<lambda>x. n * x)" |
133 |
133 |
134 definition ones :: "nat stream" where [simp]: "ones = stream_unf_coiter ((%x. 1) \<odot> id) ()" |
134 definition ones :: "nat stream" where [simp]: "ones = stream_dtor_unfold ((%x. 1) \<odot> id) ()" |
135 definition twos :: "nat stream" where [simp]: "twos = stream_unf_coiter ((%x. 2) \<odot> id) ()" |
135 definition twos :: "nat stream" where [simp]: "twos = stream_dtor_unfold ((%x. 2) \<odot> id) ()" |
136 definition ns :: "nat \<Rightarrow> nat stream" where [simp]: "ns n = scalar n ones" |
136 definition ns :: "nat \<Rightarrow> nat stream" where [simp]: "ns n = scalar n ones" |
137 |
137 |
138 lemma "ones \<oplus> ones = twos" |
138 lemma "ones \<oplus> ones = twos" |
139 by (intro stream_coind[where P="%x1 x2. \<exists>x. x1 = ones \<oplus> ones \<and> x2 = twos"]) auto |
139 by (intro stream_coind[where P="%x1 x2. \<exists>x. x1 = ones \<oplus> ones \<and> x2 = twos"]) auto |
140 |
140 |