--- 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 *}