diff -r 8194086c2a8a -r 3954579ebdaf thys2/SizeBound2.thy --- a/thys2/SizeBound2.thy Thu Jan 20 01:48:18 2022 +0000 +++ b/thys2/SizeBound2.thy Sat Jan 22 10:48:09 2022 +0000 @@ -183,6 +183,11 @@ | "bmkeps(AALTs bs (r#rs)) = (if bnullable(r) then bs @ (bmkeps r) else (bmkeps (AALTs bs rs)))" | "bmkeps(ASTAR bs r) = bs @ [S]" +fun + bmkepss :: "arexp list \ bit list" +where + "bmkepss [] = []" +| "bmkepss (r # rs) = (if bnullable(r) then (bmkeps r) else (bmkepss rs))" fun bder :: "char \ arexp \ arexp" @@ -539,9 +544,7 @@ (if (f x) \ acc then distinctBy xs f acc else x # (distinctBy xs f ({f x} \ acc)))" -lemma dB_single_step: - shows "distinctBy (a#rs) f {} = a # distinctBy rs f {f a}" - by simp + fun flts :: "arexp list \ arexp list" where @@ -559,6 +562,22 @@ | "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2" | "bsimp_ASEQ bs1 r1 r2 = ASEQ bs1 r1 r2" +lemma bsimp_ASEQ0[simp]: + shows "bsimp_ASEQ bs r1 AZERO = AZERO" + by (case_tac r1)(simp_all) + +lemma bsimp_ASEQ1: + assumes "r1 \ AZERO" "r2 \ AZERO" "\bs. r1 = AONE bs" + shows "bsimp_ASEQ bs r1 r2 = ASEQ bs r1 r2" + using assms + apply(induct bs r1 r2 rule: bsimp_ASEQ.induct) + apply(auto) + done + +lemma bsimp_ASEQ2[simp]: + shows "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2" + by (case_tac r2) (simp_all) + fun bsimp_AALTs :: "bit list \ arexp list \ arexp" where @@ -584,7 +603,7 @@ "blexer_simp r s \ if bnullable (bders_simp (intern r) s) then decode (bmkeps (bders_simp (intern r) s)) r else None" -export_code bders_simp in Scala module_name Example +(*export_code bders_simp in Scala module_name Example*) lemma bders_simp_append: shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2" @@ -657,25 +676,7 @@ -lemma bsimp_ASEQ0: - shows "bsimp_ASEQ bs r1 AZERO = AZERO" - apply(induct r1) - apply(auto) - done -lemma bsimp_ASEQ1: - assumes "r1 \ AZERO" "r2 \ AZERO" "\bs. r1 \ AONE bs" - shows "bsimp_ASEQ bs r1 r2 = ASEQ bs r1 r2" - using assms - apply(induct bs r1 r2 rule: bsimp_ASEQ.induct) - apply(auto) - done - -lemma bsimp_ASEQ2: - shows "bsimp_ASEQ bs (AONE bs1) r2 = fuse (bs @ bs1) r2" - apply(induct r2) - apply(auto) - done lemma L_bders_simp: @@ -849,6 +850,7 @@ | ss5: "(AALTs bs1 rs1 # rsb) s\ ((map (fuse bs1) rs1) @ rsb)" | ss6: "erase a1 = erase a2 \ (rsa@[a1]@rsb@[a2]@rsc) s\ (rsa@[a1]@rsb@rsc)" + inductive rrewrites:: "arexp \ arexp \ bool" ("_ \* _" [100, 100] 100) where @@ -882,14 +884,6 @@ done -lemma rewrite_fuse : - assumes "r1 \ r2" - shows "fuse bs r1 \ fuse bs r2" - using assms - apply(induct rule: rrewrite_srewrite.inducts(1)) - apply(auto intro: rrewrite_srewrite.intros) - apply (metis bs3 fuse_append) - by (metis bs7 fuse_append) lemma contextrewrites0: "rs1 s\* rs2 \ AALTs bs rs1 \* AALTs bs rs2" @@ -947,7 +941,6 @@ assumes "r1 \* r2" shows "[r1] s\* [r2]" using assms - apply(induct r1 r2 rule: rrewrites.induct) apply(auto) by (meson srewrites.simps srewrites_trans ss3) @@ -958,6 +951,58 @@ using assms by (smt (verit, best) append_Cons append_Nil srewrites1 srewrites3 srewrites6 srewrites_trans) +lemma ss6_stronger_aux: + shows "(rs1 @ rs2) s\* (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) + apply(drule_tac x="rs1 @ [a]" in meta_spec) + apply(simp) + done + +lemma ss6_stronger: + shows "rs1 s\* distinctBy rs1 erase {}" + using ss6_stronger_aux[of "[]" _] by auto + + +lemma rewrite_preserves_fuse: + shows "r2 \ r3 \ fuse bs r2 \ fuse bs r3" + and "rs2 s\ rs3 \ map (fuse bs) rs2 s\* map (fuse bs) rs3" +proof(induct rule: rrewrite_srewrite.inducts) + case (bs3 bs1 bs2 r) + then show ?case + by (metis fuse.simps(5) fuse_append rrewrite_srewrite.bs3) +next + case (bs7 bs r) + then show ?case + by (metis fuse.simps(4) fuse_append rrewrite_srewrite.bs7) +next + case (ss2 rs1 rs2 r) + then show ?case + using srewrites7 by force +next + case (ss3 r1 r2 rs) + then show ?case by (simp add: r_in_rstar srewrites7) +next + case (ss5 bs1 rs1 rsb) + then show ?case + 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 only: map_append) + by (smt (verit, ccfv_threshold) erase_fuse list.simps(8) list.simps(9) rrewrite_srewrite.ss6 srewrites.simps) +qed (auto intro: rrewrite_srewrite.intros) + + +lemma rewrites_fuse: + assumes "r1 \* r2" + shows "fuse bs r1 \* fuse bs r2" +using assms +apply(induction r1 r2 arbitrary: bs rule: rrewrites.induct) +apply(auto intro: rewrite_preserves_fuse rrewrites_trans) +done lemma star_seq: @@ -981,6 +1026,12 @@ shows "ASEQ bs1 r1 r2 \* AZERO" using assms bs1 star_seq by blast +(* +lemma continuous_rewrite2: + assumes "r1 \* AONE bs" + shows "ASEQ bs1 r1 r2 \* (fuse (bs1 @ bs) r2)" + using assms by (meson bs3 rrewrites.simps star_seq) +*) lemma bsimp_aalts_simpcases: shows "AONE bs \* bsimp (AONE bs)" @@ -988,6 +1039,9 @@ and "ACHAR bs c \* bsimp (ACHAR bs c)" by (simp_all) +lemma bsimp_AALTs_rewrites: + shows "AALTs bs1 rs \* bsimp_AALTs bs1 rs" + by (smt (verit) bs6 bs7 bsimp_AALTs.elims rrewrites.simps) lemma trivialbsimp_srewrites: "\\x. x \ set rs \ x \* f x \ \ rs s\* (map f rs)" @@ -996,129 +1050,17 @@ apply(simp) using srewrites7 by auto -lemma alts_simpalts: - "(\x. x \ set rs \ x \* bsimp x) \ - AALTs bs1 rs \* AALTs bs1 (map bsimp rs)" - apply(induct rs) - apply(auto)[1] - using trivialbsimp_srewrites apply auto[1] - by (simp add: contextrewrites0 srewrites7) - - -lemma bsimp_AALTs_rewrites: - shows "AALTs bs1 rs \* bsimp_AALTs bs1 rs" - by (smt (verit) bs6 bs7 bsimp_AALTs.elims rrewrites.simps) - -lemma fltsfrewrites: "rs s\* (flts rs)" - - apply(induction rs) - apply simp - apply(case_tac a) - apply(auto) - using ss4 apply blast - using srewrites7 apply force - using rs1 srewrites7 apply presburger - using srewrites7 apply force - apply (meson srewrites.simps srewrites1 ss5) - by (simp add: srewrites7) - - -lemma flts_rewrites: "AALTs bs1 rs \* AALTs bs1 (flts rs)" - by (simp add: contextrewrites0 fltsfrewrites) -(* delete*) -lemma threelistsappend: "rsa@a#rsb = (rsa@[a])@rsb" - apply auto - done - -lemma somewhereInside: "r \ set rs \ \rs1 rs2. rs = rs1@[r]@rs2" - using split_list by fastforce - -lemma somewhereMapInside: "f r \ f ` set rs \ \rs1 rs2 a. rs = rs1@[a]@rs2 \ f a = f r" - apply auto - by (metis split_list) - -lemma alts_dBrewrites_withFront: - "AALTs bs (rsa @ rs) \* AALTs bs (rsa @ distinctBy rs erase (erase ` set rsa))" - - apply(induction rs arbitrary: rsa) - apply simp - - apply(drule_tac x = "rsa@[a]" in meta_spec) - - apply(subst threelistsappend) - apply(rule rrewrites_trans) - apply simp - - apply(case_tac "a \ set rsa") - apply simp - apply(drule somewhereInside) - apply(erule exE)+ - apply simp - using bs10 ss6 apply auto[1] - - apply(subgoal_tac "erase ` set (rsa @ [a]) = insert (erase a) (erase ` set rsa)") - prefer 2 - - apply auto[1] - apply(case_tac "erase a \ erase `set rsa") - - apply simp - apply(subgoal_tac "AALTs bs (rsa @ a # distinctBy rs erase (insert (erase a) (erase ` set rsa))) \ - AALTs bs (rsa @ distinctBy rs erase (insert (erase a) (erase ` set rsa)))") - apply force - apply (smt (verit, ccfv_threshold) append.assoc append.left_neutral append_Cons append_Nil bs10 imageE insertCI insert_image somewhereMapInside ss6) - by simp - - +lemma fltsfrewrites: "rs s\* (flts rs)" + apply(induction rs rule: flts.induct) + apply(auto intro: rrewrite_srewrite.intros) + apply (meson srewrites.simps srewrites1 ss5) + using rs1 srewrites7 apply presburger + using srewrites7 apply force + apply (simp add: srewrites7) + by (simp add: srewrites7) -lemma alts_dBrewrites: - shows "AALTs bs rs \* AALTs bs (distinctBy rs erase {})" - - apply(induction rs) - apply simp - apply simp - using alts_dBrewrites_withFront - by (metis append_Nil dB_single_step empty_set image_empty) - -lemma bsimp_rewrite: - shows "r \* bsimp r" -proof (induction r rule: bsimp.induct) - case (1 bs1 r1 r2) - then show "ASEQ bs1 r1 r2 \* bsimp (ASEQ bs1 r1 r2)" - apply(simp) - apply(case_tac "bsimp r1 = AZERO") - apply simp - using continuous_rewrite apply blast - apply(case_tac "\bs. bsimp r1 = AONE bs") - apply(erule exE) - apply simp - apply(subst bsimp_ASEQ2) - apply (meson rrewrites_trans rrewrite_srewrite.intros(3) rrewrites.intros(2) star_seq star_seq2) - apply (smt (verit, best) bsimp_ASEQ0 bsimp_ASEQ1 rrewrites_trans rrewrite_srewrite.intros(2) rs2 star_seq star_seq2) - done -next - case (2 bs1 rs) - then show "AALTs bs1 rs \* bsimp (AALTs bs1 rs)" - by (metis alts_dBrewrites alts_simpalts bsimp.simps(2) bsimp_AALTs_rewrites flts_rewrites rrewrites_trans) -next - case "3_1" - then show "AZERO \* bsimp AZERO" - by simp -next - case ("3_2" v) - then show "AONE v \* bsimp (AONE v)" - by simp -next - case ("3_3" v va) - then show "ACHAR v va \* bsimp (ACHAR v va)" - by simp -next - case ("3_4" v va) - then show "ASTAR v va \* bsimp (ASTAR v va)" - by simp -qed lemma bnullable1: shows "r1 \ r2 \ (bnullable r1 \ bnullable r2)" @@ -1154,7 +1096,7 @@ lemma rewritesnullable: assumes "r1 \* r2" "bnullable r1" shows "bnullable r2" -using assms +using assms apply(induction r1 r2 rule: rrewrites.induct) apply simp using rewrite_non_nullable_strong by blast @@ -1240,50 +1182,70 @@ then show "bmkeps r1 = bmkeps r3" using IH by simp qed + +lemma rewrites_to_bsimp: + shows "r \* bsimp r" +proof (induction r rule: bsimp.induct) + case (1 bs1 r1 r2) + have IH1: "r1 \* bsimp r1" by fact + have IH2: "r2 \* bsimp r2" by fact + { assume as: "bsimp r1 = AZERO \ bsimp r2 = AZERO" + with IH1 IH2 have "r1 \* AZERO \ r2 \* AZERO" by auto + then have "ASEQ bs1 r1 r2 \* AZERO" + by (metis bs2 continuous_rewrite rrewrites.simps star_seq2) + then have "ASEQ bs1 r1 r2 \* bsimp (ASEQ bs1 r1 r2)" using as by auto + } + moreover + { assume "\bs. bsimp r1 = AONE bs" + then obtain bs where as: "bsimp r1 = AONE bs" by blast + with IH1 have "r1 \* AONE bs" by simp + then have "ASEQ bs1 r1 r2 \* fuse (bs1 @ bs) r2" using bs3 star_seq by blast + with IH2 have "ASEQ bs1 r1 r2 \* fuse (bs1 @ bs) (bsimp r2)" + using rewrites_fuse by (meson rrewrites_trans) + then have "ASEQ bs1 r1 r2 \* bsimp (ASEQ bs1 (AONE bs) r2)" by simp + then have "ASEQ bs1 r1 r2 \* bsimp (ASEQ bs1 r1 r2)" by (simp add: as) + } + moreover + { assume as1: "bsimp r1 \ AZERO" "bsimp r2 \ AZERO" and as2: "(\bs. bsimp r1 = AONE bs)" + then have "bsimp_ASEQ bs1 (bsimp r1) (bsimp r2) = ASEQ bs1 (bsimp r1) (bsimp r2)" + by (simp add: bsimp_ASEQ1) + then have "ASEQ bs1 r1 r2 \* bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)" using as1 as2 IH1 IH2 + by (metis rrewrites_trans star_seq star_seq2) + then have "ASEQ bs1 r1 r2 \* bsimp (ASEQ bs1 r1 r2)" by simp + } + ultimately show "ASEQ bs1 r1 r2 \* bsimp (ASEQ bs1 r1 r2)" by blast +next + case (2 bs1 rs) + have IH: "\x. x \ set rs \ x \* bsimp x" by fact + then have "rs s\* (map bsimp rs)" by (simp add: trivialbsimp_srewrites) + also have "... s\* flts (map bsimp rs)" by (simp add: fltsfrewrites) + also have "... s\* distinctBy (flts (map bsimp rs)) erase {}" by (simp add: ss6_stronger) + finally have "AALTs bs1 rs \* AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {})" + using contextrewrites0 by blast + also have "... \* bsimp_AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {})" + by (simp add: bsimp_AALTs_rewrites) + finally show "AALTs bs1 rs \* bsimp (AALTs bs1 rs)" by simp +next + case "3_1" + then show "AZERO \* bsimp AZERO" by simp +next + case ("3_2" v) + then show "AONE v \* bsimp (AONE v)" by simp +next + case ("3_3" v va) + then show "ACHAR v va \* bsimp (ACHAR v va)" by simp +next + case ("3_4" v va) + then show "ASTAR v va \* bsimp (ASTAR v va)" by simp +qed + + + lemma to_zero_in_alt: - shows "AALT bs (ASEQ [] AZERO r) r2 \ AALT bs AZERO r2" + shows "AALT bs (ASEQ [] AZERO r) r2 \ AALT bs AZERO r2" by (simp add: bs1 bs10 ss3) -lemma rewrite_fuse2: - shows "r2 \ r3 \ True" - and "rs2 s\ rs3 \ (\bs. map (fuse bs) rs2 s\* map (fuse bs) rs3)" -proof(induct rule: rrewrite_srewrite.inducts) - case ss1 - then show ?case - by simp -next - case (ss2 rs1 rs2 r) - then show ?case - using srewrites7 by force -next - case (ss3 r1 r2 rs) - then show ?case - by (simp add: r_in_rstar rewrite_fuse srewrites7) -next - case (ss4 rs) - then show ?case - by (metis fuse.simps(1) list.simps(9) rrewrite_srewrite.ss4 srewrites.simps) -next - case (ss5 bs1 rs1 rsb) - then show ?case - 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 only: map_append) - by (smt (verit, ccfv_threshold) erase_fuse list.simps(8) list.simps(9) rrewrite_srewrite.ss6 srewrites.simps) -qed (auto) - - -lemma rewrites_fuse: - assumes "r1 \* r2" - shows "fuse bs r1 \* fuse bs r2" -using assms -apply(induction r1 r2 arbitrary: bs rule: rrewrites.induct) -apply(auto intro: rewrite_fuse rrewrites_trans) -done lemma bder_fuse_list: shows "map (bder c \ fuse bs1) rs1 = map (fuse bs1 \ bder c) rs1" @@ -1292,7 +1254,7 @@ done -lemma rewrite_after_der: +lemma rewrite_preserves_bder: shows "r1 \ r2 \ (bder c r1) \* (bder c r2)" and "rs1 s\ rs2 \ map (bder c) rs1 s\* map (bder c) rs2" proof(induction rule: rrewrite_srewrite.inducts) @@ -1309,6 +1271,7 @@ 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) @@ -1364,12 +1327,12 @@ by (smt (verit, best) erase_bder list.simps(8) list.simps(9) local.ss6 rrewrite_srewrite.ss6 srewrites.simps) qed -lemma rewrites_after_der: +lemma rewrites_preserves_bder: assumes "r1 \* r2" shows "bder c r1 \* bder c r2" using assms apply(induction r1 r2 rule: rrewrites.induct) -apply(simp_all add: rewrite_after_der rrewrites_trans) +apply(simp_all add: rewrite_preserves_bder rrewrites_trans) done @@ -1383,18 +1346,14 @@ have IH: "\r. bders r xs \* bders_simp r xs" by fact have "bders r (xs @ [x]) = bders (bders r xs) [x]" by (simp add: bders_append) also have "... \* bders (bders_simp r xs) [x]" using IH - by (simp add: rewrites_after_der) + by (simp add: rewrites_preserves_bder) also have "... \* bders_simp (bders_simp r xs) [x]" using IH - by (simp add: bsimp_rewrite) + by (simp add: rewrites_to_bsimp) finally show "bders r (xs @ [x]) \* bders_simp r (xs @ [x])" by (simp add: bders_simp_append) qed - - - - -lemma quasi_main: +lemma main_aux: assumes "bnullable (bders r s)" shows "bmkeps (bders r s) = bmkeps (bders_simp r s)" proof - @@ -1407,15 +1366,15 @@ -theorem main_main: +theorem main_blexer_simp: shows "blexer r s = blexer_simp r s" unfolding blexer_def blexer_simp_def - using b4 quasi_main by simp + using b4 main_aux by simp theorem blexersimp_correctness: shows "lexer r s = blexer_simp r s" - using blexer_correctness main_main by simp + using blexer_correctness main_blexer_simp by simp