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 | "Stars_add v _ = Stars [v]" 

    27 

    28 function

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

    30 where

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

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

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

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

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

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

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

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

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

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

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

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

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

    44 by pat_completeness auto

    45 

    46 lemma decode'_smaller:

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

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

    49 using assms

    50 apply(induct ds r)

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

    52 using dual_order.trans apply blast

    53 by (meson dual_order.trans le_SucI)

    54 

    55 termination "decode'"  

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

    57 apply(auto dest!: decode'_smaller)

    58 by (metis less_Suc_eq_le snd_conv)

    59 

    60 definition

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

    62 where

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

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

    65 

    66 lemma decode'_code_Stars:

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

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

    69   using assms

    70   apply(induct vs)

    71   apply(auto)

    72   done

    73 

    74 lemma decode'_code:

    75   assumes "\<Turnstile> v : r"

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

    77 using assms

    78   apply(induct v r arbitrary: ds) 

    79   apply(auto)

    80   using decode'_code_Stars by blast

    81 

    82 lemma decode_code:

    83   assumes "\<Turnstile> v : r"

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

    85   using assms unfolding decode_def

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

    87 

    88 

    89 section {* Annotated Regular Expressions *}

    90 

    91 datatype arexp = 

    92   AZERO

    93 | AONE "bit list"

    94 | ACHAR "bit list" char

    95 | ASEQ "bit list" arexp arexp

    96 | AALTs "bit list" "arexp list"

    97 | ASTAR "bit list" arexp

    98 

    99 abbreviation

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

   101 

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

   103   "asize AZERO = 1"

   104 | "asize (AONE cs) = 1" 

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

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

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

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

   109 

   110 fun 

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

   112 where

   113   "erase AZERO = ZERO"

   114 | "erase (AONE _) = ONE"

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

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

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

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

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

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

   121 

   122 lemma decode_code_erase:

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

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

   125   using assms

   126   by (simp add: decode_code) 

   127 

   128 

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

   130   where

   131   "nonalt (AALTs bs2 rs) = False"

   132 | "nonalt r = True"

   133 

   134 

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

   136   "good AZERO = False"

   137 | "good (AONE cs) = True" 

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

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

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

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

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

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

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

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

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

   147 

   148 

   149 

   150 

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

   152   "fuse bs AZERO = AZERO"

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

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

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

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

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

   158 

   159 lemma fuse_append:

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

   161   apply(induct r)

   162   apply(auto)

   163   done

   164 

   165 

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

   167   "intern ZERO = AZERO"

   168 | "intern ONE = AONE []"

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

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

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

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

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

   174 

   175 

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

   177   "retrieve (AONE bs) Void = bs"

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

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

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

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

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

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

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

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

   186 

   187 

   188 

   189 fun

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

   191 where

   192   "bnullable (AZERO) = False"

   193 | "bnullable (AONE bs) = True"

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

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

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

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

   198 

   199 fun 

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

   201 where

   202   "bmkeps(AONE bs) = bs"

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

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

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

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

   207 

   208 

   209 fun

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

   211 where

   212   "bder c (AZERO) = AZERO"

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

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

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

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

   217      (if bnullable r1

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

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

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

   221 

   222 

   223 fun 

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

   225 where

   226   "bders r [] = r"

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

   228 

   229 lemma bders_append:

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

   231   apply(induct s1 arbitrary: r s2)

   232   apply(simp_all)

   233   done

   234 

   235 lemma bnullable_correctness:

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

   237   apply(induct r rule: erase.induct)

   238   apply(simp_all)

   239   done

   240 

   241 lemma erase_fuse:

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

   243   apply(induct r rule: erase.induct)

   244   apply(simp_all)

   245   done

   246 

   247 lemma erase_intern [simp]:

   248   shows "erase (intern r) = r"

   249   apply(induct r)

   250   apply(simp_all add: erase_fuse)

   251   done

   252 

   253 lemma erase_bder [simp]:

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

   255   apply(induct r rule: erase.induct)

   256   apply(simp_all add: erase_fuse bnullable_correctness)

   257   done

   258 

   259 lemma erase_bders [simp]:

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

   261   apply(induct s arbitrary: r )

   262   apply(simp_all)

   263   done

   264 

   265 lemma retrieve_encode_STARS:

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

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

   268   using assms

   269   apply(induct vs)

   270   apply(simp_all)

   271   done

   272 

   273 lemma retrieve_fuse2:

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

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

   276   using assms

   277   apply(induct r arbitrary: v bs)

   278          apply(auto elim: Prf_elims)[4]

   279    defer

   280   using retrieve_encode_STARS

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

   282    apply(case_tac vs)

   283     apply(simp)

   284    apply(simp)

   285   (* AALTs  case *)

   286   apply(simp)

   287   apply(case_tac x2a)

   288    apply(simp)

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

   290   apply(simp)

   291    apply(case_tac list)

   292    apply(simp)

   293   apply(auto)

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

   295   done

   296 

   297 lemma retrieve_fuse:

   298   assumes "\<Turnstile> v : r"

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

   300   using assms 

   301   by (simp_all add: retrieve_fuse2)

   302 

   303 

   304 lemma retrieve_code:

   305   assumes "\<Turnstile> v : r"

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

   307   using assms

   308   apply(induct v r )

   309   apply(simp_all add: retrieve_fuse retrieve_encode_STARS)

   310   done

   311 

   312 lemma r:

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

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

   315   using assms

   316   apply(induct rs)

   317    apply(auto)

   318   done

   319 

   320 lemma r0:

   321   assumes "bnullable a" 

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

   323   using assms

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

   325 

   326 lemma r1:

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

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

   329   using assms

   330   apply(induct rs)

   331    apply(auto)

   332   done

   333 

   334 lemma r2:

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

   336   shows "bnullable (AALTs bs rs)"

   337   using assms

   338   apply(induct rs)

   339    apply(auto)

   340   done

   341 

   342 lemma  r3:

   343   assumes "\<not> bnullable r" 

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

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

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

   347   using assms

   348   apply(induct rs arbitrary: r bs)

   349    apply(auto)[1]

   350   apply(auto)

   351   using bnullable_correctness apply blast

   352     apply(auto simp add: bnullable_correctness mkeps_nullable retrieve_fuse2)

   353    apply(subst retrieve_fuse2[symmetric])

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

   355    apply(simp)

   356   apply(case_tac "bnullable a")

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

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

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

   360   apply(drule meta_mp)

   361    apply(simp)

   362   apply(drule meta_mp)

   363    apply(auto)

   364   apply(subst retrieve_fuse2[symmetric])

   365   apply(case_tac rs)

   366     apply(simp)

   367    apply(auto)[1]

   368       apply (simp add: bnullable_correctness)

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

   370     apply (simp add: bnullable_correctness)

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

   372   apply(simp)

   373   done

   374 

   375 

   376 lemma t: 

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

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

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

   380   using assms

   381   apply(induct rs arbitrary: bs)

   382    apply(simp)

   383   apply(auto simp add: bnullable_correctness)

   384    apply(case_tac rs)

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

   386    apply(subst r1)

   387      apply(simp)

   388     apply(rule r2)

   389      apply(assumption)

   390     apply(simp)

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

   392    apply(drule meta_mp)

   393     apply(auto)[1]

   394    prefer 2

   395   apply(case_tac "bnullable a")

   396     apply(subst r0)

   397      apply blast

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

   399   prefer 2

   400   using bnullable_correctness apply blast

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

   402   apply(subst r1)

   403      apply(simp)

   404   using r2 apply blast

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

   406    apply(drule meta_mp)

   407     apply(auto)[1]

   408    apply(simp)

   409   using r3 apply blast

   410   apply(auto)

   411   using r3 by blast

   412 

   413 lemma bmkeps_retrieve:

   414   assumes "nullable (erase r)"

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

   416   using assms

   417   apply(induct r)

   418          apply(simp)

   419         apply(simp)

   420        apply(simp)

   421     apply(simp)

   422    defer

   423    apply(simp)

   424   apply(rule t)

   425    apply(auto)

   426   done

   427 

   428 lemma bder_retrieve:

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

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

   431   using assms

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

   433          apply(simp)

   434          apply(erule Prf_elims)

   435         apply(simp)

   436         apply(erule Prf_elims) 

   437         apply(simp)

   438       apply(case_tac "c = ca")

   439        apply(simp)

   440        apply(erule Prf_elims)

   441        apply(simp)

   442       apply(simp)

   443        apply(erule Prf_elims)

   444   apply(simp)

   445       apply(erule Prf_elims)

   446      apply(simp)

   447     apply(simp)

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

   449     apply(erule Prf_elims)

   450      apply(simp)

   451     apply(simp)

   452     apply(case_tac rs)

   453      apply(simp)

   454     apply(simp)

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

   456    apply(simp)

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

   458     apply(simp)

   459   apply(erule Prf_elims)

   460      apply(subgoal_tac "bnullable r1")

   461   prefer 2

   462   using bnullable_correctness apply blast

   463     apply(simp)

   464      apply(erule Prf_elims)

   465      apply(simp)

   466    apply(subgoal_tac "bnullable r1")

   467   prefer 2

   468   using bnullable_correctness apply blast

   469     apply(simp)

   470     apply(simp add: retrieve_fuse2)

   471     apply(simp add: bmkeps_retrieve)

   472    apply(simp)

   473    apply(erule Prf_elims)

   474    apply(simp)

   475   using bnullable_correctness apply blast

   476   apply(rename_tac bs r v)

   477   apply(simp)

   478   apply(erule Prf_elims)

   479      apply(clarify)

   480   apply(erule Prf_elims)

   481   apply(clarify)

   482   apply(subst injval.simps)

   483   apply(simp del: retrieve.simps)

   484   apply(subst retrieve.simps)

   485   apply(subst retrieve.simps)

   486   apply(simp)

   487   apply(simp add: retrieve_fuse2)

   488   done

   489   

   490 

   491 

   492 lemma MAIN_decode:

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

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

   495   using assms

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

   497   case Nil

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

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

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

   501     using decode_code retrieve_code by auto

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

   503     by simp

   504 next

   505   case (snoc c s v)

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

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

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

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

   510     by (simp add: Prf_injval ders_append)

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

   512     by (simp add: flex_append)

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

   514     using asm2 IH by simp

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

   516     using asm by (simp_all add: bder_retrieve ders_append)

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

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

   519 qed

   520 

   521 

   522 definition blex where

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

   524 

   525 

   526 

   527 definition blexer where

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

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

   530 

   531 lemma blexer_correctness:

   532   shows "blexer r s = lexer r s"

   533 proof -

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

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

   536     assume asm: "nullable ds"

   537     have era: "erase bds = ds" 

   538       unfolding ds_def bds_def by simp

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

   540       using asm by (simp add: mkeps_nullable)

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

   542       using bmkeps_retrieve

   543       using asm era by (simp add: bmkeps_retrieve)

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

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

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

   547       unfolding bds_def ds_def .

   548   }

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

   550     unfolding blexer_def lexer_flex

   551     apply(subst bnullable_correctness[symmetric])

   552     apply(simp)

   553     done

   554 qed

   555 

   556 lemma asize0:

   557   shows "0 < asize r"

   558   apply(induct  r)

   559   apply(auto)

   560   done

   561 

   562 lemma asize_fuse:

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

   564   apply(induct r)

   565   apply(auto)

   566   done

   567 

   568 lemma bder_fuse:

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

   570   apply(induct a arbitrary: bs c)

   571   apply(simp_all)

   572   done

   573 

   574 lemma map_bder_fuse:

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

   576   apply(induct as1)

   577   apply(auto simp add: bder_fuse)

   578   done

   579 

   580 

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

   582   where

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

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

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

   586 | "nonnested r = True"

   587 

   588 

   589 

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

   591   where

   592   "distinctBy [] f acc = []"

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

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

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

   596 

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

   598   where 

   599   "flts [] = []"

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

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

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

   603 

   604 

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

   606   where 

   607   "spill [] = []"

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

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

   610 

   611 lemma  spill_Cons:

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

   613   apply(induct r arbitrary: rs1)

   614    apply(auto)

   615   done

   616 

   617 lemma  spill_append:

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

   619   apply(induct rs1 arbitrary: rs2)

   620    apply(auto)

   621   by (metis append.assoc spill_Cons)

   622 

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

   624   where

   625   "bsimp_ASEQ _ AZERO _ = AZERO"

   626 | "bsimp_ASEQ _ _ AZERO = AZERO"

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

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

   629 

   630 

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

   632   where

   633   "bsimp_AALTs _ [] = AZERO"

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

   635 | "bsimp_AALTs bs1 rs = AALTs bs1 rs"

   636 

   637 

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

   639   where

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

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

   642 | "bsimp r = r"

   643 

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

   645   where

   646   "AONE bs >> bs"

   647 | "ACHAR bs c >> bs"

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

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

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

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

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

   653 

   654 lemma contains0:

   655   assumes "a >> bs"

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

   657   using assms

   658   apply(induct arbitrary: bs1)

   659   apply(auto intro: contains.intros)

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

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

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

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

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

   665   done

   666 

   667 lemma contains1:

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

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

   670   using assms

   671   apply(induct vs)

   672    apply(simp)

   673   using contains.simps apply blast

   674   apply(simp)

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

   676   apply(rule contains.intros)

   677    apply(auto)

   678   done

   679 

   680 

   681 lemma contains2:

   682   assumes "\<Turnstile> v : r"

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

   684   using assms

   685   apply(induct)

   686        prefer 4

   687        apply(simp)

   688        apply(rule contains.intros)

   689    prefer 4

   690        apply(simp)

   691       apply(rule contains.intros)

   692      apply(simp)

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

   694   apply(rule contains.intros)

   695       apply(simp)

   696   apply(simp)

   697     apply(simp)

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

   699     apply(rule contains.intros)

   700     apply (metis append_Cons append_self_conv2 contains0)

   701     apply(simp)

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

   703    apply(rule contains.intros)

   704    back

   705    apply(rule contains.intros)

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

   707    apply(simp)

   708   apply(simp)

   709   apply(case_tac vs)

   710    apply(simp)

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

   712   using contains1 by blast

   713 

   714 lemma qq1:

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

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

   717   using assms

   718   apply(induct rs arbitrary: rs1 bs)

   719   apply(simp)

   720   apply(simp)

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

   722 

   723 lemma qq2:

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

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

   726   using assms

   727   apply(induct rs arbitrary: rs1 bs)

   728   apply(simp)

   729   apply(simp)

   730   by (metis append_assoc in_set_conv_decomp r1 r2)

   731 

   732 lemma qq2a:

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

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

   735   using assms

   736   by (simp add: r1)

   737   

   738 lemma qq3:

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

   740   apply(induct rs arbitrary: bs)

   741   apply(simp)

   742   apply(simp)

   743   done

   744 

   745 lemma qq4:

   746   assumes "bnullable (AALTs bs rs)"

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

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

   749 

   750 

   751 lemma contains3a:

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

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

   754   using assms

   755   apply -

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

   757 

   758   

   759 lemma contains3b:

   760   assumes "a >> bs1"

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

   762   using assms

   763   apply -

   764   apply(rule contains.intros)

   765   apply(simp)

   766   done   

   767 

   768 

   769 lemma contains3:

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

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

   772   using assms

   773   apply(induct rs arbitrary: bs x)

   774    apply simp

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

   776 

   777 lemma cont1:

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

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

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

   781   using assms 

   782   apply(induct vs arbitrary: bs r)

   783    apply(simp)

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

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

   786   

   787 lemma contains4:

   788   assumes "bnullable a"

   789   shows "a >> bmkeps a"

   790   using assms

   791   apply(induct a rule: bnullable.induct)

   792        apply(auto intro: contains.intros)

   793   using contains3 by blast

   794 

   795 lemma contains5:

   796   assumes "\<Turnstile> v : r"

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

   798   using contains2[OF assms] retrieve_code[OF assms]

   799   by (simp)

   800 

   801 lemma contains6:

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

   803   shows "r >> retrieve r v"

   804   using assms

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

   806   apply(auto)[1]

   807   using Prf_elims(1) apply blast

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

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

   810   apply(auto)[1]

   811   using Prf_elims(1) apply blast

   812   apply(auto)[1]

   813   using contains3b contains3a apply blast

   814     prefer 2

   815   apply(auto)[1]

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

   817    prefer 2

   818   apply(auto)[1]

   819    apply (metis Prf_elims(6) cont1)

   820   apply(simp)

   821   apply(erule Prf_elims)

   822    apply(auto)

   823    apply (simp add: contains3b)

   824   using retrieve_fuse2 contains3b contains3a

   825   apply(subst retrieve_fuse2[symmetric])

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

   827   apply(simp)

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

   829 

   830 lemma contains7:

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

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

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

   834   by (metis assms contains6 erase_bder)

   835 

   836 

   837 lemma contains7a:

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

   839   shows "r >> retrieve r (injval (erase r) c v)"

   840   using assms

   841   apply -

   842   apply(drule Prf_injval)

   843   apply(drule contains6)

   844   apply(simp)

   845   done

   846 

   847 fun 

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

   849 where

   850   "bders_simp r [] = r"

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

   852 

   853 definition blexer_simp where

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

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

   856 

   857 

   858 

   859 

   860 

   861 lemma bders_simp_append:

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

   863   apply(induct s1 arbitrary: r s2)

   864    apply(simp)

   865   apply(simp)

   866   done

   867 

   868 lemma bsimp_ASEQ_size:

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

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

   871   apply(auto)

   872   done

   873 

   874 

   875 

   876 lemma flts_size:

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

   878   apply(induct rs rule: flts.induct)

   879         apply(simp_all)

   880   by (simp add: asize_fuse comp_def)

   881   

   882 

   883 lemma bsimp_AALTs_size:

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

   885   apply(induct rs rule: bsimp_AALTs.induct)

   886   apply(auto simp add: asize_fuse)

   887   done

   888 

   889 

   890 lemma bsimp_size:

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

   892   apply(induct r)

   893        apply(simp_all)

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

   895   apply(rule le_trans)

   896    apply(rule bsimp_AALTs_size)

   897   apply(simp)

   898    apply(rule le_trans)

   899    apply(rule flts_size)

   900   by (simp add: sum_list_mono)

   901 

   902 lemma bsimp_asize0:

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

   904   apply(induct rs)

   905    apply(auto)

   906   by (simp add: add_mono bsimp_size)

   907 

   908 lemma bsimp_AALTs_size2:

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

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

   911   using assms

   912   apply(induct rs rule: bsimp_AALTs.induct)

   913     apply(simp_all add: asize_fuse)

   914   done

   915 

   916 

   917 lemma qq:

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

   919   apply(induct rs)

   920    apply(auto simp add: asize_fuse)

   921   done

   922 

   923 lemma flts_size2:

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

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

   926   using assms

   927   apply(induct rs)

   928    apply(auto simp add: qq)

   929    apply (simp add: flts_size less_Suc_eq_le)

   930   apply(case_tac a)

   931        apply(auto simp add: qq)

   932    prefer 2

   933    apply (simp add: flts_size le_imp_less_Suc)

   934   using less_Suc_eq by auto

   935 

   936 lemma bsimp_AALTs_size3:

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

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

   939   using assms flts_size2

   940   apply  -

   941   apply(clarify)

   942   apply(simp)

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

   944   apply(drule meta_mp)

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

   946   apply(simp)

   947   apply(rule order_class.order.strict_trans1)

   948    apply(rule bsimp_AALTs_size)

   949   apply(simp)

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

   951 

   952 

   953 

   954 

   955 lemma L_bsimp_ASEQ:

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

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

   958   apply(simp_all)

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

   960 

   961 lemma L_bsimp_AALTs:

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

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

   964   apply(simp_all add: erase_fuse)

   965   done

   966 

   967 lemma L_erase_AALTs:

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

   969   apply(induct rs)

   970    apply(simp)

   971   apply(simp)

   972   apply(case_tac rs)

   973    apply(simp)

   974   apply(simp)

   975   done

   976 

   977 lemma L_erase_flts:

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

   979   apply(induct rs rule: flts.induct)

   980         apply(simp_all)

   981   apply(auto)

   982   using L_erase_AALTs erase_fuse apply auto[1]

   983   by (simp add: L_erase_AALTs erase_fuse)

   984 

   985 

   986 lemma L_bsimp_erase:

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

   988   apply(induct r)

   989   apply(simp)

   990   apply(simp)

   991   apply(simp)

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

   993   apply(subst L_bsimp_ASEQ[symmetric])

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

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

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

   997    apply(simp)

   998    apply(subst L_bsimp_AALTs[symmetric])

   999    defer

  1000    apply(simp)

  1001   apply(subst (2)L_erase_AALTs)

  1002   apply(subst L_erase_flts)

  1003   apply(auto)

  1004    apply (simp add: L_erase_AALTs)

  1005   using L_erase_AALTs by blast

  1006 

  1007 lemma bsimp_ASEQ0:

  1008   shows "bsimp_ASEQ bs r1 AZERO = AZERO"

  1009   apply(induct r1)

  1010   apply(auto)

  1011   done

  1012 

  1013 

  1014 

  1015 lemma bsimp_ASEQ1:

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

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

  1018   using assms

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

  1020   apply(auto)

  1021   done

  1022 

  1023 lemma bsimp_ASEQ2:

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

  1025   apply(induct r2)

  1026   apply(auto)

  1027   done

  1028 

  1029 

  1030 lemma L_bders_simp:

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

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

  1033    apply(simp)

  1034   apply(simp)

  1035   apply(simp add: ders_append)

  1036   apply(simp add: bders_simp_append)

  1037   apply(simp add: L_bsimp_erase[symmetric])

  1038   by (simp add: der_correctness)

  1039 

  1040 lemma b1:

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

  1042   apply(induct r)

  1043        apply(auto)

  1044   done

  1045 

  1046 lemma b2:

  1047   assumes "bnullable r"

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

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

  1050 

  1051 lemma b3:

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

  1053   using L_bsimp_erase bnullable_correctness nullable_correctness by auto

  1054 

  1055 

  1056 lemma b4:

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

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

  1059 

  1060 lemma q1:

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

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

  1063   using assms

  1064   apply(induct rs)

  1065   apply(simp)

  1066   apply(simp)

  1067   done

  1068 

  1069 lemma q3:

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

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

  1072   using assms

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

  1074     apply(simp)

  1075    apply(simp)

  1076   apply (simp add: b2)

  1077   apply(simp)

  1078   done

  1079 

  1080 

  1081 lemma fuse_empty:

  1082   shows "fuse [] r = r"

  1083   apply(induct r)

  1084        apply(auto)

  1085   done

  1086 

  1087 lemma flts_fuse:

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

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

  1090         apply(auto simp add: fuse_append)

  1091   done

  1092 

  1093 lemma bsimp_ASEQ_fuse:

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

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

  1096   apply(auto)

  1097   done

  1098 

  1099 lemma bsimp_AALTs_fuse:

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

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

  1102   using assms

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

  1104   apply(auto)

  1105   done

  1106 

  1107 

  1108 

  1109 lemma bsimp_fuse:

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

  1111 apply(induct r arbitrary: bs)

  1112        apply(simp)

  1113       apply(simp)

  1114      apply(simp)

  1115     prefer 3

  1116     apply(simp)

  1117    apply(simp)

  1118    apply (simp add: bsimp_ASEQ_fuse)

  1119   apply(simp)

  1120   by (simp add: bsimp_AALTs_fuse fuse_append)

  1121 

  1122 lemma bsimp_fuse_AALTs:

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

  1124   apply(subst bsimp_fuse) 

  1125   apply(simp)

  1126   done

  1127 

  1128 lemma bsimp_fuse_AALTs2:

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

  1130   using bsimp_AALTs_fuse fuse_append by auto

  1131   

  1132 

  1133 lemma bsimp_ASEQ_idem:

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