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 fun li :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp"

   571   where

   572   "li _ [] = AZERO"

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

   574 | "li bs as = AALTs bs as"

   575 

   576 

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

   578   where

   579   "bsimp_ASEQ _ AZERO _ = AZERO"

   580 | "bsimp_ASEQ _ _ AZERO = AZERO"

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

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

   583 

   584 

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

   586   where

   587   "bsimp_AALTs _ [] = AZERO"

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

   589 | "bsimp_AALTs bs1 rs = AALTs bs1 rs"

   590 

   591 

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

   593   where

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

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

   596 | "bsimp r = r"

   597 

   598 

   599 

   600 

   601 fun 

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

   603 where

   604   "bders_simp r [] = r"

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

   606 

   607 definition blexer_simp where

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

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

   610 

   611 

   612 lemma asize0:

   613   shows "0 < asize r"

   614   apply(induct  r)

   615        apply(auto)

   616   done

   617 

   618 

   619 lemma bders_simp_append:

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

   621   apply(induct s1 arbitrary: r s2)

   622    apply(simp)

   623   apply(simp)

   624   done

   625 

   626 lemma bsimp_ASEQ_size:

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

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

   629   apply(auto)

   630   done

   631 

   632 lemma fuse_size:

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

   634   apply(induct r)

   635   apply(auto)

   636   done

   637 

   638 lemma flts_size:

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

   640   apply(induct rs rule: flts.induct)

   641         apply(simp_all)

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

   643   

   644 

   645 lemma bsimp_AALTs_size:

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

   647   apply(induct rs rule: bsimp_AALTs.induct)

   648   apply(auto simp add: fuse_size)

   649   done

   650 

   651 

   652 lemma bsimp_size:

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

   654   apply(induct r)

   655        apply(simp_all)

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

   657   apply(rule le_trans)

   658    apply(rule bsimp_AALTs_size)

   659   apply(simp)

   660    apply(rule le_trans)

   661    apply(rule flts_size)

   662   by (simp add: sum_list_mono)

   663 

   664 lemma bsimp_asize0:

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

   666   apply(induct rs)

   667    apply(auto)

   668   by (simp add: add_mono bsimp_size)

   669 

   670 lemma bsimp_AALTs_size2:

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

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

   673   using assms

   674   apply(induct rs rule: bsimp_AALTs.induct)

   675     apply(simp_all add: fuse_size)

   676   done

   677 

   678 

   679 lemma qq:

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

   681   apply(induct rs)

   682    apply(auto simp add: fuse_size)

   683   done

   684 

   685 lemma flts_size2:

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

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

   688   using assms

   689   apply(induct rs)

   690    apply(auto simp add: qq)

   691    apply (simp add: flts_size less_Suc_eq_le)

   692   apply(case_tac a)

   693        apply(auto simp add: qq)

   694    prefer 2

   695    apply (simp add: flts_size le_imp_less_Suc)

   696   using less_Suc_eq by auto

   697 

   698 lemma bsimp_AALTs_size3:

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

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

   701   using assms flts_size2

   702   apply  -

   703   apply(clarify)

   704   apply(simp)

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

   706   apply(drule meta_mp)

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

   708   apply(simp)

   709   apply(rule order_class.order.strict_trans1)

   710    apply(rule bsimp_AALTs_size)

   711   apply(simp)

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

   713 

   714 

   715 

   716 

   717 lemma L_bsimp_ASEQ:

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

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

   720   apply(simp_all)

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

   722 

   723 lemma L_bsimp_AALTs:

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

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

   726   apply(simp_all add: erase_fuse)

   727   done

   728 

   729 lemma L_erase_AALTs:

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

   731   apply(induct rs)

   732    apply(simp)

   733   apply(simp)

   734   apply(case_tac rs)

   735    apply(simp)

   736   apply(simp)

   737   done

   738 

   739 lemma L_erase_flts:

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

   741   apply(induct rs rule: flts.induct)

   742         apply(simp_all)

   743   apply(auto)

   744   using L_erase_AALTs erase_fuse apply auto[1]

   745   by (simp add: L_erase_AALTs erase_fuse)

   746 

   747 

   748 lemma L_bsimp_erase:

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

   750   apply(induct r)

   751   apply(simp)

   752   apply(simp)

   753   apply(simp)

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

   755   apply(subst L_bsimp_ASEQ[symmetric])

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

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

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

   759    apply(simp)

   760    apply(subst L_bsimp_AALTs[symmetric])

   761    defer

   762    apply(simp)

   763   apply(subst (2)L_erase_AALTs)

   764   apply(subst L_erase_flts)

   765   apply(auto)

   766    apply (simp add: L_erase_AALTs)

   767   using L_erase_AALTs by blast

   768 

   769 lemma bsimp_ASEQ0:

   770   shows "bsimp_ASEQ bs r1 AZERO = AZERO"

   771   apply(induct r1)

   772   apply(auto)

   773   done

   774 

   775 

   776 

   777 lemma bsimp_ASEQ1:

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

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

   780   using assms

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

   782   apply(auto)

   783   done

   784 

   785 lemma bsimp_ASEQ2:

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

   787   apply(induct r2)

   788   apply(auto)

   789   done

   790 

   791 

   792 lemma L_bders_simp:

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

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

   795    apply(simp)

   796   apply(simp)

   797   apply(simp add: ders_append)

   798   apply(simp add: bders_simp_append)

   799   apply(simp add: L_bsimp_erase[symmetric])

   800   by (simp add: der_correctness)

   801 

   802 lemma b1:

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

   804   apply(induct r)

   805        apply(auto)

   806   done

   807 

   808 lemma b2:

   809   assumes "bnullable r"

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

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

   812 

   813 lemma b3:

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

   815   using L_bsimp_erase bnullable_correctness nullable_correctness by auto

   816 

   817 

   818 lemma b4:

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

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

   821 

   822 lemma q1:

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

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

   825   using assms

   826   apply(induct rs)

   827   apply(simp)

   828   apply(simp)

   829   done

   830 

   831 lemma q3:

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

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

   834   using assms

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

   836     apply(simp)

   837    apply(simp)

   838   apply (simp add: b2)

   839   apply(simp)

   840   done

   841 

   842 lemma qq1:

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

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

   845   using assms

   846   apply(induct rs arbitrary: rs1 bs)

   847   apply(simp)

   848   apply(simp)

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

   850 

   851 lemma qq2:

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

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

   854   using assms

   855   apply(induct rs arbitrary: rs1 bs)

   856   apply(simp)

   857   apply(simp)

   858   by (metis append_assoc in_set_conv_decomp r1 r2)

   859   

   860 lemma qq3:

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

   862   apply(induct rs arbitrary: bs)

   863   apply(simp)

   864   apply(simp)

   865   done

   866 

   867 lemma fuse_empty:

   868   shows "fuse [] r = r"

   869   apply(induct r)

   870        apply(auto)

   871   done

   872 

   873 lemma flts_fuse:

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

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

   876         apply(auto simp add: fuse_append)

   877   done

   878 

   879 lemma bsimp_ASEQ_fuse:

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

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

   882   apply(auto)

   883   done

   884 

   885 lemma bsimp_AALTs_fuse:

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

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

   888   using assms

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

   890   apply(auto)

   891   done

   892 

   893 

   894 

   895 lemma bsimp_fuse:

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

   897 apply(induct r arbitrary: bs)

   898        apply(simp)

   899       apply(simp)

   900      apply(simp)

   901     prefer 3

   902     apply(simp)

   903    apply(simp)

   904    apply (simp add: bsimp_ASEQ_fuse)

   905   apply(simp)

   906   by (simp add: bsimp_AALTs_fuse fuse_append)

   907 

   908 lemma bsimp_fuse_AALTs:

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

   910   apply(subst bsimp_fuse) 

   911   apply(simp)

   912   done

   913 

   914 lemma bsimp_fuse_AALTs2:

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

   916   using bsimp_AALTs_fuse fuse_append by auto

   917   

   918 

   919 lemma bsimp_ASEQ_idem:

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

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

   922   using assms

   923   apply(case_tac "bsimp r1 = AZERO")

   924     apply(simp)

   925  apply(case_tac "bsimp r2 = AZERO")

   926     apply(simp)

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

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

   929     apply(auto)[1]

   930     apply(subst bsimp_ASEQ2)

   931    apply(subst bsimp_ASEQ2)

   932   apply (metis assms(2) bsimp_fuse)

   933       apply(subst bsimp_ASEQ1)

   934       apply(auto)

   935   done

   936 

   937 

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

   939   where

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

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

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

   943 | "nonnested r = True"

   944 

   945 

   946 lemma  k0:

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

   948   apply(induct r arbitrary: rs1)

   949    apply(auto)

   950   done

   951 

   952 lemma  k00:

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

   954   apply(induct rs1 arbitrary: rs2)

   955    apply(auto)

   956   by (metis append.assoc k0)

   957 

   958 lemma  k0a:

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

   960   apply(simp)

   961   done

   962 

   963 

   964 lemma  k0b:

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

   966   shows "flts [r] = [r]"

   967   using assms

   968   apply(case_tac  r)

   969   apply(simp_all)

   970   done

   971 

   972 lemma nn1:

   973   assumes "nonnested (AALTs bs rs)"

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

   975   using assms

   976   apply(induct rs rule: flts.induct)

   977   apply(auto)

   978   done

   979 

   980 lemma nn1q:

   981   assumes "nonnested (AALTs bs rs)"

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

   983   using assms

   984   apply(induct rs rule: flts.induct)

   985   apply(auto)

   986   done

   987 

   988 lemma nn1qq:

   989   assumes "nonnested (AALTs bs rs)"

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

   991   using assms

   992   apply(induct rs rule: flts.induct)

   993   apply(auto)

   994   done

   995 

   996 lemma nn10:

   997   assumes "nonnested (AALTs cs rs)" 

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

   999   using assms

  1000   apply(induct rs arbitrary: cs bs)

  1001    apply(simp_all)

  1002   apply(case_tac a)

  1003        apply(simp_all)

  1004   done

  1005 

  1006 lemma nn11a:

  1007   assumes "nonalt r"

  1008   shows "nonalt (fuse bs r)"

  1009   using assms

  1010   apply(induct r)

  1011        apply(auto)

  1012   done

  1013 

  1014 

  1015 lemma nn1a:

  1016   assumes "nonnested r"

  1017   shows "nonnested (fuse bs r)"

  1018   using assms

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

  1020        apply(simp_all add: nn10)

  1021   done  

  1022 

  1023 lemma n0:

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

  1025   apply(induct rs  arbitrary: bs)

  1026    apply(auto)

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

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

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

  1030 

  1031   

  1032   

  1033 

  1034 lemma nn1c:

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

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

  1037   using assms

  1038   apply(induct rs rule: flts.induct)

  1039         apply(auto)

  1040   apply(rule nn11a)

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

  1042 

  1043 lemma nn1bb:

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

  1045   shows "nonnested (bsimp_AALTs bs rs)"

  1046   using assms

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

  1048     apply(auto)

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

  1050   using n0 by auto

  1051     

  1052 lemma nn1b:

  1053   shows "nonnested (bsimp r)"

  1054   apply(induct r)

  1055        apply(simp_all)

  1056   apply(case_tac "bsimp r1 = AZERO")

  1057     apply(simp)

  1058  apply(case_tac "bsimp r2 = AZERO")

  1059    apply(simp)

  1060     apply(subst bsimp_ASEQ0)

  1061   apply(simp)

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

  1063     apply(auto)[1]

  1064     apply(subst bsimp_ASEQ2)

  1065   apply (simp add: nn1a)    

  1066    apply(subst bsimp_ASEQ1)

  1067       apply(auto)

  1068   apply(rule nn1bb)

  1069   apply(auto)

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

  1071 

  1072 lemma nn1d:

  1073   assumes "bsimp r = AALTs bs rs"

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

  1075   using nn1b assms

  1076   by (metis nn1qq)

  1077 

  1078 lemma nn_flts:

  1079   assumes "nonnested (AALTs bs rs)"

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

  1081   using assms

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

  1083         apply(auto)

  1084   done

  1085 

  1086 lemma rt:

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

  1088   apply(induct rs)

  1089    apply(simp)

  1090   apply(simp)

  1091   apply(subst  k0)

  1092   apply(simp)

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

  1094 

  1095 lemma bsimp_AALTs_qq:

  1096   assumes "1 < length rs"

  1097   shows "bsimp_AALTs bs rs = AALTs bs  rs"

  1098   using  assms

  1099   apply(case_tac rs)

  1100    apply(simp)

  1101   apply(case_tac list)

  1102    apply(simp_all)

  1103   done

  1104 

  1105 

  1106 lemma bsimp_AALTs1:

  1107   assumes "nonalt r"

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

  1109   using  assms

  1110   apply(case_tac r)

  1111    apply(simp_all)

  1112   done

  1113 

  1114 lemma bbbbs:

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

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

  1117   using  assms

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

  1119 

  1120 lemma bbbbs1:

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

  1122   using nonalt.elims(3) by auto

  1123   

  1124 

  1125 lemma good_fuse:

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

  1127   apply(induct r arbitrary: bs)

  1128        apply(auto)

  1129      apply(case_tac r1)

  1130           apply(simp_all)

  1131   apply(case_tac r2)

  1132           apply(simp_all)

  1133   apply(case_tac r2)

  1134             apply(simp_all)

  1135   apply(case_tac r2)