1 

     2 theory SizeBound

     3   imports "Lexer" 

     4 begin

     5 

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

     7 

     8 datatype bit = Z | S

     9 

    10 fun code :: "val \<Rightarrow> bit list"

    11 where

    12   "code Void = []"

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

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

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

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

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

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

    19 

    20 

    21 fun 

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

    23 where

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

    25 

    26 function

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

    28 where

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

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

    31 | "decode' ds (CH d) = (Char d, ds)"

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

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

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

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

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

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

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

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

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

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

    42 by pat_completeness auto

    43 

    44 lemma decode'_smaller:

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

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

    47 using assms

    48 apply(induct ds r)

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

    50 using dual_order.trans apply blast

    51 by (meson dual_order.trans le_SucI)

    52 

    53 termination "decode'"  

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

    55 apply(auto dest!: decode'_smaller)

    56 by (metis less_Suc_eq_le snd_conv)

    57 

    58 definition

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

    60 where

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

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

    63 

    64 lemma decode'_code_Stars:

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

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

    67   using assms

    68   apply(induct vs)

    69   apply(auto)

    70   done

    71 

    72 lemma decode'_code:

    73   assumes "\<Turnstile> v : r"

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

    75 using assms

    76   apply(induct v r arbitrary: ds) 

    77   apply(auto)

    78   using decode'_code_Stars by blast

    79 

    80 lemma decode_code:

    81   assumes "\<Turnstile> v : r"

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

    83   using assms unfolding decode_def

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

    85 

    86 

    87 section {* Annotated Regular Expressions *}

    88 

    89 datatype arexp = 

    90   AZERO

    91 | AONE "bit list"

    92 | ACHAR "bit list" char

    93 | ASEQ "bit list" arexp arexp

    94 | AALTs "bit list" "arexp list"

    95 | ASTAR "bit list" arexp

    96 

    97 abbreviation

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

    99 

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

   101   "asize AZERO = 1"

   102 | "asize (AONE cs) = 1" 

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

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

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

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

   107 

   108 fun 

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

   110 where

   111   "erase AZERO = ZERO"

   112 | "erase (AONE _) = ONE"

   113 | "erase (ACHAR _ c) = CH c"

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

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

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

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

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

   119 

   120 

   121 

   122 

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

   124   where

   125   "nonalt (AALTs bs2 rs) = False"

   126 | "nonalt r = True"

   127 

   128 

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

   130   "good AZERO = False"

   131 | "good (AONE cs) = True" 

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

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

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

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

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

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

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

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

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

   141 

   142 

   143 

   144 

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

   146   "fuse bs AZERO = AZERO"

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

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

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

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

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

   152 

   153 lemma fuse_append:

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

   155   apply(induct r)

   156   apply(auto)

   157   done

   158 

   159 

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

   161   "intern ZERO = AZERO"

   162 | "intern ONE = AONE []"

   163 | "intern (CH c) = ACHAR [] c"

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

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

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

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

   168 

   169 

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

   171   "retrieve (AONE bs) Void = bs"

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

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

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

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

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

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

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

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

   180 

   181 

   182 

   183 fun

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

   185 where

   186   "bnullable (AZERO) = False"

   187 | "bnullable (AONE bs) = True"

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

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

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

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

   192 

   193 fun 

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

   195 where

   196   "bmkeps(AONE bs) = bs"

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

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

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

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

   201 

   202 

   203 fun

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

   205 where

   206   "bder c (AZERO) = AZERO"

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

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

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

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

   211      (if bnullable r1

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

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

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

   215 

   216 

   217 fun 

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

   219 where

   220   "bders r [] = r"

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

   222 

   223 lemma bders_append:

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

   225   apply(induct s1 arbitrary: r s2)

   226   apply(simp_all)

   227   done

   228 

   229 lemma bnullable_correctness:

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

   231   apply(induct r rule: erase.induct)

   232   apply(simp_all)

   233   done

   234 

   235 lemma erase_fuse:

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

   237   apply(induct r rule: erase.induct)

   238   apply(simp_all)

   239   done

   240 

   241 thm Posix.induct

   242 

   243 lemma erase_intern [simp]:

   244   shows "erase (intern r) = r"

   245   apply(induct r)

   246   apply(simp_all add: erase_fuse)

   247   done

   248 

   249 lemma erase_bder [simp]:

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

   251   apply(induct r rule: erase.induct)

   252   apply(simp_all add: erase_fuse bnullable_correctness)

   253   done

   254 

   255 lemma erase_bders [simp]:

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

   257   apply(induct s arbitrary: r )

   258   apply(simp_all)

   259   done

   260 

   261 lemma retrieve_encode_STARS:

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

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

   264   using assms

   265   apply(induct vs)

   266   apply(simp_all)

   267   done

   268 

   269 

   270 lemma retrieve_fuse2:

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

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

   273   using assms

   274   apply(induct r arbitrary: v bs)

   275          apply(auto elim: Prf_elims)[4]

   276    defer

   277   using retrieve_encode_STARS

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

   279    apply(case_tac vs)

   280     apply(simp)

   281    apply(simp)

   282   (* AALTs  case *)

   283   apply(simp)

   284   apply(case_tac x2a)

   285    apply(simp)

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

   287   apply(simp)

   288    apply(case_tac list)

   289    apply(simp)

   290   apply(auto)

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

   292   done

   293 

   294 lemma retrieve_fuse:

   295   assumes "\<Turnstile> v : r"

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

   297   using assms 

   298   by (simp_all add: retrieve_fuse2)

   299 

   300 

   301 lemma retrieve_code:

   302   assumes "\<Turnstile> v : r"

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

   304   using assms

   305   apply(induct v r )

   306   apply(simp_all add: retrieve_fuse retrieve_encode_STARS)

   307   done

   308 

   309 

   310 lemma bnullable_Hdbmkeps_Hd:

   311   assumes "bnullable a" 

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

   313   using assms

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

   315 

   316 lemma r1:

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

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

   319   using assms

   320   apply(induct rs)

   321    apply(auto)

   322   done

   323 

   324 lemma r2:

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

   326   shows "bnullable (AALTs bs rs)"

   327   using assms

   328   apply(induct rs)

   329    apply(auto)

   330   done

   331 

   332 lemma  r3:

   333   assumes "\<not> bnullable r" 

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

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

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

   337   using assms

   338   apply(induct rs arbitrary: r bs)

   339    apply(auto)[1]

   340   apply(auto)

   341   using bnullable_correctness apply blast

   342     apply(auto simp add: bnullable_correctness mkeps_nullable retrieve_fuse2)

   343    apply(subst retrieve_fuse2[symmetric])

   344   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)

   345    apply(simp)

   346   apply(case_tac "bnullable a")

   347   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)

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

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

   350   apply(drule meta_mp)

   351    apply(simp)

   352   apply(drule meta_mp)

   353    apply(auto)

   354   apply(subst retrieve_fuse2[symmetric])

   355   apply(case_tac rs)

   356     apply(simp)

   357    apply(auto)[1]

   358       apply (simp add: bnullable_correctness)

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

   360     apply (simp add: bnullable_correctness)

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

   362   apply(simp)

   363   done

   364 

   365 

   366 lemma t: 

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

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

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

   370   using assms

   371   apply(induct rs arbitrary: bs)

   372    apply(simp)

   373   apply(auto simp add: bnullable_correctness)

   374    apply(case_tac rs)

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

   376    apply(subst r1)

   377      apply(simp)

   378     apply(rule r2)

   379      apply(assumption)

   380     apply(simp)

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

   382    apply(drule meta_mp)

   383     apply(auto)[1]

   384    prefer 2

   385   apply(case_tac "bnullable a")

   386     apply(subst bnullable_Hdbmkeps_Hd)

   387      apply blast

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

   389   prefer 2

   390   using bnullable_correctness apply blast

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

   392   apply(subst r1)

   393      apply(simp)

   394   using r2 apply blast

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

   396    apply(drule meta_mp)

   397     apply(auto)[1]

   398    apply(simp)

   399   using r3 apply blast

   400   apply(auto)

   401   using r3 by blast

   402 

   403 lemma bmkeps_retrieve:

   404   assumes "nullable (erase r)"

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

   406   using assms

   407   apply(induct r)

   408          apply(simp)

   409         apply(simp)

   410        apply(simp)

   411     apply(simp)

   412    defer

   413    apply(simp)

   414   apply(rule t)

   415    apply(auto)

   416   done

   417 

   418 lemma bder_retrieve:

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

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

   421   using assms

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

   423          apply(simp)

   424          apply(erule Prf_elims)

   425         apply(simp)

   426         apply(erule Prf_elims) 

   427         apply(simp)

   428       apply(case_tac "c = ca")

   429        apply(simp)

   430        apply(erule Prf_elims)

   431        apply(simp)

   432       apply(simp)

   433        apply(erule Prf_elims)

   434   apply(simp)

   435       apply(erule Prf_elims)

   436      apply(simp)

   437     apply(simp)

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

   439     apply(erule Prf_elims)

   440      apply(simp)

   441     apply(simp)

   442     apply(case_tac rs)

   443      apply(simp)

   444     apply(simp)

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

   446    apply(simp)

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

   448     apply(simp)

   449   apply(erule Prf_elims)

   450      apply(subgoal_tac "bnullable r1")

   451   prefer 2

   452   using bnullable_correctness apply blast

   453     apply(simp)

   454      apply(erule Prf_elims)

   455      apply(simp)

   456    apply(subgoal_tac "bnullable r1")

   457   prefer 2

   458   using bnullable_correctness apply blast

   459     apply(simp)

   460     apply(simp add: retrieve_fuse2)

   461     apply(simp add: bmkeps_retrieve)

   462    apply(simp)

   463    apply(erule Prf_elims)

   464    apply(simp)

   465   using bnullable_correctness apply blast

   466   apply(rename_tac bs r v)

   467   apply(simp)

   468   apply(erule Prf_elims)

   469      apply(clarify)

   470   apply(erule Prf_elims)

   471   apply(clarify)

   472   apply(subst injval.simps)

   473   apply(simp del: retrieve.simps)

   474   apply(subst retrieve.simps)

   475   apply(subst retrieve.simps)

   476   apply(simp)

   477   apply(simp add: retrieve_fuse2)

   478   done

   479   

   480 

   481 

   482 lemma MAIN_decode:

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

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

   485   using assms

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

   487   case Nil

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

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

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

   491     using decode_code retrieve_code by auto

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

   493     by simp

   494 next

   495   case (snoc c s v)

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

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

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

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

   500     by (simp add: Prf_injval ders_append)

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

   502     by (simp add: flex_append)

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

   504     using asm2 IH by simp

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

   506     using asm by (simp_all add: bder_retrieve ders_append)

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

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

   509 qed

   510 

   511 

   512 definition blex where

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

   514 

   515 

   516 

   517 definition blexer where

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

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

   520 

   521 lemma blexer_correctness:

   522   shows "blexer r s = lexer r s"

   523 proof -

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

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

   526     assume asm: "nullable ds"

   527     have era: "erase bds = ds" 

   528       unfolding ds_def bds_def by simp

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

   530       using asm by (simp add: mkeps_nullable)

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

   532       using bmkeps_retrieve

   533       using asm era by (simp add: bmkeps_retrieve)

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

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

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

   537       unfolding bds_def ds_def .

   538   }

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

   540     unfolding blexer_def lexer_flex

   541     apply(subst bnullable_correctness[symmetric])

   542     apply(simp)

   543     done

   544 qed

   545 

   546 

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

   548   where

   549   "distinctBy [] f acc = []"

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

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

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

   553 

   554 

   555 

   556 

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

   558   where 

   559   "flts [] = []"

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

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

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

   563 

   564 

   565 

   566 

   567 fun li :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp"

   568   where

   569   "li _ [] = AZERO"

   570 | "li bs [a] = fuse bs a"

   571 | "li bs as = AALTs bs as"

   572 

   573 

   574 

   575 

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

   577   where

   578   "bsimp_ASEQ _ AZERO _ = AZERO"

   579 | "bsimp_ASEQ _ _ AZERO = AZERO"

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

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

   582 

   583 

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

   585   where

   586   "bsimp_AALTs _ [] = AZERO"

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

   588 | "bsimp_AALTs bs1 rs = AALTs bs1 rs"

   589 

   590 

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

   592   where

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

   594 | "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (distinctBy  (flts (map bsimp rs)) erase {} ) "

   595 | "bsimp r = r"

   596 

   597 

   598 

   599 

   600 fun 

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

   602 where

   603   "bders_simp r [] = r"

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

   605 

   606 definition blexer_simp where

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

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

   609 

   610 export_code bders_simp in Scala module_name Example

   611 

   612 lemma bders_simp_append:

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

   614   apply(induct s1 arbitrary: r s2)

   615    apply(simp)

   616   apply(simp)

   617   done

   618 

   619 

   620 

   621 

   622 

   623 

   624 

   625 lemma L_bsimp_ASEQ:

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

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

   628   apply(simp_all)

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

   630 

   631 lemma L_bsimp_AALTs:

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

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

   634   apply(simp_all add: erase_fuse)

   635   done

   636 

   637 lemma L_erase_AALTs:

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

   639   apply(induct rs)

   640    apply(simp)

   641   apply(simp)

   642   apply(case_tac rs)

   643    apply(simp)

   644   apply(simp)

   645   done

   646 

   647 lemma L_erase_flts:

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

   649   apply(induct rs rule: flts.induct)

   650         apply(simp_all)

   651   apply(auto)

   652   using L_erase_AALTs erase_fuse apply auto[1]

   653   by (simp add: L_erase_AALTs erase_fuse)

   654 

   655 lemma L_erase_dB_acc:

   656   shows "( \<Union>(L ` acc) \<union> ( \<Union> (L ` erase ` (set (distinctBy rs erase acc) ) ) )) = \<Union>(L ` acc) \<union>  \<Union> (L ` erase ` (set rs))"

   657   apply(induction rs arbitrary: acc)

   658    apply simp

   659   apply simp

   660   by (smt (z3) SUP_absorb UN_insert sup_assoc sup_commute)

   661 

   662 lemma L_erase_dB:

   663   shows " ( \<Union> (L ` erase ` (set (distinctBy rs erase {}) ) ) ) = \<Union> (L ` erase ` (set rs))"

   664   by (metis L_erase_dB_acc Un_commute Union_image_empty)

   665 

   666 lemma L_bsimp_erase:

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

   668   apply(induct r)

   669   apply(simp)

   670   apply(simp)

   671   apply(simp)

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

   673   apply(subst L_bsimp_ASEQ[symmetric])

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

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

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

   677    apply(simp)

   678    apply(subst L_bsimp_AALTs[symmetric])

   679    defer

   680    apply(simp)

   681   apply(subst (2)L_erase_AALTs)

   682   apply(subst L_erase_dB)

   683   apply(subst L_erase_flts)

   684   apply(auto)

   685    apply (simp add: L_erase_AALTs)

   686   using L_erase_AALTs by blast

   687 

   688 lemma bsimp_ASEQ0:

   689   shows "bsimp_ASEQ bs r1 AZERO = AZERO"

   690   apply(induct r1)

   691   apply(auto)

   692   done

   693 

   694 

   695 

   696 lemma bsimp_ASEQ1:

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

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

   699   using assms

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

   701   apply(auto)

   702   done

   703 

   704 lemma bsimp_ASEQ2:

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

   706   apply(induct r2)

   707   apply(auto)

   708   done

   709 

   710 

   711 lemma L_bders_simp:

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

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

   714    apply(simp)

   715   apply(simp)

   716   apply(simp add: ders_append)

   717   apply(simp add: bders_simp_append)

   718   apply(simp add: L_bsimp_erase[symmetric])

   719   by (simp add: der_correctness)

   720 

   721 

   722 lemma b2:

   723   assumes "bnullable r"

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

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

   726 

   727 

   728 lemma b4:

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

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

   731 

   732 

   733 lemma qq1:

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

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

   736   using assms

   737   apply(induct rs arbitrary: rs1 bs)

   738   apply(simp)

   739   apply(simp)

   740   by (metis Nil_is_append_conv bmkeps.simps(4) neq_Nil_conv bnullable_Hdbmkeps_Hd split_list_last)

   741 

   742 lemma qq2:

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

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

   745   using assms

   746   apply(induct rs arbitrary: rs1 bs)

   747   apply(simp)

   748   apply(simp)

   749   by (metis append_assoc in_set_conv_decomp r1 r2)

   750   

   751 lemma qq3:

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

   753   apply(induct rs arbitrary: bs)

   754   apply(simp)

   755   apply(simp)

   756   done

   757 

   758 

   759 

   760 

   761 

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

   763   where

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

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

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

   767 | "nonnested r = True"

   768 

   769 

   770 lemma  k0:

   771   shows "flts (r # rs1) = flts [r] @ flts rs1"

   772   apply(induct r arbitrary: rs1)

   773    apply(auto)

   774   done

   775 

   776 lemma  k00:

   777   shows "flts (rs1 @ rs2) = flts rs1 @ flts rs2"

   778   apply(induct rs1 arbitrary: rs2)

   779    apply(auto)

   780   by (metis append.assoc k0)

   781 

   782 lemma  k0a:

   783   shows "flts [AALTs bs rs] = map (fuse bs)  rs"

   784   apply(simp)

   785   done

   786 

   787 

   788 

   789 

   790 

   791 

   792 

   793 

   794 lemma bsimp_AALTs_qq:

   795   assumes "1 < length rs"

   796   shows "bsimp_AALTs bs rs = AALTs bs  rs"

   797   using  assms

   798   apply(case_tac rs)

   799    apply(simp)

   800   apply(case_tac list)

   801    apply(simp_all)

   802   done

   803 

   804 

   805 

   806 lemma bbbbs1:

   807   shows "nonalt r \<or> (\<exists>bs rs. r  = AALTs bs rs)"

   808   using nonalt.elims(3) by auto

   809   

   810 

   811 

   812 

   813 

   814 lemma flts_append:

   815   "flts (xs1 @ xs2) = flts xs1 @ flts xs2"

   816   apply(induct xs1  arbitrary: xs2  rule: rev_induct)

   817    apply(auto)

   818   apply(case_tac xs)

   819    apply(auto)

   820    apply(case_tac x)

   821         apply(auto)

   822   apply(case_tac x)

   823         apply(auto)

   824   done

   825 

   826 fun nonazero :: "arexp \<Rightarrow> bool"

   827   where

   828   "nonazero AZERO = False"

   829 | "nonazero r = True"

   830 

   831 

   832 lemma flts_single1:

   833   assumes "nonalt r" "nonazero r"

   834   shows "flts [r] = [r]"

   835   using assms

   836   apply(induct r)

   837   apply(auto)

   838   done

   839 

   840 

   841 

   842 lemma q3a:

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

   844   shows "bmkeps (AALTs bs (map (fuse bs1) rs)) = bmkeps (AALTs (bs@bs1) rs)"

   845   using assms

   846   apply(induct rs arbitrary: bs bs1)

   847    apply(simp)

   848   apply(simp)

   849   apply(auto)

   850    apply (metis append_assoc b2 bnullable_correctness erase_fuse bnullable_Hdbmkeps_Hd)

   851   apply(case_tac "bnullable a")

   852    apply (metis append.assoc b2 bnullable_correctness erase_fuse bnullable_Hdbmkeps_Hd)

   853   apply(case_tac rs)

   854   apply(simp)

   855   apply(simp)

   856   apply(auto)[1]

   857    apply (metis bnullable_correctness erase_fuse)+

   858   done

   859 

   860 lemma qq4:

   861   assumes "\<exists>x\<in>set list. bnullable x"

   862   shows "\<exists>x\<in>set (flts list). bnullable x"

   863   using assms

   864   apply(induct list rule: flts.induct)

   865         apply(auto)

   866   by (metis UnCI bnullable_correctness erase_fuse imageI)

   867   

   868 

   869 lemma qs3:

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

   871   shows "bmkeps (AALTs bs rs) = bmkeps (AALTs bs (flts rs))"

   872   using assms

   873   apply(induct rs arbitrary: bs taking: size rule: measure_induct)

   874   apply(case_tac x)

   875   apply(simp)

   876   apply(simp)

   877   apply(case_tac a)

   878        apply(simp)

   879        apply (simp add: r1)

   880       apply(simp)

   881       apply (simp add: bnullable_Hdbmkeps_Hd)

   882      apply(simp)

   883      apply(case_tac "flts list")

   884       apply(simp)

   885   apply (metis L_erase_AALTs L_erase_flts L_flat_Prf1 L_flat_Prf2 Prf_elims(1) bnullable_correctness erase.simps(4) mkeps_nullable r2)

   886      apply(simp)

   887      apply (simp add: r1)

   888     prefer 3

   889     apply(simp)

   890     apply (simp add: bnullable_Hdbmkeps_Hd)

   891    prefer 2

   892    apply(simp)

   893   apply(case_tac "\<exists>x\<in>set x52. bnullable x")

   894   apply(case_tac "list")

   895     apply(simp)

   896     apply (metis b2 fuse.simps(4) q3a r2)

   897    apply(erule disjE)

   898     apply(subst qq1)

   899      apply(auto)[1]

   900      apply (metis bnullable_correctness erase_fuse)

   901     apply(simp)

   902      apply (metis b2 fuse.simps(4) q3a r2)

   903     apply(simp)

   904     apply(auto)[1]

   905      apply(subst qq1)

   906       apply (metis bnullable_correctness erase_fuse image_eqI set_map)

   907      apply (metis b2 fuse.simps(4) q3a r2)

   908   apply(subst qq1)

   909       apply (metis bnullable_correctness erase_fuse image_eqI set_map)

   910     apply (metis b2 fuse.simps(4) q3a r2)

   911    apply(simp)

   912    apply(subst qq2)

   913      apply (metis bnullable_correctness erase_fuse imageE set_map)

   914   prefer 2

   915   apply(case_tac "list")

   916      apply(simp)

   917     apply(simp)

   918    apply (simp add: qq4)

   919   apply(simp)

   920   apply(auto)

   921    apply(case_tac list)

   922     apply(simp)

   923    apply(simp)

   924    apply (simp add: bnullable_Hdbmkeps_Hd)

   925   apply(case_tac "bnullable (ASEQ x41 x42 x43)")

   926    apply(case_tac list)

   927     apply(simp)

   928    apply(simp)

   929    apply (simp add: bnullable_Hdbmkeps_Hd)

   930   apply(simp)

   931   using qq4 r1 r2 by auto

   932 

   933 

   934 

   935   

   936 lemma bder_fuse:

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

   938   apply(induct a arbitrary: bs c)

   939        apply(simp_all)

   940   done

   941 

   942 

   943 fun flts2 :: "char \<Rightarrow> arexp list \<Rightarrow> arexp list"

   944   where 

   945   "flts2 _ [] = []"

   946 | "flts2 c (AZERO # rs) = flts2 c rs"

   947 | "flts2 c (AONE _ # rs) = flts2 c rs"

   948 | "flts2 c (ACHAR bs d # rs) = (if c = d then (ACHAR bs d # flts2 c rs) else flts2 c rs)"

   949 | "flts2 c ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ flts2 c rs"

   950 | "flts2 c (ASEQ bs r1 r2 # rs) = (if (bnullable(r1) \<and> r2 = AZERO) then 

   951     flts2 c rs

   952     else ASEQ bs r1 r2 # flts2 c rs)"

   953 | "flts2 c (r1 # rs) = r1 # flts2 c rs"

   954 

   955 

   956 

   957 

   958 

   959 

   960 

   961 

   962  

   963 

   964 

   965 

   966 

   967 lemma WQ1:

   968   assumes "s \<in> L (der c r)"

   969   shows "s \<in> der c r \<rightarrow> mkeps (ders s (der c r))"

   970   using assms

   971   oops

   972 

   973 

   974 

   975 lemma bder_bsimp_AALTs:

   976   shows "bder c (bsimp_AALTs bs rs) = bsimp_AALTs bs (map (bder c) rs)"

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

   978     apply(simp)

   979    apply(simp)

   980    apply (simp add: bder_fuse)

   981   apply(simp)

   982   done

   983 

   984 

   985 

   986 lemma

   987   assumes "asize (bsimp a) = asize a"  "a = AALTs bs [AALTs bs2 [], AZERO, AONE bs3]"

   988   shows "bsimp a = a"

   989   using assms

   990   apply(simp)

   991   oops

   992 

   993 

   994 

   995 

   996 

   997 

   998 

   999 

  1000 inductive rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)

  1001   where

  1002   "ASEQ bs AZERO r2 \<leadsto> AZERO"

  1003 | "ASEQ bs r1 AZERO \<leadsto> AZERO"

  1004 | "ASEQ bs (AONE bs1) r \<leadsto> fuse (bs@bs1) r"

  1005 | "r1 \<leadsto> r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r2 r3"

  1006 | "r3 \<leadsto> r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r1 r4"

  1007 | "r \<leadsto> r' \<Longrightarrow> (AALTs bs (rs1 @ [r] @ rs2)) \<leadsto> (AALTs bs (rs1 @ [r'] @ rs2))"

  1008 (*context rule for eliminating 0, alts--corresponds to the recursive call flts r::rs = r::(flts rs)*)

  1009 | "AALTs bs (rsa@AZERO # rsb) \<leadsto> AALTs bs (rsa@rsb)"

  1010 | "AALTs bs (rsa@(AALTs bs1 rs1)# rsb) \<leadsto> AALTs bs (rsa@(map (fuse bs1) rs1)@rsb)"

  1011 (*the below rule for extracting common prefixes between a list of rexp's bitcodes*)

  1012 | "AALTs bs (map (fuse bs1) rs) \<leadsto> AALTs (bs@bs1) rs"

  1013 (*opposite direction also allowed, which means bits  are free to be moved around

  1014 as long as they are on the right path*)

  1015 | "AALTs (bs@bs1) rs \<leadsto> AALTs bs (map (fuse bs1) rs)"

  1016 | "AALTs bs [] \<leadsto> AZERO"

  1017 | "AALTs bs [r] \<leadsto> fuse bs r"

  1018 | "erase a1 = erase a2 \<Longrightarrow> AALTs bs (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> AALTs bs (rsa@[a1]@rsb@rsc)"

  1019 

  1020 

  1021 inductive rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100)

  1022   where 

  1023 rs1[intro, simp]:"r \<leadsto>* r"

  1024 | rs2[intro]: "\<lbrakk>r1 \<leadsto>* r2; r2 \<leadsto> r3\<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"

  1025 

  1026 inductive srewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ s\<leadsto>* _" [100, 100] 100)

  1027   where

  1028 ss1: "[] s\<leadsto>* []"

  1029 |ss2: "\<lbrakk>r \<leadsto>* r'; rs s\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (r#rs) s\<leadsto>* (r'#rs')"

  1030 (*rs1 = [r1, r2, ..., rn] rs2 = [r1', r2', ..., rn']

  1031 [r1, r2, ..., rn] \<leadsto>* [r1', r2, ..., rn] \<leadsto>* [...r2',...] \<leadsto>* [r1', r2',... rn']

  1032 *)

  1033 

  1034 

  1035 

  1036 lemma r_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"

  1037   using rrewrites.intros(1) rrewrites.intros(2) by blast

  1038  

  1039 lemma real_trans: 

  1040   assumes a1: "r1 \<leadsto>* r2"  and a2: "r2 \<leadsto>* r3"

  1041   shows "r1 \<leadsto>* r3"

  1042   using a2 a1

  1043   apply(induct r2 r3 arbitrary: r1 rule: rrewrites.induct) 

  1044    apply(auto)

  1045   done

  1046 

  1047 

  1048 lemma  many_steps_later: "\<lbrakk>r1 \<leadsto> r2; r2 \<leadsto>* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"

  1049   by (meson r_in_rstar real_trans)

  1050 

  1051 

  1052 lemma contextrewrites1: "r \<leadsto>* r' \<Longrightarrow> (AALTs bs (r#rs)) \<leadsto>* (AALTs bs (r'#rs))"

  1053   apply(induct r r' rule: rrewrites.induct)

  1054    apply simp

  1055   by (metis append_Cons append_Nil rrewrite.intros(6) rs2)

  1056 

  1057 

  1058 lemma contextrewrites2: "r \<leadsto>* r' \<Longrightarrow> (AALTs bs (rs1@[r]@rs)) \<leadsto>* (AALTs bs (rs1@[r']@rs))"

  1059   apply(induct r r' rule: rrewrites.induct)

  1060    apply simp

  1061   using rrewrite.intros(6) by blast

  1062 

  1063 

  1064 

  1065 lemma srewrites_alt: "rs1 s\<leadsto>* rs2 \<Longrightarrow> (AALTs bs (rs@rs1)) \<leadsto>* (AALTs bs (rs@rs2))"

  1066 

  1067   apply(induct rs1 rs2 arbitrary: bs rs rule: srewrites.induct)

  1068    apply(rule rs1)

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

  1070   apply(drule_tac x = "rsa@[r']" in meta_spec)

  1071   apply simp

  1072   apply(rule real_trans)

  1073    prefer 2

  1074    apply(assumption)

  1075   apply(drule contextrewrites2)

  1076   apply auto

  1077   done

  1078 

  1079 

  1080 corollary srewrites_alt1: "rs1 s\<leadsto>* rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto>* AALTs bs rs2"

  1081   by (metis append.left_neutral srewrites_alt)

  1082 

  1083 

  1084 lemma star_seq:  "r1 \<leadsto>* r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto>* ASEQ bs r2 r3"

  1085   apply(induct r1 r2 arbitrary: r3 rule: rrewrites.induct)

  1086    apply(rule rs1)

  1087   apply(erule rrewrites.cases)

  1088    apply(simp)

  1089    apply(rule r_in_rstar)

  1090    apply(rule rrewrite.intros(4))

  1091    apply simp

  1092   apply(rule rs2)

  1093    apply(assumption)

  1094   apply(rule rrewrite.intros(4))

  1095   by assumption

  1096 

  1097 lemma star_seq2:  "r3 \<leadsto>* r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto>* ASEQ bs r1 r4"

  1098   apply(induct r3 r4 arbitrary: r1 rule: rrewrites.induct)

  1099    apply auto

  1100   using rrewrite.intros(5) by blast

  1101 

  1102 

  1103 lemma continuous_rewrite: "\<lbrakk>r1 \<leadsto>* AZERO\<rbrakk> \<Longrightarrow> ASEQ bs1 r1 r2 \<leadsto>* AZERO"

  1104   apply(induction ra\<equiv>"r1" rb\<equiv>"AZERO" arbitrary: bs1 r1 r2 rule: rrewrites.induct)

  1105    apply (simp add: r_in_rstar rrewrite.intros(1))

  1106 

  1107   by (meson rrewrite.intros(1) rrewrites.intros(2) star_seq)

  1108   

  1109 

  1110 

  1111 lemma bsimp_aalts_simpcases: "AONE bs \<leadsto>* (bsimp (AONE bs))"  "AZERO \<leadsto>* bsimp AZERO" "ACHAR bs c \<leadsto>* (bsimp (ACHAR bs c))"

  1112   apply (simp add: rrewrites.intros(1))

  1113   apply (simp add: rrewrites.intros(1))

  1114   by (simp add: rrewrites.intros(1))

  1115 

  1116 lemma trivialbsimpsrewrites: "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs s\<leadsto>* (map f rs)"

  1117 

  1118   apply(induction rs)

  1119    apply simp

  1120    apply(rule ss1)

  1121   by (metis insert_iff list.simps(15) list.simps(9) srewrites.simps)

  1122 

  1123 

  1124 lemma bsimp_AALTsrewrites: "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs"

  1125   apply(induction rs)

  1126   apply simp

  1127    apply(rule r_in_rstar)

  1128    apply(simp add:  rrewrite.intros(11))

  1129   apply(case_tac "rs = Nil")

  1130    apply(simp)

  1131   using rrewrite.intros(12) apply auto[1]

  1132   apply(subgoal_tac "length (a#rs) > 1")

  1133    apply(simp add: bsimp_AALTs_qq)

  1134   apply(simp)

  1135   done