# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1358865962 0
# Node ID e33306b4c62e45471fa7bea54847067b05a14b70
# Parent  7edbd5657702a19f31cf7892517ac726a4890ef2
updated

diff -r 7edbd5657702 -r e33306b4c62e thys/turing_hoare.thy
--- a/thys/turing_hoare.thy	Tue Jan 22 14:38:56 2013 +0000
+++ b/thys/turing_hoare.thy	Tue Jan 22 14:46:02 2013 +0000
@@ -99,6 +99,9 @@
           {P1} A |+| B  loops
 *}
 
+
+
+
 lemma Hoare_plus_unhalt:
   assumes a_imp: "Q1 \<mapsto> P2"
   and A_wf : "tm_wf (A, 0)"
@@ -127,7 +130,7 @@
       where "steps0 (Suc 0, l', r') B (n - n2) = (s'', l'', r'')" 
       and "\<not> is_final (s'', l'', r'')" by (metis surj_pair)
     then have "steps0 (Suc (length A div 2), l', r') (A |+| B) (n - n2) = (s''+ length A div 2, l'', r'')"
-      using A_wf by (auto dest: t_merge_second_same simp del: steps.simps)
+      using A_wf by (auto dest: t_merge_second_same simp del: tm_wf.simps)
     then have "\<not> is_final (steps0 (1, l, r) (A |+| B) (n2 + (n  - n2)))"
       using A_wf by (simp only: steps_add eq) (simp add: tm_wf.simps)
     then show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" 
@@ -152,10 +155,12 @@
 by (metis holds_for.simps surj_pair)
 
 
+declare tm_comp.simps [simp del] 
+declare adjust.simps[simp del] 
+declare shift.simps[simp del]
+declare tm_wf.simps[simp del]
 declare step.simps[simp del]
 declare steps.simps[simp del]
-declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del]
-declare tm_wf.simps[simp del]