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