theory UF_Recimports Recs Turing_Hoarebeginsection {* 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))"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 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 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. *}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 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 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. *}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)"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)"fun Trpl :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where "Trpl p q r = list_encode [p, q, r]"fun Left where "Left c = list_decode c ! 0"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)"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)))"text {* @{text "Conf 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" where "Conf 0 m r = Trpl 0 1 r"| "Conf (Suc k) m r = Newconf m (Conf k m r)"text {* @{text "Nstd c"} returns true if the configuration coded by @{text "c"} is not a stardard final configuration. *}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)"text{* @{text "Nostop t m r"} means that afer @{text "t"} steps of execution the TM coded by @{text "m"} is not at a stardard final configuration. *}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"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"}. *}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))"section {* Coding of Turing Machines *}text {* The purpose of this section is to construct the coding function of Turing Machine, which is going to be named @{text "code"}. *}fun bl2nat :: "cell list \<Rightarrow> nat \<Rightarrow> nat" where "bl2nat [] n = 0"| "bl2nat (Bk # bl) n = bl2nat bl (Suc n)"| "bl2nat (Oc # bl) n = 2 ^ n + bl2nat bl (Suc n)"fun bl2wc :: "cell list \<Rightarrow> nat" where "bl2wc xs = bl2nat xs 0"lemma bl2nat_double [simp]: "bl2nat xs (Suc n) = 2 * bl2nat xs n"apply(induct xs arbitrary: n)apply(auto)apply(case_tac a)apply(auto)donelemma bl2nat_simps1 [simp]: shows "bl2nat (Bk \<up> y) n = 0"by (induct y) (auto)lemma bl2nat_simps2 [simp]: shows "bl2nat (Oc \<up> y) 0 = 2 ^ y - 1"apply(induct y)apply(auto)apply(case_tac "(2::nat)^ y")apply(auto)donefun Trpl_code :: "config \<Rightarrow> nat" 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 "block_map Bk = 0"| "block_map Oc = 1"fun Goedel_code' :: "nat list \<Rightarrow> nat \<Rightarrow> nat" where "Goedel_code' [] n = 1"| "Goedel_code' (x # xs) n = (Pi n) ^ x * Goedel_code' xs (Suc n) "fun Goedel_code :: "nat list \<Rightarrow> nat" 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 *}definition "rec_entry = CN rec_lo [Id 2 0, CN rec_pi [CN S [Id 2 1]]]"fun rec_listsum2 :: "nat \<Rightarrow> nat \<Rightarrow> recf" where "rec_listsum2 vl 0 = CN Z [Id vl 0]"| "rec_listsum2 vl (Suc n) = CN rec_add [rec_listsum2 vl n, Id vl n]"fun rec_strt' :: "nat \<Rightarrow> nat \<Rightarrow> recf" where "rec_strt' xs 0 = Z"| "rec_strt' xs (Suc n) = (let dbound = CN rec_add [rec_listsum2 xs n, constn n] in let t1 = CN rec_power [constn 2, dbound] in let t2 = CN rec_power [constn 2, CN rec_add [Id xs n, dbound]] in CN rec_add [rec_strt' xs n, CN rec_minus [t2, t1]])"fun rec_map :: "recf \<Rightarrow> nat \<Rightarrow> recf list" where "rec_map rf vl = map (\<lambda>i. CN rf [Id vl i]) [0..<vl]"fun rec_strt :: "nat \<Rightarrow> recf" where "rec_strt xs = CN (rec_strt' xs xs) (rec_map S xs)"definition "rec_scan = CN rec_mod [Id 1 0, constn 2]"definition "rec_newleft = (let cond1 = CN rec_disj [CN rec_eq [Id 3 2, Z], CN rec_eq [Id 3 2, constn 1]] in let cond2 = CN rec_eq [Id 3 2, constn 2] in let cond3 = CN rec_eq [Id 3 2, constn 3] in let case3 = CN rec_add [CN rec_mult [constn 2, Id 3 0], CN rec_mod [Id 3 1, constn 2]] in CN rec_if [cond1, Id 3 0, CN rec_if [cond2, CN rec_quo [Id 3 0, constn 2], CN rec_if [cond3, case3, Id 3 0]]])"definition "rec_newright = (let condn = \<lambda>n. CN rec_eq [Id 3 2, constn n] in let case0 = CN rec_minus [Id 3 1, CN rec_scan [Id 3 1]] in let case1 = CN rec_minus [CN rec_add [Id 3 1, constn 1], CN rec_scan [Id 3 1]] in let case2 = CN rec_add [CN rec_mult [constn 2, Id 3 1], CN rec_mod [Id 3 0, constn 2]] in let case3 = CN rec_quo [Id 2 1, constn 2] in CN rec_if [condn 0, case0, CN rec_if [condn 1, case1, CN rec_if [condn 2, case2, CN rec_if [condn 3, case3, Id 3 1]]]])"definition "rec_actn = (let add1 = CN rec_mult [constn 4, CN rec_pred [Id 3 1]] in let add2 = CN rec_mult [constn 2, CN rec_scan [Id 3 2]] in let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]] in CN rec_if [Id 3 1, entry, constn 4])"definition rec_newstat :: "recf" where "rec_newstat = (let add1 = CN rec_mult [constn 4, CN rec_pred [Id 3 1]] in let add2 = CN S [CN rec_mult [constn 2, CN rec_scan [Id 3 2]]] in let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]] in CN rec_if [Id 3 1, entry, Z])"definition "rec_trpl = CN rec_penc [CN rec_penc [Id 3 0, Id 3 1], Id 3 2]"definition "rec_left = rec_pdec1"definition "rec_right = CN rec_pdec2 [rec_pdec1]"definition "rec_stat = CN rec_pdec2 [rec_pdec2]"definition "rec_newconf = (let act = CN rec_actn [Id 2 0, CN rec_stat [Id 2 1], CN rec_right [Id 2 1]] in let left = CN rec_left [Id 2 1] in let right = CN rec_right [Id 2 1] in let stat = CN rec_stat [Id 2 1] in let one = CN rec_newleft [left, right, act] in let two = CN rec_newstat [Id 2 0, stat, right] in let three = CN rec_newright [left, right, act] in CN rec_trpl [one, two, three])" definition "rec_conf = PR (CN rec_trpl [constn 0, constn 1, Id 2 1]) (CN rec_newconf [Id 4 2 , Id 4 1])"definition "rec_nstd = (let disj1 = CN rec_noteq [rec_stat, constn 0] in let disj2 = CN rec_noteq [rec_left, constn 0] in let rhs = CN rec_pred [CN rec_power [constn 2, CN rec_lg [CN S [rec_right], constn 2]]] in let disj3 = CN rec_noteq [rec_right, rhs] in let disj4 = CN rec_eq [rec_right, constn 0] in CN rec_disj [CN rec_disj [CN rec_disj [disj1, disj2], disj3], disj4])"definition "rec_nostop = CN rec_nstd [rec_conf]"definition "rec_value = CN rec_pred [CN rec_lg [S, constn 2]]"definition "rec_halt = MN rec_nostop" definition "rec_uf = CN rec_value [CN rec_right [CN rec_conf [rec_halt, Id 2 0, Id 2 1]]]"section {* Correctness Proofs for Recursive Functions *}lemma entry_lemma [simp]: "rec_eval rec_entry [sr, i] = Entry sr i"by(simp add: rec_entry_def)lemma listsum2_lemma [simp]: "length xs = vl \<Longrightarrow> rec_eval (rec_listsum2 vl n) xs = Listsum2 xs n"by (induct n) (simp_all)lemma strt'_lemma [simp]: "length xs = vl \<Longrightarrow> rec_eval (rec_strt' vl n) xs = Strt' xs n"by (induct n) (simp_all add: Let_def)lemma map_suc: "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map Suc xs"proof - have "Suc \<circ> (\<lambda>x. xs ! x) = (\<lambda>x. Suc (xs ! x))" by (simp add: comp_def) then have "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map (Suc \<circ> (\<lambda>x. xs ! x)) [0..<length xs]" by simp also have "... = map Suc (map (\<lambda>x. xs ! x) [0..<length xs])" by simp also have "... = map Suc xs" by (simp add: map_nth) finally show "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map Suc xs" .qedlemma strt_lemma [simp]: "length xs = vl \<Longrightarrow> rec_eval (rec_strt vl) xs = Strt xs"by (simp add: comp_def map_suc[symmetric])lemma scan_lemma [simp]: "rec_eval rec_scan [r] = r mod 2"by(simp add: rec_scan_def)lemma newleft_lemma [simp]: "rec_eval rec_newleft [p, r, a] = Newleft p r a"by (simp add: rec_newleft_def Let_def)lemma newright_lemma [simp]: "rec_eval rec_newright [p, r, a] = Newright p r a"by (simp add: rec_newright_def Let_def)lemma actn_lemma [simp]: "rec_eval rec_actn [m, q, r] = Actn m q r"by (simp add: rec_actn_def)lemma newstat_lemma [simp]: "rec_eval rec_newstat [m, q, r] = Newstat m q r"by (simp add: rec_newstat_def)lemma trpl_lemma [simp]: "rec_eval rec_trpl [p, q, r] = Trpl p q r"apply(simp)apply (simp add: rec_trpl_def)lemma left_lemma [simp]: "rec_eval rec_left [c] = Left c" by(simp add: rec_left_def)lemma right_lemma [simp]: "rec_eval rec_right [c] = Right c" by(simp add: rec_right_def)lemma stat_lemma [simp]: "rec_eval rec_stat [c] = Stat c" by(simp add: rec_stat_def)lemma newconf_lemma [simp]: "rec_eval rec_newconf [m, c] = Newconf m c"by (simp add: rec_newconf_def Let_def)lemma conf_lemma [simp]: "rec_eval rec_conf [k, m, r] = Conf k m r"by(induct k) (simp_all add: rec_conf_def)lemma nstd_lemma [simp]: "rec_eval rec_nstd [c] = (if Nstd c then 1 else 0)"by(simp add: rec_nstd_def)lemma nostop_lemma [simp]: "rec_eval rec_nostop [t, m, r] = (if Nostop t m r then 1 else 0)" by (simp add: rec_nostop_def)lemma value_lemma [simp]: "rec_eval rec_value [x] = Value x"by (simp add: rec_value_def)lemma halt_lemma [simp]: "rec_eval rec_halt [m, r] = Halt m r"by (simp add: rec_halt_def)lemma uf_lemma [simp]: "rec_eval rec_uf [m, r] = UF m r"by (simp add: rec_uf_def)subsection {* Relating interperter functions to the execution of TMs *}lemma rec_step: assumes "(\<lambda> (s, l, r). s \<le> length tp div 2) c" shows "Trpl_code (step0 c tp) = Newconf (Code tp) (Trpl_code c)"apply(cases c)apply(simp only: Trpl_code.simps)apply(simp only: Let_def step.simps)apply(case_tac "fetch tp (a - 0) (read ca)")apply(simp only: prod.cases)apply(case_tac "update aa (b, ca)")apply(simp only: prod.cases)apply(simp only: Trpl_code.simps)apply(simp only: Newconf.simps)apply(simp only: Left.simps)oopslemma rec_steps: assumes "tm_wf0 tp" shows "Trpl_code (steps0 (1, Bk \<up> l, <lm>) tp stp) = Conf stp (Code tp) (bl2wc (<lm>))"apply(induct stp)apply(simp)apply(simp)oopslemma F_correct: assumes tm: "steps0 (1, Bk \<up> l, <lm>) tp stp = (0, Bk \<up> m, Oc \<up> rs @ Bk \<up> n)" and wf: "tm_wf0 tp" "0 < rs" shows "rec_eval rec_uf [Code tp, bl2wc (<lm>)] = (rs - Suc 0)"proof - from least_steps[OF tm] obtain stp_least where before: "\<forall>stp' < stp_least. \<not> is_final (steps0 (1, Bk \<up> l, <lm>) tp stp')" and after: "\<forall>stp' \<ge> stp_least. is_final (steps0 (1, Bk \<up> l, <lm>) tp stp')" by blast have "Halt (Code tp) (bl2wc (<lm>)) = stp_least" sorry show ?thesis apply(simp only: uf_lemma) apply(simp only: UF.simps) apply(simp only: Halt.simps) oopsend