--- 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 =