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