diff -r 5c96fe5306a7 -r 57182b36ec01 thys2/SizeBound4.thy --- a/thys2/SizeBound4.thy Sat Feb 05 18:24:37 2022 +0000 +++ b/thys2/SizeBound4.thy Sun Feb 06 00:02:04 2022 +0000 @@ -206,7 +206,7 @@ (if bnullable r1 then AALT bs (ASEQ [] (bder c r1) r2) (fuse (bmkeps r1) (bder c r2)) else ASEQ bs (bder c r1) r2)" -| "bder c (ASTAR bs r) = ASEQ bs (fuse [Z] (bder c r)) (ASTAR [] r)" +| "bder c (ASTAR bs r) = ASEQ (bs @ [Z]) (bder c r) (ASTAR [] r)" fun @@ -566,8 +566,10 @@ | 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: "L(erase a2) \ L(erase a1) \ (rsa@[a1]@rsb@[a2]@rsc) s\ (rsa@[a1]@rsb@rsc)" +(*| extra: "bnullable r1 \ ASEQ bs0 (ASEQ bs1 r1 r2) r3 \ + ASEQ (bs0 @ bs1) r1 (ASEQ [] r2 r3)" +*) inductive rrewrites:: "arexp \ arexp \ bool" ("_ \* _" [100, 100] 100) @@ -586,6 +588,10 @@ shows "r1 \ r2 \ r1 \* r2" using rrewrites.intros(1) rrewrites.intros(2) by blast +lemma rs_in_rstar: + shows "r1 s\ r2 \ r1 s\* r2" + using rrewrites.intros(1) rrewrites.intros(2) by blast + lemma rrewrites_trans[trans]: assumes a1: "r1 \* r2" and a2: "r2 \* r3" shows "r1 \* r3" @@ -674,10 +680,19 @@ 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) + prefer 2 apply(drule_tac x="rs1 @ [a]" in meta_spec) + apply(simp) + apply(drule_tac x="rs1" in meta_spec) + apply(subgoal_tac "(rs1 @ a # rs2) s\* (rs1 @ rs2)") + using srewrites_trans apply blast + apply(subgoal_tac "\rs1a rs1b. rs1 = rs1a @ [x] @ rs1b") + prefer 2 + apply (simp add: split_list) + apply(erule exE)+ apply(simp) - done + using ss6[simplified] + using rs_in_rstar by force lemma ss6_stronger: shows "rs1 s\* distinctBy rs1 erase {}" @@ -710,12 +725,17 @@ finally show "map (fuse bs) (AALTs bs1 rs1 # rsb) s\ map (fuse bs) (map (fuse bs1) rs1 @ rsb)" by (simp add: comp_def fuse_append) next - case (ss6 a1 a2 rsa rsb rsc) + case (ss6 a2 a1 rsa rsb rsc) + have "L (erase a2) \ L (erase a1)" by fact then show "map (fuse bs) (rsa @ [a1] @ rsb @ [a2] @ rsc) s\ map (fuse bs) (rsa @ [a1] @ rsb @ rsc)" apply(simp) apply(rule rrewrite_srewrite.ss6[simplified]) apply(simp add: erase_fuse) done +(*next + case (extra bs0 bs1 r1 r2 r3) + then show ?case + by (metis append_assoc fuse.simps(5) rrewrite_srewrite.extra)*) qed (auto intro: rrewrite_srewrite.intros) lemma rewrites_fuse: @@ -787,8 +807,9 @@ 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) + + using bnullable_correctness nullable_correctness by blast lemma rewrites_bnullable_eq: @@ -824,11 +845,22 @@ then show "bmkepss (AALTs bs1 rs1 # rsb) = bmkepss (map (fuse bs1) rs1 @ rsb)" by (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse) next - case (ss6 a1 a2 rsa rsb rsc) - have as1: "erase a1 = erase a2" by fact + case (ss6 a2 a1 rsa rsb rsc) + have as1: "L(erase a2) \ L(erase a1)" by fact have as3: "bnullables (rsa @ [a1] @ rsb @ [a2] @ rsc)" by fact show "bmkepss (rsa @ [a1] @ rsb @ [a2] @ rsc) = bmkepss (rsa @ [a1] @ rsb @ rsc)" using as1 as3 - by (smt (verit, best) append_Cons bmkeps.simps(3) bmkepss.simps(2) bmkepss1 bmkepss2 bnullable_correctness) + by (smt (verit, ccfv_SIG) append_Cons bmkepss.simps(2) bmkepss1 bmkepss2 bnullable_correctness nullable_correctness subset_eq) +(*next + case (extra bs0 bs1 r1 bs2 r2 bs4 bs3) + then show ?case + apply(subst bmkeps.simps) + apply(subst bmkeps.simps) + apply(subst bmkeps.simps) + apply(subst bmkeps.simps) + apply(subst bmkeps.simps) + apply(subst bmkeps.simps) + apply(simp) + done*) qed (auto) lemma rewrites_bmkeps: @@ -908,6 +940,11 @@ apply(simp_all add: bder_fuse) done +lemma map_single: + shows "map f [x] = [f x]" + by simp + + 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" @@ -977,20 +1014,39 @@ apply(simp) using bder_fuse_list map_map rrewrite_srewrite.ss5 srewrites.simps by blast next - case (ss6 a1 a2 bs rsa rsb) - have as: "erase a1 = erase a2" by fact + case (ss6 a2 a1 bs rsa rsb) + have as: "L(erase a2) \ L(erase a1)" by fact show "map (bder c) (bs @ [a1] @ rsa @ [a2] @ rsb) s\* map (bder c) (bs @ [a1] @ rsa @ rsb)" apply(simp only: map_append) - by (smt (verit, best) erase_bder list.simps(8) list.simps(9) as rrewrite_srewrite.ss6 srewrites.simps) + apply(simp only: map_single) + apply(rule rs_in_rstar) + thm rrewrite_srewrite.intros + apply(rule rrewrite_srewrite.ss6) + using as + apply(auto simp add: der_correctness Der_def) + done +(*next + case (extra bs0 bs1 r1 r2 r3) + then show ?case + apply(auto simp add: comp_def) + + defer + using r_in_rstar rrewrite_srewrite.extra apply presburger + prefer 2 + using r_in_rstar rrewrite_srewrite.extra apply presburger + prefer 2 + sorry*) qed + + 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_preserves_bder rrewrites_trans) -done + done lemma central: @@ -1034,6 +1090,76 @@ (* some tests *) +definition + bders_simp_Set :: "string set \ arexp \ arexp set" +where + "bders_simp_Set A r \ bders_simp r ` A" + +lemma pders_Set_union: + shows "bders_simp_Set (A \ B) r = (bders_simp_Set A r \ bders_simp_Set B r)" + apply (simp add: bders_simp_Set_def) + by (simp add: image_Un) + +lemma pders_Set_subset: + shows "A \ B \ bders_simp_Set A r \ bders_simp_Set B r" + apply (auto simp add: bders_simp_Set_def) + done + + +lemma AZERO_r: + "bders_simp AZERO s = AZERO" + apply(induct s) + apply(auto) + done + +lemma bders_simp_Set_ZERO [simp]: + shows "bders_simp_Set UNIV1 AZERO \ {AZERO}" + unfolding UNIV1_def bders_simp_Set_def + apply(auto) + using AZERO_r by blast + +lemma AONE_r: + shows "bders_simp (AONE bs) s = AZERO \ bders_simp (AONE bs) s = AONE bs" + apply(induct s) + apply(auto) + using AZERO_r apply blast + using AZERO_r by blast + +lemma bders_simp_Set_ONE [simp]: + shows "bders_simp_Set UNIV1 (AONE bs) \ {AZERO, AONE bs}" + unfolding UNIV1_def bders_simp_Set_def + apply(auto split: if_splits) + using AONE_r by blast + +lemma ACHAR_r: + shows "bders_simp (ACHAR bs c) s = AZERO \ + bders_simp (ACHAR bs c) s = AONE bs \ + bders_simp (ACHAR bs c) s = ACHAR bs c" + apply(induct s) + apply(auto) + using AONE_r apply blast + using AZERO_r apply force + using AONE_r apply blast + using AZERO_r apply blast + using AONE_r apply blast + using AZERO_r by blast + +lemma bders_simp_Set_CHAR [simp]: + shows "bders_simp_Set UNIV1 (ACHAR bs c) \ {AZERO, AONE bs, ACHAR bs c}" +unfolding UNIV1_def bders_simp_Set_def + apply(auto) + using ACHAR_r by blast + +lemma bders_simp_Set_ALT [simp]: + shows "bders_simp_Set UNIV1 (AALT bs r1 r2) = bders_simp_Set UNIV1 r1 \ bders_simp_Set UNIV1 r2" + unfolding UNIV1_def bders_simp_Set_def + apply(auto) + oops + + + + +(* lemma asize_fuse: shows "asize (fuse bs r) = asize r" apply(induct r arbitrary: bs) @@ -1372,11 +1498,13 @@ using finite_pder apply blast oops - +*) (* below is the idempotency of bsimp *) +(* + lemma bsimp_ASEQ_fuse: shows "fuse bs1 (bsimp_ASEQ bs2 r1 r2) = bsimp_ASEQ (bs1 @ bs2) r1 r2" apply(induct r1 r2 arbitrary: bs1 bs2 rule: bsimp_ASEQ.induct) @@ -1466,6 +1594,8 @@ apply auto oops +*) + (* AALTs [] [AZERO, AALTs(bs1, [a, b]) ] @@ -1475,24 +1605,19 @@ *) -lemma normal_bsimp: - shows "\r'. bsimp r \ r'" - oops (*r' size bsimp r > size r' r' \* bsimp bsimp r size bsimp r > size r' \ size bsimp bsimp r*) -export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers - unused_thms - +(* inductive aggressive:: "arexp \ arexp \ bool" ("_ \? _" [99, 99] 99) where "ASEQ bs (AALTs bs1 rs) r \? AALTs (bs@bs1) (map (\r'. ASEQ [] r' r) rs) " - +*) end