--- 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 (\<lambda>r11. furtherSEQ r11 r2) (turnIntoTerms r1))"
| "turnIntoTerms r = [r]"
-fun regConcat :: "rexp \<Rightarrow> rexp list \<Rightarrow> rexp" where
- "regConcat acc [] = acc"
-| "regConcat ONE (r # rs1) = regConcat r rs1"
-| "regConcat acc (r # rs1) = regConcat (SEQ acc r) rs1"
+abbreviation "tint \<equiv> turnIntoTerms"
+
+fun seqFold :: "rexp \<Rightarrow> rexp list \<Rightarrow> rexp" where
+ "seqFold acc [] = acc"
+| "seqFold ONE (r # rs1) = seqFold r rs1"
+| "seqFold acc (r # rs1) = seqFold (SEQ acc r) rs1"
+
fun attachCtx :: "arexp \<Rightarrow> rexp list \<Rightarrow> 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 \<Rightarrow> rexp set \<Rightarrow> bool" where
"rs1_subseteq_rs2 rs1 rs2 = (rs1 \<subseteq> rs2)"
+
fun notZero :: "arexp \<Rightarrow> bool" where
"notZero AZERO = True"
| "notZero _ = False"
+
fun tset :: "arexp list \<Rightarrow> rexp set" where
"tset rs = set (concat (map turnIntoTerms (map erase rs)))"
@@ -101,10 +105,14 @@
fun prune6 :: "rexp set \<Rightarrow> arexp \<Rightarrow> rexp list \<Rightarrow> 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) \<Rightarrow> bsimp_ASEQ bs (prune6 acc r1 (erase r2 # ctx)) r2
- | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r.(prune6 acc r ctx)) rs0))) )"
+ | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r.(prune6 acc r ctx)) rs0))
+ | r \<Rightarrow> r
+ )
+ )
+ "
abbreviation
- "p acc r \<equiv> prune6 (set (concat (map turnIntoTerms (map erase acc)) ) ) r Nil"
+ "p6 acc r \<equiv> prune6 (tset acc) r Nil"
fun dB6 :: "arexp list \<Rightarrow> rexp set \<Rightarrow> arexp list" where
@@ -154,8 +162,9 @@
| ss4: "(AZERO # rs) s\<leadsto> rs"
| ss5: "(AALTs bs1 rs1 # rsb) s\<leadsto> ((map (fuse bs1) rs1) @ rsb)"
| ss6: "L (erase a2) \<subseteq> L (erase a1) \<Longrightarrow> (rsa@[a1]@rsb@[a2]@rsc) s\<leadsto> (rsa@[a1]@rsb@rsc)"
-| ss7: " (as @ [a] @ as1) s\<leadsto> (as @ [prune6 (set (concat (map (\<lambda>r. turnIntoTerms (erase r)) as))) a Nil] @ as1)"
+| ss7: " (as @ [a] @ as1) s\<leadsto> (as @ [p6 as a] @ as1)"
+thm tset.simps
inductive
rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100)
@@ -291,10 +300,10 @@
apply(subgoal_tac "(cc @ a # cc') s\<leadsto>* (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\<leadsto>* (cc @ (p cc a) # dB6 cc' (tset (cc @ [a])))")
+ 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)
@@ -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\<leadsto>* (rs1 @ rs2)")
- using srewrites_trans apply blast
- apply(subgoal_tac "\<exists>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\<leadsto>* 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 \<Longrightarrow> \<exists>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 \<noteq> ONE \<Longrightarrow> 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\<leadsto>* (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\<leadsto>* (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\<leadsto>* (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 \<leadsto> r3 \<Longrightarrow> fuse bs r2 \<leadsto> 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 \<leadsto> r2 \<Longrightarrow> bnullable r1 = bnullable r2"
and "rs1 s\<leadsto> rs2 \<Longrightarrow> 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 \<leadsto> r2 \<Longrightarrow> (bnullable r1 \<and> bnullable r2 \<Longrightarrow> bmkeps r1 = bmkeps r2)"