32 by (res_inst_tac [("x","x#us")] exI 1); |
32 by (res_inst_tac [("x","x#us")] exI 1); |
33 by (Asm_simp_tac 1); |
33 by (Asm_simp_tac 1); |
34 qed"acc_prefix_Cons"; |
34 qed"acc_prefix_Cons"; |
35 Addsimps [acc_prefix_Cons]; |
35 Addsimps [acc_prefix_Cons]; |
36 |
36 |
37 goal thy "!st us p y ys. acc A st p xs (ys@[y]) us ~= ([],zs)"; |
37 goal thy "!st us p y ys. acc A st p (ys@[y]) xs us ~= ([],zs)"; |
38 by (induct_tac "xs" 1); |
38 by (induct_tac "xs" 1); |
39 by (Simp_tac 1); |
39 by (Simp_tac 1); |
40 by (Asm_simp_tac 1); |
40 by (Asm_simp_tac 1); |
41 val accept_not_Nil = result() repeat_RS spec; |
41 val accept_not_Nil = result() repeat_RS spec; |
42 Addsimps [accept_not_Nil]; |
42 Addsimps [accept_not_Nil]; |
43 |
43 |
44 goal thy |
44 goal thy |
45 "!st us. acc A st ([],ys) xs [] us = ([], zs) --> \ |
45 "!st us. acc A st ([],ys) [] xs us = ([], zs) --> \ |
46 \ zs = ys & (!ys. ys ~= [] & ys<=xs --> ~fin A (delta A ys st))"; |
46 \ zs = ys & (!ys. ys ~= [] & ys<=xs --> ~fin A (delta A ys st))"; |
47 by (induct_tac "xs" 1); |
47 by (induct_tac "xs" 1); |
48 by (simp_tac (simpset() addcongs [conj_cong]) 1); |
48 by (simp_tac (simpset() addcongs [conj_cong]) 1); |
49 by (Simp_tac 1); |
49 by (Simp_tac 1); |
50 by (strip_tac 1); |
50 by (strip_tac 1); |
67 val ex_special = result(); |
67 val ex_special = result(); |
68 |
68 |
69 |
69 |
70 goal thy |
70 goal thy |
71 "! r erk l rst st ys yss zs::'a list. \ |
71 "! r erk l rst st ys yss zs::'a list. \ |
72 \ acc A st (l,rst) xs erk r = (ys#yss, zs) --> \ |
72 \ acc A st (l,rst) erk xs r = (ys#yss, zs) --> \ |
73 \ ys@concat(yss)@zs = (if acc_prefix A xs st then r@xs else erk@concat(l)@rst)"; |
73 \ ys@concat(yss)@zs = (if acc_prefix A xs st then r@xs else erk@concat(l)@rst)"; |
74 by (induct_tac "xs" 1); |
74 by (induct_tac "xs" 1); |
75 by (simp_tac (simpset() addcongs [conj_cong]) 1); |
75 by (simp_tac (simpset() addcongs [conj_cong]) 1); |
76 by (Asm_simp_tac 1); |
76 by (Asm_simp_tac 1); |
77 by (res_inst_tac [("p","acc A (start A) ([],list) list [] []")] PairE 1); |
77 by (res_inst_tac [("p","acc A (start A) ([],list) [] list []")] PairE 1); |
78 by (rename_tac "vss lrst" 1); |
78 by (rename_tac "vss lrst" 1); |
79 by (Asm_simp_tac 1); |
79 by (Asm_simp_tac 1); |
80 by (res_inst_tac[("xs","vss")] list_eq_cases 1); |
80 by (res_inst_tac[("xs","vss")] list_eq_cases 1); |
81 by (hyp_subst_tac 1); |
81 by (hyp_subst_tac 1); |
82 by (Simp_tac 1); |
82 by (Simp_tac 1); |
86 val step2_a = (result() repeat_RS spec) RS mp; |
86 val step2_a = (result() repeat_RS spec) RS mp; |
87 |
87 |
88 |
88 |
89 goal thy |
89 goal thy |
90 "! st erk r l rest ys yss zs.\ |
90 "! st erk r l rest ys yss zs.\ |
91 \ acc A st (l,rest) xs erk r = (ys#yss, zs) --> \ |
91 \ acc A st (l,rest) erk xs r = (ys#yss, zs) --> \ |
92 \ (if acc_prefix A xs st \ |
92 \ (if acc_prefix A xs st \ |
93 \ then ys ~= [] \ |
93 \ then ys ~= [] \ |
94 \ else ys ~= [] | (erk=[] & (l,rest) = (ys#yss,zs)))"; |
94 \ else ys ~= [] | (erk=[] & (l,rest) = (ys#yss,zs)))"; |
95 by (Simp_tac 1); |
95 by (Simp_tac 1); |
96 by (induct_tac "xs" 1); |
96 by (induct_tac "xs" 1); |
97 by (simp_tac (simpset() addcongs [conj_cong]) 1); |
97 by (simp_tac (simpset() addcongs [conj_cong]) 1); |
98 by (Fast_tac 1); |
98 by (Fast_tac 1); |
99 by (asm_simp_tac (simpset() addcongs [conj_cong]) 1); |
99 by (asm_simp_tac (simpset() addcongs [conj_cong]) 1); |
100 by (res_inst_tac [("p","acc A (start A) ([],list) list [] []")] PairE 1); |
100 by (res_inst_tac [("p","acc A (start A) ([],list) [] list []")] PairE 1); |
101 by (rename_tac "vss lrst" 1); |
101 by (rename_tac "vss lrst" 1); |
102 by (Asm_simp_tac 1); |
102 by (Asm_simp_tac 1); |
103 by (strip_tac 1); |
103 by (strip_tac 1); |
104 by (case_tac "acc_prefix A list (next A a st)" 1); |
104 by (case_tac "acc_prefix A list (next A a st)" 1); |
105 by (Asm_simp_tac 1); |
105 by (Asm_simp_tac 1); |
109 val step2_b = (result() repeat_RS spec) RS mp; |
109 val step2_b = (result() repeat_RS spec) RS mp; |
110 |
110 |
111 |
111 |
112 goal thy |
112 goal thy |
113 "! st erk r l rest ys yss zs. \ |
113 "! st erk r l rest ys yss zs. \ |
114 \ acc A st (l,rest) xs erk r = (ys#yss, zs) --> \ |
114 \ acc A st (l,rest) erk xs r = (ys#yss, zs) --> \ |
115 \ (if acc_prefix A xs st \ |
115 \ (if acc_prefix A xs st \ |
116 \ then ? g. ys=r@g & fin A (delta A g st) \ |
116 \ then ? g. ys=r@g & fin A (delta A g st) \ |
117 \ else (erk~=[] & erk=ys) | (erk=[] & (l,rest) = (ys#yss,zs)))"; |
117 \ else (erk~=[] & erk=ys) | (erk=[] & (l,rest) = (ys#yss,zs)))"; |
118 by (Simp_tac 1); |
118 by (Simp_tac 1); |
119 by (induct_tac "xs" 1); |
119 by (induct_tac "xs" 1); |
120 by (simp_tac (simpset() addcongs [conj_cong]) 1); |
120 by (simp_tac (simpset() addcongs [conj_cong]) 1); |
121 by (Fast_tac 1); |
121 by (Fast_tac 1); |
122 by (asm_simp_tac (simpset() addcongs [conj_cong]) 1); |
122 by (asm_simp_tac (simpset() addcongs [conj_cong]) 1); |
123 by (strip_tac 1); |
123 by (strip_tac 1); |
124 by (rtac conjI 1); |
124 by (rtac conjI 1); |
125 by (res_inst_tac [("p","acc A (start A) ([],list) list [] []")] PairE 1); |
125 by (res_inst_tac [("p","acc A (start A) ([],list) [] list []")] PairE 1); |
126 by (rename_tac "vss lrst" 1); |
126 by (rename_tac "vss lrst" 1); |
127 by (Asm_simp_tac 1); |
127 by (Asm_simp_tac 1); |
128 by (case_tac "acc_prefix A list (next A a st)" 1); |
128 by (case_tac "acc_prefix A list (next A a st)" 1); |
129 by (strip_tac 1); |
129 by (strip_tac 1); |
130 by (res_inst_tac [("f","%k. a#k")] ex_special 1); |
130 by (res_inst_tac [("f","%k. a#k")] ex_special 1); |
148 val step2_c = (result() repeat_RS spec) RS mp; |
148 val step2_c = (result() repeat_RS spec) RS mp; |
149 |
149 |
150 |
150 |
151 goal thy |
151 goal thy |
152 "! st erk r l rest ys yss zs. \ |
152 "! st erk r l rest ys yss zs. \ |
153 \ acc A st (l,rest) xs erk r = (ys#yss, zs) --> \ |
153 \ acc A st (l,rest) erk xs r = (ys#yss, zs) --> \ |
154 \ (if acc_prefix A xs st \ |
154 \ (if acc_prefix A xs st \ |
155 \ then acc A (start A) ([],concat(yss)@zs) (concat(yss)@zs) [] [] = (yss,zs) \ |
155 \ then acc A (start A) ([],concat(yss)@zs) [] (concat(yss)@zs) [] = (yss,zs) \ |
156 \ else (erk~=[] & (l,rest)=(yss,zs)) | (erk=[] & (l, rest)=(ys#yss,zs)))"; |
156 \ else (erk~=[] & (l,rest)=(yss,zs)) | (erk=[] & (l, rest)=(ys#yss,zs)))"; |
157 by (Simp_tac 1); |
157 by (Simp_tac 1); |
158 by (induct_tac "xs" 1); |
158 by (induct_tac "xs" 1); |
159 by (simp_tac (simpset() addcongs [conj_cong]) 1); |
159 by (simp_tac (simpset() addcongs [conj_cong]) 1); |
160 by (Fast_tac 1); |
160 by (Fast_tac 1); |
161 by (asm_simp_tac (simpset() addcongs [conj_cong]) 1); |
161 by (asm_simp_tac (simpset() addcongs [conj_cong]) 1); |
162 by (res_inst_tac [("p","acc A (start A) ([],list) list [] []")] PairE 1); |
162 by (res_inst_tac [("p","acc A (start A) ([],list) [] list []")] PairE 1); |
163 by (rename_tac "vss lrst" 1); |
163 by (rename_tac "vss lrst" 1); |
164 by (Asm_simp_tac 1); |
164 by (Asm_simp_tac 1); |
165 by (strip_tac 1); |
165 by (strip_tac 1); |
166 by (case_tac "acc_prefix A list (next A a st)" 1); |
166 by (case_tac "acc_prefix A list (next A a st)" 1); |
167 by (Asm_simp_tac 1); |
167 by (Asm_simp_tac 1); |
168 by (subgoal_tac "acc A (start A) ([],list) list [] [] = (yss,zs)" 1); |
168 by (subgoal_tac "acc A (start A) ([],list) [] list [] = (yss,zs)" 1); |
169 by (Asm_simp_tac 2); |
169 by (Asm_simp_tac 2); |
170 by (subgoal_tac "r@[a] ~= []" 2); |
170 by (subgoal_tac "r@[a] ~= []" 2); |
171 by (Fast_tac 2); |
171 by (Fast_tac 2); |
172 by (Simp_tac 2); |
172 by (Simp_tac 2); |
173 by (subgoal_tac "concat(yss) @ zs = list" 1); |
173 by (subgoal_tac "concat(yss) @ zs = list" 1); |
187 val step2_d = (result() repeat_RS spec) RS mp; |
187 val step2_d = (result() repeat_RS spec) RS mp; |
188 |
188 |
189 Delsimps [split_paired_All]; |
189 Delsimps [split_paired_All]; |
190 goal thy |
190 goal thy |
191 "! st erk r p ys yss zs. \ |
191 "! st erk r p ys yss zs. \ |
192 \ acc A st p xs erk r = (ys#yss, zs) --> \ |
192 \ acc A st p erk xs r = (ys#yss, zs) --> \ |
193 \ (if acc_prefix A xs st \ |
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))\ |
194 \ then ? g. ys=r@g & (!as. as<=xs & g<=as & g~=as --> ~fin A (delta A as st))\ |
195 \ else (erk~=[] & ys=erk) | (erk=[] & (ys#yss,zs)=p))"; |
195 \ else (erk~=[] & ys=erk) | (erk=[] & (ys#yss,zs)=p))"; |
196 by (Simp_tac 1); |
196 by (Simp_tac 1); |
197 by (induct_tac "xs" 1); |
197 by (induct_tac "xs" 1); |