|
1 theory Matcher3simple |
|
2 imports "Main" |
|
3 begin |
|
4 |
|
5 section {* Sequential Composition of Sets *} |
|
6 |
|
7 definition |
|
8 Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) |
|
9 where |
|
10 "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}" |
|
11 |
|
12 text {* Two Simple Properties about Sequential Composition *} |
|
13 |
|
14 lemma seq_empty [simp]: |
|
15 shows "A ;; {[]} = A" |
|
16 and "{[]} ;; A = A" |
|
17 by (simp_all add: Sequ_def) |
|
18 |
|
19 lemma seq_null [simp]: |
|
20 shows "A ;; {} = {}" |
|
21 and "{} ;; A = {}" |
|
22 by (simp_all add: Sequ_def) |
|
23 |
|
24 section {* Regular Expressions *} |
|
25 |
|
26 datatype rexp = |
|
27 NULL |
|
28 | EMPTY |
|
29 | CHAR char |
|
30 | SEQ rexp rexp |
|
31 | ALT rexp rexp |
|
32 |
|
33 section {* Semantics of Regular Expressions *} |
|
34 |
|
35 fun |
|
36 L :: "rexp \<Rightarrow> string set" |
|
37 where |
|
38 "L (NULL) = {}" |
|
39 | "L (EMPTY) = {[]}" |
|
40 | "L (CHAR c) = {[c]}" |
|
41 | "L (SEQ r1 r2) = (L r1) ;; (L r2)" |
|
42 | "L (ALT r1 r2) = (L r1) \<union> (L r2)" |
|
43 |
|
44 datatype val = |
|
45 Void |
|
46 | Char char |
|
47 | Seq val val |
|
48 | Right val |
|
49 | Left val |
|
50 |
|
51 inductive Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100) |
|
52 where |
|
53 "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2" |
|
54 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2" |
|
55 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2" |
|
56 | "\<turnstile> Void : EMPTY" |
|
57 | "\<turnstile> Char c : CHAR c" |
|
58 |
|
59 fun flat :: "val \<Rightarrow> string" |
|
60 where |
|
61 "flat(Void) = []" |
|
62 | "flat(Char c) = [c]" |
|
63 | "flat(Left v) = flat(v)" |
|
64 | "flat(Right v) = flat(v)" |
|
65 | "flat(Seq v1 v2) = flat(v1) @ flat(v2)" |
|
66 |
|
67 datatype tree = |
|
68 Leaf string |
|
69 | Branch tree tree |
|
70 |
|
71 fun flats :: "val \<Rightarrow> tree" |
|
72 where |
|
73 "flats(Void) = Leaf []" |
|
74 | "flats(Char c) = Leaf [c]" |
|
75 | "flats(Left v) = flats(v)" |
|
76 | "flats(Right v) = flats(v)" |
|
77 | "flats(Seq v1 v2) = Branch (flats v1) (flats v2)" |
|
78 |
|
79 fun flatten :: "tree \<Rightarrow> string" |
|
80 where |
|
81 "flatten (Leaf s) = s" |
|
82 | "flatten (Branch t1 t2) = flatten t1 @ flatten t2" |
|
83 |
|
84 lemma flats_flat: |
|
85 shows "flat v1 = flatten (flats v1)" |
|
86 apply(induct v1) |
|
87 apply(simp_all) |
|
88 done |
|
89 |
|
90 lemma Prf_flat_L: |
|
91 assumes "\<turnstile> v : r" shows "flat v \<in> L r" |
|
92 using assms |
|
93 apply(induct) |
|
94 apply(auto simp add: Sequ_def) |
|
95 done |
|
96 |
|
97 lemma L_flat_Prf: |
|
98 "L(r) = {flat v | v. \<turnstile> v : r}" |
|
99 apply(induct r) |
|
100 apply(auto dest: Prf_flat_L simp add: Sequ_def) |
|
101 apply (metis Prf.intros(4) flat.simps(1)) |
|
102 apply (metis Prf.intros(5) flat.simps(2)) |
|
103 apply (metis Prf.intros(1) flat.simps(5)) |
|
104 apply (metis Prf.intros(2) flat.simps(3)) |
|
105 apply (metis Prf.intros(3) flat.simps(4)) |
|
106 by (smt Prf.cases flat.simps(3) flat.simps(4) rexp.distinct(13) rexp.distinct(17) rexp.distinct(19) rexp.inject(3)) |
|
107 |
|
108 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100) |
|
109 where |
|
110 "\<lbrakk>v1 \<succ>r1 v1'; v2 \<succ>r2 v2'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" |
|
111 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)" |
|
112 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)" |
|
113 | "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')" |
|
114 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')" |
|
115 | "Void \<succ>EMPTY Void" |
|
116 | "(Char c) \<succ>(CHAR c) (Char c)" |
|
117 |
|
118 lemma |
|
119 assumes "r = SEQ (ALT EMPTY EMPTY) (ALT EMPTY (CHAR c))" |
|
120 shows "(Seq (Left Void) (Right (Char c))) \<succ>r (Seq (Left Void) (Left Void))" |
|
121 using assms |
|
122 apply(simp) |
|
123 apply(rule ValOrd.intros) |
|
124 apply(rule ValOrd.intros) |
|
125 apply(rule ValOrd.intros) |
|
126 apply(rule ValOrd.intros) |
|
127 apply(simp) |
|
128 done |
|
129 |
|
130 |
|
131 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" |
|
132 where |
|
133 "POSIX v r \<equiv> (\<forall>v'. (\<turnstile> v' : r \<and> flats v = flats v') \<longrightarrow> v \<succ>r v')" |
|
134 |
|
135 lemma POSIX: |
|
136 assumes "r = SEQ (ALT EMPTY EMPTY) (ALT EMPTY (CHAR c))" |
|
137 shows "POSIX (Seq (Left Void) (Right (Char c))) r" |
|
138 apply(simp add: POSIX_def assms) |
|
139 apply(auto) |
|
140 apply(erule Prf.cases) |
|
141 apply(simp_all) |
|
142 apply(rule ValOrd.intros) |
|
143 apply (smt POSIX_def Prf.cases Prf.simps ValOrd.intros(2) ValOrd.intros(5) ValOrd.intros(6) flats.simps(1) flats.simps(3) rexp.distinct(11) rexp.distinct(13) rexp.distinct(17) rexp.distinct(19) rexp.distinct(9) rexp.inject(3) val.distinct(19) val.inject(3)) |
|
144 by (smt Prf.simps ValOrd.intros(4) ValOrd.intros(7) flats.simps(1) flats.simps(3) list.distinct(1) rexp.distinct(11) rexp.distinct(13) rexp.distinct(15) rexp.distinct(17) rexp.distinct(19) rexp.distinct(9) rexp.inject(1) rexp.inject(3) tree.inject(1)) |
|
145 |
|
146 |
|
147 lemma Exists_POSIX: "\<exists>v. POSIX v r" |
|
148 apply(induct r) |
|
149 apply(auto simp add: POSIX_def) |
|
150 apply(rule exI) |
|
151 apply(auto) |
|
152 apply(erule Prf.cases) |
|
153 apply(simp_all)[5] |
|
154 apply (smt Prf.simps ValOrd.intros(6) rexp.distinct(11) rexp.distinct(13) rexp.distinct(9)) |
|
155 apply(rule exI) |
|
156 apply(auto) |
|
157 apply(erule Prf.cases) |
|
158 apply(simp_all)[5] |
|
159 apply(rule ValOrd.intros) |
|
160 apply(rule exI) |
|
161 apply(auto) |
|
162 apply(erule Prf.cases) |
|
163 apply(simp_all)[5] |
|
164 apply(rule ValOrd.intros) |
|
165 apply(auto)[2] |
|
166 apply(rule_tac x="Left v" in exI) |
|
167 apply(auto) |
|
168 apply(erule Prf.cases) |
|
169 apply(simp_all)[5] |
|
170 apply(rule ValOrd.intros) |
|
171 apply(auto)[1] |
|
172 apply(auto) |
|
173 apply(rule ValOrd.intros) |
|
174 by (metis flats_flat order_refl) |
|
175 |
|
176 |
|
177 lemma POSIX_SEQ: |
|
178 assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2" |
|
179 shows "POSIX v1 r1 \<and> POSIX v2 r2" |
|
180 using assms |
|
181 unfolding POSIX_def |
|
182 apply(auto) |
|
183 apply(drule_tac x="Seq v' v2" in spec) |
|
184 apply(simp) |
|
185 apply (smt Prf.intros(1) ValOrd.simps assms(3) rexp.inject(2) val.distinct(15) val.distinct(17) val.distinct(3) val.distinct(9) val.inject(2)) |
|
186 apply(drule_tac x="Seq v1 v'" in spec) |
|
187 apply(simp) |
|
188 by (smt Prf.intros(1) ValOrd.simps rexp.inject(2) val.distinct(15) val.distinct(17) val.distinct(3) val.distinct(9) val.inject(2)) |
|
189 |
|
190 lemma POSIX_SEQ_I: |
|
191 assumes "POSIX v1 r1" "POSIX v2 r2" |
|
192 shows "POSIX (Seq v1 v2) (SEQ r1 r2)" |
|
193 using assms |
|
194 unfolding POSIX_def |
|
195 apply(auto) |
|
196 apply(rotate_tac 4) |
|
197 apply(erule Prf.cases) |
|
198 apply(simp_all)[5] |
|
199 apply(auto)[1] |
|
200 apply(rule ValOrd.intros) |
|
201 apply(auto) |
|
202 done |
|
203 |
|
204 lemma POSIX_ALT: |
|
205 assumes "POSIX (Left v1) (ALT r1 r2)" |
|
206 shows "POSIX v1 r1" |
|
207 using assms |
|
208 unfolding POSIX_def |
|
209 apply(auto) |
|
210 apply(drule_tac x="Left v'" in spec) |
|
211 apply(simp) |
|
212 apply(drule mp) |
|
213 apply(rule Prf.intros) |
|
214 apply(auto) |
|
215 apply(erule ValOrd.cases) |
|
216 apply(simp_all)[7] |
|
217 done |
|
218 |
|
219 lemma POSIX_ALT1a: |
|
220 assumes "POSIX (Right v2) (ALT r1 r2)" |
|
221 shows "POSIX v2 r2" |
|
222 using assms |
|
223 unfolding POSIX_def |
|
224 apply(auto) |
|
225 apply(drule_tac x="Right v'" in spec) |
|
226 apply(simp) |
|
227 apply(drule mp) |
|
228 apply(rule Prf.intros) |
|
229 apply(auto) |
|
230 apply(erule ValOrd.cases) |
|
231 apply(simp_all)[7] |
|
232 done |
|
233 |
|
234 lemma POSIX_ALT1b: |
|
235 assumes "POSIX (Right v2) (ALT r1 r2)" |
|
236 shows "(\<forall>v'. (\<turnstile> v' : r2 \<and> flats v' = flats v2) \<longrightarrow> v2 \<succ>r2 v')" |
|
237 using assms |
|
238 apply(drule_tac POSIX_ALT1a) |
|
239 unfolding POSIX_def |
|
240 apply(auto) |
|
241 done |
|
242 |
|
243 lemma POSIX_ALT_I1: |
|
244 assumes "POSIX v1 r1" |
|
245 shows "POSIX (Left v1) (ALT r1 r2)" |
|
246 using assms |
|
247 unfolding POSIX_def |
|
248 apply(auto) |
|
249 apply(rotate_tac 3) |
|
250 apply(erule Prf.cases) |
|
251 apply(simp_all)[5] |
|
252 apply(auto) |
|
253 apply(rule ValOrd.intros) |
|
254 apply(auto) |
|
255 apply(rule ValOrd.intros) |
|
256 by (metis flats_flat order_refl) |
|
257 |
|
258 lemma POSIX_ALT_I2: |
|
259 assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')" |
|
260 shows "POSIX (Right v2) (ALT r1 r2)" |
|
261 using assms |
|
262 unfolding POSIX_def |
|
263 apply(auto) |
|
264 apply(rotate_tac 3) |
|
265 apply(erule Prf.cases) |
|
266 apply(simp_all)[5] |
|
267 apply(auto) |
|
268 prefer 2 |
|
269 apply(rule ValOrd.intros) |
|
270 apply metis |
|
271 apply(rule ValOrd.intros) |
|
272 apply(auto) |
|
273 done |
|
274 |
|
275 lemma ValOrd_refl: |
|
276 assumes "\<turnstile> v : r" |
|
277 shows "v \<succ>r v" |
|
278 using assms |
|
279 apply(induct) |
|
280 apply(auto intro: ValOrd.intros) |
|
281 done |
|
282 |
|
283 lemma ValOrd_length: |
|
284 assumes "v1 \<succ>r v2" shows "length (flat v1) \<ge> length (flat v2)" |
|
285 using assms |
|
286 apply(induct) |
|
287 apply(auto) |
|
288 done |
|
289 |
|
290 section {* The Matcher *} |
|
291 |
|
292 fun |
|
293 nullable :: "rexp \<Rightarrow> bool" |
|
294 where |
|
295 "nullable (NULL) = False" |
|
296 | "nullable (EMPTY) = True" |
|
297 | "nullable (CHAR c) = False" |
|
298 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)" |
|
299 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" |
|
300 |
|
301 lemma nullable_correctness: |
|
302 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
|
303 apply (induct r) |
|
304 apply(auto simp add: Sequ_def) |
|
305 done |
|
306 |
|
307 fun mkeps :: "rexp \<Rightarrow> val" |
|
308 where |
|
309 "mkeps(EMPTY) = Void" |
|
310 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)" |
|
311 | "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))" |
|
312 |
|
313 lemma mkeps_nullable: |
|
314 assumes "nullable(r)" shows "\<turnstile> mkeps r : r" |
|
315 using assms |
|
316 apply(induct rule: nullable.induct) |
|
317 apply(auto intro: Prf.intros) |
|
318 done |
|
319 |
|
320 lemma mkeps_flat: |
|
321 assumes "nullable(r)" shows "flat (mkeps r) = []" |
|
322 using assms |
|
323 apply(induct rule: nullable.induct) |
|
324 apply(auto) |
|
325 done |
|
326 |
|
327 |
|
328 lemma mkeps_flats: |
|
329 assumes "nullable(r)" shows "flatten (flats (mkeps r)) = []" |
|
330 using assms |
|
331 apply(induct rule: nullable.induct) |
|
332 apply(auto) |
|
333 done |
|
334 |
|
335 lemma mkeps_POSIX: |
|
336 assumes "nullable r" |
|
337 shows "POSIX (mkeps r) r" |
|
338 using assms |
|
339 apply(induct r) |
|
340 apply(auto) |
|
341 apply(simp add: POSIX_def) |
|
342 apply(auto)[1] |
|
343 apply(erule Prf.cases) |
|
344 apply(simp_all)[5] |
|
345 apply (metis ValOrd.intros(6)) |
|
346 apply(simp add: POSIX_def) |
|
347 apply(auto)[1] |
|
348 apply(erule Prf.cases) |
|
349 apply(simp_all)[5] |
|
350 apply(auto) |
|
351 apply (metis ValOrd.intros(1) append_is_Nil_conv mkeps_flat) |
|
352 apply(simp add: POSIX_def) |
|
353 apply(auto)[1] |
|
354 apply(erule Prf.cases) |
|
355 apply(simp_all)[5] |
|
356 apply(auto) |
|
357 apply (metis ValOrd.intros(5)) |
|
358 apply(rule ValOrd.intros(2)) |
|
359 apply(simp add: mkeps_flat) |
|
360 apply(simp add: flats_flat) |
|
361 apply (metis mkeps_flats) |
|
362 apply(simp add: POSIX_def) |
|
363 apply(auto)[1] |
|
364 apply(erule Prf.cases) |
|
365 apply(simp_all)[5] |
|
366 apply(auto) |
|
367 apply (metis ValOrd.intros(5)) |
|
368 apply (smt ValOrd.intros(2) flats_flat) |
|
369 apply(simp add: POSIX_def) |
|
370 apply(auto)[1] |
|
371 apply(erule Prf.cases) |
|
372 apply(simp_all)[5] |
|
373 apply (metis Prf_flat_L flats_flat mkeps_flats nullable_correctness) |
|
374 by (metis ValOrd.intros(4)) |
|
375 |
|
376 fun |
|
377 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
|
378 where |
|
379 "der c (NULL) = NULL" |
|
380 | "der c (EMPTY) = NULL" |
|
381 | "der c (CHAR c') = (if c = c' then EMPTY else NULL)" |
|
382 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)" |
|
383 | "der c (SEQ r1 r2) = |
|
384 (if nullable r1 |
|
385 then ALT (SEQ (der c r1) r2) (der c r2) |
|
386 else SEQ (der c r1) r2)" |
|
387 |
|
388 fun |
|
389 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
|
390 where |
|
391 "ders [] r = r" |
|
392 | "ders (c # s) r = ders s (der c r)" |
|
393 |
|
394 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
|
395 where |
|
396 "injval (CHAR d) c Void = Char d" |
|
397 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)" |
|
398 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)" |
|
399 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2" |
|
400 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2" |
|
401 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)" |
|
402 |
|
403 fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
|
404 where |
|
405 "projval (CHAR d) c _ = Void" |
|
406 | "projval (ALT r1 r2) c (Left v1) = Left(projval r1 c v1)" |
|
407 | "projval (ALT r1 r2) c (Right v2) = Right(projval r2 c v2)" |
|
408 | "projval (SEQ r1 r2) c (Seq v1 v2) = |
|
409 (if flat v1 = [] then Right(projval r2 c v2) |
|
410 else if nullable r1 then Left (Seq (projval r1 c v1) v2) |
|
411 else Seq (projval r1 c v1) v2)" |
|
412 |
|
413 lemma v3: |
|
414 assumes "\<turnstile> v : der c r" shows "\<turnstile> (injval r c v) : r" |
|
415 using assms |
|
416 apply(induct arbitrary: v rule: der.induct) |
|
417 apply(simp) |
|
418 apply(erule Prf.cases) |
|
419 apply(simp_all)[5] |
|
420 apply(erule Prf.cases) |
|
421 apply(simp_all)[5] |
|
422 apply(case_tac "c = c'") |
|
423 apply(simp) |
|
424 apply(erule Prf.cases) |
|
425 apply(simp_all)[5] |
|
426 apply (metis Prf.intros(5)) |
|
427 apply(erule Prf.cases) |
|
428 apply(simp_all)[5] |
|
429 apply(erule Prf.cases) |
|
430 apply(simp_all)[5] |
|
431 apply (metis Prf.intros(2)) |
|
432 apply (metis Prf.intros(3)) |
|
433 apply(simp) |
|
434 apply(case_tac "nullable r1") |
|
435 apply(simp) |
|
436 apply(erule Prf.cases) |
|
437 apply(simp_all)[5] |
|
438 apply(auto)[1] |
|
439 apply(erule Prf.cases) |
|
440 apply(simp_all)[5] |
|
441 apply(auto)[1] |
|
442 apply (metis Prf.intros(1)) |
|
443 apply(auto)[1] |
|
444 apply (metis Prf.intros(1) mkeps_nullable) |
|
445 apply(simp) |
|
446 apply(erule Prf.cases) |
|
447 apply(simp_all)[5] |
|
448 apply(auto)[1] |
|
449 apply(rule Prf.intros) |
|
450 apply(auto)[2] |
|
451 done |
|
452 |
|
453 fun head where |
|
454 "head [] = None" |
|
455 | "head (x#xs) = Some x" |
|
456 |
|
457 lemma head1: |
|
458 assumes "head (xs @ ys) = Some x" |
|
459 shows "(head xs = Some x) \<or> (xs = [] \<and> head ys = Some x)" |
|
460 using assms |
|
461 apply(induct xs) |
|
462 apply(auto) |
|
463 done |
|
464 |
|
465 lemma head2: |
|
466 assumes "head (xs @ ys) = None" |
|
467 shows "(head xs = None) \<and> (head ys = None)" |
|
468 using assms |
|
469 apply(induct xs) |
|
470 apply(auto) |
|
471 done |
|
472 |
|
473 lemma v4: |
|
474 assumes "\<turnstile> v : der c r" shows "flat (injval r c v) = c#(flat v)" |
|
475 using assms |
|
476 apply(induct arbitrary: v rule: der.induct) |
|
477 apply(simp) |
|
478 apply(erule Prf.cases) |
|
479 apply(simp_all)[5] |
|
480 apply(simp) |
|
481 apply(erule Prf.cases) |
|
482 apply(simp_all)[5] |
|
483 apply(simp) |
|
484 apply(case_tac "c = c'") |
|
485 apply(simp) |
|
486 apply(auto)[1] |
|
487 apply(erule Prf.cases) |
|
488 apply(simp_all)[5] |
|
489 apply(simp) |
|
490 apply(erule Prf.cases) |
|
491 apply(simp_all)[5] |
|
492 apply(simp) |
|
493 apply(erule Prf.cases) |
|
494 apply(simp_all)[5] |
|
495 apply(simp) |
|
496 apply(case_tac "nullable r1") |
|
497 apply(simp) |
|
498 apply(erule Prf.cases) |
|
499 apply(simp_all)[5] |
|
500 apply(auto)[1] |
|
501 apply(erule Prf.cases) |
|
502 apply(simp_all)[5] |
|
503 apply(auto)[1] |
|
504 apply (metis mkeps_flat) |
|
505 apply(simp) |
|
506 apply(erule Prf.cases) |
|
507 apply(simp_all)[5] |
|
508 done |
|
509 |
|
510 |
|
511 lemma proj_inj_id: |
|
512 assumes "\<turnstile> v : der c r" |
|
513 shows "projval r c (injval r c v) = v" |
|
514 using assms |
|
515 apply(induct r arbitrary: c v rule: rexp.induct) |
|
516 apply(simp) |
|
517 apply(erule Prf.cases) |
|
518 apply(simp_all)[5] |
|
519 apply(simp) |
|
520 apply(erule Prf.cases) |
|
521 apply(simp_all)[5] |
|
522 apply(simp) |
|
523 apply(case_tac "c = char") |
|
524 apply(simp) |
|
525 apply(erule Prf.cases) |
|
526 apply(simp_all)[5] |
|
527 apply(simp) |
|
528 apply(erule Prf.cases) |
|
529 apply(simp_all)[5] |
|
530 defer |
|
531 apply(simp) |
|
532 apply(erule Prf.cases) |
|
533 apply(simp_all)[5] |
|
534 apply(simp) |
|
535 apply(case_tac "nullable rexp1") |
|
536 apply(simp) |
|
537 apply(erule Prf.cases) |
|
538 apply(simp_all)[5] |
|
539 apply(auto)[1] |
|
540 apply(erule Prf.cases) |
|
541 apply(simp_all)[5] |
|
542 apply(auto)[1] |
|
543 apply (metis list.distinct(1) v4) |
|
544 apply(auto)[1] |
|
545 apply (metis mkeps_flat) |
|
546 apply(auto) |
|
547 apply(erule Prf.cases) |
|
548 apply(simp_all)[5] |
|
549 apply(auto)[1] |
|
550 apply(simp add: v4) |
|
551 done |
|
552 |
|
553 lemma Le_2a: "(head (flat v) = None) = (flat v = [])" |
|
554 apply(induct v) |
|
555 apply(simp_all) |
|
556 apply (metis Nil_is_append_conv head.elims option.distinct(1)) |
|
557 done |
|
558 |
|
559 lemma v5: |
|
560 assumes "\<turnstile> v : der c r" "POSIX v (der c r)" |
|
561 shows "POSIX (injval r c v) r" |
|
562 using assms |
|
563 apply(induct arbitrary: v rule: der.induct) |
|
564 apply(simp) |
|
565 apply(erule Prf.cases) |
|
566 apply(simp_all)[5] |
|
567 apply(simp) |
|
568 apply(erule Prf.cases) |
|
569 apply(simp_all)[5] |
|
570 apply(simp) |
|
571 apply(case_tac "c = c'") |
|
572 apply(auto simp add: POSIX_def)[1] |
|
573 apply(erule Prf.cases) |
|
574 apply(simp_all)[5] |
|
575 apply(erule Prf.cases) |
|
576 apply(simp_all)[5] |
|
577 apply (metis ValOrd.intros(7)) |
|
578 apply(erule Prf.cases) |
|
579 apply(simp_all)[5] |
|
580 prefer 2 |
|
581 apply(simp) |
|
582 apply(case_tac "nullable r1") |
|
583 apply(simp) |
|
584 defer |
|
585 apply(simp) |
|
586 apply(erule Prf.cases) |
|
587 apply(simp_all)[5] |
|
588 apply(auto)[1] |
|
589 apply(drule POSIX_SEQ) |
|
590 apply(assumption) |
|
591 apply(assumption) |
|
592 apply(auto)[1] |
|
593 apply(rule POSIX_SEQ_I) |
|
594 apply metis |
|
595 apply(simp) |
|
596 apply(simp) |
|
597 apply(erule Prf.cases) |
|
598 apply(simp_all)[5] |
|
599 apply(auto)[1] |
|
600 apply(drule POSIX_ALT) |
|
601 apply(rule POSIX_ALT_I1) |
|
602 apply metis |
|
603 defer |
|
604 apply(erule Prf.cases) |
|
605 apply(simp_all)[5] |
|
606 apply(auto) |
|
607 apply(rotate_tac 5) |
|
608 apply(erule Prf.cases) |
|
609 apply(simp_all)[5] |
|
610 apply(auto)[1] |
|
611 apply(drule POSIX_ALT) |
|
612 apply(drule POSIX_SEQ) |
|
613 apply(simp) |
|
614 apply(simp) |
|
615 apply(rule POSIX_SEQ_I) |
|
616 apply metis |
|
617 apply(simp) |
|
618 apply(drule POSIX_ALT1a) |
|
619 apply(rule POSIX_SEQ_I) |
|
620 apply (metis mkeps_POSIX) |
|
621 apply(metis) |
|
622 apply(frule POSIX_ALT1a) |
|
623 apply(rotate_tac 1) |
|
624 apply(drule_tac x="v2" in meta_spec) |
|
625 apply(simp) |
|
626 apply(rule POSIX_ALT_I2) |
|
627 apply(simp) |
|
628 apply(frule POSIX_ALT1a) |
|
629 apply(auto) |
|
630 apply(subst v4) |
|
631 apply(simp) |
|
632 apply(simp) |
|
633 apply(case_tac "\<exists>r. v2 \<succ>r v'") |
|
634 apply (metis ValOrd_length le_neq_implies_less less_Suc_eq) |
|
635 apply(auto)[1] |
|
636 apply(frule_tac x="der c r2" in spec) |
|
637 apply(subgoal_tac "\<not>(Right v2 \<succ>(ALT (der c r1) (der c r2)) Right v')") |
|
638 prefer 2 |
|
639 apply(rule notI) |
|
640 apply(erule ValOrd.cases) |
|
641 apply(simp_all)[7] |
|
642 apply(subst (asm) (1) POSIX_def) |
|
643 apply(simp) |
|
644 apply(subgoal_tac "(\<not> \<turnstile> Right v' : ALT (der c r1) (der c r2)) \<or> (flats v2 \<noteq> flats v')") |
|
645 prefer 2 |
|
646 apply (metis flats.simps(4)) |
|
647 apply(simp) |
|
648 apply(auto)[1] |
|
649 apply(subst v4) |
|
650 apply(simp) |
|
651 apply(simp) |
|
652 apply(case_tac "v2 \<succ>r1 v'") |
|
653 apply (metis ValOrd_length le_neq_implies_less less_Suc_eq) |
|
654 apply( |
|
655 |
|
656 apply(drule_tac x="projval (ALT r1 r2) c v'" in spec) |
|
657 apply(drule mp) |
|
658 apply(auto) |
|
659 apply(frule POSIX_ALT1b) |
|
660 apply(auto) |
|
661 apply(subst v4) |
|
662 apply(simp) |
|
663 apply(simp) |
|
664 apply(simp add: flats_flat) |
|
665 apply(rotate_tac 1) |
|
666 apply(drule_tac x="v2" in meta_spec) |
|
667 apply(simp) |
|
668 apply(rule POSIX_ALT_I2) |
|
669 apply(simp) |
|
670 apply(auto)[1] |
|
671 apply(subst v4) |
|
672 apply(simp) |
|
673 defer |
|
674 apply(erule Prf.cases) |
|
675 apply(simp_all)[5] |
|
676 apply(auto) |
|
677 apply(rotate_tac 5) |
|
678 apply(erule Prf.cases) |
|
679 apply(simp_all)[5] |
|
680 apply(auto)[1] |
|
681 apply(drule POSIX_ALT) |
|
682 apply(drule POSIX_SEQ) |
|
683 apply(simp) |
|
684 apply(simp) |
|
685 apply(rule POSIX_SEQ_I) |
|
686 apply metis |
|
687 apply(simp) |
|
688 apply(drule POSIX_ALT1a) |
|
689 apply(rule POSIX_SEQ_I) |
|
690 apply (metis mkeps_POSIX) |
|
691 apply metis |
|
692 apply(drule_tac x="projval r1 c v'" in meta_spec) |
|
693 apply(drule meta_mp) |
|
694 defer |
|
695 apply(drule meta_mp) |
|
696 defer |
|
697 apply(subst (asm) (1) POSIX_def) |
|
698 apply(simp) |
|
699 |
|
700 |
|
701 |
|
702 lemma inj_proj_id: |
|
703 assumes "\<turnstile> v : r" "POSIX v r" "head (flat v) = Some c" |
|
704 shows "injval r c (projval r c v) = v" |
|
705 using assms |
|
706 apply(induct v r arbitrary: rule: Prf.induct) |
|
707 apply(simp) |
|
708 apply(auto)[1] |
|
709 |
|
710 apply(simp) |
|
711 apply(frule POSIX_head) |
|
712 apply(assumption) |
|
713 apply(simp) |
|
714 apply(drule meta_mp) |
|
715 |
|
716 apply(frule POSIX_E1) |
|
717 apply(erule Prf.cases) |
|
718 apply(simp_all)[7] |
|
719 apply(frule POSIX_E1) |
|
720 apply(erule Prf.cases) |
|
721 apply(simp_all)[7] |
|
722 apply(frule POSIX_E1) |
|
723 apply(erule Prf.cases) |
|
724 apply(simp_all)[7] |
|
725 apply(frule POSIX_E1) |
|
726 defer |
|
727 apply(frule POSIX_E1) |
|
728 apply(erule Prf.cases) |
|
729 apply(simp_all)[7] |
|
730 apply(auto)[1] |
|
731 |
|
732 apply(simp) |
|
733 apply(erule Prf.cases) |
|
734 apply(simp_all)[7] |
|
735 apply(simp) |
|
736 apply(case_tac "c = char") |
|
737 apply(simp) |
|
738 apply(erule Prf.cases) |
|
739 apply(simp_all)[7] |
|
740 apply(simp) |
|
741 apply(erule Prf.cases) |
|
742 apply(simp_all)[7] |
|
743 |
|
744 |
|
745 lemma POSIX_head: |
|
746 assumes "POSIX (Stars (v#vs)) (STAR r)" "head (flat v @ flat (Stars vs)) = Some c" |
|
747 shows "head (flat v) = Some c" |
|
748 using assms |
|
749 apply(rule_tac ccontr) |
|
750 apply(frule POSIX_E1) |
|
751 apply(drule Le_1) |
|
752 apply(assumption) |
|
753 apply(auto)[1] |
|
754 apply(auto simp add: POSIX_def) |
|
755 apply(drule_tac x="Stars (v'#vs')" in spec) |
|
756 apply(simp) |
|
757 apply(simp add: ValOrd_eq_def) |
|
758 apply(auto) |
|
759 apply(erule ValOrd.cases) |
|
760 apply(simp_all) |
|
761 apply(auto) |
|
762 using Le_2 |
|
763 |
|
764 by (metis Le_2 Le_2a head1) |
|
765 |
|
766 |
|
767 lemma inj_proj_id: |
|
768 assumes "\<turnstile> v : r" "POSIX v r" "head (flat v) = Some c" |
|
769 shows "injval r c (projval r c v) = v" |
|
770 using assms |
|
771 apply(induct r arbitrary: rule: Prf.induct) |
|
772 apply(simp) |
|
773 apply(simp) |
|
774 apply(frule POSIX_head) |
|
775 apply(assumption) |
|
776 apply(simp) |
|
777 apply(drule meta_mp) |
|
778 |
|
779 apply(frule POSIX_E1) |
|
780 apply(erule Prf.cases) |
|
781 apply(simp_all)[7] |
|
782 apply(frule POSIX_E1) |
|
783 apply(erule Prf.cases) |
|
784 apply(simp_all)[7] |
|
785 apply(frule POSIX_E1) |
|
786 apply(erule Prf.cases) |
|
787 apply(simp_all)[7] |
|
788 apply(frule POSIX_E1) |
|
789 defer |
|
790 apply(frule POSIX_E1) |
|
791 apply(erule Prf.cases) |
|
792 apply(simp_all)[7] |
|
793 apply(auto)[1] |
|
794 |
|
795 apply(simp) |
|
796 apply(erule Prf.cases) |
|
797 apply(simp_all)[7] |
|
798 apply(simp) |
|
799 apply(case_tac "c = char") |
|
800 apply(simp) |
|
801 apply(erule Prf.cases) |
|
802 apply(simp_all)[7] |
|
803 apply(simp) |
|
804 apply(erule Prf.cases) |
|
805 apply(simp_all)[7] |
|
806 defer |
|
807 apply(simp) |
|
808 apply(erule Prf.cases) |
|
809 apply(simp_all)[7] |
|
810 apply(simp) |
|
811 apply(erule Prf.cases) |
|
812 apply(simp_all)[7] |
|
813 apply(auto)[1] |
|
814 apply(rotate_tac 2) |
|
815 apply(erule Prf.cases) |
|
816 apply(simp_all)[7] |
|
817 apply(case_tac "nullable rexp1") |
|
818 apply(simp) |
|
819 apply(erule Prf.cases) |
|
820 apply(simp_all)[7] |
|
821 apply(auto)[1] |
|
822 apply(erule Prf.cases) |
|
823 apply(simp_all)[7] |
|
824 apply(auto)[1] |
|
825 apply(simp add: v4) |
|
826 apply(auto)[1] |
|
827 apply(simp add: v2a) |
|
828 apply(simp only: der.simps) |
|
829 apply(simp) |
|
830 apply(erule Prf.cases) |
|
831 apply(simp_all)[7] |
|
832 apply(auto)[1] |
|
833 apply(simp add: v4) |
|
834 done |
|
835 |
|
836 |
|
837 |
|
838 lemma STAR_obtain: |
|
839 assumes "\<turnstile> v : STAR r" |
|
840 obtains vs where "\<turnstile> Stars vs : STAR r" and "v = Stars vs" |
|
841 using assms |
|
842 by (smt Prf.cases rexp.distinct(17) rexp.distinct(23) rexp.distinct(27) rexp.distinct(29)) |
|
843 |
|
844 fun first :: "val \<Rightarrow> char option" |
|
845 where |
|
846 "first Void = None" |
|
847 | "first (Char c) = Some c" |
|
848 | "first (Seq v1 v2) = (if (\<exists>c. first v1 = Some c) then first v1 else first v2)" |
|
849 | "first (Right v) = first v" |
|
850 | "first (Left v) = first v" |
|
851 | "first (Stars []) = None" |
|
852 | "first (Stars (v#vs)) = (if (\<exists>c. first v = Some c) then first v else first (Stars vs))" |
|
853 |
|
854 lemma flat: |
|
855 shows "flat v = [] \<longleftrightarrow> first v = None" |
|
856 and "flat (Stars vs) = [] \<longleftrightarrow> first (Stars vs) = None" |
|
857 apply(induct v and vs) |
|
858 apply(auto) |
|
859 done |
|
860 |
|
861 lemma first: |
|
862 shows "first v = Some c \<Longrightarrow> head (flat v @ ys) = Some c" |
|
863 apply(induct arbitrary: ys rule: first.induct) |
|
864 apply(auto split: if_splits simp add: flat[symmetric]) |
|
865 done |
|
866 |
|
867 |
|
868 |
|
869 lemma v5: |
|
870 assumes "POSIX v r" "head (flat v) = Some c" |
|
871 shows "\<turnstile> projval r c v : der c r" |
|
872 using assms |
|
873 apply(induct r arbitrary: c v rule: rexp.induct) |
|
874 prefer 6 |
|
875 apply(frule POSIX_E1) |
|
876 apply(erule Prf.cases) |
|
877 apply(simp_all)[7] |
|
878 apply(rule Prf.intros) |
|
879 apply(drule_tac x="c" in meta_spec) |
|
880 apply(drule_tac x="va" in meta_spec) |
|
881 apply(drule meta_mp) |
|
882 apply(simp add: POSIX_def) |
|
883 apply(auto)[1] |
|
884 apply(drule_tac x="Stars (v'#vs)" in spec) |
|
885 apply(simp) |
|
886 apply(drule mp) |
|
887 apply (metis Prf.intros(2)) |
|
888 apply(simp add: ValOrd_eq_def) |
|
889 apply(erule disjE) |
|
890 apply(simp) |
|
891 apply(erule ValOrd.cases) |
|
892 apply(simp_all)[10] |
|
893 apply(drule_tac meta_mp) |
|
894 apply(drule head1) |
|
895 apply(auto)[1] |
|
896 apply(simp add: POSIX_def) |
|
897 apply(auto)[1] |
|
898 apply(drule_tac x="Stars (va#vs)" in spec) |
|
899 apply(simp) |
|
900 prefer 6 |
|
901 apply(simp) |
|
902 apply(auto split: if_splits)[1] |
|
903 apply(erule Prf.cases) |
|
904 apply(simp_all)[7] |
|
905 apply(rule Prf.intros) |
|
906 apply metis |
|
907 apply(simp) |
|
908 apply(erule Prf.cases) |
|
909 apply(simp_all)[7] |
|
910 apply(auto split: if_splits)[1] |
|
911 apply(rule Prf.intros) |
|
912 apply(auto split: if_splits)[1] |
|
913 apply(erule Prf.cases) |
|
914 apply(simp_all)[7] |
|
915 apply(auto) |
|
916 apply(case_tac "char = c") |
|
917 apply(simp) |
|
918 apply(rule Prf.intros) |
|
919 apply(simp) |
|
920 apply(erule Prf.cases) |
|
921 apply(simp_all)[ |
|
922 |
|
923 |
|
924 lemma uu: |
|
925 assumes ih: "\<And>v c. \<lbrakk>head (flat v) = Some c\<rbrakk> \<Longrightarrow> \<turnstile> projval rexp c v : der c rexp" |
|
926 assumes "\<turnstile> Stars vs : STAR rexp" |
|
927 and "first (Stars (v#vs)) = Some c" |
|
928 shows "\<turnstile> projval rexp c v : der c rexp" |
|
929 using assms(2,3) |
|
930 apply(induct vs) |
|
931 apply(simp_all) |
|
932 apply(auto split: if_splits) |
|
933 apply (metis first head1 ih) |
|
934 apply (metis first head1 ih) |
|
935 |
|
936 apply(auto) |
|
937 |
|
938 lemma v5: |
|
939 assumes "\<turnstile> v : r" "head (flat v) = Some c" |
|
940 shows "\<turnstile> projval r c v : der c r" |
|
941 using assms |
|
942 apply(induct r arbitrary: v c rule: rexp.induct) |
|
943 apply(simp) |
|
944 apply(erule Prf.cases) |
|
945 apply(simp_all)[7] |
|
946 apply(erule Prf.cases) |
|
947 apply(simp_all)[7] |
|
948 apply(case_tac "char = c") |
|
949 apply(simp) |
|
950 apply(rule Prf.intros) |
|
951 apply(simp) |
|
952 apply(erule Prf.cases) |
|
953 apply(simp_all)[7] |
|
954 prefer 3 |
|
955 proof - |
|
956 fix rexp v c vs |
|
957 assume ih: "\<And>v c. \<lbrakk>\<turnstile> v : rexp; head (flat v) = Some c\<rbrakk> \<Longrightarrow> \<turnstile> projval rexp c v : der c rexp" |
|
958 assume a: "head (flat (Stars vs)) = Some c" |
|
959 assume b: "\<turnstile> Stars vs : STAR rexp" |
|
960 have c: "first (Stars vs) = Some c \<Longrightarrow> \<turnstile> (hd vs) : rexp \<Longrightarrow> \<turnstile> projval rexp c (hd vs) : der c rexp" |
|
961 using b |
|
962 apply(induct arbitrary: rule: Prf.induct) |
|
963 apply(simp_all) |
|
964 apply(case_tac "\<exists>c. first v = Some c") |
|
965 apply(auto)[1] |
|
966 apply(rule ih) |
|
967 apply(simp) |
|
968 apply (metis append_Nil2 first) |
|
969 apply(auto)[1] |
|
970 apply(simp) |
|
971 apply(auto split: if_splits)[1] |
|
972 apply (metis append_Nil2 first ih) |
|
973 apply(drule_tac x="v" in meta_spec) |
|
974 apply(simp) |
|
975 apply(rotate_tac 1) |
|
976 apply(erule Prf.cases) |
|
977 apply(simp_all)[7] |
|
978 apply(drule_tac x="v" in meta_spec) |
|
979 apply(simp) |
|
980 using a |
|
981 apply(rotate_tac 1) |
|
982 apply(erule Prf.cases) |
|
983 apply(simp_all)[7] |
|
984 |
|
985 |
|
986 apply (metis (full_types) Prf.cases Prf.simps a b flat.simps(6) head.simps(1) list.distinct(1) list.inject option.distinct(1) rexp.distinct(17) rexp.distinct(23) rexp.distinct(27) rexp.distinct(29) val.distinct(17) val.distinct(27) val.distinct(29) val.inject(5)) |
|
987 |
|
988 apply(auto)[1] |
|
989 apply(case_tac "\<exists>c. first a = Some c") |
|
990 apply(auto)[1] |
|
991 apply(rule ih) |
|
992 apply(simp) |
|
993 apply (metis append_Nil2 first ih) |
|
994 apply(auto)[1] |
|
995 apply(case_tac "\<exists>c. first a = Some c") |
|
996 apply(auto)[1] |
|
997 apply(rule ih) |
|
998 apply(simp) |
|
999 apply(auto)[1] |
|
1000 |
|
1001 apply(erule Prf.cases) |
|
1002 apply(simp_all)[7] |
|
1003 apply (metis append_Nil2 first) |
|
1004 apply(simp) |
|
1005 apply(simp add: ) |
|
1006 apply(simp add: flat) |
|
1007 apply(erule Prf.cases) |
|
1008 apply(simp_all)[7] |
|
1009 apply(rule Prf.intros) |
|
1010 *) |
|
1011 show "\<turnstile> projval (STAR rexp) c (Stars vs) : SEQ (der c rexp) (STAR rexp)" |
|
1012 using b a |
|
1013 apply - |
|
1014 apply(erule Prf.cases) |
|
1015 apply(simp_all)[7] |
|
1016 apply(drule head1) |
|
1017 apply(auto) |
|
1018 apply(rule Prf.intros) |
|
1019 apply(rule ih) |
|
1020 apply(simp_all)[3] |
|
1021 using k |
|
1022 apply - |
|
1023 apply(rule Prf.intros) |
|
1024 apply(auto) |
|
1025 |
|
1026 apply(simp) |
|
1027 apply(erule Prf.cases) |
|
1028 apply(simp_all)[7] |
|
1029 apply(rule Prf.intros) |
|
1030 defer |
|
1031 apply(rotate_tac 1) |
|
1032 apply(erule Prf.cases) |
|
1033 apply(simp_all)[7] |
|
1034 apply(drule_tac meta_mp) |
|
1035 apply(erule Prf.cases) |
|
1036 apply(simp_all)[7] |
|
1037 apply(rule ih) |
|
1038 apply(case_tac vs) |
|
1039 apply(simp) |
|
1040 apply(simp) |
|
1041 apply(rotate_tac 3) |
|
1042 apply(erule Prf.cases) |
|
1043 apply(simp_all)[7] |
|
1044 apply(auto)[1] |
|
1045 apply (metis Prf.intros(1) Prf.intros(3)) |
|
1046 apply(simp) |
|
1047 |
|
1048 apply(drule head1) |
|
1049 apply(auto)[1] |
|
1050 apply (metis Prf.intros(3)) |
|
1051 |
|
1052 |
|
1053 apply (metis Prf.intros) |
|
1054 apply(case_tac "nullable r1") |
|
1055 apply(simp) |
|
1056 apply(erule Prf.cases) |
|
1057 apply(simp_all)[7] |
|
1058 apply(auto)[1] |
|
1059 apply (metis Prf.intros(5)) |
|
1060 apply (metis Prf.intros(3) Prf.intros(4) head1) |
|
1061 apply(simp) |
|
1062 apply(erule Prf.cases) |
|
1063 apply(simp_all)[7] |
|
1064 apply(auto)[1] |
|
1065 apply (metis nullable_correctness v1) |
|
1066 apply(drule head1) |
|
1067 apply(auto)[1] |
|
1068 apply (metis Prf.intros(3)) |
|
1069 apply(simp) |
|
1070 apply(erule Prf.cases) |
|
1071 apply(simp_all)[7] |
|
1072 apply(auto)[1] |
|
1073 apply(drule head1) |
|
1074 apply(auto)[1] |
|
1075 apply(rule Prf.intros) |
|
1076 apply(auto) |
|
1077 apply(rule Prf.intros) |
|
1078 apply(auto) |
|
1079 apply(rotate_tac 2) |
|
1080 apply(erule Prf.cases) |
|
1081 apply(simp_all)[7] |
|
1082 apply(auto) |
|
1083 apply(drule head1) |
|
1084 apply(auto) |
|
1085 apply(rule Prf.intros) |
|
1086 apply(auto) |
|
1087 apply(rule Prf.intros) |
|
1088 apply(auto) |
|
1089 |
|
1090 defer |
|
1091 apply(erule Prf.cases) |
|
1092 apply(simp_all)[7] |
|
1093 apply(auto)[1] |
|
1094 apply(rule Prf.intros) |
|
1095 apply(auto) |
|
1096 apply(drule head1) |
|
1097 apply(auto)[1] |
|
1098 defer |
|
1099 apply(rotate_tac 3) |
|
1100 apply(erule Prf.cases) |
|
1101 apply(simp_all)[7] |
|
1102 apply(auto) |
|
1103 apply(drule head1) |
|
1104 apply(auto)[1] |
|
1105 |
|
1106 apply(simp) |
|
1107 apply(rule Prf.intros) |
|
1108 apply(auto) |
|
1109 apply(drule_tac x="v" in meta_spec) |
|
1110 apply(simp) |
|
1111 apply(erule Prf.cases) |
|
1112 apply(simp_all)[7] |
|
1113 apply(auto)[1] |
|
1114 apply(drule head1) |
|
1115 apply(auto)[1] |
|
1116 apply(rule Prf.intros) |
|
1117 apply(auto) |
|
1118 apply(drule meta_mp) |
|
1119 apply(rule Prf.intros) |
|
1120 apply(auto) |
|
1121 |
|
1122 apply(simp) |
|
1123 apply (metis Prf.intros(3) head1) |
|
1124 |
|
1125 defer |
|
1126 apply(simp) |
|
1127 apply(drule_tac head1) |
|
1128 apply(auto)[1] |
|
1129 apply(rule Prf.intros) |
|
1130 apply(rule Prf.intros) |
|
1131 apply(simp) |
|
1132 apply(simp) |
|
1133 apply(rule Prf.intros) |
|
1134 apply(simp) |
|
1135 apply(simp) |
|
1136 apply(rule Prf.intros) |
|
1137 apply(simp) |
|
1138 apply (metis nullable_correctness v1) |
|
1139 apply(simp) |
|
1140 apply(rule Prf.intros) |
|
1141 apply(simp) |
|
1142 apply(simp) |
|
1143 apply(rule Prf.intros) |
|
1144 apply(simp) |
|
1145 apply(simp) |
|
1146 apply(simp) |
|
1147 apply(rule Prf.intros) |
|
1148 apply(drule_tac head1) |
|
1149 apply(auto)[1] |
|
1150 apply (metis Prf.intros(3)) |
|
1151 apply(rotate_tac 2) |
|
1152 apply(erule Prf.cases) |
|
1153 apply(simp_all)[7] |
|
1154 apply(auto)[1] |
|
1155 apply(rule Prf.intros) |
|
1156 defer |
|
1157 apply(drule_tac x="c" in meta_spec) |
|
1158 apply(simp) |
|
1159 apply(rotate_tac 6) |
|
1160 apply(erule Prf.cases) |
|
1161 apply(simp_all)[7] |
|
1162 apply(auto)[1] |
|
1163 apply(rule Prf.intros) |
|
1164 apply(auto)[2] |
|
1165 apply(drule v1) |
|
1166 apply(simp) |
|
1167 apply(rule Prf.intros) |
|
1168 apply(simp add: nullable_correctness[symmetric]) |
|
1169 apply(rotate_tac 1) |
|
1170 apply(erule Prf.cases) |
|
1171 apply(simp_all)[7] |
|
1172 apply(auto)[1] |
|
1173 apply(drule head1) |
|
1174 apply(auto)[1] |
|
1175 apply(rule Prf.intros) |
|
1176 apply(simp) |
|
1177 apply(simp) |
|
1178 apply(simp) |
|
1179 |
|
1180 lemma inj_proj_id: |
|
1181 assumes "\<turnstile> v : r" "head (flat v) = Some c" |
|
1182 shows "injval r c (projval r c v) = v" |
|
1183 using assms |
|
1184 apply(induct arbitrary: c rule: Prf.induct) |
|
1185 apply(simp) |
|
1186 apply(simp) |
|
1187 apply(drule head1) |
|
1188 apply(auto)[1] |
|
1189 apply(rotate_tac 2) |
|
1190 apply(erule Prf.cases) |
|
1191 apply(simp_all)[7] |
|
1192 apply(auto)[1] |
|
1193 apply(drule head1) |
|
1194 apply(auto)[1] |
|
1195 apply(simp) |
|
1196 apply(erule Prf.cases) |
|
1197 apply(simp_all)[7] |
|
1198 apply(simp) |
|
1199 apply(case_tac "ca = c'") |
|
1200 apply(simp) |
|
1201 apply(erule Prf.cases) |
|
1202 apply(simp_all)[7] |
|
1203 apply(simp) |
|
1204 apply(erule Prf.cases) |
|
1205 apply(simp_all)[7] |
|
1206 defer |
|
1207 apply(simp) |
|
1208 apply(case_tac "nullable r1") |
|
1209 apply(simp) |
|
1210 apply(erule Prf.cases) |
|
1211 apply(simp_all)[7] |
|
1212 apply(auto)[1] |
|
1213 apply(erule Prf.cases) |
|
1214 apply(simp_all)[7] |
|
1215 apply(auto)[1] |
|
1216 apply(rotate_tac 2) |
|
1217 apply(erule Prf.cases) |
|
1218 apply(simp_all)[7] |
|
1219 apply(simp) |
|
1220 apply(case_tac "nullable rexp1") |
|
1221 apply(simp) |
|
1222 apply(erule Prf.cases) |
|
1223 apply(simp_all)[7] |
|
1224 apply(auto)[1] |
|
1225 apply(erule Prf.cases) |
|
1226 apply(simp_all)[7] |
|
1227 apply(auto)[1] |
|
1228 apply(simp add: v4) |
|
1229 apply(auto)[1] |
|
1230 apply(simp add: v2a) |
|
1231 apply(simp only: der.simps) |
|
1232 apply(simp) |
|
1233 apply(erule Prf.cases) |
|
1234 apply(simp_all)[7] |
|
1235 apply(auto)[1] |
|
1236 apply(simp add: v4) |
|
1237 done |
|
1238 |
|
1239 |
|
1240 |
|
1241 lemma POSIX_I: |
|
1242 assumes "\<turnstile> v : r" "\<And>v'. \<turnstile> v' : r \<Longrightarrow> flat v = flat v' \<Longrightarrow> v \<succeq>r v'" |
|
1243 shows "POSIX v r" |
|
1244 using assms |
|
1245 unfolding POSIX_def |
|
1246 apply(auto) |
|
1247 done |
|
1248 |
|
1249 lemma DISJ: |
|
1250 "(\<not> A \<Longrightarrow> B) \<Longrightarrow> A \<or> B" |
|
1251 by metis |
|
1252 |
|
1253 lemma DISJ2: |
|
1254 "\<not>(A \<and> B) \<longleftrightarrow> \<not>A \<or> \<not>B" |
|
1255 by metis |
|
1256 |
|
1257 lemma APP: "xs @ [] = xs" by simp |
|
1258 |
|
1259 lemma v5: |
|
1260 assumes "POSIX v (der c r)" |
|
1261 shows "POSIX (injval r c v) r" |
|
1262 using assms |
|
1263 apply(induct arbitrary: v rule: der.induct) |
|
1264 apply(simp) |
|
1265 apply(auto simp add: POSIX_def)[1] |
|
1266 apply(erule Prf.cases) |
|
1267 apply(simp_all)[7] |
|
1268 apply(erule Prf.cases) |
|
1269 apply(simp_all)[7] |
|
1270 apply(auto simp add: POSIX_def)[1] |
|
1271 apply(erule Prf.cases) |
|
1272 apply(simp_all)[7] |
|
1273 apply(erule Prf.cases) |
|
1274 apply(simp_all)[7] |
|
1275 apply(case_tac "c = c'") |
|
1276 apply(auto simp add: POSIX_def)[1] |
|
1277 apply(erule Prf.cases) |
|
1278 apply(simp_all)[7] |
|
1279 apply(rule Prf.intros) |
|
1280 apply(erule Prf.cases) |
|
1281 apply(simp_all)[7] |
|
1282 apply(simp add: ValOrd_eq_def) |
|
1283 apply(erule Prf.cases) |
|
1284 apply(simp_all)[7] |
|
1285 apply(simp) |
|
1286 apply(auto simp add: POSIX_def)[1] |
|
1287 apply(erule Prf.cases) |
|
1288 apply(simp_all)[7] |
|
1289 apply(erule Prf.cases) |
|
1290 apply(simp_all)[7] |
|
1291 prefer 3 |
|
1292 apply(simp) |
|
1293 apply(frule POSIX_E1) |
|
1294 apply(erule Prf.cases) |
|
1295 apply(simp_all)[7] |
|
1296 apply(auto)[1] |
|
1297 apply(drule_tac x="v1" in meta_spec) |
|
1298 apply(drule meta_mp) |
|
1299 apply(rule POSIX_I) |
|
1300 apply(simp) |
|
1301 apply(simp add: POSIX_def) |
|
1302 apply(auto)[1] |
|
1303 apply(drule_tac x="Seq v' v2" in spec) |
|
1304 apply(simp) |
|
1305 apply(drule mp) |
|
1306 apply (metis Prf.intros(3)) |
|
1307 apply(simp add: ValOrd_eq_def) |
|
1308 apply(erule disjE) |
|
1309 apply(simp) |
|
1310 apply(erule ValOrd.cases) |
|
1311 apply(simp_all)[10] |
|
1312 apply(subgoal_tac "\<exists>vs2. v2 = Stars vs2") |
|
1313 prefer 2 |
|
1314 apply(rotate_tac 2) |
|
1315 apply(erule Prf.cases) |
|
1316 apply(auto)[7] |
|
1317 apply(erule exE) |
|
1318 apply(clarify) |
|
1319 apply(simp only: injval.simps) |
|
1320 apply(case_tac "POSIX (Stars (injval r c v1 # vs2)) (STAR r)") |
|
1321 apply(simp) |
|
1322 apply(subgoal_tac "\<exists>v'' vs''. Stars (v''#vs'') \<succ>(STAR r) Stars (injval r c v1 # vs2)") |
|
1323 apply(erule exE)+ |
|
1324 apply(erule ValOrd.cases) |
|
1325 apply(simp_all)[8] |
|
1326 apply(auto)[1] |
|
1327 apply(subst (asm) (2) POSIX_def) |
|
1328 |
|
1329 |
|
1330 prefer 2 |
|
1331 apply(subst (asm) (3) POSIX_def) |
|
1332 apply(simp) |
|
1333 apply(drule mp) |
|
1334 apply (metis Prf.intros(2) v3) |
|
1335 apply(erule exE) |
|
1336 apply(auto)[1] |
|
1337 |
|
1338 apply |
|
1339 apply(subgoal_tac "\<turnstile> Stars (injval r c v1 # vs2) : STAR r") |
|
1340 apply(simp) |
|
1341 apply(case_tac "flat () = []") |
|
1342 |
|
1343 apply(rule POSIX_I) |
|
1344 apply (metis POSIX_E1 der.simps(6) v3) |
|
1345 apply(rotate_tac 2) |
|
1346 apply(erule Prf.cases) |
|
1347 defer |
|
1348 defer |
|
1349 apply(simp_all)[5] |
|
1350 prefer 4 |
|
1351 apply(clarify) |
|
1352 apply(simp only: v4 flat.simps injval.simps) |
|
1353 prefer 4 |
|
1354 apply(clarify) |
|
1355 apply(simp only: v4 APP flat.simps injval.simps) |
|
1356 prefer 2 |
|
1357 apply(erule Prf.cases) |
|
1358 apply(simp_all)[7] |
|
1359 apply(clarify) |
|
1360 |
|
1361 |
|
1362 apply(simp add: ValOrd_eq_def) |
|
1363 apply(subst (asm) POSIX_def) |
|
1364 apply(erule conjE) |
|
1365 apply(drule_tac x="va" in spec) |
|
1366 apply(simp) |
|
1367 apply(simp add: v4) |
|
1368 apply(simp add: ValOrd_eq_def) |
|
1369 apply(simp) |
|
1370 apply(rule disjI2) |
|
1371 apply(rule ValOrd.intros) |
|
1372 apply(rotate_tac 2) |
|
1373 apply(subst (asm) POSIX_def) |
|
1374 apply(simp) |
|
1375 apply(auto)[1] |
|
1376 apply(drule_tac x="v" in spec) |
|
1377 apply(simp) |
|
1378 apply(drule mp) |
|
1379 prefer 2 |
|
1380 apply(simp add: ValOrd_eq_def) |
|
1381 apply(auto)[1] |
|
1382 |
|
1383 apply(case_tac "injval rb c v1 = v \<and> [] = vs") |
|
1384 apply(simp) |
|
1385 apply(simp only: DISJ2) |
|
1386 apply(rule disjI2) |
|
1387 apply(erule disjE) |
|
1388 |
|
1389 |
|
1390 apply(auto)[1] |
|
1391 apply (metis list.distinct(1) v4) |
|
1392 apply(auto)[1] |
|
1393 apply(simp add: ValOrd_eq_def) |
|
1394 apply(rule DISJ) |
|
1395 apply(simp only: DISJ2) |
|
1396 apply(erule disjE) |
|
1397 apply(rule ValOrd.intros) |
|
1398 apply(subst (asm) POSIX_def) |
|
1399 apply(auto)[1] |
|
1400 |
|
1401 apply (metis list.distinct(1) v4) |
|
1402 apply(subst (asm) POSIX_def) |
|
1403 apply(auto)[1] |
|
1404 apply(erule Prf.cases) |
|
1405 apply(simp_all)[7] |
|
1406 apply(rotate_tac 3) |
|
1407 apply(erule Prf.cases) |
|
1408 apply(simp_all)[7] |
|
1409 apply(auto)[1] |
|
1410 apply (metis list.distinct(1) v4) |
|
1411 apply (metis list.distinct(1) v4) |
|
1412 apply(clarify) |
|
1413 apply(rotate_tac 3) |
|
1414 apply(erule Prf.cases) |
|
1415 apply(simp_all)[7] |
|
1416 prefer 2 |
|
1417 apply(clarify) |
|
1418 apply(simp add: ValOrd_eq_def) |
|
1419 apply(drule_tac x="Stars (v#vs)" in spec) |
|
1420 apply(drule mp) |
|
1421 apply(auto)[1] |
|
1422 |
|
1423 apply(simp add: ValOrd_eq_def) |
|
1424 |
|
1425 apply (metis POSIX_E1 der.simps(6) list.distinct(1) v4) |
|
1426 apply(rotate_tac 3) |
|
1427 apply(erule Prf.cases) |
|
1428 apply(simp_all)[7] |
|
1429 |
|
1430 apply(simp) |
|
1431 apply(case_tac v2) |
|
1432 apply(simp) |
|
1433 apply(simp (no_asm) POSIX_def) |
|
1434 apply(auto)[1] |
|
1435 apply(auto)[1] |
|
1436 |
|
1437 |
|
1438 apply (metis POSIX_E der.simps(6) v3) |
|
1439 |
|
1440 apply(rule Prf.intros) |
|
1441 apply(drule_tac x="v1" in meta_spec) |
|
1442 apply(drule meta_mp) |
|
1443 prefer 2 |
|
1444 |
|
1445 apply(subgoal_tac "POSIX v1 (der c r)") |
|
1446 prefer 2 |
|
1447 apply(simp add: POSIX_def) |
|
1448 apply(auto)[1] |
|
1449 apply(simp add: ValOrd_eq_def) |
|
1450 apply(auto)[1] |
|
1451 |
|
1452 |
|
1453 lemma v5: |
|
1454 assumes "\<turnstile> v : der c r" "POSIX v (der c r)" |
|
1455 shows "POSIX (injval r c v) r" |
|
1456 using assms |
|
1457 apply(induct arbitrary: v rule: der.induct) |
|
1458 apply(simp) |
|
1459 apply(erule Prf.cases) |
|
1460 apply(simp_all)[7] |
|
1461 apply(simp) |
|
1462 apply(erule Prf.cases) |
|
1463 apply(simp_all)[7] |
|
1464 apply(simp) |
|
1465 apply(case_tac "c = c'") |
|
1466 apply(simp) |
|
1467 apply(erule Prf.cases) |
|
1468 apply(simp_all)[7] |
|
1469 apply(simp add: POSIX_def) |
|
1470 apply(auto)[1] |
|
1471 apply(rule Prf.intros) |
|
1472 apply(erule Prf.cases) |
|
1473 apply(simp_all)[7] |
|
1474 apply(simp add: ValOrd_eq_def) |
|
1475 apply(erule Prf.cases) |
|
1476 apply(simp_all)[7] |
|
1477 apply(simp) |
|
1478 apply(erule Prf.cases) |
|
1479 apply(simp_all)[7] |
|
1480 prefer 3 |
|
1481 apply(simp) |
|
1482 apply(erule Prf.cases) |
|
1483 apply(simp_all)[7] |
|
1484 apply(auto)[1] |
|
1485 apply(case_tac "flat (Seq v1 v2) \<noteq> []") |
|
1486 apply(subgoal_tac "POSIX v1 (der c r)") |
|
1487 prefer 2 |
|
1488 apply(simp add: POSIX_def) |
|
1489 apply(auto)[1] |
|
1490 |
|
1491 |
|
1492 apply(drule_tac x="v1" in meta_spec) |
|
1493 apply(simp) |
|
1494 apply(simp (no_asm) add: POSIX_def) |
|
1495 apply(auto)[1] |
|
1496 apply(rule v3) |
|
1497 apply (metis Prf.intros(3) der.simps(6)) |
|
1498 apply(rotate_tac 1) |
|
1499 apply(erule Prf.cases) |
|
1500 apply(simp_all)[7] |
|
1501 apply(simp add: ValOrd_eq_def) |
|
1502 apply(rule disjI2) |
|
1503 apply(rotate_tac 1) |
|
1504 apply(erule Prf.cases) |
|
1505 apply(simp_all)[7] |
|
1506 apply(rule ValOrd.intros) |
|
1507 apply(simp) |
|
1508 apply (metis list.distinct(1) v4) |
|
1509 apply(rule ValOrd.intros) |
|
1510 apply(simp add: POSIX_def) |
|
1511 apply(auto)[1] |
|
1512 apply(rotate_tac 3) |
|
1513 apply(erule Prf.cases) |
|
1514 apply(simp_all)[7] |
|
1515 apply(simp add: ValOrd_eq_def) |
|
1516 apply(drule_tac x="v" in spec) |
|
1517 apply(simp) |
|
1518 apply(auto)[1] |
|
1519 apply(simp) |
|
1520 |
|
1521 apply(simp add: POSIX_def) |
|
1522 apply(auto)[1] |
|
1523 apply( |
|
1524 |
|
1525 apply(rotate_tac 1) |
|
1526 apply(erule Prf.cases) |
|
1527 apply(simp_all)[7] |
|
1528 apply (metis list.distinct(1) v4) |
|
1529 apply(rotate_tac 8) |
|
1530 apply(erule Prf.cases) |
|
1531 apply(simp_all)[7] |
|
1532 apply (metis POSIX_def ValOrd.intros(9) ValOrd_eq_def) |
|
1533 apply(simp add: ValOrd_eq_def) |
|
1534 apply(simp) |
|
1535 |
|
1536 apply(simp add: ValOrd_eq_def) |
|
1537 apply(simp add: POSIX_def) |
|
1538 apply(auto)[1] |
|
1539 |
|
1540 |
|
1541 apply(simp) |
|
1542 apply(simp add: ValOrd_eq_def) |
|
1543 apply(simp add: POSIX_def) |
|
1544 apply(erule conjE)+ |
|
1545 apply(drule_tac x="Seq v1 v2" in spec) |
|
1546 apply(simp) |
|
1547 |
|
1548 |
|
1549 |
|
1550 apply(rotate_tac 2) |
|
1551 apply(erule Prf.cases) |
|
1552 apply(simp_all)[7] |
|
1553 apply(auto)[1] |
|
1554 apply(simp add: POSIX_def) |
|
1555 apply(auto)[1] |
|
1556 apply(rule Prf.intros) |
|
1557 apply(rule v3) |
|
1558 apply(simp) |
|
1559 apply(rotate_tac 5) |
|
1560 apply(erule Prf.cases) |
|
1561 apply(simp_all)[7] |
|
1562 apply(auto)[1] |
|
1563 apply(rotate_tac 4) |
|
1564 apply(erule Prf.cases) |
|
1565 apply(simp_all)[7] |
|
1566 apply(auto)[1] |
|
1567 apply(simp add: ValOrd_eq_def) |
|
1568 |
|
1569 apply(simp) |
|
1570 |
|
1571 |
|
1572 prefer 2 |
|
1573 apply(auto)[1] |
|
1574 apply(subgoal_tac "POSIX v2 (der c r2)") |
|
1575 apply(rotate_tac 1) |
|
1576 apply(drule_tac x="v2" in meta_spec) |
|
1577 apply(simp) |
|
1578 apply(subgoal_tac "\<turnstile> Right (injval r2 c v2) : (ALT r1 r2)") |
|
1579 prefer 2 |
|
1580 apply (metis Prf.intros(5) v3) |
|
1581 apply(simp (no_asm) add: POSIX_def) |
|
1582 apply(auto)[1] |
|
1583 apply(rotate_tac 6) |
|
1584 apply(erule Prf.cases) |
|
1585 apply(simp_all)[7] |
|
1586 prefer 2 |
|
1587 apply(auto)[1] |
|
1588 apply(simp add: ValOrd_eq_def) |
|
1589 apply (metis POSIX_def ValOrd.intros(5) ValOrd_eq_def) |
|
1590 apply(auto)[1] |
|
1591 apply(simp add: ValOrd_eq_def) |
|
1592 |
|
1593 |
|
1594 section {* Correctness Proof of the Matcher *} |
|
1595 |
|
1596 |
|
1597 section {* Left-Quotient of a Set *} |
|
1598 |
|
1599 fun |
|
1600 zeroable :: "rexp \<Rightarrow> bool" |
|
1601 where |
|
1602 "zeroable (NULL) = True" |
|
1603 | "zeroable (EMPTY) = False" |
|
1604 | "zeroable (CHAR c) = False" |
|
1605 | "zeroable (ALT r1 r2) = (zeroable r1 \<and> zeroable r2)" |
|
1606 | "zeroable (SEQ r1 r2) = (zeroable r1 \<or> zeroable r2)" |
|
1607 | "zeroable (STAR r) = False" |
|
1608 |
|
1609 |
|
1610 lemma zeroable_correctness: |
|
1611 shows "zeroable r \<longleftrightarrow> (L r = {})" |
|
1612 apply(induct r) |
|
1613 apply(auto simp add: Seq_def)[6] |
|
1614 done |
|
1615 |
|
1616 section {* Left-Quotient of a Set *} |
|
1617 |
|
1618 definition |
|
1619 Der :: "char \<Rightarrow> string set \<Rightarrow> string set" |
|
1620 where |
|
1621 "Der c A \<equiv> {s. [c] @ s \<in> A}" |
|
1622 |
|
1623 lemma Der_null [simp]: |
|
1624 shows "Der c {} = {}" |
|
1625 unfolding Der_def |
|
1626 by auto |
|
1627 |
|
1628 lemma Der_empty [simp]: |
|
1629 shows "Der c {[]} = {}" |
|
1630 unfolding Der_def |
|
1631 by auto |
|
1632 |
|
1633 lemma Der_char [simp]: |
|
1634 shows "Der c {[d]} = (if c = d then {[]} else {})" |
|
1635 unfolding Der_def |
|
1636 by auto |
|
1637 |
|
1638 lemma Der_union [simp]: |
|
1639 shows "Der c (A \<union> B) = Der c A \<union> Der c B" |
|
1640 unfolding Der_def |
|
1641 by auto |
|
1642 |
|
1643 lemma Der_seq [simp]: |
|
1644 shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})" |
|
1645 unfolding Der_def Seq_def |
|
1646 by (auto simp add: Cons_eq_append_conv) |
|
1647 |
|
1648 lemma Der_star [simp]: |
|
1649 shows "Der c (A\<star>) = (Der c A) ;; A\<star>" |
|
1650 proof - |
|
1651 have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)" |
|
1652 by (simp only: star_cases[symmetric]) |
|
1653 also have "... = Der c (A ;; A\<star>)" |
|
1654 by (simp only: Der_union Der_empty) (simp) |
|
1655 also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})" |
|
1656 by simp |
|
1657 also have "... = (Der c A) ;; A\<star>" |
|
1658 unfolding Seq_def Der_def |
|
1659 by (auto dest: star_decomp) |
|
1660 finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" . |
|
1661 qed |
|
1662 |
|
1663 |
|
1664 lemma der_correctness: |
|
1665 shows "L (der c r) = Der c (L r)" |
|
1666 by (induct r) |
|
1667 (simp_all add: nullable_correctness) |
|
1668 |
|
1669 lemma matcher_correctness: |
|
1670 shows "matcher r s \<longleftrightarrow> s \<in> L r" |
|
1671 by (induct s arbitrary: r) |
|
1672 (simp_all add: nullable_correctness der_correctness Der_def) |
|
1673 |
|
1674 section {* Examples *} |
|
1675 |
|
1676 definition |
|
1677 "CHRA \<equiv> CHAR (CHR ''a'')" |
|
1678 |
|
1679 definition |
|
1680 "ALT1 \<equiv> ALT CHRA EMPTY" |
|
1681 |
|
1682 definition |
|
1683 "SEQ3 \<equiv> SEQ (SEQ ALT1 ALT1) ALT1" |
|
1684 |
|
1685 value "matcher SEQ3 ''aaa''" |
|
1686 |
|
1687 value "matcher NULL []" |
|
1688 value "matcher (CHAR (CHR ''a'')) [CHR ''a'']" |
|
1689 value "matcher (CHAR a) [a,a]" |
|
1690 value "matcher (STAR (CHAR a)) []" |
|
1691 value "matcher (STAR (CHAR a)) [a,a]" |
|
1692 value "matcher (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbbbc''" |
|
1693 value "matcher (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbcbbc''" |
|
1694 |
|
1695 section {* Incorrect Matcher - fun-definition rejected *} |
|
1696 |
|
1697 fun |
|
1698 match :: "rexp list \<Rightarrow> string \<Rightarrow> bool" |
|
1699 where |
|
1700 "match [] [] = True" |
|
1701 | "match [] (c # s) = False" |
|
1702 | "match (NULL # rs) s = False" |
|
1703 | "match (EMPTY # rs) s = match rs s" |
|
1704 | "match (CHAR c # rs) [] = False" |
|
1705 | "match (CHAR c # rs) (d # s) = (if c = d then match rs s else False)" |
|
1706 | "match (ALT r1 r2 # rs) s = (match (r1 # rs) s \<or> match (r2 # rs) s)" |
|
1707 | "match (SEQ r1 r2 # rs) s = match (r1 # r2 # rs) s" |
|
1708 | "match (STAR r # rs) s = (match rs s \<or> match (r # (STAR r) # rs) s)" |
|
1709 |
|
1710 |
|
1711 end |