diff -r 320f923c77b9 -r 98362002c818 thys2/SizeBound.thy --- a/thys2/SizeBound.thy Thu Nov 04 01:07:34 2021 +0000 +++ b/thys2/SizeBound.thy Thu Nov 04 09:45:41 2021 +0000 @@ -118,30 +118,12 @@ | "erase (ASTAR _ r) = STAR (erase r)" - - fun nonalt :: "arexp \ bool" where "nonalt (AALTs bs2 rs) = False" | "nonalt r = True" -fun good :: "arexp \ bool" where - "good AZERO = False" -| "good (AONE cs) = True" -| "good (ACHAR cs c) = True" -| "good (AALTs cs []) = False" -| "good (AALTs cs [r]) = False" -| "good (AALTs cs (r1#r2#rs)) = (\r' \ set (r1#r2#rs). good r' \ nonalt r')" -| "good (ASEQ _ AZERO _) = False" -| "good (ASEQ _ (AONE _) _) = False" -| "good (ASEQ _ _ AZERO) = False" -| "good (ASEQ cs r1 r2) = (good r1 \ good r2)" -| "good (ASTAR cs r) = True" - - - - fun fuse :: "bit list \ arexp \ arexp" where "fuse bs AZERO = AZERO" | "fuse bs (AONE cs) = AONE (bs @ cs)" @@ -238,8 +220,6 @@ apply(simp_all) done -thm Posix.induct - lemma erase_intern [simp]: shows "erase (intern r) = r" apply(induct r) @@ -551,8 +531,9 @@ (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 @@ -563,16 +544,6 @@ - -fun li :: "bit list \ arexp list \ arexp" - where - "li _ [] = AZERO" -| "li bs [a] = fuse bs a" -| "li bs as = AALTs bs as" - - - - fun bsimp_ASEQ :: "bit list \ arexp \ arexp \ arexp" where "bsimp_ASEQ _ AZERO _ = AZERO" @@ -591,12 +562,10 @@ 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)) erase {}) " | "bsimp r = r" - - fun bders_simp :: "arexp \ string \ arexp" where @@ -605,23 +574,16 @@ definition blexer_simp where "blexer_simp r s \ if bnullable (bders_simp (intern r) s) then - decode (bmkeps (bders_simp (intern r) s)) r else None" + decode (bmkeps (bders_simp (intern r) s)) r else None" 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" apply(induct s1 arbitrary: r s2) - apply(simp) - apply(simp) + apply(simp_all) done - - - - - - lemma L_bsimp_ASEQ: "L (SEQ (erase r1) (erase r2)) = L (erase (bsimp_ASEQ bs r1 r2))" apply(induct bs r1 r2 rule: bsimp_ASEQ.induct) @@ -674,25 +636,25 @@ apply(auto simp add: Sequ_def)[1] apply(subst (asm) L_bsimp_ASEQ[symmetric]) apply(auto simp add: Sequ_def)[1] - apply(simp) - apply(subst L_bsimp_AALTs[symmetric]) - defer - apply(simp) + apply(simp) + apply(subst L_bsimp_AALTs[symmetric]) + defer + apply(simp) apply(subst (2)L_erase_AALTs) apply(subst L_erase_dB) apply(subst L_erase_flts) apply(auto) - apply (simp add: L_erase_AALTs) + apply (simp add: L_erase_AALTs) using L_erase_AALTs by blast + + 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" @@ -711,7 +673,7 @@ lemma L_bders_simp: shows "L (erase (bders_simp r s)) = L (erase (bders r s))" apply(induct s arbitrary: r rule: rev_induct) - apply(simp) + apply(simp) apply(simp) apply(simp add: ders_append) apply(simp add: bders_simp_append) @@ -748,23 +710,6 @@ apply(simp) by (metis append_assoc in_set_conv_decomp r1 r2) -lemma qq3: - shows "bnullable (AALTs bs rs) = (\r \ set rs. bnullable r)" - apply(induct rs arbitrary: bs) - apply(simp) - apply(simp) - done - - - - - -fun nonnested :: "arexp \ bool" - where - "nonnested (AALTs bs2 []) = True" -| "nonnested (AALTs bs2 ((AALTs bs1 rs1) # rs2)) = False" -| "nonnested (AALTs bs2 (r # rs2)) = nonnested (AALTs bs2 rs2)" -| "nonnested r = True" lemma flts_append: shows "flts (xs1 @ xs2) = flts xs1 @ flts xs2" @@ -1006,41 +951,44 @@ done -corollary srewrites_alt1: "rs1 s\* rs2 \ AALTs bs rs1 \* AALTs bs rs2" +corollary srewrites_alt1: + assumes "rs1 s\* rs2" + shows "AALTs bs rs1 \* AALTs bs rs2" +using assms by (metis append.left_neutral srewrites_alt) -lemma star_seq: "r1 \* r2 \ ASEQ bs r1 r3 \* ASEQ bs r2 r3" - apply(induct r1 r2 arbitrary: r3 rule: rrewrites.induct) - apply(rule rs1) - apply(erule rrewrites.cases) - apply(simp) - apply(rule r_in_rstar) - apply(rule rrewrite.intros(4)) - apply simp - apply(rule rs2) - apply(assumption) - apply(rule rrewrite.intros(4)) - by assumption +lemma star_seq: + assumes "r1 \* r2" + shows "ASEQ bs r1 r3 \* ASEQ bs r2 r3" +using assms +apply(induct r1 r2 arbitrary: r3 rule: rrewrites.induct) +apply(auto intro: rrewrite.intros) +done -lemma star_seq2: "r3 \* r4 \ ASEQ bs r1 r3 \* ASEQ bs r1 r4" - apply(induct r3 r4 arbitrary: r1 rule: rrewrites.induct) - apply auto - using rrewrite.intros(5) by blast - +lemma star_seq2: + assumes "r3 \* r4" + shows "ASEQ bs r1 r3 \* ASEQ bs r1 r4" +using assms +apply(induct r3 r4 arbitrary: r1 rule: rrewrites.induct) +apply(auto intro: rrewrite.intros) +done -lemma continuous_rewrite: "\r1 \* AZERO\ \ ASEQ bs1 r1 r2 \* AZERO" +lemma continuous_rewrite: + assumes "r1 \* AZERO" + shows "ASEQ bs1 r1 r2 \* AZERO" +using assms apply(induction ra\"r1" rb\"AZERO" arbitrary: bs1 r1 r2 rule: rrewrites.induct) - apply (simp add: r_in_rstar rrewrite.intros(1)) - - by (meson rrewrite.intros(1) rrewrites.intros(2) star_seq) + apply(auto intro: rrewrite.intros r_in_rstar star_seq) + by (meson rrewrite.intros(1) rs2 star_seq) -lemma bsimp_aalts_simpcases: "AONE bs \* (bsimp (AONE bs))" "AZERO \* bsimp AZERO" "ACHAR bs c \* (bsimp (ACHAR bs c))" - apply (simp add: rrewrites.intros(1)) - apply (simp add: rrewrites.intros(1)) - by (simp add: rrewrites.intros(1)) +lemma bsimp_aalts_simpcases: + shows "AONE bs \* bsimp (AONE bs)" + and "AZERO \* bsimp AZERO" + and "ACHAR bs c \* bsimp (ACHAR bs c)" + by (simp_all) lemma trivialbsimpsrewrites: "\\x. x \ set rs \ x \* f x \ \ rs s\* (map f rs)" @@ -1072,8 +1020,6 @@ - - lemma flts_prepend: "\nonalt a; nonazero a\ \ flts (a#rs) = a # (flts rs)" by (metis append_Cons append_Nil flts_single1 flts_append) @@ -1098,14 +1044,14 @@ apply blast using bbbbs1 apply blast - apply(simp add: nonalt.simps)+ + apply(simp)+ apply (meson nonazero.elims(3)) by (meson fs4 nonalt.elims(3) nonazero.elims(3)) -lemma rrewrite0away: "AALTs bs ( AZERO # rsb) \ AALTs bs rsb" +lemma rrewrite0away: "AALTs bs (AZERO # rsb) \ AALTs bs rsb" by (metis append_Nil rrewrite.intros(7)) @@ -1139,7 +1085,7 @@ apply(case_tac "\bs2 rs2. a = AALTs bs2 rs2") apply(erule exE)+ - apply(simp add: flts.simps) + apply(simp) prefer 2 apply(subst flts_prepend) @@ -1164,16 +1110,6 @@ apply auto done -fun distinctByAcc :: "'a list \ ('a \ 'b) \ 'b set \ 'b set" - where - "distinctByAcc [] f acc = acc" -| "distinctByAcc (x#xs) f acc = - (if (f x) \ acc then distinctByAcc xs f acc - else (distinctByAcc xs f ({f x} \ acc)))" - -lemma dB_single_step: "distinctBy (a#rs) f {} = a # distinctBy rs f {f a}" - apply simp - done lemma somewhereInside: "r \ set rs \ \rs1 rs2. rs = rs1@[r]@rs2" using split_list by fastforce @@ -1236,7 +1172,8 @@ -lemma bsimp_rewrite: " (rrewrites r ( bsimp r))" +lemma bsimp_rewrite: + shows "r \* bsimp r" apply(induction r rule: bsimp.induct) apply simp apply(case_tac "bsimp r1 = AZERO") @@ -1315,12 +1252,11 @@ lemma nomember_bnullable: "\ \ (\r0\set rs1. bnullable r0); \ bnullable r; \ (\r0\set rs2. bnullable r0)\ \ \bnullable (AALTs bs (rs1 @ [r] @ rs2))" - using nonbnullable_lists_concat qq3 by presburger + using bnullable.simps(4) nonbnullable_lists_concat by presburger lemma bnullable_segment: " bnullable (AALTs bs (rs1@[r]@rs2)) \ bnullable (AALTs bs rs1) \ bnullable (AALTs bs rs2) \ bnullable r" apply(case_tac "\r0\set rs1. bnullable r0") - - using qq3 apply blast + using r2 apply blast apply(case_tac "bnullable r") apply blast @@ -1359,7 +1295,7 @@ apply(subgoal_tac "bnullable (AALTs bs rs3)") apply(subgoal_tac "\r \ set (rs1@rs2). \bnullable r") apply(subgoal_tac "bmkeps (AALTs bs (rs1@rs2@rs3)) = bmkeps (AALTs bs ((rs1@rs2)@rs3) )") - apply (metis qq2 qq3) + apply (metis bnullable.simps(4) qq2) apply (metis append.assoc) @@ -1380,7 +1316,7 @@ using r2 apply blast apply (metis list.set_intros(1)) - apply (smt (verit, ccfv_threshold) append_eq_append_conv2 list.set_intros(1) qq2 qq3 rewrite_nullable rrewrite.intros(8) self_append_conv2 spillbmkepslistr) + apply (smt (verit, ccfv_threshold) append_eq_append_conv2 list.set_intros(1) qq2 bnullable.simps(4) rewrite_nullable rrewrite.intros(8) self_append_conv2 spillbmkepslistr) thm qq1 @@ -1427,7 +1363,7 @@ apply (simp add: b2) - by (smt (z3) Un_iff bnullable_correctness erase.simps(5) qq1 qq2 qq3 set_append) + by (smt (z3) Un_iff bnullable_correctness erase.simps(5) qq1 qq2 bnullable.simps(4) set_append) lemma rewrites_bmkeps: assumes "r1 \* r2" "bnullable r1" @@ -1496,16 +1432,19 @@ -lemma rewrites_fuse: "r2 \* r2' \ (fuse bs1 r2) \* (fuse bs1 r2')" - apply(induction r2 r2' arbitrary: bs1 rule: rrewrites.induct) - apply simp - by (meson real_trans rewrite_fuse) +lemma rewrites_fuse: + assumes "r2 \* r2'" + shows "fuse bs1 r2 \* fuse bs1 r2'" +using assms +apply(induction r2 r2' arbitrary: bs1 rule: rrewrites.induct) +apply(auto intro: rewrite_fuse real_trans) +done -lemma bder_fuse_list: " map (bder c \ fuse bs1) rs1 = map (fuse bs1 \ bder c) rs1" - apply(induction rs1) - apply simp - by (simp add: bder_fuse) - +lemma bder_fuse_list: + shows "map (bder c \ fuse bs1) rs1 = map (fuse bs1 \ bder c) rs1" +apply(induction rs1) +apply(simp_all add: bder_fuse) +done lemma rewrite_der_altmiddle: "bder c (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) \* bder c (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"