--- 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 \<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 {* 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 \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
- where
- "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 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 \<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 \<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 (newstat (ldec m (q - 1)) r) else 0)"
-
-fun Conf :: "nat \<times> (nat \<times> nat) \<Rightarrow> 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 \<Rightarrow> nat \<Rightarrow> 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 \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 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 \<Rightarrow> bool"
- where
- "Nstd c = (Stat c \<noteq> 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 \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 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 \<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 = (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 *}
-
-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)
-done
-
-lemma 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)
-done
-
-fun Trpl_code :: "config \<Rightarrow> nat"
- where
- "Trpl_code (st, l, r) = Trpl (bl2wc l) st (bl2wc r)"
-
-
-
-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)"
-
-
-
-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" .
-qed
-
-lemma 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)
-oops
-
-lemma 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)
-oops
-
-
-lemma 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)
- oops
-
-
-end
-