--- a/thys2/SizeBound4.thy	Sun Jan 30 23:37:29 2022 +0000
+++ b/thys2/SizeBound4.thy	Wed Feb 02 14:52:41 2022 +0000
@@ -1,6 +1,6 @@
 
 theory SizeBound4
-  imports "Lexer" 
+  imports "Lexer" "PDerivs"
 begin
 
 section \<open>Bit-Encodings\<close>
@@ -26,26 +26,26 @@
 function
   decode' :: "bit list \<Rightarrow> rexp \<Rightarrow> (val * bit list)"
 where
-  "decode' ds ZERO = (Void, [])"
-| "decode' ds ONE = (Void, ds)"
-| "decode' ds (CH d) = (Char d, ds)"
+  "decode' bs ZERO = (undefined, bs)"
+| "decode' bs ONE = (Void, bs)"
+| "decode' bs (CH d) = (Char d, bs)"
 | "decode' [] (ALT r1 r2) = (Void, [])"
-| "decode' (Z # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))"
-| "decode' (S # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))"
-| "decode' ds (SEQ r1 r2) = (let (v1, ds') = decode' ds r1 in
-                             let (v2, ds'') = decode' ds' r2 in (Seq v1 v2, ds''))"
+| "decode' (Z # bs) (ALT r1 r2) = (let (v, bs') = decode' bs r1 in (Left v, bs'))"
+| "decode' (S # bs) (ALT r1 r2) = (let (v, bs') = decode' bs r2 in (Right v, bs'))"
+| "decode' bs (SEQ r1 r2) = (let (v1, bs') = decode' bs r1 in
+                             let (v2, bs'') = decode' bs' r2 in (Seq v1 v2, bs''))"
 | "decode' [] (STAR r) = (Void, [])"
-| "decode' (S # ds) (STAR r) = (Stars [], ds)"
-| "decode' (Z # ds) (STAR r) = (let (v, ds') = decode' ds r in
-                                    let (vs, ds'') = decode' ds' (STAR r) 
-                                    in (Stars_add v vs, ds''))"
+| "decode' (S # bs) (STAR r) = (Stars [], bs)"
+| "decode' (Z # bs) (STAR r) = (let (v, bs') = decode' bs r in
+                                    let (vs, bs'') = decode' bs' (STAR r) 
+                                    in (Stars_add v vs, bs''))"
 by pat_completeness auto
 
 lemma decode'_smaller:
-  assumes "decode'_dom (ds, r)"
-  shows "length (snd (decode' ds r)) \<le> length ds"
+  assumes "decode'_dom (bs, r)"
+  shows "length (snd (decode' bs r)) \<le> length bs"
 using assms
-apply(induct ds r)
+apply(induct bs r)
 apply(auto simp add: decode'.psimps split: prod.split)
 using dual_order.trans apply blast
 by (meson dual_order.trans le_SucI)
@@ -1032,6 +1032,152 @@
   using blexer_correctness main_blexer_simp by simp
 
 
+(* some tests *)
+
+fun awidth :: "arexp \<Rightarrow> nat" where
+  "awidth AZERO = 1"
+| "awidth (AONE cs) = 1" 
+| "awidth (ACHAR cs c) = 1"
+| "awidth (AALTs cs rs) = (sum_list (map awidth rs))"
+| "awidth (ASEQ cs r1 r2) = (awidth r1 + awidth r2)"
+| "awidth (ASTAR cs r) = (awidth r)"
+
+
+
+lemma 
+  shows "s \<notin> L r \<Longrightarrow> blexer_simp r s = None"
+  by (simp add: blexersimp_correctness lexer_correct_None)
+
+lemma g1:
+  "bders_simp AZERO s = AZERO"
+ apply(induct s)
+ apply(simp)
+ apply(simp)
+  done
+
+lemma g2:
+  "s \<noteq> Nil \<Longrightarrow> bders_simp (AONE bs) s = AZERO"
+ apply(induct s)
+ apply(simp)
+  apply(simp)
+  apply(case_tac s)
+  apply(simp)
+       apply(simp)
+  done
+
+lemma finite_pder:
+  shows "finite (pder c r)"
+  apply(induct c r rule: pder.induct)
+  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"
+  apply(induct r arbitrary: bs)
+  apply(auto)
+  done
+
+lemma pders_SEQs:
+  assumes "finite A"
+  shows "card (SEQs A (STAR r)) \<le> card A"
+  using assms
+  by (simp add: SEQs_eq_image card_image_le)
+
+lemma binullable_intern:
+  shows "bnullable (intern r) = nullable r"
+  apply(induct r)
+  apply(auto simp add: bnullable_fuse)
+  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)
+      apply(simp)
+     apply(simp)
+    apply(simp)
+  apply(rule order_trans)
+     apply(rule card_Un_le)
+  apply (simp add: awidth_fuse bder_fuse)
+   defer
+   apply(simp)
+  apply(rule order_trans)
+    apply(rule pders_SEQs)
+  using finite_pder apply presburger
+  apply (simp add: awidth_fuse)
+  apply(auto)
+     apply(rule order_trans)
+      apply(rule card_Un_le)
+     apply(simp add: awidth_fuse)
+     defer
+  using binullable_intern apply blast
+  using binullable_intern apply blast
+  apply (smt (verit, best) SEQs_eq_image add.commute add_Suc_right card_image_le dual_order.trans finite_pder trans_le_add2)
+  apply(subgoal_tac "card (SEQs (pder c r1) r2) \<le> card (pder c r1)")
+  apply(linarith)
+    by (simp add: UNION_singleton_eq_range card_image_le finite_pder)
+  
+lemma
+  "card (pder c r) \<le> asize (bder c (intern r))"
+  apply(induct c r rule: pder.induct)
+       apply(simp)
+  apply(simp)
+     apply(simp)
+    apply(simp)
+  apply (metis add_mono_thms_linordered_semiring(1) asize_fuse bder_fuse card_Un_le le_Suc_eq order_trans)
+  defer 
+   apply(simp)
+   apply(rule order_trans)
+    apply(rule pders_SEQs)
+  using finite_pder apply presburger
+  apply (simp add: asize_fuse)
+  apply(simp)
+  apply(auto)
+  apply(rule order_trans)
+      apply(rule card_Un_le)
+  apply (smt (z3) SEQs_eq_image add.commute add_Suc_right add_mono_thms_linordered_semiring(1) asize_fuse card_image_le dual_order.trans finite_pder le_add1)
+    apply(rule order_trans)
+     apply(rule card_Un_le)
+  using binullable_intern apply blast
+  using binullable_intern apply blast
+  by (smt (verit, best) SEQs_eq_image add.commute add_Suc_right card_image_le dual_order.trans finite_pder trans_le_add2)
+  
+lemma
+  "card (pder c r) \<le> asize (bsimp (bder c (intern r)))"
+  apply(induct c r rule: pder.induct)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+    apply(simp)
+  apply(rule order_trans)
+     apply(rule card_Un_le)
+    prefer 3
+    apply(simp)
+  apply(rule order_trans)
+     apply(rule pders_SEQs)
+  using finite_pder apply blast
+  oops
+  
+
 (* below is the idempotency of bsimp *)
 
 lemma bsimp_ASEQ_fuse: