
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 (\<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)"




