author | nipkow |
Mon, 30 Jun 1997 12:08:19 +0200 | |
changeset 3467 | a0797ba03dfe |
parent 3465 | e85c24717cad |
child 3468 | 1f972dc8eafb |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/List |
923 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Tobias Nipkow |
923 | 4 |
Copyright 1994 TU Muenchen |
5 |
||
6 |
List lemmas |
|
7 |
*) |
|
8 |
||
3011 | 9 |
goal thy "!x. xs ~= x#xs"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
10 |
by (induct_tac "xs" 1); |
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
11 |
by (ALLGOALS Asm_simp_tac); |
2608 | 12 |
qed_spec_mp "not_Cons_self"; |
2512 | 13 |
Addsimps [not_Cons_self]; |
923 | 14 |
|
3011 | 15 |
goal thy "(xs ~= []) = (? y ys. xs = y#ys)"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
16 |
by (induct_tac "xs" 1); |
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
17 |
by (Simp_tac 1); |
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
18 |
by (Asm_simp_tac 1); |
923 | 19 |
qed "neq_Nil_conv"; |
20 |
||
21 |
||
3342
ec3b55fcb165
New operator "lists" for formalizing sets of lists
paulson
parents:
3292
diff
changeset
|
22 |
(** List operator over sets **) |
ec3b55fcb165
New operator "lists" for formalizing sets of lists
paulson
parents:
3292
diff
changeset
|
23 |
|
ec3b55fcb165
New operator "lists" for formalizing sets of lists
paulson
parents:
3292
diff
changeset
|
24 |
goalw thy lists.defs "!!A B. A<=B ==> lists A <= lists B"; |
ec3b55fcb165
New operator "lists" for formalizing sets of lists
paulson
parents:
3292
diff
changeset
|
25 |
by (rtac lfp_mono 1); |
ec3b55fcb165
New operator "lists" for formalizing sets of lists
paulson
parents:
3292
diff
changeset
|
26 |
by (REPEAT (ares_tac basic_monos 1)); |
ec3b55fcb165
New operator "lists" for formalizing sets of lists
paulson
parents:
3292
diff
changeset
|
27 |
qed "lists_mono"; |
3196 | 28 |
|
29 |
||
2608 | 30 |
(** list_case **) |
31 |
||
3011 | 32 |
goal thy |
2608 | 33 |
"P(list_case a f xs) = ((xs=[] --> P(a)) & \ |
2891 | 34 |
\ (!y ys. xs=y#ys --> P(f y ys)))"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
35 |
by (induct_tac "xs" 1); |
2608 | 36 |
by (ALLGOALS Asm_simp_tac); |
2891 | 37 |
by (Blast_tac 1); |
2608 | 38 |
qed "expand_list_case"; |
39 |
||
3011 | 40 |
val prems = goal thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)"; |
3457 | 41 |
by (induct_tac "xs" 1); |
42 |
by (REPEAT(resolve_tac prems 1)); |
|
2608 | 43 |
qed "list_cases"; |
44 |
||
3011 | 45 |
goal thy "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
46 |
by (induct_tac "xs" 1); |
2891 | 47 |
by (Blast_tac 1); |
48 |
by (Blast_tac 1); |
|
2608 | 49 |
bind_thm("list_eq_cases", |
50 |
impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp)))))); |
|
51 |
||
52 |
||
923 | 53 |
(** @ - append **) |
54 |
||
3467 | 55 |
section "@ - append"; |
56 |
||
3011 | 57 |
goal thy "(xs@ys)@zs = xs@(ys@zs)"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
58 |
by (induct_tac "xs" 1); |
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
59 |
by (ALLGOALS Asm_simp_tac); |
923 | 60 |
qed "append_assoc"; |
2512 | 61 |
Addsimps [append_assoc]; |
923 | 62 |
|
3011 | 63 |
goal thy "xs @ [] = xs"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
64 |
by (induct_tac "xs" 1); |
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
65 |
by (ALLGOALS Asm_simp_tac); |
923 | 66 |
qed "append_Nil2"; |
2512 | 67 |
Addsimps [append_Nil2]; |
923 | 68 |
|
3011 | 69 |
goal thy "(xs@ys = []) = (xs=[] & ys=[])"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
70 |
by (induct_tac "xs" 1); |
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
71 |
by (ALLGOALS Asm_simp_tac); |
2608 | 72 |
qed "append_is_Nil_conv"; |
73 |
AddIffs [append_is_Nil_conv]; |
|
74 |
||
3011 | 75 |
goal thy "([] = xs@ys) = (xs=[] & ys=[])"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
76 |
by (induct_tac "xs" 1); |
2608 | 77 |
by (ALLGOALS Asm_simp_tac); |
3457 | 78 |
by (Blast_tac 1); |
2608 | 79 |
qed "Nil_is_append_conv"; |
80 |
AddIffs [Nil_is_append_conv]; |
|
923 | 81 |
|
3011 | 82 |
goal thy "(xs @ ys = xs @ zs) = (ys=zs)"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
83 |
by (induct_tac "xs" 1); |
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
84 |
by (ALLGOALS Asm_simp_tac); |
923 | 85 |
qed "same_append_eq"; |
2608 | 86 |
AddIffs [same_append_eq]; |
87 |
||
3011 | 88 |
goal thy "!ys. (xs @ [x] = ys @ [y]) = (xs = ys & x = y)"; |
3457 | 89 |
by (induct_tac "xs" 1); |
90 |
by (rtac allI 1); |
|
91 |
by (induct_tac "ys" 1); |
|
92 |
by (ALLGOALS Asm_simp_tac); |
|
93 |
by (rtac allI 1); |
|
94 |
by (induct_tac "ys" 1); |
|
95 |
by (ALLGOALS Asm_simp_tac); |
|
2608 | 96 |
qed_spec_mp "append1_eq_conv"; |
97 |
AddIffs [append1_eq_conv]; |
|
98 |
||
3011 | 99 |
goal thy "xs ~= [] --> hd xs # tl xs = xs"; |
3457 | 100 |
by (induct_tac "xs" 1); |
101 |
by (ALLGOALS Asm_simp_tac); |
|
2608 | 102 |
qed_spec_mp "hd_Cons_tl"; |
103 |
Addsimps [hd_Cons_tl]; |
|
923 | 104 |
|
3011 | 105 |
goal thy "hd(xs@ys) = (if xs=[] then hd ys else hd xs)"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
106 |
by (induct_tac "xs" 1); |
1327
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset
|
107 |
by (ALLGOALS Asm_simp_tac); |
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset
|
108 |
qed "hd_append"; |
923 | 109 |
|
3011 | 110 |
goal thy "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)"; |
3457 | 111 |
by (simp_tac (!simpset setloop(split_tac[expand_list_case])) 1); |
2608 | 112 |
qed "tl_append"; |
113 |
||
114 |
(** map **) |
|
115 |
||
3467 | 116 |
section "map"; |
117 |
||
3011 | 118 |
goal thy |
3465 | 119 |
"(!x. x : set xs --> f x = g x) --> map f xs = map g xs"; |
3457 | 120 |
by (induct_tac "xs" 1); |
121 |
by (ALLGOALS Asm_simp_tac); |
|
2608 | 122 |
bind_thm("map_ext", impI RS (allI RS (result() RS mp))); |
123 |
||
3011 | 124 |
goal thy "map (%x.x) = (%xs.xs)"; |
2608 | 125 |
by (rtac ext 1); |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
126 |
by (induct_tac "xs" 1); |
2608 | 127 |
by (ALLGOALS Asm_simp_tac); |
128 |
qed "map_ident"; |
|
129 |
Addsimps[map_ident]; |
|
130 |
||
3011 | 131 |
goal thy "map f (xs@ys) = map f xs @ map f ys"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
132 |
by (induct_tac "xs" 1); |
2608 | 133 |
by (ALLGOALS Asm_simp_tac); |
134 |
qed "map_append"; |
|
135 |
Addsimps[map_append]; |
|
136 |
||
3011 | 137 |
goalw thy [o_def] "map (f o g) xs = map f (map g xs)"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
138 |
by (induct_tac "xs" 1); |
2608 | 139 |
by (ALLGOALS Asm_simp_tac); |
140 |
qed "map_compose"; |
|
141 |
Addsimps[map_compose]; |
|
142 |
||
3011 | 143 |
goal thy "rev(map f xs) = map f (rev xs)"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
144 |
by (induct_tac "xs" 1); |
2608 | 145 |
by (ALLGOALS Asm_simp_tac); |
146 |
qed "rev_map"; |
|
147 |
||
1169 | 148 |
(** rev **) |
149 |
||
3467 | 150 |
section "rev"; |
151 |
||
3011 | 152 |
goal thy "rev(xs@ys) = rev(ys) @ rev(xs)"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
153 |
by (induct_tac "xs" 1); |
2512 | 154 |
by (ALLGOALS Asm_simp_tac); |
1169 | 155 |
qed "rev_append"; |
2512 | 156 |
Addsimps[rev_append]; |
1169 | 157 |
|
3011 | 158 |
goal thy "rev(rev l) = l"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
159 |
by (induct_tac "l" 1); |
2512 | 160 |
by (ALLGOALS Asm_simp_tac); |
1169 | 161 |
qed "rev_rev_ident"; |
2512 | 162 |
Addsimps[rev_rev_ident]; |
1169 | 163 |
|
2608 | 164 |
|
923 | 165 |
(** mem **) |
166 |
||
3467 | 167 |
section "mem"; |
168 |
||
3011 | 169 |
goal thy "x mem (xs@ys) = (x mem xs | x mem ys)"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
170 |
by (induct_tac "xs" 1); |
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
171 |
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
923 | 172 |
qed "mem_append"; |
2512 | 173 |
Addsimps[mem_append]; |
923 | 174 |
|
3011 | 175 |
goal thy "x mem [x:xs.P(x)] = (x mem xs & P(x))"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
176 |
by (induct_tac "xs" 1); |
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
177 |
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
923 | 178 |
qed "mem_filter"; |
2512 | 179 |
Addsimps[mem_filter]; |
923 | 180 |
|
3465 | 181 |
(** set **) |
1812 | 182 |
|
3467 | 183 |
section "set"; |
184 |
||
3465 | 185 |
goal thy "set (xs@ys) = (set xs Un set ys)"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
186 |
by (induct_tac "xs" 1); |
1812 | 187 |
by (ALLGOALS Asm_simp_tac); |
1908 | 188 |
qed "set_of_list_append"; |
2512 | 189 |
Addsimps[set_of_list_append]; |
1812 | 190 |
|
3465 | 191 |
goal thy "(x mem xs) = (x: set xs)"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
192 |
by (induct_tac "xs" 1); |
1812 | 193 |
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
2891 | 194 |
by (Blast_tac 1); |
1908 | 195 |
qed "set_of_list_mem_eq"; |
1812 | 196 |
|
3465 | 197 |
goal thy "set l <= set (x#l)"; |
1936 | 198 |
by (Simp_tac 1); |
2891 | 199 |
by (Blast_tac 1); |
1936 | 200 |
qed "set_of_list_subset_Cons"; |
201 |
||
3465 | 202 |
goal thy "(set xs = {}) = (xs = [])"; |
3457 | 203 |
by (induct_tac "xs" 1); |
204 |
by (ALLGOALS Asm_simp_tac); |
|
2608 | 205 |
qed "set_of_list_empty"; |
206 |
Addsimps [set_of_list_empty]; |
|
207 |
||
3465 | 208 |
goal thy "set(rev xs) = set(xs)"; |
3457 | 209 |
by (induct_tac "xs" 1); |
210 |
by (ALLGOALS Asm_simp_tac); |
|
2608 | 211 |
qed "set_of_list_rev"; |
212 |
Addsimps [set_of_list_rev]; |
|
213 |
||
3465 | 214 |
goal thy "set(map f xs) = f``(set xs)"; |
3457 | 215 |
by (induct_tac "xs" 1); |
216 |
by (ALLGOALS Asm_simp_tac); |
|
2608 | 217 |
qed "set_of_list_map"; |
218 |
Addsimps [set_of_list_map]; |
|
219 |
||
1812 | 220 |
|
923 | 221 |
(** list_all **) |
222 |
||
3467 | 223 |
section "list_all"; |
224 |
||
3011 | 225 |
goal thy "list_all (%x.True) xs = True"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
226 |
by (induct_tac "xs" 1); |
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
227 |
by (ALLGOALS Asm_simp_tac); |
923 | 228 |
qed "list_all_True"; |
2512 | 229 |
Addsimps [list_all_True]; |
923 | 230 |
|
3011 | 231 |
goal thy "list_all p (xs@ys) = (list_all p xs & list_all p ys)"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
232 |
by (induct_tac "xs" 1); |
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
233 |
by (ALLGOALS Asm_simp_tac); |
2512 | 234 |
qed "list_all_append"; |
235 |
Addsimps [list_all_append]; |
|
923 | 236 |
|
3011 | 237 |
goal thy "list_all P xs = (!x. x mem xs --> P(x))"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
238 |
by (induct_tac "xs" 1); |
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
239 |
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
2891 | 240 |
by (Blast_tac 1); |
923 | 241 |
qed "list_all_mem_conv"; |
242 |
||
243 |
||
2608 | 244 |
(** filter **) |
923 | 245 |
|
3467 | 246 |
section "filter"; |
247 |
||
3383
7707cb7a5054
Corrected statement of filter_append; added filter_size
paulson
parents:
3342
diff
changeset
|
248 |
goal thy "filter P (xs@ys) = filter P xs @ filter P ys"; |
3457 | 249 |
by (induct_tac "xs" 1); |
250 |
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
|
2608 | 251 |
qed "filter_append"; |
252 |
Addsimps [filter_append]; |
|
253 |
||
3383
7707cb7a5054
Corrected statement of filter_append; added filter_size
paulson
parents:
3342
diff
changeset
|
254 |
goal thy "size (filter P xs) <= size xs"; |
3457 | 255 |
by (induct_tac "xs" 1); |
256 |
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
|
3383
7707cb7a5054
Corrected statement of filter_append; added filter_size
paulson
parents:
3342
diff
changeset
|
257 |
qed "filter_size"; |
7707cb7a5054
Corrected statement of filter_append; added filter_size
paulson
parents:
3342
diff
changeset
|
258 |
|
2608 | 259 |
|
260 |
(** concat **) |
|
261 |
||
3467 | 262 |
section "concat"; |
263 |
||
3011 | 264 |
goal thy "concat(xs@ys) = concat(xs)@concat(ys)"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
265 |
by (induct_tac "xs" 1); |
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
266 |
by (ALLGOALS Asm_simp_tac); |
2608 | 267 |
qed"concat_append"; |
268 |
Addsimps [concat_append]; |
|
2512 | 269 |
|
3467 | 270 |
goal thy "set(concat xs) = Union(set `` set xs)"; |
271 |
by (induct_tac "xs" 1); |
|
272 |
by (ALLGOALS Asm_simp_tac); |
|
273 |
qed"set_of_list_concat"; |
|
274 |
Addsimps [set_of_list_concat]; |
|
275 |
||
276 |
goal thy "map f (concat xs) = concat (map (map f) xs)"; |
|
277 |
by (induct_tac "xs" 1); |
|
278 |
by (ALLGOALS Asm_simp_tac); |
|
279 |
qed "map_concat"; |
|
280 |
||
281 |
goal thy "filter p (concat xs) = concat (map (filter p) xs)"; |
|
282 |
by (induct_tac "xs" 1); |
|
283 |
by (ALLGOALS Asm_simp_tac); |
|
284 |
qed"filter_concat"; |
|
285 |
||
286 |
goal thy "rev(concat xs) = concat (map rev (rev xs))"; |
|
287 |
by (induct_tac "xs" 1); |
|
2512 | 288 |
by (ALLGOALS Asm_simp_tac); |
2608 | 289 |
qed "rev_concat"; |
923 | 290 |
|
962 | 291 |
(** length **) |
292 |
||
3467 | 293 |
section "length"; |
294 |
||
3011 | 295 |
goal thy "length(xs@ys) = length(xs)+length(ys)"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
296 |
by (induct_tac "xs" 1); |
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
297 |
by (ALLGOALS Asm_simp_tac); |
962 | 298 |
qed"length_append"; |
1301 | 299 |
Addsimps [length_append]; |
300 |
||
3011 | 301 |
goal thy "length (map f l) = length l"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
302 |
by (induct_tac "l" 1); |
1301 | 303 |
by (ALLGOALS Simp_tac); |
304 |
qed "length_map"; |
|
305 |
Addsimps [length_map]; |
|
962 | 306 |
|
3011 | 307 |
goal thy "length(rev xs) = length(xs)"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
308 |
by (induct_tac "xs" 1); |
1301 | 309 |
by (ALLGOALS Asm_simp_tac); |
1169 | 310 |
qed "length_rev"; |
1301 | 311 |
Addsimps [length_rev]; |
1169 | 312 |
|
3011 | 313 |
goal thy "(length xs = 0) = (xs = [])"; |
3457 | 314 |
by (induct_tac "xs" 1); |
315 |
by (ALLGOALS Asm_simp_tac); |
|
2608 | 316 |
qed "length_0_conv"; |
317 |
AddIffs [length_0_conv]; |
|
318 |
||
3011 | 319 |
goal thy "(0 < length xs) = (xs ~= [])"; |
3457 | 320 |
by (induct_tac "xs" 1); |
321 |
by (ALLGOALS Asm_simp_tac); |
|
2608 | 322 |
qed "length_greater_0_conv"; |
323 |
AddIffs [length_greater_0_conv]; |
|
324 |
||
325 |
||
923 | 326 |
(** nth **) |
327 |
||
3467 | 328 |
section "nth"; |
329 |
||
3011 | 330 |
goal thy |
2608 | 331 |
"!xs. nth n (xs@ys) = \ |
332 |
\ (if n < length xs then nth n xs else nth (n - length xs) ys)"; |
|
3457 | 333 |
by (nat_ind_tac "n" 1); |
334 |
by (Asm_simp_tac 1); |
|
335 |
by (rtac allI 1); |
|
336 |
by (exhaust_tac "xs" 1); |
|
337 |
by (ALLGOALS Asm_simp_tac); |
|
338 |
by (rtac allI 1); |
|
339 |
by (exhaust_tac "xs" 1); |
|
340 |
by (ALLGOALS Asm_simp_tac); |
|
2608 | 341 |
qed_spec_mp "nth_append"; |
342 |
||
3011 | 343 |
goal thy "!n. n < length xs --> nth n (map f xs) = f (nth n xs)"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
344 |
by (induct_tac "xs" 1); |
1301 | 345 |
(* case [] *) |
346 |
by (Asm_full_simp_tac 1); |
|
347 |
(* case x#xl *) |
|
348 |
by (rtac allI 1); |
|
349 |
by (nat_ind_tac "n" 1); |
|
350 |
by (ALLGOALS Asm_full_simp_tac); |
|
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset
|
351 |
qed_spec_mp "nth_map"; |
1301 | 352 |
Addsimps [nth_map]; |
353 |
||
3011 | 354 |
goal thy "!n. n < length xs --> list_all P xs --> P(nth n xs)"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
355 |
by (induct_tac "xs" 1); |
1301 | 356 |
(* case [] *) |
357 |
by (Simp_tac 1); |
|
358 |
(* case x#xl *) |
|
359 |
by (rtac allI 1); |
|
360 |
by (nat_ind_tac "n" 1); |
|
361 |
by (ALLGOALS Asm_full_simp_tac); |
|
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset
|
362 |
qed_spec_mp "list_all_nth"; |
1301 | 363 |
|
3011 | 364 |
goal thy "!n. n < length xs --> (nth n xs) mem xs"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
365 |
by (induct_tac "xs" 1); |
1301 | 366 |
(* case [] *) |
367 |
by (Simp_tac 1); |
|
368 |
(* case x#xl *) |
|
369 |
by (rtac allI 1); |
|
370 |
by (nat_ind_tac "n" 1); |
|
371 |
(* case 0 *) |
|
372 |
by (Asm_full_simp_tac 1); |
|
373 |
(* case Suc x *) |
|
374 |
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
|
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1465
diff
changeset
|
375 |
qed_spec_mp "nth_mem"; |
1301 | 376 |
Addsimps [nth_mem]; |
377 |
||
1327
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset
|
378 |
|
2608 | 379 |
(** take & drop **) |
380 |
section "take & drop"; |
|
1327
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset
|
381 |
|
1419
a6a034a47a71
defined take/drop by induction over list rather than nat.
nipkow
parents:
1327
diff
changeset
|
382 |
goal thy "take 0 xs = []"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
383 |
by (induct_tac "xs" 1); |
1419
a6a034a47a71
defined take/drop by induction over list rather than nat.
nipkow
parents:
1327
diff
changeset
|
384 |
by (ALLGOALS Asm_simp_tac); |
1327
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset
|
385 |
qed "take_0"; |
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset
|
386 |
|
2608 | 387 |
goal thy "drop 0 xs = xs"; |
3040
7d48671753da
Introduced a generic "induct_tac" which picks up the right induction scheme
nipkow
parents:
3011
diff
changeset
|
388 |
by (induct_tac "xs" 1); |
2608 | 389 |
by (ALLGOALS Asm_simp_tac); |
390 |
qed "drop_0"; |
|
391 |
||
1419
a6a034a47a71
defined take/drop by induction over list rather than nat.
nipkow
parents:
1327
diff
changeset
|
392 |
goal thy "take (Suc n) (x#xs) = x # take n xs"; |
1552 | 393 |
by (Simp_tac 1); |
1419
a6a034a47a71
defined take/drop by induction over list rather than nat.
nipkow
parents:
1327
diff
changeset
|
394 |
qed "take_Suc_Cons"; |
1327
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset
|
395 |
|
2608 | 396 |
goal thy "drop (Suc n) (x#xs) = drop n xs"; |
397 |
by (Simp_tac 1); |
|
398 |
qed "drop_Suc_Cons"; |
|
399 |
||
400 |
Delsimps [take_Cons,drop_Cons]; |
|
401 |
Addsimps [take_0,take_Suc_Cons,drop_0,drop_Suc_Cons]; |
|
402 |
||
3011 | 403 |
goal thy "!xs. length(take n xs) = min (length xs) n"; |
3457 | 404 |
by (nat_ind_tac "n" 1); |
405 |
by (ALLGOALS Asm_simp_tac); |
|
406 |
by (rtac allI 1); |
|
407 |
by (exhaust_tac "xs" 1); |
|
408 |
by (ALLGOALS Asm_simp_tac); |
|
2608 | 409 |
qed_spec_mp "length_take"; |
410 |
Addsimps [length_take]; |
|
923 | 411 |
|
3011 | 412 |
goal thy "!xs. length(drop n xs) = (length xs - n)"; |
3457 | 413 |
by (nat_ind_tac "n" 1); |
414 |
by (ALLGOALS Asm_simp_tac); |
|
415 |
by (rtac allI 1); |
|
416 |
by (exhaust_tac "xs" 1); |
|
417 |
by (ALLGOALS Asm_simp_tac); |
|
2608 | 418 |
qed_spec_mp "length_drop"; |
419 |
Addsimps [length_drop]; |
|
420 |
||
3011 | 421 |
goal thy "!xs. length xs <= n --> take n xs = xs"; |
3457 | 422 |
by (nat_ind_tac "n" 1); |
423 |
by (ALLGOALS Asm_simp_tac); |
|
424 |
by (rtac allI 1); |
|
425 |
by (exhaust_tac "xs" 1); |
|
426 |
by (ALLGOALS Asm_simp_tac); |
|
2608 | 427 |
qed_spec_mp "take_all"; |
923 | 428 |
|
3011 | 429 |
goal thy "!xs. length xs <= n --> drop n xs = []"; |
3457 | 430 |
by (nat_ind_tac "n" 1); |
431 |
by (ALLGOALS Asm_simp_tac); |
|
432 |
by (rtac allI 1); |
|
433 |
by (exhaust_tac "xs" 1); |
|
434 |
by (ALLGOALS Asm_simp_tac); |
|
2608 | 435 |
qed_spec_mp "drop_all"; |
436 |
||
3011 | 437 |
goal thy |
2608 | 438 |
"!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)"; |
3457 | 439 |
by (nat_ind_tac "n" 1); |
440 |
by (ALLGOALS Asm_simp_tac); |
|
441 |
by (rtac allI 1); |
|
442 |
by (exhaust_tac "xs" 1); |
|
443 |
by (ALLGOALS Asm_simp_tac); |
|
2608 | 444 |
qed_spec_mp "take_append"; |
445 |
Addsimps [take_append]; |
|
446 |
||
3011 | 447 |
goal thy "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys"; |
3457 | 448 |
by (nat_ind_tac "n" 1); |
449 |
by (ALLGOALS Asm_simp_tac); |
|
450 |
by (rtac allI 1); |
|
451 |
by (exhaust_tac "xs" 1); |
|
452 |
by (ALLGOALS Asm_simp_tac); |
|
2608 | 453 |
qed_spec_mp "drop_append"; |
454 |
Addsimps [drop_append]; |
|
455 |
||
3011 | 456 |
goal thy "!xs n. take n (take m xs) = take (min n m) xs"; |
3457 | 457 |
by (nat_ind_tac "m" 1); |
458 |
by (ALLGOALS Asm_simp_tac); |
|
459 |
by (rtac allI 1); |
|
460 |
by (exhaust_tac "xs" 1); |
|
461 |
by (ALLGOALS Asm_simp_tac); |
|
462 |
by (rtac allI 1); |
|
463 |
by (exhaust_tac "n" 1); |
|
464 |
by (ALLGOALS Asm_simp_tac); |
|
2608 | 465 |
qed_spec_mp "take_take"; |
466 |
||
3011 | 467 |
goal thy "!xs. drop n (drop m xs) = drop (n + m) xs"; |
3457 | 468 |
by (nat_ind_tac "m" 1); |
469 |
by (ALLGOALS Asm_simp_tac); |
|
470 |
by (rtac allI 1); |
|
471 |
by (exhaust_tac "xs" 1); |
|
472 |
by (ALLGOALS Asm_simp_tac); |
|
2608 | 473 |
qed_spec_mp "drop_drop"; |
923 | 474 |
|
3011 | 475 |
goal thy "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; |
3457 | 476 |
by (nat_ind_tac "m" 1); |
477 |
by (ALLGOALS Asm_simp_tac); |
|
478 |
by (rtac allI 1); |
|
479 |
by (exhaust_tac "xs" 1); |
|
480 |
by (ALLGOALS Asm_simp_tac); |
|
2608 | 481 |
qed_spec_mp "take_drop"; |
482 |
||
3011 | 483 |
goal thy "!xs. take n (map f xs) = map f (take n xs)"; |
3457 | 484 |
by (nat_ind_tac "n" 1); |
485 |
by (ALLGOALS Asm_simp_tac); |
|
486 |
by (rtac allI 1); |
|
487 |
by (exhaust_tac "xs" 1); |
|
488 |
by (ALLGOALS Asm_simp_tac); |
|
2608 | 489 |
qed_spec_mp "take_map"; |
490 |
||
3011 | 491 |
goal thy "!xs. drop n (map f xs) = map f (drop n xs)"; |
3457 | 492 |
by (nat_ind_tac "n" 1); |
493 |
by (ALLGOALS Asm_simp_tac); |
|
494 |
by (rtac allI 1); |
|
495 |
by (exhaust_tac "xs" 1); |
|
496 |
by (ALLGOALS Asm_simp_tac); |
|
2608 | 497 |
qed_spec_mp "drop_map"; |
498 |
||
3283
0db086394024
Replaced res_inst-list_cases by generic exhaust_tac.
nipkow
parents:
3196
diff
changeset
|
499 |
goal thy "!n i. i < n --> nth i (take n xs) = nth i xs"; |
3457 | 500 |
by (induct_tac "xs" 1); |
501 |
by (ALLGOALS Asm_simp_tac); |
|
502 |
by (strip_tac 1); |
|
503 |
by (exhaust_tac "n" 1); |
|
504 |
by (Blast_tac 1); |
|
505 |
by (exhaust_tac "i" 1); |
|
506 |
by (ALLGOALS Asm_full_simp_tac); |
|
2608 | 507 |
qed_spec_mp "nth_take"; |
508 |
Addsimps [nth_take]; |
|
923 | 509 |
|
3283
0db086394024
Replaced res_inst-list_cases by generic exhaust_tac.
nipkow
parents:
3196
diff
changeset
|
510 |
goal thy "!xs i. n + i < length xs --> nth i (drop n xs) = nth (n + i) xs"; |
3457 | 511 |
by (nat_ind_tac "n" 1); |
512 |
by (ALLGOALS Asm_simp_tac); |
|
513 |
by (rtac allI 1); |
|
514 |
by (exhaust_tac "xs" 1); |
|
515 |
by (ALLGOALS Asm_simp_tac); |
|
2608 | 516 |
qed_spec_mp "nth_drop"; |
517 |
Addsimps [nth_drop]; |
|
518 |
||
519 |
(** takeWhile & dropWhile **) |
|
520 |
||
3467 | 521 |
section "takeWhile & dropWhile"; |
522 |
||
3011 | 523 |
goal thy |
3465 | 524 |
"x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs"; |
3457 | 525 |
by (induct_tac "xs" 1); |
526 |
by (Simp_tac 1); |
|
527 |
by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1); |
|
528 |
by (Blast_tac 1); |
|
2608 | 529 |
bind_thm("takeWhile_append1", conjI RS (result() RS mp)); |
530 |
Addsimps [takeWhile_append1]; |
|
923 | 531 |
|
3011 | 532 |
goal thy |
3465 | 533 |
"(!x:set xs.P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys"; |
3457 | 534 |
by (induct_tac "xs" 1); |
535 |
by (Simp_tac 1); |
|
536 |
by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1); |
|
2608 | 537 |
bind_thm("takeWhile_append2", ballI RS (result() RS mp)); |
538 |
Addsimps [takeWhile_append2]; |
|
1169 | 539 |
|
3011 | 540 |
goal thy |
3465 | 541 |
"x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"; |
3457 | 542 |
by (induct_tac "xs" 1); |
543 |
by (Simp_tac 1); |
|
544 |
by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1); |
|
545 |
by (Blast_tac 1); |
|
2608 | 546 |
bind_thm("dropWhile_append1", conjI RS (result() RS mp)); |
547 |
Addsimps [dropWhile_append1]; |
|
548 |
||
3011 | 549 |
goal thy |
3465 | 550 |
"(!x:set xs.P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys"; |
3457 | 551 |
by (induct_tac "xs" 1); |
552 |
by (Simp_tac 1); |
|
553 |
by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1); |
|
2608 | 554 |
bind_thm("dropWhile_append2", ballI RS (result() RS mp)); |
555 |
Addsimps [dropWhile_append2]; |
|
556 |
||
3465 | 557 |
goal thy "x:set(takeWhile P xs) --> x:set xs & P x"; |
3457 | 558 |
by (induct_tac "xs" 1); |
559 |
by (Simp_tac 1); |
|
560 |
by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1); |
|
2608 | 561 |
qed_spec_mp"set_of_list_take_whileD"; |
562 |