# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1369140615 -3600
# Node ID 32c5e8d1f6ffea701a223706e9c8b498be62d4c7
# Parent  df6e8cb229951ab531584b926eb4025fcae1cde6
added more about UF

diff -r df6e8cb22995 -r 32c5e8d1f6ff thys/UF_Rec.thy
--- a/thys/UF_Rec.thy	Tue May 21 13:49:31 2013 +0100
+++ b/thys/UF_Rec.thy	Tue May 21 13:50:15 2013 +0100
@@ -1,111 +1,145 @@
 theory UF_Rec
-imports Recs Turing_Hoare
+imports Recs Turing2
 begin
 
+section {* Coding of Turing Machines and tapes*}
 
+text {*
+  The purpose of this section is to construct the coding function of Turing 
+  Machine, which is going to be named @{text "code"}. *}
+
+text {* Encoding of actions as numbers *}
+
+fun action_num :: "action \<Rightarrow> nat"
+  where
+  "action_num W0 = 0"
+| "action_num W1 = 1"
+| "action_num L  = 2"
+| "action_num R  = 3"
+| "action_num Nop = 4"
+
+fun cell_num :: "cell \<Rightarrow> nat" where
+  "cell_num Bk = 0"
+| "cell_num Oc = 1"
+
+fun code_tp :: "cell list \<Rightarrow> nat list"
+  where
+  "code_tp [] = []"
+| "code_tp (c # tp) = (cell_num c) # code_tp tp"
+
+fun Code_tp where
+  "Code_tp tp = lenc (code_tp tp)"
+
+fun Code_conf where
+  "Code_conf (s, l, r) = (s, Code_tp l, Code_tp r)"
+
+fun code_instr :: "instr \<Rightarrow> nat" where
+  "code_instr i = penc (action_num (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 code_tprog :: "tprog \<Rightarrow> nat list"
+  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)"
 
 section {* Universal Function in HOL *}
 
-text {*
-  @{text "Entry sr i"} returns the @{text "i"}-th entry of a list of natural 
-  numbers encoded by number @{text "sr"} using Godel's coding.
-  *}
-fun Entry where
-  "Entry sr i = Lo sr (Pi (Suc i))"
+
+text {* Scanning and writing the right tape *}
 
-fun Listsum2 :: "nat list \<Rightarrow> nat \<Rightarrow> nat"
-  where
-  "Listsum2 xs 0 = 0"
-| "Listsum2 xs (Suc n) = Listsum2 xs n + xs ! n"
-
-text {*
-  @{text "Strt"} corresponds to the @{text "strt"} function on page 90 of the 
-  B book, but this definition generalises the original one in order to deal 
-  with multiple input arguments. *}
+fun Scan where
+  "Scan r = ldec r 0"
 
-fun Strt' :: "nat list \<Rightarrow> nat \<Rightarrow> nat"
-  where
-  "Strt' xs 0 = 0"
-| "Strt' xs (Suc n) = (let dbound = Listsum2 xs n + n 
-                       in Strt' xs n + (2 ^ (xs ! n + dbound) - 2 ^ dbound))"
+fun Write where
+  "Write n r = penc n (pdec2 r)"
 
-fun Strt :: "nat list \<Rightarrow> nat"
-  where
-  "Strt xs = (let ys = map Suc xs in Strt' ys (length ys))"
-
-text {* The @{text "Scan"} function on page 90 of B book. *}
-fun Scan :: "nat \<Rightarrow> nat"
-  where
-  "Scan r = r mod 2"
-
-text {* The @{text Newleft} and @{text Newright} functions on page 91 of B book. *}
+text {* 
+  The @{text Newleft} and @{text Newright} functions on page 91 of B book. 
+  They calculate the new left and right tape (@{text p} and @{text r}) according 
+  to an action @{text a}.
+*}
 
 fun Newleft :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
   where
-  "Newleft p r a = (if a = 0 \<or> a = 1 then p 
-                    else if a = 2 then p div 2
-                    else if a = 3 then 2 * p + r mod 2
+  "Newleft p r a = (if a = 0 \<or> a = 1 then p else 
+                    if a = 2 then pdec2 p else 
+                    if a = 3 then penc (pdec1 r) p
                     else p)"
 
 fun Newright :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
   where
-  "Newright p r a  = (if a = 0 then r - Scan r
-                      else if a = 1 then r + 1 - Scan r
-                      else if a = 2 then 2 * r + p mod 2
-                      else if a = 3 then r div 2
+  "Newright p r a  = (if a = 0 then Write 0 r
+                      else if a = 1 then Write 1 r
+                      else if a = 2 then penc (pdec1 p) r
+                      else if a = 3 then pdec2 r
                       else r)"
 
 text {*
   The @{text "Actn"} function given on page 92 of B book, which is used to 
   fetch Turing Machine intructions. In @{text "Actn m q r"}, @{text "m"} is 
-  the Goedel coding of a Turing Machine, @{text "q"} is the current state of 
-  Turing Machine, @{text "r"} is the right number of Turing Machine tape. *}
+  the code of the Turing Machine, @{text "q"} is the current state of 
+  Turing Machine, and @{text "r"} is the scanned cell of is the right tape. 
+*}
+
+fun actn :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+  "actn n 0 = pdec1 (pdec1 n)"
+| "actn n _ = pdec1 (pdec2 n)"
 
 fun Actn :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
   where
-  "Actn m q r = (if q \<noteq> 0 then Entry m (4 * (q - 1) + 2 * Scan r) else 4)"
+  "Actn m q r = (if q \<noteq> 0 \<and> within m q then (actn (ldec m (q - 1)) r) else 4)"
+
+fun newstat :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+  "newstat n 0 = pdec2 (pdec1 n)"
+| "newstat n _ = pdec2 (pdec2 n)"
 
 fun Newstat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
   where
-  "Newstat m q r = (if q \<noteq> 0 then Entry m (4 * (q - 1) + 2 * Scan r + 1) else 0)"
+  "Newstat m q r = (if q \<noteq> 0 then (newstat (ldec m (q - 1)) r) else 0)"
 
-fun Trpl :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+fun Conf :: "nat \<times> (nat \<times> nat) \<Rightarrow> nat"
   where
-  "Trpl p q r = list_encode [p, q, r]"
+  "Conf (q, (l, r)) = lenc [q, l, r]"
+
+fun Stat where
+  (*"Stat c = (if c = 0 then 0 else ldec c 0)"*)
+  "Stat c = ldec c 0"
 
 fun Left where
-  "Left c = list_decode c ! 0"
+  "Left c = ldec c 1"
 
 fun Right where
-  "Right c = list_decode c ! 1"
-
-fun Stat where
-  "Stat c = list_decode c ! 2"
-
-lemma mod_dvd_simp: 
-  "(x mod y = (0::nat)) = (y dvd x)"
-by(auto simp add: dvd_def)
-
-
-fun Inpt :: "nat \<Rightarrow> nat list \<Rightarrow> nat"
-  where
-  "Inpt m xs = Trpl 0 1 (Strt xs)"
+  "Right c = ldec c 2"
 
 fun Newconf :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   where
-  "Newconf m c = Trpl (Newleft (Left c) (Right c) (Actn m (Stat c) (Right c)))
-                      (Newstat m (Stat c) (Right c)) 
-                      (Newright (Left c) (Right c) (Actn m (Stat c) (Right c)))"
+  "Newconf c m = Conf (Newstat m (Stat c) (Scan (Right c)), 
+                       (Newleft (Left c) (Right c) (Actn m (Stat c) (Scan (Right c))),
+                        Newright (Left c) (Right c) (Actn m (Stat c) (Scan (Right c)))))"
 
 text {*
-  @{text "Conf k m r"} computes the TM configuration after @{text "k"} steps of execution
+  @{text "Step k m r"} computes the TM configuration after @{text "k"} steps of execution
   of TM coded as @{text "m"} starting from the initial configuration where the left 
   number equals @{text "0"}, right number equals @{text "r"}. *}
 
-fun Conf :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+fun Steps :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
   where
-  "Conf 0 m r  = Trpl 0 1 r"
-| "Conf (Suc k) m r = Newconf m (Conf k m r)"
+  "Steps cf p 0  = cf"
+| "Steps cf p (Suc n) = Steps (Newconf cf p) p n"
 
 text {*
   @{text "Nstd c"} returns true if the configuration coded 
@@ -113,11 +147,9 @@
 
 fun Nstd :: "nat \<Rightarrow> bool"
   where
-  "Nstd c = (Stat c \<noteq> 0 \<or> 
-             Left c \<noteq> 0 \<or> 
-             Right c \<noteq> 2 ^ (Lg (Suc (Right c)) 2) - 1 \<or> 
-             Right c = 0)"
+  "Nstd c = (Stat c \<noteq> 0)"
 
+-- "tape conditions are missing"
 
 text{* 
   @{text "Nostop t m r"} means that afer @{text "t"} steps of 
@@ -126,24 +158,121 @@
 
 fun Nostop :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
   where
-  "Nostop t m r = Nstd (Conf t m r)"
-
-fun Value where
-  "Value x = (Lg (Suc x) 2) - 1"
+  "Nostop m l r = Nstd (Conf (m, (l, r)))"
 
 text{*
-  @{text "rec_halt"} is the recursive function calculating the steps a TM needs to execute before
-  to reach a stardard final configuration. This recursive function is the only one
-  using @{text "Mn"} combinator. So it is the only non-primitive recursive function 
-  needs to be used in the construction of the universal function @{text "rec_uf"}. *}
+  @{text "rec_halt"} is the recursive function calculating the steps a TM needs to 
+  execute before to reach a stardard final configuration. This recursive function is 
+  the only one using @{text "Mn"} combinator. So it is the only non-primitive recursive 
+  function needs to be used in the construction of the universal function @{text "rec_uf"}. 
+*}
 
 fun Halt :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   where
   "Halt m r = (LEAST t. \<not> Nostop t m r)"
 
+(*
 fun UF :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   where
-  "UF c m = Value (Right (Conf (Halt c m) c m))"
+  "UF c m = (Right (Conf (Halt c m) c m))"
+*)
+
+text {* reading the value is missing *}
+
+section {* The UF can simulate Turing machines *}
+
+lemma Update_left_simulate:
+  shows "Newleft (Code_tp l) (Code_tp r) (action_num a) = Code_tp (fst (update a (l, r)))"
+apply(induct a)
+apply(simp_all)
+apply(case_tac l)
+apply(simp_all)
+apply(case_tac r)
+apply(simp_all)
+done
+
+lemma Update_right_simulate:
+  shows "Newright (Code_tp l) (Code_tp r) (action_num a) = Code_tp (snd (update a (l, r)))"
+apply(induct a)
+apply(simp_all)
+apply(case_tac r)
+apply(simp_all)
+apply(case_tac r)
+apply(simp_all)
+apply(case_tac l)
+apply(simp_all)
+apply(case_tac r)
+apply(simp_all)
+done
+
+lemma Fetch_state_simulate:
+  "\<lbrakk>tm_wf tp\<rbrakk> \<Longrightarrow> Newstat (Code_tprog tp) st (cell_num c) = snd (fetch tp st c)"
+apply(induct tp st c rule: fetch.induct)
+apply(simp_all add: list_encode_inverse split: cell.split)
+done
+
+lemma Fetch_action_simulate:
+  "\<lbrakk>tm_wf tp; st \<le> length tp\<rbrakk> \<Longrightarrow> Actn (Code_tprog tp) st (cell_num c) = action_num (fst (fetch tp st c))"
+apply(induct tp st c rule: fetch.induct)
+apply(simp_all add: list_encode_inverse split: cell.split)
+done
+
+lemma Scan_simulate:
+  "Scan (Code_tp tp) = cell_num (read tp)"
+apply(case_tac tp)
+apply(simp_all)
+done
+
+lemma misc:
+  "2 < (3::nat)"
+  "1 < (3::nat)"
+  "0 < (3::nat)" 
+  "length [x] = 1"
+  "length [x, y] = 2"
+  "length [x, y , z] = 3"
+  "[x, y, z] ! 0 = x"
+  "[x, y, z] ! 1 = y"
+  "[x, y, z] ! 2 = z"
+apply(simp_all)
+done
+
+lemma New_conf_simulate:
+  assumes "tm_wf tp" "st \<le> length tp"
+  shows "Newconf (Conf (Code_conf (st, l, r))) (Code_tprog tp) = Conf (Code_conf (step (st, l, r) tp))"
+apply(subst step.simps) 
+apply(simp only: Let_def)
+apply(subst Newconf.simps)
+apply(simp only: Conf.simps Code_conf.simps Right.simps Left.simps)
+apply(simp only: list_encode_inverse)
+apply(simp only: misc if_True Code_tp.simps)
+apply(simp only: prod_case_beta) 
+apply(subst Fetch_state_simulate[OF assms, symmetric])
+apply(simp only: Stat.simps)
+apply(simp only: list_encode_inverse)
+apply(simp only: misc if_True)
+apply(simp only: Scan_simulate[simplified Code_tp.simps])
+apply(simp only: Fetch_action_simulate[OF assms])
+apply(simp only: Update_left_simulate[simplified Code_tp.simps])
+apply(simp only: Update_right_simulate[simplified Code_tp.simps])
+apply(case_tac "update (fst (fetch tp st (read r))) (l, r)")
+apply(simp only: Code_conf.simps)
+apply(simp only: Conf.simps)
+apply(simp)
+done
+
+lemma Step_simulate:
+  assumes "tm_wf tp" "fst cf \<le> length tp"
+  shows "Steps (Conf (Code_conf cf)) (Code_tprog tp) n = Conf (Code_conf (steps cf tp n))"
+apply(induct n arbitrary: cf) 
+apply(simp)
+apply(simp only: Steps.simps steps.simps)
+apply(case_tac cf)
+apply(simp only: )
+apply(subst New_conf_simulate)
+apply(rule assms)
+defer
+apply(drule_tac x="step (a, b, c) tp" in meta_spec)
+apply(simp)
 
 
 section {* Coding of Turing Machines *}
@@ -186,21 +315,7 @@
   where
   "Trpl_code (st, l, r) = Trpl (bl2wc l) st (bl2wc r)"
 
-fun action_map :: "action \<Rightarrow> nat"
-  where
-  "action_map W0 = 0"
-| "action_map W1 = 1"
-| "action_map L = 2"
-| "action_map R = 3"
-| "action_map Nop = 4"
 
-fun action_map_iff :: "nat \<Rightarrow> action"
-  where
-  "action_map_iff (0::nat) = W0"
-| "action_map_iff (Suc 0) = W1"
-| "action_map_iff (Suc (Suc 0)) = L"
-| "action_map_iff (Suc (Suc (Suc 0))) = R"
-| "action_map_iff n = Nop"
 
 fun block_map :: "cell \<Rightarrow> nat"
   where
@@ -216,15 +331,6 @@
   where
   "Goedel_code xs = 2 ^ (length xs) * (Goedel_code' xs 1)"
 
-fun modify_tprog :: "instr list \<Rightarrow> nat list"
-  where
-  "modify_tprog [] =  []"
-| "modify_tprog ((a, s) # nl) = action_map a # s # modify_tprog nl"
-
-text {* @{text "Code tp"} gives the Goedel coding of TM program @{text "tp"}. *}
-fun Code :: "instr list \<Rightarrow> nat"
-  where 
-  "Code tp = Goedel_code (modify_tprog tp)"
 
 
 section {* Universal Function as Recursive Functions *}