1 

     2 theory SizeBound2

     3   imports "Lexer" 

     4 begin

     5 

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

     7 

     8 datatype bit = Z | S

     9 

    10 fun code :: "val \<Rightarrow> bit list"

    11 where

    12   "code Void = []"

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

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

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

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

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

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

    19 

    20 

    21 fun 

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

    23 where

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

    25 

    26 function

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

    28 where

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

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

    31 | "decode' ds (CH d) = (Char d, ds)"

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

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

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

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

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

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

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

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

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

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

    42 by pat_completeness auto

    43 

    44 lemma decode'_smaller:

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

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

    47 using assms

    48 apply(induct ds r)

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

    50 using dual_order.trans apply blast

    51 by (meson dual_order.trans le_SucI)

    52 

    53 termination "decode'"  

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

    55 apply(auto dest!: decode'_smaller)

    56 by (metis less_Suc_eq_le snd_conv)

    57 

    58 definition

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

    60 where

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

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

    63 

    64 lemma decode'_code_Stars:

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

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

    67   using assms

    68   apply(induct vs)

    69   apply(auto)

    70   done

    71 

    72 lemma decode'_code:

    73   assumes "\<Turnstile> v : r"

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

    75 using assms

    76   apply(induct v r arbitrary: ds) 

    77   apply(auto)

    78   using decode'_code_Stars by blast

    79 

    80 lemma decode_code:

    81   assumes "\<Turnstile> v : r"

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

    83   using assms unfolding decode_def

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

    85 

    86 

    87 section {* Annotated Regular Expressions *}

    88 

    89 datatype arexp = 

    90   AZERO

    91 | AONE "bit list"

    92 | ACHAR "bit list" char

    93 | ASEQ "bit list" arexp arexp

    94 | AALTs "bit list" "arexp list"

    95 | ASTAR "bit list" arexp

    96 

    97 abbreviation

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

    99 

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

   101   "asize AZERO = 1"

   102 | "asize (AONE cs) = 1" 

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

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

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

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

   107 

   108 fun 

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

   110 where

   111   "erase AZERO = ZERO"

   112 | "erase (AONE _) = ONE"

   113 | "erase (ACHAR _ c) = CH c"

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

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

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

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

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

   119 

   120 

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

   122   "fuse bs AZERO = AZERO"

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

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

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

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

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

   128 

   129 lemma fuse_append:

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

   131   apply(induct r)

   132   apply(auto)

   133   done

   134 

   135 lemma fuse_Nil:

   136   shows "fuse [] r = r"

   137   by (induct r)(simp_all)

   138 

   139 lemma map_fuse_Nil:

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

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

   142 

   143 

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

   145   "intern ZERO = AZERO"

   146 | "intern ONE = AONE []"

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

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

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

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

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

   152 

   153 

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

   155   "retrieve (AONE bs) Void = bs"

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

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

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

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

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

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

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

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

   164 

   165 

   166 

   167 fun

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

   169 where

   170   "bnullable (AZERO) = False"

   171 | "bnullable (AONE bs) = True"

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

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

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

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

   176 

   177 fun 

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

   179 where

   180   "bmkeps(AONE bs) = bs"

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

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

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

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

   185 

   186 

   187 fun

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

   189 where

   190   "bder c (AZERO) = AZERO"

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

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

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

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

   195      (if bnullable r1

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

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

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

   199 

   200 

   201 fun 

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

   203 where

   204   "bders r [] = r"

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

   206 

   207 lemma bders_append:

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

   209   apply(induct s1 arbitrary: r s2)

   210   apply(simp_all)

   211   done

   212 

   213 lemma bnullable_correctness:

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

   215   apply(induct r rule: erase.induct)

   216   apply(simp_all)

   217   done

   218 

   219 lemma erase_fuse:

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

   221   apply(induct r rule: erase.induct)

   222   apply(simp_all)

   223   done

   224 

   225 lemma erase_intern [simp]:

   226   shows "erase (intern r) = r"

   227   apply(induct r)

   228   apply(simp_all add: erase_fuse)

   229   done

   230 

   231 lemma erase_bder [simp]:

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

   233   apply(induct r rule: erase.induct)

   234   apply(simp_all add: erase_fuse bnullable_correctness)

   235   done

   236 

   237 lemma erase_bders [simp]:

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

   239   apply(induct s arbitrary: r )

   240   apply(simp_all)

   241   done

   242 

   243 lemma bnullable_fuse:

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

   245   apply(induct r arbitrary: bs)

   246   apply(auto)

   247   done

   248 

   249 lemma retrieve_encode_STARS:

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

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

   252   using assms

   253   apply(induct vs)

   254   apply(simp_all)

   255   done

   256 

   257 

   258 lemma retrieve_fuse2:

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

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

   261   using assms

   262   apply(induct r arbitrary: v bs)

   263          apply(auto elim: Prf_elims)[4]

   264    defer

   265   using retrieve_encode_STARS

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

   267    apply(case_tac vs)

   268     apply(simp)

   269    apply(simp)

   270   (* AALTs  case *)

   271   apply(simp)

   272   apply(case_tac x2a)

   273    apply(simp)

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

   275   apply(simp)

   276    apply(case_tac list)

   277    apply(simp)

   278   apply(auto)

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

   280   done

   281 

   282 lemma retrieve_fuse:

   283   assumes "\<Turnstile> v : r"

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

   285   using assms 

   286   by (simp_all add: retrieve_fuse2)

   287 

   288 

   289 lemma retrieve_code:

   290   assumes "\<Turnstile> v : r"

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

   292   using assms

   293   apply(induct v r )

   294   apply(simp_all add: retrieve_fuse retrieve_encode_STARS)

   295   done

   296 

   297 

   298 lemma bnullable_Hdbmkeps_Hd:

   299   assumes "bnullable a" 

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

   301   using assms

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

   303 

   304 lemma r1:

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

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

   307   using assms

   308   apply(induct rs)

   309    apply(auto)

   310   done

   311 

   312 lemma r2:

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

   314   shows "bnullable (AALTs bs rs)"

   315   using assms

   316   apply(induct rs)

   317    apply(auto)

   318   done

   319 

   320 lemma  r3:

   321   assumes "\<not> bnullable r" 

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

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

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

   325   using assms

   326   apply(induct rs arbitrary: r bs)

   327    apply(auto)[1]

   328   apply(auto)

   329   using bnullable_correctness apply blast

   330     apply(auto simp add: bnullable_correctness mkeps_nullable retrieve_fuse2)

   331    apply(subst retrieve_fuse2[symmetric])

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

   333    apply(simp)

   334   apply(case_tac "bnullable a")

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

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

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

   338   apply(drule meta_mp)

   339    apply(simp)

   340   apply(drule meta_mp)

   341    apply(auto)

   342   apply(subst retrieve_fuse2[symmetric])

   343   apply(case_tac rs)

   344     apply(simp)

   345    apply(auto)[1]

   346       apply (simp add: bnullable_correctness)

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

   348     apply (simp add: bnullable_correctness)

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

   350   apply(simp)

   351   done

   352 

   353 

   354 lemma t: 

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

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

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

   358   using assms

   359   apply(induct rs arbitrary: bs)

   360    apply(simp)

   361   apply(auto simp add: bnullable_correctness)

   362    apply(case_tac rs)

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

   364    apply(subst r1)

   365      apply(simp)

   366     apply(rule r2)

   367      apply(assumption)

   368     apply(simp)

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

   370    apply(drule meta_mp)

   371     apply(auto)[1]

   372    prefer 2

   373   apply(case_tac "bnullable a")

   374     apply(subst bnullable_Hdbmkeps_Hd)

   375      apply blast

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

   377   prefer 2

   378   using bnullable_correctness apply blast

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

   380   apply(subst r1)

   381      apply(simp)

   382   using r2 apply blast

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

   384    apply(drule meta_mp)

   385     apply(auto)[1]

   386    apply(simp)

   387   using r3 apply blast

   388   apply(auto)

   389   using r3 by blast

   390 

   391 lemma bmkeps_retrieve:

   392   assumes "nullable (erase r)"

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

   394   using assms

   395   apply(induct r)

   396          apply(simp)

   397         apply(simp)

   398        apply(simp)

   399     apply(simp)

   400    defer

   401    apply(simp)

   402   apply(rule t)

   403    apply(auto)

   404   done

   405 

   406 lemma bder_retrieve:

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

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

   409   using assms

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

   411          apply(simp)

   412          apply(erule Prf_elims)

   413         apply(simp)

   414         apply(erule Prf_elims) 

   415         apply(simp)

   416       apply(case_tac "c = ca")

   417        apply(simp)

   418        apply(erule Prf_elims)

   419        apply(simp)

   420       apply(simp)

   421        apply(erule Prf_elims)

   422   apply(simp)

   423       apply(erule Prf_elims)

   424      apply(simp)

   425     apply(simp)

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

   427     apply(erule Prf_elims)

   428      apply(simp)

   429     apply(simp)

   430     apply(case_tac rs)

   431      apply(simp)

   432     apply(simp)

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

   434    apply(simp)

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

   436     apply(simp)

   437   apply(erule Prf_elims)

   438      apply(subgoal_tac "bnullable r1")

   439   prefer 2

   440   using bnullable_correctness apply blast

   441     apply(simp)

   442      apply(erule Prf_elims)

   443      apply(simp)

   444    apply(subgoal_tac "bnullable r1")

   445   prefer 2

   446   using bnullable_correctness apply blast

   447     apply(simp)

   448     apply(simp add: retrieve_fuse2)

   449     apply(simp add: bmkeps_retrieve)

   450    apply(simp)

   451    apply(erule Prf_elims)

   452    apply(simp)

   453   using bnullable_correctness apply blast

   454   apply(rename_tac bs r v)

   455   apply(simp)

   456   apply(erule Prf_elims)

   457      apply(clarify)

   458   apply(erule Prf_elims)

   459   apply(clarify)

   460   apply(subst injval.simps)

   461   apply(simp del: retrieve.simps)

   462   apply(subst retrieve.simps)

   463   apply(subst retrieve.simps)

   464   apply(simp)

   465   apply(simp add: retrieve_fuse2)

   466   done

   467   

   468 

   469 

   470 lemma MAIN_decode:

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

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

   473   using assms

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

   475   case Nil

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

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

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

   479     using decode_code retrieve_code by auto

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

   481     by simp

   482 next

   483   case (snoc c s v)

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

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

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

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

   488     by (simp add: Prf_injval ders_append)

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

   490     by (simp add: flex_append)

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

   492     using asm2 IH by simp

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

   494     using asm by (simp_all add: bder_retrieve ders_append)

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

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

   497 qed

   498 

   499 

   500 definition blex where

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

   502 

   503 

   504 

   505 definition blexer where

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

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

   508 

   509 lemma blexer_correctness:

   510   shows "blexer r s = lexer r s"

   511 proof -

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

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

   514     assume asm: "nullable ds"

   515     have era: "erase bds = ds" 

   516       unfolding ds_def bds_def by simp

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

   518       using asm by (simp add: mkeps_nullable)

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

   520       using bmkeps_retrieve

   521       using asm era by (simp add: bmkeps_retrieve)

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

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

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

   525       unfolding bds_def ds_def .

   526   }

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

   528     unfolding blexer_def lexer_flex

   529     apply(subst bnullable_correctness[symmetric])

   530     apply(simp)

   531     done

   532 qed

   533 

   534 

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

   536   where

   537   "distinctBy [] f acc = []"

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

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

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

   541 

   542 lemma dB_single_step: 

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

   544   by simp 

   545 

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

   547   where 

   548   "flts [] = []"

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

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

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

   552 

   553 

   554 

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

   556   where

   557   "bsimp_ASEQ _ AZERO _ = AZERO"

   558 | "bsimp_ASEQ _ _ AZERO = AZERO"

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

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

   561 

   562 

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

   564   where

   565   "bsimp_AALTs _ [] = AZERO"

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

   567 | "bsimp_AALTs bs1 rs = AALTs bs1 rs"

   568 

   569 

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

   571   where

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

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

   574 | "bsimp r = r"

   575 

   576 

   577 fun 

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

   579 where

   580   "bders_simp r [] = r"

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

   582 

   583 definition blexer_simp where

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

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

   586 

   587 export_code bders_simp in Scala module_name Example

   588 

   589 lemma bders_simp_append:

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

   591   apply(induct s1 arbitrary: r s2)

   592   apply(simp_all)

   593   done

   594 

   595 lemma L_bsimp_ASEQ:

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

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

   598   apply(simp_all)

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

   600 

   601 lemma L_bsimp_AALTs:

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

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

   604   apply(simp_all add: erase_fuse)

   605   done

   606 

   607 lemma L_erase_AALTs:

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

   609   apply(induct rs)

   610    apply(simp)

   611   apply(simp)

   612   apply(case_tac rs)

   613    apply(simp)

   614   apply(simp)

   615   done

   616 

   617 lemma L_erase_flts:

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

   619   apply(induct rs rule: flts.induct)

   620         apply(simp_all)

   621   apply(auto)

   622   using L_erase_AALTs erase_fuse apply auto[1]

   623   by (simp add: L_erase_AALTs erase_fuse)

   624 

   625 lemma L_erase_dB_acc:

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

   627   apply(induction rs arbitrary: acc)

   628    apply simp

   629   apply simp

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

   631 

   632 lemma L_erase_dB:

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

   634   by (metis L_erase_dB_acc Un_commute Union_image_empty)

   635 

   636 lemma L_bsimp_erase:

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

   638   apply(induct r)

   639   apply(simp)

   640   apply(simp)

   641   apply(simp)

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

   643   apply(subst L_bsimp_ASEQ[symmetric])

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

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

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

   647   apply(simp)

   648   apply(subst L_bsimp_AALTs[symmetric])

   649   defer

   650   apply(simp)

   651   apply(subst (2)L_erase_AALTs)

   652   apply(subst L_erase_dB)

   653   apply(subst L_erase_flts)

   654   apply(auto)

   655   apply (simp add: L_erase_AALTs)

   656   using L_erase_AALTs by blast

   657 

   658 

   659 

   660 lemma bsimp_ASEQ0:

   661   shows "bsimp_ASEQ bs r1 AZERO = AZERO"

   662   apply(induct r1)

   663   apply(auto)

   664   done

   665 

   666 lemma bsimp_ASEQ1:

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

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

   669   using assms

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

   671   apply(auto)

   672   done

   673 

   674 lemma bsimp_ASEQ2:

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

   676   apply(induct r2)

   677   apply(auto)

   678   done

   679 

   680 

   681 lemma L_bders_simp:

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

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

   684   apply(simp)

   685   apply(simp)

   686   apply(simp add: ders_append)

   687   apply(simp add: bders_simp_append)

   688   apply(simp add: L_bsimp_erase[symmetric])

   689   by (simp add: der_correctness)

   690 

   691 

   692 lemma b2:

   693   assumes "bnullable r"

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

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

   696 

   697 

   698 lemma b4:

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

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

   701 

   702 lemma qq1:

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

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

   705   using assms

   706   apply(induct rs arbitrary: rs1 bs)

   707   apply(simp)

   708   apply(simp)

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

   710 

   711 lemma qq2:

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

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

   714   using assms

   715   apply(induct rs arbitrary: rs1 bs)

   716   apply(simp)

   717   apply(simp)

   718   by (metis append_assoc in_set_conv_decomp r1 r2)

   719   

   720 lemma qq3:

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

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

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

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

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

   726   using assms

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

   728   using qq1 apply auto[1]

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

   730 

   731 

   732 lemma q3a:

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

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

   735   using assms

   736   apply(induct rs arbitrary: bs bs1)

   737    apply(simp)

   738   apply(simp)

   739   apply(auto)

   740    apply (metis append_assoc b2 bnullable_correctness erase_fuse bnullable_Hdbmkeps_Hd)

   741   apply(case_tac "bnullable a")

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

   743   apply(case_tac rs)

   744   apply(simp)

   745   apply(simp)

   746   apply(auto)[1]

   747    apply (metis bnullable_correctness erase_fuse)+

   748   done

   749 

   750 lemma qq4:

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

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

   753   using assms

   754   apply(induct list rule: flts.induct)

   755         apply(auto)

   756   by (metis UnCI bnullable_correctness erase_fuse imageI)

   757   

   758 

   759 lemma qs3:

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

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

   762   using assms

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

   764   apply(case_tac x)

   765   apply(simp)

   766   apply(simp)

   767   apply(case_tac a)

   768        apply(simp)

   769        apply (simp add: r1)

   770       apply(simp)

   771       apply (simp add: bnullable_Hdbmkeps_Hd)

   772      apply(simp)

   773      apply(case_tac "flts list")

   774       apply(simp)

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

   776      apply(simp)

   777      apply (simp add: r1)

   778     prefer 3

   779     apply(simp)

   780     apply (simp add: bnullable_Hdbmkeps_Hd)

   781    prefer 2

   782    apply(simp)

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

   784   apply(case_tac "list")

   785     apply(simp)

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

   787    apply(erule disjE)

   788     apply(subst qq1)

   789      apply(auto)[1]

   790      apply (metis bnullable_correctness erase_fuse)

   791     apply(simp)

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

   793     apply(simp)

   794     apply(auto)[1]

   795      apply(subst qq1)

   796       apply (metis bnullable_correctness erase_fuse image_eqI set_map)

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

   798   apply(subst qq1)

   799       apply (metis bnullable_correctness erase_fuse image_eqI set_map)

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

   801    apply(simp)

   802    apply(subst qq2)

   803      apply (metis bnullable_correctness erase_fuse imageE set_map)

   804   prefer 2

   805   apply(case_tac "list")

   806      apply(simp)

   807     apply(simp)

   808    apply (simp add: qq4)

   809   apply(simp)

   810   apply(auto)

   811    apply(case_tac list)

   812     apply(simp)

   813    apply(simp)

   814    apply (simp add: bnullable_Hdbmkeps_Hd)

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

   816    apply(case_tac list)

   817     apply(simp)

   818    apply(simp)

   819    apply (simp add: bnullable_Hdbmkeps_Hd)

   820   apply(simp)

   821   using qq4 r1 r2 by auto

   822 

   823 lemma bder_fuse:

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

   825   apply(induct a arbitrary: bs c)

   826        apply(simp_all)

   827   done

   828 

   829 

   830 

   831 

   832 inductive 

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

   834 and 

   835   srewrite:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ s\<leadsto> _" [100, 100] 100)

   836 where

   837   bs1: "ASEQ bs AZERO r2 \<leadsto> AZERO"

   838 | bs2: "ASEQ bs r1 AZERO \<leadsto> AZERO"

   839 | bs3: "ASEQ bs1 (AONE bs2) r \<leadsto> fuse (bs1@bs2) r"

   840 | bs4: "r1 \<leadsto> r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r2 r3"

   841 | bs5: "r3 \<leadsto> r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r1 r4"

   842 | bs6: "AALTs bs [] \<leadsto> AZERO"

   843 | bs7: "AALTs bs [r] \<leadsto> fuse bs r"

   844 | bs10: "rs1 s\<leadsto> rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto> AALTs bs rs2"

   845 | ss1:  "[] s\<leadsto> []"

   846 | ss2:  "rs1 s\<leadsto> rs2 \<Longrightarrow> (r # rs1) s\<leadsto> (r # rs2)"

   847 | ss3:  "r1 \<leadsto> r2 \<Longrightarrow> (r1 # rs) s\<leadsto> (r2 # rs)"

   848 | ss4:  "(AZERO # rs) s\<leadsto> rs"

   849 | ss5:  "(AALTs bs1 rs1 # rsb) s\<leadsto> ((map (fuse bs1) rs1) @ rsb)"

   850 | ss6:  "erase a1 = erase a2 \<Longrightarrow> (rsa@[a1]@rsb@[a2]@rsc) s\<leadsto> (rsa@[a1]@rsb@rsc)"

   851 

   852 inductive 

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

   854 where 

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

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

   857 

   858 inductive 

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

   860 where 

   861   sss1[intro, simp]:"rs s\<leadsto>* rs"

   862 | sss2[intro]: "\<lbrakk>rs1 s\<leadsto> rs2; rs2 s\<leadsto>* rs3\<rbrakk> \<Longrightarrow> rs1 s\<leadsto>* rs3"

   863 

   864 

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

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

   867  

   868 lemma rrewrites_trans[trans]: 

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

   870   shows "r1 \<leadsto>* r3"

   871   using a2 a1

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

   873   apply(auto)

   874   done

   875 

   876 lemma srewrites_trans[trans]: 

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

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

   879   using a1 a2

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

   881    apply(auto)

   882   done

   883 

   884 

   885 lemma rewrite_fuse : 

   886   assumes "r1 \<leadsto> r2"

   887   shows "fuse bs r1 \<leadsto> fuse bs r2"

   888   using assms

   889   apply(induct rule: rrewrite_srewrite.inducts(1))

   890   apply(auto intro: rrewrite_srewrite.intros)

   891   apply (metis bs3 fuse_append)

   892   by (metis bs7 fuse_append)

   893 

   894 lemma contextrewrites0: 

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

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

   897    apply simp

   898   using bs10 r_in_rstar rrewrites_trans by blast

   899 

   900 lemma contextrewrites1: 

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

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

   903    apply simp

   904   using bs10 ss3 by blast

   905 

   906 lemma srewrite1: 

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

   908   apply(induct rs)

   909    apply(auto)

   910   using ss2 by auto

   911 

   912 lemma srewrites1: 

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

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

   915    apply(auto)

   916   using srewrite1 by blast

   917 

   918 lemma srewrite2: 

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

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

   921   apply(induct rule: rrewrite_srewrite.inducts)

   922                apply(auto)

   923      apply (metis append_Cons append_Nil srewrites1)

   924     apply(meson srewrites.simps ss3)

   925   apply (meson srewrites.simps ss4)

   926   apply (meson srewrites.simps ss5)

   927   by (metis append_Cons append_Nil srewrites.simps ss6)

   928   

   929 

   930 lemma srewrites3: 

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

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

   933    apply(auto)

   934   by (meson srewrite2(2) srewrites_trans)

   935 

   936 (*

   937 lemma srewrites4:

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

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

   940   using assms

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

   942   apply (simp add: srewrites3)

   943   using srewrite1 by blast

   944 *)

   945 

   946 lemma srewrites6:

   947   assumes "r1 \<leadsto>* r2" 

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

   949   using assms

   950   

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

   952    apply(auto)

   953   by (meson srewrites.simps srewrites_trans ss3)

   954 

   955 lemma srewrites7:

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

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

   958   using assms

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

   960 

   961 

   962 

   963 lemma star_seq:  

   964   assumes "r1 \<leadsto>* r2"

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

   966 using assms

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

   968 apply(auto intro: rrewrite_srewrite.intros)

   969 done

   970 

   971 lemma star_seq2:  

   972   assumes "r3 \<leadsto>* r4"

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

   974   using assms

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

   976 apply(auto intro: rrewrite_srewrite.intros)

   977 done

   978 

   979 lemma continuous_rewrite: 

   980   assumes "r1 \<leadsto>* AZERO"

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

   982 using assms bs1 star_seq by blast

   983 

   984 

   985 lemma bsimp_aalts_simpcases: 

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

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

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

   989   by (simp_all)

   990 

   991 

   992 lemma trivialbsimp_srewrites: 

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

   994   apply(induction rs)

   995    apply simp

   996   apply(simp)

   997   using srewrites7 by auto

   998 

   999 lemma alts_simpalts: 

  1000   "(\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimp x) \<Longrightarrow> 

  1001   AALTs bs1 rs \<leadsto>* AALTs bs1 (map bsimp rs)"

  1002   apply(induct rs)

  1003    apply(auto)[1]

  1004   using trivialbsimp_srewrites apply auto[1]

  1005   by (simp add: contextrewrites0 srewrites7)

  1006 

  1007 

  1008 lemma bsimp_AALTs_rewrites: 

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

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

  1011 

  1012 lemma fltsfrewrites: "rs s\<leadsto>* (flts rs)"

  1013   

  1014   apply(induction rs)

  1015   apply simp

  1016   apply(case_tac a)

  1017        apply(auto)

  1018   using ss4 apply blast

  1019   using srewrites7 apply force

  1020   using rs1 srewrites7 apply presburger

  1021   using srewrites7 apply force

  1022   apply (meson srewrites.simps srewrites1 ss5)

  1023   by (simp add: srewrites7)

  1024 

  1025 

  1026 lemma flts_rewrites: "AALTs bs1 rs \<leadsto>* AALTs bs1 (flts rs)"

  1027   by (simp add: contextrewrites0 fltsfrewrites)

  1028 

  1029 

  1030 (* delete*)

  1031 lemma threelistsappend: "rsa@a#rsb = (rsa@[a])@rsb"

  1032   apply auto

  1033   done

  1034 

  1035 lemma somewhereInside: "r \<in> set rs \<Longrightarrow> \<exists>rs1 rs2. rs = rs1@[r]@rs2"

  1036   using split_list by fastforce

  1037 

  1038 lemma somewhereMapInside: "f r \<in> f ` set rs \<Longrightarrow> \<exists>rs1 rs2 a. rs = rs1@[a]@rs2 \<and> f a = f r"

  1039   apply auto

  1040   by (metis split_list)

  1041 

  1042 lemma alts_dBrewrites_withFront: 

  1043   "AALTs bs (rsa @ rs) \<leadsto>* AALTs bs (rsa @ distinctBy rs erase (erase ` set rsa))"

  1044   

  1045   apply(induction rs arbitrary: rsa)

  1046    apply simp

  1047   

  1048   apply(drule_tac x = "rsa@[a]" in meta_spec)

  1049   

  1050   apply(subst threelistsappend)

  1051   apply(rule rrewrites_trans)

  1052    apply simp

  1053   

  1054   apply(case_tac "a \<in> set rsa")

  1055    apply simp

  1056    apply(drule somewhereInside)

  1057    apply(erule exE)+

  1058    apply simp

  1059   using bs10 ss6 apply auto[1]

  1060   

  1061   apply(subgoal_tac "erase ` set (rsa @ [a]) = insert (erase a) (erase ` set rsa)")

  1062   prefer 2

  1063     

  1064    apply auto[1]

  1065   apply(case_tac "erase a \<in> erase `set rsa")

  1066 

  1067    apply simp

  1068   apply(subgoal_tac "AALTs bs (rsa @ a # distinctBy rs erase (insert (erase a) (erase ` set rsa))) \<leadsto>

  1069                      AALTs bs (rsa @ distinctBy rs erase (insert (erase a) (erase ` set rsa)))")

  1070     apply force

  1071   apply (smt (verit, ccfv_threshold) append.assoc append.left_neutral append_Cons append_Nil bs10 imageE insertCI insert_image somewhereMapInside ss6)

  1072   by simp

  1073 

  1074  

  1075 

  1076 lemma alts_dBrewrites: 

  1077   shows "AALTs bs rs \<leadsto>* AALTs bs (distinctBy rs erase {})"

  1078   

  1079   apply(induction rs)

  1080    apply simp

  1081   apply simp

  1082   using alts_dBrewrites_withFront

  1083   by (metis append_Nil dB_single_step empty_set image_empty)

  1084 

  1085 lemma bsimp_rewrite: 

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

  1087 proof (induction r rule: bsimp.induct)

  1088   case (1 bs1 r1 r2)

  1089   then show "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)"

  1090     apply(simp)

  1091     apply(case_tac "bsimp r1 = AZERO")

  1092         apply simp

  1093   using continuous_rewrite apply blast

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

  1095         apply(erule exE)

  1096         apply simp

  1097         apply(subst bsimp_ASEQ2)

  1098         apply (meson rrewrites_trans rrewrite_srewrite.intros(3) rrewrites.intros(2) star_seq star_seq2)

  1099        apply (smt (verit, best) bsimp_ASEQ0 bsimp_ASEQ1 rrewrites_trans rrewrite_srewrite.intros(2) rs2 star_seq star_seq2)

  1100   done

  1101 next

  1102   case (2 bs1 rs)

  1103   then show "AALTs bs1 rs \<leadsto>* bsimp (AALTs bs1 rs)"

  1104     by (metis alts_dBrewrites alts_simpalts bsimp.simps(2) bsimp_AALTs_rewrites flts_rewrites rrewrites_trans)  

  1105 next

  1106   case "3_1"

  1107   then show "AZERO \<leadsto>* bsimp AZERO"

  1108     by simp

  1109 next

  1110   case ("3_2" v)

  1111   then show "AONE v \<leadsto>* bsimp (AONE v)" 

  1112     by simp

  1113 next

  1114   case ("3_3" v va)

  1115   then show "ACHAR v va \<leadsto>* bsimp (ACHAR v va)" 

  1116     by simp

  1117 next

  1118   case ("3_4" v va)

  1119   then show "ASTAR v va \<leadsto>* bsimp (ASTAR v va)" 

  1120     by simp

  1121 qed

  1122 

  1123 lemma bnullable1:

  1124 shows "r1 \<leadsto> r2 \<Longrightarrow> (bnullable r1 \<Longrightarrow> bnullable r2)" 

  1125   and "rs1 s\<leadsto> rs2 \<Longrightarrow>  ((\<exists>x \<in> set rs1. bnullable x) \<Longrightarrow> \<exists>x\<in>set rs2. bnullable x)" 

  1126 apply(induct rule: rrewrite_srewrite.inducts)

  1127                apply(auto)

  1128   using bnullable_fuse apply blast

  1129     apply (simp add: bnullable_fuse)

  1130   apply (meson UnCI bnullable_fuse imageI)

  1131   by (metis bnullable_correctness)

  1132 

  1133 lemma bnullable2:

  1134 shows "r1 \<leadsto> r2 \<Longrightarrow> (bnullable r2 \<Longrightarrow> bnullable r1)"