Mercurial Mercurial > hg > lexing / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/BitCoded2.thy
changeset 359 fedc16924b76
parent 358 06aa99b54423
child 362 e51c9a67a68d
equal deleted inserted replaced
358:06aa99b54423 359:fedc16924b76 
   168 | "intern ONE = AONE []"
 
   168 | "intern ONE = AONE []"
 
   169 | "intern (CHAR c) = ACHAR [] c"
 
   169 | "intern (CHAR c) = ACHAR [] c"
 
   170 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) 
   170 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) 
   171                                 (fuse [S]  (intern r2))"
 
   171                                 (fuse [S]  (intern r2))"
 
   172 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)"
 
   172 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)"
 
   173 | "intern (STAR r) = ASTAR [] (intern r)"
 
   173 | "intern (STAR r) = ASTAR [S] (intern r)"
 
   174 
   174 
   175 
   175 
   176 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where
 
   176 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where
 
   177   "retrieve (AONE bs) Void = bs"
 
   177   "retrieve (AONE bs) Void = bs"
 
   178 | "retrieve (ACHAR bs c) (Char d) = bs"
 
   178 | "retrieve (ACHAR bs c) (Char d) = bs"
 
   201 where
 
   201 where
 
   202   "bmkeps(AONE bs) = bs"
 
   202   "bmkeps(AONE bs) = bs"
 
   203 | "bmkeps(ASEQ bs r1 r2) = bs @ (bmkeps r1) @ (bmkeps r2)"
 
   203 | "bmkeps(ASEQ bs r1 r2) = bs @ (bmkeps r1) @ (bmkeps r2)"
 
   204 | "bmkeps(AALTs bs [r]) = bs @ (bmkeps r)"
 
   204 | "bmkeps(AALTs bs [r]) = bs @ (bmkeps r)"
 
   205 | "bmkeps(AALTs bs (r#rs)) = (if bnullable(r) then bs @ (bmkeps r) else (bmkeps (AALTs bs rs)))"
 
   205 | "bmkeps(AALTs bs (r#rs)) = (if bnullable(r) then bs @ (bmkeps r) else (bmkeps (AALTs bs rs)))"
 
   206 | "bmkeps(ASTAR bs r) = bs @ [S]"
 
   206 | "bmkeps(ASTAR bs r) = bs"
 
   207 
   207 
   208 
   208 
   209 fun
 
   209 fun
 
   210  bder :: "char \<Rightarrow> arexp \<Rightarrow> arexp"
 
   210  bder :: "char \<Rightarrow> arexp \<Rightarrow> arexp"
 
   211 where
 
   211 where
 
   215 | "bder c (AALTs bs rs) = AALTs bs (map (bder c) rs)"
 
   215 | "bder c (AALTs bs rs) = AALTs bs (map (bder c) rs)"
 
   216 | "bder c (ASEQ bs r1 r2) = 
   216 | "bder c (ASEQ bs r1 r2) = 
   217      (if bnullable r1
 
   217      (if bnullable r1
 
   218       then AALT bs (ASEQ [] (bder c r1) r2) (fuse (bmkeps r1) (bder c r2))
 
   218       then AALT bs (ASEQ [] (bder c r1) r2) (fuse (bmkeps r1) (bder c r2))
 
   219       else ASEQ bs (bder c r1) r2)"
 
   219       else ASEQ bs (bder c r1) r2)"
 
   220 | "bder c (ASTAR bs r) = ASEQ bs (fuse [Z] (bder c r)) (ASTAR [] r)"
 
   220 | "bder c (ASTAR bs r) = ASEQ (butlast bs) (fuse [Z] (bder c r)) (ASTAR [S] r)"
 
       
   221 
       
   222 
       
   223 
       
   224 lemma bder_fuse:
 
       
   225   "fuse bs (bder c r) = bder c (fuse bs r)"
 
       
   226   apply(induct r arbitrary: bs)
 
       
   227   apply(simp_all)
 
       
   228   done
 
   221 
   229 
   222 
   230 
   223 fun 
   231 fun 
   224   bders :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
 
   232   bders :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
 
   225 where
 
   233 where
 
   298   assumes "\<Turnstile> v : r"
 
   306   assumes "\<Turnstile> v : r"
 
   299   shows "retrieve (fuse bs (intern r)) v = bs @ retrieve (intern r) v"
 
   307   shows "retrieve (fuse bs (intern r)) v = bs @ retrieve (intern r) v"
 
   300   using assms 
   308   using assms 
   301   by (simp_all add: retrieve_fuse2)
 
   309   by (simp_all add: retrieve_fuse2)
 
   302 
   310 
   303 
       
   304 lemma retrieve_code:
 
       
   305   assumes "\<Turnstile> v : r"
 
       
   306   shows "code v = retrieve (intern r) v"
 
       
   307   using assms
 
       
   308   apply(induct v r )
 
       
   309   apply(simp_all add: retrieve_fuse retrieve_encode_STARS)
 
       
   310   done
 
       
   311 
   311 
   312 lemma r:
 
   312 lemma r:
 
   313   assumes "bnullable (AALTs bs (a # rs))"
 
   313   assumes "bnullable (AALTs bs (a # rs))"
 
   314   shows "bnullable a \<or> (\<not> bnullable a \<and> bnullable (AALTs bs rs))"
 
   314   shows "bnullable a \<or> (\<not> bnullable a \<and> bnullable (AALTs bs rs))"
 
   315   using assms
 
   315   using assms
 
   408    apply(simp)
 
   408    apply(simp)
 
   409   using r3 apply blast
 
   409   using r3 apply blast
 
   410   apply(auto)
 
   410   apply(auto)
 
   411   using r3 by blast
 
   411   using r3 by blast
 
   412 
   412 
   413 lemma bmkeps_retrieve:
 
       
   414   assumes "nullable (erase r)"
 
       
   415   shows "bmkeps r = retrieve r (mkeps (erase r))"
 
       
   416   using assms
 
       
   417   apply(induct r)
 
       
   418          apply(simp)
 
       
   419         apply(simp)
 
       
   420        apply(simp)
 
       
   421     apply(simp)
 
       
   422    defer
 
       
   423    apply(simp)
 
       
   424   apply(rule t)
 
       
   425    apply(auto)
 
       
   426   done
 
       
   427 
       
   428 lemma bder_retrieve:
 
       
   429   assumes "\<Turnstile> v : der c (erase r)"
 
       
   430   shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)"
 
       
   431   using assms
 
       
   432   apply(induct r arbitrary: v rule: erase.induct)
 
       
   433          apply(simp)
 
       
   434          apply(erule Prf_elims)
 
       
   435         apply(simp)
 
       
   436         apply(erule Prf_elims) 
       
   437         apply(simp)
 
       
   438       apply(case_tac "c = ca")
 
       
   439        apply(simp)
 
       
   440        apply(erule Prf_elims)
 
       
   441        apply(simp)
 
       
   442       apply(simp)
 
       
   443        apply(erule Prf_elims)
 
       
   444   apply(simp)
 
       
   445       apply(erule Prf_elims)
 
       
   446      apply(simp)
 
       
   447     apply(simp)
 
       
   448   apply(rename_tac "r\<^sub>1" "r\<^sub>2" rs v)
 
       
   449     apply(erule Prf_elims)
 
       
   450      apply(simp)
 
       
   451     apply(simp)
 
       
   452     apply(case_tac rs)
 
       
   453      apply(simp)
 
       
   454     apply(simp)
 
       
   455   apply (smt Prf_elims(3) injval.simps(2) injval.simps(3) retrieve.simps(4) retrieve.simps(5) same_append_eq)
 
       
   456    apply(simp)
 
       
   457    apply(case_tac "nullable (erase r1)")
 
       
   458     apply(simp)
 
       
   459   apply(erule Prf_elims)
 
       
   460      apply(subgoal_tac "bnullable r1")
 
       
   461   prefer 2
 
       
   462   using bnullable_correctness apply blast
 
       
   463     apply(simp)
 
       
   464      apply(erule Prf_elims)
 
       
   465      apply(simp)
 
       
   466    apply(subgoal_tac "bnullable r1")
 
       
   467   prefer 2
 
       
   468   using bnullable_correctness apply blast
 
       
   469     apply(simp)
 
       
   470     apply(simp add: retrieve_fuse2)
 
       
   471     apply(simp add: bmkeps_retrieve)
 
       
   472    apply(simp)
 
       
   473    apply(erule Prf_elims)
 
       
   474    apply(simp)
 
       
   475   using bnullable_correctness apply blast
 
       
   476   apply(rename_tac bs r v)
 
       
   477   apply(simp)
 
       
   478   apply(erule Prf_elims)
 
       
   479      apply(clarify)
 
       
   480   apply(erule Prf_elims)
 
       
   481   apply(clarify)
 
       
   482   apply(subst injval.simps)
 
       
   483   apply(simp del: retrieve.simps)
 
       
   484   apply(subst retrieve.simps)
 
       
   485   apply(subst retrieve.simps)
 
       
   486   apply(simp)
 
       
   487   apply(simp add: retrieve_fuse2)
 
       
   488   done
 
       
   489   
       
   490 
       
   491 
       
   492 lemma MAIN_decode:
 
       
   493   assumes "\<Turnstile> v : ders s r"
 
       
   494   shows "Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r"
 
       
   495   using assms
 
       
   496 proof (induct s arbitrary: v rule: rev_induct)
 
       
   497   case Nil
 
       
   498   have "\<Turnstile> v : ders [] r" by fact
 
       
   499   then have "\<Turnstile> v : r" by simp
 
       
   500   then have "Some v = decode (retrieve (intern r) v) r"
 
       
   501     using decode_code retrieve_code by auto
 
       
   502   then show "Some (flex r id [] v) = decode (retrieve (bders (intern r) []) v) r"
 
       
   503     by simp
 
       
   504 next
 
       
   505   case (snoc c s v)
 
       
   506   have IH: "\<And>v. \<Turnstile> v : ders s r \<Longrightarrow> 
       
   507      Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" by fact
 
       
   508   have asm: "\<Turnstile> v : ders (s @ [c]) r" by fact
 
       
   509   then have asm2: "\<Turnstile> injval (ders s r) c v : ders s r" 
       
   510     by (simp add: Prf_injval ders_append)
 
       
   511   have "Some (flex r id (s @ [c]) v) = Some (flex r id s (injval (ders s r) c v))"
 
       
   512     by (simp add: flex_append)
 
       
   513   also have "... = decode (retrieve (bders (intern r) s) (injval (ders s r) c v)) r"
 
       
   514     using asm2 IH by simp
 
       
   515   also have "... = decode (retrieve (bder c (bders (intern r) s)) v) r"
 
       
   516     using asm by (simp_all add: bder_retrieve ders_append)
 
       
   517   finally show "Some (flex r id (s @ [c]) v) = 
       
   518                  decode (retrieve (bders (intern r) (s @ [c])) v) r" by (simp add: bders_append)
 
       
   519 qed
 
       
   520 
       
   521 
       
   522 definition blex where
 
       
   523  "blex a s \<equiv> if bnullable (bders a s) then Some (bmkeps (bders a s)) else None"
 
       
   524 
       
   525 
       
   526 
       
   527 definition blexer where
 
       
   528  "blexer r s \<equiv> if bnullable (bders (intern r) s) then 
       
   529                 decode (bmkeps (bders (intern r) s)) r else None"
 
       
   530 
       
   531 lemma blexer_correctness:
 
       
   532   shows "blexer r s = lexer r s"
 
       
   533 proof -
 
       
   534   { define bds where "bds \<equiv> bders (intern r) s"
 
       
   535     define ds  where "ds \<equiv> ders s r"
 
       
   536     assume asm: "nullable ds"
 
       
   537     have era: "erase bds = ds" 
       
   538       unfolding ds_def bds_def by simp
 
       
   539     have mke: "\<Turnstile> mkeps ds : ds"
 
       
   540       using asm by (simp add: mkeps_nullable)
 
       
   541     have "decode (bmkeps bds) r = decode (retrieve bds (mkeps ds)) r"
 
       
   542       using bmkeps_retrieve
 
       
   543       using asm era by (simp add: bmkeps_retrieve)
 
       
   544     also have "... =  Some (flex r id s (mkeps ds))"
 
       
   545       using mke by (simp_all add: MAIN_decode ds_def bds_def)
 
       
   546     finally have "decode (bmkeps bds) r = Some (flex r id s (mkeps ds))" 
       
   547       unfolding bds_def ds_def .
 
       
   548   }
 
       
   549   then show "blexer r s = lexer r s"
 
       
   550     unfolding blexer_def lexer_flex
 
       
   551     apply(subst bnullable_correctness[symmetric])
 
       
   552     apply(simp)
 
       
   553     done
 
       
   554 qed
 
       
   555 
   413 
   556 lemma asize0:
 
   414 lemma asize0:
 
   557   shows "0 < asize r"
 
   415   shows "0 < asize r"
 
   558   apply(induct  r)
 
   416   apply(induct  r)
 
   559   apply(auto)
 
   417   apply(auto)
 
   563   shows "asize (fuse bs r) = asize r"
 
   421   shows "asize (fuse bs r) = asize r"
 
   564   apply(induct r)
 
   422   apply(induct r)
 
   565   apply(auto)
 
   423   apply(auto)
 
   566   done
 
   424   done
 
   567 
   425 
   568 lemma bder_fuse:
 
   426 lemma TESTTEST:
 
   569   shows "bder c (fuse bs a) = fuse bs (bder c a)"
 
   427   shows "bder c (intern r) = intern (der c r)"
 
   570   apply(induct a arbitrary: bs c)
 
   428   apply(induct r)
 
   571   apply(simp_all)
 
   429        apply(simp)
 
   572   done
 
   430       apply(simp)
 
   573 
   431      apply(simp)
 
   574 lemma bders_fuse:
 
   432     prefer 2
 
   575   shows "bders (fuse bs a) s = fuse bs (bders a s)"
 
   433     apply(simp)  
   576   apply(induct s arbitrary: bs a)
 
   434     apply (simp add: bder_fuse[symmetric])
 
   577    apply(simp_all)
 
   435   prefer 3
 
   578   by (simp add: bder_fuse)
 
   436    apply(simp only: intern.simps)
 
   579 
   437    apply(simp only: der.simps)
 
   580 
   438    apply(simp only: intern.simps)
 
   581 lemma map_bder_fuse:
 
   439     apply(simp only: bder.simps)
 
   582   shows "map (bder c \<circ> fuse bs1) as1 = map (fuse bs1) (map (bder c) as1)"
 
   440   apply(simp)
 
   583   apply(induct as1)
 
   441    apply(simp only: intern.simps)
 
   584   apply(auto simp add: bder_fuse)
 
   442    prefer 2
 
   585   done
 
   443    apply(simp)
 
       
   444    prefer 2
 
       
   445    apply(simp)
 
       
   446   apply(auto)
 
   586 
   447 
   587 
   448 
   588 fun nonnested :: "arexp \<Rightarrow> bool"
 
   449 fun nonnested :: "arexp \<Rightarrow> bool"
 
   589   where
 
   450   where
 
   590   "nonnested (AALTs bs2 []) = True"
 
   451   "nonnested (AALTs bs2 []) = True"
 
   668 | "\<lbrakk>a1 >> bs1; a2 >> bs2\<rbrakk> \<Longrightarrow> ASEQ bs a1 a2 >> bs @ bs1 @ bs2"
 
   529 | "\<lbrakk>a1 >> bs1; a2 >> bs2\<rbrakk> \<Longrightarrow> ASEQ bs a1 a2 >> bs @ bs1 @ bs2"
 
   669 | "r >> bs1 \<Longrightarrow> AALTs bs (r#rs) >> bs @ bs1"
 
   530 | "r >> bs1 \<Longrightarrow> AALTs bs (r#rs) >> bs @ bs1"
 
   670 | "AALTs bs rs >> bs @ bs1 \<Longrightarrow> AALTs bs (r#rs) >> bs @ bs1"
 
   531 | "AALTs bs rs >> bs @ bs1 \<Longrightarrow> AALTs bs (r#rs) >> bs @ bs1"
 
   671 | "ASTAR bs r >> bs @ [S]"
 
   532 | "ASTAR bs r >> bs @ [S]"
 
   672 | "\<lbrakk>r >> bs1; ASTAR [] r >> bs2\<rbrakk> \<Longrightarrow> ASTAR bs r >> bs @ Z # bs1 @ bs2"
 
   533 | "\<lbrakk>r >> bs1; ASTAR [] r >> bs2\<rbrakk> \<Longrightarrow> ASTAR bs r >> bs @ Z # bs1 @ bs2"
 
       
   534 
       
   535 
   673 
   536 
   674 lemma contains0:
 
   537 lemma contains0:
 
   675   assumes "a >> bs"
 
   538   assumes "a >> bs"
 
   676   shows "(fuse bs1 a) >> bs1 @ bs"
 
   539   shows "(fuse bs1 a) >> bs1 @ bs"
 
   677   using assms
 
   540   using assms
 
   895 lemma contains8_iff:
 
   758 lemma contains8_iff:
 
   896   assumes "\<Turnstile> v : ders s (erase r)"
 
   759   assumes "\<Turnstile> v : ders s (erase r)"
 
   897   shows "(bders r s) >> retrieve r (flex (erase r) id s v) \<longleftrightarrow>
 
   760   shows "(bders r s) >> retrieve r (flex (erase r) id s v) \<longleftrightarrow>
 
   898                   r >> retrieve r (flex (erase r) id s v)"
 
   761                   r >> retrieve r (flex (erase r) id s v)"
 
   899   using Prf_flex assms contains6 contains7b by blast
 
   762   using Prf_flex assms contains6 contains7b by blast
 
       
   763 
       
   764 
   900 
   765 
   901 
   766 
   902 fun 
   767 fun 
   903   bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
 
   768   bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
 
   904 where
 
   769 where
 
  2058   apply(rule contains52)
 
  1923   apply(rule contains52)
 
  2059   apply(rule_tac x="bsimp r" in bexI)
 
  1924   apply(rule_tac x="bsimp r" in bexI)
 
  2060    apply(auto)
 
  1925    apply(auto)
 
  2061   using contains0 by blast
 
  1926   using contains0 by blast
 
  2062 
  1927 
       
  1928 lemma test1:
 
       
  1929   shows "AALT [] (ACHAR [Z] c) (ACHAR [S] c) >> [S]"
 
       
  1930   by (metis contains.intros(2) contains.intros(4) contains.intros(5) self_append_conv2)
 
       
  1931 
       
  1932 lemma test1a:
 
       
  1933   shows "bsimp (AALT [] (ACHAR [Z] c) (ACHAR [S] c)) = AALT [] (ACHAR [Z] c) (ACHAR [S] c)"
 
       
  1934   apply(simp)
 
       
  1935   done
 
  2063 
  1936 
  2064 lemma q3a:
 
  1937 lemma q3a:
 
  2065   assumes "\<exists>r \<in> set rs. bnullable r"
 
  1938   assumes "\<exists>r \<in> set rs. bnullable r"
 
  2066   shows "bmkeps (AALTs bs (map (fuse bs1) rs)) = bmkeps (AALTs (bs@bs1) rs)"
 
  1939   shows "bmkeps (AALTs bs (map (fuse bs1) rs)) = bmkeps (AALTs (bs@bs1) rs)"
 
  2067   using assms
 
  1940   using assms
 
  3037 
  2910 
  3038 lemma PPP1_eq:
 
  2911 lemma PPP1_eq:
 
  3039   shows "bsimp r >> bs \<longleftrightarrow> r >> bs"
 
  2912   shows "bsimp r >> bs \<longleftrightarrow> r >> bs"
 
  3040   using contains55 contains55a by blast
 
  2913   using contains55 contains55a by blast
 
  3041 
  2914 
       
  2915 
       
  2916 definition "SET a \<equiv> {bs . a >> bs}"
 
       
  2917 
       
  2918 lemma "SET(bsimp a) \<subseteq> SET(a)"
 
       
  2919   unfolding SET_def
 
       
  2920   apply(auto simp add: PPP1_eq)
 
       
  2921   done
 
       
  2922 
  3042 lemma retrieve_code_bder:
 
  2923 lemma retrieve_code_bder:
 
  3043   assumes "\<Turnstile> v : der c r"
 
  2924   assumes "\<Turnstile> v : der c r"
 
  3044   shows "code (injval r c v) = retrieve (bder c (intern r)) v"
 
  2925   shows "code (injval r c v) = retrieve (bder c (intern r)) v"
 
  3045   using assms
 
  2926   using assms
 
  3046   by (simp add: Prf_injval bder_retrieve retrieve_code)
 
  2927   by (simp add: Prf_injval bder_retrieve retrieve_code)
 
  3076    apply (meson assms lexer_correct_None lexer_correctness(1) lexer_flex)
 
  2957    apply (meson assms lexer_correct_None lexer_correctness(1) lexer_flex)
 
  3077   by (metis L07XX PPP0b assms erase_intern)
 
  2958   by (metis L07XX PPP0b assms erase_intern)
 
  3078 
  2959 
  3079 
  2960 
  3080 
  2961 
  3081   
  2962 lemma PPP:
 
       
  2963   assumes "\<Turnstile> v : r"
 
       
  2964   shows "intern r >> (retrieve (intern r) v)"
 
       
  2965   using assms
 
       
  2966   using contains5 by blast
 
       
  2967   
       
  2968   
       
  2969  
  3082   
  2970   
  3083   
  2971   
  3084   
  2972   
  3085 
  2973 
  3086 
  2974 
  3961 
  3849 
  3962 
  3850 
  3963 (* HERE *)
 
  3851 (* HERE *)
 
  3964 
  3852 
  3965 lemma PX:
 
  3853 lemma PX:
 
  3966   assumes "s \<in> L r" 
  3854   assumes "s \<in> L r" "bders (intern r) s >> code (PX r s)"
 
  3967   shows "bders (intern r) s >> code (PX r s) \<Longrightarrow> bders (bsimp (intern r)) s >> code (PX r s)"
 
  3855   shows "bders (bsimp (intern r)) s >> code (PX r s)"
 
  3968   
  3856   using assms
 
  3969   using FC_def contains7b
 
  3857   apply(induct s arbitrary: r rule: rev_induct)
 
  3970   using assms by me tis
 
  3858    apply(simp)
 
  3971 
  3859    apply (simp add: PPP1_eq)
 
  3972 
  3860   apply (simp add: bders_append bders_simp_append)
 
  3973 
  3861   thm PX_bder_iff PX_bders_iff
 
  3974   
  3862   apply(subst (asm) PX_bder_iff)
 
  3975   apply(simp)
 
  3863    apply(assumption)
 
  3976   (*using FC_bders_iff2[of _ _ "[b]", simplified]*)
 
  3864   apply(subst (asm) (2) PX_bders_iff)
 
  3977   apply(subst (asm) FC_bders_iff2[of _ _ "[b]", simplified])
 
  3865   find_theorems "_ >> code (PX _ _)"
 
  3978   apply(simp)
 
  3866   find_theorems "PX _ _ = _"
 
  3979   apply(subst (asm) FC_bder_iff)
 
  3867   find_theorems "(intern _) >> _"
 
  3980    apply(simp)
 
       
  3981   apply(drule bder_simp_contains)
 
       
  3982   using FC_bder_iff FC_bders_iff2 FC_bders_iff
 
       
  3983   apply(subst (asm) FC_bder_iff[symmetric])
 
       
  3984    apply(subst FC_bder_iff)
 
       
  3985     using FC_bder_iff
 
       
  3986   
       
  3987   
       
  3988   apply (simp add: bder_simp_contains)
 
       
  3989 
       
  3990 lemma bder_simp_contains_IFF2:
 
       
  3991   assumes "bders r s >> bs"
 
       
  3992   shows ""
 
       
  3993   using assms
 
       
  3994   apply(induct s arbitrary: r bs rule: rev_induct)
 
       
  3995    apply(simp)
 
       
  3996   apply (simp add: contains55)  
  3868   apply (simp add: contains55)  
  3997   apply (simp add: bders_append bders_simp_append)
 
  3869   apply (simp add: bders_append bders_simp_append)
 
  3998    apply (simp add: PPP1_eq)
 
  3870    apply (simp add: PPP1_eq)
 
  3999   find_theorems "(bder _ _ >> _) = _"
 
  3871   find_theorems "(bder _ _ >> _) = _"
 
  4000   apply(rule contains50)
 
  3872   apply(rule contains50)
lexing