diff -r 56057198e4f5 -r 70c10dc41606 thys3/BlexerSimp.thy --- a/thys3/BlexerSimp.thy Fri May 26 08:09:30 2023 +0100 +++ b/thys3/BlexerSimp.thy Fri May 26 08:10:17 2023 +0100 @@ -2,6 +2,35 @@ imports Blexer begin +fun distinctWith :: "'a list \ ('a \ 'a \ bool) \ 'a set \ 'a list" + where + "distinctWith [] eq acc = []" +| "distinctWith (x # xs) eq acc = + (if (\ y \ acc. eq x y) then distinctWith xs eq acc + else x # (distinctWith xs eq ({x} \ acc)))" + + +fun eq1 ("_ ~1 _" [80, 80] 80) where + "AZERO ~1 AZERO = True" +| "(AONE bs1) ~1 (AONE bs2) = True" +| "(ACHAR bs1 c) ~1 (ACHAR bs2 d) = (if c = d then True else False)" +| "(ASEQ bs1 ra1 ra2) ~1 (ASEQ bs2 rb1 rb2) = (ra1 ~1 rb1 \ ra2 ~1 rb2)" +| "(AALTs bs1 []) ~1 (AALTs bs2 []) = True" +| "(AALTs bs1 (r1 # rs1)) ~1 (AALTs bs2 (r2 # rs2)) = (r1 ~1 r2 \ (AALTs bs1 rs1) ~1 (AALTs bs2 rs2))" +| "(ASTAR bs1 r1) ~1 (ASTAR bs2 r2) = r1 ~1 r2" +| "(ANTIMES bs1 r1 n1) ~1 (ANTIMES bs2 r2 n2) = (r1 ~1 r2 \ n1 = n2)" +| "_ ~1 _ = False" + + + +lemma eq1_L: + assumes "x ~1 y" + shows "L (erase x) = L (erase y)" + using assms + apply(induct rule: eq1.induct) + apply(auto elim: eq1.elims) + apply presburger + done fun flts :: "arexp list \ arexp list" where @@ -42,11 +71,42 @@ | "bsimp_AALTs bs1 [r] = fuse bs1 r" | "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 (distinctWith (flts (map bsimp rs)) eq1 {}) " +| "bsimp r = r" + + +fun + bders_simp :: "arexp \ string \ arexp" +where + "bders_simp r [] = r" +| "bders_simp r (c # s) = bders_simp (bsimp (bder c r)) s" + +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" + + + +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_all) + done + lemma bmkeps_fuse: assumes "bnullable r" shows "bmkeps (fuse bs r) = bs @ bmkeps r" using assms - by (induct r rule: bnullable.induct) (auto) + apply(induct r rule: bnullable.induct) + apply(auto) + apply (metis append.assoc bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4)) + done lemma bmkepss_fuse: assumes "bnullables rs" @@ -65,84 +125,6 @@ -fun ABIncludedByC :: "'a \ 'b \ 'c \ ('a \ 'b \ 'c) \ ('c \ 'c \ bool) \ bool" where - "ABIncludedByC a b c f subseteqPred = subseteqPred (f a b) c" - -fun furtherSEQ :: "rexp \ rexp \ rexp list" and - turnIntoTerms :: "rexp \ rexp list " - where - "furtherSEQ ONE r2 = turnIntoTerms r2 " -| "furtherSEQ r11 r2 = [SEQ r11 r2]" -| "turnIntoTerms (SEQ ONE r2) = turnIntoTerms r2" -| "turnIntoTerms (SEQ r1 r2) = concat (map (\r11. furtherSEQ r11 r2) (turnIntoTerms r1))" -| "turnIntoTerms r = [r]" - -abbreviation "tint \ turnIntoTerms" - -fun seqFold :: "rexp \ rexp list \ rexp" where - "seqFold acc [] = acc" -| "seqFold ONE (r # rs1) = seqFold r rs1" -| "seqFold acc (r # rs1) = seqFold (SEQ acc r) rs1" - - -fun attachCtx :: "arexp \ rexp list \ rexp set" where - "attachCtx r ctx = set (turnIntoTerms (seqFold (erase r) ctx))" - - -fun rs1_subseteq_rs2 :: "rexp set \ rexp set \ bool" where - "rs1_subseteq_rs2 rs1 rs2 = (rs1 \ rs2)" - - -fun notZero :: "arexp \ bool" where - "notZero AZERO = True" -| "notZero _ = False" - - -fun tset :: "arexp list \ rexp set" where - "tset rs = set (concat (map turnIntoTerms (map erase rs)))" - - -fun prune6 :: "rexp set \ arexp \ rexp list \ arexp" where - "prune6 acc a ctx = (if (ABIncludedByC a ctx acc attachCtx rs1_subseteq_rs2) then AZERO else - (case a of (ASEQ bs r1 r2) \ bsimp_ASEQ bs (prune6 acc r1 (erase r2 # ctx)) r2 - | AALTs bs rs0 \ bsimp_AALTs bs (filter notZero (map (\r.(prune6 acc r ctx)) rs0)) - | r \ r - ) - ) - " - -abbreviation - "p6 acc r \ prune6 (tset acc) r Nil" - - -fun dB6 :: "arexp list \ rexp set \ arexp list" where - "dB6 [] acc = []" -| "dB6 (a # as) acc = (if (erase a \ acc) then (dB6 as acc) - else (let pruned = prune6 acc a [] in - (case pruned of - AZERO \ dB6 as acc - |xPrime \ xPrime # (dB6 as ( (set (turnIntoTerms (erase pruned))) \ acc) ) ) )) " - - -fun bsimpStrong6 :: "arexp \ arexp" - where - "bsimpStrong6 (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)" -| "bsimpStrong6 (AALTs bs1 rs) = bsimp_AALTs bs1 (dB6 (flts (map bsimpStrong6 rs)) {}) " -| "bsimpStrong6 r = r" - - -fun - bdersStrong6 :: "arexp \ string \ arexp" -where - "bdersStrong6 r [] = r" -| "bdersStrong6 r (c # s) = bdersStrong6 (bsimpStrong6 (bder c r)) s" - -definition blexerStrong where - "blexerStrong r s \ if bnullable (bdersStrong6 (intern r) s) then - decode (bmkeps (bdersStrong6 (intern r) s)) r else None" - - - inductive rrewrite:: "arexp \ arexp \ bool" ("_ \ _" [99, 99] 99) and @@ -162,9 +144,7 @@ | ss4: "(AZERO # rs) s\ rs" | ss5: "(AALTs bs1 rs1 # rsb) s\ ((map (fuse bs1) rs1) @ rsb)" | ss6: "L (erase a2) \ L (erase a1) \ (rsa@[a1]@rsb@[a2]@rsc) s\ (rsa@[a1]@rsb@rsc)" -| ss7: " (as @ [a] @ as1) s\ (as @ [p6 as a] @ as1)" -thm tset.simps inductive rrewrites:: "arexp \ arexp \ bool" ("_ \* _" [100, 100] 100) @@ -203,6 +183,8 @@ apply(auto) done + + lemma contextrewrites0: "rs1 s\* rs2 \ AALTs bs rs1 \* AALTs bs rs2" apply(induct rs1 rs2 rule: srewrites.inducts) @@ -227,24 +209,17 @@ apply(auto) using srewrite1 by blast -lemma srewrites_prepend: - shows "rs1 s\* rs2 \ (r # rs1) s\* (r # rs2)" - by (metis append_Cons append_Nil srewrites1) - lemma srewrite2: shows "r1 \ r2 \ True" and "rs1 s\ rs2 \ (rs1 @ rs) s\* (rs2 @ rs)" - apply(induct arbitrary: rs rule: rrewrite_srewrite.inducts) - apply simp+ - using srewrites_prepend apply force - apply (simp add: rs_in_rstar ss3) - using ss4 apply force - using rs_in_rstar ss5 apply auto[1] - using rs_in_rstar ss6 apply auto[1] - using rs_in_rstar ss7 by force - - - + apply(induct rule: rrewrite_srewrite.inducts) + apply(auto) + apply (metis append_Cons append_Nil srewrites1) + apply(meson srewrites.simps ss3) + apply (meson srewrites.simps ss4) + apply (meson srewrites.simps ss5) + by (metis append_Cons append_Nil srewrites.simps ss6) + lemma srewrites3: shows "rs1 s\* rs2 \ (rs1 @ rs) s\* (rs2 @ rs)" @@ -252,6 +227,15 @@ apply(auto) by (meson srewrite2(2) srewrites_trans) +(* +lemma srewrites4: + assumes "rs3 s\* rs4" "rs1 s\* rs2" + shows "(rs1 @ rs3) s\* (rs2 @ rs4)" + using assms + apply(induct rs3 rs4 arbitrary: rs1 rs2 rule: srewrites.induct) + apply (simp add: srewrites3) + using srewrite1 by blast +*) lemma srewrites6: assumes "r1 \* r2" @@ -267,178 +251,27 @@ using assms by (smt (verit, best) append_Cons append_Nil srewrites1 srewrites3 srewrites6 srewrites_trans) -(*harmless sorry*) -lemma existing_preimage : - shows "f a \ f ` set rs1 \ \rs1a rs1b x. rs1 = rs1a @ [x] @ rs1b \ f x = f a " - apply(induct rs1) - apply simp - apply(case_tac "f a = f aa") - - sorry - - -lemma deletes_dB: - shows " \erase a \ erase ` set rs1\ \ (rs1 @ a # rs2) s\* (rs1 @ rs2)" - apply(subgoal_tac "\rs1a rs1b x. rs1 = rs1a @ [x] @ rs1b \ erase x = erase a") +lemma ss6_stronger_aux: + shows "(rs1 @ rs2) s\* (rs1 @ distinctWith rs2 eq1 (set rs1))" + apply(induct rs2 arbitrary: rs1) + apply(auto) prefer 2 - apply (meson existing_preimage) + 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 - apply(subgoal_tac "(rs1a @ [x] @ rs1b @ [a] @ rs2) s\ (rs1a @ [x] @ rs1b @ rs2)") - apply (simp add: rs_in_rstar) - apply(subgoal_tac "L (erase a) \ L (erase x)") - using ss6 apply presburger - by simp - - - -lemma ss6_realistic: - shows "(rs1 @ rs2) s\* (rs1 @ dB6 rs2 (tset rs1))" - apply(induct rs2 arbitrary: rs1) - apply simp - apply(rename_tac cc' cc) - apply(subgoal_tac "(cc @ a # cc') s\* (cc @ a # dB6 cc' (tset (cc @ [a])))") - prefer 2 - apply (metis append.assoc append.left_neutral append_Cons) - apply(subgoal_tac "(cc @ a # dB6 cc' (tset (cc @ [a]))) s\* (cc @ (p6 cc a) # dB6 cc' (tset (cc @ [a])))") - sorry - - - + apply(simp) + using eq1_L rs_in_rstar ss6 by force lemma ss6_stronger: - shows "rs1 s\* dB6 rs1 {}" - using ss6 - by (metis append_Nil concat.simps(1) list.set(1) list.simps(8) ss6_realistic tset.simps) - - -lemma tint_fuse: - shows "tint (erase a) = tint (erase (fuse bs a))" - by (simp add: erase_fuse) - -lemma tint_fuse2: - shows " set (tint (erase a)) = - set (tint (erase (fuse bs a)))" - using tint_fuse by auto - -lemma fused_bits_at_head: - shows "fuse bs a = ASEQ bs1 a1 a2 \ \bs2. bs1 = bs @ bs2" - -(* by (smt (verit) arexp.distinct(13) arexp.distinct(19) arexp.distinct(25) arexp.distinct(27) arexp.distinct(5) arexp.inject(3) fuse.elims) -harmless sorry -*) - - - sorry - -thm seqFold.simps - -lemma seqFold_concats: - shows "r \ ONE \ seqFold r [r1] = SEQ r r1" - apply(case_tac r) - apply simp+ -done - - -lemma tint_seqFold_eq: shows -"set (tint (seqFold (erase x42) [erase x43])) = - set (tint (SEQ (erase x42) (erase x43)))" - apply(case_tac "erase x42 = ONE") - apply simp - using seqFold_concats - apply simp - done - -fun top :: "arexp \ bit list" where - "top AZERO = []" -| "top (AONE bs) = bs" -| "top (ASEQ bs r1 r2) = bs" -| "top (ACHAR v va) = v" -| "top (AALTs v va) = v" -| "top (ASTAR v va) = v " - - - - -lemma p6fa_aux: - shows " fuse bs - (bsimp_AALTs bs\<^sub>0 as) = - - (bsimp_AALTs (bs @ bs\<^sub>0) as)" - by (metis bsimp_AALTs.simps(1) bsimp_AALTs.simps(2) bsimp_AALTs.simps(3) fuse.simps(1) fuse.simps(4) fuse_append neq_Nil_conv) - + shows "rs1 s\* distinctWith rs1 eq1 {}" + by (metis append_Nil list.set(1) ss6_stronger_aux) -lemma p6pfuse_alts: - shows -" \bs\<^sub>0 as\<^sub>0. - \\a bs. set (tint (erase a)) = set (tint (erase (fuse bs a))); a = AALTs bs\<^sub>0 as\<^sub>0\ - \ \ set (tint (erase a)) \ (\x\set as. set (tint (erase x))) \ - fuse bs - (case a of AZERO \ AZERO | AONE x \ AONE x | ACHAR x xa \ ACHAR x xa - | ASEQ bs r1 r2 \ bsimp_ASEQ bs (prune6 (\x\set as. set (tint (erase x))) r1 [erase r2]) r2 - | AALTs bs rs0 \ bsimp_AALTs bs (filter notZero (map (\r. prune6 (\x\set as. set (tint (erase x))) r []) rs0)) | ASTAR x xa \ ASTAR x xa) - = - (case fuse bs a of AZERO \ AZERO | AONE x \ AONE x | ACHAR x xa \ ACHAR x xa - | ASEQ bs r1 r2 \ bsimp_ASEQ bs (prune6 (\x\set as. set (tint (erase x))) r1 [erase r2]) r2 - | AALTs bs rs0 \ bsimp_AALTs bs (filter notZero (map (\r. prune6 (\x\set as. set (tint (erase x))) r []) rs0)) | ASTAR x xa \ ASTAR x xa)" - apply simp - using p6fa_aux by presburger - - - - -lemma prune6_preserves_fuse: - shows "fuse bs (p6 as a) = p6 as (fuse bs a)" - using tint_fuse2 - apply simp - apply(case_tac a) - apply simp - apply simp - apply simp - - using fused_bits_at_head - - apply simp - using tint_seqFold_eq - apply simp - apply (smt (z3) bsimp_ASEQ.simps(1) bsimp_ASEQ0 bsimp_ASEQ1 bsimp_ASEQ2 fuse.simps(1) fuse.simps(5) fuse_append) - using p6pfuse_alts apply presburger - by simp - - -(* -The top-level bitlist stays the same: -\<^sub>b\<^sub>sa ------pruning-----> \<^sub>b\<^sub>s\<^sub>' b \ \bs3. bs' = bs @ bs3 -*) -lemma top_bitcodes_preserved_p6: - shows "top r = bs \ p6 as r = AZERO \ (\bs3. top (p6 as r) = bs @ bs3)" - - - apply(induct r arbitrary: as) - -(*this sorry requires more care *) - - sorry - - - -corollary prune6_preserves_fuse_srewrite: - shows "(as @ map (fuse bs) [a] @ as2) s\* (as @ map (fuse bs) [p6 as a] @ as2)" - apply(subgoal_tac "map (fuse bs) [a] = [fuse bs a]") - apply(subgoal_tac "(as @ [fuse bs a] @ as2) s\* (as @ [ (p6 as (fuse bs a))] @ as2)") - using prune6_preserves_fuse apply auto[1] - using rs_in_rstar ss7 apply presburger - by simp - -lemma prune6_invariant_fuse: - shows "p6 as a = p6 (map (fuse bs) as) a" - apply simp - using erase_fuse by presburger - - -lemma p6pfs_cor: - shows "(map (fuse bs) as @ map (fuse bs) [a] @ map (fuse bs) as1) s\* (map (fuse bs) as @ map (fuse bs) [p6 as a] @ map (fuse bs) as1)" - by (metis prune6_invariant_fuse prune6_preserves_fuse_srewrite) lemma rewrite_preserves_fuse: shows "r2 \ r3 \ fuse bs r2 \ fuse bs r3" @@ -468,13 +301,7 @@ then show ?case apply(simp only: map_append) by (smt (verit, best) erase_fuse list.simps(8) list.simps(9) rrewrite_srewrite.ss6 srewrites.simps) -next - case (ss7 as a as1) - then show ?case - apply(simp only: map_append) - using p6pfs_cor by presburger qed (auto intro: rrewrite_srewrite.intros) - lemma rewrites_fuse: @@ -507,12 +334,17 @@ 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 \* bsimpStrong6 (AONE bs)" - and "AZERO \* bsimpStrong6 AZERO" - and "ACHAR bs c \* bsimpStrong6 (ACHAR bs c)" + shows "AONE bs \* bsimp (AONE bs)" + and "AZERO \* bsimp AZERO" + and "ACHAR bs c \* bsimp (ACHAR bs c)" by (simp_all) lemma bsimp_AALTs_rewrites: @@ -535,20 +367,17 @@ using rs1 srewrites7 apply presburger using srewrites7 apply force apply (simp add: srewrites7) + apply(simp add: srewrites7) by (simp add: srewrites7) + lemma bnullable0: shows "r1 \ r2 \ bnullable r1 = bnullable r2" and "rs1 s\ rs2 \ bnullables rs1 = bnullables rs2" - apply(induct rule: rrewrite_srewrite.inducts) - apply simp - apply simp - apply (simp add: bnullable_fuse) - using bnullable.simps(5) apply presburger - apply simp - apply simp - sorry - + apply(induct rule: rrewrite_srewrite.inducts) + apply(auto simp add: bnullable_fuse) + apply (meson UnCI bnullable_fuse imageI) + using bnullable_correctness nullable_correctness by blast lemma rewritesnullable: @@ -557,7 +386,7 @@ using assms apply(induction r1 r2 rule: rrewrites.induct) apply simp - using bnullable0(1) by presburger + using bnullable0(1) by auto lemma rewrite_bmkeps_aux: shows "r1 \ r2 \ (bnullable r1 \ bnullable r2 \ bmkeps r1 = bmkeps r2)" @@ -575,19 +404,22 @@ next case (ss5 bs1 rs1 rsb) then show ?case - by (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse) + apply (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse) + apply(case_tac rs1) + apply(auto simp add: bnullable_fuse) + apply (metis bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4)) + apply (metis bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4)) + apply (metis bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4)) + by (metis bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4)) next case (ss6 a1 a2 rsa rsb rsc) then show ?case by (smt (verit, best) Nil_is_append_conv bmkepss1 bmkepss2 bnullable_correctness in_set_conv_decomp list.distinct(1) list.set_intros(1) nullable_correctness set_ConsD subsetD) next - prefer 10 - case (ss7 as a as1) + case (bs10 rs1 rs2 bs) then show ?case - -(*this sorry requires more effort*) - sorry -qed(auto) + by (metis bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4)) +qed (auto) lemma rewrites_bmkeps: assumes "r1 \* r2" "bnullable r1" @@ -609,6 +441,50 @@ 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\* distinctWith (flts (map bsimp rs)) eq1 {}" by (simp add: ss6_stronger) + finally have "AALTs bs1 rs \* AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {})" + using contextrewrites0 by auto + also have "... \* bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {})" + by (simp add: bsimp_AALTs_rewrites) + finally show "AALTs bs1 rs \* bsimp (AALTs bs1 rs)" by simp +qed (simp_all) + lemma to_zero_in_alt: shows "AALT bs (ASEQ [] AZERO r) r2 \ AALT bs AZERO r2" @@ -626,12 +502,6 @@ shows "(map f [a]) = [f a]" by (simp) -lemma "set (tint (erase a)) \ (\x\set as. set (tint (erase x))) \ - set (tint (erase (bder c a))) \ (\x\set (map (bder c) as). set (tint (erase x)))" - - sorry - - 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" @@ -707,11 +577,6 @@ apply(rule_tac rrewrite_srewrite.ss6) using Der_def der_correctness apply auto[1] by blast -next - case (ss7 as a as1) - then show ?case - apply simp - sorry qed lemma rewrites_preserves_bder: @@ -720,105 +585,49 @@ using assms apply(induction r1 r2 rule: rrewrites.induct) apply(simp_all add: rewrite_preserves_bder rrewrites_trans) - done - +done -lemma bders_simp_appendStrong : - shows "bdersStrong6 r (s1 @ s2) = bdersStrong6 (bdersStrong6 r s1) s2" - apply(induct s1 arbitrary: s2 rule: rev_induct) - apply simp - apply auto - done +lemma central: + shows "bders r s \* bders_simp r s" +proof(induct s arbitrary: r rule: rev_induct) + case Nil + then show "bders r [] \* bders_simp r []" by simp +next + case (snoc x xs) + 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_preserves_bder) + also have "... \* bders_simp (bders_simp r xs) [x]" using IH + 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 main_aux: + assumes "bnullable (bders r s)" + shows "bmkeps (bders r s) = bmkeps (bders_simp r s)" +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 -lemma rewrites_to_bsimpStrong: - shows "r \* bsimpStrong6 r" -proof (induction r rule: bsimpStrong6.induct) - case (1 bs1 r1 r2) - have IH1: "r1 \* bsimpStrong6 r1" by fact - have IH2: "r2 \* bsimpStrong6 r2" by fact - { assume as: "bsimpStrong6 r1 = AZERO \ bsimpStrong6 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 \* bsimpStrong6 (ASEQ bs1 r1 r2)" using as by auto - } - moreover - { assume "\bs. bsimpStrong6 r1 = AONE bs" - then obtain bs where as: "bsimpStrong6 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) (bsimpStrong6 r2)" - using rewrites_fuse by (meson rrewrites_trans) - then have "ASEQ bs1 r1 r2 \* bsimpStrong6 (ASEQ bs1 (AONE bs) r2)" by simp - then have "ASEQ bs1 r1 r2 \* bsimpStrong6 (ASEQ bs1 r1 r2)" by (simp add: as) - } - moreover - { assume as1: "bsimpStrong6 r1 \ AZERO" "bsimpStrong6 r2 \ AZERO" and as2: "(\bs. bsimpStrong6 r1 = AONE bs)" - then have "bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2) = ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)" - by (simp add: bsimp_ASEQ1) - then have "ASEQ bs1 r1 r2 \* bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)" using as1 as2 IH1 IH2 - by (metis rrewrites_trans star_seq star_seq2) - then have "ASEQ bs1 r1 r2 \* bsimpStrong6 (ASEQ bs1 r1 r2)" by simp - } - ultimately show "ASEQ bs1 r1 r2 \* bsimpStrong6 (ASEQ bs1 r1 r2)" - by blast -next - case (2 bs1 rs) - have IH: "\x. x \ set rs \ x \* bsimpStrong6 x" by fact - then have "rs s\* (map bsimpStrong6 rs)" by (simp add: trivialbsimp_srewrites) - also have "... s\* flts (map bsimpStrong6 rs)" by (simp add: fltsfrewrites) - also have "... s\* dB6 (flts (map bsimpStrong6 rs)) {}" by (simp add: ss6_stronger) - finally have "AALTs bs1 rs \* AALTs bs1 (dB6 (flts (map bsimpStrong6 rs)) {})" - using contextrewrites0 by auto - also have "... \* bsimp_AALTs bs1 (dB6 (flts (map bsimpStrong6 rs)) {})" - by (simp add: bsimp_AALTs_rewrites) - finally show "AALTs bs1 rs \* bsimpStrong6 (AALTs bs1 rs)" - using bsimpStrong6.simps(2) by presburger -qed (simp_all) +theorem main_blexer_simp: + shows "blexer r s = blexer_simp r s" + unfolding blexer_def blexer_simp_def + by (metis central main_aux rewritesnullable) + +theorem blexersimp_correctness: + shows "lexer r s = blexer_simp r s" + using blexer_correctness main_blexer_simp by simp - - -lemma centralStrong: - shows "bders r s \* bdersStrong6 r s" -proof(induct s arbitrary: r rule: rev_induct) - case Nil - then show "bders r [] \* bdersStrong6 r []" by simp -next - case (snoc x xs) - have IH: "\r. bders r xs \* bdersStrong6 r xs" by fact - have "bders r (xs @ [x]) = bders (bders r xs) [x]" by (simp add: bders_append) - also have "... \* bders (bdersStrong6 r xs) [x]" using IH - by (simp add: rewrites_preserves_bder) - also have "... \* bdersStrong6 (bdersStrong6 r xs) [x]" using IH - by (simp add: rewrites_to_bsimpStrong) - finally show "bders r (xs @ [x]) \* bdersStrong6 r (xs @ [x])" - by (simp add: bders_simp_appendStrong) -qed - -lemma mainStrong: - assumes "bnullable (bders r s)" - shows "bmkeps (bders r s) = bmkeps (bdersStrong6 r s)" -proof - - have "bders r s \* bdersStrong6 r s" - using centralStrong by force - then - show "bmkeps (bders r s) = bmkeps (bdersStrong6 r s)" - using assms rewrites_bmkeps by blast -qed - - - - -theorem blexerStrong_correct : - shows "blexerStrong r s = blexer r s" - unfolding blexerStrong_def blexer_def - by (metis centralStrong mainStrong rewritesnullable) - - +unused_thms end