diff -r 7fa1b8e88d76 -r 7cb94089324e thys/UTM.thy
--- a/thys/UTM.thy	Wed Feb 06 14:06:18 2013 +0000
+++ b/thys/UTM.thy	Wed Feb 06 14:09:35 2013 +0000
@@ -1235,6 +1235,7 @@
     done
 qed
 
+declare adjust.simps[simp]
 
 lemma adjust_fetch0: 
   "\<lbrakk>0 < a; a \<le> length ap div 2;  fetch ap a b = (aa, 0)\<rbrakk>
@@ -1252,6 +1253,8 @@
 apply(case_tac [!] st, auto simp: fetch.simps nth_of.simps)
 done
 
+declare adjust.simps[simp del]
+
 lemma adjust_step_eq: 
   assumes exec: "step0 (st,l,r) ap = (st', l', r')"
   and wf_tm: "tm_wf (ap, 0)"
@@ -1266,8 +1269,10 @@
     using assms
     apply(case_tac "st \<le> (length ap) div 2", simp)
     apply(case_tac st, auto simp: step.simps fetch.simps)
-    apply(case_tac "read r", simp_all add: fetch.simps nth_of.simps)
-    done   
+    apply(case_tac "read r", simp_all add: fetch.simps 
+      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)"
     using assms
     apply(case_tac "fetch ap st (read r)")
@@ -2025,7 +2030,7 @@
       done
   qed
   thus "?thesis"
-    apply(simp add: tape_of_nl_abv tape_of_nat_list.simps)
+    apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
     done
 qed
 
@@ -2957,7 +2962,7 @@
 lemma [simp]: "\<lbrakk>wprepare_add_one m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> list \<noteq> []"
 apply(simp only: wprepare_invs)
 apply(case_tac lm, simp_all add: tape_of_nl_abv 
-                         tape_of_nat_list.simps, auto)
+                         tape_of_nat_list.simps tape_of_nat_abv, auto)
 done
     
 lemma [simp]: "\<lbrakk>lm \<noteq> [];  wprepare_goto_first_end m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> list \<noteq> []"
@@ -2980,7 +2985,7 @@
 lemma [simp]: "\<lbrakk>lm \<noteq> [];  wprepare_goto_start_pos m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> list \<noteq> []"
 apply(simp only: wprepare_invs, auto)
 apply(case_tac lm, simp, case_tac list)
-apply(simp_all add: tape_of_nl_abv tape_of_nat_list.simps)
+apply(simp_all add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
 done
 
 lemma [simp]: "\<lbrakk>lm \<noteq> [];  wprepare_goto_start_pos m lm (b, Bk # list)\<rbrakk> \<Longrightarrow> b \<noteq> []"
@@ -3055,7 +3060,7 @@
 apply(auto)
 apply(drule_tac rev_equal_iff, simp add: tape_of_nl_rev)
 apply(case_tac "rev lm")
-apply(case_tac [2] list, auto simp: tape_of_nl_abv tape_of_nat_list.simps )
+apply(case_tac [2] list, auto simp: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
 done
 
 lemma [simp]: "wprepare_loop_start_in_middle m lm (b, [Bk]) = False"
@@ -3088,7 +3093,6 @@
  \<Longrightarrow> wprepare_loop_goon_in_middle m lm (Bk # b, a # lista) = False"
 apply(auto simp: wprepare_loop_start_on_rightmost.simps
                  wprepare_loop_goon_in_middle.simps)
-apply(case_tac [!] mr, simp_all)
 done
 
 lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start_on_rightmost m lm (b, Bk # a # lista)\<rbrakk>
@@ -3123,7 +3127,7 @@
 apply(case_tac lm1, simp)
 apply(rule_tac x = "Suc aa" in exI, simp)
 apply(rule_tac x = list in exI)
-apply(case_tac list, simp_all add: tape_of_nl_abv tape_of_nat_list.simps)
+apply(case_tac list, simp_all add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
 done
 
 lemma [simp]: "\<lbrakk>lm \<noteq> []; wprepare_loop_start m lm (b, Bk # a # lista)\<rbrakk> \<Longrightarrow> 
@@ -3188,6 +3192,7 @@
 lemma [simp]: "wprepare_loop_goon_on_rightmost m lm (b, Oc # list) = False"
 apply(simp add: wprepare_loop_goon_on_rightmost.simps)
 done
+
 lemma wprepare_loop1: "\<lbrakk>rev b @ Oc\<up>(mr) =  Oc\<up>(Suc m) @ Bk # Bk # <lm>; 
          b \<noteq> []; 0 < mr; Oc # list = Oc\<up>(mr) @ Bk\<up>(rn)\<rbrakk>
        \<Longrightarrow> wprepare_loop_start_on_rightmost m lm (Oc # b, list)"
@@ -3469,14 +3474,8 @@
   assume h: "args \<noteq> []"
   have "{?P1} t_wcode_prepare |+| t_wcode_main {?Q2}"
   proof(rule_tac Hoare_plus_halt)
-    show "?Q1 \<mapsto> ?P2"
-      by(simp add: assert_imp_def)
-  next
-    show "tm_wf (t_wcode_prepare, 0)"
-      by auto
-  next
     show "{?P1} t_wcode_prepare {?Q1}"
-    proof(rule_tac HoareI, auto)
+    proof(rule_tac Hoare_haltI, auto)
       show "\<exists>n. is_final (steps0 (Suc 0, [], <m # args>) t_wcode_prepare n) \<and>
         wprepare_stop m args holds_for steps0 (Suc 0, [], <m # args>) t_wcode_prepare n"
         using wprepare_correctness[of args m] h
@@ -3486,7 +3485,7 @@
     qed
   next
     show "{?P2} t_wcode_main {?Q2}"
-    proof(rule_tac HoareI, auto)
+    proof(rule_tac Hoare_haltI, auto)
       fix l r
       assume "wprepare_stop m args (l, r)"
       thus "\<exists>n. is_final (steps0 (Suc 0, l, r) t_wcode_main n) \<and>
@@ -3505,15 +3504,22 @@
           done
       qed
     qed
+  next
+    show "tm_wf0 t_wcode_prepare"
+      by auto
   qed
   thus "?thesis"
-    apply(auto simp: Hoare_def)
+    apply(auto simp: Hoare_halt_def)
     apply(rule_tac x = n in exI)
     apply(case_tac "(steps0 (Suc 0, [], <m # args>)
       (turing_basic.adjust t_wcode_prepare @ shift t_wcode_main (length t_wcode_prepare div 2)) n)")
     apply(auto simp: tm_comp.simps)
     done
 qed
+
+definition tinres :: "cell list \<Rightarrow> cell list \<Rightarrow> bool"
+  where
+  "tinres xs ys = (\<exists>n. xs = ys @ Bk \<up> n \<or> ys = xs @ Bk \<up> n)"
    
 lemma [simp]:  "tinres r r' \<Longrightarrow> 
   fetch t ss (read r) = 
@@ -3650,8 +3656,6 @@
 apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_4_eq_4)
 done
 
-thm numeral_5_eq_5
-
 lemma [simp]: "fetch t_wcode_adjust 5 Oc = (W0, 5)"
 apply(simp only: fetch.simps t_wcode_adjust_def nth_of.simps numeral_5_eq_5, simp)
 done
@@ -4533,15 +4537,13 @@
     using h by simp
   hence "{?P1} (t_wcode_prepare |+| t_wcode_main) |+| t_wcode_adjust {?Q2}"
   proof(rule_tac Hoare_plus_halt)
-    show "?Q1 \<mapsto> ?P2"
-      by(simp add: assert_imp_def)
   next
     show "tm_wf (t_wcode_prepare |+| t_wcode_main, 0)"
       apply(rule_tac tm_wf_comp, auto)
       done
   next
     show "{?P1} t_wcode_prepare |+| t_wcode_main {?Q1}"
-    proof(rule_tac HoareI, auto)
+    proof(rule_tac Hoare_haltI, auto)
       show 
         "\<exists>n. is_final (steps0 (Suc 0, [], <m # args>) (t_wcode_prepare |+| t_wcode_main) n) \<and>
         (\<lambda>(l, r). l = Bk # Oc # Oc \<up> m \<and>
@@ -4555,7 +4557,7 @@
     qed
   next
     show "{?P2} t_wcode_adjust {?Q2}"
-    proof(rule_tac HoareI, auto del: replicate_Suc)
+    proof(rule_tac Hoare_haltI, auto del: replicate_Suc)
       fix ln rn
       show "\<exists>n. is_final (steps0 (Suc 0, Bk # Oc # Oc \<up> m, 
         Bk # Oc # Bk \<up> ln @ Bk # Bk # Oc \<up> bl_bin (<args>) @ Bk \<up> rn) t_wcode_adjust n) \<and>
@@ -4570,7 +4572,7 @@
     qed
   qed
   thus "?thesis"
-    apply(simp add: Hoare_def, auto)
+    apply(simp add: Hoare_halt_def, auto)
     apply(case_tac "(steps0 (Suc 0, [], <(m::nat) # args>) 
       ((t_wcode_prepare |+| t_wcode_main) |+| t_wcode_adjust) n)")
     apply(rule_tac x = n in exI, auto simp: wadjust_stop.simps)
@@ -4603,7 +4605,7 @@
   \<exists> stp ln rn. steps0 (Suc 0, [], <m # args>)  (t_wcode) stp = 
               (0,  [Bk],  <[m ,bl_bin (<args>)]> @ Bk\<up>(rn))"
 using wcode_lemma_1[of args m]
-apply(simp add: t_wcode_def tape_of_nl_abv tape_of_nat_list.simps)
+apply(simp add: t_wcode_def tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
 done
 
 section {* The universal TM *}
@@ -4876,7 +4878,7 @@
 lemma [intro]: "tm_wf (t_utm, 0)"
 apply(simp only: t_utm_def F_tprog_def)
 apply(rule_tac t_compiled_correct, auto)
-done   
+done 
 
 lemma UTM_halt_lemma_pre: 
   assumes wf_tm: "tm_wf (tp, 0)"
@@ -4894,20 +4896,17 @@
   let ?P3 = "\<lambda> (l, r). False"
   have "{?P1} (t_wcode |+| t_utm) {?Q2}"
   proof(rule_tac Hoare_plus_halt)
-    show "?Q1 \<mapsto> ?P2"
-      by(simp add: assert_imp_def)
-  next
     show "tm_wf (t_wcode, 0)" by auto
   next
     show "{?P1} t_wcode {?Q1}"
-      apply(rule_tac HoareI, auto)
+      apply(rule_tac Hoare_haltI, auto)
       using wcode_lemma_1[of args "code tp"] args
       apply(auto)
       apply(rule_tac x = stp in exI, simp)
       done
   next
     show "{?P2} t_utm {?Q2}"
-    proof(rule_tac HoareI, auto)
+    proof(rule_tac Hoare_haltI, auto)
       fix rn
       show "\<exists>n. is_final (steps0 (Suc 0, [Bk], Oc # Oc \<up> code tp @ Bk # Oc # Oc \<up> bl_bin (<args>) @ Bk \<up> rn) t_utm n) \<and>
         (\<lambda>(l, r). (\<exists>ln. l = Bk \<up> ln) \<and>
@@ -4915,12 +4914,12 @@
         Oc # Oc \<up> code tp @ Bk # Oc # Oc \<up> bl_bin (<args>) @ Bk \<up> rn) t_utm n"
         using t_utm_halt_eq[of tp i "args" stp m rs k rn] assms
       apply(auto simp: bin_wc_eq)
-      apply(rule_tac x = stpa in exI, simp add: tape_of_nl_abv)
+      apply(rule_tac x = stpa in exI, simp add: tape_of_nl_abv tape_of_nat_abv)
       done
     qed
   qed
   thus "?thesis"
-    apply(auto simp: Hoare_def UTM_pre_def)
+    apply(auto simp: Hoare_halt_def UTM_pre_def)
     apply(case_tac "steps0 (Suc 0, [], <code tp # args>) (t_wcode |+| t_utm) n")
     apply(rule_tac x = n in exI, simp)
     done
@@ -5259,20 +5258,17 @@
   let ?P2 = ?Q1
   have "{?P1} (t_wcode |+| t_utm) \<up>"
   proof(rule_tac Hoare_plus_unhalt)
-    show "?Q1 \<mapsto> ?P2"
-      by(simp add: assert_imp_def)
-  next
     show "tm_wf (t_wcode, 0)" by auto
   next
     show "{?P1} t_wcode {?Q1}"
-      apply(rule_tac HoareI, auto)
+      apply(rule_tac Hoare_haltI, auto)
       using wcode_lemma_1[of args "code tp"] args
       apply(auto)
       apply(rule_tac x = stp in exI, simp)
       done
   next
     show "{?P2} t_utm \<up>"
-    proof(rule_tac Hoare_unhalt_I, auto)
+    proof(rule_tac Hoare_unhaltI, auto)
       fix n rn
       assume h: "is_final (steps0 (Suc 0, [Bk], Oc \<up> Suc (code tp) @ Bk # Oc \<up> Suc (bl_bin (<args>)) @ Bk \<up> rn) t_utm n)"
       have "\<forall> stp. \<not> is_final (steps0 (Suc 0, Bk\<up>(Suc 0), <[code tp, bl2wc (<args>)]> @ Bk\<up>(rn)) t_utm stp)"
@@ -5282,7 +5278,7 @@
       thus "False"
         using h
         apply(erule_tac x = n in allE)
-        apply(simp add: tape_of_nl_abv bin_wc_eq)
+        apply(simp add: tape_of_nl_abv bin_wc_eq tape_of_nat_abv)
         done
     qed
   qed