1 

     2 theory SizeBound5CT

     3   imports "Lexer" "PDerivs"

     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' bs ZERO = (undefined, bs)"

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

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

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

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

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

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

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

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

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

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

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

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

    42 by pat_completeness auto

    43 

    44 lemma decode'_smaller:

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

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

    47 using assms

    48 apply(induct bs 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 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where

   122   "fuse bs AZERO = AZERO"

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

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

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

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

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

   128 

   129 lemma fuse_append:

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

   131   apply(induct r)

   132   apply(auto)

   133   done

   134 

   135 

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

   137   "intern ZERO = AZERO"

   138 | "intern ONE = AONE []"

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

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

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

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

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

   144 

   145 

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

   147   "retrieve (AONE bs) Void = bs"

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

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

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

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

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

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

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

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

   156 

   157 

   158 

   159 fun

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

   161 where

   162   "bnullable (AZERO) = False"

   163 | "bnullable (AONE bs) = True"

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

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

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

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

   168 

   169 abbreviation

   170   bnullables :: "arexp list \<Rightarrow> bool"

   171 where

   172   "bnullables rs \<equiv> (\<exists>r \<in> set rs. bnullable r)"

   173 

   174 fun 

   175   bmkeps :: "arexp \<Rightarrow> bit list" and

   176   bmkepss :: "arexp list \<Rightarrow> bit list"

   177 where

   178   "bmkeps(AONE bs) = bs"

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

   180 | "bmkeps(AALTs bs rs) = bs @ (bmkepss rs)"

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

   182 | "bmkepss [] = []"

   183 | "bmkepss (r # rs) = (if bnullable(r) then (bmkeps r) else (bmkepss rs))"

   184 

   185 lemma bmkepss1:

   186   assumes "\<not> bnullables rs1"

   187   shows "bmkepss (rs1 @ rs2) = bmkepss rs2"

   188   using assms

   189   by (induct rs1) (auto)

   190 

   191 lemma bmkepss2:

   192   assumes "bnullables rs1"

   193   shows "bmkepss (rs1 @ rs2) = bmkepss rs1"

   194   using assms

   195   by (induct rs1) (auto)

   196 

   197 

   198 fun

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

   200 where

   201   "bder c (AZERO) = AZERO"

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

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

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

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

   206      (if bnullable r1

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

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

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

   210 

   211 

   212 fun 

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

   214 where

   215   "bders r [] = r"

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

   217 

   218 lemma bders_append:

   219   "bders c (s1 @ s2) = bders (bders c s1) s2"

   220   apply(induct s1 arbitrary: c s2)

   221   apply(simp_all)

   222   done

   223 

   224 lemma bnullable_correctness:

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

   226   apply(induct r rule: erase.induct)

   227   apply(simp_all)

   228   done

   229 

   230 lemma erase_fuse:

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

   232   apply(induct r rule: erase.induct)

   233   apply(simp_all)

   234   done

   235 

   236 lemma erase_intern [simp]:

   237   shows "erase (intern r) = r"

   238   apply(induct r)

   239   apply(simp_all add: erase_fuse)

   240   done

   241 

   242 lemma erase_bder [simp]:

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

   244   apply(induct r rule: erase.induct)

   245   apply(simp_all add: erase_fuse bnullable_correctness)

   246   done

   247 

   248 lemma erase_bders [simp]:

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

   250   apply(induct s arbitrary: r )

   251   apply(simp_all)

   252   done

   253 

   254 lemma bnullable_fuse:

   255   shows "bnullable (fuse bs r) = bnullable r"

   256   apply(induct r arbitrary: bs)

   257   apply(auto)

   258   done

   259 

   260 lemma retrieve_encode_STARS:

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

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

   263   using assms

   264   apply(induct vs)

   265   apply(simp_all)

   266   done

   267 

   268 lemma retrieve_fuse2:

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

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

   271   using assms

   272   apply(induct r arbitrary: v bs)

   273   apply(auto elim: Prf_elims)[4]

   274   apply(case_tac x2a)

   275   apply(simp)

   276   using Prf_elims(1) apply blast

   277   apply(case_tac x2a)

   278   apply(simp)

   279   apply(simp)

   280   apply(case_tac list)

   281   apply(simp)

   282   apply(simp)

   283   apply (smt (verit, best) Prf_elims(3) append_assoc retrieve.simps(4) retrieve.simps(5))

   284   apply(simp)

   285   using retrieve_encode_STARS

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

   287   apply(case_tac vs)

   288   apply(simp)

   289   apply(simp)

   290   done

   291 

   292 lemma retrieve_fuse:

   293   assumes "\<Turnstile> v : r"

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

   295   using assms 

   296   by (simp_all add: retrieve_fuse2)

   297 

   298 

   299 lemma retrieve_code:

   300   assumes "\<Turnstile> v : r"

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

   302   using assms

   303   apply(induct v r )

   304   apply(simp_all add: retrieve_fuse retrieve_encode_STARS)

   305   done

   306 

   307 

   308 lemma retrieve_AALTs_bnullable1:

   309   assumes "bnullable r"

   310   shows "retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs))))

   311          = bs @ retrieve r (mkeps (erase r))"

   312   using assms

   313   apply(case_tac rs)

   314   apply(auto simp add: bnullable_correctness)

   315   done

   316 

   317 lemma retrieve_AALTs_bnullable2:

   318   assumes "\<not>bnullable r" "bnullables rs"

   319   shows "retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs))))

   320          = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))"

   321   using assms

   322   apply(induct rs arbitrary: r bs)

   323   apply(auto)

   324   using bnullable_correctness apply blast

   325   apply(case_tac rs)

   326   apply(auto)

   327   using bnullable_correctness apply blast

   328   apply(case_tac rs)

   329   apply(auto)

   330   done

   331 

   332 lemma bmkeps_retrieve_AALTs: 

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

   334           "bnullables rs"

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

   336  using assms

   337   apply(induct rs arbitrary: bs)

   338   apply(auto)

   339   using retrieve_AALTs_bnullable1 apply presburger

   340   apply (metis retrieve_AALTs_bnullable2)

   341   apply (simp add: retrieve_AALTs_bnullable1)

   342   by (metis retrieve_AALTs_bnullable2)

   343 

   344     

   345 lemma bmkeps_retrieve:

   346   assumes "bnullable r"

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

   348   using assms

   349   apply(induct r)

   350   apply(auto)  

   351   using bmkeps_retrieve_AALTs by auto

   352 

   353 lemma bder_retrieve:

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

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

   356   using assms  

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

   358   using Prf_elims(1) apply auto[1]

   359   using Prf_elims(1) apply auto[1]

   360   apply(auto)[1]

   361   apply (metis Prf_elims(4) injval.simps(1) retrieve.simps(1) retrieve.simps(2))

   362   using Prf_elims(1) apply blast

   363   (* AALTs case *)

   364   apply(simp)

   365   apply(erule Prf_elims)

   366   apply(simp)

   367   apply(simp)

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

   369   apply(erule Prf_elims)

   370   apply(simp)

   371   apply(simp)

   372   apply(case_tac rs)

   373   apply(simp)

   374   apply(simp)

   375   using Prf_elims(3) apply fastforce

   376   (* ASEQ case *) 

   377   apply(simp)

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

   379   apply(simp)

   380   apply(erule Prf_elims)

   381   using Prf_elims(2) bnullable_correctness apply force

   382   apply (simp add: bmkeps_retrieve bnullable_correctness retrieve_fuse2)

   383   apply (simp add: bmkeps_retrieve bnullable_correctness retrieve_fuse2)

   384   using Prf_elims(2) apply force

   385   (* ASTAR case *)  

   386   apply(rename_tac bs r v)

   387   apply(simp)  

   388   apply(erule Prf_elims)

   389   apply(clarify)

   390   apply(erule Prf_elims)

   391   apply(clarify)

   392   by (simp add: retrieve_fuse2)

   393 

   394 

   395 lemma MAIN_decode:

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

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

   398   using assms

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

   400   case Nil

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

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

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

   404     using decode_code retrieve_code by auto

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

   406     by simp

   407 next

   408   case (snoc c s v)

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

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

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

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

   413     by (simp add: Prf_injval ders_append)

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

   415     by (simp add: flex_append)

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

   417     using asm2 IH by simp

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

   419     using asm by (simp_all add: bder_retrieve ders_append)

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

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

   422 qed

   423 

   424 definition blexer where

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

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

   427 

   428 lemma blexer_correctness:

   429   shows "blexer r s = lexer r s"

   430 proof -

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

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

   433     assume asm: "nullable ds"

   434     have era: "erase bds = ds" 

   435       unfolding ds_def bds_def by simp

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

   437       using asm by (simp add: mkeps_nullable)

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

   439       using bmkeps_retrieve

   440       using asm era

   441       using bnullable_correctness by force 

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

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

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

   445       unfolding bds_def ds_def .

   446   }

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

   448     unfolding blexer_def lexer_flex

   449     by (auto simp add: bnullable_correctness[symmetric])

   450 qed

   451 

   452 

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

   454   where

   455   "distinctBy [] f acc = []"

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

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

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

   459 

   460   

   461 

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

   463   where 

   464   "flts [] = []"

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

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

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

   468 

   469 

   470 

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

   472   where

   473   "bsimp_ASEQ _ AZERO _ = AZERO"

   474 | "bsimp_ASEQ _ _ AZERO = AZERO"

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

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

   477 

   478 lemma bsimp_ASEQ0[simp]:

   479   shows "bsimp_ASEQ bs r1 AZERO = AZERO"

   480   by (case_tac r1)(simp_all)

   481 

   482 lemma bsimp_ASEQ1:

   483   assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<nexists>bs. r1 = AONE bs"

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

   485   using assms

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

   487   apply(auto)

   488   done

   489 

   490 lemma bsimp_ASEQ2[simp]:

   491   shows "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2"

   492   by (case_tac r2) (simp_all)

   493 

   494 

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

   496   where

   497   "bsimp_AALTs _ [] = AZERO"

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

   499 | "bsimp_AALTs bs1 rs = AALTs bs1 rs"

   500 

   501 

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

   503   where

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

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

   506 | "bsimp r = r"

   507 

   508 

   509 fun 

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

   511 where

   512   "bders_simp r [] = r"

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

   514 

   515 definition blexer_simp where

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

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

   518 

   519 

   520 

   521 lemma bders_simp_append:

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

   523   apply(induct s1 arbitrary: r s2)

   524   apply(simp_all)

   525   done

   526 

   527 

   528 lemma bmkeps_fuse:

   529   assumes "bnullable r"

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

   531   using assms

   532   by (metis bmkeps_retrieve bnullable_correctness erase_fuse mkeps_nullable retrieve_fuse2)

   533 

   534 lemma bmkepss_fuse: 

   535   assumes "bnullables rs"

   536   shows "bmkepss (map (fuse bs) rs) = bs @ bmkepss rs"

   537   using assms

   538   apply(induct rs arbitrary: bs)

   539   apply(auto simp add: bmkeps_fuse bnullable_fuse)

   540   done

   541 

   542 lemma bder_fuse:

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

   544   apply(induct a arbitrary: bs c)

   545   apply(simp_all)

   546   done

   547 

   548 

   549 

   550 

   551 inductive 

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

   553 and 

   554   srewrite:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ s\<leadsto> _" [100, 100] 100)

   555 where

   556   bs1: "ASEQ bs AZERO r2 \<leadsto> AZERO"

   557 | bs2: "ASEQ bs r1 AZERO \<leadsto> AZERO"

   558 | bs3: "ASEQ bs1 (AONE bs2) r \<leadsto> fuse (bs1@bs2) r"

   559 | bs4: "r1 \<leadsto> r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r2 r3"

   560 | bs5: "r3 \<leadsto> r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r1 r4"

   561 | bs6: "AALTs bs [] \<leadsto> AZERO"

   562 | bs7: "AALTs bs [r] \<leadsto> fuse bs r"

   563 | bs8: "rs1 s\<leadsto> rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto> AALTs bs rs2"

   564 (*| ss1:  "[] s\<leadsto> []"*)

   565 | ss2:  "rs1 s\<leadsto> rs2 \<Longrightarrow> (r # rs1) s\<leadsto> (r # rs2)"

   566 | ss3:  "r1 \<leadsto> r2 \<Longrightarrow> (r1 # rs) s\<leadsto> (r2 # rs)"

   567 | ss4:  "(AZERO # rs) s\<leadsto> rs"

   568 | ss5:  "(AALTs bs1 rs1 # rsb) s\<leadsto> ((map (fuse bs1) rs1) @ rsb)"

   569 | ss6:  "erase a1 = erase a2 \<Longrightarrow> (rsa@[a1]@rsb@[a2]@rsc) s\<leadsto> (rsa@[a1]@rsb@rsc)"

   570 

   571 

   572 inductive 

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

   574 where 

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

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

   577 

   578 inductive 

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

   580 where 

   581   sss1[intro, simp]:"rs s\<leadsto>* rs"

   582 | sss2[intro]: "\<lbrakk>rs1 s\<leadsto> rs2; rs2 s\<leadsto>* rs3\<rbrakk> \<Longrightarrow> rs1 s\<leadsto>* rs3"

   583 

   584 

   585 lemma r_in_rstar: 

   586   shows "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"

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

   588 

   589 lemma rrewrites_trans[trans]: 

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

   591   shows "r1 \<leadsto>* r3"

   592   using a2 a1

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

   594   apply(auto)

   595   done

   596 

   597 lemma srewrites_trans[trans]: 

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

   599   shows "r1 s\<leadsto>* r3"

   600   using a1 a2

   601   apply(induct r1 r2 arbitrary: r3 rule: srewrites.induct) 

   602    apply(auto)

   603   done

   604 

   605 

   606 

   607 lemma contextrewrites0: 

   608   "rs1 s\<leadsto>* rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto>* AALTs bs rs2"

   609   apply(induct rs1 rs2 rule: srewrites.inducts)

   610    apply simp

   611   using bs8 r_in_rstar rrewrites_trans by blast

   612 

   613 lemma contextrewrites1: 

   614   "r \<leadsto>* r' \<Longrightarrow> AALTs bs (r # rs) \<leadsto>* AALTs bs (r' # rs)"

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

   616    apply simp

   617   using bs8 ss3 by blast

   618 

   619 lemma srewrite1: 

   620   shows "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs @ rs1) s\<leadsto> (rs @ rs2)"

   621   apply(induct rs)

   622    apply(auto)

   623   using ss2 by auto

   624 

   625 lemma srewrites1: 

   626   shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs @ rs1) s\<leadsto>* (rs @ rs2)"

   627   apply(induct rs1 rs2 rule: srewrites.induct)

   628    apply(auto)

   629   using srewrite1 by blast

   630 

   631 lemma srewrite2: 

   632   shows  "r1 \<leadsto> r2 \<Longrightarrow> True"

   633   and "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)"

   634   apply(induct rule: rrewrite_srewrite.inducts)

   635   apply(auto)

   636   apply (metis append_Cons append_Nil srewrites1)

   637   apply(meson srewrites.simps ss3)

   638   apply (meson srewrites.simps ss4)

   639   apply (meson srewrites.simps ss5)

   640   by (metis append_Cons append_Nil srewrites.simps ss6)

   641   

   642 

   643 lemma srewrites3: 

   644   shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)"

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

   646    apply(auto)

   647   by (meson srewrite2(2) srewrites_trans)

   648 

   649 (*

   650 lemma srewrites4:

   651   assumes "rs3 s\<leadsto>* rs4" "rs1 s\<leadsto>* rs2" 

   652   shows "(rs1 @ rs3) s\<leadsto>* (rs2 @ rs4)"

   653   using assms

   654   apply(induct rs3 rs4 arbitrary: rs1 rs2 rule: srewrites.induct)

   655   apply (simp add: srewrites3)

   656   using srewrite1 by blast

   657 *)

   658 

   659 lemma srewrites6:

   660   assumes "r1 \<leadsto>* r2" 

   661   shows "[r1] s\<leadsto>* [r2]"

   662   using assms

   663   apply(induct r1 r2 rule: rrewrites.induct)

   664   apply(auto)

   665   by (meson srewrites.simps srewrites_trans ss3)

   666 

   667 lemma srewrites7:

   668   assumes "rs3 s\<leadsto>* rs4" "r1 \<leadsto>* r2" 

   669   shows "(r1 # rs3) s\<leadsto>* (r2 # rs4)"

   670   using assms

   671   by (smt (verit, del_insts) append.simps srewrites1 srewrites3 srewrites6 srewrites_trans)

   672   

   673 lemma ss6_stronger_aux:

   674   shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ distinctBy rs2 erase (set (map erase rs1)))"

   675   apply(induct rs2 arbitrary: rs1)

   676    apply(auto)

   677   apply (smt (verit, best) append.assoc append.right_neutral append_Cons append_Nil split_list srewrite2(2) srewrites_trans ss6)

   678   apply(drule_tac x="rs1 @ [a]" in meta_spec)

   679   apply(simp)

   680   done

   681 

   682 lemma ss6_stronger:

   683   shows "rs1 s\<leadsto>* distinctBy rs1 erase {}"

   684   using ss6_stronger_aux[of "[]" _] by auto

   685 

   686 lemma rewrite_preserves_fuse: 

   687   shows "r2 \<leadsto> r3 \<Longrightarrow> fuse bs r2 \<leadsto> fuse bs r3"

   688   and   "rs2 s\<leadsto> rs3 \<Longrightarrow> map (fuse bs) rs2 s\<leadsto> map (fuse bs) rs3"

   689 proof(induct rule: rrewrite_srewrite.inducts)

   690   case (bs3 bs1 bs2 r)

   691   then show "fuse bs (ASEQ bs1 (AONE bs2) r) \<leadsto> fuse bs (fuse (bs1 @ bs2) r)"

   692     by (metis fuse.simps(5) fuse_append rrewrite_srewrite.bs3) 

   693 next

   694   case (bs7 bs1 r)

   695   then show "fuse bs (AALTs bs1 [r]) \<leadsto> fuse bs (fuse bs1 r)"

   696     by (metis fuse.simps(4) fuse_append rrewrite_srewrite.bs7) 

   697 next

   698   case (ss2 rs1 rs2 r)

   699   then show "map (fuse bs) (r # rs1) s\<leadsto> map (fuse bs) (r # rs2)"

   700     by (simp add: rrewrite_srewrite.ss2)

   701 next

   702   case (ss3 r1 r2 rs)

   703   then show "map (fuse bs) (r1 # rs) s\<leadsto> map (fuse bs) (r2 # rs)"

   704     by (simp add: rrewrite_srewrite.ss3)

   705 next

   706   case (ss5 bs1 rs1 rsb)

   707   have "map (fuse bs) (AALTs bs1 rs1 # rsb) = AALTs (bs @ bs1) rs1 # (map (fuse bs) rsb)" by simp

   708   also have "... s\<leadsto> ((map (fuse (bs @ bs1)) rs1) @ (map (fuse bs) rsb))"

   709     by (simp add: rrewrite_srewrite.ss5)  

   710   finally show "map (fuse bs) (AALTs bs1 rs1 # rsb) s\<leadsto> map (fuse bs) (map (fuse bs1) rs1 @ rsb)"

   711     by (simp add: comp_def fuse_append)

   712 next

   713   case (ss6 a1 a2 rsa rsb rsc)

   714   then show "map (fuse bs) (rsa @ [a1] @ rsb @ [a2] @ rsc) s\<leadsto> map (fuse bs) (rsa @ [a1] @ rsb @ rsc)"

   715     apply(simp)

   716     apply(rule rrewrite_srewrite.ss6[simplified])

   717     apply(simp add: erase_fuse)

   718     done

   719 qed (auto intro: rrewrite_srewrite.intros)

   720 

   721 lemma rewrites_fuse:  

   722   assumes "r1 \<leadsto>* r2"

   723   shows "fuse bs r1 \<leadsto>* fuse bs r2"

   724 using assms

   725 apply(induction r1 r2 arbitrary: bs rule: rrewrites.induct)

   726 apply(auto intro: rewrite_preserves_fuse)

   727 done

   728 

   729 

   730 lemma star_seq:  

   731   assumes "r1 \<leadsto>* r2"

   732   shows "ASEQ bs r1 r3 \<leadsto>* ASEQ bs r2 r3"

   733 using assms

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

   735 apply(auto intro: rrewrite_srewrite.intros)

   736 done

   737 

   738 lemma star_seq2:  

   739   assumes "r3 \<leadsto>* r4"

   740   shows "ASEQ bs r1 r3 \<leadsto>* ASEQ bs r1 r4"

   741   using assms

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

   743 apply(auto intro: rrewrite_srewrite.intros)

   744 done

   745 

   746 lemma continuous_rewrite: 

   747   assumes "r1 \<leadsto>* AZERO"

   748   shows "ASEQ bs1 r1 r2 \<leadsto>* AZERO"

   749 using assms bs1 star_seq by blast

   750 

   751 (*

   752 lemma continuous_rewrite2: 

   753   assumes "r1 \<leadsto>* AONE bs"

   754   shows "ASEQ bs1 r1 r2 \<leadsto>* (fuse (bs1 @ bs) r2)"

   755   using assms  by (meson bs3 rrewrites.simps star_seq)

   756 *)

   757 

   758 lemma bsimp_aalts_simpcases: 

   759   shows "AONE bs \<leadsto>* bsimp (AONE bs)"  

   760   and   "AZERO \<leadsto>* bsimp AZERO" 

   761   and   "ACHAR bs c \<leadsto>* bsimp (ACHAR bs c)"

   762   by (simp_all)

   763 

   764 lemma bsimp_AALTs_rewrites: 

   765   shows "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs"

   766   by (smt (verit) bs6 bs7 bsimp_AALTs.elims rrewrites.simps)

   767 

   768 lemma trivialbsimp_srewrites: 

   769   assumes "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x"

   770   shows "rs s\<leadsto>* (map f rs)"

   771 using assms

   772   apply(induction rs)

   773   apply(simp_all add: srewrites7)

   774   done

   775 

   776 lemma fltsfrewrites: "rs s\<leadsto>* flts rs"

   777   apply(induction rs rule: flts.induct)

   778   apply(auto intro: rrewrite_srewrite.intros)

   779   apply (meson srewrites.simps srewrites1 ss5)

   780   using rs1 srewrites7 apply presburger

   781   using srewrites7 apply force

   782   apply (simp add: srewrites7)

   783   by (simp add: srewrites7)

   784 

   785 lemma bnullable0:

   786 shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 = bnullable r2" 

   787   and "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 = bnullables rs2" 

   788   apply(induct rule: rrewrite_srewrite.inducts)

   789   apply(auto simp add:  bnullable_fuse)

   790   apply (meson UnCI bnullable_fuse imageI)

   791   by (metis bnullable_correctness)

   792 

   793 

   794 lemma rewrites_bnullable_eq: 

   795   assumes "r1 \<leadsto>* r2" 

   796   shows "bnullable r1 = bnullable r2"

   797 using assms 

   798   apply(induction r1 r2 rule: rrewrites.induct)

   799   apply simp

   800   using bnullable0(1) by auto

   801 

   802 lemma rewrite_bmkeps_aux: 

   803   shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 \<Longrightarrow> bmkeps r1 = bmkeps r2"

   804   and   "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 \<Longrightarrow> bmkepss rs1 = bmkepss rs2" 

   805 proof (induct rule: rrewrite_srewrite.inducts)

   806   case (bs3 bs1 bs2 r)

   807   have IH2: "bnullable (ASEQ bs1 (AONE bs2) r)" by fact

   808   then show "bmkeps (ASEQ bs1 (AONE bs2) r) = bmkeps (fuse (bs1 @ bs2) r)"

   809     by (simp add: bmkeps_fuse)

   810 next

   811   case (bs7 bs r)

   812   have IH2: "bnullable (AALTs bs [r])" by fact

   813   then show "bmkeps (AALTs bs [r]) = bmkeps (fuse bs r)" 

   814     by (simp add: bmkeps_fuse)

   815 next

   816   case (ss3 r1 r2 rs)

   817   have IH1: "bnullable r1 \<Longrightarrow> bmkeps r1 = bmkeps r2" by fact

   818   have as: "r1 \<leadsto> r2" by fact

   819   from IH1 as show "bmkepss (r1 # rs) = bmkepss (r2 # rs)"

   820     by (simp add: bnullable0)

   821 next

   822   case (ss5 bs1 rs1 rsb)

   823   have "bnullables (AALTs bs1 rs1 # rsb)" by fact

   824   then show "bmkepss (AALTs bs1 rs1 # rsb) = bmkepss (map (fuse bs1) rs1 @ rsb)"

   825     by (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse)

   826 next

   827   case (ss6 a1 a2 rsa rsb rsc)

   828   have as1: "erase a1 = erase a2" by fact

   829   have as3: "bnullables (rsa @ [a1] @ rsb @ [a2] @ rsc)" by fact

   830   show "bmkepss (rsa @ [a1] @ rsb @ [a2] @ rsc) = bmkepss (rsa @ [a1] @ rsb @ rsc)" using as1 as3

   831     by (smt (verit, best) append_Cons bmkeps.simps(3) bmkepss.simps(2) bmkepss1 bmkepss2 bnullable_correctness)

   832 qed (auto)

   833 

   834 lemma rewrites_bmkeps: 

   835   assumes "r1 \<leadsto>* r2" "bnullable r1" 

   836   shows "bmkeps r1 = bmkeps r2"

   837   using assms

   838 proof(induction r1 r2 rule: rrewrites.induct)

   839   case (rs1 r)

   840   then show "bmkeps r = bmkeps r" by simp

   841 next

   842   case (rs2 r1 r2 r3)

   843   then have IH: "bmkeps r1 = bmkeps r2" by simp

   844   have a1: "bnullable r1" by fact

   845   have a2: "r1 \<leadsto>* r2" by fact

   846   have a3: "r2 \<leadsto> r3" by fact

   847   have a4: "bnullable r2" using a1 a2 by (simp add: rewrites_bnullable_eq) 

   848   then have "bmkeps r2 = bmkeps r3"

   849     using a3 bnullable0(1) rewrite_bmkeps_aux(1) by blast 

   850   then show "bmkeps r1 = bmkeps r3" using IH by simp

   851 qed

   852 

   853 

   854 lemma rewrites_to_bsimp: 

   855   shows "r \<leadsto>* bsimp r"

   856 proof (induction r rule: bsimp.induct)

   857   case (1 bs1 r1 r2)

   858   have IH1: "r1 \<leadsto>* bsimp r1" by fact

   859   have IH2: "r2 \<leadsto>* bsimp r2" by fact

   860   { assume as: "bsimp r1 = AZERO \<or> bsimp r2 = AZERO"

   861     with IH1 IH2 have "r1 \<leadsto>* AZERO \<or> r2 \<leadsto>* AZERO" by auto

   862     then have "ASEQ bs1 r1 r2 \<leadsto>* AZERO"

   863       by (metis bs2 continuous_rewrite rrewrites.simps star_seq2)  

   864     then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" using as by auto

   865   }

   866   moreover

   867   { assume "\<exists>bs. bsimp r1 = AONE bs"

   868     then obtain bs where as: "bsimp r1 = AONE bs" by blast

   869     with IH1 have "r1 \<leadsto>* AONE bs" by simp

   870     then have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) r2" using bs3 star_seq by blast

   871     with IH2 have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) (bsimp r2)"

   872       using rewrites_fuse by (meson rrewrites_trans) 

   873     then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 (AONE bs) r2)" by simp

   874     then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by (simp add: as) 

   875   } 

   876   moreover

   877   { assume as1: "bsimp r1 \<noteq> AZERO" "bsimp r2 \<noteq> AZERO" and as2: "(\<nexists>bs. bsimp r1 = AONE bs)" 

   878     then have "bsimp_ASEQ bs1 (bsimp r1) (bsimp r2) = ASEQ bs1 (bsimp r1) (bsimp r2)" 

   879       by (simp add: bsimp_ASEQ1) 

   880     then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)" using as1 as2 IH1 IH2

   881       by (metis rrewrites_trans star_seq star_seq2) 

   882     then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by simp

   883   } 

   884   ultimately show "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by blast

   885 next

   886   case (2 bs1 rs)

   887   have IH: "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimp x" by fact

   888   then have "rs s\<leadsto>* (map bsimp rs)" by (simp add: trivialbsimp_srewrites)

   889   also have "... s\<leadsto>* flts (map bsimp rs)" by (simp add: fltsfrewrites) 

   890   also have "... s\<leadsto>* distinctBy (flts (map bsimp rs)) erase {}" by (simp add: ss6_stronger) 

   891   finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {})"

   892     using contextrewrites0 by blast

   893   also have "... \<leadsto>* bsimp_AALTs  bs1 (distinctBy (flts (map bsimp rs)) erase {})"

   894     by (simp add: bsimp_AALTs_rewrites)     

   895   finally show "AALTs bs1 rs \<leadsto>* bsimp (AALTs bs1 rs)" by simp

   896 qed (simp_all)

   897 

   898 

   899 lemma to_zero_in_alt: 

   900   shows "AALT bs (ASEQ [] AZERO r) r2 \<leadsto> AALT bs AZERO r2"

   901   by (simp add: bs1 bs8 ss3)

   902 

   903 

   904 

   905 lemma  bder_fuse_list: 

   906   shows "map (bder c \<circ> fuse bs1) rs1 = map (fuse bs1 \<circ> bder c) rs1"

   907   apply(induction rs1)

   908   apply(simp_all add: bder_fuse)

   909   done

   910 

   911 lemma rewrite_preserves_bder: 

   912   shows "r1 \<leadsto> r2 \<Longrightarrow> bder c r1 \<leadsto>* bder c r2"

   913   and   "rs1 s\<leadsto> rs2 \<Longrightarrow> map (bder c) rs1 s\<leadsto>* map (bder c) rs2"

   914 proof(induction rule: rrewrite_srewrite.inducts)

   915   case (bs1 bs r2)

   916   show "bder c (ASEQ bs AZERO r2) \<leadsto>* bder c AZERO"

   917     by (simp add: continuous_rewrite) 

   918 next

   919   case (bs2 bs r1)

   920   show "bder c (ASEQ bs r1 AZERO) \<leadsto>* bder c AZERO"

   921     apply(auto)

   922     apply (meson bs6 contextrewrites0 rrewrite_srewrite.bs2 rs2 ss3 ss4 sss1 sss2)

   923     by (simp add: r_in_rstar rrewrite_srewrite.bs2)

   924 next

   925   case (bs3 bs1 bs2 r)

   926   show "bder c (ASEQ bs1 (AONE bs2) r) \<leadsto>* bder c (fuse (bs1 @ bs2) r)"

   927     apply(simp)

   928     by (metis (no_types, lifting) bder_fuse bs8 bs7 fuse_append rrewrites.simps ss4 to_zero_in_alt)

   929 next

   930   case (bs4 r1 r2 bs r3)

   931   have as: "r1 \<leadsto> r2" by fact

   932   have IH: "bder c r1 \<leadsto>* bder c r2" by fact

   933   from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r2 r3)"

   934     by (metis bder.simps(5) bnullable0(1) contextrewrites1 rewrite_bmkeps_aux(1) star_seq)

   935 next

   936   case (bs5 r3 r4 bs r1)

   937   have as: "r3 \<leadsto> r4" by fact 

   938   have IH: "bder c r3 \<leadsto>* bder c r4" by fact 

   939   from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r1 r4)"

   940     apply(simp)

   941     apply(auto)

   942     using contextrewrites0 r_in_rstar rewrites_fuse srewrites6 srewrites7 star_seq2 apply presburger

   943     using star_seq2 by blast

   944 next

   945   case (bs6 bs)

   946   show "bder c (AALTs bs []) \<leadsto>* bder c AZERO"

   947     using rrewrite_srewrite.bs6 by force 

   948 next

   949   case (bs7 bs r)

   950   show "bder c (AALTs bs [r]) \<leadsto>* bder c (fuse bs r)"

   951     by (simp add: bder_fuse r_in_rstar rrewrite_srewrite.bs7) 

   952 next

   953   case (bs8 rs1 rs2 bs)

   954   have IH1: "map (bder c) rs1 s\<leadsto>* map (bder c) rs2" by fact

   955   then show "bder c (AALTs bs rs1) \<leadsto>* bder c (AALTs bs rs2)" 

   956     using contextrewrites0 by force    

   957 (*next

   958   case ss1

   959   show "map (bder c) [] s\<leadsto>* map (bder c) []" by simp*)

   960 next

   961   case (ss2 rs1 rs2 r)

   962   have IH1: "map (bder c) rs1 s\<leadsto>* map (bder c) rs2" by fact

   963   then show "map (bder c) (r # rs1) s\<leadsto>* map (bder c) (r # rs2)"

   964     by (simp add: srewrites7) 

   965 next

   966   case (ss3 r1 r2 rs)

   967   have IH: "bder c r1 \<leadsto>* bder c r2" by fact

   968   then show "map (bder c) (r1 # rs) s\<leadsto>* map (bder c) (r2 # rs)"

   969     by (simp add: srewrites7) 

   970 next

   971   case (ss4 rs)

   972   show "map (bder c) (AZERO # rs) s\<leadsto>* map (bder c) rs"

   973     using rrewrite_srewrite.ss4 by fastforce 

   974 next

   975   case (ss5 bs1 rs1 rsb)

   976   show "map (bder c) (AALTs bs1 rs1 # rsb) s\<leadsto>* map (bder c) (map (fuse bs1) rs1 @ rsb)"

   977     apply(simp)

   978     using bder_fuse_list map_map rrewrite_srewrite.ss5 srewrites.simps by blast

   979 next

   980   case (ss6 a1 a2 bs rsa rsb)

   981   have as: "erase a1 = erase a2" by fact

   982   show "map (bder c) (bs @ [a1] @ rsa @ [a2] @ rsb) s\<leadsto>* map (bder c) (bs @ [a1] @ rsa @ rsb)"

   983     apply(simp only: map_append)

   984     by (smt (verit, best) erase_bder list.simps(8) list.simps(9) as rrewrite_srewrite.ss6 srewrites.simps)

   985 qed

   986 

   987 lemma rewrites_preserves_bder: 

   988   assumes "r1 \<leadsto>* r2"

   989   shows "bder c r1 \<leadsto>* bder c r2"

   990 using assms  

   991 apply(induction r1 r2 rule: rrewrites.induct)

   992 apply(simp_all add: rewrite_preserves_bder rrewrites_trans)

   993 done

   994 

   995 

   996 lemma central:  

   997   shows "bders r s \<leadsto>* bders_simp r s"

   998 proof(induct s arbitrary: r rule: rev_induct)

   999   case Nil

  1000   then show "bders r [] \<leadsto>* bders_simp r []" by simp

  1001 next

  1002   case (snoc x xs)

  1003   have IH: "\<And>r. bders r xs \<leadsto>* bders_simp r xs" by fact

  1004   have "bders r (xs @ [x]) = bders (bders r xs) [x]" by (simp add: bders_append)

  1005   also have "... \<leadsto>* bders (bders_simp r xs) [x]" using IH

  1006     by (simp add: rewrites_preserves_bder)

  1007   also have "... \<leadsto>* bders_simp (bders_simp r xs) [x]" using IH

  1008     by (simp add: rewrites_to_bsimp)

  1009   finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])" 

  1010     by (simp add: bders_simp_append)

  1011 qed

  1012 

  1013 lemma main_aux: 

  1014   assumes "bnullable (bders r s)"

  1015   shows "bmkeps (bders r s) = bmkeps (bders_simp r s)"

  1016 proof -

  1017   have "bders r s \<leadsto>* bders_simp r s" by (rule central)

  1018   then 

  1019   show "bmkeps (bders r s) = bmkeps (bders_simp r s)" using assms

  1020     by (rule rewrites_bmkeps)

  1021 qed  

  1022 

  1023 

  1024 theorem main_blexer_simp: 

  1025   shows "blexer r s = blexer_simp r s"

  1026   unfolding blexer_def blexer_simp_def

  1027   by (metis central main_aux rewrites_bnullable_eq)

  1028 

  1029 

  1030 theorem blexersimp_correctness: 

  1031   shows "lexer r s = blexer_simp r s"

  1032   using blexer_correctness main_blexer_simp by simp

  1033 

  1034 

  1035 (* some tests *)

  1036 

  1037 lemma asize_fuse:

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

  1039   apply(induct r arbitrary: bs)

  1040   apply(auto)

  1041   done

  1042 

  1043 lemma asize_rewrite2:

  1044   shows "r1 \<leadsto> r2 \<Longrightarrow> asize r1 \<ge> asize r2"

  1045   and   "rs1 s\<leadsto> rs2 \<Longrightarrow> (sum_list (map asize rs1)) \<ge> (sum_list (map asize rs2))"

  1046    apply(induct rule: rrewrite_srewrite.inducts)

  1047    apply(auto simp add: asize_fuse comp_def)

  1048   done

  1049 

  1050 lemma asize_rrewrites:

  1051   assumes "r1 \<leadsto>* r2"

  1052   shows "asize r1 \<ge> asize r2"

  1053   using assms

  1054   apply(induct rule: rrewrites.induct)

  1055    apply(auto)

  1056   using asize_rewrite2(1) le_trans by blast

  1057   

  1058 

  1059 

  1060 fun asize2 :: "arexp \<Rightarrow> nat" where

  1061   "asize2 AZERO = 1"

  1062 | "asize2 (AONE cs) = 1" 

  1063 | "asize2 (ACHAR cs c) = 1"

  1064 | "asize2 (AALTs cs rs) = Suc (Suc (sum_list (map asize2 rs)))"

  1065 | "asize2 (ASEQ cs r1 r2) = Suc (asize2 r1 + asize2 r2)"

  1066 | "asize2 (ASTAR cs r) = Suc (asize2 r)"

  1067 

  1068 

  1069 lemma asize2_fuse:

  1070   shows "asize2 (fuse bs r) = asize2 r"

  1071   apply(induct r arbitrary: bs)

  1072   apply(auto)

  1073   done

  1074 

  1075 lemma asize2_not_zero:

  1076   shows "0 < asize2 r"

  1077   apply(induct r)

  1078   apply(auto)

  1079   done

  1080 

  1081 lemma asize_rewrite:

  1082   shows "r1 \<leadsto> r2 \<Longrightarrow> asize2 r1 > asize2 r2"

  1083   and   "rs1 s\<leadsto> rs2 \<Longrightarrow> (sum_list (map asize2 rs1)) > (sum_list (map asize2 rs2))"

  1084    apply(induct rule: rrewrite_srewrite.inducts)

  1085    apply(auto simp add: asize2_fuse comp_def)

  1086   apply(simp add: asize2_not_zero) 

  1087   done

  1088 

  1089 lemma asize2_bsimp_ASEQ:

  1090   shows "asize2 (bsimp_ASEQ bs r1 r2) \<le> Suc (asize2 r1 + asize2 r2)"

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

  1092   apply(auto)

  1093   done

  1094 

  1095 lemma asize2_bsimp_AALTs:

  1096   shows "asize2 (bsimp_AALTs bs rs) \<le> Suc (Suc (sum_list (map asize2 rs)))"

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

  1098   apply(auto simp add: asize2_fuse)

  1099   done

  1100 

  1101 lemma distinctBy_asize2:

  1102   shows "sum_list (map asize2 (distinctBy rs f acc)) \<le> sum_list (map asize2 rs)"

  1103   apply(induct rs f acc rule: distinctBy.induct)

  1104   apply(auto)

  1105   done

  1106 

  1107 lemma flts_asize2:

  1108   shows "sum_list (map asize2 (flts rs)) \<le> sum_list (map asize2 rs)"

  1109   apply(induct rs rule: flts.induct)

  1110   apply(auto simp add: comp_def asize2_fuse)

  1111   done

  1112 

  1113 lemma sumlist_asize2:

  1114   assumes "\<And>x. x \<in> set rs \<Longrightarrow> asize2 (f x) \<le> asize2 x"

  1115   shows "sum_list (map asize2 (map f rs)) \<le> sum_list (map asize2 rs)"

  1116   using assms

  1117   apply(induct rs)

  1118    apply(auto simp add: comp_def)

  1119   by (simp add: add_le_mono)

  1120 

  1121 lemma test0:

  1122   assumes "r1 \<leadsto>* r2"

  1123   shows "r1 = r2 \<or> (\<exists>r3. r1 \<leadsto> r3 \<and> r3 \<leadsto>* r2)"

  1124   using assms

  1125   apply(induct r1 r2 rule: rrewrites.induct)

  1126    apply(auto)

  1127   done

  1128 

  1129 lemma test2:

  1130   assumes "r1 \<leadsto>* r2"

  1131   shows "asize2 r1 \<ge> asize2 r2"

  1132 using assms

  1133   apply(induct r1 r2 rule: rrewrites.induct)

  1134   apply(auto)

  1135   using asize_rewrite(1) by fastforce