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