--- a/thys/PDerivs.thy	Mon Feb 11 23:18:05 2019 +0000
+++ b/thys/PDerivs.thy	Sun Feb 17 22:15:06 2019 +0000
@@ -340,5 +340,64 @@
   finally show "card (pders_Set A r) \<le> awidth r + 1" by simp
 qed
 
+(* tests *)
+
+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 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
+  
+
+lemma
+  shows "\<forall>rd \<in> (pders_Set UNIV r). size rd \<le> size 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(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
+  
+  
+  
+  
 
 end
\ No newline at end of file