diff -r 07730607b0ca -r 38d8e0e37b7d thys/UTM.thy
--- a/thys/UTM.thy	Thu Feb 07 01:00:55 2013 +0000
+++ b/thys/UTM.thy	Thu Feb 07 03:01:51 2013 +0000
@@ -3648,11 +3648,11 @@
 apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps)
 done
 
-lemma [simp]: "fetch t_wcode_adjust (Suc (Suc (Suc (Suc 0)))) Bk = (L, 8)"
+lemma [simp]: "fetch t_wcode_adjust 4 Bk = (L, 8)"
 apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_4_eq_4)
 done
 
-lemma [simp]: "fetch t_wcode_adjust (Suc (Suc (Suc (Suc 0)))) Oc = (L, 5)"
+lemma [simp]: "fetch t_wcode_adjust 4 Oc = (L, 5)"
 apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_4_eq_4)
 done
 
@@ -4471,6 +4471,30 @@
 
 declare numeral_2_eq_2[simp del]
 
+lemma [simp]: "wadjust_start m rs (c, Bk # list)
+       \<Longrightarrow> wadjust_start m rs (c, Oc # list)"
+apply(auto simp: wadjust_start.simps)
+done
+
+lemma [simp]: "wadjust_backto_standard_pos m rs (c, Bk # list)
+       \<Longrightarrow> wadjust_stop m rs (Bk # c, list)"
+apply(auto simp: wadjust_backto_standard_pos.simps 
+wadjust_stop.simps wadjust_backto_standard_pos_B.simps)
+done
+
+lemma [simp]: "wadjust_start m rs (c, Oc # list)
+       \<Longrightarrow> wadjust_loop_start m rs (Oc # c, list)"
+apply(auto simp: wadjust_start.simps wadjust_loop_start.simps)
+apply(rule_tac x = ln in exI, simp)
+apply(rule_tac x = "rn" in exI, simp)
+apply(rule_tac x = 1 in exI, simp)
+done
+
+lemma [simp]:" wadjust_erase2 m rs (c, Oc # list)
+       \<Longrightarrow> wadjust_erase2 m rs (c, Bk # list)"
+apply(auto simp: wadjust_erase2.simps)
+done
+
 lemma wadjust_correctness:
   shows "let P = (\<lambda> (len, st, l, r). st = 0) in 
   let Q = (\<lambda> (len, st, l, r). wadjust_inv st m rs (l, r)) in 
@@ -4491,9 +4515,10 @@
       apply(rule_tac allI, rule_tac impI, case_tac "?f n", simp)
       apply(simp add: step.simps)
       apply(case_tac d, case_tac [2] aa, simp_all)
+      apply(simp_all only: wadjust_inv.simps split: if_splits)
+      apply(simp_all)
       apply(simp_all add: wadjust_inv.simps wadjust_le_def
-            abacus.lex_triple_def abacus.lex_pair_def lex_square_def numeral_4_eq_4
-            split: if_splits)
+            abacus.lex_triple_def abacus.lex_pair_def lex_square_def  split: if_splits)
       done
   next
     show "?Q (?f 0)"
@@ -4928,7 +4953,7 @@
 text {*
   The correctness of @{text "UTM"}, the halt case.
 *}
-lemma UTM_halt_lemma: 
+lemma UTM_halt_lemma': 
   assumes tm_wf: "tm_wf (tp, 0)"
   and result: "0 < rs"
   and args: "args \<noteq> []"
@@ -5291,7 +5316,7 @@
   The correctness of @{text "UTM"}, the unhalt case.
   *}
 
-lemma UTM_uhalt_lemma:
+lemma UTM_uhalt_lemma':
   assumes tm_wf: "tm_wf (tp, 0)"
   and unhalt: "\<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <args>) tp stp))"
   and args: "args \<noteq> []"
@@ -5301,4 +5326,101 @@
 apply(case_tac "rec_ci rec_F", simp)
 done
 
+lemma UTM_halt_lemma:
+  assumes tm_wf: "tm_wf (p, 0)"
+  and resut: "rs > 0"
+  and args: "(args::nat list) \<noteq> []"
+  and exec: "{(\<lambda>tp. tp = (Bk\<up>i, <args>))} p {(\<lambda>tp. tp = (Bk\<up>m, Oc\<up>rs @ Bk\<up>k))}" 
+  shows "{(\<lambda>tp. tp = ([], <code p # args>))} UTM {(\<lambda>tp. (\<exists> m n. tp = (Bk\<up>m, Oc\<up>rs @ Bk\<up>n)))}"
+proof -
+  have "{(\<lambda> (l, r). l = [] \<and> r = <code p # args>)} (t_wcode |+| t_utm)
+          {(\<lambda> (l, r). (\<exists> m. l = Bk\<up>m) \<and> (\<exists> n. r = Oc\<up>rs @ Bk\<up>n))}"
+  proof(rule_tac Hoare_plus_halt)
+    show "{\<lambda>(l, r). l = [] \<and> r = <code p # args>} t_wcode {\<lambda> (l, r). (l = [Bk] \<and>
+    (\<exists> rn. r = Oc\<up>(Suc (code p)) @ Bk # Oc\<up>(Suc (bl_bin (<args>))) @ Bk\<up>(rn)))}"
+      apply(rule_tac Hoare_haltI, auto)
+      using wcode_lemma_1[of args "code p"] args
+      apply(auto)
+      apply(rule_tac x = stp in exI, simp)
+      done
+  next
+    have "\<exists> stp. steps0 (Suc 0, Bk\<up>i, <args>) p stp = (0, Bk\<up>m, Oc\<up>rs @ Bk\<up>k)"
+      using exec
+      apply(simp add: Hoare_halt_def, auto)
+      apply(case_tac "steps0 (Suc 0, Bk \<up> i, <args>) p n", simp)
+      apply(rule_tac x = n in exI, simp)
+      done
+    then obtain stp where k: "steps0 (Suc 0, Bk\<up>i, <args>) p stp = (0, Bk\<up>m, Oc\<up>rs @ Bk\<up>k)"
+      ..
+    thus "{\<lambda>(l, r). l = [Bk] \<and> (\<exists>rn. r = Oc \<up> Suc (code p) @ Bk # Oc \<up> Suc (bl_bin (<args>)) @ Bk \<up> rn)}
+      t_utm {\<lambda>(l, r). (\<exists>m. l = Bk \<up> m) \<and> (\<exists>n. r = Oc \<up> rs @ Bk \<up> n)}"
+    proof(rule_tac Hoare_haltI, auto)
+      fix rn
+      show "\<exists>n. is_final (steps0 (Suc 0, [Bk], Oc \<up> Suc (code p) @ Bk # Oc \<up> Suc (bl_bin (<args>)) @ Bk \<up> rn) t_utm n) \<and>
+             (\<lambda>(l, r). (\<exists>m. l = Bk \<up> m) \<and> (\<exists>n. r = Oc \<up> rs @ Bk \<up> n)) holds_for steps0 
+         (Suc 0, [Bk], Oc \<up> Suc (code p) @ Bk # Oc \<up> Suc (bl_bin (<args>)) @ Bk \<up> rn) t_utm n"      
+        using t_utm_halt_eq[of p i "args" stp m rs k rn] assms k
+        apply(auto simp: bin_wc_eq, auto)        
+        apply(rule_tac x = stpa in exI, simp add: tape_of_nl_abv tape_of_nat_abv)
+        done
+    qed
+  next
+    show "tm_wf0 t_wcode" by auto
+  qed
+  thus "?thesis"
+    apply(case_tac "rec_ci rec_F")
+    apply(simp add: UTM_def t_utm_def F_aprog_def F_tprog_def)
+    apply(auto simp add: Hoare_halt_def)
+    apply(rule_tac x="n" in exI)
+    apply(auto)
+    apply(case_tac "(steps0 (Suc 0, [], <code p # args>)
+           (t_wcode |+| ((tm_of (a [+] dummy_abc (Suc (Suc 0)))) @
+                        shift (mopup (Suc (Suc 0)))
+                         (length (tm_of (a [+] dummy_abc (Suc (Suc 0)))) div
+                          2))) n)")
+    apply(simp)
+    done
+qed
+
+lemma UTM_halt_lemma2:
+  assumes tm_wf: "tm_wf (p, 0)"
+  and args: "(args::nat list) \<noteq> []"
+  and exec: "{(\<lambda>tp. tp = ([], <args>))} p {(\<lambda>tp. tp = (Bk\<up>m, <(n::nat)> @ Bk\<up>k))}" 
+  shows "{(\<lambda>tp. tp = ([], <code p # args>))} UTM {(\<lambda>tp. (\<exists> m k. tp = (Bk\<up>m, <n> @ Bk\<up>k)))}"
+using UTM_halt_lemma[OF assms(1) _ assms(2), where i="0"]
+using assms(3)
+apply(simp add: tape_of_nat_abv)
+done
+
+    
+lemma UTM_unhalt_lemma: 
+  assumes tm_wf: "tm_wf (p, 0)"
+  and unhalt: "{(\<lambda>tp. tp = (Bk\<up>i, <args>))} p \<up>"
+  and args: "args \<noteq> []"
+  shows "{(\<lambda>tp. tp = ([], <code p # args>))} UTM \<up>"
+proof -
+  have "\<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(i), <args>) p stp))"
+    using unhalt
+    apply(auto simp: Hoare_unhalt_def)    
+    apply(case_tac "steps0 (Suc 0, Bk \<up> i, <args>) p stp", simp)
+    apply(erule_tac x = stp in allE, simp add: TSTD_def)
+    done
+  then have "\<forall> stp. \<not> is_final (steps0 (Suc 0, [], <code p # args>)  UTM stp)"
+    using assms
+    apply(rule_tac  UTM_uhalt_lemma', simp_all)
+    done
+  thus "?thesis"
+    apply(simp add: Hoare_unhalt_def)
+    done
+qed
+    
+lemma UTM_unhalt_lemma2: 
+  assumes tm_wf: "tm_wf (p, 0)"
+  and unhalt: "{(\<lambda>tp. tp = ([], <args>))} p \<up>"
+  and args: "args \<noteq> []"
+  shows "{(\<lambda>tp. tp = ([], <code p # args>))} UTM \<up>"
+using UTM_unhalt_lemma[OF assms(1), where i="0"]
+using assms(2-3)
+apply(simp add: tape_of_nat_abv)
+done
 end                               
\ No newline at end of file