1 (* Title: ZF/list-fn.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 For list-fn.thy. Lists in Zermelo-Fraenkel Set Theory |
|
7 *) |
|
8 |
|
9 open ListFn; |
|
10 |
|
11 (** hd and tl **) |
|
12 |
|
13 goalw ListFn.thy [hd_def] "hd(Cons(a,l)) = a"; |
|
14 by (resolve_tac List.case_eqns 1); |
|
15 val hd_Cons = result(); |
|
16 |
|
17 goalw ListFn.thy [tl_def] "tl(Nil) = Nil"; |
|
18 by (resolve_tac List.case_eqns 1); |
|
19 val tl_Nil = result(); |
|
20 |
|
21 goalw ListFn.thy [tl_def] "tl(Cons(a,l)) = l"; |
|
22 by (resolve_tac List.case_eqns 1); |
|
23 val tl_Cons = result(); |
|
24 |
|
25 goal ListFn.thy "!!l. l: list(A) ==> tl(l) : list(A)"; |
|
26 by (etac List.elim 1); |
|
27 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps (List.intrs @ [tl_Nil,tl_Cons])))); |
|
28 val tl_type = result(); |
|
29 |
|
30 (** drop **) |
|
31 |
|
32 goalw ListFn.thy [drop_def] "drop(0, l) = l"; |
|
33 by (rtac rec_0 1); |
|
34 val drop_0 = result(); |
|
35 |
|
36 goalw ListFn.thy [drop_def] "!!i. i:nat ==> drop(i, Nil) = Nil"; |
|
37 by (etac nat_induct 1); |
|
38 by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_Nil]))); |
|
39 val drop_Nil = result(); |
|
40 |
|
41 goalw ListFn.thy [drop_def] |
|
42 "!!i. i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)"; |
|
43 by (etac nat_induct 1); |
|
44 by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_Cons]))); |
|
45 val drop_succ_Cons = result(); |
|
46 |
|
47 goalw ListFn.thy [drop_def] |
|
48 "!!i l. [| i:nat; l: list(A) |] ==> drop(i,l) : list(A)"; |
|
49 by (etac nat_induct 1); |
|
50 by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_type]))); |
|
51 val drop_type = result(); |
|
52 |
|
53 (** list_rec -- by Vset recursion **) |
|
54 |
|
55 goal ListFn.thy "list_rec(Nil,c,h) = c"; |
|
56 by (rtac (list_rec_def RS def_Vrec RS trans) 1); |
|
57 by (simp_tac (ZF_ss addsimps List.case_eqns) 1); |
|
58 val list_rec_Nil = result(); |
|
59 |
|
60 goal ListFn.thy "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))"; |
|
61 by (rtac (list_rec_def RS def_Vrec RS trans) 1); |
|
62 by (simp_tac (rank_ss addsimps (rank_Cons2::List.case_eqns)) 1); |
|
63 val list_rec_Cons = result(); |
|
64 |
|
65 (*Type checking -- proved by induction, as usual*) |
|
66 val prems = goal ListFn.thy |
|
67 "[| l: list(A); \ |
|
68 \ c: C(Nil); \ |
|
69 \ !!x y r. [| x:A; y: list(A); r: C(y) |] ==> h(x,y,r): C(Cons(x,y)) \ |
|
70 \ |] ==> list_rec(l,c,h) : C(l)"; |
|
71 by (list_ind_tac "l" prems 1); |
|
72 by (ALLGOALS (asm_simp_tac |
|
73 (ZF_ss addsimps (prems@[list_rec_Nil,list_rec_Cons])))); |
|
74 val list_rec_type = result(); |
|
75 |
|
76 (** Versions for use with definitions **) |
|
77 |
|
78 val [rew] = goal ListFn.thy |
|
79 "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Nil) = c"; |
|
80 by (rewtac rew); |
|
81 by (rtac list_rec_Nil 1); |
|
82 val def_list_rec_Nil = result(); |
|
83 |
|
84 val [rew] = goal ListFn.thy |
|
85 "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Cons(a,l)) = h(a,l,j(l))"; |
|
86 by (rewtac rew); |
|
87 by (rtac list_rec_Cons 1); |
|
88 val def_list_rec_Cons = result(); |
|
89 |
|
90 fun list_recs def = map standard |
|
91 ([def] RL [def_list_rec_Nil, def_list_rec_Cons]); |
|
92 |
|
93 (** map **) |
|
94 |
|
95 val [map_Nil,map_Cons] = list_recs map_def; |
|
96 |
|
97 val prems = goalw ListFn.thy [map_def] |
|
98 "[| l: list(A); !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)"; |
|
99 by (REPEAT (ares_tac (prems@[list_rec_type, NilI, ConsI]) 1)); |
|
100 val map_type = result(); |
|
101 |
|
102 val [major] = goal ListFn.thy "l: list(A) ==> map(h,l) : list({h(u). u:A})"; |
|
103 by (rtac (major RS map_type) 1); |
|
104 by (etac RepFunI 1); |
|
105 val map_type2 = result(); |
|
106 |
|
107 (** length **) |
|
108 |
|
109 val [length_Nil,length_Cons] = list_recs length_def; |
|
110 |
|
111 goalw ListFn.thy [length_def] |
|
112 "!!l. l: list(A) ==> length(l) : nat"; |
|
113 by (REPEAT (ares_tac [list_rec_type, nat_0I, nat_succI] 1)); |
|
114 val length_type = result(); |
|
115 |
|
116 (** app **) |
|
117 |
|
118 val [app_Nil,app_Cons] = list_recs app_def; |
|
119 |
|
120 goalw ListFn.thy [app_def] |
|
121 "!!xs ys. [| xs: list(A); ys: list(A) |] ==> xs@ys : list(A)"; |
|
122 by (REPEAT (ares_tac [list_rec_type, ConsI] 1)); |
|
123 val app_type = result(); |
|
124 |
|
125 (** rev **) |
|
126 |
|
127 val [rev_Nil,rev_Cons] = list_recs rev_def; |
|
128 |
|
129 val prems = goalw ListFn.thy [rev_def] |
|
130 "xs: list(A) ==> rev(xs) : list(A)"; |
|
131 by (REPEAT (ares_tac (prems @ [list_rec_type, NilI, ConsI, app_type]) 1)); |
|
132 val rev_type = result(); |
|
133 |
|
134 |
|
135 (** flat **) |
|
136 |
|
137 val [flat_Nil,flat_Cons] = list_recs flat_def; |
|
138 |
|
139 val prems = goalw ListFn.thy [flat_def] |
|
140 "ls: list(list(A)) ==> flat(ls) : list(A)"; |
|
141 by (REPEAT (ares_tac (prems @ [list_rec_type, NilI, ConsI, app_type]) 1)); |
|
142 val flat_type = result(); |
|
143 |
|
144 |
|
145 (** list_add **) |
|
146 |
|
147 val [list_add_Nil,list_add_Cons] = list_recs list_add_def; |
|
148 |
|
149 val prems = goalw ListFn.thy [list_add_def] |
|
150 "xs: list(nat) ==> list_add(xs) : nat"; |
|
151 by (REPEAT (ares_tac (prems @ [list_rec_type, nat_0I, add_type]) 1)); |
|
152 val list_add_type = result(); |
|
153 |
|
154 (** ListFn simplification **) |
|
155 |
|
156 val list_typechecks = |
|
157 [NilI, ConsI, list_rec_type, |
|
158 map_type, map_type2, app_type, length_type, rev_type, flat_type, |
|
159 list_add_type]; |
|
160 |
|
161 val list_ss = arith_ss |
|
162 addsimps List.case_eqns |
|
163 addsimps [list_rec_Nil, list_rec_Cons, |
|
164 map_Nil, map_Cons, |
|
165 app_Nil, app_Cons, |
|
166 length_Nil, length_Cons, |
|
167 rev_Nil, rev_Cons, |
|
168 flat_Nil, flat_Cons, |
|
169 list_add_Nil, list_add_Cons] |
|
170 setsolver (type_auto_tac list_typechecks); |
|
171 (*Could also rewrite using the list_typechecks...*) |
|
172 |
|
173 (*** theorems about map ***) |
|
174 |
|
175 val prems = goal ListFn.thy |
|
176 "l: list(A) ==> map(%u.u, l) = l"; |
|
177 by (list_ind_tac "l" prems 1); |
|
178 by (ALLGOALS (asm_simp_tac list_ss)); |
|
179 val map_ident = result(); |
|
180 |
|
181 val prems = goal ListFn.thy |
|
182 "l: list(A) ==> map(h, map(j,l)) = map(%u.h(j(u)), l)"; |
|
183 by (list_ind_tac "l" prems 1); |
|
184 by (ALLGOALS (asm_simp_tac list_ss)); |
|
185 val map_compose = result(); |
|
186 |
|
187 val prems = goal ListFn.thy |
|
188 "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)"; |
|
189 by (list_ind_tac "xs" prems 1); |
|
190 by (ALLGOALS (asm_simp_tac list_ss)); |
|
191 val map_app_distrib = result(); |
|
192 |
|
193 val prems = goal ListFn.thy |
|
194 "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))"; |
|
195 by (list_ind_tac "ls" prems 1); |
|
196 by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib]))); |
|
197 val map_flat = result(); |
|
198 |
|
199 val prems = goal ListFn.thy |
|
200 "l: list(A) ==> \ |
|
201 \ list_rec(map(h,l), c, d) = \ |
|
202 \ list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))"; |
|
203 by (list_ind_tac "l" prems 1); |
|
204 by (ALLGOALS (asm_simp_tac list_ss)); |
|
205 val list_rec_map = result(); |
|
206 |
|
207 (** theorems about list(Collect(A,P)) -- used in ex/term.ML **) |
|
208 |
|
209 (* c : list(Collect(B,P)) ==> c : list(B) *) |
|
210 val list_CollectD = standard (Collect_subset RS list_mono RS subsetD); |
|
211 |
|
212 val prems = goal ListFn.thy |
|
213 "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)"; |
|
214 by (list_ind_tac "l" prems 1); |
|
215 by (ALLGOALS (asm_simp_tac list_ss)); |
|
216 val map_list_Collect = result(); |
|
217 |
|
218 (*** theorems about length ***) |
|
219 |
|
220 val prems = goal ListFn.thy |
|
221 "xs: list(A) ==> length(map(h,xs)) = length(xs)"; |
|
222 by (list_ind_tac "xs" prems 1); |
|
223 by (ALLGOALS (asm_simp_tac list_ss)); |
|
224 val length_map = result(); |
|
225 |
|
226 val prems = goal ListFn.thy |
|
227 "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)"; |
|
228 by (list_ind_tac "xs" prems 1); |
|
229 by (ALLGOALS (asm_simp_tac list_ss)); |
|
230 val length_app = result(); |
|
231 |
|
232 (* [| m: nat; n: nat |] ==> m #+ succ(n) = succ(n) #+ m |
|
233 Used for rewriting below*) |
|
234 val add_commute_succ = nat_succI RSN (2,add_commute); |
|
235 |
|
236 val prems = goal ListFn.thy |
|
237 "xs: list(A) ==> length(rev(xs)) = length(xs)"; |
|
238 by (list_ind_tac "xs" prems 1); |
|
239 by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app, add_commute_succ]))); |
|
240 val length_rev = result(); |
|
241 |
|
242 val prems = goal ListFn.thy |
|
243 "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))"; |
|
244 by (list_ind_tac "ls" prems 1); |
|
245 by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app]))); |
|
246 val length_flat = result(); |
|
247 |
|
248 (** Length and drop **) |
|
249 |
|
250 (*Lemma for the inductive step of drop_length*) |
|
251 goal ListFn.thy |
|
252 "!!xs. xs: list(A) ==> \ |
|
253 \ ALL x. EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)"; |
|
254 by (etac List.induct 1); |
|
255 by (ALLGOALS (asm_simp_tac (list_ss addsimps [drop_0,drop_succ_Cons]))); |
|
256 by (fast_tac ZF_cs 1); |
|
257 val drop_length_Cons_lemma = result(); |
|
258 val drop_length_Cons = standard (drop_length_Cons_lemma RS spec); |
|
259 |
|
260 goal ListFn.thy |
|
261 "!!l. l: list(A) ==> ALL i: length(l). EX z zs. drop(i,l) = Cons(z,zs)"; |
|
262 by (etac List.induct 1); |
|
263 by (ALLGOALS (asm_simp_tac (list_ss addsimps bquant_simps))); |
|
264 by (rtac conjI 1); |
|
265 by (etac drop_length_Cons 1); |
|
266 by (rtac ballI 1); |
|
267 by (rtac natE 1); |
|
268 by (etac ([asm_rl, length_type, Ord_nat] MRS Ord_trans) 1); |
|
269 by (assume_tac 1); |
|
270 by (asm_simp_tac (list_ss addsimps [drop_0]) 1); |
|
271 by (fast_tac ZF_cs 1); |
|
272 by (asm_simp_tac (list_ss addsimps [drop_succ_Cons]) 1); |
|
273 by (dtac bspec 1); |
|
274 by (fast_tac ZF_cs 2); |
|
275 by (fast_tac (ZF_cs addEs [succ_in_naturalD,length_type]) 1); |
|
276 val drop_length_lemma = result(); |
|
277 val drop_length = standard (drop_length_lemma RS bspec); |
|
278 |
|
279 |
|
280 (*** theorems about app ***) |
|
281 |
|
282 val [major] = goal ListFn.thy "xs: list(A) ==> xs@Nil=xs"; |
|
283 by (rtac (major RS List.induct) 1); |
|
284 by (ALLGOALS (asm_simp_tac list_ss)); |
|
285 val app_right_Nil = result(); |
|
286 |
|
287 val prems = goal ListFn.thy "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)"; |
|
288 by (list_ind_tac "xs" prems 1); |
|
289 by (ALLGOALS (asm_simp_tac list_ss)); |
|
290 val app_assoc = result(); |
|
291 |
|
292 val prems = goal ListFn.thy |
|
293 "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)"; |
|
294 by (list_ind_tac "ls" prems 1); |
|
295 by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_assoc]))); |
|
296 val flat_app_distrib = result(); |
|
297 |
|
298 (*** theorems about rev ***) |
|
299 |
|
300 val prems = goal ListFn.thy "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))"; |
|
301 by (list_ind_tac "l" prems 1); |
|
302 by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib]))); |
|
303 val rev_map_distrib = result(); |
|
304 |
|
305 (*Simplifier needs the premises as assumptions because rewriting will not |
|
306 instantiate the variable ?A in the rules' typing conditions; note that |
|
307 rev_type does not instantiate ?A. Only the premises do. |
|
308 *) |
|
309 goal ListFn.thy |
|
310 "!!xs. [| xs: list(A); ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)"; |
|
311 by (etac List.induct 1); |
|
312 by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_right_Nil,app_assoc]))); |
|
313 val rev_app_distrib = result(); |
|
314 |
|
315 val prems = goal ListFn.thy "l: list(A) ==> rev(rev(l))=l"; |
|
316 by (list_ind_tac "l" prems 1); |
|
317 by (ALLGOALS (asm_simp_tac (list_ss addsimps [rev_app_distrib]))); |
|
318 val rev_rev_ident = result(); |
|
319 |
|
320 val prems = goal ListFn.thy |
|
321 "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))"; |
|
322 by (list_ind_tac "ls" prems 1); |
|
323 by (ALLGOALS (asm_simp_tac (list_ss addsimps |
|
324 [map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil]))); |
|
325 val rev_flat = result(); |
|
326 |
|
327 |
|
328 (*** theorems about list_add ***) |
|
329 |
|
330 val prems = goal ListFn.thy |
|
331 "[| xs: list(nat); ys: list(nat) |] ==> \ |
|
332 \ list_add(xs@ys) = list_add(ys) #+ list_add(xs)"; |
|
333 by (cut_facts_tac prems 1); |
|
334 by (list_ind_tac "xs" prems 1); |
|
335 by (ALLGOALS |
|
336 (asm_simp_tac (list_ss addsimps [add_0_right, add_assoc RS sym]))); |
|
337 by (rtac (add_commute RS subst_context) 1); |
|
338 by (REPEAT (ares_tac [refl, list_add_type] 1)); |
|
339 val list_add_app = result(); |
|
340 |
|
341 val prems = goal ListFn.thy |
|
342 "l: list(nat) ==> list_add(rev(l)) = list_add(l)"; |
|
343 by (list_ind_tac "l" prems 1); |
|
344 by (ALLGOALS |
|
345 (asm_simp_tac (list_ss addsimps [list_add_app, add_0_right]))); |
|
346 val list_add_rev = result(); |
|
347 |
|
348 val prems = goal ListFn.thy |
|
349 "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))"; |
|
350 by (list_ind_tac "ls" prems 1); |
|
351 by (ALLGOALS (asm_simp_tac (list_ss addsimps [list_add_app]))); |
|
352 by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1)); |
|
353 val list_add_flat = result(); |
|
354 |
|
355 (** New induction rule **) |
|
356 |
|
357 val major::prems = goal ListFn.thy |
|
358 "[| l: list(A); \ |
|
359 \ P(Nil); \ |
|
360 \ !!x y. [| x: A; y: list(A); P(y) |] ==> P(y @ [x]) \ |
|
361 \ |] ==> P(l)"; |
|
362 by (rtac (major RS rev_rev_ident RS subst) 1); |
|
363 by (rtac (major RS rev_type RS List.induct) 1); |
|
364 by (ALLGOALS (asm_simp_tac (list_ss addsimps prems))); |
|
365 val list_append_induct = result(); |
|
366 |
|