--- a/thys/UF_Rec.thy	Fri Apr 04 13:15:07 2014 +0100
+++ b/thys/UF_Rec.thy	Tue Apr 29 15:26:48 2014 +0100
@@ -1,5 +1,5 @@
 theory UF_Rec
-imports Recs Hoare_tm
+imports Recs Hoare_tm2
 begin
 
 section {* Coding of Turing Machines and Tapes*}
@@ -12,17 +12,40 @@
 | "actnum L  = 2"
 | "actnum R  = 3"
 
-
 fun cellnum :: "Block \<Rightarrow> nat" where
   "cellnum Bk = 0"
 | "cellnum Oc = 1"
 
 
-(* NEED TO CODE TAPES *)
+(* coding programs *)
+
+thm finfun_comp_def
+term finfun_rec
+
+definition code_finfun :: "(nat \<Rightarrow>f tm_inst option) \<Rightarrow> (nat \<times> tm_inst option) list"
+  where
+  "code_finfun f = ([(x, f $ x). x \<leftarrow> finfun_to_list f])"
+
+fun lookup where
+  "lookup [] c = None"
+| "lookup ((a, b)#xs) c = (if a = c then b else lookup xs c)"
+
+lemma
+  "f $ n = lookup (code_finfun f) n"
+apply(induct f rule: finfun_weak_induct)
+apply(simp add: code_finfun_def)
+apply(simp add: finfun_to_list_const)
+thm finfun_rec_const
+apply(finfun_rec_const)
+apply(simp add: finfun_rec_def)
+apply(auto)
+thm finfun_rec_unique
+apply(rule finfun_rec_unique)
+
 
 text {* Coding tapes *}
 
-fun code_tp :: "cell list \<Rightarrow> nat list"
+fun code_tp :: "() \<Rightarrow> nat list"
   where
   "code_tp [] = []"
 | "code_tp (c # tp) = (cellnum c) # code_tp tp"