10 THEN hyp_subst_tac i THEN hyp_subst_tac (i+1); |
10 THEN hyp_subst_tac i THEN hyp_subst_tac (i+1); |
11 |
11 |
12 |
12 |
13 val [stream_con_rew1,stream_con_rew2] = stream.con_rews; |
13 val [stream_con_rew1,stream_con_rew2] = stream.con_rews; |
14 |
14 |
|
15 Addsimps stream.take_rews; |
|
16 Addsimps stream.when_rews; |
|
17 Addsimps stream.sel_rews; |
|
18 |
15 (* ----------------------------------------------------------------------- *) |
19 (* ----------------------------------------------------------------------- *) |
16 (* theorems about scons *) |
20 (* theorems about scons *) |
17 (* ----------------------------------------------------------------------- *) |
21 (* ----------------------------------------------------------------------- *) |
18 |
22 |
19 section "scons"; |
23 section "scons"; |
20 |
24 |
21 qed_goal "scons_eq_UU" thy "a && s = UU = (a = UU)" (fn _ => [ |
25 Goal "a && s = UU = (a = UU)"; |
22 safe_tac HOL_cs, |
26 by Safe_tac; |
23 etac contrapos2 1, |
27 by (etac contrapos2 1); |
24 safe_tac (HOL_cs addSIs stream.con_rews)]); |
28 by (safe_tac (claset() addSIs stream.con_rews)); |
25 |
29 qed "scons_eq_UU"; |
26 qed_goal "scons_not_empty" thy "[| a && x = UU; a ~= UU |] ==> R" |
30 |
27 (fn prems => [ |
31 Goal "[| a && x = UU; a ~= UU |] ==> R"; |
28 cut_facts_tac prems 1, |
32 by (dresolve_tac [stream_con_rew2] 1); |
29 dresolve_tac [stream_con_rew2] 1, |
33 by (contr_tac 1); |
30 contr_tac 1]); |
34 qed "scons_not_empty"; |
31 |
35 |
32 qed_goal "stream_exhaust_eq" thy "x ~= UU = (? a y. a ~= UU & x = a && y)" |
36 Goal "x ~= UU = (EX a y. a ~= UU & x = a && y)"; |
33 (fn _ =>[ |
37 by (cut_facts_tac [stream.exhaust] 1); |
34 cut_facts_tac [stream.exhaust] 1, |
38 by (best_tac (claset() addDs [stream_con_rew2]) 1); |
35 safe_tac HOL_cs, |
39 qed "stream_exhaust_eq"; |
36 contr_tac 1, |
40 |
37 fast_tac (HOL_cs addDs [stream_con_rew2]) 1, |
41 Goal |
38 fast_tac HOL_cs 1, |
42 "[| a && s << t; a ~= UU |] ==> EX b tt. t = b && tt & b ~= UU & s << tt"; |
39 fast_tac (HOL_cs addDs [stream_con_rew2]) 1]); |
43 by (stream_case_tac "t" 1); |
40 |
44 by (fast_tac (claset() addDs [eq_UU_iff RS iffD2, stream_con_rew2]) 1); |
41 qed_goal "stream_prefix" thy |
45 by (fast_tac (claset() addDs stream.inverts) 1); |
42 "[| a && s << t; a ~= UU |] ==> ? b tt. t = b && tt & b ~= UU & s << tt" |
46 qed "stream_prefix"; |
43 (fn prems => [ |
47 |
44 cut_facts_tac prems 1, |
48 Goal "[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys"; |
45 stream_case_tac "t" 1, |
49 by (cut_inst_tac [("x1","x::'a::flat"), ("x","y::'a::flat")] |
46 fast_tac (HOL_cs addDs [eq_UU_iff RS iffD2, stream_con_rew2]) 1, |
50 (ax_flat RS spec RS spec) 1); |
47 fast_tac (HOL_cs addDs stream.inverts) 1]); |
51 by (forward_tac stream.inverts 1); |
48 |
52 by Safe_tac; |
49 qed_goal "stream_flat_prefix" thy |
53 by (dtac (hd stream.con_rews RS subst) 1); |
50 "[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys" |
54 by (fast_tac (claset() addDs [eq_UU_iff RS iffD2, stream_con_rew2]) 1); |
51 (fn prems=>[ |
55 qed "stream_flat_prefix"; |
52 cut_facts_tac prems 1, |
56 |
53 (cut_facts_tac [read_instantiate[("x1","x::'a::flat"), |
57 Goal "b ~= UU ==> x << b && z = \ |
54 ("x","y::'a::flat")] |
58 \ (x = UU | (EX a y. x = a && y & a ~= UU & a << b & y << z))"; |
55 (ax_flat RS spec RS spec)] 1), |
59 by Safe_tac; |
56 (forward_tac stream.inverts 1), |
60 by (stream_case_tac "x" 1); |
57 (safe_tac HOL_cs), |
61 by (safe_tac (claset() addSDs stream.inverts |
58 (dtac (hd stream.con_rews RS subst) 1), |
62 addSIs [minimal, monofun_cfun, monofun_cfun_arg])); |
59 (fast_tac (HOL_cs addDs [eq_UU_iff RS iffD2, stream_con_rew2]) 1)]); |
63 by (Fast_tac 1); |
60 |
64 qed "stream_prefix'"; |
61 qed_goal "stream_prefix'" thy "b ~= UU ==> x << b && z = \ |
65 |
62 \(x = UU | (? a y. x = a && y & a ~= UU & a << b & y << z))" (fn prems => [ |
66 Goal "[| a ~= UU; b ~= UU |] ==> (a && s = b && t) = (a = b & s = t)"; |
63 cut_facts_tac prems 1, |
67 by (best_tac (claset() addSEs stream.injects) 1); |
64 safe_tac HOL_cs, |
68 qed "stream_inject_eq"; |
65 stream_case_tac "x" 1, |
|
66 safe_tac (HOL_cs addSDs stream.inverts |
|
67 addSIs [minimal, monofun_cfun, monofun_cfun_arg]), |
|
68 fast_tac HOL_cs 1]); |
|
69 |
|
70 qed_goal "stream_inject_eq" thy |
|
71 "[| a ~= UU; b ~= UU |] ==> (a && s = b && t) = (a = b & s = t)" (fn prems => [ |
|
72 cut_facts_tac prems 1, |
|
73 safe_tac (HOL_cs addSEs stream.injects)]); |
|
74 |
69 |
75 |
70 |
76 (* ----------------------------------------------------------------------- *) |
71 (* ----------------------------------------------------------------------- *) |
77 (* theorems about stream_when *) |
72 (* theorems about stream_when *) |
78 (* ----------------------------------------------------------------------- *) |
73 (* ----------------------------------------------------------------------- *) |
79 |
74 |
80 section "stream_when"; |
75 section "stream_when"; |
81 |
76 |
82 qed_goal "stream_when_strictf" thy "stream_when`UU`s=UU" (fn _ => [ |
77 Goal "stream_when`UU`s=UU"; |
83 stream_case_tac "s" 1, |
78 by (stream_case_tac "s" 1); |
84 ALLGOALS(asm_simp_tac (HOL_ss addsimps strict_Rep_CFun1::stream.when_rews)) |
79 by (ALLGOALS(asm_simp_tac (simpset() addsimps [strict_Rep_CFun1]))); |
85 ]); |
80 qed "stream_when_strictf"; |
86 |
81 |
87 |
82 |
88 (* ----------------------------------------------------------------------- *) |
83 (* ----------------------------------------------------------------------- *) |
89 (* theorems about ft and rt *) |
84 (* theorems about ft and rt *) |
90 (* ----------------------------------------------------------------------- *) |
85 (* ----------------------------------------------------------------------- *) |
91 |
86 |
92 section "ft & rt"; |
87 section "ft & rt"; |
93 |
88 |
94 (* |
89 (* |
95 qed_goal "stream_ft_lemma1" thy "ft`s=UU --> s=UU" (fn prems => [ |
90 Goal "ft`s=UU --> s=UU"; |
96 stream_case_tac "s" 1, |
91 by (stream_case_tac "s" 1); |
97 REPEAT (asm_simp_tac (HOLCF_ss addsimps stream.rews) 1)]); |
92 by (REPEAT (asm_simp_tac (simpset() addsimps stream.rews) 1)); |
|
93 qed "stream_ft_lemma1"; |
98 *) |
94 *) |
99 |
95 |
100 qed_goal "ft_defin" thy "s~=UU ==> ft`s~=UU" (fn prems => [ |
96 Goal "s~=UU ==> ft`s~=UU"; |
101 cut_facts_tac prems 1, |
97 by (stream_case_tac "s" 1); |
102 stream_case_tac "s" 1, |
98 by (Blast_tac 1); |
103 fast_tac HOL_cs 1, |
99 by (asm_simp_tac (simpset() addsimps stream.rews) 1); |
104 asm_simp_tac (HOLCF_ss addsimps stream.rews) 1]); |
100 qed "ft_defin"; |
105 |
101 |
106 qed_goal "rt_strict_rev" thy "rt`s~=UU ==> s~=UU" (fn prems => [ |
102 Goal "rt`s~=UU ==> s~=UU"; |
107 cut_facts_tac prems 1, |
103 by Auto_tac; |
108 etac contrapos 1, |
104 qed "rt_strict_rev"; |
109 asm_simp_tac (HOLCF_ss addsimps stream.sel_rews) 1]); |
105 |
110 |
106 Goal "(ft`s)&&(rt`s)=s"; |
111 qed_goal "surjectiv_scons" thy "(ft`s)&&(rt`s)=s" |
107 by (stream_case_tac "s" 1); |
112 (fn prems => |
108 by (ALLGOALS (asm_simp_tac (simpset() addsimps stream.rews))); |
113 [ |
109 qed "surjectiv_scons"; |
114 stream_case_tac "s" 1, |
110 |
115 REPEAT (asm_simp_tac (HOLCF_ss addsimps stream.rews) 1) |
111 Goal "ALL x s. x << s --> iterate i rt x << iterate i rt s"; |
116 ]); |
112 by (induct_tac "i" 1); |
117 |
113 by (Simp_tac 1); |
118 qed_goal_spec_mp "monofun_rt_mult" thy |
114 by (strip_tac 1); |
119 "!x s. x << s --> iterate i rt x << iterate i rt s" (fn _ => [ |
115 by (stream_case_tac "x" 1); |
120 nat_ind_tac "i" 1, |
116 by (rtac (minimal RS (monofun_iterate2 RS monofunE RS spec RS spec RS mp))1); |
121 simp_tac (HOLCF_ss addsimps stream.take_rews) 1, |
117 by (dtac stream_prefix 1); |
122 strip_tac 1, |
118 by Safe_tac; |
123 stream_case_tac "x" 1, |
119 by (asm_simp_tac (HOL_ss addsimps iterate_Suc2::stream.rews) 1); |
124 rtac (minimal RS (monofun_iterate2 RS monofunE RS spec RS spec RS mp))1, |
120 qed_spec_mp "monofun_rt_mult"; |
125 dtac stream_prefix 1, |
121 |
126 safe_tac HOL_cs, |
|
127 asm_simp_tac (HOL_ss addsimps iterate_Suc2::stream.rews) 1]); |
|
128 |
122 |
129 |
123 |
130 (* ----------------------------------------------------------------------- *) |
124 (* ----------------------------------------------------------------------- *) |
131 (* theorems about stream_take *) |
125 (* theorems about stream_take *) |
132 (* ----------------------------------------------------------------------- *) |
126 (* ----------------------------------------------------------------------- *) |
133 |
127 |
134 section "stream_take"; |
128 section "stream_take"; |
135 |
129 |
136 qed_goal "stream_reach2" thy "(LUB i. stream_take i`s) = s" |
130 Goal "(LUB i. stream_take i`s) = s"; |
137 (fn prems => |
131 by (subgoal_tac "(LUB i. stream_take i`s) = fix`stream_copy`s" 1); |
138 [ |
132 by (simp_tac (simpset() addsimps [fix_def2, stream.take_def, |
139 (res_inst_tac [("t","s")] (stream.reach RS subst) 1), |
133 contlub_cfun_fun, chain_iterate]) 2); |
140 (stac fix_def2 1), |
134 by (asm_full_simp_tac (simpset() addsimps [stream.reach]) 1); |
141 (rewrite_goals_tac [stream.take_def]), |
135 qed "stream_reach2"; |
142 (stac contlub_cfun_fun 1), |
136 |
143 (rtac chain_iterate 1), |
137 Goal "chain (%i. stream_take i`s)"; |
144 (rtac refl 1) |
138 by (rtac chainI 1); |
145 ]); |
139 by (subgoal_tac "ALL i s. stream_take i`s << stream_take (Suc i)`s" 1); |
146 |
140 by (Fast_tac 1); |
147 qed_goal "chain_stream_take" thy "chain (%i. stream_take i`s)" (fn _ => [ |
141 by (rtac allI 1); |
148 rtac chainI 1, |
142 by (induct_tac "ia" 1); |
149 subgoal_tac "!i s. stream_take i`s << stream_take (Suc i)`s" 1, |
143 by (Simp_tac 1); |
150 fast_tac HOL_cs 1, |
144 by (rtac allI 1); |
151 rtac allI 1, |
145 by (stream_case_tac "s" 1); |
152 nat_ind_tac "i" 1, |
146 by (Simp_tac 1); |
153 simp_tac (HOLCF_ss addsimps stream.take_rews) 1, |
147 by (asm_simp_tac (simpset() addsimps [monofun_cfun_arg]) 1); |
154 rtac allI 1, |
148 qed "chain_stream_take"; |
155 stream_case_tac "s" 1, |
149 |
156 simp_tac (HOLCF_ss addsimps stream.take_rews) 1, |
150 |
157 asm_simp_tac (HOLCF_ss addsimps monofun_cfun_arg::stream.take_rews) 1]); |
151 Goalw [stream.take_def] |
158 |
152 "stream_take n`x = x ==> stream_take (Suc n)`x = x"; |
159 qed_goalw "stream_take_more" thy [stream.take_def] |
153 by (rtac antisym_less 1); |
160 "stream_take n`x = x ==> stream_take (Suc n)`x = x" (fn prems => [ |
154 by (subgoal_tac "iterate (Suc n) stream_copy UU`x << fix`stream_copy`x" 1); |
161 cut_facts_tac prems 1, |
155 by (asm_full_simp_tac (simpset() addsimps [stream.reach]) 1); |
162 rtac antisym_less 1, |
156 by (rtac monofun_cfun_fun 1); |
163 rtac (stream.reach RS subst) 1, (* 1*back(); *) |
157 by (stac fix_def2 1); |
164 rtac monofun_cfun_fun 1, |
158 by (rtac is_ub_thelub 1); |
165 stac fix_def2 1, |
159 by (rtac chain_iterate 1); |
166 rtac is_ub_thelub 1, |
160 by (etac subst 1 THEN rtac monofun_cfun_fun 1); |
167 rtac chain_iterate 1, |
161 by (rtac (rewrite_rule [chain] chain_iterate RS spec) 1); |
168 etac subst 1, (* 2*back(); *) |
162 qed "stream_take_more"; |
169 rtac monofun_cfun_fun 1, |
|
170 rtac (rewrite_rule [chain] chain_iterate RS spec) 1]); |
|
171 |
163 |
172 (* |
164 (* |
173 val stream_take_lemma2 = prove_goal thy |
165 Goal |
174 "! s2. stream_take n`s2 = s2 --> stream_take (Suc n)`s2=s2" (fn prems => [ |
166 "ALL s2. stream_take n`s2 = s2 --> stream_take (Suc n)`s2=s2"; |
175 (nat_ind_tac "n" 1), |
167 by (induct_tac "n" 1); |
176 (simp_tac (simpset() addsimps stream_rews) 1), |
168 by (simp_tac (simpset() addsimps stream_rews) 1); |
177 (strip_tac 1), |
169 by (strip_tac 1); |
178 (hyp_subst_tac 1), |
170 by (hyp_subst_tac 1); |
179 (simp_tac (simpset() addsimps stream_rews) 1), |
171 by (simp_tac (simpset() addsimps stream_rews) 1); |
180 (rtac allI 1), |
172 by (rtac allI 1); |
181 (res_inst_tac [("s","s2")] streamE 1), |
173 by (res_inst_tac [("s","s2")] streamE 1); |
182 (asm_simp_tac (simpset() addsimps stream_rews) 1), |
174 by (asm_simp_tac (simpset() addsimps stream_rews) 1); |
183 (asm_simp_tac (simpset() addsimps stream_rews) 1), |
175 by (asm_simp_tac (simpset() addsimps stream_rews) 1); |
184 (strip_tac 1 ), |
176 by (strip_tac 1 ); |
185 (subgoal_tac "stream_take n1`xs = xs" 1), |
177 by (subgoal_tac "stream_take n1`xs = xs" 1); |
186 (rtac ((hd stream_inject) RS conjunct2) 2), |
178 by (rtac ((hd stream_inject) RS conjunct2) 2); |
187 (atac 4), |
179 by (atac 4); |
188 (atac 2), |
180 by (atac 2); |
189 (atac 2), |
181 by (atac 2); |
190 (rtac cfun_arg_cong 1), |
182 by (rtac cfun_arg_cong 1); |
191 (fast_tac HOL_cs 1) |
183 by (Blast_tac 1); |
192 ]); |
184 qed "stream_take_lemma2"; |
193 *) |
185 *) |
194 |
186 |
195 val stream_take_lemma3 = prove_goal thy |
187 Goal |
196 "!x xs. x~=UU --> stream_take n`(x && xs) = x && xs --> stream_take n`xs=xs" |
188 "ALL x xs. x~=UU --> stream_take n`(x && xs) = x && xs --> stream_take n`xs=xs"; |
197 (fn prems => [ |
189 by (induct_tac "n" 1); |
198 (nat_ind_tac "n" 1), |
190 by (Asm_simp_tac 1); |
199 (asm_simp_tac (HOL_ss addsimps stream.take_rews) 1), |
191 by (strip_tac 1); |
200 (strip_tac 1), |
192 by (res_inst_tac [("P","x && xs=UU")] notE 1); |
201 (res_inst_tac [("P","x && xs=UU")] notE 1), |
193 by (eresolve_tac stream.con_rews 1); |
202 (eresolve_tac stream.con_rews 1), |
194 by (etac sym 1); |
203 (etac sym 1), |
195 by (strip_tac 1); |
204 (strip_tac 1), |
196 by (rtac stream_take_more 1); |
205 (rtac stream_take_more 1), |
197 by (res_inst_tac [("a1","x")] ((hd stream.injects) RS conjunct2) 1); |
206 (res_inst_tac [("a1","x")] ((hd stream.injects) RS conjunct2) 1), |
198 by (assume_tac 3); |
207 (etac (hd(tl(tl(stream.take_rews))) RS subst) 1), |
199 by (etac (hd(tl(tl(stream.take_rews))) RS subst) 1); |
208 (atac 1), |
200 by (atac 1); |
209 (atac 1)]) RS spec RS spec RS mp RS mp; |
201 qed_spec_mp "stream_take_lemma3"; |
210 |
202 |
211 val stream_take_lemma4 = prove_goal thy |
203 Goal |
212 "!x xs. stream_take n`xs=xs --> stream_take (Suc n)`(x && xs) = x && xs" |
204 "ALL x xs. stream_take n`xs=xs --> stream_take (Suc n)`(x && xs) = x && xs"; |
213 (fn _ => [ |
205 by (induct_tac "n" 1); |
214 (nat_ind_tac "n" 1), |
206 by Auto_tac; |
215 (simp_tac (HOL_ss addsimps stream.take_rews) 1), |
207 qed_spec_mp "stream_take_lemma4"; |
216 (simp_tac (HOL_ss addsimps stream.take_rews) 1) |
|
217 ]) RS spec RS spec RS mp; |
|
218 |
208 |
219 |
209 |
220 (* ------------------------------------------------------------------------- *) |
210 (* ------------------------------------------------------------------------- *) |
221 (* special induction rules *) |
211 (* special induction rules *) |
222 (* ------------------------------------------------------------------------- *) |
212 (* ------------------------------------------------------------------------- *) |
223 |
213 |
224 section "induction"; |
214 section "induction"; |
225 |
215 |
226 qed_goalw "stream_finite_ind" thy [stream.finite_def] |
216 |
227 "[| stream_finite x; P UU; !!a s. [| a ~= UU; P s |] ==> P (a && s) |] ==> P x" |
217 val prems = Goalw [stream.finite_def] |
228 (fn prems => [ |
218 "[| stream_finite x; \ |
229 (cut_facts_tac prems 1), |
219 \ P UU; \ |
230 (etac exE 1), |
220 \ !!a s. [| a ~= UU; P s |] \ |
231 (etac subst 1), |
221 \ ==> P (a && s) |] ==> P x"; |
232 (rtac stream.finite_ind 1), |
222 by (cut_facts_tac prems 1); |
233 (atac 1), |
223 by (etac exE 1); |
234 (eresolve_tac prems 1), |
224 by (etac subst 1); |
235 (atac 1)]); |
225 by (rtac stream.finite_ind 1); |
236 |
226 by (atac 1); |
237 qed_goal "stream_finite_ind2" thy |
227 by (eresolve_tac prems 1); |
|
228 by (atac 1); |
|
229 qed "stream_finite_ind"; |
|
230 |
|
231 val major::prems = Goal |
238 "[| P UU;\ |
232 "[| P UU;\ |
239 \ !! x . x ~= UU ==> P (x && UU); \ |
233 \ !! x . x ~= UU ==> P (x && UU); \ |
240 \ !! y z s. [| y ~= UU; z ~= UU; P s |] ==> P (y && z && s ) \ |
234 \ !! y z s. [| y ~= UU; z ~= UU; P s |] ==> P (y && z && s ) \ |
241 \ |] ==> !s. P (stream_take n`s)" (fn prems => [ |
235 \ |] ==> !s. P (stream_take n`s)"; |
242 res_inst_tac [("n","n")] nat_induct2 1, |
236 by (res_inst_tac [("n","n")] nat_induct2 1); |
243 asm_simp_tac (HOL_ss addsimps (hd prems)::stream.take_rews) 1, |
237 by (asm_simp_tac (simpset() addsimps [major]) 1); |
244 rtac allI 1, |
238 by (rtac allI 1); |
245 stream_case_tac "s" 1, |
239 by (stream_case_tac "s" 1); |
246 asm_simp_tac (HOL_ss addsimps (hd prems)::stream.take_rews) 1, |
240 by (asm_simp_tac (simpset() addsimps [major]) 1); |
247 asm_simp_tac (HOL_ss addsimps stream.take_rews addsimps prems) 1, |
241 by (asm_simp_tac (simpset() addsimps prems) 1); |
248 rtac allI 1, |
242 by (rtac allI 1); |
249 stream_case_tac "s" 1, |
243 by (stream_case_tac "s" 1); |
250 asm_simp_tac (HOL_ss addsimps (hd prems)::stream.take_rews) 1, |
244 by (asm_simp_tac (simpset() addsimps [major]) 1); |
251 res_inst_tac [("x","sa")] stream.casedist 1, |
245 by (res_inst_tac [("x","sa")] stream.casedist 1); |
252 asm_simp_tac (HOL_ss addsimps stream.take_rews addsimps prems) 1, |
246 by (asm_simp_tac (simpset() addsimps prems) 1); |
253 asm_simp_tac (HOL_ss addsimps stream.take_rews addsimps prems) 1]); |
247 by (asm_simp_tac (simpset() addsimps prems) 1); |
254 |
248 qed "stream_finite_ind2"; |
255 |
249 |
256 qed_goal "stream_ind2" thy |
250 |
|
251 val prems = Goal |
257 "[| adm P; P UU; !!a. a ~= UU ==> P (a && UU); \ |
252 "[| adm P; P UU; !!a. a ~= UU ==> P (a && UU); \ |
258 \ !!a b s. [| a ~= UU; b ~= UU; P s |] ==> P (a && b && s)\ |
253 \ !!a b s. [| a ~= UU; b ~= UU; P s |] ==> P (a && b && s)\ |
259 \ |] ==> P x" (fn prems => [ |
254 \ |] ==> P x"; |
260 rtac (stream.reach RS subst) 1, |
255 by (rtac (stream.reach RS subst) 1); |
261 rtac (adm_impl_admw RS wfix_ind) 1, |
256 by (rtac (adm_impl_admw RS wfix_ind) 1); |
262 rtac adm_subst 1, |
257 by (rtac adm_subst 1); |
263 cont_tacR 1, |
258 by (cont_tacR 1); |
264 resolve_tac prems 1, |
259 by (resolve_tac prems 1); |
265 rtac allI 1, |
260 by (rtac allI 1); |
266 rtac (rewrite_rule [stream.take_def] stream_finite_ind2 RS spec) 1, |
261 by (rtac (rewrite_rule [stream.take_def] stream_finite_ind2 RS spec) 1); |
267 resolve_tac prems 1, |
262 by (resolve_tac prems 1); |
268 eresolve_tac prems 1, |
263 by (eresolve_tac prems 1); |
269 eresolve_tac prems 1, atac 1, atac 1]); |
264 by (eresolve_tac prems 1); |
|
265 by (atac 1); |
|
266 by (atac 1); |
|
267 qed "stream_ind2"; |
270 |
268 |
271 |
269 |
272 (* ----------------------------------------------------------------------- *) |
270 (* ----------------------------------------------------------------------- *) |
273 (* simplify use of coinduction *) |
271 (* simplify use of coinduction *) |
274 (* ----------------------------------------------------------------------- *) |
272 (* ----------------------------------------------------------------------- *) |
275 |
273 |
276 section "coinduction"; |
274 section "coinduction"; |
277 |
275 |
278 qed_goalw "stream_coind_lemma2" thy [stream.bisim_def] |
276 |
279 "!s1 s2. R s1 s2 --> ft`s1 = ft`s2 & R (rt`s1) (rt`s2) ==> stream_bisim R" |
277 Goalw [stream.bisim_def] |
280 (fn prems => |
278 "!s1 s2. R s1 s2 --> ft`s1 = ft`s2 & R (rt`s1) (rt`s2) ==> stream_bisim R"; |
281 [ |
279 by (strip_tac 1); |
282 (cut_facts_tac prems 1), |
280 by (etac allE 1); |
283 (strip_tac 1), |
281 by (etac allE 1); |
284 (etac allE 1), |
282 by (dtac mp 1); |
285 (etac allE 1), |
283 by (atac 1); |
286 (dtac mp 1), |
284 by (etac conjE 1); |
287 (atac 1), |
285 by (case_tac "x = UU & x' = UU" 1); |
288 (etac conjE 1), |
286 by (rtac disjI1 1); |
289 (case_tac "x = UU & x' = UU" 1), |
287 by (Blast_tac 1); |
290 (rtac disjI1 1), |
288 by (rtac disjI2 1); |
291 (fast_tac HOL_cs 1), |
289 by (rtac disjE 1); |
292 (rtac disjI2 1), |
290 by (etac (de_Morgan_conj RS subst) 1); |
293 (rtac disjE 1), |
291 by (res_inst_tac [("x","ft`x")] exI 1); |
294 (etac (de_Morgan_conj RS subst) 1), |
292 by (res_inst_tac [("x","rt`x")] exI 1); |
295 (res_inst_tac [("x","ft`x")] exI 1), |
293 by (res_inst_tac [("x","rt`x'")] exI 1); |
296 (res_inst_tac [("x","rt`x")] exI 1), |
294 by (rtac conjI 1); |
297 (res_inst_tac [("x","rt`x'")] exI 1), |
295 by (etac ft_defin 1); |
298 (rtac conjI 1), |
296 by (asm_simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1); |
299 (etac ft_defin 1), |
297 by (eres_inst_tac [("s","ft`x"),("t","ft`x'")] subst 1); |
300 (asm_simp_tac (HOLCF_ss addsimps stream.rews addsimps [surjectiv_scons]) 1), |
298 by (simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1); |
301 (eres_inst_tac [("s","ft`x"),("t","ft`x'")] subst 1), |
299 by (res_inst_tac [("x","ft`x'")] exI 1); |
302 (simp_tac (HOLCF_ss addsimps stream.rews addsimps [surjectiv_scons]) 1), |
300 by (res_inst_tac [("x","rt`x")] exI 1); |
303 (res_inst_tac [("x","ft`x'")] exI 1), |
301 by (res_inst_tac [("x","rt`x'")] exI 1); |
304 (res_inst_tac [("x","rt`x")] exI 1), |
302 by (rtac conjI 1); |
305 (res_inst_tac [("x","rt`x'")] exI 1), |
303 by (etac ft_defin 1); |
306 (rtac conjI 1), |
304 by (asm_simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1); |
307 (etac ft_defin 1), |
305 by (res_inst_tac [("s","ft`x"),("t","ft`x'")] ssubst 1); |
308 (asm_simp_tac (HOLCF_ss addsimps stream.rews addsimps [surjectiv_scons]) 1), |
306 by (etac sym 1); |
309 (res_inst_tac [("s","ft`x"),("t","ft`x'")] ssubst 1), |
307 by (simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1); |
310 (etac sym 1), |
308 qed "stream_coind_lemma2"; |
311 (simp_tac (HOLCF_ss addsimps stream.rews addsimps [surjectiv_scons]) 1) |
|
312 ]); |
|
313 |
309 |
314 (* ----------------------------------------------------------------------- *) |
310 (* ----------------------------------------------------------------------- *) |
315 (* theorems about stream_finite *) |
311 (* theorems about stream_finite *) |
316 (* ----------------------------------------------------------------------- *) |
312 (* ----------------------------------------------------------------------- *) |
317 |
313 |
318 section "stream_finite"; |
314 section "stream_finite"; |
319 |
315 |
320 qed_goalw "stream_finite_UU" thy [stream.finite_def] "stream_finite UU" |
316 |
321 (fn prems => [ |
317 Goalw [stream.finite_def] "stream_finite UU"; |
322 (rtac exI 1), |
318 by (rtac exI 1); |
323 (simp_tac (HOLCF_ss addsimps stream.rews) 1)]); |
319 by (simp_tac (simpset() addsimps stream.rews) 1); |
324 |
320 qed "stream_finite_UU"; |
325 qed_goal "stream_finite_UU_rev" thy "~ stream_finite s ==> s ~= UU" (fn prems => |
321 |
326 [ |
322 Goal "~ stream_finite s ==> s ~= UU"; |
327 (cut_facts_tac prems 1), |
323 by (blast_tac (claset() addIs [stream_finite_UU]) 1); |
328 (etac contrapos 1), |
324 qed "stream_finite_UU_rev"; |
329 (hyp_subst_tac 1), |
325 |
330 (rtac stream_finite_UU 1) |
326 Goalw [stream.finite_def] "stream_finite xs ==> stream_finite (x && xs)"; |
331 ]); |
327 by (blast_tac (claset() addIs [stream_take_lemma4]) 1); |
332 |
328 qed "stream_finite_lemma1"; |
333 qed_goalw "stream_finite_lemma1" thy [stream.finite_def] |
329 |
334 "stream_finite xs ==> stream_finite (x && xs)" (fn prems => [ |
330 Goalw [stream.finite_def] |
335 (cut_facts_tac prems 1), |
331 "[| x ~= UU; stream_finite (x && xs) |] ==> stream_finite xs"; |
336 (etac exE 1), |
332 by (blast_tac (claset() addIs [stream_take_lemma3]) 1); |
337 (rtac exI 1), |
333 qed "stream_finite_lemma2"; |
338 (etac stream_take_lemma4 1) |
334 |
339 ]); |
335 Goal "stream_finite (rt`s) = stream_finite s"; |
340 |
336 by (stream_case_tac "s" 1); |
341 qed_goalw "stream_finite_lemma2" thy [stream.finite_def] |
337 by (simp_tac (simpset() addsimps [stream_finite_UU]) 1); |
342 "[| x ~= UU; stream_finite (x && xs) |] ==> stream_finite xs" (fn prems => |
338 by (Asm_simp_tac 1); |
343 [ |
339 by (fast_tac (claset() addIs [stream_finite_lemma1] |
344 (cut_facts_tac prems 1), |
340 addDs [stream_finite_lemma2]) 1); |
345 (etac exE 1), |
341 qed "stream_finite_rt_eq"; |
346 (rtac exI 1), |
342 |
347 (etac stream_take_lemma3 1), |
343 Goal "stream_finite s ==> !t. t<<s --> stream_finite t"; |
348 (atac 1) |
344 by (eres_inst_tac [("x","s")] stream_finite_ind 1); |
349 ]); |
345 by (strip_tac 1); |
350 |
346 by (dtac UU_I 1); |
351 qed_goal "stream_finite_rt_eq" thy "stream_finite (rt`s) = stream_finite s" |
347 by (asm_simp_tac (simpset() addsimps [stream_finite_UU]) 1); |
352 (fn _ => [ |
348 by (strip_tac 1); |
353 stream_case_tac "s" 1, |
349 by (asm_full_simp_tac (simpset() addsimps [stream_prefix']) 1); |
354 simp_tac (HOL_ss addsimps stream_finite_UU::stream.sel_rews) 1, |
350 by (fast_tac (claset() addSIs [stream_finite_UU, stream_finite_lemma1]) 1); |
355 asm_simp_tac (HOL_ss addsimps stream.sel_rews) 1, |
351 qed_spec_mp "stream_finite_less"; |
356 fast_tac (HOL_cs addIs [stream_finite_lemma1] |
352 |
357 addDs [stream_finite_lemma2]) 1]); |
353 Goal "adm (%x. ~ stream_finite x)"; |
358 |
354 by (rtac admI2 1); |
359 qed_goal_spec_mp "stream_finite_less" thy |
355 by (best_tac (claset() addIs [stream_finite_less, is_ub_thelub]) 1); |
360 "stream_finite s ==> !t. t<<s --> stream_finite t" (fn prems => [ |
356 qed "adm_not_stream_finite"; |
361 cut_facts_tac prems 1, |
|
362 eres_inst_tac [("x","s")] stream_finite_ind 1, |
|
363 strip_tac 1, dtac UU_I 1, |
|
364 asm_simp_tac (HOLCF_ss addsimps [stream_finite_UU]) 1, |
|
365 strip_tac 1, |
|
366 asm_full_simp_tac (HOL_ss addsimps [stream_prefix']) 1, |
|
367 fast_tac (HOL_cs addSIs [stream_finite_UU, stream_finite_lemma1]) 1]); |
|
368 |
|
369 qed_goal "adm_not_stream_finite" thy "adm (%x. ~ stream_finite x)" (fn _ => [ |
|
370 rtac admI2 1, |
|
371 dtac spec 1, |
|
372 etac contrapos 1, |
|
373 dtac stream_finite_less 1, |
|
374 etac is_ub_thelub 1, |
|
375 atac 1]); |
|