
diff -r 320f923c77b9 -r 98362002c818 thys2/SizeBound.thy
--- a/thys2/SizeBound.thy	Thu Nov 04 01:07:34 2021 +0000
+++ b/thys2/SizeBound.thy	Thu Nov 04 09:45:41 2021 +0000
@@ -118,30 +118,12 @@
 | "erase (ASTAR _ r) = STAR (erase r)"
 
 
-
-
 fun nonalt :: "arexp \<Rightarrow> bool"
   where
   "nonalt (AALTs bs2 rs) = False"
 | "nonalt r = True"
 
 
-fun good :: "arexp \<Rightarrow> bool" where
-  "good AZERO = False"
-| "good (AONE cs) = True" 
-| "good (ACHAR cs c) = True"
-| "good (AALTs cs []) = False"
-| "good (AALTs cs [r]) = False"
-| "good (AALTs cs (r1#r2#rs)) = (\<forall>r' \<in> set (r1#r2#rs). good r' \<and> nonalt r')"
-| "good (ASEQ _ AZERO _) = False"
-| "good (ASEQ _ (AONE _) _) = False"
-| "good (ASEQ _ _ AZERO) = False"
-| "good (ASEQ cs r1 r2) = (good r1 \<and> good r2)"
-| "good (ASTAR cs r) = True"
-
-
-
-
 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where
   "fuse bs AZERO = AZERO"
 | "fuse bs (AONE cs) = AONE (bs @ cs)" 
@@ -238,8 +220,6 @@
   apply(simp_all)
   done
 
-thm Posix.induct
-
 lemma erase_intern [simp]:
   shows "erase (intern r) = r"
   apply(induct r)
@@ -551,8 +531,9 @@
      (if (f x) \<in> acc then distinctBy xs f acc 
       else x # (distinctBy xs f ({f x} \<union> acc)))"
 
-
-
+lemma dB_single_step: 
+  shows "distinctBy (a#rs) f {} = a # distinctBy rs f {f a}"
+  by simp 
 
 fun flts :: "arexp list \<Rightarrow> arexp list"
   where 
@@ -563,16 +544,6 @@
 
 
 
-
-fun li :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp"
-  where
-  "li _ [] = AZERO"
-| "li bs [a] = fuse bs a"
-| "li bs as = AALTs bs as"
-
-
-
-
 fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"
   where
   "bsimp_ASEQ _ AZERO _ = AZERO"
@@ -591,12 +562,10 @@
 fun bsimp :: "arexp \<Rightarrow> arexp" 
   where
   "bsimp (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)"
-| "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (distinctBy  (flts (map bsimp rs)) erase {} ) "
+| "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {}) "
 | "bsimp r = r"
 
 
-
-
 fun 
   bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
 where
@@ -605,23 +574,16 @@
 
 definition blexer_simp where
  "blexer_simp r s \<equiv> if bnullable (bders_simp (intern r) s) then 
-                decode (bmkeps (bders_simp (intern r) s)) r else None"
+                    decode (bmkeps (bders_simp (intern r) s)) r else None"
 
 export_code bders_simp in Scala module_name Example
 
 lemma bders_simp_append:
   shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2"
   apply(induct s1 arbitrary: r s2)
-   apply(simp)
-  apply(simp)
+  apply(simp_all)
   done
 
-
-
-
-
-
-
 lemma L_bsimp_ASEQ:
   "L (SEQ (erase r1) (erase r2)) = L (erase (bsimp_ASEQ bs r1 r2))"
   apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
@@ -674,25 +636,25 @@
   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(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(auto)
-   apply (simp add: L_erase_AALTs)
+  apply (simp add: L_erase_AALTs)
   using L_erase_AALTs by blast
 
+
+
 lemma bsimp_ASEQ0:
   shows "bsimp_ASEQ bs r1 AZERO = AZERO"
   apply(induct r1)
   apply(auto)
   done
 
-
-
 lemma bsimp_ASEQ1:
   assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<forall>bs. r1 \<noteq> AONE bs"
   shows "bsimp_ASEQ bs r1 r2 = ASEQ bs r1 r2"
@@ -711,7 +673,7 @@
 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)
   apply(simp add: ders_append)
   apply(simp add: bders_simp_append)
@@ -748,23 +710,6 @@
   apply(simp)
   by (metis append_assoc in_set_conv_decomp r1 r2)
   
-lemma qq3:
-  shows "bnullable (AALTs bs rs) = (\<exists>r \<in> set rs. bnullable r)"
-  apply(induct rs arbitrary: bs)
-  apply(simp)
-  apply(simp)
-  done
-
-
-
-
-
-fun nonnested :: "arexp \<Rightarrow> bool"
-  where
-  "nonnested (AALTs bs2 []) = True"
-| "nonnested (AALTs bs2 ((AALTs bs1 rs1) # rs2)) = False"
-| "nonnested (AALTs bs2 (r # rs2)) = nonnested (AALTs bs2 rs2)"
-| "nonnested r = True"
 
 lemma flts_append:
   shows "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
@@ -1006,41 +951,44 @@
   done
 
 
-corollary srewrites_alt1: "rs1 s\<leadsto>* rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto>* AALTs bs rs2"
+corollary srewrites_alt1: 
+  assumes "rs1 s\<leadsto>* rs2"
+  shows "AALTs bs rs1 \<leadsto>* AALTs bs rs2"
+using assms
   by (metis append.left_neutral srewrites_alt)
 
 
-lemma star_seq:  "r1 \<leadsto>* r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto>* ASEQ bs r2 r3"
-  apply(induct r1 r2 arbitrary: r3 rule: rrewrites.induct)
-   apply(rule rs1)
-  apply(erule rrewrites.cases)
-   apply(simp)
-   apply(rule r_in_rstar)
-   apply(rule rrewrite.intros(4))
-   apply simp
-  apply(rule rs2)
-   apply(assumption)
-  apply(rule rrewrite.intros(4))
-  by assumption
+lemma star_seq:  
+  assumes "r1 \<leadsto>* r2"
+  shows "ASEQ bs r1 r3 \<leadsto>* ASEQ bs r2 r3"
+using assms
+apply(induct r1 r2 arbitrary: r3 rule: rrewrites.induct)
+apply(auto intro: rrewrite.intros)
+done
 
-lemma star_seq2:  "r3 \<leadsto>* r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto>* ASEQ bs r1 r4"
-  apply(induct r3 r4 arbitrary: r1 rule: rrewrites.induct)
-   apply auto
-  using rrewrite.intros(5) by blast
-
+lemma star_seq2:  
+  assumes "r3 \<leadsto>* r4"
+  shows "ASEQ bs r1 r3 \<leadsto>* ASEQ bs r1 r4"
+using assms
+apply(induct r3 r4 arbitrary: r1 rule: rrewrites.induct)
+apply(auto intro: rrewrite.intros)
+done
 
-lemma continuous_rewrite: "\<lbrakk>r1 \<leadsto>* AZERO\<rbrakk> \<Longrightarrow> ASEQ bs1 r1 r2 \<leadsto>* AZERO"
+lemma continuous_rewrite: 
+  assumes "r1 \<leadsto>* AZERO"
+  shows "ASEQ bs1 r1 r2 \<leadsto>* AZERO"
+using assms
   apply(induction ra\<equiv>"r1" rb\<equiv>"AZERO" arbitrary: bs1 r1 r2 rule: rrewrites.induct)
-   apply (simp add: r_in_rstar rrewrite.intros(1))
-
-  by (meson rrewrite.intros(1) rrewrites.intros(2) star_seq)
+  apply(auto intro: rrewrite.intros r_in_rstar star_seq)
+  by (meson rrewrite.intros(1) rs2 star_seq)
   
 
 
-lemma bsimp_aalts_simpcases: "AONE bs \<leadsto>* (bsimp (AONE bs))"  "AZERO \<leadsto>* bsimp AZERO" "ACHAR bs c \<leadsto>* (bsimp (ACHAR bs c))"
-  apply (simp add: rrewrites.intros(1))
-  apply (simp add: rrewrites.intros(1))
-  by (simp add: rrewrites.intros(1))
+lemma bsimp_aalts_simpcases: 
+  shows "AONE bs \<leadsto>* bsimp (AONE bs)"  
+  and   "AZERO \<leadsto>* bsimp AZERO" 
+  and   "ACHAR bs c \<leadsto>* bsimp (ACHAR bs c)"
+  by (simp_all)
 
 lemma trivialbsimpsrewrites: "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs s\<leadsto>* (map f rs)"
 
@@ -1072,8 +1020,6 @@
 
 
 
-
-
 lemma flts_prepend: "\<lbrakk>nonalt a; nonazero a\<rbrakk> \<Longrightarrow> flts (a#rs) = a # (flts rs)"
   by (metis append_Cons append_Nil flts_single1 flts_append)
 
@@ -1098,14 +1044,14 @@
          apply blast
    
   using bbbbs1 apply blast
-       apply(simp add: nonalt.simps)+
+       apply(simp)+
    
    apply (meson nonazero.elims(3))
    
   by (meson fs4 nonalt.elims(3) nonazero.elims(3))
 
 
-lemma rrewrite0away: "AALTs bs ( AZERO # rsb) \<leadsto> AALTs bs rsb"
+lemma rrewrite0away: "AALTs bs (AZERO # rsb) \<leadsto> AALTs bs rsb"
   by (metis append_Nil rrewrite.intros(7))
 
 
@@ -1139,7 +1085,7 @@
 
   apply(case_tac "\<exists>bs2 rs2. a = AALTs bs2 rs2")
    apply(erule exE)+
-   apply(simp add: flts.simps)
+   apply(simp)
    prefer 2
 
   apply(subst flts_prepend)
@@ -1164,16 +1110,6 @@
   apply auto
   done
 
-fun distinctByAcc :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> 'b set"
-  where
-  "distinctByAcc [] f acc = acc"
-| "distinctByAcc (x#xs) f acc = 
-     (if (f x) \<in> acc then distinctByAcc xs f acc 
-      else  (distinctByAcc xs f ({f x} \<union> acc)))"
-
-lemma dB_single_step: "distinctBy (a#rs) f {} = a # distinctBy rs f {f a}"
-  apply simp
-  done
 
 lemma somewhereInside: "r \<in> set rs \<Longrightarrow> \<exists>rs1 rs2. rs = rs1@[r]@rs2"
   using split_list by fastforce
@@ -1236,7 +1172,8 @@
   
 
 
-lemma bsimp_rewrite: " (rrewrites r ( bsimp r))"
+lemma bsimp_rewrite: 
+  shows "r \<leadsto>* bsimp r"
   apply(induction r rule: bsimp.induct)
        apply simp
        apply(case_tac "bsimp r1 = AZERO")
@@ -1315,12 +1252,11 @@
 
 lemma nomember_bnullable: "\<lbrakk> \<not> (\<exists>r0\<in>set rs1. bnullable r0); \<not> bnullable r; \<not> (\<exists>r0\<in>set rs2. bnullable r0)\<rbrakk>
  \<Longrightarrow> \<not>bnullable (AALTs bs (rs1 @ [r] @ rs2))"
-  using nonbnullable_lists_concat qq3 by presburger
+  using bnullable.simps(4) nonbnullable_lists_concat by presburger
 
 lemma bnullable_segment: " bnullable (AALTs bs (rs1@[r]@rs2)) \<Longrightarrow> bnullable (AALTs bs rs1) \<or> bnullable (AALTs bs rs2) \<or> bnullable r"
   apply(case_tac "\<exists>r0\<in>set rs1.  bnullable r0")
-
-  using qq3 apply blast
+  using r2 apply blast
   apply(case_tac "bnullable r")
 
   apply blast
@@ -1359,7 +1295,7 @@
   apply(subgoal_tac "bnullable (AALTs bs rs3)")
    apply(subgoal_tac "\<forall>r \<in> set (rs1@rs2). \<not>bnullable r")
   apply(subgoal_tac "bmkeps (AALTs bs (rs1@rs2@rs3)) = bmkeps (AALTs bs ((rs1@rs2)@rs3) )")
-  apply (metis qq2 qq3)
+  apply (metis bnullable.simps(4) qq2)
 
   apply (metis append.assoc)
 
@@ -1380,7 +1316,7 @@
   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 rewrite_nullable rrewrite.intros(8) self_append_conv2 spillbmkepslistr)
+  apply (smt (verit, ccfv_threshold) append_eq_append_conv2 list.set_intros(1) qq2 bnullable.simps(4) rewrite_nullable rrewrite.intros(8) self_append_conv2 spillbmkepslistr)
 
 
   thm qq1
@@ -1427,7 +1363,7 @@
 
   apply (simp add: b2)
  
-  by (smt (z3) Un_iff bnullable_correctness erase.simps(5) qq1 qq2 qq3 set_append)
+  by (smt (z3) Un_iff bnullable_correctness erase.simps(5) qq1 qq2 bnullable.simps(4) set_append)
 
 lemma rewrites_bmkeps: 
   assumes "r1 \<leadsto>* r2" "bnullable r1" 
@@ -1496,16 +1432,19 @@
 
   
 
-lemma rewrites_fuse:  "r2 \<leadsto>* r2' \<Longrightarrow>  (fuse bs1 r2) \<leadsto>*  (fuse bs1 r2')"
-  apply(induction r2 r2' arbitrary: bs1 rule: rrewrites.induct)
-   apply simp
-  by (meson real_trans rewrite_fuse)
+lemma rewrites_fuse:  
+  assumes "r2 \<leadsto>* r2'"
+  shows "fuse bs1 r2 \<leadsto>* fuse bs1 r2'"
+using assms
+apply(induction r2 r2' arbitrary: bs1 rule: rrewrites.induct)
+apply(auto intro: rewrite_fuse real_trans)
+done
 
-lemma  bder_fuse_list: " map (bder c \<circ> fuse bs1) rs1 = map (fuse bs1 \<circ> bder c) rs1"
-  apply(induction rs1)
-  apply simp
-  by (simp add: bder_fuse)
-
+lemma  bder_fuse_list: 
+  shows "map (bder c \<circ> fuse bs1) rs1 = map (fuse bs1 \<circ> bder c) rs1"
+apply(induction rs1)
+apply(simp_all add: bder_fuse)
+done
 
 
 lemma rewrite_der_altmiddle: "bder c (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) \<leadsto>* bder c (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"




