--- a/thys2/SizeBound4.thy	Sat Jan 29 16:43:51 2022 +0000
+++ b/thys2/SizeBound4.thy	Sat Jan 29 23:53:21 2022 +0000
@@ -1032,12 +1032,78 @@
   using blexer_correctness main_blexer_simp by simp
 
 
+(* below is the idempotency of bsimp *)
 
-lemma asize_idem:
-  shows "asize (bsimp (bsimp r)) = asize (bsimp r)"
+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)
-  prefer 2
+  using bsimp_ASEQ_idem apply presburger
   oops
 
 export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers