25 type_synonym tprog = "instr list"

    22 type_synonym tprog = "instr list \<times> nat"

    30   "nth_of [] _ = None"

    27   "nth_of xs i = (if i \<ge> length xs then None

    31 | "nth_of (x # xs) 0 = Some x"

    28                   else Some (xs ! i))"

    32 | "nth_of (x # xs) (Suc n) = nth_of xs n" 

    43   fetch :: "tprog \<Rightarrow> state \<Rightarrow> cell \<Rightarrow> instr"

    39   fetch :: "instr list \<Rightarrow> state \<Rightarrow> cell \<Rightarrow> instr"

    75 

    71 fun step :: "config \<Rightarrow> tprog \<Rightarrow> config"

    76 fun 

    72   where 

    77   step :: "config \<Rightarrow> tprog \<Rightarrow> config"

    73   "step (s, l, r) (p, off) = 

    78 where

    74   (let (a, s') = fetch p (s - off) (read r) in (s', update a (l, r)))"

    79   "step (s, l, r) p = (let (a, s') = fetch p s (read r) in (s', update a (l, r)))"

    94 definition 

    89 fun 

    97   "tm_wf p = (length p \<ge> 2 \<and> iseven (length p) \<and> (\<forall>(a, s) \<in> set p. s \<le> length p div 2))"

    92   "tm_wf (p, off) = (length p \<ge> 2 \<and> length p mod 2 = 0 \<and> 

    93                     (\<forall>(a, s) \<in> set p. s \<le> length p div 2

    94                                              + off \<and> s \<ge> off))"

   113   shift :: "tprog \<Rightarrow> nat \<Rightarrow> tprog"

   110   shift :: "instr list \<Rightarrow> nat \<Rightarrow> instr list"

   123   adjust :: "tprog \<Rightarrow> tprog"

   120   adjust :: "instr list \<Rightarrow> instr list"

   124 where

   121 where

   125   "adjust p = map (\<lambda> (a, s). (a, if s = 0 then ((length p) div 2) + 1 else s)) p"

   122   "adjust p = map (\<lambda> (a, s). (a, if s = 0 then (Suc (length p div 2)) else s)) p"

   131 definition

   128 fun

   132   tm_comp :: "tprog \<Rightarrow> tprog \<Rightarrow> tprog" ("_ |+| _" [0, 0] 100)

   129   tm_comp :: "instr list \<Rightarrow> instr list \<Rightarrow> instr list" ("_ |+| _" [0, 0] 100)

   143   shows "is_final (steps (s, l, r) p n)"

   140   shows "is_final (steps (s, l, r) (p, off) n)"

   161   shows "Q holds_for (steps c p n) = Q holds_for c"

   160   shows "Q holds_for (steps c (p, off) n) = Q holds_for c"

   188     by auto

   187     by(case_tac p) (auto)

   210   obtains n' where "\<not> is_final (steps (1, tp) A n')" and "steps (1, tp) A (Suc n') = (0, tp')"

   219   obtains n' where "\<not> is_final (steps (1, tp) A n')" 

   211 using assms 

   220         and "steps (1, tp) A (Suc n') = (0, tp')"

   212 apply(induct n)

   221 proof -

   222   from assms have "\<exists> n'. \<not> is_final (steps (1, tp) A n') \<and> 

   223                steps (1, tp) A (Suc n') = (0, tp')"

   224   proof(induct n arbitrary: tp', simp add: steps.simps)

   225     fix n tp'

   226     assume ind: 

   227       "\<And>tp'. steps (1, tp) A n = (0, tp') \<Longrightarrow>

   228       \<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')"

   229     and h: " steps (1, tp) A (Suc n) = (0, tp')"

   230     from h show  "\<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')"

   231     proof(simp add: step_red del: steps.simps, 

   232                      case_tac "(steps (Suc 0, tp) A n)", case_tac "a = 0", simp)

   233       fix a b c

   234       assume " steps (Suc 0, tp) A n = (0, tp')"

   235       hence "\<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')"

   236         apply(rule_tac ind, simp)

   237         done

   238       thus "\<exists>n'. \<not> is_final (steps (Suc 0, tp) A n') \<and> step (steps (Suc 0, tp) A n') A = (0, tp')"

   239         apply(simp)

   240         done

   241     next

   242       fix a b c

   243       assume "steps (Suc 0, tp) A n = (a, b, c)"

   244              "step (steps (Suc 0, tp) A n) A = (0, tp')"

   245         "a \<noteq> 0"

   246       thus "\<exists>n'. \<not> is_final (steps (Suc 0, tp) A n') \<and> 

   247         step (steps (Suc 0, tp) A n') A = (0, tp')"

   248         apply(rule_tac x = n in exI, simp)

   249         done

   250     qed

   251   qed

   252   thus "(\<And>n'. \<lbrakk>\<not> is_final (steps (1, tp) A n'); 

   253     steps (1, tp) A (Suc n') = (0, tp')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis"

   254     by auto

   255 qed

   256 

   257 declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del]

   258 

   259 lemma length_comp:

   260 "length (A |+| B) = length A + length B"

   261 apply(auto simp: tm_comp.simps)

   262 done

   263 

   264 lemma tmcomp_fetch_in_first:

   265   assumes "case (fetch A a x) of (ac, ns) \<Rightarrow> ns \<noteq> 0"

   266   shows "fetch (A |+| B) a x = fetch A a x"

   267 using assms

   268 apply(case_tac a, case_tac [!] x, 

   269 auto simp: length_comp tm_comp.simps length_adjust nth_append)

   270 apply(simp_all add: adjust.simps)

   271 done

   272 

   273 

   274 lemma is_final_eq: "is_final (ba, tp) = (ba = 0)"

   275 apply(case_tac tp, simp add: is_final.simps)

   276 done

   277 

   278 lemma t_merge_pre_eq_step: 

   279   assumes step: "step (a, b, c) (A, 0) = cf"

   280   and     tm_wf: "tm_wf (A, 0)" 

   281   and     unfinal: "\<not> is_final cf"

   282   shows "step (a, b, c) (A |+| B, 0) = cf"

   283 proof -

   284   have "fetch (A |+| B) a (read c) = fetch A a (read c)"

   285   proof(rule_tac tmcomp_fetch_in_first)

   286     from step and unfinal show "case fetch A a (read c) of (ac, ns) \<Rightarrow> ns \<noteq> 0"

   287       apply(auto simp: is_final.simps)

   288       apply(case_tac "fetch A a (read c)", simp_all add: is_final_eq)

   289       done

   290   qed      

   291   thus "?thesis"

   292     using step

   293     apply(auto simp: step.simps is_final.simps)

   294     done

   295 qed

   296 

   297 declare tm_wf.simps[simp del] step.simps[simp del]

   298 

   299 lemma t_merge_pre_eq:  

   300   "\<lbrakk>steps (Suc 0, tp) (A, 0) stp = cf; \<not> is_final cf; tm_wf (A, 0)\<rbrakk>

   301   \<Longrightarrow> steps (Suc 0, tp) (A |+| B, 0) stp = cf"

   302 proof(induct stp arbitrary: cf, simp add: steps.simps)

   303   fix stp cf

   304   assume ind: "\<And>cf. \<lbrakk>steps (Suc 0, tp) (A, 0) stp = cf; \<not> is_final cf; tm_wf (A, 0)\<rbrakk> 

   305     \<Longrightarrow> steps (Suc 0, tp) (A |+| B, 0) stp = cf"

   306   and h: "steps (Suc 0, tp) (A, 0) (Suc stp) = cf"

   307       "\<not> is_final cf" "tm_wf (A, 0)"

   308   from h show "steps (Suc 0, tp) (A |+| B, 0) (Suc stp) = cf"

   309   proof(simp add: step_red, case_tac "(steps (Suc 0, tp) (A, 0) stp)", simp)

   310     fix a b c

   311     assume g: "steps (Suc 0, tp) (A, 0) stp = (a, b, c)"

   312       "step (a, b, c) (A, 0) = cf"

   313     have "(steps (Suc 0, tp) (A |+| B, 0) stp) = (a, b, c)"

   314     proof(rule ind, simp_all add: h g)

   315       show "0 < a"

   316         using g h

   317         apply(simp add: step_red)

   318         apply(case_tac a, auto simp: step_0)

   319         apply(case_tac "steps (Suc 0, tp) (A, 0) stp", simp)

   320         done

   321     qed

   322     thus "step (steps (Suc 0, tp) (A |+| B, 0) stp) (A |+| B, 0) = cf"

   323       apply(simp)

   324       apply(rule_tac t_merge_pre_eq_step, simp_all add: g h)

   325       done

   326   qed

   327 qed

   328 

   329 lemma tmcomp_fetch_in_first2:

   330   assumes "fetch A a x = (ac, 0)"

   331           "tm_wf (A, 0)"

   332           "a \<le> length A div 2" "a > 0"

   333   shows "fetch (A |+| B) a x = (ac, Suc (length A div 2))"

   334 using assms

   335 apply(case_tac a, case_tac [!] x, 

   336 auto simp: length_comp tm_comp.simps length_adjust nth_append)

   337 apply(simp_all add: adjust.simps)

   338 done

   339 

   340 lemma tmcomp_exec_after_first:

   341   "\<lbrakk>0 < a; step (a, b, c) (A, 0) = (0, tp'); tm_wf (A, 0); 

   342        a \<le> length A div 2\<rbrakk>

   343        \<Longrightarrow> step (a, b, c) (A |+| B, 0) = (Suc (length A div 2), tp')"

   344 apply(simp add: step.simps, auto)

   345 apply(case_tac "fetch A a Bk", simp add: tmcomp_fetch_in_first2)

   346 apply(case_tac "fetch A a (hd c)", simp add: tmcomp_fetch_in_first2)

   347 done

   348 

   349 lemma step_nothalt_pre: "\<lbrakk>step (aa, ba, ca) (A, 0) = (a, b, c);  0 < a\<rbrakk> \<Longrightarrow> 0 < aa"

   350 apply(case_tac "aa = 0", simp add: step_0, simp)

   351 done

   352 

   353 lemma nth_in_set: 

   354   "\<lbrakk> A ! i = x; i <  length A\<rbrakk> \<Longrightarrow> x \<in> set A"

   355 by auto

   356 

   357 lemma step_nothalt: 

   358   "\<lbrakk>step (aa, ba, ca) (A, 0) = (a, b, c); 0 < a; tm_wf (A, 0)\<rbrakk> \<Longrightarrow> 

   359   a \<le> length A div 2"

   360 apply(simp add: step.simps)

   361 apply(case_tac aa, case_tac [!] aa, auto split: if_splits simp: tm_wf.simps)

   362 apply(case_tac "A ! (2 * nat)", simp)

   363 apply(erule_tac x = "(aa, a)" in ballE, simp_all add: nth_in_set)

   364 apply(case_tac "hd ca", auto split: if_splits simp: tm_wf.simps)

   365 apply(case_tac "A ! (2 * nat)", simp)

   366 apply(erule_tac x = "(aa, a)" in ballE, simp_all add: nth_in_set)

   367 apply(case_tac "A ! (Suc (2 * nat))")

   368 apply(erule_tac x = "(aa,bb)" in ballE, simp_all add: nth_in_set)

   369 done

   370 

   371 lemma steps_in_range: 

   372   " \<lbrakk>0 < a; steps (Suc 0, tp) (A, 0) stp = (a, b, c); tm_wf (A, 0)\<rbrakk>

   373   \<Longrightarrow> a \<le> length A div 2"

   374 proof(induct stp arbitrary: a b c)

   375   fix a b c

   376   assume h: "0 < a" "steps (Suc 0, tp) (A, 0) 0 = (a, b, c)" 

   377             "tm_wf (A, 0)"

   378   thus "a \<le> length A div 2"

   379     apply(simp add: steps.simps tm_wf.simps, auto)

   380     done

   381 next

   382   fix stp a b c

   383   assume ind: "\<And>a b c. \<lbrakk>0 < a; steps (Suc 0, tp) (A, 0) stp = (a, b, c); 

   384     tm_wf (A, 0)\<rbrakk> \<Longrightarrow> a \<le> length A div 2"

   385   and h: "0 < a" "steps (Suc 0, tp) (A, 0) (Suc stp) = (a, b, c)" "tm_wf (A, 0)"

   386   from h show "a \<le> length A div 2"

   387   proof(simp add: step_red, case_tac "(steps (Suc 0, tp) (A, 0) stp)", simp)

   388     fix aa ba ca

   389     assume g: "step (aa, ba, ca) (A, 0) = (a, b, c)" 

   390            "steps (Suc 0, tp) (A, 0) stp = (aa, ba, ca)"

   391     hence "aa \<le> length A div 2"

   392       apply(rule_tac ind, auto simp: h step_nothalt_pre)

   393       done

   394     thus "?thesis"

   395       using g h

   396       apply(rule_tac step_nothalt, auto)

   397       done

   398   qed

   399 qed

   400 

   401 lemma t_merge_pre_halt_same: 

   402   assumes a_ht: "steps (1, tp) (A, 0) n = (0, tp')"

   403   and a_wf: "tm_wf (A, 0)"

   404   obtains n' where "steps (1, tp) (A |+| B, 0) n' = (Suc (length A div 2), tp')"

   405 proof -

   406   assume a: "\<And>n. steps (1, tp) (A |+| B, 0) n = (Suc (length A div 2), tp') \<Longrightarrow> thesis"

   407   obtain stp' where "\<not> is_final (steps (1, tp) (A, 0) stp')" and 

   408                           "steps (1, tp) (A, 0) (Suc stp') = (0, tp')"

   409   using a_ht before_final by blast

   410   then have "steps (1, tp) (A |+| B, 0) (Suc stp') = (Suc (length A div 2), tp')"

   411   proof(simp add: step_red)

   412     assume "\<not> is_final (steps (Suc 0, tp) (A, 0) stp')"

   413            " step (steps (Suc 0, tp) (A, 0) stp') (A, 0) = (0, tp')"

   414     moreover hence "(steps (Suc 0, tp) (A |+| B, 0) stp') = (steps (Suc 0, tp) (A, 0) stp')"

   415       apply(rule_tac t_merge_pre_eq)

   416       apply(simp_all add: a_wf a_ht)

   417       done

   418     ultimately show "step (steps (Suc 0, tp) (A |+| B, 0) stp') (A |+| B, 0) = (Suc (length A div 2), tp')"

   419       apply(case_tac " steps (Suc 0, tp) (A, 0) stp'", simp)

   420       apply(rule tmcomp_exec_after_first, simp_all add: a_wf)

   421       apply(erule_tac steps_in_range, auto simp: a_wf)

   422       done

   423   qed

   424   with a show thesis by blast

   425 qed

   426 

   427 lemma tm_comp_fetch_second_zero:

   428   "\<lbrakk>fetch B sa' x = (a, 0); tm_wf (A, 0); tm_wf (B, 0); sa' > 0\<rbrakk>

   429      \<Longrightarrow> fetch (A |+| B) (sa' + (length A div 2)) x = (a, 0)"

   430 apply(case_tac x)

   431 apply(case_tac [!] sa',

   432   auto simp: fetch.simps length_comp length_adjust nth_append tm_comp.simps

   433              tm_wf.simps shift.simps split: if_splits)

   434 done 

   435 

   436 lemma tm_comp_fetch_second_inst:

   437   "\<lbrakk>sa > 0; s > 0;  tm_wf (A, 0); tm_wf (B, 0); fetch B sa x = (a, s)\<rbrakk>

   438      \<Longrightarrow> fetch (A |+| B) (sa + length A div 2) x = (a, s + length A div 2)"

   439 apply(case_tac x)

   440 apply(case_tac [!] sa,

   441   auto simp: fetch.simps length_comp length_adjust nth_append tm_comp.simps

   442              tm_wf.simps shift.simps split: if_splits)

   443 done 

   444 

   445 lemma t_merge_second_same:

   446   assumes a_wf: "tm_wf (A, 0)"

   447   and b_wf: "tm_wf (B, 0)"

   448   and steps: "steps (Suc 0, l, r) (B, 0) stp = (s, l', r')"

   449   shows "steps (Suc (length A div 2), l, r)  (A |+| B, 0) stp

   450        = (if s = 0 then 0

   451           else s + length A div 2, l', r')"

   452 using a_wf b_wf steps

   453 proof(induct stp arbitrary: s l' r', simp add: steps.simps, simp)

   454   fix stpa sa l'a r'a

   455   assume ind: "\<And>s l' r'. steps (Suc 0, l, r) (B, 0) stpa = (s, l', r') \<Longrightarrow>

   456     steps (Suc (length A div 2), l, r) (A |+| B, 0) stpa = 

   457                 (if s = 0 then 0 else s + length A div 2, l', r')"

   458   and h: "step (steps (Suc 0, l, r) (B, 0) stpa) (B, 0) = (sa, l'a, r'a)"

   459   obtain sa' l'' r'' where a: "(steps (Suc 0, l, r) (B, 0) stpa) = (sa', l'', r'')"

   460     apply(case_tac "steps (Suc 0, l, r) (B, 0) stpa", auto)

   461     done

   462   from this have b: "steps (Suc (length A div 2), l, r) (A |+| B, 0) stpa = 

   463                 (if sa' = 0 then 0 else sa' + length A div 2, l'', r'')"

   464     apply(erule_tac ind)

   465     done

   466   from a b h show 

   467     "(sa = 0 \<longrightarrow> step (steps (Suc (length A div 2), l, r) (A |+| B, 0) stpa) (A |+| B, 0) = (0, l'a, r'a)) \<and>

   468     (0 < sa \<longrightarrow> step (steps (Suc (length A div 2), l, r) (A |+| B, 0) stpa) (A |+| B, 0) = (sa + length A div 2, l'a, r'a))"

   469   proof(case_tac "sa' = 0", auto)

   470     assume "step (sa', l'', r'') (B, 0) = (0, l'a, r'a)" "0 < sa'"

   471     thus "step (sa' + length A div 2, l'', r'') (A |+| B, 0) = (0, l'a, r'a)"

   472       using a_wf b_wf

   473       apply(simp add:  step.simps)

   474       apply(case_tac "fetch B sa' (read r'')", auto)

   475       apply(simp_all add: step.simps tm_comp_fetch_second_zero)

   476       done

   477   next

   478     assume "step (sa', l'', r'') (B, 0) = (sa, l'a, r'a)" "0 < sa'" "0 < sa"

   479     thus "step (sa' + length A div 2, l'', r'') (A |+| B, 0) = (sa + length A div 2, l'a, r'a)"

   480       using a_wf b_wf

   481       apply(simp add: step.simps)

   482       apply(case_tac "fetch B sa' (read r'')", auto)

   483       apply(simp_all add: step.simps tm_comp_fetch_second_inst)

   484       done

   485   qed

   486 qed

   487 

   488 lemma t_merge_second_halt_same:

   489   "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0); 

   490    steps (1, l, r) (B, 0) stp = (0, l', r')\<rbrakk>

   491      \<Longrightarrow> steps (Suc (length A div 2), l, r)  (A |+| B, 0) stp

   492        = (0, l', r')"

   493 using t_merge_second_same[where s = "0"]

   214 by (metis is_final.simps step_red steps.simps steps_0 surj_pair)

   495 done

   215 

   496 

   216 lemma t_merge_fetch_pre:

   497 lemma Hoare_plus_halt: 

   217   assumes "fetch A s b = (ac, ns)" "s \<le> length A div 2" "tm_wf A" "s \<noteq> 0" 

   218   shows "fetch (adjustA |+| B) s b = (ac, if ns = 0 then Suc (length A div 2) else ns)"

   219 using assms

   220 unfolding tm_comp_def

   221 apply(induct A)

   222 apply(auto)

   223 apply(subgoal_tac "2 * (s - Suc 0) < length A \<and> Suc (2 * (s - Suc 0)) < length A")

   224 apply(auto simp: tm_wf_def iseven_def tm_comp_def split: if_splits cell.splits)

   225 oops

   226 

   227 lemma t_merge_pre_eq_step: 

   228   "\<lbrakk>step (a, b, c) A = cf; tm_wf A; \<not> is_final cf\<rbrakk> 

   229         \<Longrightarrow> step (a, b, c) (A |+| B) = cf"

   230 apply(subgoal_tac "a \<le> length A div 2 \<and> a \<noteq> 0")

   231 apply(simp)

   232 apply(case_tac "fetch A a (read c)", simp)

   233 apply(auto)

   234 oops

   235 

   236 lemma t_merge_pre_eq:  

   237   "\<lbrakk>steps (Suc 0, tp) A stp = cf; \<not> is_final cf; tm_wf A\<rbrakk>

   238   \<Longrightarrow> steps (Suc 0, tp) (A |+| B) stp = cf"

   239 apply(induct stp arbitrary: cf)

   240 apply(auto)[1]

   241 apply(auto)

   242 oops

   243 

   244 lemma t_merge_pre_halt_same: 

   245   assumes a_ht: "steps (1, tp) A n = (0, tp')"

   246   and a_wf: "t_correct A"

   247   obtains n' where "steps (1, tp) (A |+| B) n' = (Suc (length A div 2), tp')"

   248 proof -

   249   assume a: "\<And>n. steps (1, tp) (A |+| B) n = (Suc (length A div 2), tp') \<Longrightarrow> thesis"

   250   

   251   obtain stp' where "\<not> is_final (steps (1, tp) A stp')" and "steps (1, tp) A (Suc stp') = (0, tp')"

   252   using a_ht before_final by blast

   253   then have "steps (1, tp) (A |+| B) (Suc stp') = (Suc (length A div 2), tp')"

   254     sorry (*using a_wf t_merge_pre_halt_same' by blast*)

   255   with a show thesis by blast

   256 qed

   257 

   258 

   259 

   260 lemma steps_comp:

   261   assumes a1: "steps (1, l, r) A n1 = (s1, l1, r1)"

   262   and a2: "steps (1, l1, r1) B n2 = (s2, l2, r2)"

   263   shows "steps (1, l, r) (A |+| B) (n1 + n2) = (s2, l2, r2)"

   264 using assms

   265 apply(induct n2)

   266 apply(simp)

   267 apply(simp add: tm_comp_def)

   268 oops

   269 

   270 lemma Hoare_plus: 

   272   and A_wf : "tm_wf A"

   499   and A_wf : "tm_wf (A, 0)"

   273   and B_wf : "tm_wf B"

   500   and B_wf : "tm_wf (B, 0)"

   274   and A_halt : "{P1} A {Q1}"

   501   and A_halt : "{P1} (A, 0) {Q1}"

   275   and B_halt : "{P2} B {Q2}"

   502   and B_halt : "{P2} (B, 0) {Q2}"

   276   shows "{P1} A |+| B {Q2}"

   503   shows "{P1} (A |+| B, 0) {Q2}"

   280   then obtain n1 where a: "is_final (steps (1, l, r) A n1)" and b: "Q1 holds_for (steps (1, l, r) A n1)"

   507   then obtain n1 where a: "is_final (steps (1, l, r) (A, 0) n1)" and b: "Q1 holds_for (steps (1, l, r) (A, 0) n1)"

   282   from b aimpb have "P2 holds_for (steps (1, l, r) A n1)"

   509   then obtain l' r' where "steps (1, l, r) (A, 0) n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')"

   283     by (rule holds_for_imp)

   510     by(case_tac "steps (1, l, r) (A, 0) n1", auto)

   284   then obtain l' r' where "P2 (l', r')"

   511   then obtain stpa where d: "steps (1, l, r) (A |+| B, 0) stpa = (Suc (length A div 2), l', r')"

   285     apply(auto)

   512     using A_wf

   286     apply(case_tac "steps (Suc 0, l, r) A n1")

   513     by(rule_tac t_merge_pre_halt_same, auto)

   287     apply(simp)

   514   from c aimpb have "P2 holds_for (0, l', r')"

   515     by(rule holds_for_imp)

   516   from this have "P2 (l', r')" by auto

   517   from this obtain n2 where e: "is_final (steps (1, l', r') (B, 0) n2)" and f: "Q2 holds_for (steps (1, l', r') (B, 0) n2)"

   518     using B_halt unfolding Hoare_def

   519     by auto

   520   then obtain l'' r'' where "steps (1, l', r') (B, 0) n2 = (0, l'', r'')" and g: "Q2 holds_for (0, l'', r'')"

   521     by(case_tac "steps (1, l', r') (B, 0) n2", auto)

   522   from this have "steps (Suc (length A div 2), l', r')  (A |+| B, 0) n2

   523     = (0, l'', r'')"

   524     apply(rule_tac t_merge_second_halt_same, auto simp: A_wf B_wf)

   289   then obtain n2 where a: "is_final (steps (1, l', r') B n2)" and b: "Q2 holds_for (steps (1, l', r') B n2)"

   526   thus "\<exists>n. is_final (steps (1, l, r) (A |+| B, 0) n) \<and> Q2 holds_for (steps (1, l, r) (A |+| B, 0) n)"

   290     using B_halt unfolding Hoare_def by auto

   527     using d g

   291   show "\<exists>n. is_final (steps (1, l, r) (A |+| B) n) \<and> Q2 holds_for (steps (1, l, r) (A |+| B) n)"

   528     apply(rule_tac x = "stpa + n2" in exI)

   292     apply(rule_tac x="n1 + n2" in exI)

   529     apply(simp add: steps_add)

   293     apply(rule conjI)

   294     apply(simp)

   295     apply(simp only: steps_add[symmetric])

   296     sorry

   297 qed

   298 

   299 

   300 

   301 

   302 

   303 locale turing_merge =

   304   fixes A :: "tprog" and B :: "tprog" and P1 :: "assert"

   305   and P2 :: "assert"

   306   and P3 :: "assert"

   307   and P4 :: "assert"

   308   and Q1:: "assert"

   309   and Q2 :: "assert"

   310   assumes 

   311   A_wf : "tm_wf A"

   312   and B_wf : "tm_wf B"

   313   and A_halt : "P1 tp \<Longrightarrow> \<exists> stp. let (s, tp') = steps (Suc 0, tp) A stp in s = 0 \<and> Q1 tp'"

   314   and B_halt : "P2 tp \<Longrightarrow> \<exists> stp. let (s, tp') = steps (Suc 0, tp) B stp in s = 0 \<and> Q2 tp'"

   315   and A_uhalt : "P3 tp \<Longrightarrow> \<not> (\<exists> stp. is_final (steps (Suc 0, tp) A stp))"

   316   and B_uhalt: "P4 tp \<Longrightarrow> \<not> (\<exists> stp. is_final (steps (Suc 0, tp) B stp))"

   317 begin

   318 

   319 

   320 text {*

   321   The following lemma tries to derive the Hoare logic rule for sequentially combined TMs.

   322   It deals with the situtation when both @{text "A"} and @{text "B"} are terminated.

   323 *}

   324 

   325 

   326 

   327 lemma  t_merge_uhalt_tmp:

   328   assumes B_uh: "\<forall>stp. \<not> is_final (steps (Suc 0, b, c) B stp)"

   329   and merge_ah: "steps (Suc 0, tp) (A |+| B) stpa = (Suc (length A div 2), b, c)" 

   330   shows "\<forall> stp. \<not> is_final (steps (Suc 0, tp) (A |+| B) stp)"

   331   using B_uh merge_ah

   332 apply(rule_tac allI)

   333 apply(case_tac "stp > stpa")

   334 apply(erule_tac x = "stp - stpa" in allE)

   335 apply(case_tac "(steps (Suc 0, b, c) B (stp - stpa))", simp)

   336 proof -

   337   fix stp a ba ca 

   338   assume h1: "\<not> is_final (a, ba, ca)" "stpa < stp"

   339   and h2: "steps (Suc 0, b, c) B (stp - stpa) = (a, ba, ca)"

   340   have "steps (Suc 0 + length A div 2, b, c) (A |+| B) (stp - stpa) = 

   341       (if a = 0 then 0 else a + length A div 2, ba, ca)"

   342     using A_wf B_wf h2

   343     by(rule_tac t_merge_snd_eq_steps, auto)

   344   moreover have "a > 0" using h1 by(simp add: is_final_def)

   345   moreover have "\<exists> stpb. stp = stpa + stpb" 

   346     using h1 by(rule_tac x = "stp - stpa" in exI, simp)

   347   ultimately show "\<not> is_final (steps (Suc 0, tp) (A |+| B) stp)"

   348     using merge_ah

   349     by(auto simp: steps_add is_final_def)

   350 next

   351   fix stp

   352   assume h: "steps (Suc 0, tp) (A |+| B) stpa = (Suc (length A div 2), b, c)" "\<not> stpa < stp"

   353   hence "\<exists> stpb. stpa = stp + stpb" apply(rule_tac x = "stpa - stp" in exI, auto) done

   354   thus "\<not> is_final (steps (Suc 0, tp) (A |+| B) stp)"

   355     using h

   356     apply(auto)

   357     apply(cases "steps (Suc 0, tp) (A |+| B) stp", simp add: steps_add is_final_def steps_0)

   361 text {*

   533 definition

   362   The following lemma deals with the situation when TM @{text "B"} can not terminate.

   534   Hoare_unhalt :: "assert \<Rightarrow> tprog \<Rightarrow> bool" ("({(1_)}/ (_))" 50)

   363   *}

   535 where

   364 

   536   "{P} p \<equiv> 

   365 lemma t_merge_uhalt: 

   537      (\<forall>l r. P (l, r) \<longrightarrow> (\<forall> n . \<not> (is_final (steps (1, (l, r)) p n))))"

   366   assumes aimpb: "Q1 \<mapsto> P4"

   538 

   367   shows "P1 \<mapsto> \<lambda> tp. \<not> (\<exists> stp. is_final (steps (Suc 0, tp) (A |+| B) stp))"

   539 lemma Hoare_unhalt_I:

   368 proof(simp only: assert_imp_def, rule_tac allI, rule_tac impI)

   540   assumes "\<And>l r. P (l, r) \<Longrightarrow> \<forall> n. \<not> is_final (steps (1, (l, r)) p n)"

   369   fix tp 

   541   shows "{P} p"

   370   assume init_asst: "P1 tp"

   542 unfolding Hoare_unhalt_def using assms by auto

   371   show "\<not> (\<exists>stp. is_final (steps (Suc 0, tp) (A |+| B) stp))"

   543 

   372   proof -

   544 lemma Hoare_plus_unhalt: 

   373     have "\<exists> stp. let (s, tp') = steps (Suc 0, tp) A stp in s = 0 \<and> Q1 tp'"

   545   assumes aimpb: "Q1 \<mapsto> P2"

   374       using A_halt[of tp] init_asst

   546   and A_wf : "tm_wf (A, 0)"

   375       by(simp)

   547   and B_wf : "tm_wf (B, 0)"

   376     from this obtain stpx where "let (s, tp') = steps (Suc 0, tp) A stpx in s = 0 \<and> Q1 tp'" ..

   548   and A_halt : "{P1} (A, 0) {Q1}"

   377     thus "?thesis"

   549   and B_uhalt : "{P2} (B, 0)"

   378     proof(cases "steps (Suc 0, tp) A stpx", simp, erule_tac conjE)

   550   shows "{P1} (A |+| B, 0)"

   379       fix a b c

   551 proof(rule_tac Hoare_unhalt_I)

   380       assume "Q1 (b, c)"

   552   fix l r

   381         and h3: "steps (Suc 0, tp) A stpx = (0, b, c)"

   553   assume h: "P1 (l, r)"

   382       hence h2: "P4 (b, c)"  using aimpb

   554   then obtain n1 where a: "is_final (steps (1, l, r) (A, 0) n1)" and b: "Q1 holds_for (steps (1, l, r) (A, 0) n1)"

   383         by(simp add: assert_imp_def)

   555     using A_halt unfolding Hoare_def by auto

   384       have "\<exists> stp. steps (Suc 0, tp) (A |+| B) stp = (Suc (length A div 2), b, c)"

   556   then obtain l' r' where "steps (1, l, r) (A, 0) n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')"

   385         using h3 A_wf B_wf

   557     by(case_tac "steps (1, l, r) (A, 0) n1", auto)

   386         apply(rule_tac stp = stpx in t_merge_pre_halt_same, auto)

   558   then obtain stpa where d: "steps (1, l, r) (A |+| B, 0) stpa = (Suc (length A div 2), l', r')"

   559     using A_wf

   560     by(rule_tac t_merge_pre_halt_same, auto)

   561   from c aimpb have "P2 holds_for (0, l', r')"

   562     by(rule holds_for_imp)

   563   from this have "P2 (l', r')" by auto

   564   from this have e: "\<forall> n. \<not> is_final (steps (Suc 0, l', r') (B, 0) n)  "

   565     using B_uhalt unfolding Hoare_unhalt_def

   566     by auto

   567   from e show "\<forall>n. \<not> is_final (steps (1, l, r) (A |+| B, 0) n)"

   568   proof(rule_tac allI, case_tac "n > stpa")

   569     fix n

   570     assume h2: "stpa < n"

   571     hence "\<not> is_final (steps (Suc 0, l', r') (B, 0) (n - stpa))"

   572       using e

   573       apply(erule_tac x = "n - stpa" in allE) by simp

   574     then obtain s'' l'' r'' where f: "steps (Suc 0, l', r') (B, 0) (n - stpa) = (s'', l'', r'')" and g: "s'' \<noteq> 0"

   575       apply(case_tac "steps (Suc 0, l', r') (B, 0) (n - stpa)", auto)

   576       done

   577     have k: "steps (Suc (length A div 2), l', r') (A |+| B, 0) (n - stpa) = (s''+ length A div 2, l'', r'') "

   578       using A_wf B_wf f g

   579       apply(drule_tac t_merge_second_same, auto)

   580       done

   581     show "\<not> is_final (steps (1, l, r) (A |+| B, 0) n)"

   582     proof -

   583       have "\<not> is_final (steps (1, l, r) (A |+| B, 0) (stpa + (n  - stpa)))"

   584         using d k A_wf

   585         apply(simp only: steps_add d, simp add: tm_wf.simps)

   388       from this obtain stpa where h4:"steps (Suc 0, tp) (A |+| B) stpa = (Suc (length A div 2), b, c)" ..

   587       thus "\<not> is_final (steps (1, l, r) (A |+| B, 0) n)"

   389       have " \<not> (\<exists> stp. is_final (steps (Suc 0, b, c) B stp))"

   588         using h2 by simp

   390         using B_uhalt [of "(b, c)"] h2 apply simp

   391         done

   392       from this and h4 show "\<forall>stp. \<not> is_final (steps (Suc 0, tp) (A |+| B) stp)"

   393         by(rule_tac t_merge_uhalt_tmp, auto)