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