1 

     2 theory BitCoded2

     3   imports "Lexer" 

     4 begin

     5 

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

     7 

     8 datatype bit = Z | S

     9 

    10 fun 

    11   code :: "val \<Rightarrow> bit list"

    12 where

    13   "code Void = []"

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

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

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

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

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

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

    20 

    21 

    22 fun 

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

    24 where

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

    26 

    27 function

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

    29 where

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

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

    32 | "decode' ds (CHAR d) = (Char d, ds)"

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

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

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

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

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

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

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

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

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

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

    43 by pat_completeness auto

    44 

    45 lemma decode'_smaller:

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

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

    48 using assms

    49 apply(induct ds r)

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

    51 using dual_order.trans apply blast

    52 by (meson dual_order.trans le_SucI)

    53 

    54 termination "decode'"  

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

    56 apply(auto dest!: decode'_smaller)

    57 by (metis less_Suc_eq_le snd_conv)

    58 

    59 definition

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

    61 where

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

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

    64 

    65 lemma decode'_code_Stars:

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

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

    68   using assms

    69   apply(induct vs)

    70   apply(auto)

    71   done

    72 

    73 lemma decode'_code:

    74   assumes "\<Turnstile> v : r"

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

    76 using assms

    77   apply(induct v r arbitrary: ds) 

    78   apply(auto)

    79   using decode'_code_Stars by blast

    80 

    81 lemma decode_code:

    82   assumes "\<Turnstile> v : r"

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

    84   using assms unfolding decode_def

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

    86 

    87 

    88 section {* Annotated Regular Expressions *}

    89 

    90 datatype arexp = 

    91   AZERO

    92 | AONE "bit list"

    93 | ACHAR "bit list" char

    94 | ASEQ "bit list" arexp arexp

    95 | AALTs "bit list" "arexp list"

    96 | ASTAR "bit list" arexp

    97 

    98 abbreviation

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

   100 

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

   102   "asize AZERO = 1"

   103 | "asize (AONE cs) = 1" 

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

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

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

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

   108 

   109 fun 

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

   111 where

   112   "erase AZERO = ZERO"

   113 | "erase (AONE _) = ONE"

   114 | "erase (ACHAR _ c) = CHAR c"

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

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

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

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

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

   120 

   121 lemma decode_code_erase:

   122   assumes "\<Turnstile> v : (erase  a)"

   123   shows "decode (code v) (erase a) = Some v"

   124   using assms

   125   by (simp add: decode_code) 

   126 

   127 

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

   129   where

   130   "nonalt (AALTs bs2 rs) = False"

   131 | "nonalt r = True"

   132 

   133 

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

   135   "good AZERO = False"

   136 | "good (AONE cs) = True" 

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

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

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

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

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

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

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

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

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

   146 

   147 

   148 

   149 

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

   151   "fuse bs AZERO = AZERO"

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

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

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

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

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

   157 

   158 lemma fuse_append:

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

   160   apply(induct r)

   161   apply(auto)

   162   done

   163 

   164 

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

   166   "intern ZERO = AZERO"

   167 | "intern ONE = AONE []"

   168 | "intern (CHAR c) = ACHAR [] c"

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

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

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

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

   173 

   174 

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

   176   "retrieve (AONE bs) Void = bs"

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

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

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

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

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

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

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

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

   185 

   186 

   187 

   188 fun

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

   190 where

   191   "bnullable (AZERO) = False"

   192 | "bnullable (AONE bs) = True"

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

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

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

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

   197 

   198 fun 

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

   200 where

   201   "bmkeps(AONE bs) = bs"

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

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

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

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

   206 

   207 

   208 fun

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

   210 where

   211   "bder c (AZERO) = AZERO"

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

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

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

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

   216      (if bnullable r1

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

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

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

   220 

   221 

   222 fun 

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

   224 where

   225   "bders r [] = r"

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

   227 

   228 lemma bders_append:

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

   230   apply(induct s1 arbitrary: r s2)

   231   apply(simp_all)

   232   done

   233 

   234 lemma bnullable_correctness:

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

   236   apply(induct r rule: erase.induct)

   237   apply(simp_all)

   238   done

   239 

   240 lemma erase_fuse:

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

   242   apply(induct r rule: erase.induct)

   243   apply(simp_all)

   244   done

   245 

   246 lemma erase_intern [simp]:

   247   shows "erase (intern r) = r"

   248   apply(induct r)

   249   apply(simp_all add: erase_fuse)

   250   done

   251 

   252 lemma erase_bder [simp]:

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

   254   apply(induct r rule: erase.induct)

   255   apply(simp_all add: erase_fuse bnullable_correctness)

   256   done

   257 

   258 lemma erase_bders [simp]:

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

   260   apply(induct s arbitrary: r )

   261   apply(simp_all)

   262   done

   263 

   264 lemma retrieve_encode_STARS:

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

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

   267   using assms

   268   apply(induct vs)

   269   apply(simp_all)

   270   done

   271 

   272 lemma retrieve_fuse2:

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

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

   275   using assms

   276   apply(induct r arbitrary: v bs)

   277          apply(auto elim: Prf_elims)[4]

   278    defer

   279   using retrieve_encode_STARS

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

   281    apply(case_tac vs)

   282     apply(simp)

   283    apply(simp)

   284   (* AALTs  case *)

   285   apply(simp)

   286   apply(case_tac x2a)

   287    apply(simp)

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

   289   apply(simp)

   290    apply(case_tac list)

   291    apply(simp)

   292   apply(auto)

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

   294   done

   295 

   296 lemma retrieve_fuse:

   297   assumes "\<Turnstile> v : r"

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

   299   using assms 

   300   by (simp_all add: retrieve_fuse2)

   301 

   302 

   303 lemma retrieve_code:

   304   assumes "\<Turnstile> v : r"

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

   306   using assms

   307   apply(induct v r )

   308   apply(simp_all add: retrieve_fuse retrieve_encode_STARS)

   309   done

   310 

   311 lemma r:

   312   assumes "bnullable (AALTs bs (a # rs))"

   313   shows "bnullable a \<or> (\<not> bnullable a \<and> bnullable (AALTs bs rs))"

   314   using assms

   315   apply(induct rs)

   316    apply(auto)

   317   done

   318 

   319 lemma r0:

   320   assumes "bnullable a" 

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

   322   using assms

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

   324 

   325 lemma r1:

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

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

   328   using assms

   329   apply(induct rs)

   330    apply(auto)

   331   done

   332 

   333 lemma r2:

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

   335   shows "bnullable (AALTs bs rs)"

   336   using assms

   337   apply(induct rs)

   338    apply(auto)

   339   done

   340 

   341 lemma  r3:

   342   assumes "\<not> bnullable r" 

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

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

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

   346   using assms

   347   apply(induct rs arbitrary: r bs)

   348    apply(auto)[1]

   349   apply(auto)

   350   using bnullable_correctness apply blast

   351     apply(auto simp add: bnullable_correctness mkeps_nullable retrieve_fuse2)

   352    apply(subst retrieve_fuse2[symmetric])

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

   354    apply(simp)

   355   apply(case_tac "bnullable a")

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

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

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

   359   apply(drule meta_mp)

   360    apply(simp)

   361   apply(drule meta_mp)

   362    apply(auto)

   363   apply(subst retrieve_fuse2[symmetric])

   364   apply(case_tac rs)

   365     apply(simp)

   366    apply(auto)[1]

   367       apply (simp add: bnullable_correctness)

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

   369     apply (simp add: bnullable_correctness)

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

   371   apply(simp)

   372   done

   373 

   374 

   375 lemma t: 

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

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

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

   379   using assms

   380   apply(induct rs arbitrary: bs)

   381    apply(simp)

   382   apply(auto simp add: bnullable_correctness)

   383    apply(case_tac rs)

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

   385    apply(subst r1)

   386      apply(simp)

   387     apply(rule r2)

   388      apply(assumption)

   389     apply(simp)

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

   391    apply(drule meta_mp)

   392     apply(auto)[1]

   393    prefer 2

   394   apply(case_tac "bnullable a")

   395     apply(subst r0)

   396      apply blast

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

   398   prefer 2

   399   using bnullable_correctness apply blast

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

   401   apply(subst r1)

   402      apply(simp)

   403   using r2 apply blast

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

   405    apply(drule meta_mp)

   406     apply(auto)[1]

   407    apply(simp)

   408   using r3 apply blast

   409   apply(auto)

   410   using r3 by blast

   411 

   412 lemma bmkeps_retrieve:

   413   assumes "nullable (erase r)"

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

   415   using assms

   416   apply(induct r)

   417          apply(simp)

   418         apply(simp)

   419        apply(simp)

   420     apply(simp)

   421    defer

   422    apply(simp)

   423   apply(rule t)

   424    apply(auto)

   425   done

   426 

   427 lemma bder_retrieve:

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

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

   430   using assms

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

   432          apply(simp)

   433          apply(erule Prf_elims)

   434         apply(simp)

   435         apply(erule Prf_elims) 

   436         apply(simp)

   437       apply(case_tac "c = ca")

   438        apply(simp)

   439        apply(erule Prf_elims)

   440        apply(simp)

   441       apply(simp)

   442        apply(erule Prf_elims)

   443   apply(simp)

   444       apply(erule Prf_elims)

   445      apply(simp)

   446     apply(simp)

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

   448     apply(erule Prf_elims)

   449      apply(simp)

   450     apply(simp)

   451     apply(case_tac rs)

   452      apply(simp)

   453     apply(simp)

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

   455    apply(simp)

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

   457     apply(simp)

   458   apply(erule Prf_elims)

   459      apply(subgoal_tac "bnullable r1")

   460   prefer 2

   461   using bnullable_correctness apply blast

   462     apply(simp)

   463      apply(erule Prf_elims)

   464      apply(simp)

   465    apply(subgoal_tac "bnullable r1")

   466   prefer 2

   467   using bnullable_correctness apply blast

   468     apply(simp)

   469     apply(simp add: retrieve_fuse2)

   470     apply(simp add: bmkeps_retrieve)

   471    apply(simp)

   472    apply(erule Prf_elims)

   473    apply(simp)

   474   using bnullable_correctness apply blast

   475   apply(rename_tac bs r v)

   476   apply(simp)

   477   apply(erule Prf_elims)

   478      apply(clarify)

   479   apply(erule Prf_elims)

   480   apply(clarify)

   481   apply(subst injval.simps)

   482   apply(simp del: retrieve.simps)

   483   apply(subst retrieve.simps)

   484   apply(subst retrieve.simps)

   485   apply(simp)

   486   apply(simp add: retrieve_fuse2)

   487   done

   488   

   489 

   490 

   491 lemma MAIN_decode:

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

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

   494   using assms

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

   496   case Nil

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

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

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

   500     using decode_code retrieve_code by auto

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

   502     by simp

   503 next

   504   case (snoc c s v)

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

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

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

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

   509     by (simp add: Prf_injval ders_append)

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

   511     by (simp add: flex_append)

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

   513     using asm2 IH by simp

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

   515     using asm by (simp_all add: bder_retrieve ders_append)

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

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

   518 qed

   519 

   520 

   521 definition blex where

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

   523 

   524 

   525 

   526 definition blexer where

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

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

   529 

   530 lemma blexer_correctness:

   531   shows "blexer r s = lexer r s"

   532 proof -

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

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

   535     assume asm: "nullable ds"

   536     have era: "erase bds = ds" 

   537       unfolding ds_def bds_def by simp

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

   539       using asm by (simp add: mkeps_nullable)

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

   541       using bmkeps_retrieve

   542       using asm era by (simp add: bmkeps_retrieve)

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

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

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

   546       unfolding bds_def ds_def .

   547   }

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

   549     unfolding blexer_def lexer_flex

   550     apply(subst bnullable_correctness[symmetric])

   551     apply(simp)

   552     done

   553 qed

   554 

   555 lemma asize0:

   556   shows "0 < asize r"

   557   apply(induct  r)

   558   apply(auto)

   559   done

   560 

   561 lemma asize_fuse:

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

   563   apply(induct r)

   564   apply(auto)

   565   done

   566 

   567 lemma bder_fuse:

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

   569   apply(induct a arbitrary: bs c)

   570   apply(simp_all)

   571   done

   572 

   573 lemma map_bder_fuse:

   574   shows "map (bder c \<circ> fuse bs1) as1 = map (fuse bs1) (map (bder c) as1)"

   575   apply(induct as1)

   576   apply(auto simp add: bder_fuse)

   577   done

   578 

   579 

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

   581   where

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

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

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

   585 | "nonnested r = True"

   586 

   587 

   588 

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

   590   where

   591   "distinctBy [] f acc = []"

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

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

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

   595 

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

   597   where 

   598   "flts [] = []"

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

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

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

   602 

   603 

   604 fun spill :: "arexp list \<Rightarrow> arexp list"

   605   where 

   606   "spill [] = []"

   607 | "spill ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ spill rs"

   608 | "spill (r1 # rs) = r1 # spill rs"

   609 

   610 lemma  spill_Cons:

   611   shows "spill (r # rs1) = spill [r] @ spill rs1"

   612   apply(induct r arbitrary: rs1)

   613    apply(auto)

   614   done

   615 

   616 lemma  spill_append:

   617   shows "spill (rs1 @ rs2) = spill rs1 @ spill rs2"

   618   apply(induct rs1 arbitrary: rs2)

   619    apply(auto)

   620   by (metis append.assoc spill_Cons)

   621 

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

   623   where

   624   "bsimp_ASEQ _ AZERO _ = AZERO"

   625 | "bsimp_ASEQ _ _ AZERO = AZERO"

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

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

   628 

   629 

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

   631   where

   632   "bsimp_AALTs _ [] = AZERO"

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

   634 | "bsimp_AALTs bs1 rs = AALTs bs1 rs"

   635 

   636 

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

   638   where

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

   640 | "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (flts (map bsimp rs))"

   641 | "bsimp r = r"

   642 

   643 inductive contains :: "arexp \<Rightarrow> bit list \<Rightarrow> bool" ("_ >> _" [51, 50] 50)

   644   where

   645   "AONE bs >> bs"

   646 | "ACHAR bs c >> bs"

   647 | "\<lbrakk>a1 >> bs1; a2 >> bs2\<rbrakk> \<Longrightarrow> ASEQ bs a1 a2 >> bs @ bs1 @ bs2"

   648 | "r >> bs1 \<Longrightarrow> AALTs bs (r#rs) >> bs @ bs1"

   649 | "AALTs bs rs >> bs @ bs1 \<Longrightarrow> AALTs bs (r#rs) >> bs @ bs1"

   650 | "ASTAR bs r >> bs @ [S]"

   651 | "\<lbrakk>r >> bs1; ASTAR [] r >> bs2\<rbrakk> \<Longrightarrow> ASTAR bs r >> bs @ Z # bs1 @ bs2"

   652 

   653 lemma contains0:

   654   assumes "a >> bs"

   655   shows "(fuse bs1 a) >> bs1 @ bs"

   656   using assms

   657   apply(induct arbitrary: bs1)

   658   apply(auto intro: contains.intros)

   659        apply (metis append.assoc contains.intros(3))

   660      apply (metis append.assoc contains.intros(4))

   661   apply (metis append.assoc contains.intros(5))

   662     apply (metis append.assoc contains.intros(6))

   663    apply (metis append_assoc contains.intros(7))

   664   done

   665 

   666 lemma contains1:

   667   assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> intern r >> code v"

   668   shows "ASTAR [] (intern r) >> code (Stars vs)"

   669   using assms

   670   apply(induct vs)

   671    apply(simp)

   672   using contains.simps apply blast

   673   apply(simp)

   674    apply(subst (2) append_Nil[symmetric])

   675   apply(rule contains.intros)

   676    apply(auto)

   677   done

   678 

   679 

   680 lemma contains2:

   681   assumes "\<Turnstile> v : r"

   682   shows "(intern r) >> code v"

   683   using assms

   684   apply(induct)

   685        prefer 4

   686        apply(simp)

   687        apply(rule contains.intros)

   688    prefer 4

   689        apply(simp)

   690       apply(rule contains.intros)

   691      apply(simp)

   692   apply(subst (3) append_Nil[symmetric])

   693   apply(rule contains.intros)

   694       apply(simp)

   695   apply(simp)

   696     apply(simp)

   697   apply(subst (9) append_Nil[symmetric])

   698     apply(rule contains.intros)

   699     apply (metis append_Cons append_self_conv2 contains0)

   700     apply(simp)

   701      apply(subst (9) append_Nil[symmetric])

   702    apply(rule contains.intros)

   703    back

   704    apply(rule contains.intros)

   705   apply(drule_tac ?bs1.0="[S]" in contains0)

   706    apply(simp)

   707   apply(simp)

   708   apply(case_tac vs)

   709    apply(simp)

   710   apply (metis append_Nil contains.intros(6))

   711   using contains1 by blast

   712 

   713 lemma qq1:

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

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

   716   using assms

   717   apply(induct rs arbitrary: rs1 bs)

   718   apply(simp)

   719   apply(simp)

   720   by (metis Nil_is_append_conv bmkeps.simps(4) neq_Nil_conv r0 split_list_last)

   721 

   722 lemma qq2:

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

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

   725   using assms

   726   apply(induct rs arbitrary: rs1 bs)

   727   apply(simp)

   728   apply(simp)

   729   by (metis append_assoc in_set_conv_decomp r1 r2)

   730 

   731 lemma qq2a:

   732   assumes "\<not> bnullable r" "\<exists>r \<in> set rs1. bnullable r"

   733   shows "bmkeps (AALTs bs (r # rs1)) = bmkeps (AALTs bs rs1)"

   734   using assms

   735   by (simp add: r1)

   736   

   737 lemma qq3:

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

   739   apply(induct rs arbitrary: bs)

   740   apply(simp)

   741   apply(simp)

   742   done

   743 

   744 lemma qq4:

   745   assumes "bnullable (AALTs bs rs)"

   746   shows "bmkeps (AALTs bs rs) = bs @ bmkeps (AALTs [] rs)"

   747   by (metis append_Nil2 assms bmkeps_retrieve bnullable_correctness erase_fuse fuse.simps(4) mkeps_nullable retrieve_fuse2)

   748 

   749 

   750 lemma contains3a:

   751   assumes "AALTs bs lst >> bs @ bs1"

   752   shows "AALTs bs (a # lst) >> bs @ bs1"

   753   using assms

   754   apply -

   755   by (simp add: contains.intros(5))

   756 

   757   

   758 lemma contains3b:

   759   assumes "a >> bs1"

   760   shows "AALTs bs (a # lst) >> bs @ bs1"

   761   using assms

   762   apply -

   763   apply(rule contains.intros)

   764   apply(simp)

   765   done   

   766 

   767 

   768 lemma contains3:

   769   assumes "\<And>x. \<lbrakk>x \<in> set rs; bnullable x\<rbrakk> \<Longrightarrow> x >> bmkeps x" "x \<in> set rs" "bnullable x"

   770   shows "AALTs bs rs >> bmkeps (AALTs bs rs)"

   771   using assms

   772   apply(induct rs arbitrary: bs x)

   773    apply simp

   774   by (metis contains.intros(4) contains.intros(5) list.set_intros(1) list.set_intros(2) qq3 qq4 r r0 r1)

   775 

   776 lemma cont1:

   777   assumes "\<And>v. \<Turnstile> v : erase r \<Longrightarrow> r >> retrieve r v" 

   778           "\<forall>v\<in>set vs. \<Turnstile> v : erase r \<and> flat v \<noteq> []" 

   779   shows "ASTAR bs r >> retrieve (ASTAR bs r) (Stars vs)"

   780   using assms 

   781   apply(induct vs arbitrary: bs r)

   782    apply(simp)

   783   using contains.intros(6) apply auto[1]

   784   by (simp add: contains.intros(7))

   785   

   786 lemma contains4:

   787   assumes "bnullable a"

   788   shows "a >> bmkeps a"

   789   using assms

   790   apply(induct a rule: bnullable.induct)

   791        apply(auto intro: contains.intros)

   792   using contains3 by blast

   793 

   794 lemma contains5:

   795   assumes "\<Turnstile> v : r"

   796   shows "(intern r) >> retrieve (intern r) v"

   797   using contains2[OF assms] retrieve_code[OF assms]

   798   by (simp)

   799 

   800 lemma contains6:

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

   802   shows "r >> retrieve r v"

   803   using assms

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

   805   apply(auto)[1]

   806   using Prf_elims(1) apply blast

   807   using Prf_elims(4) contains.intros(1) apply force

   808   using Prf_elims(5) contains.intros(2) apply force

   809   apply(auto)[1]

   810   using Prf_elims(1) apply blast

   811   apply(auto)[1]

   812   using contains3b contains3a apply blast

   813     prefer 2

   814   apply(auto)[1]

   815     apply (metis Prf_elims(2) contains.intros(3) retrieve.simps(6))

   816    prefer 2

   817   apply(auto)[1]

   818    apply (metis Prf_elims(6) cont1)

   819   apply(simp)

   820   apply(erule Prf_elims)

   821    apply(auto)

   822    apply (simp add: contains3b)

   823   using retrieve_fuse2 contains3b contains3a

   824   apply(subst retrieve_fuse2[symmetric])

   825   apply (metis append_Nil2 erase_fuse fuse.simps(4))

   826   apply(simp)

   827   by (metis append_Nil2 erase_fuse fuse.simps(4))

   828 

   829 lemma contains7:

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

   831   shows "(bder c r) >> retrieve r (injval (erase r) c v)"

   832   using bder_retrieve[OF assms(1)] retrieve_code[OF assms(1)]

   833   by (metis assms contains6 erase_bder)

   834 

   835 

   836 fun 

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

   838 where

   839   "bders_simp r [] = r"

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

   841 

   842 definition blexer_simp where

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

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

   845 

   846 

   847 

   848 

   849 

   850 lemma bders_simp_append:

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

   852   apply(induct s1 arbitrary: r s2)

   853    apply(simp)

   854   apply(simp)

   855   done

   856 

   857 lemma bsimp_ASEQ_size:

   858   shows "asize (bsimp_ASEQ bs r1 r2) \<le> Suc (asize r1 + asize r2)"

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

   860   apply(auto)

   861   done

   862 

   863 

   864 

   865 lemma flts_size:

   866   shows "sum_list (map asize (flts rs)) \<le> sum_list (map asize rs)"

   867   apply(induct rs rule: flts.induct)

   868         apply(simp_all)

   869   by (simp add: asize_fuse comp_def)

   870   

   871 

   872 lemma bsimp_AALTs_size:

   873   shows "asize (bsimp_AALTs bs rs) \<le> Suc (sum_list (map asize rs))"

   874   apply(induct rs rule: bsimp_AALTs.induct)

   875   apply(auto simp add: asize_fuse)

   876   done

   877 

   878 

   879 lemma bsimp_size:

   880   shows "asize (bsimp r) \<le> asize r"

   881   apply(induct r)

   882        apply(simp_all)

   883    apply (meson Suc_le_mono add_mono_thms_linordered_semiring(1) bsimp_ASEQ_size le_trans)

   884   apply(rule le_trans)

   885    apply(rule bsimp_AALTs_size)

   886   apply(simp)

   887    apply(rule le_trans)

   888    apply(rule flts_size)

   889   by (simp add: sum_list_mono)

   890 

   891 lemma bsimp_asize0:

   892   shows "(\<Sum>x\<leftarrow>rs. asize (bsimp x)) \<le> sum_list (map asize rs)"

   893   apply(induct rs)

   894    apply(auto)

   895   by (simp add: add_mono bsimp_size)

   896 

   897 lemma bsimp_AALTs_size2:

   898   assumes "\<forall>r \<in> set  rs. nonalt r"

   899   shows "asize (bsimp_AALTs bs rs) \<ge> sum_list (map asize rs)"

   900   using assms

   901   apply(induct rs rule: bsimp_AALTs.induct)

   902     apply(simp_all add: asize_fuse)

   903   done

   904 

   905 

   906 lemma qq:

   907   shows "map (asize \<circ> fuse bs) rs = map asize rs"

   908   apply(induct rs)

   909    apply(auto simp add: asize_fuse)

   910   done

   911 

   912 lemma flts_size2:

   913   assumes "\<exists>bs rs'. AALTs bs  rs' \<in> set rs"

   914   shows "sum_list (map asize (flts rs)) < sum_list (map asize rs)"

   915   using assms

   916   apply(induct rs)

   917    apply(auto simp add: qq)

   918    apply (simp add: flts_size less_Suc_eq_le)

   919   apply(case_tac a)

   920        apply(auto simp add: qq)

   921    prefer 2

   922    apply (simp add: flts_size le_imp_less_Suc)

   923   using less_Suc_eq by auto

   924 

   925 lemma bsimp_AALTs_size3:

   926   assumes "\<exists>r \<in> set  (map bsimp rs). \<not>nonalt r"

   927   shows "asize (bsimp (AALTs bs rs)) < asize (AALTs bs rs)"

   928   using assms flts_size2

   929   apply  -

   930   apply(clarify)

   931   apply(simp)

   932   apply(drule_tac x="map bsimp rs" in meta_spec)

   933   apply(drule meta_mp)

   934   apply (metis list.set_map nonalt.elims(3))

   935   apply(simp)

   936   apply(rule order_class.order.strict_trans1)

   937    apply(rule bsimp_AALTs_size)

   938   apply(simp)

   939   by (smt Suc_leI bsimp_asize0 comp_def le_imp_less_Suc le_trans map_eq_conv not_less_eq)

   940 

   941 

   942 

   943 

   944 lemma L_bsimp_ASEQ:

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

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

   947   apply(simp_all)

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

   949 

   950 lemma L_bsimp_AALTs:

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

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

   953   apply(simp_all add: erase_fuse)

   954   done

   955 

   956 lemma L_erase_AALTs:

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

   958   apply(induct rs)

   959    apply(simp)

   960   apply(simp)

   961   apply(case_tac rs)

   962    apply(simp)

   963   apply(simp)

   964   done

   965 

   966 lemma L_erase_flts:

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

   968   apply(induct rs rule: flts.induct)

   969         apply(simp_all)

   970   apply(auto)

   971   using L_erase_AALTs erase_fuse apply auto[1]

   972   by (simp add: L_erase_AALTs erase_fuse)

   973 

   974 

   975 lemma L_bsimp_erase:

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

   977   apply(induct r)

   978   apply(simp)

   979   apply(simp)

   980   apply(simp)

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

   982   apply(subst L_bsimp_ASEQ[symmetric])

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

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

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

   986    apply(simp)

   987    apply(subst L_bsimp_AALTs[symmetric])

   988    defer

   989    apply(simp)

   990   apply(subst (2)L_erase_AALTs)

   991   apply(subst L_erase_flts)

   992   apply(auto)

   993    apply (simp add: L_erase_AALTs)

   994   using L_erase_AALTs by blast

   995 

   996 lemma bsimp_ASEQ0:

   997   shows "bsimp_ASEQ bs r1 AZERO = AZERO"

   998   apply(induct r1)

   999   apply(auto)

  1000   done

  1001 

  1002 

  1003 

  1004 lemma bsimp_ASEQ1:

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

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

  1007   using assms

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

  1009   apply(auto)

  1010   done

  1011 

  1012 lemma bsimp_ASEQ2:

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

  1014   apply(induct r2)

  1015   apply(auto)

  1016   done

  1017 

  1018 

  1019 lemma L_bders_simp:

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

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

  1022    apply(simp)

  1023   apply(simp)

  1024   apply(simp add: ders_append)

  1025   apply(simp add: bders_simp_append)

  1026   apply(simp add: L_bsimp_erase[symmetric])

  1027   by (simp add: der_correctness)

  1028 

  1029 lemma b1:

  1030   "bsimp_ASEQ bs1 (AONE bs) r =  fuse (bs1 @ bs) r" 

  1031   apply(induct r)

  1032        apply(auto)

  1033   done

  1034 

  1035 lemma b2:

  1036   assumes "bnullable r"

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

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

  1039 

  1040 lemma b3:

  1041   shows "bnullable r = bnullable (bsimp r)"

  1042   using L_bsimp_erase bnullable_correctness nullable_correctness by auto

  1043 

  1044 

  1045 lemma b4:

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

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

  1048 

  1049 lemma q1:

  1050   assumes "\<forall>r \<in> set rs. bmkeps(bsimp r) = bmkeps r"

  1051   shows "map (\<lambda>r. bmkeps(bsimp r)) rs = map bmkeps rs"

  1052   using assms

  1053   apply(induct rs)

  1054   apply(simp)

  1055   apply(simp)

  1056   done

  1057 

  1058 lemma q3:

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

  1060   shows "bmkeps (AALTs bs rs) = bmkeps (bsimp_AALTs bs rs)"

  1061   using assms

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

  1063     apply(simp)

  1064    apply(simp)

  1065   apply (simp add: b2)

  1066   apply(simp)

  1067   done

  1068 

  1069 

  1070 lemma fuse_empty:

  1071   shows "fuse [] r = r"

  1072   apply(induct r)

  1073        apply(auto)

  1074   done

  1075 

  1076 lemma flts_fuse:

  1077   shows "map (fuse bs) (flts rs) = flts (map (fuse bs) rs)"

  1078   apply(induct rs arbitrary: bs rule: flts.induct)

  1079         apply(auto simp add: fuse_append)

  1080   done

  1081 

  1082 lemma bsimp_ASEQ_fuse:

  1083   shows "fuse bs1 (bsimp_ASEQ bs2 r1 r2) = bsimp_ASEQ (bs1 @ bs2) r1 r2"

  1084   apply(induct r1 r2 arbitrary: bs1 bs2 rule: bsimp_ASEQ.induct)

  1085   apply(auto)

  1086   done

  1087 

  1088 lemma bsimp_AALTs_fuse:

  1089   assumes "\<forall>r \<in> set rs. fuse bs1 (fuse bs2 r) = fuse (bs1 @ bs2) r"

  1090   shows "fuse bs1 (bsimp_AALTs bs2 rs) = bsimp_AALTs (bs1 @ bs2) rs"

  1091   using assms

  1092   apply(induct bs2 rs arbitrary: bs1 rule: bsimp_AALTs.induct)

  1093   apply(auto)

  1094   done

  1095 

  1096 

  1097 

  1098 lemma bsimp_fuse:

  1099   shows "fuse bs (bsimp r) = bsimp (fuse bs r)"

  1100 apply(induct r arbitrary: bs)

  1101        apply(simp)

  1102       apply(simp)

  1103      apply(simp)

  1104     prefer 3

  1105     apply(simp)

  1106    apply(simp)

  1107    apply (simp add: bsimp_ASEQ_fuse)

  1108   apply(simp)

  1109   by (simp add: bsimp_AALTs_fuse fuse_append)

  1110 

  1111 lemma bsimp_fuse_AALTs:

  1112   shows "fuse bs (bsimp (AALTs [] rs)) = bsimp (AALTs bs rs)"

  1113   apply(subst bsimp_fuse) 

  1114   apply(simp)

  1115   done

  1116 

  1117 lemma bsimp_fuse_AALTs2:

  1118   shows "fuse bs (bsimp_AALTs [] rs) = bsimp_AALTs bs rs"

  1119   using bsimp_AALTs_fuse fuse_append by auto

  1120   

  1121 

  1122 lemma bsimp_ASEQ_idem:

  1123   assumes "bsimp (bsimp r1) = bsimp r1" "bsimp (bsimp r2) = bsimp r2"

  1124   shows "bsimp (bsimp_ASEQ x1 (bsimp r1) (bsimp r2)) = bsimp_ASEQ x1 (bsimp r1) (bsimp r2)"

  1125   using assms

  1126   apply(case_tac "bsimp r1 = AZERO")

  1127     apply(simp)

  1128  apply(case_tac "bsimp r2 = AZERO")

  1129     apply(simp)

  1130   apply (metis bnullable.elims(2) bnullable.elims(3) bsimp.simps(3) bsimp_ASEQ.simps(2) bsimp_ASEQ.simps(3) bsimp_ASEQ.simps(4) bsimp_ASEQ.simps(5) bsimp_ASEQ.simps(6))  

  1131   apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")

  1132     apply(auto)[1]

  1133     apply(subst bsimp_ASEQ2)

  1134    apply(subst bsimp_ASEQ2)

  1135   apply (metis assms(2) bsimp_fuse)