--- a/thys2/UF_Rec.thy Fri May 24 22:18:52 2013 +0100
+++ b/thys2/UF_Rec.thy Sat May 25 01:32:35 2013 +0100
@@ -111,27 +111,27 @@
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 @{text "Action"} function given on page 92 of B book, which is used to
+ fetch Turing Machine intructions. In @{text "Action 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" where
+ "Actn n 0 = pdec1 (pdec1 n)"
+| "Actn n _ = pdec1 (pdec2 n)"
-fun Actn :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+fun Action :: "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)"
+ "Action m q c = (if q \<noteq> 0 \<and> within m (q - 1) then Actn (ldec m (q - 1)) c else 4)"
-fun newstate :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
- "newstate n 0 = pdec2 (pdec1 n)"
-| "newstate n _ = pdec2 (pdec2 n)"
+fun Newstat :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+ "Newstat n 0 = pdec2 (pdec1 n)"
+| "Newstat 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)"
+ "Newstate 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
@@ -149,8 +149,8 @@
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))))"
+ 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
@@ -347,7 +347,7 @@
done
lemma Fetch_action_simulate:
- "tm_wf tp \<Longrightarrow> Actn (Code_tprog tp) st (cell_num c) = action_num (fst (fetch tp st c))"
+ "tm_wf tp \<Longrightarrow> Action (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
@@ -465,57 +465,109 @@
"rec_eval rec_write [x, y] = Write x y"
by (simp add: rec_write_def)
-
-
-
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 cond0 = CN rec_eq [Id 3 2, constn 0] in
+ let cond1 = 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]]])"
+ let case3 = CN rec_penc [CN S [CN rec_read [Id 3 1]], Id 3 0] in
+ CN rec_if [cond0, Id 3 0,
+ CN rec_if [cond1, Id 3 0,
+ CN rec_if [cond2, CN rec_pdec2 [Id 3 0],
+ 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]]]])"
+ (let cond0 = CN rec_eq [Id 3 2, constn 0] in
+ let cond1 = 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 case2 = CN rec_penc [CN S [CN rec_read [Id 3 0]], Id 3 1] in
+ CN rec_if [cond0, CN rec_write [constn 0, Id 3 1],
+ CN rec_if [cond1, CN rec_write [constn 1, Id 3 1],
+ 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_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])"
+ "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]]))"
-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])"
+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_trpl = CN rec_penc [CN rec_penc [Id 3 0, Id 3 1], Id 3 2]"
+ "rec_state = CN rec_ldec [Id 1 0, Z]"
definition
- "rec_left = rec_pdec1"
+ "rec_left = CN rec_ldec [Id 1 0, constn 1]"
definition
- "rec_right = CN rec_pdec2 [rec_pdec1]"
+ "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)
-definition
- "rec_stat = CN rec_pdec2 [rec_pdec2]"
+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)
+
+(* HERE *)
definition
"rec_newconf = (let act = CN rec_actn [Id 2 0, CN rec_stat [Id 2 1], CN rec_right [Id 2 1]] in