lexing: comparison thys2/SizeBound4.thy

equal deleted inserted replaced

-:e1b74d618f1b
+:dac6d27c99c6
 where
 "bders r [] = r"
 | "bders r (c#s) = bders (bder c r) s"
 lemma bders_append:
-"bders r (s1 @ s2) = bders (bders r s1) s2"
+"bders c (s1 @ s2) = bders (bders c s1) s2"
-apply(induct s1 arbitrary: r s2)
+apply(induct s1 arbitrary: c s2)
 apply(simp_all)
 done
 lemma bnullable_correctness:
 shows "nullable (erase r) = bnullable r"
 shows "code (Stars vs) = retrieve (ASTAR [] (intern r)) (Stars vs)"
 using assms
 apply(induct vs)
 apply(simp_all)
 done
 lemma retrieve_fuse2:
 assumes "\<Turnstile> v : (erase r)"
 shows "retrieve (fuse bs r) v = bs @ retrieve r v"
 using assms
 lemma bmkeps_fuse:
 assumes "bnullable r"
 shows "bmkeps (fuse bs r) = bs @ bmkeps r"
-by (metis assms bmkeps_retrieve bnullable_correctness erase_fuse mkeps_nullable retrieve_fuse2)
+using assms
+by (metis bmkeps_retrieve bnullable_correctness erase_fuse mkeps_nullable retrieve_fuse2)
 lemma bmkepss_fuse:
 assumes "bnullables rs"
 shows "bmkepss (map (fuse bs) rs) = bs @ bmkepss rs"
 using assms
 done
 lemma bder_fuse:
 shows "bder c (fuse bs a) = fuse bs  (bder c a)"
 apply(induct a arbitrary: bs c)
 apply(simp_all)
 done
 | bs3: "ASEQ bs1 (AONE bs2) r \<leadsto> fuse (bs1@bs2) r"
 | bs4: "r1 \<leadsto> r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r2 r3"
 | bs5: "r3 \<leadsto> r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r1 r4"
 | bs6: "AALTs bs [] \<leadsto> AZERO"
 | bs7: "AALTs bs [r] \<leadsto> fuse bs r"
-| bs10: "rs1 s\<leadsto> rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto> AALTs bs rs2"
+| bs8: "rs1 s\<leadsto> rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto> AALTs bs rs2"
 | ss1:  "[] s\<leadsto> []"
 | ss2:  "rs1 s\<leadsto> rs2 \<Longrightarrow> (r # rs1) s\<leadsto> (r # rs2)"
 | ss3:  "r1 \<leadsto> r2 \<Longrightarrow> (r1 # rs) s\<leadsto> (r2 # rs)"
 | ss4:  "(AZERO # rs) s\<leadsto> rs"
 | ss5:  "(AALTs bs1 rs1 # rsb) s\<leadsto> ((map (fuse bs1) rs1) @ rsb)"
 lemma r_in_rstar:
 shows "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
 using rrewrites.intros(1) rrewrites.intros(2) by blast
-lemma srewrites_single :
-shows "rs1 s\<leadsto> rs2 \<Longrightarrow> rs1 s\<leadsto>* rs2"
-using rrewrites.intros(1) rrewrites.intros(2) by blast
 lemma rrewrites_trans[trans]:
 assumes a1: "r1 \<leadsto>* r2"  and a2: "r2 \<leadsto>* r3"
 shows "r1 \<leadsto>* r3"
 using a2 a1
 apply(induct r2 r3 arbitrary: r1 rule: rrewrites.induct)
 lemma contextrewrites0:
 "rs1 s\<leadsto>* rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto>* AALTs bs rs2"
 apply(induct rs1 rs2 rule: srewrites.inducts)
 apply simp
-using bs10 r_in_rstar rrewrites_trans by blast
+using bs8 r_in_rstar rrewrites_trans by blast
 lemma contextrewrites1:
 "r \<leadsto>* r' \<Longrightarrow> AALTs bs (r # rs) \<leadsto>* AALTs bs (r' # rs)"
 apply(induct r r' rule: rrewrites.induct)
 apply simp
-using bs10 ss3 by blast
+using bs8 ss3 by blast
 lemma srewrite1:
 shows "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs @ rs1) s\<leadsto> (rs @ rs2)"
 apply(induct rs)
 apply(auto)
 lemma srewrite2:
 shows  "r1 \<leadsto> r2 \<Longrightarrow> True"
 and "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)"
 apply(induct rule: rrewrite_srewrite.inducts)
 apply(auto)
 apply (metis append_Cons append_Nil srewrites1)
 apply(meson srewrites.simps ss3)
 apply (meson srewrites.simps ss4)
 apply (meson srewrites.simps ss5)
 by (metis append_Cons append_Nil srewrites.simps ss6)
 lemma srewrites6:
 assumes "r1 \<leadsto>* r2"
 shows "[r1] s\<leadsto>* [r2]"
 using assms
 apply(induct r1 r2 rule: rrewrites.induct)
 apply(auto)
 by (meson srewrites.simps srewrites_trans ss3)
 lemma srewrites7:
 assumes "rs3 s\<leadsto>* rs4" "r1 \<leadsto>* r2"
 shows "(r1 # rs3) s\<leadsto>* (r2 # rs4)"
 using assms
-by (smt (verit, best) append_Cons append_Nil srewrites1 srewrites3 srewrites6 srewrites_trans)
+by (smt (verit, del_insts) append.simps srewrites1 srewrites3 srewrites6 srewrites_trans)
 lemma ss6_stronger_aux:
 shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ distinctBy rs2 erase (set (map erase rs1)))"
 apply(induct rs2 arbitrary: rs1)
 apply(auto)
 apply (smt (verit, best) append.assoc append.right_neutral append_Cons append_Nil split_list srewrite2(2) srewrites_trans ss6)
 lemma ss6_stronger:
 shows "rs1 s\<leadsto>* distinctBy rs1 erase {}"
 using ss6_stronger_aux[of "[]" _] by auto
 lemma rewrite_preserves_fuse:
 shows "r2 \<leadsto> r3 \<Longrightarrow> fuse bs r2 \<leadsto> fuse bs r3"
-and   "rs2 s\<leadsto> rs3 \<Longrightarrow> map (fuse bs) rs2 s\<leadsto>* map (fuse bs) rs3"
+and   "rs2 s\<leadsto> rs3 \<Longrightarrow> map (fuse bs) rs2 s\<leadsto> map (fuse bs) rs3"
 proof(induct rule: rrewrite_srewrite.inducts)
 case (bs3 bs1 bs2 r)
-then show ?case
+then show "fuse bs (ASEQ bs1 (AONE bs2) r) \<leadsto> fuse bs (fuse (bs1 @ bs2) r)"
 by (metis fuse.simps(5) fuse_append rrewrite_srewrite.bs3)
 next
-case (bs7 bs r)
+case (bs7 bs1 r)
-then show ?case
+then show "fuse bs (AALTs bs1 [r]) \<leadsto> fuse bs (fuse bs1 r)"
 by (metis fuse.simps(4) fuse_append rrewrite_srewrite.bs7)
 next
 case (ss2 rs1 rs2 r)
-then show ?case
+then show "map (fuse bs) (r # rs1) s\<leadsto> map (fuse bs) (r # rs2)"
-using srewrites7 by force
+by (simp add: rrewrite_srewrite.ss2)
 next
 case (ss3 r1 r2 rs)
-then show ?case by (simp add: r_in_rstar srewrites7)
+then show "map (fuse bs) (r1 # rs) s\<leadsto> map (fuse bs) (r2 # rs)"
+by (simp add: rrewrite_srewrite.ss3)
 next
 case (ss5 bs1 rs1 rsb)
-then show ?case
+have "map (fuse bs) (AALTs bs1 rs1 # rsb) = AALTs (bs @ bs1) rs1 # (map (fuse bs) rsb)" by simp
+also have "... s\<leadsto> ((map (fuse (bs @ bs1)) rs1) @ (map (fuse bs) rsb))"
+by (simp add: rrewrite_srewrite.ss5)
+finally show "map (fuse bs) (AALTs bs1 rs1 # rsb) s\<leadsto> map (fuse bs) (map (fuse bs1) rs1 @ rsb)"
+by (simp add: comp_def fuse_append)
+next
+case (ss6 a1 a2 rsa rsb rsc)
+then show "map (fuse bs) (rsa @ [a1] @ rsb @ [a2] @ rsc) s\<leadsto> map (fuse bs) (rsa @ [a1] @ rsb @ rsc)"
 apply(simp)
-by (metis (mono_tags, lifting) comp_def fuse_append map_eq_conv rrewrite_srewrite.ss5 srewrites.simps)
-next
-case (ss6 a1 a2 rsa rsb rsc)
-then show ?case
-apply(simp)
-apply(rule srewrites_single)
 apply(rule rrewrite_srewrite.ss6[simplified])
 apply(simp add: erase_fuse)
 done
 qed (auto intro: rrewrite_srewrite.intros)
 lemma rewrites_fuse:
 assumes "r1 \<leadsto>* r2"
 shows "fuse bs r1 \<leadsto>* fuse bs r2"
 using assms
 apply(induction r1 r2 arbitrary: bs rule: rrewrites.induct)
-apply(auto intro: rewrite_preserves_fuse rrewrites_trans)
+apply(auto intro: rewrite_preserves_fuse)
 done
 lemma star_seq:
 assumes "r1 \<leadsto>* r2"
 lemma bsimp_AALTs_rewrites:
 shows "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs"
 by (smt (verit) bs6 bs7 bsimp_AALTs.elims rrewrites.simps)
 lemma trivialbsimp_srewrites:
-"\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs s\<leadsto>* (map f rs)"
+assumes "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x"
+shows "rs s\<leadsto>* (map f rs)"
+using assms
 apply(induction rs)
-apply simp
+apply(simp_all add: srewrites7)
-apply(simp)
+done
-using srewrites7 by auto
 lemma fltsfrewrites: "rs s\<leadsto>* flts rs"
 apply(induction rs rule: flts.induct)
 apply(auto intro: rrewrite_srewrite.intros)
 apply (meson srewrites.simps srewrites1 ss5)
 qed (simp_all)
 lemma to_zero_in_alt:
 shows "AALT bs (ASEQ [] AZERO r) r2 \<leadsto> AALT bs AZERO r2"
-by (simp add: bs1 bs10 ss3)
+by (simp add: bs1 bs8 ss3)
 lemma  bder_fuse_list:
 shows "map (bder c \<circ> fuse bs1) rs1 = map (fuse bs1 \<circ> bder c) rs1"
 apply(induction rs1)
 apply(simp_all add: bder_fuse)
 done
 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)
 by (simp add: r_in_rstar rrewrite_srewrite.bs2)
 next
 case (bs3 bs1 bs2 r)
 show "bder c (ASEQ bs1 (AONE bs2) r) \<leadsto>* bder c (fuse (bs1 @ bs2) r)"
 apply(simp)
-by (metis (no_types, lifting) bder_fuse bs10 bs7 fuse_append rrewrites.simps ss4 to_zero_in_alt)
+by (metis (no_types, lifting) bder_fuse bs8 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)"
 next
 case (bs7 bs r)
 show "bder c (AALTs bs [r]) \<leadsto>* bder c (fuse bs r)"
 by (simp add: bder_fuse r_in_rstar rrewrite_srewrite.bs7)
 next
-case (bs10 rs1 rs2 bs)
+case (bs8 rs1 rs2 bs)
 have IH1: "map (bder c) rs1 s\<leadsto>* map (bder c) rs2" by fact
 then show "bder c (AALTs bs rs1) \<leadsto>* bder c (AALTs bs rs2)"
 using contextrewrites0 by force
 next
 case ss1
 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 rewrites_bnullable_eq)
 shows "lexer r s = blexer_simp r s"
 using blexer_correctness main_blexer_simp by simp
+lemma asize_idem:
+shows "asize (bsimp (bsimp r)) = asize (bsimp r)"
+apply(induct r rule: bsimp.induct)
+apply(auto)
+prefer 2
+oops
 export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers
 unused_thms

changeset 398	dac6d27c99c6
parent 397	e1b74d618f1b
child 400	46e5566ad4ba