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