104 fun intern :: "rexp \<Rightarrow> arexp" where |
104 fun intern :: "rexp \<Rightarrow> arexp" where |
105 "intern ZERO = AZERO" |
105 "intern ZERO = AZERO" |
106 | "intern ONE = AONE []" |
106 | "intern ONE = AONE []" |
107 | "intern (CHAR c) = ACHAR [] c" |
107 | "intern (CHAR c) = ACHAR [] c" |
108 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) |
108 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) |
109 (fuse [S] (intern r2))" |
109 (fuse [S] (intern r2))" |
110 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)" |
110 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)" |
111 | "intern (STAR r) = ASTAR [] (intern r)" |
111 | "intern (STAR r) = ASTAR [] (intern r)" |
112 |
112 |
113 |
113 |
114 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where |
114 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where |
315 apply(subst bnullable_correctness[symmetric]) |
315 apply(subst bnullable_correctness[symmetric]) |
316 apply(simp) |
316 apply(simp) |
317 done |
317 done |
318 qed |
318 qed |
319 |
319 |
|
320 |
|
321 lemma |
|
322 "[a, a, a, a] \<in> (STAR(STAR(CHAR(a)))) \<rightarrow> |
|
323 (Stars [(Stars [Char a, Char a, Char a, Char a])])" |
|
324 oops |
|
325 |
|
326 lemma |
|
327 "([a,a] @ []) \<in> (STAR(STAR(CHAR(a)))) \<rightarrow> |
|
328 (Stars [(Stars [Char a, Char a])])" |
|
329 apply(rule Posix.intros) |
|
330 defer |
|
331 apply (simp add: Posix_STAR2) |
|
332 apply(simp) |
|
333 apply(auto)[1] |
|
334 apply(rule_tac s="[a] @ [a]" in subst) |
|
335 apply(simp) |
|
336 apply(rule Posix_STAR1) |
|
337 apply(rule Posix_CHAR) |
|
338 apply(rule_tac s="[a] @ []" in subst) |
|
339 apply(simp) |
|
340 apply(rule Posix_STAR1) |
|
341 apply(rule Posix_CHAR) |
|
342 apply(rule Posix_STAR2) |
|
343 apply(simp) |
|
344 apply(auto) |
|
345 done |
|
346 |
|
347 |
|
348 lemma "lexer (STAR(STAR(CHAR(a)))) [a, a] = XXX" |
|
349 apply(simp) |
|
350 oops |
|
351 |
|
352 |
|
353 |
|
354 |
|
355 |
320 fun simp where |
356 fun simp where |
321 "simp (AALT bs a AZERO) = fuse bs (simp a)" |
357 "simp (AALT bs a AZERO) = fuse bs (simp a)" |
322 | "simp (AALT bs AZERO a) = fuse bs (simp a)" |
358 | "simp (AALT bs AZERO a) = fuse bs (simp a)" |
323 | "simp (ASEQ bs a AZERO) = AZERO" |
359 | "simp (ASEQ bs a AZERO) = AZERO" |
324 | "simp (ASEQ bs AZERO a) = AZERO" |
360 | "simp (ASEQ bs AZERO a) = AZERO" |
325 | "simp a = a" |
361 | "simp a = a" |
326 |
362 |
327 |
363 |
|
364 |
|
365 |
|
366 |
|
367 |
|
368 |
|
369 definition blexers where |
|
370 "blexer r s \<equiv> if bnullable (bders (intern r) s) then |
|
371 decode (bmkeps (bders (intern r) s)) r else None" |
|
372 |
328 unused_thms |
373 unused_thms |
329 |
374 |
|
375 |
|
376 |
|
377 |
330 end |
378 end |