# HG changeset patch # User Christian Urban # Date 1641594326 0 # Node ID 0c666a0c57d74aba956e2c95c611f5acaa92cbdf # Parent c892847df987e93931835fe0bf2c8cfa1772f2ce isarfied some proofs diff -r c892847df987 -r 0c666a0c57d7 thys2/Positions.thy --- a/thys2/Positions.thy Tue Dec 14 16:32:33 2021 +0000 +++ b/thys2/Positions.thy Fri Jan 07 22:25:26 2022 +0000 @@ -206,37 +206,34 @@ shows "ordering (\v1 v2. v1 :\val v2) (\ v1 v2. v1 :\val v2)" unfolding ordering_def PosOrd_ex_eq_def apply(auto) -using PosOrd_irrefl apply blast -using PosOrd_assym apply blast -using PosOrd_trans by blast +using PosOrd_trans partial_preordering_def apply blast +using PosOrd_assym ordering_axioms_def by blast lemma PosOrd_order: shows "class.order (\v1 v2. v1 :\val v2) (\ v1 v2. v1 :\val v2)" using PosOrd_ordering apply(simp add: class.order_def class.preorder_def class.order_axioms_def) -unfolding ordering_def -by blast + by (metis (full_types) PosOrd_ex_eq_def PosOrd_irrefl PosOrd_trans) lemma PosOrd_ex_eq2: shows "v1 :\val v2 \ (v1 :\val v2 \ v1 \ v2)" -using PosOrd_ordering -unfolding ordering_def -by auto + using PosOrd_ordering + using PosOrd_ex_eq_def PosOrd_irrefl by blast lemma PosOrdeq_trans: assumes "v1 :\val v2" "v2 :\val v3" shows "v1 :\val v3" using assms PosOrd_ordering -unfolding ordering_def -by blast + unfolding ordering_def + by (metis partial_preordering.trans) lemma PosOrdeq_antisym: assumes "v1 :\val v2" "v2 :\val v1" shows "v1 = v2" using assms PosOrd_ordering -unfolding ordering_def -by blast + unfolding ordering_def + by (simp add: ordering_axioms_def) lemma PosOrdeq_refl: shows "v :\val v" diff -r c892847df987 -r 0c666a0c57d7 thys2/SizeBound.thy --- a/thys2/SizeBound.thy Tue Dec 14 16:32:33 2021 +0000 +++ b/thys2/SizeBound.thy Fri Jan 07 22:25:26 2022 +0000 @@ -238,6 +238,12 @@ apply(simp_all) done +lemma bnullable_fuse: + shows "bnullable (fuse bs r) = bnullable r" + apply(induct r arbitrary: bs) + apply(auto) + done + lemma retrieve_encode_STARS: assumes "\v\set vs. \ v : r \ code v = retrieve (intern r) v" shows "code (Stars vs) = retrieve (ASTAR [] (intern r)) (Stars vs)" @@ -691,7 +697,6 @@ shows "bnullable (bders_simp r s) = bnullable (bders r s)" by (metis L_bders_simp bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1)) - lemma qq1: assumes "\r \ set rs. bnullable r" shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs rs)" @@ -710,6 +715,17 @@ apply(simp) by (metis append_assoc in_set_conv_decomp r1 r2) +lemma qq3: + assumes "bnullable (AALTs bs (rs @ rs1))" + "bnullable (AALTs bs (rs @ rs2))" + "\bnullable (AALTs bs rs1); bnullable (AALTs bs rs2); \r\set rs. \bnullable r\ \ + bmkeps (AALTs bs rs1) = bmkeps (AALTs bs rs2)" + shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs (rs @ rs2))" + using assms + apply(case_tac "\r \ set rs. bnullable r") + using qq1 apply auto[1] + by (metis UnE bnullable.simps(4) qq2 set_append) + lemma flts_append: shows "flts (xs1 @ xs2) = flts xs1 @ flts xs2" @@ -739,10 +755,6 @@ - - - - fun nonazero :: "arexp \ bool" where "nonazero AZERO = False" @@ -850,17 +862,15 @@ apply(simp) using qq4 r1 r2 by auto - - - lemma bder_fuse: shows "bder c (fuse bs a) = fuse bs (bder c a)" apply(induct a arbitrary: bs c) apply(simp_all) done -inductive rrewrite:: "arexp \ arexp \ bool" ("_ \ _" [99, 99] 99) - where +inductive + rrewrite:: "arexp \ arexp \ bool" ("_ \ _" [99, 99] 99) +where "ASEQ bs AZERO r2 \ AZERO" | "ASEQ bs r1 AZERO \ AZERO" | "ASEQ bs (AONE bs1) r \ fuse (bs@bs1) r" @@ -880,17 +890,21 @@ | "erase a1 = erase a2 \ AALTs bs (rsa@[a1]@rsb@[a2]@rsc) \ AALTs bs (rsa@[a1]@rsb@rsc)" -inductive rrewrites:: "arexp \ arexp \ bool" ("_ \* _" [100, 100] 100) - where -rs1[intro, simp]:"r \* r" +inductive + rrewrites:: "arexp \ arexp \ bool" ("_ \* _" [100, 100] 100) +where + rs1[intro, simp]:"r \* r" | rs2[intro]: "\r1 \* r2; r2 \ r3\ \ r1 \* r3" -inductive srewrites:: "arexp list \ arexp list \ bool" (" _ s\* _" [100, 100] 100) - where -ss1: "[] s\* []" -|ss2: "\r \* r'; rs s\* rs'\ \ (r#rs) s\* (r'#rs')" -(*rs1 = [r1, r2, ..., rn] rs2 = [r1', r2', ..., rn'] -[r1, r2, ..., rn] \* [r1', r2, ..., rn] \* [...r2',...] \* [r1', r2',... rn'] +inductive + srewrites:: "arexp list \ arexp list \ bool" (" _ s\* _" [100, 100] 100) +where + ss1: "[] s\* []" +| ss2: "\r \* r'; rs s\* rs'\ \ (r#rs) s\* (r'#rs')" + +(* +rs1 = [r1, r2, ..., rn] rs2 = [r1', r2', ..., rn'] + [r1, r2, ..., rn] \* [r1', r2, ..., rn] \* [...r2',...] \* [r1', r2',... rn'] *) @@ -898,12 +912,12 @@ lemma r_in_rstar : "r1 \ r2 \ r1 \* r2" using rrewrites.intros(1) rrewrites.intros(2) by blast -lemma real_trans [trans]: +lemma real_trans[trans]: assumes a1: "r1 \* r2" and a2: "r2 \* r3" shows "r1 \* r3" using a2 a1 apply(induct r2 r3 arbitrary: r1 rule: rrewrites.induct) - apply(auto) + apply(auto) done @@ -978,7 +992,8 @@ 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)" +lemma trivialbsimpsrewrites: + "\\x. x \ set rs \ x \* f x \ \ rs s\* (map f rs)" apply(induction rs) apply simp @@ -986,7 +1001,8 @@ by (metis insert_iff list.simps(15) list.simps(9) srewrites.simps) -lemma bsimp_AALTsrewrites: "AALTs bs1 rs \* bsimp_AALTs bs1 rs" +lemma bsimp_AALTsrewrites: + "AALTs bs1 rs \* bsimp_AALTs bs1 rs" apply(induction rs) apply simp apply(rule r_in_rstar) @@ -1000,12 +1016,14 @@ apply(simp) done -inductive frewrites:: "arexp list \ arexp list \ bool" (" _ f\* _" [100, 100] 100) - where -fs1: "[] f\* []" -|fs2: "\rs f\* rs'\ \ (AZERO#rs) f\* rs'" -|fs3: "\rs f\* rs'\ \ ((AALTs bs rs1) # rs) f\* ((map (fuse bs) rs1) @ rs')" -|fs4: "\rs f\* rs';nonalt r; nonazero r\ \ (r#rs) f\* (r#rs')" +(* rewrites for lists *) +inductive + frewrites:: "arexp list \ arexp list \ bool" (" _ f\* _" [100, 100] 100) +where + fs1: "[] f\* []" +| fs2: "\rs f\* rs'\ \ (AZERO#rs) f\* rs'" +| fs3: "\rs f\* rs'\ \ ((AALTs bs rs1) # rs) f\* ((map (fuse bs) rs1) @ rs')" +| fs4: "\rs f\* rs'; nonalt r; nonazero r\ \ (r#rs) f\* (r#rs')" @@ -1105,7 +1123,8 @@ apply auto by (metis split_list) -lemma alts_dBrewrites_withFront: " AALTs bs (rsa @ rs) \* AALTs bs (rsa @ distinctBy rs erase (erase ` set rsa))" +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) @@ -1154,16 +1173,13 @@ using alts_dBrewrites_withFront by (metis append_Nil dB_single_step empty_set image_empty) - - - - - lemma bsimp_rewrite: shows "r \* bsimp r" - apply(induction r rule: bsimp.induct) - apply simp - apply(case_tac "bsimp r1 = AZERO") +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") @@ -1172,37 +1188,28 @@ apply(subst bsimp_ASEQ2) apply (meson real_trans rrewrite.intros(3) rrewrites.intros(2) star_seq star_seq2) apply (smt (verit, best) bsimp_ASEQ0 bsimp_ASEQ1 real_trans rrewrite.intros(2) rs2 star_seq star_seq2) - defer - using bsimp_aalts_simpcases(2) apply blast - apply simp - apply simp - apply simp - - apply auto - - - apply(subgoal_tac "AALTs bs1 rs \* AALTs bs1 (map bsimp rs)") - apply(subgoal_tac "AALTs bs1 (map bsimp rs) \* AALTs bs1 (flts (map bsimp rs))") - apply(subgoal_tac "AALTs bs1 (flts (map bsimp rs)) \* AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {})") - apply(subgoal_tac "AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {}) \* bsimp_AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {} )") - - - apply (meson real_trans) - - apply (meson bsimp_AALTsrewrites) - - apply (meson alts_dBrewrites) - - using fltsrewrites apply auto[1] - - using alts_simpalts by force - - -lemma rewrite_non_nullable: "\r1 \ r2; \bnullable r1 \ \ \bnullable r2" - apply(induction r1 r2 rule: rrewrite.induct) - apply auto - apply (metis bnullable_correctness erase_fuse)+ 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_AALTsrewrites fltsrewrites real_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 rewrite_non_nullable_strong: assumes "r1 \ r2" @@ -1229,41 +1236,16 @@ apply simp using rewrite_non_nullable_strong by blast -lemma nonbnullable_lists_concat: " \ \ (\r0\set rs1. bnullable r0); \ bnullable r; \ (\r0\set rs2. bnullable r0)\ \ -\(\r0 \ (set (rs1@[r]@rs2)). bnullable r0 ) " - apply simp - apply blast - done - - -lemma nomember_bnullable: "\ \ (\r0\set rs1. bnullable r0); \ bnullable r; \ (\r0\set rs2. bnullable r0)\ - \ \bnullable (AALTs bs (rs1 @ [r] @ rs2))" - 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 r2 apply blast - apply(case_tac "bnullable r") - - apply blast - apply(case_tac "\r0\set rs2. bnullable r0") - - using bnullable.simps(4) apply presburger - apply(subgoal_tac "False") - - apply blast - - using nomember_bnullable by blast - - +lemma bnullable_segment: + "bnullable (AALTs bs (rs1@[r]@rs2)) \ bnullable (AALTs bs rs1) \ bnullable (AALTs bs rs2) \ bnullable r" + by auto lemma bnullablewhichbmkeps: "\bnullable (AALTs bs (rs1@[r]@rs2)); \ bnullable (AALTs bs rs1); bnullable r \ \ bmkeps (AALTs bs (rs1@[r]@rs2)) = bs @ (bmkeps r)" + using qq2 bnullable_Hdbmkeps_Hd by force - - lemma spillbmkepslistr: "bnullable (AALTs bs1 rs1) \ bmkeps (AALTs bs (AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs ( map (fuse bs1) rs1 @ rsb))" apply(subst bnullable_Hdbmkeps_Hd) @@ -1271,102 +1253,84 @@ apply simp by (metis bmkeps.simps(3) k0a list.set_intros(1) qq1 qq4 qs3) -lemma third_segment_bnullable: "\bnullable (AALTs bs (rs1@rs2@rs3)); \bnullable (AALTs bs rs1); \bnullable (AALTs bs rs2)\ \ -bnullable (AALTs bs rs3)" - - by (metis append.left_neutral append_Cons bnullable.simps(1) bnullable_segment rrewrite.intros(7) rewrite_non_nullable) +lemma third_segment_bnullable: + "\bnullable (AALTs bs (rs1@rs2@rs3)); \bnullable (AALTs bs rs1); \bnullable (AALTs bs rs2)\ \ + bnullable (AALTs bs rs3)" + apply(auto) + done +lemma third_segment_bmkeps: + "\bnullable (AALTs bs (rs1@rs2@rs3)); \bnullable (AALTs bs rs1); \bnullable (AALTs bs rs2)\ \ + bmkeps (AALTs bs (rs1@rs2@rs3) ) = bmkeps (AALTs bs rs3)" + by (metis bnullable.simps(1) bnullable.simps(4) bsimp_AALTs.simps(1) bsimp_AALTsrewrites qq2 rewritesnullable self_append_conv third_segment_bnullable) -lemma third_segment_bmkeps: "\bnullable (AALTs bs (rs1@rs2@rs3)); \bnullable (AALTs bs rs1); \bnullable (AALTs bs rs2)\ \ -bmkeps (AALTs bs (rs1@rs2@rs3) ) = bmkeps (AALTs bs rs3)" - 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 bnullable.simps(4) qq2) - - apply (metis append.assoc) - - apply (metis append.assoc in_set_conv_decomp r2 third_segment_bnullable) - - using third_segment_bnullable by blast - +lemma rewrite_bmkepsalt: + "\bnullable (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)); bnullable (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))\ + \ bmkeps (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))" + apply(rule qq3) + apply(simp) + apply(simp) + apply(case_tac "bnullable (AALTs bs1 rs1)") + using spillbmkepslistr apply blast + apply(subst qq2) + apply(auto simp add: bnullable_fuse r1) + done -lemma rewrite_bmkepsalt: " \bnullable (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)); bnullable (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))\ - \ bmkeps (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))" - apply(case_tac "bnullable (AALTs bs rsa)") - - using qq1 apply force - apply(case_tac "bnullable (AALTs bs1 rs1)") - apply(subst qq2) - - - using r2 apply blast - - apply (metis list.set_intros(1)) - apply (metis append_Nil bnullable.simps(1) rewrite_non_nullable_strong rrewrite.intros(10) spillbmkepslistr third_segment_bmkeps) - apply(subgoal_tac "bmkeps (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs rsb) ") - prefer 2 - - apply (metis append_Cons append_Nil bnullable.simps(1) bnullable_segment rewrite_nullable rrewrite.intros(10) third_segment_bmkeps) - by (metis bnullable.simps(4) rewrite_non_nullable_strong rrewrite.intros(9) third_segment_bmkeps) - +lemma rewrite_bmkeps_aux: + assumes "r1 \ r2" "bnullable r1" "bnullable r2" + shows "bmkeps r1 = bmkeps r2" + using assms +proof (induction r1 r2 rule: rrewrite.induct) + case (1 bs r2) + then show ?case by simp +next + case (2 bs r1) + then show ?case by simp +next + case (3 bs bs1 r) + then show ?case by (simp add: b2) +next + case (4 r1 r2 bs r3) + then show ?case by simp +next + case (5 r3 r4 bs r1) + then show ?case by simp +next + case (6 r r' bs rs1 rs2) + then show ?case + by (metis append_Cons append_Nil bnullable.simps(4) bnullable_segment bnullablewhichbmkeps qq3 r1 rewrite_non_nullable_strong) +next + case (7 bs rsa rsb) + then show ?case + by (metis bnullable.simps(1) bnullable.simps(4) bnullable_segment qq1 qq2 rewrite_nullable rrewrite.intros(10) rrewrite0away third_segment_bmkeps) +next + case (8 bs rsa bs1 rs1 rsb) + then show ?case + by (simp add: rewrite_bmkepsalt) +next + case (9 bs bs1 rs) + then show ?case + by (simp add: q3a) +next + case (10 bs) + then show ?case + by fastforce +next + case (11 bs r) + then show ?case + by (simp add: b2) +next + case (12 a1 a2 bs rsa rsb rsc) + then show ?case + by (smt (verit, ccfv_threshold) append_Cons append_eq_appendI append_self_conv2 bnullable_correctness list.set_intros(1) qq3 r1) +qed -lemma rewrite_bmkeps: "\ r1 \ r2; bnullable r1\ \ bmkeps r1 = bmkeps r2" - - apply(frule rewrite_nullable) - apply simp - apply(induction r1 r2 rule: rrewrite.induct) - apply simp - using bnullable.simps(1) bnullable.simps(5) apply blast - apply (simp add: b2) - apply simp - apply simp - apply(frule bnullable_segment) - apply(case_tac "bnullable (AALTs bs rs1)") - using qq1 apply force - apply(case_tac "bnullable r") - using bnullablewhichbmkeps rewrite_nullable apply presburger - apply(subgoal_tac "bnullable (AALTs bs rs2)") - apply(subgoal_tac "\ bnullable r'") - apply (simp add: qq2 r1) +lemma rewrite_bmkeps: + assumes "r1 \ r2" "bnullable r1" + shows "bmkeps r1 = bmkeps r2" + using assms(1) assms(2) rewrite_bmkeps_aux rewrite_nullable by blast - using rewrite_non_nullable apply blast - - apply blast - apply (simp add: flts_append qs3) - apply (simp add: rewrite_bmkepsalt) - using q3a apply force - - apply (simp add: q3a) - apply (simp add: b2) - apply(simp del: append.simps) - apply(case_tac "bnullable a1") - apply (metis append.assoc in_set_conv_decomp qq1) - apply(case_tac "\r \ set rsa. bnullable r") - using qq1 apply presburger - apply(case_tac "\r \ set rsb. bnullable r") - apply (metis UnCI append.assoc qq1 set_append) - apply(case_tac "bnullable a2") - apply (metis bnullable_correctness) - apply(subst qq2) - apply blast - apply(auto)[1] - apply(subst qq2) - apply (metis empty_iff list.set(1) set_ConsD) - apply(auto)[1] - apply(subst qq2) - apply(auto)[2] - apply(subst qq2) - apply(auto)[2] - apply(subst qq2) - apply(auto)[2] - apply(subst qq2) - apply(auto)[2] - apply(subst qq2) - apply(auto)[2] - apply(simp) - done lemma rewrites_bmkeps: assumes "r1 \* r2" "bnullable r1" @@ -1389,50 +1353,68 @@ lemma alts_rewrite_front: "r \ r' \ AALTs bs (r # rs) \ AALTs bs (r' # rs)" by (metis append_Cons append_Nil rrewrite.intros(6)) -lemma alt_rewrite_front: "r \ r' \ AALT bs r r2 \ AALT bs r' r2" - using alts_rewrite_front by blast - lemma to_zero_in_alt: " AALT bs (ASEQ [] AZERO r) r2 \ AALT bs AZERO r2" by (simp add: alts_rewrite_front rrewrite.intros(1)) -lemma alt_remove0_front: " AALT bs AZERO r \ AALTs bs [r]" - by (simp add: rrewrite0away) - -lemma alt_rewrites_back: "r2 \* r2' \AALT bs r1 r2 \* AALT bs r1 r2'" - apply(induction r2 r2' arbitrary: bs rule: rrewrites.induct) - apply simp - by (meson rs1 rs2 srewrites_alt1 ss1 ss2) - -lemma rewrite_fuse: " r2 \ r3 \ fuse bs r2 \* fuse bs r3" - apply(induction r2 r3 arbitrary: bs rule: rrewrite.induct) - apply auto - - apply (simp add: continuous_rewrite) - - apply (simp add: r_in_rstar rrewrite.intros(2)) - - apply (metis fuse_append r_in_rstar rrewrite.intros(3)) - - using r_in_rstar star_seq apply blast - - using r_in_rstar star_seq2 apply blast - - using contextrewrites2 r_in_rstar apply auto[1] - - using rrewrite.intros(8) apply auto[1] - using rrewrite.intros(7) apply auto[1] - using rrewrite.intros(8) apply force - apply (metis append_assoc r_in_rstar rrewrite.intros(9)) - apply (simp add: r_in_rstar rrewrite.intros(10)) - apply (metis fuse_append r_in_rstar rrewrite.intros(11)) - using rrewrite.intros(12) by auto - +lemma rewrite_fuse: + assumes "r2 \ r3" + shows "fuse bs r2 \* fuse bs r3" + using assms +proof(induction r2 r3 arbitrary: bs rule: rrewrite.induct) + case (1 bs r2) + then show ?case + by (simp add: continuous_rewrite) +next + case (2 bs r1) + then show ?case + using rrewrite.intros(2) by force +next + case (3 bs bs1 r) + then show ?case + by (metis fuse.simps(5) fuse_append r_in_rstar rrewrite.intros(3)) +next + case (4 r1 r2 bs r3) + then show ?case + by (simp add: r_in_rstar star_seq) +next + case (5 r3 r4 bs r1) + then show ?case + using fuse.simps(5) r_in_rstar star_seq2 by auto +next + case (6 r r' bs rs1 rs2) + then show ?case + using contextrewrites2 r_in_rstar by force +next + case (7 bs rsa rsb) + then show ?case + using rrewrite.intros(7) by force +next + case (8 bs rsa bs1 rs1 rsb) + then show ?case + using rrewrite.intros(8) by force +next + case (9 bs bs1 rs) + then show ?case + by (metis append.assoc fuse.simps(4) r_in_rstar rrewrite.intros(9)) +next + case (10 bs) + then show ?case + by (simp add: r_in_rstar rrewrite.intros(10)) +next + case (11 bs r) + then show ?case + by (metis fuse.simps(4) fuse_append r_in_rstar rrewrite.intros(11)) +next + case (12 a1 a2 bs rsa rsb rsc) + then show ?case + using fuse.simps(4) r_in_rstar rrewrite.intros(12) by auto +qed lemma rewrites_fuse: - assumes "r2 \* r2'" - shows "fuse bs1 r2 \* fuse bs1 r2'" + assumes "r1 \* r2" + shows "fuse bs r1 \* fuse bs r2" using assms -apply(induction r2 r2' arbitrary: bs1 rule: rrewrites.induct) +apply(induction r1 r2 arbitrary: bs rule: rrewrites.induct) apply(auto intro: rewrite_fuse real_trans) done @@ -1443,7 +1425,8 @@ done -lemma rewrite_der_altmiddle: "bder c (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) \* bder c (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))" +lemma rewrite_der_altmiddle: + "bder c (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) \* bder c (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))" apply simp apply(simp add: bder_fuse_list del: append.simps) by (metis append.assoc map_map r_in_rstar rrewrite.intros(8) threelistsappend) @@ -1456,63 +1439,72 @@ using rrewrite.intros(12) by auto -lemma rewrite_after_der: "r1 \ r2 \ (bder c r1) \* (bder c r2)" - apply(induction r1 r2 arbitrary: c rule: rrewrite.induct) - - apply (simp add: r_in_rstar rrewrite.intros(1)) - apply simp - - apply (meson contextrewrites1 r_in_rstar rrewrite.intros(10) rrewrite.intros(2) rrewrite0away rs2) - apply(simp) - apply(rule many_steps_later) - apply(rule to_zero_in_alt) - apply(rule many_steps_later) - apply(rule alt_remove0_front) - apply(rule many_steps_later) - apply(rule rrewrite.intros(11)) - using bder_fuse fuse_append rs1 apply presburger - apply(case_tac "bnullable r1") - prefer 2 - apply(subgoal_tac "\bnullable r2") - prefer 2 - using rewrite_non_nullable apply presburger - apply simp+ - - using star_seq apply auto[1] - apply(subgoal_tac "bnullable r2") - apply simp+ - apply(subgoal_tac "bmkeps r1 = bmkeps r2") - prefer 2 - using rewrite_bmkeps apply auto[1] - using contextrewrites1 star_seq apply auto[1] - using rewrite_nullable apply auto[1] - apply(case_tac "bnullable r1") - apply simp - apply(subgoal_tac "ASEQ [] (bder c r1) r3 \ ASEQ [] (bder c r1) r4") - prefer 2 - using rrewrite.intros(5) apply blast - apply(rule many_steps_later) - apply(rule alt_rewrite_front) - apply assumption - apply (meson alt_rewrites_back rewrites_fuse) - - apply (simp add: r_in_rstar rrewrite.intros(5)) - - using contextrewrites2 apply force - - using rrewrite.intros(7) apply force - - using rewrite_der_altmiddle apply auto[1] - - apply (metis bder.simps(4) bder_fuse_list map_map r_in_rstar rrewrite.intros(9)) - apply (simp add: r_in_rstar rrewrite.intros(10)) - - apply (simp add: r_in_rstar rrewrite.intros(10)) - using bder_fuse r_in_rstar rrewrite.intros(11) apply presburger - - - using lock_step_der_removal by auto - +lemma rewrite_after_der: + assumes "r1 \ r2" + shows "(bder c r1) \* (bder c r2)" + using assms +proof(induction r1 r2 rule: rrewrite.induct) + case (1 bs r2) + then show "bder c (ASEQ bs AZERO r2) \* bder c AZERO" + by (simp add: continuous_rewrite) +next + case (2 bs r1) + then show "bder c (ASEQ bs r1 AZERO) \* bder c AZERO" + apply(simp) + by (meson contextrewrites1 r_in_rstar real_trans rrewrite.intros(10) rrewrite.intros(2) rrewrite0away) +next + case (3 bs bs1 r) + then show "bder c (ASEQ bs (AONE bs1) r) \* bder c (fuse (bs @ bs1) r)" + apply(simp) + by (metis bder_fuse fuse_append rrewrite.intros(11) rrewrite0away rrewrites.simps to_zero_in_alt) +next + case (4 r1 r2 bs r3) + have as: "r1 \ r2" by fact + have IH: "bder c r1 \* bder c r2" by fact + from as IH show "bder c (ASEQ bs r1 r3) \* bder c (ASEQ bs r2 r3)" + by (simp add: contextrewrites1 rewrite_bmkeps rewrite_non_nullable_strong star_seq) +next + case (5 r3 r4 bs r1) + have as: "r3 \ r4" by fact + have IH: "bder c r3 \* bder c r4" by fact + from as IH show "bder c (ASEQ bs r1 r3) \* bder c (ASEQ bs r1 r4)" + apply(simp) + using r_in_rstar rewrites_fuse srewrites_alt1 ss1 ss2 star_seq2 by presburger +next + case (6 r r' bs rs1 rs2) + have as: "r \ r'" by fact + have IH: "bder c r \* bder c r'" by fact + from as IH show "bder c (AALTs bs (rs1 @ [r] @ rs2)) \* bder c (AALTs bs (rs1 @ [r'] @ rs2))" + apply(simp) + using contextrewrites2 by force +next + case (7 bs rsa rsb) + then show "bder c (AALTs bs (rsa @ [AZERO] @ rsb)) \* bder c (AALTs bs (rsa @ rsb))" + apply(simp) + using rrewrite.intros(7) by auto +next + case (8 bs rsa bs1 rs1 rsb) + then show + "bder c (AALTs bs (rsa @ [AALTs bs1 rs1] @ rsb)) \* bder c (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))" + using rewrite_der_altmiddle by auto +next + case (9 bs bs1 rs) + then show "bder c (AALTs (bs @ bs1) rs) \* bder c (AALTs bs (map (fuse bs1) rs))" + by (metis bder.simps(4) bder_fuse_list list.map_comp r_in_rstar rrewrite.intros(9)) +next + case (10 bs) + then show "bder c (AALTs bs []) \* bder c AZERO" + by (simp add: r_in_rstar rrewrite.intros(10)) +next + case (11 bs r) + then show "bder c (AALTs bs [r]) \* bder c (fuse bs r)" + by (simp add: bder_fuse r_in_rstar rrewrite.intros(11)) +next + case (12 a1 a2 bs rsa rsb rsc) + have as: "erase a1 = erase a2" by fact + then show "bder c (AALTs bs (rsa @ [a1] @ rsb @ [a2] @ rsc)) \* bder c (AALTs bs (rsa @ [a1] @ rsb @ rsc))" + using lock_step_der_removal by force +qed lemma rewrites_after_der: @@ -1523,6 +1515,7 @@ apply(simp_all add: rewrite_after_der real_trans) done + lemma central: shows "bders r s \* bders_simp r s" proof(induct s arbitrary: r rule: rev_induct) @@ -1540,20 +1533,27 @@ by (simp add: bders_simp_append) qed - lemma quasi_main: assumes "bnullable (bders r s)" shows "bmkeps (bders r s) = bmkeps (bders_simp r s)" - using assms central rewrites_bmkeps by blast + using assms central rewrites_bmkeps +proof - + have "bders r s \* bders_simp r s" by (rule central) + then + show "bmkeps (bders r s) = bmkeps (bders_simp r s)" using assms + by (rule rewrites_bmkeps) +qed + theorem main_main: shows "blexer r s = blexer_simp r s" - by (simp add: b4 blexer_def blexer_simp_def quasi_main) + unfolding blexer_def blexer_simp_def + using b4 quasi_main by simp theorem blexersimp_correctness: shows "lexer r s = blexer_simp r s" - using blexer_correctness main_main by auto + using blexer_correctness main_main by simp