1 

     2 theory SizeBound4

     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: 

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

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

   728 

   729 lemma srewrites_single : 

   730   shows "rs1 s\<leadsto> rs2 \<Longrightarrow> rs1 s\<leadsto>* rs2"

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

   732  

   733 

   734 lemma rrewrites_trans[trans]: 

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

   736   shows "r1 \<leadsto>* r3"

   737   using a2 a1

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

   739   apply(auto)

   740   done

   741 

   742 lemma srewrites_trans[trans]: 

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

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

   745   using a1 a2

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

   747    apply(auto)

   748   done

   749 

   750 

   751 

   752 lemma contextrewrites0: 

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

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

   755    apply simp

   756   using bs10 r_in_rstar rrewrites_trans by blast

   757 

   758 lemma contextrewrites1: 

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

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

   761    apply simp

   762   using bs10 ss3 by blast

   763 

   764 lemma srewrite1: 

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

   766   apply(induct rs)

   767    apply(auto)

   768   using ss2 by auto

   769 

   770 lemma srewrites1: 

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

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

   773    apply(auto)

   774   using srewrite1 by blast

   775 

   776 lemma srewrite2: 

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

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

   779   apply(induct rule: rrewrite_srewrite.inducts)

   780                apply(auto)

   781      apply (metis append_Cons append_Nil srewrites1)

   782     apply(meson srewrites.simps ss3)

   783   apply (meson srewrites.simps ss4)

   784   apply (meson srewrites.simps ss5)

   785   by (metis append_Cons append_Nil srewrites.simps ss6)

   786   

   787 

   788 lemma srewrites3: 

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

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

   791    apply(auto)

   792   by (meson srewrite2(2) srewrites_trans)

   793 

   794 (*

   795 lemma srewrites4:

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

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

   798   using assms

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

   800   apply (simp add: srewrites3)

   801   using srewrite1 by blast

   802 *)

   803 

   804 lemma srewrites6:

   805   assumes "r1 \<leadsto>* r2" 

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

   807   using assms

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

   809    apply(auto)

   810   by (meson srewrites.simps srewrites_trans ss3)

   811 

   812 lemma srewrites7:

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

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

   815   using assms

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

   817 

   818 lemma ss6_stronger_aux:

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

   820   apply(induct rs2 arbitrary: rs1)

   821    apply(auto)

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

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

   824   apply(simp)

   825   done

   826 

   827 lemma ss6_stronger:

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

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

   830 

   831 

   832 lemma rewrite_preserves_fuse: 

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

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

   835 proof(induct rule: rrewrite_srewrite.inducts)

   836   case (bs3 bs1 bs2 r)

   837   then show ?case

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

   839 next

   840   case (bs7 bs r)

   841   then show ?case

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

   843 next

   844   case (ss2 rs1 rs2 r)

   845   then show ?case

   846     using srewrites7 by force 

   847 next

   848   case (ss3 r1 r2 rs)

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

   850 next

   851   case (ss5 bs1 rs1 rsb)

   852   then show ?case 

   853     apply(simp)

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

   855 next

   856   case (ss6 a1 a2 rsa rsb rsc)

   857   then show ?case 

   858     apply(simp)

   859     apply(rule srewrites_single)

   860     apply(rule rrewrite_srewrite.ss6[simplified])

   861     apply(simp add: erase_fuse)

   862     done

   863  qed (auto intro: rrewrite_srewrite.intros)

   864 

   865 

   866 lemma rewrites_fuse:  

   867   assumes "r1 \<leadsto>* r2"

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

   869 using assms

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

   871 apply(auto intro: rewrite_preserves_fuse rrewrites_trans)

   872 done

   873 

   874 

   875 lemma star_seq:  

   876   assumes "r1 \<leadsto>* r2"

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

   878 using assms

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

   880 apply(auto intro: rrewrite_srewrite.intros)

   881 done

   882 

   883 lemma star_seq2:  

   884   assumes "r3 \<leadsto>* r4"

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

   886   using assms

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

   888 apply(auto intro: rrewrite_srewrite.intros)

   889 done

   890 

   891 lemma continuous_rewrite: 

   892   assumes "r1 \<leadsto>* AZERO"

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

   894 using assms bs1 star_seq by blast

   895 

   896 (*

   897 lemma continuous_rewrite2: 

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

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

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

   901 *)

   902 

   903 lemma bsimp_aalts_simpcases: 

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

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

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

   907   by (simp_all)

   908 

   909 lemma bsimp_AALTs_rewrites: 

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

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

   912 

   913 lemma trivialbsimp_srewrites: 

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

   915   apply(induction rs)

   916    apply simp

   917   apply(simp)

   918   using srewrites7 by auto

   919 

   920 

   921 

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

   923   apply(induction rs rule: flts.induct)

   924   apply(auto intro: rrewrite_srewrite.intros)

   925   apply (meson srewrites.simps srewrites1 ss5)

   926   using rs1 srewrites7 apply presburger

   927   using srewrites7 apply force

   928   apply (simp add: srewrites7)

   929   by (simp add: srewrites7)

   930 

   931 lemma bnullable0:

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

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

   934   apply(induct rule: rrewrite_srewrite.inducts)

   935   apply(auto simp add:  bnullable_fuse)

   936   apply (meson UnCI bnullable_fuse imageI)

   937   by (metis bnullable_correctness)

   938 

   939 

   940 lemma rewritesnullable: 

   941   assumes "r1 \<leadsto>* r2" 

   942   shows "bnullable r1 = bnullable r2"

   943 using assms 

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

   945   apply simp

   946   using bnullable0(1) by auto

   947 

   948 lemma rewrite_bmkeps_aux: 

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

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

   951 proof (induct rule: rrewrite_srewrite.inducts)

   952   case (bs3 bs1 bs2 r)

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

   954 next

   955   case (bs7 bs r)

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

   957 next

   958   case (ss3 r1 r2 rs)

   959   then show ?case

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

   961 next

   962   case (ss5 bs1 rs1 rsb)

   963   then show ?case

   964     by (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse)

   965 next

   966   case (ss6 a1 a2 rsa rsb rsc)

   967   then show ?case

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

   969 qed (auto)

   970 

   971 lemma rewrites_bmkeps: 

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

   973   shows "bmkeps r1 = bmkeps r2"

   974   using assms

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

   976   case (rs1 r)

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

   978 next

   979   case (rs2 r1 r2 r3)

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

   981   have a1: "bnullable r1" by fact

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

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

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

   985   then have "bmkeps r2 = bmkeps r3"

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

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

   988 qed

   989 

   990 

   991 lemma rewrites_to_bsimp: 

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

   993 proof (induction r rule: bsimp.induct)

   994   case (1 bs1 r1 r2)

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

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

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

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

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

  1000       by (metis bs2 continuous_rewrite rrewrites.simps star_seq2)  

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

  1002   }

  1003   moreover

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

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

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

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

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

  1009       using rewrites_fuse by (meson rrewrites_trans) 

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

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

  1012   } 

  1013   moreover

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

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

  1016       by (simp add: bsimp_ASEQ1) 

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

  1018       by (metis rrewrites_trans star_seq star_seq2) 

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

  1020   } 

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

  1022 next

  1023   case (2 bs1 rs)

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

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

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

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

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

  1029     using contextrewrites0 by blast

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

  1031     by (simp add: bsimp_AALTs_rewrites)     

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

  1033 qed (simp_all)

  1034 

  1035 

  1036 lemma to_zero_in_alt: 

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

  1038   by (simp add: bs1 bs10 ss3)

  1039 

  1040 

  1041 

  1042 lemma  bder_fuse_list: 

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

  1044   apply(induction rs1)

  1045   apply(simp_all add: bder_fuse)

  1046   done

  1047 

  1048 

  1049 lemma rewrite_preserves_bder: 

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

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

  1052 proof(induction rule: rrewrite_srewrite.inducts)

  1053   case (bs1 bs r2)

  1054   then show ?case

  1055     by (simp add: continuous_rewrite) 

  1056 next

  1057   case (bs2 bs r1)

  1058   then show ?case 

  1059     apply(auto)

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

  1061     by (simp add: r_in_rstar rrewrite_srewrite.bs2)

  1062 next

  1063   case (bs3 bs1 bs2 r)

  1064   then show ?case 

  1065     apply(simp)

  1066     

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

  1068 next

  1069   case (bs4 r1 r2 bs r3)

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

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

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

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

  1074 next

  1075   case (bs5 r3 r4 bs r1)

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

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

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

  1079     apply(simp)

  1080     apply(auto)

  1081     using contextrewrites0 r_in_rstar rewrites_fuse srewrites6 srewrites7 star_seq2 apply presburger

  1082     using star_seq2 by blast

  1083 next

  1084   case (bs6 bs)

  1085   then show ?case

  1086     using rrewrite_srewrite.bs6 by force 

  1087 next

  1088   case (bs7 bs r)

  1089   then show ?case

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

  1091 next

  1092   case (bs10 rs1 rs2 bs)

  1093   then show ?case

  1094     using contextrewrites0 by force    

  1095 next

  1096   case ss1

  1097   then show ?case by simp

  1098 next

  1099   case (ss2 rs1 rs2 r)

  1100   then show ?case

  1101     by (simp add: srewrites7) 

  1102 next

  1103   case (ss3 r1 r2 rs)

  1104   then show ?case

  1105     by (simp add: srewrites7) 

  1106 next

  1107   case (ss4 rs)

  1108   then show ?case

  1109     using rrewrite_srewrite.ss4 by fastforce 

  1110 next

  1111   case (ss5 bs1 rs1 rsb)

  1112   then show ?case 

  1113     apply(simp)

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

  1115 next

  1116   case (ss6 a1 a2 bs rsa rsb)

  1117   then show ?case

  1118     apply(simp only: map_append)

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

  1120 qed

  1121 

  1122 lemma rewrites_preserves_bder: 

  1123   assumes "r1 \<leadsto>* r2"

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

  1125 using assms  

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

  1127 apply(simp_all add: rewrite_preserves_bder rrewrites_trans)

  1128 done

  1129 

  1130 

  1131 lemma central:  

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

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

  1134   case Nil