author | wenzelm |
Thu, 13 Dec 2001 15:45:03 +0100 | |
changeset 12486 | 0ed8bdd883e0 |
parent 11232 | 558a4feebb04 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/Lex/AutoChopper.ML |
1344 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Richard Mayr & Tobias Nipkow |
1344 | 4 |
Copyright 1995 TUM |
5 |
||
6 |
Main result: auto_chopper satisfies the is_auto_chopper specification. |
|
7 |
*) |
|
8 |
||
1950
97f1c6bf3ace
Miniscoping rules are deleted, as these brittle proofs
paulson
parents:
1894
diff
changeset
|
9 |
Delsimps (ex_simps @ all_simps); |
5609 | 10 |
Delsimps [split_paired_All]; |
1344 | 11 |
|
12 |
Addsimps [Let_def]; |
|
13 |
||
5069 | 14 |
Goalw [acc_prefix_def] "~acc_prefix A [] s"; |
4832 | 15 |
by (Simp_tac 1); |
16 |
qed"acc_prefix_Nil"; |
|
17 |
Addsimps [acc_prefix_Nil]; |
|
18 |
||
5069 | 19 |
Goalw [acc_prefix_def] |
4832 | 20 |
"acc_prefix A (x#xs) s = (fin A (next A x s) | acc_prefix A xs (next A x s))"; |
10338 | 21 |
by (simp_tac (simpset() addsimps [thm "prefix_Cons"]) 1); |
4832 | 22 |
by Safe_tac; |
23 |
by (Asm_full_simp_tac 1); |
|
24 |
by (case_tac "zs=[]" 1); |
|
25 |
by (hyp_subst_tac 1); |
|
26 |
by (Asm_full_simp_tac 1); |
|
27 |
by (Fast_tac 1); |
|
28 |
by (res_inst_tac [("x","[x]")] exI 1); |
|
29 |
by (asm_simp_tac (simpset() addsimps [eq_sym_conv]) 1); |
|
30 |
by (res_inst_tac [("x","x#us")] exI 1); |
|
31 |
by (Asm_simp_tac 1); |
|
32 |
qed"acc_prefix_Cons"; |
|
33 |
Addsimps [acc_prefix_Cons]; |
|
34 |
||
5069 | 35 |
Goal "!st us p y ys. acc A st p (ys@[y]) xs us ~= ([],zs)"; |
4931 | 36 |
by (induct_tac "xs" 1); |
1344 | 37 |
by (Simp_tac 1); |
4686 | 38 |
by (Asm_simp_tac 1); |
5609 | 39 |
qed_spec_mp "accept_not_Nil"; |
1344 | 40 |
Addsimps [accept_not_Nil]; |
41 |
||
5069 | 42 |
Goal |
4955 | 43 |
"!st us. acc A st ([],ys) [] xs us = ([], zs) --> \ |
4832 | 44 |
\ zs = ys & (!ys. ys ~= [] & ys<=xs --> ~fin A (delta A ys st))"; |
4931 | 45 |
by (induct_tac "xs" 1); |
4089 | 46 |
by (simp_tac (simpset() addcongs [conj_cong]) 1); |
4686 | 47 |
by (Simp_tac 1); |
1344 | 48 |
by (strip_tac 1); |
1465 | 49 |
by (rtac conjI 1); |
1894 | 50 |
by (Fast_tac 1); |
10338 | 51 |
by (simp_tac (simpset() addsimps [thm "prefix_Cons"] addcongs [conj_cong]) 1); |
1344 | 52 |
by (strip_tac 1); |
2056
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
53 |
by (REPEAT(eresolve_tac [conjE,exE] 1)); |
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
54 |
by (hyp_subst_tac 1); |
1344 | 55 |
by (Simp_tac 1); |
56 |
by (case_tac "zsa = []" 1); |
|
57 |
by (Asm_simp_tac 1); |
|
1894 | 58 |
by (Fast_tac 1); |
4931 | 59 |
qed_spec_mp "no_acc"; |
1344 | 60 |
|
61 |
||
3842 | 62 |
val [prem] = goal HOL.thy "? x. P(f(x)) ==> ? y. P(y)"; |
1344 | 63 |
by (cut_facts_tac [prem] 1); |
1894 | 64 |
by (Fast_tac 1); |
1344 | 65 |
val ex_special = result(); |
66 |
||
67 |
||
5069 | 68 |
Goal |
1344 | 69 |
"! r erk l rst st ys yss zs::'a list. \ |
4955 | 70 |
\ acc A st (l,rst) erk xs r = (ys#yss, zs) --> \ |
4832 | 71 |
\ ys@concat(yss)@zs = (if acc_prefix A xs st then r@xs else erk@concat(l)@rst)"; |
4931 | 72 |
by (induct_tac "xs" 1); |
4686 | 73 |
by (simp_tac (simpset() addcongs [conj_cong]) 1); |
74 |
by (Asm_simp_tac 1); |
|
4955 | 75 |
by (res_inst_tac [("p","acc A (start A) ([],list) [] list []")] PairE 1); |
2056
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
76 |
by (rename_tac "vss lrst" 1); |
4686 | 77 |
by (Asm_simp_tac 1); |
9270 | 78 |
by (case_tac "vss" 1); |
2056
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
79 |
by (hyp_subst_tac 1); |
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
80 |
by (Simp_tac 1); |
4089 | 81 |
by (fast_tac (claset() addSDs [no_acc]) 1); |
2056
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
82 |
by (hyp_subst_tac 1); |
4686 | 83 |
by (Asm_simp_tac 1); |
5609 | 84 |
qed_spec_mp "step2_a"; |
1344 | 85 |
|
86 |
||
5069 | 87 |
Goal |
1344 | 88 |
"! st erk r l rest ys yss zs.\ |
4955 | 89 |
\ acc A st (l,rest) erk xs r = (ys#yss, zs) --> \ |
4832 | 90 |
\ (if acc_prefix A xs st \ |
1344 | 91 |
\ then ys ~= [] \ |
92 |
\ else ys ~= [] | (erk=[] & (l,rest) = (ys#yss,zs)))"; |
|
4686 | 93 |
by (Simp_tac 1); |
4931 | 94 |
by (induct_tac "xs" 1); |
4686 | 95 |
by (simp_tac (simpset() addcongs [conj_cong]) 1); |
96 |
by (asm_simp_tac (simpset() addcongs [conj_cong]) 1); |
|
4955 | 97 |
by (res_inst_tac [("p","acc A (start A) ([],list) [] list []")] PairE 1); |
2056
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
98 |
by (rename_tac "vss lrst" 1); |
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
99 |
by (Asm_simp_tac 1); |
1344 | 100 |
by (strip_tac 1); |
4832 | 101 |
by (case_tac "acc_prefix A list (next A a st)" 1); |
2056
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
102 |
by (Asm_simp_tac 1); |
1344 | 103 |
by (subgoal_tac "r @ [a] ~= []" 1); |
1894 | 104 |
by (Fast_tac 1); |
1344 | 105 |
by (Simp_tac 1); |
5609 | 106 |
qed_spec_mp "step2_b"; |
1344 | 107 |
|
108 |
||
5069 | 109 |
Goal |
1344 | 110 |
"! st erk r l rest ys yss zs. \ |
4955 | 111 |
\ acc A st (l,rest) erk xs r = (ys#yss, zs) --> \ |
4832 | 112 |
\ (if acc_prefix A xs st \ |
113 |
\ then ? g. ys=r@g & fin A (delta A g st) \ |
|
1344 | 114 |
\ else (erk~=[] & erk=ys) | (erk=[] & (l,rest) = (ys#yss,zs)))"; |
4686 | 115 |
by (Simp_tac 1); |
4931 | 116 |
by (induct_tac "xs" 1); |
4686 | 117 |
by (simp_tac (simpset() addcongs [conj_cong]) 1); |
118 |
by (asm_simp_tac (simpset() addcongs [conj_cong]) 1); |
|
1344 | 119 |
by (strip_tac 1); |
1465 | 120 |
by (rtac conjI 1); |
4955 | 121 |
by (res_inst_tac [("p","acc A (start A) ([],list) [] list []")] PairE 1); |
2056
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
122 |
by (rename_tac "vss lrst" 1); |
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
123 |
by (Asm_simp_tac 1); |
4832 | 124 |
by (case_tac "acc_prefix A list (next A a st)" 1); |
1344 | 125 |
by (strip_tac 1); |
3842 | 126 |
by (res_inst_tac [("f","%k. a#k")] ex_special 1); |
1344 | 127 |
by (Simp_tac 1); |
3842 | 128 |
by (res_inst_tac [("t","%k. ys=r@a#k"),("s","%k. ys=(r@[a])@k")] subst 1); |
1344 | 129 |
by (Simp_tac 1); |
1894 | 130 |
by (Fast_tac 1); |
1344 | 131 |
by (strip_tac 1); |
132 |
by (res_inst_tac [("x","[a]")] exI 1); |
|
133 |
by (Asm_simp_tac 1); |
|
134 |
by (subgoal_tac "r @ [a] ~= []" 1); |
|
2056
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
135 |
by (rtac sym 1); |
1894 | 136 |
by (Fast_tac 1); |
1344 | 137 |
by (Simp_tac 1); |
138 |
by (strip_tac 1); |
|
3842 | 139 |
by (res_inst_tac [("f","%k. a#k")] ex_special 1); |
1344 | 140 |
by (Simp_tac 1); |
3842 | 141 |
by (res_inst_tac [("t","%k. ys=r@a#k"),("s","%k. ys=(r@[a])@k")] subst 1); |
1344 | 142 |
by (Simp_tac 1); |
1894 | 143 |
by (Fast_tac 1); |
5609 | 144 |
qed_spec_mp "step2_c"; |
1344 | 145 |
|
146 |
||
5069 | 147 |
Goal |
1344 | 148 |
"! st erk r l rest ys yss zs. \ |
4955 | 149 |
\ acc A st (l,rest) erk xs r = (ys#yss, zs) --> \ |
4832 | 150 |
\ (if acc_prefix A xs st \ |
4955 | 151 |
\ then acc A (start A) ([],concat(yss)@zs) [] (concat(yss)@zs) [] = (yss,zs) \ |
1344 | 152 |
\ else (erk~=[] & (l,rest)=(yss,zs)) | (erk=[] & (l, rest)=(ys#yss,zs)))"; |
4686 | 153 |
by (Simp_tac 1); |
4931 | 154 |
by (induct_tac "xs" 1); |
4686 | 155 |
by (simp_tac (simpset() addcongs [conj_cong]) 1); |
156 |
by (asm_simp_tac (simpset() addcongs [conj_cong]) 1); |
|
4955 | 157 |
by (res_inst_tac [("p","acc A (start A) ([],list) [] list []")] PairE 1); |
2056
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
158 |
by (rename_tac "vss lrst" 1); |
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
159 |
by (Asm_simp_tac 1); |
1344 | 160 |
by (strip_tac 1); |
4832 | 161 |
by (case_tac "acc_prefix A list (next A a st)" 1); |
1344 | 162 |
by (Asm_simp_tac 1); |
4955 | 163 |
by (subgoal_tac "acc A (start A) ([],list) [] list [] = (yss,zs)" 1); |
1344 | 164 |
by (Asm_simp_tac 2); |
165 |
by (subgoal_tac "r@[a] ~= []" 2); |
|
1894 | 166 |
by (Fast_tac 2); |
1344 | 167 |
by (Simp_tac 2); |
2609 | 168 |
by (subgoal_tac "concat(yss) @ zs = list" 1); |
2056
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
169 |
by (hyp_subst_tac 1); |
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
170 |
by (atac 1); |
1344 | 171 |
by (case_tac "yss = []" 1); |
172 |
by (Asm_simp_tac 1); |
|
173 |
by (hyp_subst_tac 1); |
|
4089 | 174 |
by (fast_tac (claset() addSDs [no_acc]) 1); |
1465 | 175 |
by (etac ((neq_Nil_conv RS iffD1) RS exE) 1); |
176 |
by (etac exE 1); |
|
1344 | 177 |
by (hyp_subst_tac 1); |
178 |
by (Simp_tac 1); |
|
1465 | 179 |
by (rtac trans 1); |
2056
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
180 |
by (etac step2_a 1); |
4686 | 181 |
by (Simp_tac 1); |
5609 | 182 |
qed_spec_mp "step2_d"; |
1344 | 183 |
|
5069 | 184 |
Goal |
1344 | 185 |
"! st erk r p ys yss zs. \ |
4955 | 186 |
\ acc A st p erk xs r = (ys#yss, zs) --> \ |
4832 | 187 |
\ (if acc_prefix A xs st \ |
188 |
\ then ? g. ys=r@g & (!as. as<=xs & g<=as & g~=as --> ~fin A (delta A as st))\ |
|
1344 | 189 |
\ else (erk~=[] & ys=erk) | (erk=[] & (ys#yss,zs)=p))"; |
4686 | 190 |
by (Simp_tac 1); |
4931 | 191 |
by (induct_tac "xs" 1); |
4686 | 192 |
by (simp_tac (simpset() addcongs [conj_cong]) 1); |
193 |
by (asm_simp_tac (simpset() addcongs [conj_cong]) 1); |
|
1344 | 194 |
by (strip_tac 1); |
4832 | 195 |
by (case_tac "acc_prefix A list (next A a st)" 1); |
2056
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
196 |
by (rtac conjI 1); |
1344 | 197 |
by (strip_tac 1); |
3842 | 198 |
by (res_inst_tac [("f","%k. a#k")] ex_special 1); |
199 |
by (res_inst_tac [("t","%k. ys=r@a#k"),("s","%k. ys=(r@[a])@k")] subst 1); |
|
1344 | 200 |
by (Simp_tac 1); |
4832 | 201 |
by (res_inst_tac [("P","%k. ys = (r@[a])@k & (!as. as<=list & k<=as & k ~= as --> ~ fin A (delta A as (next A a st)))")] exE 1); |
1344 | 202 |
by (asm_simp_tac HOL_ss 1); |
203 |
by (res_inst_tac [("x","x")] exI 1); |
|
204 |
by (Asm_simp_tac 1); |
|
12486 | 205 |
by (rtac allI 1); |
206 |
by (case_tac "as" 1); |
|
9270 | 207 |
by (Asm_simp_tac 1); |
4089 | 208 |
by (asm_simp_tac (simpset() addcongs[conj_cong]) 1); |
1344 | 209 |
by (strip_tac 1); |
3842 | 210 |
by (res_inst_tac [("f","%k. a#k")] ex_special 1); |
211 |
by (res_inst_tac [("t","%k. ys=r@a#k"),("s","%k. ys=(r@[a])@k")] subst 1); |
|
1344 | 212 |
by (Simp_tac 1); |
4832 | 213 |
by (res_inst_tac [("P","%k. ys=(r@[a])@k & (!as. as<=list & k<=as & k~=as --> ~ fin A (delta A as (next A a st)))")] exE 1); |
1344 | 214 |
by (asm_simp_tac HOL_ss 1); |
215 |
by (res_inst_tac [("x","x")] exI 1); |
|
216 |
by (Asm_simp_tac 1); |
|
12486 | 217 |
by (rtac allI 1); |
218 |
by (case_tac "as" 1); |
|
9270 | 219 |
by (Asm_simp_tac 1); |
4089 | 220 |
by (asm_simp_tac (simpset() addcongs[conj_cong]) 1); |
1344 | 221 |
by (Asm_simp_tac 1); |
222 |
by (strip_tac 1); |
|
223 |
by (res_inst_tac [("x","[a]")] exI 1); |
|
1465 | 224 |
by (rtac conjI 1); |
1344 | 225 |
by (subgoal_tac "r @ [a] ~= []" 1); |
1894 | 226 |
by (Fast_tac 1); |
1344 | 227 |
by (Simp_tac 1); |
12486 | 228 |
by (rtac allI 1); |
229 |
by (case_tac "as" 1); |
|
9270 | 230 |
by (Asm_simp_tac 1); |
4089 | 231 |
by (asm_full_simp_tac (simpset() addsimps [acc_prefix_def] addcongs[conj_cong]) 1); |
1465 | 232 |
by (etac thin_rl 1); (* speed up *) |
1894 | 233 |
by (Fast_tac 1); |
5609 | 234 |
qed_spec_mp "step2_e"; |
235 |
||
1344 | 236 |
Addsimps[split_paired_All]; |
237 |
||
5069 | 238 |
Goalw [accepts_def, is_auto_chopper_def, auto_chopper_def, |
4832 | 239 |
Chopper.is_longest_prefix_chopper_def] |
1344 | 240 |
"is_auto_chopper(auto_chopper)"; |
241 |
by (REPEAT(ares_tac [no_acc,allI,impI,conjI] 1)); |
|
2056
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
242 |
by (rtac mp 1); |
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
243 |
by (etac step2_b 2); |
4686 | 244 |
by (Simp_tac 1); |
1465 | 245 |
by (rtac conjI 1); |
2056
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
246 |
by (rtac mp 1); |
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
247 |
by (etac step2_c 2); |
4686 | 248 |
by (Simp_tac 1); |
1465 | 249 |
by (rtac conjI 1); |
4686 | 250 |
by (asm_simp_tac (simpset() addsimps [step2_a]) 1); |
1465 | 251 |
by (rtac conjI 1); |
2056
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
252 |
by (rtac mp 1); |
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
253 |
by (etac step2_d 2); |
4686 | 254 |
by (Simp_tac 1); |
1465 | 255 |
by (rtac mp 1); |
2056
93c093620c28
Removed commands made redundant by new one-point rules
paulson
parents:
1950
diff
changeset
|
256 |
by (etac step2_e 2); |
4686 | 257 |
by (Simp_tac 1); |
1344 | 258 |
qed"auto_chopper_is_auto_chopper"; |