|
1 (* Title: HOLCF/FOCUS/Fstream.ML |
|
2 ID: $ $ |
|
3 Author: David von Oheimb, TU Muenchen |
|
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 *) |
|
6 |
|
7 Goal "a = Def d \\<Longrightarrow> a\\<sqsubseteq>b \\<Longrightarrow> b = Def d"; |
|
8 by (rtac (flat_eq RS iffD1 RS sym) 1); |
|
9 by (rtac Def_not_UU 1); |
|
10 by (dtac antisym_less_inverse 1); |
|
11 by (eatac (conjunct2 RS trans_less) 1 1); |
|
12 qed "Def_maximal"; |
|
13 |
|
14 |
|
15 section "fscons"; |
|
16 |
|
17 Goalw [fscons_def] "a~>s = Def a && s"; |
|
18 by (Simp_tac 1); |
|
19 qed "fscons_def2"; |
|
20 |
|
21 qed_goal "fstream_exhaust" thy "x = UU | (? a y. x = a~> y)" (fn _ => [ |
|
22 simp_tac (simpset() addsimps [fscons_def2]) 1, |
|
23 cut_facts_tac [stream.exhaust] 1, |
|
24 fast_tac (claset() addDs [not_Undef_is_Def RS iffD1]) 1]); |
|
25 |
|
26 qed_goal "fstream_cases" thy "[| x = UU ==> P; !!a y. x = a~> y ==> P |] ==> P" |
|
27 (fn prems => [ |
|
28 cut_facts_tac [fstream_exhaust] 1, |
|
29 etac disjE 1, |
|
30 eresolve_tac prems 1, |
|
31 REPEAT(etac exE 1), |
|
32 eresolve_tac prems 1]); |
|
33 |
|
34 fun fstream_case_tac s i = res_inst_tac [("x",s)] fstream_cases i |
|
35 THEN hyp_subst_tac i THEN hyp_subst_tac (i+1); |
|
36 |
|
37 qed_goal "fstream_exhaust_eq" thy "x ~= UU = (? a y. x = a~> y)" (fn _ => [ |
|
38 simp_tac(simpset() addsimps [fscons_def2,stream_exhaust_eq]) 1, |
|
39 fast_tac (claset() addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]); |
|
40 |
|
41 |
|
42 qed_goal "fscons_not_empty" thy "a~> s ~= <>" (fn _ => [ |
|
43 stac fscons_def2 1, |
|
44 Simp_tac 1]); |
|
45 Addsimps[fscons_not_empty]; |
|
46 |
|
47 |
|
48 qed_goal "fscons_inject" thy "(a~> s = b~> t) = (a = b & s = t)" (fn _ => [ |
|
49 simp_tac (HOL_ss addsimps [fscons_def2]) 1, |
|
50 stac (hd lift.inject RS sym) 1, (*2*back();*) |
|
51 Simp_tac 1]); |
|
52 Addsimps[fscons_inject]; |
|
53 |
|
54 qed_goal "fstream_prefix" thy "a~> s << t ==> ? tt. t = a~> tt & s << tt" (fn prems =>[ |
|
55 cut_facts_tac prems 1, |
|
56 stream_case_tac "t" 1, |
|
57 cut_facts_tac [fscons_not_empty] 1, |
|
58 fast_tac (HOL_cs addDs [eq_UU_iff RS iffD2]) 1, |
|
59 asm_full_simp_tac (HOL_ss addsimps [fscons_def2]) 1, |
|
60 dtac stream_flat_prefix 1, |
|
61 rtac Def_not_UU 1, |
|
62 fast_tac HOL_cs 1]); |
|
63 |
|
64 qed_goal "fstream_prefix'" thy |
|
65 "x << a~> z = (x = <> | (? y. x = a~> y & y << z))" (fn _ => [ |
|
66 simp_tac(HOL_ss addsimps [fscons_def2, Def_not_UU RS stream_prefix'])1, |
|
67 Step_tac 1, |
|
68 ALLGOALS(etac swap), |
|
69 fast_tac (HOL_cs addIs [refl_less] addEs [DefE]) 2, |
|
70 rtac Lift_cases 1, |
|
71 contr_tac 1, |
|
72 Step_tac 1, |
|
73 dtac (Def_inject_less_eq RS iffD1) 1, |
|
74 Fast_tac 1]); |
|
75 Addsimps[fstream_prefix']; |
|
76 |
|
77 (* ------------------------------------------------------------------------- *) |
|
78 |
|
79 section "ft & rt"; |
|
80 |
|
81 bind_thm("ft_empty",hd stream.sel_rews); |
|
82 qed_goalw "ft_fscons" thy [fscons_def] "ft\\<cdot>(m~> s) = Def m" (fn _ => [ |
|
83 (Simp_tac 1)]); |
|
84 Addsimps[ft_fscons]; |
|
85 |
|
86 bind_thm("rt_empty",hd (tl stream.sel_rews)); |
|
87 qed_goalw "rt_fscons" thy [fscons_def] "rt\\<cdot>(m~> s) = s" (fn _ => [ |
|
88 (Simp_tac 1)]); |
|
89 Addsimps[rt_fscons]; |
|
90 |
|
91 qed_goalw "ft_eq" thy [fscons_def] "(ft\\<cdot>s = Def a) = (? t. s = a~> t)" (K [ |
|
92 Simp_tac 1, |
|
93 Safe_tac, |
|
94 etac subst 1, |
|
95 rtac exI 1, |
|
96 rtac (surjectiv_scons RS sym) 1, |
|
97 Simp_tac 1]); |
|
98 Addsimps[ft_eq]; |
|
99 |
|
100 Goal "(d\\<leadsto>y = x) = (ft\\<cdot>x = Def d & rt\\<cdot>x = y)"; |
|
101 by Auto_tac; |
|
102 qed "surjective_fscons_lemma"; |
|
103 Goal "ft\\<cdot>x = Def d \\<Longrightarrow> d\\<leadsto>rt\\<cdot>x = x"; |
|
104 by (asm_simp_tac (simpset() addsimps [surjective_fscons_lemma]) 1); |
|
105 qed "surjective_fscons"; |
|
106 |
|
107 |
|
108 (* ------------------------------------------------------------------------- *) |
|
109 |
|
110 section "take"; |
|
111 |
|
112 qed_goalw "fstream_take_Suc" thy [fscons_def] |
|
113 "stream_take (Suc n)\\<cdot>(a~> s) = a~> stream_take n\\<cdot>s" (K [ |
|
114 Simp_tac 1]); |
|
115 Addsimps[fstream_take_Suc]; |
|
116 |
|
117 |
|
118 (* ------------------------------------------------------------------------- *) |
|
119 |
|
120 section "slen"; |
|
121 |
|
122 (*bind_thm("slen_empty", slen_empty);*) |
|
123 |
|
124 qed_goalw "slen_fscons" thy [fscons_def] "#(m~> s) = iSuc (#s)" (fn _ => [ |
|
125 (Simp_tac 1)]); |
|
126 |
|
127 qed_goal "slen_fscons_eq" thy |
|
128 "Fin (Suc n) < #x = (? a y. x = a~> y & Fin n < #y)" (fn _ => [ |
|
129 simp_tac (HOL_ss addsimps [fscons_def2, slen_scons_eq]) 1, |
|
130 fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]); |
|
131 |
|
132 qed_goal "slen_fscons_eq_rev" thy |
|
133 "#x < Fin (Suc (Suc n)) = (!a y. x ~= a~> y | #y < Fin (Suc n))" (K [ |
|
134 simp_tac (HOL_ss addsimps [fscons_def2, slen_scons_eq_rev]) 1, |
|
135 step_tac (HOL_cs addSEs [DefE]) 1, |
|
136 step_tac (HOL_cs addSEs [DefE]) 1, |
|
137 step_tac (HOL_cs addSEs [DefE]) 1, |
|
138 step_tac (HOL_cs addSEs [DefE]) 1, |
|
139 step_tac (HOL_cs addSEs [DefE]) 1, |
|
140 step_tac (HOL_cs addSEs [DefE]) 1, |
|
141 etac swap 1, |
|
142 fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]); |
|
143 |
|
144 qed_goal "slen_fscons_less_eq" thy |
|
145 "#(a~> y) < Fin (Suc (Suc n)) = (#y < Fin (Suc n))" (fn _ => [ |
|
146 stac slen_fscons_eq_rev 1, |
|
147 fast_tac (HOL_cs addSDs [fscons_inject RS iffD1]) 1]); |
|
148 |
|
149 |
|
150 (* ------------------------------------------------------------------------- *) |
|
151 |
|
152 section "induction"; |
|
153 |
|
154 qed_goal "fstream_ind" thy |
|
155 "[| adm P; P <>; !!a s. P s ==> P (a~> s) |] ==> P x" (fn prems => [ |
|
156 cut_facts_tac prems 1, |
|
157 etac stream.ind 1, |
|
158 atac 1, |
|
159 fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] |
|
160 addEs (tl (tl prems) RL [fscons_def2 RS subst])) 1]); |
|
161 |
|
162 qed_goal "fstream_ind2" thy |
|
163 "[| adm P; P UU; !!a. P (a~> UU); !!a b s. P s ==> P (a~> b~> s) |] ==> P x" (fn prems => [ |
|
164 cut_facts_tac prems 1, |
|
165 etac stream_ind2 1, |
|
166 atac 1, |
|
167 fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] |
|
168 addIs ([hd(tl(tl prems))]RL[fscons_def2 RS subst]))1, |
|
169 fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] |
|
170 addEs [hd(tl(tl(tl prems))RL[fscons_def2 RS subst] |
|
171 RL[fscons_def2 RS subst])])1]); |
|
172 |
|
173 |
|
174 (* ------------------------------------------------------------------------- *) |
|
175 |
|
176 section "fsfilter"; |
|
177 |
|
178 qed_goalw "fsfilter_empty" thy [fsfilter_def] "A(C)UU = UU" (fn _ => [ |
|
179 rtac sfilter_empty 1]); |
|
180 |
|
181 qed_goalw "fsfilter_fscons" thy [fsfilter_def] |
|
182 "A(C)x~> xs = (if x:A then x~> (A(C)xs) else A(C)xs)" (fn _ => [ |
|
183 simp_tac (simpset() addsimps [fscons_def2,sfilter_scons,If_and_if]) 1]); |
|
184 |
|
185 qed_goal "fsfilter_emptys" thy "{}(C)x = UU" (fn _ => [ |
|
186 res_inst_tac [("x","x")] fstream_ind 1, |
|
187 resolve_tac adm_lemmas 1, |
|
188 cont_tacR 1, |
|
189 rtac fsfilter_empty 1, |
|
190 asm_simp_tac (simpset()addsimps [fsfilter_fscons]) 1]); |
|
191 |
|
192 qed_goal "fsfilter_insert" thy "(insert a A)(C)a~> x = a~> ((insert a A)(C)x)" (fn _=> [ |
|
193 simp_tac (simpset() addsimps [fsfilter_fscons]) 1]); |
|
194 |
|
195 qed_goal "fsfilter_single_in" thy "{a}(C)a~> x = a~> ({a}(C)x)" (fn _=> [ |
|
196 rtac fsfilter_insert 1]); |
|
197 |
|
198 qed_goal "fsfilter_single_out" thy "b ~= a ==> {a}(C)b~> x = ({a}(C)x)" (fn prems => [ |
|
199 cut_facts_tac prems 1, |
|
200 asm_simp_tac (simpset() addsimps[fsfilter_fscons]) 1]); |
|
201 |
|
202 Goal "\\<lbrakk>chain Y; lub (range Y) = a\\<leadsto>s\\<rbrakk> \\<Longrightarrow> \\<exists>j t. Y j = a\\<leadsto>t"; |
|
203 by (case_tac "max_in_chain i Y" 1); |
|
204 by (datac (lub_finch1 RS thelubI RS sym) 1 1); |
|
205 by (Force_tac 1); |
|
206 by (rewtac max_in_chain_def); |
|
207 by Auto_tac; |
|
208 by (fatac chain_mono3 1 1); |
|
209 by (res_inst_tac [("x","Y j")] fstream_cases 1); |
|
210 by (Force_tac 1); |
|
211 by (dres_inst_tac [("x","j")] is_ub_thelub 1); |
|
212 by (Force_tac 1); |
|
213 qed "fstream_lub_lemma1"; |
|
214 |
|
215 Goal "\\<lbrakk>chain Y; lub (range Y) = a\\<leadsto>s\\<rbrakk> \\<Longrightarrow> (\\<exists>j t. Y j = a\\<leadsto>t) & (\\<exists>X. chain X & (!i. ? j. Y j = a\\<leadsto>X i) & lub (range X) = s)"; |
|
216 by (fatac fstream_lub_lemma1 1 1); |
|
217 by (Clarsimp_tac 1); |
|
218 by (res_inst_tac [("x","%i. rt\\<cdot>(Y(i+j))")] exI 1); |
|
219 by (rtac conjI 1); |
|
220 by (etac (chain_shift RS chain_monofun) 1); |
|
221 by Safe_tac; |
|
222 by (dres_inst_tac [("x","j"),("y","i+j")] chain_mono3 1); |
|
223 by (Simp_tac 1); |
|
224 by (Asm_full_simp_tac 1); |
|
225 by (res_inst_tac [("x","i+j")] exI 1); |
|
226 by (dtac fstream_prefix 1); |
|
227 by (Clarsimp_tac 1); |
|
228 by (stac (contlub_cfun RS sym) 1); |
|
229 by (rtac chainI 1); |
|
230 by (Fast_tac 1); |
|
231 by (etac chain_shift 1); |
|
232 by (stac (lub_const RS thelubI) 1); |
|
233 by (stac lub_range_shift 1); |
|
234 by (atac 1); |
|
235 by (Asm_simp_tac 1); |
|
236 qed "fstream_lub_lemma"; |
|
237 |
|
238 |