--- a/thys3/BlexerSimp.thy Thu Jul 21 20:22:35 2022 +0100
+++ b/thys3/BlexerSimp.thy Tue Aug 02 22:11:22 2022 +0100
@@ -303,27 +303,7 @@
apply(subgoal_tac "(cc @ a # dB6 cc' (tset (cc @ [a]))) s\<leadsto>* (cc @ (p6 cc a) # dB6 cc' (tset (cc @ [a])))")
sorry
-(*
-lemma ss6_stronger_aux:
- shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (set (map erase rs1)))"
- apply(induct rs2 arbitrary: rs1)
- apply simp
- apply(case_tac "erase a \<in> erase ` set rs1")
- apply(simp)
- apply(drule_tac x = "rs1" in meta_spec)
- apply(subgoal_tac "(rs1 @ a # rs2) s\<leadsto>* (rs1 @ rs2)")
- using srewrites_trans apply blast
- using deletes_dB apply presburger
- apply(case_tac "set (turnIntoTerms (erase a)) \<subseteq> erase ` set rs1")
-
- apply simp
- apply(auto)
- prefer 2
- apply(drule_tac x="rs1 @ [a]" in meta_spec)
- apply(simp)
- sorry
-*)
lemma ss6_stronger:
@@ -348,6 +328,7 @@
harmless sorry
*)
+
sorry
thm seqFold.simps
@@ -359,7 +340,8 @@
done
-lemma tint_seqFold_eq: shows"set (tint (seqFold (erase x42) [erase x43])) =
+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
@@ -377,18 +359,31 @@
-lemma top_bitcodes_preserved_p6:
- shows "\<lbrakk> r = ASEQ bs a1 a2 \<rbrakk> \<Longrightarrow> p6 as r = AZERO \<or> (\<exists>bs3. top (p6 as r) = bs @ bs3)"
- apply(induct r arbitrary: as)
- apply simp
- apply simp
- apply simp
- apply(case_tac "a1")
- apply simp
+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)
- sorry
+lemma p6pfuse_alts:
+ shows
+" \<And>bs\<^sub>0 as\<^sub>0.
+ \<lbrakk>\<And>a bs. set (tint (erase a)) = set (tint (erase (fuse bs a))); a = AALTs bs\<^sub>0 as\<^sub>0\<rbrakk>
+ \<Longrightarrow> \<not> set (tint (erase a)) \<subseteq> (\<Union>x\<in>set as. set (tint (erase x))) \<longrightarrow>
+ fuse bs
+ (case a of AZERO \<Rightarrow> AZERO | AONE x \<Rightarrow> AONE x | ACHAR x xa \<Rightarrow> ACHAR x xa
+ | ASEQ bs r1 r2 \<Rightarrow> bsimp_ASEQ bs (prune6 (\<Union>x\<in>set as. set (tint (erase x))) r1 [erase r2]) r2
+ | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r. prune6 (\<Union>x\<in>set as. set (tint (erase x))) r []) rs0)) | ASTAR x xa \<Rightarrow> ASTAR x xa)
+ =
+ (case fuse bs a of AZERO \<Rightarrow> AZERO | AONE x \<Rightarrow> AONE x | ACHAR x xa \<Rightarrow> ACHAR x xa
+ | ASEQ bs r1 r2 \<Rightarrow> bsimp_ASEQ bs (prune6 (\<Union>x\<in>set as. set (tint (erase x))) r1 [erase r2]) r2
+ | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r. prune6 (\<Union>x\<in>set as. set (tint (erase x))) r []) rs0)) | ASTAR x xa \<Rightarrow> ASTAR x xa)"
+ apply simp
+ using p6fa_aux by presburger
+
@@ -406,9 +401,27 @@
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 \<Longrightarrow> \<exists>bs3. bs' = bs @ bs3
+*)
+lemma top_bitcodes_preserved_p6:
+ shows "top r = bs \<Longrightarrow> p6 as r = AZERO \<or> (\<exists>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\<leadsto>* (as @ map (fuse bs) [p6 as a] @ as2)"
apply(subgoal_tac "map (fuse bs) [a] = [fuse bs a]")
@@ -567,7 +580,14 @@
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)
-qed (auto)
+next
+ prefer 10
+ case (ss7 as a as1)
+ then show ?case
+
+(*this sorry requires more effort*)
+ sorry
+qed(auto)
lemma rewrites_bmkeps:
assumes "r1 \<leadsto>* r2" "bnullable r1"
@@ -606,6 +626,12 @@
shows "(map f [a]) = [f a]"
by (simp)
+lemma "set (tint (erase a)) \<subseteq> (\<Union>x\<in>set as. set (tint (erase x))) \<Longrightarrow>
+ set (tint (erase (bder c a))) \<subseteq> (\<Union>x\<in>set (map (bder c) as). set (tint (erase x)))"
+
+ sorry
+
+
lemma rewrite_preserves_bder:
shows "r1 \<leadsto> r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)"
and "rs1 s\<leadsto> rs2 \<Longrightarrow> map (bder c) rs1 s\<leadsto>* map (bder c) rs2"
@@ -681,6 +707,11 @@
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:
@@ -733,18 +764,20 @@
by (metis rrewrites_trans star_seq star_seq2)
then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" by simp
}
- ultimately show "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" sorry
+ ultimately show "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)"
+ by blast
next
case (2 bs1 rs)
have IH: "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimpStrong6 x" by fact
then have "rs s\<leadsto>* (map bsimpStrong6 rs)" by (simp add: trivialbsimp_srewrites)
also have "... s\<leadsto>* flts (map bsimpStrong6 rs)" by (simp add: fltsfrewrites)
- also have "... s\<leadsto>* distinctWith (flts (map bsimpStrong6 rs)) eq1 {}" by (simp add: ss6_stronger)
- finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (distinctWith (flts (map bsimpStrong6 rs)) eq1 {})"
+ also have "... s\<leadsto>* dB6 (flts (map bsimpStrong6 rs)) {}" by (simp add: ss6_stronger)
+ finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (dB6 (flts (map bsimpStrong6 rs)) {})"
using contextrewrites0 by auto
- also have "... \<leadsto>* bsimp_AALTs bs1 (distinctWith (flts (map bsimpStrong6 rs)) eq1 {})"
+ also have "... \<leadsto>* bsimp_AALTs bs1 (dB6 (flts (map bsimpStrong6 rs)) {})"
by (simp add: bsimp_AALTs_rewrites)
- finally show "AALTs bs1 rs \<leadsto>* bsimpStrong6 (AALTs bs1 rs)" sorry
+ finally show "AALTs bs1 rs \<leadsto>* bsimpStrong6 (AALTs bs1 rs)"
+ using bsimpStrong6.simps(2) by presburger
qed (simp_all)