diff -r 32c5e8d1f6ff -r 4524c5edcafb thys2/UF_Rec.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/UF_Rec.thy	Wed May 22 13:50:20 2013 +0100
@@ -0,0 +1,574 @@
+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 {* Reading and writing the encoded tape *}
+
+fun Read where
+  "Read tp = ldec tp 0"
+
+fun Write where
+  "Write n tp = penc (Suc n) (pdec2 tp)"
+
+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 l r a = (if a = 0 then l else 
+                    if a = 1 then l else 
+                    if a = 2 then pdec2 l else 
+                    if a = 3 then penc (Suc (Read r)) l
+                    else l)"
+
+fun Newright :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "Newright l r a  = (if a = 0 then Write 0 r
+                      else if a = 1 then Write 1 r
+                      else if a = 2 then penc (Suc (Read l)) 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 - 1) then (actn (ldec m (q - 1)) r) else 4)"
+
+fun newstate :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+  "newstate n 0 = pdec2 (pdec1 n)"
+| "newstate n _ = pdec2 (pdec2 n)"
+
+fun Newstate :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "Newstate m q r = (if q \<noteq> 0 then (newstate (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 State where
+  "State cf = ldec cf 0"
+
+fun Left where
+  "Left cf = ldec cf 1"
+
+fun Right where
+  "Right cf = ldec cf 2"
+
+fun Step :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "Step cf m = Conf (Newstate m (State cf) (Read (Right cf)), 
+                    (Newleft (Left cf) (Right cf) (Actn m (State cf) (Read (Right cf))),
+                     Newright (Left cf) (Right cf) (Actn m (State cf) (Read (Right cf)))))"
+
+text {*
+  @{text "Steps cf m k"} computes the TM configuration after @{text "k"} steps of execution
+  of TM coded as @{text "m"}. 
+*}
+
+fun Steps :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "Steps cf p 0  = cf"
+| "Steps cf p (Suc n) = Steps (Step cf p) p n"
+
+text {*
+  Decoding tapes into binary or stroke numbers.
+*}
+
+definition Binnum :: "nat \<Rightarrow> nat"
+  where
+  "Binnum z \<equiv> (\<Sum>i < enclen z. ldec z i * 2 ^ i)"
+
+definition Stknum :: "nat \<Rightarrow> nat"
+  where
+  "Stknum z \<equiv> (\<Sum>i < enclen z. ldec z i) - 1"
+
+lemma Binnum_simulate1:
+  "(Binnum z = 0) \<longleftrightarrow> (\<forall>i \<in> {..<enclen z}. ldec z i = 0)"
+by(auto simp add: Binnum_def)
+
+lemma Binnum_simulate2:
+  "(\<forall>i \<in> {..<enclen (Code_tp tp)}. ldec (Code_tp tp) i = 0) \<longleftrightarrow> (\<exists>k. tp = Bk \<up> k)"
+apply(induct tp)
+apply(simp)
+apply(simp)
+apply(simp add: lessThan_Suc)
+apply(case_tac a)
+apply(simp)
+defer
+apply(simp)
+oops
+
+apply(simp add: Binnum_def)
+
+text {*
+  @{text "Std cf"} returns true, if the  configuration  @{text "cf"} 
+  is a stardard tape. 
+*}
+
+fun Std :: "nat \<Rightarrow> bool"
+  where
+  "Std cf = (Binnum (Left cf) = 0 \<and> 
+            (\<exists>x\<le>(enclen (Right cf)). Binnum (Right cf) = 2 ^ x))"
+
+text{* 
+  @{text "Nostop m cf k"} means that afer @{text k} steps of 
+  execution the TM coded by @{text m} and started in configuration
+  @{text cf} is not at a stardard final configuration. *}
+
+fun Final :: "nat \<Rightarrow> bool"
+  where
+    "Final cf = (State cf = 0)"
+
+fun Nostop :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+  where
+  "Nostop m cf k = (Final (Steps cf m k) \<and> \<not> Std (Steps cf m k))"
+
+text{*
+  @{text "Halt"} is the function calculating the steps a TM needs to 
+  execute before reaching a stardard final configuration. This recursive 
+  function is the only one that uses unbounded minimization. So it is the 
+  only non-primitive recursive function needs to be used in the construction 
+  of the universal function @{text "UF"}. 
+*}
+
+fun Halt :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "Halt m cf = (LEAST k. \<not> Nostop m cf k)"
+
+fun UF :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "UF m cf = Stknum (Right (Steps m cf (Halt m cf)))"
+
+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 \<Longrightarrow> Newstate (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 \<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 Read_simulate:
+  "Read (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 Step_simulate:
+  assumes "tm_wf tp"
+  shows "Step (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 Step.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: State.simps)
+apply(simp only: list_encode_inverse)
+apply(simp only: misc if_True)
+apply(simp only: Read_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 Steps_simulate:
+  assumes "tm_wf 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 Step_simulate)
+apply(rule assms)
+apply(drule_tac x="step (a, b, c) tp" in meta_spec)
+apply(simp)
+done
+
+lemma Final_simulate:
+  "Final (Conf (Code_conf cf)) = is_final cf"
+by (case_tac cf) (simp)
+
+lemma Std_simulate:
+  "Std (Conf (Code_conf cf)) = std_tape (snd cf)" 
+apply(case_tac cf)
+apply(simp add: std_tape_def del: Std.simps)
+apply(subst Std.simps)
+
+(* UNTIL HERE *)
+
+
+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
+