5 *) |
5 *) |
6 |
6 |
7 (* Termination of chop *) |
7 (* Termination of chop *) |
8 |
8 |
9 Goalw [reducing_def] "reducing(%qs. maxsplit P ([],qs) [] qs)"; |
9 Goalw [reducing_def] "reducing(%qs. maxsplit P ([],qs) [] qs)"; |
10 by(asm_full_simp_tac (simpset() addsimps [maxsplit_eq]) 1); |
10 by (asm_full_simp_tac (simpset() addsimps [maxsplit_eq]) 1); |
11 qed "reducing_maxsplit"; |
11 qed "reducing_maxsplit"; |
12 |
12 |
13 val [tc] = chopr.tcs; |
13 val [tc] = chopr.tcs; |
14 goalw_cterm [reducing_def] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc)); |
14 goalw_cterm [reducing_def] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc)); |
15 by(blast_tac (claset() addDs [sym]) 1); |
15 by (blast_tac (claset() addDs [sym]) 1); |
16 val lemma = result(); |
16 val lemma = result(); |
17 |
17 |
18 val chopr_rule = let val [chopr_rule] = chopr.rules in lemma RS chopr_rule end; |
18 val chopr_rule = let val [chopr_rule] = chopr.rules in lemma RS chopr_rule end; |
19 |
19 |
20 Goalw [chop_def] "reducing splitf ==> \ |
20 Goalw [chop_def] "reducing splitf ==> \ |
21 \ chop splitf xs = (let (pre,post) = splitf xs \ |
21 \ chop splitf xs = (let (pre,post) = splitf xs \ |
22 \ in if pre=[] then ([],xs) \ |
22 \ in if pre=[] then ([],xs) \ |
23 \ else let (xss,zs) = chop splitf post \ |
23 \ else let (xss,zs) = chop splitf post \ |
24 \ in (pre#xss,zs))"; |
24 \ in (pre#xss,zs))"; |
25 by(asm_simp_tac (simpset() addsimps [chopr_rule] addcongs [if_weak_cong]) 1); |
25 by (asm_simp_tac (simpset() addsimps [chopr_rule] addcongs [if_weak_cong]) 1); |
26 by(simp_tac (simpset() addsimps [Let_def] addsplits [split_split]) 1); |
26 by (simp_tac (simpset() addsimps [Let_def] addsplits [split_split]) 1); |
27 qed "chop_rule"; |
27 qed "chop_rule"; |
28 |
28 |
29 Goalw [is_maxsplitter_def,reducing_def] |
29 Goalw [is_maxsplitter_def,reducing_def] |
30 "is_maxsplitter P splitf ==> reducing splitf"; |
30 "is_maxsplitter P splitf ==> reducing splitf"; |
31 by(Asm_full_simp_tac 1); |
31 by (Asm_full_simp_tac 1); |
32 qed "is_maxsplitter_reducing"; |
32 qed "is_maxsplitter_reducing"; |
33 |
33 |
34 Goal "is_maxsplitter P splitf ==> \ |
34 Goal "is_maxsplitter P splitf ==> \ |
35 \ !yss zs. chop splitf xs = (yss,zs) --> xs = concat yss @ zs"; |
35 \ !yss zs. chop splitf xs = (yss,zs) --> xs = concat yss @ zs"; |
36 by(res_inst_tac [("xs","xs")] length_induct 1); |
36 by (res_inst_tac [("xs","xs")] length_induct 1); |
37 by(asm_simp_tac (simpset() delsplits [split_if] |
37 by (asm_simp_tac (simpset() delsplits [split_if] |
38 addsimps [chop_rule,is_maxsplitter_reducing] |
38 addsimps [chop_rule,is_maxsplitter_reducing] |
39 addcongs [if_weak_cong]) 1); |
39 addcongs [if_weak_cong]) 1); |
40 by(asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def] |
40 by (asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def] |
41 addsplits [split_split]) 1); |
41 addsplits [split_split]) 1); |
42 qed_spec_mp "chop_concat"; |
42 qed_spec_mp "chop_concat"; |
43 |
43 |
44 Goal "is_maxsplitter P splitf ==> \ |
44 Goal "is_maxsplitter P splitf ==> \ |
45 \ !yss zs. chop splitf xs = (yss,zs) --> (!ys : set yss. ys ~= [])"; |
45 \ !yss zs. chop splitf xs = (yss,zs) --> (!ys : set yss. ys ~= [])"; |
46 by(res_inst_tac [("xs","xs")] length_induct 1); |
46 by (res_inst_tac [("xs","xs")] length_induct 1); |
47 by(asm_simp_tac (simpset() addsimps [chop_rule,is_maxsplitter_reducing] |
47 by (asm_simp_tac (simpset() addsimps [chop_rule,is_maxsplitter_reducing] |
48 addcongs [if_weak_cong]) 1); |
48 addcongs [if_weak_cong]) 1); |
49 by(asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def] |
49 by (asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def] |
50 addsplits [split_split]) 1); |
50 addsplits [split_split]) 1); |
51 by(simp_tac (simpset() addsimps [Let_def,maxsplit_eq] |
51 by (simp_tac (simpset() addsimps [Let_def,maxsplit_eq] |
52 addsplits [split_split]) 1); |
52 addsplits [split_split]) 1); |
53 be thin_rl 1; |
53 by (etac thin_rl 1); |
54 by(strip_tac 1); |
54 by (strip_tac 1); |
55 br ballI 1; |
55 by (rtac ballI 1); |
56 be exE 1; |
56 by (etac exE 1); |
57 be allE 1; |
57 by (etac allE 1); |
58 auto(); |
58 by Auto_tac; |
59 qed_spec_mp "chop_nonempty"; |
59 qed_spec_mp "chop_nonempty"; |
60 |
60 |
61 val [prem] = goalw thy [is_maxchopper_def] |
61 val [prem] = goalw thy [is_maxchopper_def] |
62 "is_maxsplitter P splitf ==> is_maxchopper P (chop splitf)"; |
62 "is_maxsplitter P splitf ==> is_maxchopper P (chop splitf)"; |
63 by(Clarify_tac 1); |
63 by (Clarify_tac 1); |
64 br iffI 1; |
64 by (rtac iffI 1); |
65 br conjI 1; |
65 by (rtac conjI 1); |
66 be (prem RS chop_concat) 1; |
66 by (etac (prem RS chop_concat) 1); |
67 br conjI 1; |
67 by (rtac conjI 1); |
68 be (prem RS chop_nonempty) 1; |
68 by (etac (prem RS chop_nonempty) 1); |
69 be rev_mp 1; |
69 by (etac rev_mp 1); |
70 by(stac (prem RS is_maxsplitter_reducing RS chop_rule) 1); |
70 by (stac (prem RS is_maxsplitter_reducing RS chop_rule) 1); |
71 by(simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem] |
71 by (simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem] |
72 addsplits [split_split]) 1); |
72 addsplits [split_split]) 1); |
73 by(Clarify_tac 1); |
73 by (Clarify_tac 1); |
74 br conjI 1; |
74 by (rtac conjI 1); |
75 by(Clarify_tac 1); |
75 by (Clarify_tac 1); |
76 by(Asm_full_simp_tac 1); |
76 by (Asm_full_simp_tac 1); |
77 by(Clarify_tac 1); |
77 by (Clarify_tac 1); |
78 by(Asm_full_simp_tac 1); |
78 by (Asm_full_simp_tac 1); |
79 by(forward_tac [prem RS chop_concat] 1); |
79 by (forward_tac [prem RS chop_concat] 1); |
80 by(Clarify_tac 1); |
80 by (Clarify_tac 1); |
81 ba 1; |
81 by (assume_tac 1); |
82 by(stac (prem RS is_maxsplitter_reducing RS chop_rule) 1); |
82 by (stac (prem RS is_maxsplitter_reducing RS chop_rule) 1); |
83 by(simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem] |
83 by (simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem] |
84 addsplits [split_split]) 1); |
84 addsplits [split_split]) 1); |
85 by(Clarify_tac 1); |
85 by (Clarify_tac 1); |
86 br conjI 1; |
86 by (rtac conjI 1); |
87 by(Clarify_tac 1); |
87 by (Clarify_tac 1); |
88 by(exhaust_tac "yss" 1); |
88 by (exhaust_tac "yss" 1); |
89 by(Asm_simp_tac 1); |
89 by (Asm_simp_tac 1); |
90 by(Asm_full_simp_tac 1); |
90 by (Asm_full_simp_tac 1); |
91 by(full_simp_tac (simpset() addsimps [is_maxpref_def]) 1); |
91 by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1); |
92 by(blast_tac (claset() addIs [prefix_append RS iffD2]) 1); |
92 by (blast_tac (claset() addIs [prefix_append RS iffD2]) 1); |
93 by(exhaust_tac "yss" 1); |
93 by (exhaust_tac "yss" 1); |
94 by(Asm_full_simp_tac 1); |
94 by (Asm_full_simp_tac 1); |
95 by(full_simp_tac (simpset() addsimps [is_maxpref_def]) 1); |
95 by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1); |
96 by(blast_tac (claset() addIs [prefix_append RS iffD2]) 1); |
96 by (blast_tac (claset() addIs [prefix_append RS iffD2]) 1); |
97 by(Clarify_tac 1); |
97 by (Clarify_tac 1); |
98 by(Asm_full_simp_tac 1); |
98 by (Asm_full_simp_tac 1); |
99 by(subgoal_tac "x=a" 1); |
99 by (subgoal_tac "x=a" 1); |
100 by(Clarify_tac 1); |
100 by (Clarify_tac 1); |
101 by(Asm_full_simp_tac 1); |
101 by (Asm_full_simp_tac 1); |
102 by(rotate_tac ~2 1); |
102 by (rotate_tac ~2 1); |
103 by(Asm_full_simp_tac 1); |
103 by (Asm_full_simp_tac 1); |
104 by(full_simp_tac (simpset() addsimps [is_maxpref_def]) 1); |
104 by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1); |
105 by(blast_tac (claset() addIs [prefix_append RS iffD2,prefix_antisym]) 1); |
105 by (blast_tac (claset() addIs [prefix_append RS iffD2,prefix_antisym]) 1); |
106 qed "is_maxchopper_chop"; |
106 qed "is_maxchopper_chop"; |