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 [S] (intern r)"

   174 

   175 

   176 

   177 

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

   179   "retrieve (AONE bs) Void = bs"

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

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

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

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

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

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

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

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

   188 

   189 

   190 

   191 fun

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

   193 where

   194   "bnullable (AZERO) = False"

   195 | "bnullable (AONE bs) = True"

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

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

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

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

   200 

   201 fun 

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

   203 where

   204   "bmkeps(AONE bs) = bs"

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

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

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

   208 | "bmkeps(ASTAR bs r) = bs"

   209 

   210 

   211 fun

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

   213 where

   214   "bder c (AZERO) = AZERO"

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

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

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

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

   219      (if bnullable r1

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

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

   222 | "bder c (ASTAR bs r) = ASEQ (butlast bs) (fuse [Z] (bder c r)) (ASTAR [S] r)"

   223 

   224 

   225 

   226 lemma bder_fuse:

   227   "fuse bs (bder c r) = bder c (fuse bs r)"

   228   apply(induct r arbitrary: bs)

   229   apply(simp_all)

   230   done

   231 

   232 

   233 fun 

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

   235 where

   236   "bders r [] = r"

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

   238 

   239 lemma bders_append:

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

   241   apply(induct s1 arbitrary: r s2)

   242   apply(simp_all)

   243   done

   244 

   245 lemma bnullable_correctness:

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

   247   apply(induct r rule: erase.induct)

   248   apply(simp_all)

   249   done

   250 

   251 lemma erase_fuse:

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

   253   apply(induct r rule: erase.induct)

   254   apply(simp_all)

   255   done

   256 

   257 lemma erase_intern [simp]:

   258   shows "erase (intern r) = r"

   259   apply(induct r)

   260   apply(simp_all add: erase_fuse)

   261   done

   262 

   263 lemma erase_bder [simp]:

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

   265   apply(induct r rule: erase.induct)

   266   apply(simp_all add: erase_fuse bnullable_correctness)

   267   done

   268 

   269 lemma erase_bders [simp]:

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

   271   apply(induct s arbitrary: r )

   272   apply(simp_all)

   273   done

   274 

   275 lemma retrieve_encode_STARS:

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

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

   278   using assms

   279   apply(induct vs)

   280   apply(simp_all)

   281   done

   282 

   283 lemma retrieve_fuse2:

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

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

   286   using assms

   287   apply(induct r arbitrary: v bs)

   288          apply(auto elim: Prf_elims)[4]

   289    defer

   290   using retrieve_encode_STARS

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

   292    apply(case_tac vs)

   293     apply(simp)

   294    apply(simp)

   295   (* AALTs  case *)

   296   apply(simp)

   297   apply(case_tac x2a)

   298    apply(simp)

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

   300   apply(simp)

   301    apply(case_tac list)

   302    apply(simp)

   303   apply(auto)

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

   305   done

   306 

   307 lemma retrieve_fuse:

   308   assumes "\<Turnstile> v : r"

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

   310   using assms 

   311   by (simp_all add: retrieve_fuse2)

   312 

   313 

   314 lemma r:

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

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

   317   using assms

   318   apply(induct rs)

   319    apply(auto)

   320   done

   321 

   322 lemma r0:

   323   assumes "bnullable a" 

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

   325   using assms

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

   327 

   328 lemma r1:

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

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

   331   using assms

   332   apply(induct rs)

   333    apply(auto)

   334   done

   335 

   336 lemma r2:

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

   338   shows "bnullable (AALTs bs rs)"

   339   using assms

   340   apply(induct rs)

   341    apply(auto)

   342   done

   343 

   344 lemma  r3:

   345   assumes "\<not> bnullable r" 

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

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

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

   349   using assms

   350   apply(induct rs arbitrary: r bs)

   351    apply(auto)[1]

   352   apply(auto)

   353   using bnullable_correctness apply blast

   354     apply(auto simp add: bnullable_correctness mkeps_nullable retrieve_fuse2)

   355    apply(subst retrieve_fuse2[symmetric])

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

   357    apply(simp)

   358   apply(case_tac "bnullable a")

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

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

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

   362   apply(drule meta_mp)

   363    apply(simp)

   364   apply(drule meta_mp)

   365    apply(auto)

   366   apply(subst retrieve_fuse2[symmetric])

   367   apply(case_tac rs)

   368     apply(simp)

   369    apply(auto)[1]

   370       apply (simp add: bnullable_correctness)

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

   372     apply (simp add: bnullable_correctness)

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

   374   apply(simp)

   375   done

   376 

   377 

   378 lemma t: 

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

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

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

   382   using assms

   383   apply(induct rs arbitrary: bs)

   384    apply(simp)

   385   apply(auto simp add: bnullable_correctness)

   386    apply(case_tac rs)

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

   388    apply(subst r1)

   389      apply(simp)

   390     apply(rule r2)

   391      apply(assumption)

   392     apply(simp)

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

   394    apply(drule meta_mp)

   395     apply(auto)[1]

   396    prefer 2

   397   apply(case_tac "bnullable a")

   398     apply(subst r0)

   399      apply blast

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

   401   prefer 2

   402   using bnullable_correctness apply blast

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

   404   apply(subst r1)

   405      apply(simp)

   406   using r2 apply blast

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

   408    apply(drule meta_mp)

   409     apply(auto)[1]

   410    apply(simp)

   411   using r3 apply blast

   412   apply(auto)

   413   using r3 by blast

   414 

   415 

   416 lemma asize0:

   417   shows "0 < asize r"

   418   apply(induct  r)

   419   apply(auto)

   420   done

   421 

   422 lemma asize_fuse:

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

   424   apply(induct r)

   425   apply(auto)

   426   done

   427 

   428 lemma TESTTEST:

   429   shows "bder c (intern r) = intern (der c r)"

   430   apply(induct r)

   431        apply(simp)

   432       apply(simp)

   433      apply(simp)

   434     prefer 2

   435     apply(simp)  

   436     apply (simp add: bder_fuse[symmetric])

   437   prefer 3

   438    apply(simp only: intern.simps)

   439    apply(simp only: der.simps)

   440    apply(simp only: intern.simps)

   441     apply(simp only: bder.simps)

   442   apply(simp)

   443    apply(simp only: intern.simps)

   444    prefer 2

   445    apply(simp)

   446    prefer 2

   447    apply(simp)

   448   apply(auto)

   449 

   450 

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

   452   where

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

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

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

   456 | "nonnested r = True"

   457 

   458 

   459 

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

   461   where

   462   "distinctBy [] f acc = []"

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

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

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

   466 

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

   468   where 

   469   "flts [] = []"

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

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

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

   473 

   474 

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

   476   where 

   477   "spill [] = []"

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

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

   480 

   481 lemma  spill_Cons:

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

   483   apply(induct r arbitrary: rs1)

   484    apply(auto)

   485   done

   486 

   487 lemma  spill_append:

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

   489   apply(induct rs1 arbitrary: rs2)

   490    apply(auto)

   491   by (metis append.assoc spill_Cons)

   492 

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

   494   where

   495   "bsimp_ASEQ _ AZERO _ = AZERO"

   496 | "bsimp_ASEQ _ _ AZERO = AZERO"

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

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

   499 

   500 

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

   502   where

   503   "bsimp_AALTs _ [] = AZERO"

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

   505 | "bsimp_AALTs bs1 rs = AALTs bs1 rs"

   506 

   507 

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

   509   where

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

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

   512 | "bsimp r = r"

   513 

   514 

   515 inductive contains2 :: "arexp \<Rightarrow> bit list \<Rightarrow> bool" ("_ >>2 _" [51, 50] 50)

   516   where

   517   "AONE bs >>2 bs"

   518 | "ACHAR bs c >>2 bs"

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

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

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

   522 | "ASTAR bs r >>2 bs @ [S]"

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

   524 | "r >>2 bs \<Longrightarrow> (bsimp r) >>2 bs"

   525 

   526 

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

   528   where

   529   "AONE bs >> bs"

   530 | "ACHAR bs c >> bs"

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

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

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

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

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

   536 

   537 

   538 

   539 lemma contains0:

   540   assumes "a >> bs"

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

   542   using assms

   543   apply(induct arbitrary: bs1)

   544   apply(auto intro: contains.intros)

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

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

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

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

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

   550   done

   551 

   552 lemma contains1:

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

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

   555   using assms

   556   apply(induct vs)

   557    apply(simp)

   558   using contains.simps apply blast

   559   apply(simp)

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

   561   apply(rule contains.intros)

   562    apply(auto)

   563   done

   564 

   565 

   566 

   567 

   568 

   569 lemma contains2:

   570   assumes "\<Turnstile> v : r"

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

   572   using assms

   573   apply(induct)

   574        prefer 4

   575        apply(simp)

   576        apply(rule contains.intros)

   577    prefer 4

   578        apply(simp)

   579       apply(rule contains.intros)

   580      apply(simp)

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

   582   apply(rule contains.intros)

   583       apply(simp)

   584   apply(simp)

   585     apply(simp)

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

   587     apply(rule contains.intros)

   588     apply (metis append_Cons append_self_conv2 contains0)

   589     apply(simp)

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

   591    apply(rule contains.intros)

   592    back

   593    apply(rule contains.intros)

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

   595    apply(simp)

   596   apply(simp)

   597   apply(case_tac vs)

   598    apply(simp)

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

   600   using contains1 by blast

   601 

   602 lemma qq1:

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

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

   605   using assms

   606   apply(induct rs arbitrary: rs1 bs)

   607   apply(simp)

   608   apply(simp)

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

   610 

   611 lemma qq2:

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

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

   614   using assms

   615   apply(induct rs arbitrary: rs1 bs)

   616   apply(simp)

   617   apply(simp)

   618   by (metis append_assoc in_set_conv_decomp r1 r2)

   619 

   620 lemma qq2a:

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

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

   623   using assms

   624   by (simp add: r1)

   625   

   626 lemma qq3:

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

   628   apply(induct rs arbitrary: bs)

   629   apply(simp)

   630   apply(simp)

   631   done

   632 

   633 lemma qq4:

   634   assumes "bnullable (AALTs bs rs)"

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

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

   637 

   638 

   639 lemma contains3a:

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

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

   642   using assms

   643   apply -

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

   645 

   646   

   647 lemma contains3b:

   648   assumes "a >> bs1"

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

   650   using assms

   651   apply -

   652   apply(rule contains.intros)

   653   apply(simp)

   654   done   

   655 

   656 

   657 lemma contains3:

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

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

   660   using assms

   661   apply(induct rs arbitrary: bs x)

   662    apply simp

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

   664 

   665 lemma cont1:

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

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

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

   669   using assms 

   670   apply(induct vs arbitrary: bs r)

   671    apply(simp)

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

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

   674   

   675 lemma contains4:

   676   assumes "bnullable a"

   677   shows "a >> bmkeps a"

   678   using assms

   679   apply(induct a rule: bnullable.induct)

   680        apply(auto intro: contains.intros)

   681   using contains3 by blast

   682 

   683 lemma contains5:

   684   assumes "\<Turnstile> v : r"

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

   686   using contains2[OF assms] retrieve_code[OF assms]

   687   by (simp)

   688 

   689 

   690 lemma contains6:

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

   692   shows "r >> retrieve r v"

   693   using assms

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

   695   apply(auto)[1]

   696   using Prf_elims(1) apply blast

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

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

   699   apply(auto)[1]

   700   using Prf_elims(1) apply blast

   701   apply(auto)[1]

   702   using contains3b contains3a apply blast

   703     prefer 2

   704   apply(auto)[1]

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

   706    prefer 2

   707   apply(auto)[1]

   708    apply (metis Prf_elims(6) cont1)

   709   apply(simp)

   710   apply(erule Prf_elims)

   711    apply(auto)

   712    apply (simp add: contains3b)

   713   using retrieve_fuse2 contains3b contains3a

   714   apply(subst retrieve_fuse2[symmetric])

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

   716   apply(simp)

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

   718 

   719 lemma contains7:

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

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

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

   723   by (metis assms contains6 erase_bder)

   724 

   725 

   726 lemma contains7a:

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

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

   729   using assms

   730   apply -

   731   apply(drule Prf_injval)

   732   apply(drule contains6)

   733   apply(simp)

   734   done

   735 

   736 lemma contains7b:

   737   assumes "\<Turnstile> v : ders s (erase r)"

   738   shows "(bders r s) >> retrieve r (flex (erase r) id s v)"

   739   using assms

   740   apply(induct s arbitrary: r v)

   741    apply(simp)

   742    apply (simp add: contains6)

   743   apply(simp add: bders_append flex_append ders_append)

   744   apply(drule_tac x="bder a r" in meta_spec)

   745   apply(drule meta_spec)

   746   apply(drule meta_mp)

   747    apply(simp)

   748   apply(simp)

   749   apply(subst (asm) bder_retrieve)

   750    defer

   751   apply (simp add: flex_injval)

   752   by (simp add: Prf_flex)

   753 

   754 lemma contains7_iff:

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

   756   shows "(bder c r) >> retrieve r (injval (erase r) c v) \<longleftrightarrow>

   757                   r >> retrieve r (injval (erase r) c v)"

   758   by (simp add: assms contains7 contains7a)

   759 

   760 lemma contains8_iff:

   761   assumes "\<Turnstile> v : ders s (erase r)"

   762   shows "(bders r s) >> retrieve r (flex (erase r) id s v) \<longleftrightarrow>

   763                   r >> retrieve r (flex (erase r) id s v)"

   764   using Prf_flex assms contains6 contains7b by blast

   765 

   766 

   767 

   768 

   769 fun 

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

   771 where

   772   "bders_simp r [] = r"

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

   774 

   775 definition blexer_simp where

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

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

   778 

   779 

   780 

   781 

   782 

   783 lemma bders_simp_append:

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

   785   apply(induct s1 arbitrary: r s2)

   786    apply(simp)

   787   apply(simp)

   788   done

   789 

   790 lemma bsimp_ASEQ_size:

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

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

   793   apply(auto)

   794   done

   795 

   796 

   797 

   798 lemma flts_size:

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

   800   apply(induct rs rule: flts.induct)

   801         apply(simp_all)

   802   by (simp add: asize_fuse comp_def)

   803   

   804 

   805 lemma bsimp_AALTs_size:

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

   807   apply(induct rs rule: bsimp_AALTs.induct)

   808   apply(auto simp add: asize_fuse)

   809   done

   810 

   811 

   812 lemma bsimp_size:

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

   814   apply(induct r)

   815        apply(simp_all)

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

   817   apply(rule le_trans)

   818    apply(rule bsimp_AALTs_size)

   819   apply(simp)

   820    apply(rule le_trans)

   821    apply(rule flts_size)

   822   by (simp add: sum_list_mono)

   823 

   824 lemma bsimp_asize0:

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

   826   apply(induct rs)

   827    apply(auto)

   828   by (simp add: add_mono bsimp_size)

   829 

   830 lemma bsimp_AALTs_size2:

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

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

   833   using assms

   834   apply(induct rs rule: bsimp_AALTs.induct)

   835     apply(simp_all add: asize_fuse)

   836   done

   837 

   838 

   839 lemma qq:

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

   841   apply(induct rs)

   842    apply(auto simp add: asize_fuse)

   843   done

   844 

   845 lemma flts_size2:

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

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

   848   using assms

   849   apply(induct rs)

   850    apply(auto simp add: qq)

   851    apply (simp add: flts_size less_Suc_eq_le)

   852   apply(case_tac a)

   853        apply(auto simp add: qq)

   854    prefer 2

   855    apply (simp add: flts_size le_imp_less_Suc)

   856   using less_Suc_eq by auto

   857 

   858 lemma bsimp_AALTs_size3:

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

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

   861   using assms flts_size2

   862   apply  -

   863   apply(clarify)

   864   apply(simp)

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

   866   apply(drule meta_mp)

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

   868   apply(simp)

   869   apply(rule order_class.order.strict_trans1)

   870    apply(rule bsimp_AALTs_size)

   871   apply(simp)

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

   873 

   874 

   875 

   876 

   877 lemma L_bsimp_ASEQ:

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

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

   880   apply(simp_all)

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

   882 

   883 lemma L_bsimp_AALTs:

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

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

   886   apply(simp_all add: erase_fuse)

   887   done

   888 

   889 lemma L_erase_AALTs:

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

   891   apply(induct rs)

   892    apply(simp)

   893   apply(simp)

   894   apply(case_tac rs)

   895    apply(simp)

   896   apply(simp)

   897   done

   898 

   899 lemma L_erase_flts:

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

   901   apply(induct rs rule: flts.induct)

   902         apply(simp_all)

   903   apply(auto)

   904   using L_erase_AALTs erase_fuse apply auto[1]

   905   by (simp add: L_erase_AALTs erase_fuse)

   906 

   907 

   908 lemma L_bsimp_erase:

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

   910   apply(induct r)

   911   apply(simp)

   912   apply(simp)

   913   apply(simp)

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

   915   apply(subst L_bsimp_ASEQ[symmetric])

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

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

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

   919    apply(simp)

   920    apply(subst L_bsimp_AALTs[symmetric])

   921    defer

   922    apply(simp)

   923   apply(subst (2)L_erase_AALTs)

   924   apply(subst L_erase_flts)

   925   apply(auto)

   926    apply (simp add: L_erase_AALTs)

   927   using L_erase_AALTs by blast

   928 

   929 lemma bsimp_ASEQ0:

   930   shows "bsimp_ASEQ bs r1 AZERO = AZERO"

   931   apply(induct r1)

   932   apply(auto)

   933   done

   934 

   935 

   936 

   937 lemma bsimp_ASEQ1:

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

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

   940   using assms

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

   942   apply(auto)

   943   done

   944 

   945 lemma bsimp_ASEQ2:

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

   947   apply(induct r2)

   948   apply(auto)

   949   done

   950 

   951 

   952 lemma L_bders_simp:

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

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

   955    apply(simp)

   956   apply(simp)

   957   apply(simp add: ders_append)

   958   apply(simp add: bders_simp_append)

   959   apply(simp add: L_bsimp_erase[symmetric])

   960   by (simp add: der_correctness)

   961 

   962 lemma b1:

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

   964   apply(induct r)

   965        apply(auto)

   966   done

   967 

   968 lemma b2:

   969   assumes "bnullable r"

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

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

   972 

   973 lemma b3:

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

   975   using L_bsimp_erase bnullable_correctness nullable_correctness by auto

   976 

   977 

   978 lemma b4:

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

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

   981 

   982 lemma q1:

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

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

   985   using assms

   986   apply(induct rs)

   987   apply(simp)

   988   apply(simp)

   989   done

   990 

   991 lemma q3:

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

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

   994   using assms

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

   996     apply(simp)

   997    apply(simp)

   998   apply (simp add: b2)

   999   apply(simp)

  1000   done

  1001 

  1002 

  1003 lemma fuse_empty:

  1004   shows "fuse [] r = r"

  1005   apply(induct r)

  1006        apply(auto)

  1007   done

  1008 

  1009 lemma flts_fuse:

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

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

  1012         apply(auto simp add: fuse_append)

  1013   done

  1014 

  1015 lemma bsimp_ASEQ_fuse:

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

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

  1018   apply(auto)

  1019   done

  1020 

  1021 lemma bsimp_AALTs_fuse:

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

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

  1024   using assms

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

  1026   apply(auto)

  1027   done

  1028 

  1029 

  1030 

  1031 lemma bsimp_fuse:

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

  1033 apply(induct r arbitrary: bs)

  1034        apply(simp)

  1035       apply(simp)

  1036      apply(simp)

  1037     prefer 3

  1038     apply(simp)

  1039    apply(simp)

  1040    apply (simp add: bsimp_ASEQ_fuse)

  1041   apply(simp)

  1042   by (simp add: bsimp_AALTs_fuse fuse_append)

  1043 

  1044 lemma bsimp_fuse_AALTs:

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

  1046   apply(subst bsimp_fuse) 

  1047   apply(simp)

  1048   done

  1049 

  1050 lemma bsimp_fuse_AALTs2:

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

  1052   using bsimp_AALTs_fuse fuse_append by auto

  1053   

  1054 

  1055 lemma bsimp_ASEQ_idem:

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

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

  1058   using assms

  1059   apply(case_tac "bsimp r1 = AZERO")

  1060     apply(simp)

  1061  apply(case_tac "bsimp r2 = AZERO")

  1062     apply(simp)

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

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

  1065     apply(auto)[1]

  1066     apply(subst bsimp_ASEQ2)

  1067    apply(subst bsimp_ASEQ2)

  1068   apply (metis assms(2) bsimp_fuse)

  1069       apply(subst bsimp_ASEQ1)

  1070       apply(auto)

  1071   done

  1072 

  1073 

  1074 

  1075 lemma  k0:

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

  1077   apply(induct r arbitrary: rs1)

  1078    apply(auto)

  1079   done

  1080 

  1081 lemma  k00:

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

  1083   apply(induct rs1 arbitrary: rs2)

  1084    apply(auto)

  1085   by (metis append.assoc k0)

  1086 

  1087 lemma  k0a:

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

  1089   apply(simp)

  1090   done

  1091 

  1092 

  1093 lemma  k0b:

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

  1095   shows "flts [r] = [r]"

  1096   using assms

  1097   apply(case_tac  r)

  1098   apply(simp_all)

  1099   done

  1100 

  1101 lemma nn1:

  1102   assumes "nonnested (AALTs bs rs)"

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

  1104   using assms

  1105   apply(induct rs rule: flts.induct)

  1106   apply(auto)

  1107   done

  1108 

  1109 lemma nn1q:

  1110   assumes "nonnested (AALTs bs rs)"

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

  1112   using assms

  1113   apply(induct rs rule: flts.induct)

  1114   apply(auto)

  1115   done

  1116 

  1117 lemma nn1qq:

  1118   assumes "nonnested (AALTs bs rs)"

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

  1120   using assms

  1121   apply(induct rs rule: flts.induct)

  1122   apply(auto)

  1123   done

  1124 

  1125 lemma nn10:

  1126   assumes "nonnested (AALTs cs rs)" 

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

  1128   using assms

  1129   apply(induct rs arbitrary: cs bs)

  1130    apply(simp_all)

  1131   apply(case_tac a)

  1132        apply(simp_all)

  1133   done

  1134 

  1135 lemma nn11a: