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 291 93db7414931d
parent 288 a9003e6d0463
child 292 293e9c6f22e1
equal deleted inserted replaced
290:6e1c03614d36 291:93db7414931d 
    75          if s = 2 then inv_begin2 n tp else
 
    75          if s = 2 then inv_begin2 n tp else
 
    76          if s = 3 then inv_begin3 n tp else
 
    76          if s = 3 then inv_begin3 n tp else
 
    77          if s = 4 then inv_begin4 n tp 
    77          if s = 4 then inv_begin4 n tp 
    78          else False)"
 
    78          else False)"
 
    79 
    79 
    80 lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> 
    80 lemma inv_begin_step_E: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> 
    81   \<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia"
 
    81   \<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia"
 
    82 by (rule_tac x = "Suc i" in exI, simp)
 
    82 by (rule_tac x = "Suc i" in exI, simp)
 
    83 
    83 
    84 lemma inv_begin_step: 
    84 lemma inv_begin_step: 
    85   assumes "inv_begin n cf"
 
    85   assumes "inv_begin n cf"
 
    86   and "n > 0"
 
    86   and "n > 0"
 
    87   shows "inv_begin n (step0 cf tcopy_begin)"
 
    87   shows "inv_begin n (step0 cf tcopy_begin)"
 
    88 using assms
 
    88 using assms
 
    89 unfolding tcopy_begin_def
 
    89 unfolding tcopy_begin_def
 
    90 apply(cases cf)
 
    90 apply(cases cf)
 
    91 apply(auto simp: numeral split: if_splits)
 
    91 apply(auto simp: numeral split: if_splits elim:inv_begin_step_E)
 
    92 apply(case_tac "hd c")
 
    92 apply(case_tac "hd c")
 
    93 apply(auto)
 
    93 apply(auto)
 
    94 apply(case_tac c)
 
    94 apply(case_tac c)
 
    95 apply(simp_all)
 
    95 apply(simp_all)
 
    96 done
 
    96 done
 
   237 declare inv_loop.simps[simp del] inv_loop1.simps[simp del]
 
   237 declare inv_loop.simps[simp del] inv_loop1.simps[simp del]
 
   238         inv_loop2.simps[simp del] inv_loop3.simps[simp del] 
   238         inv_loop2.simps[simp del] inv_loop3.simps[simp del] 
   239         inv_loop4.simps[simp del] inv_loop5.simps[simp del] 
   239         inv_loop4.simps[simp del] inv_loop5.simps[simp del] 
   240         inv_loop6.simps[simp del]
 
   240         inv_loop6.simps[simp del]
 
   241 
   241 
   242 lemma [elim]: "Bk # list = Oc \<up> t \<Longrightarrow> RR"
 
   242 lemma Bk_no_Oc_repeatE[elim]: "Bk # list = Oc \<up> t \<Longrightarrow> RR"
 
   243 by (case_tac t, auto)
 
   243 by (case_tac t, auto)
 
   244 
   244 
   245 lemma [simp]: "inv_loop1 x (b, []) = False"
 
   245 lemma inv_loop3_Bk_empty_via_2[elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
 
   246 by (simp add: inv_loop1.simps)
 
       
   247 
       
   248 lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
 
       
   249 by (auto simp: inv_loop2.simps inv_loop3.simps)
 
   246 by (auto simp: inv_loop2.simps inv_loop3.simps)
 
   250 
   247 
   251 
   248 lemma inv_loop3_Bk_empty[elim]: "\<lbrakk>0 < x; inv_loop3 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
 
   252 lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
 
       
   253 by (auto simp: inv_loop3.simps)
 
   249 by (auto simp: inv_loop3.simps)
 
   254 
   250 
   255 
   251 lemma inv_loop5_Oc_empty_via_4[elim]: "\<lbrakk>0 < x; inv_loop4 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop5 x (b, [Oc])"
 
   256 lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop5 x (b, [Oc])"
 
       
   257 apply(auto simp: inv_loop4.simps inv_loop5.simps)
 
   252 apply(auto simp: inv_loop4.simps inv_loop5.simps)
 
   258 apply(rule_tac [!] x = i in exI, 
   253 apply(rule_tac [!] x = i in exI, 
   259       rule_tac [!] x  = "Suc j" in exI, simp_all)
 
   254       rule_tac [!] x  = "Suc j" in exI, simp_all)
 
   260 done
 
   255 done
 
   261 
   256 
   262 lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], [])\<rbrakk> \<Longrightarrow> RR"
 
   257 lemma inv_loop1_Bk[elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> list = Oc # Bk \<up> x @ Oc \<up> x"
 
   263 by (auto simp: inv_loop4.simps inv_loop5.simps)
 
       
   264 
       
   265 lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, []); b \<noteq> []\<rbrakk> \<Longrightarrow> RR"
 
       
   266 by (auto simp: inv_loop4.simps inv_loop5.simps)
 
       
   267 
       
   268 lemma [elim]: "inv_loop6 x ([], []) \<Longrightarrow> RR"
 
       
   269 by (auto simp: inv_loop6.simps)
 
       
   270 
       
   271 lemma [elim]: "inv_loop6 x (b, []) \<Longrightarrow> RR" 
       
   272 by (auto simp: inv_loop6.simps)
 
       
   273 
       
   274 lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> b = []"
 
       
   275 by (auto simp: inv_loop1.simps)
 
   258 by (auto simp: inv_loop1.simps)
 
   276 
   259 
   277 lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> list = Oc # Bk \<up> x @ Oc \<up> x"
 
   260 lemma inv_loop3_Bk_via_2[elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
 
   278 by (auto simp: inv_loop1.simps)
 
       
   279 
       
   280 lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
 
       
   281 apply(auto simp: inv_loop2.simps inv_loop3.simps)
 
   261 apply(auto simp: inv_loop2.simps inv_loop3.simps)
 
   282 apply(rule_tac [!] x = i  in exI, rule_tac [!] x = j in exI, simp_all)
 
   262 apply(rule_tac [!] x = i  in exI, rule_tac [!] x = j in exI, simp_all)
 
   283 done
 
   263 done
 
   284 
   264 
   285 lemma [elim]: "Bk # list = Oc \<up> j \<Longrightarrow> RR"
 
   265 lemma inv_loop3_Bk_move[elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
 
   286 by (case_tac j, simp_all)
 
       
   287 
       
   288 lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
 
       
   289 apply(auto simp: inv_loop3.simps)
 
   266 apply(auto simp: inv_loop3.simps)
 
   290 apply(rule_tac [!] x = i in exI, 
   267 apply(rule_tac [!] x = i in exI, 
   291       rule_tac [!] x = j in exI, simp_all)
 
   268       rule_tac [!] x = j in exI, simp_all)
 
   292 apply(case_tac [!] t, auto)
 
   269 apply(case_tac [!] t, auto)
 
   293 done
 
   270 done
 
   294 
   271 
   295 lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop5 x (b, Oc # list)"
 
   272 lemma inv_loop5_Oc_via_4_Bk[elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop5 x (b, Oc # list)"
 
   296 by (auto simp: inv_loop4.simps inv_loop5.simps)
 
   273 by (auto simp: inv_loop4.simps inv_loop5.simps)
 
   297 
   274 
   298 lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
 
   275 lemma inv_loop6_Bk_via_5[elim]: "\<lbrakk>0 < x; inv_loop5 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
 
   299 by (auto simp: inv_loop6.simps inv_loop5.simps)
 
   276 by (auto simp: inv_loop6.simps inv_loop5.simps)
 
   300 
   277 
   301 lemma [simp]: "inv_loop5_loop x (b, Bk # list) = False"
 
   278 lemma inv_loop5_loop_no_Bk[simp]: "inv_loop5_loop x (b, Bk # list) = False"
 
   302 by (auto simp: inv_loop5.simps)
 
   279 by (auto simp: inv_loop5.simps)
 
   303 
   280 
   304 lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"
 
   281 lemma inv_loop6_exit_no_Bk[simp]: "inv_loop6_exit x (b, Bk # list) = False"
 
   305 by (auto simp: inv_loop6.simps)
 
   282 by (auto simp: inv_loop6.simps)
 
   306 
   283 
   307 declare inv_loop5_loop.simps[simp del]  inv_loop5_exit.simps[simp del]
 
   284 declare inv_loop5_loop.simps[simp del]  inv_loop5_exit.simps[simp del]
 
   308        inv_loop6_loop.simps[simp del]  inv_loop6_exit.simps[simp del]
 
   285        inv_loop6_loop.simps[simp del]  inv_loop6_exit.simps[simp del]
 
   309 
   286 
   310 lemma [elim]:"\<lbrakk>0 < x; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk> 
   287 lemma inv_loop6_loopBk_via_5[elim]:"\<lbrakk>0 < x; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk> 
   311           \<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"
 
   288           \<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"
 
   312 apply(simp only: inv_loop5_exit.simps inv_loop6_loop.simps )
 
   289 apply(simp only: inv_loop5_exit.simps inv_loop6_loop.simps )
 
   313 apply(erule_tac exE)+
 
   290 apply(erule_tac exE)+
 
   314 apply(rule_tac x = i in exI, 
   291 apply(rule_tac x = i in exI, 
   315       rule_tac x = j in exI,
 
   292       rule_tac x = j in exI,
 
   317       rule_tac x = "Suc 0" in exI, auto)
 
   294       rule_tac x = "Suc 0" in exI, auto)
 
   318 apply(case_tac [!] j, simp_all)
 
   295 apply(case_tac [!] j, simp_all)
 
   319 apply(case_tac [!] nat, simp_all)
 
   296 apply(case_tac [!] nat, simp_all)
 
   320 done
 
   297 done
 
   321 
   298 
   322 lemma [simp]: "inv_loop6_loop x (b, Oc # Bk # list) = False"
 
   299 lemma inv_loop6_loop_no_Oc_Bk[simp]: "inv_loop6_loop x (b, Oc # Bk # list) = False"
 
   323 by (auto simp: inv_loop6_loop.simps)
 
   300 by (auto simp: inv_loop6_loop.simps)
 
   324 
   301 
   325 lemma [elim]: "\<lbrakk>x > 0; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow> 
   302 lemma inv_loop6_exit_Oc_Bk_via_5[elim]: "\<lbrakk>x > 0; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow> 
   326   inv_loop6_exit x (tl b, Oc # Bk # list)"
 
   303   inv_loop6_exit x (tl b, Oc # Bk # list)"
 
   327 apply(simp only: inv_loop5_exit.simps inv_loop6_exit.simps)
 
   304 apply(simp only: inv_loop5_exit.simps inv_loop6_exit.simps)
 
   328 apply(erule_tac exE)+
 
   305 apply(erule_tac exE)+
 
   329 apply(rule_tac x = "x - 1" in exI, rule_tac x = 1 in exI, simp)
 
   306 apply(rule_tac x = "x - 1" in exI, rule_tac x = 1 in exI, simp)
 
   330 apply(case_tac j, auto)
 
   307 apply(case_tac j, auto)
 
   331 apply(case_tac [!] nat, auto)
 
   308 apply(case_tac [!] nat, auto)
 
   332 done
 
   309 done
 
   333 
   310 
   334 lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"
 
   311 lemma inv_loop6_Bk_tail_via_5[elim]: "\<lbrakk>0 < x; inv_loop5 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"
 
   335 apply(simp add: inv_loop5.simps inv_loop6.simps)
 
   312 apply(simp add: inv_loop5.simps inv_loop6.simps)
 
   336 apply(case_tac "hd b", simp_all, auto)
 
   313 apply(case_tac "hd b", simp_all, auto)
 
   337 done
 
   314 done
 
   338 
   315 
   339 lemma  [simp]: "inv_loop6 x ([], Bk # xs) = False"
 
   316 lemma inv_loop6_loop_Bk_Bk_drop[elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk>
 
   340 apply(simp add: inv_loop6.simps inv_loop6_loop.simps
 
       
   341                 inv_loop6_exit.simps)
 
       
   342 apply(auto)
 
       
   343 done
 
       
   344 
       
   345 lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
 
       
   346 by (simp)
 
       
   347 
       
   348 lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"
 
       
   349 by (simp add: inv_loop6_exit.simps)
 
       
   350 
       
   351 lemma [elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk>
 
       
   352               \<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"
 
   317               \<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"
 
   353 apply(simp only: inv_loop6_loop.simps)
 
   318 apply(simp only: inv_loop6_loop.simps)
 
   354 apply(erule_tac exE)+
 
   319 apply(erule_tac exE)+
 
   355 apply(rule_tac x = i in exI, rule_tac x = j in exI, 
   320 apply(rule_tac x = i in exI, rule_tac x = j in exI, 
   356       rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI, auto)
 
   321       rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI, auto)
 
   357 apply(case_tac [!] k, auto)
 
   322 apply(case_tac [!] k, auto)
 
   358 done
 
   323 done
 
   359 
   324 
   360 lemma [elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk> 
   325 lemma inv_loop6_exit_Oc_Bk_via_loop6[elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk> 
   361         \<Longrightarrow> inv_loop6_exit x (tl b, Oc # Bk # list)"
 
   326         \<Longrightarrow> inv_loop6_exit x (tl b, Oc # Bk # list)"
 
   362 apply(simp only: inv_loop6_loop.simps inv_loop6_exit.simps)
 
   327 apply(simp only: inv_loop6_loop.simps inv_loop6_exit.simps)
 
   363 apply(erule_tac exE)+
 
   328 apply(erule_tac exE)+
 
   364 apply(rule_tac x = "i - 1" in exI, rule_tac x = j in exI, auto)
 
   329 apply(rule_tac x = "i - 1" in exI, rule_tac x = j in exI, auto)
 
   365 apply(case_tac [!] k, auto)
 
   330 apply(case_tac [!] k, auto)
 
   366 done
 
   331 done
 
   367 
   332 
   368 lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"
 
   333 lemma inv_loop6_Bk_tail[elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"
 
   369 apply(simp add: inv_loop6.simps)
 
   334 apply(simp add: inv_loop6.simps)
 
   370 apply(case_tac "hd b", simp_all, auto)
 
   335 apply(case_tac "hd b", simp_all, auto)
 
   371 done
 
   336 done
 
   372 
   337 
   373 lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (Oc # b, list)"
 
   338 lemma inv_loop2_Oc_via_1[elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (Oc # b, list)"
 
   374 apply(auto simp: inv_loop1.simps inv_loop2.simps)
 
   339 apply(auto simp: inv_loop1.simps inv_loop2.simps)
 
   375 apply(rule_tac x = "Suc i" in exI, auto)
 
   340 apply(rule_tac x = "Suc i" in exI, auto)
 
   376 done
 
   341 done
 
   377 
   342 
   378 lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (b, Bk # list)"
 
   343 lemma inv_loop2_Bk_via_Oc[elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (b, Bk # list)"
 
   379 by (auto simp: inv_loop2.simps)
 
   344 by (auto simp: inv_loop2.simps)
 
   380 
   345 
   381 lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"
 
   346 lemma inv_loop4_Oc_via_3[elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"
 
   382 apply(auto simp: inv_loop3.simps inv_loop4.simps)
 
   347 apply(auto simp: inv_loop3.simps inv_loop4.simps)
 
   383 apply(rule_tac [!] x = i in exI, auto)
 
   348 apply(rule_tac [!] x = i in exI, auto)
 
   384 apply(rule_tac [!] x = "Suc 0" in exI, rule_tac [!] x = "j - 1" in exI, auto)
 
   349 apply(rule_tac [!] x = "Suc 0" in exI, rule_tac [!] x = "j - 1" in exI, auto)
 
   385 apply(case_tac [!] t, auto)
 
   350 apply(case_tac [!] t, auto)
 
   386 apply(case_tac [!] j, auto)
 
   351 apply(case_tac [!] j, auto)
 
   387 done
 
   352 done
 
   388 
   353 
   389 lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"
 
   354 lemma inv_loop4_Oc_move[elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"
 
   390 apply(auto simp: inv_loop4.simps)
 
   355 apply(auto simp: inv_loop4.simps)
 
   391 apply(rule_tac [!] x = "i" in exI, auto)
 
   356 apply(rule_tac [!] x = "i" in exI, auto)
 
   392 apply(rule_tac [!] x = "Suc k" in exI, rule_tac [!] x = "t - 1" in exI, auto)
 
   357 apply(rule_tac [!] x = "Suc k" in exI, rule_tac [!] x = "t - 1" in exI, auto)
 
   393 apply(case_tac [!] t, simp_all)
 
   358 apply(case_tac [!] t, simp_all)
 
   394 done
 
   359 done
 
   395 
   360 
   396 lemma [simp]: "inv_loop5 x ([], list) = False"
 
   361 lemma inv_loop5_exit_no_Oc[simp]: "inv_loop5_exit x (b, Oc # list) = False"
 
   397 by (auto simp: inv_loop5.simps inv_loop5_exit.simps inv_loop5_loop.simps)
 
       
   398 
       
   399 lemma [simp]: "inv_loop5_exit x (b, Oc # list) = False"
 
       
   400 by (auto simp: inv_loop5_exit.simps)
 
   362 by (auto simp: inv_loop5_exit.simps)
 
   401 
   363 
   402 lemma [elim]: " \<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk>
 
   364 lemma inv_loop5_exit_Bk_Oc_via_loop[elim]: " \<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk>
 
   403   \<Longrightarrow> inv_loop5_exit x (tl b, Bk # Oc # list)"
 
   365   \<Longrightarrow> inv_loop5_exit x (tl b, Bk # Oc # list)"
 
   404 apply(simp only: inv_loop5_loop.simps inv_loop5_exit.simps)
 
   366 apply(simp only: inv_loop5_loop.simps inv_loop5_exit.simps)
 
   405 apply(erule_tac exE)+
 
   367 apply(erule_tac exE)+
 
   406 apply(rule_tac x = i in exI, auto)
 
   368 apply(rule_tac x = i in exI, auto)
 
   407 apply(case_tac [!] k, auto)
 
   369 apply(case_tac [!] k, auto)
 
   408 done
 
   370 done
 
   409 
   371 
   410 lemma [elim]: "\<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Oc\<rbrakk> 
   372 lemma inv_loop5_loop_Oc_Oc_drop[elim]: "\<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Oc\<rbrakk> 
   411            \<Longrightarrow> inv_loop5_loop x (tl b, Oc # Oc # list)"
 
   373            \<Longrightarrow> inv_loop5_loop x (tl b, Oc # Oc # list)"
 
   412 apply(simp only:  inv_loop5_loop.simps)
 
   374 apply(simp only:  inv_loop5_loop.simps)
 
   413 apply(erule_tac exE)+
 
   375 apply(erule_tac exE)+
 
   414 apply(rule_tac x = i in exI, rule_tac x = j in exI)
 
   376 apply(rule_tac x = i in exI, rule_tac x = j in exI)
 
   415 apply(rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI, auto)
 
   377 apply(rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI, auto)
 
   416 apply(case_tac [!] k, auto)
 
   378 apply(case_tac [!] k, auto)
 
   417 done
 
   379 done
 
   418 
   380 
   419 lemma [elim]: "\<lbrakk>inv_loop5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop5 x (tl b, hd b # Oc # list)"
 
   381 lemma inv_loop5_Oc_tl[elim]: "\<lbrakk>inv_loop5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop5 x (tl b, hd b # Oc # list)"
 
   420 apply(simp add: inv_loop5.simps)
 
   382 apply(simp add: inv_loop5.simps)
 
   421 apply(case_tac "hd b", simp_all, auto)
 
   383 apply(case_tac "hd b", simp_all, auto)
 
   422 done
 
   384 done
 
   423 
   385 
   424 lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_loop1 x ([], Bk # Oc # list)"
 
   386 lemma inv_loop1_Bk_Oc_via_6[elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_loop1 x ([], Bk # Oc # list)"
 
   425 apply(auto simp: inv_loop6.simps inv_loop1.simps 
   387 apply(auto simp: inv_loop6.simps inv_loop1.simps 
   426   inv_loop6_loop.simps inv_loop6_exit.simps)
 
   388   inv_loop6_loop.simps inv_loop6_exit.simps)
 
   427 done
 
   389 done
 
   428 
   390 
   429 lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Oc # list); b \<noteq> []\<rbrakk> 
   391 lemma inv_loop1_Oc_via_6[elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Oc # list); b \<noteq> []\<rbrakk> 
   430            \<Longrightarrow> inv_loop1 x (tl b, hd b # Oc # list)"
 
   392            \<Longrightarrow> inv_loop1 x (tl b, hd b # Oc # list)"
 
   431 apply(auto simp: inv_loop6.simps inv_loop1.simps 
   393 apply(auto simp: inv_loop6.simps inv_loop1.simps 
   432   inv_loop6_loop.simps inv_loop6_exit.simps)
 
   394   inv_loop6_loop.simps inv_loop6_exit.simps)
 
   433 done
 
   395 done
 
       
   396 
       
   397 
       
   398 lemma inv_loop_nonempty[simp]:
 
       
   399   "inv_loop1 x (b, []) = False"
 
       
   400   "inv_loop2 x ([], b) = False"
 
       
   401   "inv_loop2 x (l', []) = False"
 
       
   402   "inv_loop3 x (b, []) = False"
 
       
   403   "inv_loop4 x ([], b) = False"
 
       
   404   "inv_loop5 x ([], list) = False"
 
       
   405   "inv_loop6 x ([], Bk # xs) = False"
 
       
   406   by (auto simp: inv_loop1.simps inv_loop2.simps inv_loop3.simps inv_loop4.simps 
       
   407    inv_loop5.simps inv_loop6.simps inv_loop5_exit.simps inv_loop5_loop.simps
 
       
   408    inv_loop6_loop.simps)
 
       
   409 
       
   410 lemma inv_loop_nonemptyE[elim]:
 
       
   411   "\<lbrakk>inv_loop5 x (b, [])\<rbrakk> \<Longrightarrow> RR" "inv_loop6 x (b, []) \<Longrightarrow> RR" 
       
   412   "\<lbrakk>inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> b = []"
 
       
   413   by (auto simp: inv_loop4.simps inv_loop5.simps inv_loop5_exit.simps inv_loop5_loop.simps
 
       
   414  inv_loop6.simps inv_loop6_exit.simps inv_loop6_loop.simps inv_loop1.simps)
 
       
   415 
       
   416 lemma inv_loop6_Bk_Bk_drop[elim]: "\<lbrakk>inv_loop6 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
 
       
   417   by (simp)
 
   434 
   418 
   435 lemma inv_loop_step: 
   419 lemma inv_loop_step: 
   436   "\<lbrakk>inv_loop x cf; x > 0\<rbrakk> \<Longrightarrow> inv_loop x (step cf (tcopy_loop, 0))"
 
   420   "\<lbrakk>inv_loop x cf; x > 0\<rbrakk> \<Longrightarrow> inv_loop x (step cf (tcopy_loop, 0))"
 
   437 apply(case_tac cf, case_tac c, case_tac [2] aa)
 
   421 apply(case_tac cf, case_tac c, case_tac [2] aa)
 
   438 apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral split: if_splits)
 
   422 apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral split: if_splits)
 
   474 lemma measure_loop_induct [case_names Step]: 
   458 lemma measure_loop_induct [case_names Step]: 
   475   "\<lbrakk>\<And>n. \<not> P (f n) \<Longrightarrow> (f (Suc n), (f n)) \<in> measure_loop\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
 
   459   "\<lbrakk>\<And>n. \<not> P (f n) \<Longrightarrow> (f (Suc n), (f n)) \<in> measure_loop\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
 
   476 using wf_measure_loop
 
   460 using wf_measure_loop
 
   477 by (metis wf_iff_no_infinite_down_chain)
 
   461 by (metis wf_iff_no_infinite_down_chain)
 
   478 
   462 
   479 
   463 lemma inv_loop4_not_just_Oc[elim]: 
   480 
   464   "\<lbrakk>inv_loop4 x (l', []);
 
   481 lemma [simp]: "inv_loop2 x ([], b) = False"
 
       
   482 by (auto simp: inv_loop2.simps)
 
       
   483 
       
   484 lemma  [simp]: "inv_loop2 x (l', []) = False"
 
       
   485 by (auto simp: inv_loop2.simps)
 
       
   486 
       
   487 lemma [simp]: "inv_loop3 x (b, []) = False"
 
       
   488 by (auto simp: inv_loop3.simps)
 
       
   489 
       
   490 lemma [simp]: "inv_loop4 x ([], b) = False"
 
       
   491 by (auto simp: inv_loop4.simps)
 
       
   492 
       
   493 
       
   494 lemma [elim]: 
       
   495   "\<lbrakk>inv_loop4 x (l', []); l' \<noteq> []; x > 0;
 
       
   496   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ [Oc])) \<noteq> 
   465   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ [Oc])) \<noteq> 
   497   length (takeWhile (\<lambda>a. a = Oc) (rev l'))\<rbrakk>
 
   466   length (takeWhile (\<lambda>a. a = Oc) (rev l'))\<rbrakk>
 
   498   \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ [Oc])) < length (takeWhile (\<lambda>a. a = Oc) (rev l'))"
 
   467   \<Longrightarrow> RR"
 
       
   468   "\<lbrakk>inv_loop4 x (l', Bk # list);
 
       
   469    length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) \<noteq> 
       
   470     length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
 
       
   471     \<Longrightarrow> RR"
 
   499 apply(auto simp: inv_loop4.simps)
 
   472 apply(auto simp: inv_loop4.simps)
 
   500 apply(case_tac [!] j, simp_all add: List.takeWhile_tail)
 
   473 apply(case_tac [!] j, simp_all add: List.takeWhile_tail)
 
   501 done
 
   474 done
 
   502 
       
   503 
       
   504 lemma [elim]: 
       
   505   "\<lbrakk>inv_loop4 x (l', Bk # list); l' \<noteq> []; 0 < x;
 
       
   506    length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) \<noteq> 
       
   507     length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
 
       
   508     \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) < 
       
   509     length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"
 
       
   510 by (auto simp: inv_loop4.simps)
 
       
   511 
   475 
   512 lemma takeWhile_replicate_append: 
   476 lemma takeWhile_replicate_append: 
   513   "P a \<Longrightarrow> takeWhile P (a\<up>x @ ys) = a\<up>x @ takeWhile P ys"
 
   477   "P a \<Longrightarrow> takeWhile P (a\<up>x @ ys) = a\<up>x @ takeWhile P ys"
 
   514 by (induct x, auto)
 
   478 by (induct x, auto)
 
   515 
   479 
   516 lemma takeWhile_replicate: 
   480 lemma takeWhile_replicate: 
   517   "P a \<Longrightarrow> takeWhile P (a\<up>x) = a\<up>x"
 
   481   "P a \<Longrightarrow> takeWhile P (a\<up>x) = a\<up>x"
 
   518 by (induct x, auto)
 
   482 by (induct x, auto)
 
   519 
   483 
   520 lemma [elim]: 
   484 lemma inv_loop5_Bk_E[elim]: 
   521    "\<lbrakk>inv_loop5 x (l', Bk # list); l' \<noteq> []; 0 < x;
 
   485    "\<lbrakk>inv_loop5 x (l', Bk # list); l' \<noteq> []; 
   522    length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \<noteq>
 
   486    length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \<noteq>
 
   523    length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
 
   487    length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
 
   524    \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) < 
   488    \<Longrightarrow> RR"
 
   525    length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"
 
       
   526 apply(auto simp: inv_loop5.simps inv_loop5_exit.simps)
 
   489 apply(auto simp: inv_loop5.simps inv_loop5_exit.simps)
 
   527 apply(case_tac [!] j, simp_all)
 
   490 apply(case_tac [!] j, simp_all)
 
   528 apply(case_tac [!] "nat", simp_all)
 
   491 apply(case_tac [!] "nat", simp_all)
 
   529 apply(case_tac  nata, simp_all add: List.takeWhile_tail)
 
   492 apply(case_tac  nata, simp_all add: List.takeWhile_tail)
 
   530 apply(simp add: takeWhile_replicate_append takeWhile_replicate)
 
   493 apply(simp add: takeWhile_replicate_append takeWhile_replicate)
 
   531 apply(case_tac  nata, simp_all add: List.takeWhile_tail)
 
   494 apply(case_tac  nata, simp_all add: List.takeWhile_tail)
 
   532 done
 
   495 done
 
   533 
   496 
   534 lemma [elim]: "\<lbrakk>inv_loop1 x (l', Oc # list)\<rbrakk> \<Longrightarrow> hd list = Oc"
 
   497 lemma inv_loop1_hd_Oc[elim]: "\<lbrakk>inv_loop1 x (l', Oc # list)\<rbrakk> \<Longrightarrow> hd list = Oc"
 
   535 by (auto simp: inv_loop1.simps)
 
   498 by (auto simp: inv_loop1.simps)
 
   536 
   499 
   537 lemma [elim]: 
   500 lemma inv_loop6_not_just_Bk[elim]: 
   538   "\<lbrakk>inv_loop6 x (l', Bk # list); l' \<noteq> []; 0 < x;
 
   501   "\<lbrakk>inv_loop6 x (l', Bk # list); l' \<noteq> [];
 
   539   length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \<noteq> 
   502   length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \<noteq> 
   540   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
 
   503   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
 
   541   \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) < 
   504   \<Longrightarrow> RR"
 
   542   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"
 
       
   543 apply(auto simp: inv_loop6.simps)
 
   505 apply(auto simp: inv_loop6.simps)
 
   544 apply(case_tac l', simp_all)
 
   506 apply(case_tac l', simp_all)
 
   545 done
 
   507 done
 
   546 
   508 
   547 lemma [elim]:
 
   509 lemma inv_loop2_OcE[elim]:
 
   548   "\<lbrakk>inv_loop2 x (l', Oc # list); l' \<noteq> []; 0 < x\<rbrakk> \<Longrightarrow> 
   510   "\<lbrakk>inv_loop2 x (l', Oc # list); l' \<noteq> []\<rbrakk> \<Longrightarrow> 
   549   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list)) <
 
   511   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list)) <
 
   550   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"
 
   512   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"
 
   551 apply(auto simp: inv_loop2.simps)
 
   513 apply(auto simp: inv_loop2.simps)
 
   552 apply(simp_all add: takeWhile_tail takeWhile_replicate_append
 
   514 apply(simp_all add: takeWhile_tail takeWhile_replicate_append
 
   553                 takeWhile_replicate)
 
   515                 takeWhile_replicate)
 
   554 done
 
   516 done
 
   555 
   517 
   556 lemma [elim]: 
   518 lemma inv_loop5_OcE[elim]: 
   557   "\<lbrakk>inv_loop5 x (l', Oc # list); l' \<noteq> []; 0 < x;
 
   519   "\<lbrakk>inv_loop5 x (l', Oc # list); l' \<noteq> [];
 
   558   length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) \<noteq> 
   520   length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) \<noteq> 
   559   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))\<rbrakk>
 
   521   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))\<rbrakk>
 
   560   \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) < 
   522   \<Longrightarrow> RR"
 
   561   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"
 
       
   562 apply(auto simp: inv_loop5.simps)
 
   523 apply(auto simp: inv_loop5.simps)
 
   563 apply(case_tac l', auto)
 
   524 apply(case_tac l', auto)
 
   564 done
 
   525 done
 
   565 
   526 
   566 lemma[elim]: 
   527 lemma inv_loop6_OcE[elim]: 
   567   "\<lbrakk>inv_loop6 x (l', Oc # list); l' \<noteq> []; 0 < x;
 
   528   "\<lbrakk>inv_loop6 x (l', Oc # list); l' \<noteq> []; 
   568   length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list))
 
   529   length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list))
 
   569   \<noteq> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))\<rbrakk>
 
   530   \<noteq> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))\<rbrakk>
 
   570   \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) < 
   531   \<Longrightarrow> RR"
 
   571       length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"
 
       
   572 apply(case_tac l')
 
   532 apply(case_tac l')
 
   573 apply(auto simp: inv_loop6.simps)
 
   533 apply(auto simp: inv_loop6.simps)
 
   574 done
 
   534 done
 
   575 
   535 
   576 lemma loop_halts: 
   536 lemma loop_halts: 
   666 declare inv_end.simps[simp del] inv_end1.simps[simp del]
 
   626 declare inv_end.simps[simp del] inv_end1.simps[simp del]
 
   667         inv_end0.simps[simp del] inv_end2.simps[simp del]
 
   627         inv_end0.simps[simp del] inv_end2.simps[simp del]
 
   668         inv_end3.simps[simp del] inv_end4.simps[simp del]
 
   628         inv_end3.simps[simp del] inv_end4.simps[simp del]
 
   669         inv_end5.simps[simp del]
 
   629         inv_end5.simps[simp del]
 
   670 
   630 
   671 lemma [simp]:  "inv_end1 x (b, []) = False"
 
   631 lemma inv_end_nonempty[simp]:
 
   672 by (auto simp: inv_end1.simps)
 
   632   "inv_end1 x (b, []) = False"
 
   673 
   633   "inv_end1 x ([], list) = False"
 
   674 lemma [simp]: "inv_end2 x (b, []) = False"
 
   634   "inv_end2 x (b, []) = False"
 
   675 by (auto simp: inv_end2.simps)
 
   635   "inv_end3 x (b, []) = False"
 
   676 
   636   "inv_end4 x (b, []) = False"
 
   677 lemma [simp]: "inv_end3 x (b, []) = False"
 
   637   "inv_end5 x (b, []) = False"
 
   678 by (auto simp: inv_end3.simps)
 
   638   "inv_end5 x ([], Oc # list) = False"
 
   679 
   639 by (auto simp: inv_end1.simps inv_end2.simps inv_end3.simps inv_end4.simps inv_end5.simps)
 
   680 lemma [simp]: "inv_end4 x (b, []) = False"
 
   640 
   681 by (auto simp: inv_end4.simps)
 
   641 lemma inv_end0_Bk_via_1[elim]: "\<lbrakk>0 < x; inv_end1 x (b, Bk # list); b \<noteq> []\<rbrakk>
 
   682 
       
   683 lemma [simp]: "inv_end5 x (b, []) = False"
 
       
   684 by (auto simp: inv_end5.simps)
 
       
   685 
       
   686 lemma [simp]: "inv_end1 x ([], list) = False"
 
       
   687 by (auto simp: inv_end1.simps)
 
       
   688 
       
   689 lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Bk # list); b \<noteq> []\<rbrakk>
 
       
   690   \<Longrightarrow> inv_end0 x (tl b, hd b # Bk # list)"
 
   642   \<Longrightarrow> inv_end0 x (tl b, hd b # Bk # list)"
 
   691 by (auto simp: inv_end1.simps inv_end0.simps)
 
   643 by (auto simp: inv_end1.simps inv_end0.simps)
 
   692 
   644 
   693 lemma [elim]: "\<lbrakk>0 < x; inv_end2 x (b, Bk # list)\<rbrakk> 
   645 lemma inv_end3_Oc_via_2[elim]: "\<lbrakk>0 < x; inv_end2 x (b, Bk # list)\<rbrakk> 
   694   \<Longrightarrow> inv_end3 x (b, Oc # list)"
 
   646   \<Longrightarrow> inv_end3 x (b, Oc # list)"
 
   695 apply(auto simp: inv_end2.simps inv_end3.simps)
 
   647 apply(auto simp: inv_end2.simps inv_end3.simps)
 
   696 apply(rule_tac x = "j - 1" in exI)
 
   648 apply(rule_tac x = "j - 1" in exI)
 
   697 apply(case_tac j, simp_all)
 
   649 apply(case_tac j, simp_all)
 
   698 apply(case_tac x, simp_all)
 
   650 apply(case_tac x, simp_all)
 
   699 done
 
   651 done
 
   700 
   652 
   701 lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Bk # b, list)"
 
   653 lemma inv_end2_Bk_via_3[elim]: "\<lbrakk>0 < x; inv_end3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Bk # b, list)"
 
   702 by (auto simp: inv_end2.simps inv_end3.simps)
 
   654 by (auto simp: inv_end2.simps inv_end3.simps)
 
   703   
   655   
   704 lemma [elim]: "\<lbrakk>0 < x; inv_end4 x ([], Bk # list)\<rbrakk> \<Longrightarrow> 
   656 lemma inv_end5_Bk_via_4[elim]: "\<lbrakk>0 < x; inv_end4 x ([], Bk # list)\<rbrakk> \<Longrightarrow> 
   705   inv_end5 x ([], Bk # Bk # list)"
 
   657   inv_end5 x ([], Bk # Bk # list)"
 
   706 by (auto simp: inv_end4.simps inv_end5.simps)
 
   658 by (auto simp: inv_end4.simps inv_end5.simps)
 
   707  
   659  
   708 lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> 
   660 lemma inv_end5_Bk_tail_via_4[elim]: "\<lbrakk>0 < x; inv_end4 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> 
   709   inv_end5 x (tl b, hd b # Bk # list)"
 
   661   inv_end5 x (tl b, hd b # Bk # list)"
 
   710 apply(auto simp: inv_end4.simps inv_end5.simps)
 
   662 apply(auto simp: inv_end4.simps inv_end5.simps)
 
   711 apply(rule_tac x = 1 in exI, simp)
 
   663 apply(rule_tac x = 1 in exI, simp)
 
   712 done
 
   664 done
 
   713 
   665 
   714 lemma [elim]: "\<lbrakk>0 < x; inv_end5 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end0 x (Bk # b, list)"
 
   666 lemma inv_end0_Bk_via_5[elim]: "\<lbrakk>0 < x; inv_end5 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end0 x (Bk # b, list)"
 
   715 apply(auto simp: inv_end5.simps inv_end0.simps)
 
   667 apply(auto simp: inv_end5.simps inv_end0.simps)
 
   716 apply(case_tac [!] j, simp_all)
 
   668 apply(case_tac [!] j, simp_all)
 
   717 done
 
   669 done
 
   718 
   670 
   719 lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
 
   671 lemma inv_end2_Oc_via_1[elim]: "\<lbrakk>0 < x; inv_end1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
 
   720 by (auto simp: inv_end1.simps inv_end2.simps)
 
   672 by (auto simp: inv_end1.simps inv_end2.simps)
 
   721 
   673 
   722 lemma [elim]: "\<lbrakk>0 < x; inv_end2 x ([], Oc # list)\<rbrakk> \<Longrightarrow>
 
   674 lemma inv_end4_Bk_Oc_via_2[elim]: "\<lbrakk>0 < x; inv_end2 x ([], Oc # list)\<rbrakk> \<Longrightarrow>
 
   723                inv_end4 x ([], Bk # Oc # list)"
 
   675                inv_end4 x ([], Bk # Oc # list)"
 
   724 by (auto simp: inv_end2.simps inv_end4.simps)
 
   676 by (auto simp: inv_end2.simps inv_end4.simps)
 
   725 
   677 
   726 lemma [elim]:  "\<lbrakk>0 < x; inv_end2 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
 
   678 lemma inv_end4_Oc_via_2[elim]:  "\<lbrakk>0 < x; inv_end2 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
 
   727   inv_end4 x (tl b, hd b # Oc # list)"
 
   679   inv_end4 x (tl b, hd b # Oc # list)"
 
   728 apply(auto simp: inv_end2.simps inv_end4.simps)
 
   680 apply(auto simp: inv_end2.simps inv_end4.simps)
 
   729 apply(case_tac [!] j, simp_all)
 
   681 apply(case_tac [!] j, simp_all)
 
   730 done
 
   682 done
 
   731 
   683 
   732 lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
 
   684 lemma inv_end2_Oc_via_3[elim]: "\<lbrakk>0 < x; inv_end3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
 
   733 by (auto simp: inv_end2.simps inv_end3.simps)
 
   685 by (auto simp: inv_end2.simps inv_end3.simps)
 
   734 
   686 
   735 lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end4 x (b, Bk # list)"
 
   687 lemma inv_end4_Bk_via_Oc[elim]: "\<lbrakk>0 < x; inv_end4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end4 x (b, Bk # list)"
 
   736 by (auto simp: inv_end2.simps inv_end4.simps)
 
   688 by (auto simp: inv_end2.simps inv_end4.simps)
 
   737 
   689 
   738 lemma [elim]: "\<lbrakk>0 < x; inv_end5 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_end5 x ([], Bk # Oc # list)"
 
   690 lemma inv_end5_Bk_drop_Oc[elim]: "\<lbrakk>0 < x; inv_end5 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_end5 x ([], Bk # Oc # list)"
 
   739 by (auto simp: inv_end2.simps inv_end5.simps)
 
   691 by (auto simp: inv_end2.simps inv_end5.simps)
 
   740 
   692 
   741 declare inv_end5_loop.simps[simp del]
 
   693 declare inv_end5_loop.simps[simp del]
 
   742         inv_end5_exit.simps[simp del]
 
   694         inv_end5_exit.simps[simp del]
 
   743 
   695 
   744 lemma [simp]: "inv_end5_exit x (b, Oc # list) = False"
 
   696 lemma inv_end5_exit_no_Oc[simp]: "inv_end5_exit x (b, Oc # list) = False"
 
   745 by (auto simp: inv_end5_exit.simps)
 
   697 by (auto simp: inv_end5_exit.simps)
 
   746 
   698 
   747 lemma [simp]: "inv_end5_loop x (tl b, Bk # Oc # list) = False"
 
   699 lemma inv_end5_loop_no_Bk_Oc[simp]: "inv_end5_loop x (tl b, Bk # Oc # list) = False"
 
   748 apply(auto simp: inv_end5_loop.simps)
 
   700 apply(auto simp: inv_end5_loop.simps)
 
   749 apply(case_tac [!] j, simp_all)
 
   701 apply(case_tac [!] j, simp_all)
 
   750 done
 
   702 done
 
   751 
   703 
   752 lemma [elim]:
 
   704 lemma inv_end5_exit_Bk_Oc_via_loop[elim]:
 
   753   "\<lbrakk>0 < x; inv_end5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk> \<Longrightarrow>
 
   705   "\<lbrakk>0 < x; inv_end5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk> \<Longrightarrow>
 
   754   inv_end5_exit x (tl b, Bk # Oc # list)"
 
   706   inv_end5_exit x (tl b, Bk # Oc # list)"
 
   755 apply(auto simp: inv_end5_loop.simps inv_end5_exit.simps)
 
   707 apply(auto simp: inv_end5_loop.simps inv_end5_exit.simps)
 
   756 apply(case_tac [!] i, simp_all)
 
   708 apply(case_tac [!] i, simp_all)
 
   757 done
 
   709 done
 
   758 
   710 
   759 lemma [elim]: 
   711 lemma inv_end5_loop_Oc_Oc_drop[elim]: 
   760   "\<lbrakk>0 < x; inv_end5_loop x (b, Oc # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow>
 
   712   "\<lbrakk>0 < x; inv_end5_loop x (b, Oc # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow>
 
   761   inv_end5_loop x (tl b, Oc # Oc # list)"
 
   713   inv_end5_loop x (tl b, Oc # Oc # list)"
 
   762 apply(simp only: inv_end5_loop.simps inv_end5_exit.simps)
 
   714 apply(simp only: inv_end5_loop.simps inv_end5_exit.simps)
 
   763 apply(erule_tac exE)+
 
   715 apply(erule_tac exE)+
 
   764 apply(rule_tac x = "i - 1" in exI, 
   716 apply(rule_tac x = "i - 1" in exI, 
   765       rule_tac x = "Suc j" in exI, auto)
 
   717       rule_tac x = "Suc j" in exI, auto)
 
   766 apply(case_tac [!] i, simp_all)
 
   718 apply(case_tac [!] i, simp_all)
 
   767 done
 
   719 done
 
   768 
   720 
   769 lemma [elim]: "\<lbrakk>0 < x; inv_end5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow> 
   721 lemma inv_end5_Oc_tail[elim]: "\<lbrakk>0 < x; inv_end5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow> 
   770   inv_end5 x (tl b, hd b # Oc # list)"
 
   722   inv_end5 x (tl b, hd b # Oc # list)"
 
   771 apply(simp add: inv_end2.simps inv_end5.simps)
 
   723 apply(simp add: inv_end2.simps inv_end5.simps)
 
   772 apply(case_tac "hd b", simp_all, auto)
 
   724 apply(case_tac "hd b", simp_all, auto)
 
   773 done
 
   725 done
 
   774 
   726 
   813    "end_LE = measures [end_state, end_stage, end_step]"
 
   765    "end_LE = measures [end_state, end_stage, end_step]"
 
   814 
   766 
   815 lemma wf_end_le: "wf end_LE"
 
   767 lemma wf_end_le: "wf end_LE"
 
   816 unfolding end_LE_def
 
   768 unfolding end_LE_def
 
   817 by (auto)
 
   769 by (auto)
 
   818 
       
   819 lemma [simp]: "inv_end5 x ([], Oc # list) = False"
 
       
   820 by (auto simp: inv_end5.simps inv_end5_loop.simps)
 
       
   821 
   770 
   822 lemma halt_lemma: 
   771 lemma halt_lemma: 
   823   "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
 
   772   "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
 
   824 by (metis wf_iff_no_infinite_down_chain)
 
   773 by (metis wf_iff_no_infinite_down_chain)
 
   825 
   774 
   876     done
 
   825     done
 
   877 qed
 
   826 qed
 
   878 
   827 
   879 (* tcopy *)
 
   828 (* tcopy *)
 
   880 
   829 
   881 lemma [intro]: "tm_wf (tcopy_begin, 0)"
 
   830 lemma tm_wf_tcopy[intro]:
 
   882 by (auto simp: tm_wf.simps tcopy_begin_def)
 
   831   "tm_wf (tcopy_begin, 0)"
 
   883 
   832   "tm_wf (tcopy_loop, 0)"
 
   884 lemma [intro]: "tm_wf (tcopy_loop, 0)"
 
   833   "tm_wf (tcopy_end, 0)"
 
   885 by (auto simp: tm_wf.simps tcopy_loop_def)
 
   834 by (auto simp: tm_wf.simps tcopy_end_def tcopy_loop_def tcopy_begin_def)
 
   886 
       
   887 lemma [intro]: "tm_wf (tcopy_end, 0)"
 
       
   888 by (auto simp: tm_wf.simps tcopy_end_def)
 
       
   889 
   835 
   890 lemma tcopy_correct1: 
   836 lemma tcopy_correct1: 
   891   assumes "0 < x"
 
   837   assumes "0 < x"
 
   892   shows "{inv_begin1 x} tcopy {inv_end0 x}"
 
   838   shows "{inv_begin1 x} tcopy {inv_end0 x}"
 
   893 proof -
 
   839 proof -
 
   997 
   943 
   998 definition halts :: "tprog0 \<Rightarrow> nat list \<Rightarrow> bool"
 
   944 definition halts :: "tprog0 \<Rightarrow> nat list \<Rightarrow> bool"
 
   999   where
 
   945   where
 
  1000   "halts p ns \<equiv> {(\<lambda>tp. tp = ([], <ns>))} p {(\<lambda>tp. (\<exists>k n l. tp = (Bk \<up> k,  <n::nat> @ Bk \<up> l)))}"
 
   946   "halts p ns \<equiv> {(\<lambda>tp. tp = ([], <ns>))} p {(\<lambda>tp. (\<exists>k n l. tp = (Bk \<up> k,  <n::nat> @ Bk \<up> l)))}"
 
  1001 
   947 
  1002 lemma [intro, simp]: "tm_wf0 tcopy"
 
   948 lemma tm_wf0_tcopy[intro, simp]: "tm_wf0 tcopy"
 
  1003 by (auto simp: tcopy_def)
 
   949 by (auto simp: tcopy_def)
 
  1004 
   950 
  1005 lemma [intro, simp]: "tm_wf0 dither"
 
   951 lemma tm_wf0_dither[intro, simp]: "tm_wf0 dither"
 
  1006 by (auto simp: tm_wf.simps dither_def)
 
   952 by (auto simp: tm_wf.simps dither_def)
 
  1007 
   953 
  1008 text {*
 
   954 text {*
 
  1009   The following locale specifies that TM @{text "H"} can be used to solve 
   955   The following locale specifies that TM @{text "H"} can be used to solve 
  1010   the {\em Halting Problem} and @{text "False"} is going to be derived 
   956   the {\em Halting Problem} and @{text "False"} is going to be derived
tm