--- 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)