1 

     2 theory BitCoded2CT

     3   imports "Lexer" 

     4 begin

     5 

     6 section \<open>Bit-Encodings\<close>

     7 

     8 datatype bit = Z | S

     9 

    10 fun 

    11   code :: "val \<Rightarrow> bit list"

    12 where

    13   "code Void = []"

    14 | "code (Char c) = []"

    15 | "code (Left v) = Z # (code v)"

    16 | "code (Right v) = S # (code v)"

    17 | "code (Seq v1 v2) = (code v1) @ (code v2)"

    18 | "code (Stars []) = [S]"

    19 | "code (Stars (v # vs)) =  (Z # code v) @ code (Stars vs)"

    20 

    21 

    22 fun 

    23   Stars_add :: "val \<Rightarrow> val \<Rightarrow> val"

    24 where

    25   "Stars_add v (Stars vs) = Stars (v # vs)"

    26 | "Stars_add v _ = Stars [v]" 

    27 

    28 function

    29   decode' :: "bit list \<Rightarrow> rexp \<Rightarrow> (val * bit list)"

    30 where

    31   "decode' ds ZERO = (Void, [])"

    32 | "decode' ds ONE = (Void, ds)"

    33 | "decode' ds (CHAR d) = (Char d, ds)"

    34 | "decode' [] (ALT r1 r2) = (Void, [])"

    35 | "decode' (Z # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))"

    36 | "decode' (S # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))"

    37 | "decode' ds (SEQ r1 r2) = (let (v1, ds') = decode' ds r1 in

    38                              let (v2, ds'') = decode' ds' r2 in (Seq v1 v2, ds''))"

    39 | "decode' [] (STAR r) = (Void, [])"

    40 | "decode' (S # ds) (STAR r) = (Stars [], ds)"

    41 | "decode' (Z # ds) (STAR r) = (let (v, ds') = decode' ds r in

    42                                     let (vs, ds'') = decode' ds' (STAR r) 

    43                                     in (Stars_add v vs, ds''))"

    44 by pat_completeness auto

    45 

    46 lemma decode'_smaller:

    47   assumes "decode'_dom (ds, r)"

    48   shows "length (snd (decode' ds r)) \<le> length ds"

    49 using assms

    50 apply(induct ds r)

    51 apply(auto simp add: decode'.psimps split: prod.split)

    52 using dual_order.trans apply blast

    53 by (meson dual_order.trans le_SucI)

    54 

    55 termination "decode'"  

    56 apply(relation "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))") 

    57 apply(auto dest!: decode'_smaller)

    58 by (metis less_Suc_eq_le snd_conv)

    59 

    60 definition

    61   decode :: "bit list \<Rightarrow> rexp \<Rightarrow> val option"

    62 where

    63   "decode ds r \<equiv> (let (v, ds') = decode' ds r 

    64                   in (if ds' = [] then Some v else None))"

    65 

    66 lemma decode'_code_Stars:

    67   assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> (\<forall>x. decode' (code v @ x) r = (v, x)) \<and> flat v \<noteq> []" 

    68   shows "decode' (code (Stars vs) @ ds) (STAR r) = (Stars vs, ds)"

    69   using assms

    70   apply(induct vs)

    71   apply(auto)

    72   done

    73 

    74 lemma decode'_code:

    75   assumes "\<Turnstile> v : r"

    76   shows "decode' ((code v) @ ds) r = (v, ds)"

    77 using assms

    78   apply(induct v r arbitrary: ds) 

    79   apply(auto)

    80   using decode'_code_Stars by blast

    81 

    82 lemma decode_code:

    83   assumes "\<Turnstile> v : r"

    84   shows "decode (code v) r = Some v"

    85   using assms unfolding decode_def

    86   by (smt append_Nil2 decode'_code old.prod.case)

    87 

    88 

    89 section {* Annotated Regular Expressions *}

    90 

    91 datatype arexp = 

    92   AZERO

    93 | AONE "bit list"

    94 | ACHAR "bit list" char

    95 | ASEQ "bit list" arexp arexp

    96 | AALTs "bit list" "arexp list"

    97 | ASTAR "bit list" arexp

    98 

    99 abbreviation

   100   "AALT bs r1 r2 \<equiv> AALTs bs [r1, r2]"

   101 

   102 fun asize :: "arexp \<Rightarrow> nat" where

   103   "asize AZERO = 1"

   104 | "asize (AONE cs) = 1" 

   105 | "asize (ACHAR cs c) = 1"

   106 | "asize (AALTs cs rs) = Suc (sum_list (map asize rs))"

   107 | "asize (ASEQ cs r1 r2) = Suc (asize r1 + asize r2)"

   108 | "asize (ASTAR cs r) = Suc (asize r)"

   109 

   110 fun 

   111   erase :: "arexp \<Rightarrow> rexp"

   112 where

   113   "erase AZERO = ZERO"

   114 | "erase (AONE _) = ONE"

   115 | "erase (ACHAR _ c) = CHAR c"

   116 | "erase (AALTs _ []) = ZERO"

   117 | "erase (AALTs _ [r]) = (erase r)"

   118 | "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))"

   119 | "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)"

   120 | "erase (ASTAR _ r) = STAR (erase r)"

   121 

   122 lemma decode_code_erase:

   123   assumes "\<Turnstile> v : (erase  a)"

   124   shows "decode (code v) (erase a) = Some v"

   125   using assms

   126   by (simp add: decode_code) 

   127 

   128 

   129 fun nonalt :: "arexp \<Rightarrow> bool"

   130   where

   131   "nonalt (AALTs bs2 rs) = False"

   132 | "nonalt r = True"

   133 

   134 

   135 fun good :: "arexp \<Rightarrow> bool" where

   136   "good AZERO = False"

   137 | "good (AONE cs) = True" 

   138 | "good (ACHAR cs c) = True"

   139 | "good (AALTs cs []) = False"

   140 | "good (AALTs cs [r]) = False"

   141 | "good (AALTs cs (r1#r2#rs)) = (\<forall>r' \<in> set (r1#r2#rs). good r' \<and> nonalt r')"

   142 | "good (ASEQ _ AZERO _) = False"

   143 | "good (ASEQ _ (AONE _) _) = False"

   144 | "good (ASEQ _ _ AZERO) = False"

   145 | "good (ASEQ cs r1 r2) = (good r1 \<and> good r2)"

   146 | "good (ASTAR cs r) = True"

   147 

   148 

   149 

   150 

   151 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where

   152   "fuse bs AZERO = AZERO"

   153 | "fuse bs (AONE cs) = AONE (bs @ cs)" 

   154 | "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c"

   155 | "fuse bs (AALTs cs rs) = AALTs (bs @ cs) rs"

   156 | "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2"

   157 | "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r"

   158 

   159 lemma fuse_append:

   160   shows "fuse (bs1 @ bs2) r = fuse bs1 (fuse bs2 r)"

   161   apply(induct r)

   162   apply(auto)

   163   done

   164 

   165 

   166 fun intern :: "rexp \<Rightarrow> arexp" where

   167   "intern ZERO = AZERO"

   168 | "intern ONE = AONE []"

   169 | "intern (CHAR c) = ACHAR [] c"

   170 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) 

   171                                 (fuse [S]  (intern r2))"

   172 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)"

   173 | "intern (STAR r) = ASTAR [] (intern r)"

   174 

   175 

   176 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where

   177   "retrieve (AONE bs) Void = bs"

   178 | "retrieve (ACHAR bs c) (Char d) = bs"

   179 | "retrieve (AALTs bs [r]) v = bs @ retrieve r v" 

   180 | "retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v"

   181 | "retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v"

   182 | "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2"

   183 | "retrieve (ASTAR bs r) (Stars []) = bs @ [S]"

   184 | "retrieve (ASTAR bs r) (Stars (v#vs)) = 

   185      bs @ [Z] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)"

   186 

   187 

   188 

   189 fun

   190  bnullable :: "arexp \<Rightarrow> bool"

   191 where

   192   "bnullable (AZERO) = False"

   193 | "bnullable (AONE bs) = True"

   194 | "bnullable (ACHAR bs c) = False"

   195 | "bnullable (AALTs bs rs) = (\<exists>r \<in> set rs. bnullable r)"

   196 | "bnullable (ASEQ bs r1 r2) = (bnullable r1 \<and> bnullable r2)"

   197 | "bnullable (ASTAR bs r) = True"

   198 

   199 fun 

   200   bmkeps :: "arexp \<Rightarrow> bit list"

   201 where

   202   "bmkeps(AONE bs) = bs"

   203 | "bmkeps(ASEQ bs r1 r2) = bs @ (bmkeps r1) @ (bmkeps r2)"

   204 | "bmkeps(AALTs bs [r]) = bs @ (bmkeps r)"

   205 | "bmkeps(AALTs bs (r#rs)) = (if bnullable(r) then bs @ (bmkeps r) else (bmkeps (AALTs bs rs)))"

   206 | "bmkeps(ASTAR bs r) = bs @ [S]"

   207 

   208 

   209 fun

   210  bder :: "char \<Rightarrow> arexp \<Rightarrow> arexp"

   211 where

   212   "bder c (AZERO) = AZERO"

   213 | "bder c (AONE bs) = AZERO"

   214 | "bder c (ACHAR bs d) = (if c = d then AONE bs else AZERO)"

   215 | "bder c (AALTs bs rs) = AALTs bs (map (bder c) rs)"

   216 | "bder c (ASEQ bs r1 r2) = 

   217      (if bnullable r1

   218       then AALT bs (ASEQ [] (bder c r1) r2) (fuse (bmkeps r1) (bder c r2))

   219       else ASEQ bs (bder c r1) r2)"

   220 | "bder c (ASTAR bs r) = ASEQ bs (fuse [Z] (bder c r)) (ASTAR [] r)"

   221 

   222 

   223 fun 

   224   bders :: "arexp \<Rightarrow> string \<Rightarrow> arexp"

   225 where

   226   "bders r [] = r"

   227 | "bders r (c#s) = bders (bder c r) s"

   228 

   229 lemma bders_append:

   230   "bders r (s1 @ s2) = bders (bders r s1) s2"

   231   apply(induct s1 arbitrary: r s2)

   232   apply(simp_all)

   233   done

   234 

   235 lemma bnullable_correctness:

   236   shows "nullable (erase r) = bnullable r"

   237   apply(induct r rule: erase.induct)

   238   apply(simp_all)

   239   done

   240 

   241 lemma erase_fuse:

   242   shows "erase (fuse bs r) = erase r"

   243   apply(induct r rule: erase.induct)

   244   apply(simp_all)

   245   done

   246 

   247 lemma erase_intern [simp]:

   248   shows "erase (intern r) = r"

   249   apply(induct r)

   250   apply(simp_all add: erase_fuse)

   251   done

   252 

   253 lemma erase_bder [simp]:

   254   shows "erase (bder a r) = der a (erase r)"

   255   apply(induct r rule: erase.induct)

   256   apply(simp_all add: erase_fuse bnullable_correctness)

   257   done

   258 

   259 lemma erase_bders [simp]:

   260   shows "erase (bders r s) = ders s (erase r)"

   261   apply(induct s arbitrary: r )

   262   apply(simp_all)

   263   done

   264 

   265 lemma retrieve_encode_STARS:

   266   assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> code v = retrieve (intern r) v"

   267   shows "code (Stars vs) = retrieve (ASTAR [] (intern r)) (Stars vs)"

   268   using assms

   269   apply(induct vs)

   270   apply(simp_all)

   271   done

   272 

   273 lemma retrieve_fuse2:

   274   assumes "\<Turnstile> v : (erase r)"

   275   shows "retrieve (fuse bs r) v = bs @ retrieve r v"

   276   using assms

   277   apply(induct r arbitrary: v bs)

   278          apply(auto elim: Prf_elims)[4]

   279    defer

   280   using retrieve_encode_STARS

   281    apply(auto elim!: Prf_elims)[1]

   282    apply(case_tac vs)

   283     apply(simp)

   284    apply(simp)

   285   (* AALTs  case *)

   286   apply(simp)

   287   apply(case_tac x2a)

   288    apply(simp)

   289    apply(auto elim!: Prf_elims)[1]

   290   apply(simp)

   291    apply(case_tac list)

   292    apply(simp)

   293   apply(auto)

   294   apply(auto elim!: Prf_elims)[1]

   295   done

   296 

   297 lemma retrieve_fuse:

   298   assumes "\<Turnstile> v : r"

   299   shows "retrieve (fuse bs (intern r)) v = bs @ retrieve (intern r) v"

   300   using assms 

   301   by (simp_all add: retrieve_fuse2)

   302 

   303 

   304 lemma retrieve_code:

   305   assumes "\<Turnstile> v : r"

   306   shows "code v = retrieve (intern r) v"

   307   using assms

   308   apply(induct v r )

   309   apply(simp_all add: retrieve_fuse retrieve_encode_STARS)

   310   done

   311 

   312 lemma r:

   313   assumes "bnullable (AALTs bs (a # rs))"

   314   shows "bnullable a \<or> (\<not> bnullable a \<and> bnullable (AALTs bs rs))"

   315   using assms

   316   apply(induct rs)

   317    apply(auto)

   318   done

   319 

   320 lemma r0:

   321   assumes "bnullable a" 

   322   shows  "bmkeps (AALTs bs (a # rs)) = bs @ (bmkeps a)"

   323   using assms

   324   by (metis bmkeps.simps(3) bmkeps.simps(4) list.exhaust)

   325 

   326 lemma r1:

   327   assumes "\<not> bnullable a" "bnullable (AALTs bs rs)"

   328   shows  "bmkeps (AALTs bs (a # rs)) = bmkeps (AALTs bs rs)"

   329   using assms

   330   apply(induct rs)

   331    apply(auto)

   332   done

   333 

   334 lemma r2:

   335   assumes "x \<in> set rs" "bnullable x"

   336   shows "bnullable (AALTs bs rs)"

   337   using assms

   338   apply(induct rs)

   339    apply(auto)

   340   done

   341 

   342 lemma  r3:

   343   assumes "\<not> bnullable r" 

   344           " \<exists> x \<in> set rs. bnullable x"

   345   shows "retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs))) =

   346          retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs))))"

   347   using assms

   348   apply(induct rs arbitrary: r bs)

   349    apply(auto)[1]

   350   apply(auto)

   351   using bnullable_correctness apply blast

   352     apply(auto simp add: bnullable_correctness mkeps_nullable retrieve_fuse2)

   353    apply(subst retrieve_fuse2[symmetric])

   354   apply (smt bnullable.simps(4) bnullable_correctness erase.simps(5) erase.simps(6) insert_iff list.exhaust list.set(2) mkeps.simps(3) mkeps_nullable)

   355    apply(simp)

   356   apply(case_tac "bnullable a")

   357   apply (smt append_Nil2 bnullable.simps(4) bnullable_correctness erase.simps(5) erase.simps(6) fuse.simps(4) insert_iff list.exhaust list.set(2) mkeps.simps(3) mkeps_nullable retrieve_fuse2)

   358   apply(drule_tac x="a" in meta_spec)

   359   apply(drule_tac x="bs" in meta_spec)

   360   apply(drule meta_mp)

   361    apply(simp)

   362   apply(drule meta_mp)

   363    apply(auto)

   364   apply(subst retrieve_fuse2[symmetric])

   365   apply(case_tac rs)

   366     apply(simp)

   367    apply(auto)[1]

   368       apply (simp add: bnullable_correctness)

   369   apply (metis append_Nil2 bnullable_correctness erase_fuse fuse.simps(4) list.set_intros(1) mkeps.simps(3) mkeps_nullable nullable.simps(4) r2)

   370     apply (simp add: bnullable_correctness)

   371   apply (metis append_Nil2 bnullable_correctness erase.simps(6) erase_fuse fuse.simps(4) list.set_intros(2) mkeps.simps(3) mkeps_nullable r2)

   372   apply(simp)

   373   done

   374 

   375 

   376 lemma t: 

   377   assumes "\<forall>r \<in> set rs. nullable (erase r) \<longrightarrow> bmkeps r = retrieve r (mkeps (erase r))" 

   378           "nullable (erase (AALTs bs rs))"

   379   shows " bmkeps (AALTs bs rs) = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))"

   380   using assms

   381   apply(induct rs arbitrary: bs)

   382    apply(simp)

   383   apply(auto simp add: bnullable_correctness)

   384    apply(case_tac rs)

   385      apply(auto simp add: bnullable_correctness)[2]

   386    apply(subst r1)

   387      apply(simp)

   388     apply(rule r2)

   389      apply(assumption)

   390     apply(simp)

   391    apply(drule_tac x="bs" in meta_spec)

   392    apply(drule meta_mp)

   393     apply(auto)[1]

   394    prefer 2

   395   apply(case_tac "bnullable a")

   396     apply(subst r0)

   397      apply blast

   398     apply(subgoal_tac "nullable (erase a)")

   399   prefer 2

   400   using bnullable_correctness apply blast

   401   apply (metis (no_types, lifting) erase.simps(5) erase.simps(6) list.exhaust mkeps.simps(3) retrieve.simps(3) retrieve.simps(4))

   402   apply(subst r1)

   403      apply(simp)

   404   using r2 apply blast

   405   apply(drule_tac x="bs" in meta_spec)

   406    apply(drule meta_mp)

   407     apply(auto)[1]

   408    apply(simp)

   409   using r3 apply blast

   410   apply(auto)

   411   using r3 by blast

   412 

   413 lemma bmkeps_retrieve:

   414   assumes "nullable (erase r)"

   415   shows "bmkeps r = retrieve r (mkeps (erase r))"

   416   using assms

   417   apply(induct r)

   418          apply(simp)

   419         apply(simp)

   420        apply(simp)

   421     apply(simp)

   422    defer

   423    apply(simp)

   424   apply(rule t)

   425    apply(auto)

   426   done

   427 

   428 lemma bder_retrieve:

   429   assumes "\<Turnstile> v : der c (erase r)"

   430   shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)"

   431   using assms

   432   apply(induct r arbitrary: v rule: erase.induct)

   433          apply(simp)

   434          apply(erule Prf_elims)

   435         apply(simp)

   436         apply(erule Prf_elims) 

   437         apply(simp)

   438       apply(case_tac "c = ca")

   439        apply(simp)

   440        apply(erule Prf_elims)

   441        apply(simp)

   442       apply(simp)

   443        apply(erule Prf_elims)

   444   apply(simp)

   445       apply(erule Prf_elims)

   446      apply(simp)

   447     apply(simp)

   448   apply(rename_tac "r\<^sub>1" "r\<^sub>2" rs v)

   449     apply(erule Prf_elims)

   450      apply(simp)

   451     apply(simp)

   452     apply(case_tac rs)

   453      apply(simp)

   454     apply(simp)

   455   apply (smt Prf_elims(3) injval.simps(2) injval.simps(3) retrieve.simps(4) retrieve.simps(5) same_append_eq)

   456    apply(simp)

   457    apply(case_tac "nullable (erase r1)")

   458     apply(simp)

   459   apply(erule Prf_elims)

   460      apply(subgoal_tac "bnullable r1")

   461   prefer 2

   462   using bnullable_correctness apply blast

   463     apply(simp)

   464      apply(erule Prf_elims)

   465      apply(simp)

   466    apply(subgoal_tac "bnullable r1")

   467   prefer 2

   468   using bnullable_correctness apply blast

   469     apply(simp)

   470     apply(simp add: retrieve_fuse2)

   471     apply(simp add: bmkeps_retrieve)

   472    apply(simp)

   473    apply(erule Prf_elims)

   474    apply(simp)

   475   using bnullable_correctness apply blast

   476   apply(rename_tac bs r v)

   477   apply(simp)

   478   apply(erule Prf_elims)

   479      apply(clarify)

   480   apply(erule Prf_elims)

   481   apply(clarify)

   482   apply(subst injval.simps)

   483   apply(simp del: retrieve.simps)

   484   apply(subst retrieve.simps)

   485   apply(subst retrieve.simps)

   486   apply(simp)

   487   apply(simp add: retrieve_fuse2)

   488   done

   489   

   490 

   491 

   492 lemma MAIN_decode:

   493   assumes "\<Turnstile> v : ders s r"

   494   shows "Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r"

   495   using assms

   496 proof (induct s arbitrary: v rule: rev_induct)

   497   case Nil

   498   have "\<Turnstile> v : ders [] r" by fact

   499   then have "\<Turnstile> v : r" by simp

   500   then have "Some v = decode (retrieve (intern r) v) r"

   501     using decode_code retrieve_code by auto

   502   then show "Some (flex r id [] v) = decode (retrieve (bders (intern r) []) v) r"

   503     by simp

   504 next

   505   case (snoc c s v)

   506   have IH: "\<And>v. \<Turnstile> v : ders s r \<Longrightarrow> 

   507      Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" by fact

   508   have asm: "\<Turnstile> v : ders (s @ [c]) r" by fact

   509   then have asm2: "\<Turnstile> injval (ders s r) c v : ders s r" 

   510     by (simp add: Prf_injval ders_append)

   511   have "Some (flex r id (s @ [c]) v) = Some (flex r id s (injval (ders s r) c v))"

   512     by (simp add: flex_append)

   513   also have "... = decode (retrieve (bders (intern r) s) (injval (ders s r) c v)) r"

   514     using asm2 IH by simp

   515   also have "... = decode (retrieve (bder c (bders (intern r) s)) v) r"

   516     using asm by (simp_all add: bder_retrieve ders_append)

   517   finally show "Some (flex r id (s @ [c]) v) = 

   518                  decode (retrieve (bders (intern r) (s @ [c])) v) r" by (simp add: bders_append)

   519 qed

   520 

   521 

   522 definition blex where

   523  "blex a s \<equiv> if bnullable (bders a s) then Some (bmkeps (bders a s)) else None"

   524 

   525 

   526 

   527 definition blexer where

   528  "blexer r s \<equiv> if bnullable (bders (intern r) s) then 

   529                 decode (bmkeps (bders (intern r) s)) r else None"

   530 

   531 lemma blexer_correctness:

   532   shows "blexer r s = lexer r s"

   533 proof -

   534   { define bds where "bds \<equiv> bders (intern r) s"

   535     define ds  where "ds \<equiv> ders s r"

   536     assume asm: "nullable ds"

   537     have era: "erase bds = ds" 

   538       unfolding ds_def bds_def by simp

   539     have mke: "\<Turnstile> mkeps ds : ds"

   540       using asm by (simp add: mkeps_nullable)

   541     have "decode (bmkeps bds) r = decode (retrieve bds (mkeps ds)) r"

   542       using bmkeps_retrieve

   543       using asm era by (simp add: bmkeps_retrieve)

   544     also have "... =  Some (flex r id s (mkeps ds))"

   545       using mke by (simp_all add: MAIN_decode ds_def bds_def)

   546     finally have "decode (bmkeps bds) r = Some (flex r id s (mkeps ds))" 

   547       unfolding bds_def ds_def .

   548   }

   549   then show "blexer r s = lexer r s"

   550     unfolding blexer_def lexer_flex

   551     apply(subst bnullable_correctness[symmetric])

   552     apply(simp)

   553     done

   554 qed

   555 

   556 lemma asize0:

   557   shows "0 < asize r"

   558   apply(induct  r)

   559   apply(auto)

   560   done

   561 

   562 lemma asize_fuse:

   563   shows "asize (fuse bs r) = asize r"

   564   apply(induct r)

   565   apply(auto)

   566   done

   567 

   568 lemma bder_fuse:

   569   shows "bder c (fuse bs a) = fuse bs  (bder c a)"

   570   apply(induct a arbitrary: bs c)

   571   apply(simp_all)

   572   done

   573 

   574 lemma map_bder_fuse:

   575   shows "map (bder c \<circ> fuse bs1) as1 = map (fuse bs1) (map (bder c) as1)"

   576   apply(induct as1)

   577   apply(auto simp add: bder_fuse)

   578   done

   579 

   580 

   581 fun nonnested :: "arexp \<Rightarrow> bool"

   582   where

   583   "nonnested (AALTs bs2 []) = True"

   584 | "nonnested (AALTs bs2 ((AALTs bs1 rs1) # rs2)) = False"

   585 | "nonnested (AALTs bs2 (r # rs2)) = nonnested (AALTs bs2 rs2)"

   586 | "nonnested r = True"

   587 

   588 

   589 

   590 fun distinctBy :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> 'a list"

   591   where

   592   "distinctBy [] f acc = []"

   593 | "distinctBy (x#xs) f acc = 

   594      (if (f x) \<in> acc then distinctBy xs f acc 

   595       else x # (distinctBy xs f ({f x} \<union> acc)))"

   596 

   597 fun flts :: "arexp list \<Rightarrow> arexp list"

   598   where 

   599   "flts [] = []"

   600 | "flts (AZERO # rs) = flts rs"

   601 | "flts ((AALTs bs  rs1) # rs) = (map (fuse bs) rs1) @ flts rs"

   602 | "flts (r1 # rs) = r1 # flts rs"

   603 

   604 

   605 fun spill :: "arexp list \<Rightarrow> arexp list"

   606   where 

   607   "spill [] = []"

   608 | "spill ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ spill rs"

   609 | "spill (r1 # rs) = r1 # spill rs"

   610 

   611 lemma  spill_Cons:

   612   shows "spill (r # rs1) = spill [r] @ spill rs1"

   613   apply(induct r arbitrary: rs1)

   614    apply(auto)

   615   done

   616 

   617 lemma  spill_append:

   618   shows "spill (rs1 @ rs2) = spill rs1 @ spill rs2"

   619   apply(induct rs1 arbitrary: rs2)

   620    apply(auto)

   621   by (metis append.assoc spill_Cons)

   622 

   623 fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"

   624   where

   625   "bsimp_ASEQ _ AZERO _ = AZERO"

   626 | "bsimp_ASEQ _ _ AZERO = AZERO"

   627 | "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2"

   628 | "bsimp_ASEQ bs1 r1 r2 = ASEQ  bs1 r1 r2"

   629 

   630 

   631 fun bsimp_AALTs :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp"

   632   where

   633   "bsimp_AALTs _ [] = AZERO"

   634 | "bsimp_AALTs bs1 [r] = fuse bs1 r"

   635 | "bsimp_AALTs bs1 rs = AALTs bs1 rs"

   636 

   637 

   638 fun bsimp :: "arexp \<Rightarrow> arexp" 

   639   where

   640   "bsimp (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)"

   641 | "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (flts (map bsimp rs))"

   642 | "bsimp r = r"

   643 

   644 

   645 inductive contains2 :: "arexp \<Rightarrow> bit list \<Rightarrow> bool" ("_ >>2 _" [51, 50] 50)

   646   where

   647   "AONE bs >>2 bs"

   648 | "ACHAR bs c >>2 bs"

   649 | "\<lbrakk>a1 >>2 bs1; a2 >>2 bs2\<rbrakk> \<Longrightarrow> ASEQ bs a1 a2 >>2 bs @ bs1 @ bs2"

   650 | "r >>2 bs1 \<Longrightarrow> AALTs bs (r#rs) >>2 bs @ bs1"

   651 | "AALTs bs rs >>2 bs @ bs1 \<Longrightarrow> AALTs bs (r#rs) >>2 bs @ bs1"

   652 | "ASTAR bs r >>2 bs @ [S]"

   653 | "\<lbrakk>r >>2 bs1; ASTAR [] r >>2 bs2\<rbrakk> \<Longrightarrow> ASTAR bs r >>2 bs @ Z # bs1 @ bs2"

   654 | "r >>2 bs \<Longrightarrow> (bsimp r) >>2 bs"

   655 

   656 

   657 inductive contains :: "arexp \<Rightarrow> bit list \<Rightarrow> bool" ("_ >> _" [51, 50] 50)

   658   where

   659   "AONE bs >> bs"

   660 | "ACHAR bs c >> bs"

   661 | "\<lbrakk>a1 >> bs1; a2 >> bs2\<rbrakk> \<Longrightarrow> ASEQ bs a1 a2 >> bs @ bs1 @ bs2"

   662 | "r >> bs1 \<Longrightarrow> AALTs bs (r#rs) >> bs @ bs1"

   663 | "AALTs bs rs >> bs @ bs1 \<Longrightarrow> AALTs bs (r#rs) >> bs @ bs1"

   664 | "ASTAR bs r >> bs @ [S]"

   665 | "\<lbrakk>r >> bs1; ASTAR [] r >> bs2\<rbrakk> \<Longrightarrow> ASTAR bs r >> bs @ Z # bs1 @ bs2"

   666 

   667 lemma contains0:

   668   assumes "a >> bs"

   669   shows "(fuse bs1 a) >> bs1 @ bs"

   670   using assms

   671   apply(induct arbitrary: bs1)

   672   apply(auto intro: contains.intros)

   673        apply (metis append.assoc contains.intros(3))

   674      apply (metis append.assoc contains.intros(4))

   675   apply (metis append.assoc contains.intros(5))

   676     apply (metis append.assoc contains.intros(6))

   677    apply (metis append_assoc contains.intros(7))

   678   done

   679 

   680 lemma contains1:

   681   assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> intern r >> code v"

   682   shows "ASTAR [] (intern r) >> code (Stars vs)"

   683   using assms

   684   apply(induct vs)

   685    apply(simp)

   686   using contains.simps apply blast

   687   apply(simp)

   688    apply(subst (2) append_Nil[symmetric])

   689   apply(rule contains.intros)

   690    apply(auto)

   691   done

   692 

   693 

   694 

   695 

   696 

   697 lemma contains2:

   698   assumes "\<Turnstile> v : r"

   699   shows "(intern r) >> code v"

   700   using assms

   701   apply(induct)

   702        prefer 4

   703        apply(simp)

   704        apply(rule contains.intros)

   705    prefer 4

   706        apply(simp)

   707       apply(rule contains.intros)

   708      apply(simp)

   709   apply(subst (3) append_Nil[symmetric])

   710   apply(rule contains.intros)

   711       apply(simp)

   712   apply(simp)

   713     apply(simp)

   714   apply(subst (9) append_Nil[symmetric])

   715     apply(rule contains.intros)

   716     apply (metis append_Cons append_self_conv2 contains0)

   717     apply(simp)

   718      apply(subst (9) append_Nil[symmetric])

   719    apply(rule contains.intros)

   720    back

   721    apply(rule contains.intros)

   722   apply(drule_tac ?bs1.0="[S]" in contains0)

   723    apply(simp)

   724   apply(simp)

   725   apply(case_tac vs)

   726    apply(simp)

   727   apply (metis append_Nil contains.intros(6))

   728   using contains1 by blast

   729 

   730 lemma qq1:

   731   assumes "\<exists>r \<in> set rs. bnullable r"

   732   shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs rs)"

   733   using assms

   734   apply(induct rs arbitrary: rs1 bs)

   735   apply(simp)

   736   apply(simp)

   737   by (metis Nil_is_append_conv bmkeps.simps(4) neq_Nil_conv r0 split_list_last)

   738 

   739 lemma qq2:

   740   assumes "\<forall>r \<in> set rs. \<not> bnullable r" "\<exists>r \<in> set rs1. bnullable r"

   741   shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs rs1)"

   742   using assms

   743   apply(induct rs arbitrary: rs1 bs)

   744   apply(simp)

   745   apply(simp)

   746   by (metis append_assoc in_set_conv_decomp r1 r2)

   747 

   748 lemma qq2a:

   749   assumes "\<not> bnullable r" "\<exists>r \<in> set rs1. bnullable r"

   750   shows "bmkeps (AALTs bs (r # rs1)) = bmkeps (AALTs bs rs1)"

   751   using assms

   752   by (simp add: r1)

   753   

   754 lemma qq3:

   755   shows "bnullable (AALTs bs rs) = (\<exists>r \<in> set rs. bnullable r)"

   756   apply(induct rs arbitrary: bs)

   757   apply(simp)

   758   apply(simp)

   759   done

   760 

   761 lemma qq4:

   762   assumes "bnullable (AALTs bs rs)"

   763   shows "bmkeps (AALTs bs rs) = bs @ bmkeps (AALTs [] rs)"

   764   by (metis append_Nil2 assms bmkeps_retrieve bnullable_correctness erase_fuse fuse.simps(4) mkeps_nullable retrieve_fuse2)

   765 

   766 

   767 lemma contains3a:

   768   assumes "AALTs bs lst >> bs @ bs1"

   769   shows "AALTs bs (a # lst) >> bs @ bs1"

   770   using assms

   771   apply -

   772   by (simp add: contains.intros(5))

   773 

   774   

   775 lemma contains3b:

   776   assumes "a >> bs1"

   777   shows "AALTs bs (a # lst) >> bs @ bs1"

   778   using assms

   779   apply -

   780   apply(rule contains.intros)

   781   apply(simp)

   782   done   

   783 

   784 

   785 lemma contains3:

   786   assumes "\<And>x. \<lbrakk>x \<in> set rs; bnullable x\<rbrakk> \<Longrightarrow> x >> bmkeps x" "x \<in> set rs" "bnullable x"

   787   shows "AALTs bs rs >> bmkeps (AALTs bs rs)"

   788   using assms

   789   apply(induct rs arbitrary: bs x)

   790    apply simp

   791   by (metis contains.intros(4) contains.intros(5) list.set_intros(1) list.set_intros(2) qq3 qq4 r r0 r1)

   792 

   793 lemma cont1:

   794   assumes "\<And>v. \<Turnstile> v : erase r \<Longrightarrow> r >> retrieve r v" 

   795           "\<forall>v\<in>set vs. \<Turnstile> v : erase r \<and> flat v \<noteq> []" 

   796   shows "ASTAR bs r >> retrieve (ASTAR bs r) (Stars vs)"

   797   using assms 

   798   apply(induct vs arbitrary: bs r)

   799    apply(simp)

   800   using contains.intros(6) apply auto[1]

   801   by (simp add: contains.intros(7))

   802   

   803 lemma contains4:

   804   assumes "bnullable a"

   805   shows "a >> bmkeps a"

   806   using assms

   807   apply(induct a rule: bnullable.induct)

   808        apply(auto intro: contains.intros)

   809   using contains3 by blast

   810 

   811 lemma contains5:

   812   assumes "\<Turnstile> v : r"

   813   shows "(intern r) >> retrieve (intern r) v"

   814   using contains2[OF assms] retrieve_code[OF assms]

   815   by (simp)

   816 

   817 

   818 lemma contains6:

   819   assumes "\<Turnstile> v : (erase r)"

   820   shows "r >> retrieve r v"

   821   using assms

   822   apply(induct r arbitrary: v rule: erase.induct)

   823   apply(auto)[1]

   824   using Prf_elims(1) apply blast

   825   using Prf_elims(4) contains.intros(1) apply force

   826   using Prf_elims(5) contains.intros(2) apply force

   827   apply(auto)[1]

   828   using Prf_elims(1) apply blast

   829   apply(auto)[1]

   830   using contains3b contains3a apply blast

   831     prefer 2

   832   apply(auto)[1]

   833     apply (metis Prf_elims(2) contains.intros(3) retrieve.simps(6))

   834    prefer 2

   835   apply(auto)[1]

   836    apply (metis Prf_elims(6) cont1)

   837   apply(simp)

   838   apply(erule Prf_elims)

   839    apply(auto)

   840    apply (simp add: contains3b)

   841   using retrieve_fuse2 contains3b contains3a

   842   apply(subst retrieve_fuse2[symmetric])

   843   apply (metis append_Nil2 erase_fuse fuse.simps(4))

   844   apply(simp)

   845   by (metis append_Nil2 erase_fuse fuse.simps(4))

   846 

   847 lemma contains7:

   848   assumes "\<Turnstile> v : der c (erase r)"

   849   shows "(bder c r) >> retrieve r (injval (erase r) c v)"

   850   using bder_retrieve[OF assms(1)] retrieve_code[OF assms(1)]

   851   by (metis assms contains6 erase_bder)

   852 

   853 

   854 lemma contains7a:

   855   assumes "\<Turnstile> v : der c (erase r)"

   856   shows "r >> retrieve r (injval (erase r) c v)"

   857   using assms

   858   apply -

   859   apply(drule Prf_injval)

   860   apply(drule contains6)

   861   apply(simp)

   862   done

   863 

   864 lemma contains7b:

   865   assumes "\<Turnstile> v : ders s (erase r)"

   866   shows "(bders r s) >> retrieve r (flex (erase r) id s v)"

   867   using assms

   868   apply(induct s arbitrary: r v)

   869    apply(simp)

   870    apply (simp add: contains6)

   871   apply(simp add: bders_append flex_append ders_append)

   872   apply(drule_tac x="bder a r" in meta_spec)

   873   apply(drule meta_spec)

   874   apply(drule meta_mp)

   875    apply(simp)

   876   apply(simp)

   877   apply(subst (asm) bder_retrieve)

   878    defer

   879   apply (simp add: flex_injval)

   880   by (simp add: Prf_flex)

   881 

   882 lemma contains7_iff:

   883   assumes "\<Turnstile> v : der c (erase r)"

   884   shows "(bder c r) >> retrieve r (injval (erase r) c v) \<longleftrightarrow>

   885                   r >> retrieve r (injval (erase r) c v)"

   886   by (simp add: assms contains7 contains7a)

   887 

   888 lemma contains8_iff:

   889   assumes "\<Turnstile> v : ders s (erase r)"

   890   shows "(bders r s) >> retrieve r (flex (erase r) id s v) \<longleftrightarrow>

   891                   r >> retrieve r (flex (erase r) id s v)"

   892   using Prf_flex assms contains6 contains7b by blast

   893 

   894 

   895 fun 

   896   bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp"

   897 where

   898   "bders_simp r [] = r"

   899 | "bders_simp r (c # s) = bders_simp (bsimp (bder c r)) s"

   900 

   901 definition blexer_simp where

   902  "blexer_simp r s \<equiv> if bnullable (bders_simp (intern r) s) then 

   903                 decode (bmkeps (bders_simp (intern r) s)) r else None"

   904 

   905 

   906 

   907 

   908 

   909 lemma bders_simp_append:

   910   shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2"

   911   apply(induct s1 arbitrary: r s2)

   912    apply(simp)

   913   apply(simp)

   914   done

   915 

   916 lemma bsimp_ASEQ_size:

   917   shows "asize (bsimp_ASEQ bs r1 r2) \<le> Suc (asize r1 + asize r2)"

   918   apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)

   919   apply(auto)

   920   done

   921 

   922 

   923 

   924 lemma flts_size:

   925   shows "sum_list (map asize (flts rs)) \<le> sum_list (map asize rs)"

   926   apply(induct rs rule: flts.induct)

   927         apply(simp_all)

   928   by (simp add: asize_fuse comp_def)

   929   

   930 

   931 lemma bsimp_AALTs_size:

   932   shows "asize (bsimp_AALTs bs rs) \<le> Suc (sum_list (map asize rs))"

   933   apply(induct rs rule: bsimp_AALTs.induct)

   934   apply(auto simp add: asize_fuse)

   935   done

   936 

   937 

   938 lemma bsimp_size:

   939   shows "asize (bsimp r) \<le> asize r"

   940   apply(induct r)

   941        apply(simp_all)

   942    apply (meson Suc_le_mono add_mono_thms_linordered_semiring(1) bsimp_ASEQ_size le_trans)

   943   apply(rule le_trans)

   944    apply(rule bsimp_AALTs_size)

   945   apply(simp)

   946    apply(rule le_trans)

   947    apply(rule flts_size)

   948   by (simp add: sum_list_mono)

   949 

   950 lemma bsimp_asize0:

   951   shows "(\<Sum>x\<leftarrow>rs. asize (bsimp x)) \<le> sum_list (map asize rs)"

   952   apply(induct rs)

   953    apply(auto)

   954   by (simp add: add_mono bsimp_size)

   955 

   956 lemma bsimp_AALTs_size2:

   957   assumes "\<forall>r \<in> set  rs. nonalt r"

   958   shows "asize (bsimp_AALTs bs rs) \<ge> sum_list (map asize rs)"

   959   using assms

   960   apply(induct rs rule: bsimp_AALTs.induct)

   961     apply(simp_all add: asize_fuse)

   962   done

   963 

   964 

   965 lemma qq:

   966   shows "map (asize \<circ> fuse bs) rs = map asize rs"

   967   apply(induct rs)

   968    apply(auto simp add: asize_fuse)

   969   done

   970 

   971 lemma flts_size2:

   972   assumes "\<exists>bs rs'. AALTs bs  rs' \<in> set rs"

   973   shows "sum_list (map asize (flts rs)) < sum_list (map asize rs)"

   974   using assms

   975   apply(induct rs)

   976    apply(auto simp add: qq)

   977    apply (simp add: flts_size less_Suc_eq_le)

   978   apply(case_tac a)

   979        apply(auto simp add: qq)

   980    prefer 2

   981    apply (simp add: flts_size le_imp_less_Suc)

   982   using less_Suc_eq by auto

   983 

   984 lemma bsimp_AALTs_size3:

   985   assumes "\<exists>r \<in> set  (map bsimp rs). \<not>nonalt r"

   986   shows "asize (bsimp (AALTs bs rs)) < asize (AALTs bs rs)"

   987   using assms flts_size2

   988   apply  -

   989   apply(clarify)

   990   apply(simp)

   991   apply(drule_tac x="map bsimp rs" in meta_spec)

   992   apply(drule meta_mp)

   993   apply (metis list.set_map nonalt.elims(3))

   994   apply(simp)

   995   apply(rule order_class.order.strict_trans1)

   996    apply(rule bsimp_AALTs_size)

   997   apply(simp)

   998   by (smt Suc_leI bsimp_asize0 comp_def le_imp_less_Suc le_trans map_eq_conv not_less_eq)

   999 

  1000 

  1001 

  1002 

  1003 lemma L_bsimp_ASEQ:

  1004   "L (SEQ (erase r1) (erase r2)) = L (erase (bsimp_ASEQ bs r1 r2))"

  1005   apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)

  1006   apply(simp_all)

  1007   by (metis erase_fuse fuse.simps(4))

  1008 

  1009 lemma L_bsimp_AALTs:

  1010   "L (erase (AALTs bs rs)) = L (erase (bsimp_AALTs bs rs))"

  1011   apply(induct bs rs rule: bsimp_AALTs.induct)

  1012   apply(simp_all add: erase_fuse)

  1013   done

  1014 

  1015 lemma L_erase_AALTs:

  1016   shows "L (erase (AALTs bs rs)) = \<Union> (L ` erase ` (set rs))"

  1017   apply(induct rs)

  1018    apply(simp)

  1019   apply(simp)

  1020   apply(case_tac rs)

  1021    apply(simp)

  1022   apply(simp)

  1023   done

  1024 

  1025 lemma L_erase_flts:

  1026   shows "\<Union> (L ` erase ` (set (flts rs))) = \<Union> (L ` erase ` (set rs))"

  1027   apply(induct rs rule: flts.induct)

  1028         apply(simp_all)

  1029   apply(auto)

  1030   using L_erase_AALTs erase_fuse apply auto[1]

  1031   by (simp add: L_erase_AALTs erase_fuse)

  1032 

  1033 

  1034 lemma L_bsimp_erase:

  1035   shows "L (erase r) = L (erase (bsimp r))"

  1036   apply(induct r)

  1037   apply(simp)

  1038   apply(simp)

  1039   apply(simp)

  1040   apply(auto simp add: Sequ_def)[1]

  1041   apply(subst L_bsimp_ASEQ[symmetric])

  1042   apply(auto simp add: Sequ_def)[1]

  1043   apply(subst (asm)  L_bsimp_ASEQ[symmetric])

  1044   apply(auto simp add: Sequ_def)[1]

  1045    apply(simp)

  1046    apply(subst L_bsimp_AALTs[symmetric])

  1047    defer

  1048    apply(simp)

  1049   apply(subst (2)L_erase_AALTs)

  1050   apply(subst L_erase_flts)

  1051   apply(auto)

  1052    apply (simp add: L_erase_AALTs)

  1053   using L_erase_AALTs by blast

  1054 

  1055 lemma bsimp_ASEQ0:

  1056   shows "bsimp_ASEQ bs r1 AZERO = AZERO"

  1057   apply(induct r1)

  1058   apply(auto)

  1059   done

  1060 

  1061 

  1062 

  1063 lemma bsimp_ASEQ1:

  1064   assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<forall>bs. r1 \<noteq> AONE bs"

  1065   shows "bsimp_ASEQ bs r1 r2 = ASEQ bs r1 r2"

  1066   using assms

  1067   apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)

  1068   apply(auto)

  1069   done

  1070 

  1071 lemma bsimp_ASEQ2:

  1072   shows "bsimp_ASEQ bs (AONE bs1) r2 = fuse (bs @ bs1) r2"

  1073   apply(induct r2)

  1074   apply(auto)

  1075   done

  1076 

  1077 

  1078 lemma L_bders_simp:

  1079   shows "L (erase (bders_simp r s)) = L (erase (bders r s))"

  1080   apply(induct s arbitrary: r rule: rev_induct)

  1081    apply(simp)

  1082   apply(simp)

  1083   apply(simp add: ders_append)

  1084   apply(simp add: bders_simp_append)

  1085   apply(simp add: L_bsimp_erase[symmetric])

  1086   by (simp add: der_correctness)

  1087 

  1088 lemma b1:

  1089   "bsimp_ASEQ bs1 (AONE bs) r =  fuse (bs1 @ bs) r" 

  1090   apply(induct r)

  1091        apply(auto)

  1092   done

  1093 

  1094 lemma b2:

  1095   assumes "bnullable r"

  1096   shows "bmkeps (fuse bs r) = bs @ bmkeps r"

  1097   by (simp add: assms bmkeps_retrieve bnullable_correctness erase_fuse mkeps_nullable retrieve_fuse2)

  1098 

  1099 lemma b3:

  1100   shows "bnullable r = bnullable (bsimp r)"

  1101   using L_bsimp_erase bnullable_correctness nullable_correctness by auto

  1102 

  1103 

  1104 lemma b4:

  1105   shows "bnullable (bders_simp r s) = bnullable (bders r s)"

  1106   by (metis L_bders_simp bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1))

  1107 

  1108 lemma q1:

  1109   assumes "\<forall>r \<in> set rs. bmkeps(bsimp r) = bmkeps r"

  1110   shows "map (\<lambda>r. bmkeps(bsimp r)) rs = map bmkeps rs"

  1111   using assms

  1112   apply(induct rs)

  1113   apply(simp)

  1114   apply(simp)

  1115   done

  1116 

  1117 lemma q3:

  1118   assumes "\<exists>r \<in> set rs. bnullable r"

  1119   shows "bmkeps (AALTs bs rs) = bmkeps (bsimp_AALTs bs rs)"

  1120   using assms

  1121   apply(induct bs rs rule: bsimp_AALTs.induct)

  1122     apply(simp)

  1123    apply(simp)

  1124   apply (simp add: b2)

  1125   apply(simp)

  1126   done

  1127 

  1128 

  1129 lemma fuse_empty:

  1130   shows "fuse [] r = r"

  1131   apply(induct r)

  1132        apply(auto)

  1133   done

  1134 

  1135 lemma flts_fuse: