1 

     2 theory SizeBoundStrong

     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 nonalt :: "arexp \<Rightarrow> bool"

   122   where

   123   "nonalt (AALTs bs2 rs) = False"

   124 | "nonalt r = True"

   125 

   126 

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

   128   "fuse bs AZERO = AZERO"

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

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

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

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

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

   134 

   135 lemma fuse_append:

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

   137   apply(induct r)

   138   apply(auto)

   139   done

   140 

   141 lemma fuse_Nil:

   142   shows "fuse [] r = r"

   143   by (induct r)(simp_all)

   144 

   145 lemma map_fuse_Nil:

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

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

   148 

   149 

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

   151   "intern ZERO = AZERO"

   152 | "intern ONE = AONE []"

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

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

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

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

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

   158 

   159 

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

   161   "retrieve (AONE bs) Void = bs"

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

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

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

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

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

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

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

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

   170 

   171 

   172 

   173 fun

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

   175 where

   176   "bnullable (AZERO) = False"

   177 | "bnullable (AONE bs) = True"

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

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

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

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

   182 

   183 fun 

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

   185 where

   186   "bmkeps(AONE bs) = bs"

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

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

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

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

   191 

   192 

   193 fun

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

   195 where

   196   "bder c (AZERO) = AZERO"

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

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

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

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

   201      (if bnullable r1

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

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

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

   205 

   206 

   207 fun 

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

   209 where

   210   "bders r [] = r"

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

   212 

   213 lemma bders_append:

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

   215   apply(induct s1 arbitrary: r s2)

   216   apply(simp_all)

   217   done

   218 

   219 lemma bnullable_correctness:

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

   221   apply(induct r rule: erase.induct)

   222   apply(simp_all)

   223   done

   224 

   225 lemma erase_fuse:

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

   227   apply(induct r rule: erase.induct)

   228   apply(simp_all)

   229   done

   230 

   231 lemma erase_intern [simp]:

   232   shows "erase (intern r) = r"

   233   apply(induct r)

   234   apply(simp_all add: erase_fuse)

   235   done

   236 

   237 lemma erase_bder [simp]:

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

   239   apply(induct r rule: erase.induct)

   240   apply(simp_all add: erase_fuse bnullable_correctness)

   241   done

   242 

   243 lemma erase_bders [simp]:

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

   245   apply(induct s arbitrary: r )

   246   apply(simp_all)

   247   done

   248 

   249 lemma bnullable_fuse:

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

   251   apply(induct r arbitrary: bs)

   252   apply(auto)

   253   done

   254 

   255 lemma retrieve_encode_STARS:

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

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

   258   using assms

   259   apply(induct vs)

   260   apply(simp_all)

   261   done

   262 

   263 

   264 lemma retrieve_fuse2:

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

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

   267   using assms

   268   apply(induct r arbitrary: v bs)

   269          apply(auto elim: Prf_elims)[4]

   270    defer

   271   using retrieve_encode_STARS

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

   273    apply(case_tac vs)

   274     apply(simp)

   275    apply(simp)

   276   (* AALTs  case *)

   277   apply(simp)

   278   apply(case_tac x2a)

   279    apply(simp)

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

   281   apply(simp)

   282    apply(case_tac list)

   283    apply(simp)

   284   apply(auto)

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

   286   done

   287 

   288 lemma retrieve_fuse:

   289   assumes "\<Turnstile> v : r"

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

   291   using assms 

   292   by (simp_all add: retrieve_fuse2)

   293 

   294 

   295 lemma retrieve_code:

   296   assumes "\<Turnstile> v : r"

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

   298   using assms

   299   apply(induct v r )

   300   apply(simp_all add: retrieve_fuse retrieve_encode_STARS)

   301   done

   302 

   303 

   304 lemma bnullable_Hdbmkeps_Hd:

   305   assumes "bnullable a" 

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

   307   using assms

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

   309 

   310 lemma r1:

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

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

   313   using assms

   314   apply(induct rs)

   315    apply(auto)

   316   done

   317 

   318 lemma r2:

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

   320   shows "bnullable (AALTs bs rs)"

   321   using assms

   322   apply(induct rs)

   323    apply(auto)

   324   done

   325 

   326 lemma  r3:

   327   assumes "\<not> bnullable r" 

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

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

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

   331   using assms

   332   apply(induct rs arbitrary: r bs)

   333    apply(auto)[1]

   334   apply(auto)

   335   using bnullable_correctness apply blast

   336     apply(auto simp add: bnullable_correctness mkeps_nullable retrieve_fuse2)

   337    apply(subst retrieve_fuse2[symmetric])

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

   339    apply(simp)

   340   apply(case_tac "bnullable a")

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

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

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

   344   apply(drule meta_mp)

   345    apply(simp)

   346   apply(drule meta_mp)

   347    apply(auto)

   348   apply(subst retrieve_fuse2[symmetric])

   349   apply(case_tac rs)

   350     apply(simp)

   351    apply(auto)[1]

   352       apply (simp add: bnullable_correctness)

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

   354     apply (simp add: bnullable_correctness)

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

   356   apply(simp)

   357   done

   358 

   359 

   360 lemma t: 

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

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

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

   364   using assms

   365   apply(induct rs arbitrary: bs)

   366    apply(simp)

   367   apply(auto simp add: bnullable_correctness)

   368    apply(case_tac rs)

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

   370    apply(subst r1)

   371      apply(simp)

   372     apply(rule r2)

   373      apply(assumption)

   374     apply(simp)

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

   376    apply(drule meta_mp)

   377     apply(auto)[1]

   378    prefer 2

   379   apply(case_tac "bnullable a")

   380     apply(subst bnullable_Hdbmkeps_Hd)

   381      apply blast

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

   383   prefer 2

   384   using bnullable_correctness apply blast

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

   386   apply(subst r1)

   387      apply(simp)

   388   using r2 apply blast

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

   390    apply(drule meta_mp)

   391     apply(auto)[1]

   392    apply(simp)

   393   using r3 apply blast

   394   apply(auto)

   395   using r3 by blast

   396 

   397 lemma bmkeps_retrieve:

   398   assumes "nullable (erase r)"

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

   400   using assms

   401   apply(induct r)

   402          apply(simp)

   403         apply(simp)

   404        apply(simp)

   405     apply(simp)

   406    defer

   407    apply(simp)

   408   apply(rule t)

   409    apply(auto)

   410   done

   411 

   412 lemma bder_retrieve:

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

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

   415   using assms

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

   417          apply(simp)

   418          apply(erule Prf_elims)

   419         apply(simp)

   420         apply(erule Prf_elims) 

   421         apply(simp)

   422       apply(case_tac "c = ca")

   423        apply(simp)

   424        apply(erule Prf_elims)

   425        apply(simp)

   426       apply(simp)

   427        apply(erule Prf_elims)

   428   apply(simp)

   429       apply(erule Prf_elims)

   430      apply(simp)

   431     apply(simp)

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

   433     apply(erule Prf_elims)

   434      apply(simp)

   435     apply(simp)

   436     apply(case_tac rs)

   437      apply(simp)

   438     apply(simp)

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

   440    apply(simp)

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

   442     apply(simp)

   443   apply(erule Prf_elims)

   444      apply(subgoal_tac "bnullable r1")

   445   prefer 2

   446   using bnullable_correctness apply blast

   447     apply(simp)

   448      apply(erule Prf_elims)

   449      apply(simp)

   450    apply(subgoal_tac "bnullable r1")

   451   prefer 2

   452   using bnullable_correctness apply blast

   453     apply(simp)

   454     apply(simp add: retrieve_fuse2)

   455     apply(simp add: bmkeps_retrieve)

   456    apply(simp)

   457    apply(erule Prf_elims)

   458    apply(simp)

   459   using bnullable_correctness apply blast

   460   apply(rename_tac bs r v)

   461   apply(simp)

   462   apply(erule Prf_elims)

   463      apply(clarify)

   464   apply(erule Prf_elims)

   465   apply(clarify)

   466   apply(subst injval.simps)

   467   apply(simp del: retrieve.simps)

   468   apply(subst retrieve.simps)

   469   apply(subst retrieve.simps)

   470   apply(simp)

   471   apply(simp add: retrieve_fuse2)

   472   done

   473   

   474 

   475 

   476 lemma MAIN_decode:

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

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

   479   using assms

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

   481   case Nil

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

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

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

   485     using decode_code retrieve_code by auto

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

   487     by simp

   488 next

   489   case (snoc c s v)

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

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

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

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

   494     by (simp add: Prf_injval ders_append)

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

   496     by (simp add: flex_append)

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

   498     using asm2 IH by simp

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

   500     using asm by (simp_all add: bder_retrieve ders_append)

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

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

   503 qed

   504 

   505 

   506 definition blex where

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

   508 

   509 

   510 

   511 definition blexer where

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

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

   514 

   515 lemma blexer_correctness:

   516   shows "blexer r s = lexer r s"

   517 proof -

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

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

   520     assume asm: "nullable ds"

   521     have era: "erase bds = ds" 

   522       unfolding ds_def bds_def by simp

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

   524       using asm by (simp add: mkeps_nullable)

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

   526       using bmkeps_retrieve

   527       using asm era by (simp add: bmkeps_retrieve)

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

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

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

   531       unfolding bds_def ds_def .

   532   }

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

   534     unfolding blexer_def lexer_flex

   535     apply(subst bnullable_correctness[symmetric])

   536     apply(simp)

   537     done

   538 qed

   539 

   540 

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

   542   where

   543   "distinctBy [] f acc = []"

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

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

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

   547 

   548 (*filter  (\<lambda>rt. case rt of 

   549                                       SEQ r1p r2p \<Rightarrow> r2p = (erase r2)

   550                                       r           \<Rightarrow> False ) allowableTerms*)

   551 

   552 

   553 lemma dB_single_step: 

   554   shows "distinctBy (a#rs) f {} = a # distinctBy rs f {f a}"

   555   by simp 

   556 

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

   558   where 

   559   "flts [] = []"

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

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

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

   563 

   564 

   565 

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

   567   where

   568   "bsimp_ASEQ _ AZERO _ = AZERO"

   569 | "bsimp_ASEQ _ _ AZERO = AZERO"

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

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

   572 

   573 

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

   575   where

   576   "bsimp_AALTs _ [] = AZERO"

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

   578 | "bsimp_AALTs bs1 rs = AALTs bs1 rs"

   579 

   580 

   581 fun bsimp_ASEQ1 :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"

   582   where

   583   "bsimp_ASEQ1 _ AZERO _ = AZERO"

   584 | "bsimp_ASEQ1 bs (AONE bs1) r2 = fuse (bs @ bs1) r2"

   585 | "bsimp_ASEQ1 bs r1 r2 = ASEQ  bs r1 r2"

   586 

   587 

   588 fun collect where

   589   \<open>collect _ [] = []\<close>

   590 |  \<open>collect erasedR2  ((SEQ r1 r2) # rs) = (if r2 = erasedR2 then r1 # (collect erasedR2 rs)

   591                                         else collect erasedR2 rs)\<close>

   592 | \<open>collect erasedR2 (r # rs) = collect erasedR2 rs\<close>

   593 

   594 

   595 fun pruneRexp where

   596   \<open>pruneRexp (ASEQ bs r1 r2) allowableTerms = 

   597 ( let termsTruncated = (collect (erase r2) allowableTerms) in (let pruned = pruneRexp r1 termsTruncated in (bsimp_ASEQ1 bs pruned r2))    )\<close>

   598 | \<open>pruneRexp (AALTs bs rs) allowableTerms = (let rsp = (filter (\<lambda>r. r \<noteq> AZERO)  (map (\<lambda>r. pruneRexp r allowableTerms) rs) ) in bsimp_AALTs bs rsp )

   599 \<close>

   600 | \<open>pruneRexp r allowableTerms = (if (erase r) \<in> (set allowableTerms) then r else AZERO)\<close>

   601 

   602 

   603 fun oneSimp :: \<open>rexp \<Rightarrow> rexp\<close> where

   604   \<open> oneSimp (SEQ ONE r) = r \<close>

   605 | \<open> oneSimp (SEQ r1 r2) = SEQ (oneSimp r1) r2 \<close>

   606 | \<open> oneSimp r = r \<close>

   607 

   608 fun breakIntoTerms where

   609   \<open>breakIntoTerms (SEQ r1 r2) = map (\<lambda>r1p. SEQ r1p r2) (breakIntoTerms r1)\<close>

   610 | \<open>breakIntoTerms (ALT r1 r2) = (breakIntoTerms r1) @ (breakIntoTerms r2)\<close>

   611 | \<open>breakIntoTerms r = r # [] \<close>

   612 

   613 fun addToAcc :: "arexp \<Rightarrow> rexp list \<Rightarrow> rexp list"

   614   where

   615 \<open>addToAcc r acc = filter (\<lambda>r1. oneSimp r1 \<notin> set acc) (breakIntoTerms (erase r)) \<close>

   616 

   617 fun dBStrong :: "arexp list \<Rightarrow> rexp list \<Rightarrow> arexp list"

   618   where

   619 "dBStrong [] acc = []"

   620 | "dBStrong (r # rs) acc = (if (erase r) \<in> (set acc) then dBStrong rs acc

   621                             else (case (pruneRexp r (addToAcc r acc)) of  

   622                                     AZERO \<Rightarrow> dBStrong rs ((addToAcc r acc) @ acc) |

   623                                     r1    \<Rightarrow> r1 # (dBStrong rs ((addToAcc r acc) @ acc))

   624                                  )

   625                            )

   626                     "

   627 fun bsimpStrong :: "arexp \<Rightarrow> arexp "

   628   where

   629   "bsimpStrong (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimpStrong r1) (bsimpStrong r2)"

   630 | "bsimpStrong (AALTs bs1 rs) = bsimp_AALTs bs1 (dBStrong (flts (map bsimpStrong rs)) []) "

   631 | "bsimpStrong r = r"

   632 

   633 

   634 fun bdersStrong :: "arexp \<Rightarrow> string \<Rightarrow> arexp"

   635 where

   636   "bdersStrong r [] = r"

   637 | "bdersStrong r (c # s) = bdersStrong (bsimpStrong (bder c r)) s"

   638 

   639 

   640 definition blexerStrong where

   641  "blexerStrong r s \<equiv> if bnullable (bdersStrong (intern r) s) then 

   642                     decode (bmkeps (bdersStrong (intern r) s)) r else None"

   643 

   644 

   645 

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

   647   where

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

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

   650 | "bsimp r = r"

   651 

   652 

   653 fun 

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

   655 where

   656   "bders_simp r [] = r"

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

   658 

   659 definition blexer_simp where

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

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

   662 

   663 export_code bders_simp in Scala module_name Example

   664 

   665 lemma bders_simp_append:

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

   667   apply(induct s1 arbitrary: r s2)

   668   apply(simp_all)

   669   done

   670 

   671 lemma L_bsimp_ASEQ:

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

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

   674   apply(simp_all)

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

   676 

   677 lemma L_bsimp_AALTs:

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

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

   680   apply(simp_all add: erase_fuse)

   681   done

   682 

   683 lemma L_erase_AALTs:

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

   685   apply(induct rs)

   686    apply(simp)

   687   apply(simp)

   688   apply(case_tac rs)

   689    apply(simp)

   690   apply(simp)

   691   done

   692 

   693 lemma L_erase_flts:

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

   695   apply(induct rs rule: flts.induct)

   696         apply(simp_all)

   697   apply(auto)

   698   using L_erase_AALTs erase_fuse apply auto[1]

   699   by (simp add: L_erase_AALTs erase_fuse)

   700 

   701 lemma L_erase_dB_acc:

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

   703   apply(induction rs arbitrary: acc)

   704    apply simp

   705   apply simp

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

   707 

   708 lemma L_erase_dB:

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

   710   by (metis L_erase_dB_acc Un_commute Union_image_empty)

   711 

   712 lemma L_bsimp_erase:

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

   714   apply(induct r)

   715   apply(simp)

   716   apply(simp)

   717   apply(simp)

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

   719   apply(subst L_bsimp_ASEQ[symmetric])

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

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

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

   723   apply(simp)

   724   apply(subst L_bsimp_AALTs[symmetric])

   725   defer

   726   apply(simp)

   727   apply(subst (2)L_erase_AALTs)

   728   apply(subst L_erase_dB)

   729   apply(subst L_erase_flts)

   730   apply(auto)

   731   apply (simp add: L_erase_AALTs)

   732   using L_erase_AALTs by blast

   733 

   734 

   735 

   736 lemma bsimp_ASEQ0:

   737   shows "bsimp_ASEQ bs r1 AZERO = AZERO"

   738   apply(induct r1)

   739   apply(auto)

   740   done

   741 

   742 lemma bsimp_ASEQ1:

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

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

   745   using assms

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

   747   apply(auto)

   748   done

   749 

   750 lemma bsimp_ASEQ2:

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

   752   apply(induct r2)

   753   apply(auto)

   754   done

   755 

   756 

   757 lemma L_bders_simp:

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

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

   760   apply(simp)

   761   apply(simp)

   762   apply(simp add: ders_append)

   763   apply(simp add: bders_simp_append)

   764   apply(simp add: L_bsimp_erase[symmetric])

   765   by (simp add: der_correctness)

   766 

   767 

   768 lemma b2:

   769   assumes "bnullable r"

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

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

   772 

   773 

   774 lemma b4:

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

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

   777 

   778 lemma qq1:

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

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

   781   using assms

   782   apply(induct rs arbitrary: rs1 bs)

   783   apply(simp)

   784   apply(simp)

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

   786 

   787 lemma qq2:

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

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

   790   using assms

   791   apply(induct rs arbitrary: rs1 bs)

   792   apply(simp)

   793   apply(simp)

   794   by (metis append_assoc in_set_conv_decomp r1 r2)

   795   

   796 lemma qq3:

   797   assumes "bnullable (AALTs bs (rs @ rs1))"

   798           "bnullable (AALTs bs (rs @ rs2))"

   799           "\<lbrakk>bnullable (AALTs bs rs1); bnullable (AALTs bs rs2); \<forall>r\<in>set rs. \<not>bnullable r\<rbrakk> \<Longrightarrow> 

   800                bmkeps (AALTs bs rs1) = bmkeps (AALTs bs rs2)"

   801   shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs (rs @ rs2))"

   802   using assms

   803   apply(case_tac "\<exists>r \<in> set rs. bnullable r")

   804   using qq1 apply auto[1]

   805   by (metis UnE bnullable.simps(4) qq2 set_append)

   806   

   807 

   808 lemma flts_append:

   809   shows "flts (xs1 @ xs2) = flts xs1 @ flts xs2"

   810 by (induct xs1  arbitrary: xs2  rule: flts.induct)(auto)

   811 

   812 lemma  k0a:

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

   814   apply(simp)

   815   done

   816 

   817 

   818 lemma bbbbs1:

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

   820   using nonalt.elims(3) by auto

   821   

   822 

   823 

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

   825   where

   826   "nonazero AZERO = False"

   827 | "nonazero r = True"

   828 

   829 

   830 lemma flts_single1:

   831   assumes "nonalt r" "nonazero r"

   832   shows "flts [r] = [r]"

   833   using assms

   834   apply(induct r)

   835   apply(auto)

   836   done

   837 

   838 

   839 

   840 lemma q3a:

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

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

   843   using assms

   844   apply(induct rs arbitrary: bs bs1)

   845    apply(simp)

   846   apply(simp)

   847   apply(auto)

   848    apply (metis append_assoc b2 bnullable_correctness erase_fuse bnullable_Hdbmkeps_Hd)

   849   apply(case_tac "bnullable a")

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

   851   apply(case_tac rs)

   852   apply(simp)

   853   apply(simp)

   854   apply(auto)[1]

   855    apply (metis bnullable_correctness erase_fuse)+

   856   done

   857 

   858 lemma qq4:

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

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

   861   using assms

   862   apply(induct list rule: flts.induct)

   863         apply(auto)

   864   by (metis UnCI bnullable_correctness erase_fuse imageI)

   865   

   866 

   867 lemma qs3:

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

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

   870   using assms

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

   872   apply(case_tac x)

   873   apply(simp)

   874   apply(simp)

   875   apply(case_tac a)

   876        apply(simp)

   877        apply (simp add: r1)

   878       apply(simp)

   879       apply (simp add: bnullable_Hdbmkeps_Hd)

   880      apply(simp)

   881      apply(case_tac "flts list")

   882       apply(simp)

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

   884      apply(simp)

   885      apply (simp add: r1)

   886     prefer 3

   887     apply(simp)

   888     apply (simp add: bnullable_Hdbmkeps_Hd)

   889    prefer 2

   890    apply(simp)

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

   892   apply(case_tac "list")

   893     apply(simp)

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

   895    apply(erule disjE)

   896     apply(subst qq1)

   897      apply(auto)[1]

   898      apply (metis bnullable_correctness erase_fuse)

   899     apply(simp)

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

   901     apply(simp)

   902     apply(auto)[1]

   903      apply(subst qq1)

   904       apply (metis bnullable_correctness erase_fuse image_eqI set_map)

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

   906   apply(subst qq1)

   907       apply (metis bnullable_correctness erase_fuse image_eqI set_map)

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

   909    apply(simp)

   910    apply(subst qq2)

   911      apply (metis bnullable_correctness erase_fuse imageE set_map)

   912   prefer 2

   913   apply(case_tac "list")

   914      apply(simp)

   915     apply(simp)

   916    apply (simp add: qq4)

   917   apply(simp)

   918   apply(auto)

   919    apply(case_tac list)

   920     apply(simp)

   921    apply(simp)

   922    apply (simp add: bnullable_Hdbmkeps_Hd)

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

   924    apply(case_tac list)

   925     apply(simp)

   926    apply(simp)

   927    apply (simp add: bnullable_Hdbmkeps_Hd)

   928   apply(simp)

   929   using qq4 r1 r2 by auto

   930 

   931 lemma bder_fuse:

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

   933   apply(induct a arbitrary: bs c)

   934        apply(simp_all)

   935   done

   936 

   937 

   938 

   939 

   940 inductive 

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

   942 where

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

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

   945 | "ASEQ bs1 (AONE bs2) r \<leadsto> fuse (bs1@bs2) r"

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

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

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

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

   950 | "AALTs bs (rsa@ [AZERO] @ rsb) \<leadsto> AALTs bs (rsa @ rsb)"

   951 | "AALTs bs (rsa@ [AALTs bs1 rs1] @ rsb) \<leadsto> AALTs bs (rsa@(map (fuse bs1) rs1)@rsb)"

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

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

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

   955 

   956 

   957 inductive 

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

   959 where 

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

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

   962 

   963 

   964 inductive 

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

   966 where

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

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

   969 

   970 

   971 (* rewrites for lists *)

   972 inductive 

   973   frewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ f\<leadsto>* _" [100, 100] 100)

   974 where

   975   fs1: "[] f\<leadsto>* []"

   976 | fs2: "\<lbrakk>rs f\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (AZERO#rs) f\<leadsto>* rs'"

   977 | fs3: "\<lbrakk>rs f\<leadsto>* rs'\<rbrakk> \<Longrightarrow> ((AALTs bs rs1) # rs) f\<leadsto>* ((map (fuse bs) rs1) @ rs')"

   978 | fs4: "\<lbrakk>rs f\<leadsto>* rs'; nonalt r; nonazero r\<rbrakk> \<Longrightarrow> (r#rs) f\<leadsto>* (r#rs')"

   979 

   980 

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

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

   983  

   984 lemma real_trans[trans]: 

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

   986   shows "r1 \<leadsto>* r3"

   987   using a2 a1

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

   989   apply(auto)

   990   done

   991 

   992 

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

   994   by (meson r_in_rstar real_trans)

   995 

   996 

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

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

   999    apply simp

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

  1001 

  1002 

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

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

  1005    apply simp

  1006   using rrewrite.intros(6) by blast

  1007 

  1008 

  1009 

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

  1011 

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

  1013    apply(rule rs1)

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

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

  1016   apply simp

  1017   apply(rule real_trans)

  1018    prefer 2

  1019    apply(assumption)

  1020   apply(drule contextrewrites2)

  1021   apply auto

  1022   done

  1023 

  1024 corollary srewrites_alt1: 

  1025   assumes "rs1 s\<leadsto>* rs2"

  1026   shows "AALTs bs rs1 \<leadsto>* AALTs bs rs2"

  1027 using assms

  1028   by (metis append.left_neutral srewrites_alt)

  1029 

  1030 

  1031 lemma star_seq:  

  1032   assumes "r1 \<leadsto>* r2"

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

  1034 using assms

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

  1036 apply(auto intro: rrewrite.intros)

  1037 done

  1038 

  1039 lemma star_seq2:  

  1040   assumes "r3 \<leadsto>* r4"

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

  1042 using assms

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

  1044 apply(auto intro: rrewrite.intros)

  1045 done

  1046 

  1047 lemma continuous_rewrite: 

  1048   assumes "r1 \<leadsto>* AZERO"

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

  1050 using assms

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

  1052   apply(auto intro: rrewrite.intros r_in_rstar star_seq)

  1053   by (meson rrewrite.intros(1) rs2 star_seq)

  1054   

  1055 

  1056 

  1057 lemma bsimp_aalts_simpcases: 

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

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

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

  1061   by (simp_all)

  1062 

  1063 

  1064 lemma trivialbsimp_srewrites: 

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

  1066 

  1067   apply(induction rs)

  1068    apply simp

  1069    apply(rule ss1)

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

  1071 

  1072 

  1073 lemma bsimp_AALTs_rewrites: 

  1074   "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs"

  1075   apply(induction rs)

  1076   apply simp

  1077    apply(rule r_in_rstar)

  1078   using rrewrite.intros(9) apply blast

  1079   by (metis bsimp_AALTs.elims list.discI rrewrite.intros(10) rrewrites.simps)

  1080 

  1081 

  1082 

  1083 lemma flts_prepend: "\<lbrakk>nonalt a; nonazero a\<rbrakk> \<Longrightarrow> flts (a#rs) = a # (flts rs)"

  1084   by (metis append_Cons append_Nil flts_single1 flts_append)

  1085 

  1086 lemma fltsfrewrites: "rs f\<leadsto>* (flts rs)"

  1087   apply(induction rs)

  1088   apply simp

  1089    apply(rule fs1)

  1090 

  1091   apply(case_tac "a = AZERO")

  1092 

  1093    

  1094   using fs2 apply auto[1]

  1095   apply(case_tac "\<exists>bs rs. a = AALTs bs rs")

  1096    apply(erule exE)+

  1097    

  1098    apply (simp add: fs3)

  1099   apply(subst flts_prepend)

  1100     apply(rule nonalt.elims(2))

  1101   prefer 2

  1102   thm nonalt.elims

  1103    

  1104          apply blast

  1105    

  1106   using bbbbs1 apply blast

  1107        apply(simp)+

  1108    

  1109    apply (meson nonazero.elims(3))

  1110    

  1111   by (meson fs4 nonalt.elims(3) nonazero.elims(3))

  1112 

  1113 

  1114 lemma rrewrite0away: "AALTs bs (AZERO # rsb) \<leadsto> AALTs bs rsb"

  1115   by (metis append_Cons append_Nil rrewrite.intros(7))

  1116 

  1117 

  1118 lemma frewritesaalts:"rs f\<leadsto>* rs' \<Longrightarrow> (AALTs bs (rs1@rs)) \<leadsto>* (AALTs bs (rs1@rs'))"

  1119   apply(induct rs rs' arbitrary: bs rs1 rule:frewrites.induct)

  1120     apply(rule rs1)

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

  1122   apply(drule_tac x = "rs1 @ [AZERO]" in meta_spec)

  1123     apply(rule real_trans)

  1124      apply simp

  1125   using rrewrite.intros(7) apply auto[1]

  1126     apply(drule_tac x = "bsa" in meta_spec)

  1127   apply(drule_tac x = "rs1a @ [AALTs bs rs1]" in meta_spec)

  1128    apply(rule real_trans)

  1129     apply simp

  1130   using r_in_rstar rrewrite.intros(8) apply auto[1]

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

  1132   apply(drule_tac x = "rs1@[r]" in meta_spec)

  1133     apply(rule real_trans)

  1134    apply simp

  1135   apply auto