--- a/thys/UTM.thy Wed Apr 24 09:49:00 2013 +0100
+++ b/thys/UTM.thy Thu Apr 25 21:37:05 2013 +0100
@@ -1216,8 +1216,8 @@
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 twice_lemma: "rec_eval rec_twice [rs] = 2*rs"
+by(auto simp: rec_twice_def rec_eval.simps)
lemma t_twice_correct:
"\<exists>stp ln rn. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
@@ -1227,13 +1227,13 @@
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 (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))"
+ (length (tm_of abc_twice) div 2)) stp = (0, Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (rec_eval 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 "terminate rec_twice [rs]"
- apply(rule_tac primerec_terminate, auto)
+ show "terminates rec_twice [rs]"
+ apply(rule_tac primerec_terminates, auto)
apply(simp add: rec_twice_def, auto simp: constn.simps numeral_2_eq_2)
by(auto)
next
@@ -1242,7 +1242,7 @@
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 rec_exec.simps twice_lemma)
+ apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv rec_eval.simps twice_lemma)
done
qed
@@ -2005,8 +2005,8 @@
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 fourtimes_lemma: "rec_eval rec_fourtimes [rs] = 4 * rs"
+by(simp add: rec_eval.simps rec_fourtimes_def)
lemma t_fourtimes_correct:
@@ -2017,13 +2017,13 @@
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 (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))"
+ (length (tm_of abc_fourtimes) div 2)) stp = (0, Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (rec_eval 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 "terminate rec_fourtimes [rs]"
- apply(rule_tac primerec_terminate)
+ show "terminates rec_fourtimes [rs]"
+ apply(rule_tac primerec_terminates)
by auto
next
show "tm_of abc_fourtimes = tm_of (a [+] dummy_abc (length [rs]))"
@@ -4729,19 +4729,19 @@
proof -
obtain ap arity fp where a: "rec_ci rec_F = (ap, arity, fp)"
by (metis prod_cases3)
- moreover have b: "rec_exec rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)"
+ moreover have b: "rec_eval 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 (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)"
+ = (0, Bk\<up>m @ Bk # Bk # [], Oc\<up>Suc (rec_eval 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 "terminate rec_F [code tp, bl2wc (<lm>)]"
+ show "terminates rec_F [code tp, bl2wc (<lm>)]"
using assms
- by(rule_tac terminate_F, simp_all)
+ by(rule_tac terminates_F, simp_all)
next
show "F_tprog = tm_of (ap [+] dummy_abc (length [code tp, bl2wc (<lm>)]))"
using a
@@ -4751,14 +4751,14 @@
then obtain stp m l where
"steps0 (Suc 0, Bk # Bk # [], <[code tp, bl2wc (<lm>)]> @ Bk\<up>i)
(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
+ = (0, Bk\<up>m @ Bk # Bk # [], Oc\<up>Suc (rec_eval 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 (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)"
+ (0, Bk \<up> m @ [Bk, Bk], Oc \<up> Suc ((rec_eval rec_F [code tp, bl2wc (<lm>)])) @ Bk \<up> l)"
moreover have "tinres [Bk, Bk] [Bk]"
apply(auto simp: tinres_def)
done
@@ -4936,7 +4936,7 @@
done
lemma NSTD_1: "\<not> TSTD (a, b, c)
- \<Longrightarrow> rec_exec rec_NSTD [trpl_code (a, b, c)] = Suc 0"
+ \<Longrightarrow> rec_eval rec_NSTD [trpl_code (a, b, c)] = Suc 0"
using NSTD_lemma1[of "trpl_code (a, b, c)"]
NSTD_lemma2[of "trpl_code (a, b, c)"]
apply(simp add: TSTD_def)
@@ -4949,10 +4949,10 @@
"\<lbrakk>tm_wf (tp, 0);
steps0 (Suc 0, Bk\<up>(l), <lm>) tp stp = (a, b, c);
\<not> TSTD (a, b, c)\<rbrakk>
- \<Longrightarrow> rec_exec rec_nonstop [code tp, bl2wc (<lm>), stp] = Suc 0"
-apply(simp add: rec_nonstop_def rec_exec.simps)
+ \<Longrightarrow> rec_eval rec_nonstop [code tp, bl2wc (<lm>), stp] = Suc 0"
+apply(simp add: rec_nonstop_def rec_eval.simps)
apply(subgoal_tac
- "rec_exec rec_conf [code tp, bl2wc (<lm>), stp] =
+ "rec_eval rec_conf [code tp, bl2wc (<lm>), stp] =
trpl_code (a, b, c)", simp)
apply(erule_tac NSTD_1)
using rec_t_eq_steps[of tp l lm stp]
@@ -4962,7 +4962,7 @@
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_exec rec_nonstop ([code tp, bl2wc (<lm>), y]) = (Suc 0)"
+ \<Longrightarrow> \<forall>y. rec_eval 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)
@@ -5021,11 +5021,11 @@
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)
+ show "terminates rec_nonstop [code tp, bl2wc (<lm>), i]"
+ by(rule_tac primerec_terminates, auto)
next
fix i
- show "0 < rec_exec rec_nonstop [code tp, bl2wc (<lm>), i]"
+ show "0 < rec_eval rec_nonstop [code tp, bl2wc (<lm>), i]"
using assms
by(drule_tac nonstop_true, auto)
qed
@@ -5035,22 +5035,22 @@
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>)] #
+ rec_eval ([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)
+ apply(rule_tac [!] primerec_terminates)
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))
+ {\<lambda>nl. nl = code tp # bl2wc (<lm>) # rec_eval ([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)
+ thus "terminates ([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)
+ by(case_tac j, auto intro!: primerec_terminates)
qed
thus "{\<lambda>nl. nl = code tp # bl2wc (<lm>) # 0 \<up> (ft2 - Suc (Suc 0)) @ anything} ap2 \<up>"
by simp