1 

     2 theory SizeBound3

     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 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 lemma fuse_Nil:

   136   shows "fuse [] r = r"

   137   by (induct r)(simp_all)

   138 

   139 (*

   140 lemma map_fuse_Nil:

   141   shows "map (fuse []) rs = rs"

   142   by (induct rs)(simp_all add: fuse_Nil)

   143 *)

   144 

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

   146   "intern ZERO = AZERO"

   147 | "intern ONE = AONE []"

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

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

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

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

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

   153 

   154 

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

   156   "retrieve (AONE bs) Void = bs"

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

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

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

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

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

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

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

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

   165 

   166 

   167 

   168 fun

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

   170 where

   171   "bnullable (AZERO) = False"

   172 | "bnullable (AONE bs) = True"

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

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

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

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

   177 

   178 abbreviation

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

   180 where

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

   182 

   183 fun 

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

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

   186 where

   187   "bmkeps(AONE bs) = bs"

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

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

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

   191 | "bmkepss [] = []"

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

   193 

   194 lemma bmkepss1:

   195   assumes "\<not> bnullables rs1"

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

   197   using assms

   198   by (induct rs1) (auto)

   199 

   200 lemma bmkepss2:

   201   assumes "bnullables rs1"

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

   203   using assms

   204   by (induct rs1) (auto)

   205 

   206 

   207 fun

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

   209 where

   210   "bder c (AZERO) = AZERO"

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

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

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

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

   215      (if bnullable r1

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

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

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

   219 

   220 

   221 fun 

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

   223 where

   224   "bders r [] = r"

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

   226 

   227 lemma bders_append:

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

   229   apply(induct s1 arbitrary: r s2)

   230   apply(simp_all)

   231   done

   232 

   233 lemma bnullable_correctness:

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

   235   apply(induct r rule: erase.induct)

   236   apply(simp_all)

   237   done

   238 

   239 lemma erase_fuse:

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

   241   apply(induct r rule: erase.induct)

   242   apply(simp_all)

   243   done

   244 

   245 lemma erase_intern [simp]:

   246   shows "erase (intern r) = r"

   247   apply(induct r)

   248   apply(simp_all add: erase_fuse)

   249   done

   250 

   251 lemma erase_bder [simp]:

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

   253   apply(induct r rule: erase.induct)

   254   apply(simp_all add: erase_fuse bnullable_correctness)

   255   done

   256 

   257 lemma erase_bders [simp]:

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

   259   apply(induct s arbitrary: r )

   260   apply(simp_all)

   261   done

   262 

   263 lemma bnullable_fuse:

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

   265   apply(induct r arbitrary: bs)

   266   apply(auto)

   267   done

   268 

   269 lemma retrieve_encode_STARS:

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

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

   272   using assms

   273   apply(induct vs)

   274   apply(simp_all)

   275   done

   276 

   277 

   278 lemma retrieve_fuse2:

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

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

   281   using assms

   282   apply(induct r arbitrary: v bs)

   283          apply(auto elim: Prf_elims)[4]

   284    defer

   285   using retrieve_encode_STARS

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

   287    apply(case_tac vs)

   288     apply(simp)

   289    apply(simp)

   290   (* AALTs  case *)

   291   apply(simp)

   292   apply(case_tac x2a)

   293    apply(simp)

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

   295   apply(simp)

   296    apply(case_tac list)

   297    apply(simp)

   298   apply(auto)

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

   300   done

   301 

   302 lemma retrieve_fuse:

   303   assumes "\<Turnstile> v : r"

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

   305   using assms 

   306   by (simp_all add: retrieve_fuse2)

   307 

   308 

   309 lemma retrieve_code:

   310   assumes "\<Turnstile> v : r"

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

   312   using assms

   313   apply(induct v r )

   314   apply(simp_all add: retrieve_fuse retrieve_encode_STARS)

   315   done

   316 

   317 (*

   318 lemma bnullable_Hdbmkeps_Hd:

   319   assumes "bnullable a" 

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

   321   using assms by simp

   322 *)

   323 

   324 

   325 lemma r2:

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

   327   shows "bnullable (AALTs bs rs)"

   328   using assms

   329   apply(induct rs)

   330    apply(auto)

   331   done

   332 

   333 lemma  r3:

   334   assumes "\<not> bnullable r" 

   335           "bnullables rs"

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

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

   338   using assms

   339   apply(induct rs arbitrary: r bs)

   340    apply(auto)[1]

   341   apply(auto)

   342   using bnullable_correctness apply blast

   343     apply(auto simp add: bnullable_correctness mkeps_nullable retrieve_fuse2)

   344    apply(subst retrieve_fuse2[symmetric])

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

   346    apply(simp)

   347   apply(case_tac "bnullable a")

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

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

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

   351   apply(drule meta_mp)

   352    apply(simp)

   353   apply(drule meta_mp)

   354    apply(auto)

   355   apply(subst retrieve_fuse2[symmetric])

   356   apply(case_tac rs)

   357     apply(simp)

   358    apply(auto)[1]

   359       apply (simp add: bnullable_correctness)

   360   

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

   362     apply (simp add: bnullable_correctness)

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

   364   apply(simp)

   365   done

   366 

   367 lemma t: 

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

   369           "bnullables rs"

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

   371  using assms

   372   apply(induct rs arbitrary: bs)

   373   apply(auto)

   374   apply (metis (no_types, opaque_lifting) bmkepss.cases bnullable_correctness erase.simps(5) erase.simps(6) mkeps.simps(3) retrieve.simps(3) retrieve.simps(4))

   375   apply (metis r3)

   376   apply (metis (no_types, lifting) bmkepss.cases bnullable_correctness empty_iff erase.simps(6) list.set(1) mkeps.simps(3) retrieve.simps(4))

   377   apply (metis r3)

   378   done

   379       

   380 lemma bmkeps_retrieve:

   381   assumes "bnullable r"

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

   383   using assms

   384   apply(induct r)

   385   apply(auto)

   386   using t by auto

   387 

   388 lemma bder_retrieve:

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

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

   391   using assms  

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

   393          apply(simp)

   394          apply(erule Prf_elims)

   395         apply(simp)

   396         apply(erule Prf_elims) 

   397         apply(simp)

   398       apply(case_tac "c = ca")

   399        apply(simp)

   400        apply(erule Prf_elims)

   401        apply(simp)

   402       apply(simp)

   403        apply(erule Prf_elims)

   404   apply(simp)

   405       apply(erule Prf_elims)

   406      apply(simp)

   407     apply(simp)

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

   409     apply(erule Prf_elims)

   410      apply(simp)

   411     apply(simp)

   412     apply(case_tac rs)

   413      apply(simp)

   414     apply(simp)

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

   416    apply(simp)

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

   418     apply(simp)

   419   apply(erule Prf_elims)

   420      apply(subgoal_tac "bnullable r1")

   421   prefer 2

   422   using bnullable_correctness apply blast

   423     apply(simp)

   424      apply(erule Prf_elims)

   425      apply(simp)

   426    apply(subgoal_tac "bnullable r1")

   427   prefer 2

   428   using bnullable_correctness apply blast

   429     apply(simp)

   430     apply(simp add: retrieve_fuse2)

   431     apply(simp add: bmkeps_retrieve)

   432    apply(simp)

   433    apply(erule Prf_elims)

   434    apply(simp)

   435   using bnullable_correctness apply blast

   436   apply(rename_tac bs r v)

   437   apply(simp)

   438   apply(erule Prf_elims)

   439      apply(clarify)

   440   apply(erule Prf_elims)

   441   apply(clarify)

   442   apply(subst injval.simps)

   443   apply(simp del: retrieve.simps)

   444   apply(subst retrieve.simps)

   445   apply(subst retrieve.simps)

   446   apply(simp)

   447   apply(simp add: retrieve_fuse2)

   448   done

   449   

   450 

   451 

   452 lemma MAIN_decode:

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

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

   455   using assms

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

   457   case Nil

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

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

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

   461     using decode_code retrieve_code by auto

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

   463     by simp

   464 next

   465   case (snoc c s v)

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

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

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

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

   470     by (simp add: Prf_injval ders_append)

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

   472     by (simp add: flex_append)

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

   474     using asm2 IH by simp

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

   476     using asm by (simp_all add: bder_retrieve ders_append)

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

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

   479 qed

   480 

   481 definition blexer where

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

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

   484 

   485 lemma blexer_correctness:

   486   shows "blexer r s = lexer r s"

   487 proof -

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

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

   490     assume asm: "nullable ds"

   491     have era: "erase bds = ds" 

   492       unfolding ds_def bds_def by simp

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

   494       using asm by (simp add: mkeps_nullable)

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

   496       using bmkeps_retrieve

   497       using asm era

   498       using bnullable_correctness by force 

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

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

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

   502       unfolding bds_def ds_def .

   503   }

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

   505     unfolding blexer_def lexer_flex

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

   507 qed

   508 

   509 

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

   511   where

   512   "distinctBy [] f acc = []"

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

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

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

   516 

   517  

   518 

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

   520   where 

   521   "flts [] = []"

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

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

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

   525 

   526 

   527 

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

   529   where

   530   "bsimp_ASEQ _ AZERO _ = AZERO"

   531 | "bsimp_ASEQ _ _ AZERO = AZERO"

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

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

   534 

   535 lemma bsimp_ASEQ0[simp]:

   536   shows "bsimp_ASEQ bs r1 AZERO = AZERO"

   537   by (case_tac r1)(simp_all)

   538 

   539 lemma bsimp_ASEQ1:

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

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

   542   using assms

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

   544   apply(auto)

   545   done

   546 

   547 lemma bsimp_ASEQ2[simp]:

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

   549   by (case_tac r2) (simp_all)

   550 

   551 

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

   553   where

   554   "bsimp_AALTs _ [] = AZERO"

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

   556 | "bsimp_AALTs bs1 rs = AALTs bs1 rs"

   557 

   558 

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

   560   where

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

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

   563 | "bsimp r = r"

   564 

   565 

   566 fun 

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

   568 where

   569   "bders_simp r [] = r"

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

   571 

   572 definition blexer_simp where

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

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

   575 

   576 

   577 

   578 lemma bders_simp_append:

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

   580   apply(induct s1 arbitrary: r s2)

   581   apply(simp_all)

   582   done

   583 

   584 lemma L_bsimp_ASEQ:

   585   "L (erase (ASEQ bs r1 r2)) = L (erase (bsimp_ASEQ bs r1 r2))"

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

   587   apply(simp_all)

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

   589 

   590 lemma L_bsimp_AALTs:

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

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

   593   apply(simp_all add: erase_fuse)

   594   done

   595 

   596 lemma L_erase_AALTs:

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

   598   apply(induct rs)

   599    apply(simp)

   600   apply(simp)

   601   apply(case_tac rs)

   602    apply(simp)

   603   apply(simp)

   604   done

   605 

   606 lemma L_erase_flts:

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

   608   apply(induct rs rule: flts.induct)

   609   apply(simp_all)

   610   apply(auto)

   611   using L_erase_AALTs erase_fuse apply auto[1]

   612   by (simp add: L_erase_AALTs erase_fuse)

   613 

   614 lemma L_erase_dB_acc:

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

   616             = \<Union> (L ` acc) \<union>  \<Union> (L ` erase ` (set rs))"

   617   apply(induction rs arbitrary: acc)

   618   apply simp_all

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

   620 

   621 

   622 lemma L_erase_dB:

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

   624   by (metis L_erase_dB_acc Un_commute Union_image_empty)

   625 

   626 lemma L_bsimp_erase:

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

   628   apply(induct r)

   629   apply(simp)

   630   apply(simp)

   631   apply(simp)

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

   633   apply(subst L_bsimp_ASEQ[symmetric])

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

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

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

   637   apply(simp)

   638   apply(subst L_bsimp_AALTs[symmetric])

   639   defer

   640   apply(simp)

   641   apply(subst (2)L_erase_AALTs)  

   642   apply(subst L_erase_dB)

   643   apply(subst L_erase_flts)

   644   apply (simp add: L_erase_AALTs)

   645   done

   646 

   647 lemma L_bders_simp:

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

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

   650   apply(simp)

   651   apply(simp)

   652   apply(simp add: ders_append)

   653   apply(simp add: bders_simp_append)

   654   apply(simp add: L_bsimp_erase[symmetric])

   655   by (simp add: der_correctness)

   656 

   657 

   658 lemma bmkeps_fuse:

   659   assumes "bnullable r"

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

   661   by (metis assms bmkeps_retrieve bnullable_correctness erase_fuse mkeps_nullable retrieve_fuse2)

   662 

   663 lemma bmkepss_fuse: 

   664   assumes "bnullables rs"

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

   666   using assms

   667   apply(induct rs arbitrary: bs)

   668   apply(auto simp add: bmkeps_fuse bnullable_fuse)

   669   done

   670 

   671 

   672 lemma b4:

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

   674 proof -

   675   have "L (erase (bders_simp r s)) = L (erase (bders r s))"

   676     using L_bders_simp by force

   677   then show "bnullable (bders_simp r s) = bnullable (bders r s)"

   678     using bnullable_correctness nullable_correctness by blast

   679 qed

   680 

   681 

   682 lemma bder_fuse:

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

   684   apply(induct a arbitrary: bs c)

   685        apply(simp_all)

   686   done

   687 

   688 

   689 

   690 

   691 inductive 

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

   693 and 

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

   695 where

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

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

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

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

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

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

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

   703 | bs10: "rs1 s\<leadsto> rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto> AALTs bs rs2"

   704 | ss1:  "[] s\<leadsto> []"

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

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

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

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

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

   710 

   711 

   712 inductive 

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

   714 where 

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

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

   717 

   718 inductive 

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

   720 where 

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

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

   723 

   724 

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

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

   727  

   728 lemma rrewrites_trans[trans]: 

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

   730   shows "r1 \<leadsto>* r3"

   731   using a2 a1

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

   733   apply(auto)

   734   done

   735 

   736 lemma srewrites_trans[trans]: 

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

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

   739   using a1 a2

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

   741    apply(auto)

   742   done

   743 

   744 

   745 

   746 lemma contextrewrites0: 

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

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

   749    apply simp

   750   using bs10 r_in_rstar rrewrites_trans by blast

   751 

   752 lemma contextrewrites1: 

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

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

   755    apply simp

   756   using bs10 ss3 by blast

   757 

   758 lemma srewrite1: 

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

   760   apply(induct rs)

   761    apply(auto)

   762   using ss2 by auto

   763 

   764 lemma srewrites1: 

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

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

   767    apply(auto)

   768   using srewrite1 by blast

   769 

   770 lemma srewrite2: 

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

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

   773   apply(induct rule: rrewrite_srewrite.inducts)

   774                apply(auto)

   775      apply (metis append_Cons append_Nil srewrites1)

   776     apply(meson srewrites.simps ss3)

   777   apply (meson srewrites.simps ss4)

   778   apply (meson srewrites.simps ss5)

   779   by (metis append_Cons append_Nil srewrites.simps ss6)

   780   

   781 

   782 lemma srewrites3: 

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

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

   785    apply(auto)

   786   by (meson srewrite2(2) srewrites_trans)

   787 

   788 (*

   789 lemma srewrites4:

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

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

   792   using assms

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

   794   apply (simp add: srewrites3)

   795   using srewrite1 by blast

   796 *)

   797 

   798 lemma srewrites6:

   799   assumes "r1 \<leadsto>* r2" 

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

   801   using assms

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

   803    apply(auto)

   804   by (meson srewrites.simps srewrites_trans ss3)

   805 

   806 lemma srewrites7:

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

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

   809   using assms

   810   by (smt (verit, best) append_Cons append_Nil srewrites1 srewrites3 srewrites6 srewrites_trans)

   811 

   812 lemma ss6_stronger_aux:

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

   814   apply(induct rs2 arbitrary: rs1)

   815    apply(auto)

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

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

   818   apply(simp)

   819   done

   820 

   821 lemma ss6_stronger:

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

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

   824 

   825 

   826 lemma rewrite_preserves_fuse: 

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

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

   829 proof(induct rule: rrewrite_srewrite.inducts)

   830   case (bs3 bs1 bs2 r)

   831   then show ?case

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

   833 next

   834   case (bs7 bs r)

   835   then show ?case

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

   837 next

   838   case (ss2 rs1 rs2 r)

   839   then show ?case

   840     using srewrites7 by force 

   841 next

   842   case (ss3 r1 r2 rs)

   843   then show ?case by (simp add: r_in_rstar srewrites7)

   844 next

   845   case (ss5 bs1 rs1 rsb)

   846   then show ?case 

   847     apply(simp)

   848     by (metis (mono_tags, lifting) comp_def fuse_append map_eq_conv rrewrite_srewrite.ss5 srewrites.simps)

   849 next

   850   case (ss6 a1 a2 rsa rsb rsc)

   851   then show ?case 

   852     apply(simp only: map_append)

   853     by (smt (verit, ccfv_threshold) erase_fuse list.simps(8) list.simps(9) rrewrite_srewrite.ss6 srewrites.simps)  

   854 qed (auto intro: rrewrite_srewrite.intros)

   855 

   856 

   857 lemma rewrites_fuse:  

   858   assumes "r1 \<leadsto>* r2"

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

   860 using assms

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

   862 apply(auto intro: rewrite_preserves_fuse rrewrites_trans)

   863 done

   864 

   865 

   866 lemma star_seq:  

   867   assumes "r1 \<leadsto>* r2"

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

   869 using assms

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

   871 apply(auto intro: rrewrite_srewrite.intros)

   872 done

   873 

   874 lemma star_seq2:  

   875   assumes "r3 \<leadsto>* r4"

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

   877   using assms

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

   879 apply(auto intro: rrewrite_srewrite.intros)

   880 done

   881 

   882 lemma continuous_rewrite: 

   883   assumes "r1 \<leadsto>* AZERO"

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

   885 using assms bs1 star_seq by blast

   886 

   887 (*

   888 lemma continuous_rewrite2: 

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

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

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

   892 *)

   893 

   894 lemma bsimp_aalts_simpcases: 

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

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

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

   898   by (simp_all)

   899 

   900 lemma bsimp_AALTs_rewrites: 

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

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

   903 

   904 lemma trivialbsimp_srewrites: 

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

   906   apply(induction rs)

   907    apply simp

   908   apply(simp)

   909   using srewrites7 by auto

   910 

   911 

   912 

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

   914   apply(induction rs rule: flts.induct)

   915   apply(auto intro: rrewrite_srewrite.intros)

   916   apply (meson srewrites.simps srewrites1 ss5)

   917   using rs1 srewrites7 apply presburger

   918   using srewrites7 apply force

   919   apply (simp add: srewrites7)

   920   by (simp add: srewrites7)

   921 

   922 lemma bnullable0:

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

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

   925   apply(induct rule: rrewrite_srewrite.inducts)

   926   apply(auto simp add:  bnullable_fuse)

   927   apply (meson UnCI bnullable_fuse imageI)

   928   by (metis bnullable_correctness)

   929 

   930 

   931 lemma rewritesnullable: 

   932   assumes "r1 \<leadsto>* r2" 

   933   shows "bnullable r1 = bnullable r2"

   934 using assms 

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

   936   apply simp

   937   using bnullable0(1) by auto

   938 

   939 lemma rewrite_bmkeps_aux: 

   940   shows "r1 \<leadsto> r2 \<Longrightarrow> (bnullable r1 \<and> bnullable r2 \<Longrightarrow> bmkeps r1 = bmkeps r2)"

   941   and   "rs1 s\<leadsto> rs2 \<Longrightarrow> (bnullables rs1 \<and> bnullables rs2 \<Longrightarrow> bmkepss rs1 = bmkepss rs2)" 

   942 proof (induct rule: rrewrite_srewrite.inducts)

   943   case (bs3 bs1 bs2 r)

   944   then show ?case by (simp add: bmkeps_fuse) 

   945 next

   946   case (bs7 bs r)

   947   then show ?case by (simp add: bmkeps_fuse) 

   948 next

   949   case (ss3 r1 r2 rs)

   950   then show ?case

   951     by (metis bmkepss.simps(2) bnullable0(1))

   952 next

   953   case (ss5 bs1 rs1 rsb)

   954   then show ?case

   955     by (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse)

   956 next

   957   case (ss6 a1 a2 rsa rsb rsc)

   958   then show ?case

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

   960 qed (auto)

   961 

   962 lemma rewrites_bmkeps: 

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

   964   shows "bmkeps r1 = bmkeps r2"

   965   using assms

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

   967   case (rs1 r)

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

   969 next

   970   case (rs2 r1 r2 r3)

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

   972   have a1: "bnullable r1" by fact

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

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

   975   have a4: "bnullable r2" using a1 a2 by (simp add: rewritesnullable) 

   976   then have "bmkeps r2 = bmkeps r3"

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

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

   979 qed

   980 

   981 

   982 lemma rewrites_to_bsimp: 

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

   984 proof (induction r rule: bsimp.induct)

   985   case (1 bs1 r1 r2)

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

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

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

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

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

   991       by (metis bs2 continuous_rewrite rrewrites.simps star_seq2)  

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

   993   }

   994   moreover

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

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

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

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

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

  1000       using rewrites_fuse by (meson rrewrites_trans) 

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

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

  1003   } 

  1004   moreover

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

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

  1007       by (simp add: bsimp_ASEQ1) 

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

  1009       by (metis rrewrites_trans star_seq star_seq2) 

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

  1011   } 

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

  1013 next

  1014   case (2 bs1 rs)

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

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

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

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

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

  1020     using contextrewrites0 by blast

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

  1022     by (simp add: bsimp_AALTs_rewrites)     

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

  1024 qed (simp_all)

  1025 

  1026 

  1027 lemma to_zero_in_alt: 

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

  1029   by (simp add: bs1 bs10 ss3)

  1030 

  1031 

  1032 

  1033 lemma  bder_fuse_list: 

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

  1035   apply(induction rs1)

  1036   apply(simp_all add: bder_fuse)

  1037   done

  1038 

  1039 

  1040 lemma rewrite_preserves_bder: 

  1041   shows "r1 \<leadsto> r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)"

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

  1043 proof(induction rule: rrewrite_srewrite.inducts)

  1044   case (bs1 bs r2)

  1045   then show ?case

  1046     by (simp add: continuous_rewrite) 

  1047 next

  1048   case (bs2 bs r1)

  1049   then show ?case 

  1050     apply(auto)

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

  1052     by (simp add: r_in_rstar rrewrite_srewrite.bs2)

  1053 next

  1054   case (bs3 bs1 bs2 r)

  1055   then show ?case 

  1056     apply(simp)

  1057     

  1058     by (metis (no_types, lifting) bder_fuse bs10 bs7 fuse_append rrewrites.simps ss4 to_zero_in_alt)

  1059 next

  1060   case (bs4 r1 r2 bs r3)

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

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

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

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

  1065 next

  1066   case (bs5 r3 r4 bs r1)

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

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

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

  1070     apply(simp)

  1071     apply(auto)

  1072     using contextrewrites0 r_in_rstar rewrites_fuse srewrites6 srewrites7 star_seq2 apply presburger

  1073     using star_seq2 by blast

  1074 next

  1075   case (bs6 bs)

  1076   then show ?case

  1077     using rrewrite_srewrite.bs6 by force 

  1078 next

  1079   case (bs7 bs r)

  1080   then show ?case

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

  1082 next

  1083   case (bs10 rs1 rs2 bs)

  1084   then show ?case

  1085     using contextrewrites0 by force    

  1086 next

  1087   case ss1

  1088   then show ?case by simp

  1089 next

  1090   case (ss2 rs1 rs2 r)

  1091   then show ?case

  1092     by (simp add: srewrites7) 

  1093 next

  1094   case (ss3 r1 r2 rs)

  1095   then show ?case

  1096     by (simp add: srewrites7) 

  1097 next

  1098   case (ss4 rs)

  1099   then show ?case

  1100     using rrewrite_srewrite.ss4 by fastforce 

  1101 next

  1102   case (ss5 bs1 rs1 rsb)

  1103   then show ?case 

  1104     apply(simp)

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

  1106 next

  1107   case (ss6 a1 a2 bs rsa rsb)

  1108   then show ?case

  1109     apply(simp only: map_append)

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

  1111 qed

  1112 

  1113 lemma rewrites_preserves_bder: 

  1114   assumes "r1 \<leadsto>* r2"

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

  1116 using assms  

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

  1118 apply(simp_all add: rewrite_preserves_bder rrewrites_trans)

  1119 done

  1120 

  1121 

  1122 lemma central:  

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

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

  1125   case Nil

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

  1127 next

  1128   case (snoc x xs)

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

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

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

  1132     by (simp add: rewrites_preserves_bder)

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

  1134     by (simp add: rewrites_to_bsimp)