diff -r 5974111de158 -r f1ecb4a68a54 thys/UTM.thy
--- a/thys/UTM.thy	Thu Feb 21 05:33:57 2013 +0000
+++ b/thys/UTM.thy	Thu Feb 21 05:34:39 2013 +0000
@@ -543,7 +543,7 @@
 
 definition t_twice :: "instr list"
   where
-  "t_twice = adjust t_twice_compile"
+  "t_twice = adjust0 t_twice_compile"
 
 definition t_fourtimes_compile :: "instr list"
 where
@@ -551,7 +551,7 @@
 
 definition t_fourtimes :: "instr list"
   where
-  "t_fourtimes = adjust t_fourtimes_compile"
+  "t_fourtimes = adjust0 t_fourtimes_compile"
 
 definition t_twice_len :: "nat"
   where
@@ -1266,7 +1266,7 @@
 
 lemma adjust_fetch0: 
   "\<lbrakk>0 < a; a \<le> length ap div 2;  fetch ap a b = (aa, 0)\<rbrakk>
-  \<Longrightarrow> fetch (adjust ap) a b = (aa, Suc (length ap div 2))"
+  \<Longrightarrow> fetch (adjust0 ap) a b = (aa, Suc (length ap div 2))"
 apply(case_tac b, auto simp: fetch.simps nth_of.simps nth_map
                        split: if_splits)
 apply(case_tac [!] a, auto simp: fetch.simps nth_of.simps)
@@ -1274,7 +1274,7 @@
 
 lemma adjust_fetch_norm: 
   "\<lbrakk>st > 0;  st \<le> length tp div 2; fetch ap st b = (aa, ns); ns \<noteq> 0\<rbrakk>
- \<Longrightarrow>  fetch (Turing.adjust ap) st b = (aa, ns)"
+ \<Longrightarrow>  fetch (adjust0 ap) st b = (aa, ns)"
  apply(case_tac b, auto simp: fetch.simps nth_of.simps nth_map
                        split: if_splits)
 apply(case_tac [!] st, auto simp: fetch.simps nth_of.simps)
@@ -1286,7 +1286,7 @@
   assumes exec: "step0 (st,l,r) ap = (st', l', r')"
   and wf_tm: "tm_wf (ap, 0)"
   and notfinal: "st' > 0"
-  shows "step0 (st, l, r) (adjust ap) = (st', l', r')"
+  shows "step0 (st, l, r) (adjust0 ap) = (st', l', r')"
   using assms
 proof -
   have "st > 0"
@@ -1300,7 +1300,7 @@
       nth_of.simps adjust.simps tm_wf.simps split: if_splits)
     apply(auto simp: mod_ex2)
     done    
-  ultimately have "fetch (adjust ap) st (read r) = fetch ap st (read r)"
+  ultimately have "fetch (adjust0 ap) st (read r) = fetch ap st (read r)"
     using assms
     apply(case_tac "fetch ap st (read r)")
     apply(drule_tac adjust_fetch_norm, simp_all)
@@ -1317,7 +1317,7 @@
   assumes exec: "steps0 (st,l,r) ap stp = (st', l', r')"
   and wf_tm: "tm_wf (ap, 0)"
   and notfinal: "st' > 0"
-  shows "steps0 (st, l, r) (adjust ap) stp = (st', l', r')"
+  shows "steps0 (st, l, r) (adjust0 ap) stp = (st', l', r')"
   using exec notfinal
 proof(induct stp arbitrary: st' l' r')
   case 0
@@ -1326,7 +1326,7 @@
 next
   case (Suc stp st' l' r')
   have ind: "\<And>st' l' r'. \<lbrakk>steps0 (st, l, r) ap stp = (st', l', r'); 0 < st'\<rbrakk> 
-    \<Longrightarrow> steps0 (st, l, r) (Turing.adjust ap) stp = (st', l', r')" by fact
+    \<Longrightarrow> steps0 (st, l, r) (adjust0 ap) stp = (st', l', r')" by fact
   have h: "steps0 (st, l, r) ap (Suc stp) = (st', l', r')" by fact
   have g:   "0 < st'" by fact
   obtain st'' l'' r'' where a: "steps0 (st, l, r) ap stp = (st'', l'', r'')"
@@ -1336,7 +1336,7 @@
     apply(simp add: step_red)
     apply(case_tac st'', auto)
     done
-  hence b: "steps0 (st, l, r) (Turing.adjust ap) stp = (st'', l'', r'')"
+  hence b: "steps0 (st, l, r) (adjust0 ap) stp = (st'', l'', r'')"
     using a
     by(rule_tac ind, simp_all)
   thus "?case"
@@ -1349,7 +1349,7 @@
 lemma adjust_halt_eq:
   assumes exec: "steps0 (1, l, r) ap stp = (0, l', r')"
   and tm_wf: "tm_wf (ap, 0)" 
-  shows "\<exists> stp. steps0 (Suc 0, l, r) (adjust ap) stp = 
+  shows "\<exists> stp. steps0 (Suc 0, l, r) (adjust0 ap) stp = 
         (Suc (length ap div 2), l', r')"
 proof -
   have "\<exists> stp. \<not> is_final (steps0 (1, l, r) ap stp) \<and> (steps0 (1, l, r) ap (Suc stp) = (0, l', r'))"
@@ -1358,7 +1358,7 @@
   then obtain stpa where a: 
     "\<not> is_final (steps0 (1, l, r) ap stpa) \<and> (steps0 (1, l, r) ap (Suc stpa) = (0, l', r'))" ..
   obtain sa la ra where b:"steps0 (1, l, r) ap stpa = (sa, la, ra)"  by (metis prod_cases3)
-  hence c: "steps0 (Suc 0, l, r) (adjust ap) stpa = (sa, la, ra)"
+  hence c: "steps0 (Suc 0, l, r) (adjust0 ap) stpa = (sa, la, ra)"
     using assms a
     apply(rule_tac adjust_steps_eq, simp_all)
     done
@@ -1371,7 +1371,7 @@
     using b a
     apply(simp add: step_red step.simps)
     done
-  have k: "fetch (adjust ap) sa (read ra) = (ac, Suc (length ap div 2))"
+  have k: "fetch (adjust0 ap) sa (read ra) = (ac, Suc (length ap div 2))"
     using a b c d e f
     apply(rule_tac adjust_fetch0, simp_all)
     done
@@ -1402,14 +1402,14 @@
     (tm_of abc_twice @ shift (mopup (Suc 0)) ((length (tm_of abc_twice) div 2))) stp =
     (0, Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(rn))" by blast
   hence "\<exists> stp. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
-    (adjust t_twice_compile) stp
+    (adjust0 t_twice_compile) stp
      = (Suc (length t_twice_compile div 2), Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(rn))"
     apply(rule_tac stp = stp in adjust_halt_eq)
     apply(simp add: t_twice_compile_def, auto)
     done
   then obtain stpb where 
     "steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
-    (adjust t_twice_compile) stpb
+    (adjust0 t_twice_compile) stpb
      = (Suc (length t_twice_compile div 2), Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(rn))" ..
   thus "?thesis"
     apply(simp add: t_twice_def t_twice_len_def)
@@ -2079,14 +2079,14 @@
     (tm_of abc_fourtimes @ shift (mopup 1) ((length (tm_of abc_fourtimes) div 2))) stp =
     (0, Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (4 * rs)) @ Bk\<up>(rn))" by blast
   hence "\<exists> stp. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
-    (adjust t_fourtimes_compile) stp
+    (adjust0 t_fourtimes_compile) stp
      = (Suc (length t_fourtimes_compile div 2), Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (4 * rs)) @ Bk\<up>(rn))"
     apply(rule_tac stp = stp in adjust_halt_eq)
     apply(simp add: t_fourtimes_compile_def, auto)
     done
   then obtain stpb where 
     "steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
-    (adjust t_fourtimes_compile) stpb
+    (adjust0 t_fourtimes_compile) stpb
      = (Suc (length t_fourtimes_compile div 2), Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (4 * rs)) @ Bk\<up>(rn))" ..
   thus "?thesis"
     apply(simp add: t_fourtimes_def t_fourtimes_len_def)
@@ -3356,7 +3356,7 @@
 
 
 lemma tm_wf_change_termi: "tm_wf (tp, 0) \<Longrightarrow> 
-      list_all (\<lambda>(acn, st). (st \<le> Suc (length tp div 2))) (adjust tp)"
+      list_all (\<lambda>(acn, st). (st \<le> Suc (length tp div 2))) (adjust0 tp)"
 apply(auto simp: tm_wf.simps List.list_all_length)
 apply(case_tac "tp!n", auto simp: adjust.simps split: if_splits)
 apply(erule_tac x = "(a, b)" in ballE, auto)
@@ -3376,28 +3376,36 @@
 apply(auto simp: mopup.simps)
 done
 
-lemma [elim]: "(a, b) \<in> set (shift (Turing.adjust t_twice_compile) 12) \<Longrightarrow> 
+lemma [elim]: "(a, b) \<in> set (shift (adjust0 t_twice_compile) 12) \<Longrightarrow> 
   b \<le> (28 + (length t_twice_compile + length t_fourtimes_compile)) div 2"
 apply(simp add: t_twice_compile_def t_fourtimes_compile_def)
 proof -
-  assume g: "(a, b) \<in> set (shift (Turing.adjust (tm_of abc_twice @ shift (mopup (Suc 0)) (length (tm_of abc_twice) div 2))) 12)"
+  assume g: "(a, b)
+    \<in> set (shift
+            (adjust
+              (tm_of abc_twice @
+               shift (mopup (Suc 0)) (length (tm_of abc_twice) div 2))
+              (Suc ((length (tm_of abc_twice) + 16) div 2)))
+            12)"
   moreover have "length (tm_of abc_twice) mod 2 = 0" by auto
   moreover have "length (tm_of abc_fourtimes) mod 2 = 0" by auto
   ultimately have "list_all (\<lambda>(acn, st). (st \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2)) 
-    (shift (Turing.adjust t_twice_compile) 12)"
-  proof(auto simp: mod_ex1)
+    (shift (adjust0 t_twice_compile) 12)"
+  proof(auto simp add: mod_ex1 del: adjust.simps)
     fix q qa
     assume h: "length (tm_of abc_twice) = 2 * q" "length (tm_of abc_fourtimes) = 2 * qa"
-    hence "list_all (\<lambda>(acn, st). st \<le> (18 + (q + qa)) + 12) (shift (Turing.adjust t_twice_compile) 12)"
+    hence "list_all (\<lambda>(acn, st). st \<le> (18 + (q + qa)) + 12) (shift (adjust0 t_twice_compile) 12)"
     proof(rule_tac tm_wf_shift t_twice_compile_def)
-      have "list_all (\<lambda>(acn, st). st \<le> Suc (length t_twice_compile div 2)) (adjust t_twice_compile)"
+      have "list_all (\<lambda>(acn, st). st \<le> Suc (length t_twice_compile div 2)) (adjust0 t_twice_compile)"
         by(rule_tac tm_wf_change_termi, auto)
-      thus "list_all (\<lambda>(acn, st). st \<le> 18 + (q + qa)) (Turing.adjust t_twice_compile)"
+      thus "list_all (\<lambda>(acn, st). st \<le> 18 + (q + qa)) (adjust0 t_twice_compile)"
         using h
         apply(simp add: t_twice_compile_def, auto simp: List.list_all_length)
         done
     qed
-    thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa)) (shift (Turing.adjust t_twice_compile) 12)"
+    thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa))
+           (shift
+             (adjust t_twice_compile (Suc (length t_twice_compile div 2))) 12)"
       by simp
   qed
   thus "b \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2"
@@ -3408,37 +3416,50 @@
     done
 qed 
 
-lemma [elim]: "(a, b) \<in> set (shift (Turing.adjust t_fourtimes_compile) (t_twice_len + 13)) 
+lemma [elim]: "(a, b) \<in> set (shift (adjust0 t_fourtimes_compile) (t_twice_len + 13)) 
   \<Longrightarrow> b \<le> (28 + (length t_twice_compile + length t_fourtimes_compile)) div 2"
 apply(simp add: t_twice_compile_def t_fourtimes_compile_def t_twice_len_def)
 proof -
-  assume g: "(a, b) \<in> set (shift (Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0))
-    (length (tm_of abc_fourtimes) div 2))) (length t_twice div 2 + 13))"
+  assume g: "(a, b)
+    \<in> set (shift
+            (adjust
+              (tm_of abc_fourtimes @
+               shift (mopup (Suc 0)) (length (tm_of abc_fourtimes) div 2))
+              (Suc ((length (tm_of abc_fourtimes) + 16) div 2)))
+            (length t_twice div 2 + 13))"
   moreover have "length (tm_of abc_twice) mod 2 = 0" by auto
   moreover have "length (tm_of abc_fourtimes) mod 2 = 0" by auto
   ultimately have "list_all (\<lambda>(acn, st). (st \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2)) 
-    (shift (Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0))
+    (shift (adjust0 (tm_of abc_fourtimes @ shift (mopup (Suc 0))
     (length (tm_of abc_fourtimes) div 2))) (length t_twice div 2 + 13))"
   proof(auto simp: mod_ex1 t_twice_def t_twice_compile_def)
     fix q qa
     assume h: "length (tm_of abc_twice) = 2 * q" "length (tm_of abc_fourtimes) = 2 * qa"
     hence "list_all (\<lambda>(acn, st). st \<le> (9 + qa + (21 + q)))
-      (shift (Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)) (21 + q))"
+      (shift (adjust0 (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)) (21 + q))"
     proof(rule_tac tm_wf_shift t_twice_compile_def)
       have "list_all (\<lambda>(acn, st). st \<le> Suc (length (tm_of abc_fourtimes @ shift 
-        (mopup (Suc 0)) qa) div 2)) (adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa))"
+        (mopup (Suc 0)) qa) div 2)) (adjust0 (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa))"
         apply(rule_tac tm_wf_change_termi)
         using wf_fourtimes h
         apply(simp add: t_fourtimes_compile_def)
-        done        
-      thus "list_all (\<lambda>(acn, st). st \<le> 9 + qa) ((Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)))"
+        done
+      thus "list_all (\<lambda>(acn, st). st \<le> 9 + qa)
+        (adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)
+          (Suc (length (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa) div
+                2)))"
         using h
         apply(simp)
         done
     qed
-    thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa)) (shift (Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)) (21 + q))"
+    thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa))
+           (shift
+             (adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)
+               (9 + qa))
+             (21 + q))"
       apply(subgoal_tac "qa + q = q + qa")
-      apply(simp, simp)
+      apply(simp add: h)
+      apply(simp)
       done
   qed
   thus "b \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2"
@@ -3515,7 +3536,7 @@
     apply(auto simp: Hoare_halt_def)
     apply(rule_tac x = n in exI)
     apply(case_tac "(steps0 (Suc 0, [], <m # args>)
-      (Turing.adjust t_wcode_prepare @ shift t_wcode_main (length t_wcode_prepare div 2)) n)")
+      (adjust0 t_wcode_prepare @ shift t_wcode_main (length t_wcode_prepare div 2)) n)")
     apply(auto simp: tm_comp.simps)
     done
 qed
@@ -4613,7 +4634,7 @@
   *}
 definition t_wcode :: "instr list"
   where
-  "t_wcode = (t_wcode_prepare |+| t_wcode_main) |+| t_wcode_adjust"
+  "t_wcode = (t_wcode_prepare |+| t_wcode_main) |+| t_wcode_adjust        "
 
 
 text {*