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 [expand_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 thy [is_maxsplitter_def,reducing_def] |
29 goalw thy [is_maxsplitter_def,reducing_def] |
30 "!!splitf. is_maxsplitter P splitf ==> reducing splitf"; |
30 "!!splitf. 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 thy "!!P. is_maxsplitter P splitf ==> \ |
34 goal thy "!!P. 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 [expand_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 [expand_split]) 1); |
41 addsplits [split_split]) 1); |
42 qed_spec_mp "chop_concat"; |
42 qed_spec_mp "chop_concat"; |
43 |
43 |
44 goal thy "!!P. is_maxsplitter P splitf ==> \ |
44 goal thy "!!P. 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 [expand_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 [expand_split]) 1); |
52 addsplits [split_split]) 1); |
53 be thin_rl 1; |
53 be thin_rl 1; |
54 by(strip_tac 1); |
54 by(strip_tac 1); |
55 br ballI 1; |
55 br ballI 1; |
56 be exE 1; |
56 be exE 1; |
57 be allE 1; |
57 be allE 1; |