--- a/thys2/SizeBound4.thy	Wed Feb 02 14:52:41 2022 +0000
+++ b/thys2/SizeBound4.thy	Wed Feb 02 22:29:55 2022 +0000
@@ -561,7 +561,7 @@
 | bs6: "AALTs bs [] \<leadsto> AZERO"
 | bs7: "AALTs bs [r] \<leadsto> fuse bs r"
 | bs8: "rs1 s\<leadsto> rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto> AALTs bs rs2"
-| ss1:  "[] s\<leadsto> []"
+(*| 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)"
 | ss4:  "(AZERO # rs) s\<leadsto> rs"
@@ -954,9 +954,9 @@
   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    
-next
+(*next
   case ss1
-  show "map (bder c) [] s\<leadsto>* map (bder c) []" by simp
+  show "map (bder c) [] s\<leadsto>* map (bder c) []" by simp*)
 next
   case (ss2 rs1 rs2 r)
   have IH1: "map (bder c) rs1 s\<leadsto>* map (bder c) rs2" by fact
@@ -1034,6 +1034,215 @@
 
 (* some tests *)
 
+lemma asize_fuse:
+  shows "asize (fuse bs r) = asize r"
+  apply(induct r arbitrary: bs)
+  apply(auto)
+  done
+
+lemma asize_rewrite2:
+  shows "r1 \<leadsto> r2 \<Longrightarrow> asize r1 \<ge> asize r2"
+  and   "rs1 s\<leadsto> rs2 \<Longrightarrow> (sum_list (map asize rs1)) \<ge> (sum_list (map asize rs2))"
+   apply(induct rule: rrewrite_srewrite.inducts)
+   apply(auto simp add: asize_fuse comp_def)
+  done
+
+lemma asize_rrewrites:
+  assumes "r1 \<leadsto>* r2"
+  shows "asize r1 \<ge> asize r2"
+  using assms
+  apply(induct rule: rrewrites.induct)
+   apply(auto)
+  using asize_rewrite2(1) le_trans by blast
+  
+
+
+fun asize2 :: "arexp \<Rightarrow> nat" where
+  "asize2 AZERO = 1"
+| "asize2 (AONE cs) = 1" 
+| "asize2 (ACHAR cs c) = 1"
+| "asize2 (AALTs cs rs) = Suc (Suc (sum_list (map asize2 rs)))"
+| "asize2 (ASEQ cs r1 r2) = Suc (asize2 r1 + asize2 r2)"
+| "asize2 (ASTAR cs r) = Suc (asize2 r)"
+
+
+lemma asize2_fuse:
+  shows "asize2 (fuse bs r) = asize2 r"
+  apply(induct r arbitrary: bs)
+  apply(auto)
+  done
+
+lemma asize2_not_zero:
+  shows "0 < asize2 r"
+  apply(induct r)
+  apply(auto)
+  done
+
+lemma asize_rewrite:
+  shows "r1 \<leadsto> r2 \<Longrightarrow> asize2 r1 > asize2 r2"
+  and   "rs1 s\<leadsto> rs2 \<Longrightarrow> (sum_list (map asize2 rs1)) > (sum_list (map asize2 rs2))"
+   apply(induct rule: rrewrite_srewrite.inducts)
+   apply(auto simp add: asize2_fuse comp_def)
+  apply(simp add: asize2_not_zero) 
+  done
+
+lemma asize2_bsimp_ASEQ:
+  shows "asize2 (bsimp_ASEQ bs r1 r2) \<le> Suc (asize2 r1 + asize2 r2)"
+  apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
+  apply(auto)
+  done
+
+lemma asize2_bsimp_AALTs:
+  shows "asize2 (bsimp_AALTs bs rs) \<le> Suc (Suc (sum_list (map asize2 rs)))"
+  apply(induct bs rs rule: bsimp_AALTs.induct)
+  apply(auto simp add: asize2_fuse)
+  done
+
+lemma distinctBy_asize2:
+  shows "sum_list (map asize2 (distinctBy rs f acc)) \<le> sum_list (map asize2 rs)"
+  apply(induct rs f acc rule: distinctBy.induct)
+  apply(auto)
+  done
+
+lemma flts_asize2:
+  shows "sum_list (map asize2 (flts rs)) \<le> sum_list (map asize2 rs)"
+  apply(induct rs rule: flts.induct)
+  apply(auto simp add: comp_def asize2_fuse)
+  done
+
+lemma sumlist_asize2:
+  assumes "\<And>x. x \<in> set rs \<Longrightarrow> asize2 (f x) \<le> asize2 x"
+  shows "sum_list (map asize2 (map f rs)) \<le> sum_list (map asize2 rs)"
+  using assms
+  apply(induct rs)
+   apply(auto simp add: comp_def)
+  by (simp add: add_le_mono)
+
+lemma test0:
+  assumes "r1 \<leadsto>* r2"
+  shows "r1 = r2 \<or> (\<exists>r3. r1 \<leadsto> r3 \<and> r3 \<leadsto>* r2)"
+  using assms
+  apply(induct r1 r2 rule: rrewrites.induct)
+   apply(auto)
+  done
+
+lemma test2:
+  assumes "r1 \<leadsto>* r2"
+  shows "asize2 r1 \<ge> asize2 r2"
+using assms
+  apply(induct r1 r2 rule: rrewrites.induct)
+  apply(auto)
+  using asize_rewrite(1) by fastforce
+  
+
+lemma test3:
+  shows "r = bsimp r \<or> (asize2 (bsimp r) < asize2 r)"
+proof -
+  have "r \<leadsto>* bsimp r"
+    by (simp add: rewrites_to_bsimp)
+  then have "r = bsimp r \<or> (\<exists>r3. r \<leadsto> r3 \<and> r3 \<leadsto>* bsimp r)"
+    using test0 by blast
+  then show ?thesis
+    by (meson asize_rewrite(1) dual_order.strict_trans2 test2)
+qed
+
+lemma test3Q:
+  shows "r = bsimp r \<or> (asize (bsimp r) \<le> asize r)"
+proof -
+  have "r \<leadsto>* bsimp r"
+    by (simp add: rewrites_to_bsimp)
+  then have "r = bsimp r \<or> (\<exists>r3. r \<leadsto> r3 \<and> r3 \<leadsto>* bsimp r)"
+    using test0 by blast
+  then show ?thesis
+    using asize_rewrite2(1) asize_rrewrites le_trans by blast
+qed
+
+lemma test4:
+  shows "asize2 (bsimp (bsimp r)) \<le> asize2 (bsimp r)"
+  apply(induct r rule: bsimp.induct)
+       apply(auto)
+  using rewrites_to_bsimp test2 apply fastforce
+  using rewrites_to_bsimp test2 by presburger
+
+lemma test4Q:
+  shows "asize (bsimp (bsimp r)) \<le> asize (bsimp r)"
+  apply(induct r rule: bsimp.induct)
+       apply(auto)
+  apply (metis order_refl test3Q)
+  by (metis le_refl test3Q)
+
+
+
+lemma testb0:
+  shows "fuse bs1 (bsimp_ASEQ bs r1 r2) =  bsimp_ASEQ (bs1 @ bs) r1 r2"
+  apply(induct bs r1 r2 arbitrary: bs1 rule: bsimp_ASEQ.induct)
+  apply(auto)
+  done
+
+lemma testb1:
+  shows "fuse bs1 (bsimp_AALTs bs rs) =  bsimp_AALTs (bs1 @ bs) rs"
+  apply(induct bs rs arbitrary: bs1 rule: bsimp_AALTs.induct)
+  apply(auto simp add: fuse_append)
+  done
+
+lemma testb2:
+  shows "bsimp (bsimp_ASEQ bs r1 r2) =  bsimp_ASEQ bs (bsimp r1) (bsimp r2)"
+  apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
+  apply(auto simp add: testb0 testb1)
+  done  
+
+lemma testb3:
+  shows "\<nexists>r'. (bsimp r \<leadsto> r') \<and> asize2 (bsimp r) > asize2 r'"
+apply(induct r rule: bsimp.induct)
+       apply(auto)
+       defer
+       defer
+  using rrewrite.cases apply blast
+  using rrewrite.cases apply blast
+  using rrewrite.cases apply blast
+  using rrewrite.cases apply blast
+  oops
+
+lemma testb4:
+  assumes "sum_list (map asize rs1) \<le> sum_list (map asize rs2)"
+  shows "asize (bsimp_AALTs bs1 rs1) \<le> Suc (asize (bsimp_AALTs bs1 rs2))"
+  using assms 
+apply(induct bs1 rs2 arbitrary: rs1 rule: bsimp_AALTs.induct)
+    apply(auto)
+    apply(case_tac rs1)
+     apply(auto)
+  using asize2.elims apply auto[1]
+  apply (metis One_nat_def Zero_not_Suc asize.elims)
+      apply(case_tac rs1)
+    apply(auto)
+   apply(case_tac list)
+    apply(auto)
+  using asize_fuse apply force
+  apply (simp add: asize_fuse)
+  by (smt (verit, ccfv_threshold) One_nat_def add.right_neutral asize.simps(1) asize.simps(4) asize_fuse bsimp_AALTs.elims le_Suc_eq list.map(1) list.map(2) not_less_eq_eq sum_list_simps(1) sum_list_simps(2))
+
+lemma flts_asize:
+  shows "sum_list (map asize (flts rs)) \<le> sum_list (map asize rs)"
+  apply(induct rs rule: flts.induct)
+  apply(auto simp add: comp_def asize_fuse)
+  done
+
+
+lemma test5:
+  shows "asize2 r \<ge> asize2 (bsimp r)"
+  apply(induct r rule: bsimp.induct)
+       apply(auto)
+  apply (meson Suc_le_mono add_le_mono asize2_bsimp_ASEQ order_trans)
+  apply(rule order_trans)
+   apply(rule asize2_bsimp_AALTs)
+  apply(simp)
+  apply(rule order_trans)
+   apply(rule distinctBy_asize2)
+  apply(rule order_trans)
+   apply(rule flts_asize2)
+  using sumlist_asize2 by force
+  
+
 fun awidth :: "arexp \<Rightarrow> nat" where
   "awidth AZERO = 1"
 | "awidth (AONE cs) = 1" 
@@ -1071,11 +1280,7 @@
   apply(auto)
   done
 
-lemma asize_fuse:
-  shows "asize (fuse bs r) = asize r"
-  apply(induct r arbitrary: bs)
-  apply(auto)
-  done
+
 
 lemma awidth_fuse:
   shows "awidth (fuse bs r) = awidth r"
@@ -1096,19 +1301,6 @@
   done
 
 lemma
-  "asize (bsimp (bder c (intern r))) \<le> Suc ((Suc (card (pder c r))) * (size r) * (size r))"
-  oops
-
-lemma
-  "card (pder c r) \<le> awidth (bsimp (bder c (intern r)))"
- apply(induct c r rule: pder.induct)
-  apply(simp)
-      apply(simp)
-     apply(simp)
-    apply(simp)
-  oops
-
-lemma
   "card (pder c r) \<le> awidth (bder c (intern r))"
   apply(induct c r rule: pder.induct)
   apply(simp)