--- a/thys2/SizeBound4.thy	Sat Feb 05 18:24:37 2022 +0000
+++ b/thys2/SizeBound4.thy	Sun Feb 06 00:02:04 2022 +0000
@@ -206,7 +206,7 @@
      (if bnullable r1
       then AALT bs (ASEQ [] (bder c r1) r2) (fuse (bmkeps r1) (bder c r2))
       else ASEQ bs (bder c r1) r2)"
-| "bder c (ASTAR bs r) = ASEQ bs (fuse [Z] (bder c r)) (ASTAR [] r)"
+| "bder c (ASTAR bs r) = ASEQ (bs @ [Z]) (bder c r) (ASTAR [] r)"
 
 
 fun 
@@ -566,8 +566,10 @@
 | ss3:  "r1 \<leadsto> r2 \<Longrightarrow> (r1 # rs) s\<leadsto> (r2 # rs)"
 | ss4:  "(AZERO # rs) s\<leadsto> rs"
 | ss5:  "(AALTs bs1 rs1 # rsb) s\<leadsto> ((map (fuse bs1) rs1) @ rsb)"
-| ss6:  "erase a1 = erase a2 \<Longrightarrow> (rsa@[a1]@rsb@[a2]@rsc) s\<leadsto> (rsa@[a1]@rsb@rsc)"
-
+| ss6:  "L(erase a2) \<subseteq> L(erase a1) \<Longrightarrow> (rsa@[a1]@rsb@[a2]@rsc) s\<leadsto> (rsa@[a1]@rsb@rsc)"
+(*| extra: "bnullable r1 \<Longrightarrow> ASEQ bs0 (ASEQ bs1 r1 r2) r3 \<leadsto>
+            ASEQ (bs0 @ bs1) r1 (ASEQ [] r2 r3)"
+*)
 
 inductive 
   rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100)
@@ -586,6 +588,10 @@
   shows "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
   using rrewrites.intros(1) rrewrites.intros(2) by blast
 
+lemma rs_in_rstar: 
+  shows "r1 s\<leadsto> r2 \<Longrightarrow> r1 s\<leadsto>* r2"
+  using rrewrites.intros(1) rrewrites.intros(2) by blast
+
 lemma rrewrites_trans[trans]: 
   assumes a1: "r1 \<leadsto>* r2"  and a2: "r2 \<leadsto>* r3"
   shows "r1 \<leadsto>* r3"
@@ -674,10 +680,19 @@
   shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ distinctBy rs2 erase (set (map erase rs1)))"
   apply(induct rs2 arbitrary: rs1)
    apply(auto)
-  apply (smt (verit, best) append.assoc append.right_neutral append_Cons append_Nil split_list srewrite2(2) srewrites_trans ss6)
+  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)
-  done
+  using ss6[simplified]
+  using rs_in_rstar by force
 
 lemma ss6_stronger:
   shows "rs1 s\<leadsto>* distinctBy rs1 erase {}"
@@ -710,12 +725,17 @@
   finally show "map (fuse bs) (AALTs bs1 rs1 # rsb) s\<leadsto> map (fuse bs) (map (fuse bs1) rs1 @ rsb)"
     by (simp add: comp_def fuse_append)
 next
-  case (ss6 a1 a2 rsa rsb rsc)
+  case (ss6 a2 a1 rsa rsb rsc)
+  have "L (erase a2) \<subseteq> L (erase a1)" by fact
   then show "map (fuse bs) (rsa @ [a1] @ rsb @ [a2] @ rsc) s\<leadsto> map (fuse bs) (rsa @ [a1] @ rsb @ rsc)"
     apply(simp)
     apply(rule rrewrite_srewrite.ss6[simplified])
     apply(simp add: erase_fuse)
     done
+(*next 
+  case (extra bs0 bs1 r1 r2 r3)
+  then show ?case
+    by (metis append_assoc fuse.simps(5) rrewrite_srewrite.extra)*)
 qed (auto intro: rrewrite_srewrite.intros)
 
 lemma rewrites_fuse:  
@@ -787,8 +807,9 @@
   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)
-  by (metis bnullable_correctness)
+   apply (meson UnCI bnullable_fuse imageI)
+  
+  using bnullable_correctness nullable_correctness by blast
 
 
 lemma rewrites_bnullable_eq: 
@@ -824,11 +845,22 @@
   then show "bmkepss (AALTs bs1 rs1 # rsb) = bmkepss (map (fuse bs1) rs1 @ rsb)"
     by (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse)
 next
-  case (ss6 a1 a2 rsa rsb rsc)
-  have as1: "erase a1 = erase a2" by fact
+  case (ss6 a2 a1 rsa rsb rsc)
+  have as1: "L(erase a2) \<subseteq> L(erase a1)" by fact
   have as3: "bnullables (rsa @ [a1] @ rsb @ [a2] @ rsc)" by fact
   show "bmkepss (rsa @ [a1] @ rsb @ [a2] @ rsc) = bmkepss (rsa @ [a1] @ rsb @ rsc)" using as1 as3
-    by (smt (verit, best) append_Cons bmkeps.simps(3) bmkepss.simps(2) bmkepss1 bmkepss2 bnullable_correctness)
+    by (smt (verit, ccfv_SIG) append_Cons bmkepss.simps(2) bmkepss1 bmkepss2 bnullable_correctness nullable_correctness subset_eq)
+(*next 
+  case (extra bs0 bs1 r1 bs2 r2 bs4 bs3)
+  then show ?case 
+    apply(subst bmkeps.simps)
+    apply(subst bmkeps.simps)
+    apply(subst bmkeps.simps)
+    apply(subst bmkeps.simps)
+    apply(subst bmkeps.simps)
+    apply(subst bmkeps.simps)
+    apply(simp)
+    done*)
 qed (auto)
 
 lemma rewrites_bmkeps: 
@@ -908,6 +940,11 @@
   apply(simp_all add: bder_fuse)
   done
 
+lemma map_single:
+  shows "map f [x] = [f x]"
+  by simp
+
+
 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"
@@ -977,20 +1014,39 @@
     apply(simp)
     using bder_fuse_list map_map rrewrite_srewrite.ss5 srewrites.simps by blast
 next
-  case (ss6 a1 a2 bs rsa rsb)
-  have as: "erase a1 = erase a2" by fact
+  case (ss6 a2 a1 bs rsa rsb)
+  have as: "L(erase a2) \<subseteq> L(erase a1)" by fact
   show "map (bder c) (bs @ [a1] @ rsa @ [a2] @ rsb) s\<leadsto>* map (bder c) (bs @ [a1] @ rsa @ rsb)"
     apply(simp only: map_append)
-    by (smt (verit, best) erase_bder list.simps(8) list.simps(9) as rrewrite_srewrite.ss6 srewrites.simps)
+    apply(simp only: map_single)
+    apply(rule rs_in_rstar)
+    thm rrewrite_srewrite.intros
+    apply(rule rrewrite_srewrite.ss6)
+    using as
+    apply(auto simp add: der_correctness Der_def)
+    done 
+(*next 
+  case (extra bs0 bs1 r1 r2 r3)
+  then show ?case
+    apply(auto simp add: comp_def)
+    
+       defer
+    using r_in_rstar rrewrite_srewrite.extra apply presburger
+      prefer 2
+    using r_in_rstar rrewrite_srewrite.extra apply presburger
+     prefer 2
+    sorry*)
 qed
 
+
+
 lemma rewrites_preserves_bder: 
   assumes "r1 \<leadsto>* r2"
   shows "bder c r1 \<leadsto>* bder c r2"
 using assms  
 apply(induction r1 r2 rule: rrewrites.induct)
 apply(simp_all add: rewrite_preserves_bder rrewrites_trans)
-done
+  done
 
 
 lemma central:  
@@ -1034,6 +1090,76 @@
 
 (* some tests *)
 
+definition
+  bders_simp_Set :: "string set \<Rightarrow> arexp \<Rightarrow> arexp set"
+where
+  "bders_simp_Set A r \<equiv> bders_simp r ` A"
+
+lemma pders_Set_union:
+  shows "bders_simp_Set (A \<union> B) r = (bders_simp_Set A r \<union> bders_simp_Set B r)"
+  apply (simp add: bders_simp_Set_def)
+  by (simp add: image_Un)
+  
+lemma pders_Set_subset:
+  shows "A \<subseteq> B \<Longrightarrow> bders_simp_Set A r \<subseteq> bders_simp_Set B r"
+  apply (auto simp add: bders_simp_Set_def)
+  done
+
+
+lemma AZERO_r:
+  "bders_simp AZERO s = AZERO"
+  apply(induct s)
+   apply(auto)
+  done
+
+lemma bders_simp_Set_ZERO [simp]:
+  shows "bders_simp_Set UNIV1 AZERO \<subseteq> {AZERO}"
+  unfolding UNIV1_def bders_simp_Set_def 
+  apply(auto)
+  using AZERO_r by blast
+
+lemma AONE_r:
+  shows "bders_simp (AONE bs) s = AZERO \<or> bders_simp (AONE bs) s = AONE bs"
+  apply(induct s)
+   apply(auto)
+  using AZERO_r apply blast
+  using AZERO_r by blast
+
+lemma bders_simp_Set_ONE [simp]:
+  shows "bders_simp_Set UNIV1 (AONE bs) \<subseteq> {AZERO, AONE bs}"
+  unfolding UNIV1_def bders_simp_Set_def 
+  apply(auto split: if_splits)
+  using AONE_r by blast
+
+lemma ACHAR_r:
+  shows "bders_simp (ACHAR bs c) s = AZERO \<or> 
+         bders_simp (ACHAR bs c) s = AONE bs \<or>
+         bders_simp (ACHAR bs c) s = ACHAR bs c"
+  apply(induct s)
+   apply(auto)
+  using AONE_r apply blast
+  using AZERO_r apply force
+  using AONE_r apply blast
+  using AZERO_r apply blast
+  using AONE_r apply blast
+  using AZERO_r by blast
+
+lemma bders_simp_Set_CHAR [simp]:
+  shows "bders_simp_Set UNIV1 (ACHAR bs c) \<subseteq> {AZERO, AONE bs, ACHAR bs c}"
+unfolding UNIV1_def bders_simp_Set_def
+  apply(auto)
+  using ACHAR_r by blast
+  
+lemma bders_simp_Set_ALT [simp]:
+  shows "bders_simp_Set UNIV1 (AALT bs r1 r2) = bders_simp_Set UNIV1 r1 \<union> bders_simp_Set UNIV1 r2"
+  unfolding UNIV1_def bders_simp_Set_def
+  apply(auto)
+  oops
+
+
+
+
+(*
 lemma asize_fuse:
   shows "asize (fuse bs r) = asize r"
   apply(induct r arbitrary: bs)
@@ -1372,11 +1498,13 @@
   using finite_pder apply blast
   oops
   
-
+*)
 
 
 (* below is the idempotency of bsimp *)
 
+(*
+
 lemma bsimp_ASEQ_fuse:
   shows "fuse bs1 (bsimp_ASEQ bs2 r1 r2) = bsimp_ASEQ (bs1 @ bs2) r1 r2"
   apply(induct r1 r2 arbitrary: bs1 bs2 rule: bsimp_ASEQ.induct)
@@ -1466,6 +1594,8 @@
         apply auto
 
   oops
+*)
+
 
 (*
 AALTs [] [AZERO, AALTs(bs1, [a, b]) ] 
@@ -1475,24 +1605,19 @@
 
 *)
 
-lemma normal_bsimp: 
-  shows "\<nexists>r'. bsimp r \<leadsto> r'"
-  oops
 
   (*r' size bsimp r > size r' 
     r' \<leadsto>* bsimp bsimp r
 size bsimp r > size r' \<ge> size bsimp bsimp r*)
 
-export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers
-
 
 unused_thms
 
-
+(*
 inductive aggressive:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>? _" [99, 99] 99)
   where
  "ASEQ bs (AALTs bs1 rs) r \<leadsto>? AALTs (bs@bs1) (map (\<lambda>r'. ASEQ [] r' r) rs) "
-
+*)
 
 
 end