--- a/thys2/Recs.thy	Fri May 24 22:18:52 2013 +0100
+++ b/thys2/Recs.thy	Sat May 25 01:32:35 2013 +0100
@@ -326,6 +326,7 @@
 
 text {* Dvd, Quotient, Modulo *}
 
+(* FIXME: probably all not needed *)
 definition 
   "rec_dvd = 
      rec_swap (CN (rec_ex2 (CN rec_eq [Id 3 2, CN rec_mult [Id 3 1, Id 3 0]])) [Id 2 0, Id 2 1, Id 2 0])"  
@@ -349,7 +350,7 @@
   "Iter f 0 = id"
 | "Iter f (Suc n) = f \<circ> (Iter f n)"
 
-lemma iter_comm:
+lemma Iter_comm:
   "(Iter f n) (f x) = f ((Iter f n) x)"
 by (induct n) (simp_all)
 
@@ -697,6 +698,8 @@
   "rec_eval rec_penc [m, n] = penc m n"
 by (simp add: rec_penc_def prod_encode_def)
 
+text {* encoding and decoding of lists of natural numbers *}
+
 fun 
   lenc :: "nat list \<Rightarrow> nat" 
 where
@@ -714,17 +717,15 @@
   "pdec2 0 = 0"
 by (simp_all add: prod_decode_def prod_decode_aux.simps)
 
-lemma w:
+lemma ldec_zero:
   "ldec 0 n = 0"
 by (induct n) (simp_all add: prod_decode_def prod_decode_aux.simps)
 
 lemma list_encode_inverse: 
   "ldec (lenc xs) n = (if n < length xs then xs ! n else 0)"
-apply(induct xs arbitrary: n rule: lenc.induct) 
-apply(simp_all add: w)
-apply(case_tac n)
-apply(simp_all)
-done
+by (induct xs arbitrary: n rule: lenc.induct) 
+   (auto simp add: ldec_zero nth_Cons split: nat.splits)
+
 
 lemma lenc_length_le:
   "length xs \<le> lenc xs"  
@@ -766,21 +767,45 @@
   "enclen 0 = 0"
 by (simp add: enclen_def)
 
+fun 
+  rec_lenc :: "recf list \<Rightarrow> recf" 
+where
+  "rec_lenc [] = Z"
+| "rec_lenc (f # fs) = CN rec_penc [CN S [f], rec_lenc fs]"
 
 definition 
   "rec_ldec = CN rec_pred [CN rec_pdec1 [rec_swap (rec_iter rec_pdec2)]]"
 
+definition 
+  "rec_within = CN rec_less [Z, rec_swap (rec_iter rec_pdec2)]"
+
+definition
+  "rec_enclen = CN (rec_max1 (CN rec_not [CN rec_within [Id 2 1, CN rec_pred [Id 2 0]]])) [Id 1 0, Id 1 0]"
+
 lemma ldec_iter:
   "ldec z n = pdec1 ((Iter pdec2 n) z) - 1"
-apply(induct n arbitrary: z)
-apply(simp_all)
-apply(subst iter_comm)
-apply(simp)
-done
+by (induct n arbitrary: z) (simp | subst Iter_comm)+
+
+lemma within_iter:
+  "within z n = (0 < (Iter pdec2 n) z)"
+by (induct n arbitrary: z) (simp | subst Iter_comm)+
+
+lemma lenc_lemma [simp]:
+  "rec_eval (rec_lenc fs) xs = lenc (map (\<lambda>f. rec_eval f xs) fs)"
+by (induct fs) (simp_all)
 
 lemma ldec_lemma [simp]:
   "rec_eval rec_ldec [z, n] = ldec z n"
 by (simp add: ldec_iter rec_ldec_def)
 
+lemma within_lemma [simp]:
+  "rec_eval rec_within [z, n] = (if within z n then 1 else 0)"
+by (simp add: within_iter rec_within_def)
+
+lemma enclen_lemma [simp]:
+  "rec_eval rec_enclen [z] = enclen z"
+by (simp add: rec_enclen_def enclen_def)
+
+
 end