author | wenzelm |
Thu, 22 Apr 2004 10:52:32 +0200 | |
changeset 14643 | 130076a81b84 |
parent 12218 | 6597093b77e7 |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOLCF/IOA/meta_theory/Sequence.ML |
3275 | 2 |
ID: $Id$ |
12218 | 3 |
Author: Olaf Müller |
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
3071 | 5 |
|
12218 | 6 |
Theorems about Sequences over flat domains with lifted elements. |
3071 | 7 |
*) |
8 |
||
3656 | 9 |
|
3071 | 10 |
Addsimps [andalso_and,andalso_or]; |
11 |
||
12 |
(* ----------------------------------------------------------------------------------- *) |
|
13 |
||
14 |
section "recursive equations of operators"; |
|
15 |
||
16 |
(* ---------------------------------------------------------------- *) |
|
17 |
(* Map *) |
|
18 |
(* ---------------------------------------------------------------- *) |
|
19 |
||
10835 | 20 |
Goal "Map f$UU =UU"; |
4098 | 21 |
by (simp_tac (simpset() addsimps [Map_def]) 1); |
3071 | 22 |
qed"Map_UU"; |
23 |
||
10835 | 24 |
Goal "Map f$nil =nil"; |
4098 | 25 |
by (simp_tac (simpset() addsimps [Map_def]) 1); |
3071 | 26 |
qed"Map_nil"; |
27 |
||
10835 | 28 |
Goal "Map f$(x>>xs)=(f x) >> Map f$xs"; |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
29 |
by (simp_tac (simpset() addsimps [Map_def, Consq_def,flift2_def]) 1); |
3071 | 30 |
qed"Map_cons"; |
31 |
||
32 |
(* ---------------------------------------------------------------- *) |
|
33 |
(* Filter *) |
|
34 |
(* ---------------------------------------------------------------- *) |
|
35 |
||
10835 | 36 |
Goal "Filter P$UU =UU"; |
4098 | 37 |
by (simp_tac (simpset() addsimps [Filter_def]) 1); |
3071 | 38 |
qed"Filter_UU"; |
39 |
||
10835 | 40 |
Goal "Filter P$nil =nil"; |
4098 | 41 |
by (simp_tac (simpset() addsimps [Filter_def]) 1); |
3071 | 42 |
qed"Filter_nil"; |
43 |
||
10835 | 44 |
Goal "Filter P$(x>>xs)= (if P x then x>>(Filter P$xs) else Filter P$xs)"; |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
45 |
by (simp_tac (simpset() addsimps [Filter_def, Consq_def,flift2_def,If_and_if]) 1); |
3071 | 46 |
qed"Filter_cons"; |
47 |
||
48 |
(* ---------------------------------------------------------------- *) |
|
49 |
(* Forall *) |
|
50 |
(* ---------------------------------------------------------------- *) |
|
51 |
||
5068 | 52 |
Goal "Forall P UU"; |
4098 | 53 |
by (simp_tac (simpset() addsimps [Forall_def,sforall_def]) 1); |
3071 | 54 |
qed"Forall_UU"; |
55 |
||
5068 | 56 |
Goal "Forall P nil"; |
4098 | 57 |
by (simp_tac (simpset() addsimps [Forall_def,sforall_def]) 1); |
3071 | 58 |
qed"Forall_nil"; |
59 |
||
5068 | 60 |
Goal "Forall P (x>>xs)= (P x & Forall P xs)"; |
4098 | 61 |
by (simp_tac (simpset() addsimps [Forall_def, sforall_def, |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
62 |
Consq_def,flift2_def]) 1); |
3071 | 63 |
qed"Forall_cons"; |
64 |
||
65 |
(* ---------------------------------------------------------------- *) |
|
66 |
(* Conc *) |
|
67 |
(* ---------------------------------------------------------------- *) |
|
68 |
||
69 |
||
5068 | 70 |
Goal "(x>>xs) @@ y = x>>(xs @@y)"; |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
71 |
by (simp_tac (simpset() addsimps [Consq_def]) 1); |
3071 | 72 |
qed"Conc_cons"; |
73 |
||
74 |
(* ---------------------------------------------------------------- *) |
|
75 |
(* Takewhile *) |
|
76 |
(* ---------------------------------------------------------------- *) |
|
77 |
||
10835 | 78 |
Goal "Takewhile P$UU =UU"; |
4098 | 79 |
by (simp_tac (simpset() addsimps [Takewhile_def]) 1); |
3071 | 80 |
qed"Takewhile_UU"; |
81 |
||
10835 | 82 |
Goal "Takewhile P$nil =nil"; |
4098 | 83 |
by (simp_tac (simpset() addsimps [Takewhile_def]) 1); |
3071 | 84 |
qed"Takewhile_nil"; |
85 |
||
10835 | 86 |
Goal "Takewhile P$(x>>xs)= (if P x then x>>(Takewhile P$xs) else nil)"; |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
87 |
by (simp_tac (simpset() addsimps [Takewhile_def, Consq_def,flift2_def,If_and_if]) 1); |
3071 | 88 |
qed"Takewhile_cons"; |
89 |
||
90 |
(* ---------------------------------------------------------------- *) |
|
91 |
(* Dropwhile *) |
|
92 |
(* ---------------------------------------------------------------- *) |
|
93 |
||
10835 | 94 |
Goal "Dropwhile P$UU =UU"; |
4098 | 95 |
by (simp_tac (simpset() addsimps [Dropwhile_def]) 1); |
3071 | 96 |
qed"Dropwhile_UU"; |
97 |
||
10835 | 98 |
Goal "Dropwhile P$nil =nil"; |
4098 | 99 |
by (simp_tac (simpset() addsimps [Dropwhile_def]) 1); |
3071 | 100 |
qed"Dropwhile_nil"; |
101 |
||
10835 | 102 |
Goal "Dropwhile P$(x>>xs)= (if P x then Dropwhile P$xs else x>>xs)"; |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
103 |
by (simp_tac (simpset() addsimps [Dropwhile_def, Consq_def,flift2_def,If_and_if]) 1); |
3071 | 104 |
qed"Dropwhile_cons"; |
105 |
||
106 |
(* ---------------------------------------------------------------- *) |
|
107 |
(* Last *) |
|
108 |
(* ---------------------------------------------------------------- *) |
|
109 |
||
110 |
||
10835 | 111 |
Goal "Last$UU =UU"; |
4098 | 112 |
by (simp_tac (simpset() addsimps [Last_def]) 1); |
3071 | 113 |
qed"Last_UU"; |
114 |
||
10835 | 115 |
Goal "Last$nil =UU"; |
4098 | 116 |
by (simp_tac (simpset() addsimps [Last_def]) 1); |
3071 | 117 |
qed"Last_nil"; |
118 |
||
10835 | 119 |
Goal "Last$(x>>xs)= (if xs=nil then Def x else Last$xs)"; |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
120 |
by (simp_tac (simpset() addsimps [Last_def, Consq_def]) 1); |
4042 | 121 |
by (res_inst_tac [("x","xs")] seq.casedist 1); |
4833 | 122 |
by (Asm_simp_tac 1); |
3071 | 123 |
by (REPEAT (Asm_simp_tac 1)); |
124 |
qed"Last_cons"; |
|
125 |
||
126 |
||
127 |
(* ---------------------------------------------------------------- *) |
|
128 |
(* Flat *) |
|
129 |
(* ---------------------------------------------------------------- *) |
|
130 |
||
10835 | 131 |
Goal "Flat$UU =UU"; |
4098 | 132 |
by (simp_tac (simpset() addsimps [Flat_def]) 1); |
3071 | 133 |
qed"Flat_UU"; |
134 |
||
10835 | 135 |
Goal "Flat$nil =nil"; |
4098 | 136 |
by (simp_tac (simpset() addsimps [Flat_def]) 1); |
3071 | 137 |
qed"Flat_nil"; |
138 |
||
10835 | 139 |
Goal "Flat$(x##xs)= x @@ (Flat$xs)"; |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
140 |
by (simp_tac (simpset() addsimps [Flat_def, Consq_def]) 1); |
3071 | 141 |
qed"Flat_cons"; |
142 |
||
143 |
||
144 |
(* ---------------------------------------------------------------- *) |
|
145 |
(* Zip *) |
|
146 |
(* ---------------------------------------------------------------- *) |
|
147 |
||
5068 | 148 |
Goal "Zip = (LAM t1 t2. case t1 of \ |
3071 | 149 |
\ nil => nil \ |
150 |
\ | x##xs => (case t2 of \ |
|
151 |
\ nil => UU \ |
|
152 |
\ | y##ys => (case x of \ |
|
12028 | 153 |
\ UU => UU \ |
3071 | 154 |
\ | Def a => (case y of \ |
12028 | 155 |
\ UU => UU \ |
10835 | 156 |
\ | Def b => Def (a,b)##(Zip$xs$ys)))))"; |
3071 | 157 |
by (rtac trans 1); |
3457 | 158 |
by (rtac fix_eq2 1); |
159 |
by (rtac Zip_def 1); |
|
160 |
by (rtac beta_cfun 1); |
|
3071 | 161 |
by (Simp_tac 1); |
162 |
qed"Zip_unfold"; |
|
163 |
||
10835 | 164 |
Goal "Zip$UU$y =UU"; |
3071 | 165 |
by (stac Zip_unfold 1); |
166 |
by (Simp_tac 1); |
|
167 |
qed"Zip_UU1"; |
|
168 |
||
10835 | 169 |
Goal "x~=nil ==> Zip$x$UU =UU"; |
3071 | 170 |
by (stac Zip_unfold 1); |
171 |
by (Simp_tac 1); |
|
4042 | 172 |
by (res_inst_tac [("x","x")] seq.casedist 1); |
3071 | 173 |
by (REPEAT (Asm_full_simp_tac 1)); |
174 |
qed"Zip_UU2"; |
|
175 |
||
10835 | 176 |
Goal "Zip$nil$y =nil"; |
3071 | 177 |
by (stac Zip_unfold 1); |
178 |
by (Simp_tac 1); |
|
179 |
qed"Zip_nil"; |
|
180 |
||
10835 | 181 |
Goal "Zip$(x>>xs)$nil= UU"; |
3071 | 182 |
by (stac Zip_unfold 1); |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
183 |
by (simp_tac (simpset() addsimps [Consq_def]) 1); |
3071 | 184 |
qed"Zip_cons_nil"; |
185 |
||
10835 | 186 |
Goal "Zip$(x>>xs)$(y>>ys)= (x,y) >> Zip$xs$ys"; |
3457 | 187 |
by (rtac trans 1); |
3071 | 188 |
by (stac Zip_unfold 1); |
189 |
by (Simp_tac 1); |
|
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
190 |
by (simp_tac (simpset() addsimps [Consq_def]) 1); |
3071 | 191 |
qed"Zip_cons"; |
192 |
||
193 |
||
194 |
Delsimps [sfilter_UU,sfilter_nil,sfilter_cons, |
|
195 |
smap_UU,smap_nil,smap_cons, |
|
196 |
sforall2_UU,sforall2_nil,sforall2_cons, |
|
197 |
slast_UU,slast_nil,slast_cons, |
|
198 |
stakewhile_UU, stakewhile_nil, stakewhile_cons, |
|
199 |
sdropwhile_UU, sdropwhile_nil, sdropwhile_cons, |
|
200 |
sflat_UU,sflat_nil,sflat_cons, |
|
201 |
szip_UU1,szip_UU2,szip_nil,szip_cons_nil,szip_cons]; |
|
202 |
||
203 |
||
204 |
Addsimps [Filter_UU,Filter_nil,Filter_cons, |
|
205 |
Map_UU,Map_nil,Map_cons, |
|
206 |
Forall_UU,Forall_nil,Forall_cons, |
|
207 |
Last_UU,Last_nil,Last_cons, |
|
3275 | 208 |
Conc_cons, |
3071 | 209 |
Takewhile_UU, Takewhile_nil, Takewhile_cons, |
210 |
Dropwhile_UU, Dropwhile_nil, Dropwhile_cons, |
|
211 |
Zip_UU1,Zip_UU2,Zip_nil,Zip_cons_nil,Zip_cons]; |
|
212 |
||
213 |
||
214 |
||
215 |
(* ------------------------------------------------------------------------------------- *) |
|
216 |
||
217 |
||
218 |
section "Cons"; |
|
219 |
||
5068 | 220 |
Goal "a>>s = (Def a)##s"; |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
221 |
by (simp_tac (simpset() addsimps [Consq_def]) 1); |
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
222 |
qed"Consq_def2"; |
3071 | 223 |
|
5068 | 224 |
Goal "x = UU | x = nil | (? a s. x = a >> s)"; |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
225 |
by (simp_tac (simpset() addsimps [Consq_def2]) 1); |
3071 | 226 |
by (cut_facts_tac [seq.exhaust] 1); |
227 |
by (fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1]) 1); |
|
228 |
qed"Seq_exhaust"; |
|
229 |
||
230 |
||
5068 | 231 |
Goal "!!P. [| x = UU ==> P; x = nil ==> P; !!a s. x = a >> s ==> P |] ==> P"; |
3071 | 232 |
by (cut_inst_tac [("x","x")] Seq_exhaust 1); |
3457 | 233 |
by (etac disjE 1); |
3071 | 234 |
by (Asm_full_simp_tac 1); |
3457 | 235 |
by (etac disjE 1); |
3071 | 236 |
by (Asm_full_simp_tac 1); |
237 |
by (REPEAT (etac exE 1)); |
|
238 |
by (Asm_full_simp_tac 1); |
|
239 |
qed"Seq_cases"; |
|
240 |
||
241 |
fun Seq_case_tac s i = res_inst_tac [("x",s)] Seq_cases i |
|
242 |
THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2); |
|
243 |
||
244 |
(* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *) |
|
245 |
fun Seq_case_simp_tac s i = Seq_case_tac s i THEN Asm_simp_tac (i+2) |
|
246 |
THEN Asm_full_simp_tac (i+1) |
|
247 |
THEN Asm_full_simp_tac i; |
|
248 |
||
5068 | 249 |
Goal "a>>s ~= UU"; |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
250 |
by (stac Consq_def2 1); |
3071 | 251 |
by (resolve_tac seq.con_rews 1); |
3457 | 252 |
by (rtac Def_not_UU 1); |
3071 | 253 |
qed"Cons_not_UU"; |
254 |
||
3275 | 255 |
|
5068 | 256 |
Goal "~(a>>x) << UU"; |
3071 | 257 |
by (rtac notI 1); |
258 |
by (dtac antisym_less 1); |
|
259 |
by (Simp_tac 1); |
|
4098 | 260 |
by (asm_full_simp_tac (simpset() addsimps [Cons_not_UU]) 1); |
3071 | 261 |
qed"Cons_not_less_UU"; |
262 |
||
5068 | 263 |
Goal "~a>>s << nil"; |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
264 |
by (stac Consq_def2 1); |
3071 | 265 |
by (resolve_tac seq.rews 1); |
3457 | 266 |
by (rtac Def_not_UU 1); |
3071 | 267 |
qed"Cons_not_less_nil"; |
268 |
||
5068 | 269 |
Goal "a>>s ~= nil"; |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
270 |
by (stac Consq_def2 1); |
3071 | 271 |
by (resolve_tac seq.rews 1); |
272 |
qed"Cons_not_nil"; |
|
273 |
||
5068 | 274 |
Goal "nil ~= a>>s"; |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
275 |
by (simp_tac (simpset() addsimps [Consq_def2]) 1); |
3275 | 276 |
qed"Cons_not_nil2"; |
277 |
||
5068 | 278 |
Goal "(a>>s = b>>t) = (a = b & s = t)"; |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
279 |
by (simp_tac (HOL_ss addsimps [Consq_def2]) 1); |
3071 | 280 |
by (stac (hd lift.inject RS sym) 1); |
281 |
back(); back(); |
|
282 |
by (rtac scons_inject_eq 1); |
|
283 |
by (REPEAT(rtac Def_not_UU 1)); |
|
284 |
qed"Cons_inject_eq"; |
|
285 |
||
5068 | 286 |
Goal "(a>>s<<b>>t) = (a = b & s<<t)"; |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
287 |
by (simp_tac (simpset() addsimps [Consq_def2]) 1); |
3071 | 288 |
by (stac (Def_inject_less_eq RS sym) 1); |
289 |
back(); |
|
290 |
by (rtac iffI 1); |
|
291 |
(* 1 *) |
|
292 |
by (etac (hd seq.inverts) 1); |
|
293 |
by (REPEAT(rtac Def_not_UU 1)); |
|
294 |
(* 2 *) |
|
295 |
by (Asm_full_simp_tac 1); |
|
296 |
by (etac conjE 1); |
|
297 |
by (etac monofun_cfun_arg 1); |
|
298 |
qed"Cons_inject_less_eq"; |
|
299 |
||
10835 | 300 |
Goal "seq_take (Suc n)$(a>>x) = a>> (seq_take n$x)"; |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
301 |
by (simp_tac (simpset() addsimps [Consq_def]) 1); |
3071 | 302 |
qed"seq_take_Cons"; |
303 |
||
3275 | 304 |
Addsimps [Cons_not_nil2,Cons_inject_eq,Cons_inject_less_eq,seq_take_Cons, |
3071 | 305 |
Cons_not_UU,Cons_not_less_UU,Cons_not_less_nil,Cons_not_nil]; |
306 |
||
3275 | 307 |
(* Instead of adding UU_neq_Cons every equation UU~=x could be changed to x~=UU *) |
5068 | 308 |
Goal "UU ~= x>>xs"; |
3275 | 309 |
by (res_inst_tac [("s1","UU"),("t1","x>>xs")] (sym RS rev_contrapos) 1); |
310 |
by (REPEAT (Simp_tac 1)); |
|
311 |
qed"UU_neq_Cons"; |
|
312 |
||
313 |
Addsimps [UU_neq_Cons]; |
|
314 |
||
3071 | 315 |
|
316 |
(* ----------------------------------------------------------------------------------- *) |
|
317 |
||
318 |
section "induction"; |
|
319 |
||
5068 | 320 |
Goal "!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a>>s)|] ==> P x"; |
3457 | 321 |
by (etac seq.ind 1); |
3071 | 322 |
by (REPEAT (atac 1)); |
323 |
by (def_tac 1); |
|
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
324 |
by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1); |
3071 | 325 |
qed"Seq_induct"; |
326 |
||
5068 | 327 |
Goal "!! P.[|P UU;P nil; !! a s. P s ==> P(a>>s) |] \ |
3071 | 328 |
\ ==> seq_finite x --> P x"; |
3457 | 329 |
by (etac seq_finite_ind 1); |
3071 | 330 |
by (REPEAT (atac 1)); |
331 |
by (def_tac 1); |
|
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
332 |
by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1); |
3071 | 333 |
qed"Seq_FinitePartial_ind"; |
334 |
||
5068 | 335 |
Goal "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x"; |
3457 | 336 |
by (etac sfinite.induct 1); |
337 |
by (assume_tac 1); |
|
3071 | 338 |
by (def_tac 1); |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
339 |
by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1); |
3071 | 340 |
qed"Seq_Finite_ind"; |
341 |
||
342 |
||
343 |
(* rws are definitions to be unfolded for admissibility check *) |
|
344 |
fun Seq_induct_tac s rws i = res_inst_tac [("x",s)] Seq_induct i |
|
345 |
THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac (i+1)))) |
|
4098 | 346 |
THEN simp_tac (simpset() addsimps rws) i; |
3071 | 347 |
|
348 |
fun Seq_Finite_induct_tac i = etac Seq_Finite_ind i |
|
349 |
THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac i))); |
|
350 |
||
351 |
fun pair_tac s = res_inst_tac [("p",s)] PairE |
|
352 |
THEN' hyp_subst_tac THEN' Asm_full_simp_tac; |
|
353 |
||
354 |
(* induction on a sequence of pairs with pairsplitting and simplification *) |
|
355 |
fun pair_induct_tac s rws i = |
|
356 |
res_inst_tac [("x",s)] Seq_induct i |
|
357 |
THEN pair_tac "a" (i+3) |
|
358 |
THEN (REPEAT_DETERM (CHANGED (Simp_tac (i+1)))) |
|
4098 | 359 |
THEN simp_tac (simpset() addsimps rws) i; |
3071 | 360 |
|
361 |
||
362 |
||
363 |
(* ------------------------------------------------------------------------------------ *) |
|
364 |
||
365 |
section "HD,TL"; |
|
366 |
||
10835 | 367 |
Goal "HD$(x>>y) = Def x"; |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
368 |
by (simp_tac (simpset() addsimps [Consq_def]) 1); |
3071 | 369 |
qed"HD_Cons"; |
370 |
||
10835 | 371 |
Goal "TL$(x>>y) = y"; |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
372 |
by (simp_tac (simpset() addsimps [Consq_def]) 1); |
3071 | 373 |
qed"TL_Cons"; |
374 |
||
375 |
Addsimps [HD_Cons,TL_Cons]; |
|
376 |
||
377 |
(* ------------------------------------------------------------------------------------ *) |
|
378 |
||
379 |
section "Finite, Partial, Infinite"; |
|
380 |
||
5068 | 381 |
Goal "Finite (a>>xs) = Finite xs"; |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
382 |
by (simp_tac (simpset() addsimps [Consq_def2,Finite_cons]) 1); |
3071 | 383 |
qed"Finite_Cons"; |
384 |
||
385 |
Addsimps [Finite_Cons]; |
|
6161 | 386 |
Goal "Finite (x::'a Seq) ==> Finite y --> Finite (x@@y)"; |
3275 | 387 |
by (Seq_Finite_induct_tac 1); |
388 |
qed"FiniteConc_1"; |
|
389 |
||
6161 | 390 |
Goal "Finite (z::'a Seq) ==> !x y. z= x@@y --> (Finite x & Finite y)"; |
3275 | 391 |
by (Seq_Finite_induct_tac 1); |
392 |
(* nil*) |
|
393 |
by (strip_tac 1); |
|
394 |
by (Seq_case_simp_tac "x" 1); |
|
395 |
by (Asm_full_simp_tac 1); |
|
396 |
(* cons *) |
|
397 |
by (strip_tac 1); |
|
398 |
by (Seq_case_simp_tac "x" 1); |
|
399 |
by (Seq_case_simp_tac "y" 1); |
|
4098 | 400 |
by (SELECT_GOAL (auto_tac (claset(),simpset()))1); |
3275 | 401 |
by (eres_inst_tac [("x","sa")] allE 1); |
402 |
by (eres_inst_tac [("x","y")] allE 1); |
|
403 |
by (Asm_full_simp_tac 1); |
|
404 |
qed"FiniteConc_2"; |
|
405 |
||
5068 | 406 |
Goal "Finite(x@@y) = (Finite (x::'a Seq) & Finite y)"; |
3275 | 407 |
by (rtac iffI 1); |
3457 | 408 |
by (etac (FiniteConc_2 RS spec RS spec RS mp) 1); |
409 |
by (rtac refl 1); |
|
410 |
by (rtac (FiniteConc_1 RS mp) 1); |
|
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
411 |
by Auto_tac; |
3275 | 412 |
qed"FiniteConc"; |
413 |
||
414 |
Addsimps [FiniteConc]; |
|
415 |
||
416 |
||
10835 | 417 |
Goal "Finite s ==> Finite (Map f$s)"; |
3275 | 418 |
by (Seq_Finite_induct_tac 1); |
419 |
qed"FiniteMap1"; |
|
420 |
||
10835 | 421 |
Goal "Finite s ==> ! t. (s = Map f$t) --> Finite t"; |
3275 | 422 |
by (Seq_Finite_induct_tac 1); |
423 |
by (strip_tac 1); |
|
424 |
by (Seq_case_simp_tac "t" 1); |
|
425 |
by (Asm_full_simp_tac 1); |
|
426 |
(* main case *) |
|
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
427 |
by Auto_tac; |
3275 | 428 |
by (Seq_case_simp_tac "t" 1); |
429 |
by (Asm_full_simp_tac 1); |
|
430 |
qed"FiniteMap2"; |
|
431 |
||
10835 | 432 |
Goal "Finite (Map f$s) = Finite s"; |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
433 |
by Auto_tac; |
3457 | 434 |
by (etac (FiniteMap2 RS spec RS mp) 1); |
435 |
by (rtac refl 1); |
|
436 |
by (etac FiniteMap1 1); |
|
3275 | 437 |
qed"Map2Finite"; |
438 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
439 |
|
10835 | 440 |
Goal "Finite s ==> Finite (Filter P$s)"; |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
441 |
by (Seq_Finite_induct_tac 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
442 |
qed"FiniteFilter"; |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
443 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3361
diff
changeset
|
444 |
|
3361 | 445 |
(* ----------------------------------------------------------------------------------- *) |
446 |
||
447 |
||
448 |
section "admissibility"; |
|
449 |
||
450 |
(* Finite x is proven to be adm: Finite_flat shows that there are only chains of length one. |
|
3461 | 451 |
Then the assumption that an _infinite_ chain exists (from admI2) is set to a contradiction |
3361 | 452 |
to Finite_flat *) |
453 |
||
5068 | 454 |
Goal "!! (x:: 'a Seq). Finite x ==> !y. Finite (y:: 'a Seq) & x<<y --> x=y"; |
3361 | 455 |
by (Seq_Finite_induct_tac 1); |
456 |
by (strip_tac 1); |
|
3457 | 457 |
by (etac conjE 1); |
458 |
by (etac nil_less_is_nil 1); |
|
3361 | 459 |
(* main case *) |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
460 |
by Auto_tac; |
3361 | 461 |
by (Seq_case_simp_tac "y" 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
462 |
by Auto_tac; |
3361 | 463 |
qed_spec_mp"Finite_flat"; |
464 |
||
465 |
||
5068 | 466 |
Goal "adm(%(x:: 'a Seq).Finite x)"; |
3461 | 467 |
by (rtac admI2 1); |
3361 | 468 |
by (eres_inst_tac [("x","0")] allE 1); |
469 |
back(); |
|
3457 | 470 |
by (etac exE 1); |
3361 | 471 |
by (REPEAT (etac conjE 1)); |
472 |
by (res_inst_tac [("x","0")] allE 1); |
|
3457 | 473 |
by (assume_tac 1); |
3361 | 474 |
by (eres_inst_tac [("x","j")] allE 1); |
475 |
by (cut_inst_tac [("x","Y 0"),("y","Y j")] Finite_flat 1); |
|
476 |
(* Generates a contradiction in subgoal 3 *) |
|
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
477 |
by Auto_tac; |
3361 | 478 |
qed"adm_Finite"; |
479 |
||
480 |
Addsimps [adm_Finite]; |
|
481 |
||
3071 | 482 |
|
483 |
(* ------------------------------------------------------------------------------------ *) |
|
484 |
||
485 |
section "Conc"; |
|
486 |
||
5068 | 487 |
Goal "!! x::'a Seq. Finite x ==> ((x @@ y) = (x @@ z)) = (y = z)"; |
3071 | 488 |
by (Seq_Finite_induct_tac 1); |
489 |
qed"Conc_cong"; |
|
490 |
||
5068 | 491 |
Goal "(x @@ y) @@ z = (x::'a Seq) @@ y @@ z"; |
3275 | 492 |
by (Seq_induct_tac "x" [] 1); |
493 |
qed"Conc_assoc"; |
|
494 |
||
5068 | 495 |
Goal "s@@ nil = s"; |
3275 | 496 |
by (res_inst_tac[("x","s")] seq.ind 1); |
497 |
by (Simp_tac 1); |
|
498 |
by (Simp_tac 1); |
|
499 |
by (Simp_tac 1); |
|
500 |
by (Asm_full_simp_tac 1); |
|
501 |
qed"nilConc"; |
|
502 |
||
503 |
Addsimps [nilConc]; |
|
504 |
||
5976 | 505 |
(* should be same as nil_is_Conc2 when all nils are turned to right side !! *) |
5068 | 506 |
Goal "(nil = x @@ y) = ((x::'a Seq)= nil & y = nil)"; |
3361 | 507 |
by (Seq_case_simp_tac "x" 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
508 |
by Auto_tac; |
3361 | 509 |
qed"nil_is_Conc"; |
510 |
||
5068 | 511 |
Goal "(x @@ y = nil) = ((x::'a Seq)= nil & y = nil)"; |
3361 | 512 |
by (Seq_case_simp_tac "x" 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
513 |
by Auto_tac; |
3361 | 514 |
qed"nil_is_Conc2"; |
515 |
||
3275 | 516 |
|
3071 | 517 |
(* ------------------------------------------------------------------------------------ *) |
518 |
||
519 |
section "Last"; |
|
520 |
||
10835 | 521 |
Goal "Finite s ==> s~=nil --> Last$s~=UU"; |
3071 | 522 |
by (Seq_Finite_induct_tac 1); |
523 |
qed"Finite_Last1"; |
|
524 |
||
10835 | 525 |
Goal "Finite s ==> Last$s=UU --> s=nil"; |
3071 | 526 |
by (Seq_Finite_induct_tac 1); |
527 |
by (fast_tac HOL_cs 1); |
|
528 |
qed"Finite_Last2"; |
|
529 |
||
530 |
||
531 |
(* ------------------------------------------------------------------------------------ *) |
|
532 |
||
533 |
||
534 |
section "Filter, Conc"; |
|
535 |
||
536 |
||
10835 | 537 |
Goal "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s"; |
3071 | 538 |
by (Seq_induct_tac "s" [Filter_def] 1); |
539 |
qed"FilterPQ"; |
|
540 |
||
10835 | 541 |
Goal "Filter P$(x @@ y) = (Filter P$x @@ Filter P$y)"; |
4098 | 542 |
by (simp_tac (simpset() addsimps [Filter_def,sfiltersconc]) 1); |
3071 | 543 |
qed"FilterConc"; |
544 |
||
545 |
(* ------------------------------------------------------------------------------------ *) |
|
546 |
||
547 |
section "Map"; |
|
548 |
||
10835 | 549 |
Goal "Map f$(Map g$s) = Map (f o g)$s"; |
3071 | 550 |
by (Seq_induct_tac "s" [] 1); |
551 |
qed"MapMap"; |
|
552 |
||
10835 | 553 |
Goal "Map f$(x@@y) = (Map f$x) @@ (Map f$y)"; |
3071 | 554 |
by (Seq_induct_tac "x" [] 1); |
555 |
qed"MapConc"; |
|
556 |
||
10835 | 557 |
Goal "Filter P$(Map f$x) = Map f$(Filter (P o f)$x)"; |
3071 | 558 |
by (Seq_induct_tac "x" [] 1); |
559 |
qed"MapFilter"; |
|
560 |
||
10835 | 561 |
Goal "nil = (Map f$s) --> s= nil"; |
3275 | 562 |
by (Seq_case_simp_tac "s" 1); |
563 |
qed"nilMap"; |
|
564 |
||
3361 | 565 |
|
10835 | 566 |
Goal "Forall P (Map f$s) = Forall (P o f) s"; |
3275 | 567 |
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1); |
3361 | 568 |
qed"ForallMap"; |
3275 | 569 |
|
570 |
||
571 |
||
3071 | 572 |
|
573 |
(* ------------------------------------------------------------------------------------ *) |
|
574 |
||
3275 | 575 |
section "Forall"; |
3071 | 576 |
|
577 |
||
5068 | 578 |
Goal "Forall P ys & (! x. P x --> Q x) \ |
3071 | 579 |
\ --> Forall Q ys"; |
580 |
by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1); |
|
581 |
qed"ForallPForallQ1"; |
|
582 |
||
583 |
bind_thm ("ForallPForallQ",impI RSN (2,allI RSN (2,conjI RS (ForallPForallQ1 RS mp)))); |
|
584 |
||
5068 | 585 |
Goal "(Forall P x & Forall P y) --> Forall P (x @@ y)"; |
3071 | 586 |
by (Seq_induct_tac "x" [Forall_def,sforall_def] 1); |
587 |
qed"Forall_Conc_impl"; |
|
588 |
||
6161 | 589 |
Goal "Finite x ==> Forall P (x @@ y) = (Forall P x & Forall P y)"; |
3071 | 590 |
by (Seq_Finite_induct_tac 1); |
591 |
qed"Forall_Conc"; |
|
592 |
||
3275 | 593 |
Addsimps [Forall_Conc]; |
594 |
||
10835 | 595 |
Goal "Forall P s --> Forall P (TL$s)"; |
3275 | 596 |
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1); |
597 |
qed"ForallTL1"; |
|
598 |
||
599 |
bind_thm ("ForallTL",ForallTL1 RS mp); |
|
600 |
||
10835 | 601 |
Goal "Forall P s --> Forall P (Dropwhile Q$s)"; |
3275 | 602 |
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1); |
603 |
qed"ForallDropwhile1"; |
|
604 |
||
605 |
bind_thm ("ForallDropwhile",ForallDropwhile1 RS mp); |
|
606 |
||
607 |
||
608 |
(* only admissible in t, not if done in s *) |
|
609 |
||
5068 | 610 |
Goal "! s. Forall P s --> t<<s --> Forall P t"; |
3275 | 611 |
by (Seq_induct_tac "t" [Forall_def,sforall_def] 1); |
612 |
by (strip_tac 1); |
|
613 |
by (Seq_case_simp_tac "sa" 1); |
|
614 |
by (Asm_full_simp_tac 1); |
|
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
615 |
by Auto_tac; |
3275 | 616 |
qed"Forall_prefix"; |
4681 | 617 |
|
3275 | 618 |
bind_thm ("Forall_prefixclosed",Forall_prefix RS spec RS mp RS mp); |
619 |
||
620 |
||
6161 | 621 |
Goal "[| Finite h; Forall P s; s= h @@ t |] ==> Forall P t"; |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
622 |
by Auto_tac; |
3275 | 623 |
qed"Forall_postfixclosed"; |
624 |
||
625 |
||
10835 | 626 |
Goal "((! x. P x --> (Q x = R x)) & Forall P tr) --> Filter Q$tr = Filter R$tr"; |
3275 | 627 |
by (Seq_induct_tac "tr" [Forall_def,sforall_def] 1); |
628 |
qed"ForallPFilterQR1"; |
|
629 |
||
630 |
bind_thm("ForallPFilterQR",allI RS (conjI RS (ForallPFilterQR1 RS mp))); |
|
631 |
||
3071 | 632 |
|
633 |
(* ------------------------------------------------------------------------------------- *) |
|
634 |
||
635 |
section "Forall, Filter"; |
|
636 |
||
637 |
||
10835 | 638 |
Goal "Forall P (Filter P$x)"; |
4098 | 639 |
by (simp_tac (simpset() addsimps [Filter_def,Forall_def,forallPsfilterP]) 1); |
3071 | 640 |
qed"ForallPFilterP"; |
641 |
||
3275 | 642 |
(* holds also in other direction, then equal to forallPfilterP *) |
10835 | 643 |
Goal "Forall P x --> Filter P$x = x"; |
3071 | 644 |
by (Seq_induct_tac "x" [Forall_def,sforall_def,Filter_def] 1); |
645 |
qed"ForallPFilterPid1"; |
|
646 |
||
4034 | 647 |
bind_thm("ForallPFilterPid",ForallPFilterPid1 RS mp); |
3071 | 648 |
|
649 |
||
3275 | 650 |
(* holds also in other direction *) |
5068 | 651 |
Goal "!! ys . Finite ys ==> \ |
10835 | 652 |
\ Forall (%x. ~P x) ys --> Filter P$ys = nil "; |
3275 | 653 |
by (Seq_Finite_induct_tac 1); |
3071 | 654 |
qed"ForallnPFilterPnil1"; |
655 |
||
3275 | 656 |
bind_thm ("ForallnPFilterPnil",ForallnPFilterPnil1 RS mp); |
3071 | 657 |
|
658 |
||
3275 | 659 |
(* holds also in other direction *) |
6161 | 660 |
Goal "~Finite ys & Forall (%x. ~P x) ys \ |
10835 | 661 |
\ --> Filter P$ys = UU "; |
3361 | 662 |
by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1); |
3071 | 663 |
qed"ForallnPFilterPUU1"; |
664 |
||
3275 | 665 |
bind_thm ("ForallnPFilterPUU",conjI RS (ForallnPFilterPUU1 RS mp)); |
666 |
||
667 |
||
668 |
(* inverse of ForallnPFilterPnil *) |
|
669 |
||
10835 | 670 |
Goal "!! ys . Filter P$ys = nil --> \ |
3275 | 671 |
\ (Forall (%x. ~P x) ys & Finite ys)"; |
672 |
by (res_inst_tac[("x","ys")] Seq_induct 1); |
|
673 |
(* adm *) |
|
3361 | 674 |
(* FIX: not admissible, search other proof!! *) |
3457 | 675 |
by (rtac adm_all 1); |
3275 | 676 |
(* base cases *) |
677 |
by (Simp_tac 1); |
|
678 |
by (Simp_tac 1); |
|
679 |
(* main case *) |
|
4833 | 680 |
by (Asm_full_simp_tac 1); |
3275 | 681 |
qed"FilternPnilForallP1"; |
682 |
||
683 |
bind_thm ("FilternPnilForallP",FilternPnilForallP1 RS mp); |
|
684 |
||
3361 | 685 |
(* inverse of ForallnPFilterPUU. proved by 2 lemmas because of adm problems *) |
686 |
||
10835 | 687 |
Goal "Finite ys ==> Filter P$ys ~= UU"; |
3361 | 688 |
by (Seq_Finite_induct_tac 1); |
689 |
qed"FilterUU_nFinite_lemma1"; |
|
3275 | 690 |
|
10835 | 691 |
Goal "~ Forall (%x. ~P x) ys --> Filter P$ys ~= UU"; |
3361 | 692 |
by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1); |
693 |
qed"FilterUU_nFinite_lemma2"; |
|
694 |
||
10835 | 695 |
Goal "Filter P$ys = UU ==> \ |
3275 | 696 |
\ (Forall (%x. ~P x) ys & ~Finite ys)"; |
3361 | 697 |
by (rtac conjI 1); |
698 |
by (cut_inst_tac [] (FilterUU_nFinite_lemma2 RS mp COMP rev_contrapos) 1); |
|
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
699 |
by Auto_tac; |
4098 | 700 |
by (blast_tac (claset() addSDs [FilterUU_nFinite_lemma1]) 1); |
3361 | 701 |
qed"FilternPUUForallP"; |
3071 | 702 |
|
703 |
||
5068 | 704 |
Goal "!! Q P.[| Forall Q ys; Finite ys; !!x. Q x ==> ~P x|] \ |
10835 | 705 |
\ ==> Filter P$ys = nil"; |
3457 | 706 |
by (etac ForallnPFilterPnil 1); |
707 |
by (etac ForallPForallQ 1); |
|
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
708 |
by Auto_tac; |
3071 | 709 |
qed"ForallQFilterPnil"; |
710 |
||
5068 | 711 |
Goal "!! Q P. [| ~Finite ys; Forall Q ys; !!x. Q x ==> ~P x|] \ |
10835 | 712 |
\ ==> Filter P$ys = UU "; |
3457 | 713 |
by (etac ForallnPFilterPUU 1); |
714 |
by (etac ForallPForallQ 1); |
|
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
715 |
by Auto_tac; |
3071 | 716 |
qed"ForallQFilterPUU"; |
717 |
||
718 |
||
719 |
||
720 |
(* ------------------------------------------------------------------------------------- *) |
|
721 |
||
722 |
section "Takewhile, Forall, Filter"; |
|
723 |
||
724 |
||
10835 | 725 |
Goal "Forall P (Takewhile P$x)"; |
4098 | 726 |
by (simp_tac (simpset() addsimps [Forall_def,Takewhile_def,sforallPstakewhileP]) 1); |
3071 | 727 |
qed"ForallPTakewhileP"; |
728 |
||
729 |
||
10835 | 730 |
Goal"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q$x)"; |
3457 | 731 |
by (rtac ForallPForallQ 1); |
732 |
by (rtac ForallPTakewhileP 1); |
|
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
733 |
by Auto_tac; |
3071 | 734 |
qed"ForallPTakewhileQ"; |
735 |
||
736 |
||
10835 | 737 |
Goal "!! Q P.[| Finite (Takewhile Q$ys); !!x. Q x ==> ~P x |] \ |
738 |
\ ==> Filter P$(Takewhile Q$ys) = nil"; |
|
3457 | 739 |
by (etac ForallnPFilterPnil 1); |
740 |
by (rtac ForallPForallQ 1); |
|
741 |
by (rtac ForallPTakewhileP 1); |
|
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
742 |
by Auto_tac; |
3071 | 743 |
qed"FilterPTakewhileQnil"; |
744 |
||
5068 | 745 |
Goal "!! Q P. [| !!x. Q x ==> P x |] ==> \ |
10835 | 746 |
\ Filter P$(Takewhile Q$ys) = (Takewhile Q$ys)"; |
3457 | 747 |
by (rtac ForallPFilterPid 1); |
748 |
by (rtac ForallPForallQ 1); |
|
749 |
by (rtac ForallPTakewhileP 1); |
|
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
750 |
by Auto_tac; |
3071 | 751 |
qed"FilterPTakewhileQid"; |
752 |
||
753 |
Addsimps [ForallPTakewhileP,ForallPTakewhileQ, |
|
754 |
FilterPTakewhileQnil,FilterPTakewhileQid]; |
|
755 |
||
10835 | 756 |
Goal "Takewhile P$(Takewhile P$s) = Takewhile P$s"; |
3275 | 757 |
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1); |
758 |
qed"Takewhile_idempotent"; |
|
3071 | 759 |
|
10835 | 760 |
Goal "Forall P s --> Takewhile (%x. Q x | (~P x))$s = Takewhile Q$s"; |
3275 | 761 |
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1); |
762 |
qed"ForallPTakewhileQnP"; |
|
763 |
||
10835 | 764 |
Goal "Forall P s --> Dropwhile (%x. Q x | (~P x))$s = Dropwhile Q$s"; |
3275 | 765 |
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1); |
766 |
qed"ForallPDropwhileQnP"; |
|
767 |
||
768 |
Addsimps [ForallPTakewhileQnP RS mp, ForallPDropwhileQnP RS mp]; |
|
769 |
||
770 |
||
10835 | 771 |
Goal "Forall P s --> Takewhile P$(s @@ t) = s @@ (Takewhile P$t)"; |
3275 | 772 |
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1); |
773 |
qed"TakewhileConc1"; |
|
774 |
||
775 |
bind_thm("TakewhileConc",TakewhileConc1 RS mp); |
|
776 |
||
10835 | 777 |
Goal "Finite s ==> Forall P s --> Dropwhile P$(s @@ t) = Dropwhile P$t"; |
3275 | 778 |
by (Seq_Finite_induct_tac 1); |
779 |
qed"DropwhileConc1"; |
|
780 |
||
781 |
bind_thm("DropwhileConc",DropwhileConc1 RS mp); |
|
3071 | 782 |
|
783 |
||
784 |
||
785 |
(* ----------------------------------------------------------------------------------- *) |
|
786 |
||
787 |
section "coinductive characterizations of Filter"; |
|
788 |
||
789 |
||
10835 | 790 |
Goal "HD$(Filter P$y) = Def x \ |
791 |
\ --> y = ((Takewhile (%x. ~P x)$y) @@ (x >> TL$(Dropwhile (%a.~P a)$y))) \ |
|
792 |
\ & Finite (Takewhile (%x. ~ P x)$y) & P x"; |
|
3071 | 793 |
|
794 |
(* FIX: pay attention: is only admissible with chain-finite package to be added to |
|
3656 | 795 |
adm test and Finite f x admissibility *) |
3071 | 796 |
by (Seq_induct_tac "y" [] 1); |
3457 | 797 |
by (rtac adm_all 1); |
3071 | 798 |
by (Asm_full_simp_tac 1); |
799 |
by (case_tac "P a" 1); |
|
4681 | 800 |
by (Asm_full_simp_tac 1); |
801 |
by (Blast_tac 1); |
|
3071 | 802 |
(* ~ P a *) |
803 |
by (Asm_full_simp_tac 1); |
|
804 |
qed"divide_Seq_lemma"; |
|
805 |
||
10835 | 806 |
Goal "(x>>xs) << Filter P$y \ |
807 |
\ ==> y = ((Takewhile (%a. ~ P a)$y) @@ (x >> TL$(Dropwhile (%a.~P a)$y))) \ |
|
808 |
\ & Finite (Takewhile (%a. ~ P a)$y) & P x"; |
|
3457 | 809 |
by (rtac (divide_Seq_lemma RS mp) 1); |
3071 | 810 |
by (dres_inst_tac [("fo","HD"),("xa","x>>xs")] monofun_cfun_arg 1); |
811 |
by (Asm_full_simp_tac 1); |
|
812 |
qed"divide_Seq"; |
|
813 |
||
3656 | 814 |
|
10835 | 815 |
Goal "~Forall P y --> (? x. HD$(Filter (%a. ~P a)$y) = Def x)"; |
3656 | 816 |
(* Pay attention: is only admissible with chain-finite package to be added to |
3071 | 817 |
adm test *) |
3656 | 818 |
by (Seq_induct_tac "y" [Forall_def,sforall_def] 1); |
3071 | 819 |
qed"nForall_HDFilter"; |
820 |
||
821 |
||
6161 | 822 |
Goal "~Forall P y \ |
10835 | 823 |
\ ==> ? x. y= (Takewhile P$y @@ (x >> TL$(Dropwhile P$y))) & \ |
824 |
\ Finite (Takewhile P$y) & (~ P x)"; |
|
3457 | 825 |
by (dtac (nForall_HDFilter RS mp) 1); |
3071 | 826 |
by (safe_tac set_cs); |
827 |
by (res_inst_tac [("x","x")] exI 1); |
|
828 |
by (cut_inst_tac [("P1","%x. ~ P x")] (divide_Seq_lemma RS mp) 1); |
|
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
829 |
by Auto_tac; |
3071 | 830 |
qed"divide_Seq2"; |
831 |
||
832 |
||
6161 | 833 |
Goal "~Forall P y \ |
3071 | 834 |
\ ==> ? x bs rs. y= (bs @@ (x>>rs)) & Finite bs & Forall P bs & (~ P x)"; |
835 |
by (cut_inst_tac [] divide_Seq2 1); |
|
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
836 |
(*Auto_tac no longer proves it*) |
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
837 |
by (REPEAT (fast_tac (claset() addss (simpset())) 1)); |
3071 | 838 |
qed"divide_Seq3"; |
839 |
||
3275 | 840 |
Addsimps [FilterPQ,FilterConc,Conc_cong]; |
3071 | 841 |
|
842 |
||
843 |
(* ------------------------------------------------------------------------------------- *) |
|
844 |
||
845 |
||
846 |
section "take_lemma"; |
|
847 |
||
10835 | 848 |
Goal "(!n. seq_take n$x = seq_take n$x') = (x = x')"; |
3071 | 849 |
by (rtac iffI 1); |
4042 | 850 |
by (resolve_tac seq.take_lemmas 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
851 |
by Auto_tac; |
3071 | 852 |
qed"seq_take_lemma"; |
853 |
||
5068 | 854 |
Goal |
10835 | 855 |
" ! n. ((! k. k < n --> seq_take k$y1 = seq_take k$y2) \ |
856 |
\ --> seq_take n$(x @@ (t>>y1)) = seq_take n$(x @@ (t>>y2)))"; |
|
3275 | 857 |
by (Seq_induct_tac "x" [] 1); |
858 |
by (strip_tac 1); |
|
8439 | 859 |
by (case_tac "n" 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
860 |
by Auto_tac; |
8439 | 861 |
by (case_tac "n" 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
862 |
by Auto_tac; |
3275 | 863 |
qed"take_reduction1"; |
3071 | 864 |
|
865 |
||
10835 | 866 |
Goal "!! n.[| x=y; s=t; !! k. k<n ==> seq_take k$y1 = seq_take k$y2|] \ |
867 |
\ ==> seq_take n$(x @@ (s>>y1)) = seq_take n$(y @@ (t>>y2))"; |
|
3071 | 868 |
|
4098 | 869 |
by (auto_tac (claset() addSIs [take_reduction1 RS spec RS mp],simpset())); |
3071 | 870 |
qed"take_reduction"; |
3275 | 871 |
|
3361 | 872 |
(* ------------------------------------------------------------------ |
873 |
take-lemma and take_reduction for << instead of = |
|
874 |
------------------------------------------------------------------ *) |
|
875 |
||
5068 | 876 |
Goal |
10835 | 877 |
" ! n. ((! k. k < n --> seq_take k$y1 << seq_take k$y2) \ |
878 |
\ --> seq_take n$(x @@ (t>>y1)) << seq_take n$(x @@ (t>>y2)))"; |
|
3361 | 879 |
by (Seq_induct_tac "x" [] 1); |
880 |
by (strip_tac 1); |
|
8439 | 881 |
by (case_tac "n" 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
882 |
by Auto_tac; |
8439 | 883 |
by (case_tac "n" 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
884 |
by Auto_tac; |
3361 | 885 |
qed"take_reduction_less1"; |
886 |
||
887 |
||
10835 | 888 |
Goal "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k$y1 << seq_take k$y2|] \ |
889 |
\ ==> seq_take n$(x @@ (s>>y1)) << seq_take n$(y @@ (t>>y2))"; |
|
4098 | 890 |
by (auto_tac (claset() addSIs [take_reduction_less1 RS spec RS mp],simpset())); |
3361 | 891 |
qed"take_reduction_less"; |
892 |
||
893 |
||
894 |
val prems = goalw thy [seq.take_def] |
|
10835 | 895 |
"(!! n. seq_take n$s1 << seq_take n$s2) ==> s1<<s2"; |
3361 | 896 |
|
897 |
by (res_inst_tac [("t","s1")] (seq.reach RS subst) 1); |
|
898 |
by (res_inst_tac [("t","s2")] (seq.reach RS subst) 1); |
|
899 |
by (rtac (fix_def2 RS ssubst ) 1); |
|
3457 | 900 |
by (stac contlub_cfun_fun 1); |
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
4716
diff
changeset
|
901 |
by (rtac chain_iterate 1); |
3457 | 902 |
by (stac contlub_cfun_fun 1); |
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
4716
diff
changeset
|
903 |
by (rtac chain_iterate 1); |
3361 | 904 |
by (rtac lub_mono 1); |
5291 | 905 |
by (rtac (chain_iterate RS ch2ch_Rep_CFunL) 1); |
906 |
by (rtac (chain_iterate RS ch2ch_Rep_CFunL) 1); |
|
3361 | 907 |
by (rtac allI 1); |
908 |
by (resolve_tac prems 1); |
|
909 |
qed"take_lemma_less1"; |
|
910 |
||
911 |
||
10835 | 912 |
Goal "(!n. seq_take n$x << seq_take n$x') = (x << x')"; |
3361 | 913 |
by (rtac iffI 1); |
3457 | 914 |
by (rtac take_lemma_less1 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
915 |
by Auto_tac; |
3457 | 916 |
by (etac monofun_cfun_arg 1); |
3361 | 917 |
qed"take_lemma_less"; |
918 |
||
919 |
(* ------------------------------------------------------------------ |
|
920 |
take-lemma proof principles |
|
921 |
------------------------------------------------------------------ *) |
|
3071 | 922 |
|
5068 | 923 |
Goal "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \ |
3071 | 924 |
\ !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|] \ |
925 |
\ ==> (f (s1 @@ y>>s2)) = (g (s1 @@ y>>s2)) |] \ |
|
926 |
\ ==> A x --> (f x)=(g x)"; |
|
927 |
by (case_tac "Forall Q x" 1); |
|
4098 | 928 |
by (auto_tac (claset() addSDs [divide_Seq3],simpset())); |
3071 | 929 |
qed"take_lemma_principle1"; |
930 |
||
5068 | 931 |
Goal "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \ |
3071 | 932 |
\ !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|] \ |
10835 | 933 |
\ ==> ! n. seq_take n$(f (s1 @@ y>>s2)) \ |
934 |
\ = seq_take n$(g (s1 @@ y>>s2)) |] \ |
|
3071 | 935 |
\ ==> A x --> (f x)=(g x)"; |
936 |
by (case_tac "Forall Q x" 1); |
|
4098 | 937 |
by (auto_tac (claset() addSDs [divide_Seq3],simpset())); |
4042 | 938 |
by (resolve_tac seq.take_lemmas 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
939 |
by Auto_tac; |
3071 | 940 |
qed"take_lemma_principle2"; |
941 |
||
942 |
||
943 |
(* Note: in the following proofs the ordering of proof steps is very |
|
944 |
important, as otherwise either (Forall Q s1) would be in the IH as |
|
945 |
assumption (then rule useless) or it is not possible to strengthen |
|
946 |
the IH by doing a forall closure of the sequence t (then rule also useless). |
|
9877 | 947 |
This is also the reason why the induction rule (nat_less_induct or nat_induct) has to |
3071 | 948 |
to be imbuilt into the rule, as induction has to be done early and the take lemma |
949 |
has to be used in the trivial direction afterwards for the (Forall Q x) case. *) |
|
950 |
||
5068 | 951 |
Goal |
3071 | 952 |
"!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \ |
10835 | 953 |
\ !! s1 s2 y n. [| ! t. A t --> seq_take n$(f t) = seq_take n$(g t);\ |
3071 | 954 |
\ Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |] \ |
10835 | 955 |
\ ==> seq_take (Suc n)$(f (s1 @@ y>>s2)) \ |
956 |
\ = seq_take (Suc n)$(g (s1 @@ y>>s2)) |] \ |
|
3071 | 957 |
\ ==> A x --> (f x)=(g x)"; |
3457 | 958 |
by (rtac impI 1); |
4042 | 959 |
by (resolve_tac seq.take_lemmas 1); |
3457 | 960 |
by (rtac mp 1); |
961 |
by (assume_tac 2); |
|
3071 | 962 |
by (res_inst_tac [("x","x")] spec 1); |
3457 | 963 |
by (rtac nat_induct 1); |
3071 | 964 |
by (Simp_tac 1); |
3457 | 965 |
by (rtac allI 1); |
3071 | 966 |
by (case_tac "Forall Q xa" 1); |
4098 | 967 |
by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec], |
968 |
simpset())) 1); |
|
969 |
by (auto_tac (claset() addSDs [divide_Seq3],simpset())); |
|
3071 | 970 |
qed"take_lemma_induct"; |
971 |
||
972 |
||
5068 | 973 |
Goal |
3071 | 974 |
"!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \ |
10835 | 975 |
\ !! s1 s2 y n. [| ! t m. m < n --> A t --> seq_take m$(f t) = seq_take m$(g t);\ |
3071 | 976 |
\ Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |] \ |
10835 | 977 |
\ ==> seq_take n$(f (s1 @@ y>>s2)) \ |
978 |
\ = seq_take n$(g (s1 @@ y>>s2)) |] \ |
|
3071 | 979 |
\ ==> A x --> (f x)=(g x)"; |
3457 | 980 |
by (rtac impI 1); |
4042 | 981 |
by (resolve_tac seq.take_lemmas 1); |
3457 | 982 |
by (rtac mp 1); |
983 |
by (assume_tac 2); |
|
3071 | 984 |
by (res_inst_tac [("x","x")] spec 1); |
9877 | 985 |
by (rtac nat_less_induct 1); |
3457 | 986 |
by (rtac allI 1); |
3071 | 987 |
by (case_tac "Forall Q xa" 1); |
4098 | 988 |
by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec], |
989 |
simpset())) 1); |
|
990 |
by (auto_tac (claset() addSDs [divide_Seq3],simpset())); |
|
3071 | 991 |
qed"take_lemma_less_induct"; |
992 |
||
3275 | 993 |
|
994 |
(* |
|
3521 | 995 |
local |
996 |
||
997 |
fun qnt_tac i (tac, var) = tac THEN res_inst_tac [("x", var)] spec i; |
|
998 |
||
999 |
fun add_frees tsig = |
|
1000 |
let |
|
1001 |
fun add (Free (x, T), vars) = |
|
1002 |
if Type.of_sort tsig (T, HOLogic.termS) then x ins vars |
|
1003 |
else vars |
|
1004 |
| add (Abs (_, _, t), vars) = add (t, vars) |
|
1005 |
| add (t $ u, vars) = add (t, add (u, vars)) |
|
1006 |
| add (_, vars) = vars; |
|
1007 |
in add end; |
|
1008 |
||
1009 |
||
1010 |
in |
|
1011 |
||
1012 |
(*Generalizes over all free variables, with the named var outermost.*) |
|
1013 |
fun all_frees_tac x i thm = |
|
1014 |
let |
|
14643 | 1015 |
val tsig = Sign.tsig_of (Thm.sign_of_thm thm); |
3521 | 1016 |
val frees = add_frees tsig (nth_elem (i - 1, prems_of thm), [x]); |
1017 |
val frees' = sort (op >) (frees \ x) @ [x]; |
|
1018 |
in |
|
1019 |
foldl (qnt_tac i) (all_tac, frees') thm |
|
1020 |
end; |
|
1021 |
||
1022 |
end; |
|
1023 |
||
3275 | 1024 |
|
5068 | 1025 |
Goal |
3275 | 1026 |
"!! Q. [|!! s h1 h2. [| Forall Q s; A s h1 h2|] ==> (f s h1 h2) = (g s h1 h2) ; \ |
10835 | 1027 |
\ !! s1 s2 y n. [| ! t h1 h2 m. m < n --> (A t h1 h2) --> seq_take m$(f t h1 h2) = seq_take m$(g t h1 h2);\ |
3275 | 1028 |
\ Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) h1 h2|] \ |
10835 | 1029 |
\ ==> seq_take n$(f (s1 @@ y>>s2) h1 h2) \ |
1030 |
\ = seq_take n$(g (s1 @@ y>>s2) h1 h2) |] \ |
|
3275 | 1031 |
\ ==> ! h1 h2. (A x h1 h2) --> (f x h1 h2)=(g x h1 h2)"; |
1032 |
by (strip_tac 1); |
|
4042 | 1033 |
by (resolve_tac seq.take_lemmas 1); |
3457 | 1034 |
by (rtac mp 1); |
1035 |
by (assume_tac 2); |
|
3275 | 1036 |
by (res_inst_tac [("x","h2a")] spec 1); |
1037 |
by (res_inst_tac [("x","h1a")] spec 1); |
|
1038 |
by (res_inst_tac [("x","x")] spec 1); |
|
9877 | 1039 |
by (rtac nat_less_induct 1); |
3457 | 1040 |
by (rtac allI 1); |
3275 | 1041 |
by (case_tac "Forall Q xa" 1); |
4098 | 1042 |
by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec], |
1043 |
simpset())) 1); |
|
1044 |
by (auto_tac (claset() addSDs [divide_Seq3],simpset())); |
|
3275 | 1045 |
qed"take_lemma_less_induct"; |
1046 |
||
1047 |
||
1048 |
||
5068 | 1049 |
Goal |
3275 | 1050 |
"!! Q. [|!! s. Forall Q s ==> P ((f s) = (g s)) ; \ |
10835 | 1051 |
\ !! s1 s2 y n. [| ! t m. m < n --> P (seq_take m$(f t) = seq_take m$(g t));\ |
3275 | 1052 |
\ Forall Q s1; Finite s1; ~ Q y|] \ |
10835 | 1053 |
\ ==> P (seq_take n$(f (s1 @@ y>>s2)) \ |
1054 |
\ = seq_take n$(g (s1 @@ y>>s2))) |] \ |
|
3275 | 1055 |
\ ==> P ((f x)=(g x))"; |
1056 |
||
1057 |
by (res_inst_tac [("t","f x = g x"), |
|
10835 | 1058 |
("s","!n. seq_take n$(f x) = seq_take n$(g x)")] subst 1); |
3457 | 1059 |
by (rtac seq_take_lemma 1); |
3275 | 1060 |
|
1061 |
wie ziehe ich n durch P, d.h. evtl. ns in P muessen umbenannt werden..... |
|
1062 |
||
1063 |
||
1064 |
FIX |
|
1065 |
||
9877 | 1066 |
by (rtac nat_less_induct 1); |
3457 | 1067 |
by (rtac allI 1); |
3275 | 1068 |
by (case_tac "Forall Q xa" 1); |
4098 | 1069 |
by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec], |
1070 |
simpset())) 1); |
|
1071 |
by (auto_tac (claset() addSDs [divide_Seq3],simpset())); |
|
3275 | 1072 |
qed"take_lemma_less_induct"; |
1073 |
||
1074 |
||
1075 |
*) |
|
1076 |
||
1077 |
||
5068 | 1078 |
Goal |
3071 | 1079 |
"!! Q. [| A UU ==> (f UU) = (g UU) ; \ |
1080 |
\ A nil ==> (f nil) = (g nil) ; \ |
|
10835 | 1081 |
\ !! s y n. [| ! t. A t --> seq_take n$(f t) = seq_take n$(g t);\ |
3071 | 1082 |
\ A (y>>s) |] \ |
10835 | 1083 |
\ ==> seq_take (Suc n)$(f (y>>s)) \ |
1084 |
\ = seq_take (Suc n)$(g (y>>s)) |] \ |
|
3071 | 1085 |
\ ==> A x --> (f x)=(g x)"; |
3457 | 1086 |
by (rtac impI 1); |
4042 | 1087 |
by (resolve_tac seq.take_lemmas 1); |
3457 | 1088 |
by (rtac mp 1); |
1089 |
by (assume_tac 2); |
|
3071 | 1090 |
by (res_inst_tac [("x","x")] spec 1); |
3457 | 1091 |
by (rtac nat_induct 1); |
3071 | 1092 |
by (Simp_tac 1); |
3457 | 1093 |
by (rtac allI 1); |
3071 | 1094 |
by (Seq_case_simp_tac "xa" 1); |
1095 |
qed"take_lemma_in_eq_out"; |
|
1096 |
||
1097 |
||
1098 |
(* ------------------------------------------------------------------------------------ *) |
|
1099 |
||
1100 |
section "alternative take_lemma proofs"; |
|
1101 |
||
1102 |
||
1103 |
(* --------------------------------------------------------------- *) |
|
1104 |
(* Alternative Proof of FilterPQ *) |
|
1105 |
(* --------------------------------------------------------------- *) |
|
1106 |
||
1107 |
Delsimps [FilterPQ]; |
|
1108 |
||
1109 |
||
1110 |
(* In general: How to do this case without the same adm problems |
|
1111 |
as for the entire proof ? *) |
|
5068 | 1112 |
Goal "Forall (%x.~(P x & Q x)) s \ |
10835 | 1113 |
\ --> Filter P$(Filter Q$s) =\ |
1114 |
\ Filter (%x. P x & Q x)$s"; |
|
3071 | 1115 |
|
1116 |
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1); |
|
1117 |
qed"Filter_lemma1"; |
|
1118 |
||
6161 | 1119 |
Goal "Finite s ==> \ |
3071 | 1120 |
\ (Forall (%x. (~P x) | (~ Q x)) s \ |
10835 | 1121 |
\ --> Filter P$(Filter Q$s) = nil)"; |
3071 | 1122 |
by (Seq_Finite_induct_tac 1); |
1123 |
qed"Filter_lemma2"; |
|
1124 |
||
6161 | 1125 |
Goal "Finite s ==> \ |
3071 | 1126 |
\ Forall (%x. (~P x) | (~ Q x)) s \ |
10835 | 1127 |
\ --> Filter (%x. P x & Q x)$s = nil"; |
3071 | 1128 |
by (Seq_Finite_induct_tac 1); |
1129 |
qed"Filter_lemma3"; |
|
1130 |
||
1131 |
||
10835 | 1132 |
Goal "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s"; |
3842 | 1133 |
by (res_inst_tac [("A1","%x. True") |
3275 | 1134 |
,("Q1","%x.~(P x & Q x)"),("x1","s")] |
3071 | 1135 |
(take_lemma_induct RS mp) 1); |
5976 | 1136 |
(* better support for A = %x. True *) |
3071 | 1137 |
by (Fast_tac 3); |
4098 | 1138 |
by (asm_full_simp_tac (simpset() addsimps [Filter_lemma1]) 1); |
4833 | 1139 |
by (asm_full_simp_tac (simpset() addsimps [Filter_lemma2,Filter_lemma3]) 1); |
3071 | 1140 |
qed"FilterPQ_takelemma"; |
1141 |
||
1142 |
Addsimps [FilterPQ]; |
|
1143 |
||
1144 |
||
1145 |
(* --------------------------------------------------------------- *) |
|
1146 |
(* Alternative Proof of MapConc *) |
|
1147 |
(* --------------------------------------------------------------- *) |
|
1148 |
||
3275 | 1149 |
|
3071 | 1150 |
|
10835 | 1151 |
Goal "Map f$(x@@y) = (Map f$x) @@ (Map f$y)"; |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
1152 |
by (res_inst_tac [("A1","%x. True"), ("x1","x")] |
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
1153 |
(take_lemma_in_eq_out RS mp) 1); |
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4098
diff
changeset
|
1154 |
by Auto_tac; |
3071 | 1155 |
qed"MapConc_takelemma"; |
1156 |
||
1157 |