clasohm@1465
|
1 |
(* Title: HOL/List
|
clasohm@923
|
2 |
ID: $Id$
|
clasohm@1465
|
3 |
Author: Tobias Nipkow
|
clasohm@923
|
4 |
Copyright 1994 TU Muenchen
|
clasohm@923
|
5 |
|
clasohm@923
|
6 |
List lemmas
|
clasohm@923
|
7 |
*)
|
clasohm@923
|
8 |
|
nipkow@4935
|
9 |
Goal "!x. xs ~= x#xs";
|
nipkow@3040
|
10 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
11 |
by (Auto_tac);
|
nipkow@2608
|
12 |
qed_spec_mp "not_Cons_self";
|
nipkow@3574
|
13 |
bind_thm("not_Cons_self2",not_Cons_self RS not_sym);
|
nipkow@3574
|
14 |
Addsimps [not_Cons_self,not_Cons_self2];
|
clasohm@923
|
15 |
|
nipkow@4935
|
16 |
Goal "(xs ~= []) = (? y ys. xs = y#ys)";
|
nipkow@3040
|
17 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
18 |
by (Auto_tac);
|
clasohm@923
|
19 |
qed "neq_Nil_conv";
|
clasohm@923
|
20 |
|
nipkow@4830
|
21 |
(* Induction over the length of a list: *)
|
nipkow@4935
|
22 |
val [prem] = Goal
|
nipkow@4911
|
23 |
"(!!xs. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P(xs)";
|
wenzelm@5132
|
24 |
by (rtac measure_induct 1 THEN etac prem 1);
|
nipkow@4911
|
25 |
qed "length_induct";
|
nipkow@4911
|
26 |
|
clasohm@923
|
27 |
|
paulson@3468
|
28 |
(** "lists": the list-forming operator over sets **)
|
paulson@3342
|
29 |
|
nipkow@5043
|
30 |
Goalw lists.defs "A<=B ==> lists A <= lists B";
|
paulson@3342
|
31 |
by (rtac lfp_mono 1);
|
paulson@3342
|
32 |
by (REPEAT (ares_tac basic_monos 1));
|
paulson@3342
|
33 |
qed "lists_mono";
|
paulson@3196
|
34 |
|
paulson@3468
|
35 |
val listsE = lists.mk_cases list.simps "x#l : lists A";
|
paulson@3468
|
36 |
AddSEs [listsE];
|
paulson@3468
|
37 |
AddSIs lists.intrs;
|
paulson@3468
|
38 |
|
nipkow@5043
|
39 |
Goal "l: lists A ==> l: lists B --> l: lists (A Int B)";
|
paulson@3468
|
40 |
by (etac lists.induct 1);
|
paulson@3468
|
41 |
by (ALLGOALS Blast_tac);
|
paulson@3468
|
42 |
qed_spec_mp "lists_IntI";
|
paulson@3468
|
43 |
|
nipkow@4935
|
44 |
Goal "lists (A Int B) = lists A Int lists B";
|
wenzelm@4423
|
45 |
by (rtac (mono_Int RS equalityI) 1);
|
wenzelm@4089
|
46 |
by (simp_tac (simpset() addsimps [mono_def, lists_mono]) 1);
|
wenzelm@4089
|
47 |
by (blast_tac (claset() addSIs [lists_IntI]) 1);
|
paulson@3468
|
48 |
qed "lists_Int_eq";
|
paulson@3468
|
49 |
Addsimps [lists_Int_eq];
|
paulson@3468
|
50 |
|
paulson@3196
|
51 |
|
nipkow@4643
|
52 |
(** Case analysis **)
|
nipkow@4643
|
53 |
section "Case analysis";
|
nipkow@2608
|
54 |
|
nipkow@4935
|
55 |
val prems = Goal "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
|
paulson@3457
|
56 |
by (induct_tac "xs" 1);
|
paulson@3457
|
57 |
by (REPEAT(resolve_tac prems 1));
|
nipkow@2608
|
58 |
qed "list_cases";
|
nipkow@2608
|
59 |
|
nipkow@4935
|
60 |
Goal "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
|
nipkow@3040
|
61 |
by (induct_tac "xs" 1);
|
paulson@2891
|
62 |
by (Blast_tac 1);
|
paulson@2891
|
63 |
by (Blast_tac 1);
|
nipkow@2608
|
64 |
bind_thm("list_eq_cases",
|
nipkow@2608
|
65 |
impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp))))));
|
nipkow@2608
|
66 |
|
nipkow@3860
|
67 |
(** length **)
|
nipkow@3860
|
68 |
(* needs to come before "@" because of thm append_eq_append_conv *)
|
nipkow@3860
|
69 |
|
nipkow@3860
|
70 |
section "length";
|
nipkow@3860
|
71 |
|
nipkow@4935
|
72 |
Goal "length(xs@ys) = length(xs)+length(ys)";
|
nipkow@3860
|
73 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
74 |
by (Auto_tac);
|
nipkow@3860
|
75 |
qed"length_append";
|
nipkow@3860
|
76 |
Addsimps [length_append];
|
nipkow@3860
|
77 |
|
nipkow@5129
|
78 |
Goal "length (map f xs) = length xs";
|
nipkow@5129
|
79 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
80 |
by (Auto_tac);
|
nipkow@3860
|
81 |
qed "length_map";
|
nipkow@3860
|
82 |
Addsimps [length_map];
|
nipkow@3860
|
83 |
|
nipkow@4935
|
84 |
Goal "length(rev xs) = length(xs)";
|
nipkow@3860
|
85 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
86 |
by (Auto_tac);
|
nipkow@3860
|
87 |
qed "length_rev";
|
nipkow@3860
|
88 |
Addsimps [length_rev];
|
nipkow@3860
|
89 |
|
nipkow@5043
|
90 |
Goal "xs ~= [] ==> length(tl xs) = (length xs) - 1";
|
wenzelm@4423
|
91 |
by (exhaust_tac "xs" 1);
|
nipkow@5129
|
92 |
by (Auto_tac);
|
nipkow@3896
|
93 |
qed "length_tl";
|
nipkow@3896
|
94 |
Addsimps [length_tl];
|
nipkow@3896
|
95 |
|
nipkow@4935
|
96 |
Goal "(length xs = 0) = (xs = [])";
|
nipkow@3860
|
97 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
98 |
by (Auto_tac);
|
nipkow@3860
|
99 |
qed "length_0_conv";
|
nipkow@3860
|
100 |
AddIffs [length_0_conv];
|
nipkow@3860
|
101 |
|
nipkow@4935
|
102 |
Goal "(0 = length xs) = (xs = [])";
|
nipkow@3860
|
103 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
104 |
by (Auto_tac);
|
nipkow@3860
|
105 |
qed "zero_length_conv";
|
nipkow@3860
|
106 |
AddIffs [zero_length_conv];
|
nipkow@3860
|
107 |
|
nipkow@4935
|
108 |
Goal "(0 < length xs) = (xs ~= [])";
|
nipkow@3860
|
109 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
110 |
by (Auto_tac);
|
nipkow@3860
|
111 |
qed "length_greater_0_conv";
|
nipkow@3860
|
112 |
AddIffs [length_greater_0_conv];
|
nipkow@3860
|
113 |
|
oheimb@5296
|
114 |
Goal "(length xs = Suc n) = (? y ys. xs = y#ys & length ys = n)";
|
oheimb@5296
|
115 |
by (induct_tac "xs" 1);
|
oheimb@5296
|
116 |
by (Auto_tac);
|
oheimb@5296
|
117 |
qed "length_Suc_conv";
|
oheimb@5296
|
118 |
AddIffs [length_Suc_conv];
|
oheimb@5296
|
119 |
|
clasohm@923
|
120 |
(** @ - append **)
|
clasohm@923
|
121 |
|
nipkow@3467
|
122 |
section "@ - append";
|
nipkow@3467
|
123 |
|
nipkow@4935
|
124 |
Goal "(xs@ys)@zs = xs@(ys@zs)";
|
nipkow@3040
|
125 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
126 |
by (Auto_tac);
|
clasohm@923
|
127 |
qed "append_assoc";
|
nipkow@2512
|
128 |
Addsimps [append_assoc];
|
clasohm@923
|
129 |
|
nipkow@4935
|
130 |
Goal "xs @ [] = xs";
|
nipkow@3040
|
131 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
132 |
by (Auto_tac);
|
clasohm@923
|
133 |
qed "append_Nil2";
|
nipkow@2512
|
134 |
Addsimps [append_Nil2];
|
clasohm@923
|
135 |
|
nipkow@4935
|
136 |
Goal "(xs@ys = []) = (xs=[] & ys=[])";
|
nipkow@3040
|
137 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
138 |
by (Auto_tac);
|
nipkow@2608
|
139 |
qed "append_is_Nil_conv";
|
nipkow@2608
|
140 |
AddIffs [append_is_Nil_conv];
|
nipkow@2608
|
141 |
|
nipkow@4935
|
142 |
Goal "([] = xs@ys) = (xs=[] & ys=[])";
|
nipkow@3040
|
143 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
144 |
by (Auto_tac);
|
nipkow@2608
|
145 |
qed "Nil_is_append_conv";
|
nipkow@2608
|
146 |
AddIffs [Nil_is_append_conv];
|
clasohm@923
|
147 |
|
nipkow@4935
|
148 |
Goal "(xs @ ys = xs) = (ys=[])";
|
nipkow@3574
|
149 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
150 |
by (Auto_tac);
|
nipkow@3574
|
151 |
qed "append_self_conv";
|
nipkow@3574
|
152 |
|
nipkow@4935
|
153 |
Goal "(xs = xs @ ys) = (ys=[])";
|
nipkow@3574
|
154 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
155 |
by (Auto_tac);
|
nipkow@3574
|
156 |
qed "self_append_conv";
|
nipkow@3574
|
157 |
AddIffs [append_self_conv,self_append_conv];
|
nipkow@3574
|
158 |
|
nipkow@4935
|
159 |
Goal "!ys. length xs = length ys | length us = length vs \
|
nipkow@3860
|
160 |
\ --> (xs@us = ys@vs) = (xs=ys & us=vs)";
|
wenzelm@4423
|
161 |
by (induct_tac "xs" 1);
|
wenzelm@4423
|
162 |
by (rtac allI 1);
|
wenzelm@4423
|
163 |
by (exhaust_tac "ys" 1);
|
wenzelm@4423
|
164 |
by (Asm_simp_tac 1);
|
wenzelm@4423
|
165 |
by (fast_tac (claset() addIs [less_add_Suc2] addss simpset()
|
nipkow@3860
|
166 |
addEs [less_not_refl2 RSN (2,rev_notE)]) 1);
|
wenzelm@4423
|
167 |
by (rtac allI 1);
|
wenzelm@4423
|
168 |
by (exhaust_tac "ys" 1);
|
oheimb@5296
|
169 |
by (fast_tac (claset() addIs [less_add_Suc2]
|
oheimb@5296
|
170 |
addss (simpset() delsimps [length_Suc_conv])
|
oheimb@5296
|
171 |
addEs [(less_not_refl2 RS not_sym) RSN (2,rev_notE)]) 1);
|
wenzelm@4423
|
172 |
by (Asm_simp_tac 1);
|
nipkow@3860
|
173 |
qed_spec_mp "append_eq_append_conv";
|
nipkow@3860
|
174 |
Addsimps [append_eq_append_conv];
|
nipkow@3860
|
175 |
|
nipkow@4935
|
176 |
Goal "(xs @ ys = xs @ zs) = (ys=zs)";
|
nipkow@3896
|
177 |
by (Simp_tac 1);
|
nipkow@3896
|
178 |
qed "same_append_eq";
|
nipkow@3860
|
179 |
|
nipkow@4935
|
180 |
Goal "(xs @ [x] = ys @ [y]) = (xs = ys & x = y)";
|
nipkow@3896
|
181 |
by (Simp_tac 1);
|
nipkow@3896
|
182 |
qed "append1_eq_conv";
|
nipkow@2608
|
183 |
|
nipkow@4935
|
184 |
Goal "(ys @ xs = zs @ xs) = (ys=zs)";
|
nipkow@3896
|
185 |
by (Simp_tac 1);
|
nipkow@3896
|
186 |
qed "append_same_eq";
|
nipkow@2608
|
187 |
|
nipkow@3896
|
188 |
AddSIs
|
nipkow@3896
|
189 |
[same_append_eq RS iffD2, append1_eq_conv RS iffD2, append_same_eq RS iffD2];
|
nipkow@3896
|
190 |
AddSDs
|
nipkow@3896
|
191 |
[same_append_eq RS iffD1, append1_eq_conv RS iffD1, append_same_eq RS iffD1];
|
nipkow@3571
|
192 |
|
nipkow@4935
|
193 |
Goal "(xs @ ys = ys) = (xs=[])";
|
wenzelm@5132
|
194 |
by (cut_inst_tac [("zs","[]")] append_same_eq 1);
|
nipkow@5129
|
195 |
by (Auto_tac);
|
nipkow@4647
|
196 |
qed "append_self_conv2";
|
nipkow@4647
|
197 |
|
nipkow@4935
|
198 |
Goal "(ys = xs @ ys) = (xs=[])";
|
wenzelm@5132
|
199 |
by (simp_tac (simpset() addsimps
|
nipkow@4647
|
200 |
[simplify (simpset()) (read_instantiate[("ys","[]")]append_same_eq)]) 1);
|
wenzelm@5132
|
201 |
by (Blast_tac 1);
|
nipkow@4647
|
202 |
qed "self_append_conv2";
|
nipkow@4647
|
203 |
AddIffs [append_self_conv2,self_append_conv2];
|
nipkow@4647
|
204 |
|
nipkow@4935
|
205 |
Goal "xs ~= [] --> hd xs # tl xs = xs";
|
paulson@3457
|
206 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
207 |
by (Auto_tac);
|
nipkow@2608
|
208 |
qed_spec_mp "hd_Cons_tl";
|
nipkow@2608
|
209 |
Addsimps [hd_Cons_tl];
|
clasohm@923
|
210 |
|
nipkow@4935
|
211 |
Goal "hd(xs@ys) = (if xs=[] then hd ys else hd xs)";
|
nipkow@3040
|
212 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
213 |
by (Auto_tac);
|
nipkow@1327
|
214 |
qed "hd_append";
|
clasohm@923
|
215 |
|
nipkow@5043
|
216 |
Goal "xs ~= [] ==> hd(xs @ ys) = hd xs";
|
wenzelm@4089
|
217 |
by (asm_simp_tac (simpset() addsimps [hd_append]
|
berghofe@5183
|
218 |
addsplits [list.split]) 1);
|
nipkow@3571
|
219 |
qed "hd_append2";
|
nipkow@3571
|
220 |
Addsimps [hd_append2];
|
nipkow@3571
|
221 |
|
nipkow@4935
|
222 |
Goal "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)";
|
berghofe@5183
|
223 |
by (simp_tac (simpset() addsplits [list.split]) 1);
|
nipkow@2608
|
224 |
qed "tl_append";
|
nipkow@2608
|
225 |
|
nipkow@5043
|
226 |
Goal "xs ~= [] ==> tl(xs @ ys) = (tl xs) @ ys";
|
wenzelm@4089
|
227 |
by (asm_simp_tac (simpset() addsimps [tl_append]
|
berghofe@5183
|
228 |
addsplits [list.split]) 1);
|
nipkow@3571
|
229 |
qed "tl_append2";
|
nipkow@3571
|
230 |
Addsimps [tl_append2];
|
nipkow@3571
|
231 |
|
nipkow@5272
|
232 |
(* trivial rules for solving @-equations automatically *)
|
nipkow@5272
|
233 |
|
nipkow@5272
|
234 |
Goal "xs = ys ==> xs = [] @ ys";
|
nipkow@5272
|
235 |
by(Asm_simp_tac 1);
|
nipkow@5272
|
236 |
qed "eq_Nil_appendI";
|
nipkow@5272
|
237 |
|
nipkow@5272
|
238 |
Goal "[| x#xs1 = ys; xs = xs1 @ zs |] ==> x#xs = ys@zs";
|
nipkow@5272
|
239 |
bd sym 1;
|
nipkow@5272
|
240 |
by(Asm_simp_tac 1);
|
nipkow@5272
|
241 |
qed "Cons_eq_appendI";
|
nipkow@5272
|
242 |
|
nipkow@5272
|
243 |
Goal "[| xs@xs1 = zs; ys = xs1 @ us |] ==> xs@ys = zs@us";
|
nipkow@5272
|
244 |
bd sym 1;
|
nipkow@5272
|
245 |
by(Asm_simp_tac 1);
|
nipkow@5272
|
246 |
qed "append_eq_appendI";
|
nipkow@5272
|
247 |
|
nipkow@4830
|
248 |
|
nipkow@2608
|
249 |
(** map **)
|
nipkow@2608
|
250 |
|
nipkow@3467
|
251 |
section "map";
|
nipkow@3467
|
252 |
|
paulson@5278
|
253 |
Goal "(!x. x : set xs --> f x = g x) --> map f xs = map g xs";
|
paulson@3457
|
254 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
255 |
by (Auto_tac);
|
nipkow@2608
|
256 |
bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
|
nipkow@2608
|
257 |
|
nipkow@4935
|
258 |
Goal "map (%x. x) = (%xs. xs)";
|
nipkow@2608
|
259 |
by (rtac ext 1);
|
nipkow@3040
|
260 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
261 |
by (Auto_tac);
|
nipkow@2608
|
262 |
qed "map_ident";
|
nipkow@2608
|
263 |
Addsimps[map_ident];
|
nipkow@2608
|
264 |
|
nipkow@4935
|
265 |
Goal "map f (xs@ys) = map f xs @ map f ys";
|
nipkow@3040
|
266 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
267 |
by (Auto_tac);
|
nipkow@2608
|
268 |
qed "map_append";
|
nipkow@2608
|
269 |
Addsimps[map_append];
|
nipkow@2608
|
270 |
|
nipkow@4935
|
271 |
Goalw [o_def] "map (f o g) xs = map f (map g xs)";
|
nipkow@3040
|
272 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
273 |
by (Auto_tac);
|
nipkow@2608
|
274 |
qed "map_compose";
|
nipkow@2608
|
275 |
Addsimps[map_compose];
|
nipkow@2608
|
276 |
|
nipkow@4935
|
277 |
Goal "rev(map f xs) = map f (rev xs)";
|
nipkow@3040
|
278 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
279 |
by (Auto_tac);
|
nipkow@2608
|
280 |
qed "rev_map";
|
nipkow@2608
|
281 |
|
nipkow@3589
|
282 |
(* a congruence rule for map: *)
|
paulson@5278
|
283 |
Goal "(xs=ys) --> (!x. x : set ys --> f x = g x) --> map f xs = map g ys";
|
wenzelm@4423
|
284 |
by (rtac impI 1);
|
wenzelm@4423
|
285 |
by (hyp_subst_tac 1);
|
wenzelm@4423
|
286 |
by (induct_tac "ys" 1);
|
nipkow@5129
|
287 |
by (Auto_tac);
|
nipkow@3589
|
288 |
val lemma = result();
|
nipkow@3589
|
289 |
bind_thm("map_cong",impI RSN (2,allI RSN (2,lemma RS mp RS mp)));
|
nipkow@3589
|
290 |
|
nipkow@4935
|
291 |
Goal "(map f xs = []) = (xs = [])";
|
wenzelm@4423
|
292 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
293 |
by (Auto_tac);
|
nipkow@3860
|
294 |
qed "map_is_Nil_conv";
|
nipkow@3860
|
295 |
AddIffs [map_is_Nil_conv];
|
nipkow@3860
|
296 |
|
nipkow@4935
|
297 |
Goal "([] = map f xs) = (xs = [])";
|
wenzelm@4423
|
298 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
299 |
by (Auto_tac);
|
nipkow@3860
|
300 |
qed "Nil_is_map_conv";
|
nipkow@3860
|
301 |
AddIffs [Nil_is_map_conv];
|
nipkow@3860
|
302 |
|
nipkow@3860
|
303 |
|
lcp@1169
|
304 |
(** rev **)
|
lcp@1169
|
305 |
|
nipkow@3467
|
306 |
section "rev";
|
nipkow@3467
|
307 |
|
nipkow@4935
|
308 |
Goal "rev(xs@ys) = rev(ys) @ rev(xs)";
|
nipkow@3040
|
309 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
310 |
by (Auto_tac);
|
lcp@1169
|
311 |
qed "rev_append";
|
nipkow@2512
|
312 |
Addsimps[rev_append];
|
lcp@1169
|
313 |
|
nipkow@4935
|
314 |
Goal "rev(rev l) = l";
|
nipkow@3040
|
315 |
by (induct_tac "l" 1);
|
nipkow@5129
|
316 |
by (Auto_tac);
|
lcp@1169
|
317 |
qed "rev_rev_ident";
|
nipkow@2512
|
318 |
Addsimps[rev_rev_ident];
|
lcp@1169
|
319 |
|
nipkow@4935
|
320 |
Goal "(rev xs = []) = (xs = [])";
|
wenzelm@4423
|
321 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
322 |
by (Auto_tac);
|
nipkow@3860
|
323 |
qed "rev_is_Nil_conv";
|
nipkow@3860
|
324 |
AddIffs [rev_is_Nil_conv];
|
nipkow@3860
|
325 |
|
nipkow@4935
|
326 |
Goal "([] = rev xs) = (xs = [])";
|
wenzelm@4423
|
327 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
328 |
by (Auto_tac);
|
nipkow@3860
|
329 |
qed "Nil_is_rev_conv";
|
nipkow@3860
|
330 |
AddIffs [Nil_is_rev_conv];
|
nipkow@3860
|
331 |
|
nipkow@4935
|
332 |
val prems = Goal "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs";
|
wenzelm@5132
|
333 |
by (stac (rev_rev_ident RS sym) 1);
|
nipkow@4935
|
334 |
br(read_instantiate [("P","%xs. ?P(rev xs)")]list.induct)1;
|
wenzelm@5132
|
335 |
by (ALLGOALS Simp_tac);
|
wenzelm@5132
|
336 |
by (resolve_tac prems 1);
|
wenzelm@5132
|
337 |
by (eresolve_tac prems 1);
|
nipkow@4935
|
338 |
qed "rev_induct";
|
nipkow@4935
|
339 |
|
nipkow@5272
|
340 |
fun rev_induct_tac xs = res_inst_tac [("xs",xs)] rev_induct;
|
nipkow@5272
|
341 |
|
nipkow@4935
|
342 |
Goal "(xs = [] --> P) --> (!ys y. xs = ys@[y] --> P) --> P";
|
wenzelm@5132
|
343 |
by (res_inst_tac [("xs","xs")] rev_induct 1);
|
wenzelm@5132
|
344 |
by (Auto_tac);
|
nipkow@4935
|
345 |
bind_thm ("rev_exhaust",
|
nipkow@4935
|
346 |
impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp)))));
|
nipkow@4935
|
347 |
|
nipkow@2608
|
348 |
|
clasohm@923
|
349 |
(** mem **)
|
clasohm@923
|
350 |
|
nipkow@3467
|
351 |
section "mem";
|
nipkow@3467
|
352 |
|
nipkow@4935
|
353 |
Goal "x mem (xs@ys) = (x mem xs | x mem ys)";
|
nipkow@3040
|
354 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
355 |
by (Auto_tac);
|
clasohm@923
|
356 |
qed "mem_append";
|
nipkow@2512
|
357 |
Addsimps[mem_append];
|
clasohm@923
|
358 |
|
nipkow@4935
|
359 |
Goal "x mem [x:xs. P(x)] = (x mem xs & P(x))";
|
nipkow@3040
|
360 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
361 |
by (Auto_tac);
|
clasohm@923
|
362 |
qed "mem_filter";
|
nipkow@2512
|
363 |
Addsimps[mem_filter];
|
clasohm@923
|
364 |
|
nipkow@3465
|
365 |
(** set **)
|
paulson@1812
|
366 |
|
nipkow@3467
|
367 |
section "set";
|
nipkow@3467
|
368 |
|
oheimb@5296
|
369 |
qed_goal "finite_set" thy "finite (set xs)"
|
oheimb@5296
|
370 |
(K [induct_tac "xs" 1, Auto_tac]);
|
oheimb@5296
|
371 |
Addsimps[finite_set];
|
oheimb@5296
|
372 |
AddSIs[finite_set];
|
oheimb@5296
|
373 |
|
nipkow@4935
|
374 |
Goal "set (xs@ys) = (set xs Un set ys)";
|
nipkow@3040
|
375 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
376 |
by (Auto_tac);
|
paulson@3647
|
377 |
qed "set_append";
|
paulson@3647
|
378 |
Addsimps[set_append];
|
paulson@1812
|
379 |
|
nipkow@4935
|
380 |
Goal "(x mem xs) = (x: set xs)";
|
nipkow@3040
|
381 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
382 |
by (Auto_tac);
|
paulson@3647
|
383 |
qed "set_mem_eq";
|
paulson@1812
|
384 |
|
nipkow@4935
|
385 |
Goal "set l <= set (x#l)";
|
nipkow@5129
|
386 |
by (Auto_tac);
|
paulson@3647
|
387 |
qed "set_subset_Cons";
|
paulson@1936
|
388 |
|
nipkow@4935
|
389 |
Goal "(set xs = {}) = (xs = [])";
|
paulson@3457
|
390 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
391 |
by (Auto_tac);
|
paulson@3647
|
392 |
qed "set_empty";
|
paulson@3647
|
393 |
Addsimps [set_empty];
|
nipkow@2608
|
394 |
|
nipkow@4935
|
395 |
Goal "set(rev xs) = set(xs)";
|
paulson@3457
|
396 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
397 |
by (Auto_tac);
|
paulson@3647
|
398 |
qed "set_rev";
|
paulson@3647
|
399 |
Addsimps [set_rev];
|
nipkow@2608
|
400 |
|
nipkow@4935
|
401 |
Goal "set(map f xs) = f``(set xs)";
|
paulson@3457
|
402 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
403 |
by (Auto_tac);
|
paulson@3647
|
404 |
qed "set_map";
|
paulson@3647
|
405 |
Addsimps [set_map];
|
nipkow@2608
|
406 |
|
nipkow@4935
|
407 |
Goal "(x : set(filter P xs)) = (x : set xs & P x)";
|
nipkow@4605
|
408 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
409 |
by (Auto_tac);
|
nipkow@4605
|
410 |
qed "in_set_filter";
|
nipkow@4605
|
411 |
Addsimps [in_set_filter];
|
nipkow@4605
|
412 |
|
nipkow@5272
|
413 |
Goal "(x : set xs) = (? ys zs. xs = ys@x#zs)";
|
nipkow@5272
|
414 |
by(induct_tac "xs" 1);
|
nipkow@5272
|
415 |
by(Simp_tac 1);
|
nipkow@5272
|
416 |
by(Asm_simp_tac 1);
|
nipkow@5272
|
417 |
br iffI 1;
|
nipkow@5272
|
418 |
by(blast_tac (claset() addIs [eq_Nil_appendI,Cons_eq_appendI]) 1);
|
nipkow@5272
|
419 |
by(REPEAT(etac exE 1));
|
nipkow@5272
|
420 |
by(exhaust_tac "ys" 1);
|
nipkow@5272
|
421 |
by(Auto_tac);
|
nipkow@5272
|
422 |
qed "in_set_conv_decomp";
|
nipkow@5272
|
423 |
|
nipkow@5272
|
424 |
(* eliminate `lists' in favour of `set' *)
|
nipkow@5272
|
425 |
|
nipkow@5272
|
426 |
Goal "(xs : lists A) = (!x : set xs. x : A)";
|
nipkow@5272
|
427 |
by(induct_tac "xs" 1);
|
nipkow@5272
|
428 |
by(Auto_tac);
|
nipkow@5272
|
429 |
qed "in_lists_conv_set";
|
nipkow@5272
|
430 |
|
nipkow@5272
|
431 |
bind_thm("in_listsD",in_lists_conv_set RS iffD1);
|
nipkow@5272
|
432 |
AddSDs [in_listsD];
|
nipkow@5272
|
433 |
bind_thm("in_listsI",in_lists_conv_set RS iffD2);
|
nipkow@5272
|
434 |
AddSIs [in_listsI];
|
paulson@1812
|
435 |
|
clasohm@923
|
436 |
(** list_all **)
|
clasohm@923
|
437 |
|
nipkow@3467
|
438 |
section "list_all";
|
nipkow@3467
|
439 |
|
nipkow@4935
|
440 |
Goal "list_all (%x. True) xs = True";
|
nipkow@3040
|
441 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
442 |
by (Auto_tac);
|
clasohm@923
|
443 |
qed "list_all_True";
|
nipkow@2512
|
444 |
Addsimps [list_all_True];
|
clasohm@923
|
445 |
|
nipkow@4935
|
446 |
Goal "list_all p (xs@ys) = (list_all p xs & list_all p ys)";
|
nipkow@3040
|
447 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
448 |
by (Auto_tac);
|
nipkow@2512
|
449 |
qed "list_all_append";
|
nipkow@2512
|
450 |
Addsimps [list_all_append];
|
clasohm@923
|
451 |
|
nipkow@4935
|
452 |
Goal "list_all P xs = (!x. x mem xs --> P(x))";
|
nipkow@3040
|
453 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
454 |
by (Auto_tac);
|
clasohm@923
|
455 |
qed "list_all_mem_conv";
|
clasohm@923
|
456 |
|
clasohm@923
|
457 |
|
nipkow@2608
|
458 |
(** filter **)
|
clasohm@923
|
459 |
|
nipkow@3467
|
460 |
section "filter";
|
nipkow@3467
|
461 |
|
nipkow@4935
|
462 |
Goal "filter P (xs@ys) = filter P xs @ filter P ys";
|
paulson@3457
|
463 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
464 |
by (Auto_tac);
|
nipkow@2608
|
465 |
qed "filter_append";
|
nipkow@2608
|
466 |
Addsimps [filter_append];
|
nipkow@2608
|
467 |
|
nipkow@4935
|
468 |
Goal "filter (%x. True) xs = xs";
|
nipkow@4605
|
469 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
470 |
by (Auto_tac);
|
nipkow@4605
|
471 |
qed "filter_True";
|
nipkow@4605
|
472 |
Addsimps [filter_True];
|
nipkow@4605
|
473 |
|
nipkow@4935
|
474 |
Goal "filter (%x. False) xs = []";
|
nipkow@4605
|
475 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
476 |
by (Auto_tac);
|
nipkow@4605
|
477 |
qed "filter_False";
|
nipkow@4605
|
478 |
Addsimps [filter_False];
|
nipkow@4605
|
479 |
|
nipkow@4935
|
480 |
Goal "length (filter P xs) <= length xs";
|
paulson@3457
|
481 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
482 |
by (Auto_tac);
|
nipkow@4605
|
483 |
qed "length_filter";
|
paulson@3383
|
484 |
|
nipkow@2608
|
485 |
|
nipkow@2608
|
486 |
(** concat **)
|
nipkow@2608
|
487 |
|
nipkow@3467
|
488 |
section "concat";
|
nipkow@3467
|
489 |
|
nipkow@4935
|
490 |
Goal "concat(xs@ys) = concat(xs)@concat(ys)";
|
nipkow@3040
|
491 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
492 |
by (Auto_tac);
|
nipkow@2608
|
493 |
qed"concat_append";
|
nipkow@2608
|
494 |
Addsimps [concat_append];
|
nipkow@2512
|
495 |
|
nipkow@4935
|
496 |
Goal "(concat xss = []) = (!xs:set xss. xs=[])";
|
wenzelm@4423
|
497 |
by (induct_tac "xss" 1);
|
nipkow@5129
|
498 |
by (Auto_tac);
|
nipkow@3896
|
499 |
qed "concat_eq_Nil_conv";
|
nipkow@3896
|
500 |
AddIffs [concat_eq_Nil_conv];
|
nipkow@3896
|
501 |
|
nipkow@4935
|
502 |
Goal "([] = concat xss) = (!xs:set xss. xs=[])";
|
wenzelm@4423
|
503 |
by (induct_tac "xss" 1);
|
nipkow@5129
|
504 |
by (Auto_tac);
|
nipkow@3896
|
505 |
qed "Nil_eq_concat_conv";
|
nipkow@3896
|
506 |
AddIffs [Nil_eq_concat_conv];
|
nipkow@3896
|
507 |
|
nipkow@4935
|
508 |
Goal "set(concat xs) = Union(set `` set xs)";
|
nipkow@3467
|
509 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
510 |
by (Auto_tac);
|
paulson@3647
|
511 |
qed"set_concat";
|
paulson@3647
|
512 |
Addsimps [set_concat];
|
nipkow@3467
|
513 |
|
nipkow@4935
|
514 |
Goal "map f (concat xs) = concat (map (map f) xs)";
|
nipkow@3467
|
515 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
516 |
by (Auto_tac);
|
nipkow@3467
|
517 |
qed "map_concat";
|
nipkow@3467
|
518 |
|
nipkow@4935
|
519 |
Goal "filter p (concat xs) = concat (map (filter p) xs)";
|
nipkow@3467
|
520 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
521 |
by (Auto_tac);
|
nipkow@3467
|
522 |
qed"filter_concat";
|
nipkow@3467
|
523 |
|
nipkow@4935
|
524 |
Goal "rev(concat xs) = concat (map rev (rev xs))";
|
nipkow@3467
|
525 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
526 |
by (Auto_tac);
|
nipkow@2608
|
527 |
qed "rev_concat";
|
clasohm@923
|
528 |
|
clasohm@923
|
529 |
(** nth **)
|
clasohm@923
|
530 |
|
nipkow@3467
|
531 |
section "nth";
|
nipkow@3467
|
532 |
|
paulson@5278
|
533 |
Goal "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
|
berghofe@5183
|
534 |
by (induct_tac "n" 1);
|
paulson@3457
|
535 |
by (Asm_simp_tac 1);
|
paulson@3457
|
536 |
by (rtac allI 1);
|
paulson@3457
|
537 |
by (exhaust_tac "xs" 1);
|
nipkow@5129
|
538 |
by (Auto_tac);
|
nipkow@2608
|
539 |
qed_spec_mp "nth_append";
|
nipkow@2608
|
540 |
|
nipkow@4935
|
541 |
Goal "!n. n < length xs --> (map f xs)!n = f(xs!n)";
|
nipkow@3040
|
542 |
by (induct_tac "xs" 1);
|
nipkow@1301
|
543 |
(* case [] *)
|
nipkow@1301
|
544 |
by (Asm_full_simp_tac 1);
|
nipkow@1301
|
545 |
(* case x#xl *)
|
nipkow@1301
|
546 |
by (rtac allI 1);
|
berghofe@5183
|
547 |
by (induct_tac "n" 1);
|
nipkow@5129
|
548 |
by (Auto_tac);
|
nipkow@1485
|
549 |
qed_spec_mp "nth_map";
|
nipkow@1301
|
550 |
Addsimps [nth_map];
|
nipkow@1301
|
551 |
|
nipkow@4935
|
552 |
Goal "!n. n < length xs --> list_all P xs --> P(xs!n)";
|
nipkow@3040
|
553 |
by (induct_tac "xs" 1);
|
nipkow@1301
|
554 |
(* case [] *)
|
nipkow@1301
|
555 |
by (Simp_tac 1);
|
nipkow@1301
|
556 |
(* case x#xl *)
|
nipkow@1301
|
557 |
by (rtac allI 1);
|
berghofe@5183
|
558 |
by (induct_tac "n" 1);
|
nipkow@5129
|
559 |
by (Auto_tac);
|
nipkow@1485
|
560 |
qed_spec_mp "list_all_nth";
|
nipkow@1301
|
561 |
|
nipkow@4935
|
562 |
Goal "!n. n < length xs --> xs!n mem xs";
|
nipkow@3040
|
563 |
by (induct_tac "xs" 1);
|
nipkow@1301
|
564 |
(* case [] *)
|
nipkow@1301
|
565 |
by (Simp_tac 1);
|
nipkow@1301
|
566 |
(* case x#xl *)
|
nipkow@1301
|
567 |
by (rtac allI 1);
|
berghofe@5183
|
568 |
by (induct_tac "n" 1);
|
nipkow@1301
|
569 |
(* case 0 *)
|
nipkow@1301
|
570 |
by (Asm_full_simp_tac 1);
|
nipkow@1301
|
571 |
(* case Suc x *)
|
nipkow@4686
|
572 |
by (Asm_full_simp_tac 1);
|
nipkow@1485
|
573 |
qed_spec_mp "nth_mem";
|
nipkow@1301
|
574 |
Addsimps [nth_mem];
|
nipkow@1301
|
575 |
|
nipkow@5077
|
576 |
(** list update **)
|
nipkow@5077
|
577 |
|
nipkow@5077
|
578 |
section "list update";
|
nipkow@5077
|
579 |
|
nipkow@5077
|
580 |
Goal "!i. length(xs[i:=x]) = length xs";
|
nipkow@5077
|
581 |
by (induct_tac "xs" 1);
|
nipkow@5077
|
582 |
by (Simp_tac 1);
|
berghofe@5183
|
583 |
by (asm_full_simp_tac (simpset() addsplits [nat.split]) 1);
|
nipkow@5077
|
584 |
qed_spec_mp "length_list_update";
|
nipkow@5077
|
585 |
Addsimps [length_list_update];
|
nipkow@5077
|
586 |
|
nipkow@5077
|
587 |
|
nipkow@3896
|
588 |
(** last & butlast **)
|
nipkow@1327
|
589 |
|
nipkow@4935
|
590 |
Goal "last(xs@[x]) = x";
|
wenzelm@4423
|
591 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
592 |
by (Auto_tac);
|
nipkow@3896
|
593 |
qed "last_snoc";
|
nipkow@3896
|
594 |
Addsimps [last_snoc];
|
nipkow@3896
|
595 |
|
nipkow@4935
|
596 |
Goal "butlast(xs@[x]) = xs";
|
wenzelm@4423
|
597 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
598 |
by (Auto_tac);
|
nipkow@3896
|
599 |
qed "butlast_snoc";
|
nipkow@3896
|
600 |
Addsimps [butlast_snoc];
|
nipkow@3896
|
601 |
|
nipkow@4935
|
602 |
Goal "length(butlast xs) = length xs - 1";
|
nipkow@4935
|
603 |
by (res_inst_tac [("xs","xs")] rev_induct 1);
|
nipkow@5129
|
604 |
by (Auto_tac);
|
nipkow@4643
|
605 |
qed "length_butlast";
|
nipkow@4643
|
606 |
Addsimps [length_butlast];
|
nipkow@4643
|
607 |
|
paulson@5278
|
608 |
Goal "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
|
wenzelm@4423
|
609 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
610 |
by (Auto_tac);
|
nipkow@3896
|
611 |
qed_spec_mp "butlast_append";
|
nipkow@3896
|
612 |
|
nipkow@4935
|
613 |
Goal "x:set(butlast xs) --> x:set xs";
|
wenzelm@4423
|
614 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
615 |
by (Auto_tac);
|
nipkow@3896
|
616 |
qed_spec_mp "in_set_butlastD";
|
nipkow@3896
|
617 |
|
nipkow@5043
|
618 |
Goal "x:set(butlast xs) ==> x:set(butlast(xs@ys))";
|
nipkow@4686
|
619 |
by (asm_simp_tac (simpset() addsimps [butlast_append]) 1);
|
wenzelm@4423
|
620 |
by (blast_tac (claset() addDs [in_set_butlastD]) 1);
|
nipkow@3896
|
621 |
qed "in_set_butlast_appendI1";
|
nipkow@3896
|
622 |
|
nipkow@5043
|
623 |
Goal "x:set(butlast ys) ==> x:set(butlast(xs@ys))";
|
nipkow@4686
|
624 |
by (asm_simp_tac (simpset() addsimps [butlast_append]) 1);
|
wenzelm@4423
|
625 |
by (Clarify_tac 1);
|
wenzelm@4423
|
626 |
by (Full_simp_tac 1);
|
nipkow@3896
|
627 |
qed "in_set_butlast_appendI2";
|
nipkow@3902
|
628 |
|
nipkow@2608
|
629 |
(** take & drop **)
|
nipkow@2608
|
630 |
section "take & drop";
|
nipkow@1327
|
631 |
|
nipkow@4935
|
632 |
Goal "take 0 xs = []";
|
nipkow@3040
|
633 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
634 |
by (Auto_tac);
|
nipkow@1327
|
635 |
qed "take_0";
|
nipkow@1327
|
636 |
|
nipkow@4935
|
637 |
Goal "drop 0 xs = xs";
|
nipkow@3040
|
638 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
639 |
by (Auto_tac);
|
nipkow@2608
|
640 |
qed "drop_0";
|
nipkow@2608
|
641 |
|
nipkow@4935
|
642 |
Goal "take (Suc n) (x#xs) = x # take n xs";
|
paulson@1552
|
643 |
by (Simp_tac 1);
|
nipkow@1419
|
644 |
qed "take_Suc_Cons";
|
nipkow@1327
|
645 |
|
nipkow@4935
|
646 |
Goal "drop (Suc n) (x#xs) = drop n xs";
|
nipkow@2608
|
647 |
by (Simp_tac 1);
|
nipkow@2608
|
648 |
qed "drop_Suc_Cons";
|
nipkow@2608
|
649 |
|
nipkow@2608
|
650 |
Delsimps [take_Cons,drop_Cons];
|
nipkow@2608
|
651 |
Addsimps [take_0,take_Suc_Cons,drop_0,drop_Suc_Cons];
|
nipkow@2608
|
652 |
|
nipkow@4935
|
653 |
Goal "!xs. length(take n xs) = min (length xs) n";
|
berghofe@5183
|
654 |
by (induct_tac "n" 1);
|
nipkow@5129
|
655 |
by (Auto_tac);
|
paulson@3457
|
656 |
by (exhaust_tac "xs" 1);
|
nipkow@5129
|
657 |
by (Auto_tac);
|
nipkow@2608
|
658 |
qed_spec_mp "length_take";
|
nipkow@2608
|
659 |
Addsimps [length_take];
|
clasohm@923
|
660 |
|
nipkow@4935
|
661 |
Goal "!xs. length(drop n xs) = (length xs - n)";
|
berghofe@5183
|
662 |
by (induct_tac "n" 1);
|
nipkow@5129
|
663 |
by (Auto_tac);
|
paulson@3457
|
664 |
by (exhaust_tac "xs" 1);
|
nipkow@5129
|
665 |
by (Auto_tac);
|
nipkow@2608
|
666 |
qed_spec_mp "length_drop";
|
nipkow@2608
|
667 |
Addsimps [length_drop];
|
nipkow@2608
|
668 |
|
nipkow@4935
|
669 |
Goal "!xs. length xs <= n --> take n xs = xs";
|
berghofe@5183
|
670 |
by (induct_tac "n" 1);
|
nipkow@5129
|
671 |
by (Auto_tac);
|
paulson@3457
|
672 |
by (exhaust_tac "xs" 1);
|
nipkow@5129
|
673 |
by (Auto_tac);
|
nipkow@2608
|
674 |
qed_spec_mp "take_all";
|
clasohm@923
|
675 |
|
nipkow@4935
|
676 |
Goal "!xs. length xs <= n --> drop n xs = []";
|
berghofe@5183
|
677 |
by (induct_tac "n" 1);
|
nipkow@5129
|
678 |
by (Auto_tac);
|
paulson@3457
|
679 |
by (exhaust_tac "xs" 1);
|
nipkow@5129
|
680 |
by (Auto_tac);
|
nipkow@2608
|
681 |
qed_spec_mp "drop_all";
|
nipkow@2608
|
682 |
|
paulson@5278
|
683 |
Goal "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
|
berghofe@5183
|
684 |
by (induct_tac "n" 1);
|
nipkow@5129
|
685 |
by (Auto_tac);
|
paulson@3457
|
686 |
by (exhaust_tac "xs" 1);
|
nipkow@5129
|
687 |
by (Auto_tac);
|
nipkow@2608
|
688 |
qed_spec_mp "take_append";
|
nipkow@2608
|
689 |
Addsimps [take_append];
|
nipkow@2608
|
690 |
|
nipkow@4935
|
691 |
Goal "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys";
|
berghofe@5183
|
692 |
by (induct_tac "n" 1);
|
nipkow@5129
|
693 |
by (Auto_tac);
|
paulson@3457
|
694 |
by (exhaust_tac "xs" 1);
|
nipkow@5129
|
695 |
by (Auto_tac);
|
nipkow@2608
|
696 |
qed_spec_mp "drop_append";
|
nipkow@2608
|
697 |
Addsimps [drop_append];
|
nipkow@2608
|
698 |
|
nipkow@4935
|
699 |
Goal "!xs n. take n (take m xs) = take (min n m) xs";
|
berghofe@5183
|
700 |
by (induct_tac "m" 1);
|
nipkow@5129
|
701 |
by (Auto_tac);
|
paulson@3457
|
702 |
by (exhaust_tac "xs" 1);
|
nipkow@5129
|
703 |
by (Auto_tac);
|
berghofe@5183
|
704 |
by (exhaust_tac "na" 1);
|
nipkow@5129
|
705 |
by (Auto_tac);
|
nipkow@2608
|
706 |
qed_spec_mp "take_take";
|
nipkow@2608
|
707 |
|
nipkow@4935
|
708 |
Goal "!xs. drop n (drop m xs) = drop (n + m) xs";
|
berghofe@5183
|
709 |
by (induct_tac "m" 1);
|
nipkow@5129
|
710 |
by (Auto_tac);
|
paulson@3457
|
711 |
by (exhaust_tac "xs" 1);
|
nipkow@5129
|
712 |
by (Auto_tac);
|
nipkow@2608
|
713 |
qed_spec_mp "drop_drop";
|
clasohm@923
|
714 |
|
nipkow@4935
|
715 |
Goal "!xs n. take n (drop m xs) = drop m (take (n + m) xs)";
|
berghofe@5183
|
716 |
by (induct_tac "m" 1);
|
nipkow@5129
|
717 |
by (Auto_tac);
|
paulson@3457
|
718 |
by (exhaust_tac "xs" 1);
|
nipkow@5129
|
719 |
by (Auto_tac);
|
nipkow@2608
|
720 |
qed_spec_mp "take_drop";
|
nipkow@2608
|
721 |
|
nipkow@4935
|
722 |
Goal "!xs. take n (map f xs) = map f (take n xs)";
|
berghofe@5183
|
723 |
by (induct_tac "n" 1);
|
nipkow@5129
|
724 |
by (Auto_tac);
|
paulson@3457
|
725 |
by (exhaust_tac "xs" 1);
|
nipkow@5129
|
726 |
by (Auto_tac);
|
nipkow@2608
|
727 |
qed_spec_mp "take_map";
|
nipkow@2608
|
728 |
|
nipkow@4935
|
729 |
Goal "!xs. drop n (map f xs) = map f (drop n xs)";
|
berghofe@5183
|
730 |
by (induct_tac "n" 1);
|
nipkow@5129
|
731 |
by (Auto_tac);
|
paulson@3457
|
732 |
by (exhaust_tac "xs" 1);
|
nipkow@5129
|
733 |
by (Auto_tac);
|
nipkow@2608
|
734 |
qed_spec_mp "drop_map";
|
nipkow@2608
|
735 |
|
nipkow@4935
|
736 |
Goal "!n i. i < n --> (take n xs)!i = xs!i";
|
paulson@3457
|
737 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
738 |
by (Auto_tac);
|
paulson@3457
|
739 |
by (exhaust_tac "n" 1);
|
paulson@3457
|
740 |
by (Blast_tac 1);
|
paulson@3457
|
741 |
by (exhaust_tac "i" 1);
|
nipkow@5129
|
742 |
by (Auto_tac);
|
nipkow@2608
|
743 |
qed_spec_mp "nth_take";
|
nipkow@2608
|
744 |
Addsimps [nth_take];
|
clasohm@923
|
745 |
|
nipkow@4935
|
746 |
Goal "!xs i. n + i <= length xs --> (drop n xs)!i = xs!(n+i)";
|
berghofe@5183
|
747 |
by (induct_tac "n" 1);
|
nipkow@5129
|
748 |
by (Auto_tac);
|
paulson@3457
|
749 |
by (exhaust_tac "xs" 1);
|
nipkow@5129
|
750 |
by (Auto_tac);
|
nipkow@2608
|
751 |
qed_spec_mp "nth_drop";
|
nipkow@2608
|
752 |
Addsimps [nth_drop];
|
nipkow@2608
|
753 |
|
nipkow@2608
|
754 |
(** takeWhile & dropWhile **)
|
nipkow@2608
|
755 |
|
nipkow@3467
|
756 |
section "takeWhile & dropWhile";
|
nipkow@3467
|
757 |
|
nipkow@4935
|
758 |
Goal "takeWhile P xs @ dropWhile P xs = xs";
|
nipkow@3586
|
759 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
760 |
by (Auto_tac);
|
nipkow@3586
|
761 |
qed "takeWhile_dropWhile_id";
|
nipkow@3586
|
762 |
Addsimps [takeWhile_dropWhile_id];
|
nipkow@3586
|
763 |
|
nipkow@4935
|
764 |
Goal "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
|
paulson@3457
|
765 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
766 |
by (Auto_tac);
|
nipkow@2608
|
767 |
bind_thm("takeWhile_append1", conjI RS (result() RS mp));
|
nipkow@2608
|
768 |
Addsimps [takeWhile_append1];
|
clasohm@923
|
769 |
|
nipkow@4935
|
770 |
Goal "(!x:set xs. P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
|
paulson@3457
|
771 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
772 |
by (Auto_tac);
|
nipkow@2608
|
773 |
bind_thm("takeWhile_append2", ballI RS (result() RS mp));
|
nipkow@2608
|
774 |
Addsimps [takeWhile_append2];
|
lcp@1169
|
775 |
|
nipkow@4935
|
776 |
Goal "x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
|
paulson@3457
|
777 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
778 |
by (Auto_tac);
|
nipkow@2608
|
779 |
bind_thm("dropWhile_append1", conjI RS (result() RS mp));
|
nipkow@2608
|
780 |
Addsimps [dropWhile_append1];
|
nipkow@2608
|
781 |
|
nipkow@4935
|
782 |
Goal "(!x:set xs. P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
|
paulson@3457
|
783 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
784 |
by (Auto_tac);
|
nipkow@2608
|
785 |
bind_thm("dropWhile_append2", ballI RS (result() RS mp));
|
nipkow@2608
|
786 |
Addsimps [dropWhile_append2];
|
nipkow@2608
|
787 |
|
nipkow@4935
|
788 |
Goal "x:set(takeWhile P xs) --> x:set xs & P x";
|
paulson@3457
|
789 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
790 |
by (Auto_tac);
|
paulson@3647
|
791 |
qed_spec_mp"set_take_whileD";
|
nipkow@2608
|
792 |
|
oheimb@4132
|
793 |
qed_goal "zip_Nil_Nil" thy "zip [] [] = []" (K [Simp_tac 1]);
|
oheimb@4132
|
794 |
qed_goal "zip_Cons_Cons" thy "zip (x#xs) (y#ys) = (x,y)#zip xs ys"
|
oheimb@4132
|
795 |
(K [Simp_tac 1]);
|
nipkow@4605
|
796 |
|
nipkow@5272
|
797 |
|
nipkow@5272
|
798 |
(** foldl **)
|
nipkow@5272
|
799 |
section "foldl";
|
nipkow@5272
|
800 |
|
nipkow@5272
|
801 |
Goal "!a. foldl f a (xs @ ys) = foldl f (foldl f a xs) ys";
|
nipkow@5272
|
802 |
by(induct_tac "xs" 1);
|
nipkow@5272
|
803 |
by(Auto_tac);
|
nipkow@5272
|
804 |
qed_spec_mp "foldl_append";
|
nipkow@5272
|
805 |
Addsimps [foldl_append];
|
nipkow@5272
|
806 |
|
nipkow@5272
|
807 |
(* Note: `n <= foldl op+ n ns' looks simpler, but is more difficult to use
|
nipkow@5272
|
808 |
because it requires an additional transitivity step
|
nipkow@5272
|
809 |
*)
|
nipkow@5272
|
810 |
Goal "!n::nat. m <= n --> m <= foldl op+ n ns";
|
nipkow@5272
|
811 |
by(induct_tac "ns" 1);
|
nipkow@5272
|
812 |
by(Simp_tac 1);
|
nipkow@5272
|
813 |
by(Asm_full_simp_tac 1);
|
nipkow@5272
|
814 |
by(blast_tac (claset() addIs [trans_le_add1]) 1);
|
nipkow@5272
|
815 |
qed_spec_mp "start_le_sum";
|
nipkow@5272
|
816 |
|
nipkow@5272
|
817 |
Goal "n : set ns ==> n <= foldl op+ 0 ns";
|
nipkow@5272
|
818 |
by(auto_tac (claset() addIs [start_le_sum],
|
nipkow@5272
|
819 |
simpset() addsimps [in_set_conv_decomp]));
|
nipkow@5272
|
820 |
qed "elem_le_sum";
|
nipkow@5272
|
821 |
|
nipkow@5272
|
822 |
Goal "!m. (foldl op+ m ns = 0) = (m=0 & (!n : set ns. n=0))";
|
nipkow@5272
|
823 |
by(induct_tac "ns" 1);
|
nipkow@5272
|
824 |
by(Auto_tac);
|
nipkow@5272
|
825 |
qed_spec_mp "sum_eq_0_conv";
|
nipkow@5272
|
826 |
AddIffs [sum_eq_0_conv];
|
nipkow@5272
|
827 |
|
nipkow@5272
|
828 |
|
nipkow@4605
|
829 |
(** nodups & remdups **)
|
nipkow@4605
|
830 |
section "nodups & remdups";
|
nipkow@4605
|
831 |
|
nipkow@4935
|
832 |
Goal "set(remdups xs) = set xs";
|
nipkow@4605
|
833 |
by (induct_tac "xs" 1);
|
nipkow@4605
|
834 |
by (Simp_tac 1);
|
nipkow@4686
|
835 |
by (asm_full_simp_tac (simpset() addsimps [insert_absorb]) 1);
|
nipkow@4605
|
836 |
qed "set_remdups";
|
nipkow@4605
|
837 |
Addsimps [set_remdups];
|
nipkow@4605
|
838 |
|
nipkow@4935
|
839 |
Goal "nodups(remdups xs)";
|
nipkow@4605
|
840 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
841 |
by (Auto_tac);
|
nipkow@4605
|
842 |
qed "nodups_remdups";
|
nipkow@4605
|
843 |
|
nipkow@4935
|
844 |
Goal "nodups xs --> nodups (filter P xs)";
|
nipkow@4605
|
845 |
by (induct_tac "xs" 1);
|
nipkow@5129
|
846 |
by (Auto_tac);
|
nipkow@4605
|
847 |
qed_spec_mp "nodups_filter";
|
nipkow@4605
|
848 |
|
nipkow@3589
|
849 |
(** replicate **)
|
nipkow@3589
|
850 |
section "replicate";
|
nipkow@3589
|
851 |
|
nipkow@4935
|
852 |
Goal "set(replicate (Suc n) x) = {x}";
|
wenzelm@4423
|
853 |
by (induct_tac "n" 1);
|
nipkow@5129
|
854 |
by (Auto_tac);
|
nipkow@3589
|
855 |
val lemma = result();
|
nipkow@3589
|
856 |
|
nipkow@5043
|
857 |
Goal "n ~= 0 ==> set(replicate n x) = {x}";
|
wenzelm@4423
|
858 |
by (fast_tac (claset() addSDs [not0_implies_Suc] addSIs [lemma]) 1);
|
nipkow@3589
|
859 |
qed "set_replicate";
|
nipkow@3589
|
860 |
Addsimps [set_replicate];
|
nipkow@5162
|
861 |
|
nipkow@5162
|
862 |
|
nipkow@5281
|
863 |
(*** Lexcicographic orderings on lists ***)
|
nipkow@5281
|
864 |
section"Lexcicographic orderings on lists";
|
nipkow@5281
|
865 |
|
nipkow@5281
|
866 |
Goal "wf r ==> wf(lexn r n)";
|
nipkow@5281
|
867 |
by(induct_tac "n" 1);
|
nipkow@5281
|
868 |
by(Simp_tac 1);
|
nipkow@5281
|
869 |
by(Simp_tac 1);
|
nipkow@5281
|
870 |
br wf_subset 1;
|
nipkow@5281
|
871 |
br Int_lower1 2;
|
nipkow@5281
|
872 |
br wf_prod_fun_image 1;
|
nipkow@5281
|
873 |
br injI 2;
|
nipkow@5281
|
874 |
by(Auto_tac);
|
nipkow@5281
|
875 |
qed "wf_lexn";
|
nipkow@5281
|
876 |
|
nipkow@5281
|
877 |
Goal "!xs ys. (xs,ys) : lexn r n --> length xs = n & length ys = n";
|
nipkow@5281
|
878 |
by(induct_tac "n" 1);
|
nipkow@5281
|
879 |
by(Auto_tac);
|
nipkow@5281
|
880 |
qed_spec_mp "lexn_length";
|
nipkow@5281
|
881 |
|
nipkow@5281
|
882 |
Goalw [lex_def] "wf r ==> wf(lex r)";
|
nipkow@5281
|
883 |
br wf_UN 1;
|
nipkow@5281
|
884 |
by(blast_tac (claset() addIs [wf_lexn]) 1);
|
nipkow@5281
|
885 |
by(Clarify_tac 1);
|
nipkow@5281
|
886 |
by(rename_tac "m n" 1);
|
nipkow@5281
|
887 |
by(subgoal_tac "m ~= n" 1);
|
nipkow@5281
|
888 |
by(Blast_tac 2);
|
nipkow@5281
|
889 |
by(blast_tac (claset() addDs [lexn_length,not_sym]) 1);
|
nipkow@5281
|
890 |
qed "wf_lex";
|
nipkow@5281
|
891 |
AddSIs [wf_lex];
|
nipkow@5281
|
892 |
|
nipkow@5281
|
893 |
Goal
|
nipkow@5281
|
894 |
"lexn r n = \
|
nipkow@5281
|
895 |
\ {(xs,ys). length xs = n & length ys = n & \
|
nipkow@5281
|
896 |
\ (? xys x y xs' ys'. xs= xys @ x#xs' & ys= xys @ y#ys' & (x,y):r)}";
|
nipkow@5281
|
897 |
by(induct_tac "n" 1);
|
nipkow@5281
|
898 |
by(Simp_tac 1);
|
nipkow@5281
|
899 |
by(Blast_tac 1);
|
oheimb@5296
|
900 |
by(asm_full_simp_tac (simpset() delsimps [length_Suc_conv]
|
oheimb@5296
|
901 |
addsimps [lex_prod_def]) 1);
|
oheimb@5296
|
902 |
by(auto_tac (claset(), simpset() delsimps [length_Suc_conv]));
|
nipkow@5281
|
903 |
by(Blast_tac 1);
|
nipkow@5281
|
904 |
by(rename_tac "a xys x xs' y ys'" 1);
|
nipkow@5281
|
905 |
by(res_inst_tac [("x","a#xys")] exI 1);
|
nipkow@5281
|
906 |
by(Simp_tac 1);
|
nipkow@5281
|
907 |
by(exhaust_tac "xys" 1);
|
oheimb@5296
|
908 |
by(ALLGOALS (asm_full_simp_tac (simpset() delsimps [length_Suc_conv])));
|
nipkow@5281
|
909 |
by(Blast_tac 1);
|
nipkow@5281
|
910 |
qed "lexn_conv";
|
nipkow@5281
|
911 |
|
nipkow@5281
|
912 |
Goalw [lex_def]
|
nipkow@5281
|
913 |
"lex r = \
|
nipkow@5281
|
914 |
\ {(xs,ys). length xs = length ys & \
|
nipkow@5281
|
915 |
\ (? xys x y xs' ys'. xs= xys @ x#xs' & ys= xys @ y#ys' & (x,y):r)}";
|
oheimb@5296
|
916 |
by(force_tac (claset(), simpset() delsimps [length_Suc_conv] addsimps [lexn_conv]) 1);
|
nipkow@5281
|
917 |
qed "lex_conv";
|
nipkow@5281
|
918 |
|
nipkow@5281
|
919 |
Goalw [lexico_def] "wf r ==> wf(lexico r)";
|
nipkow@5281
|
920 |
by(Blast_tac 1);
|
nipkow@5281
|
921 |
qed "wf_lexico";
|
nipkow@5281
|
922 |
AddSIs [wf_lexico];
|
nipkow@5281
|
923 |
|
nipkow@5281
|
924 |
Goalw
|
nipkow@5281
|
925 |
[lexico_def,diag_def,lex_prod_def,measure_def,inv_image_def]
|
nipkow@5281
|
926 |
"lexico r = {(xs,ys). length xs < length ys | \
|
nipkow@5281
|
927 |
\ length xs = length ys & (xs,ys) : lex r}";
|
nipkow@5281
|
928 |
by(Simp_tac 1);
|
nipkow@5281
|
929 |
qed "lexico_conv";
|
nipkow@5281
|
930 |
|
nipkow@5283
|
931 |
Goal "([],ys) ~: lex r";
|
nipkow@5283
|
932 |
by(simp_tac (simpset() addsimps [lex_conv]) 1);
|
nipkow@5283
|
933 |
qed "Nil_notin_lex";
|
nipkow@5283
|
934 |
|
nipkow@5283
|
935 |
Goal "(xs,[]) ~: lex r";
|
nipkow@5283
|
936 |
by(simp_tac (simpset() addsimps [lex_conv]) 1);
|
nipkow@5283
|
937 |
qed "Nil2_notin_lex";
|
nipkow@5283
|
938 |
|
nipkow@5283
|
939 |
AddIffs [Nil_notin_lex,Nil2_notin_lex];
|
nipkow@5283
|
940 |
|
nipkow@5283
|
941 |
Goal "((x#xs,y#ys) : lex r) = \
|
nipkow@5283
|
942 |
\ ((x,y) : r & length xs = length ys | x=y & (xs,ys) : lex r)";
|
nipkow@5283
|
943 |
by(simp_tac (simpset() addsimps [lex_conv]) 1);
|
nipkow@5283
|
944 |
br iffI 1;
|
nipkow@5283
|
945 |
by(blast_tac (claset() addIs [Cons_eq_appendI]) 2);
|
nipkow@5283
|
946 |
by(REPEAT(eresolve_tac [conjE, exE] 1));
|
nipkow@5283
|
947 |
by(exhaust_tac "xys" 1);
|
nipkow@5283
|
948 |
by(Asm_full_simp_tac 1);
|
nipkow@5283
|
949 |
by(Asm_full_simp_tac 1);
|
nipkow@5283
|
950 |
by(Blast_tac 1);
|
nipkow@5283
|
951 |
qed "Cons_in_lex";
|
nipkow@5283
|
952 |
AddIffs [Cons_in_lex];
|
nipkow@5283
|
953 |
|
nipkow@5283
|
954 |
|
nipkow@5162
|
955 |
(***
|
nipkow@5162
|
956 |
Simplification procedure for all list equalities.
|
nipkow@5162
|
957 |
Currently only tries to rearranges @ to see if
|
nipkow@5162
|
958 |
- both lists end in a singleton list,
|
nipkow@5162
|
959 |
- or both lists end in the same list.
|
nipkow@5162
|
960 |
***)
|
nipkow@5162
|
961 |
local
|
nipkow@5162
|
962 |
|
nipkow@5162
|
963 |
val list_eq_pattern =
|
nipkow@5162
|
964 |
read_cterm (sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);
|
nipkow@5162
|
965 |
|
berghofe@5183
|
966 |
fun last (cons as Const("List.list.op #",_) $ _ $ xs) =
|
berghofe@5183
|
967 |
(case xs of Const("List.list.[]",_) => cons | _ => last xs)
|
nipkow@5200
|
968 |
| last (Const("List.op @",_) $ _ $ ys) = last ys
|
nipkow@5162
|
969 |
| last t = t;
|
nipkow@5162
|
970 |
|
berghofe@5183
|
971 |
fun list1 (Const("List.list.op #",_) $ _ $ Const("List.list.[]",_)) = true
|
nipkow@5162
|
972 |
| list1 _ = false;
|
nipkow@5162
|
973 |
|
berghofe@5183
|
974 |
fun butlast ((cons as Const("List.list.op #",_) $ x) $ xs) =
|
berghofe@5183
|
975 |
(case xs of Const("List.list.[]",_) => xs | _ => cons $ butlast xs)
|
nipkow@5200
|
976 |
| butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
|
berghofe@5183
|
977 |
| butlast xs = Const("List.list.[]",fastype_of xs);
|
nipkow@5162
|
978 |
|
nipkow@5162
|
979 |
val rearr_tac =
|
nipkow@5162
|
980 |
simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons]);
|
nipkow@5162
|
981 |
|
nipkow@5162
|
982 |
fun list_eq sg _ (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
|
nipkow@5162
|
983 |
let
|
nipkow@5162
|
984 |
val lastl = last lhs and lastr = last rhs
|
nipkow@5162
|
985 |
fun rearr conv =
|
nipkow@5162
|
986 |
let val lhs1 = butlast lhs and rhs1 = butlast rhs
|
nipkow@5162
|
987 |
val Type(_,listT::_) = eqT
|
nipkow@5162
|
988 |
val appT = [listT,listT] ---> listT
|
nipkow@5200
|
989 |
val app = Const("List.op @",appT)
|
nipkow@5162
|
990 |
val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
|
nipkow@5162
|
991 |
val ct = cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(F,F2)))
|
nipkow@5162
|
992 |
val thm = prove_goalw_cterm [] ct (K [rearr_tac 1])
|
nipkow@5162
|
993 |
handle ERROR =>
|
nipkow@5162
|
994 |
error("The error(s) above occurred while trying to prove " ^
|
nipkow@5162
|
995 |
string_of_cterm ct)
|
nipkow@5162
|
996 |
in Some((conv RS (thm RS trans)) RS eq_reflection) end
|
nipkow@5162
|
997 |
|
nipkow@5162
|
998 |
in if list1 lastl andalso list1 lastr
|
nipkow@5162
|
999 |
then rearr append1_eq_conv
|
nipkow@5162
|
1000 |
else
|
nipkow@5162
|
1001 |
if lastl aconv lastr
|
nipkow@5162
|
1002 |
then rearr append_same_eq
|
nipkow@5162
|
1003 |
else None
|
nipkow@5162
|
1004 |
end;
|
nipkow@5162
|
1005 |
in
|
nipkow@5162
|
1006 |
val list_eq_simproc = mk_simproc "list_eq" [list_eq_pattern] list_eq;
|
nipkow@5162
|
1007 |
end;
|
nipkow@5162
|
1008 |
|
nipkow@5162
|
1009 |
Addsimprocs [list_eq_simproc];
|