diff -r feae84f66472 -r e5db23c100ea thys3/BlexerSimp.thy
--- a/thys3/BlexerSimp.thy	Thu Jun 23 18:32:14 2022 +0100
+++ b/thys3/BlexerSimp.thy	Thu Jun 23 18:50:59 2022 +0100
@@ -98,6 +98,8 @@
   apply(simp_all)
   done
 
+
+
 lemma bmkeps_fuse:
   assumes "bnullable r"
   shows "bmkeps (fuse bs r) = bs @ bmkeps r"
@@ -371,7 +373,9 @@
   apply(induct rule: rrewrite_srewrite.inducts)
   apply(auto simp add:  bnullable_fuse)
    apply (meson UnCI bnullable_fuse imageI)
-  using bnullable_correctness nullable_correctness by blast 
+  using bnullable_correctness nullable_correctness by blast
+
+
 
 
 lemma rewritesnullable: 
@@ -569,49 +573,7 @@
 using assms  
 apply(induction r1 r2 rule: rrewrites.induct)
 apply(simp_all add: rewrite_preserves_bder rrewrites_trans)
-done
-
-
-
-lemma central:  
-  shows "bders r s \<leadsto>* bders_simp r s"
-proof(induct s arbitrary: r rule: rev_induct)
-  case Nil
-  then show "bders r [] \<leadsto>* bders_simp r []" by simp
-next
-  case (snoc x xs)
-  have IH: "\<And>r. bders r xs \<leadsto>* bders_simp r xs" by fact
-  have "bders r (xs @ [x]) = bders (bders r xs) [x]" by (simp add: bders_append)
-  also have "... \<leadsto>* bders (bders_simp r xs) [x]" using IH
-    by (simp add: rewrites_preserves_bder)
-  also have "... \<leadsto>* bders_simp (bders_simp r xs) [x]" using IH
-    by (simp add: rewrites_to_bsimp)
-  finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])" 
-    by (simp add: bders_simp_append)
-qed
-
-lemma main_aux: 
-  assumes "bnullable (bders r s)"
-  shows "bmkeps (bders r s) = bmkeps (bders_simp r s)"
-proof -
-  have "bders r s \<leadsto>* bders_simp r s" by (rule central)
-  then 
-  show "bmkeps (bders r s) = bmkeps (bders_simp r s)" using assms
-    by (rule rewrites_bmkeps)
-qed  
-
-
-
-
-theorem main_blexer_simp: 
-  shows "blexer r s = blexer_simp r s"
-  unfolding blexer_def blexer_simp_def
-  by (metis central main_aux rewritesnullable)
-
-theorem blexersimp_correctness: 
-  shows "lexer r s = blexer_simp r s"
-  using blexer_correctness main_blexer_simp by simp
-
+  done
 
 
 
@@ -678,84 +640,14 @@
                     decode (bmkeps (bdersStrong6 (intern r) s)) r else None"
 
 
-(*
-lemma rewrite_preserves_bder: 
-  shows "r1 \<leadsto> r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)"
-  and   "rs1 s\<leadsto> rs2 \<Longrightarrow> map (bder c) rs1 s\<leadsto>* map (bder c) rs2"
-proof(induction rule: rrewrite_srewrite.inducts)
-  case (bs1 bs r2)
-  then show ?case
-    by (simp add: continuous_rewrite) 
-next
-  case (bs2 bs r1)
-  then show ?case 
-    apply(auto)
-    apply (meson bs6 contextrewrites0 rrewrite_srewrite.bs2 rs2 ss3 ss4 sss1 sss2)
-    by (simp add: r_in_rstar rrewrite_srewrite.bs2)
-next
-  case (bs3 bs1 bs2 r)
-  then show ?case 
-    apply(simp)
-    
-    by (metis (no_types, lifting) bder_fuse bs10 bs7 fuse_append rrewrites.simps ss4 to_zero_in_alt)
-next
-  case (bs4 r1 r2 bs r3)
-  have as: "r1 \<leadsto> r2" by fact
-  have IH: "bder c r1 \<leadsto>* bder c r2" by fact
-  from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r2 r3)"
-    by (metis bder.simps(5) bnullable0(1) contextrewrites1 rewrite_bmkeps_aux(1) star_seq)
-next
-  case (bs5 r3 r4 bs r1)
-  have as: "r3 \<leadsto> r4" by fact 
-  have IH: "bder c r3 \<leadsto>* bder c r4" by fact 
-  from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r1 r4)"
-    apply(simp)
-    apply(auto)
-    using contextrewrites0 r_in_rstar rewrites_fuse srewrites6 srewrites7 star_seq2 apply presburger
-    using star_seq2 by blast
-next
-  case (bs6 bs)
-  then show ?case
-    using rrewrite_srewrite.bs6 by force 
-next
-  case (bs7 bs r)
-  then show ?case
-    by (simp add: bder_fuse r_in_rstar rrewrite_srewrite.bs7) 
-next
-  case (bs10 rs1 rs2 bs)
-  then show ?case
-    using contextrewrites0 by force    
-next
-  case ss1
-  then show ?case by simp
-next
-  case (ss2 rs1 rs2 r)
-  then show ?case
-    by (simp add: srewrites7) 
-next
-  case (ss3 r1 r2 rs)
-  then show ?case
-    by (simp add: srewrites7) 
-next
-  case (ss4 rs)
-  then show ?case
-    using rrewrite_srewrite.ss4 by fastforce 
-next
-  case (ss5 bs1 rs1 rsb)
-  then show ?case 
-    apply(simp)
-    using bder_fuse_list map_map rrewrite_srewrite.ss5 srewrites.simps by blast
-next
-  case (ss6 a1 a2 bs rsa rsb)
-  then show ?case
-    apply(simp only: map_append map1)
-    apply(rule srewrites_trans)
-    apply(rule rs_in_rstar)
-    apply(rule_tac rrewrite_srewrite.ss6)
-    using Der_def der_correctness apply auto[1]
-    by blast
-qed
-*)
+lemma bders_simp_appendStrong :
+  shows "bdersStrong6 r (s1 @ s2) = bdersStrong6 (bdersStrong6 r s1) s2"
+  apply(induct s1 arbitrary: s2 rule: rev_induct)
+   apply simp
+  apply auto
+  done
+
+
 
 
 lemma rewrites_to_bsimpStrong: 
@@ -802,12 +694,7 @@
   finally show "AALTs bs1 rs \<leadsto>* bsimpStrong6 (AALTs bs1 rs)" sorry
 qed (simp_all)
 
-lemma bders_simp_appendStrong :
-  shows "bdersStrong6 r (s1 @ s2) = bdersStrong6 (bdersStrong6 r s1) s2"
-  apply(induct s1 arbitrary: s2 rule: rev_induct)
-   apply simp
-  apply auto
-  done
+
 
 
 lemma centralStrong:  
@@ -831,20 +718,20 @@
   assumes "bnullable (bders r s)"
   shows "bmkeps (bders r s) = bmkeps (bdersStrong6 r s)"
 proof -
-  have "bders_simp r s \<leadsto>* bdersStrong6 r s" sorry
+  have "bders r s \<leadsto>* bdersStrong6 r s" 
+    using centralStrong by force
   then 
   show "bmkeps (bders r s) = bmkeps (bdersStrong6 r s)" 
-
-  sorry
+    using assms rewrites_bmkeps by blast
 qed
 
 
 
 
 theorem blexerStrong_correct :
-  shows "blexerStrong r s = blexer_simp r s"
-  
-  sorry
+  shows "blexerStrong r s = blexer r s"
+  unfolding blexerStrong_def blexer_def
+  by (metis centralStrong mainStrong rewritesnullable)