# HG changeset patch # User Chengsong # Date 1650549531 -3600 # Node ID 1481f465e6ead6d5235a628690ace7b27b22ccc6 # Parent 61eff2abb0b640bfa3282362066ff00afa369ad7 done diff -r 61eff2abb0b6 -r 1481f465e6ea thys2/SizeBound3.thy --- a/thys2/SizeBound3.thy Tue Apr 19 09:08:01 2022 +0100 +++ b/thys2/SizeBound3.thy Thu Apr 21 14:58:51 2022 +0100 @@ -117,6 +117,16 @@ | "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)" | "erase (ASTAR _ r) = STAR (erase r)" +fun rerase :: "arexp \ rrexp" +where + "rerase AZERO = RZERO" +| "rerase (AONE _) = RONE" +| "rerase (ACHAR _ c) = RCHAR c" +| "rerase (AALTs bs rs) = RALTS (map rerase rs)" +| "rerase (ASEQ _ r1 r2) = RSEQ (rerase r1) (rerase r2)" +| "rerase (ASTAR _ r) = RSTAR (rerase r)" + + fun fuse :: "bit list \ arexp \ arexp" where "fuse bs AZERO = AZERO" @@ -236,12 +246,28 @@ apply(simp_all) done +lemma rbnullable_correctness: + shows "rnullable (rerase r) = bnullable r" + apply(induct r rule: rerase.induct) + apply simp+ + done + + lemma erase_fuse: shows "erase (fuse bs r) = erase r" apply(induct r rule: erase.induct) apply(simp_all) done +lemma rerase_fuse: + shows "rerase (fuse bs r) = rerase r" + apply(induct r) + apply simp+ + done + + + + lemma erase_intern [simp]: shows "erase (intern r) = r" apply(induct r) @@ -254,6 +280,10 @@ apply(simp_all add: erase_fuse bnullable_correctness) done + + + + lemma erase_bders [simp]: shows "erase (bders r s) = ders s (erase r)" apply(induct s arbitrary: r ) @@ -376,7 +406,8 @@ apply (metis (no_types, lifting) bmkepss.cases bnullable_correctness empty_iff erase.simps(6) list.set(1) mkeps.simps(3) retrieve.simps(4)) apply (metis r3) done - + + lemma bmkeps_retrieve: assumes "bnullable r" shows "bmkeps r = retrieve r (mkeps (erase r))" @@ -556,10 +587,12 @@ | "bsimp_AALTs bs1 rs = AALTs bs1 rs" + + fun bsimp :: "arexp \ arexp" where "bsimp (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)" -| "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {}) " +| "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (distinctBy (flts (map bsimp rs)) rerase {}) " | "bsimp r = r" @@ -587,12 +620,31 @@ apply(simp_all) by (metis erase_fuse fuse.simps(4)) +lemma RL_bsimp_ASEQ: + "RL (rerase (ASEQ bs r1 r2)) = RL (rerase (bsimp_ASEQ bs r1 r2))" + apply(induct bs r1 r2 rule: bsimp_ASEQ.induct) + apply simp+ + done + lemma L_bsimp_AALTs: "L (erase (AALTs bs rs)) = L (erase (bsimp_AALTs bs rs))" apply(induct bs rs rule: bsimp_AALTs.induct) apply(simp_all add: erase_fuse) done +lemma RL_bsimp_AALTs: + "RL (rerase (AALTs bs rs)) = RL (rerase (bsimp_AALTs bs rs))" + apply(induct bs rs rule: bsimp_AALTs.induct) + apply(simp_all add: rerase_fuse) + done + +lemma RL_rerase_AALTs: + shows "RL (rerase (AALTs bs rs)) = \ (RL ` rerase ` (set rs))" + apply(induct rs) + apply(simp) + apply(simp) + done + lemma L_erase_AALTs: shows "L (erase (AALTs bs rs)) = \ (L ` erase ` (set rs))" apply(induct rs) @@ -603,6 +655,8 @@ apply(simp) done + + lemma L_erase_flts: shows "\ (L ` erase ` (set (flts rs))) = \ (L ` erase ` (set rs))" apply(induct rs rule: flts.induct) @@ -611,6 +665,19 @@ using L_erase_AALTs erase_fuse apply auto[1] by (simp add: L_erase_AALTs erase_fuse) + +lemma RL_erase_flts: + shows "\ (RL ` rerase ` (set (flts rs))) = + \ (RL ` rerase ` (set rs))" + apply(induct rs rule: flts.induct) + apply simp+ + apply auto + apply (smt (verit) fuse.elims rerase.simps(2) rerase.simps(3) rerase.simps(4) rerase.simps(5) rerase.simps(6)) + by (smt (verit, best) fuse.elims rerase.simps(2) rerase.simps(3) rerase.simps(4) rerase.simps(5) rerase.simps(6)) + + + + lemma L_erase_dB_acc: shows "(\ (L ` acc) \ (\ (L ` erase ` (set (distinctBy rs erase acc))))) = \ (L ` acc) \ \ (L ` erase ` (set rs))" @@ -618,11 +685,25 @@ apply simp_all by (smt (z3) SUP_absorb UN_insert sup_assoc sup_commute) +lemma RL_rerase_dB_acc: + shows "(\ (RL ` acc) \ (\ (RL ` rerase ` (set (distinctBy rs rerase acc))))) + = \ (RL ` acc) \ \ (RL ` rerase ` (set rs))" + apply(induction rs arbitrary: acc) + apply simp_all + by (smt (z3) SUP_absorb UN_insert sup_assoc sup_commute) + + + lemma L_erase_dB: shows "(\ (L ` erase ` (set (distinctBy rs erase {})))) = \ (L ` erase ` (set rs))" by (metis L_erase_dB_acc Un_commute Union_image_empty) +lemma RL_rerase_dB: + shows "(\ (RL ` rerase ` (set (distinctBy rs rerase {})))) = \ (RL ` rerase ` (set rs))" + by (metis RL_rerase_dB_acc Un_commute Union_image_empty) + +(* lemma L_bsimp_erase: shows "L (erase r) = L (erase (bsimp r))" apply(induct r) @@ -643,16 +724,81 @@ apply(subst L_erase_flts) apply (simp add: L_erase_AALTs) done +*) -lemma L_bders_simp: - shows "L (erase (bders_simp r s)) = L (erase (bders r s))" +lemma RL_bsimp_rerase: + shows "RL (rerase r) = RL (rerase (bsimp r))" + apply(induct r) + apply(simp) + apply(simp) + apply(simp) + apply(auto simp add: Sequ_def)[1] + apply(subst RL_bsimp_ASEQ[symmetric]) + apply(auto simp add: Sequ_def)[1] + apply(subst (asm) RL_bsimp_ASEQ[symmetric]) + apply(auto simp add: Sequ_def)[1] + apply(simp) + apply(subst RL_bsimp_AALTs[symmetric]) + defer + apply(simp) + using RL_erase_flts RL_rerase_dB by force + +lemma rder_correctness: + shows "RL (rder c r) = Der c (RL r)" + by (simp add: RL_rder) + + + + +lemma asize_rsize: + shows "rsize (rerase r) = asize r" + apply(induct r) + apply simp+ + + apply (metis (mono_tags, lifting) comp_apply map_eq_conv) + by simp + +lemma rb_nullability: + shows " rnullable (rerase a) = bnullable a" + apply(induct a) + apply simp+ + done + +lemma fuse_anything_doesnt_matter: + shows "rerase a = rerase (fuse bs a)" + by (smt (verit) fuse.elims rerase.simps(2) rerase.simps(3) rerase.simps(4) rerase.simps(5) rerase.simps(6)) + + + +lemma rder_bder_rerase: + shows "rder c (rerase r ) = rerase (bder c r)" + apply (induct r) + apply simp+ + apply(case_tac "bnullable r1") + apply simp + apply (simp add: rb_nullability rerase_fuse) + using rb_nullability apply presburger + apply simp + apply simp + using rerase_fuse by presburger + + + + +lemma RL_bder_preserved: + shows "RL (rerase a1) = RL (rerase a2) \ RL (rerase (bder c a1 )) = RL (rerase (bder c a2))" + by (metis rder_bder_rerase rder_correctness) + + +lemma RL_bders_simp: + shows "RL (rerase (bders_simp r s)) = RL (rerase (bders r s))" apply(induct s arbitrary: r rule: rev_induct) apply(simp) - apply(simp) - apply(simp add: ders_append) + apply(simp add: bders_append) apply(simp add: bders_simp_append) - apply(simp add: L_bsimp_erase[symmetric]) - by (simp add: der_correctness) + apply(simp add: RL_bsimp_rerase[symmetric]) + using RL_bder_preserved by blast + lemma bmkeps_fuse: @@ -672,10 +818,10 @@ lemma b4: shows "bnullable (bders_simp r s) = bnullable (bders r s)" proof - - have "L (erase (bders_simp r s)) = L (erase (bders r s))" - using L_bders_simp by force + have "RL (rerase (bders_simp r s)) = RL (rerase (bders r s))" + by (simp add: RL_bders_simp) then show "bnullable (bders_simp r s) = bnullable (bders r s)" - using bnullable_correctness nullable_correctness by blast + using RL_rnullable rb_nullability by blast qed @@ -706,7 +852,7 @@ | ss3: "r1 \ r2 \ (r1 # rs) s\ (r2 # rs)" | ss4: "(AZERO # rs) s\ rs" | 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)" +| ss6: "rerase a1 = rerase a2 \ (rsa@[a1]@rsb@[a2]@rsc) s\ (rsa@[a1]@rsb@rsc)" inductive @@ -810,7 +956,7 @@ 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)))" + shows "(rs1 @ rs2) s\* (rs1 @ distinctBy rs2 rerase (set (map rerase 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) @@ -819,8 +965,8 @@ done lemma ss6_stronger: - shows "rs1 s\* distinctBy rs1 erase {}" - using ss6_stronger_aux[of "[]" _] by auto + shows "rs1 s\* distinctBy rs1 rerase {}" + by (metis append_Nil list.set(1) list.simps(8) ss6_stronger_aux) lemma rewrite_preserves_fuse: @@ -850,7 +996,7 @@ 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) + by (smt (verit, ccfv_threshold) rerase_fuse list.simps(8) list.simps(9) rrewrite_srewrite.ss6 srewrites.simps) qed (auto intro: rrewrite_srewrite.intros) @@ -924,8 +1070,8 @@ and "rs1 s\ rs2 \ bnullables rs1 = bnullables rs2" apply(induct rule: rrewrite_srewrite.inducts) apply(auto simp add: bnullable_fuse) - apply (meson UnCI bnullable_fuse imageI) - by (metis bnullable_correctness) + apply (meson UnCI bnullable_fuse imageI) + by (metis rb_nullability) lemma rewritesnullable: @@ -956,7 +1102,7 @@ next case (ss6 a1 a2 rsa rsb rsc) then show ?case - by (smt (verit, best) append_Cons bmkeps.simps(3) bmkepss.simps(2) bmkepss1 bmkepss2 bnullable_correctness) + by (smt (z3) append_is_Nil_conv bmkepss1 bmkepss2 in_set_conv_decomp_first list.set_intros(1) rb_nullability set_ConsD) qed (auto) lemma rewrites_bmkeps: @@ -1015,10 +1161,10 @@ 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 {})" + also have "... s\* distinctBy (flts (map bsimp rs)) rerase {}" by (simp add: ss6_stronger) + finally have "AALTs bs1 rs \* AALTs bs1 (distinctBy (flts (map bsimp rs)) rerase {})" + using contextrewrites0 by auto + also have "... \* bsimp_AALTs bs1 (distinctBy (flts (map bsimp rs)) rerase {})" by (simp add: bsimp_AALTs_rewrites) finally show "AALTs bs1 rs \* bsimp (AALTs bs1 rs)" by simp qed (simp_all) @@ -1107,7 +1253,7 @@ case (ss6 a1 a2 bs rsa rsb) then show ?case apply(simp only: map_append) - by (smt (verit, best) erase_bder list.simps(8) list.simps(9) local.ss6 rrewrite_srewrite.ss6 srewrites.simps) + by (smt (verit, best) rder_bder_rerase list.simps(8) list.simps(9) local.ss6 rrewrite_srewrite.ss6 srewrites.simps) qed lemma rewrites_preserves_bder: @@ -1160,36 +1306,6 @@ using blexer_correctness main_blexer_simp by simp -fun - rerase :: "arexp \ rrexp" -where - "rerase AZERO = RZERO" -| "rerase (AONE _) = RONE" -| "rerase (ACHAR _ c) = RCHAR c" -| "rerase (AALTs bs rs) = RALTS (map rerase rs)" -| "rerase (ASEQ _ r1 r2) = RSEQ (rerase r1) (rerase r2)" -| "rerase (ASTAR _ r) = RSTAR (rerase r)" - - - -lemma asize_rsize: - shows "rsize (rerase r) = asize r" - apply(induct r) - apply simp+ - - apply (metis (mono_tags, lifting) comp_apply map_eq_conv) - by simp - -lemma rb_nullability: - shows " rnullable (rerase a) = bnullable a" - apply(induct a) - apply simp+ - done - -lemma fuse_anything_doesnt_matter: - shows "rerase a = rerase (fuse bs a)" - by (smt (verit) fuse.elims rerase.simps(2) rerase.simps(3) rerase.simps(4) rerase.simps(5) rerase.simps(6)) - lemma rerase_preimage: shows "rerase r = RZERO \ r = AZERO" @@ -1307,7 +1423,7 @@ | "agood (ACHAR cs c) = True" | "agood (AALTs cs []) = False" | "agood (AALTs cs [r]) = False" -| "agood (AALTs cs (r1#r2#rs)) = (distinct (map erase (r1 # r2 # rs)) \(\r' \ set (r1#r2#rs). agood r' \ anonalt r'))" +| "agood (AALTs cs (r1#r2#rs)) = (distinct (map rerase (r1 # r2 # rs)) \(\r' \ set (r1#r2#rs). agood r' \ anonalt r'))" | "agood (ASEQ _ AZERO _) = False" | "agood (ASEQ _ (AONE _) _) = False" | "agood (ASEQ _ _ AZERO) = False" @@ -1383,7 +1499,7 @@ done lemma good0: - assumes "rs \ Nil" "\r \ set rs. anonalt r" "distinct (map erase rs)" + assumes "rs \ Nil" "\r \ set rs. anonalt r" "distinct (map rerase rs)" shows "agood (bsimp_AALTs bs rs) \ (\r \ set rs. agood r)" using assms apply(induct bs rs rule: bsimp_AALTs.induct) @@ -1395,18 +1511,19 @@ using bsimp_AALTs.simps(3) apply presburger apply(simp only:) - apply(subgoal_tac "agood (AALTs bs1 (v # vb # vc)) = ((\r \ (set (v # vb # vc)). agood r \ anonalt r) \ distinct (map erase (v # vb # vc)))") + apply(subgoal_tac "agood (AALTs bs1 (v # vb # vc)) = ((\r \ (set (v # vb # vc)). agood r \ anonalt r) \ distinct (map rerase (v # vb # vc)))") prefer 2 using agood.simps(6) apply blast apply(simp only:) - apply(subgoal_tac "((\r\set (v # vb # vc). agood r \ anonalt r) \ distinct (map erase (v # vb # vc))) = ((\r\set (v # vb # vc). agood r) \ distinct (map erase (v # vb # vc)))") + apply(subgoal_tac "((\r\set (v # vb # vc). agood r \ anonalt r) \ distinct (map rerase (v # vb # vc))) = ((\r\set (v # vb # vc). agood r) \ distinct (map rerase (v # vb # vc)))") prefer 2 apply blast apply(simp only:) - apply(subgoal_tac "((\r \ set (v # vb # vc). agood r) \ distinct (map erase (v # vb # vc))) = (\ r \ set (v # vb # vc). agood r) ") + apply(subgoal_tac "((\r \ set (v # vb # vc). agood r) \ distinct (map rerase (v # vb # vc))) = (\ r \ set (v # vb # vc). agood r) ") prefer 2 - apply(subgoal_tac "distinct (map erase (v # vb # vc)) = True") - prefer 2 + apply(subgoal_tac "distinct (map rerase (v # vb # vc)) = True") + prefer 2 + sledgehammer apply blast prefer 2 apply force @@ -1628,13 +1745,13 @@ done lemma dB_keeps_property: - shows "(\r \ set rs. P r) \ (\r \ set (distinctBy rs erase rset). P r)" + shows "(\r \ set rs. P r) \ (\r \ set (distinctBy rs rerase rset). P r)" apply(induct rs arbitrary: rset) apply simp+ done lemma dB_filters_out: - shows "erase a \ rset \ a \ set (distinctBy rs erase (rset))" + shows "rerase a \ rset \ a \ set (distinctBy rs rerase (rset))" apply(induct rs arbitrary: rset) apply simp apply(case_tac "a = aa") @@ -1642,33 +1759,32 @@ done lemma dB_will_be_distinct: - shows "distinct (distinctBy rs erase (insert (erase a) rset)) \ distinct (a # (distinctBy rs erase (insert (erase a) rset)))" + shows "distinct (distinctBy rs rerase (insert (rerase a) rset)) \ distinct (a # (distinctBy rs rerase (insert (rerase a) rset)))" using dB_filters_out by force - lemma dB_does_the_job2: - shows "distinct (distinctBy rs erase rset)" + shows "distinct (distinctBy rs rerase rset)" apply(induct rs arbitrary: rset) apply simp - apply(case_tac "erase a \ rset") + apply(case_tac "rerase a \ rset") apply simp - apply(drule_tac x = "insert (erase a) rset" in meta_spec) - apply(subgoal_tac "distinctBy (a # rs) erase rset = a # distinctBy rs erase (insert (erase a ) rset)") + apply(drule_tac x = "insert (rerase a) rset" in meta_spec) + apply(subgoal_tac "distinctBy (a # rs) rerase rset = a # distinctBy rs rerase (insert (rerase a ) rset)") apply(simp only:) using dB_will_be_distinct apply presburger by auto lemma dB_does_more_job: - shows "distinct (map erase (distinctBy rs erase rset))" + shows "distinct (map rerase (distinctBy rs rerase rset))" apply(induct rs arbitrary:rset) apply simp - apply(case_tac "erase a \ rset") + apply(case_tac "rerase a \ rset") apply simp+ using dB_filters_out by force lemma dB_mono2: - shows "rset \ rset' \ distinctBy rs erase rset = [] \ distinctBy rs erase rset' = []" + shows "rset \ rset' \ distinctBy rs rerase rset = [] \ distinctBy rs rerase rset' = []" apply(induct rs arbitrary: rset rset') apply simp+ by (meson in_mono list.discI) @@ -1692,12 +1808,11 @@ apply(subgoal_tac "\r \ set (flts (map bsimp x2a)). anonalt r") prefer 2 apply (metis (mono_tags, lifting) SizeBound3.nn1c image_iff list.set_map) - apply(subgoal_tac "\r \ set (distinctBy (flts (map bsimp x2a)) erase {}). anonalt r") - prefer 2 + apply(subgoal_tac "\r \ set (distinctBy (flts (map bsimp x2a)) rerase {}). anonalt r") + prefer 2 using dB_keeps_property apply presburger by blast - lemma induct_smaller_elem_list: shows "\r \ set list. asize r < Suc (sum_list (map asize list))" apply(induct list) @@ -1761,6 +1876,8 @@ prefer 2 apply (metis Cons_eq_map_conv SizeBound3.nn1b SizeBound3.nn1c ex_map_conv) using dB_keeps_property apply presburger + sledgehammer + using dB_does_more_job apply presburger apply(subgoal_tac " Ball (set ( (flts (bsimp a # map bsimp list)) )) agood") using dB_keeps_property apply presburger @@ -1820,10 +1937,10 @@ lemma good1a: - assumes "L (erase a) \ {}" + assumes "RL (rerase a) \ {}" shows "agood (bsimp a)" using good1 assms - using L_bsimp_erase by force + using RL_bsimp_rerase by force @@ -1940,7 +2057,7 @@ using test good1 oops - +(* lemma erase_preimage1: assumes "anonalt r" shows "erase r = ONE \ \bs. r = AONE bs" @@ -2036,7 +2153,8 @@ apply(subgoal_tac "rerase r'2 = rerase r2") using rerase.simps(5) apply presburger - sledgehammer + oops + lemma rerase_erase_good: @@ -2114,7 +2232,7 @@ apply(insert rerase_erase) by (metis assms image_empty) - +*) @@ -2123,20 +2241,55 @@ lemma nonalt_flts : shows "\r \ set (flts (map bsimp rs)). r \ AZERO" using SizeBound3.qqq1 by force + + +lemma rerase_map_bsimp: + assumes "\ r. r \ set x2a \ rerase (bsimp r) = (rsimp \ rerase) r" + shows " map rerase (map bsimp x2a) = map (rsimp \ rerase) x2a " + using assms + + apply(induct x2a) + apply simp + apply(subgoal_tac "a \ set (a # x2a)") + prefer 2 + apply (meson list.set_intros(1)) + apply(subgoal_tac "rerase (bsimp a ) = (rsimp \ rerase) a") + apply simp + by presburger + + + +lemma rerase_flts: + shows "map rerase (flts rs) = rflts (map rerase rs)" + apply(induct rs) + apply simp+ + apply(case_tac a) + apply simp+ + apply(simp add: rerase_fuse) + apply simp + done + +lemma rerase_dB: + shows "map rerase (distinctBy rs rerase acc) = rdistinct (map rerase rs) acc" + apply(induct rs arbitrary: acc) + apply simp+ + done -lemma rerase_list_ders: - shows "\x1 x2a. - (\x2aa. x2aa \ set x2a \ rerase (bsimp x2aa) = rsimp (rerase x2aa)) \ - (map rerase (distinctBy (flts (map bsimp x2a)) erase {})) = (rdistinct (rflts (map (rsimp \ rerase) x2a)) {})" - apply(subgoal_tac "\r \ set (flts (map bsimp x2a)). anonalt r ") - prefer 2 - apply (metis SizeBound3.nn1b SizeBound3.nn1c ex_map_conv) - sledgehammer +lemma rerase_earlier_later_same: + assumes " \r. r \ set x2a \ rerase (bsimp r) = rsimp (rerase r)" + shows " (map rerase (distinctBy (flts (map bsimp x2a)) rerase {})) = + (rdistinct (rflts (map (rsimp \ rerase) x2a)) {})" + apply(subst rerase_dB) + apply(subst rerase_flts) + apply(subst rerase_map_bsimp) + apply auto + using assms + apply simp + done - sorry lemma simp_rerase: @@ -2146,10 +2299,13 @@ using rerase_bsimp_ASEQ apply presburger apply simp apply(subst rerase_bsimp_AALTs) - apply(subgoal_tac "map rerase (distinctBy (flts (map bsimp x2a)) erase {}) = rdistinct (rflts (map (rsimp \ rerase) x2a)) {}") + apply(subgoal_tac "map rerase (distinctBy (flts (map bsimp x2a)) rerase {}) = rdistinct (rflts (map (rsimp \ rerase) x2a)) {}") + apply simp + using rerase_earlier_later_same apply presburger apply simp - using rerase_list_ders apply blast - by simp + done + + lemma rders_simp_size: shows " rders_simp (rerase r) s = rerase (bders_simp r s)" diff -r 61eff2abb0b6 -r 1481f465e6ea thys2/blexer2.sc --- a/thys2/blexer2.sc Tue Apr 19 09:08:01 2022 +0100 +++ b/thys2/blexer2.sc Thu Apr 21 14:58:51 2022 +0100 @@ -137,7 +137,7 @@ if(len <= 0) single(Nil) else{ for { - c <- chars + c <- chars_range('a', 'd') tail <- char_list(len - 1) } yield c :: tail } @@ -145,6 +145,19 @@ def strings(len: Int): Generator[String] = for(cs <- char_list(len)) yield cs.toString +def sampleString(r: Rexp) : List[String] = r match { + case STAR(r) => stringsFromRexp(r).flatMap(s => List("", s, s ++ s))//only generate 0, 1, 2 reptitions + case SEQ(r1, r2) => stringsFromRexp(r1).flatMap(s1 => stringsFromRexp(r2).map(s2 => s1 ++ s2) ) + case ALTS(r1, r2) => throw new Error(s" Rexp ${r} not expected: all alternatives are supposed to have been opened up") + case ONE => "" :: Nil + case ZERO => Nil + case CHAR(c) => c.toString :: Nil + +} + +def stringsFromRexp(r: Rexp) : List[String] = + breakIntoTerms(r).flatMap(r => sampleString(r)) + // (simple) binary trees trait Tree[T] @@ -682,7 +695,6 @@ def blex_simp(r: ARexp, s: List[Char]) : Bits = s match { case Nil => { if (bnullable(r)) { - //println(asize(r)) val bits = mkepsBC(r) bits } @@ -923,11 +935,51 @@ // test(rexp(10), 1000) { r => height(r) <= size(r) } // println("XXX faulty test") // test(rexp(10), 100) { r => height(r) <= size_faulty(r) } - println("testing strongbsimp against bsimp") - test2(rexp(10), strings(2), 100) { (r : Rexp, s: String) => - (simpBlexer(r, s) == strongBlexer(r, s)) + + + /* For inspection of counterexamples should they arise*/ +// println("testing strongbsimp against bsimp") +// val r = SEQ(SEQ(SEQ(ONE,CHAR('b')),STAR(CHAR('b'))), +// SEQ(ALTS(ALTS(ZERO,STAR(CHAR('b'))), +// STAR(ALTS(CHAR('a'),SEQ(SEQ(STAR(ALTS(STAR(CHAR('c')),CHAR('a'))), +// SEQ(CHAR('a'),SEQ(ALTS(CHAR('b'),ZERO),SEQ(ONE,CHAR('b'))))),ONE)))),ONE)) + +// val ss = stringsFromRexp(r) +// val boolList = ss.map(s => { +// val simpVal = simpBlexer(r, s) +// val strongVal = strongBlexer(r, s) +// println(simpVal) +// println(strongVal) +// (simpVal == strongVal) && (simpVal != None) +// }) +// println(boolList) +// println(boolList.exists(b => b == false)) + + + test(rexp(9), 100000) { (r: Rexp) => + val ss = stringsFromRexp(r) + val boolList = ss.map(s => { + val simpVal = simpBlexer(r, s) + val strongVal = strongBlexer(r, s) + // println(simpVal) + // println(strongVal) + (simpVal == strongVal) && (simpVal != None) + }) + !boolList.exists(b => b == false) } - + + } // small() generator_test() + +1 + +SEQ(SEQ(SEQ(ONE,CHAR('b')),STAR(CHAR('b'))), +SEQ(ALTS(ALTS(ZERO,STAR(CHAR('b'))), +STAR(ALTS(CHAR('a'),SEQ(SEQ(STAR(ALTS(STAR(CHAR('c')),CHAR('a'))), +SEQ(CHAR('a'),SEQ(ALTS(CHAR('b'),ZERO),SEQ(ONE,CHAR('b'))))),ONE)))),ONE)) + + +// Sequ(Sequ(Sequ(Empty,Chr(b)),Stars(List(Chr(b), Chr(b)))),Sequ(Right(Stars(List(Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty)), Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty))))),Empty)) +// Sequ(Sequ(Sequ(Empty,Chr(b)),Stars(List(Chr(b), Chr(b)))),Sequ(Right(Stars(List(Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty)), Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty))))),Empty)) \ No newline at end of file