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.
thys2/SizeBound.thy
changeset 381 0c666a0c57d7
parent 379 28458dec90f8
child 385 c80720289645
equal deleted inserted replaced
380:c892847df987 381:0c666a0c57d7 
   234 
   234 
   235 lemma erase_bders [simp]:
 
   235 lemma erase_bders [simp]:
 
   236   shows "erase (bders r s) = ders s (erase r)"
 
   236   shows "erase (bders r s) = ders s (erase r)"
 
   237   apply(induct s arbitrary: r )
 
   237   apply(induct s arbitrary: r )
 
   238   apply(simp_all)
 
   238   apply(simp_all)
 
       
   239   done
 
       
   240 
       
   241 lemma bnullable_fuse:
 
       
   242   shows "bnullable (fuse bs r) = bnullable r"
 
       
   243   apply(induct r arbitrary: bs)
 
       
   244   apply(auto)
 
   239   done
 
   245   done
 
   240 
   246 
   241 lemma retrieve_encode_STARS:
 
   247 lemma retrieve_encode_STARS:
 
   242   assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> code v = retrieve (intern r) v"
 
   248   assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> code v = retrieve (intern r) v"
 
   243   shows "code (Stars vs) = retrieve (ASTAR [] (intern r)) (Stars vs)"
 
   249   shows "code (Stars vs) = retrieve (ASTAR [] (intern r)) (Stars vs)"
 
   689 
   695 
   690 lemma b4:
 
   696 lemma b4:
 
   691   shows "bnullable (bders_simp r s) = bnullable (bders r s)"
 
   697   shows "bnullable (bders_simp r s) = bnullable (bders r s)"
 
   692   by (metis L_bders_simp bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1))
 
   698   by (metis L_bders_simp bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1))
 
   693 
   699 
   694 
       
   695 lemma qq1:
 
   700 lemma qq1:
 
   696   assumes "\<exists>r \<in> set rs. bnullable r"
 
   701   assumes "\<exists>r \<in> set rs. bnullable r"
 
   697   shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs rs)"
 
   702   shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs rs)"
 
   698   using assms
 
   703   using assms
 
   699   apply(induct rs arbitrary: rs1 bs)
 
   704   apply(induct rs arbitrary: rs1 bs)
 
   707   using assms
 
   712   using assms
 
   708   apply(induct rs arbitrary: rs1 bs)
 
   713   apply(induct rs arbitrary: rs1 bs)
 
   709   apply(simp)
 
   714   apply(simp)
 
   710   apply(simp)
 
   715   apply(simp)
 
   711   by (metis append_assoc in_set_conv_decomp r1 r2)
 
   716   by (metis append_assoc in_set_conv_decomp r1 r2)
 
       
   717   
       
   718 lemma qq3:
 
       
   719   assumes "bnullable (AALTs bs (rs @ rs1))"
 
       
   720           "bnullable (AALTs bs (rs @ rs2))"
 
       
   721           "\<lbrakk>bnullable (AALTs bs rs1); bnullable (AALTs bs rs2); \<forall>r\<in>set rs. \<not>bnullable r\<rbrakk> \<Longrightarrow> 
       
   722                bmkeps (AALTs bs rs1) = bmkeps (AALTs bs rs2)"
 
       
   723   shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs (rs @ rs2))"
 
       
   724   using assms
 
       
   725   apply(case_tac "\<exists>r \<in> set rs. bnullable r")
 
       
   726   using qq1 apply auto[1]
 
       
   727   by (metis UnE bnullable.simps(4) qq2 set_append)
 
   712   
   728   
   713 
   729 
   714 lemma flts_append:
 
   730 lemma flts_append:
 
   715   shows "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
 
   731   shows "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
 
   716 by (induct xs1  arbitrary: xs2  rule: flts.induct)(auto)
 
   732 by (induct xs1  arbitrary: xs2  rule: flts.induct)(auto)
 
   735 
   751 
   736 lemma bbbbs1:
 
   752 lemma bbbbs1:
 
   737   shows "nonalt r \<or> (\<exists>bs rs. r  = AALTs bs rs)"
 
   753   shows "nonalt r \<or> (\<exists>bs rs. r  = AALTs bs rs)"
 
   738   using nonalt.elims(3) by auto
 
   754   using nonalt.elims(3) by auto
 
   739   
   755   
   740 
       
   741 
       
   742 
       
   743 
       
   744 
   756 
   745 
   757 
   746 fun nonazero :: "arexp \<Rightarrow> bool"
 
   758 fun nonazero :: "arexp \<Rightarrow> bool"
 
   747   where
 
   759   where
 
   748   "nonazero AZERO = False"
 
   760   "nonazero AZERO = False"
 
   848    apply(simp)
 
   860    apply(simp)
 
   849    apply (simp add: bnullable_Hdbmkeps_Hd)
 
   861    apply (simp add: bnullable_Hdbmkeps_Hd)
 
   850   apply(simp)
 
   862   apply(simp)
 
   851   using qq4 r1 r2 by auto
 
   863   using qq4 r1 r2 by auto
 
   852 
   864 
   853 
       
   854 
       
   855   
       
   856 lemma bder_fuse:
 
   865 lemma bder_fuse:
 
   857   shows "bder c (fuse bs a) = fuse bs  (bder c a)"
 
   866   shows "bder c (fuse bs a) = fuse bs  (bder c a)"
 
   858   apply(induct a arbitrary: bs c)
 
   867   apply(induct a arbitrary: bs c)
 
   859        apply(simp_all)
 
   868        apply(simp_all)
 
   860   done
 
   869   done
 
   861 
   870 
   862 inductive rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
 
   871 inductive 
   863   where
 
   872   rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
 
       
   873 where
 
   864   "ASEQ bs AZERO r2 \<leadsto> AZERO"
 
   874   "ASEQ bs AZERO r2 \<leadsto> AZERO"
 
   865 | "ASEQ bs r1 AZERO \<leadsto> AZERO"
 
   875 | "ASEQ bs r1 AZERO \<leadsto> AZERO"
 
   866 | "ASEQ bs (AONE bs1) r \<leadsto> fuse (bs@bs1) r"
 
   876 | "ASEQ bs (AONE bs1) r \<leadsto> fuse (bs@bs1) r"
 
   867 | "r1 \<leadsto> r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r2 r3"
 
   877 | "r1 \<leadsto> r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r2 r3"
 
   868 | "r3 \<leadsto> r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r1 r4"
 
   878 | "r3 \<leadsto> r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r1 r4"
 
   878 | "AALTs bs [] \<leadsto> AZERO"
 
   888 | "AALTs bs [] \<leadsto> AZERO"
 
   879 | "AALTs bs [r] \<leadsto> fuse bs r"
 
   889 | "AALTs bs [r] \<leadsto> fuse bs r"
 
   880 | "erase a1 = erase a2 \<Longrightarrow> AALTs bs (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> AALTs bs (rsa@[a1]@rsb@rsc)"
 
   890 | "erase a1 = erase a2 \<Longrightarrow> AALTs bs (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> AALTs bs (rsa@[a1]@rsb@rsc)"
 
   881 
   891 
   882 
   892 
   883 inductive rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100)
 
   893 inductive 
   884   where 
   894   rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100)
 
   885 rs1[intro, simp]:"r \<leadsto>* r"
 
   895 where 
       
   896   rs1[intro, simp]:"r \<leadsto>* r"
 
   886 | rs2[intro]: "\<lbrakk>r1 \<leadsto>* r2; r2 \<leadsto> r3\<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
 
   897 | rs2[intro]: "\<lbrakk>r1 \<leadsto>* r2; r2 \<leadsto> r3\<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
 
   887 
   898 
   888 inductive srewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ s\<leadsto>* _" [100, 100] 100)
 
   899 inductive 
   889   where
 
   900   srewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ s\<leadsto>* _" [100, 100] 100)
 
   890 ss1: "[] s\<leadsto>* []"
 
   901 where
 
   891 |ss2: "\<lbrakk>r \<leadsto>* r'; rs s\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (r#rs) s\<leadsto>* (r'#rs')"
 
   902   ss1: "[] s\<leadsto>* []"
 
   892 (*rs1 = [r1, r2, ..., rn] rs2 = [r1', r2', ..., rn']
 
   903 | ss2: "\<lbrakk>r \<leadsto>* r'; rs s\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (r#rs) s\<leadsto>* (r'#rs')"
 
   893 [r1, r2, ..., rn] \<leadsto>* [r1', r2, ..., rn] \<leadsto>* [...r2',...] \<leadsto>* [r1', r2',... rn']
 
   904 
       
   905 (*
 
       
   906 rs1 = [r1, r2, ..., rn] rs2 = [r1', r2', ..., rn']
 
       
   907     [r1, r2, ..., rn] \<leadsto>* [r1', r2, ..., rn] \<leadsto>* [...r2',...] \<leadsto>* [r1', r2',... rn']
 
   894 *)
 
   908 *)
 
   895 
   909 
   896 
   910 
   897 
   911 
   898 lemma r_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
 
   912 lemma r_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
 
   899   using rrewrites.intros(1) rrewrites.intros(2) by blast
 
   913   using rrewrites.intros(1) rrewrites.intros(2) by blast
 
   900  
   914  
   901 lemma real_trans [trans]: 
   915 lemma real_trans[trans]: 
   902   assumes a1: "r1 \<leadsto>* r2"  and a2: "r2 \<leadsto>* r3"
 
   916   assumes a1: "r1 \<leadsto>* r2"  and a2: "r2 \<leadsto>* r3"
 
   903   shows "r1 \<leadsto>* r3"
 
   917   shows "r1 \<leadsto>* r3"
 
   904   using a2 a1
 
   918   using a2 a1
 
   905   apply(induct r2 r3 arbitrary: r1 rule: rrewrites.induct) 
   919   apply(induct r2 r3 arbitrary: r1 rule: rrewrites.induct) 
   906    apply(auto)
 
   920   apply(auto)
 
   907   done
 
   921   done
 
   908 
   922 
   909 
   923 
   910 lemma  many_steps_later: "\<lbrakk>r1 \<leadsto> r2; r2 \<leadsto>* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
 
   924 lemma  many_steps_later: "\<lbrakk>r1 \<leadsto> r2; r2 \<leadsto>* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
 
   911   by (meson r_in_rstar real_trans)
 
   925   by (meson r_in_rstar real_trans)
 
   976   shows "AONE bs \<leadsto>* bsimp (AONE bs)"  
   990   shows "AONE bs \<leadsto>* bsimp (AONE bs)"  
   977   and   "AZERO \<leadsto>* bsimp AZERO" 
   991   and   "AZERO \<leadsto>* bsimp AZERO" 
   978   and   "ACHAR bs c \<leadsto>* bsimp (ACHAR bs c)"
 
   992   and   "ACHAR bs c \<leadsto>* bsimp (ACHAR bs c)"
 
   979   by (simp_all)
 
   993   by (simp_all)
 
   980 
   994 
   981 lemma trivialbsimpsrewrites: "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs s\<leadsto>* (map f rs)"
 
   995 lemma trivialbsimpsrewrites: 
       
   996   "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs s\<leadsto>* (map f rs)"
 
   982 
   997 
   983   apply(induction rs)
 
   998   apply(induction rs)
 
   984    apply simp
 
   999    apply simp
 
   985    apply(rule ss1)
 
  1000    apply(rule ss1)
 
   986   by (metis insert_iff list.simps(15) list.simps(9) srewrites.simps)
 
  1001   by (metis insert_iff list.simps(15) list.simps(9) srewrites.simps)
 
   987 
  1002 
   988 
  1003 
   989 lemma bsimp_AALTsrewrites: "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs"
 
  1004 lemma bsimp_AALTsrewrites: 
       
  1005   "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs"
 
   990   apply(induction rs)
 
  1006   apply(induction rs)
 
   991   apply simp
 
  1007   apply simp
 
   992    apply(rule r_in_rstar)
 
  1008    apply(rule r_in_rstar)
 
   993   apply (simp add: rrewrite.intros(10))
 
  1009   apply (simp add: rrewrite.intros(10))
 
   994   apply(case_tac "rs = Nil")
 
  1010   apply(case_tac "rs = Nil")
 
   998   apply(subgoal_tac "length (a#rs) > 1")
 
  1014   apply(subgoal_tac "length (a#rs) > 1")
 
   999    apply(simp add: bsimp_AALTs_qq)
 
  1015    apply(simp add: bsimp_AALTs_qq)
 
  1000   apply(simp)
 
  1016   apply(simp)
 
  1001   done 
  1017   done 
  1002 
  1018 
  1003 inductive frewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ f\<leadsto>* _" [100, 100] 100)
 
  1019 (* rewrites for lists *)
 
  1004   where
 
  1020 inductive 
  1005 fs1: "[] f\<leadsto>* []"
 
  1021   frewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ f\<leadsto>* _" [100, 100] 100)
 
  1006 |fs2: "\<lbrakk>rs f\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (AZERO#rs) f\<leadsto>* rs'"
 
  1022 where
 
  1007 |fs3: "\<lbrakk>rs f\<leadsto>* rs'\<rbrakk> \<Longrightarrow> ((AALTs bs rs1) # rs) f\<leadsto>* ((map (fuse bs) rs1) @ rs')"
 
  1023   fs1: "[] f\<leadsto>* []"
 
  1008 |fs4: "\<lbrakk>rs f\<leadsto>* rs';nonalt r; nonazero r\<rbrakk> \<Longrightarrow> (r#rs) f\<leadsto>* (r#rs')"
 
  1024 | fs2: "\<lbrakk>rs f\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (AZERO#rs) f\<leadsto>* rs'"
 
       
  1025 | fs3: "\<lbrakk>rs f\<leadsto>* rs'\<rbrakk> \<Longrightarrow> ((AALTs bs rs1) # rs) f\<leadsto>* ((map (fuse bs) rs1) @ rs')"
 
       
  1026 | fs4: "\<lbrakk>rs f\<leadsto>* rs'; nonalt r; nonazero r\<rbrakk> \<Longrightarrow> (r#rs) f\<leadsto>* (r#rs')"
 
  1009 
  1027 
  1010 
  1028 
  1011 
  1029 
  1012 lemma flts_prepend: "\<lbrakk>nonalt a; nonazero a\<rbrakk> \<Longrightarrow> flts (a#rs) = a # (flts rs)"
 
  1030 lemma flts_prepend: "\<lbrakk>nonalt a; nonazero a\<rbrakk> \<Longrightarrow> flts (a#rs) = a # (flts rs)"
 
  1013   by (metis append_Cons append_Nil flts_single1 flts_append)
 
  1031   by (metis append_Cons append_Nil flts_single1 flts_append)
 
  1103 
  1121 
  1104 lemma somewhereMapInside: "f r \<in> f ` set rs \<Longrightarrow> \<exists>rs1 rs2 a. rs = rs1@[a]@rs2 \<and> f a = f r"
 
  1122 lemma somewhereMapInside: "f r \<in> f ` set rs \<Longrightarrow> \<exists>rs1 rs2 a. rs = rs1@[a]@rs2 \<and> f a = f r"
 
  1105   apply auto
 
  1123   apply auto
 
  1106   by (metis split_list)
 
  1124   by (metis split_list)
 
  1107 
  1125 
  1108 lemma alts_dBrewrites_withFront: " AALTs bs (rsa @ rs) \<leadsto>* AALTs bs (rsa @ distinctBy rs erase (erase ` set rsa))"
 
  1126 lemma alts_dBrewrites_withFront: 
       
  1127   "AALTs bs (rsa @ rs) \<leadsto>* AALTs bs (rsa @ distinctBy rs erase (erase ` set rsa))"
 
  1109   apply(induction rs arbitrary: rsa)
 
  1128   apply(induction rs arbitrary: rsa)
 
  1110    apply simp
 
  1129    apply simp
 
  1111   apply(drule_tac x = "rsa@[a]" in meta_spec)
 
  1130   apply(drule_tac x = "rsa@[a]" in meta_spec)
 
  1112   apply(subst threelistsappend)
 
  1131   apply(subst threelistsappend)
 
  1113   apply(rule real_trans)
 
  1132   apply(rule real_trans)
 
  1152    apply simp
 
  1171    apply simp
 
  1153   apply simp
 
  1172   apply simp
 
  1154   using alts_dBrewrites_withFront
 
  1173   using alts_dBrewrites_withFront
 
  1155   by (metis append_Nil dB_single_step empty_set image_empty)
 
  1174   by (metis append_Nil dB_single_step empty_set image_empty)
 
  1156 
  1175 
  1157 
       
  1158 
       
  1159   
       
  1160 
       
  1161 
       
  1162 lemma bsimp_rewrite: 
  1176 lemma bsimp_rewrite: 
  1163   shows "r \<leadsto>* bsimp r"
 
  1177   shows "r \<leadsto>* bsimp r"
 
  1164   apply(induction r rule: bsimp.induct)
 
  1178 proof (induction r rule: bsimp.induct)
 
  1165        apply simp
 
  1179   case (1 bs1 r1 r2)
 
  1166        apply(case_tac "bsimp r1 = AZERO")
 
  1180   then show "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)"
 
       
  1181     apply(simp)
 
       
  1182     apply(case_tac "bsimp r1 = AZERO")
 
  1167         apply simp
 
  1183         apply simp
 
  1168   using continuous_rewrite apply blast
 
  1184   using continuous_rewrite apply blast
 
  1169        apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
 
  1185        apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
 
  1170         apply(erule exE)
 
  1186         apply(erule exE)
 
  1171         apply simp
 
  1187         apply simp
 
  1172         apply(subst bsimp_ASEQ2)
 
  1188         apply(subst bsimp_ASEQ2)
 
  1173         apply (meson real_trans rrewrite.intros(3) rrewrites.intros(2) star_seq star_seq2)
 
  1189         apply (meson real_trans rrewrite.intros(3) rrewrites.intros(2) star_seq star_seq2)
 
  1174        apply (smt (verit, best) bsimp_ASEQ0 bsimp_ASEQ1 real_trans rrewrite.intros(2) rs2 star_seq star_seq2)
 
  1190        apply (smt (verit, best) bsimp_ASEQ0 bsimp_ASEQ1 real_trans rrewrite.intros(2) rs2 star_seq star_seq2)
 
  1175       defer
 
  1191   done
 
  1176   using bsimp_aalts_simpcases(2) apply blast
 
  1192 next
 
  1177   apply simp
 
  1193   case (2 bs1 rs)
 
  1178   apply simp
 
  1194   then show "AALTs bs1 rs \<leadsto>* bsimp (AALTs bs1 rs)"
 
  1179   apply simp
 
  1195     by (metis alts_dBrewrites alts_simpalts bsimp.simps(2) bsimp_AALTsrewrites fltsrewrites real_trans)  
  1180 
  1196 next
 
  1181   apply auto
 
  1197   case "3_1"
 
  1182 
  1198   then show "AZERO \<leadsto>* bsimp AZERO"
 
  1183 
  1199     by simp
 
  1184   apply(subgoal_tac "AALTs bs1 rs \<leadsto>* AALTs bs1 (map bsimp rs)")
 
  1200 next
 
  1185    apply(subgoal_tac "AALTs bs1 (map bsimp rs) \<leadsto>* AALTs bs1 (flts (map bsimp rs))")
 
  1201   case ("3_2" v)
 
  1186   apply(subgoal_tac "AALTs bs1 (flts (map bsimp rs)) \<leadsto>* AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {})")
 
  1202   then show "AONE v \<leadsto>* bsimp (AONE v)" 
  1187     apply(subgoal_tac "AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {}) \<leadsto>* bsimp_AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {} )")
 
  1203     by simp
 
  1188 
  1204 next
 
  1189   
  1205   case ("3_3" v va)
 
  1190       apply (meson real_trans)
 
  1206   then show "ACHAR v va \<leadsto>* bsimp (ACHAR v va)" 
  1191 
  1207     by simp
 
  1192    apply (meson bsimp_AALTsrewrites)
 
  1208 next
 
  1193 
  1209   case ("3_4" v va)
 
  1194   apply (meson alts_dBrewrites)
 
  1210   then show "ASTAR v va \<leadsto>* bsimp (ASTAR v va)" 
  1195 
  1211     by simp
 
  1196   using fltsrewrites apply auto[1]
 
  1212 qed
 
  1197 
       
  1198   using alts_simpalts by force
 
       
  1199 
       
  1200 
       
  1201 lemma rewrite_non_nullable: "\<lbrakk>r1 \<leadsto> r2; \<not>bnullable r1 \<rbrakk> \<Longrightarrow> \<not>bnullable r2"
 
       
  1202   apply(induction r1 r2 rule: rrewrite.induct)
 
       
  1203              apply auto 
       
  1204       apply (metis bnullable_correctness erase_fuse)+
 
       
  1205   done
 
       
  1206 
  1213 
  1207 lemma rewrite_non_nullable_strong: 
  1214 lemma rewrite_non_nullable_strong: 
  1208   assumes "r1 \<leadsto> r2"
 
  1215   assumes "r1 \<leadsto> r2"
 
  1209   shows "bnullable r1 = bnullable r2"
 
  1216   shows "bnullable r1 = bnullable r2"
 
  1210 using assms
 
  1217 using assms
 
  1227 using assms
 
  1234 using assms
 
  1228   apply(induction r1 r2 rule: rrewrites.induct)
 
  1235   apply(induction r1 r2 rule: rrewrites.induct)
 
  1229   apply simp
 
  1236   apply simp
 
  1230   using rewrite_non_nullable_strong by blast
 
  1237   using rewrite_non_nullable_strong by blast
 
  1231 
  1238 
  1232 lemma nonbnullable_lists_concat: " \<lbrakk> \<not> (\<exists>r0\<in>set rs1. bnullable r0); \<not> bnullable r; \<not> (\<exists>r0\<in>set rs2. bnullable r0)\<rbrakk> \<Longrightarrow> 
  1239 
  1233 \<not>(\<exists>r0 \<in> (set (rs1@[r]@rs2)). bnullable r0 ) "
 
  1240 lemma bnullable_segment: 
  1234   apply simp
 
  1241   "bnullable (AALTs bs (rs1@[r]@rs2)) \<Longrightarrow> bnullable (AALTs bs rs1) \<or> bnullable (AALTs bs rs2) \<or> bnullable r"
 
  1235   apply blast
 
  1242   by auto
 
  1236   done
 
       
  1237 
       
  1238 
       
  1239 
       
  1240 lemma nomember_bnullable: "\<lbrakk> \<not> (\<exists>r0\<in>set rs1. bnullable r0); \<not> bnullable r; \<not> (\<exists>r0\<in>set rs2. bnullable r0)\<rbrakk>
 
       
  1241  \<Longrightarrow> \<not>bnullable (AALTs bs (rs1 @ [r] @ rs2))"
 
       
  1242   using bnullable.simps(4) nonbnullable_lists_concat by presburger
 
       
  1243 
       
  1244 lemma bnullable_segment: " bnullable (AALTs bs (rs1@[r]@rs2)) \<Longrightarrow> bnullable (AALTs bs rs1) \<or> bnullable (AALTs bs rs2) \<or> bnullable r"
 
       
  1245   apply(case_tac "\<exists>r0\<in>set rs1.  bnullable r0")
 
       
  1246   using r2 apply blast
 
       
  1247   apply(case_tac "bnullable r")
 
       
  1248 
       
  1249   apply blast
 
       
  1250   apply(case_tac "\<exists>r0\<in>set rs2.  bnullable r0")
 
       
  1251 
       
  1252   using bnullable.simps(4) apply presburger
 
       
  1253   apply(subgoal_tac "False")
 
       
  1254 
       
  1255   apply blast
 
       
  1256 
       
  1257   using nomember_bnullable by blast
 
       
  1258 
       
  1259   
       
  1260 
  1243 
  1261 lemma bnullablewhichbmkeps: "\<lbrakk>bnullable  (AALTs bs (rs1@[r]@rs2)); \<not> bnullable (AALTs bs rs1); bnullable r \<rbrakk>
 
  1244 lemma bnullablewhichbmkeps: "\<lbrakk>bnullable  (AALTs bs (rs1@[r]@rs2)); \<not> bnullable (AALTs bs rs1); bnullable r \<rbrakk>
 
  1262  \<Longrightarrow> bmkeps (AALTs bs (rs1@[r]@rs2)) = bs @ (bmkeps r)"
 
  1245  \<Longrightarrow> bmkeps (AALTs bs (rs1@[r]@rs2)) = bs @ (bmkeps r)"
 
       
  1246   
  1263   using qq2 bnullable_Hdbmkeps_Hd by force
 
  1247   using qq2 bnullable_Hdbmkeps_Hd by force
 
  1264 
       
  1265 
       
  1266 
  1248 
  1267 lemma spillbmkepslistr: "bnullable (AALTs bs1 rs1)
 
  1249 lemma spillbmkepslistr: "bnullable (AALTs bs1 rs1)
 
  1268     \<Longrightarrow> bmkeps (AALTs bs (AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs ( map (fuse bs1) rs1 @ rsb))"
 
  1250     \<Longrightarrow> bmkeps (AALTs bs (AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs ( map (fuse bs1) rs1 @ rsb))"
 
  1269   apply(subst bnullable_Hdbmkeps_Hd)
 
  1251   apply(subst bnullable_Hdbmkeps_Hd)
 
  1270   
  1252   
  1271    apply simp
 
  1253    apply simp
 
  1272   by (metis bmkeps.simps(3) k0a list.set_intros(1) qq1 qq4 qs3)
 
  1254   by (metis bmkeps.simps(3) k0a list.set_intros(1) qq1 qq4 qs3)
 
  1273 
  1255 
  1274 lemma third_segment_bnullable: "\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow> 
  1256 lemma third_segment_bnullable: 
  1275 bnullable (AALTs bs rs3)"
 
  1257   "\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow> 
       
  1258    bnullable (AALTs bs rs3)"
 
       
  1259   apply(auto)
 
       
  1260   done
 
       
  1261 
       
  1262 lemma third_segment_bmkeps:  
       
  1263   "\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow> 
       
  1264    bmkeps (AALTs bs (rs1@rs2@rs3) ) = bmkeps (AALTs bs rs3)"
 
       
  1265   by (metis bnullable.simps(1) bnullable.simps(4) bsimp_AALTs.simps(1) bsimp_AALTsrewrites qq2 rewritesnullable self_append_conv third_segment_bnullable)
 
       
  1266 
       
  1267 lemma rewrite_bmkepsalt: 
       
  1268   "\<lbrakk>bnullable (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)); bnullable (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))\<rbrakk>
 
       
  1269        \<Longrightarrow> bmkeps (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"
 
       
  1270   apply(rule qq3)
 
       
  1271   apply(simp)
 
       
  1272   apply(simp)
 
       
  1273   apply(case_tac "bnullable (AALTs bs1 rs1)")
 
       
  1274   using spillbmkepslistr apply blast
 
       
  1275   apply(subst qq2)
 
       
  1276     apply(auto simp add: bnullable_fuse r1)
 
       
  1277   done
 
       
  1278 
       
  1279 lemma rewrite_bmkeps_aux: 
       
  1280   assumes "r1 \<leadsto> r2" "bnullable r1" "bnullable r2"
 
       
  1281   shows "bmkeps r1 = bmkeps r2"
 
       
  1282   using assms 
       
  1283 proof (induction r1 r2 rule: rrewrite.induct)
 
       
  1284   case (1 bs r2)
 
       
  1285   then show ?case by simp 
       
  1286 next
 
       
  1287   case (2 bs r1)
 
       
  1288   then show ?case by simp
 
       
  1289 next
 
       
  1290   case (3 bs bs1 r)
 
       
  1291   then show ?case by (simp add: b2) 
       
  1292 next
 
       
  1293   case (4 r1 r2 bs r3)
 
       
  1294   then show ?case by simp
 
       
  1295 next
 
       
  1296   case (5 r3 r4 bs r1)
 
       
  1297   then show ?case by simp
 
       
  1298 next
 
       
  1299   case (6 r r' bs rs1 rs2)
 
       
  1300   then show ?case
 
       
  1301     by (metis append_Cons append_Nil bnullable.simps(4) bnullable_segment bnullablewhichbmkeps qq3 r1 rewrite_non_nullable_strong)
 
       
  1302 next
 
       
  1303   case (7 bs rsa rsb)
 
       
  1304   then show ?case
 
       
  1305     by (metis bnullable.simps(1) bnullable.simps(4) bnullable_segment qq1 qq2 rewrite_nullable rrewrite.intros(10) rrewrite0away third_segment_bmkeps) 
       
  1306 next
 
       
  1307   case (8 bs rsa bs1 rs1 rsb)
 
       
  1308   then show ?case
 
       
  1309     by (simp add: rewrite_bmkepsalt) 
       
  1310 next
 
       
  1311   case (9 bs bs1 rs)
 
       
  1312   then show ?case
 
       
  1313     by (simp add: q3a) 
       
  1314 next
 
       
  1315   case (10 bs)
 
       
  1316   then show ?case
 
       
  1317     by fastforce 
       
  1318 next
 
       
  1319   case (11 bs r)
 
       
  1320   then show ?case
 
       
  1321     by (simp add: b2) 
       
  1322 next
 
       
  1323   case (12 a1 a2 bs rsa rsb rsc)
 
       
  1324   then show ?case
 
       
  1325     by (smt (verit, ccfv_threshold) append_Cons append_eq_appendI append_self_conv2 bnullable_correctness list.set_intros(1) qq3 r1)
 
       
  1326 qed
 
       
  1327 
       
  1328 
       
  1329 lemma rewrite_bmkeps: 
       
  1330   assumes "r1 \<leadsto> r2" "bnullable r1"
 
       
  1331   shows "bmkeps r1 = bmkeps r2"
 
       
  1332   using assms(1) assms(2) rewrite_bmkeps_aux rewrite_nullable by blast
 
  1276   
  1333   
  1277   by (metis append.left_neutral append_Cons bnullable.simps(1) bnullable_segment rrewrite.intros(7) rewrite_non_nullable)
 
       
  1278 
       
  1279 
       
  1280 lemma third_segment_bmkeps:  "\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow> 
       
  1281 bmkeps (AALTs bs (rs1@rs2@rs3) ) = bmkeps (AALTs bs rs3)"
 
       
  1282   apply(subgoal_tac "bnullable (AALTs bs rs3)")
 
       
  1283    apply(subgoal_tac "\<forall>r \<in> set (rs1@rs2). \<not>bnullable r")
 
       
  1284   apply(subgoal_tac "bmkeps (AALTs bs (rs1@rs2@rs3)) = bmkeps (AALTs bs ((rs1@rs2)@rs3) )")
 
       
  1285   apply (metis bnullable.simps(4) qq2)
 
       
  1286 
       
  1287   apply (metis append.assoc)
 
       
  1288 
       
  1289   apply (metis append.assoc in_set_conv_decomp r2 third_segment_bnullable)
 
       
  1290 
       
  1291   using third_segment_bnullable by blast
 
       
  1292 
       
  1293 
       
  1294 lemma rewrite_bmkepsalt: " \<lbrakk>bnullable (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)); bnullable (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))\<rbrakk>
 
       
  1295        \<Longrightarrow> bmkeps (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"
 
       
  1296   apply(case_tac "bnullable (AALTs bs rsa)")
 
       
  1297   
       
  1298   using qq1 apply force
 
       
  1299   apply(case_tac "bnullable (AALTs bs1 rs1)")
 
       
  1300   apply(subst qq2)
 
       
  1301 
       
  1302   
       
  1303   using r2 apply blast
 
       
  1304   
       
  1305     apply (metis list.set_intros(1))
 
       
  1306   apply (metis append_Nil bnullable.simps(1) rewrite_non_nullable_strong rrewrite.intros(10) spillbmkepslistr third_segment_bmkeps)
 
       
  1307   apply(subgoal_tac "bmkeps  (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs rsb) ")
 
       
  1308    prefer 2
 
       
  1309   
       
  1310   apply (metis append_Cons append_Nil bnullable.simps(1) bnullable_segment rewrite_nullable rrewrite.intros(10) third_segment_bmkeps)
 
       
  1311   by (metis bnullable.simps(4) rewrite_non_nullable_strong rrewrite.intros(9) third_segment_bmkeps)
 
       
  1312 
       
  1313 
       
  1314 
       
  1315 lemma rewrite_bmkeps: "\<lbrakk> r1 \<leadsto> r2; bnullable r1\<rbrakk> \<Longrightarrow> bmkeps r1 = bmkeps r2"
 
       
  1316 
       
  1317   apply(frule rewrite_nullable)
 
       
  1318   apply simp
 
       
  1319   apply(induction r1 r2 rule: rrewrite.induct)
 
       
  1320              apply simp
 
       
  1321   using bnullable.simps(1) bnullable.simps(5) apply blast
 
       
  1322          apply (simp add: b2)
 
       
  1323         apply simp
 
       
  1324          apply simp
 
       
  1325   apply(frule bnullable_segment)
 
       
  1326         apply(case_tac "bnullable (AALTs bs rs1)")
 
       
  1327   using qq1 apply force
 
       
  1328         apply(case_tac "bnullable r")
 
       
  1329   using bnullablewhichbmkeps rewrite_nullable apply presburger
 
       
  1330         apply(subgoal_tac "bnullable (AALTs bs rs2)")
 
       
  1331   apply(subgoal_tac "\<not> bnullable r'")
 
       
  1332   apply (simp add: qq2 r1)
 
       
  1333   
       
  1334   using rewrite_non_nullable apply blast
 
       
  1335 
       
  1336         apply blast
 
       
  1337        apply (simp add: flts_append qs3)
 
       
  1338   apply (simp add: rewrite_bmkepsalt)
 
       
  1339   using q3a apply force
 
       
  1340 
       
  1341   apply (simp add: q3a)
 
       
  1342   apply (simp add: b2)
 
       
  1343   apply(simp del: append.simps)
 
       
  1344   apply(case_tac "bnullable a1")
 
       
  1345   apply (metis append.assoc in_set_conv_decomp qq1)
 
       
  1346   apply(case_tac "\<exists>r \<in> set rsa. bnullable r")
 
       
  1347   using qq1 apply presburger
 
       
  1348   apply(case_tac "\<exists>r \<in> set rsb. bnullable r")
 
       
  1349   apply (metis UnCI append.assoc qq1 set_append)
 
       
  1350   apply(case_tac "bnullable a2")
 
       
  1351   apply (metis bnullable_correctness)
 
       
  1352   apply(subst qq2)
 
       
  1353   apply blast
 
       
  1354   apply(auto)[1]
 
       
  1355   apply(subst qq2)
 
       
  1356   apply (metis empty_iff list.set(1) set_ConsD)
 
       
  1357   apply(auto)[1]
 
       
  1358   apply(subst qq2)
 
       
  1359   apply(auto)[2]
 
       
  1360   apply(subst qq2)
 
       
  1361   apply(auto)[2]
 
       
  1362   apply(subst qq2)
 
       
  1363   apply(auto)[2]
 
       
  1364   apply(subst qq2)
 
       
  1365   apply(auto)[2]
 
       
  1366   apply(subst qq2)
 
       
  1367   apply(auto)[2]
 
       
  1368   apply(simp)
 
       
  1369   done
 
       
  1370 
  1334 
  1371 lemma rewrites_bmkeps: 
  1335 lemma rewrites_bmkeps: 
  1372   assumes "r1 \<leadsto>* r2" "bnullable r1" 
  1336   assumes "r1 \<leadsto>* r2" "bnullable r1" 
  1373   shows "bmkeps r1 = bmkeps r2"
 
  1337   shows "bmkeps r1 = bmkeps r2"
 
  1374   using assms
 
  1338   using assms
 
  1387 qed
 
  1351 qed
 
  1388 
  1352 
  1389 lemma alts_rewrite_front: "r \<leadsto> r' \<Longrightarrow> AALTs bs (r # rs) \<leadsto> AALTs bs (r' # rs)"
 
  1353 lemma alts_rewrite_front: "r \<leadsto> r' \<Longrightarrow> AALTs bs (r # rs) \<leadsto> AALTs bs (r' # rs)"
 
  1390   by (metis append_Cons append_Nil rrewrite.intros(6))
 
  1354   by (metis append_Cons append_Nil rrewrite.intros(6))
 
  1391 
  1355 
  1392 lemma alt_rewrite_front: "r \<leadsto> r' \<Longrightarrow> AALT bs r r2 \<leadsto> AALT bs r' r2"
 
       
  1393   using alts_rewrite_front by blast
 
       
  1394 
       
  1395 lemma to_zero_in_alt: " AALT bs (ASEQ [] AZERO r) r2 \<leadsto>  AALT bs AZERO r2"
 
  1356 lemma to_zero_in_alt: " AALT bs (ASEQ [] AZERO r) r2 \<leadsto>  AALT bs AZERO r2"
 
  1396   by (simp add: alts_rewrite_front rrewrite.intros(1))
 
  1357   by (simp add: alts_rewrite_front rrewrite.intros(1))
 
  1397 
  1358 
  1398 lemma alt_remove0_front: " AALT bs AZERO r \<leadsto> AALTs bs [r]"
 
  1359 lemma rewrite_fuse: 
  1399   by (simp add: rrewrite0away)
 
  1360   assumes "r2 \<leadsto> r3"
 
  1400 
  1361   shows "fuse bs r2 \<leadsto>* fuse bs r3"
 
  1401 lemma alt_rewrites_back: "r2 \<leadsto>* r2' \<Longrightarrow>AALT bs r1 r2 \<leadsto>* AALT bs r1 r2'"
 
  1362   using assms
 
  1402   apply(induction r2 r2' arbitrary: bs rule: rrewrites.induct)
 
  1363 proof(induction r2 r3 arbitrary: bs rule: rrewrite.induct)
 
  1403    apply simp
 
  1364   case (1 bs r2)
 
  1404   by (meson rs1 rs2 srewrites_alt1 ss1 ss2)
 
  1365   then show ?case
 
  1405 
  1366     by (simp add: continuous_rewrite) 
  1406 lemma rewrite_fuse: " r2 \<leadsto> r3 \<Longrightarrow> fuse bs r2 \<leadsto>* fuse bs r3"
 
  1367 next
 
  1407   apply(induction r2 r3 arbitrary: bs rule: rrewrite.induct)
 
  1368   case (2 bs r1)
 
  1408              apply auto
 
  1369   then show ?case
 
  1409 
  1370     using rrewrite.intros(2) by force 
  1410            apply (simp add: continuous_rewrite)
 
  1371 next
 
  1411 
  1372   case (3 bs bs1 r)
 
  1412           apply (simp add: r_in_rstar rrewrite.intros(2))
 
  1373   then show ?case
 
  1413 
  1374     by (metis fuse.simps(5) fuse_append r_in_rstar rrewrite.intros(3)) 
  1414          apply (metis fuse_append r_in_rstar rrewrite.intros(3))
 
  1375 next
 
  1415 
  1376   case (4 r1 r2 bs r3)
 
  1416   using r_in_rstar star_seq apply blast
 
  1377   then show ?case
 
  1417 
  1378     by (simp add: r_in_rstar star_seq) 
  1418   using r_in_rstar star_seq2 apply blast
 
  1379 next
 
  1419 
  1380   case (5 r3 r4 bs r1)
 
  1420   using contextrewrites2 r_in_rstar apply auto[1]
 
  1381   then show ?case
 
  1421   
  1382     using fuse.simps(5) r_in_rstar star_seq2 by auto  
  1422   using rrewrite.intros(8) apply auto[1]
 
  1383 next
 
  1423   using rrewrite.intros(7) apply auto[1]
 
  1384   case (6 r r' bs rs1 rs2)
 
  1424   using rrewrite.intros(8) apply force
 
  1385   then show ?case
 
  1425   apply (metis append_assoc r_in_rstar rrewrite.intros(9))
 
  1386     using contextrewrites2 r_in_rstar by force 
  1426   apply (simp add: r_in_rstar rrewrite.intros(10))
 
  1387 next
 
  1427   apply (metis fuse_append r_in_rstar rrewrite.intros(11))
 
  1388   case (7 bs rsa rsb)
 
  1428   using rrewrite.intros(12) by auto
 
  1389   then show ?case
 
  1429   
  1390     using rrewrite.intros(7) by force  
       
  1391 next
 
       
  1392   case (8 bs rsa bs1 rs1 rsb)
 
       
  1393   then show ?case
 
       
  1394     using rrewrite.intros(8) by force 
       
  1395 next
 
       
  1396   case (9 bs bs1 rs)
 
       
  1397   then show ?case
 
       
  1398     by (metis append.assoc fuse.simps(4) r_in_rstar rrewrite.intros(9)) 
       
  1399 next
 
       
  1400   case (10 bs)
 
       
  1401   then show ?case
 
       
  1402     by (simp add: r_in_rstar rrewrite.intros(10)) 
       
  1403 next
 
       
  1404   case (11 bs r)
 
       
  1405   then show ?case
 
       
  1406     by (metis fuse.simps(4) fuse_append r_in_rstar rrewrite.intros(11)) 
       
  1407 next
 
       
  1408   case (12 a1 a2 bs rsa rsb rsc)
 
       
  1409   then show ?case
 
       
  1410     using fuse.simps(4) r_in_rstar rrewrite.intros(12) by auto 
       
  1411 qed
 
  1430 
  1412 
  1431 lemma rewrites_fuse:  
  1413 lemma rewrites_fuse:  
  1432   assumes "r2 \<leadsto>* r2'"
 
  1414   assumes "r1 \<leadsto>* r2"
 
  1433   shows "fuse bs1 r2 \<leadsto>* fuse bs1 r2'"
 
  1415   shows "fuse bs r1 \<leadsto>* fuse bs r2"
 
  1434 using assms
 
  1416 using assms
 
  1435 apply(induction r2 r2' arbitrary: bs1 rule: rrewrites.induct)
 
  1417 apply(induction r1 r2 arbitrary: bs rule: rrewrites.induct)
 
  1436 apply(auto intro: rewrite_fuse real_trans)
 
  1418 apply(auto intro: rewrite_fuse real_trans)
 
  1437 done
 
  1419 done
 
  1438 
  1420 
  1439 lemma  bder_fuse_list: 
  1421 lemma  bder_fuse_list: 
  1440   shows "map (bder c \<circ> fuse bs1) rs1 = map (fuse bs1 \<circ> bder c) rs1"
 
  1422   shows "map (bder c \<circ> fuse bs1) rs1 = map (fuse bs1 \<circ> bder c) rs1"
 
  1441 apply(induction rs1)
 
  1423 apply(induction rs1)
 
  1442 apply(simp_all add: bder_fuse)
 
  1424 apply(simp_all add: bder_fuse)
 
  1443 done
 
  1425 done
 
  1444 
  1426 
  1445 
  1427 
  1446 lemma rewrite_der_altmiddle: "bder c (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) \<leadsto>* bder c (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"
 
  1428 lemma rewrite_der_altmiddle: 
       
  1429   "bder c (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) \<leadsto>* bder c (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"
 
  1447    apply simp
 
  1430    apply simp
 
  1448    apply(simp add: bder_fuse_list del: append.simps)
 
  1431    apply(simp add: bder_fuse_list del: append.simps)
 
  1449   by (metis append.assoc map_map r_in_rstar rrewrite.intros(8) threelistsappend)
 
  1432   by (metis append.assoc map_map r_in_rstar rrewrite.intros(8) threelistsappend)
 
  1450 
  1433 
  1451 lemma lock_step_der_removal: 
  1434 lemma lock_step_der_removal: 
  1454                                   bder c (AALTs bs (rsa @ [a1] @ rsb @ rsc))"
 
  1437                                   bder c (AALTs bs (rsa @ [a1] @ rsb @ rsc))"
 
  1455   apply(simp)
 
  1438   apply(simp)
 
  1456   
  1439   
  1457   using rrewrite.intros(12) by auto
 
  1440   using rrewrite.intros(12) by auto
 
  1458 
  1441 
  1459 lemma rewrite_after_der: "r1 \<leadsto> r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)"
 
  1442 lemma rewrite_after_der: 
  1460   apply(induction r1 r2 arbitrary: c rule: rrewrite.induct)
 
  1443   assumes "r1 \<leadsto> r2"
 
  1461   
  1444   shows "(bder c r1) \<leadsto>* (bder c r2)"
 
  1462               apply (simp add: r_in_rstar rrewrite.intros(1))
 
  1445   using assms
 
  1463   apply simp
 
  1446 proof(induction r1 r2 rule: rrewrite.induct)
 
  1464   
  1447   case (1 bs r2)
 
  1465   apply (meson contextrewrites1 r_in_rstar rrewrite.intros(10) rrewrite.intros(2) rrewrite0away rs2)
 
  1448   then show "bder c (ASEQ bs AZERO r2) \<leadsto>* bder c AZERO"
 
  1466            apply(simp)
 
  1449     by (simp add: continuous_rewrite) 
  1467            apply(rule many_steps_later)
 
  1450 next
 
  1468             apply(rule to_zero_in_alt)
 
  1451   case (2 bs r1)
 
  1469            apply(rule many_steps_later)
 
  1452   then show "bder c (ASEQ bs r1 AZERO) \<leadsto>* bder c AZERO"
 
  1470   apply(rule alt_remove0_front)
 
  1453     apply(simp)
 
  1471            apply(rule many_steps_later)
 
  1454     by (meson contextrewrites1 r_in_rstar real_trans rrewrite.intros(10) rrewrite.intros(2) rrewrite0away)
 
  1472             apply(rule rrewrite.intros(11))
 
  1455 next
 
  1473   using bder_fuse fuse_append rs1 apply presburger
 
  1456   case (3 bs bs1 r)
 
  1474           apply(case_tac "bnullable r1")
 
  1457   then show "bder c (ASEQ bs (AONE bs1) r) \<leadsto>* bder c (fuse (bs @ bs1) r)" 
  1475   prefer 2
 
  1458     apply(simp)
 
  1476            apply(subgoal_tac "\<not>bnullable r2")
 
  1459     by (metis bder_fuse fuse_append rrewrite.intros(11) rrewrite0away rrewrites.simps to_zero_in_alt)
 
  1477             prefer 2
 
  1460 next
 
  1478   using rewrite_non_nullable apply presburger
 
  1461   case (4 r1 r2 bs r3)
 
  1479            apply simp+
 
  1462   have as: "r1 \<leadsto> r2" by fact
 
  1480   
  1463   have IH: "bder c r1 \<leadsto>* bder c r2" by fact
 
  1481   using star_seq apply auto[1]
 
  1464   from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r2 r3)"
 
  1482           apply(subgoal_tac "bnullable r2")
 
  1465     by (simp add: contextrewrites1 rewrite_bmkeps rewrite_non_nullable_strong star_seq) 
  1483            apply simp+
 
  1466 next
 
  1484   apply(subgoal_tac "bmkeps r1 = bmkeps r2")
 
  1467   case (5 r3 r4 bs r1)
 
  1485   prefer 2
 
  1468   have as: "r3 \<leadsto> r4" by fact 
  1486   using rewrite_bmkeps apply auto[1]
 
  1469   have IH: "bder c r3 \<leadsto>* bder c r4" by fact 
  1487   using contextrewrites1 star_seq apply auto[1]
 
  1470   from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r1 r4)" 
  1488   using rewrite_nullable apply auto[1]
 
  1471     apply(simp)
 
  1489          apply(case_tac "bnullable r1")
 
  1472     using r_in_rstar rewrites_fuse srewrites_alt1 ss1 ss2 star_seq2 by presburger
 
  1490           apply simp
 
  1473 next
 
  1491           apply(subgoal_tac "ASEQ [] (bder c r1) r3 \<leadsto> ASEQ [] (bder c r1) r4") 
  1474   case (6 r r' bs rs1 rs2)
 
  1492            prefer 2
 
  1475   have as: "r \<leadsto> r'" by fact
 
  1493   using rrewrite.intros(5) apply blast
 
  1476   have IH: "bder c r \<leadsto>* bder c r'" by fact
 
  1494           apply(rule many_steps_later)
 
  1477   from as IH show "bder c (AALTs bs (rs1 @ [r] @ rs2)) \<leadsto>* bder c (AALTs bs (rs1 @ [r'] @ rs2))" 
  1495            apply(rule alt_rewrite_front)
 
  1478     apply(simp)
 
  1496            apply assumption
 
  1479     using contextrewrites2 by force
 
  1497   apply (meson alt_rewrites_back rewrites_fuse) 
  1480 next
 
  1498 
  1481   case (7 bs rsa rsb)
 
  1499        apply (simp add: r_in_rstar rrewrite.intros(5))
 
  1482   then show "bder c (AALTs bs (rsa @ [AZERO] @ rsb)) \<leadsto>* bder c (AALTs bs (rsa @ rsb))" 
  1500 
  1483     apply(simp)
 
  1501   using contextrewrites2 apply force
 
  1484     using rrewrite.intros(7) by auto
 
  1502 
  1485 next
 
  1503   using rrewrite.intros(7) apply force
 
  1486   case (8 bs rsa bs1 rs1 rsb)
 
  1504   
  1487   then show 
  1505   using rewrite_der_altmiddle apply auto[1]
 
  1488     "bder c (AALTs bs (rsa @ [AALTs bs1 rs1] @ rsb)) \<leadsto>* bder c (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"
 
  1506   
  1489     using rewrite_der_altmiddle by auto 
  1507   apply (metis bder.simps(4) bder_fuse_list map_map r_in_rstar rrewrite.intros(9))
 
  1490 next
 
  1508   apply (simp add: r_in_rstar rrewrite.intros(10))
 
  1491   case (9 bs bs1 rs)
 
  1509 
  1492   then show "bder c (AALTs (bs @ bs1) rs) \<leadsto>* bder c (AALTs bs (map (fuse bs1) rs))"
 
  1510   apply (simp add: r_in_rstar rrewrite.intros(10))
 
  1493     by (metis bder.simps(4) bder_fuse_list list.map_comp r_in_rstar rrewrite.intros(9)) 
  1511   using bder_fuse r_in_rstar rrewrite.intros(11) apply presburger
 
  1494 next
 
  1512 
  1495   case (10 bs)
 
  1513   
  1496   then show "bder c (AALTs bs []) \<leadsto>* bder c AZERO"
 
  1514   using lock_step_der_removal by auto
 
  1497     by (simp add: r_in_rstar rrewrite.intros(10))
 
  1515 
  1498 next
 
       
  1499   case (11 bs r)
 
       
  1500   then show "bder c (AALTs bs [r]) \<leadsto>* bder c (fuse bs r)"
 
       
  1501     by (simp add: bder_fuse r_in_rstar rrewrite.intros(11)) 
       
  1502 next
 
       
  1503   case (12 a1 a2 bs rsa rsb rsc)
 
       
  1504   have as: "erase a1 = erase a2" by fact
 
       
  1505   then show "bder c (AALTs bs (rsa @ [a1] @ rsb @ [a2] @ rsc)) \<leadsto>* bder c (AALTs bs (rsa @ [a1] @ rsb @ rsc))"
 
       
  1506     using lock_step_der_removal by force 
       
  1507 qed
 
  1516 
  1508 
  1517 
  1509 
  1518 lemma rewrites_after_der: 
  1510 lemma rewrites_after_der: 
  1519   assumes "r1 \<leadsto>* r2"
 
  1511   assumes "r1 \<leadsto>* r2"
 
  1520   shows "bder c r1 \<leadsto>* bder c r2"
 
  1512   shows "bder c r1 \<leadsto>* bder c r2"
 
  1521 using assms  
  1513 using assms  
  1522 apply(induction r1 r2 rule: rrewrites.induct)
 
  1514 apply(induction r1 r2 rule: rrewrites.induct)
 
  1523 apply(simp_all add: rewrite_after_der real_trans)
 
  1515 apply(simp_all add: rewrite_after_der real_trans)
 
  1524 done
 
  1516 done
 
       
  1517 
  1525 
  1518 
  1526 lemma central:  
  1519 lemma central:  
  1527   shows "bders r s \<leadsto>* bders_simp r s"
 
  1520   shows "bders r s \<leadsto>* bders_simp r s"
 
  1528 proof(induct s arbitrary: r rule: rev_induct)
 
  1521 proof(induct s arbitrary: r rule: rev_induct)
 
  1529   case Nil
 
  1522   case Nil
 
  1538     by (simp add: bsimp_rewrite)
 
  1531     by (simp add: bsimp_rewrite)
 
  1539   finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])" 
  1532   finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])" 
  1540     by (simp add: bders_simp_append)
 
  1533     by (simp add: bders_simp_append)
 
  1541 qed
 
  1534 qed
 
  1542 
  1535 
  1543 
       
  1544 lemma quasi_main: 
  1536 lemma quasi_main: 
  1545   assumes "bnullable (bders r s)"
 
  1537   assumes "bnullable (bders r s)"
 
  1546   shows "bmkeps (bders r s) = bmkeps (bders_simp r s)"
 
  1538   shows "bmkeps (bders r s) = bmkeps (bders_simp r s)"
 
  1547   using assms central rewrites_bmkeps by blast
 
  1539   using assms central rewrites_bmkeps 
       
  1540 proof -
 
       
  1541   have "bders r s \<leadsto>* bders_simp r s" by (rule central)
 
       
  1542   then 
       
  1543   show "bmkeps (bders r s) = bmkeps (bders_simp r s)" using assms
 
       
  1544     by (rule rewrites_bmkeps)
 
       
  1545 qed  
       
  1546 
  1548 
  1547 
  1549 theorem main_main: 
  1548 theorem main_main: 
  1550   shows "blexer r s = blexer_simp r s"
 
  1549   shows "blexer r s = blexer_simp r s"
 
  1551   by (simp add: b4 blexer_def blexer_simp_def quasi_main)
 
  1550   unfolding blexer_def blexer_simp_def
 
       
  1551   using b4 quasi_main by simp
 
  1552 
  1552 
  1553 
  1553 
  1554 theorem blexersimp_correctness: 
  1554 theorem blexersimp_correctness: 
  1555   shows "lexer r s = blexer_simp r s"
 
  1555   shows "lexer r s = blexer_simp r s"
 
  1556   using blexer_correctness main_main by auto
 
  1556   using blexer_correctness main_main by simp
 
  1557 
  1557 
  1558 
  1558 
  1559 
  1559 
  1560 export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers
 
  1560 export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers
 
  1561 
  1561
lexing