diff -r 57e33978e55d -r 3cbcd7cda0a9 thys3/BlexerSimp.thy --- a/thys3/BlexerSimp.thy Tue Jul 05 00:42:06 2022 +0100 +++ b/thys3/BlexerSimp.thy Wed Jul 13 08:27:28 2022 +0100 @@ -77,23 +77,27 @@ | "turnIntoTerms (SEQ r1 r2) = concat (map (\r11. furtherSEQ r11 r2) (turnIntoTerms r1))" | "turnIntoTerms r = [r]" -fun regConcat :: "rexp \ rexp list \ rexp" where - "regConcat acc [] = acc" -| "regConcat ONE (r # rs1) = regConcat r rs1" -| "regConcat acc (r # rs1) = regConcat (SEQ acc r) rs1" +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 (regConcat (erase r) ctx))" - + "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)))" @@ -101,10 +105,14 @@ 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))) )" + | AALTs bs rs0 \ bsimp_AALTs bs (filter notZero (map (\r.(prune6 acc r ctx)) rs0)) + | r \ r + ) + ) + " abbreviation - "p acc r \ prune6 (set (concat (map turnIntoTerms (map erase acc)) ) ) r Nil" + "p6 acc r \ prune6 (tset acc) r Nil" fun dB6 :: "arexp list \ rexp set \ arexp list" where @@ -154,8 +162,9 @@ | 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 @ [prune6 (set (concat (map (\r. turnIntoTerms (erase r)) as))) a Nil] @ as1)" +| ss7: " (as @ [a] @ as1) s\ (as @ [p6 as a] @ as1)" +thm tset.simps inductive rrewrites:: "arexp \ arexp \ bool" ("_ \* _" [100, 100] 100) @@ -291,10 +300,10 @@ 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 @ (p cc a) # dB6 cc' (tset (cc @ [a])))") + apply(subgoal_tac "(cc @ a # dB6 cc' (tset (cc @ [a]))) s\* (cc @ (p6 cc a) # dB6 cc' (tset (cc @ [a])))") sorry - +(* lemma ss6_stronger_aux: shows "(rs1 @ rs2) s\* (rs1 @ dB6 rs2 (set (map erase rs1)))" apply(induct rs2 arbitrary: rs1) @@ -313,22 +322,83 @@ 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) - using eq1_L rs_in_rstar ss sorry +*) 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 "set (tint (seqFold (erase x42) [erase x43])) = + set (tint (SEQ (erase x42) (erase x43)))" + apply(case_tac "erase x42 = ONE") + apply simp + apply simp + +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 + apply(case_tac "erase x42 = ONE") + apply simp + + 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" @@ -358,7 +428,13 @@ 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: @@ -424,11 +500,14 @@ lemma bnullable0: shows "r1 \ r2 \ bnullable r1 = bnullable r2" 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) - using bnullable_correctness nullable_correctness by blast - + 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 @@ -438,7 +517,7 @@ using assms apply(induction r1 r2 rule: rrewrites.induct) apply simp - using bnullable0(1) by auto + using bnullable0(1) by presburger lemma rewrite_bmkeps_aux: shows "r1 \ r2 \ (bnullable r1 \ bnullable r2 \ bmkeps r1 = bmkeps r2)"