tm: comparison thys/UTM.thy

equal deleted inserted replaced

-:e9ef4ada308b
+:d8e6f0798e23
 lemma t_twice_len_ge: "Suc 0 \<le> length t_twice div 2"
 apply(simp add: t_twice_def mopup.simps t_twice_compile_def)
 done
-lemma [intro]: "rec_calc_rel (recf.id (Suc 0) 0) [rs] rs"
-apply(rule_tac calc_id, simp_all)
-done
-lemma [intro]: "rec_calc_rel (constn 2) [rs] 2"
-using prime_rel_exec_eq[of "constn 2" "[rs]" 2]
-apply(subgoal_tac "primerec (constn 2) 1", auto)
-done
-lemma  [intro]: "rec_calc_rel rec_mult [rs, 2] (2 * rs)"
-using prime_rel_exec_eq[of "rec_mult" "[rs, 2]"  "2*rs"]
-apply(subgoal_tac "primerec rec_mult (Suc (Suc 0))", auto)
-done
 declare start_of.simps[simp del]
+lemma twice_lemma: "rec_exec rec_twice [rs] = 2*rs"
+by(auto simp: rec_twice_def rec_exec.simps)
 lemma t_twice_correct:
 "\<exists>stp ln rn. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
 (tm_of abc_twice @ shift (mopup (Suc 0)) ((length (tm_of abc_twice) div 2))) stp =
 (0, Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(rn))"
 proof(case_tac "rec_ci rec_twice")
 fix a b c
 assume h: "rec_ci rec_twice = (a, b, c)"
-have "\<exists>stp m l. steps0 (Suc 0, Bk # Bk # ires, <[rs]> @ Bk\<up>(n)) (tm_of abc_twice @ shift (mopup 1)
+have "\<exists>stp m l. steps0 (Suc 0, Bk # Bk # ires, <[rs]> @ Bk\<up>(n)) (tm_of abc_twice @ shift (mopup (length [rs]))
-(length (tm_of abc_twice) div 2)) stp = (0, Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (2*rs)) @ Bk\<up>(l))"
+(length (tm_of abc_twice) div 2)) stp = (0, Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (rec_exec rec_twice [rs])) @ Bk\<up>(l))"
-proof(rule_tac recursive_compile_to_tm_correct)
+thm  recursive_compile_to_tm_correct1
+proof(rule_tac recursive_compile_to_tm_correct1)
 show "rec_ci rec_twice = (a, b, c)" by (simp add: h)
 next
-show "rec_calc_rel rec_twice [rs] (2 * rs)"
+show "terminate rec_twice [rs]"
-apply(simp add: rec_twice_def)
+apply(rule_tac primerec_terminate, auto)
-apply(rule_tac rs =  "[rs, 2]" in calc_cn, simp_all)
+apply(simp add: rec_twice_def, auto simp: constn.simps numeral_2_eq_2)
-apply(rule_tac allI, case_tac k, auto)
+by(auto)
-done
 next
-show "length [rs] = 1" by simp
+show "tm_of abc_twice = tm_of (a [+] dummy_abc (length [rs]))"
-next
-show "layout_of (a [+] dummy_abc 1) = layout_of (a [+] dummy_abc 1)" by simp
-next
-show "tm_of abc_twice = tm_of (a [+] dummy_abc 1)"
 using h
-apply(simp add: abc_twice_def)
+by(simp add: abc_twice_def)
-done
 qed
 thus "?thesis"
-apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
+apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv rec_exec.simps twice_lemma)
 done
 qed
 declare adjust.simps[simp]
 declare tm_wf.simps[simp del]
 lemma [simp]: " tm_wf (t_twice_compile, 0)"
 apply(simp only: t_twice_compile_def)
-apply(rule_tac t_compiled_correct)
+apply(rule_tac wf_tm_from_abacus, simp)
-apply(simp_all add: abc_twice_def)
 done
 lemma t_twice_change_term_state:
 "\<exists> stp ln rn. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n)) t_twice stp
 = (Suc t_twice_len, Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(rn))"
 apply(erule_tac exE)
 apply(simp add: wcode_main_first_part_len)
 apply(rule_tac x = stp in exI, rule_tac x = "ln + lna" in exI,
 rule_tac x = rn in exI)
 apply(simp add: t_wcode_main_def)
-apply(simp add: replicate_Suc[THEN sym] exp_add[THEN sym] del: replicate_Suc)
+apply(simp add: replicate_Suc[THEN sym] replicate_add [THEN sym] del: replicate_Suc)
 done
 from this obtain stpb lnb rnb where stp2:
 "steps0 (13, Bk # Bk # Bk\<up>(lna) @ Oc # ires, Oc\<up>(Suc (Suc rs)) @ Bk\<up>(rna)) t_wcode_main stpb =
 (13 + t_twice_len, Bk # Bk # Bk\<up>(lnb) @ Oc # ires, Oc\<up>(Suc (Suc (Suc (2 *rs)))) @ Bk\<up>(rnb))" by blast
 have "\<exists>stp ln rn. steps0 (13 + t_twice_len, Bk # Bk # Bk\<up>(lnb) @ Oc # ires,
 lemma t_fourtimes_len_gr:  "t_fourtimes_len > 0"
 apply(simp add: t_fourtimes_len_def t_fourtimes_def mopup.simps t_fourtimes_compile_def)
 done
-lemma [intro]: "rec_calc_rel (constn 4) [rs] 4"
+lemma [intro]: "primerec rec_fourtimes (Suc 0)"
-using prime_rel_exec_eq[of "constn 4" "[rs]" 4]
+apply(auto simp: rec_fourtimes_def numeral_4_eq_4 constn.simps)
-apply(subgoal_tac "primerec (constn 4) 1", auto)
+by auto
-done
+lemma fourtimes_lemma: "rec_exec rec_fourtimes [rs] = 4 * rs"
-lemma [intro]: "rec_calc_rel rec_mult [rs, 4] (4 * rs)"
+by(simp add: rec_exec.simps rec_fourtimes_def)
-using prime_rel_exec_eq[of "rec_mult" "[rs, 4]"  "4*rs"]
-apply(subgoal_tac "primerec rec_mult 2", auto simp: numeral_2_eq_2)
-done
 lemma t_fourtimes_correct:
 "\<exists>stp ln rn. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
 (tm_of abc_fourtimes @ shift (mopup 1) (length (tm_of abc_fourtimes) div 2)) stp =
 (0, Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (4 * rs)) @ Bk\<up>(rn))"
 proof(case_tac "rec_ci rec_fourtimes")
 fix a b c
 assume h: "rec_ci rec_fourtimes = (a, b, c)"
-have "\<exists>stp m l. steps0 (Suc 0, Bk # Bk # ires, <[rs]> @ Bk\<up>(n)) (tm_of abc_fourtimes @ shift (mopup 1)
+have "\<exists>stp m l. steps0 (Suc 0, Bk # Bk # ires, <[rs]> @ Bk\<up>(n)) (tm_of abc_fourtimes @ shift (mopup (length [rs]))
-(length (tm_of abc_fourtimes) div 2)) stp = (0, Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (4*rs)) @ Bk\<up>(l))"
+(length (tm_of abc_fourtimes) div 2)) stp = (0, Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (rec_exec rec_fourtimes [rs])) @ Bk\<up>(l))"
-proof(rule_tac recursive_compile_to_tm_correct)
+thm recursive_compile_to_tm_correct1
+proof(rule_tac recursive_compile_to_tm_correct1)
 show "rec_ci rec_fourtimes = (a, b, c)" by (simp add: h)
 next
-show "rec_calc_rel rec_fourtimes [rs] (4 * rs)"
+show "terminate rec_fourtimes [rs]"
-apply(simp add: rec_fourtimes_def)
+apply(rule_tac primerec_terminate)
-apply(rule_tac rs =  "[rs, 4]" in calc_cn, simp_all)
+by auto
-apply(rule_tac allI, case_tac k, auto simp: mult_lemma)
-done
 next
-show "length [rs] = 1" by simp
+show "tm_of abc_fourtimes = tm_of (a [+] dummy_abc (length [rs]))"
-next
-show "layout_of (a [+] dummy_abc 1) = layout_of (a [+] dummy_abc 1)" by simp
-next
-show "tm_of abc_fourtimes = tm_of (a [+] dummy_abc 1)"
 using h
-apply(simp add: abc_fourtimes_def)
+by(simp add: abc_fourtimes_def)
-done
 qed
 thus "?thesis"
-apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
+apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv fourtimes_lemma)
 done
 qed
 lemma wf_fourtimes[intro]: "tm_wf (t_fourtimes_compile, 0)"
 apply(simp only: t_fourtimes_compile_def)
-apply(rule_tac t_compiled_correct)
+apply(rule_tac wf_tm_from_abacus, simp)
-apply(simp_all add: abc_twice_def)
 done
 lemma t_fourtimes_change_term_state:
 "\<exists> stp ln rn. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n)) t_fourtimes stp
 = (Suc t_fourtimes_len, Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (4 * rs)) @ Bk\<up>(rn))"
 lemma [simp]: "fetch t_wcode_main (14 + length t_twice div 2 + t_fourtimes_len) Oc
 = (L, Suc 0)"
 apply(subgoal_tac "14 = Suc 13")
 apply(simp only: fetch.simps add_Suc nth_of.simps t_wcode_main_def)
-apply(simp add:length_append length_shift Parity.two_times_even_div_two even_twice_len t_fourtimes_len_def)
+apply(simp add:length_append length_shift Parity.two_times_even_div_two even_twice_len t_fourtimes_len_def nth_append)
 by arith
 lemma [simp]: "fetch t_wcode_main (14 + length t_twice div 2 + t_fourtimes_len) Bk
 = (L, Suc 0)"
 apply(subgoal_tac "14 = Suc 13")
 apply(erule_tac exE)
 apply(simp add: t_wcode_main_def)
 apply(rule_tac x = stp in exI,
 rule_tac x = "ln + lna" in exI,
 rule_tac x = rn in exI, simp)
-apply(simp add: replicate_Suc[THEN sym] exp_add[THEN sym] del: replicate_Suc)
+apply(simp add: replicate_Suc[THEN sym] replicate_add[THEN sym] del: replicate_Suc)
 done
 from this obtain stpb lnb rnb where stp2:
 "steps0 (t_twice_len + 14, Bk # Bk # Bk\<up>(lna) @ Oc # ires, Oc\<up>(Suc (rs + 1)) @ Bk\<up>(rna))
 t_wcode_main stpb =
 (t_twice_len + 14 + t_fourtimes_len, Bk # Bk # Bk\<up>(lnb) @ Oc # ires,  Oc\<up>(Suc (4*rs + 4)) @ Bk\<up>(rnb))"
 apply(rule_tac x = "stpa + stpb + stpc" in exI,
 rule_tac x = lnc in exI, rule_tac x = rnc in exI)
 apply(simp add: steps_add)
 done
 qed
-(**********************************************************)
 fun wcode_on_left_moving_3_B :: "bin_inv_t"
 where
 "wcode_on_left_moving_3_B ires rs (l, r) =
 (\<exists> ml mr rn. l = Bk\<up>(ml) @ Oc # Bk # Bk # ires \<and>
 apply(simp add: exp_ind del: replicate_Suc)
 apply(case_tac nat, simp add: exp_ind)
 apply(rule_tac x = "Suc m" in exI, simp only: exp_ind)
 apply(simp only: exp_ind, simp)
 apply(subgoal_tac "m = length la + nata")
-apply(rule_tac x = "m - nata" in exI, simp add: exp_add)
+apply(rule_tac x = "m - nata" in exI, simp add: replicate_add)
 apply(drule_tac length_equal, simp)
 apply(simp only: exp_ind[THEN sym] replicate_Suc[THEN sym] replicate_add[THEN sym])
 apply(rule_tac x = "m + Suc (Suc n)" in exI, simp)
 done
 shows "\<exists>stp m n. steps0 (Suc 0, [Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>(i)) t_utm stp =
 (0, Bk\<up>(m), Oc\<up>(rs) @ Bk\<up>(n))"
 proof -
 obtain ap arity fp where a: "rec_ci rec_F = (ap, arity, fp)"
 by (metis prod_cases3)
-moreover have b: "rec_calc_rel  rec_F [code tp, (bl2wc (<lm>))] (rs - Suc 0)"
+moreover have b: "rec_exec rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)"
 using assms
 apply(rule_tac F_correct, simp_all)
 done
 have "\<exists> stp m l. steps0 (Suc 0, Bk # Bk # [], <[code tp, bl2wc (<lm>)]> @ Bk\<up>i)
-(F_tprog @ shift (mopup 2) (length F_tprog div 2)) stp
+(F_tprog @ shift (mopup (length [code tp, bl2wc (<lm>)])) (length F_tprog div 2)) stp
-= (0, Bk\<up>m @ Bk # Bk # [], Oc\<up>Suc (rs - 1) @ Bk\<up>l)"
+= (0, Bk\<up>m @ Bk # Bk # [], Oc\<up>Suc (rec_exec rec_F [code tp, (bl2wc (<lm>))]) @ Bk\<up>l)"
-proof(rule_tac recursive_compile_to_tm_correct)
+proof(rule_tac recursive_compile_to_tm_correct1)
 show "rec_ci rec_F = (ap, arity, fp)" using a by simp
 next
-show "rec_calc_rel rec_F [code tp, bl2wc (<lm>)] (rs - 1)"
+show "terminate rec_F [code tp, bl2wc (<lm>)]"
-using b by simp
+using assms
+by(rule_tac terminate_F, simp_all)
 next
-show "length [code tp, bl2wc (<lm>)] = 2" by simp
+show "F_tprog = tm_of (ap [+] dummy_abc (length [code tp, bl2wc (<lm>)]))"
-next
-show "layout_of (ap [+] dummy_abc 2) = layout_of (ap [+] dummy_abc 2)"
-by simp
-next
-show "F_tprog = tm_of (ap [+] dummy_abc 2)"
 using a
 apply(simp add: F_tprog_def F_aprog_def numeral_2_eq_2)
 done
 qed
 then obtain stp m l where
 "steps0 (Suc 0, Bk # Bk # [], <[code tp, bl2wc (<lm>)]> @ Bk\<up>i)
-(F_tprog @ shift (mopup 2) (length F_tprog div 2)) stp
+(F_tprog @ shift (mopup (length [code tp, (bl2wc (<lm>))])) (length F_tprog div 2)) stp
-= (0, Bk\<up>m @ Bk # Bk # [], Oc\<up>Suc (rs - 1) @ Bk\<up>l)" by blast
+= (0, Bk\<up>m @ Bk # Bk # [], Oc\<up>Suc (rec_exec rec_F [code tp, (bl2wc (<lm>))]) @ Bk\<up>l)" by blast
 hence "\<exists> m. steps0 (Suc 0, [Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>i)
 (F_tprog @ shift (mopup 2) (length F_tprog div 2)) stp
 = (0, Bk\<up>m, Oc\<up>Suc (rs - 1) @ Bk\<up>l)"
 proof -
 assume g: "steps0 (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]> @ Bk \<up> i)
-(F_tprog @ shift (mopup 2) (length F_tprog div 2)) stp =
+(F_tprog @ shift (mopup (length [code tp, bl2wc (<lm>)])) (length F_tprog div 2)) stp =
-(0, Bk \<up> m @ [Bk, Bk], Oc \<up> Suc (rs - 1) @ Bk \<up> l)"
+(0, Bk \<up> m @ [Bk, Bk], Oc \<up> Suc ((rec_exec rec_F [code tp, bl2wc (<lm>)])) @ Bk \<up> l)"
 moreover have "tinres [Bk, Bk] [Bk]"
 apply(auto simp: tinres_def)
 done
 moreover obtain sa la ra where "steps0 (Suc 0, [Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>i)
 (F_tprog @ shift (mopup 2) (length F_tprog div 2)) stp = (sa, la, ra)"
 apply(case_tac "steps0 (Suc 0, [Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>i)
 (F_tprog @ shift (mopup 2) (length F_tprog div 2)) stp", auto)
 done
 ultimately show "?thesis"
-apply(drule_tac tinres_steps1, auto)
+using b
+apply(drule_tac la = "Bk\<up>m @ [Bk, Bk]" in tinres_steps1, auto simp: numeral_2_eq_2)
 done
 qed
 thus "?thesis"
 apply(auto)
 apply(rule_tac x = stp in exI, simp add: t_utm_def)
 apply(rule_tac tm_wf_comp, auto)
 done
 lemma [intro]: "tm_wf (t_utm, 0)"
 apply(simp only: t_utm_def F_tprog_def)
-apply(rule_tac t_compiled_correct, auto)
+apply(rule_tac wf_tm_from_abacus, auto)
 done
 lemma UTM_halt_lemma_pre:
 assumes wf_tm: "tm_wf (tp, 0)"
 and result: "0 < rs"
 done
 lemma nonstop_true:
 "\<lbrakk>tm_wf (tp, 0);
 \<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <lm>) tp stp))\<rbrakk>
-\<Longrightarrow> \<forall>y. rec_calc_rel rec_nonstop
+\<Longrightarrow> \<forall>y. rec_exec rec_nonstop ([code tp, bl2wc (<lm>), y]) =  (Suc 0)"
-([code tp, bl2wc (<lm>), y]) (Suc 0)"
 apply(rule_tac allI, erule_tac x = y in allE)
 apply(case_tac "steps0 (Suc 0, Bk\<up>(l), <lm>) tp y", simp)
 apply(rule_tac nonstop_t_uhalt_eq, simp_all)
 done
-declare ci_cn_para_eq[simp]
+lemma cn_arity:  "rec_ci (Cn n f gs) = (a, b, c) \<Longrightarrow> b = n"
+by(case_tac "rec_ci f", simp add: rec_ci.simps)
+lemma mn_arity: "rec_ci (Mn n f) = (a, b, c) \<Longrightarrow> b = n"
+by(case_tac "rec_ci f", simp add: rec_ci.simps)
 lemma F_aprog_uhalt:
-"\<lbrakk>tm_wf (tp,0);
+assumes wf_tm: "tm_wf (tp,0)"
-\<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <lm>) tp stp));
+and unhalt:  "\<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <lm>) tp stp))"
-rec_ci rec_F = (F_ap, rs_pos, a_md)\<rbrakk>
+and compile: "rec_ci rec_F = (F_ap, rs_pos, a_md)"
-\<Longrightarrow> \<forall> stp. case abc_steps_l (0, [code tp, bl2wc (<lm>)] @ 0\<up>(a_md - rs_pos )
+shows "{\<lambda> nl. nl = [code tp, bl2wc (<lm>)] @ 0\<up>(a_md - rs_pos ) @ suflm} (F_ap) \<up>"
-@ suflm) (F_ap) stp of (ss, e) \<Rightarrow> ss < length (F_ap)"
+using compile
-apply(case_tac "rec_ci (Cn (Suc (Suc 0)) rec_right [Cn (Suc (Suc 0)) rec_conf
+proof(simp only: rec_F_def)
-([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt])])")
+assume h: "rec_ci (Cn (Suc (Suc 0)) rec_valu [Cn (Suc (Suc 0)) rec_right [Cn (Suc (Suc 0))
-apply(simp only: rec_F_def, rule_tac i = 0  and ga = a and gb = b and
+rec_conf [recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), rec_halt]]]) =
-gc = c in cn_gi_uhalt, simp, simp, simp, simp, simp, simp, simp)
+(F_ap, rs_pos, a_md)"
-apply(simp add: ci_cn_para_eq)
+moreover hence "rs_pos = Suc (Suc 0)"
-apply(case_tac "rec_ci (Cn (Suc (Suc 0)) rec_conf
+using cn_arity
-([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt]))")
+by simp
-apply(rule_tac rf = "(Cn (Suc (Suc 0)) rec_right [Cn (Suc (Suc 0)) rec_conf
+moreover obtain ap1 ar1 ft1 where a: "rec_ci
-([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt])])"
+(Cn (Suc (Suc 0)) rec_right
-and n = "Suc (Suc 0)" and f = rec_right and
+[Cn (Suc (Suc 0)) rec_conf [recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), rec_halt]]) = (ap1, ar1, ft1)"
-gs = "[Cn (Suc (Suc 0)) rec_conf
+by(case_tac "rec_ci (Cn (Suc (Suc 0)) rec_right [Cn (Suc (Suc 0))
-([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt])]"
+rec_conf [recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), rec_halt]])", auto)
-and i = 0 and ga = aa and gb = ba and gc = ca in
+moreover hence b: "ar1 = Suc (Suc 0)"
-cn_gi_uhalt)
+using cn_arity by simp
-apply(simp, simp, simp, simp, simp, simp, simp,
+ultimately show "?thesis"
-simp add: ci_cn_para_eq)
+proof(rule_tac i = 0 in cn_unhalt_case, auto)
-apply(case_tac "rec_ci rec_halt")
+fix anything
-apply(rule_tac rf = "(Cn (Suc (Suc 0)) rec_conf
+obtain ap2 ar2 ft2 where c:
-([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt]))"
+"rec_ci (Cn (Suc (Suc 0)) rec_conf [recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), rec_halt])
-and n = "Suc (Suc 0)" and f = "rec_conf" and
+= (ap2, ar2, ft2)"
-gs = "([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt])"  and
+by(case_tac "rec_ci (Cn (Suc (Suc 0)) rec_conf
-i = "Suc (Suc 0)" and gi = "rec_halt" and ga = ab and gb = bb and
+[recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), rec_halt])", auto)
-gc = cb in cn_gi_uhalt)
+moreover hence d:"ar2 = Suc (Suc 0)"
-apply(simp, simp, simp, simp, simp add: nth_append, simp,
+using cn_arity by simp
-simp add: nth_append, simp add: rec_halt_def)
+ultimately have "{\<lambda>nl. nl = [code tp, bl2wc (<lm>)] @ 0 \<up> (ft1 - Suc (Suc 0)) @ anything} ap1 \<up>"
-apply(simp only: rec_halt_def)
+using a b c d
-apply(case_tac [!] "rec_ci ((rec_nonstop))")
+proof(rule_tac i = 0 in cn_unhalt_case, auto)
-apply(rule_tac allI, rule_tac impI, simp)
+fix anything
-apply(case_tac j, simp)
+obtain ap3 ar3 ft3 where e: "rec_ci rec_halt = (ap3, ar3, ft3)"
-apply(rule_tac x = "code tp" in exI, rule_tac calc_id, simp, simp, simp, simp)
+by(case_tac "rec_ci rec_halt", auto)
-apply(rule_tac x = "bl2wc (<lm>)" in exI, rule_tac calc_id, simp, simp, simp)
+hence f: "ar3 = Suc (Suc 0)"
-apply(rule_tac rf = "Mn (Suc (Suc 0)) (rec_nonstop)"
+using mn_arity
-and f = "(rec_nonstop)" and n = "Suc (Suc 0)"
+by(simp add: rec_halt_def)
-and  aprog' = ac and rs_pos' =  bc and a_md' = cc in Mn_unhalt)
+have "{\<lambda>nl. nl = [code tp, bl2wc (<lm>)] @ 0 \<up> (ft2 - Suc (Suc 0)) @ anything} ap2 \<up>"
-apply(simp, simp add: rec_halt_def , simp, simp)
+using c d e f
-apply(drule_tac  nonstop_true, simp_all)
+proof(rule_tac i = 2 in cn_unhalt_case, auto simp: rec_halt_def)
-apply(rule_tac allI)
+fix anything
-apply(erule_tac x = y in allE)+
+have "{\<lambda>nl. nl = [code tp, bl2wc (<lm>)] @ 0 \<up> (ft3 - Suc (Suc 0)) @ anything} ap3 \<up>"
-apply(simp)
+using e f
-done
+proof(rule_tac mn_unhalt_case, auto simp: rec_halt_def)
+fix i
+show "terminate rec_nonstop [code tp, bl2wc (<lm>), i]"
+by(rule_tac primerec_terminate, auto)
+next
+fix i
+show "0 < rec_exec rec_nonstop [code tp, bl2wc (<lm>), i]"
+using assms
+by(drule_tac nonstop_true, auto)
+qed
+thus "{\<lambda>nl. nl = code tp # bl2wc (<lm>) # 0 \<up> (ft3 - Suc (Suc 0)) @ anything} ap3 \<up>" by simp
+next
+fix apj arj ftj j  anything
+assume "j<2" "rec_ci ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) = (apj, arj, ftj)"
+hence "{\<lambda>nl. nl = [code tp, bl2wc (<lm>)] @ 0 \<up> (ftj - arj) @ anything} apj
+{\<lambda>nl. nl = [code tp, bl2wc (<lm>)] @
+rec_exec ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) [code tp, bl2wc (<lm>)] #
+0 \<up> (ftj - Suc arj) @ anything}"
+apply(rule_tac recursive_compile_correct)
+apply(case_tac j, auto)
+apply(rule_tac [!] primerec_terminate)
+by(auto)
+thus "{\<lambda>nl. nl = code tp # bl2wc (<lm>) # 0 \<up> (ftj - arj) @ anything} apj
+{\<lambda>nl. nl = code tp # bl2wc (<lm>) # rec_exec ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0))
+(Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) [code tp, bl2wc (<lm>)] # 0 \<up> (ftj - Suc arj) @ anything}"
+by simp
+next
+fix j
+assume "(j::nat) < 2"
+thus "terminate ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j)
+[code tp, bl2wc (<lm>)]"
+by(case_tac j, auto intro!: primerec_terminate)
+qed
+thus "{\<lambda>nl. nl = code tp # bl2wc (<lm>) # 0 \<up> (ft2 - Suc (Suc 0)) @ anything} ap2 \<up>"
+by simp
+qed
+thus "{\<lambda>nl. nl = code tp # bl2wc (<lm>) # 0 \<up> (ft1 - Suc (Suc 0)) @ anything} ap1 \<up>" by simp
+qed
+qed
 lemma uabc_uhalt':
 "\<lbrakk>tm_wf (tp, 0);
 \<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <lm>) tp stp));
 rec_ci rec_F = (ap, pos, md)\<rbrakk>
-\<Longrightarrow> \<forall> stp. case abc_steps_l (0, [code tp, bl2wc (<lm>)]) ap stp of (ss, e)
+\<Longrightarrow> {\<lambda> nl. nl = [code tp, bl2wc (<lm>)]} ap \<up>"
-\<Rightarrow>  ss < length ap"
 proof(frule_tac F_ap = ap and rs_pos = pos and a_md = md
-and suflm = "[]" in F_aprog_uhalt, auto)
+and suflm = "[]" in F_aprog_uhalt, auto simp: abc_Hoare_unhalt_def,
-fix stp a b
+case_tac "abc_steps_l (0, [code tp, bl2wc (<lm>)]) ap n", simp)
+fix n a b
 assume h:
-"\<forall>stp. case abc_steps_l (0, code tp # bl2wc (<lm>) # 0\<up>(md - pos)) ap stp of
+"\<forall>n. abc_notfinal (abc_steps_l (0, code tp # bl2wc (<lm>) # 0 \<up> (md - pos)) ap n) ap"
-(ss, e) \<Rightarrow> ss < length ap"
+"abc_steps_l (0, [code tp, bl2wc (<lm>)]) ap n = (a, b)"
-"abc_steps_l (0, [code tp, bl2wc (<lm>)]) ap stp = (a, b)"
 "tm_wf (tp, 0)"
 "rec_ci rec_F = (ap, pos, md)"
-moreover have "ap \<noteq> []"
+moreover have a: "ap \<noteq> []"
-using h apply(rule_tac rec_ci_not_null, simp)
+using h rec_ci_not_null[of "rec_F" pos md] by auto
-done
 ultimately show "a < length ap"
-proof(erule_tac x = stp in allE,
+proof(erule_tac x = n in allE)
-case_tac "abc_steps_l (0, code tp # bl2wc (<lm>) # 0\<up>(md - pos)) ap stp", simp)
+assume g: "abc_notfinal (abc_steps_l (0, code tp # bl2wc (<lm>) # 0 \<up> (md - pos)) ap n) ap"
-fix aa ba
+obtain ss nl where b : "abc_steps_l (0, code tp # bl2wc (<lm>) # 0 \<up> (md - pos)) ap n = (ss, nl)"
-assume g: "aa < length ap"
+by (metis prod.exhaust)
-"abc_steps_l (0, code tp # bl2wc (<lm>) # 0\<up>(md - pos)) ap stp = (aa, ba)"
+then have c: "ss < length ap"
-"ap \<noteq> []"
+using g by simp
 thus "?thesis"
+using a b c
 using abc_list_crsp_steps[of "[code tp, bl2wc (<lm>)]"
-"md - pos" ap stp aa ba] h
+"md - pos" ap n ss nl] h
-apply(simp)
+by(simp)
-done
 qed
 qed
 lemma uabc_uhalt:
 "\<lbrakk>tm_wf (tp, 0);
 \<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <lm>) tp stp))\<rbrakk>
-\<Longrightarrow> \<forall> stp. case abc_steps_l (0, [code tp, bl2wc (<lm>)]) F_aprog
+\<Longrightarrow> {\<lambda> nl. nl = [code tp, bl2wc (<lm>)]} F_aprog \<up> "
-stp of (ss, e) \<Rightarrow> ss < length F_aprog"
 apply(case_tac "rec_ci rec_F", simp add: F_aprog_def)
 apply(drule_tac ap = a and pos = b and md = c in uabc_uhalt', simp_all)
-proof -
+apply(rule_tac abc_Hoare_plus_unhalt1, simp)
-fix a b c
+done
-assume
-"\<forall>stp. case abc_steps_l (0, [code tp, bl2wc (<lm>)]) a stp of (ss, e)
-\<Rightarrow> ss < length a"
-"rec_ci rec_F = (a, b, c)"
-thus
-"\<forall>stp. case abc_steps_l (0, [code tp, bl2wc (<lm>)])
-(a [+] dummy_abc (Suc (Suc 0))) stp of (ss, e) \<Rightarrow>
-ss < Suc (Suc (Suc (length a)))"
-using abc_append_uhalt1[of a "[code tp, bl2wc (<lm>)]"
-"a [+] dummy_abc (Suc (Suc 0))" "[]" "dummy_abc (Suc (Suc 0))"]
-apply(simp)
-done
-qed
 lemma tutm_uhalt':
 assumes tm_wf:  "tm_wf (tp,0)"
 and unhalt: "\<forall> stp. (\<not> TSTD (steps0 (1, Bk\<up>(l), <lm>) tp stp))"
 shows "\<forall> stp. \<not> is_final (steps0 (1, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stp)"
 unfolding t_utm_def
-proof(rule_tac compile_correct_unhalt)
+proof(rule_tac compile_correct_unhalt, auto)
-show "layout_of F_aprog = layout_of F_aprog" by simp
-next
 show "F_tprog = tm_of F_aprog"
 by(simp add:  F_tprog_def)
 next
-show "crsp (layout_of F_aprog) (0, [code tp, bl2wc (<lm>)]) (1, [Bk, Bk], <[code tp, bl2wc (<lm>)]>)  []"
+show "crsp (layout_of F_aprog) (0, [code tp, bl2wc (<lm>)]) (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>)  []"
 by(auto simp: crsp.simps start_of.simps)
 next
-show "length F_tprog div 2 = length F_tprog div 2" by simp
+fix stp a b
-next
+show "abc_steps_l (0, [code tp, bl2wc (<lm>)]) F_aprog stp = (a, b) \<Longrightarrow> a < length F_aprog"
-show "\<forall>stp. case abc_steps_l (0, [code tp, bl2wc (<lm>)]) F_aprog stp of (as, am) \<Rightarrow> as < length F_aprog"
 using assms
-apply(erule_tac uabc_uhalt, simp)
+apply(drule_tac uabc_uhalt, auto simp: abc_Hoare_unhalt_def)
-done
+by(erule_tac x = stp in allE, erule_tac x = stp in allE, simp)
 qed
 lemma tinres_commute: "tinres r r' \<Longrightarrow> tinres r' r"
 apply(auto simp: tinres_def)
 done
 lemma inres_tape:
 apply(drule_tac inres_tape, auto)
 apply(auto simp: tinres_def)
 apply(case_tac "m > Suc (Suc 0)")
 apply(rule_tac x = "m - Suc (Suc 0)" in exI)
 apply(case_tac m, simp_all add: , case_tac nat, simp_all add: replicate_Suc)
-apply(rule_tac x = "2 - m" in exI, simp add: exp_add[THEN sym])
+apply(rule_tac x = "2 - m" in exI, simp add: replicate_add[THEN sym])
 apply(simp only: numeral_2_eq_2, simp add: replicate_Suc)
 done
 lemma tutm_uhalt:
 "\<lbrakk>tm_wf (tp,0);
 shows "{(\<lambda>tp. tp = ([], <code p # args>))} UTM \<up>"
 using UTM_unhalt_lemma[OF assms(1), where i="0"]
 using assms(2-3)
 apply(simp add: tape_of_nat_abv)
 done
 end

changeset 229	d8e6f0798e23
parent 190	f1ecb4a68a54
child 240	696081f445c2