
diff -r 5704925ad138 -r aa102c182132 thys2/UF_Rec.thy
--- 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




