# HG changeset patch
# User Christian Urban <christian.urban@kcl.ac.uk>
# Date 1635988054 0
# Node ID 320f923c77b96071686aa87ef83330548901d432
# Parent  78cc255e286fac1702c5f01f4375ea18f4d88871
slightly

diff -r 78cc255e286f -r 320f923c77b9 thys2/SizeBound.thy
--- a/thys2/SizeBound.thy	Tue Nov 02 19:42:52 2021 +0000
+++ b/thys2/SizeBound.thy	Thu Nov 04 01:07:34 2021 +0000
@@ -766,18 +766,9 @@
 | "nonnested (AALTs bs2 (r # rs2)) = nonnested (AALTs bs2 rs2)"
 | "nonnested r = True"
 
-
-lemma  k0:
-  shows "flts (r # rs1) = flts [r] @ flts rs1"
-  apply(induct r arbitrary: rs1)
-   apply(auto)
-  done
-
-lemma  k00:
-  shows "flts (rs1 @ rs2) = flts rs1 @ flts rs2"
-  apply(induct rs1 arbitrary: rs2)
-   apply(auto)
-  by (metis append.assoc k0)
+lemma flts_append:
+  shows "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
+by (induct xs1  arbitrary: xs2  rule: flts.induct)(auto)
 
 lemma  k0a:
   shows "flts [AALTs bs rs] = map (fuse bs)  rs"
@@ -785,12 +776,6 @@
   done
 
 
-
-
-
-
-
-
 lemma bsimp_AALTs_qq:
   assumes "1 < length rs"
   shows "bsimp_AALTs bs rs = AALTs bs  rs"
@@ -811,17 +796,7 @@
 
 
 
-lemma flts_append:
-  "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
-  apply(induct xs1  arbitrary: xs2  rule: rev_induct)
-   apply(auto)
-  apply(case_tac xs)
-   apply(auto)
-   apply(case_tac x)
-        apply(auto)
-  apply(case_tac x)
-        apply(auto)
-  done
+
 
 fun nonazero :: "arexp \<Rightarrow> bool"
   where
@@ -940,38 +915,6 @@
   done
 
 
-fun flts2 :: "char \<Rightarrow> arexp list \<Rightarrow> arexp list"
-  where 
-  "flts2 _ [] = []"
-| "flts2 c (AZERO # rs) = flts2 c rs"
-| "flts2 c (AONE _ # rs) = flts2 c rs"
-| "flts2 c (ACHAR bs d # rs) = (if c = d then (ACHAR bs d # flts2 c rs) else flts2 c rs)"
-| "flts2 c ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ flts2 c rs"
-| "flts2 c (ASEQ bs r1 r2 # rs) = (if (bnullable(r1) \<and> r2 = AZERO) then 
-    flts2 c rs
-    else ASEQ bs r1 r2 # flts2 c rs)"
-| "flts2 c (r1 # rs) = r1 # flts2 c rs"
-
-
-
-
-
-
-
-
- 
-
-
-
-
-lemma WQ1:
-  assumes "s \<in> L (der c r)"
-  shows "s \<in> der c r \<rightarrow> mkeps (ders s (der c r))"
-  using assms
-  oops
-
-
-
 lemma bder_bsimp_AALTs:
   shows "bder c (bsimp_AALTs bs rs) = bsimp_AALTs bs (map (bder c) rs)"
   apply(induct bs rs rule: bsimp_AALTs.induct)  
@@ -983,20 +926,6 @@
 
 
 
-lemma
-  assumes "asize (bsimp a) = asize a"  "a = AALTs bs [AALTs bs2 [], AZERO, AONE bs3]"
-  shows "bsimp a = a"
-  using assms
-  apply(simp)
-  oops
-
-
-
-
-
-
-
-
 inductive rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
   where
   "ASEQ bs AZERO r2 \<leadsto> AZERO"
@@ -1036,7 +965,7 @@
 lemma r_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
   using rrewrites.intros(1) rrewrites.intros(2) by blast
  
-lemma real_trans: 
+lemma real_trans [trans]: 
   assumes a1: "r1 \<leadsto>* r2"  and a2: "r2 \<leadsto>* r3"
   shows "r1 \<leadsto>* r3"
   using a2 a1
@@ -1146,7 +1075,7 @@
 
 
 lemma flts_prepend: "\<lbrakk>nonalt a; nonazero a\<rbrakk> \<Longrightarrow> flts (a#rs) = a # (flts rs)"
-  by (metis append_Cons append_Nil flts_single1 k00)
+  by (metis append_Cons append_Nil flts_single1 flts_append)
 
 lemma fltsfrewrites: "rs f\<leadsto>* (flts rs)"
   apply(induction rs)
@@ -1221,7 +1150,7 @@
    apply(subgoal_tac "(a#rs) f\<leadsto>* (a#flts rs)")
   apply (metis append_Nil frewritesaalts)
   apply (meson fltsfrewrites fs4 nonalt.elims(3) nonazero.elims(3))
-  by (metis append_Cons append_Nil fltsfrewrites frewritesaalts k00 k0a)
+  by (metis append_Cons append_Nil fltsfrewrites frewritesaalts flts_append k0a)
 
 lemma alts_simpalts: "\<And>bs1 rs. (\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimp x) \<Longrightarrow> 
 AALTs bs1 rs \<leadsto>* AALTs bs1 (map bsimp rs)"
@@ -1345,38 +1274,36 @@
   using alts_simpalts by force
 
 
-lemma rewritenullable: "\<lbrakk>r1 \<leadsto> r2; bnullable r1 \<rbrakk> \<Longrightarrow> bnullable r2"
-  apply(induction r1 r2 rule: rrewrite.induct)
-             apply(simp)+
-  apply (metis bnullable_correctness erase_fuse)
-          apply simp
-         apply simp
-        apply auto[1]
-       apply auto[1]
-      apply auto[4]
-     apply (metis UnCI bnullable_correctness erase_fuse imageI)
-    apply (metis bnullable_correctness erase_fuse)
-    apply (metis bnullable_correctness erase_fuse)
-  
-   apply (metis bnullable_correctness erase.simps(5) erase_fuse)
-  
-
-  by (smt (z3) Un_iff bnullable_correctness insert_iff list.set(2) qq3 set_append)
-
 lemma rewrite_non_nullable: "\<lbrakk>r1 \<leadsto> r2; \<not>bnullable r1 \<rbrakk> \<Longrightarrow> \<not>bnullable r2"
   apply(induction r1 r2 rule: rrewrite.induct)
              apply auto 
       apply (metis bnullable_correctness erase_fuse)+
   done
 
+lemma rewrite_non_nullable_strong: 
+  assumes "r1 \<leadsto> r2"
+  shows "bnullable r1 = bnullable r2"
+using assms
+apply(induction r1 r2 rule: rrewrite.induct)
+apply(auto)
+apply(metis bnullable_correctness erase_fuse)+
+apply(metis UnCI bnullable_correctness erase_fuse imageI)
+apply(metis bnullable_correctness erase_fuse)+
+done
 
-lemma rewritesnullable: "\<lbrakk> r1 \<leadsto>* r2; bnullable r1 \<rbrakk> \<Longrightarrow> bnullable r2"
+lemma rewrite_nullable: 
+  assumes "r1 \<leadsto> r2" "bnullable r1"
+  shows "bnullable r2"
+using assms rewrite_non_nullable_strong
+by auto
+
+lemma rewritesnullable: 
+  assumes "r1 \<leadsto>* r2" "bnullable r1"
+  shows "bnullable r2"
+using assms
   apply(induction r1 r2 rule: rrewrites.induct)
-   apply simp
-  apply(rule rewritenullable)
-   apply simp
   apply simp
-  done
+  using rewrite_non_nullable_strong by blast
 
 lemma nonbnullable_lists_concat: " \<lbrakk> \<not> (\<exists>r0\<in>set rs1. bnullable r0); \<not> bnullable r; \<not> (\<exists>r0\<in>set rs2. bnullable r0)\<rbrakk> \<Longrightarrow> 
 \<not>(\<exists>r0 \<in> (set (rs1@[r]@rs2)). bnullable r0 ) "
@@ -1412,30 +1339,6 @@
  \<Longrightarrow> bmkeps (AALTs bs (rs1@[r]@rs2)) = bs @ (bmkeps r)"
   using qq2 bnullable_Hdbmkeps_Hd by force
 
-lemma rrewrite_nbnullable: "\<lbrakk> r1 \<leadsto> r2 ; \<not> bnullable r1 \<rbrakk> \<Longrightarrow> \<not>bnullable r2"
-  apply(induction rule: rrewrite.induct)
-             apply auto[1]
-            apply auto[1]
-           apply auto[1]
-           apply (metis bnullable_correctness erase_fuse)
-          apply auto[1]
-         apply auto[1]
-        apply auto[1]
-       apply auto[1]
-      apply auto[1]
-      apply (metis bnullable_correctness erase_fuse)
-     apply auto[1]
-     apply (metis bnullable_correctness erase_fuse)
-    apply auto[1]
-    apply (metis bnullable_correctness erase_fuse)
-   apply auto[1]
-   apply auto[1]
-
-  apply (metis bnullable_correctness erase_fuse)
-
-  by (meson rewrite_non_nullable rrewrite.intros(13))
-
-
 
 
 lemma spillbmkepslistr: "bnullable (AALTs bs1 rs1)
@@ -1448,7 +1351,7 @@
 lemma third_segment_bnullable: "\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow> 
 bnullable (AALTs bs rs3)"
   
-  by (metis append.left_neutral append_Cons bnullable.simps(1) bnullable_segment rrewrite.intros(7) rrewrite_nbnullable)
+  by (metis append.left_neutral append_Cons bnullable.simps(1) bnullable_segment rrewrite.intros(7) rewrite_non_nullable)
 
 
 lemma third_segment_bmkeps:  "\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow> 
@@ -1477,22 +1380,22 @@
   using r2 apply blast
   
     apply (metis list.set_intros(1))
-  apply (smt (verit, ccfv_threshold) append_eq_append_conv2 list.set_intros(1) qq2 qq3 rewritenullable rrewrite.intros(8) self_append_conv2 spillbmkepslistr)
+  apply (smt (verit, ccfv_threshold) append_eq_append_conv2 list.set_intros(1) qq2 qq3 rewrite_nullable rrewrite.intros(8) self_append_conv2 spillbmkepslistr)
 
 
   thm qq1
   apply(subgoal_tac "bmkeps  (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs rsb) ")
    prefer 2
   
-  apply (metis append_Cons append_Nil bnullable.simps(1) bnullable_segment rewritenullable rrewrite.intros(11) third_segment_bmkeps)
-
+  apply (metis append_Cons append_Nil bnullable.simps(1) bnullable_segment rewrite_nullable rrewrite.intros(11) third_segment_bmkeps)
+  
   by (metis bnullable.simps(4) rewrite_non_nullable rrewrite.intros(10) third_segment_bmkeps)
 
 
 
 lemma rewrite_bmkeps: "\<lbrakk> r1 \<leadsto> r2; (bnullable r1)\<rbrakk> \<Longrightarrow> bmkeps r1 = bmkeps r2"
 
-  apply(frule rewritenullable)
+  apply(frule rewrite_nullable)
   apply simp
   apply(induction r1 r2 rule: rrewrite.induct)
              apply simp
@@ -1504,12 +1407,12 @@
         apply(case_tac "bnullable (AALTs bs rs1)")
   using qq1 apply force
         apply(case_tac "bnullable r")
-  using bnullablewhichbmkeps rewritenullable apply presburger
+  using bnullablewhichbmkeps rewrite_nullable apply presburger
         apply(subgoal_tac "bnullable (AALTs bs rs2)")
   apply(subgoal_tac "\<not> bnullable r'")
   apply (simp add: qq2 r1)
   
-  using rrewrite_nbnullable apply blast
+  using rewrite_non_nullable apply blast
 
         apply blast
        apply (simp add: flts_append qs3)
@@ -1526,21 +1429,24 @@
  
   by (smt (z3) Un_iff bnullable_correctness erase.simps(5) qq1 qq2 qq3 set_append)
 
-
+lemma rewrites_bmkeps: 
+  assumes "r1 \<leadsto>* r2" "bnullable r1" 
+  shows "bmkeps r1 = bmkeps r2"
+  using assms
+proof(induction r1 r2 rule: rrewrites.induct)
+  case (rs1 r)
+  then show "bmkeps r = bmkeps r" by simp
+next
+  case (rs2 r1 r2 r3)
+  then have IH: "bmkeps r1 = bmkeps r2" by simp
+  have a1: "bnullable r1" by fact
+  have a2: "r1 \<leadsto>* r2" by fact
+  have a3: "r2 \<leadsto> r3" by fact
+  have a4: "bnullable r2" using a1 a2 by (simp add: rewritesnullable) 
+  then have "bmkeps r2 = bmkeps r3" using rewrite_bmkeps a3 a4 by simp
+  then show "bmkeps r1 = bmkeps r3" using IH by simp
+qed
 
-lemma rewrites_bmkeps: "\<lbrakk> (r1 \<leadsto>* r2); (bnullable r1)\<rbrakk> \<Longrightarrow> bmkeps r1 = bmkeps r2"
-  apply(induction r1 r2 rule: rrewrites.induct)
-   apply simp
-  apply(subgoal_tac "bnullable r2")
-  prefer 2
-   apply(metis rewritesnullable)
-  apply(subgoal_tac "bmkeps r1 = bmkeps r2")
-   prefer 2
-   apply fastforce
-  using rewrite_bmkeps by presburger
-
-
-thm rrewrite.intros(12)
 lemma alts_rewrite_front: "r \<leadsto> r' \<Longrightarrow> AALTs bs (r # rs) \<leadsto> AALTs bs (r' # rs)"
   by (metis append_Cons append_Nil rrewrite.intros(6))
 
@@ -1648,7 +1554,7 @@
   prefer 2
   using rewrite_bmkeps apply auto[1]
   using contextrewrites1 star_seq apply auto[1]
-  using rewritenullable apply auto[1]
+  using rewrite_nullable apply auto[1]
          apply(case_tac "bnullable r1")
           apply simp
           apply(subgoal_tac "ASEQ [] (bder c r1) r3 \<leadsto> ASEQ [] (bder c r1) r4") 
@@ -1680,34 +1586,44 @@
 
 
 
-lemma rewrites_after_der: "  r1 \<leadsto>* r2  \<Longrightarrow>  (bder c r1) \<leadsto>* (bder c r2)"
-  apply(induction r1 r2 rule: rrewrites.induct)
-   apply(rule rs1)
-  by (meson real_trans rewrite_after_der)
-  
+lemma rewrites_after_der: 
+  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_after_der real_trans)
+done
 
+lemma central:  
+  shows "bders r s \<leadsto>* bders_simp r s"
+proof(induct s arbitrary: r rule: rev_induct)
+  case Nil
+  then show "bders r [] \<leadsto>* bders_simp r []" by simp
+next
+  case (snoc x xs)
+  have IH: "\<And>r. bders r xs \<leadsto>* bders_simp r xs" by fact
+  have "bders r (xs @ [x]) = bders (bders r xs) [x]" by (simp add: bders_append)
+  also have "... \<leadsto>* bders (bders_simp r xs) [x]" using IH
+    by (simp add: rewrites_after_der)
+  also have "... \<leadsto>* bders_simp (bders_simp r xs) [x]" using IH
+    by (simp add: bsimp_rewrite)
+  finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])" 
+    by (simp add: bders_simp_append)
+qed
 
 
-lemma central: " (bders r s) \<leadsto>*  (bders_simp r s)" 
-  apply(induct s arbitrary: r rule: rev_induct)
-
-   apply simp
-  apply(subst bders_append)
-  apply(subst bders_simp_append)
-  by (metis bders.simps(1) bders.simps(2) bders_simp.simps(1) bders_simp.simps(2) bsimp_rewrite real_trans rewrites_after_der)
+lemma quasi_main: 
+  assumes "bnullable (bders r s)"
+  shows "bmkeps (bders r s) = bmkeps (bders_simp r s)"
+  using assms central rewrites_bmkeps by blast
 
-
-
-thm arexp.induct
-
-lemma quasi_main: "bnullable (bders r s) \<Longrightarrow> bmkeps (bders r s) = bmkeps (bders_simp r s)"
-  using central rewrites_bmkeps by blast
-
-theorem main_main: "blexer r s = blexer_simp r s"
+theorem main_main: 
+  shows "blexer r s = blexer_simp r s"
   by (simp add: b4 blexer_def blexer_simp_def quasi_main)
 
 
-theorem blexersimp_correctness: "blexer_simp r s= lexer r s"
+theorem blexersimp_correctness: 
+  shows "lexer r s = blexer_simp r s"
   using blexer_correctness main_main by auto