# HG changeset patch
# User Christian Urban <christian.urban@kcl.ac.uk>
# Date 1643371345 0
# Node ID dac6d27c99c63cbf59c022a261987cd7354606f2
# Parent  e1b74d618f1b013a023bf9d35e4b3fccd689bdbe
updated

diff -r e1b74d618f1b -r dac6d27c99c6 thys2/Paper/Paper.thy
--- a/thys2/Paper/Paper.thy	Thu Jan 27 23:25:26 2022 +0000
+++ b/thys2/Paper/Paper.thy	Fri Jan 28 12:02:25 2022 +0000
@@ -10,6 +10,11 @@
 
 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"
 
@@ -157,6 +162,30 @@
    problem with retrieve 
 
    correctness
+
+
+
+   \begin{figure}[t]
+  \begin{center}
+  \begin{tabular}{c}
+  @{thm[mode=Axiom] bs1}\qquad
+  @{thm[mode=Axiom] bs2}\qquad
+  @{thm[mode=Axiom] bs3}\\
+  @{thm[mode=Rule] bs4}\qquad
+  @{thm[mode=Rule] bs5}\\
+  @{thm[mode=Rule] bs6}\qquad
+  @{thm[mode=Rule] bs7}\\
+  @{thm[mode=Rule] bs8}\\
+  @{thm[mode=Axiom] ss1}\qquad
+  @{thm[mode=Rule] ss2}\qquad
+  @{thm[mode=Rule] ss3}\\
+  @{thm[mode=Axiom] ss4}\qquad
+  @{thm[mode=Axiom] ss5}\qquad
+  @{thm[mode=Rule] ss6}\\
+  \end{tabular}
+  \end{center}
+  \caption{???}\label{SimpRewrites}
+  \end{figure}
 *}
 
 section {* Bound - NO *}
diff -r e1b74d618f1b -r dac6d27c99c6 thys2/Paper/document/root.tex
--- a/thys2/Paper/document/root.tex	Thu Jan 27 23:25:26 2022 +0000
+++ b/thys2/Paper/document/root.tex	Fri Jan 28 12:02:25 2022 +0000
@@ -45,6 +45,7 @@
 \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}
diff -r e1b74d618f1b -r dac6d27c99c6 thys2/SizeBound4.thy
--- a/thys2/SizeBound4.thy	Thu Jan 27 23:25:26 2022 +0000
+++ b/thys2/SizeBound4.thy	Fri Jan 28 12:02:25 2022 +0000
@@ -216,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
 
@@ -265,7 +265,6 @@
   apply(simp_all)
   done
 
-
 lemma retrieve_fuse2:
   assumes "\<Turnstile> v : (erase r)"
   shows "retrieve (fuse bs r) v = bs @ retrieve r v"
@@ -529,7 +528,8 @@
 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"
@@ -542,7 +542,7 @@
 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
 
 
@@ -560,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)"
@@ -586,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"
@@ -613,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)"
@@ -637,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)
@@ -666,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)
@@ -688,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)
 
-
 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
 
 
@@ -771,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)
@@ -904,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)
 
 
 
@@ -914,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"
@@ -932,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
@@ -957,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    
@@ -1028,8 +1021,6 @@
 qed  
 
 
-
-
 theorem main_blexer_simp: 
   shows "blexer r s = blexer_simp r s"
   unfolding blexer_def blexer_simp_def
@@ -1042,6 +1033,13 @@
 
 
 
+lemma asize_idem:
+  shows "asize (bsimp (bsimp r)) = asize (bsimp r)"
+  apply(induct r rule: bsimp.induct)
+  apply(auto)
+  prefer 2
+  oops
+
 export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers
 
 
diff -r e1b74d618f1b -r dac6d27c99c6 thys2/paper.pdf
Binary file thys2/paper.pdf has changed