1 (* Title: HOL/Lex/MaxChop.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1998 TUM |
|
5 *) |
|
6 |
|
7 (* Termination of chop *) |
|
8 |
|
9 Goalw [reducing_def] "reducing(%qs. maxsplit P ([],qs) [] qs)"; |
|
10 by (asm_full_simp_tac (simpset() addsimps [maxsplit_eq]) 1); |
|
11 qed "reducing_maxsplit"; |
|
12 |
|
13 val [tc] = chopr.tcs; |
|
14 goalw_cterm [reducing_def] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc)); |
|
15 by (blast_tac (claset() addDs [sym]) 1); |
|
16 val lemma = result(); |
|
17 |
|
18 val chopr_rule = let val [chopr_rule] = chopr.simps in lemma RS chopr_rule end; |
|
19 |
|
20 Goalw [chop_def] "reducing splitf ==> \ |
|
21 \ chop splitf xs = (let (pre,post) = splitf xs \ |
|
22 \ in if pre=[] then ([],xs) \ |
|
23 \ else let (xss,zs) = chop splitf post \ |
|
24 \ in (pre#xss,zs))"; |
|
25 by (asm_simp_tac (simpset() addsimps [chopr_rule]) 1); |
|
26 by (simp_tac (simpset() addsimps [Let_def] addsplits [split_split]) 1); |
|
27 qed "chop_rule"; |
|
28 |
|
29 Goalw [is_maxsplitter_def,reducing_def] |
|
30 "is_maxsplitter P splitf ==> reducing splitf"; |
|
31 by (Asm_full_simp_tac 1); |
|
32 qed "is_maxsplitter_reducing"; |
|
33 |
|
34 Goal "is_maxsplitter P splitf ==> \ |
|
35 \ !yss zs. chop splitf xs = (yss,zs) --> xs = concat yss @ zs"; |
|
36 by (induct_thm_tac length_induct "xs" 1); |
|
37 by (asm_simp_tac (simpset() delsplits [split_if] |
|
38 addsimps [chop_rule,is_maxsplitter_reducing]) 1); |
|
39 by (asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def] |
|
40 addsplits [split_split]) 1); |
|
41 qed_spec_mp "chop_concat"; |
|
42 |
|
43 Goal "is_maxsplitter P splitf ==> \ |
|
44 \ !yss zs. chop splitf xs = (yss,zs) --> (!ys : set yss. ys ~= [])"; |
|
45 by (induct_thm_tac length_induct "xs" 1); |
|
46 by (asm_simp_tac (simpset() addsimps [chop_rule,is_maxsplitter_reducing]) 1); |
|
47 by (asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def] |
|
48 addsplits [split_split]) 1); |
|
49 by (simp_tac (simpset() addsimps [Let_def,maxsplit_eq] |
|
50 addsplits [split_split]) 1); |
|
51 by (etac thin_rl 1); |
|
52 by (strip_tac 1); |
|
53 by (rtac ballI 1); |
|
54 by (etac exE 1); |
|
55 by (etac allE 1); |
|
56 by Auto_tac; |
|
57 qed "chop_nonempty"; |
|
58 |
|
59 val [prem] = goalw thy [is_maxchopper_def] |
|
60 "is_maxsplitter P splitf ==> is_maxchopper P (chop splitf)"; |
|
61 by (Clarify_tac 1); |
|
62 by (rtac iffI 1); |
|
63 by (rtac conjI 1); |
|
64 by (etac (prem RS chop_concat) 1); |
|
65 by (rtac conjI 1); |
|
66 by (etac (prem RS (chop_nonempty RS spec RS spec RS mp)) 1); |
|
67 by (etac rev_mp 1); |
|
68 by (stac (prem RS is_maxsplitter_reducing RS chop_rule) 1); |
|
69 by (simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem] |
|
70 addsplits [split_split]) 1); |
|
71 by (Clarify_tac 1); |
|
72 by (rtac conjI 1); |
|
73 by (Clarify_tac 1); |
|
74 by (Clarify_tac 1); |
|
75 by (Asm_full_simp_tac 1); |
|
76 by (forward_tac [prem RS chop_concat] 1); |
|
77 by (Clarify_tac 1); |
|
78 by (stac (prem RS is_maxsplitter_reducing RS chop_rule) 1); |
|
79 by (simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem] |
|
80 addsplits [split_split]) 1); |
|
81 by (Clarify_tac 1); |
|
82 by (rename_tac "xs1 ys1 xss1 ys" 1); |
|
83 by (split_asm_tac [thm "list.split_asm"] 1); |
|
84 by (Asm_full_simp_tac 1); |
|
85 by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1); |
|
86 by (blast_tac (claset() addIs [thm "prefix_append" RS iffD2]) 1); |
|
87 by (rtac conjI 1); |
|
88 by (Clarify_tac 1); |
|
89 by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1); |
|
90 by (blast_tac (claset() addIs [thm "prefix_append" RS iffD2]) 1); |
|
91 by (Clarify_tac 1); |
|
92 by (rename_tac "us uss" 1); |
|
93 by (subgoal_tac "xs1=us" 1); |
|
94 by (Asm_full_simp_tac 1); |
|
95 by (Asm_full_simp_tac 1); |
|
96 by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1); |
|
97 by (blast_tac (claset() addIs [thm "prefix_append" RS iffD2, order_antisym]) 1); |
|
98 qed "is_maxchopper_chop"; |
|