|
1 (* Title: ZF/UNITY/GenPrefix.ML |
|
2 ID: $Id$ |
|
3 Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
|
4 Copyright 2001 University of Cambridge |
|
5 |
|
6 Charpentier's Generalized Prefix Relation |
|
7 <xs,ys>:gen_prefix(r) |
|
8 if ys = xs' @ zs where length(xs) = length(xs') |
|
9 and corresponding elements of xs, xs' are pairwise related by r |
|
10 |
|
11 Based on Lex/Prefix |
|
12 *) |
|
13 |
|
14 Goalw [refl_def] |
|
15 "[| refl(A, r); x:A |] ==> <x,x>:r"; |
|
16 by Auto_tac; |
|
17 qed "reflD"; |
|
18 |
|
19 (*** preliminary lemmas ***) |
|
20 |
|
21 Goal "xs:list(A) ==> <[], xs>:gen_prefix(A, r)"; |
|
22 by (dtac (rotate_prems 1 gen_prefix.append) 1); |
|
23 by (rtac gen_prefix.Nil 1); |
|
24 by Auto_tac; |
|
25 qed "Nil_gen_prefix"; |
|
26 Addsimps [Nil_gen_prefix]; |
|
27 |
|
28 |
|
29 Goal "<xs,ys>:gen_prefix(A, r) ==> length(xs) le length(ys)"; |
|
30 by (etac gen_prefix.induct 1); |
|
31 by (subgoal_tac "ys:list(A)" 3); |
|
32 by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD] |
|
33 addIs [le_trans], |
|
34 simpset() addsimps [length_app])); |
|
35 qed "gen_prefix_length_le"; |
|
36 |
|
37 |
|
38 Goal "[| <xs', ys'>:gen_prefix(A, r) |] \ |
|
39 \ ==> (ALL x xs. x:A --> xs'= Cons(x,xs) --> \ |
|
40 \ (EX y ys. y:A & ys' = Cons(y,ys) &\ |
|
41 \ <x,y>:r & <xs, ys>:gen_prefix(A, r)))"; |
|
42 by (etac gen_prefix.induct 1); |
|
43 by (force_tac (claset() addIs [gen_prefix.append], |
|
44 simpset()) 3); |
|
45 by (REPEAT(Asm_simp_tac 1)); |
|
46 val lemma = result(); |
|
47 |
|
48 (*As usual converting it to an elimination rule is tiresome*) |
|
49 val major::prems = |
|
50 Goal "[| <Cons(x,xs), zs>:gen_prefix(A, r); \ |
|
51 \ !!y ys. [|zs = Cons(y, ys); y:A; x:A; <x,y>:r; \ |
|
52 \ <xs,ys>:gen_prefix(A, r) |] ==> P \ |
|
53 \ |] ==> P"; |
|
54 by (cut_facts_tac [major] 1); |
|
55 by (forward_tac [gen_prefix.dom_subset RS subsetD] 1); |
|
56 by (Clarify_tac 1); |
|
57 by (etac ConsE 1); |
|
58 by (cut_facts_tac [major RS lemma] 1); |
|
59 by (Full_simp_tac 1); |
|
60 by (dtac mp 1); |
|
61 by (Asm_simp_tac 1); |
|
62 by (REPEAT (eresolve_tac [exE, conjE] 1)); |
|
63 by (REPEAT (ares_tac prems 1)); |
|
64 qed "Cons_gen_prefixE"; |
|
65 AddSEs [Cons_gen_prefixE]; |
|
66 |
|
67 Goal |
|
68 "(<Cons(x,xs),Cons(y,ys)>:gen_prefix(A, r)) \ |
|
69 \ <-> (x:A & y:A & <x,y>:r & <xs,ys>:gen_prefix(A, r))"; |
|
70 by (auto_tac (claset() addIs [gen_prefix.prepend], simpset())); |
|
71 qed"Cons_gen_prefix_Cons"; |
|
72 AddIffs [Cons_gen_prefix_Cons]; |
|
73 |
|
74 (** Monotonicity of gen_prefix **) |
|
75 |
|
76 Goal "r<=s ==> gen_prefix(A, r) <= gen_prefix(A, s)"; |
|
77 by (Clarify_tac 1); |
|
78 by (forward_tac [gen_prefix.dom_subset RS subsetD] 1); |
|
79 by (Clarify_tac 1); |
|
80 by (etac rev_mp 1); |
|
81 by (etac gen_prefix.induct 1); |
|
82 by (auto_tac (claset() addIs |
|
83 [gen_prefix.append], simpset())); |
|
84 qed "gen_prefix_mono2"; |
|
85 |
|
86 Goal "A<=B ==>gen_prefix(A, r) <= gen_prefix(B, r)"; |
|
87 by (Clarify_tac 1); |
|
88 by (forward_tac [gen_prefix.dom_subset RS subsetD] 1); |
|
89 by (Clarify_tac 1); |
|
90 by (etac rev_mp 1); |
|
91 by (eres_inst_tac [("P", "y:list(A)")] rev_mp 1); |
|
92 by (eres_inst_tac [("P", "xa:list(A)")] rev_mp 1); |
|
93 by (etac gen_prefix.induct 1); |
|
94 by (Asm_simp_tac 1); |
|
95 by (Clarify_tac 1); |
|
96 by (REPEAT(etac ConsE 1)); |
|
97 by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD] |
|
98 addIs [gen_prefix.append, list_mono RS subsetD], |
|
99 simpset())); |
|
100 qed "gen_prefix_mono1"; |
|
101 |
|
102 Goal "[| A <= B; r <= s |] ==> gen_prefix(A, r) <= gen_prefix(B, s)"; |
|
103 by (rtac subset_trans 1); |
|
104 by (rtac gen_prefix_mono1 1); |
|
105 by (rtac gen_prefix_mono2 2); |
|
106 by Auto_tac; |
|
107 qed "gen_prefix_mono"; |
|
108 |
|
109 (*** gen_prefix order ***) |
|
110 |
|
111 (* reflexivity *) |
|
112 Goalw [refl_def] "refl(A, r) ==> refl(list(A), gen_prefix(A, r))"; |
|
113 by Auto_tac; |
|
114 by (induct_tac "x" 1); |
|
115 by Auto_tac; |
|
116 qed "refl_gen_prefix"; |
|
117 Addsimps [refl_gen_prefix RS reflD]; |
|
118 |
|
119 (* Transitivity *) |
|
120 (* A lemma for proving gen_prefix_trans_comp *) |
|
121 |
|
122 Goal "xs:list(A) ==> \ |
|
123 \ ALL zs. <xs @ ys, zs>:gen_prefix(A, r) --> <xs, zs>: gen_prefix(A, r)"; |
|
124 by (etac list.induct 1); |
|
125 by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD], simpset())); |
|
126 qed_spec_mp "append_gen_prefix"; |
|
127 |
|
128 (* Lemma proving transitivity and more*) |
|
129 |
|
130 Goal "<x, y>: gen_prefix(A, r) ==> \ |
|
131 \ (ALL z:list(A). <y,z>:gen_prefix(A, s)--><x, z>:gen_prefix(A, s O r))"; |
|
132 by (etac gen_prefix.induct 1); |
|
133 by (auto_tac (claset() addEs [ConsE], simpset() addsimps [Nil_gen_prefix])); |
|
134 by (subgoal_tac "ys:list(A)" 1); |
|
135 by (blast_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]) 2); |
|
136 by (dres_inst_tac [("xs", "ys"), ("r", "s")] append_gen_prefix 1); |
|
137 by Auto_tac; |
|
138 qed_spec_mp "gen_prefix_trans_comp"; |
|
139 |
|
140 Goal "trans(r) ==> r O r <= r"; |
|
141 by (auto_tac (claset() addDs [transD], simpset())); |
|
142 qed "trans_comp_subset"; |
|
143 |
|
144 Goal "trans(r) ==> trans(gen_prefix(A,r))"; |
|
145 by (simp_tac (simpset() addsimps [trans_def]) 1); |
|
146 by (Clarify_tac 1); |
|
147 by (rtac (impOfSubs (trans_comp_subset RS gen_prefix_mono2)) 1); |
|
148 by (assume_tac 2); |
|
149 by (rtac gen_prefix_trans_comp 1); |
|
150 by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD], simpset())); |
|
151 qed_spec_mp "trans_gen_prefix"; |
|
152 |
|
153 Goal |
|
154 "trans(r) ==> trans[list(A)](gen_prefix(A, r))"; |
|
155 by (dres_inst_tac [("A", "A")] trans_gen_prefix 1); |
|
156 by (rewrite_goal_tac [trans_def, trans_on_def] 1); |
|
157 by (Blast_tac 1); |
|
158 qed "trans_on_gen_prefix"; |
|
159 |
|
160 Goalw [prefix_def] |
|
161 "[| <x,y>:prefix(A); <y, z>:gen_prefix(A, r); r<=A*A |] \ |
|
162 \ ==> <x, z>:gen_prefix(A, r)"; |
|
163 by (res_inst_tac [("P", "%r. <x,z>:gen_prefix(A, r)")] |
|
164 (right_comp_id RS subst) 1); |
|
165 by (REPEAT(blast_tac (claset() addDs [gen_prefix_trans_comp, |
|
166 gen_prefix.dom_subset RS subsetD]) 1)); |
|
167 qed_spec_mp "prefix_gen_prefix_trans"; |
|
168 |
|
169 |
|
170 Goalw [prefix_def] |
|
171 "[| <x,y>:gen_prefix(A,r); <y, z>:prefix(A); r<=A*A |] \ |
|
172 \ ==> <x, z>:gen_prefix(A, r)"; |
|
173 by (res_inst_tac [("P", "%r. <x,z>:gen_prefix(A, r)")] (left_comp_id RS subst) 1); |
|
174 by (REPEAT(blast_tac (claset() addDs [gen_prefix_trans_comp, |
|
175 gen_prefix.dom_subset RS subsetD]) 1)); |
|
176 qed_spec_mp "gen_prefix_prefix_trans"; |
|
177 |
|
178 (** Antisymmetry **) |
|
179 |
|
180 Goal "n:nat ==> ALL b:nat. n #+ b le n --> b = 0"; |
|
181 by (induct_tac "n" 1); |
|
182 by Auto_tac; |
|
183 qed_spec_mp "nat_le_lemma"; |
|
184 |
|
185 Goal "antisym(r) ==> antisym(gen_prefix(A, r))"; |
|
186 by (simp_tac (simpset() addsimps [antisym_def]) 1); |
|
187 by (rtac (impI RS allI RS allI) 1); |
|
188 by (etac gen_prefix.induct 1); |
|
189 by (full_simp_tac (simpset() addsimps [antisym_def]) 2); |
|
190 by (Blast_tac 2); |
|
191 by (Blast_tac 1); |
|
192 (*append case is hardest*) |
|
193 by (Clarify_tac 1); |
|
194 by (subgoal_tac "length(zs) = 0" 1); |
|
195 by (subgoal_tac "ys:list(A)" 1); |
|
196 by (blast_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]) 2); |
|
197 by (dres_inst_tac [("psi", "<ys @ zs, xs>:gen_prefix(A,r)")] asm_rl 1); |
|
198 by (Asm_full_simp_tac 1); |
|
199 by (subgoal_tac "length(ys @ zs) = length(ys) #+ length(zs) &ys:list(A)&xs:list(A)" 1); |
|
200 by (blast_tac (claset() addIs [length_app] |
|
201 addDs [gen_prefix.dom_subset RS subsetD]) 2); |
|
202 by (REPEAT (dtac gen_prefix_length_le 1)); |
|
203 by (Clarify_tac 1); |
|
204 by (Asm_full_simp_tac 1); |
|
205 by (dres_inst_tac [("j", "length(xs)")] le_trans 1); |
|
206 by (Blast_tac 1); |
|
207 by (auto_tac (claset() addIs [nat_le_lemma], simpset())); |
|
208 qed_spec_mp "antisym_gen_prefix"; |
|
209 |
|
210 (*** recursion equations ***) |
|
211 |
|
212 Goal "xs:list(A) ==> <xs, []>:gen_prefix(A,r) <-> (xs = [])"; |
|
213 by (induct_tac "xs" 1); |
|
214 by Auto_tac; |
|
215 qed "gen_prefix_Nil"; |
|
216 Addsimps [gen_prefix_Nil]; |
|
217 |
|
218 Goalw [refl_def] |
|
219 "[| refl(A, r); xs:list(A) |] ==> \ |
|
220 \ <xs@ys, xs@zs>: gen_prefix(A, r) <-> <ys,zs>:gen_prefix(A, r)"; |
|
221 by (induct_tac "xs" 1); |
|
222 by (ALLGOALS Asm_simp_tac); |
|
223 qed "same_gen_prefix_gen_prefix"; |
|
224 Addsimps [same_gen_prefix_gen_prefix]; |
|
225 |
|
226 Goal "[| xs:list(A); ys:list(A); y:A |] ==> \ |
|
227 \ <xs, Cons(y,ys)> : gen_prefix(A,r) <-> \ |
|
228 \ (xs=[] | (EX z zs. xs=Cons(z,zs) & z:A & <z,y>:r & <zs,ys>:gen_prefix(A,r)))"; |
|
229 by (induct_tac "xs" 1); |
|
230 by Auto_tac; |
|
231 qed "gen_prefix_Cons"; |
|
232 |
|
233 Goal "[| refl(A,r); <xs,ys>:gen_prefix(A, r); zs:list(A) |] \ |
|
234 \ ==> <xs@zs, take(length(xs), ys) @ zs> : gen_prefix(A, r)"; |
|
235 by (etac gen_prefix.induct 1); |
|
236 by (Asm_simp_tac 1); |
|
237 by (ALLGOALS(forward_tac [gen_prefix.dom_subset RS subsetD])); |
|
238 by Auto_tac; |
|
239 by (ftac gen_prefix_length_le 1); |
|
240 by (subgoal_tac "take(length(xs), ys):list(A)" 1); |
|
241 by (ALLGOALS (asm_simp_tac (simpset() addsimps |
|
242 [diff_is_0_iff RS iffD2, take_type ]))); |
|
243 qed "gen_prefix_take_append"; |
|
244 |
|
245 Goal "[| refl(A, r); <xs,ys>:gen_prefix(A,r); \ |
|
246 \ length(xs) = length(ys); zs:list(A) |] \ |
|
247 \ ==> <xs@zs, ys @ zs> : gen_prefix(A, r)"; |
|
248 by (dres_inst_tac [("zs", "zs")] gen_prefix_take_append 1); |
|
249 by (REPEAT(assume_tac 1)); |
|
250 by (subgoal_tac "take(length(xs), ys)=ys" 1); |
|
251 by (auto_tac (claset() addSIs [take_all] |
|
252 addDs [gen_prefix.dom_subset RS subsetD], |
|
253 simpset())); |
|
254 qed "gen_prefix_append_both"; |
|
255 |
|
256 (*NOT suitable for rewriting since [y] has the form y#ys*) |
|
257 Goal "xs:list(A) ==> xs @ Cons(y, ys) = (xs @ [y]) @ ys"; |
|
258 by (auto_tac (claset(), simpset() addsimps [app_assoc])); |
|
259 qed "append_cons_conv"; |
|
260 |
|
261 Goal "[| <xs,ys>:gen_prefix(A, r); refl(A, r) |] \ |
|
262 \ ==> length(xs) < length(ys) --> \ |
|
263 \ <xs @ [nth(length(xs), ys)], ys>:gen_prefix(A, r)"; |
|
264 by (etac gen_prefix.induct 1); |
|
265 by (Blast_tac 1); |
|
266 by (forward_tac [gen_prefix.dom_subset RS subsetD] 1); |
|
267 by (Clarify_tac 1); |
|
268 by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [length_type]))); |
|
269 (* Append case is hardest *) |
|
270 by (forward_tac [gen_prefix_length_le RS (le_iff RS iffD1) ] 1); |
|
271 by (forward_tac [gen_prefix.dom_subset RS subsetD] 1); |
|
272 by (Clarify_tac 1); |
|
273 by (subgoal_tac "length(xs):nat&length(ys):nat &length(zs):nat" 1); |
|
274 by (blast_tac (claset() addIs [length_type]) 2); |
|
275 by (Clarify_tac 1); |
|
276 by (ALLGOALS (asm_full_simp_tac (simpset() |
|
277 addsimps [nth_append, length_type, length_app]))); |
|
278 by (Clarify_tac 1); |
|
279 by (rtac conjI 1); |
|
280 by (blast_tac (claset() addIs [gen_prefix.append]) 1); |
|
281 by (thin_tac "length(xs) < length(ys) -->?u" 1); |
|
282 by (case_tac "zs=[]" 1); |
|
283 by (auto_tac (claset(), simpset() addsimps [neq_Nil_iff])); |
|
284 by (res_inst_tac [("P1", "%x. <?u(x), ?v>:?w")] (nat_diff_split RS iffD2) 1); |
|
285 by Auto_tac; |
|
286 by (stac append_cons_conv 1); |
|
287 by (rtac gen_prefix.append 2); |
|
288 by (auto_tac (claset() addEs [ConsE], |
|
289 simpset() addsimps [gen_prefix_append_both])); |
|
290 val lemma = result() RS mp; |
|
291 |
|
292 Goal "[| <xs,ys>: gen_prefix(A, r); length(xs) < length(ys); refl(A, r) |] \ |
|
293 \ ==> <xs @ [nth(length(xs), ys)], ys>:gen_prefix(A, r)"; |
|
294 by (blast_tac (claset() addIs [lemma]) 1); |
|
295 qed "append_one_gen_prefix"; |
|
296 |
|
297 |
|
298 (** Proving the equivalence with Charpentier's definition **) |
|
299 |
|
300 Goal "xs:list(A) ==> \ |
|
301 \ ALL ys:list(A). ALL i:nat. i < length(xs) \ |
|
302 \ --> <xs, ys>: gen_prefix(A, r) --> <nth(i, xs), nth(i, ys)>:r"; |
|
303 by (induct_tac "xs" 1); |
|
304 by (ALLGOALS(Clarify_tac)); |
|
305 by (ALLGOALS(Asm_full_simp_tac)); |
|
306 by (etac natE 1); |
|
307 by (ALLGOALS(Asm_full_simp_tac)); |
|
308 by (dres_inst_tac [("x", "ysa")] bspec 1); |
|
309 by (dres_inst_tac [("x", "x")] bspec 2); |
|
310 by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD], simpset())); |
|
311 qed_spec_mp "gen_prefix_imp_nth"; |
|
312 |
|
313 Goal "xs:list(A) ==> \ |
|
314 \ ALL ys:list(A). length(xs) le length(ys) \ |
|
315 \ --> (ALL i:nat. i < length(xs)--> <nth(i, xs), nth(i,ys)>:r) \ |
|
316 \ --> <xs, ys> : gen_prefix(A, r)"; |
|
317 by (induct_tac "xs" 1); |
|
318 by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_succ_eq_0_disj]))); |
|
319 by (Clarify_tac 1); |
|
320 by (case_tac "x=[]" 1); |
|
321 by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [neq_Nil_iff]))); |
|
322 by (Clarify_tac 1); |
|
323 by (dres_inst_tac [("x", "ys")] bspec 1); |
|
324 by (ALLGOALS(Clarify_tac)); |
|
325 by Auto_tac; |
|
326 qed_spec_mp "nth_imp_gen_prefix"; |
|
327 |
|
328 Goal "(<xs,ys>: gen_prefix(A,r)) <-> \ |
|
329 \ (xs:list(A) & ys:list(A) & length(xs) le length(ys) & \ |
|
330 \ (ALL i:nat. i < length(xs) --> <nth(i,xs), nth(i, ys)>: r))"; |
|
331 by (rtac iffI 1); |
|
332 by (forward_tac [gen_prefix.dom_subset RS subsetD] 1); |
|
333 by (forward_tac [gen_prefix_length_le] 1); |
|
334 by (ALLGOALS(Clarify_tac)); |
|
335 by (rtac nth_imp_gen_prefix 2); |
|
336 by (dtac (rotate_prems 4 gen_prefix_imp_nth) 1); |
|
337 by Auto_tac; |
|
338 qed "gen_prefix_iff_nth"; |
|
339 |
|
340 (** prefix is a partial order: **) |
|
341 |
|
342 Goalw [prefix_def] |
|
343 "refl(list(A), prefix(A))"; |
|
344 by (rtac refl_gen_prefix 1); |
|
345 by (auto_tac (claset(), simpset() addsimps [refl_def])); |
|
346 qed "refl_prefix"; |
|
347 Addsimps [refl_prefix RS reflD]; |
|
348 |
|
349 Goalw [prefix_def] "trans(prefix(A))"; |
|
350 by (rtac trans_gen_prefix 1); |
|
351 by (auto_tac (claset(), simpset() addsimps [trans_def])); |
|
352 qed "trans_prefix"; |
|
353 |
|
354 bind_thm("prefix_trans", trans_prefix RS transD); |
|
355 |
|
356 Goalw [prefix_def] "trans[list(A)](prefix(A))"; |
|
357 by (rtac trans_on_gen_prefix 1); |
|
358 by (auto_tac (claset(), simpset() addsimps [trans_def])); |
|
359 qed "trans_on_prefix"; |
|
360 |
|
361 bind_thm("prefix_trans_on", trans_on_prefix RS trans_onD); |
|
362 |
|
363 (* Monotonicity of "set" operator WRT prefix *) |
|
364 |
|
365 Goalw [prefix_def] |
|
366 "<xs,ys>:prefix(A) ==> set_of_list(xs) <= set_of_list(ys)"; |
|
367 by (etac gen_prefix.induct 1); |
|
368 by (subgoal_tac "xs:list(A)&ys:list(A)" 3); |
|
369 by (blast_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]) 4); |
|
370 by (auto_tac (claset(), simpset() addsimps [set_of_list_append])); |
|
371 qed "set_of_list_prefix_mono"; |
|
372 |
|
373 (** recursion equations **) |
|
374 |
|
375 Goalw [prefix_def] "xs:list(A) ==> <[],xs>:prefix(A)"; |
|
376 by (asm_simp_tac (simpset() addsimps [Nil_gen_prefix]) 1); |
|
377 qed "Nil_prefix"; |
|
378 Addsimps[Nil_prefix]; |
|
379 |
|
380 |
|
381 Goalw [prefix_def] "<xs, []>:prefix(A) <-> (xs = [])"; |
|
382 by Auto_tac; |
|
383 by (forward_tac [gen_prefix.dom_subset RS subsetD] 1); |
|
384 by (dres_inst_tac [("psi", "<xs, []>:gen_prefix(A, id(A))")] asm_rl 1); |
|
385 by (asm_full_simp_tac (simpset() addsimps [gen_prefix_Nil]) 1); |
|
386 qed "prefix_Nil"; |
|
387 AddIffs [prefix_Nil]; |
|
388 |
|
389 Goalw [prefix_def] |
|
390 "<Cons(x,xs), Cons(y,ys)>:prefix(A) <-> (x=y & <xs,ys>:prefix(A) & y:A)"; |
|
391 by Auto_tac; |
|
392 qed"Cons_prefix_Cons"; |
|
393 AddIffs [Cons_prefix_Cons]; |
|
394 |
|
395 Goalw [prefix_def] |
|
396 "xs:list(A)==> <xs@ys,xs@zs>:prefix(A) <-> (<ys,zs>:prefix(A))"; |
|
397 by (subgoal_tac "refl(A,id(A))" 1); |
|
398 by (Asm_simp_tac 1); |
|
399 by (auto_tac (claset(), simpset() addsimps[refl_def])); |
|
400 qed "same_prefix_prefix"; |
|
401 Addsimps [same_prefix_prefix]; |
|
402 |
|
403 Goal "xs:list(A) ==> <xs@ys,xs>:prefix(A) <-> (<ys,[]>:prefix(A))"; |
|
404 by (res_inst_tac [("P", "%x. <?u, x>:?v <-> ?w(x)")] (app_right_Nil RS subst) 1); |
|
405 by (rtac same_prefix_prefix 2); |
|
406 by Auto_tac; |
|
407 qed "same_prefix_prefix_Nil"; |
|
408 Addsimps [same_prefix_prefix_Nil]; |
|
409 |
|
410 Goalw [prefix_def] |
|
411 "[| <xs,ys>:prefix(A); zs:list(A) |] ==> <xs,ys@zs>:prefix(A)"; |
|
412 by (etac gen_prefix.append 1); |
|
413 by (assume_tac 1); |
|
414 qed "prefix_appendI"; |
|
415 Addsimps [prefix_appendI]; |
|
416 |
|
417 Goalw [prefix_def] |
|
418 "[| xs:list(A); ys:list(A); y:A |] ==> \ |
|
419 \ <xs,Cons(y,ys)>:prefix(A) <-> \ |
|
420 \ (xs=[] | (EX zs. xs=Cons(y,zs) & <zs,ys>:prefix(A)))"; |
|
421 by (auto_tac (claset(), simpset() addsimps [gen_prefix_Cons])); |
|
422 qed "prefix_Cons"; |
|
423 |
|
424 Goalw [prefix_def] |
|
425 "[| <xs,ys>:prefix(A); length(xs) < length(ys) |] \ |
|
426 \ ==> <xs @ [nth(length(xs),ys)], ys>:prefix(A)"; |
|
427 by (subgoal_tac "refl(A, id(A))" 1); |
|
428 by (asm_simp_tac (simpset() addsimps [append_one_gen_prefix]) 1); |
|
429 by (auto_tac (claset(), simpset() addsimps [refl_def])); |
|
430 qed "append_one_prefix"; |
|
431 |
|
432 Goalw [prefix_def] |
|
433 "<xs,ys>:prefix(A) ==> length(xs) le length(ys)"; |
|
434 by (blast_tac (claset() addDs [gen_prefix_length_le]) 1); |
|
435 qed "prefix_length_le"; |
|
436 |
|
437 Goalw [prefix_def] |
|
438 "<xs,ys>:prefix(A) ==> xs~=ys --> length(xs) < length(ys)"; |
|
439 by (etac gen_prefix.induct 1); |
|
440 by (Clarify_tac 1); |
|
441 by (ALLGOALS(subgoal_tac "ys:list(A)&xs:list(A)")); |
|
442 by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD], |
|
443 simpset() addsimps [length_app, length_type])); |
|
444 by (subgoal_tac "length(zs)=0" 1); |
|
445 by (dtac not_lt_imp_le 2); |
|
446 by (res_inst_tac [("j", "length(ys)")] lt_trans2 5); |
|
447 by Auto_tac; |
|
448 val lemma = result(); |
|
449 |
|
450 Goalw [prefix_def] |
|
451 "prefix(A)<=list(A)*list(A)"; |
|
452 by (blast_tac (claset() addSIs [gen_prefix.dom_subset]) 1); |
|
453 qed "prefix_type"; |
|
454 |
|
455 Goalw [strict_prefix_def] |
|
456 "strict_prefix(A) <= list(A)*list(A)"; |
|
457 by (blast_tac (claset() addSIs [prefix_type RS subsetD]) 1); |
|
458 qed "strict_prefix_type"; |
|
459 |
|
460 Goalw [strict_prefix_def] |
|
461 "<xs,ys>:strict_prefix(A) ==> length(xs) < length(ys)"; |
|
462 by (resolve_tac [lemma RS mp] 1); |
|
463 by (auto_tac (claset() addDs [prefix_type RS subsetD], simpset())); |
|
464 qed "strict_prefix_length_lt"; |
|
465 |
|
466 (*Equivalence to the definition used in Lex/Prefix.thy*) |
|
467 Goalw [prefix_def] |
|
468 "<xs,zs>:prefix(A) <-> (EX ys:list(A). zs = xs@ys) & xs:list(A)"; |
|
469 by (auto_tac (claset(), |
|
470 simpset() addsimps [gen_prefix_iff_nth, |
|
471 nth_append, nth_type, app_type, length_app])); |
|
472 by (subgoal_tac "length(xs):nat&length(zs):nat & \ |
|
473 \ drop(length(xs), zs):list(A)" 1); |
|
474 by (res_inst_tac [("x", "drop(length(xs), zs)")] bexI 1); |
|
475 by (ALLGOALS(Clarify_tac)); |
|
476 by (asm_simp_tac (simpset() addsimps [length_type, drop_type]) 2); |
|
477 by (rtac nth_equalityI 1); |
|
478 by (ALLGOALS (asm_simp_tac (simpset() addsimps |
|
479 [nth_append, app_type, drop_type, length_app, length_drop]))); |
|
480 by (rtac (nat_diff_split RS iffD2) 1); |
|
481 by (ALLGOALS(Asm_full_simp_tac)); |
|
482 by (Clarify_tac 1); |
|
483 by (dres_inst_tac [("i", "length(zs)")] leI 1); |
|
484 by (force_tac (claset(), simpset() addsimps [le_subset_iff]) 1); |
|
485 by Safe_tac; |
|
486 by (Blast_tac 1); |
|
487 by (subgoal_tac "length(xs) #+ (x #- length(xs)) = x" 1); |
|
488 by (rtac (nth_drop RS ssubst) 1); |
|
489 by (ALLGOALS(asm_simp_tac (simpset() addsimps [leI]))); |
|
490 by (rtac (nat_diff_split RS iffD2) 1); |
|
491 by Auto_tac; |
|
492 qed "prefix_iff"; |
|
493 |
|
494 Goal |
|
495 "[|xs:list(A); ys:list(A); y:A |] ==> \ |
|
496 \ <xs, ys@[y]>:prefix(A) <-> (xs = ys@[y] | <xs,ys>:prefix(A))"; |
|
497 by (simp_tac (simpset() addsimps [prefix_iff]) 1); |
|
498 by (rtac iffI 1); |
|
499 by (Clarify_tac 1); |
|
500 by (eres_inst_tac [("xs", "ysa")] rev_list_elim 1); |
|
501 by (Asm_full_simp_tac 1); |
|
502 by (dres_inst_tac [("psi", "ya:list(A)")] asm_rl 1); |
|
503 by (rotate_tac ~1 1); |
|
504 by (asm_full_simp_tac (simpset() addsimps |
|
505 [app_type, app_assoc RS sym] delsimps [app_assoc]) 1); |
|
506 by (auto_tac (claset(), simpset() addsimps [app_assoc, app_type])); |
|
507 qed "prefix_snoc"; |
|
508 Addsimps [prefix_snoc]; |
|
509 |
|
510 |
|
511 Goal "zs:list(A) ==> ALL xs:list(A). ALL ys:list(A). \ |
|
512 \ (<xs, ys@zs>:prefix(A)) <-> \ |
|
513 \ (<xs,ys>:prefix(A) | (EX us. xs = ys@us & <us,zs>:prefix(A)))"; |
|
514 by (etac list_append_induct 1); |
|
515 by (Clarify_tac 2); |
|
516 by (rtac iffI 2); |
|
517 by (asm_full_simp_tac (simpset() delsimps [app_assoc] |
|
518 addsimps [app_assoc RS sym]) 2); |
|
519 by (etac disjE 2 THEN etac disjE 3); |
|
520 by (rtac disjI2 2); |
|
521 by (res_inst_tac [("x", "y @ [x]")] exI 2); |
|
522 by (asm_full_simp_tac (simpset() delsimps [app_assoc] |
|
523 addsimps [app_assoc RS sym]) 2); |
|
524 by (REPEAT(Force_tac 1)); |
|
525 qed_spec_mp "prefix_append_iff"; |
|
526 |
|
527 |
|
528 (*Although the prefix ordering is not linear, the prefixes of a list |
|
529 are linearly ordered.*) |
|
530 Goal "[| zs:list(A); xs:list(A); ys:list(A) |] \ |
|
531 \ ==> <xs, zs>:prefix(A) --> <ys,zs>:prefix(A) \ |
|
532 \ --><xs,ys>:prefix(A) | <ys,xs>:prefix(A)"; |
|
533 by (etac list_append_induct 1); |
|
534 by Auto_tac; |
|
535 qed_spec_mp "common_prefix_linear"; |
|
536 |
|
537 |
|
538 (*** pfixLe, pfixGe: properties inherited from the translations ***) |
|
539 |
|
540 |
|
541 |
|
542 (** pfixLe **) |
|
543 |
|
544 Goalw [refl_def, Le_def] "refl(nat,Le)"; |
|
545 by Auto_tac; |
|
546 qed "refl_Le"; |
|
547 AddIffs [refl_Le]; |
|
548 |
|
549 Goalw [antisym_def, Le_def] "antisym(Le)"; |
|
550 by (auto_tac (claset() addIs [le_anti_sym], simpset())); |
|
551 qed "antisym_Le"; |
|
552 AddIffs [antisym_Le]; |
|
553 |
|
554 Goalw [trans_def, Le_def] "trans(Le)"; |
|
555 by (auto_tac (claset() addIs [le_trans], simpset())); |
|
556 qed "trans_Le"; |
|
557 AddIffs [trans_Le]; |
|
558 |
|
559 Goal "x:list(nat) ==> x pfixLe x"; |
|
560 by (blast_tac (claset() addIs [refl_gen_prefix RS reflD]) 1); |
|
561 qed "pfixLe_refl"; |
|
562 Addsimps[pfixLe_refl]; |
|
563 |
|
564 Goal "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z"; |
|
565 by (blast_tac (claset() addIs [trans_gen_prefix RS transD]) 1); |
|
566 qed "pfixLe_trans"; |
|
567 |
|
568 Goal "[| x pfixLe y; y pfixLe x |] ==> x = y"; |
|
569 by (blast_tac (claset() addIs [antisym_gen_prefix RS antisymE]) 1); |
|
570 qed "pfixLe_antisym"; |
|
571 |
|
572 |
|
573 Goalw [prefix_def, Le_def] |
|
574 "<xs,ys>:prefix(nat)==> xs pfixLe ys"; |
|
575 by (rtac (gen_prefix_mono RS subsetD) 1); |
|
576 by Auto_tac; |
|
577 qed "prefix_imp_pfixLe"; |
|
578 |
|
579 Goalw [refl_def, Ge_def] "refl(nat, Ge)"; |
|
580 by Auto_tac; |
|
581 qed "refl_Ge"; |
|
582 AddIffs [refl_Ge]; |
|
583 |
|
584 Goalw [antisym_def, Ge_def] "antisym(Ge)"; |
|
585 by (auto_tac (claset() addIs [le_anti_sym], simpset())); |
|
586 qed "antisym_Ge"; |
|
587 AddIffs [antisym_Ge]; |
|
588 |
|
589 Goalw [trans_def, Ge_def] "trans(Ge)"; |
|
590 by (auto_tac (claset() addIs [le_trans], simpset())); |
|
591 qed "trans_Ge"; |
|
592 AddIffs [trans_Ge]; |
|
593 |
|
594 Goal "x:list(nat) ==> x pfixGe x"; |
|
595 by (blast_tac (claset() addIs [refl_gen_prefix RS reflD]) 1); |
|
596 qed "pfixGe_refl"; |
|
597 Addsimps[pfixGe_refl]; |
|
598 |
|
599 Goal "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z"; |
|
600 by (blast_tac (claset() addIs [trans_gen_prefix RS transD]) 1); |
|
601 qed "pfixGe_trans"; |
|
602 |
|
603 Goal "[| x pfixGe y; y pfixGe x |] ==> x = y"; |
|
604 by (blast_tac (claset() addIs [antisym_gen_prefix RS antisymE]) 1); |
|
605 qed "pfixGe_antisym"; |
|
606 |
|
607 Goalw [prefix_def, Ge_def] |
|
608 "<xs,ys>:prefix(nat) ==> xs pfixGe ys"; |
|
609 by (rtac (gen_prefix_mono RS subsetD) 1); |
|
610 by Auto_tac; |
|
611 qed "prefix_imp_pfixGe"; |
|
612 |
|
613 |
|
614 |
|
615 |
|
616 |
|
617 |