--- a/thys/PDerivs.thy	Sat Jun 29 20:50:24 2019 +0100
+++ b/thys/PDerivs.thy	Tue Jul 23 21:21:49 2019 +0100
@@ -1,8 +1,10 @@
    
 theory PDerivs
-  imports Spec
+  imports Spec 
 begin
 
+
+
 abbreviation
   "SEQs rs r \<equiv> (\<Union>r' \<in> rs. {SEQ r' r})"
 
@@ -344,6 +346,21 @@
 
 (* other result by antimirov *)
 
+lemma card_pders_awidth: 
+  shows "card (pders s r) \<le> awidth r + 1"
+proof -
+  have "pders s r \<subseteq> pders_Set UNIV r"
+    using pders_Set_def by auto
+  then have "card (pders s r) \<le> card (pders_Set UNIV r)"
+    by (simp add: card_mono finite_pders_set)
+  then show "card (pders s r) \<le> awidth r + 1"
+    using card_pders_set_le_awidth order_trans by blast
+qed
+    
+  
+  
+
+
 fun subs :: "rexp \<Rightarrow> rexp set" where
 "subs ZERO = {ZERO}" |
 "subs ONE = {ONE}" |
@@ -352,6 +369,14 @@
 "subs (SEQ r1 r2) = (subs r1 \<union> subs r2 \<union> {SEQ r1 r2} \<union>  SEQs (subs r1) r2)" |
 "subs (STAR r1) = (subs r1 \<union> {STAR r1} \<union> SEQs (subs r1) (STAR r1))"
 
+lemma subs_finite:
+  shows "finite (subs r)"
+  apply(induct r) 
+  apply(simp_all)
+  done
+
+
+
 lemma pders_subs:
   shows "pders s r \<subseteq> subs r"
   apply(induct r arbitrary: s)
@@ -400,7 +425,16 @@
   apply(simp_all)
   done
 
-lemma
+lemma subs_card:
+  shows "card (subs r) \<le> Suc (size2 r + size2 r)"
+  apply(induct r)
+       apply(auto)
+    apply(subst card_insert)
+     apply(simp add: subs_finite)
+    apply(simp add: subs_finite)
+  oops
+
+lemma subs_size2:
   shows "\<forall>r1 \<in> subs r. size2 r1 \<le> Suc (size2 r * size2 r)"
   apply(induct r)
        apply(simp)
@@ -427,7 +461,74 @@
   using size_rexp
   apply(simp)
   done
+
+lemma awidth_size:
+  shows "awidth r \<le> size2 r"
+  apply(induct r)
+       apply(simp_all)
+  done
+
+lemma Sum1:
+  fixes A B :: "nat set"
+  assumes "A \<subseteq> B" "finite A" "finite B"
+  shows "\<Sum>A \<le> \<Sum>B"
+  using  assms
+  by (simp add: sum_mono2)
+
+lemma Sum2:
+  fixes A :: "rexp set"  
+  and   f g :: "rexp \<Rightarrow> nat" 
+  assumes "finite A" "\<forall>x \<in> A. f x \<le> g x"
+  shows "sum f A \<le> sum g A"
+  using  assms
+  apply(induct A)
+   apply(auto)
+  done
+
+
+
+
+
+lemma pders_max_size:
+  shows "(sum size2 (pders s r)) \<le> (Suc (size2 r)) ^ 3"
+proof -
+  have "(sum size2 (pders s r)) \<le> sum (\<lambda>_. Suc (size2 r  * size2 r)) (pders s r)" 
+    apply(rule_tac Sum2)
+     apply (meson pders_subs rev_finite_subset subs_finite)
+    using pders_subs subs_size2 by blast
+  also have "... \<le> (Suc (size2 r  * size2 r)) * (sum (\<lambda>_. 1) (pders s r))"
+    by simp
+  also have "... \<le> (Suc (size2 r  * size2 r)) * card (pders s r)"
+    by simp
+  also have "... \<le> (Suc (size2 r  * size2 r)) * (Suc (awidth r))"
+    using Suc_eq_plus1 card_pders_awidth mult_le_mono2 by presburger
+  also have "... \<le> (Suc (size2 r  * size2 r)) * (Suc (size2 r))"
+    using Suc_le_mono awidth_size mult_le_mono2 by presburger
+  also have "... \<le> (Suc (size2 r)) ^ 3"
+    by (smt One_nat_def Suc_1 Suc_mult_le_cancel1 Suc_n_not_le_n antisym_conv le_Suc_eq mult.commute nat_le_linear numeral_3_eq_3 power2_eq_square power2_le_imp_le power_Suc size_rexp)    
+  finally show ?thesis  .
+qed
   
+lemma pders_Set_max_size:
+  shows "(sum size2 (pders_Set A r)) \<le> (Suc (size2 r)) ^ 3"
+proof -
+  have "(sum size2 (pders_Set A r)) \<le> sum (\<lambda>_. Suc (size2 r  * size2 r)) (pders_Set A r)" 
+    apply(rule_tac Sum2)
+     apply (simp add: finite_pders_set)
+    by (meson pders_Set_subsetI pders_subs subs_size2 subsetD)
+  also have "... \<le> (Suc (size2 r  * size2 r)) * (sum (\<lambda>_. 1) (pders_Set A r))"
+    by simp
+  also have "... \<le> (Suc (size2 r  * size2 r)) * card (pders_Set A r)"
+    by simp
+  also have "... \<le> (Suc (size2 r  * size2 r)) * (Suc (awidth r))"
+    using Suc_eq_plus1 card_pders_set_le_awidth mult_le_mono2 by presburger
+  also have "... \<le> (Suc (size2 r  * size2 r)) * (Suc (size2 r))"
+    using Suc_le_mono awidth_size mult_le_mono2 by presburger
+  also have "... \<le> (Suc (size2 r)) ^ 3"
+    by (smt One_nat_def Suc_1 Suc_mult_le_cancel1 Suc_n_not_le_n antisym_conv le_Suc_eq mult.commute nat_le_linear numeral_3_eq_3 power2_eq_square power2_le_imp_le power_Suc size_rexp)    
+  finally show ?thesis  .
+qed    
+
 fun height :: "rexp \<Rightarrow> nat" where
   "height ZERO = 1" |
   "height ONE = 1" |
@@ -436,6 +537,12 @@
   "height (SEQ r1 r2) = Suc (max (height r1) (height r2))" |
   "height (STAR r1) = Suc (height r1)" 
 
+lemma height_size2:
+  shows "height r \<le> size2 r"
+  apply(induct r)
+  apply(simp_all)
+  done
+
 lemma height_rexp:
   fixes r :: rexp
   shows "1 \<le> height r"
@@ -443,16 +550,12 @@
   apply(simp_all)
   done
 
-lemma 
+lemma subs_height:
   shows "\<forall>r1 \<in> subs r. height r1 \<le> Suc (height r)"
   apply(induct r)
   apply(auto)+
   done  
   
-
-
-(* tests *)
-
   
 
 end
\ No newline at end of file