--- a/thys/UTM.thy Thu Mar 14 20:43:43 2013 +0000
+++ b/thys/UTM.thy Wed Mar 27 09:47:02 2013 +0000
@@ -1214,22 +1214,11 @@
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 =
@@ -1237,28 +1226,23 @@
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)
- (length (tm_of abc_twice) div 2)) stp = (0, Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (2*rs)) @ Bk\<up>(l))"
- proof(rule_tac recursive_compile_to_tm_correct)
+ 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 (rec_exec rec_twice [rs])) @ Bk\<up>(l))"
+ 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)"
- apply(simp add: rec_twice_def)
- apply(rule_tac rs = "[rs, 2]" in calc_cn, simp_all)
- apply(rule_tac allI, case_tac k, auto)
- done
+ show "terminate rec_twice [rs]"
+ apply(rule_tac primerec_terminate, auto)
+ apply(simp add: rec_twice_def, auto simp: constn.simps numeral_2_eq_2)
+ by(auto)
next
- show "length [rs] = 1" by simp
- 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)"
+ show "tm_of abc_twice = tm_of (a [+] dummy_abc (length [rs]))"
using h
- apply(simp add: abc_twice_def)
- done
+ by(simp add: abc_twice_def)
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
@@ -1386,8 +1370,7 @@
lemma [simp]: " tm_wf (t_twice_compile, 0)"
apply(simp only: t_twice_compile_def)
-apply(rule_tac t_compiled_correct)
-apply(simp_all add: abc_twice_def)
+apply(rule_tac wf_tm_from_abacus, simp)
done
lemma t_twice_change_term_state:
@@ -1503,7 +1486,7 @@
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 =
@@ -2018,15 +2001,13 @@
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"
-using prime_rel_exec_eq[of "constn 4" "[rs]" 4]
-apply(subgoal_tac "primerec (constn 4) 1", auto)
-done
-
-lemma [intro]: "rec_calc_rel rec_mult [rs, 4] (4 * rs)"
-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 [intro]: "primerec rec_fourtimes (Suc 0)"
+apply(auto simp: rec_fourtimes_def numeral_4_eq_4 constn.simps)
+by auto
+
+lemma fourtimes_lemma: "rec_exec rec_fourtimes [rs] = 4 * rs"
+by(simp add: rec_exec.simps rec_fourtimes_def)
+
lemma t_fourtimes_correct:
"\<exists>stp ln rn. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
@@ -2035,35 +2016,28 @@
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)
- (length (tm_of abc_fourtimes) div 2)) stp = (0, Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (4*rs)) @ Bk\<up>(l))"
- proof(rule_tac recursive_compile_to_tm_correct)
+ 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 (rec_exec rec_fourtimes [rs])) @ Bk\<up>(l))"
+ 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)"
- apply(simp add: rec_fourtimes_def)
- apply(rule_tac rs = "[rs, 4]" in calc_cn, simp_all)
- apply(rule_tac allI, case_tac k, auto simp: mult_lemma)
- done
+ show "terminate rec_fourtimes [rs]"
+ apply(rule_tac primerec_terminate)
+ by auto
next
- show "length [rs] = 1" by simp
- 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)"
+ show "tm_of abc_fourtimes = tm_of (a [+] dummy_abc (length [rs]))"
using h
- apply(simp add: abc_fourtimes_def)
- done
+ by(simp add: abc_fourtimes_def)
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(simp_all add: abc_twice_def)
+apply(rule_tac wf_tm_from_abacus, simp)
done
lemma t_fourtimes_change_term_state:
@@ -2175,7 +2149,7 @@
= (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
@@ -2228,7 +2202,7 @@
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))
@@ -2254,8 +2228,6 @@
done
qed
-(**********************************************************)
-
fun wcode_on_left_moving_3_B :: "bin_inv_t"
where
"wcode_on_left_moving_3_B ires rs (l, r) =
@@ -4742,7 +4714,7 @@
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)
@@ -4757,40 +4729,36 @@
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
- = (0, Bk\<up>m @ Bk # Bk # [], Oc\<up>Suc (rs - 1) @ Bk\<up>l)"
- proof(rule_tac recursive_compile_to_tm_correct)
+ (F_tprog @ shift (mopup (length [code tp, bl2wc (<lm>)])) (length F_tprog div 2)) stp
+ = (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_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)"
- using b by simp
- next
- show "length [code tp, bl2wc (<lm>)] = 2" by simp
+ show "terminate rec_F [code tp, bl2wc (<lm>)]"
+ using assms
+ by(rule_tac terminate_F, simp_all)
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)"
+ show "F_tprog = tm_of (ap [+] dummy_abc (length [code tp, bl2wc (<lm>)]))"
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
- = (0, Bk\<up>m @ Bk # Bk # [], Oc\<up>Suc (rs - 1) @ Bk\<up>l)" by blast
+ (F_tprog @ shift (mopup (length [code tp, (bl2wc (<lm>))])) (length F_tprog div 2)) stp
+ = (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 =
- (0, Bk \<up> m @ [Bk, Bk], Oc \<up> Suc (rs - 1) @ Bk \<up> l)"
+ (F_tprog @ shift (mopup (length [code tp, bl2wc (<lm>)])) (length F_tprog div 2)) stp =
+ (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
@@ -4800,7 +4768,8 @@
(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"
@@ -4819,7 +4788,7 @@
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:
@@ -4993,141 +4962,162 @@
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
- ([code tp, bl2wc (<lm>), y]) (Suc 0)"
+ \<Longrightarrow> \<forall>y. rec_exec rec_nonstop ([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);
- \<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <lm>) tp stp));
- rec_ci rec_F = (F_ap, rs_pos, a_md)\<rbrakk>
- \<Longrightarrow> \<forall> stp. case abc_steps_l (0, [code tp, bl2wc (<lm>)] @ 0\<up>(a_md - rs_pos )
- @ suflm) (F_ap) stp of (ss, e) \<Rightarrow> ss < length (F_ap)"
-apply(case_tac "rec_ci (Cn (Suc (Suc 0)) rec_right [Cn (Suc (Suc 0)) rec_conf
- ([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt])])")
-apply(simp only: rec_F_def, rule_tac i = 0 and ga = a and gb = b and
- gc = c in cn_gi_uhalt, simp, simp, simp, simp, simp, simp, simp)
-apply(simp add: ci_cn_para_eq)
-apply(case_tac "rec_ci (Cn (Suc (Suc 0)) rec_conf
- ([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt]))")
-apply(rule_tac rf = "(Cn (Suc (Suc 0)) rec_right [Cn (Suc (Suc 0)) rec_conf
- ([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt])])"
- and n = "Suc (Suc 0)" and f = rec_right and
- gs = "[Cn (Suc (Suc 0)) rec_conf
- ([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt])]"
- and i = 0 and ga = aa and gb = ba and gc = ca in
- cn_gi_uhalt)
-apply(simp, simp, simp, simp, simp, simp, simp,
- simp add: ci_cn_para_eq)
-apply(case_tac "rec_ci rec_halt")
-apply(rule_tac rf = "(Cn (Suc (Suc 0)) rec_conf
- ([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt]))"
- and n = "Suc (Suc 0)" and f = "rec_conf" and
- gs = "([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt])" and
- i = "Suc (Suc 0)" and gi = "rec_halt" and ga = ab and gb = bb and
- gc = cb in cn_gi_uhalt)
-apply(simp, simp, simp, simp, simp add: nth_append, simp,
- simp add: nth_append, simp add: rec_halt_def)
-apply(simp only: rec_halt_def)
-apply(case_tac [!] "rec_ci ((rec_nonstop))")
-apply(rule_tac allI, rule_tac impI, simp)
-apply(case_tac j, simp)
-apply(rule_tac x = "code tp" in exI, rule_tac calc_id, simp, simp, simp, simp)
-apply(rule_tac x = "bl2wc (<lm>)" in exI, rule_tac calc_id, simp, simp, simp)
-apply(rule_tac rf = "Mn (Suc (Suc 0)) (rec_nonstop)"
- and f = "(rec_nonstop)" and n = "Suc (Suc 0)"
- and aprog' = ac and rs_pos' = bc and a_md' = cc in Mn_unhalt)
-apply(simp, simp add: rec_halt_def , simp, simp)
-apply(drule_tac nonstop_true, simp_all)
-apply(rule_tac allI)
-apply(erule_tac x = y in allE)+
-apply(simp)
-done
+ assumes wf_tm: "tm_wf (tp,0)"
+ and unhalt: "\<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <lm>) tp stp))"
+ and compile: "rec_ci rec_F = (F_ap, rs_pos, a_md)"
+ shows "{\<lambda> nl. nl = [code tp, bl2wc (<lm>)] @ 0\<up>(a_md - rs_pos ) @ suflm} (F_ap) \<up>"
+ using compile
+proof(simp only: rec_F_def)
+ assume h: "rec_ci (Cn (Suc (Suc 0)) rec_valu [Cn (Suc (Suc 0)) rec_right [Cn (Suc (Suc 0))
+ rec_conf [recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), rec_halt]]]) =
+ (F_ap, rs_pos, a_md)"
+ moreover hence "rs_pos = Suc (Suc 0)"
+ using cn_arity
+ by simp
+ moreover obtain ap1 ar1 ft1 where a: "rec_ci
+ (Cn (Suc (Suc 0)) rec_right
+ [Cn (Suc (Suc 0)) rec_conf [recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), rec_halt]]) = (ap1, ar1, ft1)"
+ by(case_tac "rec_ci (Cn (Suc (Suc 0)) rec_right [Cn (Suc (Suc 0))
+ rec_conf [recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), rec_halt]])", auto)
+ moreover hence b: "ar1 = Suc (Suc 0)"
+ using cn_arity by simp
+ ultimately show "?thesis"
+ proof(rule_tac i = 0 in cn_unhalt_case, auto)
+ fix anything
+ obtain ap2 ar2 ft2 where c:
+ "rec_ci (Cn (Suc (Suc 0)) rec_conf [recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), rec_halt])
+ = (ap2, ar2, ft2)"
+ by(case_tac "rec_ci (Cn (Suc (Suc 0)) rec_conf
+ [recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), rec_halt])", auto)
+ moreover hence d:"ar2 = Suc (Suc 0)"
+ using cn_arity by simp
+ ultimately have "{\<lambda>nl. nl = [code tp, bl2wc (<lm>)] @ 0 \<up> (ft1 - Suc (Suc 0)) @ anything} ap1 \<up>"
+ using a b c d
+ proof(rule_tac i = 0 in cn_unhalt_case, auto)
+ fix anything
+ obtain ap3 ar3 ft3 where e: "rec_ci rec_halt = (ap3, ar3, ft3)"
+ by(case_tac "rec_ci rec_halt", auto)
+ hence f: "ar3 = Suc (Suc 0)"
+ using mn_arity
+ by(simp add: rec_halt_def)
+ have "{\<lambda>nl. nl = [code tp, bl2wc (<lm>)] @ 0 \<up> (ft2 - Suc (Suc 0)) @ anything} ap2 \<up>"
+ using c d e f
+ proof(rule_tac i = 2 in cn_unhalt_case, auto simp: rec_halt_def)
+ fix anything
+ have "{\<lambda>nl. nl = [code tp, bl2wc (<lm>)] @ 0 \<up> (ft3 - Suc (Suc 0)) @ anything} ap3 \<up>"
+ using e f
+ 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)
- \<Rightarrow> ss < length ap"
+ \<Longrightarrow> {\<lambda> nl. nl = [code tp, bl2wc (<lm>)]} ap \<up>"
proof(frule_tac F_ap = ap and rs_pos = pos and a_md = md
- and suflm = "[]" in F_aprog_uhalt, auto)
- fix stp a b
+ and suflm = "[]" in F_aprog_uhalt, auto simp: abc_Hoare_unhalt_def,
+ 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
- (ss, e) \<Rightarrow> ss < length ap"
- "abc_steps_l (0, [code tp, bl2wc (<lm>)]) ap stp = (a, b)"
+ "\<forall>n. abc_notfinal (abc_steps_l (0, code tp # bl2wc (<lm>) # 0 \<up> (md - pos)) ap n) ap"
+ "abc_steps_l (0, [code tp, bl2wc (<lm>)]) ap n = (a, b)"
"tm_wf (tp, 0)"
"rec_ci rec_F = (ap, pos, md)"
- moreover have "ap \<noteq> []"
- using h apply(rule_tac rec_ci_not_null, simp)
- done
+ moreover have a: "ap \<noteq> []"
+ using h rec_ci_not_null[of "rec_F" pos md] by auto
ultimately show "a < length ap"
- proof(erule_tac x = stp in allE,
- case_tac "abc_steps_l (0, code tp # bl2wc (<lm>) # 0\<up>(md - pos)) ap stp", simp)
- fix aa ba
- assume g: "aa < length ap"
- "abc_steps_l (0, code tp # bl2wc (<lm>) # 0\<up>(md - pos)) ap stp = (aa, ba)"
- "ap \<noteq> []"
+ proof(erule_tac x = n in allE)
+ assume g: "abc_notfinal (abc_steps_l (0, code tp # bl2wc (<lm>) # 0 \<up> (md - pos)) ap n) ap"
+ obtain ss nl where b : "abc_steps_l (0, code tp # bl2wc (<lm>) # 0 \<up> (md - pos)) ap n = (ss, nl)"
+ by (metis prod.exhaust)
+ then have c: "ss < length ap"
+ 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
- apply(simp)
- done
+ "md - pos" ap n ss nl] h
+ 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))\<rbrakk>
- \<Longrightarrow> \<forall> stp. case abc_steps_l (0, [code tp, bl2wc (<lm>)]) F_aprog
- stp of (ss, e) \<Rightarrow> ss < length F_aprog"
+ \<Longrightarrow> {\<lambda> nl. nl = [code tp, bl2wc (<lm>)]} F_aprog \<up> "
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 -
- fix a b c
- 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
+apply(rule_tac abc_Hoare_plus_unhalt1, simp)
+done
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)
- show "layout_of F_aprog = layout_of F_aprog" by simp
-next
+proof(rule_tac compile_correct_unhalt, auto)
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
-next
- show "\<forall>stp. case abc_steps_l (0, [code tp, bl2wc (<lm>)]) F_aprog stp of (as, am) \<Rightarrow> as < length F_aprog"
+ fix stp a b
+ show "abc_steps_l (0, [code tp, bl2wc (<lm>)]) F_aprog stp = (a, b) \<Longrightarrow> a < length F_aprog"
using assms
- apply(erule_tac uabc_uhalt, simp)
- done
+ apply(drule_tac uabc_uhalt, auto simp: abc_Hoare_unhalt_def)
+ 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
@@ -5166,7 +5156,7 @@
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
@@ -5330,4 +5320,5 @@
using assms(2-3)
apply(simp add: tape_of_nat_abv)
done
+
end
\ No newline at end of file