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 

   356 fun simp where

   357   "simp (AALT bs a AZERO) = fuse bs (simp a)"

   358 | "simp (AALT bs AZERO a) = fuse bs (simp a)"

   359 | "simp (ASEQ bs a AZERO) = AZERO"

   360 | "simp (ASEQ bs AZERO a) = AZERO"

   361 | "simp a = a"

   362 

   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 

   373 unused_thms

   374 

   375 

   376