1 (* Title: Turing machine's definition and its charater

     2    Author: XuJian <xujian817@hotmail.com>

     3    Maintainer: Xujian

     4 *)

     5 

     6 header {* Undeciablity of the {\em Halting problem} *}

     7 

     8 theory uncomputable

     9 imports Main turing_basic

    10 begin

    11 

    12 text {*

    13   The {\em Copying} TM, which duplicates its input. 

    14 *}

    15 

    16 definition tcopy_init :: "instr list"

    17 where

    18 "tcopy_init \<equiv> [(W0, 0), (R, 2), (R, 3), (R, 2),

    19                (W1, 3), (L, 4), (L, 4), (L, 0)]"

    20 

    21 fun inv_init1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

    22   where

    23    "inv_init1 x (l, r) = (l = [] \<and> r = Oc\<up>x )"

    24 

    25 fun inv_init2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

    26   where 

    27   "inv_init2 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc\<up>i \<and> r = Oc\<up>j)"

    28 

    29 fun inv_init3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

    30   where

    31   "inv_init3 x (l, r) = (x > 0 \<and> l = Bk # Oc\<up>x \<and> tl r = [])"

    32 

    33 fun inv_init4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

    34   where

    35   "inv_init4 x (l, r) = (x > 0 \<and> ((l = Oc\<up>x \<and> r = [Bk, Oc]) \<or> (l = Oc\<up>(x - 1) \<and> r = [Oc, Bk, Oc])))"

    36 

    37 fun inv_init0 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

    38   where

    39   "inv_init0 x (l, r) = ((x >  Suc 0 \<and> l = Oc\<up>(x - 2) \<and> r = [Oc, Oc, Bk, Oc]) \<or>   

    40                         (x = 1 \<and> l = [] \<and> r = [Bk, Oc, Bk, Oc]))"

    41 

    42 fun inv_init :: "nat \<Rightarrow> config \<Rightarrow> bool"

    43   where

    44   "inv_init x (s, l, r) = (

    45          if s = 0 then inv_init0 x (l, r) 

    46          else if s = Suc 0 then inv_init1 x (l, r)

    47          else if s = 2 then inv_init2 x (l, r)

    48          else if s = 3 then inv_init3 x (l, r)

    49          else if s = 4 then inv_init4 x (l, r)

    50          else False)"

    51 

    52 declare inv_init.simps[simp del]

    53 

    54 lemma numeral_4_eq_4: "4 = Suc 3"

    55 by arith

    56 

    57 lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> 

    58   \<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia"

    59 apply(rule_tac x = "Suc i" in exI, simp)

    60 done

    61 

    62 lemma inv_init_step: 

    63   "\<lbrakk>inv_init x cf; x > 0\<rbrakk>

    64  \<Longrightarrow> inv_init x (step cf (tcopy_init, 0))"

    65 apply(case_tac cf)

    66 apply(auto simp: inv_init.simps step.simps tcopy_init_def numeral_2_eq_2 

    67   numeral_3_eq_3 numeral_4_eq_4 split: if_splits)

    68 apply(case_tac "hd c", auto simp: inv_init.simps)

    69 apply(case_tac c, simp_all)

    70 done

    71 

    72 lemma inv_init_steps: 

    73   "\<lbrakk>inv_init x (s, l, r); x > 0\<rbrakk>

    74  \<Longrightarrow> inv_init x (steps (s, l, r) (tcopy_init, 0) stp)"

    75 apply(induct stp, simp add: steps.simps)

    76 apply(auto simp: step_red)

    77 apply(rule_tac inv_init_step, simp_all)

    78 done

    79 

    80 fun init_state :: "config \<Rightarrow> nat"

    81   where

    82   "init_state (s, l, r) = (if s = 0 then 0

    83                              else 5 - s)"

    84 

    85 fun init_step :: "config \<Rightarrow> nat"

    86   where

    87   "init_step (s, l, r) = (if s = 2 then length r

    88                             else if s = 3 then if r = [] \<or> r = [Bk] then Suc 0 else 0

    89                             else if s = 4 then length l

    90                             else 0)"

    91 

    92 fun init_measure :: "config \<Rightarrow> nat \<times> nat"

    93   where

    94   "init_measure c = 

    95    (init_state c, init_step c)"

    96 

    97 

    98 definition lex_pair :: "((nat \<times> nat) \<times> nat \<times> nat) set"

    99   where

   100   "lex_pair \<equiv> less_than <*lex*> less_than"

   101 

   102 definition init_LE :: "(config \<times> config) set"

   103   where

   104    "init_LE \<equiv> (inv_image lex_pair init_measure)"

   105 

   106 lemma [simp]: "\<lbrakk>tl r = []; r \<noteq> []; r \<noteq> [Bk]\<rbrakk> \<Longrightarrow> r = [Oc]"

   107 apply(case_tac r, auto, case_tac a, auto)

   108 done

   109 

   110 lemma wf_init_le: "wf init_LE"

   111 by(auto intro:wf_inv_image simp:init_LE_def lex_pair_def)

   112 

   113 lemma init_halt: 

   114   "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_init, 0) stp)"

   115 proof(rule_tac LE = init_LE in halt_lemma)

   116   show "wf init_LE" by(simp add: wf_init_le)

   117 next

   118   assume h: "0 < x"

   119   show "\<forall>n. \<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) \<longrightarrow>

   120         (steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) (Suc n), 

   121             steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) \<in> init_LE"

   122   proof(rule_tac allI, rule_tac impI)

   123     fix n

   124     assume a: "\<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n)"

   125     have b: "inv_init x (steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n)"

   126       apply(rule_tac inv_init_steps)

   127       apply(simp_all add: inv_init.simps h)

   128       done 

   129     obtain s l r where c: "(steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) = (s, l, r)"

   130       apply(case_tac "steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n", auto)

   131       done

   132     moreover hence "inv_init x (s, l, r)" 

   133       using c b by simp

   134     ultimately show "(steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) (Suc n), 

   135       steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) \<in> init_LE"

   136       using a 

   137     proof(simp)

   138       assume "inv_init x (s, l, r)" "0 < s"

   139       thus "(step (s, l, r) (tcopy_init, 0), s, l, r) \<in> init_LE"

   140         apply(auto simp: inv_init.simps init_LE_def lex_pair_def step.simps tcopy_init_def numeral_2_eq_2

   141           numeral_3_eq_3 numeral_4_eq_4 split: if_splits)

   142         apply(case_tac r, auto, case_tac a, auto)

   143         done

   144     qed

   145   qed

   146 qed

   147     

   148 lemma init_correct: 

   149   "x > 0 \<Longrightarrow> 

   150   {inv_init1 x} (tcopy_init, 0) {inv_init0 x}"

   151 proof(rule_tac HoareI)

   152   fix l r

   153   assume h: "0 < x"

   154     "inv_init1 x (l, r)"

   155   hence "\<exists> stp. is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_init, 0) stp)"

   156     by(erule_tac init_halt)    

   157   then obtain stp where "is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_init, 0) stp)" ..

   158   moreover have "inv_init x (steps (Suc 0, [], Oc\<up>x) (tcopy_init, 0) stp)"

   159     apply(rule_tac inv_init_steps)

   160     using h by(simp_all add: inv_init.simps)

   161   ultimately show

   162     "\<exists>n. is_final (steps (1, l, r) (tcopy_init, 0) n) \<and> 

   163     inv_init0 x holds_for steps (1, l, r) (tcopy_init, 0) n"

   164     using h

   165     apply(rule_tac x = stp in exI)

   166     apply(case_tac "(steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) stp)", simp add: inv_init.simps)

   167     done

   168 qed

   169 

   170 definition tcopy_loop :: "instr list"

   171 where

   172 "tcopy_loop \<equiv> [(R, 0), (R, 2),  (R, 3), (W0, 2),

   173                 (R, 3), (R, 4), (W1, 5), (R, 4),

   174                  (L, 6), (L, 5), (L, 6), (L, 1)]"

   175 

   176 fun inv_loop1_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   177   where

   178   "inv_loop1_loop x (l, r) = 

   179        (\<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)"

   180 

   181 fun inv_loop1_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   182   where

   183   "inv_loop1_exit x (l, r) = 

   184       (l = [] \<and> r = Bk # Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0 )"

   185 

   186 fun inv_loop1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   187   where

   188   "inv_loop1 x (l, r) = (inv_loop1_loop x (l, r) \<or> inv_loop1_exit x (l, r))"

   189 

   190 fun inv_loop2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   191   where

   192   "inv_loop2 x (l, r) = 

   193        (\<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)"

   194 

   195 fun inv_loop3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   196   where

   197   "inv_loop3 x (l, r) = 

   198          (\<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)"

   199 

   200 fun inv_loop4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   201   where

   202   "inv_loop4 x (l, r) = 

   203            (\<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)"

   204 

   205 fun inv_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   206 where

   207   "inv_loop5_loop x (l, r) = 

   208           (\<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)"

   209 

   210 fun inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   211   where

   212   "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)"

   213 

   214 fun inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   215   where

   216   "inv_loop5 x (l, r) = (inv_loop5_loop x (l, r) \<or> 

   217                          inv_loop5_exit x (l, r))"

   218 

   219 fun inv_loop6_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   220   where

   221   "inv_loop6_loop x (l, r) = 

   222      (\<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)"

   223 

   224 fun inv_loop6_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   225   where

   226   "inv_loop6_exit x (l, r) = 

   227      (\<exists> i j. i + j = x \<and> j > 0 \<and> l = Oc\<up>i \<and> r = Oc # Bk\<up>j @ Oc\<up>j)"

   228 

   229 fun inv_loop6 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   230   where

   231   "inv_loop6 x (l, r) = (inv_loop6_loop x (l, r) \<or> inv_loop6_exit x (l, r))"

   232 

   233 fun inv_loop0 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   234   where

   235   "inv_loop0 x (l, r) = 

   236       (l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0 )"

   237 

   238 fun inv_loop :: "nat \<Rightarrow> config \<Rightarrow> bool"

   239   where

   240   "inv_loop x (s, l, r) = 

   241          (if s = 0 then inv_loop0 x (l, r)

   242           else if s = 1 then inv_loop1 x (l, r)

   243           else if s = 2 then inv_loop2 x (l, r)

   244           else if s = 3 then inv_loop3 x (l, r)

   245           else if s = 4 then inv_loop4 x (l, r)

   246           else if s = 5 then inv_loop5 x (l, r)

   247           else if s = 6 then inv_loop6 x (l, r)

   248           else False)"

   249        

   250 declare inv_loop.simps[simp del] inv_loop1.simps[simp del]

   251         inv_loop2.simps[simp del] inv_loop3.simps[simp del] 

   252         inv_loop4.simps[simp del] inv_loop5.simps[simp del] 

   253         inv_loop6.simps[simp del]

   254 lemma [elim]: "Bk # list = Oc \<up> t \<Longrightarrow> RR"

   255 apply(case_tac t, auto)

   256 done

   257 

   258 lemma numeral_5_eq_5: "5 = Suc 4" by arith

   259 

   260 lemma numeral_6_eq_6: "6 = Suc (Suc 4)" by arith

   261 

   262 lemma [simp]: "inv_loop1 x (b, []) = False"

   263 by(simp add: inv_loop1.simps)

   264 

   265 lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"

   266 apply(auto simp: inv_loop2.simps inv_loop3.simps)

   267 done

   268 

   269 lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"

   270 apply(auto simp: inv_loop3.simps)

   271 done

   272 

   273 lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop5 x (b, [Oc])"

   274 apply(auto simp: inv_loop4.simps inv_loop5.simps)

   275 apply(rule_tac [!] x = i in exI, 

   276       rule_tac [!] x  = "Suc j" in exI, simp_all)

   277 done

   278 

   279 lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], [])\<rbrakk> \<Longrightarrow> RR"

   280 apply(auto simp: inv_loop4.simps inv_loop5.simps)

   281 done

   282 

   283 lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, []); b \<noteq> []\<rbrakk> \<Longrightarrow> RR"

   284 apply(auto simp: inv_loop4.simps inv_loop5.simps)

   285 done

   286 

   287 lemma [elim]: "inv_loop6 x ([], []) \<Longrightarrow> RR"

   288 apply(auto simp: inv_loop6.simps)

   289 done

   290 

   291 thm inv_loop6_exit.simps

   292 lemma [elim]: "inv_loop6 x (b, []) \<Longrightarrow> RR" 

   293 apply(auto simp: inv_loop6.simps)

   294 done

   295 

   296 lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> b = []"

   297 apply(auto simp: inv_loop1.simps)

   298 done

   299 

   300 lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> list = Oc # Bk \<up> x @ Oc \<up> x"

   301 apply(auto simp: inv_loop1.simps)

   302 done

   303 

   304 lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"

   305 apply(auto simp: inv_loop2.simps inv_loop3.simps)

   306 apply(rule_tac [!] x = i  in exI, rule_tac [!] x = j in exI, simp_all)

   307 done

   308 

   309 lemma [elim]: "Bk # list = Oc \<up> j \<Longrightarrow> RR"

   310 apply(case_tac j, simp_all)

   311 done

   312 

   313 lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"

   314 apply(auto simp: inv_loop3.simps)

   315 apply(rule_tac [!] x = i in exI, 

   316       rule_tac [!] x = j in exI, simp_all)

   317 apply(case_tac [!] t, auto)

   318 done

   319 

   320 lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop5 x (b, Oc # list)"

   321 apply(auto simp: inv_loop4.simps inv_loop5.simps)

   322 done

   323 

   324 lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"

   325 apply(auto simp: inv_loop6.simps inv_loop5.simps)

   326 done

   327 

   328 lemma [simp]: "inv_loop5_loop x (b, Bk # list) = False"

   329 apply(auto simp: inv_loop5_loop.simps)

   330 done

   331 

   332 lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"

   333 apply(auto simp: inv_loop6.simps)

   334 done

   335 

   336 declare inv_loop5_loop.simps[simp del]  inv_loop5_exit.simps[simp del]

   337        inv_loop6_loop.simps[simp del]  inv_loop6_exit.simps[simp del]

   338 

   339 lemma [elim]:"\<lbrakk>0 < x; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk> 

   340           \<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"

   341 apply(simp only: inv_loop5_exit.simps inv_loop6_loop.simps )

   342 apply(erule_tac exE)+

   343 apply(rule_tac x = i in exI, 

   344       rule_tac x = j in exI,

   345       rule_tac x = "j - Suc (Suc 0)" in exI, 

   346       rule_tac x = "Suc 0" in exI, auto)

   347 apply(case_tac [!] j, simp_all)

   348 apply(case_tac [!] nat, simp_all)

   349 done

   350 

   351 lemma [simp]: "inv_loop6_loop x (b, Oc # Bk # list) = False"

   352 apply(auto simp: inv_loop6_loop.simps)

   353 done

   354 

   355 lemma [elim]: "\<lbrakk>x > 0; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow> 

   356   inv_loop6_exit x (tl b, Oc # Bk # list)"

   357 apply(simp only: inv_loop5_exit.simps inv_loop6_exit.simps)

   358 apply(erule_tac exE)+

   359 apply(rule_tac x = "x - 1" in exI, rule_tac x = 1 in exI, simp)

   360 apply(case_tac j, auto)

   361 apply(case_tac [!] nat, auto)

   362 done

   363 

   364 lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"

   365 apply(simp add: inv_loop5.simps inv_loop6.simps)

   366 apply(case_tac "hd b", simp_all, auto)

   367 done

   368 

   369 lemma  [simp]: "inv_loop6 x ([], Bk # xs) = False"

   370 apply(simp add: inv_loop6.simps inv_loop6_loop.simps

   371                 inv_loop6_exit.simps)

   372 apply(auto)

   373 done

   374 

   375 lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"

   376 apply(simp)

   377 done

   378 

   379 lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"

   380 apply(simp add: inv_loop6_exit.simps)

   381 done

   382 

   383 lemma [elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk>

   384               \<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"

   385 apply(simp only: inv_loop6_loop.simps)

   386 apply(erule_tac exE)+

   387 apply(rule_tac x = i in exI, rule_tac x = j in exI, 

   388       rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI, auto)

   389 apply(case_tac [!] k, auto)

   390 done

   391 

   392 lemma [elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk> 

   393         \<Longrightarrow> inv_loop6_exit x (tl b, Oc # Bk # list)"

   394 apply(simp only: inv_loop6_loop.simps inv_loop6_exit.simps)

   395 apply(erule_tac exE)+

   396 apply(rule_tac x = "i - 1" in exI, rule_tac x = j in exI, auto)

   397 apply(case_tac [!] k, auto)

   398 done

   399 

   400 lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"

   401 apply(simp add: inv_loop6.simps)

   402 apply(case_tac "hd b", simp_all, auto)

   403 done

   404 

   405 lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (Oc # b, list)"

   406 apply(auto simp: inv_loop1.simps inv_loop2.simps)

   407 apply(rule_tac x = "Suc i" in exI, auto)

   408 done

   409 

   410 lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (b, Bk # list)"

   411 apply(auto simp: inv_loop2.simps)

   412 done

   413 

   414 lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"

   415 apply(auto simp: inv_loop3.simps inv_loop4.simps)

   416 apply(rule_tac [!] x = i in exI, auto)

   417 apply(rule_tac [!] x = "Suc 0" in exI, rule_tac [!] x = "j - 1" in exI, auto)

   418 apply(case_tac [!] t, auto)

   419 apply(case_tac [!] j, auto)

   420 done

   421 

   422 lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"

   423 apply(auto simp: inv_loop4.simps)

   424 apply(rule_tac [!] x = "i" in exI, auto)

   425 apply(rule_tac [!] x = "Suc k" in exI, rule_tac [!] x = "t - 1" in exI, auto)

   426 apply(case_tac [!] t, simp_all)

   427 done

   428 

   429 lemma [simp]: "inv_loop5 x ([], list) = False"

   430 apply(auto simp: inv_loop5.simps inv_loop5_exit.simps inv_loop5_loop.simps)

   431 done

   432 

   433 lemma [simp]: "inv_loop5_exit x (b, Oc # list) = False"

   434 apply(auto simp: inv_loop5_exit.simps)

   435 done

   436 

   437 lemma [elim]: " \<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk>

   438   \<Longrightarrow> inv_loop5_exit x (tl b, Bk # Oc # list)"

   439 apply(simp only: inv_loop5_loop.simps inv_loop5_exit.simps)

   440 apply(erule_tac exE)+

   441 apply(rule_tac x = i in exI, auto)

   442 apply(case_tac [!] k, auto)

   443 done

   444 

   445 lemma [elim]: "\<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Oc\<rbrakk> 

   446            \<Longrightarrow> inv_loop5_loop x (tl b, Oc # Oc # list)"

   447 apply(simp only:  inv_loop5_loop.simps)

   448 apply(erule_tac exE)+

   449 apply(rule_tac x = i in exI, rule_tac x = j in exI)

   450 apply(rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI, auto)

   451 apply(case_tac [!] k, auto)

   452 done

   453 

   454 lemma [elim]: "\<lbrakk>inv_loop5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow> 

   455   inv_loop5 x (tl b, hd b # Oc # list)"

   456 apply(simp add: inv_loop5.simps)

   457 apply(case_tac "hd b", simp_all, auto)

   458 done

   459 

   460 lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Oc # list)\<rbrakk> \<Longrightarrow> 

   461                inv_loop1 x ([], Bk # Oc # list)"

   462 apply(auto simp: inv_loop6.simps inv_loop1.simps 

   463   inv_loop6_loop.simps inv_loop6_exit.simps)

   464 done

   465 

   466 lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Oc # list); b \<noteq> []\<rbrakk> 

   467            \<Longrightarrow> inv_loop1 x (tl b, hd b # Oc # list)"

   468 apply(auto simp: inv_loop6.simps inv_loop1.simps 

   469   inv_loop6_loop.simps inv_loop6_exit.simps)

   470 done

   471 

   472 lemma inv_loop_step: 

   473   "\<lbrakk>inv_loop x cf; x > 0\<rbrakk>

   474  \<Longrightarrow> inv_loop x (step cf (tcopy_loop, 0))"

   475 apply(case_tac cf, case_tac c, case_tac [2] aa)

   476 apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral_2_eq_2  

   477   numeral_3_eq_3 numeral_4_eq_4 numeral_5_eq_5 numeral_6_eq_6 split: if_splits)

   478 done

   479 

   480 lemma inv_loop_steps:

   481   "\<lbrakk>inv_loop x cf; x > 0\<rbrakk>

   482   \<Longrightarrow> inv_loop x (steps cf (tcopy_loop, 0) stp)"

   483 apply(induct stp, simp add: steps.simps, simp)

   484 apply(erule_tac inv_loop_step, simp)

   485 done

   486 

   487 fun loop_stage :: "config \<Rightarrow> nat"

   488   where

   489   "loop_stage (s, l, r) = (if s = 0 then 0

   490                            else (Suc (length (takeWhile (\<lambda>a. a = Oc) (rev l @ r)))))"

   491 

   492 fun loop_state :: "config \<Rightarrow> nat"

   493   where

   494   "loop_state (s, l, r) = (if s = 2 \<and> hd r = Oc then 0

   495                            else if s = 1 then 1

   496                            else 10 - s)"

   497 

   498 fun loop_step :: "config \<Rightarrow> nat"

   499   where

   500   "loop_step (s, l, r) = (if s = 3 then length r

   501                           else if s = 4 then length r

   502                           else if s = 5 then length l 

   503                           else if s = 6 then length l

   504                           else 0)"

   505 

   506 definition lex_triple :: 

   507  "((nat \<times> (nat \<times> nat)) \<times> (nat \<times> (nat \<times> nat))) set"

   508   where

   509   "lex_triple \<equiv> less_than <*lex*> lex_pair"

   510 

   511 lemma wf_lex_triple: "wf lex_triple"

   512   by (auto intro:wf_lex_prod simp:lex_triple_def lex_pair_def)

   513 

   514 fun loop_measure :: "config \<Rightarrow> nat \<times> nat \<times> nat"

   515   where

   516   "loop_measure c = 

   517    (loop_stage c, loop_state c, loop_step c)"

   518 

   519 definition loop_LE :: "(config \<times> config) set"

   520   where

   521    "loop_LE \<equiv> (inv_image lex_triple loop_measure)"

   522 

   523 lemma wf_loop_le: "wf loop_LE"

   524 by(auto intro:wf_inv_image simp: loop_LE_def wf_lex_triple)

   525 

   526 lemma [simp]: "inv_loop2 x ([], b) = False"

   527 apply(auto simp: inv_loop2.simps)

   528 done

   529 

   530 lemma  [simp]: "inv_loop2 x (l', []) = False"

   531 apply(auto simp: inv_loop2.simps)

   532 done

   533 

   534 lemma [simp]: "inv_loop3 x (b, []) = False"

   535 apply(auto simp: inv_loop3.simps)

   536 done

   537 

   538 lemma [simp]: "inv_loop4 x ([], b) = False"

   539 apply(auto simp: inv_loop4.simps)

   540 done

   541 

   542 lemma [elim]: 

   543   "\<lbrakk>inv_loop4 x (l', []); l' \<noteq> []; x > 0;

   544   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ [Oc])) \<noteq> 

   545   length (takeWhile (\<lambda>a. a = Oc) (rev l'))\<rbrakk>

   546   \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ [Oc])) < length (takeWhile (\<lambda>a. a = Oc) (rev l'))"

   547 apply(auto simp: inv_loop4.simps)

   548 apply(case_tac [!] j, simp_all add: List.takeWhile_tail)

   549 done

   550 

   551 

   552 lemma [elim]: 

   553   "\<lbrakk>inv_loop4 x (l', Bk # list); l' \<noteq> []; 0 < x;

   554    length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) \<noteq> 

   555     length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>

   556     \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) < 

   557     length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"

   558 apply(auto simp: inv_loop4.simps)

   559 done

   560 

   561 lemma takeWhile_replicate_append: 

   562   "P a \<Longrightarrow> takeWhile P (a\<up>x @ ys) = a\<up>x @ takeWhile P ys"

   563 apply(induct x, auto)

   564 done

   565 

   566 lemma takeWhile_replicate: 

   567   "P a \<Longrightarrow> takeWhile P (a\<up>x) = a\<up>x"

   568 by(induct x, auto)

   569 

   570 lemma [elim]: 

   571    "\<lbrakk>inv_loop5 x (l', Bk # list); l' \<noteq> []; 0 < x;

   572    length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \<noteq>

   573    length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>

   574    \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) < 

   575    length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"

   576 apply(auto simp: inv_loop5.simps inv_loop5_exit.simps)

   577 apply(case_tac [!] j, simp_all)

   578 apply(case_tac [!] "nat", simp_all)

   579 apply(case_tac  nata, simp_all add: List.takeWhile_tail)

   580 apply(simp add: takeWhile_replicate_append takeWhile_replicate)

   581 apply(case_tac  nata, simp_all add: List.takeWhile_tail)

   582 done

   583 

   584 lemma [elim]: "\<lbrakk>inv_loop1 x (l', Oc # list)\<rbrakk> \<Longrightarrow> hd list = Oc"

   585 apply(auto simp: inv_loop1.simps)

   586 done

   587 

   588 lemma [elim]: 

   589   "\<lbrakk>inv_loop6 x (l', Bk # list); l' \<noteq> []; 0 < x;

   590   length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \<noteq> 

   591   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>

   592   \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) < 

   593   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"

   594 apply(auto simp: inv_loop6.simps)

   595 apply(case_tac l', simp_all)

   596 done

   597 

   598 lemma [elim]:

   599   "\<lbrakk>inv_loop2 x (l', Oc # list); l' \<noteq> []; 0 < x\<rbrakk> \<Longrightarrow> 

   600   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list)) <

   601   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"

   602 apply(auto simp: inv_loop2.simps)

   603 apply(simp_all add: takeWhile_tail takeWhile_replicate_append

   604                 takeWhile_replicate)

   605 done

   606 

   607 lemma [elim]: 

   608   "\<lbrakk>inv_loop5 x (l', Oc # list); l' \<noteq> []; 0 < x;

   609   length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) \<noteq> 

   610   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))\<rbrakk>

   611   \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) < 

   612   length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"

   613 apply(auto simp: inv_loop5.simps)

   614 apply(case_tac l', auto)

   615 done

   616 

   617 

   618 lemma[elim]: 

   619   "\<lbrakk>inv_loop6 x (l', Oc # list); l' \<noteq> []; 0 < x;

   620   length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list))

   621   \<noteq> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))\<rbrakk>

   622   \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) < 

   623       length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"

   624 apply(case_tac l')

   625 apply(auto simp: inv_loop6.simps)

   626 done

   627 

   628 lemma loop_halt: 

   629   "\<lbrakk>x > 0; inv_loop x (Suc 0, l, r)\<rbrakk> \<Longrightarrow> 

   630       \<exists> stp. is_final (steps (Suc 0, l, r) (tcopy_loop, 0) stp)"

   631 proof(rule_tac LE = loop_LE in halt_lemma)

   632   show "wf loop_LE" by(intro wf_loop_le)

   633 next

   634   assume h: "0 < x"  and g: "inv_loop x (Suc 0, l, r)"

   635   show "\<forall>n. \<not> is_final (steps (Suc 0, l, r) (tcopy_loop, 0) n) \<longrightarrow> 

   636         (steps (Suc 0, l, r) (tcopy_loop, 0) (Suc n), steps (Suc 0, l, r) (tcopy_loop, 0) n) \<in> loop_LE"

   637   proof(rule_tac allI, rule_tac impI)

   638     fix n

   639     assume a: "\<not> is_final (steps (Suc 0, l, r) (tcopy_loop, 0) n)"

   640     obtain s' l' r' where d: "(steps (Suc 0, l, r) (tcopy_loop, 0) n) = (s', l', r')"

   641       by(case_tac "(steps (Suc 0, l, r) (tcopy_loop, 0) n)", auto)

   642     hence "inv_loop x (s', l', r') \<and> s' \<noteq> 0"

   643       using h g

   644       apply(drule_tac stp = n in inv_loop_steps, auto)

   645       using a

   646       apply(simp)

   647       done

   648     hence "(step(s', l', r') (tcopy_loop, 0), s', l', r') \<in> loop_LE"

   649       using h 

   650       apply(case_tac r', case_tac [2] a)

   651       apply(auto simp: inv_loop.simps step.simps tcopy_loop_def 

   652                        numeral_2_eq_2 numeral_3_eq_3 numeral_4_eq_4

   653                        numeral_5_eq_5 numeral_6_eq_6 loop_LE_def lex_triple_def lex_pair_def split: if_splits)

   654       done

   655     thus "(steps (Suc 0, l, r) (tcopy_loop, 0) (Suc n), 

   656           steps (Suc 0, l, r) (tcopy_loop, 0) n) \<in> loop_LE"

   657       using d

   658       apply(simp add: step_red)

   659       done

   660   qed

   661 qed

   662 

   663 lemma loop_correct:

   664   "x > 0 \<Longrightarrow> 

   665       {inv_loop1 x} (tcopy_loop, 0) {inv_loop0 x}"

   666 proof(rule_tac HoareI)

   667   fix l r

   668   assume h: "0 < x"

   669     "inv_loop1 x (l, r)"

   670   hence "\<exists> stp. is_final (steps (Suc 0, l, r) (tcopy_loop, 0) stp)"

   671     apply(rule_tac loop_halt, simp_all add: inv_loop.simps)

   672     done

   673   then obtain stp where "is_final (steps (Suc 0, l, r) (tcopy_loop, 0) stp)" ..

   674   moreover have "inv_loop x (steps (Suc 0, l, r) (tcopy_loop, 0) stp)"

   675     apply(rule_tac inv_loop_steps)

   676     using h by(simp_all add: inv_loop.simps)

   677   ultimately show

   678     "\<exists>n. is_final (steps (1, l, r) (tcopy_loop, 0) n) \<and> 

   679     inv_loop0 x holds_for steps (1, l, r) (tcopy_loop, 0) n"    

   680     using h

   681     apply(rule_tac x = stp in exI)

   682     apply(case_tac "(steps (Suc 0, l, r) (tcopy_loop, 0) stp)", 

   683       simp add: inv_init.simps inv_loop.simps)

   684     done

   685 qed

   686   

   687 definition tcopy_end :: "instr list"

   688   where

   689   "tcopy_end \<equiv> [(L, 0), (R, 2), (W1, 3), (L, 4),

   690                 (R, 2), (R, 2), (L, 5), (W0, 4),

   691                 (R, 0), (L, 5)]"

   692 

   693 fun inv_end1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   694   where

   695   "inv_end1 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x)"

   696 

   697 fun inv_end2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   698   where

   699   "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>)"

   700 

   701 fun inv_end3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   702   where

   703   "inv_end3 x (l, r) =

   704         (\<exists> i j. x > 0 \<and> i + j = x \<and> l = Oc\<up>i @ [Bk] \<and> r = Oc # Bk\<up>j@ Oc\<up>x )"

   705 

   706 fun inv_end4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   707   where

   708   "inv_end4 x (l, r) = (\<exists> any. x > 0 \<and> l = Oc\<up>x @ [Bk] \<and> r = any#Oc\<up>x)"

   709 

   710 fun inv_end5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   711   where

   712   "inv_end5_loop x (l, r) = 

   713          (\<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)"

   714 

   715 fun inv_end5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   716   where

   717   "inv_end5_exit x (l, r) = (x > 0 \<and> l = [] \<and> r = Bk # Oc\<up>x @ Bk # Oc\<up>x)"

   718 

   719 fun inv_end5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

   720   where

   721   "inv_end5 x (l, r) = (inv_end5_loop x (l, r) \<or> inv_end5_exit x (l, r))"

   722 

   723 fun inv_end0 :: "nat \<Rightarrow> tape \<Rightarrow>  bool"

   724   where

   725   "inv_end0 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc\<up>x @ Bk # Oc\<up>x)"

   726 

   727 fun inv_end :: "nat \<Rightarrow> config \<Rightarrow> bool"

   728   where

   729   "inv_end x (s, l, r) = (if s = 0 then inv_end0 x (l, r)

   730                           else if s = 1 then inv_end1 x (l, r)

   731                           else if s = 2 then inv_end2 x (l, r)

   732                           else if s = 3 then inv_end3 x (l, r)

   733                           else if s = 4 then inv_end4 x (l, r)

   734                           else if s = 5 then inv_end5 x (l, r)

   735                           else False)"

   736 

   737 declare inv_end.simps[simp del] inv_end1.simps[simp del]

   738         inv_end0.simps[simp del] inv_end2.simps[simp del]

   739         inv_end3.simps[simp del] inv_end4.simps[simp del]

   740         inv_end5.simps[simp del]

   741 

   742 lemma [simp]:  "inv_end1 x (b, []) = False"

   743 apply(auto simp: inv_end1.simps)

   744 done

   745 

   746 lemma [simp]: "inv_end2 x (b, []) = False"

   747 apply(auto simp: inv_end2.simps)

   748 done

   749 

   750 lemma [simp]: "inv_end3 x (b, []) = False"

   751 apply(auto simp: inv_end3.simps)

   752 done

   753 

   754 thm inv_end4.simps

   755 lemma [simp]: "inv_end4 x (b, []) = False"

   756 apply(auto simp: inv_end4.simps)

   757 done

   758 

   759 lemma [simp]: "inv_end5 x (b, []) = False"

   760 apply(auto simp: inv_end5.simps)

   761 done

   762 

   763 lemma [simp]: "inv_end1 x ([], list) = False"

   764 apply(auto simp: inv_end1.simps)

   765 done

   766 

   767 lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Bk # list); b \<noteq> []\<rbrakk>

   768   \<Longrightarrow> inv_end0 x (tl b, hd b # Bk # list)"

   769 apply(auto simp: inv_end1.simps inv_end0.simps)

   770 done

   771 

   772 lemma [elim]: "\<lbrakk>0 < x; inv_end2 x (b, Bk # list)\<rbrakk> 

   773   \<Longrightarrow> inv_end3 x (b, Oc # list)"

   774 apply(auto simp: inv_end2.simps inv_end3.simps)

   775 apply(rule_tac x = "j - 1" in exI)

   776 apply(case_tac j, simp_all)

   777 apply(case_tac x, simp_all)

   778 done

   779 

   780 lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Bk # b, list)"

   781 apply(auto simp: inv_end2.simps inv_end3.simps)

   782 done

   783   

   784 lemma [elim]: "\<lbrakk>0 < x; inv_end4 x ([], Bk # list)\<rbrakk> \<Longrightarrow> 

   785   inv_end5 x ([], Bk # Bk # list)"

   786 apply(auto simp: inv_end4.simps inv_end5.simps)

   787 done

   788  

   789 lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> 

   790   inv_end5 x (tl b, hd b # Bk # list)"

   791 apply(auto simp: inv_end4.simps inv_end5.simps)

   792 apply(rule_tac x = 1 in exI, simp)

   793 done

   794 

   795 lemma [elim]: "\<lbrakk>0 < x; inv_end5 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end0 x (Bk # b, list)"

   796 apply(auto simp: inv_end5.simps inv_end0.simps)

   797 apply(case_tac [!] j, simp_all)

   798 done

   799 

   800 lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"

   801 apply(auto simp: inv_end1.simps inv_end2.simps)

   802 done

   803 

   804 lemma [elim]: "\<lbrakk>0 < x; inv_end2 x ([], Oc # list)\<rbrakk> \<Longrightarrow>

   805                inv_end4 x ([], Bk # Oc # list)"

   806 apply(auto simp: inv_end2.simps inv_end4.simps)

   807 done

   808 

   809 lemma [elim]:  "\<lbrakk>0 < x; inv_end2 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>

   810   inv_end4 x (tl b, hd b # Oc # list)"

   811 apply(auto simp: inv_end2.simps inv_end4.simps)

   812 apply(case_tac [!] j, simp_all)

   813 done

   814 

   815 lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"

   816 apply(auto simp: inv_end2.simps inv_end3.simps)

   817 done

   818 

   819 lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end4 x (b, Bk # list)"

   820 apply(auto simp: inv_end2.simps inv_end4.simps)

   821 done

   822 

   823 lemma [elim]: "\<lbrakk>0 < x; inv_end5 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_end5 x ([], Bk # Oc # list)"

   824 apply(auto simp: inv_end2.simps inv_end5.simps)

   825 done

   826 

   827 declare inv_end5_loop.simps[simp del]

   828         inv_end5_exit.simps[simp del]

   829 

   830 lemma [simp]: "inv_end5_exit x (b, Oc # list) = False"

   831 apply(auto simp: inv_end5_exit.simps)

   832 done

   833 

   834 lemma [simp]: "inv_end5_loop x (tl b, Bk # Oc # list) = False"

   835 apply(auto simp: inv_end5_loop.simps)

   836 apply(case_tac [!] j, simp_all)

   837 done

   838 

   839 lemma [elim]:

   840   "\<lbrakk>0 < x; inv_end5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk> \<Longrightarrow>

   841   inv_end5_exit x (tl b, Bk # Oc # list)"

   842 apply(auto simp: inv_end5_loop.simps inv_end5_exit.simps)

   843 apply(case_tac [!] i, simp_all)

   844 done

   845 

   846 lemma [elim]: 

   847   "\<lbrakk>0 < x; inv_end5_loop x (b, Oc # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow>

   848   inv_end5_loop x (tl b, Oc # Oc # list)"

   849 apply(simp only: inv_end5_loop.simps inv_end5_exit.simps)

   850 apply(erule_tac exE)+

   851 apply(rule_tac x = "i - 1" in exI, 

   852       rule_tac x = "Suc j" in exI, auto)

   853 apply(case_tac [!] i, simp_all)

   854 done

   855 

   856 lemma [elim]: "\<lbrakk>0 < x; inv_end5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow> 

   857   inv_end5 x (tl b, hd b # Oc # list)"

   858 apply(simp add: inv_end2.simps inv_end5.simps)

   859 apply(case_tac "hd b", simp_all, auto)

   860 done

   861 

   862 lemma inv_end_step:

   863   "\<lbrakk>x > 0;

   864  inv_end x cf\<rbrakk>

   865  \<Longrightarrow> inv_end x (step cf (tcopy_end, 0))"

   866 apply(case_tac cf, case_tac c, case_tac [2] aa)

   867 apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral_2_eq_2 

   868   numeral_3_eq_3 numeral_4_eq_4 numeral_5_eq_5 split: if_splits)

   869 done

   870 

   871 lemma inv_end_steps:

   872   "\<lbrakk>x > 0; inv_end x cf\<rbrakk>

   873 \<Longrightarrow> inv_end x (steps cf (tcopy_end, 0) stp)"

   874 apply(induct stp, simp add:steps.simps, simp)

   875 apply(erule_tac inv_end_step, simp)

   876 done

   877 

   878 fun end_state :: "config \<Rightarrow> nat"

   879   where

   880   "end_state (s, l, r) = 

   881        (if s = 0 then 0

   882         else if s = 1 then 5

   883         else if s = 2 \<or> s = 3 then 4

   884         else if s = 4 then 3 

   885         else if s = 5 then 2

   886         else 0)"

   887 

   888 fun end_stage :: "config \<Rightarrow> nat"

   889   where

   890   "end_stage (s, l, r) = 

   891           (if s = 2 \<or> s = 3 then (length r)

   892            else 0)"

   893 

   894 fun end_step :: "config \<Rightarrow> nat"

   895   where

   896   "end_step (s, l, r) = 

   897          (if s = 4 then (if hd r = Oc then 1 else 0)

   898           else if s = 5 then length l

   899           else if s = 2 then 1

   900           else if s = 3 then 0

   901           else 0)"

   902 

   903 fun end_measure :: "config \<Rightarrow> nat \<times> nat \<times> nat"

   904   where

   905   "end_measure c = 

   906    (end_state c, end_stage c, end_step c)"

   907 

   908 definition end_LE :: "(config \<times> config) set"

   909   where

   910    "end_LE \<equiv> (inv_image lex_triple end_measure)"

   911 

   912 lemma wf_end_le: "wf end_LE"

   913 by(auto intro:wf_inv_image simp: end_LE_def wf_lex_triple)

   914 

   915 lemma [simp]: "inv_end5 x ([], Oc # list) = False"

   916 apply(auto simp: inv_end5.simps inv_end5_loop.simps)

   917 done

   918 

   919 lemma end_halt: 

   920   "\<lbrakk>x > 0; inv_end x (Suc 0, l, r)\<rbrakk> \<Longrightarrow> 

   921       \<exists> stp. is_final (steps (Suc 0, l, r) (tcopy_end, 0) stp)"

   922 proof(rule_tac LE = end_LE in halt_lemma)

   923   show "wf end_LE" by(intro wf_end_le)

   924 next

   925   assume great: "0 < x"

   926     and inv_start: "inv_end x (Suc 0, l, r)"

   927   show "\<forall>n. \<not> is_final (steps (Suc 0, l, r) (tcopy_end, 0) n) \<longrightarrow> 

   928     (steps (Suc 0, l, r) (tcopy_end, 0) (Suc n), steps (Suc 0, l, r) (tcopy_end, 0) n) \<in> end_LE"

   929   proof(rule_tac allI, rule_tac impI)

   930     fix n

   931     assume notfinal: "\<not> is_final (steps (Suc 0, l, r) (tcopy_end, 0) n)"

   932     obtain s' l' r' where d: "steps (Suc 0, l, r) (tcopy_end, 0) n = (s', l', r')"

   933       apply(case_tac "steps (Suc 0, l, r) (tcopy_end, 0) n", auto)

   934       done

   935     hence "inv_end x (s', l', r') \<and> s' \<noteq> 0"

   936       using great inv_start notfinal

   937       apply(drule_tac stp = n in inv_end_steps, auto)

   938       done

   939     hence "(step (s', l', r') (tcopy_end, 0), s', l', r') \<in> end_LE"

   940       apply(case_tac r', case_tac [2] a)

   941       apply(auto simp: inv_end.simps step.simps tcopy_end_def 

   942                        numeral_2_eq_2 numeral_3_eq_3 numeral_4_eq_4 

   943                        numeral_5_eq_5 numeral_6_eq_6 end_LE_def lex_triple_def lex_pair_def split: if_splits)

   944       done

   945     thus "(steps (Suc 0, l, r) (tcopy_end, 0) (Suc n), 

   946       steps (Suc 0, l, r) (tcopy_end, 0) n) \<in> end_LE"

   947       using d

   948       by simp

   949   qed

   950 qed

   951 

   952 lemma end_correct:

   953   "x > 0 \<Longrightarrow> 

   954       {inv_end1 x} (tcopy_end, 0) {inv_end0 x}"

   955 proof(rule_tac HoareI)

   956   fix l r

   957   assume h: "0 < x"

   958     "inv_end1 x (l, r)"

   959   hence "\<exists> stp. is_final (steps (Suc 0, l, r) (tcopy_end, 0) stp)"

   960     apply(rule_tac end_halt, simp_all add: inv_end.simps)

   961     done

   962   then obtain stp where "is_final (steps (Suc 0, l, r) (tcopy_end, 0) stp)" ..

   963   moreover have "inv_end x (steps (Suc 0, l, r) (tcopy_end, 0) stp)"

   964     apply(rule_tac inv_end_steps)

   965     using h by(simp_all add: inv_end.simps)

   966   ultimately show

   967     "\<exists>n. is_final (steps (1, l, r) (tcopy_end, 0) n) \<and> 

   968     inv_end0 x holds_for steps (1, l, r) (tcopy_end, 0) n"        

   969     using h

   970     apply(rule_tac x = stp in exI)

   971     apply(case_tac "(steps (Suc 0, l, r) (tcopy_end, 0) stp)", 

   972       simp add:  inv_end.simps)

   973     done

   974 qed

   975 

   976 definition tcopy :: "instr list"

   977   where

   978   "tcopy = ((tcopy_init |+| tcopy_loop) |+| tcopy_end)"

   979 

   980 lemma [intro]: "tm_wf (tcopy_init, 0)"

   981 by(auto simp: tm_wf.simps tcopy_init_def)

   982 

   983 lemma [intro]: "tm_wf (tcopy_loop, 0)"

   984 by(auto simp: tm_wf.simps tcopy_loop_def)

   985 

   986 lemma [intro]: "tm_wf (tcopy_end, 0)"

   987 by(auto simp: tm_wf.simps tcopy_end_def)

   988 

   989 lemma [intro]: "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0)\<rbrakk> \<Longrightarrow> tm_wf (A |+| B, 0)"

   990 apply(auto simp: tm_wf.simps shift.simps adjust.simps length_comp

   991                  tm_comp.simps)

   992 done

   993 

   994 lemma tcopy_correct1: 

   995   "\<lbrakk>x > 0\<rbrakk> \<Longrightarrow> {inv_init1 x} (tcopy, 0) {inv_end0 x}"

   996 proof(simp add: tcopy_def, rule_tac Hoare_plus_halt)

   997   show "inv_loop0 x \<mapsto> inv_end1 x"

   998     by(auto simp: inv_end1.simps inv_loop1.simps assert_imp_def)

   999 next

  1000   show "tm_wf (tcopy_init |+| tcopy_loop, 0)" by auto

  1001 next

  1002   show "tm_wf (tcopy_end, 0)" by auto

  1003 next

  1004   assume "0 < x"

  1005   thus "{inv_init1 x} (tcopy_init |+| tcopy_loop, 0) {inv_loop0 x}"

  1006   proof(rule_tac Hoare_plus_halt)

  1007     show "inv_init0 x \<mapsto> inv_loop1 x"

  1008       apply(auto simp: inv_init0.simps inv_loop1.simps assert_imp_def)

  1009       apply(rule_tac x = "Suc 0" in exI, auto)

  1010       done

  1011   next

  1012     show "tm_wf (tcopy_init, 0)" by auto

  1013   next

  1014     show "tm_wf (tcopy_loop, 0)" by auto

  1015   next

  1016     assume "0 < x"

  1017     thus "{inv_init1 x} (tcopy_init, 0) {inv_init0 x}"

  1018       by(erule_tac init_correct)

  1019   next

  1020     assume "0 < x"

  1021     thus "{inv_loop1 x} (tcopy_loop, 0) {inv_loop0 x}"

  1022       by(erule_tac loop_correct)

  1023   qed

  1024 next

  1025   assume "0 < x"

  1026   thus "{inv_end1 x} (tcopy_end, 0) {inv_end0 x}"

  1027     by(erule_tac end_correct)

  1028 qed

  1029 

  1030 section {*

  1031   The {\em Dithering} Turing Machine 

  1032 *}

  1033 

  1034 text {*

  1035   The {\em Dithering} TM, when the input is @{text "1"}, it will loop forever, otherwise, it will

  1036   terminate.

  1037 *}

  1038 definition dither :: "instr list"

  1039   where

  1040   "dither \<equiv> [(W0, 1), (R, 2), (L, 1), (L, 0)] "

  1041 

  1042 lemma dither_halt_rs: 

  1043   "\<exists> stp. steps (Suc 0, Bk\<up>m, [Oc, Oc]) (dither, 0) stp = 

  1044                                  (0, Bk\<up>m, [Oc, Oc])"

  1045 apply(rule_tac x = "Suc (Suc (Suc 0))" in exI)

  1046 apply(simp add: dither_def steps.simps 

  1047                 step.simps fetch.simps numeral_2_eq_2)

  1048 done

  1049 

  1050 lemma dither_unhalt_state: 

  1051   "(steps (Suc 0, Bk\<up>m, [Oc]) (dither, 0) stp = 

  1052    (Suc 0, Bk\<up>m, [Oc])) \<or> 

  1053    (steps (Suc 0, Bk\<up>m, [Oc]) (dither, 0) stp = (2, Oc # Bk\<up>m, []))"

  1054   apply(induct stp, simp add: steps.simps)

  1055   apply(simp add: step_red, auto)

  1056   apply(auto simp: step.simps fetch.simps dither_def numeral_2_eq_2)

  1057   done

  1058 

  1059 lemma dither_unhalt_rs: 

  1060   "\<not> is_final (steps (Suc 0, Bk\<up>m, [Oc]) (dither,0) stp)"

  1061 using dither_unhalt_state[of m stp]

  1062 apply(auto)

  1063 done

  1064 

  1065 section {*

  1066   The final diagnal arguments to show the undecidability of Halting problem.

  1067 *}

  1068 

  1069 text {*

  1070   @{text "haltP tp x"} means TM @{text "tp"} terminates on input @{text "x"}

  1071   and the final configuration is standard.

  1072 *}

  1073 

  1074 

  1075 fun tape_of_nat_list :: "nat list \<Rightarrow> cell list" ("< _ >" [0] 100)

  1076   where 

  1077   "tape_of_nat_list [] = []" |

  1078   "tape_of_nat_list [n] = Oc\<up>(Suc n)" |

  1079   "tape_of_nat_list (n#ns) = Oc\<up>(Suc n) @ Bk # (tape_of_nat_list ns)"

  1080 

  1081 definition haltP :: "tprog \<Rightarrow> nat list \<Rightarrow> bool"

  1082   where

  1083   "haltP t lm = (\<exists>n a b c. steps (Suc 0, [], <lm>) t n = (0, Bk\<up>a,  Oc\<up>b @ Bk\<up>c))"

  1084 

  1085 lemma [intro]: "tm_wf (tcopy, 0)"

  1086 by(auto simp: tcopy_def)

  1087 

  1088 lemma [intro]: "tm_wf (dither, 0)"

  1089 apply(auto simp: tm_wf.simps dither_def)

  1090 done

  1091 

  1092 text {*

  1093   The following lemma shows the meaning of @{text "tinres"} with respect to 

  1094   one step execution.

  1095   *}

  1096 lemma tinres_step: 

  1097   "\<lbrakk>tinres l l'; step (ss, l, r) (t, 0) = (sa, la, ra); 

  1098                  step (ss, l', r) (t, 0) = (sb, lb, rb)\<rbrakk>

  1099     \<Longrightarrow> tinres la lb \<and> ra = rb \<and> sa = sb"

  1100 apply(case_tac ss, case_tac [!]r, case_tac [!] "a::cell")

  1101 apply(auto simp: step.simps fetch.simps

  1102         split: if_splits )

  1103 apply(case_tac [!] "t ! (2 * nat)", 

  1104      auto simp: tinres_def split: if_splits)

  1105 apply(case_tac [1-8] a, auto split: if_splits)

  1106 apply(case_tac [!] "t ! (2 * nat)", 

  1107      auto simp: tinres_def split: if_splits)

  1108 apply(case_tac [1-4] a, auto split: if_splits)

  1109 apply(case_tac [!] "t ! Suc (2 * nat)", 

  1110      auto simp: if_splits)

  1111 apply(case_tac [!] aa, auto split: if_splits)

  1112 done

  1113 

  1114 text {*

  1115   The following lemma shows the meaning of @{text "tinres"} with respect to 

  1116   many step execution.

  1117   *}

  1118 

  1119 lemma tinres_steps: 

  1120   "\<lbrakk>tinres l l'; steps (ss, l, r) (t, 0) stp = (sa, la, ra); 

  1121                  steps (ss, l', r) (t, 0) stp = (sb, lb, rb)\<rbrakk>

  1122     \<Longrightarrow> tinres la lb \<and> ra = rb \<and> sa = sb"

  1123 apply(induct stp arbitrary: sa la ra sb lb rb, simp add: steps.simps)

  1124 apply(simp add: step_red)

  1125 apply(case_tac "(steps (ss, l, r) (t, 0) stp)")

  1126 apply(case_tac "(steps (ss, l', r) (t, 0) stp)")

  1127 proof -

  1128   fix stp sa la ra sb lb rb a b c aa ba ca

  1129   assume ind: "\<And>sa la ra sb lb rb. \<lbrakk>steps (ss, l, r) (t, 0) stp = (sa, (la::cell list), ra); 

  1130           steps (ss, l', r) (t, 0) stp = (sb, lb, rb)\<rbrakk> \<Longrightarrow> tinres la lb \<and> ra = rb \<and> sa = sb"

  1131   and h: " tinres l l'" "step (steps (ss, l, r) (t, 0) stp) (t, 0) = (sa, la, ra)"

  1132          "step (steps (ss, l', r) (t, 0) stp) (t, 0) = (sb, lb, rb)" "steps (ss, l, r) (t, 0) stp = (a, b, c)" 

  1133          "steps (ss, l', r) (t, 0) stp = (aa, ba, ca)"

  1134   have "tinres b ba \<and> c = ca \<and> a = aa"

  1135     apply(rule_tac ind, simp_all add: h)