Mercurial Mercurial > hg > tm / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/uncomputable.thy
changeset 82 c470f1705baa
parent 81 2e9881578cb2
child 83 8dc659af1bd2
equal deleted inserted replaced
81:2e9881578cb2 82:c470f1705baa 
   195 
   195 
   196 
   196 
   197 (* tcopy_loop *)
 
   197 (* tcopy_loop *)
 
   198 
   198 
   199 fun 
   199 fun 
   200   inv_loop0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
       
   201   inv_loop1_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   200   inv_loop1_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   202   inv_loop1_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   201   inv_loop1_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
       
   202   inv_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
       
   203   inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
       
   204   inv_loop6_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
       
   205   inv_loop6_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 
       
   206 where
 
       
   207   "inv_loop1_loop x (l, r) = (\<exists> i j. i + j + 1 = x \<and> l = Oc\<up>i \<and> r = Oc # Oc # Bk\<up>j @ Oc\<up>j \<and> j > 0)"
 
       
   208 | "inv_loop1_exit x (l, r) = (l = [] \<and> r = Bk # Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0)"
 
       
   209 | "inv_loop5_loop x (l, r) = 
       
   210      (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> t > 0 \<and> l = Oc\<up>k@Bk\<up>j@Oc\<up>i \<and> r = Oc\<up>t)"
 
       
   211 | "inv_loop5_exit x (l, r) = 
       
   212      (\<exists> i j. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and>  l = Bk\<up>(j - 1)@Oc\<up>i \<and> r = Bk # Oc\<up>j)"
 
       
   213 | "inv_loop6_loop x (l, r) = 
       
   214      (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> k + t + 1 = j \<and> l = Bk\<up>k @ Oc\<up>i \<and> r = Bk\<up>(Suc t) @ Oc\<up>j)"
 
       
   215 | "inv_loop6_exit x (l, r) = 
       
   216      (\<exists> i j. i + j = x \<and> j > 0 \<and> l = Oc\<up>i \<and> r = Oc # Bk\<up>j @ Oc\<up>j)"
 
       
   217 
       
   218 fun 
       
   219   inv_loop0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   203   inv_loop1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   220   inv_loop1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   204   inv_loop2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   221   inv_loop2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   205   inv_loop3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   222   inv_loop3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   206   inv_loop4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   223   inv_loop4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   207   inv_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   224   inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   208   inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   225   inv_loop6 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 
   209   inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 
       
   210 where
 
   226 where
 
   211   "inv_loop0 x (l, r) =  (l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0 )"
 
   227   "inv_loop0 x (l, r) =  (l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0 )"
 
   212 | "inv_loop1_loop x (l, r) = (\<exists> i j. i + j + 1 = x \<and> l = Oc\<up>i \<and> r = Oc # Oc # Bk\<up>j @ Oc\<up>j \<and> j > 0)"
 
       
   213 | "inv_loop1_exit x (l, r) = (l = [] \<and> r = Bk # Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0)"
 
       
   214 | "inv_loop1 x (l, r) = (inv_loop1_loop x (l, r) \<or> inv_loop1_exit x (l, r))"
 
   228 | "inv_loop1 x (l, r) = (inv_loop1_loop x (l, r) \<or> inv_loop1_exit x (l, r))"
 
   215 | "inv_loop2 x (l, r) = (\<exists> i j any. i + j = x \<and> x > 0 \<and> i > 0 \<and> j > 0 \<and> l = Oc\<up>i \<and> r = any#Bk\<up>j@Oc\<up>j)"
 
   229 | "inv_loop2 x (l, r) = (\<exists> i j any. i + j = x \<and> x > 0 \<and> i > 0 \<and> j > 0 \<and> l = Oc\<up>i \<and> r = any#Bk\<up>j@Oc\<up>j)"
 
   216 | "inv_loop3 x (l, r) = 
   230 | "inv_loop3 x (l, r) = 
   217      (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = Suc j \<and> l = Bk\<up>k@Oc\<up>i \<and> r = Bk\<up>t@Oc\<up>j)"
 
   231      (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = Suc j \<and> l = Bk\<up>k@Oc\<up>i \<and> r = Bk\<up>t@Oc\<up>j)"
 
   218 | "inv_loop4 x (l, r) = 
   232 | "inv_loop4 x (l, r) = 
   219      (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = j \<and> l = Oc\<up>k @ Bk\<up>(Suc j)@Oc\<up>i \<and> r = Oc\<up>t)"
 
   233      (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = j \<and> l = Oc\<up>k @ Bk\<up>(Suc j)@Oc\<up>i \<and> r = Oc\<up>t)"
 
   220 | "inv_loop5_loop x (l, r) = 
       
   221      (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> t > 0 \<and> l = Oc\<up>k@Bk\<up>j@Oc\<up>i \<and> r = Oc\<up>t)"
 
       
   222 | "inv_loop5_exit x (l, r) = (\<exists> i j. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and>  l = Bk\<up>(j - 1)@Oc\<up>i \<and> r = Bk # Oc\<up>j)"
 
       
   223 | "inv_loop5 x (l, r) = (inv_loop5_loop x (l, r) \<or> inv_loop5_exit x (l, r))"
 
   234 | "inv_loop5 x (l, r) = (inv_loop5_loop x (l, r) \<or> inv_loop5_exit x (l, r))"
 
   224 
   235 | "inv_loop6 x (l, r) = (inv_loop6_loop x (l, r) \<or> inv_loop6_exit x (l, r))"
 
   225 fun inv_loop6_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 
       
   226   where
 
       
   227   "inv_loop6_loop x (l, r) = 
       
   228      (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> k + t + 1 = j \<and> l = Bk\<up>k @ Oc\<up>i \<and> r = Bk\<up>(Suc t) @ Oc\<up>j)"
 
       
   229 
       
   230 fun inv_loop6_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 
       
   231   where
 
       
   232   "inv_loop6_exit x (l, r) = 
       
   233      (\<exists> i j. i + j = x \<and> j > 0 \<and> l = Oc\<up>i \<and> r = Oc # Bk\<up>j @ Oc\<up>j)"
 
       
   234 
       
   235 fun inv_loop6 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 
       
   236   where
 
       
   237   "inv_loop6 x (l, r) = (inv_loop6_loop x (l, r) \<or> inv_loop6_exit x (l, r))"
 
       
   238 
   236 
   239 fun inv_loop :: "nat \<Rightarrow> config \<Rightarrow> bool"
 
   237 fun inv_loop :: "nat \<Rightarrow> config \<Rightarrow> bool"
 
   240   where
 
   238   where
 
   241   "inv_loop x (s, l, r) = 
   239   "inv_loop x (s, l, r) = 
   242          (if s = 0 then inv_loop0 x (l, r)
 
   240          (if s = 0 then inv_loop0 x (l, r)
 
   255 
   253 
   256 lemma [elim]: "Bk # list = Oc \<up> t \<Longrightarrow> RR"
 
   254 lemma [elim]: "Bk # list = Oc \<up> t \<Longrightarrow> RR"
 
   257 by (case_tac t, auto)
 
   255 by (case_tac t, auto)
 
   258 
   256 
   259 lemma [simp]: "inv_loop1 x (b, []) = False"
 
   257 lemma [simp]: "inv_loop1 x (b, []) = False"
 
   260 by(simp add: inv_loop1.simps)
 
   258 by (simp add: inv_loop1.simps)
 
   261 
   259 
   262 lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
 
   260 lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
 
   263 by (auto simp: inv_loop2.simps inv_loop3.simps)
 
   261 by (auto simp: inv_loop2.simps inv_loop3.simps)
 
   264 
   262 
   265 
   263 
   272 apply(rule_tac [!] x = i in exI, 
   270 apply(rule_tac [!] x = i in exI, 
   273       rule_tac [!] x  = "Suc j" in exI, simp_all)
 
   271       rule_tac [!] x  = "Suc j" in exI, simp_all)
 
   274 done
 
   272 done
 
   275 
   273 
   276 lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], [])\<rbrakk> \<Longrightarrow> RR"
 
   274 lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], [])\<rbrakk> \<Longrightarrow> RR"
 
   277 apply(auto simp: inv_loop4.simps inv_loop5.simps)
 
   275 by (auto simp: inv_loop4.simps inv_loop5.simps)
 
   278 done
 
       
   279 
   276 
   280 lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, []); b \<noteq> []\<rbrakk> \<Longrightarrow> RR"
 
   277 lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, []); b \<noteq> []\<rbrakk> \<Longrightarrow> RR"
 
   281 apply(auto simp: inv_loop4.simps inv_loop5.simps)
 
   278 by (auto simp: inv_loop4.simps inv_loop5.simps)
 
   282 done
 
       
   283 
   279 
   284 lemma [elim]: "inv_loop6 x ([], []) \<Longrightarrow> RR"
 
   280 lemma [elim]: "inv_loop6 x ([], []) \<Longrightarrow> RR"
 
   285 apply(auto simp: inv_loop6.simps)
 
   281 by (auto simp: inv_loop6.simps)
 
   286 done
 
   282 
   287 
       
   288 thm inv_loop6_exit.simps
 
       
   289 lemma [elim]: "inv_loop6 x (b, []) \<Longrightarrow> RR" 
   283 lemma [elim]: "inv_loop6 x (b, []) \<Longrightarrow> RR" 
   290 apply(auto simp: inv_loop6.simps)
 
   284 by (auto simp: inv_loop6.simps)
 
   291 done
 
       
   292 
   285 
   293 lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> b = []"
 
   286 lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> b = []"
 
   294 apply(auto simp: inv_loop1.simps)
 
   287 by (auto simp: inv_loop1.simps)
 
   295 done
 
       
   296 
   288 
   297 lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> list = Oc # Bk \<up> x @ Oc \<up> x"
 
   289 lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> list = Oc # Bk \<up> x @ Oc \<up> x"
 
   298 apply(auto simp: inv_loop1.simps)
 
   290 by (auto simp: inv_loop1.simps)
 
   299 done
 
       
   300 
   291 
   301 lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
 
   292 lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
 
   302 apply(auto simp: inv_loop2.simps inv_loop3.simps)
 
   293 apply(auto simp: inv_loop2.simps inv_loop3.simps)
 
   303 apply(rule_tac [!] x = i  in exI, rule_tac [!] x = j in exI, simp_all)
 
   294 apply(rule_tac [!] x = i  in exI, rule_tac [!] x = j in exI, simp_all)
 
   304 done
 
   295 done
 
   305 
   296 
   306 lemma [elim]: "Bk # list = Oc \<up> j \<Longrightarrow> RR"
 
   297 lemma [elim]: "Bk # list = Oc \<up> j \<Longrightarrow> RR"
 
   307 apply(case_tac j, simp_all)
 
   298 by (case_tac j, simp_all)
 
   308 done
 
       
   309 
   299 
   310 lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
 
   300 lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
 
   311 apply(auto simp: inv_loop3.simps)
 
   301 apply(auto simp: inv_loop3.simps)
 
   312 apply(rule_tac [!] x = i in exI, 
   302 apply(rule_tac [!] x = i in exI, 
   313       rule_tac [!] x = j in exI, simp_all)
 
   303       rule_tac [!] x = j in exI, simp_all)
 
   314 apply(case_tac [!] t, auto)
 
   304 apply(case_tac [!] t, auto)
 
   315 done
 
   305 done
 
   316 
   306 
   317 lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop5 x (b, Oc # list)"
 
   307 lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop5 x (b, Oc # list)"
 
   318 apply(auto simp: inv_loop4.simps inv_loop5.simps)
 
   308 by (auto simp: inv_loop4.simps inv_loop5.simps)
 
   319 done
 
       
   320 
   309 
   321 lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
 
   310 lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
 
   322 apply(auto simp: inv_loop6.simps inv_loop5.simps)
 
   311 by (auto simp: inv_loop6.simps inv_loop5.simps)
 
   323 done
 
       
   324 
   312 
   325 lemma [simp]: "inv_loop5_loop x (b, Bk # list) = False"
 
   313 lemma [simp]: "inv_loop5_loop x (b, Bk # list) = False"
 
   326 apply(auto simp: inv_loop5_loop.simps)
 
   314 by (auto simp: inv_loop5.simps)
 
   327 done
 
       
   328 
   315 
   329 lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"
 
   316 lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"
 
   330 apply(auto simp: inv_loop6.simps)
 
   317 by (auto simp: inv_loop6.simps)
 
   331 done
 
       
   332 
   318 
   333 declare inv_loop5_loop.simps[simp del]  inv_loop5_exit.simps[simp del]
 
   319 declare inv_loop5_loop.simps[simp del]  inv_loop5_exit.simps[simp del]
 
   334        inv_loop6_loop.simps[simp del]  inv_loop6_exit.simps[simp del]
 
   320        inv_loop6_loop.simps[simp del]  inv_loop6_exit.simps[simp del]
 
   335 
   321 
   336 lemma [elim]:"\<lbrakk>0 < x; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk> 
   322 lemma [elim]:"\<lbrakk>0 < x; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk> 
   344 apply(case_tac [!] j, simp_all)
 
   330 apply(case_tac [!] j, simp_all)
 
   345 apply(case_tac [!] nat, simp_all)
 
   331 apply(case_tac [!] nat, simp_all)
 
   346 done
 
   332 done
 
   347 
   333 
   348 lemma [simp]: "inv_loop6_loop x (b, Oc # Bk # list) = False"
 
   334 lemma [simp]: "inv_loop6_loop x (b, Oc # Bk # list) = False"
 
   349 apply(auto simp: inv_loop6_loop.simps)
 
   335 by (auto simp: inv_loop6_loop.simps)
 
   350 done
 
       
   351 
   336 
   352 lemma [elim]: "\<lbrakk>x > 0; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow> 
   337 lemma [elim]: "\<lbrakk>x > 0; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow> 
   353   inv_loop6_exit x (tl b, Oc # Bk # list)"
 
   338   inv_loop6_exit x (tl b, Oc # Bk # list)"
 
   354 apply(simp only: inv_loop5_exit.simps inv_loop6_exit.simps)
 
   339 apply(simp only: inv_loop5_exit.simps inv_loop6_exit.simps)
 
   355 apply(erule_tac exE)+
 
   340 apply(erule_tac exE)+
 
   368                 inv_loop6_exit.simps)
 
   353                 inv_loop6_exit.simps)
 
   369 apply(auto)
 
   354 apply(auto)
 
   370 done
 
   355 done
 
   371 
   356 
   372 lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
 
   357 lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
 
   373 apply(simp)
 
   358 by (simp)
 
   374 done
 
       
   375 
   359 
   376 lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"
 
   360 lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"
 
   377 apply(simp add: inv_loop6_exit.simps)
 
   361 by (simp add: inv_loop6_exit.simps)
 
   378 done
 
       
   379 
   362 
   380 lemma [elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk>
 
   363 lemma [elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk>
 
   381               \<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"
 
   364               \<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"
 
   382 apply(simp only: inv_loop6_loop.simps)
 
   365 apply(simp only: inv_loop6_loop.simps)
 
   383 apply(erule_tac exE)+
 
   366 apply(erule_tac exE)+
 
   403 apply(auto simp: inv_loop1.simps inv_loop2.simps)
 
   386 apply(auto simp: inv_loop1.simps inv_loop2.simps)
 
   404 apply(rule_tac x = "Suc i" in exI, auto)
 
   387 apply(rule_tac x = "Suc i" in exI, auto)
 
   405 done
 
   388 done
 
   406 
   389 
   407 lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (b, Bk # list)"
 
   390 lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (b, Bk # list)"
 
   408 apply(auto simp: inv_loop2.simps)
 
   391 by (auto simp: inv_loop2.simps)
 
   409 done
 
       
   410 
   392 
   411 lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"
 
   393 lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"
 
   412 apply(auto simp: inv_loop3.simps inv_loop4.simps)
 
   394 apply(auto simp: inv_loop3.simps inv_loop4.simps)
 
   413 apply(rule_tac [!] x = i in exI, auto)
 
   395 apply(rule_tac [!] x = i in exI, auto)
 
   414 apply(rule_tac [!] x = "Suc 0" in exI, rule_tac [!] x = "j - 1" in exI, auto)
 
   396 apply(rule_tac [!] x = "Suc 0" in exI, rule_tac [!] x = "j - 1" in exI, auto)
 
   422 apply(rule_tac [!] x = "Suc k" in exI, rule_tac [!] x = "t - 1" in exI, auto)
 
   404 apply(rule_tac [!] x = "Suc k" in exI, rule_tac [!] x = "t - 1" in exI, auto)
 
   423 apply(case_tac [!] t, simp_all)
 
   405 apply(case_tac [!] t, simp_all)
 
   424 done
 
   406 done
 
   425 
   407 
   426 lemma [simp]: "inv_loop5 x ([], list) = False"
 
   408 lemma [simp]: "inv_loop5 x ([], list) = False"
 
   427 apply(auto simp: inv_loop5.simps inv_loop5_exit.simps inv_loop5_loop.simps)
 
   409 by (auto simp: inv_loop5.simps inv_loop5_exit.simps inv_loop5_loop.simps)
 
   428 done
 
       
   429 
   410 
   430 lemma [simp]: "inv_loop5_exit x (b, Oc # list) = False"
 
   411 lemma [simp]: "inv_loop5_exit x (b, Oc # list) = False"
 
   431 apply(auto simp: inv_loop5_exit.simps)
 
   412 by (auto simp: inv_loop5_exit.simps)
 
   432 done
 
       
   433 
   413 
   434 lemma [elim]: " \<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk>
 
   414 lemma [elim]: " \<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk>
 
   435   \<Longrightarrow> inv_loop5_exit x (tl b, Bk # Oc # list)"
 
   415   \<Longrightarrow> inv_loop5_exit x (tl b, Bk # Oc # list)"
 
   436 apply(simp only: inv_loop5_loop.simps inv_loop5_exit.simps)
 
   416 apply(simp only: inv_loop5_loop.simps inv_loop5_exit.simps)
 
   437 apply(erule_tac exE)+
 
   417 apply(erule_tac exE)+
 
   446 apply(rule_tac x = i in exI, rule_tac x = j in exI)
 
   426 apply(rule_tac x = i in exI, rule_tac x = j in exI)
 
   447 apply(rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI, auto)
 
   427 apply(rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI, auto)
 
   448 apply(case_tac [!] k, auto)
 
   428 apply(case_tac [!] k, auto)
 
   449 done
 
   429 done
 
   450 
   430 
   451 lemma [elim]: "\<lbrakk>inv_loop5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow> 
   431 lemma [elim]: "\<lbrakk>inv_loop5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop5 x (tl b, hd b # Oc # list)"
 
   452   inv_loop5 x (tl b, hd b # Oc # list)"
 
       
   453 apply(simp add: inv_loop5.simps)
 
   432 apply(simp add: inv_loop5.simps)
 
   454 apply(case_tac "hd b", simp_all, auto)
 
   433 apply(case_tac "hd b", simp_all, auto)
 
   455 done
 
   434 done
 
   456 
   435 
   457 lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Oc # list)\<rbrakk> \<Longrightarrow> 
   436 lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_loop1 x ([], Bk # Oc # list)"
 
   458                inv_loop1 x ([], Bk # Oc # list)"
 
       
   459 apply(auto simp: inv_loop6.simps inv_loop1.simps 
   437 apply(auto simp: inv_loop6.simps inv_loop1.simps 
   460   inv_loop6_loop.simps inv_loop6_exit.simps)
 
   438   inv_loop6_loop.simps inv_loop6_exit.simps)
 
   461 done
 
   439 done
 
   462 
   440 
   463 lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Oc # list); b \<noteq> []\<rbrakk> 
   441 lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Oc # list); b \<noteq> []\<rbrakk> 
   465 apply(auto simp: inv_loop6.simps inv_loop1.simps 
   443 apply(auto simp: inv_loop6.simps inv_loop1.simps 
   466   inv_loop6_loop.simps inv_loop6_exit.simps)
 
   444   inv_loop6_loop.simps inv_loop6_exit.simps)
 
   467 done
 
   445 done
 
   468 
   446 
   469 lemma inv_loop_step: 
   447 lemma inv_loop_step: 
   470   "\<lbrakk>inv_loop x cf; x > 0\<rbrakk>
 
   448   "\<lbrakk>inv_loop x cf; x > 0\<rbrakk> \<Longrightarrow> inv_loop x (step cf (tcopy_loop, 0))"
 
   471  \<Longrightarrow> inv_loop x (step cf (tcopy_loop, 0))"
 
       
   472 apply(case_tac cf, case_tac c, case_tac [2] aa)
 
   449 apply(case_tac cf, case_tac c, case_tac [2] aa)
 
   473 apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral split: if_splits)
 
   450 apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral split: if_splits)
 
   474 done
 
   451 done
 
   475 
   452 
   476 lemma inv_loop_steps:
 
   453 lemma inv_loop_steps:
 
   515 definition loop_LE :: "(config \<times> config) set"
 
   492 definition loop_LE :: "(config \<times> config) set"
 
   516   where
 
   493   where
 
   517    "loop_LE \<equiv> (inv_image lex_triple loop_measure)"
 
   494    "loop_LE \<equiv> (inv_image lex_triple loop_measure)"
 
   518 
   495 
   519 lemma wf_loop_le: "wf loop_LE"
 
   496 lemma wf_loop_le: "wf loop_LE"
 
   520 by(auto intro:wf_inv_image simp: loop_LE_def wf_lex_triple)
 
   497 by (auto intro:wf_inv_image simp: loop_LE_def wf_lex_triple)
 
   521 
   498 
   522 lemma [simp]: "inv_loop2 x ([], b) = False"
 
   499 lemma [simp]: "inv_loop2 x ([], b) = False"
 
   523 apply(auto simp: inv_loop2.simps)
 
   500 by (auto simp: inv_loop2.simps)
 
   524 done
 
       
   525 
   501 
   526 lemma  [simp]: "inv_loop2 x (l', []) = False"
 
   502 lemma  [simp]: "inv_loop2 x (l', []) = False"
 
   527 apply(auto simp: inv_loop2.simps)
 
   503 by (auto simp: inv_loop2.simps)
 
   528 done
 
       
   529 
   504 
   530 lemma [simp]: "inv_loop3 x (b, []) = False"
 
   505 lemma [simp]: "inv_loop3 x (b, []) = False"
 
   531 apply(auto simp: inv_loop3.simps)
 
   506 by (auto simp: inv_loop3.simps)
 
   532 done
 
       
   533 
   507 
   534 lemma [simp]: "inv_loop4 x ([], b) = False"
 
   508 lemma [simp]: "inv_loop4 x ([], b) = False"
 
   535 apply(auto simp: inv_loop4.simps)
 
   509 by (auto simp: inv_loop4.simps)
 
   536 done
 
       
   537 
   510 
   538 lemma [elim]: 
   511 lemma [elim]: 
   539   "\<lbrakk>inv_loop4 x (l', []); l' \<noteq> []; x > 0;
 
   512   "\<lbrakk>inv_loop4 x (l', []); l' \<noteq> []; x > 0;
 
   540   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ [Oc])) \<noteq> 
   513   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ [Oc])) \<noteq> 
   541   length (takeWhile (\<lambda>a. a = Oc) (rev l'))\<rbrakk>
 
   514   length (takeWhile (\<lambda>a. a = Oc) (rev l'))\<rbrakk>
 
   549   "\<lbrakk>inv_loop4 x (l', Bk # list); l' \<noteq> []; 0 < x;
 
   522   "\<lbrakk>inv_loop4 x (l', Bk # list); l' \<noteq> []; 0 < x;
 
   550    length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) \<noteq> 
   523    length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) \<noteq> 
   551     length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
 
   524     length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
 
   552     \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) < 
   525     \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) < 
   553     length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"
 
   526     length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"
 
   554 apply(auto simp: inv_loop4.simps)
 
   527 by (auto simp: inv_loop4.simps)
 
   555 done
 
       
   556 
   528 
   557 lemma takeWhile_replicate_append: 
   529 lemma takeWhile_replicate_append: 
   558   "P a \<Longrightarrow> takeWhile P (a\<up>x @ ys) = a\<up>x @ takeWhile P ys"
 
   530   "P a \<Longrightarrow> takeWhile P (a\<up>x @ ys) = a\<up>x @ takeWhile P ys"
 
   559 apply(induct x, auto)
 
   531 by (induct x, auto)
 
   560 done
 
       
   561 
   532 
   562 lemma takeWhile_replicate: 
   533 lemma takeWhile_replicate: 
   563   "P a \<Longrightarrow> takeWhile P (a\<up>x) = a\<up>x"
 
   534   "P a \<Longrightarrow> takeWhile P (a\<up>x) = a\<up>x"
 
   564 by(induct x, auto)
 
   535 by (induct x, auto)
 
   565 
   536 
   566 lemma [elim]: 
   537 lemma [elim]: 
   567    "\<lbrakk>inv_loop5 x (l', Bk # list); l' \<noteq> []; 0 < x;
 
   538    "\<lbrakk>inv_loop5 x (l', Bk # list); l' \<noteq> []; 0 < x;
 
   568    length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \<noteq>
 
   539    length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \<noteq>
 
   569    length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
 
   540    length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
 
   576 apply(simp add: takeWhile_replicate_append takeWhile_replicate)
 
   547 apply(simp add: takeWhile_replicate_append takeWhile_replicate)
 
   577 apply(case_tac  nata, simp_all add: List.takeWhile_tail)
 
   548 apply(case_tac  nata, simp_all add: List.takeWhile_tail)
 
   578 done
 
   549 done
 
   579 
   550 
   580 lemma [elim]: "\<lbrakk>inv_loop1 x (l', Oc # list)\<rbrakk> \<Longrightarrow> hd list = Oc"
 
   551 lemma [elim]: "\<lbrakk>inv_loop1 x (l', Oc # list)\<rbrakk> \<Longrightarrow> hd list = Oc"
 
   581 apply(auto simp: inv_loop1.simps)
 
   552 by (auto simp: inv_loop1.simps)
 
   582 done
 
       
   583 
   553 
   584 lemma [elim]: 
   554 lemma [elim]: 
   585   "\<lbrakk>inv_loop6 x (l', Bk # list); l' \<noteq> []; 0 < x;
 
   555   "\<lbrakk>inv_loop6 x (l', Bk # list); l' \<noteq> []; 0 < x;
 
   586   length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \<noteq> 
   556   length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \<noteq> 
   587   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
 
   557   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
 
   678     done
 
   648     done
 
   679 qed
 
   649 qed
 
   680 
   650 
   681 
   651 
   682 (* tcopy_end *)
 
   652 (* tcopy_end *)
 
   683   
   653 
   684 fun inv_end1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 
   654 fun
 
   685   where
 
   655   inv_end5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   686   "inv_end1 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x)"
 
   656   inv_end5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" 
   687 
   657 where  
   688 fun inv_end2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 
       
   689   where
 
       
   690   "inv_end2 x (l, r) = (\<exists> i j. i + j = Suc x \<and> x > 0 \<and> l = Oc\<up>i @ [Bk] \<and> r = Bk\<up>j @ Oc\<up>x)"
 
       
   691 
       
   692 fun inv_end3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 
       
   693   where
 
       
   694   "inv_end3 x (l, r) =
 
       
   695         (\<exists> i j. x > 0 \<and> i + j = x \<and> l = Oc\<up>i @ [Bk] \<and> r = Oc # Bk\<up>j@ Oc\<up>x )"
 
       
   696 
       
   697 fun inv_end4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 
       
   698   where
 
       
   699   "inv_end4 x (l, r) = (\<exists> any. x > 0 \<and> l = Oc\<up>x @ [Bk] \<and> r = any#Oc\<up>x)"
 
       
   700 
       
   701 fun inv_end5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 
       
   702   where
 
       
   703   "inv_end5_loop x (l, r) = 
   658   "inv_end5_loop x (l, r) = 
   704          (\<exists> i j. i + j = x \<and> x > 0 \<and> j > 0 \<and> l = Oc\<up>i @ [Bk] \<and> r = Oc\<up>j @ Bk # Oc\<up>x)"
 
   659      (\<exists> i j. i + j = x \<and> x > 0 \<and> j > 0 \<and> l = Oc\<up>i @ [Bk] \<and> r = Oc\<up>j @ Bk # Oc\<up>x)"
 
   705 
   660 | "inv_end5_exit x (l, r) = (x > 0 \<and> l = [] \<and> r = Bk # Oc\<up>x @ Bk # Oc\<up>x)"
 
   706 fun inv_end5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 
   661 
   707   where
 
   662 fun 
   708   "inv_end5_exit x (l, r) = (x > 0 \<and> l = [] \<and> r = Bk # Oc\<up>x @ Bk # Oc\<up>x)"
 
   663   inv_end0 :: "nat \<Rightarrow> tape \<Rightarrow>  bool" and
 
   709 
   664   inv_end1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   710 fun inv_end5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 
   665   inv_end2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   711   where
 
   666   inv_end3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   712   "inv_end5 x (l, r) = (inv_end5_loop x (l, r) \<or> inv_end5_exit x (l, r))"
 
   667   inv_end4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
 
   713 
   668  
   714 fun inv_end0 :: "nat \<Rightarrow> tape \<Rightarrow>  bool"
 
   669   inv_end5 :: "nat \<Rightarrow> tape \<Rightarrow> bool" 
   715   where
 
   670 where
 
   716   "inv_end0 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc\<up>x @ Bk # Oc\<up>x)"
 
   671   "inv_end0 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc\<up>x @ Bk # Oc\<up>x)"
 
   717 
   672 | "inv_end1 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x)"
 
   718 fun inv_end :: "nat \<Rightarrow> config \<Rightarrow> bool"
 
   673 | "inv_end2 x (l, r) = (\<exists> i j. i + j = Suc x \<and> x > 0 \<and> l = Oc\<up>i @ [Bk] \<and> r = Bk\<up>j @ Oc\<up>x)"
 
   719   where
 
   674 | "inv_end3 x (l, r) =
 
       
   675      (\<exists> i j. x > 0 \<and> i + j = x \<and> l = Oc\<up>i @ [Bk] \<and> r = Oc # Bk\<up>j@ Oc\<up>x)"
 
       
   676 | "inv_end4 x (l, r) = (\<exists> any. x > 0 \<and> l = Oc\<up>x @ [Bk] \<and> r = any#Oc\<up>x)"
 
       
   677 | "inv_end5 x (l, r) = (inv_end5_loop x (l, r) \<or> inv_end5_exit x (l, r))"
 
       
   678 
       
   679 fun 
       
   680   inv_end :: "nat \<Rightarrow> config \<Rightarrow> bool"
 
       
   681 where
 
   720   "inv_end x (s, l, r) = (if s = 0 then inv_end0 x (l, r)
 
   682   "inv_end x (s, l, r) = (if s = 0 then inv_end0 x (l, r)
 
   721                           else if s = 1 then inv_end1 x (l, r)
 
   683                           else if s = 1 then inv_end1 x (l, r)
 
   722                           else if s = 2 then inv_end2 x (l, r)
 
   684                           else if s = 2 then inv_end2 x (l, r)
 
   723                           else if s = 3 then inv_end3 x (l, r)
 
   685                           else if s = 3 then inv_end3 x (l, r)
 
   724                           else if s = 4 then inv_end4 x (l, r)
 
   686                           else if s = 4 then inv_end4 x (l, r)
 
   729         inv_end0.simps[simp del] inv_end2.simps[simp del]
 
   691         inv_end0.simps[simp del] inv_end2.simps[simp del]
 
   730         inv_end3.simps[simp del] inv_end4.simps[simp del]
 
   692         inv_end3.simps[simp del] inv_end4.simps[simp del]
 
   731         inv_end5.simps[simp del]
 
   693         inv_end5.simps[simp del]
 
   732 
   694 
   733 lemma [simp]:  "inv_end1 x (b, []) = False"
 
   695 lemma [simp]:  "inv_end1 x (b, []) = False"
 
   734 apply(auto simp: inv_end1.simps)
 
   696 by (auto simp: inv_end1.simps)
 
   735 done
 
       
   736 
   697 
   737 lemma [simp]: "inv_end2 x (b, []) = False"
 
   698 lemma [simp]: "inv_end2 x (b, []) = False"
 
   738 apply(auto simp: inv_end2.simps)
 
   699 by (auto simp: inv_end2.simps)
 
   739 done
 
       
   740 
   700 
   741 lemma [simp]: "inv_end3 x (b, []) = False"
 
   701 lemma [simp]: "inv_end3 x (b, []) = False"
 
   742 apply(auto simp: inv_end3.simps)
 
   702 by (auto simp: inv_end3.simps)
 
   743 done
 
   703 
   744 
       
   745 thm inv_end4.simps
 
       
   746 lemma [simp]: "inv_end4 x (b, []) = False"
 
   704 lemma [simp]: "inv_end4 x (b, []) = False"
 
   747 apply(auto simp: inv_end4.simps)
 
   705 by (auto simp: inv_end4.simps)
 
   748 done
 
       
   749 
   706 
   750 lemma [simp]: "inv_end5 x (b, []) = False"
 
   707 lemma [simp]: "inv_end5 x (b, []) = False"
 
   751 apply(auto simp: inv_end5.simps)
 
   708 by (auto simp: inv_end5.simps)
 
   752 done
 
       
   753 
   709 
   754 lemma [simp]: "inv_end1 x ([], list) = False"
 
   710 lemma [simp]: "inv_end1 x ([], list) = False"
 
   755 apply(auto simp: inv_end1.simps)
 
   711 by (auto simp: inv_end1.simps)
 
   756 done
 
       
   757 
   712 
   758 lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Bk # list); b \<noteq> []\<rbrakk>
 
   713 lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Bk # list); b \<noteq> []\<rbrakk>
 
   759   \<Longrightarrow> inv_end0 x (tl b, hd b # Bk # list)"
 
   714   \<Longrightarrow> inv_end0 x (tl b, hd b # Bk # list)"
 
   760 apply(auto simp: inv_end1.simps inv_end0.simps)
 
   715 by (auto simp: inv_end1.simps inv_end0.simps)
 
   761 done
 
       
   762 
   716 
   763 lemma [elim]: "\<lbrakk>0 < x; inv_end2 x (b, Bk # list)\<rbrakk> 
   717 lemma [elim]: "\<lbrakk>0 < x; inv_end2 x (b, Bk # list)\<rbrakk> 
   764   \<Longrightarrow> inv_end3 x (b, Oc # list)"
 
   718   \<Longrightarrow> inv_end3 x (b, Oc # list)"
 
   765 apply(auto simp: inv_end2.simps inv_end3.simps)
 
   719 apply(auto simp: inv_end2.simps inv_end3.simps)
 
   766 apply(rule_tac x = "j - 1" in exI)
 
   720 apply(rule_tac x = "j - 1" in exI)
 
   767 apply(case_tac j, simp_all)
 
   721 apply(case_tac j, simp_all)
 
   768 apply(case_tac x, simp_all)
 
   722 apply(case_tac x, simp_all)
 
   769 done
 
   723 done
 
   770 
   724 
   771 lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Bk # b, list)"
 
   725 lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Bk # b, list)"
 
   772 apply(auto simp: inv_end2.simps inv_end3.simps)
 
   726 by (auto simp: inv_end2.simps inv_end3.simps)
 
   773 done
 
       
   774   
   727   
   775 lemma [elim]: "\<lbrakk>0 < x; inv_end4 x ([], Bk # list)\<rbrakk> \<Longrightarrow> 
   728 lemma [elim]: "\<lbrakk>0 < x; inv_end4 x ([], Bk # list)\<rbrakk> \<Longrightarrow> 
   776   inv_end5 x ([], Bk # Bk # list)"
 
   729   inv_end5 x ([], Bk # Bk # list)"
 
   777 apply(auto simp: inv_end4.simps inv_end5.simps)
 
   730 by (auto simp: inv_end4.simps inv_end5.simps)
 
   778 done
 
       
   779  
   731  
   780 lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> 
   732 lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> 
   781   inv_end5 x (tl b, hd b # Bk # list)"
 
   733   inv_end5 x (tl b, hd b # Bk # list)"
 
   782 apply(auto simp: inv_end4.simps inv_end5.simps)
 
   734 apply(auto simp: inv_end4.simps inv_end5.simps)
 
   783 apply(rule_tac x = 1 in exI, simp)
 
   735 apply(rule_tac x = 1 in exI, simp)
 
   787 apply(auto simp: inv_end5.simps inv_end0.simps)
 
   739 apply(auto simp: inv_end5.simps inv_end0.simps)
 
   788 apply(case_tac [!] j, simp_all)
 
   740 apply(case_tac [!] j, simp_all)
 
   789 done
 
   741 done
 
   790 
   742 
   791 lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
 
   743 lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
 
   792 apply(auto simp: inv_end1.simps inv_end2.simps)
 
   744 by (auto simp: inv_end1.simps inv_end2.simps)
 
   793 done
 
       
   794 
   745 
   795 lemma [elim]: "\<lbrakk>0 < x; inv_end2 x ([], Oc # list)\<rbrakk> \<Longrightarrow>
 
   746 lemma [elim]: "\<lbrakk>0 < x; inv_end2 x ([], Oc # list)\<rbrakk> \<Longrightarrow>
 
   796                inv_end4 x ([], Bk # Oc # list)"
 
   747                inv_end4 x ([], Bk # Oc # list)"
 
   797 apply(auto simp: inv_end2.simps inv_end4.simps)
 
   748 by (auto simp: inv_end2.simps inv_end4.simps)
 
   798 done
 
       
   799 
   749 
   800 lemma [elim]:  "\<lbrakk>0 < x; inv_end2 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
 
   750 lemma [elim]:  "\<lbrakk>0 < x; inv_end2 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
 
   801   inv_end4 x (tl b, hd b # Oc # list)"
 
   751   inv_end4 x (tl b, hd b # Oc # list)"
 
   802 apply(auto simp: inv_end2.simps inv_end4.simps)
 
   752 apply(auto simp: inv_end2.simps inv_end4.simps)
 
   803 apply(case_tac [!] j, simp_all)
 
   753 apply(case_tac [!] j, simp_all)
 
   804 done
 
   754 done
 
   805 
   755 
   806 lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
 
   756 lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
 
   807 apply(auto simp: inv_end2.simps inv_end3.simps)
 
   757 by (auto simp: inv_end2.simps inv_end3.simps)
 
   808 done
 
       
   809 
   758 
   810 lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end4 x (b, Bk # list)"
 
   759 lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end4 x (b, Bk # list)"
 
   811 apply(auto simp: inv_end2.simps inv_end4.simps)
 
   760 by (auto simp: inv_end2.simps inv_end4.simps)
 
   812 done
 
       
   813 
   761 
   814 lemma [elim]: "\<lbrakk>0 < x; inv_end5 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_end5 x ([], Bk # Oc # list)"
 
   762 lemma [elim]: "\<lbrakk>0 < x; inv_end5 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_end5 x ([], Bk # Oc # list)"
 
   815 apply(auto simp: inv_end2.simps inv_end5.simps)
 
   763 by (auto simp: inv_end2.simps inv_end5.simps)
 
   816 done
 
       
   817 
   764 
   818 declare inv_end5_loop.simps[simp del]
 
   765 declare inv_end5_loop.simps[simp del]
 
   819         inv_end5_exit.simps[simp del]
 
   766         inv_end5_exit.simps[simp del]
 
   820 
   767 
   821 lemma [simp]: "inv_end5_exit x (b, Oc # list) = False"
 
   768 lemma [simp]: "inv_end5_exit x (b, Oc # list) = False"
 
   822 apply(auto simp: inv_end5_exit.simps)
 
   769 by (auto simp: inv_end5_exit.simps)
 
   823 done
 
       
   824 
   770 
   825 lemma [simp]: "inv_end5_loop x (tl b, Bk # Oc # list) = False"
 
   771 lemma [simp]: "inv_end5_loop x (tl b, Bk # Oc # list) = False"
 
   826 apply(auto simp: inv_end5_loop.simps)
 
   772 apply(auto simp: inv_end5_loop.simps)
 
   827 apply(case_tac [!] j, simp_all)
 
   773 apply(case_tac [!] j, simp_all)
 
   828 done
 
   774 done
 
   849 apply(simp add: inv_end2.simps inv_end5.simps)
 
   795 apply(simp add: inv_end2.simps inv_end5.simps)
 
   850 apply(case_tac "hd b", simp_all, auto)
 
   796 apply(case_tac "hd b", simp_all, auto)
 
   851 done
 
   797 done
 
   852 
   798 
   853 lemma inv_end_step:
 
   799 lemma inv_end_step:
 
   854   "\<lbrakk>x > 0;
 
   800   "\<lbrakk>x > 0; inv_end x cf\<rbrakk> \<Longrightarrow> inv_end x (step cf (tcopy_end, 0))"
 
   855  inv_end x cf\<rbrakk>
 
       
   856  \<Longrightarrow> inv_end x (step cf (tcopy_end, 0))"
 
       
   857 apply(case_tac cf, case_tac c, case_tac [2] aa)
 
   801 apply(case_tac cf, case_tac c, case_tac [2] aa)
 
   858 apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral split: if_splits)
 
   802 apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral split: if_splits)
 
   859 done
 
   803 done
 
   860 
   804 
   861 lemma inv_end_steps:
 
   805 lemma inv_end_steps:
 
   862   "\<lbrakk>x > 0; inv_end x cf\<rbrakk>
 
   806   "\<lbrakk>x > 0; inv_end x cf\<rbrakk> \<Longrightarrow> inv_end x (steps cf (tcopy_end, 0) stp)"
 
   863 \<Longrightarrow> inv_end x (steps cf (tcopy_end, 0) stp)"
 
       
   864 apply(induct stp, simp add:steps.simps, simp)
 
   807 apply(induct stp, simp add:steps.simps, simp)
 
   865 apply(erule_tac inv_end_step, simp)
 
   808 apply(erule_tac inv_end_step, simp)
 
   866 done
 
   809 done
 
   867 
   810 
   868 fun end_state :: "config \<Rightarrow> nat"
 
   811 fun end_state :: "config \<Rightarrow> nat"
 
   876         else 0)"
 
   819         else 0)"
 
   877 
   820 
   878 fun end_stage :: "config \<Rightarrow> nat"
 
   821 fun end_stage :: "config \<Rightarrow> nat"
 
   879   where
 
   822   where
 
   880   "end_stage (s, l, r) = 
   823   "end_stage (s, l, r) = 
   881           (if s = 2 \<or> s = 3 then (length r)
 
   824           (if s = 2 \<or> s = 3 then (length r) else 0)"
 
   882            else 0)"
 
       
   883 
   825 
   884 fun end_step :: "config \<Rightarrow> nat"
 
   826 fun end_step :: "config \<Rightarrow> nat"
 
   885   where
 
   827   where
 
   886   "end_step (s, l, r) = 
   828   "end_step (s, l, r) = 
   887          (if s = 4 then (if hd r = Oc then 1 else 0)
 
   829          (if s = 4 then (if hd r = Oc then 1 else 0)
 
   898 definition end_LE :: "(config \<times> config) set"
 
   840 definition end_LE :: "(config \<times> config) set"
 
   899   where
 
   841   where
 
   900    "end_LE \<equiv> (inv_image lex_triple end_measure)"
 
   842    "end_LE \<equiv> (inv_image lex_triple end_measure)"
 
   901 
   843 
   902 lemma wf_end_le: "wf end_LE"
 
   844 lemma wf_end_le: "wf end_LE"
 
   903 by(auto intro:wf_inv_image simp: end_LE_def wf_lex_triple)
 
   845 by (auto intro: wf_inv_image simp: end_LE_def wf_lex_triple)
 
   904 
   846 
   905 lemma [simp]: "inv_end5 x ([], Oc # list) = False"
 
   847 lemma [simp]: "inv_end5 x ([], Oc # list) = False"
 
   906 apply(auto simp: inv_end5.simps inv_end5_loop.simps)
 
   848 by (auto simp: inv_end5.simps inv_end5_loop.simps)
 
   907 done
 
       
   908 
   849 
   909 lemma end_halt: 
   850 lemma end_halt: 
   910   "\<lbrakk>x > 0; inv_end x (Suc 0, l, r)\<rbrakk> \<Longrightarrow> 
   851   "\<lbrakk>x > 0; inv_end x (Suc 0, l, r)\<rbrakk> \<Longrightarrow> 
   911       \<exists> stp. is_final (steps (Suc 0, l, r) (tcopy_end, 0) stp)"
 
   852       \<exists> stp. is_final (steps (Suc 0, l, r) (tcopy_end, 0) stp)"
 
   912 proof(rule_tac LE = end_LE in halt_lemma)
 
   853 proof(rule_tac LE = end_LE in halt_lemma)
 
   962 qed
 
   903 qed
 
   963 
   904 
   964 (* tcopy *)
 
   905 (* tcopy *)
 
   965 
   906 
   966 lemma [intro]: "tm_wf (tcopy_init, 0)"
 
   907 lemma [intro]: "tm_wf (tcopy_init, 0)"
 
   967 by(auto simp: tm_wf.simps tcopy_init_def)
 
   908 by (auto simp: tm_wf.simps tcopy_init_def)
 
   968 
   909 
   969 lemma [intro]: "tm_wf (tcopy_loop, 0)"
 
   910 lemma [intro]: "tm_wf (tcopy_loop, 0)"
 
   970 by(auto simp: tm_wf.simps tcopy_loop_def)
 
   911 by (auto simp: tm_wf.simps tcopy_loop_def)
 
   971 
   912 
   972 lemma [intro]: "tm_wf (tcopy_end, 0)"
 
   913 lemma [intro]: "tm_wf (tcopy_end, 0)"
 
   973 by(auto simp: tm_wf.simps tcopy_end_def)
 
   914 by (auto simp: tm_wf.simps tcopy_end_def)
 
   974 
   915 
   975 lemma [intro]: "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0)\<rbrakk> \<Longrightarrow> tm_wf (A |+| B, 0)"
 
   916 lemma [intro]: "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0)\<rbrakk> \<Longrightarrow> tm_wf (A |+| B, 0)"
 
   976 apply(auto simp: tm_wf.simps shift.simps adjust.simps tm_comp_length
 
   917 by (auto simp: tm_wf.simps shift.simps adjust.simps tm_comp_length tm_comp.simps)
 
   977                  tm_comp.simps)
 
       
   978 done
 
       
   979 
   918 
   980 lemma tcopy_correct1: 
   919 lemma tcopy_correct1: 
   981   "\<lbrakk>x > 0\<rbrakk> \<Longrightarrow> {inv_init1 x} tcopy {inv_end0 x}"
 
   920   "\<lbrakk>x > 0\<rbrakk> \<Longrightarrow> {inv_init1 x} tcopy {inv_end0 x}"
 
   982 proof(simp add: tcopy_def, rule_tac Hoare_plus_halt)
 
   921 proof(simp add: tcopy_def, rule_tac Hoare_plus_halt)
 
   983   show "inv_loop0 x \<mapsto> inv_end1 x"
 
   922   show "inv_loop0 x \<mapsto> inv_end1 x"
 
  1008   thus "{inv_end1 x} tcopy_end {inv_end0 x}"
 
   947   thus "{inv_end1 x} tcopy_end {inv_end0 x}"
 
  1009     by(erule_tac end_correct)
 
   948     by(erule_tac end_correct)
 
  1010 qed
 
   949 qed
 
  1011 
   950 
  1012 abbreviation
 
   951 abbreviation
 
  1013   "pre_tcopy n \<equiv> \<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[n::nat]>)"
 
   952   "pre_tcopy n \<equiv> \<lambda>(l::cell list, r::cell list). ((l, r) = ([], <[n::nat]>))"
 
  1014 abbreviation
 
   953 abbreviation
 
  1015   "post_tcopy n \<equiv> \<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[n, n::nat]>)"
 
   954   "post_tcopy n \<equiv> \<lambda>(l::cell list, r::cell list). ((l, r) = ([Bk], <[n, n::nat]>))"
 
  1016 
   955 
  1017 lemma tcopy_correct2:
 
   956 lemma tcopy_correct2:
 
  1018   shows "{pre_tcopy n} tcopy {post_tcopy n}"
 
   957   shows "{pre_tcopy n} tcopy {post_tcopy n}"
 
  1019 proof -
 
   958 proof -
 
  1020   have "{inv_init1 (Suc n)} tcopy {inv_end0 (Suc n)}"
 
   959   have "{inv_init1 (Suc n)} tcopy {inv_end0 (Suc n)}"
 
  1085   and the final configuration is standard.
 
  1024   and the final configuration is standard.
 
  1086 *}
 
  1025 *}
 
  1087 
  1026 
  1088 definition haltP :: "tprog \<Rightarrow> nat list \<Rightarrow> bool"
 
  1027 definition haltP :: "tprog \<Rightarrow> nat list \<Rightarrow> bool"
 
  1089   where
 
  1028   where
 
  1090   "haltP p lm \<equiv> \<exists>n a b c. steps (Suc 0, [], <lm>) p n = (0, Bk \<up> a,  Oc \<up> b @ Bk \<up> c)"
 
  1029   "haltP p lm \<equiv> \<exists>n a b c. steps (1, [], <lm>) p n = (0, Bk \<up> a,  Oc \<up> b @ Bk \<up> c)"
 
  1091 
  1030 
  1092 abbreviation
 
  1031 abbreviation
 
  1093   "haltP0 p lm \<equiv> haltP (p, 0) lm" 
  1032   "haltP0 p lm \<equiv> haltP (p, 0) lm" 
  1094 
  1033 
  1095 lemma [intro, simp]: "tm_wf0 tcopy"
 
  1034 lemma [intro, simp]: "tm_wf0 tcopy"
 
  1096 by(auto simp: tcopy_def)
 
  1035 by (auto simp: tcopy_def)
 
  1097 
  1036 
  1098 lemma [intro, simp]: "tm_wf0 dither"
 
  1037 lemma [intro, simp]: "tm_wf0 dither"
 
  1099 by (auto simp: tm_wf.simps dither_def)
 
  1038 by (auto simp: tm_wf.simps dither_def)
 
  1100 
  1039 
  1101 
  1040 
  1178   assumes h_wf[intro]: "tm_wf0 H"
 
  1117   assumes h_wf[intro]: "tm_wf0 H"
 
  1179   -- {*
 
  1118   -- {*
 
  1180   The following two assumptions specifies that @{text "H"} does solve the Halting problem.
 
  1119   The following two assumptions specifies that @{text "H"} does solve the Halting problem.
 
  1181   *}
 
  1120   *}
 
  1182   and h_case: 
  1121   and h_case: 
  1183   "\<And> M lm. (haltP0 M lm) \<Longrightarrow> \<exists> na nb. (steps0 (1, [], <code M # lm>) H na = (0, Bk \<up> nb, [Oc]))"
 
  1122   "\<And> M lm. (haltP0 M lm) \<Longrightarrow> \<exists> na nb. (steps0 (1, [Bk], <code M # lm>) H na = (0, Bk \<up> nb, [Oc]))"
 
  1184   and nh_case: 
  1123   and nh_case: 
  1185   "\<And> M lm. (\<not> haltP0 M lm) \<Longrightarrow>
 
  1124   "\<And> M lm. (\<not> haltP0 M lm) \<Longrightarrow> \<exists> na nb. (steps0 (1, [Bk], <code M # lm>) H na = (0, Bk \<up> nb, [Oc, Oc]))"
 
  1186              \<exists> na nb. (steps0 (1, [],  <code M # lm>) H na = (0, Bk \<up> nb, [Oc, Oc]))"
 
       
  1187 begin
 
  1125 begin
 
  1188 
       
  1189 lemma h_newcase: 
       
  1190   "\<And> M lm. haltP0 M lm \<Longrightarrow> \<exists> na nb. (steps0 (1, Bk \<up> x , <code M # lm>) H na = (0, Bk \<up> nb, [Oc]))"
 
       
  1191 proof -
 
       
  1192   fix M lm
 
       
  1193   assume "haltP (M, 0) lm"
 
       
  1194   hence "\<exists> na nb. (steps (1, [], <code M # lm>) (H, 0) na
 
       
  1195             = (0, Bk\<up>nb, [Oc]))"
 
       
  1196     by (rule h_case)
 
       
  1197   from this obtain na nb where 
       
  1198     cond1:"(steps (1, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc]))" by blast
 
       
  1199   thus "\<exists> na nb. (steps (1, Bk\<up>x, <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc]))"
 
       
  1200   proof(rule_tac x = na in exI, case_tac "steps (1, Bk\<up>x, <code M # lm>) (H, 0) na", simp)
 
       
  1201     fix a b c
 
       
  1202     assume cond2: "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
 
       
  1203     have "tinres (Bk\<up>nb) b \<and> [Oc] = c \<and> 0 = a"
 
       
  1204     proof(rule_tac tinres_steps)
 
       
  1205       show "tinres [] (Bk\<up>x)"
 
       
  1206         apply(simp add: tinres_def)
 
       
  1207         apply(auto)
 
       
  1208         done
 
       
  1209     next
 
       
  1210       show "(steps (1, [], <code M # lm>) (H, 0) na
 
       
  1211             = (0, Bk\<up>nb, [Oc]))"
 
       
  1212         by(simp add: cond1[simplified])
 
       
  1213     next
 
       
  1214       show "steps (1, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
 
       
  1215         by(simp add: cond2[simplified])
 
       
  1216     qed
 
       
  1217     thus "a = 0 \<and> (\<exists>nb. b = (Bk\<up>nb)) \<and> c = [Oc]"
 
       
  1218       by(auto elim: tinres_ex1)
 
       
  1219   qed
 
       
  1220 qed
 
       
  1221 
       
  1222 lemma nh_newcase: 
       
  1223   "\<And> M lm. \<not> (haltP (M, 0) lm) \<Longrightarrow> \<exists> na nb. (steps0 (1, Bk\<up>x, <code M # lm>) H na = (0, Bk\<up>nb, [Oc, Oc]))"
 
       
  1224 proof -
 
       
  1225   fix M lm
 
       
  1226   assume "\<not> haltP (M, 0) lm"
 
       
  1227   hence "\<exists> na nb. (steps (1, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
 
       
  1228     by (rule nh_case)
 
       
  1229   from this obtain na nb where 
       
  1230     cond1: "(steps (1, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))" by blast
 
       
  1231   thus "\<exists> na nb. (steps (1, Bk\<up>x, <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
 
       
  1232   proof(rule_tac x = na in exI, case_tac "steps (1, Bk\<up>x, <code M # lm>) (H, 0) na", simp)
 
       
  1233     fix a b c
 
       
  1234     assume cond2: "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
 
       
  1235     have "tinres (Bk\<up>nb) b \<and> [Oc, Oc] = c \<and> 0 = a"
 
       
  1236     proof(rule_tac tinres_steps)
 
       
  1237       show "tinres [] (Bk\<up>x)"
 
       
  1238         apply(auto simp: tinres_def)
 
       
  1239         done
 
       
  1240     next
 
       
  1241       show "(steps (Suc 0, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
 
       
  1242         by(simp add: cond1[simplified])
 
       
  1243     next
 
       
  1244       show "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
 
       
  1245         by(simp add: cond2[simplified])
 
       
  1246     qed
 
       
  1247     thus "a = 0 \<and> (\<exists>nb. b =  Bk\<up>nb) \<and> c = [Oc, Oc]"
 
       
  1248       by(auto elim: tinres_ex1)
 
       
  1249   qed
 
       
  1250 qed
 
       
  1251 
       
  1252 
  1126 
  1253 (* invariants for H *)
 
  1127 (* invariants for H *)
 
  1254 abbreviation
 
  1128 abbreviation
 
  1255   "pre_H_inv M n \<equiv> \<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code M, n]>)"
 
  1129   "pre_H_inv M n \<equiv> \<lambda>(l::cell list, r::cell list). ((l, r) = ([Bk], <[code M, n]>))"
 
  1256 
  1130 
  1257 abbreviation
 
  1131 abbreviation
 
  1258   "post_H_halt_inv \<equiv> \<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]"
 
  1132   "post_H_halt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc, Oc]))"
 
  1259 
  1133 
  1260 abbreviation
 
  1134 abbreviation
 
  1261   "post_H_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]"
 
  1135   "post_H_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc]))"
 
  1262 
  1136 
  1263 
  1137 
  1264 lemma H_halt_inv:
 
  1138 lemma H_halt_inv:
 
  1265   assumes "\<not> haltP0 M [n]" 
  1139   assumes "\<not> haltP0 M [n]" 
  1266   shows "{pre_H_inv M n} H {post_H_halt_inv}"
 
  1140   shows "{pre_H_inv M n} H {post_H_halt_inv}"
 
  1267 proof -
 
  1141 proof -
 
  1268   obtain stp i
 
  1142   obtain stp i
 
  1269     where "steps0 (1, Bk \<up> 1, <[code M, n]>) H stp = (0, Bk \<up> i, [Oc, Oc])"
 
  1143     where "steps0 (1, [Bk], <[code M, n]>) H stp = (0, Bk \<up> i, [Oc, Oc])"
 
  1270     using nh_newcase[of "M" "[n]" "1", OF assms] by auto 
  1144     using nh_case[of "M" "[n]", OF assms] by auto
 
  1271   then show "{pre_H_inv M n} H {post_H_halt_inv}"
 
  1145   then show "{pre_H_inv M n} H {post_H_halt_inv}"
 
  1272     unfolding Hoare_halt_def
 
  1146     unfolding Hoare_halt_def
 
  1273     apply(auto)
 
  1147     apply(auto)
 
  1274     apply(rule_tac x = stp in exI)
 
  1148     apply(rule_tac x = stp in exI)
 
  1275     apply(auto)
 
  1149     apply(auto)
 
  1279 lemma H_unhalt_inv:
 
  1153 lemma H_unhalt_inv:
 
  1280   assumes "haltP0 M [n]" 
  1154   assumes "haltP0 M [n]" 
  1281   shows "{pre_H_inv M n} H {post_H_unhalt_inv}"
 
  1155   shows "{pre_H_inv M n} H {post_H_unhalt_inv}"
 
  1282 proof -
 
  1156 proof -
 
  1283   obtain stp i
 
  1157   obtain stp i
 
  1284     where "steps0 (1, Bk \<up> 1, <[code M, n]>) H stp = (0, Bk \<up> i, [Oc])"
 
  1158     where "steps0 (1, [Bk], <[code M, n]>) H stp = (0, Bk \<up> i, [Oc])"
 
  1285     using h_newcase[of "M" "[n]" "1", OF assms] by auto 
  1159     using h_case[of "M" "[n]", OF assms] by auto 
  1286   then show "{pre_H_inv M n} H {post_H_unhalt_inv}"
 
  1160   then show "{pre_H_inv M n} H {post_H_unhalt_inv}"
 
  1287     unfolding Hoare_halt_def
 
  1161     unfolding Hoare_halt_def
 
  1288     apply(auto)
 
  1162     apply(auto)
 
  1289     apply(rule_tac x = stp in exI)
 
  1163     apply(rule_tac x = stp in exI)
 
  1290     apply(auto)
 
  1164     apply(auto)
 
  1321   (* {P1} (tcopy |+| H) {P3} *)
 
  1195   (* {P1} (tcopy |+| H) {P3} *)
 
  1322   have first: "{P1} (tcopy |+| H) {P3}" 
  1196   have first: "{P1} (tcopy |+| H) {P3}" 
  1323   proof (cases rule: Hoare_plus_halt_simple)
 
  1197   proof (cases rule: Hoare_plus_halt_simple)
 
  1324     case A_halt (* of tcopy *)
 
  1198     case A_halt (* of tcopy *)
 
  1325     show "{P1} tcopy {P2}" unfolding P1_def P2_def
 
  1199     show "{P1} tcopy {P2}" unfolding P1_def P2_def
 
  1326       by (simp) (rule tcopy_correct2)
 
  1200       by (rule tcopy_correct2)
 
  1327   next
 
  1201   next
 
  1328     case B_halt (* of H *)
 
  1202     case B_halt (* of H *)
 
  1329     show "{P2} H {P3}"
 
  1203     show "{P2} H {P3}"
 
  1330       unfolding P2_def P3_def
 
  1204       unfolding P2_def P3_def
 
  1331       using assms by (simp) (rule H_halt_inv)
 
  1205       using assms by (rule H_halt_inv)
 
  1332   qed (simp)
 
  1206   qed (simp)
 
  1333 
  1207 
  1334   (* {P3} dither {P3} *)
 
  1208   (* {P3} dither {P3} *)
 
  1335   have second: "{P3} dither {P3}" unfolding P3_def 
  1209   have second: "{P3} dither {P3}" unfolding P3_def 
  1336     by (rule dither_halts)
 
  1210     by (rule dither_halts)
 
  1375   (* {P1} (tcopy |+| H) {P3} *)
 
  1249   (* {P1} (tcopy |+| H) {P3} *)
 
  1376   have first: "{P1} (tcopy |+| H) {P3}" 
  1250   have first: "{P1} (tcopy |+| H) {P3}" 
  1377   proof (cases rule: Hoare_plus_halt_simple)
 
  1251   proof (cases rule: Hoare_plus_halt_simple)
 
  1378     case A_halt (* of tcopy *)
 
  1252     case A_halt (* of tcopy *)
 
  1379     show "{P1} tcopy {P2}" unfolding P1_def P2_def
 
  1253     show "{P1} tcopy {P2}" unfolding P1_def P2_def
 
  1380       by (simp) (rule tcopy_correct2)
 
  1254       by (rule tcopy_correct2)
 
  1381   next
 
  1255   next
 
  1382     case B_halt (* of H *)
 
  1256     case B_halt (* of H *)
 
  1383     then show "{P2} H {P3}"
 
  1257     then show "{P2} H {P3}"
 
  1384       unfolding P2_def P3_def
 
  1258       unfolding P2_def P3_def
 
  1385       using assms by (simp) (rule H_unhalt_inv)
 
  1259       using assms by (rule H_unhalt_inv)
 
  1386   qed (simp)
 
  1260   qed (simp)
 
  1387 
  1261 
  1388   (* {P3} dither loops *)
 
  1262   (* {P3} dither loops *)
 
  1389   have second: "{P3} dither \<up>" unfolding P3_def 
  1263   have second: "{P3} dither \<up>" unfolding P3_def 
  1390     by (rule dither_loops)
 
  1264     by (rule dither_loops)
tm