ha
authorChengsong
Sun, 30 Jan 2022 23:37:29 +0000
changeset 404 1500f96707b0
parent 403 6291181fad07 (current diff)
parent 402 1612f2a77bf6 (diff)
child 405 3cfea5bb5e23
ha
Binary file Literature/Verbatim-2021-paper.pdf has changed
Binary file Literature/VerbatimPP-Lexer.pdf has changed
--- a/thys/BitCodedCT.thy	Sun Jan 30 23:36:31 2022 +0000
+++ b/thys/BitCodedCT.thy	Sun Jan 30 23:37:29 2022 +0000
@@ -29,7 +29,7 @@
 where
   "decode' ds ZERO = (Void, [])"
 | "decode' ds ONE = (Void, ds)"
-| "decode' ds (CHAR d) = (Char d, ds)"
+| "decode' ds (CH d) = (Char d, ds)"
 | "decode' [] (ALT r1 r2) = (Void, [])"
 | "decode' (Z # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))"
 | "decode' (S # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))"
--- a/thys/LexerExt.thy	Sun Jan 30 23:36:31 2022 +0000
+++ b/thys/LexerExt.thy	Sun Jan 30 23:37:29 2022 +0000
@@ -17,10 +17,15 @@
 | "mkeps(NTIMES r n) = Stars (replicate n (mkeps r))"
 | "mkeps(FROMNTIMES r n) = Stars (replicate n (mkeps r))"
 | "mkeps(NMTIMES r n m) = Stars (replicate n (mkeps r))"
-  
+| "mkeps(NOT ZERO) = Nt Void"
+| "mkeps(NOT (CH _ )) = Nt Void"
+| "mkeps(NOT (SEQ r1 r2)) = Seq (mkeps (NOT r1)) (mkeps (NOT r1))"
+| "mkeps(NOT (ALT r1 r2)) = (if nullable(r1) then Right (mkeps (NOT r2)) else  (mkeps (NOT r1)))"
+
+
 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
 where
-  "injval (CHAR d) c Void = Char d"
+  "injval (CH d) c Void = Char d"
 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
@@ -49,9 +54,11 @@
   shows "flat (mkeps r) = []"
 using assms
   apply(induct rule: nullable.induct) 
-         apply(auto)
-  by presburger  
-  
+          apply(auto)
+  apply presburger  
+  apply(case_tac r)
+  apply(auto)
+  sorry
   
 lemma mkeps_nullable:
   assumes "nullable(r)" 
@@ -81,7 +88,7 @@
     apply (simp add: mkeps_flat)
    apply(simp)
   apply(simp)
-done
+  sorry
     
 
 lemma Prf_injval_flat:
@@ -90,7 +97,7 @@
 using assms
 apply(induct arbitrary: v rule: der.induct)
 apply(auto elim!: Prf_elims intro: mkeps_flat split: if_splits)
-done
+  sorry
 
 lemma Prf_injval:
   assumes "\<Turnstile> v : der c r" 
@@ -170,7 +177,8 @@
      apply(simp add: Prf_injval_flat)
      apply(simp)
    apply(simp)
-done
+  sorry
+
 
 
 
@@ -186,8 +194,10 @@
 apply(auto intro: Posix.intros simp add: nullable_correctness Sequ_def)
 apply(subst append.simps(1)[symmetric])
 apply(rule Posix.intros)
-      apply(auto)
-  done
+   apply(auto)
+  apply(case_tac r)
+  apply(auto)
+  sorry
     
 
 lemma Posix_injval:
@@ -207,22 +217,22 @@
   then have "False" by cases
   then show "(c # s) \<in> ONE \<rightarrow> (injval ONE c v)" by simp
 next 
-  case (CHAR d)
+  case (CH d)
   consider (eq) "c = d" | (ineq) "c \<noteq> d" by blast
-  then show "(c # s) \<in> (CHAR d) \<rightarrow> (injval (CHAR d) c v)"
+  then show "(c # s) \<in> (CH d) \<rightarrow> (injval (CH d) c v)"
   proof (cases)
     case eq
-    have "s \<in> der c (CHAR d) \<rightarrow> v" by fact
+    have "s \<in> der c (CH d) \<rightarrow> v" by fact
     then have "s \<in> ONE \<rightarrow> v" using eq by simp
     then have eqs: "s = [] \<and> v = Void" by cases simp
-    show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" using eq eqs 
+    show "(c # s) \<in> CH d \<rightarrow> injval (CH d) c v" using eq eqs 
     by (auto intro: Posix.intros)
   next
     case ineq
-    have "s \<in> der c (CHAR d) \<rightarrow> v" by fact
+    have "s \<in> der c (CH d) \<rightarrow> v" by fact
     then have "s \<in> ZERO \<rightarrow> v" using ineq by simp
     then have "False" by cases
-    then show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" by simp
+    then show "(c # s) \<in> CH d \<rightarrow> injval (CH d) c v" by simp
   qed
 next
   case (ALT r1 r2)
@@ -319,7 +329,6 @@
     apply(simp)
     apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
     apply(clarify)
-    apply(drule_tac x="v1" in meta_spec)
     apply(drule_tac x="vss" in meta_spec)
     apply(drule_tac x="s1" in meta_spec)
     apply(drule_tac x="s2" in meta_spec)
@@ -401,7 +410,6 @@
     apply(simp)
     apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
     apply(clarify)
-    apply(drule_tac x="v1" in meta_spec)
     apply(drule_tac x="vss" in meta_spec)
     apply(drule_tac x="s1" in meta_spec)
     apply(drule_tac x="s2" in meta_spec)
@@ -454,7 +462,6 @@
     apply(simp)
     apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
     apply(clarify)
-    apply(drule_tac x="v1" in meta_spec)
     apply(drule_tac x="vss" in meta_spec)
     apply(drule_tac x="s1" in meta_spec)
     apply(drule_tac x="s2" in meta_spec)
@@ -544,7 +551,6 @@
     apply(simp)
     apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
     apply(clarify)
-    apply(drule_tac x="v1" in meta_spec)
     apply(drule_tac x="vss" in meta_spec)
     apply(drule_tac x="s1" in meta_spec)
     apply(drule_tac x="s2" in meta_spec)
@@ -618,6 +624,9 @@
           apply(simp)
           done  
       qed    
+   next
+     case (NOT r s v)
+     then show ?case sorry
 qed
 
 section {* Lexer Correctness *}
--- a/thys/SpecExt.thy	Sun Jan 30 23:36:31 2022 +0000
+++ b/thys/SpecExt.thy	Sun Jan 30 23:37:29 2022 +0000
@@ -1,6 +1,6 @@
    
 theory SpecExt
-  imports Main (*"~~/src/HOL/Library/Sublist"*)
+  imports Main "HOL-Library.Sublist" (*"~~/src/HOL/Library/Sublist"*)
 begin
 
 section {* Sequential Composition of Languages *}
@@ -165,10 +165,6 @@
 apply(auto simp add: Sequ_def)
   done
 
-lemma
-  assumes "[] \<in> A" "n \<noteq> 0" "A \<noteq> {}"
-  shows "A \<up> (Suc n) = A \<up> n"
-
 lemma Der_Pow_0:
   shows "Der c (A \<up> 0) = {}"
 by(simp add: Der_def)
@@ -221,7 +217,7 @@
 datatype rexp =
   ZERO
 | ONE
-| CHAR char
+| CH char
 | SEQ rexp rexp
 | ALT rexp rexp
 | STAR rexp
@@ -238,7 +234,7 @@
 where
   "L (ZERO) = {}"
 | "L (ONE) = {[]}"
-| "L (CHAR c) = {[c]}"
+| "L (CH c) = {[c]}"
 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 | "L (STAR r) = (L r)\<star>"
@@ -255,7 +251,7 @@
 where
   "nullable (ZERO) = False"
 | "nullable (ONE) = True"
-| "nullable (CHAR c) = False"
+| "nullable (CH c) = False"
 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
 | "nullable (STAR r) = True"
@@ -270,7 +266,7 @@
 where
   "der c (ZERO) = ZERO"
 | "der c (ONE) = ZERO"
-| "der c (CHAR d) = (if c = d then ONE else ZERO)"
+| "der c (CH d) = (if c = d then ONE else ZERO)"
 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
 | "der c (SEQ r1 r2) = 
      (if nullable r1
@@ -340,48 +336,6 @@
   by (metis append.assoc)
   
 
-
-lemma
- "L(FROMNTIMES r n) = L(SEQ (NTIMES r n) (STAR r))"
-  apply(auto simp add: Sequ_def)
-  defer
-   apply(subgoal_tac "\<exists>m. s2 \<in> (L r) \<up> m")
-  prefer 2
-    apply (simp add: Star_Pow)
-  apply(auto)
-  apply(rule_tac x="n + m" in bexI)
-    apply (simp add: pow_add)
-   apply simp
-  apply(subgoal_tac "\<exists>m. m + n = xa")
-   apply(auto)
-   prefer 2
-  using le_add_diff_inverse2 apply auto[1]
-  by (smt Pow_Star Sequ_def add.commute mem_Collect_eq pow_add2)
-  
-lemma
-   "L (der c (FROMNTIMES r n)) = 
-     L (SEQ (der c r) (FROMNTIMES r (n - 1)))"
-  apply(auto simp add: Sequ_def)
-  using Star_Pow apply blast
-  using Pow_Star by blast
-  
-lemma
- "L (der c (UPNTIMES r n)) = 
-    L(if n = 0 then ZERO  else 
-      ALT (der c r) (SEQ (der c r) (UPNTIMES r (n - 1))))"
-  apply(auto simp add: Sequ_def)
-  using SpecExt.Pow_empty by blast 
-
-abbreviation "FROM \<equiv> FROMNTIMES"
-
-lemma
-  shows "L (der c (FROM r n)) = 
-         L (if n <= 0 then SEQ (der c r) (ALT ONE (FROM r 0))
-                      else SEQ (der c r) (ALT ZERO (FROM r (n -1))))"
-  apply(auto simp add: Sequ_def)
-  oops
-
-
 fun 
  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
 where
@@ -454,8 +408,10 @@
 apply(auto simp add: Sequ_def Der_def Cons_eq_append_conv)[1]
 apply(rule_tac x="Suc xa" in bexI)
 apply(auto simp add: Sequ_def)[2]
-apply (metis append_Cons)
-apply (metis (no_types, hide_lams) Pow_decomp atMost_iff diff_Suc_eq_diff_pred diff_is_0_eq)
+     apply (metis append_Cons)
+ apply(rule_tac x="xa - 1" in bexI)
+     apply(auto simp add: Sequ_def)[2]
+  apply (metis One_nat_def Pow_decomp)
 apply(rule impI)+
 apply(subst Sequ_Union_in)
 apply(subst Der_Pow_Sequ[symmetric])
@@ -485,7 +441,7 @@
 | Right val
 | Left val
 | Stars "val list"
-
+| Nt val
 
 section {* The string behind a value *}
 
@@ -499,6 +455,7 @@
 | "flat (Seq v1 v2) = (flat v1) @ (flat v2)"
 | "flat (Stars []) = []"
 | "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))" 
+| "flat (Nt v) = flat v"
 
 abbreviation
   "flats vs \<equiv> concat (map flat vs)"
@@ -597,7 +554,7 @@
 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
 | "\<Turnstile> Void : ONE"
-| "\<Turnstile> Char c : CHAR c"
+| "\<Turnstile> Char c : CH c"
 | "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : STAR r"
 | "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> []; length vs \<le> n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : UPNTIMES r n"
 | "\<lbrakk>\<forall>v \<in> set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []; 
@@ -622,7 +579,7 @@
   "\<Turnstile> v : SEQ r1 r2"
   "\<Turnstile> v : ALT r1 r2"
   "\<Turnstile> v : ONE"
-  "\<Turnstile> v : CHAR c"
+  "\<Turnstile> v : CH c"
   "\<Turnstile> vs : STAR r"
   "\<Turnstile> vs : UPNTIMES r n"
   "\<Turnstile> vs : NTIMES r n"
@@ -867,7 +824,10 @@
   then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> []" "length vs \<le> n"
   using IH flats_cval_nonempty by (smt order.trans) 
   then show "\<exists>v. \<Turnstile> v : UPNTIMES r n \<and> flat v = s"
-  using Prf.intros(7) flat_Stars by blast
+    using Prf.intros(7) flat_Stars by blast
+next 
+  case (NOT r)
+  then show ?case sorry
 qed (auto intro: Prf.intros)
 
 
@@ -917,7 +877,7 @@
 lemma LV_simps:
   shows "LV ZERO s = {}"
   and   "LV ONE s = (if s = [] then {Void} else {})"
-  and   "LV (CHAR c) s = (if s = [c] then {Char c} else {})"
+  and   "LV (CH c) s = (if s = [c] then {Char c} else {})"
   and   "LV (ALT r1 r2) s = Left ` LV r1 s \<union> Right ` LV r2 s"
 unfolding LV_def
 apply(auto intro: Prf.intros elim: Prf.cases)
@@ -1226,8 +1186,8 @@
   case (ONE s)
   show "finite (LV ONE s)" by (simp add: LV_simps)
 next
-  case (CHAR c s)
-  show "finite (LV (CHAR c) s)" by (simp add: LV_simps)
+  case (CH c s)
+  show "finite (LV (CH c) s)" by (simp add: LV_simps)
 next 
   case (ALT r1 r2 s)
   then show "finite (LV (ALT r1 r2) s)" by (simp add: LV_simps)
@@ -1270,7 +1230,10 @@
   case (NMTIMES r n m s)
   have "\<And>s. finite (LV r s)" by fact
   then show "finite (LV (NMTIMES r n m) s)"
-    by (simp add: LV_NMTIMES_6)         
+    by (simp add: LV_NMTIMES_6)    
+next 
+  case (NOT r s)
+  then show ?case sorry
 qed
 
 
@@ -1281,7 +1244,7 @@
   Posix :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
 where
   Posix_ONE: "[] \<in> ONE \<rightarrow> Void"
-| Posix_CHAR: "[c] \<in> (CHAR c) \<rightarrow> (Char c)"
+| Posix_CHAR: "[c] \<in> (CH c) \<rightarrow> (Char c)"
 | Posix_ALT1: "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
 | Posix_ALT2: "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
 | Posix_SEQ: "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
@@ -1320,7 +1283,7 @@
 inductive_cases Posix_elims:
   "s \<in> ZERO \<rightarrow> v"
   "s \<in> ONE \<rightarrow> v"
-  "s \<in> CHAR c \<rightarrow> v"
+  "s \<in> CH c \<rightarrow> v"
   "s \<in> ALT r1 r2 \<rightarrow> v"
   "s \<in> SEQ r1 r2 \<rightarrow> v"
   "s \<in> STAR r \<rightarrow> v"
@@ -1396,7 +1359,7 @@
   then show "Void = v2" by cases auto
 next 
   case (Posix_CHAR c v2)
-  have "[c] \<in> CHAR c \<rightarrow> v2" by fact
+  have "[c] \<in> CH c \<rightarrow> v2" by fact
   then show "Char c = v2" by cases auto
 next 
   case (Posix_ALT1 s r1 v r2 v2)
@@ -1503,14 +1466,9 @@
     using Posix1(1) Posix1(2) apply blast 
      apply(case_tac n)
       apply(simp)
-      apply(simp)
-    apply(drule_tac x="va" in meta_spec)
-    apply(drule_tac x="vs" in meta_spec)
-    apply(simp)
-     apply(drule meta_mp)
-    apply (metis L.simps(9) Posix1(1) UN_E append.right_neutral append_Nil diff_Suc_1 local.Posix_FROMNTIMES1(4) val.inject(5))
-    apply (metis L.simps(9) Posix1(1) UN_E append.right_neutral append_Nil)
-    by (metis One_nat_def Posix1(1) Posix_FROMNTIMES1.hyps(7) self_append_conv self_append_conv2)
+     apply(simp)
+    apply (smt (verit, ccfv_threshold) L.simps(9) Posix1(1) UN_E append_eq_append_conv2)
+    by (metis One_nat_def Posix1(1) Posix_FROMNTIMES1.hyps(7) append_Nil2 append_self_conv2)
   moreover
   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
             "\<And>v2. s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
@@ -1555,18 +1513,8 @@
        apply(case_tac m)
       apply(simp)
      apply(simp)
-    apply(drule_tac x="va" in meta_spec)
-    apply(drule_tac x="vs" in meta_spec)
-    apply(simp)
-     apply(drule meta_mp)
-      apply(drule Posix1(1))
-      apply(drule Posix1(1))
-      apply(drule Posix1(1))
-      apply(frule Posix1(1))
-      apply(simp)
-    using Posix_NMTIMES1.hyps(4) apply force
-     apply (metis L.simps(10) Posix1(1) UN_E append_Nil2 append_self_conv2)
-    by (metis One_nat_def Posix1(1) Posix_NMTIMES1.hyps(8) append.right_neutral append_Nil)      
+    apply (metis L.simps(10) Posix1(1) UN_E append.right_neutral append_Nil)
+    by (metis One_nat_def Posix1(1) Posix_NMTIMES1.hyps(8) append_Nil self_append_conv)
   moreover
   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
             "\<And>v2. s2 \<in> NMTIMES r (n - 1) (m - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
@@ -1616,7 +1564,6 @@
      apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)[2]
   apply (metis (mono_tags, lifting) Prf.intros(9) append_Nil empty_iff flat_Stars flats_empty list.set(1) mem_Collect_eq)
      apply(simp)
-     apply(clarify)
      apply(case_tac n)
       apply(simp)
      apply(simp)
@@ -1632,7 +1579,6 @@
       apply(simp)
      apply(simp)
     apply(simp)
-   apply(clarify)
    apply(erule Prf_elims)
       apply(simp)
   apply(rule Prf.intros)  
@@ -1660,7 +1606,6 @@
   apply(simp)
   apply (metis Prf.intros(11) append_Nil empty_iff list.set(1))
   apply(simp)
-  apply(clarify)
   apply(rotate_tac 6)
   apply(erule Prf_elims)
    apply(simp)
@@ -1675,7 +1620,6 @@
   apply(simp)
   apply(simp)
   apply(simp)
-  apply(clarify)
   apply(rotate_tac 6)
   apply(erule Prf_elims)
    apply(simp)
--- a/thys2/Paper/Paper.thy	Sun Jan 30 23:36:31 2022 +0000
+++ b/thys2/Paper/Paper.thy	Sun Jan 30 23:37:29 2022 +0000
@@ -7,7 +7,342 @@
    "../SizeBound4" 
    "HOL-Library.LaTeXsugar"
 begin
+
+declare [[show_question_marks = false]]
+
+notation (latex output)
+  If  ("(\<^latex>\<open>\\textrm{\<close>if\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>then\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>else\<^latex>\<open>}\<close> (_))" 10) and
+  Cons ("_\<^latex>\<open>\\mbox{$\\,$}\<close>::\<^latex>\<open>\\mbox{$\\,$}\<close>_" [75,73] 73) 
+
+
+abbreviation 
+  "der_syn r c \<equiv> der c r"
+
+notation (latex output)
+  der_syn ("_\\_" [79, 1000] 76) and
+
+  ZERO ("\<^bold>0" 81) and 
+  ONE ("\<^bold>1" 81) and 
+  CH ("_" [1000] 80) and
+  ALT ("_ + _" [77,77] 78) and
+  SEQ ("_ \<cdot> _" [77,77] 78) and
+  STAR ("_\<^sup>\<star>" [79] 78) and
+
+  val.Void ("Empty" 78) and
+  val.Char ("Char _" [1000] 78) and
+  val.Left ("Left _" [79] 78) and
+  val.Right ("Right _" [1000] 78) and
+  val.Seq ("Seq _ _" [79,79] 78) and
+  val.Stars ("Stars _" [79] 78) and
+
+  Posix ("'(_, _') \<rightarrow> _" [63,75,75] 75) and
+
+  flat ("|_|" [75] 74) and
+  flats ("|_|" [72] 74) and
+  injval ("inj _ _ _" [79,77,79] 76) and 
+  mkeps ("mkeps _" [79] 76) and 
+  length ("len _" [73] 73) and
+  set ("_" [73] 73) and
+
+  AZERO ("ZERO" 81) and 
+  AONE ("ONE _" [79] 81) and 
+  ACHAR ("CHAR _ _" [79, 79] 80) and
+  AALTs ("ALTs _ _" [77,77] 78) and
+  ASEQ ("SEQ _ _ _" [79, 77,77] 78) and
+  ASTAR ("STAR _ _" [79, 79] 78) and
+
+  code ("code _" [79] 74) and
+  intern ("_\<^latex>\<open>\\mbox{$^\\uparrow$}\<close>" [900] 80) and
+  erase ("_\<^latex>\<open>\\mbox{$^\\downarrow$}\<close>" [1000] 74) and
+  bnullable ("nullable\<^latex>\<open>\\mbox{$_b$}\<close> _" [1000] 80) and
+  bmkeps ("mkeps\<^latex>\<open>\\mbox{$_b$}\<close> _" [1000] 80)
+
+
+lemma better_retrieve:
+   shows "rs \<noteq> Nil ==> retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v"
+   and   "rs \<noteq> Nil ==> retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v"
+  apply (metis list.exhaust retrieve.simps(4))
+  by (metis list.exhaust retrieve.simps(5))
+
 (*>*)
+
+section {* Introduction *}
+
+text {*
+
+In the last fifteen or so years, Brzozowski's derivatives of regular
+expressions have sparked quite a bit of interest in the functional
+programming and theorem prover communities.  The beauty of
+Brzozowski's derivatives \cite{Brzozowski1964} is that they are neatly
+expressible in any functional language, and easily definable and
+reasoned about in theorem provers---the definitions just consist of
+inductive datatypes and simple recursive functions. A mechanised
+correctness proof of Brzozowski's matcher in for example HOL4 has been
+mentioned by Owens and Slind~\cite{Owens2008}. Another one in
+Isabelle/HOL is part of the work by Krauss and Nipkow
+\cite{Krauss2011}.  And another one in Coq is given by Coquand and
+Siles \cite{Coquand2012}.
+
+
+The notion of derivatives
+\cite{Brzozowski1964}, written @{term "der c r"}, of a regular
+expression give a simple solution to the problem of matching a string
+@{term s} with a regular expression @{term r}: if the derivative of
+@{term r} w.r.t.\ (in succession) all the characters of the string
+matches the empty string, then @{term r} matches @{term s} (and {\em
+vice versa}). The derivative has the property (which may almost be
+regarded as its specification) that, for every string @{term s} and
+regular expression @{term r} and character @{term c}, one has @{term
+"cs \<in> L(r)"} if and only if \mbox{@{term "s \<in> L(der c r)"}}.
+
+
+If a regular expression matches a string, then in general there is more
+than one way of how the string is matched. There are two commonly used
+disambiguation strategies to generate a unique answer: one is called
+GREEDY matching \cite{Frisch2004} and the other is POSIX
+matching~\cite{POSIX,Kuklewicz,OkuiSuzuki2010,Sulzmann2014,Vansummeren2006}.
+For example consider the string @{term xy} and the regular expression
+\mbox{@{term "STAR (ALT (ALT x y) xy)"}}. Either the string can be
+matched in two `iterations' by the single letter-regular expressions
+@{term x} and @{term y}, or directly in one iteration by @{term xy}. The
+first case corresponds to GREEDY matching, which first matches with the
+left-most symbol and only matches the next symbol in case of a mismatch
+(this is greedy in the sense of preferring instant gratification to
+delayed repletion). The second case is POSIX matching, which prefers the
+longest match.
+
+
+\begin{center}
+\begin{tabular}{cc}
+  \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+  @{thm (lhs) der.simps(1)} & $\dn$ & @{thm (rhs) der.simps(1)}\\
+  @{thm (lhs) der.simps(2)} & $\dn$ & @{thm (rhs) der.simps(2)}\\
+  @{thm (lhs) der.simps(3)} & $\dn$ & @{thm (rhs) der.simps(3)}\\
+  @{thm (lhs) der.simps(4)[of c "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) der.simps(4)[of c "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{text "if"} @{term "nullable(r\<^sub>1)"}\\
+  & & @{text "then"} @{term "ALT (SEQ (der c r\<^sub>1) r\<^sub>2) (der c r\<^sub>2)"}\\
+  & & @{text "else"} @{term "SEQ (der c r\<^sub>1) r\<^sub>2"}\\
+  % & & @{thm (rhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) der.simps(6)} & $\dn$ & @{thm (rhs) der.simps(6)}
+  \end{tabular}
+  &
+  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+  @{thm (lhs) nullable.simps(1)} & $\dn$ & @{thm (rhs) nullable.simps(1)}\\
+  @{thm (lhs) nullable.simps(2)} & $\dn$ & @{thm (rhs) nullable.simps(2)}\\
+  @{thm (lhs) nullable.simps(3)} & $\dn$ & @{thm (rhs) nullable.simps(3)}\\
+  @{thm (lhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) nullable.simps(6)} & $\dn$ & @{thm (rhs) nullable.simps(6)}\medskip\\
+  \end{tabular}  
+\end{tabular}  
+\end{center}
+
+
+\begin{figure}[t]
+\begin{center}
+\begin{tikzpicture}[scale=2,node distance=1.3cm,
+                    every node/.style={minimum size=6mm}]
+\node (r1)  {@{term "r\<^sub>1"}};
+\node (r2) [right=of r1]{@{term "r\<^sub>2"}};
+\draw[->,line width=1mm](r1)--(r2) node[above,midway] {@{term "der a DUMMY"}};
+\node (r3) [right=of r2]{@{term "r\<^sub>3"}};
+\draw[->,line width=1mm](r2)--(r3) node[above,midway] {@{term "der b DUMMY"}};
+\node (r4) [right=of r3]{@{term "r\<^sub>4"}};
+\draw[->,line width=1mm](r3)--(r4) node[above,midway] {@{term "der c DUMMY"}};
+\draw (r4) node[anchor=west] {\;\raisebox{3mm}{@{term nullable}}};
+\node (v4) [below=of r4]{@{term "v\<^sub>4"}};
+\draw[->,line width=1mm](r4) -- (v4);
+\node (v3) [left=of v4] {@{term "v\<^sub>3"}};
+\draw[->,line width=1mm](v4)--(v3) node[below,midway] {\<open>inj r\<^sub>3 c\<close>};
+\node (v2) [left=of v3]{@{term "v\<^sub>2"}};
+\draw[->,line width=1mm](v3)--(v2) node[below,midway] {\<open>inj r\<^sub>2 b\<close>};
+\node (v1) [left=of v2] {@{term "v\<^sub>1"}};
+\draw[->,line width=1mm](v2)--(v1) node[below,midway] {\<open>inj r\<^sub>1 a\<close>};
+\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{@{term "mkeps"}}};
+\end{tikzpicture}
+\end{center}
+\mbox{}\\[-13mm]
+
+\caption{The two phases of the algorithm by Sulzmann \& Lu \cite{Sulzmann2014},
+matching the string @{term "[a,b,c]"}. The first phase (the arrows from 
+left to right) is \Brz's matcher building successive derivatives. If the 
+last regular expression is @{term nullable}, then the functions of the 
+second phase are called (the top-down and right-to-left arrows): first 
+@{term mkeps} calculates a value @{term "v\<^sub>4"} witnessing
+how the empty string has been recognised by @{term "r\<^sub>4"}. After
+that the function @{term inj} ``injects back'' the characters of the string into
+the values.
+\label{Sulz}}
+\end{figure} 
+
+
+*}
+
+section {* Background *}
+
+text {*
+  Sulzmann-Lu algorithm with inj. State that POSIX rules.
+  metion slg is correct.
+
+
+  \begin{figure}[t]
+  \begin{center}
+  \begin{tabular}{c}
+  @{thm[mode=Axiom] Posix.intros(1)}\<open>P\<close>@{term "ONE"} \qquad
+  @{thm[mode=Axiom] Posix.intros(2)}\<open>P\<close>@{term "c"}\medskip\\
+  @{thm[mode=Rule] Posix.intros(3)[of "s" "r\<^sub>1" "v" "r\<^sub>2"]}\<open>P+L\<close>\qquad
+  @{thm[mode=Rule] Posix.intros(4)[of "s" "r\<^sub>2" "v" "r\<^sub>1"]}\<open>P+R\<close>\medskip\\
+  $\mprset{flushleft}
+   \inferrule
+   {@{thm (prem 1) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]} \qquad
+    @{thm (prem 2) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]} \\\\
+    @{thm (prem 3) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}
+   {@{thm (concl) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}$\<open>PS\<close>\\
+  @{thm[mode=Axiom] Posix.intros(7)}\<open>P[]\<close>\medskip\\
+  $\mprset{flushleft}
+   \inferrule
+   {@{thm (prem 1) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad
+    @{thm (prem 2) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad
+    @{thm (prem 3) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \\\\
+    @{thm (prem 4) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}}
+   {@{thm (concl) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}}$\<open>P\<star>\<close>
+  \end{tabular}
+  \end{center}
+  \caption{Our inductive definition of POSIX values.}\label{POSIXrules}
+  \end{figure}
+
+
+  \begin{center}
+  \begin{tabular}{lcl}
+  @{thm (lhs) mkeps.simps(1)} & $\dn$ & @{thm (rhs) mkeps.simps(1)}\\
+  @{thm (lhs) mkeps.simps(2)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) mkeps.simps(2)[of "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) mkeps.simps(3)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) mkeps.simps(3)[of "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) mkeps.simps(4)} & $\dn$ & @{thm (rhs) mkeps.simps(4)}\\
+  \end{tabular}
+  \end{center}
+
+  \begin{center}
+  \begin{tabular}{l@ {\hspace{5mm}}lcl}
+  \textit{(1)} & @{thm (lhs) injval.simps(1)} & $\dn$ & @{thm (rhs) injval.simps(1)}\\
+  \textit{(2)} & @{thm (lhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & 
+      @{thm (rhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\
+  \textit{(3)} & @{thm (lhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & 
+      @{thm (rhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\
+  \textit{(4)} & @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ 
+      & @{thm (rhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\
+  \textit{(5)} & @{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ 
+      & @{thm (rhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\
+  \textit{(6)} & @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ 
+      & @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\
+  \textit{(7)} & @{thm (lhs) injval.simps(7)[of "r" "c" "v" "vs"]} & $\dn$ 
+      & @{thm (rhs) injval.simps(7)[of "r" "c" "v" "vs"]}\\
+  \end{tabular}
+  \end{center}
+
+*}
+
+section {* Bitcoded Regular Expressions and Derivatives *}
+
+text {*
+  bitcoded regexes / decoding / bmkeps
+  gets rid of the second phase (only single phase)   
+  correctness
+
+
+  \begin{center}
+  \begin{tabular}{lcl}
+  @{thm (lhs) code.simps(1)} & $\dn$ & @{thm (rhs) code.simps(1)}\\
+  @{thm (lhs) code.simps(2)} & $\dn$ & @{thm (rhs) code.simps(2)}\\
+  @{thm (lhs) code.simps(3)} & $\dn$ & @{thm (rhs) code.simps(3)}\\
+  @{thm (lhs) code.simps(4)} & $\dn$ & @{thm (rhs) code.simps(4)}\\
+  @{thm (lhs) code.simps(5)[of "v\<^sub>1" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) code.simps(5)[of "v\<^sub>1" "v\<^sub>2"]}\\
+  @{thm (lhs) code.simps(6)} & $\dn$ & @{thm (rhs) code.simps(6)}\\
+  @{thm (lhs) code.simps(7)} & $\dn$ & @{thm (rhs) code.simps(7)}
+  \end{tabular}
+  \end{center}
+
+
+  The idea of the bitcodes is to annotate them to regular expressions and generate values
+  incrementally. The bitcodes can be read off from the @{text breg} and then decoded into a value.
+
+  \begin{center}
+  \begin{tabular}{lcl}
+  @{term breg} & $::=$ & @{term "AZERO"}\\
+               & $\mid$ & @{term "AONE bs"}\\
+               & $\mid$ & @{term "ACHAR bs c"}\\
+               & $\mid$ & @{term "AALTs bs rs"}\\
+               & $\mid$ & @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}\\
+               & $\mid$ & @{term "ASTAR bs r"}
+  \end{tabular}
+  \end{center}
+
+
+
+  \begin{center}
+  \begin{tabular}{lcl}
+  @{thm (lhs) retrieve.simps(1)} & $\dn$ & @{thm (rhs) retrieve.simps(1)}\\
+  @{thm (lhs) retrieve.simps(2)} & $\dn$ & @{thm (rhs) retrieve.simps(2)}\\
+  @{thm (lhs) retrieve.simps(3)} & $\dn$ & @{thm (rhs) retrieve.simps(3)}\\
+  @{thm (lhs) better_retrieve(1)} & $\dn$ & @{thm (rhs) better_retrieve(1)}\\
+  @{thm (lhs) better_retrieve(2)} & $\dn$ & @{thm (rhs) better_retrieve(2)}\\
+  @{thm (lhs) retrieve.simps(6)[of _ "r\<^sub>1" "r\<^sub>2" "v\<^sub>1" "v\<^sub>2"]}
+      & $\dn$ & @{thm (rhs) retrieve.simps(6)[of _ "r\<^sub>1" "r\<^sub>2" "v\<^sub>1" "v\<^sub>2"]}\\
+  @{thm (lhs) retrieve.simps(7)} & $\dn$ & @{thm (rhs) retrieve.simps(7)}\\
+  @{thm (lhs) retrieve.simps(8)} & $\dn$ & @{thm (rhs) retrieve.simps(8)}
+  \end{tabular}
+  \end{center}
+
+
+  \begin{theorem}
+  @{thm blexer_correctness} 
+  \end{theorem}
+*}
+
+
+section {* Simplification *}
+
+text {*
+     Sulzmann \& Lu apply simplification via a fixpoint operation; also does not use erase to filter out duplicates.
+  
+   not direct correspondence with PDERs, because of example
+   problem with retrieve 
+
+   correctness
+
+   
+    
+
+
+
+   \begin{figure}[t]
+  \begin{center}
+  \begin{tabular}{c}
+  @{thm[mode=Axiom] bs1[of _ "r\<^sub>2"]}\qquad
+  @{thm[mode=Axiom] bs2[of _ "r\<^sub>1"]}\qquad
+  @{thm[mode=Axiom] bs3[of "bs\<^sub>1" "bs\<^sub>2"]}\\
+  @{thm[mode=Rule] bs4[of "r\<^sub>1" "r\<^sub>2" _ "r\<^sub>3"]}\qquad
+  @{thm[mode=Rule] bs5[of "r\<^sub>3" "r\<^sub>4" _ "r\<^sub>1"]}\\
+  @{thm[mode=Axiom] bs6}\qquad
+  @{thm[mode=Axiom] bs7}\\
+  @{thm[mode=Rule] bs8[of "rs\<^sub>1" "rs\<^sub>2"]}\\
+  @{thm[mode=Axiom] ss1}\qquad
+  @{thm[mode=Rule] ss2[of "rs\<^sub>1" "rs\<^sub>2"]}\qquad
+  @{thm[mode=Rule] ss3[of "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm[mode=Axiom] ss4}\qquad
+  @{thm[mode=Axiom] ss5[of "bs" "rs\<^sub>1" "rs\<^sub>2"]}\\
+  @{thm[mode=Rule] ss6[of "r\<^sub>1" "r\<^sub>2" "rs\<^sub>1" "rs\<^sub>2" "rs\<^sub>3"]}\\
+  \end{tabular}
+  \end{center}
+  \caption{???}\label{SimpRewrites}
+  \end{figure}
+*}
+
+section {* Bound - NO *}
+
+section {* Bounded Regex / Not *}
+
+section {* Conclusion *}
+
 text {*
 
 \cite{AusafDyckhoffUrban2016}
--- a/thys2/Paper/document/root.tex	Sun Jan 30 23:36:31 2022 +0000
+++ b/thys2/Paper/document/root.tex	Sun Jan 30 23:37:29 2022 +0000
@@ -45,33 +45,59 @@
 \titlerunning{POSIX Lexing with Bitcoded Derivatives}
 \author{Chengsong Tan}{King's College London}{chengsong.tan@kcl.ac.uk}{}{}
 \author{Christian Urban}{King's College London}{christian.urban@kcl.ac.uk}{}{}
+\authorrunning{C.~Tan and C.~Urban}
+\keywords{POSIX matching, Derivatives of Regular Expressions, Isabelle/HOL}
+\category{}
+\ccsdesc[100]{Design and analysis of algorithms}
+\ccsdesc[100]{Formal languages and automata theory}
+\Copyright{\mbox{}}
+\nolinenumbers
 
 
 \begin{document}
 \maketitle
 
 \begin{abstract}
-Brzozowski introduced the notion of derivatives for regular
-expressions. They can be used for a very simple regular expression
-matching algorithm.  Sulzmann and Lu cleverly extended this algorithm
-in order to deal with POSIX matching, which is the underlying
-disambiguation strategy for regular expressions needed in lexers.
-Their algorithm generates POSIX values which encode the information of
-\emph{how} a regular expression matches a string---that is, which part
-of the string is matched by which part of the regular expression.  In
-this paper we give our inductive definition of what a POSIX value is
-and show $(i)$ that such a value is unique (for given regular
-expression and string being matched) and $(ii)$ that Sulzmann and Lu's
-algorithm always generates such a value (provided that the regular
-expression matches the string). We show that $(iii)$ our inductive
-definition of a POSIX value is equivalent to an alternative definition
-by Okui and Suzuki which identifies POSIX values as least elements
-according to an ordering of values.  We also prove the correctness of
-Sulzmann's bitcoded version of the POSIX matching algorithm and extend the
-results to additional constructors for regular expressions.  \smallskip
-
-{\bf Keywords:} POSIX matching, Derivatives of Regular Expressions,
-Isabelle/HOL
+  Sulzmann and Lu described a lexing algorithm that calculates
+  Brzozowski derivatives using bitcodes annotated to regular
+  expressions.  Their algorithm generates POSIX values which encode
+  the information of \emph{how} a regular expression matches a
+  string---that is, which part of the string is matched by which part
+  of the regular expression.  The purpose of the bitcodes is to generate POSIX values incrementally while
+  derivatives are calculated. They also help with designing
+  an `aggressive' simplification function that keeps the size of
+  derivatives small. Without simplification derivatives can grow
+  exponentially resulting in an extremely slow lexing algorithm.  In this
+  paper we describe a variant of Sulzmann and Lu's algorithm: Our
+  algorithm is a recursive functional program, whereas Sulzmann
+  and Lu's version involves a fixpoint construction. We \textit{(i)}
+  prove in Isabelle/HOL that our program is correct and generates
+  unique POSIX values; we also \textit{(ii)} establish a polynomial
+  bound for the size of the derivatives. The size can be seen as a
+  proxy measure for the efficiency of the lexing algorithm: because of
+  the polynomial bound our algorithm does not suffer from
+  the exponential blowup in earlier works.
+  
+  % Brzozowski introduced the notion of derivatives for regular
+  % expressions. They can be used for a very simple regular expression
+  % matching algorithm.  Sulzmann and Lu cleverly extended this
+  % algorithm in order to deal with POSIX matching, which is the
+  % underlying disambiguation strategy for regular expressions needed
+  % in lexers.  Their algorithm generates POSIX values which encode
+  % the information of \emph{how} a regular expression matches a
+  % string---that is, which part of the string is matched by which
+  % part of the regular expression.  In this paper we give our
+  % inductive definition of what a POSIX value is and show $(i)$ that
+  % such a value is unique (for given regular expression and string
+  % being matched) and $(ii)$ that Sulzmann and Lu's algorithm always
+  % generates such a value (provided that the regular expression
+  % matches the string). We show that $(iii)$ our inductive definition
+  % of a POSIX value is equivalent to an alternative definition by
+  % Okui and Suzuki which identifies POSIX values as least elements
+  % according to an ordering of values.  We also prove the correctness
+  % of Sulzmann's bitcoded version of the POSIX matching algorithm and
+  % extend the results to additional constructors for regular
+  % expressions.  \smallskip
 \end{abstract}
 
 
--- a/thys2/SizeBound4.thy	Sun Jan 30 23:36:31 2022 +0000
+++ b/thys2/SizeBound4.thy	Sun Jan 30 23:37:29 2022 +0000
@@ -132,15 +132,6 @@
   apply(auto)
   done
 
-lemma fuse_Nil:
-  shows "fuse [] r = r"
-  by (induct r)(simp_all)
-
-(*
-lemma map_fuse_Nil:
-  shows "map (fuse []) rs = rs"
-  by (induct rs)(simp_all add: fuse_Nil)
-*)
 
 fun intern :: "rexp \<Rightarrow> arexp" where
   "intern ZERO = AZERO"
@@ -155,7 +146,7 @@
 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where
   "retrieve (AONE bs) Void = bs"
 | "retrieve (ACHAR bs c) (Char d) = bs"
-| "retrieve (AALTs bs [r]) v = bs @ retrieve r v" 
+| "retrieve (AALTs bs [r]) v = bs @ retrieve r v"
 | "retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v"
 | "retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v"
 | "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2"
@@ -225,8 +216,8 @@
 | "bders r (c#s) = bders (bder c r) s"
 
 lemma bders_append:
-  "bders r (s1 @ s2) = bders (bders r s1) s2"
-  apply(induct s1 arbitrary: r s2)
+  "bders c (s1 @ s2) = bders (bders c s1) s2"
+  apply(induct s1 arbitrary: c s2)
   apply(simp_all)
   done
 
@@ -274,29 +265,28 @@
   apply(simp_all)
   done
 
-
 lemma retrieve_fuse2:
   assumes "\<Turnstile> v : (erase r)"
   shows "retrieve (fuse bs r) v = bs @ retrieve r v"
   using assms
   apply(induct r arbitrary: v bs)
-         apply(auto elim: Prf_elims)[4]
-   defer
-  using retrieve_encode_STARS
-   apply(auto elim!: Prf_elims)[1]
-   apply(case_tac vs)
-    apply(simp)
-   apply(simp)
-  (* AALTs  case *)
+  apply(auto elim: Prf_elims)[4]
+  apply(case_tac x2a)
+  apply(simp)
+  using Prf_elims(1) apply blast
+  apply(case_tac x2a)
+  apply(simp)
+  apply(simp)
+  apply(case_tac list)
   apply(simp)
-  apply(case_tac x2a)
-   apply(simp)
-   apply(auto elim!: Prf_elims)[1]
+  apply(simp)
+  apply (smt (verit, best) Prf_elims(3) append_assoc retrieve.simps(4) retrieve.simps(5))
   apply(simp)
-   apply(case_tac list)
-   apply(simp)
-  apply(auto)
+  using retrieve_encode_STARS
   apply(auto elim!: Prf_elims)[1]
+  apply(case_tac vs)
+  apply(simp)
+  apply(simp)
   done
 
 lemma retrieve_fuse:
@@ -314,139 +304,92 @@
   apply(simp_all add: retrieve_fuse retrieve_encode_STARS)
   done
 
-(*
-lemma bnullable_Hdbmkeps_Hd:
-  assumes "bnullable a" 
-  shows  "bmkeps (AALTs bs (a # rs)) = bs @ (bmkeps a)"
-  using assms by simp
-*)
 
-
-lemma r2:
-  assumes "x \<in> set rs" "bnullable x"
-  shows "bnullable (AALTs bs rs)"
+lemma retrieve_AALTs_bnullable1:
+  assumes "bnullable r"
+  shows "retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs))))
+         = bs @ retrieve r (mkeps (erase r))"
   using assms
-  apply(induct rs)
-   apply(auto)
+  apply(case_tac rs)
+  apply(auto simp add: bnullable_correctness)
   done
 
-lemma  r3:
-  assumes "\<not> bnullable r" 
-          "bnullables rs"
-  shows "retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs))) =
-         retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs))))"
+lemma retrieve_AALTs_bnullable2:
+  assumes "\<not>bnullable r" "bnullables rs"
+  shows "retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs))))
+         = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))"
   using assms
   apply(induct rs arbitrary: r bs)
-   apply(auto)[1]
   apply(auto)
   using bnullable_correctness apply blast
-    apply(auto simp add: bnullable_correctness mkeps_nullable retrieve_fuse2)
-   apply(subst retrieve_fuse2[symmetric])
-  apply (smt bnullable.simps(4) bnullable_correctness erase.simps(5) erase.simps(6) insert_iff list.exhaust list.set(2) mkeps.simps(3) mkeps_nullable)
-   apply(simp)
-  apply(case_tac "bnullable a")
-  apply (smt append_Nil2 bnullable.simps(4) bnullable_correctness erase.simps(5) erase.simps(6) fuse.simps(4) insert_iff list.exhaust list.set(2) mkeps.simps(3) mkeps_nullable retrieve_fuse2)
-  apply(drule_tac x="a" in meta_spec)
-  apply(drule_tac x="bs" in meta_spec)
-  apply(drule meta_mp)
-   apply(simp)
-  apply(drule meta_mp)
-   apply(auto)
-  apply(subst retrieve_fuse2[symmetric])
   apply(case_tac rs)
-    apply(simp)
-   apply(auto)[1]
-      apply (simp add: bnullable_correctness)
-  
-  apply (metis append_Nil2 bnullable_correctness erase_fuse fuse.simps(4) list.set_intros(1) mkeps.simps(3) mkeps_nullable nullable.simps(4) r2)
-    apply (simp add: bnullable_correctness)
-  apply (metis append_Nil2 bnullable_correctness erase.simps(6) erase_fuse fuse.simps(4) list.set_intros(2) mkeps.simps(3) mkeps_nullable r2)
-  apply(simp)
+  apply(auto)
+  using bnullable_correctness apply blast
+  apply(case_tac rs)
+  apply(auto)
   done
 
-lemma t: 
+lemma bmkeps_retrieve_AALTs: 
   assumes "\<forall>r \<in> set rs. bnullable r \<longrightarrow> bmkeps r = retrieve r (mkeps (erase r))" 
           "bnullables rs"
   shows "bs @ bmkepss rs = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))"
  using assms
   apply(induct rs arbitrary: bs)
   apply(auto)
-  apply (metis (no_types, opaque_lifting) bmkepss.cases bnullable_correctness erase.simps(5) erase.simps(6) mkeps.simps(3) retrieve.simps(3) retrieve.simps(4))
-  apply (metis r3)
-  apply (metis (no_types, lifting) bmkepss.cases bnullable_correctness empty_iff erase.simps(6) list.set(1) mkeps.simps(3) retrieve.simps(4))
-  apply (metis r3)
-  done
-      
+  using retrieve_AALTs_bnullable1 apply presburger
+  apply (metis retrieve_AALTs_bnullable2)
+  apply (simp add: retrieve_AALTs_bnullable1)
+  by (metis retrieve_AALTs_bnullable2)
+
+    
 lemma bmkeps_retrieve:
   assumes "bnullable r"
   shows "bmkeps r = retrieve r (mkeps (erase r))"
   using assms
   apply(induct r)
-  apply(auto)
-  using t by auto
+  apply(auto)  
+  using bmkeps_retrieve_AALTs by auto
 
 lemma bder_retrieve:
   assumes "\<Turnstile> v : der c (erase r)"
   shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)"
   using assms  
   apply(induct r arbitrary: v rule: erase.induct)
-         apply(simp)
-         apply(erule Prf_elims)
-        apply(simp)
-        apply(erule Prf_elims) 
-        apply(simp)
-      apply(case_tac "c = ca")
-       apply(simp)
-       apply(erule Prf_elims)
-       apply(simp)
-      apply(simp)
-       apply(erule Prf_elims)
-  apply(simp)
-      apply(erule Prf_elims)
-     apply(simp)
-    apply(simp)
-  apply(rename_tac "r\<^sub>1" "r\<^sub>2" rs v)
-    apply(erule Prf_elims)
-     apply(simp)
-    apply(simp)
-    apply(case_tac rs)
-     apply(simp)
-    apply(simp)
-  apply (smt Prf_elims(3) injval.simps(2) injval.simps(3) retrieve.simps(4) retrieve.simps(5) same_append_eq)
-   apply(simp)
-   apply(case_tac "nullable (erase r1)")
-    apply(simp)
-  apply(erule Prf_elims)
-     apply(subgoal_tac "bnullable r1")
-  prefer 2
-  using bnullable_correctness apply blast
-    apply(simp)
-     apply(erule Prf_elims)
-     apply(simp)
-   apply(subgoal_tac "bnullable r1")
-  prefer 2
-  using bnullable_correctness apply blast
-    apply(simp)
-    apply(simp add: retrieve_fuse2)
-    apply(simp add: bmkeps_retrieve)
-   apply(simp)
-   apply(erule Prf_elims)
-   apply(simp)
-  using bnullable_correctness apply blast
-  apply(rename_tac bs r v)
+  using Prf_elims(1) apply auto[1]
+  using Prf_elims(1) apply auto[1]
+  apply(auto)[1]
+  apply (metis Prf_elims(4) injval.simps(1) retrieve.simps(1) retrieve.simps(2))
+  using Prf_elims(1) apply blast
+  (* AALTs case *)
   apply(simp)
   apply(erule Prf_elims)
-     apply(clarify)
+  apply(simp)
+  apply(simp)
+  apply(rename_tac "r\<^sub>1" "r\<^sub>2" rs v)
+  apply(erule Prf_elims)
+  apply(simp)
+  apply(simp)
+  apply(case_tac rs)
+  apply(simp)
+  apply(simp)
+  using Prf_elims(3) apply fastforce
+  (* ASEQ case *) 
+  apply(simp)
+  apply(case_tac "nullable (erase r1)")
+  apply(simp)
+  apply(erule Prf_elims)
+  using Prf_elims(2) bnullable_correctness apply force
+  apply (simp add: bmkeps_retrieve bnullable_correctness retrieve_fuse2)
+  apply (simp add: bmkeps_retrieve bnullable_correctness retrieve_fuse2)
+  using Prf_elims(2) apply force
+  (* ASTAR case *)  
+  apply(rename_tac bs r v)
+  apply(simp)  
   apply(erule Prf_elims)
   apply(clarify)
-  apply(subst injval.simps)
-  apply(simp del: retrieve.simps)
-  apply(subst retrieve.simps)
-  apply(subst retrieve.simps)
-  apply(simp)
-  apply(simp add: retrieve_fuse2)
-  done
-  
+  apply(erule Prf_elims)
+  apply(clarify)
+  by (simp add: retrieve_fuse2)
 
 
 lemma MAIN_decode:
@@ -514,7 +457,7 @@
      (if (f x) \<in> acc then distinctBy xs f acc 
       else x # (distinctBy xs f ({f x} \<union> acc)))"
 
- 
+  
 
 fun flts :: "arexp list \<Rightarrow> arexp list"
   where 
@@ -581,84 +524,12 @@
   apply(simp_all)
   done
 
-lemma L_bsimp_ASEQ:
-  "L (erase (ASEQ bs r1 r2)) = L (erase (bsimp_ASEQ bs r1 r2))"
-  apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
-  apply(simp_all)
-  by (metis erase_fuse fuse.simps(4))
-
-lemma L_bsimp_AALTs:
-  "L (erase (AALTs bs rs)) = L (erase (bsimp_AALTs bs rs))"
-  apply(induct bs rs rule: bsimp_AALTs.induct)
-  apply(simp_all add: erase_fuse)
-  done
-
-lemma L_erase_AALTs:
-  shows "L (erase (AALTs bs rs)) = \<Union> (L ` erase ` (set rs))"
-  apply(induct rs)
-   apply(simp)
-  apply(simp)
-  apply(case_tac rs)
-   apply(simp)
-  apply(simp)
-  done
-
-lemma L_erase_flts:
-  shows "\<Union> (L ` erase ` (set (flts rs))) = \<Union> (L ` erase ` (set rs))"
-  apply(induct rs rule: flts.induct)
-  apply(simp_all)
-  apply(auto)
-  using L_erase_AALTs erase_fuse apply auto[1]
-  by (simp add: L_erase_AALTs erase_fuse)
-
-lemma L_erase_dB_acc:
-  shows "(\<Union> (L ` acc) \<union> (\<Union> (L ` erase ` (set (distinctBy rs erase acc))))) 
-            = \<Union> (L ` acc) \<union>  \<Union> (L ` erase ` (set rs))"
-  apply(induction rs arbitrary: acc)
-  apply simp_all
-  by (smt (z3) SUP_absorb UN_insert sup_assoc sup_commute)
-
-
-lemma L_erase_dB:
-  shows "(\<Union> (L ` erase ` (set (distinctBy rs erase {})))) = \<Union> (L ` erase ` (set rs))"
-  by (metis L_erase_dB_acc Un_commute Union_image_empty)
-
-lemma L_bsimp_erase:
-  shows "L (erase r) = L (erase (bsimp r))"
-  apply(induct r)
-  apply(simp)
-  apply(simp)
-  apply(simp)
-  apply(auto simp add: Sequ_def)[1]
-  apply(subst L_bsimp_ASEQ[symmetric])
-  apply(auto simp add: Sequ_def)[1]
-  apply(subst (asm)  L_bsimp_ASEQ[symmetric])
-  apply(auto simp add: Sequ_def)[1]
-  apply(simp)
-  apply(subst L_bsimp_AALTs[symmetric])
-  defer
-  apply(simp)
-  apply(subst (2)L_erase_AALTs)  
-  apply(subst L_erase_dB)
-  apply(subst L_erase_flts)
-  apply (simp add: L_erase_AALTs)
-  done
-
-lemma L_bders_simp:
-  shows "L (erase (bders_simp r s)) = L (erase (bders r s))"
-  apply(induct s arbitrary: r rule: rev_induct)
-  apply(simp)
-  apply(simp)
-  apply(simp add: ders_append)
-  apply(simp add: bders_simp_append)
-  apply(simp add: L_bsimp_erase[symmetric])
-  by (simp add: der_correctness)
-
 
 lemma bmkeps_fuse:
   assumes "bnullable r"
   shows "bmkeps (fuse bs r) = bs @ bmkeps r"
-  by (metis assms bmkeps_retrieve bnullable_correctness erase_fuse mkeps_nullable retrieve_fuse2)
+  using assms
+  by (metis bmkeps_retrieve bnullable_correctness erase_fuse mkeps_nullable retrieve_fuse2)
 
 lemma bmkepss_fuse: 
   assumes "bnullables rs"
@@ -668,21 +539,10 @@
   apply(auto simp add: bmkeps_fuse bnullable_fuse)
   done
 
-
-lemma b4:
-  shows "bnullable (bders_simp r s) = bnullable (bders r s)"
-proof -
-  have "L (erase (bders_simp r s)) = L (erase (bders r s))"
-    using L_bders_simp by force
-  then show "bnullable (bders_simp r s) = bnullable (bders r s)"
-    using bnullable_correctness nullable_correctness by blast
-qed
-
-
 lemma bder_fuse:
   shows "bder c (fuse bs a) = fuse bs  (bder c a)"
   apply(induct a arbitrary: bs c)
-       apply(simp_all)
+  apply(simp_all)
   done
 
 
@@ -700,7 +560,7 @@
 | bs5: "r3 \<leadsto> r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r1 r4"
 | bs6: "AALTs bs [] \<leadsto> AZERO"
 | bs7: "AALTs bs [r] \<leadsto> fuse bs r"
-| bs10: "rs1 s\<leadsto> rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto> AALTs bs rs2"
+| bs8: "rs1 s\<leadsto> rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto> AALTs bs rs2"
 | ss1:  "[] s\<leadsto> []"
 | ss2:  "rs1 s\<leadsto> rs2 \<Longrightarrow> (r # rs1) s\<leadsto> (r # rs2)"
 | ss3:  "r1 \<leadsto> r2 \<Longrightarrow> (r1 # rs) s\<leadsto> (r2 # rs)"
@@ -726,11 +586,6 @@
   shows "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
   using rrewrites.intros(1) rrewrites.intros(2) by blast
 
-lemma srewrites_single : 
-  shows "rs1 s\<leadsto> rs2 \<Longrightarrow> rs1 s\<leadsto>* rs2"
-  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"
@@ -753,13 +608,13 @@
   "rs1 s\<leadsto>* rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto>* AALTs bs rs2"
   apply(induct rs1 rs2 rule: srewrites.inducts)
    apply simp
-  using bs10 r_in_rstar rrewrites_trans by blast
+  using bs8 r_in_rstar rrewrites_trans by blast
 
 lemma contextrewrites1: 
   "r \<leadsto>* r' \<Longrightarrow> AALTs bs (r # rs) \<leadsto>* AALTs bs (r' # rs)"
   apply(induct r r' rule: rrewrites.induct)
    apply simp
-  using bs10 ss3 by blast
+  using bs8 ss3 by blast
 
 lemma srewrite1: 
   shows "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs @ rs1) s\<leadsto> (rs @ rs2)"
@@ -777,9 +632,9 @@
   shows  "r1 \<leadsto> r2 \<Longrightarrow> True"
   and "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)"
   apply(induct rule: rrewrite_srewrite.inducts)
-               apply(auto)
-     apply (metis append_Cons append_Nil srewrites1)
-    apply(meson srewrites.simps ss3)
+  apply(auto)
+  apply (metis append_Cons append_Nil srewrites1)
+  apply(meson srewrites.simps ss3)
   apply (meson srewrites.simps ss4)
   apply (meson srewrites.simps ss5)
   by (metis append_Cons append_Nil srewrites.simps ss6)
@@ -806,15 +661,15 @@
   shows "[r1] s\<leadsto>* [r2]"
   using assms
   apply(induct r1 r2 rule: rrewrites.induct)
-   apply(auto)
+  apply(auto)
   by (meson srewrites.simps srewrites_trans ss3)
 
 lemma srewrites7:
   assumes "rs3 s\<leadsto>* rs4" "r1 \<leadsto>* r2" 
   shows "(r1 # rs3) s\<leadsto>* (r2 # rs4)"
   using assms
-  by (smt (verit, best) append_Cons append_Nil srewrites1 srewrites3 srewrites6 srewrites_trans)
-
+  by (smt (verit, del_insts) append.simps srewrites1 srewrites3 srewrites6 srewrites_trans)
+  
 lemma ss6_stronger_aux:
   shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ distinctBy rs2 erase (set (map erase rs1)))"
   apply(induct rs2 arbitrary: rs1)
@@ -828,47 +683,47 @@
   shows "rs1 s\<leadsto>* distinctBy rs1 erase {}"
   using ss6_stronger_aux[of "[]" _] by auto
 
-
 lemma rewrite_preserves_fuse: 
   shows "r2 \<leadsto> r3 \<Longrightarrow> fuse bs r2 \<leadsto> fuse bs r3"
-  and   "rs2 s\<leadsto> rs3 \<Longrightarrow> map (fuse bs) rs2 s\<leadsto>* map (fuse bs) rs3"
+  and   "rs2 s\<leadsto> rs3 \<Longrightarrow> map (fuse bs) rs2 s\<leadsto> map (fuse bs) rs3"
 proof(induct rule: rrewrite_srewrite.inducts)
   case (bs3 bs1 bs2 r)
-  then show ?case
+  then show "fuse bs (ASEQ bs1 (AONE bs2) r) \<leadsto> fuse bs (fuse (bs1 @ bs2) r)"
     by (metis fuse.simps(5) fuse_append rrewrite_srewrite.bs3) 
 next
-  case (bs7 bs r)
-  then show ?case
+  case (bs7 bs1 r)
+  then show "fuse bs (AALTs bs1 [r]) \<leadsto> fuse bs (fuse bs1 r)"
     by (metis fuse.simps(4) fuse_append rrewrite_srewrite.bs7) 
 next
   case (ss2 rs1 rs2 r)
-  then show ?case
-    using srewrites7 by force 
+  then show "map (fuse bs) (r # rs1) s\<leadsto> map (fuse bs) (r # rs2)"
+    by (simp add: rrewrite_srewrite.ss2)
 next
   case (ss3 r1 r2 rs)
-  then show ?case by (simp add: r_in_rstar srewrites7)
+  then show "map (fuse bs) (r1 # rs) s\<leadsto> map (fuse bs) (r2 # rs)"
+    by (simp add: rrewrite_srewrite.ss3)
 next
   case (ss5 bs1 rs1 rsb)
-  then show ?case 
-    apply(simp)
-    by (metis (mono_tags, lifting) comp_def fuse_append map_eq_conv rrewrite_srewrite.ss5 srewrites.simps)
+  have "map (fuse bs) (AALTs bs1 rs1 # rsb) = AALTs (bs @ bs1) rs1 # (map (fuse bs) rsb)" by simp
+  also have "... s\<leadsto> ((map (fuse (bs @ bs1)) rs1) @ (map (fuse bs) rsb))"
+    by (simp add: rrewrite_srewrite.ss5)  
+  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)
-  then show ?case 
+  then show "map (fuse bs) (rsa @ [a1] @ rsb @ [a2] @ rsc) s\<leadsto> map (fuse bs) (rsa @ [a1] @ rsb @ rsc)"
     apply(simp)
-    apply(rule srewrites_single)
     apply(rule rrewrite_srewrite.ss6[simplified])
     apply(simp add: erase_fuse)
     done
- qed (auto intro: rrewrite_srewrite.intros)
-
+qed (auto intro: rrewrite_srewrite.intros)
 
 lemma rewrites_fuse:  
   assumes "r1 \<leadsto>* r2"
   shows "fuse bs r1 \<leadsto>* fuse bs r2"
 using assms
 apply(induction r1 r2 arbitrary: bs rule: rrewrites.induct)
-apply(auto intro: rewrite_preserves_fuse rrewrites_trans)
+apply(auto intro: rewrite_preserves_fuse)
 done
 
 
@@ -911,13 +766,12 @@
   by (smt (verit) bs6 bs7 bsimp_AALTs.elims rrewrites.simps)
 
 lemma trivialbsimp_srewrites: 
-  "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs s\<leadsto>* (map f rs)"
+  assumes "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x"
+  shows "rs s\<leadsto>* (map f rs)"
+using assms
   apply(induction rs)
-   apply simp
-  apply(simp)
-  using srewrites7 by auto
-
-
+  apply(simp_all add: srewrites7)
+  done
 
 lemma fltsfrewrites: "rs s\<leadsto>* flts rs"
   apply(induction rs rule: flts.induct)
@@ -1044,7 +898,7 @@
 
 lemma to_zero_in_alt: 
   shows "AALT bs (ASEQ [] AZERO r) r2 \<leadsto> AALT bs AZERO r2"
-  by (simp add: bs1 bs10 ss3)
+  by (simp add: bs1 bs8 ss3)
 
 
 
@@ -1054,7 +908,6 @@
   apply(simp_all add: bder_fuse)
   done
 
-
 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"
@@ -1072,7 +925,7 @@
   case (bs3 bs1 bs2 r)
   show "bder c (ASEQ bs1 (AONE bs2) r) \<leadsto>* bder c (fuse (bs1 @ bs2) r)"
     apply(simp)
-    by (metis (no_types, lifting) bder_fuse bs10 bs7 fuse_append rrewrites.simps ss4 to_zero_in_alt)
+    by (metis (no_types, lifting) bder_fuse bs8 bs7 fuse_append rrewrites.simps ss4 to_zero_in_alt)
 next
   case (bs4 r1 r2 bs r3)
   have as: "r1 \<leadsto> r2" by fact
@@ -1097,7 +950,7 @@
   show "bder c (AALTs bs [r]) \<leadsto>* bder c (fuse bs r)"
     by (simp add: bder_fuse r_in_rstar rrewrite_srewrite.bs7) 
 next
-  case (bs10 rs1 rs2 bs)
+  case (bs8 rs1 rs2 bs)
   have IH1: "map (bder c) rs1 s\<leadsto>* map (bder c) rs2" by fact
   then show "bder c (AALTs bs rs1) \<leadsto>* bder c (AALTs bs rs2)" 
     using contextrewrites0 by force    
@@ -1168,12 +1021,10 @@
 qed  
 
 
-
-
 theorem main_blexer_simp: 
   shows "blexer r s = blexer_simp r s"
   unfolding blexer_def blexer_simp_def
-  using b4 main_aux by simp
+  by (metis central main_aux rewrites_bnullable_eq)
 
 
 theorem blexersimp_correctness: 
@@ -1181,6 +1032,79 @@
   using blexer_correctness main_blexer_simp by simp
 
 
+(* 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)
+  apply(auto)
+  done
+
+lemma bsimp_AALTs_fuse:
+  assumes "\<forall>r \<in> set rs. fuse bs1 (fuse bs2 r) = fuse (bs1 @ bs2) r"
+  shows "fuse bs1 (bsimp_AALTs bs2 rs) = bsimp_AALTs (bs1 @ bs2) rs"
+  using assms
+  apply(induct bs2 rs arbitrary: bs1 rule: bsimp_AALTs.induct)
+  apply(auto)
+  done
+
+lemma bsimp_fuse:
+  shows "fuse bs (bsimp r) = bsimp (fuse bs r)"
+  apply(induct r arbitrary: bs)
+  apply(simp_all add: bsimp_ASEQ_fuse bsimp_AALTs_fuse fuse_append)
+  done
+
+lemma bsimp_ASEQ_idem:
+  assumes "bsimp (bsimp r1) = bsimp r1" "bsimp (bsimp r2) = bsimp r2"
+  shows "bsimp (bsimp_ASEQ x1 (bsimp r1) (bsimp r2)) = bsimp_ASEQ x1 (bsimp r1) (bsimp r2)"
+  using assms
+  apply(case_tac "bsimp r1 = AZERO")
+  apply(simp)
+  apply(case_tac "bsimp r2 = AZERO")
+  apply(simp)
+  apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
+  apply(auto)[1]
+  apply (metis bsimp_fuse)
+  apply(simp add: bsimp_ASEQ1)
+  done  
+
+lemma bsimp_AALTs_idem:
+  assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r" 
+  shows "bsimp (bsimp_AALTs bs rs) = bsimp_AALTs bs (map bsimp rs)" 
+  using assms
+  apply(induct bs rs rule: bsimp_AALTs.induct)
+  apply(simp)
+   apply(simp)
+  using bsimp_fuse apply presburger
+  oops   
+  
+lemma bsimp_idem_rev:
+  shows "\<nexists>r2. bsimp r1 \<leadsto> r2"
+  apply(induct r1 rule: bsimp.induct)
+  apply(auto)
+  defer
+  defer
+  using rrewrite.simps apply blast
+  using rrewrite.cases apply blast
+  using rrewrite.simps apply blast
+  using rrewrite.cases apply blast
+  apply(case_tac "bsimp r1 = AZERO")
+  apply(simp)
+  apply(case_tac "bsimp r2 = AZERO")
+  apply(simp)
+  apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
+  apply(auto)[1]
+  prefer 2
+  apply (smt (verit, best) arexp.distinct(25) arexp.inject(3) bsimp_ASEQ1 rrewrite.simps)
+  defer
+  oops
+
+lemma bsimp_idem:
+  shows "bsimp (bsimp r) = bsimp r"
+  apply(induct r rule: bsimp.induct)
+  apply(auto)
+  using bsimp_ASEQ_idem apply presburger
+  oops
 
 export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers
 
Binary file thys2/paper.pdf has changed