279 (*Equivalence to the definition used in Lex/Prefix.thy*) |
279 (*Equivalence to the definition used in Lex/Prefix.thy*) |
280 Goalw [prefix_def] "(xs <= zs) = (EX ys. zs = xs@ys)"; |
280 Goalw [prefix_def] "(xs <= zs) = (EX ys. zs = xs@ys)"; |
281 by (auto_tac (claset(), |
281 by (auto_tac (claset(), |
282 simpset() addsimps [genPrefix_iff_nth, nth_append])); |
282 simpset() addsimps [genPrefix_iff_nth, nth_append])); |
283 by (res_inst_tac [("x", "drop (length xs) zs")] exI 1); |
283 by (res_inst_tac [("x", "drop (length xs) zs")] exI 1); |
284 br nth_equalityI 1; |
284 by (rtac nth_equalityI 1); |
285 by (ALLGOALS (asm_simp_tac (simpset() addsimps [nth_append]))); |
285 by (ALLGOALS (asm_simp_tac (simpset() addsimps [nth_append]))); |
286 qed "prefix_iff"; |
286 qed "prefix_iff"; |
287 |
287 |
288 Goal "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)"; |
288 Goal "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)"; |
289 by (simp_tac (simpset() addsimps [prefix_iff]) 1); |
289 by (simp_tac (simpset() addsimps [prefix_iff]) 1); |
306 addsimps [append_assoc RS sym])1); |
306 addsimps [append_assoc RS sym])1); |
307 by (Force_tac 1); |
307 by (Force_tac 1); |
308 qed "prefix_append_iff"; |
308 qed "prefix_append_iff"; |
309 |
309 |
310 |
310 |
311 (*** pfix_le: partial ordering, etc. ***) |
311 (*** pfixLe, pfixGe: properties inherited from the translations ***) |
312 |
312 |
313 Goalw [refl_def, Le_def] "reflexive Le"; |
313 Goalw [refl_def, Le_def] "reflexive Le"; |
314 auto(); |
314 by Auto_tac; |
315 qed "reflexive_Le"; |
315 qed "reflexive_Le"; |
316 |
316 |
317 Goalw [antisym_def, Le_def] "antisym Le"; |
317 Goalw [antisym_def, Le_def] "antisym Le"; |
318 auto(); |
318 by Auto_tac; |
319 qed "antisym_Le"; |
319 qed "antisym_Le"; |
320 |
320 |
321 Goalw [trans_def, Le_def] "trans Le"; |
321 Goalw [trans_def, Le_def] "trans Le"; |
322 auto(); |
322 by Auto_tac; |
323 qed "trans_Le"; |
323 qed "trans_Le"; |
324 |
324 |
325 AddIffs [reflexive_Le, antisym_Le, trans_Le]; |
325 AddIffs [reflexive_Le, antisym_Le, trans_Le]; |
326 |
326 |
327 Goal "xs pfix_le xs"; |
|
328 by (Simp_tac 1); |
|
329 qed "pfix_le_refl"; |
|
330 AddIffs[pfix_le_refl]; |
|
331 |
|
332 Goal "[| xs pfix_le ys; ys pfix_le zs |] ==> xs pfix_le zs"; |
|
333 by (blast_tac (claset() addIs [genPrefix_trans]) 1); |
|
334 qed "pfix_le_trans"; |
|
335 |
|
336 Goal "[| xs pfix_le ys; ys pfix_le xs |] ==> xs = ys"; |
|
337 by (blast_tac (claset() addIs [genPrefix_antisym]) 1); |
|
338 qed "pfix_le_antisym"; |
|
339 |
|
340 Goal "(xs@ys pfix_le xs@zs) = (ys pfix_le zs)"; |
|
341 by (Simp_tac 1); |
|
342 qed "same_pfix_le_pfix_le"; |
|
343 Addsimps [same_pfix_le_pfix_le]; |
|
344 |
|
345 Goal "[| xs pfix_le ys; length xs < length ys |] \ |
|
346 \ ==> xs @ [ys ! length xs] pfix_le ys"; |
|
347 by (asm_simp_tac (simpset() addsimps [append_one_genPrefix]) 1); |
|
348 qed "append_one_pfix_le"; |
|
349 |
|
350 |
|
351 (*** pfix_ge: partial ordering, etc. ***) |
|
352 |
|
353 Goalw [refl_def, Ge_def] "reflexive Ge"; |
327 Goalw [refl_def, Ge_def] "reflexive Ge"; |
354 auto(); |
328 by Auto_tac; |
355 qed "reflexive_Ge"; |
329 qed "reflexive_Ge"; |
356 |
330 |
357 Goalw [antisym_def, Ge_def] "antisym Ge"; |
331 Goalw [antisym_def, Ge_def] "antisym Ge"; |
358 auto(); |
332 by Auto_tac; |
359 qed "antisym_Ge"; |
333 qed "antisym_Ge"; |
360 |
334 |
361 Goalw [trans_def, Ge_def] "trans Ge"; |
335 Goalw [trans_def, Ge_def] "trans Ge"; |
362 auto(); |
336 by Auto_tac; |
363 qed "trans_Ge"; |
337 qed "trans_Ge"; |
364 |
338 |
365 AddIffs [reflexive_Ge, antisym_Ge, trans_Ge]; |
339 AddIffs [reflexive_Ge, antisym_Ge, trans_Ge]; |
366 |
|
367 Goal "xs pfix_ge xs"; |
|
368 by (Simp_tac 1); |
|
369 qed "pfix_ge_refl"; |
|
370 AddIffs[pfix_ge_refl]; |
|
371 |
|
372 Goal "[| xs pfix_ge ys; ys pfix_ge zs |] ==> xs pfix_ge zs"; |
|
373 by (blast_tac (claset() addIs [genPrefix_trans]) 1); |
|
374 qed "pfix_ge_trans"; |
|
375 |
|
376 Goal "[| xs pfix_ge ys; ys pfix_ge xs |] ==> xs = ys"; |
|
377 by (blast_tac (claset() addIs [genPrefix_antisym]) 1); |
|
378 qed "pfix_ge_antisym"; |
|
379 |
|
380 Goal "(xs@ys pfix_ge xs@zs) = (ys pfix_ge zs)"; |
|
381 by (Simp_tac 1); |
|
382 qed "same_pfix_ge_pfix_ge"; |
|
383 Addsimps [same_pfix_ge_pfix_ge]; |
|
384 |
|
385 Goal "[| xs pfix_ge ys; length xs < length ys |] \ |
|
386 \ ==> xs @ [ys ! length xs] pfix_ge ys"; |
|
387 by (asm_simp_tac (simpset() addsimps [append_one_genPrefix]) 1); |
|
388 qed "append_one_pfix_ge"; |
|