--- a/thys/UF_Rec.thy	Tue Apr 29 15:26:48 2014 +0100
+++ b/thys/UF_Rec.thy	Fri May 30 12:04:49 2014 +0100
@@ -1,110 +1,60 @@
 theory UF_Rec
-imports Recs Hoare_tm2
+imports Recs Hoare_tm3
 begin
 
 section {* Coding of Turing Machines and Tapes*}
 
 
-fun actnum :: "taction \<Rightarrow> nat"
+fun actenc :: "action \<Rightarrow> nat"
   where
-  "actnum W0 = 0"
-| "actnum W1 = 1"
-| "actnum L  = 2"
-| "actnum R  = 3"
-
-fun cellnum :: "Block \<Rightarrow> nat" where
-  "cellnum Bk = 0"
-| "cellnum Oc = 1"
-
-
-(* coding programs *)
-
-thm finfun_comp_def
-term finfun_rec
+  "actenc W0 = 0"
+| "actenc W1 = 1"
+| "actenc L  = 2"
+| "actenc R  = 3"
 
-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)
+fun cellenc :: "Block \<Rightarrow> nat" where
+  "cellenc Bk = 0"
+| "cellenc Oc = 1"
 
 
 text {* Coding tapes *}
 
-fun code_tp :: "() \<Rightarrow> nat list"
-  where
-  "code_tp [] = []"
-| "code_tp (c # tp) = (cellnum c) # code_tp tp"
+definition 
+  "intenc i \<equiv> (if (0 \<le> i) then penc 0 (nat i) else penc 1 (nat (-i)))" 
 
-fun Code_tp where
-  "Code_tp tp = lenc (code_tp tp)"
-
-lemma code_tp_append [simp]:
-  "code_tp (tp1 @ tp2) = code_tp tp1 @ code_tp tp2"
-by(induct tp1) (simp_all)
+definition
+  "intdec n \<equiv> (if (0 = pdec1 n) then (int (pdec2 n)) else -(int (pdec2 n)))"
 
-lemma code_tp_length [simp]:
-  "length (code_tp tp) = length tp"
-by (induct tp) (simp_all)
+definition 
+  tapeenc :: "(int f\<rightharpoonup> Block) \<Rightarrow> nat"
+where
+  "tapeenc tp = lenc (map (\<lambda>(x, y). penc (intenc x) (cellenc y)) (fmap_to_alist tp))"
 
-lemma code_tp_nth [simp]:
-  "n < length tp \<Longrightarrow> (code_tp tp) ! n = cellnum (tp ! n)"
-apply(induct n arbitrary: tp) 
-apply(simp_all)
-apply(case_tac [!] tp)
-apply(simp_all)
-done
-
-lemma code_tp_replicate [simp]:
-  "code_tp (c \<up> n) = (cellnum c) \<up> n"
-by(induct n) (simp_all)
+fun 
+  instenc :: "tm_inst \<Rightarrow> nat"
+where
+  "instenc ((a1, s1), (a2, s2)) = lenc [actenc a1, s1, actenc a2, s2]"
 
-text {* Coding Configurations and TMs *}
+definition 
+  progenc :: "(nat f\<rightharpoonup> tm_inst) \<Rightarrow> nat"
+where
+  "progenc p = lenc (map (\<lambda>(x, y). penc x (instenc y)) (fmap_to_alist p))"
 
-fun Code_conf where
-  "Code_conf (s, l, r) = (s, Code_tp l, Code_tp r)"
+text {* Coding Configurations of TMs *}
 
-fun code_instr :: "instr \<Rightarrow> nat" where
-  "code_instr i = penc (actnum (fst i)) (snd i)"
-  
-fun Code_instr :: "instr \<times> instr \<Rightarrow> nat" where
-  "Code_instr i = penc (code_instr (fst i)) (code_instr (snd i))"
+fun confenc where
+  "confenc (faults, prog, s, pos, tp) = lenc [faults, progenc prog, s, intenc pos, tapeenc tp]"
 
-fun code_tprog :: "tprog \<Rightarrow> nat list"
+section {* A Universal Function in HOL *}
+
+fun Step :: "nat \<Rightarrow> nat"
   where
-  "code_tprog [] =  []"
-| "code_tprog (i # tm) = Code_instr i # code_tprog tm"
-
-lemma code_tprog_length [simp]:
-  "length (code_tprog tp) = length tp"
-by (induct tp) (simp_all)
-
-lemma code_tprog_nth [simp]:
-  "n < length tp \<Longrightarrow> (code_tprog tp) ! n = Code_instr (tp ! n)"
-by (induct tp arbitrary: n) (simp_all add: nth_Cons')
-
-fun Code_tprog :: "tprog \<Rightarrow> nat"
-  where 
-  "Code_tprog tm = lenc (code_tprog tm)"
+  "Step cf = Conf (Newstate m (State cf) (Read (Right cf)), 
+                     Newleft (Left cf) (Right cf) (Action m (State cf) (Read (Right cf))),
+                     Newright (Left cf) (Right cf) (Action m (State cf) (Read (Right cf))))"
 
 
-section {* An Universal Function in HOL *}
-
-text {* Reading and writing the encoded tape *}
+text {* Reading and Writing the Encoded Tape *}
 
 fun Read where
   "Read tp = ldec tp 0"