1 

     2 theory BitCodedCT

     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 

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

   557   where

   558   "distinctBy [] f acc = []"

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

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

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

   562 

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

   564   where 

   565   "flts [] = []"

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

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

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

   569 

   570 

   571 

   572 

   573 fun li :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp"

   574   where

   575   "li _ [] = AZERO"

   576 | "li bs [a] = fuse bs a"

   577 | "li bs as = AALTs bs as"

   578 

   579 

   580 

   581 

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

   583   where

   584   "bsimp_ASEQ _ AZERO _ = AZERO"

   585 | "bsimp_ASEQ _ _ AZERO = AZERO"

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

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

   588 

   589 

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

   591   where

   592   "bsimp_AALTs _ [] = AZERO"

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

   594 | "bsimp_AALTs bs1 rs = AALTs bs1 rs"

   595 

   596 

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

   598   where

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

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

   601 | "bsimp r = r"

   602 

   603 

   604 

   605 

   606 fun 

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

   608 where

   609   "bders_simp r [] = r"

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

   611 

   612 definition blexer_simp where

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

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

   615 

   616 

   617 lemma asize0:

   618   shows "0 < asize r"

   619   apply(induct  r)

   620        apply(auto)

   621   done

   622 

   623 

   624 lemma bders_simp_append:

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

   626   apply(induct s1 arbitrary: r s2)

   627    apply(simp)

   628   apply(simp)

   629   done

   630 

   631 lemma bsimp_ASEQ_size:

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

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

   634   apply(auto)

   635   done

   636 

   637 lemma fuse_size:

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

   639   apply(induct r)

   640   apply(auto)

   641   done

   642 

   643 lemma flts_size:

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

   645   apply(induct rs rule: flts.induct)

   646         apply(simp_all)

   647   by (metis (mono_tags, lifting) add_mono comp_apply eq_imp_le fuse_size le_SucI map_eq_conv)

   648   

   649 

   650 lemma bsimp_AALTs_size:

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

   652   apply(induct rs rule: bsimp_AALTs.induct)

   653   apply(auto simp add: fuse_size)

   654   done

   655 

   656 

   657 lemma bsimp_size:

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

   659   apply(induct r)

   660        apply(simp_all)

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

   662   apply(rule le_trans)

   663    apply(rule bsimp_AALTs_size)

   664   apply(simp)

   665    apply(rule le_trans)

   666    apply(rule flts_size)

   667   by (simp add: sum_list_mono)

   668 

   669 lemma bsimp_asize0:

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

   671   apply(induct rs)

   672    apply(auto)

   673   by (simp add: add_mono bsimp_size)

   674 

   675 lemma bsimp_AALTs_size2:

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

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

   678   using assms

   679   apply(induct rs rule: bsimp_AALTs.induct)

   680     apply(simp_all add: fuse_size)

   681   done

   682 

   683 

   684 lemma qq:

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

   686   apply(induct rs)

   687    apply(auto simp add: fuse_size)

   688   done

   689 

   690 lemma flts_size2:

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

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

   693   using assms

   694   apply(induct rs)

   695    apply(auto simp add: qq)

   696    apply (simp add: flts_size less_Suc_eq_le)

   697   apply(case_tac a)

   698        apply(auto simp add: qq)

   699    prefer 2

   700    apply (simp add: flts_size le_imp_less_Suc)

   701   using less_Suc_eq by auto

   702 

   703 lemma bsimp_AALTs_size3:

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

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

   706   using assms flts_size2

   707   apply  -

   708   apply(clarify)

   709   apply(simp)

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

   711   apply(drule meta_mp)

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

   713   apply(simp)

   714   apply(rule order_class.order.strict_trans1)

   715    apply(rule bsimp_AALTs_size)

   716   apply(simp)

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

   718 

   719 

   720 

   721 

   722 lemma L_bsimp_ASEQ:

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

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

   725   apply(simp_all)

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

   727 

   728 lemma L_bsimp_AALTs:

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

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

   731   apply(simp_all add: erase_fuse)

   732   done

   733 

   734 lemma L_erase_AALTs:

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

   736   apply(induct rs)

   737    apply(simp)

   738   apply(simp)

   739   apply(case_tac rs)

   740    apply(simp)

   741   apply(simp)

   742   done

   743 

   744 lemma L_erase_flts:

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

   746   apply(induct rs rule: flts.induct)

   747         apply(simp_all)

   748   apply(auto)

   749   using L_erase_AALTs erase_fuse apply auto[1]

   750   by (simp add: L_erase_AALTs erase_fuse)

   751 

   752 

   753 lemma L_bsimp_erase:

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

   755   apply(induct r)

   756   apply(simp)

   757   apply(simp)

   758   apply(simp)

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

   760   apply(subst L_bsimp_ASEQ[symmetric])

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

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

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

   764    apply(simp)

   765    apply(subst L_bsimp_AALTs[symmetric])

   766    defer

   767    apply(simp)

   768   apply(subst (2)L_erase_AALTs)

   769   apply(subst L_erase_flts)

   770   apply(auto)

   771    apply (simp add: L_erase_AALTs)

   772   using L_erase_AALTs by blast

   773 

   774 lemma bsimp_ASEQ0:

   775   shows "bsimp_ASEQ bs r1 AZERO = AZERO"

   776   apply(induct r1)

   777   apply(auto)

   778   done

   779 

   780 

   781 

   782 lemma bsimp_ASEQ1:

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

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

   785   using assms

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

   787   apply(auto)

   788   done

   789 

   790 lemma bsimp_ASEQ2:

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

   792   apply(induct r2)

   793   apply(auto)

   794   done

   795 

   796 

   797 lemma L_bders_simp:

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

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

   800    apply(simp)

   801   apply(simp)

   802   apply(simp add: ders_append)

   803   apply(simp add: bders_simp_append)

   804   apply(simp add: L_bsimp_erase[symmetric])

   805   by (simp add: der_correctness)

   806 

   807 lemma b1:

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

   809   apply(induct r)

   810        apply(auto)

   811   done

   812 

   813 lemma b2:

   814   assumes "bnullable r"

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

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

   817 

   818 lemma b3:

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

   820   using L_bsimp_erase bnullable_correctness nullable_correctness by auto

   821 

   822 

   823 lemma b4:

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

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

   826 

   827 lemma q1:

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

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

   830   using assms

   831   apply(induct rs)

   832   apply(simp)

   833   apply(simp)

   834   done

   835 

   836 lemma q3:

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

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

   839   using assms

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

   841     apply(simp)

   842    apply(simp)

   843   apply (simp add: b2)

   844   apply(simp)

   845   done

   846 

   847 lemma qq1:

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

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

   850   using assms

   851   apply(induct rs arbitrary: rs1 bs)

   852   apply(simp)

   853   apply(simp)

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

   855 

   856 lemma qq2:

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

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

   859   using assms

   860   apply(induct rs arbitrary: rs1 bs)

   861   apply(simp)

   862   apply(simp)

   863   by (metis append_assoc in_set_conv_decomp r1 r2)

   864   

   865 lemma qq3:

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

   867   apply(induct rs arbitrary: bs)

   868   apply(simp)

   869   apply(simp)

   870   done

   871 

   872 lemma fuse_empty:

   873   shows "fuse [] r = r"

   874   apply(induct r)

   875        apply(auto)

   876   done

   877 

   878 lemma flts_fuse:

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

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

   881         apply(auto simp add: fuse_append)

   882   done

   883 

   884 lemma bsimp_ASEQ_fuse:

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

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

   887   apply(auto)

   888   done

   889 

   890 lemma bsimp_AALTs_fuse:

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

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

   893   using assms

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

   895   apply(auto)

   896   done

   897 

   898 

   899 

   900 lemma bsimp_fuse:

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

   902 apply(induct r arbitrary: bs)

   903        apply(simp)

   904       apply(simp)

   905      apply(simp)

   906     prefer 3

   907     apply(simp)

   908    apply(simp)

   909    apply (simp add: bsimp_ASEQ_fuse)

   910   apply(simp)

   911   by (simp add: bsimp_AALTs_fuse fuse_append)

   912 

   913 lemma bsimp_fuse_AALTs:

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

   915   apply(subst bsimp_fuse) 

   916   apply(simp)

   917   done

   918 

   919 lemma bsimp_fuse_AALTs2:

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

   921   using bsimp_AALTs_fuse fuse_append by auto

   922   

   923 

   924 lemma bsimp_ASEQ_idem:

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

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

   927   using assms

   928   apply(case_tac "bsimp r1 = AZERO")

   929     apply(simp)

   930  apply(case_tac "bsimp r2 = AZERO")

   931     apply(simp)

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

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

   934     apply(auto)[1]

   935     apply(subst bsimp_ASEQ2)

   936    apply(subst bsimp_ASEQ2)

   937   apply (metis assms(2) bsimp_fuse)

   938       apply(subst bsimp_ASEQ1)

   939       apply(auto)

   940   done

   941 

   942 

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

   944   where

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

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

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

   948 | "nonnested r = True"

   949 

   950 

   951 lemma  k0:

   952   shows "flts (r # rs1) = flts [r] @ flts rs1"

   953   apply(induct r arbitrary: rs1)

   954    apply(auto)

   955   done

   956 

   957 lemma  k00:

   958   shows "flts (rs1 @ rs2) = flts rs1 @ flts rs2"

   959   apply(induct rs1 arbitrary: rs2)

   960    apply(auto)

   961   by (metis append.assoc k0)

   962 

   963 lemma  k0a:

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

   965   apply(simp)

   966   done

   967 

   968 

   969 lemma  k0b:

   970   assumes "nonalt r" "r \<noteq> AZERO"

   971   shows "flts [r] = [r]"

   972   using assms

   973   apply(case_tac  r)

   974   apply(simp_all)

   975   done

   976 

   977 lemma nn1:

   978   assumes "nonnested (AALTs bs rs)"

   979   shows "\<nexists>bs1 rs1. flts rs = [AALTs bs1 rs1]"

   980   using assms

   981   apply(induct rs rule: flts.induct)

   982   apply(auto)

   983   done

   984 

   985 lemma nn1q:

   986   assumes "nonnested (AALTs bs rs)"

   987   shows "\<nexists>bs1 rs1. AALTs bs1 rs1 \<in> set (flts rs)"

   988   using assms

   989   apply(induct rs rule: flts.induct)

   990   apply(auto)

   991   done

   992 

   993 lemma nn1qq:

   994   assumes "nonnested (AALTs bs rs)"

   995   shows "\<nexists>bs1 rs1. AALTs bs1 rs1 \<in> set rs"

   996   using assms

   997   apply(induct rs rule: flts.induct)

   998   apply(auto)

   999   done

  1000 

  1001 lemma nn10:

  1002   assumes "nonnested (AALTs cs rs)" 

  1003   shows "nonnested (AALTs (bs @ cs) rs)"

  1004   using assms

  1005   apply(induct rs arbitrary: cs bs)

  1006    apply(simp_all)

  1007   apply(case_tac a)

  1008        apply(simp_all)

  1009   done

  1010 

  1011 lemma nn11a:

  1012   assumes "nonalt r"

  1013   shows "nonalt (fuse bs r)"

  1014   using assms

  1015   apply(induct r)

  1016        apply(auto)

  1017   done

  1018 

  1019 

  1020 lemma nn1a:

  1021   assumes "nonnested r"

  1022   shows "nonnested (fuse bs r)"

  1023   using assms

  1024   apply(induct bs r arbitrary: rule: fuse.induct)

  1025        apply(simp_all add: nn10)

  1026   done  

  1027 

  1028 lemma n0:

  1029   shows "nonnested (AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. nonalt r)"

  1030   apply(induct rs  arbitrary: bs)

  1031    apply(auto)

  1032     apply (metis list.set_intros(1) nn1qq nonalt.elims(3))

  1033    apply (metis list.set_intros(2) nn1qq nonalt.elims(3))

  1034   by (metis nonalt.elims(2) nonnested.simps(3) nonnested.simps(4) nonnested.simps(5) nonnested.simps(6) nonnested.simps(7))

  1035 

  1036   

  1037   

  1038 

  1039 lemma nn1c:

  1040   assumes "\<forall>r \<in> set rs. nonnested r"

  1041   shows "\<forall>r \<in> set (flts rs). nonalt r"

  1042   using assms

  1043   apply(induct rs rule: flts.induct)

  1044         apply(auto)

  1045   apply(rule nn11a)

  1046   by (metis nn1qq nonalt.elims(3))

  1047 

  1048 lemma nn1bb:

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

  1050   shows "nonnested (bsimp_AALTs bs rs)"

  1051   using assms

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

  1053     apply(auto)

  1054    apply (metis nn11a nonalt.simps(1) nonnested.elims(3))

  1055   using n0 by auto

  1056     

  1057 lemma nn1b:

  1058   shows "nonnested (bsimp r)"

  1059   apply(induct r)

  1060        apply(simp_all)

  1061   apply(case_tac "bsimp r1 = AZERO")

  1062     apply(simp)

  1063  apply(case_tac "bsimp r2 = AZERO")

  1064    apply(simp)

  1065     apply(subst bsimp_ASEQ0)

  1066   apply(simp)

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

  1068     apply(auto)[1]

  1069     apply(subst bsimp_ASEQ2)

  1070   apply (simp add: nn1a)    

  1071    apply(subst bsimp_ASEQ1)

  1072       apply(auto)

  1073   apply(rule nn1bb)

  1074   apply(auto)

  1075   by (metis (mono_tags, hide_lams) imageE nn1c set_map)

  1076 

  1077 lemma nn1d:

  1078   assumes "bsimp r = AALTs bs rs"

  1079   shows "\<forall>r1 \<in> set rs. \<forall>  bs. r1 \<noteq> AALTs bs  rs2"

  1080   using nn1b assms

  1081   by (metis nn1qq)

  1082 

  1083 lemma nn_flts:

  1084   assumes "nonnested (AALTs bs rs)"

  1085   shows "\<forall>r \<in>  set (flts rs). nonalt r"

  1086   using assms

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

  1088         apply(auto)

  1089   done

  1090 

  1091 

  1092 

  1093 lemma rt:

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

  1095   apply(induct rs)

  1096    apply(simp)

  1097   apply(simp)

  1098   apply(subst  k0)

  1099   apply(simp)

  1100   by (smt add_le_cancel_right add_mono bsimp_size flts.simps(1) flts_size k0 le_iff_add list.simps(9) map_append sum_list.Cons sum_list.append trans_le_add1)

  1101 

  1102 lemma bsimp_AALTs_qq:

  1103   assumes "1 < length rs"

  1104   shows "bsimp_AALTs bs rs = AALTs bs  rs"

  1105   using  assms

  1106   apply(case_tac rs)

  1107    apply(simp)

  1108   apply(case_tac list)

  1109    apply(simp_all)

  1110   done

  1111 

  1112 

  1113 lemma bsimp_AALTs1:

  1114   assumes "nonalt r"

  1115   shows "bsimp_AALTs bs (flts [r]) = fuse bs r"

  1116   using  assms

  1117   apply(case_tac r)

  1118    apply(simp_all)

  1119   done

  1120 

  1121 lemma bbbbs:

  1122   assumes "good r" "r = AALTs bs1 rs"

  1123   shows "bsimp_AALTs bs (flts [r]) = AALTs bs (map (fuse bs1) rs)"

  1124   using  assms

  1125   by (metis (no_types, lifting) Nil_is_map_conv append.left_neutral append_butlast_last_id bsimp_AALTs.elims butlast.simps(2) good.simps(4) good.simps(5) k0a map_butlast)

  1126 

  1127 lemma bbbbs1:

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

  1129   using nonalt.elims(3) by auto

  1130   

  1131 

  1132 lemma good_fuse:

  1133   shows "good (fuse bs r) = good r"

  1134   apply(induct r arbitrary: bs)

  1135        apply(auto)