|
1 theory Simplifying |
|
2 imports "ReStar" |
|
3 begin |
|
4 |
|
5 section {* Lexer including simplifications *} |
|
6 |
|
7 |
|
8 fun F_RIGHT where |
|
9 "F_RIGHT f v = Right (f v)" |
|
10 |
|
11 fun F_LEFT where |
|
12 "F_LEFT f v = Left (f v)" |
|
13 |
|
14 fun F_ALT where |
|
15 "F_ALT f\<^sub>1 f\<^sub>2 (Right v) = Right (f\<^sub>2 v)" |
|
16 | "F_ALT f\<^sub>1 f\<^sub>2 (Left v) = Left (f\<^sub>1 v)" |
|
17 | "F_ALT f1 f2 v = v" |
|
18 |
|
19 |
|
20 fun F_SEQ1 where |
|
21 "F_SEQ1 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 Void) (f\<^sub>2 v)" |
|
22 |
|
23 fun F_SEQ2 where |
|
24 "F_SEQ2 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 v) (f\<^sub>2 Void)" |
|
25 |
|
26 fun F_SEQ where |
|
27 "F_SEQ f\<^sub>1 f\<^sub>2 (Seq v\<^sub>1 v\<^sub>2) = Seq (f\<^sub>1 v\<^sub>1) (f\<^sub>2 v\<^sub>2)" |
|
28 | "F_SEQ f1 f2 v = v" |
|
29 |
|
30 fun simp_ALT where |
|
31 "simp_ALT (ZERO, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_RIGHT f\<^sub>2)" |
|
32 | "simp_ALT (r\<^sub>1, f\<^sub>1) (ZERO, f\<^sub>2) = (r\<^sub>1, F_LEFT f\<^sub>1)" |
|
33 | "simp_ALT (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (ALT r\<^sub>1 r\<^sub>2, F_ALT f\<^sub>1 f\<^sub>2)" |
|
34 |
|
35 fun simp_SEQ where |
|
36 "simp_SEQ (ONE, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_SEQ1 f\<^sub>1 f\<^sub>2)" |
|
37 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2) = (r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)" |
|
38 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (SEQ r\<^sub>1 r\<^sub>2, F_SEQ f\<^sub>1 f\<^sub>2)" |
|
39 |
|
40 lemma simp_SEQ_simps: |
|
41 "simp_SEQ p1 p2 = (if (fst p1 = ONE) then (fst p2, F_SEQ1 (snd p1) (snd p2)) |
|
42 else (if (fst p2 = ONE) then (fst p1, F_SEQ2 (snd p1) (snd p2)) |
|
43 else (SEQ (fst p1) (fst p2), F_SEQ (snd p1) (snd p2))))" |
|
44 apply(auto) |
|
45 apply(case_tac p1) |
|
46 apply(case_tac p2) |
|
47 apply(simp) |
|
48 apply(case_tac p1) |
|
49 apply(case_tac p2) |
|
50 apply(simp) |
|
51 apply(case_tac a) |
|
52 apply(simp_all) |
|
53 apply(case_tac p1) |
|
54 apply(case_tac p2) |
|
55 apply(simp) |
|
56 apply(case_tac p1) |
|
57 apply(case_tac p2) |
|
58 apply(simp) |
|
59 apply(case_tac a) |
|
60 apply(simp_all) |
|
61 apply(case_tac aa) |
|
62 apply(simp_all) |
|
63 apply(auto) |
|
64 apply(case_tac aa) |
|
65 apply(simp_all) |
|
66 apply(case_tac aa) |
|
67 apply(simp_all) |
|
68 apply(case_tac aa) |
|
69 apply(simp_all) |
|
70 apply(case_tac aa) |
|
71 apply(simp_all) |
|
72 done |
|
73 |
|
74 lemma simp_ALT_simps: |
|
75 "simp_ALT p1 p2 = (if (fst p1 = ZERO) then (fst p2, F_RIGHT (snd p2)) |
|
76 else (if (fst p2 = ZERO) then (fst p1, F_LEFT (snd p1)) |
|
77 else (ALT (fst p1) (fst p2), F_ALT (snd p1) (snd p2))))" |
|
78 apply(auto) |
|
79 apply(case_tac p1) |
|
80 apply(case_tac p2) |
|
81 apply(simp) |
|
82 apply(case_tac p1) |
|
83 apply(case_tac p2) |
|
84 apply(simp) |
|
85 apply(case_tac a) |
|
86 apply(simp_all) |
|
87 apply(case_tac p1) |
|
88 apply(case_tac p2) |
|
89 apply(simp) |
|
90 apply(case_tac p1) |
|
91 apply(case_tac p2) |
|
92 apply(simp) |
|
93 apply(case_tac a) |
|
94 apply(simp_all) |
|
95 apply(case_tac aa) |
|
96 apply(simp_all) |
|
97 apply(auto) |
|
98 apply(case_tac aa) |
|
99 apply(simp_all) |
|
100 apply(case_tac aa) |
|
101 apply(simp_all) |
|
102 apply(case_tac aa) |
|
103 apply(simp_all) |
|
104 apply(case_tac aa) |
|
105 apply(simp_all) |
|
106 done |
|
107 |
|
108 |
|
109 fun |
|
110 simp :: "rexp \<Rightarrow> rexp * (val \<Rightarrow> val)" |
|
111 where |
|
112 "simp (ALT r1 r2) = simp_ALT (simp r1) (simp r2)" |
|
113 | "simp (SEQ r1 r2) = simp_SEQ (simp r1) (simp r2)" |
|
114 | "simp r = (r, id)" |
|
115 |
|
116 fun |
|
117 slexer :: "rexp \<Rightarrow> string \<Rightarrow> val option" |
|
118 where |
|
119 "slexer r [] = (if nullable r then Some(mkeps r) else None)" |
|
120 | "slexer r (c#s) = (let (rs, fr) = simp (der c r) in |
|
121 (case (slexer rs s) of |
|
122 None \<Rightarrow> None |
|
123 | Some(v) \<Rightarrow> Some(injval r c (fr v))))" |
|
124 |
|
125 |
|
126 lemma L_fst_simp: |
|
127 shows "L(r) = L(fst (simp r))" |
|
128 using assms |
|
129 apply(induct r rule: rexp.induct) |
|
130 apply(auto simp add: simp_SEQ_simps simp_ALT_simps) |
|
131 done |
|
132 |
|
133 lemma |
|
134 shows "\<turnstile> ((snd (simp r)) v) : r \<longleftrightarrow> \<turnstile> v : (fst (simp r))" |
|
135 using assms |
|
136 apply(induct r arbitrary: v rule: simp.induct) |
|
137 apply(auto simp add: simp_SEQ_simps simp_ALT_simps intro: Prf.intros) |
|
138 using Prf_elims(3) apply blast |
|
139 apply(erule Prf_elims) |
|
140 apply(simp) |
|
141 apply(clarify) |
|
142 apply(blast) |
|
143 apply(simp) |
|
144 apply(erule Prf_elims) |
|
145 apply(simp) |
|
146 apply(simp) |
|
147 apply(clarify) |
|
148 apply(blast) |
|
149 apply(erule Prf_elims) |
|
150 apply(case_tac v) |
|
151 apply(simp_all) |
|
152 apply(rule Prf.intros) |
|
153 apply(clarify) |
|
154 apply(simp) |
|
155 apply(case_tac v) |
|
156 apply(simp_all) |
|
157 apply(rule Prf.intros) |
|
158 apply(clarify) |
|
159 apply(simp) |
|
160 apply(erule Prf_elims) |
|
161 apply(simp) |
|
162 apply(rule Prf.intros) |
|
163 apply(simp) |
|
164 apply(simp) |
|
165 apply(rule Prf.intros) |
|
166 apply(simp) |
|
167 apply(erule Prf_elims) |
|
168 apply(simp) |
|
169 apply(blast) |
|
170 apply(rule Prf.intros) |
|
171 apply(erule Prf_elims) |
|
172 apply(simp) |
|
173 apply(rule Prf.intros) |
|
174 apply(erule Prf_elims) |
|
175 apply(simp) |
|
176 apply(rule Prf.intros) |
|
177 apply(erule Prf_elims) |
|
178 apply(simp) |
|
179 apply(clarify) |
|
180 apply(blast) |
|
181 apply(rule Prf.intros) |
|
182 apply(blast) |
|
183 using Prf.intros(4) apply blast |
|
184 apply(erule Prf_elims) |
|
185 apply(simp) |
|
186 apply(clarify) |
|
187 apply(blast) |
|
188 apply(rule Prf.intros) |
|
189 using Prf.intros(4) apply blast |
|
190 apply blast |
|
191 apply(erule Prf_elims) |
|
192 apply(case_tac v) |
|
193 apply(simp_all) |
|
194 apply(rule Prf.intros) |
|
195 apply(clarify) |
|
196 apply(simp) |
|
197 apply(clarify) |
|
198 apply(blast) |
|
199 apply(erule Prf_elims) |
|
200 apply(case_tac v) |
|
201 apply(simp_all) |
|
202 apply(rule Prf.intros) |
|
203 apply(clarify) |
|
204 apply(simp) |
|
205 apply(simp) |
|
206 done |
|
207 |
|
208 lemma Posix_simp_nullable: |
|
209 assumes "nullable r" "[] \<in> (fst (simp r)) \<rightarrow> v" |
|
210 shows "((snd (simp r)) v) = mkeps r" |
|
211 using assms |
|
212 apply(induct r arbitrary: v) |
|
213 apply(auto simp add: simp_SEQ_simps simp_ALT_simps) |
|
214 apply(erule Posix_elims) |
|
215 apply(simp) |
|
216 apply(erule Posix_elims) |
|
217 apply(clarify) |
|
218 using Posix.intros(1) apply blast |
|
219 using Posix.intros(1) apply blast |
|
220 using Posix.intros(1) apply blast |
|
221 apply(erule Posix_elims) |
|
222 apply(simp) |
|
223 apply(erule Posix_elims) |
|
224 apply (metis L_fst_simp nullable.simps(1) nullable_correctness) |
|
225 apply(erule Posix_elims) |
|
226 apply(clarify) |
|
227 apply(simp) |
|
228 apply(clarify) |
|
229 apply(simp) |
|
230 apply(simp only: L_fst_simp[symmetric]) |
|
231 apply (simp add: nullable_correctness) |
|
232 apply(erule Posix_elims) |
|
233 using L_fst_simp Posix1(1) nullable_correctness apply blast |
|
234 apply (metis L.simps(1) L_fst_simp Prf_flat_L empty_iff mkeps_nullable) |
|
235 apply(erule Posix_elims) |
|
236 apply(clarify) |
|
237 apply(simp) |
|
238 apply(simp only: L_fst_simp[symmetric]) |
|
239 apply (simp add: nullable_correctness) |
|
240 apply(erule Posix_elims) |
|
241 apply(clarify) |
|
242 apply(simp) |
|
243 using L_fst_simp Posix1(1) nullable_correctness apply blast |
|
244 apply(simp) |
|
245 apply(erule Posix_elims) |
|
246 apply(clarify) |
|
247 apply(simp) |
|
248 using Posix1(2) apply auto[1] |
|
249 apply(simp) |
|
250 done |
|
251 |
|
252 lemma Posix_simp: |
|
253 assumes "s \<in> (fst (simp r)) \<rightarrow> v" |
|
254 shows "s \<in> r \<rightarrow> ((snd (simp r)) v)" |
|
255 using assms |
|
256 apply(induct r arbitrary: s v rule: rexp.induct) |
|
257 apply(auto split: if_splits simp add: simp_SEQ_simps simp_ALT_simps) |
|
258 prefer 3 |
|
259 apply(erule Posix_elims) |
|
260 apply(clarify) |
|
261 apply(simp) |
|
262 apply(rule Posix.intros) |
|
263 apply(blast) |
|
264 apply(blast) |
|
265 apply(auto)[1] |
|
266 apply(simp add: L_fst_simp[symmetric]) |
|
267 apply(auto)[1] |
|
268 prefer 3 |
|
269 apply(rule Posix.intros) |
|
270 apply(blast) |
|
271 apply (metis L.simps(1) L_fst_simp equals0D) |
|
272 prefer 3 |
|
273 apply(rule Posix.intros) |
|
274 apply(blast) |
|
275 prefer 3 |
|
276 apply(erule Posix_elims) |
|
277 apply(clarify) |
|
278 apply(simp) |
|
279 apply(rule Posix.intros) |
|
280 apply(blast) |
|
281 apply(simp) |
|
282 apply(rule Posix.intros) |
|
283 apply(blast) |
|
284 apply(simp add: L_fst_simp[symmetric]) |
|
285 apply(subst append.simps[symmetric]) |
|
286 apply(rule Posix.intros) |
|
287 prefer 2 |
|
288 apply(blast) |
|
289 prefer 2 |
|
290 apply(auto)[1] |
|
291 apply (metis L_fst_simp Posix_elims(2) lex_correct3a) |
|
292 apply(subst Posix_simp_nullable) |
|
293 using Posix.intros(1) Posix1(1) nullable_correctness apply blast |
|
294 apply(simp) |
|
295 apply(rule Posix.intros) |
|
296 apply(rule Posix_mkeps) |
|
297 using Posix.intros(1) Posix1(1) nullable_correctness apply blast |
|
298 apply(subst append_Nil2[symmetric]) |
|
299 apply(rule Posix.intros) |
|
300 apply(blast) |
|
301 apply(subst Posix_simp_nullable) |
|
302 using Posix.intros(1) Posix1(1) nullable_correctness apply blast |
|
303 apply(simp) |
|
304 apply(rule Posix.intros) |
|
305 apply(rule Posix_mkeps) |
|
306 using Posix.intros(1) Posix1(1) nullable_correctness apply blast |
|
307 apply(auto) |
|
308 done |
|
309 |
|
310 lemma slexer_correctness: |
|
311 shows "slexer r s = lexer r s" |
|
312 apply(induct s arbitrary: r) |
|
313 apply(simp) |
|
314 apply(simp) |
|
315 apply(auto split: option.split prod.split) |
|
316 apply (metis L_fst_simp fst_conv lex_correct1a) |
|
317 using L_fst_simp lex_correct1a apply fastforce |
|
318 by (metis Posix_determ Posix_simp fst_conv lex_correct1 lex_correct3a option.distinct(1) option.inject snd_conv) |
|
319 |
|
320 |
|
321 |
|
322 end |