4714
|
1 |
(* Title: HOL/Lex/MaxChop.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 1998 TUM
|
|
5 |
*)
|
|
6 |
|
|
7 |
(* Termination of chop *)
|
|
8 |
|
5069
|
9 |
Goalw [reducing_def] "reducing(%qs. maxsplit P ([],qs) [] qs)";
|
4714
|
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.rules in lemma RS chopr_rule end;
|
|
19 |
|
5069
|
20 |
Goalw [chop_def] "!!splitf. reducing splitf ==> \
|
4714
|
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] addcongs [if_weak_cong]) 1);
|
4832
|
26 |
by(simp_tac (simpset() addsimps [Let_def] addsplits [split_split]) 1);
|
4714
|
27 |
qed "chop_rule";
|
|
28 |
|
5069
|
29 |
Goalw [is_maxsplitter_def,reducing_def]
|
4714
|
30 |
"!!splitf. is_maxsplitter P splitf ==> reducing splitf";
|
|
31 |
by(Asm_full_simp_tac 1);
|
|
32 |
qed "is_maxsplitter_reducing";
|
|
33 |
|
5069
|
34 |
Goal "!!P. is_maxsplitter P splitf ==> \
|
4714
|
35 |
\ !yss zs. chop splitf xs = (yss,zs) --> xs = concat yss @ zs";
|
|
36 |
by(res_inst_tac [("xs","xs")] length_induct 1);
|
4832
|
37 |
by(asm_simp_tac (simpset() delsplits [split_if]
|
4714
|
38 |
addsimps [chop_rule,is_maxsplitter_reducing]
|
|
39 |
addcongs [if_weak_cong]) 1);
|
|
40 |
by(asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
|
4832
|
41 |
addsplits [split_split]) 1);
|
4714
|
42 |
qed_spec_mp "chop_concat";
|
|
43 |
|
5069
|
44 |
Goal "!!P. is_maxsplitter P splitf ==> \
|
4714
|
45 |
\ !yss zs. chop splitf xs = (yss,zs) --> (!ys : set yss. ys ~= [])";
|
|
46 |
by(res_inst_tac [("xs","xs")] length_induct 1);
|
|
47 |
by(asm_simp_tac (simpset() addsimps [chop_rule,is_maxsplitter_reducing]
|
|
48 |
addcongs [if_weak_cong]) 1);
|
|
49 |
by(asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
|
4832
|
50 |
addsplits [split_split]) 1);
|
4714
|
51 |
by(simp_tac (simpset() addsimps [Let_def,maxsplit_eq]
|
4832
|
52 |
addsplits [split_split]) 1);
|
4714
|
53 |
be thin_rl 1;
|
|
54 |
by(strip_tac 1);
|
|
55 |
br ballI 1;
|
|
56 |
be exE 1;
|
|
57 |
be allE 1;
|
|
58 |
auto();
|
|
59 |
qed_spec_mp "chop_nonempty";
|
|
60 |
|
|
61 |
val [prem] = goalw thy [is_maxchopper_def]
|
|
62 |
"is_maxsplitter P splitf ==> is_maxchopper P (chop splitf)";
|
|
63 |
by(Clarify_tac 1);
|
|
64 |
br iffI 1;
|
|
65 |
br conjI 1;
|
|
66 |
be (prem RS chop_concat) 1;
|
|
67 |
br conjI 1;
|
|
68 |
be (prem RS chop_nonempty) 1;
|
|
69 |
be rev_mp 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]
|
4832
|
72 |
addsplits [split_split]) 1);
|
4714
|
73 |
by(Clarify_tac 1);
|
|
74 |
br conjI 1;
|
|
75 |
by(Clarify_tac 1);
|
|
76 |
by(Asm_full_simp_tac 1);
|
|
77 |
by(Clarify_tac 1);
|
|
78 |
by(Asm_full_simp_tac 1);
|
|
79 |
by(forward_tac [prem RS chop_concat] 1);
|
|
80 |
by(Clarify_tac 1);
|
|
81 |
ba 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]
|
4832
|
84 |
addsplits [split_split]) 1);
|
4714
|
85 |
by(Clarify_tac 1);
|
|
86 |
br conjI 1;
|
|
87 |
by(Clarify_tac 1);
|
|
88 |
by(exhaust_tac "yss" 1);
|
|
89 |
by(Asm_simp_tac 1);
|
|
90 |
by(Asm_full_simp_tac 1);
|
|
91 |
by(full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
|
|
92 |
by(blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
|
|
93 |
by(exhaust_tac "yss" 1);
|
|
94 |
by(Asm_full_simp_tac 1);
|
|
95 |
by(full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
|
|
96 |
by(blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
|
|
97 |
by(Clarify_tac 1);
|
|
98 |
by(Asm_full_simp_tac 1);
|
|
99 |
by(subgoal_tac "x=a" 1);
|
|
100 |
by(Clarify_tac 1);
|
|
101 |
by(Asm_full_simp_tac 1);
|
|
102 |
by(rotate_tac ~2 1);
|
|
103 |
by(Asm_full_simp_tac 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);
|
|
106 |
qed "is_maxchopper_chop";
|