|
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 |
|
12 (** list_rec -- by Vset recursion **) |
|
13 |
|
14 (*Used to verify list_rec*) |
|
15 val list_rec_ss = ZF_ss |
|
16 addcongs (mk_typed_congs ListFn.thy [("h", "[i,i,i]=>i")]) |
|
17 addrews List.case_eqns; |
|
18 |
|
19 goal ListFn.thy "list_rec(Nil,c,h) = c"; |
|
20 by (rtac (list_rec_def RS def_Vrec RS trans) 1); |
|
21 by (SIMP_TAC list_rec_ss 1); |
|
22 val list_rec_Nil = result(); |
|
23 |
|
24 goal ListFn.thy "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))"; |
|
25 by (rtac (list_rec_def RS def_Vrec RS trans) 1); |
|
26 by (SIMP_TAC (list_rec_ss addrews [Vset_rankI, rank_Cons2]) 1); |
|
27 val list_rec_Cons = result(); |
|
28 |
|
29 (*Type checking -- proved by induction, as usual*) |
|
30 val prems = goal ListFn.thy |
|
31 "[| l: list(A); \ |
|
32 \ c: C(Nil); \ |
|
33 \ !!x y r. [| x:A; y: list(A); r: C(y) |] ==> h(x,y,r): C(Cons(x,y)) \ |
|
34 \ |] ==> list_rec(l,c,h) : C(l)"; |
|
35 by (list_ind_tac "l" prems 1); |
|
36 by (ALLGOALS (ASM_SIMP_TAC |
|
37 (ZF_ss addrews (prems@[list_rec_Nil,list_rec_Cons])))); |
|
38 val list_rec_type = result(); |
|
39 |
|
40 (** Versions for use with definitions **) |
|
41 |
|
42 val [rew] = goal ListFn.thy |
|
43 "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Nil) = c"; |
|
44 by (rewtac rew); |
|
45 by (rtac list_rec_Nil 1); |
|
46 val def_list_rec_Nil = result(); |
|
47 |
|
48 val [rew] = goal ListFn.thy |
|
49 "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Cons(a,l)) = h(a,l,j(l))"; |
|
50 by (rewtac rew); |
|
51 by (rtac list_rec_Cons 1); |
|
52 val def_list_rec_Cons = result(); |
|
53 |
|
54 fun list_recs def = map standard |
|
55 ([def] RL [def_list_rec_Nil, def_list_rec_Cons]); |
|
56 |
|
57 (** map **) |
|
58 |
|
59 val [map_Nil,map_Cons] = list_recs map_def; |
|
60 |
|
61 val prems = goalw ListFn.thy [map_def] |
|
62 "[| l: list(A); !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)"; |
|
63 by (REPEAT (ares_tac (prems@[list_rec_type, NilI, ConsI]) 1)); |
|
64 val map_type = result(); |
|
65 |
|
66 val [major] = goal ListFn.thy "l: list(A) ==> map(h,l) : list({h(u). u:A})"; |
|
67 by (rtac (major RS map_type) 1); |
|
68 by (etac RepFunI 1); |
|
69 val map_type2 = result(); |
|
70 |
|
71 (** length **) |
|
72 |
|
73 val [length_Nil,length_Cons] = list_recs length_def; |
|
74 |
|
75 val prems = goalw ListFn.thy [length_def] |
|
76 "l: list(A) ==> length(l) : nat"; |
|
77 by (REPEAT (ares_tac (prems @ [list_rec_type, nat_0I, nat_succI]) 1)); |
|
78 val length_type = result(); |
|
79 |
|
80 (** app **) |
|
81 |
|
82 val [app_Nil,app_Cons] = list_recs app_def; |
|
83 |
|
84 val prems = goalw ListFn.thy [app_def] |
|
85 "[| xs: list(A); ys: list(A) |] ==> xs@ys : list(A)"; |
|
86 by (REPEAT (ares_tac (prems @ [list_rec_type, ConsI]) 1)); |
|
87 val app_type = result(); |
|
88 |
|
89 (** rev **) |
|
90 |
|
91 val [rev_Nil,rev_Cons] = list_recs rev_def; |
|
92 |
|
93 val prems = goalw ListFn.thy [rev_def] |
|
94 "xs: list(A) ==> rev(xs) : list(A)"; |
|
95 by (REPEAT (ares_tac (prems @ [list_rec_type, NilI, ConsI, app_type]) 1)); |
|
96 val rev_type = result(); |
|
97 |
|
98 |
|
99 (** flat **) |
|
100 |
|
101 val [flat_Nil,flat_Cons] = list_recs flat_def; |
|
102 |
|
103 val prems = goalw ListFn.thy [flat_def] |
|
104 "ls: list(list(A)) ==> flat(ls) : list(A)"; |
|
105 by (REPEAT (ares_tac (prems @ [list_rec_type, NilI, ConsI, app_type]) 1)); |
|
106 val flat_type = result(); |
|
107 |
|
108 |
|
109 (** list_add **) |
|
110 |
|
111 val [list_add_Nil,list_add_Cons] = list_recs list_add_def; |
|
112 |
|
113 val prems = goalw ListFn.thy [list_add_def] |
|
114 "xs: list(nat) ==> list_add(xs) : nat"; |
|
115 by (REPEAT (ares_tac (prems @ [list_rec_type, nat_0I, add_type]) 1)); |
|
116 val list_add_type = result(); |
|
117 |
|
118 (** ListFn simplification **) |
|
119 |
|
120 val list_typechecks = |
|
121 [NilI, ConsI, list_rec_type, |
|
122 map_type, map_type2, app_type, length_type, rev_type, flat_type, |
|
123 list_add_type]; |
|
124 |
|
125 val list_congs = |
|
126 List.congs @ |
|
127 mk_congs ListFn.thy |
|
128 ["list_rec","map","op @","length","rev","flat","list_add"]; |
|
129 |
|
130 val list_ss = arith_ss |
|
131 addcongs list_congs |
|
132 addrews List.case_eqns |
|
133 addrews list_typechecks |
|
134 addrews [list_rec_Nil, list_rec_Cons, |
|
135 map_Nil, map_Cons, |
|
136 app_Nil, app_Cons, |
|
137 length_Nil, length_Cons, |
|
138 rev_Nil, rev_Cons, |
|
139 flat_Nil, flat_Cons, |
|
140 list_add_Nil, list_add_Cons]; |
|
141 |
|
142 (*** theorems about map ***) |
|
143 |
|
144 val prems = goal ListFn.thy |
|
145 "l: list(A) ==> map(%u.u, l) = l"; |
|
146 by (list_ind_tac "l" prems 1); |
|
147 by (ALLGOALS (ASM_SIMP_TAC list_ss)); |
|
148 val map_ident = result(); |
|
149 |
|
150 val prems = goal ListFn.thy |
|
151 "l: list(A) ==> map(h, map(j,l)) = map(%u.h(j(u)), l)"; |
|
152 by (list_ind_tac "l" prems 1); |
|
153 by (ALLGOALS (ASM_SIMP_TAC list_ss)); |
|
154 val map_compose = result(); |
|
155 |
|
156 val prems = goal ListFn.thy |
|
157 "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)"; |
|
158 by (list_ind_tac "xs" prems 1); |
|
159 by (ALLGOALS (ASM_SIMP_TAC list_ss)); |
|
160 val map_app_distrib = result(); |
|
161 |
|
162 val prems = goal ListFn.thy |
|
163 "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))"; |
|
164 by (list_ind_tac "ls" prems 1); |
|
165 by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [map_app_distrib]))); |
|
166 val map_flat = result(); |
|
167 |
|
168 val prems = goal ListFn.thy |
|
169 "l: list(A) ==> \ |
|
170 \ list_rec(map(h,l), c, d) = \ |
|
171 \ list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))"; |
|
172 by (list_ind_tac "l" prems 1); |
|
173 by (ALLGOALS |
|
174 (ASM_SIMP_TAC |
|
175 (list_ss addcongs (mk_typed_congs ListFn.thy [("d", "[i,i,i]=>i")])))); |
|
176 val list_rec_map = result(); |
|
177 |
|
178 (** theorems about list(Collect(A,P)) -- used in ex/term.ML **) |
|
179 |
|
180 (* c : list(Collect(B,P)) ==> c : list(B) *) |
|
181 val list_CollectD = standard (Collect_subset RS list_mono RS subsetD); |
|
182 |
|
183 val prems = goal ListFn.thy |
|
184 "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)"; |
|
185 by (list_ind_tac "l" prems 1); |
|
186 by (ALLGOALS (ASM_SIMP_TAC list_ss)); |
|
187 val map_list_Collect = result(); |
|
188 |
|
189 (*** theorems about length ***) |
|
190 |
|
191 val prems = goal ListFn.thy |
|
192 "xs: list(A) ==> length(map(h,xs)) = length(xs)"; |
|
193 by (list_ind_tac "xs" prems 1); |
|
194 by (ALLGOALS (ASM_SIMP_TAC list_ss)); |
|
195 val length_map = result(); |
|
196 |
|
197 val prems = goal ListFn.thy |
|
198 "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)"; |
|
199 by (list_ind_tac "xs" prems 1); |
|
200 by (ALLGOALS (ASM_SIMP_TAC list_ss)); |
|
201 val length_app = result(); |
|
202 |
|
203 (* [| m: nat; n: nat |] ==> m #+ succ(n) = succ(n) #+ m |
|
204 Used for rewriting below*) |
|
205 val add_commute_succ = nat_succI RSN (2,add_commute); |
|
206 |
|
207 val prems = goal ListFn.thy |
|
208 "xs: list(A) ==> length(rev(xs)) = length(xs)"; |
|
209 by (list_ind_tac "xs" prems 1); |
|
210 by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [length_app, add_commute_succ]))); |
|
211 val length_rev = result(); |
|
212 |
|
213 val prems = goal ListFn.thy |
|
214 "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))"; |
|
215 by (list_ind_tac "ls" prems 1); |
|
216 by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [length_app]))); |
|
217 val length_flat = result(); |
|
218 |
|
219 (*** theorems about app ***) |
|
220 |
|
221 val [major] = goal ListFn.thy "xs: list(A) ==> xs@Nil=xs"; |
|
222 by (rtac (major RS List.induct) 1); |
|
223 by (ALLGOALS (ASM_SIMP_TAC list_ss)); |
|
224 val app_right_Nil = result(); |
|
225 |
|
226 val prems = goal ListFn.thy "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)"; |
|
227 by (list_ind_tac "xs" prems 1); |
|
228 by (ALLGOALS (ASM_SIMP_TAC list_ss)); |
|
229 val app_assoc = result(); |
|
230 |
|
231 val prems = goal ListFn.thy |
|
232 "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)"; |
|
233 by (list_ind_tac "ls" prems 1); |
|
234 by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [app_assoc]))); |
|
235 val flat_app_distrib = result(); |
|
236 |
|
237 (*** theorems about rev ***) |
|
238 |
|
239 val prems = goal ListFn.thy "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))"; |
|
240 by (list_ind_tac "l" prems 1); |
|
241 by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [map_app_distrib]))); |
|
242 val rev_map_distrib = result(); |
|
243 |
|
244 (*Simplifier needs the premises as assumptions because rewriting will not |
|
245 instantiate the variable ?A in the rules' typing conditions; note that |
|
246 rev_type does not instantiate ?A. Only the premises do. |
|
247 *) |
|
248 val prems = goal ListFn.thy |
|
249 "[| xs: list(A); ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)"; |
|
250 by (cut_facts_tac prems 1); |
|
251 by (etac List.induct 1); |
|
252 by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [app_right_Nil,app_assoc]))); |
|
253 val rev_app_distrib = result(); |
|
254 |
|
255 val prems = goal ListFn.thy "l: list(A) ==> rev(rev(l))=l"; |
|
256 by (list_ind_tac "l" prems 1); |
|
257 by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [rev_app_distrib]))); |
|
258 val rev_rev_ident = result(); |
|
259 |
|
260 val prems = goal ListFn.thy |
|
261 "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))"; |
|
262 by (list_ind_tac "ls" prems 1); |
|
263 by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews |
|
264 [map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil]))); |
|
265 val rev_flat = result(); |
|
266 |
|
267 |
|
268 (*** theorems about list_add ***) |
|
269 |
|
270 val prems = goal ListFn.thy |
|
271 "[| xs: list(nat); ys: list(nat) |] ==> \ |
|
272 \ list_add(xs@ys) = list_add(ys) #+ list_add(xs)"; |
|
273 by (cut_facts_tac prems 1); |
|
274 by (list_ind_tac "xs" prems 1); |
|
275 by (ALLGOALS |
|
276 (ASM_SIMP_TAC (list_ss addrews [add_0_right, add_assoc RS sym]))); |
|
277 by (resolve_tac arith_congs 1); |
|
278 by (REPEAT (ares_tac [refl, list_add_type, add_commute] 1)); |
|
279 val list_add_app = result(); |
|
280 |
|
281 val prems = goal ListFn.thy |
|
282 "l: list(nat) ==> list_add(rev(l)) = list_add(l)"; |
|
283 by (list_ind_tac "l" prems 1); |
|
284 by (ALLGOALS |
|
285 (ASM_SIMP_TAC (list_ss addrews [list_add_app, add_0_right]))); |
|
286 val list_add_rev = result(); |
|
287 |
|
288 val prems = goal ListFn.thy |
|
289 "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))"; |
|
290 by (list_ind_tac "ls" prems 1); |
|
291 by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [list_add_app]))); |
|
292 by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1)); |
|
293 val list_add_flat = result(); |
|
294 |
|
295 (** New induction rule **) |
|
296 |
|
297 val major::prems = goal ListFn.thy |
|
298 "[| l: list(A); \ |
|
299 \ P(Nil); \ |
|
300 \ !!x y. [| x: A; y: list(A); P(y) |] ==> P(y @ [x]) \ |
|
301 \ |] ==> P(l)"; |
|
302 by (rtac (major RS rev_rev_ident RS subst) 1); |
|
303 by (rtac (major RS rev_type RS List.induct) 1); |
|
304 by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews prems))); |
|
305 val list_append_induct = result(); |
|
306 |