--- a/thys2/Recs.thy	Fri May 24 20:35:28 2013 +0100
+++ b/thys2/Recs.thy	Fri May 24 22:18:52 2013 +0100
@@ -340,17 +340,22 @@
 definition
   "rec_mod = CN rec_minus [Id 2 0, CN rec_mult [Id 2 1, rec_quo]]"
 
+text {* Iteration *}
 
-section {* Prime Numbers *}
+definition
+   "rec_iter f = PR (Id 2 0) (CN f [Id 3 1])"
 
-definition 
-  "rec_prime = 
-    (let conj1 = CN rec_less [constn 1, Id 1 0] in
-     let disj  = CN rec_disj [CN rec_eq [Id 2 0, constn 1], rec_eq] in
-     let imp   = CN rec_imp [rec_dvd, disj] in
-     let conj2 = CN (rec_all1 imp) [Id 1 0, Id 1 0] in
-     CN rec_conj [conj1, conj2])"
+fun Iter where
+  "Iter f 0 = id"
+| "Iter f (Suc n) = f \<circ> (Iter f n)"
 
+lemma iter_comm:
+  "(Iter f n) (f x) = f ((Iter f n) x)"
+by (induct n) (simp_all)
+
+lemma iter_lemma [simp]:
+  "rec_eval (rec_iter f) [n, x] =  Iter (\<lambda>x. rec_eval f [x]) n x"
+by (induct n) (simp_all add: rec_iter_def)
 
 section {* Correctness of Recursive Functions *}
 
@@ -529,20 +534,6 @@
 by (simp add: rec_mod_def mod_div_equality' nat_mult_commute)
 
 
-section {* Prime Numbers *}
-
-lemma prime_alt_def:
-  fixes p::nat
-  shows "prime p = (1 < p \<and> (\<forall>m \<le> p. m dvd p \<longrightarrow> m = 1 \<or> m = p))"
-apply(auto simp add: prime_nat_def dvd_def)
-apply(drule_tac x="k" in spec)
-apply(auto)
-done
-
-lemma prime_lemma [simp]: 
-  "rec_eval rec_prime [x] = (if prime x then 1 else 0)"
-by (auto simp add: rec_prime_def Let_def prime_alt_def)
-
 section {* Bounded Maximisation *}
 
 fun BMax_rec where
@@ -776,90 +767,20 @@
 by (simp add: enclen_def)
 
 
-
-section {* Discrete Logarithms *}
-
-definition
-  "rec_lg = 
-     (let calc = CN rec_not [CN rec_le [CN rec_power [Id 3 2, Id 3 0], Id 3 1]] in
-      let max  = CN (rec_max2 calc) [Id 2 0, Id 2 0, Id 2 1] in
-      let cond = CN rec_conj [CN rec_less [constn 1, Id 2 0], CN rec_less [constn 1, Id 2 1]] 
-      in CN rec_ifz [cond, Z, max])"
-
-definition
-  "Lg x y = (if 1 < x \<and> 1 < y then BMax_rec (\<lambda>u. y ^ u \<le> x) x else 0)"
-
-lemma lg_lemma [simp]:
-  "rec_eval rec_lg [x, y] = Lg x y"
-by (simp add: rec_lg_def Lg_def Let_def)
-
-definition
-  "Lo x y = (if 1 < x \<and> 1 < y then BMax_rec (\<lambda>u. x mod (y ^ u) = 0) x else 0)"
-
-definition
-  "rec_lo = 
-     (let calc = CN rec_noteq [CN rec_mod [Id 3 1, CN rec_power [Id 3 2, Id 3 0]], Z] in
-      let max  = CN (rec_max2 calc) [Id 2 0, Id 2 0, Id 2 1] in
-      let cond = CN rec_conj [CN rec_less [constn 1, Id 2 0], CN rec_less [constn 1, Id 2 1]] 
-      in CN rec_ifz [cond, Z, max])"
-
-lemma lo_lemma [simp]:
-  "rec_eval rec_lo [x, y] = Lo x y"
-by (simp add: rec_lo_def Lo_def Let_def)
-
-section {* NextPrime number function *}
+definition 
+  "rec_ldec = CN rec_pred [CN rec_pdec1 [rec_swap (rec_iter rec_pdec2)]]"
 
-text {* 
-  @{text "NextPrime x"} returns the first prime number after @{text "x"};
-  @{text "Pi i"} returns the i-th prime number. *}
-
-definition NextPrime ::"nat \<Rightarrow> nat"
-  where
-  "NextPrime x = (LEAST y. y \<le> Suc (fact x) \<and> x < y \<and> prime y)"
-
-definition rec_nextprime :: "recf"
-  where
-  "rec_nextprime = (let conj1 = CN rec_le [Id 2 0, CN S [CN rec_fact [Id 2 1]]] in
-                    let conj2 = CN rec_less [Id 2 1, Id 2 0] in
-                    let conj3 = CN rec_prime [Id 2 0] in 
-                    let conjs = CN rec_conj [CN rec_conj [conj2, conj1], conj3]
-                    in MN (CN rec_not [conjs]))"
-
-lemma nextprime_lemma [simp]:
-  "rec_eval rec_nextprime [x] = NextPrime x"
-by (simp add: rec_nextprime_def Let_def NextPrime_def)
-
-lemma NextPrime_simps [simp]:
-  shows "NextPrime 2 = 3"
-  and   "NextPrime 3 = 5"
-apply(simp_all add: NextPrime_def)
-apply(rule Least_equality)
-apply(auto)
-apply(eval)
-apply(rule Least_equality)
-apply(auto)
-apply(eval)
-apply(case_tac "y = 4")
-apply(auto)
+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
 
-fun Pi :: "nat \<Rightarrow> nat"
-  where
-  "Pi 0 = 2" |
-  "Pi (Suc x) = NextPrime (Pi x)"
-
-lemma Pi_simps [simp]:
-  shows "Pi 1 = 3"
-  and   "Pi 2 = 5"
-using NextPrime_simps
-by(simp_all add: numeral_eq_Suc One_nat_def)
-
-definition 
-  "rec_pi = PR (constn 2) (CN rec_nextprime [Id 2 1])"
-
-lemma pi_lemma [simp]:
-  "rec_eval rec_pi [x] = Pi x"
-by (induct x) (simp_all add: rec_pi_def)
+lemma ldec_lemma [simp]:
+  "rec_eval rec_ldec [z, n] = ldec z n"
+by (simp add: ldec_iter rec_ldec_def)
 
 end
 

--- a/thys2/UF_Rec.thy	Fri May 24 20:35:28 2013 +0100
+++ b/thys2/UF_Rec.thy	Fri May 24 22:18:52 2013 +0100
@@ -448,37 +448,25 @@
 apply(simp only: Stop.simps[symmetric])
 done
 
-text {* UNTIL HERE *}
 
 section {* Universal Function as Recursive Functions *}
 
 definition 
-  "rec_entry = CN rec_lo [Id 2 0, CN rec_pi [CN S [Id 2 1]]]"
-
-fun rec_listsum2 :: "nat \<Rightarrow> nat \<Rightarrow> recf"
-  where
-  "rec_listsum2 vl 0 = CN Z [Id vl 0]"
-| "rec_listsum2 vl (Suc n) = CN rec_add [rec_listsum2 vl n, Id vl n]"
-
-fun rec_strt' :: "nat \<Rightarrow> nat \<Rightarrow> recf"
-  where
-  "rec_strt' xs 0 = Z"
-| "rec_strt' xs (Suc n) = 
-      (let dbound = CN rec_add [rec_listsum2 xs n, constn n] in
-       let t1 = CN rec_power [constn 2, dbound] in
-       let t2 = CN rec_power [constn 2, CN rec_add [Id xs n, dbound]] in
-       CN rec_add [rec_strt' xs n, CN rec_minus [t2, t1]])"
-
-fun rec_map :: "recf \<Rightarrow> nat \<Rightarrow> recf list"
-  where
-  "rec_map rf vl = map (\<lambda>i. CN rf [Id vl i]) [0..<vl]"
-
-fun rec_strt :: "nat \<Rightarrow> recf"
-  where
-  "rec_strt xs = CN (rec_strt' xs xs) (rec_map S xs)"
+  "rec_read = CN rec_ldec [Id 1 0, constn 0]"
 
 definition 
-  "rec_scan = CN rec_mod [Id 1 0, constn 2]"
+  "rec_write = CN rec_penc [S, CN rec_pdec2 [Id 2 1]]"
+
+lemma read_lemma [simp]:
+  "rec_eval rec_read [x] = Read x"
+by (simp add: rec_read_def)
+
+lemma write_lemma [simp]:
+  "rec_eval rec_write [x, y] = Write x y"
+by (simp add: rec_write_def)
+
+
+
 
 definition
     "rec_newleft =