--- a/thys/PDerivs.thy	Sun Feb 17 22:15:06 2019 +0000
+++ b/thys/PDerivs.thy	Wed Feb 20 00:00:30 2019 +0000
@@ -159,7 +159,7 @@
 unfolding pders_Set_def
 by (simp add: PSuf_Union pders_snoc)
 
-lemma pderivs_SEQ:
+lemma pders_SEQ:
   shows "pders s (SEQ r1 r2) \<subseteq> SEQs (pders s r1) r2 \<union> (pders_Set (PSuf s) r2)"
 proof (induct s rule: rev_induct)
   case (snoc c s)
@@ -200,7 +200,7 @@
   shows "pders_Set UNIV1 (SEQ r1 r2) \<subseteq> SEQs (pders_Set UNIV1 r1) r2 \<union> pders_Set UNIV1 r2"
 apply(rule pders_Set_subsetI)
 apply(rule subset_trans)
-apply(rule pderivs_SEQ)
+apply(rule pders_SEQ)
 using pders_Set_SEQ_aux1 pders_Set_SEQ_aux2
 apply auto
 apply blast
@@ -248,6 +248,8 @@
   shows "finite (SEQs A r)"
 using a by auto
 
+thm finite.intros
+
 lemma finite_pders_Set_UNIV1:
   shows "finite (pders_Set UNIV1 r)"
 apply(induct r)
@@ -340,64 +342,111 @@
   finally show "card (pders_Set A r) \<le> awidth r + 1" by simp
 qed
 
-(* tests *)
+(* other result by antimirov *)
+
+fun subs :: "rexp \<Rightarrow> rexp set" where
+"subs ZERO = {ZERO}" |
+"subs ONE = {ONE}" |
+"subs (CHAR a) = {CHAR a, ONE}" |
+"subs (ALT r1 r2) = (subs r1 \<union> subs r2 \<union> {ALT r1 r2})" |
+"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 b: 
-  assumes "rd \<in> pder c r"
-  shows "size rd \<le> (Suc (size r)) * (Suc (size r))"
-  using assms
-  apply(induct r arbitrary: rd)
-  apply(auto)[3]
-  apply(case_tac "c = x")
-      apply(auto)[2]
-  prefer 2
-    apply(auto)[1]
-  oops
-  
-  
+lemma pders_subs:
+  shows "pders s r \<subseteq> subs r"
+  apply(induct r arbitrary: s)
+       apply(simp)
+      apply(simp)
+     apply(simp add: pders_CHAR)
+    apply(simp)
+    apply(rule subset_trans)
+     apply(rule pders_SEQ)
+    defer
+    apply(simp)
+    apply(rule impI)
+    apply(rule conjI)
+  apply blast
+  apply blast
+    apply(case_tac s)
+    apply(simp)
+   apply(rule subset_trans)
+  thm pders_STAR
+     apply(rule pders_STAR)
+     apply(simp)
+    apply(simp)
+  apply (smt UN_I UN_least Un_iff insertCI pders_Set_def subsetCE subsetI)
+  apply(simp)
+  apply(rule conjI)
+  apply blast
+  by (metis Un_insert_right le_supI1 pders_Set_subsetI subset_trans sup_ge2)
 
-lemma a: 
-  assumes "rd \<in> pders s (SEQ r1 r2)"
-  shows "size  rd \<le> Suc (size r1 + size r2)"
-  using assms
-  apply(induct s arbitrary: r1 r2 rd)
-   apply(simp)
-  apply(auto)
-  apply(case_tac "nullable r1")
-   apply(auto)
-  oops
-  
+fun size2 :: "rexp \<Rightarrow> nat" where
+  "size2 ZERO = 1" |
+  "size2 ONE = 1" |
+  "size2 (CHAR c) = 1" |
+  "size2 (ALT r1 r2) = Suc (size2 r1 + size2 r2)" |
+  "size2 (SEQ r1 r2) = Suc (size2 r1 + size2 r2)" |
+  "size2 (STAR r1) = Suc (size2 r1)" 
+
+
+lemma size_rexp:
+  fixes r :: rexp
+  shows "1 \<le> size2 r"
+  apply(induct r)
+  apply(simp)
+  apply(simp_all)
+  done
 
 lemma
-  shows "\<forall>rd \<in> (pders_Set UNIV r). size rd \<le> size r"
+  shows "\<forall>r1 \<in> subs r. size2 r1 \<le> Suc (size2 r * size2 r)"
   apply(induct r)
-       apply(auto)[1]
-       apply(simp add: pders_Set_def)
-      apply(simp add: pders_Set_def)
-     apply(simp add: pders_Set_def pders_CHAR)
-  using pders_CHAR apply fastforce
-    prefer 2
-    apply(simp add: pders_Set_def)
-    apply (meson Un_iff le_SucI trans_le_add1 trans_le_add2)
-  apply(simp add: pders_Set_def)
-   apply(auto)[1]
-  apply(case_tac y)
-  apply(simp)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+    apply(simp)
+    apply(auto)[1]
+  apply (smt Suc_n_not_le_n add.commute distrib_left le_Suc_eq left_add_mult_distrib nat_le_linear trans_le_add1)
+  apply (smt Suc_le_mono Suc_n_not_le_n le_trans nat_le_linear power2_eq_square power2_sum semiring_normalization_rules(23) trans_le_add2)
+  apply (smt Groups.add_ac(3) Suc_n_not_le_n distrib_left le_Suc_eq left_add_mult_distrib nat_le_linear trans_le_add1)
    apply(simp)
    apply(auto)[1]
-   apply(case_tac "nullable r1")
-    apply(simp)
-    apply(auto)[1]
-     prefer 3
-     apply(simp)
-     apply(auto)[1]
-     apply(subgoal_tac "size xa \<le> size r1")
-      prefer 2
-      apply (metis UN_I pders.simps(1) pders_snoc singletonI)
-  oops
+  apply (smt Groups.add_ac(2) Suc_le_mono Suc_n_not_le_n le_add2 linear order_trans power2_eq_square power2_sum)
+  apply (smt Groups.add_ac(2) Suc_le_mono Suc_n_not_le_n left_add_mult_distrib linear mult.commute order.trans trans_le_add1)
+  apply(auto)[1]
+  apply(drule_tac x="r'" in bspec)
+   apply(simp)
+  apply(rule le_trans)
+   apply(assumption)
+  apply(simp)
+  using size_rexp
+  apply(simp)
+  done
   
+fun height :: "rexp \<Rightarrow> nat" where
+  "height ZERO = 1" |
+  "height ONE = 1" |
+  "height (CHAR c) = 1" |
+  "height (ALT r1 r2) = Suc (max (height r1) (height r2))" |
+  "height (SEQ r1 r2) = Suc (max (height r1) (height r2))" |
+  "height (STAR r1) = Suc (height r1)" 
+
+lemma height_rexp:
+  fixes r :: rexp
+  shows "1 \<le> height r"
+  apply(induct r)
+  apply(simp_all)
+  done
+
+lemma 
+  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