--- a/thys2/Recs.thy	Sat May 25 01:33:31 2013 +0100
+++ b/thys2/Recs.thy	Sat May 25 11:46:25 2013 +0100
@@ -310,6 +310,11 @@
 definition 
   "rec_accum2 f = PR (CN f [Z, Id 2 0, Id 2 1]) (CN rec_mult [Id 4 1, CN f [S, Id 4 2, Id 4 3]])"
 
+definition 
+  "rec_accum3 f = PR (CN f [Z, Id 3 0, Id 3 1, Id 3 2]) 
+                     (CN rec_mult [Id 5 1, CN f [S, Id 5 2, Id 5 3, Id 5 4]])"
+
+
 text {* Bounded quantifiers for one and two arguments *}
 
 definition
@@ -319,6 +324,17 @@
   "rec_all2 f = CN rec_sign [rec_accum2 f]"
 
 definition
+  "rec_all3 f = CN rec_sign [rec_accum3 f]"
+
+definition
+  "rec_all1_less f = (let f' = CN rec_disj [CN rec_eq [Id 3 0, Id 3 1], CN f [Id 3 0, Id 3 2]] 
+                      in CN (rec_all2 f') [Id 2 0, Id 2 0, Id 2 1])"
+
+definition
+  "rec_all2_less f = (let f' = CN rec_disj [CN rec_eq [Id 4 0, Id 4 1], CN f [Id 4 0, Id 4 2, Id 4 3]] 
+                      in CN (rec_all3 f') [Id 3 0, Id 3 0, Id 3 1, Id 3 2])"
+
+definition
   "rec_ex1 f = CN rec_sign [rec_sigma1 f]"
 
 definition
@@ -452,6 +468,10 @@
   shows "rec_eval (rec_accum2 f) [x, y1, y2] = (\<Prod> z \<le> x. (rec_eval f)  [z, y1, y2])"
 by (induct x) (simp_all add: rec_accum2_def)
 
+lemma accum3_lemma [simp]: 
+  shows "rec_eval (rec_accum3 f) [x, y1, y2, y3] = (\<Prod> z \<le> x. (rec_eval f)  [z, y1, y2, y3])"
+by (induct x) (simp_all add: rec_accum3_def)
+
 lemma ex1_lemma [simp]:
  "rec_eval (rec_ex1 f) [x, y] = (if (\<exists>z \<le> x. 0 < rec_eval f [z, y]) then 1 else 0)"
 by (simp add: rec_ex1_def)
@@ -468,6 +488,22 @@
  "rec_eval (rec_all2 f) [x, y1, y2] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)"
 by (simp add: rec_all2_def)
 
+lemma all3_lemma [simp]:
+ "rec_eval (rec_all3 f) [x, y1, y2, y3] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y1, y2, y3]) then 1 else 0)"
+by (simp add: rec_all3_def)
+
+lemma all1_less_lemma [simp]:
+  "rec_eval (rec_all1_less f) [x, y] = (if (\<forall>z < x. 0 < rec_eval f [z, y]) then 1 else 0)"
+apply(auto simp add: Let_def rec_all1_less_def)
+apply (metis nat_less_le)+
+done
+
+lemma all2_less_lemma [simp]:
+  "rec_eval (rec_all2_less f) [x, y1, y2] = (if (\<forall>z < x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)"
+apply(auto simp add: Let_def rec_all2_less_def)
+apply(metis nat_less_le)+
+done
+
 
 lemma dvd_alt_def:
   fixes x y k:: nat