# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1369498492 -3600
# Node ID 28d85e8ff391e3b8e45a8f5a738f94a0c8d67347
# Parent  b1b47d28c2956e725ec6d65d9f55d87bee85969a
more cleaning

diff -r b1b47d28c295 -r 28d85e8ff391 thys2/UF_Rec.thy
--- a/thys2/UF_Rec.thy	Sat May 25 16:40:48 2013 +0100
+++ b/thys2/UF_Rec.thy	Sat May 25 17:14:52 2013 +0100
@@ -2,30 +2,27 @@
 imports Recs Turing2
 begin
 
-section {* Coding of Turing Machines and tapes*}
+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"
+fun actnum :: "action \<Rightarrow> nat"
   where
-  "action_num W0 = 0"
-| "action_num W1 = 1"
-| "action_num L  = 2"
-| "action_num R  = 3"
-| "action_num Nop = 4"
+  "actnum W0 = 0"
+| "actnum W1 = 1"
+| "actnum L  = 2"
+| "actnum R  = 3"
+| "actnum Nop = 4"
 
-fun cell_num :: "cell \<Rightarrow> nat" where
-  "cell_num Bk = 0"
-| "cell_num Oc = 1"
+fun cellnum :: "cell \<Rightarrow> nat" where
+  "cellnum Bk = 0"
+| "cellnum Oc = 1"
+
+text {* Coding tapes *}
 
 fun code_tp :: "cell list \<Rightarrow> nat list"
   where
   "code_tp [] = []"
-| "code_tp (c # tp) = (cell_num c) # code_tp tp"
+| "code_tp (c # tp) = (cellnum c) # code_tp tp"
 
 fun Code_tp where
   "Code_tp tp = lenc (code_tp tp)"
@@ -39,7 +36,7 @@
 by (induct tp) (simp_all)
 
 lemma code_tp_nth [simp]:
-  "n < length tp \<Longrightarrow> (code_tp tp) ! n = cell_num (tp ! n)"
+  "n < length tp \<Longrightarrow> (code_tp tp) ! n = cellnum (tp ! n)"
 apply(induct n arbitrary: tp) 
 apply(simp_all)
 apply(case_tac [!] tp)
@@ -47,15 +44,16 @@
 done
 
 lemma code_tp_replicate [simp]:
-  "code_tp (c \<up> n) = (cell_num c) \<up> n"
+  "code_tp (c \<up> n) = (cellnum c) \<up> n"
 by(induct n) (simp_all)
 
+text {* Coding Configurations and TMs *}
 
 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)"
+  "code_instr i = penc (actnum (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))"
@@ -77,8 +75,8 @@
   where 
   "Code_tprog tm = lenc (code_tprog tm)"
 
-section {* Universal Function in HOL *}
 
+section {* An Universal Function in HOL *}
 
 text {* Reading and writing the encoded tape *}
 
@@ -90,8 +88,8 @@
 
 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}.
+  They calculate the new left and right tape (@{text p} and @{text r}) 
+  according to an action @{text a}. Adapted to our encoding functions.
 *}
 
 fun Newleft :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
@@ -146,17 +144,17 @@
 fun Right where
   "Right cf = ldec cf 2"
 
+text {*
+  @{text "Steps cf m k"} computes the TM configuration after @{text "k"} steps of 
+  execution of TM coded as @{text "m"}. @{text Step} is a single step of the TM.
+*}
+
 fun Step :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   where
   "Step cf m = Conf (Newstate m (State cf) (Read (Right cf)), 
                      Newleft (Left cf) (Right cf) (Action m (State cf) (Read (Right cf))),
                      Newright (Left cf) (Right cf) (Action 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"
@@ -167,74 +165,12 @@
 by (induct n arbitrary: cf) (simp_all only: Steps.simps)
 
 
-text {*
-  Decoding tapes into binary or stroke numbers.
-*}
+text {* Decoding tapes back into numbers. *}
 
 definition Stknum :: "nat \<Rightarrow> nat"
   where
   "Stknum z \<equiv> (\<Sum>i < enclen z. ldec z i)"
 
-
-definition
-  "right_std z \<equiv> (\<exists>i \<le> enclen z. 1 \<le> i \<and> (\<forall>j < i. ldec z j = 1) \<and> (\<forall>j < enclen z - i. ldec z (i + j) = 0))"
-
-definition
-  "left_std z \<equiv> (\<forall>j < enclen z. ldec z j = 0)"
-
-lemma ww:
- "(\<exists>k l. 1 \<le> k \<and> tp = Oc \<up> k @ Bk \<up> l) \<longleftrightarrow> 
-  (\<exists>i\<le>length tp. 1 \<le> i \<and> (\<forall>j < i. tp ! j = Oc) \<and> (\<forall>j < length tp - i. tp ! (i + j) = Bk))"
-apply(rule iffI)
-apply(erule exE)+
-apply(simp)
-apply(rule_tac x="k" in exI)
-apply(auto)[1]
-apply(simp add: nth_append)
-apply(simp add: nth_append)
-apply(erule exE)
-apply(rule_tac x="i" in exI)
-apply(rule_tac x="length tp - i" in exI)
-apply(auto)
-apply(rule sym)
-apply(subst append_eq_conv_conj)
-apply(simp)
-apply(rule conjI)
-apply (smt length_replicate length_take nth_equalityI nth_replicate nth_take)
-by (smt length_drop length_replicate nth_drop nth_equalityI nth_replicate)
-
-lemma right_std:
-  "(\<exists>k l. 1 \<le> k \<and> tp = Oc \<up> k @ Bk \<up> l) \<longleftrightarrow> right_std (Code_tp tp)"
-apply(simp only: ww)
-apply(simp add: right_std_def)
-apply(simp only: list_encode_inverse)
-apply(simp)
-apply(auto)
-apply(rule_tac x="i" in exI)
-apply(simp)
-apply(rule conjI)
-apply (metis Suc_eq_plus1 Suc_neq_Zero cell_num.cases cell_num.simps(1) leD less_trans linorder_neqE_nat)
-apply(auto)
-by (metis One_nat_def cell_num.cases cell_num.simps(2) less_diff_conv n_not_Suc_n nat_add_commute)
-
-lemma left_std:
-  "(\<exists>k. tp = Bk \<up> k) \<longleftrightarrow> left_std (Code_tp tp)"
-apply(simp add: left_std_def)
-apply(simp only: list_encode_inverse)
-apply(simp)
-apply(auto)
-apply(rule_tac x="length tp" in exI)
-apply(induct tp)
-apply(simp)
-apply(simp)
-apply(auto)
-apply(case_tac a)
-apply(auto)
-apply(case_tac a)
-apply(auto)
-by (metis Suc_less_eq nth_Cons_Suc)
-
-
 lemma Stknum_append:
   "Stknum (Code_tp (tp1 @ tp2)) = Stknum (Code_tp tp1) + Stknum (Code_tp tp2)"
 apply(simp only: Code_tp.simps)
@@ -276,11 +212,75 @@
 apply(simp only: tape_of_nat.simps)
 apply(simp only: Code_tp.simps)
 apply(simp only: code_tp_replicate)
-apply(simp only: cell_num.simps)
+apply(simp only: cellnum.simps)
 apply(simp only: Stknum_up)
 apply(simp)
 done
 
+
+section  {* Standard Tapes *}
+
+definition
+  "right_std z \<equiv> (\<exists>i \<le> enclen z. 1 \<le> i \<and> (\<forall>j < i. ldec z j = 1) \<and> (\<forall>j < enclen z - i. ldec z (i + j) = 0))"
+
+definition
+  "left_std z \<equiv> (\<forall>j < enclen z. ldec z j = 0)"
+
+lemma ww:
+ "(\<exists>k l. 1 \<le> k \<and> tp = Oc \<up> k @ Bk \<up> l) \<longleftrightarrow> 
+  (\<exists>i\<le>length tp. 1 \<le> i \<and> (\<forall>j < i. tp ! j = Oc) \<and> (\<forall>j < length tp - i. tp ! (i + j) = Bk))"
+apply(rule iffI)
+apply(erule exE)+
+apply(simp)
+apply(rule_tac x="k" in exI)
+apply(auto)[1]
+apply(simp add: nth_append)
+apply(simp add: nth_append)
+apply(erule exE)
+apply(rule_tac x="i" in exI)
+apply(rule_tac x="length tp - i" in exI)
+apply(auto)
+apply(rule sym)
+apply(subst append_eq_conv_conj)
+apply(simp)
+apply(rule conjI)
+apply (smt length_replicate length_take nth_equalityI nth_replicate nth_take)
+by (smt length_drop length_replicate nth_drop nth_equalityI nth_replicate)
+
+lemma right_std:
+  "(\<exists>k l. 1 \<le> k \<and> tp = Oc \<up> k @ Bk \<up> l) \<longleftrightarrow> right_std (Code_tp tp)"
+apply(simp only: ww)
+apply(simp add: right_std_def)
+apply(simp only: list_encode_inverse)
+apply(simp)
+apply(auto)
+apply(rule_tac x="i" in exI)
+apply(simp)
+apply(rule conjI)
+apply (metis Suc_eq_plus1 Suc_neq_Zero cellnum.cases cellnum.simps(1) leD less_trans linorder_neqE_nat)
+apply(auto)
+by (metis One_nat_def cellnum.cases cellnum.simps(2) less_diff_conv n_not_Suc_n nat_add_commute)
+
+lemma left_std:
+  "(\<exists>k. tp = Bk \<up> k) \<longleftrightarrow> left_std (Code_tp tp)"
+apply(simp add: left_std_def)
+apply(simp only: list_encode_inverse)
+apply(simp)
+apply(auto)
+apply(rule_tac x="length tp" in exI)
+apply(induct tp)
+apply(simp)
+apply(simp)
+apply(auto)
+apply(case_tac a)
+apply(auto)
+apply(case_tac a)
+apply(auto)
+by (metis Suc_less_eq nth_Cons_Suc)
+
+
+section {* Standard- and Final Configurations, the Universal Function *}
+
 text {*
   @{text "Std cf"} returns true, if the  configuration  @{text "cf"} 
   is a stardard tape. 
@@ -315,16 +315,15 @@
   where
   "Halt m cf = (LEAST k. Stop m cf k)"
 
-thm Steps.simps
-
 fun UF :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   where
   "UF m cf = Stknum (Right (Steps cf m (Halt m cf))) - 1"
 
-section {* The UF can simulate Turing machines *}
+
+section {* The UF simulates Turing machines *}
 
 lemma Update_left_simulate:
-  shows "Newleft (Code_tp l) (Code_tp r) (action_num a) = Code_tp (fst (update a (l, r)))"
+  shows "Newleft (Code_tp l) (Code_tp r) (actnum a) = Code_tp (fst (update a (l, r)))"
 apply(induct a)
 apply(simp_all)
 apply(case_tac l)
@@ -334,7 +333,7 @@
 done
 
 lemma Update_right_simulate:
-  shows "Newright (Code_tp l) (Code_tp r) (action_num a) = Code_tp (snd (update a (l, r)))"
+  shows "Newright (Code_tp l) (Code_tp r) (actnum a) = Code_tp (snd (update a (l, r)))"
 apply(induct a)
 apply(simp_all)
 apply(case_tac r)
@@ -348,19 +347,19 @@
 done
 
 lemma Fetch_state_simulate:
-  "tm_wf tp \<Longrightarrow> Newstate (Code_tprog tp) st (cell_num c) = snd (fetch tp st c)"
+  "tm_wf tp \<Longrightarrow> Newstate (Code_tprog tp) st (cellnum 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> Action (Code_tprog tp) st (cell_num c) = action_num (fst (fetch tp st c))"
+  "tm_wf tp \<Longrightarrow> Action (Code_tprog tp) st (cellnum c) = actnum (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)"
+  "Read (Code_tp tp) = cellnum (read tp)"
 apply(case_tac tp)
 apply(simp_all)
 done
@@ -464,14 +463,6 @@
 definition 
   "rec_write = CN rec_penc [S, CN rec_pdec2 [Id 2 1]]"
 
-lemma read_lemma [simp]:
-  "rec_eval rec_read [x] = Read x"
-by (simp add: rec_read_def)
-
-lemma write_lemma [simp]:
-  "rec_eval rec_write [x, y] = Write x y"
-by (simp add: rec_write_def)
-
 definition
     "rec_newleft =
        (let cond0 = CN rec_eq [Id 3 2, constn 0] in 
@@ -496,63 +487,28 @@
             CN rec_if [cond2, case2,
               CN rec_if [cond3, CN rec_pdec2 [Id 3 1], Id 3 1]]]])"
 
-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)
-
-
 definition
   "rec_actn = rec_swap (PR (CN rec_pdec1 [CN rec_pdec1 [Id 1 0]])
                            (CN rec_pdec1 [CN rec_pdec2 [Id 3 2]]))"
 
-lemma act_lemma [simp]:
-  "rec_eval rec_actn [n, c] = Actn n c"
-apply(simp add: rec_actn_def)
-apply(case_tac c)
-apply(simp_all)
-done
-
 definition 
   "rec_action = (let cond1 = CN rec_noteq [Id 3 1, Z] in 
                  let cond2 = CN rec_within [Id 3 0, CN rec_pred [Id 3 1]] in
                  let if_branch = CN rec_actn [CN rec_ldec [Id 3 0, CN rec_pred [Id 3 1]], Id 3 2]
                  in CN rec_if [CN rec_conj [cond1, cond2], if_branch, constn 4])"
 
-lemma action_lemma [simp]:
-  "rec_eval rec_action [m, q, c] = Action m q c"
-by (simp add: rec_action_def)
-
 definition
   "rec_newstat = rec_swap (PR (CN rec_pdec2 [CN rec_pdec1 [Id 1 0]])
                               (CN rec_pdec2 [CN rec_pdec2 [Id 3 2]]))"
 
-lemma newstat_lemma [simp]:
-  "rec_eval rec_newstat [n, c] = Newstat n c"
-apply(simp add: rec_newstat_def)
-apply(case_tac c)
-apply(simp_all)
-done
-
 definition
   "rec_newstate = (let cond = CN rec_noteq [Id 3 1, Z] in
                    let if_branch = CN rec_newstat [CN rec_ldec [Id 3 0, CN rec_pred [Id 3 1]], Id 3 2]
                    in CN rec_if [cond, if_branch, Z])"
 
-lemma newstate_lemma [simp]:
-  "rec_eval rec_newstate [m, q, r] = Newstate m q r"
-by (simp add: rec_newstate_def)
-
 definition
   "rec_conf = rec_lenc [Id 3 0, Id 3 1, Id 3 2]"
 
-lemma conf_lemma [simp]:
-  "rec_eval rec_conf [q, l, r] = Conf (q, l, r)"
-by(simp add: rec_conf_def)
-
 definition 
   "rec_state = CN rec_ldec [Id 1 0, Z]"
 
@@ -562,18 +518,6 @@
 definition 
   "rec_right = CN rec_ldec [Id 1 0, constn 2]"
 
-lemma state_lemma [simp]:
-  "rec_eval rec_state [cf] = State cf"
-by (simp add: rec_state_def)
-
-lemma left_lemma [simp]:
-  "rec_eval rec_left [cf] = Left cf"
-by (simp add: rec_left_def)
-
-lemma right_lemma [simp]:
-  "rec_eval rec_right [cf] = Right cf"
-by (simp add: rec_right_def)
-
 definition 
   "rec_step = (let left = CN rec_left [Id 2 0] in
                let right = CN rec_right [Id 2 0] in
@@ -585,28 +529,14 @@
                let newright = CN rec_newright [left, right, action] 
                in CN rec_conf [newstate, newleft, newright])" 
 
-lemma step_lemma [simp]:
-  "rec_eval rec_step [cf, m] = Step cf m"
-by (simp add: Let_def rec_step_def)
-
 definition 
-  "rec_steps = PR (Id 3 0)
-                  (CN rec_step [Id 4 1, Id 4 3])"
-
-lemma steps_lemma [simp]:
-  "rec_eval rec_steps [n, cf, p] = Steps cf p n"
-by (induct n) (simp_all add: rec_steps_def Step_Steps_comm del: Step.simps)
-
+  "rec_steps = PR (Id 3 0) (CN rec_step [Id 4 1, Id 4 3])"
 
 definition
   "rec_stknum = CN rec_minus 
                   [CN (rec_sigma1 (CN rec_ldec [Id 2 1, Id 2 0])) [CN rec_enclen [Id 1 0], Id 1 0],
                    CN rec_ldec [Id 1 0, CN rec_enclen [Id 1 0]]]"
 
-lemma stknum_lemma [simp]:
-  "rec_eval rec_stknum [z] = Stknum z"
-by (simp add: rec_stknum_def Stknum_def lessThan_Suc_atMost[symmetric])
-
 definition
   "rec_right_std = (let bound = CN rec_enclen [Id 1 0] in
                     let cond1 = CN rec_le [constn 1, Id 2 0] in
@@ -621,14 +551,6 @@
   "rec_left_std = (let cond = CN rec_eq [CN rec_ldec [Id 2 1, Id 2 0], Z]
                    in CN (rec_all1_less cond) [CN rec_enclen [Id 1 0], Id 1 0])"
 
-lemma left_std_lemma [simp]:
-  "rec_eval rec_left_std [z] = (if left_std z then 1 else 0)"
-by (simp add: Let_def rec_left_std_def left_std_def)
-
-lemma right_std_lemma [simp]:
-  "rec_eval rec_right_std [z] = (if right_std z then 1 else 0)"
-by (simp add: Let_def rec_right_std_def right_std_def)
-
 definition
   "rec_std = CN rec_conj [CN rec_left_std [CN rec_left [Id 1 0]],
                           CN rec_right_std [CN rec_right [Id 1 0]]]"
@@ -640,6 +562,89 @@
   "rec_stop = (let steps = CN rec_steps [Id 3 2, Id 3 1, Id 3 0] in
                CN rec_conj [CN rec_final [steps], CN rec_std [steps]])"
 
+definition
+  "rec_halt = MN (CN rec_not [CN rec_stop [Id 3 1, Id 3 2, Id 3 0]])"
+
+definition 
+  "rec_uf = CN rec_pred 
+              [CN rec_stknum 
+                  [CN rec_right 
+                     [CN rec_steps [CN rec_halt [Id 2 0, Id 2 1], Id 2 1, Id 2 0]]]]"
+
+lemma read_lemma [simp]:
+  "rec_eval rec_read [x] = Read x"
+by (simp add: rec_read_def)
+
+lemma write_lemma [simp]:
+  "rec_eval rec_write [x, y] = Write x y"
+by (simp add: rec_write_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 act_lemma [simp]:
+  "rec_eval rec_actn [n, c] = Actn n c"
+apply(simp add: rec_actn_def)
+apply(case_tac c)
+apply(simp_all)
+done
+
+lemma action_lemma [simp]:
+  "rec_eval rec_action [m, q, c] = Action m q c"
+by (simp add: rec_action_def)
+
+lemma newstat_lemma [simp]:
+  "rec_eval rec_newstat [n, c] = Newstat n c"
+apply(simp add: rec_newstat_def)
+apply(case_tac c)
+apply(simp_all)
+done
+
+lemma newstate_lemma [simp]:
+  "rec_eval rec_newstate [m, q, r] = Newstate m q r"
+by (simp add: rec_newstate_def)
+
+lemma conf_lemma [simp]:
+  "rec_eval rec_conf [q, l, r] = Conf (q, l, r)"
+by(simp add: rec_conf_def)
+
+lemma state_lemma [simp]:
+  "rec_eval rec_state [cf] = State cf"
+by (simp add: rec_state_def)
+
+lemma left_lemma [simp]:
+  "rec_eval rec_left [cf] = Left cf"
+by (simp add: rec_left_def)
+
+lemma right_lemma [simp]:
+  "rec_eval rec_right [cf] = Right cf"
+by (simp add: rec_right_def)
+
+lemma step_lemma [simp]:
+  "rec_eval rec_step [cf, m] = Step cf m"
+by (simp add: Let_def rec_step_def)
+
+lemma steps_lemma [simp]:
+  "rec_eval rec_steps [n, cf, p] = Steps cf p n"
+by (induct n) (simp_all add: rec_steps_def Step_Steps_comm del: Step.simps)
+
+lemma stknum_lemma [simp]:
+  "rec_eval rec_stknum [z] = Stknum z"
+by (simp add: rec_stknum_def Stknum_def lessThan_Suc_atMost[symmetric])
+
+lemma left_std_lemma [simp]:
+  "rec_eval rec_left_std [z] = (if left_std z then 1 else 0)"
+by (simp add: Let_def rec_left_std_def left_std_def)
+
+lemma right_std_lemma [simp]:
+  "rec_eval rec_right_std [z] = (if right_std z then 1 else 0)"
+by (simp add: Let_def rec_right_std_def right_std_def)
+
 lemma std_lemma [simp]:
   "rec_eval rec_std [cf] = (if Std cf then 1 else 0)"
 by (simp add: rec_std_def)
@@ -652,19 +657,10 @@
   "rec_eval rec_stop [m, cf, k] = (if Stop m cf k then 1 else 0)"
 by (simp add: Let_def rec_stop_def)
 
-definition
-  "rec_halt = MN (CN rec_not [CN rec_stop [Id 3 1, Id 3 2, Id 3 0]])"
-
 lemma halt_lemma [simp]:
   "rec_eval rec_halt [m, cf] = Halt m cf"
 by (simp add: rec_halt_def del: Stop.simps)
 
-definition 
-  "rec_uf = CN rec_pred 
-              [CN rec_stknum 
-                  [CN rec_right 
-                     [CN rec_steps [CN rec_halt [Id 2 0, Id 2 1], Id 2 1, Id 2 0]]]]"
-
 lemma uf_lemma [simp]:
   "rec_eval rec_uf [m, cf] = UF m cf"
 by (simp add: rec_uf_def)