# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1358423460 0
# Node ID 251e192339b75d634c8227564facc0b4346aa871
# Parent  df4c7bb6c79eb11ad21feced45db311a27c9d618
added abacus

diff -r df4c7bb6c79e -r 251e192339b7 thys/abacus.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/abacus.thy	Thu Jan 17 11:51:00 2013 +0000
@@ -0,0 +1,712 @@
+header {* 
+ {\em abacus} a kind of register machine
+*}
+
+theory abacus
+imports Main turing_basic
+begin
+
+text {*
+  {\em Abacus} instructions:
+*}
+
+datatype abc_inst =
+  -- {* @{text "Inc n"} increments the memory cell (or register) with address @{text "n"} by one.
+     *}
+     Inc nat
+  -- {*
+     @{text "Dec n label"} decrements the memory cell with address @{text "n"} by one. 
+      If cell @{text "n"} is already zero, no decrements happens and the executio jumps to
+      the instruction labeled by @{text "label"}.
+     *}
+   | Dec nat nat
+  -- {*
+  @{text "Goto label"} unconditionally jumps to the instruction labeled by @{text "label"}.
+  *}
+   | Goto nat
+  
+
+text {*
+  Abacus programs are defined as lists of Abacus instructions.
+*}
+type_synonym abc_prog = "abc_inst list"
+
+section {*
+  Sample Abacus programs
+  *}
+
+text {*
+  Abacus for addition and clearance.
+*}
+fun plus_clear :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"  
+  where
+  "plus_clear m n e = [Dec m e, Inc n, Goto 0]"
+
+text {*
+  Abacus for clearing memory untis.
+*}
+fun clear :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"
+  where
+  "clear n e = [Dec n e, Goto 0]"
+
+fun plus:: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"
+  where
+  "plus m n p e = [Dec m 4, Inc n, Inc p,
+                   Goto 0, Dec p e, Inc m, Goto 4]"
+
+fun mult :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"
+  where
+  "mult m1 m2 n p e = [Dec m1 e]@ plus m1 m2 p 1"
+
+fun expo :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"
+  where
+  "expo n m1 m2 p e = [Inc n, Dec m1 e] @ mult m2 n n p 2"
+
+
+text {*
+  The state of Abacus machine.
+  *}
+type_synonym abc_state = nat
+
+(* text {*
+  The memory of Abacus machine is defined as a function from address to contents.
+*}
+type_synonym abc_mem = "nat \<Rightarrow> nat" *)
+
+text {*
+  The memory of Abacus machine is defined as a list of contents, with 
+  every units addressed by index into the list.
+  *}
+type_synonym abc_lm = "nat list"
+
+text {*
+  Fetching contents out of memory. Units not represented by list elements are considered
+  as having content @{text "0"}.
+*}
+fun abc_lm_v :: "abc_lm \<Rightarrow> nat \<Rightarrow> nat"
+  where 
+    "abc_lm_v lm n = (if (n < length lm) then (lm!n) else 0)"         
+
+
+text {*
+  Set the content of memory unit @{text "n"} to value @{text "v"}.
+  @{text "am"} is the Abacus memory before setting.
+  If address @{text "n"} is outside to scope of @{text "am"}, @{text "am"} 
+  is extended so that @{text "n"} becomes in scope.
+*}
+
+fun abc_lm_s :: "abc_lm \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_lm"
+  where
+    "abc_lm_s am n v = (if (n < length am) then (am[n:=v]) else 
+                           am@ (replicate (n - length am) 0) @ [v])"
+
+
+text {*
+  The configuration of Abaucs machines consists of its current state and its
+  current memory:
+*}
+type_synonym abc_conf = "abc_state \<times> abc_lm"
+
+text {*
+  Fetch instruction out of Abacus program:
+*}
+
+fun abc_fetch :: "nat \<Rightarrow> abc_prog \<Rightarrow> abc_inst option" 
+  where
+  "abc_fetch s p = (if (s < length p) then Some (p ! s)
+                    else None)"
+
+text {*
+  Single step execution of Abacus machine. If no instruction is feteched, 
+  configuration does not change.
+*}
+fun abc_step_l :: "abc_conf \<Rightarrow> abc_inst option \<Rightarrow> abc_conf"
+  where
+  "abc_step_l (s, lm) a = (case a of 
+               None \<Rightarrow> (s, lm) |
+               Some (Inc n)  \<Rightarrow> (let nv = abc_lm_v lm n in
+                       (s + 1, abc_lm_s lm n (nv + 1))) |
+               Some (Dec n e) \<Rightarrow> (let nv = abc_lm_v lm n in
+                       if (nv = 0) then (e, abc_lm_s lm n 0) 
+                       else (s + 1,  abc_lm_s lm n (nv - 1))) |
+               Some (Goto n) \<Rightarrow> (n, lm) 
+               )"
+
+text {*
+  Multi-step execution of Abacus machine.
+*}
+fun abc_steps_l :: "abc_conf \<Rightarrow> abc_prog \<Rightarrow> nat \<Rightarrow> abc_conf"
+  where
+  "abc_steps_l (s, lm) p 0 = (s, lm)" |
+  "abc_steps_l (s, lm) p (Suc n) = 
+      abc_steps_l (abc_step_l (s, lm) (abc_fetch s p)) p n"
+
+section {*
+  Compiling Abacus machines into Truing machines
+*}
+
+subsection {*
+  Compiling functions
+*}
+
+text {*
+  @{text "findnth n"} returns the TM which locates the represention of
+  memory cell @{text "n"} on the tape and changes representation of zero
+  on the way.
+*}
+
+fun findnth :: "nat \<Rightarrow> instr list"
+  where
+  "findnth 0 = []" |
+  "findnth (Suc n) = (findnth n @ [(W1, 2 * n + 1), 
+           (R, 2 * n + 2), (R, 2 * n + 3), (R, 2 * n + 2)])"
+
+text {*
+  @{text "tinc_b"} returns the TM which increments the representation 
+  of the memory cell under rw-head by one and move the representation 
+  of cells afterwards to the right accordingly.
+  *}
+
+definition tinc_b :: "instr list"
+  where
+  "tinc_b \<equiv> [(W1, 1), (R, 2), (W1, 3), (R, 2), (W1, 3), (R, 4), 
+             (L, 7), (W0, 5), (R, 6), (W0, 5), (W1, 3), (R, 6),
+             (L, 8), (L, 7), (R, 9), (L, 7), (R, 10), (W0, 9)]" 
+
+text {*
+  @{text "tinc ss n"} returns the TM which simulates the execution of 
+  Abacus instruction @{text "Inc n"}, assuming that TM is located at
+  location @{text "ss"} in the final TM complied from the whole
+  Abacus program.
+*}
+
+fun tinc :: "nat \<Rightarrow> nat \<Rightarrow> instr list"
+  where
+  "tinc ss n = shift (findnth n @ shift tinc_b (2 * n)) (ss - 1)"
+
+text {*
+  @{text "tinc_b"} returns the TM which decrements the representation 
+  of the memory cell under rw-head by one and move the representation 
+  of cells afterwards to the left accordingly.
+  *}
+
+definition tdec_b :: "instr list"
+  where
+  "tdec_b \<equiv>  [(W1, 1), (R, 2), (L, 14), (R, 3), (L, 4), (R, 3),
+              (R, 5), (W0, 4), (R, 6), (W0, 5), (L, 7), (L, 8),
+              (L, 11), (W0, 7), (W1, 8), (R, 9), (L, 10), (R, 9),
+              (R, 5), (W0, 10), (L, 12), (L, 11), (R, 13), (L, 11),
+              (R, 17), (W0, 13), (L, 15), (L, 14), (R, 16), (L, 14),
+              (R, 0), (W0, 16)]"
+
+text {*
+  @{text "sete tp e"} attaches the termination edges (edges leading to state @{text "0"}) 
+  of TM @{text "tp"} to the intruction labelled by @{text "e"}.
+  *}
+
+fun sete :: "instr list \<Rightarrow> nat \<Rightarrow> instr list"
+  where
+  "sete tp e = map (\<lambda> (action, state). (action, if state = 0 then e else state)) tp"
+
+text {*
+  @{text "tdec ss n label"} returns the TM which simulates the execution of 
+  Abacus instruction @{text "Dec n label"}, assuming that TM is located at
+  location @{text "ss"} in the final TM complied from the whole
+  Abacus program.
+*}
+
+fun tdec :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> instr list"
+  where
+  "tdec ss n e = sete (shift (findnth n @ shift tdec_b (2 * n)) 
+                 (ss - 1)) e"
+ 
+text {*
+  @{text "tgoto f(label)"} returns the TM simulating the execution of Abacus instruction
+  @{text "Goto label"}, where @{text "f(label)"} is the corresponding location of
+  @{text "label"} in the final TM compiled from the overall Abacus program.
+*}
+
+fun tgoto :: "nat \<Rightarrow> instr list"
+  where
+  "tgoto n = [(Nop, n), (Nop, n)]"
+
+text {*
+  The layout of the final TM compiled from an Abacus program is represented
+  as a list of natural numbers, where the list element at index @{text "n"} represents the 
+  starting state of the TM simulating the execution of @{text "n"}-th instruction
+  in the Abacus program.
+*}
+
+type_synonym layout = "nat list"
+
+text {*
+  @{text "length_of i"} is the length of the 
+  TM simulating the Abacus instruction @{text "i"}.
+*}
+fun length_of :: "abc_inst \<Rightarrow> nat"
+  where
+  "length_of i = (case i of 
+                    Inc n   \<Rightarrow> 2 * n + 9 |
+                    Dec n e \<Rightarrow> 2 * n + 16 |
+                    Goto n  \<Rightarrow> 1)"
+
+text {*
+  @{text "layout_of ap"} returns the layout of Abacus program @{text "ap"}.
+*}
+fun layout_of :: "abc_prog \<Rightarrow> layout"
+  where "layout_of ap = map length_of ap"
+
+
+text {*
+  @{text "start_of layout n"} looks out the starting state of @{text "n"}-th
+  TM in the finall TM.
+*}
+thm listsum_def
+
+fun start_of :: "nat list \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "start_of ly x = (Suc (listsum (take x ly))) "
+
+text {*
+  @{text "ci lo ss i"} complies Abacus instruction @{text "i"}
+  assuming the TM of @{text "i"} starts from state @{text "ss"} 
+  within the overal layout @{text "lo"}.
+*}
+
+fun ci :: "layout \<Rightarrow> nat \<Rightarrow> abc_inst \<Rightarrow> instr list"
+  where
+  "ci ly ss (Inc n) = tinc ss n"
+| "ci ly ss (Dec n e) = tdec ss n (start_of ly e)"
+| "ci ly ss (Goto n) = tgoto (start_of ly n)"
+
+text {*
+  @{text "tpairs_of ap"} transfroms Abacus program @{text "ap"} pairing
+  every instruction with its starting state.
+*}
+
+fun tpairs_of :: "abc_prog \<Rightarrow> (nat \<times> abc_inst) list"
+  where "tpairs_of ap = (zip (map (start_of (layout_of ap)) 
+                         [0..<(length ap)]) ap)"
+
+text {*
+  @{text "tms_of ap"} returns the list of TMs, where every one of them simulates
+  the corresponding Abacus intruction in @{text "ap"}.
+*}
+
+fun tms_of :: "abc_prog \<Rightarrow> (instr list) list"
+  where "tms_of ap = map (\<lambda> (n, tm). ci (layout_of ap) n tm) 
+                         (tpairs_of ap)"
+
+text {*
+  @{text "tm_of ap"} returns the final TM machine compiled from Abacus program @{text "ap"}.
+*}
+fun tm_of :: "abc_prog \<Rightarrow> instr list"
+  where "tm_of ap = concat (tms_of ap)"
+
+text {*
+  The following two functions specify the well-formedness of complied TM.
+*}
+(*
+fun t_ncorrect :: "tprog \<Rightarrow> bool"
+  where
+  "t_ncorrect tp = (length tp mod 2 = 0)"
+
+fun abc2t_correct :: "abc_prog \<Rightarrow> bool"
+  where 
+  "abc2t_correct ap = list_all (\<lambda> (n, tm). 
+             t_ncorrect (ci (layout_of ap) n tm)) (tpairs_of ap)"
+*)
+
+lemma length_findnth: 
+  "length (findnth n) = 4 * n"
+apply(induct n, auto)
+done
+
+lemma ci_length : "length (ci ns n ai) div 2 = length_of ai"
+apply(auto simp: ci.simps tinc_b_def tdec_b_def length_findnth
+                 split: abc_inst.splits)
+done
+
+subsection {*
+  Representation of Abacus memory by TM tape
+*}
+
+text {*
+  @{text "crsp acf tcf"} meams the abacus configuration @{text "acf"}
+  is corretly represented by the TM configuration @{text "tcf"}.
+*}
+
+fun crsp :: "layout \<Rightarrow> abc_conf \<Rightarrow> config \<Rightarrow> cell list \<Rightarrow> bool"
+  where 
+  "crsp ly (as, lm) (s, l, r) inres = 
+           (s = start_of ly as \<and> (\<exists> x. r = <lm> @ Bk\<up>x) \<and> 
+            l = Bk # Bk # inres)"
+
+declare crsp.simps[simp del]
+
+subsection {*
+  A more general definition of TM execution. 
+*}
+
+                    
+text {*
+  The type of invarints expressing correspondence between 
+  Abacus configuration and TM configuration.
+*}
+
+type_synonym inc_inv_t = "abc_conf \<Rightarrow> config \<Rightarrow> cell list \<Rightarrow> bool"
+
+declare tms_of.simps[simp del] tm_of.simps[simp del]
+        layout_of.simps[simp del] abc_fetch.simps [simp del]  
+        tpairs_of.simps[simp del] start_of.simps[simp del]
+        ci.simps [simp del] length_of.simps[simp del] 
+        layout_of.simps[simp del]
+
+
+(*
+subsection {* The compilation of @{text "Inc n"} *}
+*)
+
+text {*
+  The lemmas in this section lead to the correctness of 
+  the compilation of @{text "Inc n"} instruction.
+*}
+
+
+declare abc_step_l.simps[simp del] abc_steps_l.simps[simp del]
+lemma [simp]: "start_of ly as > 0"
+apply(simp add: start_of.simps)
+done
+
+lemma abc_step_red: 
+ "abc_steps_l ac aprog stp = (as, am) \<Longrightarrow> 
+   abc_steps_l ac aprog (Suc stp) = abc_step_l (as, am) (abc_fetch as aprog) "
+sorry
+
+lemma tm_shift_fetch: 
+  "\<lbrakk>fetch A s b = (ac, ns); ns \<noteq> 0 \<rbrakk>
+  \<Longrightarrow> fetch (shift A off) s b = (ac, ns + off)"
+apply(case_tac b)
+apply(case_tac [!] s, auto simp: fetch.simps shift.simps)
+done
+
+lemma tm_shift_eq_step:
+  assumes exec: "step (s, l, r) (A, 0) = (s', l', r')"
+  and notfinal: "s' \<noteq> 0"
+  shows "step (s + off, l, r) (shift A off, off) = (s' + off, l', r')"
+using assms
+apply(simp add: step.simps)
+apply(case_tac "fetch A s (read r)", auto)
+apply(drule_tac [!] off = off in tm_shift_fetch, simp_all)
+done
+
+lemma tm_shift_eq_steps: 
+  assumes layout: "ly = layout_of ap"
+  and compile: "tp = tm_of ap"
+  and exec: "steps (s, l, r) (A, 0) stp = (s', l', r')"
+  and notfinal: "s' \<noteq> 0"
+  shows "steps (s + off, l, r) (shift A off, off) stp = (s' + off, l', r')"
+  using exec notfinal
+proof(induct stp arbitrary: s' l' r', simp add: steps.simps)
+  fix stp s' l' r'
+  assume ind: "\<And>s' l' r'. \<lbrakk>steps (s, l, r) (A, 0) stp = (s', l', r'); s' \<noteq> 0\<rbrakk> 
+     \<Longrightarrow> steps (s + off, l, r) (shift A off, off) stp = (s' + off, l', r')"
+  and h: " steps (s, l, r) (A, 0) (Suc stp) = (s', l', r')" "s' \<noteq> 0"
+  obtain s1 l1 r1 where g: "steps (s, l, r) (A, 0) stp = (s1, l1, r1)" 
+    apply(case_tac "steps (s, l, r) (A, 0) stp") by blast
+  moreover then have "s1 \<noteq> 0"
+    using h
+    apply(simp add: step_red, case_tac "0 < s1", simp, simp)
+    done
+  ultimately have "steps (s + off, l, r) (shift A off, off) stp =
+                   (s1 + off, l1, r1)"
+    apply(rule_tac ind, simp_all)
+    done
+  thus "steps (s + off, l, r) (shift A off, off) (Suc stp) = (s' + off, l', r')"
+    using h g assms
+    apply(simp add: step_red)
+    apply(rule_tac tm_shift_eq_step, auto)
+    done
+qed
+
+lemma startof_not0[simp]: "0 < start_of ly as"
+apply(simp add: start_of.simps)
+done
+
+lemma startof_ge1[simp]: "Suc 0 \<le> start_of ly as"
+apply(simp add: start_of.simps)
+done
+
+lemma step_eq_fetch: 
+  assumes layout: "ly = layout_of ap"
+  and compile: "tp = tm_of ap"
+  and abc_fetch: "abc_fetch as ap = Some ins" 
+  and fetch: "fetch (ci ly (start_of ly as) ins)
+       (Suc s - start_of ly as) b = (ac, ns)"
+  and notfinal: "ns \<noteq> 0"
+  shows "fetch tp s b = (ac, ns)"
+proof -
+  have "s > start_of ly as \<and> s < start_of ly (Suc as)"
+    sorry
+  thus "fetch tp s b = (ac, ns)"
+    sorry
+qed
+  
+lemma step_eq_in:
+  assumes layout: "ly = layout_of ap"
+  and compile: "tp = tm_of ap"
+  and fetch: "abc_fetch as ap = Some ins"    
+  and exec: "step (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) 
+  = (s', l', r')"
+  and notfinal: "s' \<noteq> 0"
+  shows "step (s, l, r) (tp, 0) = (s', l', r')"
+  using assms
+  apply(simp add: step.simps)
+  apply(case_tac "fetch (ci (layout_of ap) (start_of (layout_of ap) as) ins)
+    (Suc s - start_of (layout_of ap) as) (read r)", simp)
+  using layout
+  apply(drule_tac s = s and b = "read r" and ac = a in step_eq_fetch, auto)
+  done
+
+lemma steps_eq_in:
+  assumes layout: "ly = layout_of ap"
+  and compile: "tp = tm_of ap"
+  and crsp: "crsp ly (as, lm) (s, l, r) ires"
+  and fetch: "abc_fetch as ap = Some ins"    
+  and exec: "steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp 
+  = (s', l', r')"
+  and notfinal: "s' \<noteq> 0"
+  shows "steps (s, l, r) (tp, 0) stp = (s', l', r')"
+  using exec notfinal
+proof(induct stp arbitrary: s' l' r', simp add: steps.simps)
+  fix stp s' l' r'
+  assume ind: 
+    "\<And>s' l' r'. \<lbrakk>steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp = (s', l', r'); s' \<noteq> 0\<rbrakk>
+              \<Longrightarrow> steps (s, l, r) (tp, 0) stp = (s', l', r')"
+  and h: "steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) (Suc stp) = (s', l', r')" "s' \<noteq> 0"
+  obtain s1 l1 r1 where g: "steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp = 
+                        (s1, l1, r1)"
+    apply(case_tac "steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp") by blast
+  moreover hence "s1 \<noteq> 0"
+    using h
+    apply(simp add: step_red)
+    apply(case_tac "0 < s1", simp_all)
+    done
+  ultimately have "steps (s, l, r) (tp, 0) stp = (s1, l1, r1)"
+    apply(rule_tac ind, auto)
+    done
+  thus "steps (s, l, r) (tp, 0) (Suc stp) = (s', l', r')"
+    using h g assms
+    apply(simp add: step_red)
+    apply(rule_tac step_eq_in, auto)
+    done
+qed
+
+lemma tm_append_fetch_first: 
+  "\<lbrakk>fetch A s b = (ac, ns); ns \<noteq> 0\<rbrakk> \<Longrightarrow> 
+    fetch (A @ B) s b = (ac, ns)"
+apply(case_tac b)
+apply(case_tac [!] s, auto simp: fetch.simps nth_append split: if_splits)
+done
+
+lemma tm_append_first_step_eq: 
+  assumes "step (s, l, r) (A, 0) = (s', l', r')"
+  and "s' \<noteq> 0"
+  shows "step (s, l, r) (A @ B, 0) = (s', l', r')"
+using assms
+apply(simp add: step.simps)
+apply(case_tac "fetch A s (read r)")
+apply(frule_tac  B = B and b = "read r" in tm_append_fetch_first, auto)
+done
+
+lemma tm_append_first_steps_eq: 
+  assumes "steps (s, l, r) (A, 0) stp = (s', l', r')"
+  and "s' \<noteq> 0"
+  shows "steps (s, l, r) (A @ B, 0) stp = (s', l', r')"
+using assms
+sorry
+
+lemma tm_append_second_steps_eq: 
+  assumes 
+  exec: "steps (s, l, r) (B, 0) stp = (s', l', r')"
+  and notfinal: "s' \<noteq> 0"
+  and off: "off = length A div 2"
+  and even: "length A mod 2 = 0"
+  shows "steps (s + off, l, r) (A @ shift B off, 0) stp = (s' + off, l', r')"
+using assms
+sorry
+
+lemma tm_append_steps: 
+  assumes 
+  aexec: "steps (s, l, r) (A, 0) stpa = (Suc (length A div 2), la, ra)"
+  and bexec: "steps (Suc 0, la, ra) (B, 0) stpb =  (sb, lb, rb)"
+  and notfinal: "sb \<noteq> 0"
+  and off: "off = length A div 2"
+  and even: "length A mod 2 = 0"
+  shows "steps (s, l, r) (A @ shift B off, 0) (stpa + stpb) = (sb + off, lb, rb)"
+proof -
+  have "steps (s, l, r) (A@shift B off, 0) stpa = (Suc (length A div 2), la, ra)"
+    apply(rule_tac tm_append_first_steps_eq)
+    apply(auto simp: assms)
+    done
+  moreover have "steps (1 + off, la, ra) (A @ shift B off, 0) stpb = (sb + off, lb, rb)"
+    apply(rule_tac tm_append_second_steps_eq)
+    apply(auto simp: assms bexec)
+    done
+  ultimately show "steps (s, l, r) (A @ shift B off, 0) (stpa + stpb) = (sb + off, lb, rb)"
+    apply(simp add: steps_add off)
+    done
+qed
+       
+subsection {* Crsp of Inc*}
+
+lemma crsp_step_inc:
+  assumes layout: "ly = layout_of ap"
+  and crsp: "crsp ly (as, lm) (s, l, r) ires"
+  and fetch: "abc_fetch as ap = Some (Inc n)"
+  shows "\<exists>stp. crsp ly (abc_step_l (as, lm) (Some (Inc n)))
+  (steps (s, l, r) (ci ly (start_of ly as) (Inc n), start_of ly as - Suc 0) stp) ires"
+  sorry
+    
+subsection{* Crsp of Dec n e*}
+lemma crsp_step_dec: 
+  assumes layout: "ly = layout_of ap"
+  and crsp: "crsp ly (as, lm) (s, l, r) ires"
+  shows "\<exists>stp. crsp ly (abc_step_l (as, lm) (Some (Dec n e)))
+  (steps (s, l, r) (ci ly (start_of ly as) (Dec n e), start_of ly as - Suc 0) stp) ires"
+sorry
+
+subsection{*Crsp of Goto*}
+lemma crsp_step_goto:
+  assumes layout: "ly = layout_of ap"
+  and crsp: "crsp ly (as, lm) (s, l, r) ires"
+  shows "\<exists>stp. crsp ly (abc_step_l (as, lm) (Some (Goto n)))
+  (steps (s, l, r) (ci ly (start_of ly as) (Goto n), 
+            start_of ly as - Suc 0) stp) ires"
+sorry
+
+
+lemma crsp_step_in:
+  assumes layout: "ly = layout_of ap"
+  and compile: "tp = tm_of ap"
+  and crsp: "crsp ly (as, lm) (s, l, r) ires"
+  and fetch: "abc_fetch as ap = Some ins"
+  shows "\<exists> stp. crsp ly (abc_step_l (as, lm) (Some ins))
+                      (steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp) ires"
+  using assms
+  apply(case_tac ins, simp_all)
+  apply(rule crsp_step_inc, simp_all)
+  apply(rule crsp_step_dec, simp_all)
+  apply(rule_tac crsp_step_goto, simp_all)
+  done
+
+lemma crsp_step:
+  assumes layout: "ly = layout_of ap"
+  and compile: "tp = tm_of ap"
+  and crsp: "crsp ly (as, lm) (s, l, r) ires"
+  and fetch: "abc_fetch as ap = Some ins"
+  shows "\<exists> stp. crsp ly (abc_step_l (as, lm) (Some ins))
+                      (steps (s, l, r) (tp, 0) stp) ires"
+proof -
+  have "\<exists> stp. crsp ly (abc_step_l (as, lm) (Some ins))
+                      (steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp) ires"
+    using assms
+    apply(erule_tac crsp_step_in, simp_all)
+    done
+  from this obtain stp where d: "crsp ly (abc_step_l (as, lm) (Some ins))
+                      (steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp) ires" ..
+  obtain s' l' r' where e:
+    "(steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp) = (s', l', r')"
+    apply(case_tac "(steps (s, l, r) (ci ly (start_of ly as) ins, start_of ly as - 1) stp)")
+    by blast
+  then have "steps (s, l, r) (tp, 0) stp = (s', l', r')"
+    using assms d
+    apply(rule_tac steps_eq_in)
+    apply(simp_all)
+    apply(case_tac "(abc_step_l (as, lm) (Some ins))", simp add: crsp.simps)
+    done    
+  thus " \<exists>stp. crsp ly (abc_step_l (as, lm) (Some ins)) (steps (s, l, r) (tp, 0) stp) ires"
+    using d e
+    apply(rule_tac x = stp in exI, simp)
+    done
+qed
+
+lemma crsp_steps:
+  assumes layout: "ly = layout_of ap"
+  and compile: "tp = tm_of ap"
+  and crsp: "crsp ly (as, lm) (s, l, r) ires"
+  shows "\<exists> stp. crsp ly (abc_steps_l (as, lm) ap n)
+                      (steps (s, l, r) (tp, 0) stp) ires"
+  using crsp
+  apply(induct n)
+  apply(rule_tac x = 0 in exI) 
+  apply(simp add: steps.simps abc_steps_l.simps, simp)
+  apply(case_tac "(abc_steps_l (as, lm) ap n)", auto)
+  apply(frule_tac abc_step_red, simp)
+  apply(case_tac "abc_fetch a ap", simp add: abc_step_l.simps, auto)
+  apply(case_tac "steps (s, l, r) (tp, 0) stp", simp)
+  using assms
+  apply(drule_tac s = ab and l = ba and r = c in crsp_step, auto)
+  apply(rule_tac x = "stp + stpa" in exI, simp add: steps_add)
+  done
+
+lemma tp_correct': 
+  assumes layout: "ly = layout_of ap"
+  and compile: "tp = tm_of ap"
+  and crsp: "crsp ly (0, lm) (Suc 0, l, r) ires"
+  and abc_halt: "abc_steps_l (0, lm) ap stp = (length ap, am)"
+  shows "\<exists> stp k. steps (Suc 0, l, r) (tp, 0) stp = (start_of ly (length ap), Bk # Bk # ires, <am> @ Bk\<up>k)"
+  using assms
+  apply(drule_tac n = stp in crsp_steps, auto)
+  apply(rule_tac x = stpa in exI)
+  apply(case_tac "steps (Suc 0, l, r) (tm_of ap, 0) stpa", simp add: crsp.simps)
+  done
+
+(***normalize the tp compiled from ap, and we can use Hoare_plus when composed with mopup machine*)
+definition tp_norm :: "abc_prog \<Rightarrow> instr list"
+  where
+  "tp_norm ap = tm_of ap @ [(Nop, 0), (Nop, 0)]"
+
+lemma tp_correct: 
+  assumes layout: "ly = layout_of ap"
+  and crsp: "crsp ly (0, lm) (Suc 0, l, r) ires"
+  and abc_halt: "abc_steps_l (0, lm) ap stp = (length ap, am)"
+  shows "\<exists> stp k. steps (Suc 0, l, r) (tp_norm ap, 0) stp = (0, Bk # Bk # ires, <am> @ Bk\<up>k)"
+ sorry
+
+(****mop_up***)
+fun mopup_a :: "nat \<Rightarrow> instr list"
+  where
+  "mopup_a 0 = []" |
+  "mopup_a (Suc n) = mopup_a n @ 
+       [(R, 2*n + 3), (W0, 2*n + 2), (R, 2*n + 1), (W1, 2*n + 2)]"
+
+definition mopup_b :: "instr list"
+  where
+  "mopup_b \<equiv> [(R, 2), (R, 1), (L, 5), (W0, 3), (R, 4), (W0, 3),
+            (R, 2), (W0, 3), (L, 5), (L, 6), (R, 0), (L, 6)]"
+
+fun mopup :: "nat \<Rightarrow> instr list"
+  where 
+  "mopup n = mopup_a n @ shift mopup_b (2*n)"
+(****)
+
+(*we can use Hoare_plus here*)
+lemma compile_correct_halt: 
+  assumes layout: "ly = layout_of ap"
+  and crsp: "crsp ly (0, lm) (Suc 0, l, r) ires"
+  and abc_halt: "abc_steps_l (0, lm) ap stp = (length ap, am)"
+  and rs_loc: "n < length am"
+  and rs: "rs = abc_lm_v am n"
+  shows "\<exists> stp i j. steps (Suc 0, l, r) (tp_norm ap |+| mopup n, 0) stp = (0, Bk\<up>i @ Bk # Bk # ires, Oc\<up>Suc rs @ Bk\<up>j)"
+sorry
+
+lemma compile_correct_unhalt: 
+  assumes layout: "ly = layout_of ap"
+  and crsp: "crsp ly (0, lm) (Suc 0, l, r) ires"
+  and abc_unhalt: "\<forall> stp. (\<lambda> (as, am). as < length ap) (abc_steps_l (0, lm) ap stp)"
+  shows "\<forall> stp.\<not> is_final (steps (Suc 0, l, r) (tp_norm ap |+| mopup n, 0) stp)"
+sorry
+
+end
+
diff -r df4c7bb6c79e -r 251e192339b7 thys/turing_basic.thy
--- a/thys/turing_basic.thy	Wed Jan 16 15:17:02 2013 +0000
+++ b/thys/turing_basic.thy	Thu Jan 17 11:51:00 2013 +0000
@@ -93,7 +93,6 @@
                     (\<forall>(a, s) \<in> set p. s \<le> length p div 2
                                              + off \<and> s \<ge> off))"
 
-
 (* FIXME: needed? *)
 lemma halt_lemma: 
   "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
@@ -102,6 +101,18 @@
 abbreviation exponent :: "'a \<Rightarrow> nat \<Rightarrow> 'a list" ("_ \<up> _" [100, 99] 100)
   where "x \<up> n == replicate n x"
 
+consts tape_of :: "'a \<Rightarrow> cell list" ("<_>" 100)
+
+fun tape_of_nat_list :: "nat list \<Rightarrow> cell list" 
+  where 
+  "tape_of_nat_list [] = []" |
+  "tape_of_nat_list [n] = Oc\<up>(Suc n)" |
+  "tape_of_nat_list (n#ns) = Oc\<up>(Suc n) @ Bk # (tape_of_nat_list ns)"
+
+defs (overloaded)
+  tape_of_nl_abv: "<am> \<equiv> tape_of_nat_list am"
+  tape_of_nat_abv : "<(n::nat)> \<equiv> Oc\<up>(Suc n)"
+
 definition tinres :: "cell list \<Rightarrow> cell list \<Rightarrow> bool"
   where
   "tinres xs ys = (\<exists>n. xs = ys @ Bk \<up> n \<or> ys = xs @ Bk \<up> n)"
@@ -598,8 +609,6 @@
       done
   qed
 qed
-    
-      
-       
+        
 end
 
diff -r df4c7bb6c79e -r 251e192339b7 thys/uncomputable.thy
--- a/thys/uncomputable.thy	Wed Jan 16 15:17:02 2013 +0000
+++ b/thys/uncomputable.thy	Thu Jan 17 11:51:00 2013 +0000
@@ -1071,13 +1071,6 @@
   and the final configuration is standard.
 *}
 
-
-fun tape_of_nat_list :: "nat list \<Rightarrow> cell list" ("< _ >" [0] 100)
-  where 
-  "tape_of_nat_list [] = []" |
-  "tape_of_nat_list [n] = Oc\<up>(Suc n)" |
-  "tape_of_nat_list (n#ns) = Oc\<up>(Suc n) @ Bk # (tape_of_nat_list ns)"
-
 definition haltP :: "tprog \<Rightarrow> nat list \<Rightarrow> bool"
   where
   "haltP t lm = (\<exists>n a b c. steps (Suc 0, [], <lm>) t n = (0, Bk\<up>a,  Oc\<up>b @ Bk\<up>c))"
@@ -1341,7 +1334,7 @@
         using Hoare_def nh_newcase[of ?tcontr "[code ?tcontr]" 1] h
         apply(auto)
         apply(rule_tac x = na in exI)
-        apply(simp add: replicate_Suc)
+        apply(simp add: replicate_Suc tape_of_nl_abv)
         done
     qed
   next
@@ -1364,8 +1357,9 @@
     apply(erule_tac x = n in allE)
     apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n")
     apply(simp, auto)
-    apply(erule_tac x = 2 in allE, erule_tac x = 0 in allE)
-    apply(simp add: numeral_2_eq_2 replicate_Suc)
+    apply(erule_tac x = nd in allE, erule_tac x = 2 in allE)
+    apply(simp add: numeral_2_eq_2 replicate_Suc tape_of_nl_abv)
+    apply(erule_tac x = 0 in allE, simp)
     done
 qed
   
@@ -1416,7 +1410,7 @@
         using Hoare_def h_newcase[of ?tcontr "[code ?tcontr]" 1] h
         apply(auto)
         apply(rule_tac x = na in exI)
-        apply(simp add: replicate_Suc)
+        apply(simp add: replicate_Suc tape_of_nl_abv)
         done
     qed
   next
@@ -1434,7 +1428,8 @@
     using h
     apply(auto simp: haltP_def Hoare_unhalt_def)
     apply(erule_tac x = n in allE)
-    apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n", simp)
+    apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n")
+    apply(simp add: tape_of_nl_abv)
     done
 qed