diff -r 32c5e8d1f6ff -r 4524c5edcafb thys/UF_Rec.thy --- a/thys/UF_Rec.thy Tue May 21 13:50:15 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,589 +0,0 @@ -theory UF_Rec -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 \ 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 \ nat" where - "cell_num Bk = 0" -| "cell_num Oc = 1" - -fun code_tp :: "cell list \ 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 \ nat" where - "code_instr i = penc (action_num (fst i)) (snd i)" - -fun Code_instr :: "instr \ instr \ nat" where - "Code_instr i = penc (code_instr (fst i)) (code_instr (snd i))" - -fun code_tprog :: "tprog \ 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 \ (code_tprog tp) ! n = Code_instr (tp ! n)" -by (induct tp arbitrary: n) (simp_all add: nth_Cons') - -fun Code_tprog :: "tprog \ nat" - where - "Code_tprog tm = lenc (code_tprog tm)" - -section {* Universal Function in HOL *} - - -text {* Scanning and writing the right tape *} - -fun Scan where - "Scan r = ldec r 0" - -fun Write where - "Write n r = penc n (pdec2 r)" - -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 \ nat \ nat \ nat" - where - "Newleft p r a = (if a = 0 \ 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 \ nat \ nat \ nat" - where - "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 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 \ nat \ nat" where - "actn n 0 = pdec1 (pdec1 n)" -| "actn n _ = pdec1 (pdec2 n)" - -fun Actn :: "nat \ nat \ nat \ nat" - where - "Actn m q r = (if q \ 0 \ within m q then (actn (ldec m (q - 1)) r) else 4)" - -fun newstat :: "nat \ nat \ nat" where - "newstat n 0 = pdec2 (pdec1 n)" -| "newstat n _ = pdec2 (pdec2 n)" - -fun Newstat :: "nat \ nat \ nat \ nat" - where - "Newstat m q r = (if q \ 0 then (newstat (ldec m (q - 1)) r) else 0)" - -fun Conf :: "nat \ (nat \ nat) \ nat" - where - "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 = ldec c 1" - -fun Right where - "Right c = ldec c 2" - -fun Newconf :: "nat \ nat \ nat" - where - "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 "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 Steps :: "nat \ nat \ nat \ nat" - where - "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 - by @{text "c"} is not a stardard final configuration. *} - -fun Nstd :: "nat \ bool" - where - "Nstd c = (Stat c \ 0)" - --- "tape conditions are missing" - -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 \ nat \ nat \ bool" - where - "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"}. -*} - -fun Halt :: "nat \ nat \ nat" - where - "Halt m r = (LEAST t. \ Nostop t m r)" - -(* -fun UF :: "nat \ nat \ nat" - where - "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: - "\tm_wf tp\ \ 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: - "\tm_wf tp; st \ length tp\ \ 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 \ 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 \ 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 *} - -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 \ nat \ 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 \ 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) -done - -lemma bl2nat_simps1 [simp]: - shows "bl2nat (Bk \ y) n = 0" -by (induct y) (auto) - -lemma bl2nat_simps2 [simp]: - shows "bl2nat (Oc \ y) 0 = 2 ^ y - 1" -apply(induct y) -apply(auto) -apply(case_tac "(2::nat)^ y") -apply(auto) -done - -fun Trpl_code :: "config \ nat" - where - "Trpl_code (st, l, r) = Trpl (bl2wc l) st (bl2wc r)" - - - -fun block_map :: "cell \ nat" - where - "block_map Bk = 0" -| "block_map Oc = 1" - -fun Goedel_code' :: "nat list \ nat \ nat" - where - "Goedel_code' [] n = 1" -| "Goedel_code' (x # xs) n = (Pi n) ^ x * Goedel_code' xs (Suc n) " - -fun Goedel_code :: "nat list \ nat" - where - "Goedel_code xs = 2 ^ (length xs) * (Goedel_code' xs 1)" - - - -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 \ nat \ 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 \ nat \ 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 \ nat \ recf list" - where - "rec_map rf vl = map (\i. CN rf [Id vl i]) [0.. 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 = \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 \ rec_eval (rec_listsum2 vl n) xs = Listsum2 xs n" -by (induct n) (simp_all) - -lemma strt'_lemma [simp]: - "length xs = vl \ rec_eval (rec_strt' vl n) xs = Strt' xs n" -by (induct n) (simp_all add: Let_def) - -lemma map_suc: - "map (\x. Suc (xs ! x)) [0.. (\x. xs ! x) = (\x. Suc (xs ! x))" by (simp add: comp_def) - then have "map (\x. Suc (xs ! x)) [0.. (\x. xs ! x)) [0..x. xs ! x) [0..x. Suc (xs ! x)) [0.. 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 "(\ (s, l, r). s \ 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) -oops - -lemma rec_steps: - assumes "tm_wf0 tp" - shows "Trpl_code (steps0 (1, Bk \ l, ) tp stp) = Conf stp (Code tp) (bl2wc ())" -apply(induct stp) -apply(simp) -apply(simp) -oops - - -lemma F_correct: - assumes tm: "steps0 (1, Bk \ l, ) tp stp = (0, Bk \ m, Oc \ rs @ Bk \ n)" - and wf: "tm_wf0 tp" "0 < rs" - shows "rec_eval rec_uf [Code tp, bl2wc ()] = (rs - Suc 0)" -proof - - from least_steps[OF tm] - obtain stp_least where - before: "\stp' < stp_least. \ is_final (steps0 (1, Bk \ l, ) tp stp')" and - after: "\stp' \ stp_least. is_final (steps0 (1, Bk \ l, ) tp stp')" by blast - have "Halt (Code tp) (bl2wc ()) = stp_least" sorry - show ?thesis - apply(simp only: uf_lemma) - apply(simp only: UF.simps) - apply(simp only: Halt.simps) - oops - - -end -