author | paulson |
Thu, 18 Jul 2002 10:37:55 +0200 | |
changeset 13387 | b7464ca2ebbb |
parent 13356 | c9cfe1638bf2 |
child 13396 | 11219ca224ab |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/List |
516 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
516 | 4 |
Copyright 1994 University of Cambridge |
5 |
||
6 |
*) |
|
7 |
||
13327 | 8 |
header{*Lists in Zermelo-Fraenkel Set Theory*} |
9 |
||
10 |
theory List = Datatype + ArithSimp: |
|
516 | 11 |
|
12 |
consts |
|
12789 | 13 |
list :: "i=>i" |
13327 | 14 |
|
516 | 15 |
datatype |
581 | 16 |
"list(A)" = Nil | Cons ("a:A", "l: list(A)") |
516 | 17 |
|
18 |
||
2539 | 19 |
syntax |
20 |
"[]" :: i ("[]") |
|
12789 | 21 |
"@List" :: "is => i" ("[(_)]") |
2539 | 22 |
|
516 | 23 |
translations |
24 |
"[x, xs]" == "Cons(x, [xs])" |
|
25 |
"[x]" == "Cons(x, [])" |
|
26 |
"[]" == "Nil" |
|
27 |
||
28 |
||
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
29 |
consts |
12789 | 30 |
length :: "i=>i" |
31 |
hd :: "i=>i" |
|
32 |
tl :: "i=>i" |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
33 |
|
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
34 |
primrec |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
35 |
"length([]) = 0" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
36 |
"length(Cons(a,l)) = succ(length(l))" |
13327 | 37 |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
38 |
primrec |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
39 |
"hd(Cons(a,l)) = a" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
40 |
|
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
41 |
primrec |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
42 |
"tl([]) = []" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
43 |
"tl(Cons(a,l)) = l" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
44 |
|
6070 | 45 |
|
46 |
consts |
|
13327 | 47 |
map :: "[i=>i, i] => i" |
12789 | 48 |
set_of_list :: "i=>i" |
13327 | 49 |
app :: "[i,i]=>i" (infixr "@" 60) |
50 |
||
51 |
(*map is a binding operator -- it applies to meta-level functions, not |
|
52 |
object-level functions. This simplifies the final form of term_rec_conv, |
|
53 |
although complicating its derivation.*) |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
54 |
primrec |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
55 |
"map(f,[]) = []" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
56 |
"map(f,Cons(a,l)) = Cons(f(a), map(f,l))" |
13327 | 57 |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
58 |
primrec |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
59 |
"set_of_list([]) = 0" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
60 |
"set_of_list(Cons(a,l)) = cons(a, set_of_list(l))" |
13327 | 61 |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
62 |
primrec |
13327 | 63 |
app_Nil: "[] @ ys = ys" |
64 |
app_Cons: "(Cons(a,l)) @ ys = Cons(a, l @ ys)" |
|
65 |
||
6070 | 66 |
|
67 |
consts |
|
12789 | 68 |
rev :: "i=>i" |
69 |
flat :: "i=>i" |
|
70 |
list_add :: "i=>i" |
|
6070 | 71 |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
72 |
primrec |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
73 |
"rev([]) = []" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
74 |
"rev(Cons(a,l)) = rev(l) @ [a]" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
75 |
|
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
76 |
primrec |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
77 |
"flat([]) = []" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
78 |
"flat(Cons(l,ls)) = l @ flat(ls)" |
13327 | 79 |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
80 |
primrec |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
81 |
"list_add([]) = 0" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
82 |
"list_add(Cons(a,l)) = a #+ list_add(l)" |
13327 | 83 |
|
6070 | 84 |
consts |
12789 | 85 |
drop :: "[i,i]=>i" |
6070 | 86 |
|
87 |
primrec |
|
13327 | 88 |
drop_0: "drop(0,l) = l" |
13387 | 89 |
drop_succ: "drop(succ(i), l) = tl (drop(i,l))" |
516 | 90 |
|
12789 | 91 |
|
92 |
(*** Thanks to Sidi Ehmety for the following ***) |
|
93 |
||
94 |
constdefs |
|
95 |
(* Function `take' returns the first n elements of a list *) |
|
96 |
take :: "[i,i]=>i" |
|
97 |
"take(n, as) == list_rec(lam n:nat. [], |
|
98 |
%a l r. lam n:nat. nat_case([], %m. Cons(a, r`m), n), as)`n" |
|
13327 | 99 |
|
12789 | 100 |
nth :: "[i, i]=>i" |
13387 | 101 |
--{*returns the (n+1)th element of a list, or 0 if the |
102 |
list is too short.*} |
|
12789 | 103 |
"nth(n, as) == list_rec(lam n:nat. 0, |
13387 | 104 |
%a l r. lam n:nat. nat_case(a, %m. r`m, n), as) ` n" |
12789 | 105 |
|
106 |
list_update :: "[i, i, i]=>i" |
|
107 |
"list_update(xs, i, v) == list_rec(lam n:nat. Nil, |
|
108 |
%u us vs. lam n:nat. nat_case(Cons(v, us), %m. Cons(u, vs`m), n), xs)`i" |
|
109 |
||
110 |
consts |
|
111 |
filter :: "[i=>o, i] => i" |
|
112 |
upt :: "[i, i] =>i" |
|
113 |
||
114 |
primrec |
|
115 |
"filter(P, Nil) = Nil" |
|
116 |
"filter(P, Cons(x, xs)) = |
|
117 |
(if P(x) then Cons(x, filter(P, xs)) else filter(P, xs))" |
|
118 |
||
119 |
primrec |
|
120 |
"upt(i, 0) = Nil" |
|
121 |
"upt(i, succ(j)) = (if i le j then upt(i, j)@[j] else Nil)" |
|
122 |
||
123 |
constdefs |
|
124 |
min :: "[i,i] =>i" |
|
125 |
"min(x, y) == (if x le y then x else y)" |
|
13327 | 126 |
|
12789 | 127 |
max :: "[i, i] =>i" |
128 |
"max(x, y) == (if x le y then y else x)" |
|
129 |
||
13327 | 130 |
(*** Aspects of the datatype definition ***) |
131 |
||
132 |
declare list.intros [simp,TC] |
|
133 |
||
134 |
(*An elimination rule, for type-checking*) |
|
135 |
inductive_cases ConsE: "Cons(a,l) : list(A)" |
|
136 |
||
137 |
(*Proving freeness results*) |
|
138 |
lemma Cons_iff: "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'" |
|
139 |
by auto |
|
140 |
||
141 |
lemma Nil_Cons_iff: "~ Nil=Cons(a,l)" |
|
142 |
by auto |
|
143 |
||
144 |
lemma list_unfold: "list(A) = {0} + (A * list(A))" |
|
145 |
by (blast intro!: list.intros [unfolded list.con_defs] |
|
146 |
elim: list.cases [unfolded list.con_defs]) |
|
147 |
||
148 |
||
149 |
(** Lemmas to justify using "list" in other recursive type definitions **) |
|
150 |
||
151 |
lemma list_mono: "A<=B ==> list(A) <= list(B)" |
|
152 |
apply (unfold list.defs ) |
|
153 |
apply (rule lfp_mono) |
|
154 |
apply (simp_all add: list.bnd_mono) |
|
155 |
apply (assumption | rule univ_mono basic_monos)+ |
|
156 |
done |
|
157 |
||
158 |
(*There is a similar proof by list induction.*) |
|
159 |
lemma list_univ: "list(univ(A)) <= univ(A)" |
|
160 |
apply (unfold list.defs list.con_defs) |
|
161 |
apply (rule lfp_lowerbound) |
|
162 |
apply (rule_tac [2] A_subset_univ [THEN univ_mono]) |
|
163 |
apply (blast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ) |
|
164 |
done |
|
165 |
||
166 |
(*These two theorems justify datatypes involving list(nat), list(A), ...*) |
|
167 |
lemmas list_subset_univ = subset_trans [OF list_mono list_univ] |
|
168 |
||
169 |
lemma list_into_univ: "[| l: list(A); A <= univ(B) |] ==> l: univ(B)" |
|
170 |
by (blast intro: list_subset_univ [THEN subsetD]) |
|
171 |
||
172 |
lemma list_case_type: |
|
173 |
"[| l: list(A); |
|
174 |
c: C(Nil); |
|
175 |
!!x y. [| x: A; y: list(A) |] ==> h(x,y): C(Cons(x,y)) |
|
176 |
|] ==> list_case(c,h,l) : C(l)" |
|
13387 | 177 |
by (erule list.induct, auto) |
178 |
||
179 |
lemma list_0_triv: "list(0) = {Nil}" |
|
180 |
apply (rule equalityI, auto) |
|
181 |
apply (induct_tac x, auto) |
|
13327 | 182 |
done |
183 |
||
184 |
||
185 |
(*** List functions ***) |
|
186 |
||
187 |
lemma tl_type: "l: list(A) ==> tl(l) : list(A)" |
|
188 |
apply (induct_tac "l") |
|
189 |
apply (simp_all (no_asm_simp) add: list.intros) |
|
190 |
done |
|
191 |
||
192 |
(** drop **) |
|
193 |
||
194 |
lemma drop_Nil [simp]: "i:nat ==> drop(i, Nil) = Nil" |
|
195 |
apply (induct_tac "i") |
|
196 |
apply (simp_all (no_asm_simp)) |
|
197 |
done |
|
198 |
||
199 |
lemma drop_succ_Cons [simp]: "i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)" |
|
200 |
apply (rule sym) |
|
201 |
apply (induct_tac "i") |
|
202 |
apply (simp (no_asm)) |
|
203 |
apply (simp (no_asm_simp)) |
|
204 |
done |
|
205 |
||
206 |
lemma drop_type [simp,TC]: "[| i:nat; l: list(A) |] ==> drop(i,l) : list(A)" |
|
207 |
apply (induct_tac "i") |
|
208 |
apply (simp_all (no_asm_simp) add: tl_type) |
|
209 |
done |
|
210 |
||
13387 | 211 |
declare drop_succ [simp del] |
13327 | 212 |
|
213 |
||
214 |
(** Type checking -- proved by induction, as usual **) |
|
215 |
||
216 |
lemma list_rec_type [TC]: |
|
217 |
"[| l: list(A); |
|
218 |
c: C(Nil); |
|
219 |
!!x y r. [| x:A; y: list(A); r: C(y) |] ==> h(x,y,r): C(Cons(x,y)) |
|
220 |
|] ==> list_rec(c,h,l) : C(l)" |
|
221 |
by (induct_tac "l", auto) |
|
222 |
||
223 |
(** map **) |
|
224 |
||
225 |
lemma map_type [TC]: |
|
226 |
"[| l: list(A); !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)" |
|
227 |
apply (simp add: map_list_def) |
|
228 |
apply (typecheck add: list.intros list_rec_type, blast) |
|
229 |
done |
|
230 |
||
231 |
lemma map_type2 [TC]: "l: list(A) ==> map(h,l) : list({h(u). u:A})" |
|
232 |
apply (erule map_type) |
|
233 |
apply (erule RepFunI) |
|
234 |
done |
|
235 |
||
236 |
(** length **) |
|
237 |
||
238 |
lemma length_type [TC]: "l: list(A) ==> length(l) : nat" |
|
239 |
by (simp add: length_list_def) |
|
240 |
||
241 |
lemma lt_length_in_nat: |
|
242 |
"[|x < length(xs); xs \<in> list(A)|] ==> x \<in> nat" |
|
243 |
by (frule lt_nat_in_nat, typecheck) |
|
244 |
||
245 |
(** app **) |
|
246 |
||
247 |
lemma app_type [TC]: "[| xs: list(A); ys: list(A) |] ==> xs@ys : list(A)" |
|
248 |
by (simp add: app_list_def) |
|
249 |
||
250 |
(** rev **) |
|
251 |
||
252 |
lemma rev_type [TC]: "xs: list(A) ==> rev(xs) : list(A)" |
|
253 |
by (simp add: rev_list_def) |
|
254 |
||
255 |
||
256 |
(** flat **) |
|
257 |
||
258 |
lemma flat_type [TC]: "ls: list(list(A)) ==> flat(ls) : list(A)" |
|
259 |
by (simp add: flat_list_def) |
|
260 |
||
261 |
||
262 |
(** set_of_list **) |
|
263 |
||
264 |
lemma set_of_list_type [TC]: "l: list(A) ==> set_of_list(l) : Pow(A)" |
|
265 |
apply (unfold set_of_list_list_def) |
|
266 |
apply (erule list_rec_type, auto) |
|
267 |
done |
|
268 |
||
269 |
lemma set_of_list_append: |
|
270 |
"xs: list(A) ==> set_of_list (xs@ys) = set_of_list(xs) Un set_of_list(ys)" |
|
271 |
apply (erule list.induct) |
|
272 |
apply (simp_all (no_asm_simp) add: Un_cons) |
|
273 |
done |
|
274 |
||
275 |
||
276 |
(** list_add **) |
|
277 |
||
278 |
lemma list_add_type [TC]: "xs: list(nat) ==> list_add(xs) : nat" |
|
279 |
by (simp add: list_add_list_def) |
|
280 |
||
281 |
||
282 |
(*** theorems about map ***) |
|
283 |
||
284 |
lemma map_ident [simp]: "l: list(A) ==> map(%u. u, l) = l" |
|
285 |
apply (induct_tac "l") |
|
286 |
apply (simp_all (no_asm_simp)) |
|
287 |
done |
|
288 |
||
289 |
lemma map_compose: "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)" |
|
290 |
apply (induct_tac "l") |
|
291 |
apply (simp_all (no_asm_simp)) |
|
292 |
done |
|
293 |
||
294 |
lemma map_app_distrib: "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)" |
|
295 |
apply (induct_tac "xs") |
|
296 |
apply (simp_all (no_asm_simp)) |
|
297 |
done |
|
298 |
||
299 |
lemma map_flat: "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))" |
|
300 |
apply (induct_tac "ls") |
|
301 |
apply (simp_all (no_asm_simp) add: map_app_distrib) |
|
302 |
done |
|
303 |
||
304 |
lemma list_rec_map: |
|
305 |
"l: list(A) ==> |
|
306 |
list_rec(c, d, map(h,l)) = |
|
307 |
list_rec(c, %x xs r. d(h(x), map(h,xs), r), l)" |
|
308 |
apply (induct_tac "l") |
|
309 |
apply (simp_all (no_asm_simp)) |
|
310 |
done |
|
311 |
||
312 |
(** theorems about list(Collect(A,P)) -- used in Induct/Term.thy **) |
|
313 |
||
314 |
(* c : list(Collect(B,P)) ==> c : list(B) *) |
|
315 |
lemmas list_CollectD = Collect_subset [THEN list_mono, THEN subsetD, standard] |
|
316 |
||
317 |
lemma map_list_Collect: "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)" |
|
318 |
apply (induct_tac "l") |
|
319 |
apply (simp_all (no_asm_simp)) |
|
320 |
done |
|
321 |
||
322 |
(*** theorems about length ***) |
|
323 |
||
324 |
lemma length_map [simp]: "xs: list(A) ==> length(map(h,xs)) = length(xs)" |
|
13387 | 325 |
by (induct_tac "xs", simp_all) |
13327 | 326 |
|
327 |
lemma length_app [simp]: |
|
328 |
"[| xs: list(A); ys: list(A) |] |
|
329 |
==> length(xs@ys) = length(xs) #+ length(ys)" |
|
13387 | 330 |
by (induct_tac "xs", simp_all) |
13327 | 331 |
|
332 |
lemma length_rev [simp]: "xs: list(A) ==> length(rev(xs)) = length(xs)" |
|
333 |
apply (induct_tac "xs") |
|
334 |
apply (simp_all (no_asm_simp) add: length_app) |
|
335 |
done |
|
336 |
||
337 |
lemma length_flat: |
|
338 |
"ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))" |
|
339 |
apply (induct_tac "ls") |
|
340 |
apply (simp_all (no_asm_simp) add: length_app) |
|
341 |
done |
|
342 |
||
343 |
(** Length and drop **) |
|
344 |
||
345 |
(*Lemma for the inductive step of drop_length*) |
|
346 |
lemma drop_length_Cons [rule_format]: |
|
347 |
"xs: list(A) ==> |
|
348 |
\<forall>x. EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)" |
|
13387 | 349 |
by (erule list.induct, simp_all) |
13327 | 350 |
|
351 |
lemma drop_length [rule_format]: |
|
352 |
"l: list(A) ==> \<forall>i \<in> length(l). (EX z zs. drop(i,l) = Cons(z,zs))" |
|
13387 | 353 |
apply (erule list.induct, simp_all) |
13327 | 354 |
apply safe |
355 |
apply (erule drop_length_Cons) |
|
356 |
apply (rule natE) |
|
13387 | 357 |
apply (erule Ord_trans [OF asm_rl length_type Ord_nat], assumption, simp_all) |
13327 | 358 |
apply (blast intro: succ_in_naturalD length_type) |
359 |
done |
|
360 |
||
361 |
||
362 |
(*** theorems about app ***) |
|
363 |
||
364 |
lemma app_right_Nil [simp]: "xs: list(A) ==> xs@Nil=xs" |
|
13387 | 365 |
by (erule list.induct, simp_all) |
13327 | 366 |
|
367 |
lemma app_assoc: "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)" |
|
13387 | 368 |
by (induct_tac "xs", simp_all) |
13327 | 369 |
|
370 |
lemma flat_app_distrib: "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)" |
|
371 |
apply (induct_tac "ls") |
|
372 |
apply (simp_all (no_asm_simp) add: app_assoc) |
|
373 |
done |
|
374 |
||
375 |
(*** theorems about rev ***) |
|
376 |
||
377 |
lemma rev_map_distrib: "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))" |
|
378 |
apply (induct_tac "l") |
|
379 |
apply (simp_all (no_asm_simp) add: map_app_distrib) |
|
380 |
done |
|
381 |
||
382 |
(*Simplifier needs the premises as assumptions because rewriting will not |
|
383 |
instantiate the variable ?A in the rules' typing conditions; note that |
|
384 |
rev_type does not instantiate ?A. Only the premises do. |
|
385 |
*) |
|
386 |
lemma rev_app_distrib: |
|
387 |
"[| xs: list(A); ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)" |
|
388 |
apply (erule list.induct) |
|
389 |
apply (simp_all add: app_assoc) |
|
390 |
done |
|
391 |
||
392 |
lemma rev_rev_ident [simp]: "l: list(A) ==> rev(rev(l))=l" |
|
393 |
apply (induct_tac "l") |
|
394 |
apply (simp_all (no_asm_simp) add: rev_app_distrib) |
|
395 |
done |
|
396 |
||
397 |
lemma rev_flat: "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))" |
|
398 |
apply (induct_tac "ls") |
|
399 |
apply (simp_all add: map_app_distrib flat_app_distrib rev_app_distrib) |
|
400 |
done |
|
401 |
||
402 |
||
403 |
(*** theorems about list_add ***) |
|
404 |
||
405 |
lemma list_add_app: |
|
406 |
"[| xs: list(nat); ys: list(nat) |] |
|
407 |
==> list_add(xs@ys) = list_add(ys) #+ list_add(xs)" |
|
13387 | 408 |
apply (induct_tac "xs", simp_all) |
13327 | 409 |
done |
410 |
||
411 |
lemma list_add_rev: "l: list(nat) ==> list_add(rev(l)) = list_add(l)" |
|
412 |
apply (induct_tac "l") |
|
413 |
apply (simp_all (no_asm_simp) add: list_add_app) |
|
414 |
done |
|
415 |
||
416 |
lemma list_add_flat: |
|
417 |
"ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))" |
|
418 |
apply (induct_tac "ls") |
|
419 |
apply (simp_all (no_asm_simp) add: list_add_app) |
|
420 |
done |
|
421 |
||
422 |
(** New induction rule **) |
|
423 |
||
424 |
||
425 |
lemma list_append_induct: |
|
426 |
"[| l: list(A); |
|
427 |
P(Nil); |
|
428 |
!!x y. [| x: A; y: list(A); P(y) |] ==> P(y @ [x]) |
|
429 |
|] ==> P(l)" |
|
430 |
apply (subgoal_tac "P(rev(rev(l)))", simp) |
|
431 |
apply (erule rev_type [THEN list.induct], simp_all) |
|
432 |
done |
|
433 |
||
13356 | 434 |
lemmas list_append_induct = list_append_induct [case_names Nil snoc, consumes 1] |
435 |
||
13327 | 436 |
|
437 |
(*** Thanks to Sidi Ehmety for these results about min, take, etc. ***) |
|
438 |
||
439 |
(** min FIXME: replace by Int! **) |
|
440 |
(* Min theorems are also true for i, j ordinals *) |
|
441 |
lemma min_sym: "[| i:nat; j:nat |] ==> min(i,j)=min(j,i)" |
|
442 |
apply (unfold min_def) |
|
443 |
apply (auto dest!: not_lt_imp_le dest: lt_not_sym intro: le_anti_sym) |
|
444 |
done |
|
445 |
||
446 |
lemma min_type [simp,TC]: "[| i:nat; j:nat |] ==> min(i,j):nat" |
|
447 |
by (unfold min_def, auto) |
|
448 |
||
449 |
lemma min_0 [simp]: "i:nat ==> min(0,i) = 0" |
|
450 |
apply (unfold min_def) |
|
451 |
apply (auto dest: not_lt_imp_le) |
|
452 |
done |
|
453 |
||
454 |
lemma min_02 [simp]: "i:nat ==> min(i, 0) = 0" |
|
455 |
apply (unfold min_def) |
|
456 |
apply (auto dest: not_lt_imp_le) |
|
457 |
done |
|
458 |
||
459 |
lemma lt_min_iff: "[| i:nat; j:nat; k:nat |] ==> i<min(j,k) <-> i<j & i<k" |
|
460 |
apply (unfold min_def) |
|
461 |
apply (auto dest!: not_lt_imp_le intro: lt_trans2 lt_trans) |
|
462 |
done |
|
463 |
||
464 |
lemma min_succ_succ [simp]: |
|
465 |
"[| i:nat; j:nat |] ==> min(succ(i), succ(j))= succ(min(i, j))" |
|
466 |
apply (unfold min_def, auto) |
|
467 |
done |
|
468 |
||
469 |
(*** more theorems about lists ***) |
|
470 |
||
471 |
(** filter **) |
|
472 |
||
473 |
lemma filter_append [simp]: |
|
474 |
"xs:list(A) ==> filter(P, xs@ys) = filter(P, xs) @ filter(P, ys)" |
|
475 |
by (induct_tac "xs", auto) |
|
476 |
||
477 |
lemma filter_type [simp,TC]: "xs:list(A) ==> filter(P, xs):list(A)" |
|
478 |
by (induct_tac "xs", auto) |
|
479 |
||
480 |
lemma length_filter: "xs:list(A) ==> length(filter(P, xs)) le length(xs)" |
|
481 |
apply (induct_tac "xs", auto) |
|
482 |
apply (rule_tac j = "length (l) " in le_trans) |
|
483 |
apply (auto simp add: le_iff) |
|
484 |
done |
|
485 |
||
486 |
lemma filter_is_subset: "xs:list(A) ==> set_of_list(filter(P,xs)) <= set_of_list(xs)" |
|
487 |
by (induct_tac "xs", auto) |
|
488 |
||
489 |
lemma filter_False [simp]: "xs:list(A) ==> filter(%p. False, xs) = Nil" |
|
490 |
by (induct_tac "xs", auto) |
|
491 |
||
492 |
lemma filter_True [simp]: "xs:list(A) ==> filter(%p. True, xs) = xs" |
|
493 |
by (induct_tac "xs", auto) |
|
494 |
||
495 |
(** length **) |
|
496 |
||
497 |
lemma length_is_0_iff [simp]: "xs:list(A) ==> length(xs)=0 <-> xs=Nil" |
|
498 |
by (erule list.induct, auto) |
|
499 |
||
500 |
lemma length_is_0_iff2 [simp]: "xs:list(A) ==> 0 = length(xs) <-> xs=Nil" |
|
501 |
by (erule list.induct, auto) |
|
502 |
||
503 |
lemma length_tl [simp]: "xs:list(A) ==> length(tl(xs)) = length(xs) #- 1" |
|
504 |
by (erule list.induct, auto) |
|
505 |
||
506 |
lemma length_greater_0_iff: "xs:list(A) ==> 0<length(xs) <-> xs ~= Nil" |
|
507 |
by (erule list.induct, auto) |
|
508 |
||
509 |
lemma length_succ_iff: "xs:list(A) ==> length(xs)=succ(n) <-> (EX y ys. xs=Cons(y, ys) & length(ys)=n)" |
|
510 |
by (erule list.induct, auto) |
|
511 |
||
512 |
(** more theorems about append **) |
|
513 |
||
514 |
lemma append_is_Nil_iff [simp]: |
|
515 |
"xs:list(A) ==> (xs@ys = Nil) <-> (xs=Nil & ys = Nil)" |
|
516 |
by (erule list.induct, auto) |
|
517 |
||
518 |
lemma append_is_Nil_iff2 [simp]: |
|
519 |
"xs:list(A) ==> (Nil = xs@ys) <-> (xs=Nil & ys = Nil)" |
|
520 |
by (erule list.induct, auto) |
|
521 |
||
522 |
lemma append_left_is_self_iff [simp]: |
|
523 |
"xs:list(A) ==> (xs@ys = xs) <-> (ys = Nil)" |
|
524 |
by (erule list.induct, auto) |
|
525 |
||
526 |
lemma append_left_is_self_iff2 [simp]: |
|
527 |
"xs:list(A) ==> (xs = xs@ys) <-> (ys = Nil)" |
|
528 |
by (erule list.induct, auto) |
|
529 |
||
530 |
(*TOO SLOW as a default simprule!*) |
|
531 |
lemma append_left_is_Nil_iff [rule_format]: |
|
532 |
"[| xs:list(A); ys:list(A); zs:list(A) |] ==> |
|
533 |
length(ys)=length(zs) --> (xs@ys=zs <-> (xs=Nil & ys=zs))" |
|
534 |
apply (erule list.induct) |
|
535 |
apply (auto simp add: length_app) |
|
536 |
done |
|
537 |
||
538 |
(*TOO SLOW as a default simprule!*) |
|
539 |
lemma append_left_is_Nil_iff2 [rule_format]: |
|
540 |
"[| xs:list(A); ys:list(A); zs:list(A) |] ==> |
|
541 |
length(ys)=length(zs) --> (zs=ys@xs <-> (xs=Nil & ys=zs))" |
|
542 |
apply (erule list.induct) |
|
543 |
apply (auto simp add: length_app) |
|
544 |
done |
|
545 |
||
546 |
lemma append_eq_append_iff [rule_format,simp]: |
|
547 |
"xs:list(A) ==> \<forall>ys \<in> list(A). |
|
548 |
length(xs)=length(ys) --> (xs@us = ys@vs) <-> (xs=ys & us=vs)" |
|
549 |
apply (erule list.induct) |
|
550 |
apply (simp (no_asm_simp)) |
|
551 |
apply clarify |
|
13387 | 552 |
apply (erule_tac a = ys in list.cases, auto) |
13327 | 553 |
done |
554 |
||
555 |
lemma append_eq_append [rule_format]: |
|
556 |
"xs:list(A) ==> |
|
557 |
\<forall>ys \<in> list(A). \<forall>us \<in> list(A). \<forall>vs \<in> list(A). |
|
558 |
length(us) = length(vs) --> (xs@us = ys@vs) --> (xs=ys & us=vs)" |
|
559 |
apply (induct_tac "xs") |
|
560 |
apply (force simp add: length_app, clarify) |
|
13387 | 561 |
apply (erule_tac a = ys in list.cases, simp) |
13327 | 562 |
apply (subgoal_tac "Cons (a, l) @ us =vs") |
13387 | 563 |
apply (drule rev_iffD1 [OF _ append_left_is_Nil_iff], simp_all, blast) |
13327 | 564 |
done |
565 |
||
566 |
lemma append_eq_append_iff2 [simp]: |
|
567 |
"[| xs:list(A); ys:list(A); us:list(A); vs:list(A); length(us)=length(vs) |] |
|
568 |
==> xs@us = ys@vs <-> (xs=ys & us=vs)" |
|
569 |
apply (rule iffI) |
|
570 |
apply (rule append_eq_append, auto) |
|
571 |
done |
|
572 |
||
573 |
lemma append_self_iff [simp]: |
|
574 |
"[| xs:list(A); ys:list(A); zs:list(A) |] ==> xs@ys=xs@zs <-> ys=zs" |
|
575 |
apply (simp (no_asm_simp)) |
|
576 |
done |
|
577 |
||
578 |
lemma append_self_iff2 [simp]: |
|
579 |
"[| xs:list(A); ys:list(A); zs:list(A) |] ==> ys@xs=zs@xs <-> ys=zs" |
|
580 |
apply (simp (no_asm_simp)) |
|
581 |
done |
|
582 |
||
583 |
(* Can also be proved from append_eq_append_iff2, |
|
584 |
but the proof requires two more hypotheses: x:A and y:A *) |
|
585 |
lemma append1_eq_iff [rule_format,simp]: |
|
586 |
"xs:list(A) ==> \<forall>ys \<in> list(A). xs@[x] = ys@[y] <-> (xs = ys & x=y)" |
|
587 |
apply (erule list.induct) |
|
588 |
apply clarify |
|
589 |
apply (erule list.cases) |
|
590 |
apply simp_all |
|
591 |
txt{*Inductive step*} |
|
592 |
apply clarify |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13327
diff
changeset
|
593 |
apply (erule_tac a=ys in list.cases, simp_all) |
13327 | 594 |
done |
595 |
||
596 |
||
597 |
lemma append_right_is_self_iff [simp]: |
|
598 |
"[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) <-> (xs=Nil)" |
|
599 |
apply (simp (no_asm_simp) add: append_left_is_Nil_iff) |
|
600 |
done |
|
601 |
||
602 |
lemma append_right_is_self_iff2 [simp]: |
|
603 |
"[| xs:list(A); ys:list(A) |] ==> (ys = xs@ys) <-> (xs=Nil)" |
|
604 |
apply (rule iffI) |
|
605 |
apply (drule sym, auto) |
|
606 |
done |
|
607 |
||
608 |
lemma hd_append [rule_format,simp]: |
|
609 |
"xs:list(A) ==> xs ~= Nil --> hd(xs @ ys) = hd(xs)" |
|
610 |
by (induct_tac "xs", auto) |
|
611 |
||
612 |
lemma tl_append [rule_format,simp]: |
|
613 |
"xs:list(A) ==> xs~=Nil --> tl(xs @ ys) = tl(xs)@ys" |
|
614 |
by (induct_tac "xs", auto) |
|
615 |
||
616 |
(** rev **) |
|
617 |
lemma rev_is_Nil_iff [simp]: "xs:list(A) ==> (rev(xs) = Nil <-> xs = Nil)" |
|
618 |
by (erule list.induct, auto) |
|
619 |
||
620 |
lemma Nil_is_rev_iff [simp]: "xs:list(A) ==> (Nil = rev(xs) <-> xs = Nil)" |
|
621 |
by (erule list.induct, auto) |
|
622 |
||
623 |
lemma rev_is_rev_iff [rule_format,simp]: |
|
624 |
"xs:list(A) ==> \<forall>ys \<in> list(A). rev(xs)=rev(ys) <-> xs=ys" |
|
13387 | 625 |
apply (erule list.induct, force, clarify) |
626 |
apply (erule_tac a = ys in list.cases, auto) |
|
13327 | 627 |
done |
628 |
||
629 |
lemma rev_list_elim [rule_format]: |
|
630 |
"xs:list(A) ==> |
|
631 |
(xs=Nil --> P) --> (\<forall>ys \<in> list(A). \<forall>y \<in> A. xs =ys@[y] -->P)-->P" |
|
632 |
apply (erule list_append_induct, auto) |
|
633 |
done |
|
634 |
||
635 |
||
636 |
(** more theorems about drop **) |
|
637 |
||
638 |
lemma length_drop [rule_format,simp]: |
|
639 |
"n:nat ==> \<forall>xs \<in> list(A). length(drop(n, xs)) = length(xs) #- n" |
|
640 |
apply (erule nat_induct) |
|
641 |
apply (auto elim: list.cases) |
|
642 |
done |
|
643 |
||
644 |
lemma drop_all [rule_format,simp]: |
|
645 |
"n:nat ==> \<forall>xs \<in> list(A). length(xs) le n --> drop(n, xs)=Nil" |
|
646 |
apply (erule nat_induct) |
|
647 |
apply (auto elim: list.cases) |
|
648 |
done |
|
649 |
||
650 |
lemma drop_append [rule_format]: |
|
651 |
"n:nat ==> |
|
652 |
\<forall>xs \<in> list(A). drop(n, xs@ys) = drop(n,xs) @ drop(n #- length(xs), ys)" |
|
653 |
apply (induct_tac "n") |
|
654 |
apply (auto elim: list.cases) |
|
655 |
done |
|
656 |
||
657 |
lemma drop_drop: |
|
658 |
"m:nat ==> \<forall>xs \<in> list(A). \<forall>n \<in> nat. drop(n, drop(m, xs))=drop(n #+ m, xs)" |
|
659 |
apply (induct_tac "m") |
|
660 |
apply (auto elim: list.cases) |
|
661 |
done |
|
662 |
||
663 |
(** take **) |
|
664 |
||
665 |
lemma take_0 [simp]: "xs:list(A) ==> take(0, xs) = Nil" |
|
666 |
apply (unfold take_def) |
|
667 |
apply (erule list.induct, auto) |
|
668 |
done |
|
669 |
||
670 |
lemma take_succ_Cons [simp]: |
|
671 |
"n:nat ==> take(succ(n), Cons(a, xs)) = Cons(a, take(n, xs))" |
|
672 |
by (simp add: take_def) |
|
673 |
||
674 |
(* Needed for proving take_all *) |
|
675 |
lemma take_Nil [simp]: "n:nat ==> take(n, Nil) = Nil" |
|
676 |
by (unfold take_def, auto) |
|
677 |
||
678 |
lemma take_all [rule_format,simp]: |
|
679 |
"n:nat ==> \<forall>xs \<in> list(A). length(xs) le n --> take(n, xs) = xs" |
|
680 |
apply (erule nat_induct) |
|
681 |
apply (auto elim: list.cases) |
|
682 |
done |
|
683 |
||
684 |
lemma take_type [rule_format,simp,TC]: |
|
685 |
"xs:list(A) ==> \<forall>n \<in> nat. take(n, xs):list(A)" |
|
13387 | 686 |
apply (erule list.induct, simp, clarify) |
13327 | 687 |
apply (erule natE, auto) |
688 |
done |
|
689 |
||
690 |
lemma take_append [rule_format,simp]: |
|
691 |
"xs:list(A) ==> |
|
692 |
\<forall>ys \<in> list(A). \<forall>n \<in> nat. take(n, xs @ ys) = |
|
693 |
take(n, xs) @ take(n #- length(xs), ys)" |
|
13387 | 694 |
apply (erule list.induct, simp, clarify) |
13327 | 695 |
apply (erule natE, auto) |
696 |
done |
|
697 |
||
698 |
lemma take_take [rule_format]: |
|
699 |
"m : nat ==> |
|
700 |
\<forall>xs \<in> list(A). \<forall>n \<in> nat. take(n, take(m,xs))= take(min(n, m), xs)" |
|
701 |
apply (induct_tac "m", auto) |
|
13387 | 702 |
apply (erule_tac a = xs in list.cases) |
13327 | 703 |
apply (auto simp add: take_Nil) |
704 |
apply (rotate_tac 1) |
|
705 |
apply (erule natE) |
|
706 |
apply (auto intro: take_0 take_type) |
|
707 |
done |
|
708 |
||
709 |
(** nth **) |
|
710 |
||
13387 | 711 |
lemma nth_0 [simp]: "nth(0, Cons(a, l)) = a" |
712 |
by (simp add: nth_def) |
|
713 |
||
714 |
lemma nth_Cons [simp]: "n:nat ==> nth(succ(n), Cons(a,l)) = nth(n,l)" |
|
715 |
by (simp add: nth_def) |
|
13327 | 716 |
|
13387 | 717 |
lemma nth_empty [simp]: "nth(n, Nil) = 0" |
718 |
by (simp add: nth_def) |
|
719 |
||
720 |
lemma nth_type [rule_format,simp,TC]: |
|
721 |
"xs:list(A) ==> \<forall>n \<in> nat. n < length(xs) --> nth(n,xs) : A" |
|
722 |
apply (erule list.induct, simp, clarify) |
|
723 |
apply (erule natE, auto) |
|
13327 | 724 |
done |
725 |
||
13387 | 726 |
lemma nth_eq_0 [rule_format]: |
727 |
"xs:list(A) ==> \<forall>n \<in> nat. length(xs) le n --> nth(n,xs) = 0" |
|
728 |
apply (erule list.induct, simp, clarify) |
|
13327 | 729 |
apply (erule natE, auto) |
730 |
done |
|
731 |
||
732 |
lemma nth_append [rule_format]: |
|
733 |
"xs:list(A) ==> |
|
734 |
\<forall>n \<in> nat. nth(n, xs @ ys) = (if n < length(xs) then nth(n,xs) |
|
13387 | 735 |
else nth(n #- length(xs), ys))" |
736 |
apply (induct_tac "xs", simp, clarify) |
|
13327 | 737 |
apply (erule natE, auto) |
738 |
done |
|
739 |
||
740 |
lemma set_of_list_conv_nth: |
|
741 |
"xs:list(A) |
|
13387 | 742 |
==> set_of_list(xs) = {x:A. EX i:nat. i<length(xs) & x = nth(i,xs)}" |
13327 | 743 |
apply (induct_tac "xs", simp_all) |
744 |
apply (rule equalityI, auto) |
|
13387 | 745 |
apply (rule_tac x = 0 in bexI, auto) |
13327 | 746 |
apply (erule natE, auto) |
747 |
done |
|
748 |
||
749 |
(* Other theorems about lists *) |
|
750 |
||
751 |
lemma nth_take_lemma [rule_format]: |
|
752 |
"k:nat ==> |
|
753 |
\<forall>xs \<in> list(A). (\<forall>ys \<in> list(A). k le length(xs) --> k le length(ys) --> |
|
13387 | 754 |
(\<forall>i \<in> nat. i<k --> nth(i,xs) = nth(i,ys))--> take(k,xs) = take(k,ys))" |
13327 | 755 |
apply (induct_tac "k") |
756 |
apply (simp_all (no_asm_simp) add: lt_succ_eq_0_disj all_conj_distrib) |
|
757 |
apply clarify |
|
758 |
(*Both lists are non-empty*) |
|
13387 | 759 |
apply (erule_tac a=xs in list.cases, simp) |
760 |
apply (erule_tac a=ys in list.cases, clarify) |
|
13327 | 761 |
apply (simp (no_asm_use) ) |
762 |
apply clarify |
|
763 |
apply (simp (no_asm_simp)) |
|
764 |
apply (rule conjI, force) |
|
765 |
apply (rename_tac y ys z zs) |
|
13387 | 766 |
apply (drule_tac x = zs and x1 = ys in bspec [THEN bspec], auto) |
13327 | 767 |
done |
768 |
||
769 |
lemma nth_equalityI [rule_format]: |
|
770 |
"[| xs:list(A); ys:list(A); length(xs) = length(ys); |
|
771 |
\<forall>i \<in> nat. i < length(xs) --> nth(i,xs) = nth(i,ys) |] |
|
772 |
==> xs = ys" |
|
773 |
apply (subgoal_tac "length (xs) le length (ys) ") |
|
774 |
apply (cut_tac k="length(xs)" and xs=xs and ys=ys in nth_take_lemma) |
|
775 |
apply (simp_all add: take_all) |
|
776 |
done |
|
777 |
||
778 |
(*The famous take-lemma*) |
|
779 |
||
780 |
lemma take_equalityI [rule_format]: |
|
781 |
"[| xs:list(A); ys:list(A); (\<forall>i \<in> nat. take(i, xs) = take(i,ys)) |] |
|
782 |
==> xs = ys" |
|
783 |
apply (case_tac "length (xs) le length (ys) ") |
|
784 |
apply (drule_tac x = "length (ys) " in bspec) |
|
785 |
apply (drule_tac [3] not_lt_imp_le) |
|
786 |
apply (subgoal_tac [5] "length (ys) le length (xs) ") |
|
787 |
apply (rule_tac [6] j = "succ (length (ys))" in le_trans) |
|
788 |
apply (rule_tac [6] leI) |
|
789 |
apply (drule_tac [5] x = "length (xs) " in bspec) |
|
790 |
apply (simp_all add: take_all) |
|
791 |
done |
|
792 |
||
793 |
lemma nth_drop [rule_format]: |
|
13387 | 794 |
"n:nat ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A). nth(i, drop(n, xs)) = nth(n #+ i, xs)" |
795 |
apply (induct_tac "n", simp_all, clarify) |
|
796 |
apply (erule list.cases, auto) |
|
13327 | 797 |
done |
798 |
||
799 |
subsection{*The function zip*} |
|
800 |
||
801 |
text{*Crafty definition to eliminate a type argument*} |
|
802 |
||
803 |
consts |
|
804 |
zip_aux :: "[i,i]=>i" |
|
805 |
||
806 |
primrec (*explicit lambda is required because both arguments of "un" vary*) |
|
807 |
"zip_aux(B,[]) = |
|
808 |
(\<lambda>ys \<in> list(B). list_case([], %y l. [], ys))" |
|
809 |
||
810 |
"zip_aux(B,Cons(x,l)) = |
|
811 |
(\<lambda>ys \<in> list(B). |
|
812 |
list_case(Nil, %y zs. Cons(<x,y>, zip_aux(B,l)`zs), ys))" |
|
813 |
||
814 |
constdefs |
|
815 |
zip :: "[i, i]=>i" |
|
816 |
"zip(xs, ys) == zip_aux(set_of_list(ys),xs)`ys" |
|
817 |
||
818 |
||
819 |
(* zip equations *) |
|
820 |
||
821 |
lemma list_on_set_of_list: "xs \<in> list(A) ==> xs \<in> list(set_of_list(xs))" |
|
822 |
apply (induct_tac xs, simp_all) |
|
823 |
apply (blast intro: list_mono [THEN subsetD]) |
|
824 |
done |
|
825 |
||
826 |
lemma zip_Nil [simp]: "ys:list(A) ==> zip(Nil, ys)=Nil" |
|
827 |
apply (simp add: zip_def list_on_set_of_list [of _ A]) |
|
828 |
apply (erule list.cases, simp_all) |
|
829 |
done |
|
830 |
||
831 |
lemma zip_Nil2 [simp]: "xs:list(A) ==> zip(xs, Nil)=Nil" |
|
832 |
apply (simp add: zip_def list_on_set_of_list [of _ A]) |
|
833 |
apply (erule list.cases, simp_all) |
|
834 |
done |
|
835 |
||
836 |
lemma zip_aux_unique [rule_format]: |
|
837 |
"[|B<=C; xs \<in> list(A)|] |
|
838 |
==> \<forall>ys \<in> list(B). zip_aux(C,xs) ` ys = zip_aux(B,xs) ` ys" |
|
839 |
apply (induct_tac xs) |
|
840 |
apply simp_all |
|
841 |
apply (blast intro: list_mono [THEN subsetD], clarify) |
|
13387 | 842 |
apply (erule_tac a=ys in list.cases, auto) |
13327 | 843 |
apply (blast intro: list_mono [THEN subsetD]) |
844 |
done |
|
845 |
||
846 |
lemma zip_Cons_Cons [simp]: |
|
847 |
"[| xs:list(A); ys:list(B); x:A; y:B |] ==> |
|
848 |
zip(Cons(x,xs), Cons(y, ys)) = Cons(<x,y>, zip(xs, ys))" |
|
849 |
apply (simp add: zip_def, auto) |
|
850 |
apply (rule zip_aux_unique, auto) |
|
851 |
apply (simp add: list_on_set_of_list [of _ B]) |
|
852 |
apply (blast intro: list_on_set_of_list list_mono [THEN subsetD]) |
|
853 |
done |
|
854 |
||
855 |
lemma zip_type [rule_format,simp,TC]: |
|
856 |
"xs:list(A) ==> \<forall>ys \<in> list(B). zip(xs, ys):list(A*B)" |
|
857 |
apply (induct_tac "xs") |
|
858 |
apply (simp (no_asm)) |
|
859 |
apply clarify |
|
13387 | 860 |
apply (erule_tac a = ys in list.cases, auto) |
13327 | 861 |
done |
862 |
||
863 |
(* zip length *) |
|
864 |
lemma length_zip [rule_format,simp]: |
|
865 |
"xs:list(A) ==> \<forall>ys \<in> list(B). length(zip(xs,ys)) = |
|
866 |
min(length(xs), length(ys))" |
|
867 |
apply (unfold min_def) |
|
13387 | 868 |
apply (induct_tac "xs", simp_all, clarify) |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13327
diff
changeset
|
869 |
apply (erule_tac a = ys in list.cases, auto) |
13327 | 870 |
done |
871 |
||
872 |
lemma zip_append1 [rule_format]: |
|
873 |
"[| ys:list(A); zs:list(B) |] ==> |
|
874 |
\<forall>xs \<in> list(A). zip(xs @ ys, zs) = |
|
875 |
zip(xs, take(length(xs), zs)) @ zip(ys, drop(length(xs),zs))" |
|
13387 | 876 |
apply (induct_tac "zs", force, clarify) |
877 |
apply (erule_tac a = xs in list.cases, simp_all) |
|
13327 | 878 |
done |
879 |
||
880 |
lemma zip_append2 [rule_format]: |
|
881 |
"[| xs:list(A); zs:list(B) |] ==> \<forall>ys \<in> list(B). zip(xs, ys@zs) = |
|
882 |
zip(take(length(ys), xs), ys) @ zip(drop(length(ys), xs), zs)" |
|
13387 | 883 |
apply (induct_tac "xs", force, clarify) |
884 |
apply (erule_tac a = ys in list.cases, auto) |
|
13327 | 885 |
done |
886 |
||
887 |
lemma zip_append [simp]: |
|
888 |
"[| length(xs) = length(us); length(ys) = length(vs); |
|
889 |
xs:list(A); us:list(B); ys:list(A); vs:list(B) |] |
|
890 |
==> zip(xs@ys,us@vs) = zip(xs, us) @ zip(ys, vs)" |
|
891 |
by (simp (no_asm_simp) add: zip_append1 drop_append diff_self_eq_0) |
|
892 |
||
893 |
||
894 |
lemma zip_rev [rule_format,simp]: |
|
895 |
"ys:list(B) ==> \<forall>xs \<in> list(A). |
|
896 |
length(xs) = length(ys) --> zip(rev(xs), rev(ys)) = rev(zip(xs, ys))" |
|
13387 | 897 |
apply (induct_tac "ys", force, clarify) |
898 |
apply (erule_tac a = xs in list.cases) |
|
13327 | 899 |
apply (auto simp add: length_rev) |
900 |
done |
|
901 |
||
902 |
lemma nth_zip [rule_format,simp]: |
|
903 |
"ys:list(B) ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A). |
|
904 |
i < length(xs) --> i < length(ys) --> |
|
905 |
nth(i,zip(xs, ys)) = <nth(i,xs),nth(i, ys)>" |
|
13387 | 906 |
apply (induct_tac "ys", force, clarify) |
907 |
apply (erule_tac a = xs in list.cases, simp) |
|
13327 | 908 |
apply (auto elim: natE) |
909 |
done |
|
910 |
||
911 |
lemma set_of_list_zip [rule_format]: |
|
912 |
"[| xs:list(A); ys:list(B); i:nat |] |
|
913 |
==> set_of_list(zip(xs, ys)) = |
|
914 |
{<x, y>:A*B. EX i:nat. i < min(length(xs), length(ys)) |
|
13387 | 915 |
& x = nth(i, xs) & y = nth(i, ys)}" |
13327 | 916 |
by (force intro!: Collect_cong simp add: lt_min_iff set_of_list_conv_nth) |
917 |
||
918 |
(** list_update **) |
|
919 |
||
920 |
lemma list_update_Nil [simp]: "i:nat ==>list_update(Nil, i, v) = Nil" |
|
921 |
by (unfold list_update_def, auto) |
|
922 |
||
923 |
lemma list_update_Cons_0 [simp]: "list_update(Cons(x, xs), 0, v)= Cons(v, xs)" |
|
924 |
by (unfold list_update_def, auto) |
|
925 |
||
926 |
lemma list_update_Cons_succ [simp]: |
|
927 |
"n:nat ==> |
|
928 |
list_update(Cons(x, xs), succ(n), v)= Cons(x, list_update(xs, n, v))" |
|
929 |
apply (unfold list_update_def, auto) |
|
930 |
done |
|
931 |
||
932 |
lemma list_update_type [rule_format,simp,TC]: |
|
933 |
"[| xs:list(A); v:A |] ==> \<forall>n \<in> nat. list_update(xs, n, v):list(A)" |
|
934 |
apply (induct_tac "xs") |
|
935 |
apply (simp (no_asm)) |
|
936 |
apply clarify |
|
937 |
apply (erule natE, auto) |
|
938 |
done |
|
939 |
||
940 |
lemma length_list_update [rule_format,simp]: |
|
941 |
"xs:list(A) ==> \<forall>i \<in> nat. length(list_update(xs, i, v))=length(xs)" |
|
942 |
apply (induct_tac "xs") |
|
943 |
apply (simp (no_asm)) |
|
944 |
apply clarify |
|
945 |
apply (erule natE, auto) |
|
946 |
done |
|
947 |
||
948 |
lemma nth_list_update [rule_format]: |
|
949 |
"[| xs:list(A) |] ==> \<forall>i \<in> nat. \<forall>j \<in> nat. i < length(xs) --> |
|
950 |
nth(j, list_update(xs, i, x)) = (if i=j then x else nth(j, xs))" |
|
951 |
apply (induct_tac "xs") |
|
952 |
apply simp_all |
|
953 |
apply clarify |
|
954 |
apply (rename_tac i j) |
|
955 |
apply (erule_tac n=i in natE) |
|
956 |
apply (erule_tac [2] n=j in natE) |
|
957 |
apply (erule_tac n=j in natE, simp_all, force) |
|
958 |
done |
|
959 |
||
960 |
lemma nth_list_update_eq [simp]: |
|
961 |
"[| i < length(xs); xs:list(A) |] ==> nth(i, list_update(xs, i,x)) = x" |
|
962 |
by (simp (no_asm_simp) add: lt_length_in_nat nth_list_update) |
|
963 |
||
964 |
||
965 |
lemma nth_list_update_neq [rule_format,simp]: |
|
13387 | 966 |
"xs:list(A) ==> |
967 |
\<forall>i \<in> nat. \<forall>j \<in> nat. i ~= j --> nth(j, list_update(xs,i,x)) = nth(j,xs)" |
|
13327 | 968 |
apply (induct_tac "xs") |
969 |
apply (simp (no_asm)) |
|
970 |
apply clarify |
|
971 |
apply (erule natE) |
|
972 |
apply (erule_tac [2] natE, simp_all) |
|
973 |
apply (erule natE, simp_all) |
|
974 |
done |
|
975 |
||
976 |
lemma list_update_overwrite [rule_format,simp]: |
|
977 |
"xs:list(A) ==> \<forall>i \<in> nat. i < length(xs) |
|
978 |
--> list_update(list_update(xs, i, x), i, y) = list_update(xs, i,y)" |
|
979 |
apply (induct_tac "xs") |
|
980 |
apply (simp (no_asm)) |
|
981 |
apply clarify |
|
982 |
apply (erule natE, auto) |
|
983 |
done |
|
984 |
||
985 |
lemma list_update_same_conv [rule_format]: |
|
13387 | 986 |
"xs:list(A) ==> |
987 |
\<forall>i \<in> nat. i < length(xs) --> |
|
988 |
(list_update(xs, i, x) = xs) <-> (nth(i, xs) = x)" |
|
13327 | 989 |
apply (induct_tac "xs") |
990 |
apply (simp (no_asm)) |
|
991 |
apply clarify |
|
992 |
apply (erule natE, auto) |
|
993 |
done |
|
994 |
||
995 |
lemma update_zip [rule_format]: |
|
13387 | 996 |
"ys:list(B) ==> |
997 |
\<forall>i \<in> nat. \<forall>xy \<in> A*B. \<forall>xs \<in> list(A). |
|
998 |
length(xs) = length(ys) --> |
|
999 |
list_update(zip(xs, ys), i, xy) = zip(list_update(xs, i, fst(xy)), |
|
1000 |
list_update(ys, i, snd(xy)))" |
|
13327 | 1001 |
apply (induct_tac "ys") |
1002 |
apply auto |
|
13387 | 1003 |
apply (erule_tac a = xs in list.cases) |
13327 | 1004 |
apply (auto elim: natE) |
1005 |
done |
|
1006 |
||
1007 |
lemma set_update_subset_cons [rule_format]: |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13327
diff
changeset
|
1008 |
"xs:list(A) ==> |
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13327
diff
changeset
|
1009 |
\<forall>i \<in> nat. set_of_list(list_update(xs, i, x)) <= cons(x, set_of_list(xs))" |
13327 | 1010 |
apply (induct_tac "xs") |
1011 |
apply simp |
|
1012 |
apply (rule ballI) |
|
13387 | 1013 |
apply (erule natE, simp_all, auto) |
13327 | 1014 |
done |
1015 |
||
1016 |
lemma set_of_list_update_subsetI: |
|
1017 |
"[| set_of_list(xs) <= A; xs:list(A); x:A; i:nat|] |
|
1018 |
==> set_of_list(list_update(xs, i,x)) <= A" |
|
1019 |
apply (rule subset_trans) |
|
1020 |
apply (rule set_update_subset_cons, auto) |
|
1021 |
done |
|
1022 |
||
1023 |
(** upt **) |
|
1024 |
||
1025 |
lemma upt_rec: |
|
1026 |
"j:nat ==> upt(i,j) = (if i<j then Cons(i, upt(succ(i), j)) else Nil)" |
|
1027 |
apply (induct_tac "j", auto) |
|
1028 |
apply (drule not_lt_imp_le) |
|
1029 |
apply (auto simp: lt_Ord intro: le_anti_sym) |
|
1030 |
done |
|
1031 |
||
1032 |
lemma upt_conv_Nil [simp]: "[| j le i; j:nat |] ==> upt(i,j) = Nil" |
|
1033 |
apply (subst upt_rec, auto) |
|
1034 |
apply (auto simp add: le_iff) |
|
1035 |
apply (drule lt_asym [THEN notE], auto) |
|
1036 |
done |
|
1037 |
||
1038 |
(*Only needed if upt_Suc is deleted from the simpset*) |
|
1039 |
lemma upt_succ_append: |
|
1040 |
"[| i le j; j:nat |] ==> upt(i,succ(j)) = upt(i, j)@[j]" |
|
1041 |
by simp |
|
1042 |
||
1043 |
lemma upt_conv_Cons: |
|
1044 |
"[| i<j; j:nat |] ==> upt(i,j) = Cons(i,upt(succ(i),j))" |
|
1045 |
apply (rule trans) |
|
1046 |
apply (rule upt_rec, auto) |
|
1047 |
done |
|
1048 |
||
1049 |
lemma upt_type [simp,TC]: "j:nat ==> upt(i,j):list(nat)" |
|
1050 |
by (induct_tac "j", auto) |
|
1051 |
||
1052 |
(*LOOPS as a simprule, since j<=j*) |
|
1053 |
lemma upt_add_eq_append: |
|
1054 |
"[| i le j; j:nat; k:nat |] ==> upt(i, j #+k) = upt(i,j)@upt(j,j#+k)" |
|
1055 |
apply (induct_tac "k") |
|
1056 |
apply (auto simp add: app_assoc app_type) |
|
13387 | 1057 |
apply (rule_tac j = j in le_trans, auto) |
13327 | 1058 |
done |
1059 |
||
1060 |
lemma length_upt [simp]: "[| i:nat; j:nat |] ==>length(upt(i,j)) = j #- i" |
|
1061 |
apply (induct_tac "j") |
|
1062 |
apply (rule_tac [2] sym) |
|
1063 |
apply (auto dest!: not_lt_imp_le simp add: length_app diff_succ diff_is_0_iff) |
|
1064 |
done |
|
1065 |
||
1066 |
lemma nth_upt [rule_format,simp]: |
|
1067 |
"[| i:nat; j:nat; k:nat |] ==> i #+ k < j --> nth(k, upt(i,j)) = i #+ k" |
|
13387 | 1068 |
apply (induct_tac "j", simp) |
1069 |
apply (simp add: nth_append le_iff split add: nat_diff_split) |
|
1070 |
apply (auto dest!: not_lt_imp_le |
|
1071 |
simp add: nth_append diff_self_eq_0 less_diff_conv add_commute) |
|
1072 |
apply (drule_tac j = x in lt_trans2, auto) |
|
13327 | 1073 |
done |
1074 |
||
1075 |
lemma take_upt [rule_format,simp]: |
|
1076 |
"[| m:nat; n:nat |] ==> |
|
13387 | 1077 |
\<forall>i \<in> nat. i #+ m le n --> take(m, upt(i,n)) = upt(i,i#+m)" |
13327 | 1078 |
apply (induct_tac "m") |
1079 |
apply (simp (no_asm_simp) add: take_0) |
|
1080 |
apply clarify |
|
1081 |
apply (subst upt_rec, simp) |
|
1082 |
apply (rule sym) |
|
1083 |
apply (subst upt_rec, simp) |
|
1084 |
apply (simp_all del: upt.simps) |
|
1085 |
apply (rule_tac j = "succ (i #+ x) " in lt_trans2) |
|
1086 |
apply auto |
|
1087 |
done |
|
1088 |
||
1089 |
lemma map_succ_upt: |
|
1090 |
"[| m:nat; n:nat |] ==> map(succ, upt(m,n))= upt(succ(m), succ(n))" |
|
1091 |
apply (induct_tac "n") |
|
1092 |
apply (auto simp add: map_app_distrib) |
|
1093 |
done |
|
1094 |
||
1095 |
lemma nth_map [rule_format,simp]: |
|
1096 |
"xs:list(A) ==> |
|
1097 |
\<forall>n \<in> nat. n < length(xs) --> nth(n, map(f, xs)) = f(nth(n, xs))" |
|
1098 |
apply (induct_tac "xs", simp) |
|
1099 |
apply (rule ballI) |
|
1100 |
apply (induct_tac "n", auto) |
|
1101 |
done |
|
1102 |
||
1103 |
lemma nth_map_upt [rule_format]: |
|
1104 |
"[| m:nat; n:nat |] ==> |
|
1105 |
\<forall>i \<in> nat. i < n #- m --> nth(i, map(f, upt(m,n))) = f(m #+ i)" |
|
13387 | 1106 |
apply (rule_tac n = m and m = n in diff_induct, typecheck, simp) |
13327 | 1107 |
apply simp |
13387 | 1108 |
apply (subst map_succ_upt [symmetric], simp_all, clarify) |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13327
diff
changeset
|
1109 |
apply (subgoal_tac "i < length (upt (0, x))") |
13327 | 1110 |
prefer 2 |
1111 |
apply (simp add: less_diff_conv) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13327
diff
changeset
|
1112 |
apply (rule_tac j = "succ (i #+ y) " in lt_trans2) |
13327 | 1113 |
apply simp |
1114 |
apply simp |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13327
diff
changeset
|
1115 |
apply (subgoal_tac "i < length (upt (y, x))") |
13327 | 1116 |
apply (simp_all add: add_commute less_diff_conv) |
1117 |
done |
|
1118 |
||
1119 |
(** sublist (a generalization of nth to sets) **) |
|
1120 |
||
1121 |
constdefs |
|
1122 |
sublist :: "[i, i] => i" |
|
1123 |
"sublist(xs, A)== |
|
1124 |
map(fst, (filter(%p. snd(p): A, zip(xs, upt(0,length(xs))))))" |
|
1125 |
||
1126 |
lemma sublist_0 [simp]: "xs:list(A) ==>sublist(xs, 0) =Nil" |
|
1127 |
by (unfold sublist_def, auto) |
|
1128 |
||
1129 |
lemma sublist_Nil [simp]: "sublist(Nil, A) = Nil" |
|
1130 |
by (unfold sublist_def, auto) |
|
1131 |
||
1132 |
lemma sublist_shift_lemma: |
|
1133 |
"[| xs:list(B); i:nat |] ==> |
|
1134 |
map(fst, filter(%p. snd(p):A, zip(xs, upt(i,i #+ length(xs))))) = |
|
1135 |
map(fst, filter(%p. snd(p):nat & snd(p) #+ i:A, zip(xs,upt(0,length(xs)))))" |
|
1136 |
apply (erule list_append_induct) |
|
1137 |
apply (simp (no_asm_simp)) |
|
1138 |
apply (auto simp add: add_commute length_app filter_append map_app_distrib) |
|
1139 |
done |
|
1140 |
||
1141 |
lemma sublist_type [simp,TC]: |
|
1142 |
"xs:list(B) ==> sublist(xs, A):list(B)" |
|
1143 |
apply (unfold sublist_def) |
|
1144 |
apply (induct_tac "xs") |
|
1145 |
apply (auto simp add: filter_append map_app_distrib) |
|
1146 |
done |
|
1147 |
||
1148 |
lemma upt_add_eq_append2: |
|
1149 |
"[| i:nat; j:nat |] ==> upt(0, i #+ j) = upt(0, i) @ upt(i, i #+ j)" |
|
1150 |
by (simp add: upt_add_eq_append [of 0] nat_0_le) |
|
1151 |
||
1152 |
lemma sublist_append: |
|
1153 |
"[| xs:list(B); ys:list(B) |] ==> |
|
1154 |
sublist(xs@ys, A) = sublist(xs, A) @ sublist(ys, {j:nat. j #+ length(xs): A})" |
|
1155 |
apply (unfold sublist_def) |
|
13387 | 1156 |
apply (erule_tac l = ys in list_append_induct, simp) |
13327 | 1157 |
apply (simp (no_asm_simp) add: upt_add_eq_append2 app_assoc [symmetric]) |
1158 |
apply (auto simp add: sublist_shift_lemma length_type map_app_distrib app_assoc) |
|
1159 |
apply (simp_all add: add_commute) |
|
1160 |
done |
|
1161 |
||
1162 |
||
1163 |
lemma sublist_Cons: |
|
1164 |
"[| xs:list(B); x:B |] ==> |
|
1165 |
sublist(Cons(x, xs), A) = |
|
1166 |
(if 0:A then [x] else []) @ sublist(xs, {j:nat. succ(j) : A})" |
|
13387 | 1167 |
apply (erule_tac l = xs in list_append_induct) |
13327 | 1168 |
apply (simp (no_asm_simp) add: sublist_def) |
1169 |
apply (simp del: app_Cons add: app_Cons [symmetric] sublist_append, simp) |
|
1170 |
done |
|
1171 |
||
1172 |
lemma sublist_singleton [simp]: |
|
1173 |
"sublist([x], A) = (if 0 : A then [x] else [])" |
|
1174 |
by (simp (no_asm) add: sublist_Cons) |
|
1175 |
||
1176 |
||
1177 |
lemma sublist_upt_eq_take [simp]: |
|
1178 |
"[| xs:list(A); n:nat |] ==> sublist(xs, less_than(n)) = take(n,xs)" |
|
1179 |
apply (unfold less_than_def) |
|
13387 | 1180 |
apply (erule_tac l = xs in list_append_induct, simp) |
13327 | 1181 |
apply (simp split add: nat_diff_split add: sublist_append, auto) |
1182 |
apply (subgoal_tac "n #- length (y) = 0") |
|
1183 |
apply (simp (no_asm_simp)) |
|
1184 |
apply (auto dest!: not_lt_imp_le simp add: diff_is_0_iff) |
|
1185 |
done |
|
1186 |
||
13387 | 1187 |
text{*Repetition of a List Element*} |
1188 |
||
1189 |
consts repeat :: "[i,i]=>i" |
|
1190 |
primrec |
|
1191 |
"repeat(a,0) = []" |
|
1192 |
||
1193 |
"repeat(a,succ(n)) = Cons(a,repeat(a,n))" |
|
1194 |
||
1195 |
lemma length_repeat: "n \<in> nat ==> length(repeat(a,n)) = n" |
|
1196 |
by (induct_tac n, auto) |
|
1197 |
||
1198 |
lemma repeat_succ_app: "n \<in> nat ==> repeat(a,succ(n)) = repeat(a,n) @ [a]" |
|
1199 |
apply (induct_tac n) |
|
1200 |
apply (simp_all del: app_Cons add: app_Cons [symmetric]) |
|
1201 |
done |
|
1202 |
||
1203 |
lemma repeat_type [TC]: "[|a \<in> A; n \<in> nat|] ==> repeat(a,n) \<in> list(A)" |
|
1204 |
by (induct_tac n, auto) |
|
1205 |
||
1206 |
||
13327 | 1207 |
ML |
1208 |
{* |
|
1209 |
val ConsE = thm "ConsE"; |
|
1210 |
val Cons_iff = thm "Cons_iff"; |
|
1211 |
val Nil_Cons_iff = thm "Nil_Cons_iff"; |
|
1212 |
val list_unfold = thm "list_unfold"; |
|
1213 |
val list_mono = thm "list_mono"; |
|
1214 |
val list_univ = thm "list_univ"; |
|
1215 |
val list_subset_univ = thm "list_subset_univ"; |
|
1216 |
val list_into_univ = thm "list_into_univ"; |
|
1217 |
val list_case_type = thm "list_case_type"; |
|
1218 |
val tl_type = thm "tl_type"; |
|
1219 |
val drop_Nil = thm "drop_Nil"; |
|
1220 |
val drop_succ_Cons = thm "drop_succ_Cons"; |
|
1221 |
val drop_type = thm "drop_type"; |
|
1222 |
val list_rec_type = thm "list_rec_type"; |
|
1223 |
val map_type = thm "map_type"; |
|
1224 |
val map_type2 = thm "map_type2"; |
|
1225 |
val length_type = thm "length_type"; |
|
1226 |
val lt_length_in_nat = thm "lt_length_in_nat"; |
|
1227 |
val app_type = thm "app_type"; |
|
1228 |
val rev_type = thm "rev_type"; |
|
1229 |
val flat_type = thm "flat_type"; |
|
1230 |
val set_of_list_type = thm "set_of_list_type"; |
|
1231 |
val set_of_list_append = thm "set_of_list_append"; |
|
1232 |
val list_add_type = thm "list_add_type"; |
|
1233 |
val map_ident = thm "map_ident"; |
|
1234 |
val map_compose = thm "map_compose"; |
|
1235 |
val map_app_distrib = thm "map_app_distrib"; |
|
1236 |
val map_flat = thm "map_flat"; |
|
1237 |
val list_rec_map = thm "list_rec_map"; |
|
1238 |
val list_CollectD = thm "list_CollectD"; |
|
1239 |
val map_list_Collect = thm "map_list_Collect"; |
|
1240 |
val length_map = thm "length_map"; |
|
1241 |
val length_app = thm "length_app"; |
|
1242 |
val length_rev = thm "length_rev"; |
|
1243 |
val length_flat = thm "length_flat"; |
|
1244 |
val drop_length_Cons = thm "drop_length_Cons"; |
|
1245 |
val drop_length = thm "drop_length"; |
|
1246 |
val app_right_Nil = thm "app_right_Nil"; |
|
1247 |
val app_assoc = thm "app_assoc"; |
|
1248 |
val flat_app_distrib = thm "flat_app_distrib"; |
|
1249 |
val rev_map_distrib = thm "rev_map_distrib"; |
|
1250 |
val rev_app_distrib = thm "rev_app_distrib"; |
|
1251 |
val rev_rev_ident = thm "rev_rev_ident"; |
|
1252 |
val rev_flat = thm "rev_flat"; |
|
1253 |
val list_add_app = thm "list_add_app"; |
|
1254 |
val list_add_rev = thm "list_add_rev"; |
|
1255 |
val list_add_flat = thm "list_add_flat"; |
|
1256 |
val list_append_induct = thm "list_append_induct"; |
|
1257 |
val min_sym = thm "min_sym"; |
|
1258 |
val min_type = thm "min_type"; |
|
1259 |
val min_0 = thm "min_0"; |
|
1260 |
val min_02 = thm "min_02"; |
|
1261 |
val lt_min_iff = thm "lt_min_iff"; |
|
1262 |
val min_succ_succ = thm "min_succ_succ"; |
|
1263 |
val filter_append = thm "filter_append"; |
|
1264 |
val filter_type = thm "filter_type"; |
|
1265 |
val length_filter = thm "length_filter"; |
|
1266 |
val filter_is_subset = thm "filter_is_subset"; |
|
1267 |
val filter_False = thm "filter_False"; |
|
1268 |
val filter_True = thm "filter_True"; |
|
1269 |
val length_is_0_iff = thm "length_is_0_iff"; |
|
1270 |
val length_is_0_iff2 = thm "length_is_0_iff2"; |
|
1271 |
val length_tl = thm "length_tl"; |
|
1272 |
val length_greater_0_iff = thm "length_greater_0_iff"; |
|
1273 |
val length_succ_iff = thm "length_succ_iff"; |
|
1274 |
val append_is_Nil_iff = thm "append_is_Nil_iff"; |
|
1275 |
val append_is_Nil_iff2 = thm "append_is_Nil_iff2"; |
|
1276 |
val append_left_is_self_iff = thm "append_left_is_self_iff"; |
|
1277 |
val append_left_is_self_iff2 = thm "append_left_is_self_iff2"; |
|
1278 |
val append_left_is_Nil_iff = thm "append_left_is_Nil_iff"; |
|
1279 |
val append_left_is_Nil_iff2 = thm "append_left_is_Nil_iff2"; |
|
1280 |
val append_eq_append_iff = thm "append_eq_append_iff"; |
|
1281 |
val append_eq_append = thm "append_eq_append"; |
|
1282 |
val append_eq_append_iff2 = thm "append_eq_append_iff2"; |
|
1283 |
val append_self_iff = thm "append_self_iff"; |
|
1284 |
val append_self_iff2 = thm "append_self_iff2"; |
|
1285 |
val append1_eq_iff = thm "append1_eq_iff"; |
|
1286 |
val append_right_is_self_iff = thm "append_right_is_self_iff"; |
|
1287 |
val append_right_is_self_iff2 = thm "append_right_is_self_iff2"; |
|
1288 |
val hd_append = thm "hd_append"; |
|
1289 |
val tl_append = thm "tl_append"; |
|
1290 |
val rev_is_Nil_iff = thm "rev_is_Nil_iff"; |
|
1291 |
val Nil_is_rev_iff = thm "Nil_is_rev_iff"; |
|
1292 |
val rev_is_rev_iff = thm "rev_is_rev_iff"; |
|
1293 |
val rev_list_elim = thm "rev_list_elim"; |
|
1294 |
val length_drop = thm "length_drop"; |
|
1295 |
val drop_all = thm "drop_all"; |
|
1296 |
val drop_append = thm "drop_append"; |
|
1297 |
val drop_drop = thm "drop_drop"; |
|
1298 |
val take_0 = thm "take_0"; |
|
1299 |
val take_succ_Cons = thm "take_succ_Cons"; |
|
1300 |
val take_Nil = thm "take_Nil"; |
|
1301 |
val take_all = thm "take_all"; |
|
1302 |
val take_type = thm "take_type"; |
|
1303 |
val take_append = thm "take_append"; |
|
1304 |
val take_take = thm "take_take"; |
|
1305 |
val nth_0 = thm "nth_0"; |
|
1306 |
val nth_Cons = thm "nth_Cons"; |
|
1307 |
val nth_type = thm "nth_type"; |
|
1308 |
val nth_append = thm "nth_append"; |
|
1309 |
val set_of_list_conv_nth = thm "set_of_list_conv_nth"; |
|
1310 |
val nth_take_lemma = thm "nth_take_lemma"; |
|
1311 |
val nth_equalityI = thm "nth_equalityI"; |
|
1312 |
val take_equalityI = thm "take_equalityI"; |
|
1313 |
val nth_drop = thm "nth_drop"; |
|
1314 |
val list_on_set_of_list = thm "list_on_set_of_list"; |
|
1315 |
val zip_Nil = thm "zip_Nil"; |
|
1316 |
val zip_Nil2 = thm "zip_Nil2"; |
|
1317 |
val zip_Cons_Cons = thm "zip_Cons_Cons"; |
|
1318 |
val zip_type = thm "zip_type"; |
|
1319 |
val length_zip = thm "length_zip"; |
|
1320 |
val zip_append1 = thm "zip_append1"; |
|
1321 |
val zip_append2 = thm "zip_append2"; |
|
1322 |
val zip_append = thm "zip_append"; |
|
1323 |
val zip_rev = thm "zip_rev"; |
|
1324 |
val nth_zip = thm "nth_zip"; |
|
1325 |
val set_of_list_zip = thm "set_of_list_zip"; |
|
1326 |
val list_update_Nil = thm "list_update_Nil"; |
|
1327 |
val list_update_Cons_0 = thm "list_update_Cons_0"; |
|
1328 |
val list_update_Cons_succ = thm "list_update_Cons_succ"; |
|
1329 |
val list_update_type = thm "list_update_type"; |
|
1330 |
val length_list_update = thm "length_list_update"; |
|
1331 |
val nth_list_update = thm "nth_list_update"; |
|
1332 |
val nth_list_update_eq = thm "nth_list_update_eq"; |
|
1333 |
val nth_list_update_neq = thm "nth_list_update_neq"; |
|
1334 |
val list_update_overwrite = thm "list_update_overwrite"; |
|
1335 |
val list_update_same_conv = thm "list_update_same_conv"; |
|
1336 |
val update_zip = thm "update_zip"; |
|
1337 |
val set_update_subset_cons = thm "set_update_subset_cons"; |
|
1338 |
val set_of_list_update_subsetI = thm "set_of_list_update_subsetI"; |
|
1339 |
val upt_rec = thm "upt_rec"; |
|
1340 |
val upt_conv_Nil = thm "upt_conv_Nil"; |
|
1341 |
val upt_succ_append = thm "upt_succ_append"; |
|
1342 |
val upt_conv_Cons = thm "upt_conv_Cons"; |
|
1343 |
val upt_type = thm "upt_type"; |
|
1344 |
val upt_add_eq_append = thm "upt_add_eq_append"; |
|
1345 |
val length_upt = thm "length_upt"; |
|
1346 |
val nth_upt = thm "nth_upt"; |
|
1347 |
val take_upt = thm "take_upt"; |
|
1348 |
val map_succ_upt = thm "map_succ_upt"; |
|
1349 |
val nth_map = thm "nth_map"; |
|
1350 |
val nth_map_upt = thm "nth_map_upt"; |
|
1351 |
val sublist_0 = thm "sublist_0"; |
|
1352 |
val sublist_Nil = thm "sublist_Nil"; |
|
1353 |
val sublist_shift_lemma = thm "sublist_shift_lemma"; |
|
1354 |
val sublist_type = thm "sublist_type"; |
|
1355 |
val upt_add_eq_append2 = thm "upt_add_eq_append2"; |
|
1356 |
val sublist_append = thm "sublist_append"; |
|
1357 |
val sublist_Cons = thm "sublist_Cons"; |
|
1358 |
val sublist_singleton = thm "sublist_singleton"; |
|
1359 |
val sublist_upt_eq_take = thm "sublist_upt_eq_take"; |
|
1360 |
||
1361 |
structure list = |
|
1362 |
struct |
|
1363 |
val induct = thm "list.induct" |
|
1364 |
val elim = thm "list.cases" |
|
1365 |
val intrs = thms "list.intros" |
|
1366 |
end; |
|
1367 |
*} |
|
1368 |
||
516 | 1369 |
end |