--- a/thys/UTM.thy Thu Feb 21 05:33:57 2013 +0000
+++ b/thys/UTM.thy Thu Feb 21 05:34:39 2013 +0000
@@ -543,7 +543,7 @@
definition t_twice :: "instr list"
where
- "t_twice = adjust t_twice_compile"
+ "t_twice = adjust0 t_twice_compile"
definition t_fourtimes_compile :: "instr list"
where
@@ -551,7 +551,7 @@
definition t_fourtimes :: "instr list"
where
- "t_fourtimes = adjust t_fourtimes_compile"
+ "t_fourtimes = adjust0 t_fourtimes_compile"
definition t_twice_len :: "nat"
where
@@ -1266,7 +1266,7 @@
lemma adjust_fetch0:
"\<lbrakk>0 < a; a \<le> length ap div 2; fetch ap a b = (aa, 0)\<rbrakk>
- \<Longrightarrow> fetch (adjust ap) a b = (aa, Suc (length ap div 2))"
+ \<Longrightarrow> fetch (adjust0 ap) a b = (aa, Suc (length ap div 2))"
apply(case_tac b, auto simp: fetch.simps nth_of.simps nth_map
split: if_splits)
apply(case_tac [!] a, auto simp: fetch.simps nth_of.simps)
@@ -1274,7 +1274,7 @@
lemma adjust_fetch_norm:
"\<lbrakk>st > 0; st \<le> length tp div 2; fetch ap st b = (aa, ns); ns \<noteq> 0\<rbrakk>
- \<Longrightarrow> fetch (Turing.adjust ap) st b = (aa, ns)"
+ \<Longrightarrow> fetch (adjust0 ap) st b = (aa, ns)"
apply(case_tac b, auto simp: fetch.simps nth_of.simps nth_map
split: if_splits)
apply(case_tac [!] st, auto simp: fetch.simps nth_of.simps)
@@ -1286,7 +1286,7 @@
assumes exec: "step0 (st,l,r) ap = (st', l', r')"
and wf_tm: "tm_wf (ap, 0)"
and notfinal: "st' > 0"
- shows "step0 (st, l, r) (adjust ap) = (st', l', r')"
+ shows "step0 (st, l, r) (adjust0 ap) = (st', l', r')"
using assms
proof -
have "st > 0"
@@ -1300,7 +1300,7 @@
nth_of.simps adjust.simps tm_wf.simps split: if_splits)
apply(auto simp: mod_ex2)
done
- ultimately have "fetch (adjust ap) st (read r) = fetch ap st (read r)"
+ ultimately have "fetch (adjust0 ap) st (read r) = fetch ap st (read r)"
using assms
apply(case_tac "fetch ap st (read r)")
apply(drule_tac adjust_fetch_norm, simp_all)
@@ -1317,7 +1317,7 @@
assumes exec: "steps0 (st,l,r) ap stp = (st', l', r')"
and wf_tm: "tm_wf (ap, 0)"
and notfinal: "st' > 0"
- shows "steps0 (st, l, r) (adjust ap) stp = (st', l', r')"
+ shows "steps0 (st, l, r) (adjust0 ap) stp = (st', l', r')"
using exec notfinal
proof(induct stp arbitrary: st' l' r')
case 0
@@ -1326,7 +1326,7 @@
next
case (Suc stp st' l' r')
have ind: "\<And>st' l' r'. \<lbrakk>steps0 (st, l, r) ap stp = (st', l', r'); 0 < st'\<rbrakk>
- \<Longrightarrow> steps0 (st, l, r) (Turing.adjust ap) stp = (st', l', r')" by fact
+ \<Longrightarrow> steps0 (st, l, r) (adjust0 ap) stp = (st', l', r')" by fact
have h: "steps0 (st, l, r) ap (Suc stp) = (st', l', r')" by fact
have g: "0 < st'" by fact
obtain st'' l'' r'' where a: "steps0 (st, l, r) ap stp = (st'', l'', r'')"
@@ -1336,7 +1336,7 @@
apply(simp add: step_red)
apply(case_tac st'', auto)
done
- hence b: "steps0 (st, l, r) (Turing.adjust ap) stp = (st'', l'', r'')"
+ hence b: "steps0 (st, l, r) (adjust0 ap) stp = (st'', l'', r'')"
using a
by(rule_tac ind, simp_all)
thus "?case"
@@ -1349,7 +1349,7 @@
lemma adjust_halt_eq:
assumes exec: "steps0 (1, l, r) ap stp = (0, l', r')"
and tm_wf: "tm_wf (ap, 0)"
- shows "\<exists> stp. steps0 (Suc 0, l, r) (adjust ap) stp =
+ shows "\<exists> stp. steps0 (Suc 0, l, r) (adjust0 ap) stp =
(Suc (length ap div 2), l', r')"
proof -
have "\<exists> stp. \<not> is_final (steps0 (1, l, r) ap stp) \<and> (steps0 (1, l, r) ap (Suc stp) = (0, l', r'))"
@@ -1358,7 +1358,7 @@
then obtain stpa where a:
"\<not> is_final (steps0 (1, l, r) ap stpa) \<and> (steps0 (1, l, r) ap (Suc stpa) = (0, l', r'))" ..
obtain sa la ra where b:"steps0 (1, l, r) ap stpa = (sa, la, ra)" by (metis prod_cases3)
- hence c: "steps0 (Suc 0, l, r) (adjust ap) stpa = (sa, la, ra)"
+ hence c: "steps0 (Suc 0, l, r) (adjust0 ap) stpa = (sa, la, ra)"
using assms a
apply(rule_tac adjust_steps_eq, simp_all)
done
@@ -1371,7 +1371,7 @@
using b a
apply(simp add: step_red step.simps)
done
- have k: "fetch (adjust ap) sa (read ra) = (ac, Suc (length ap div 2))"
+ have k: "fetch (adjust0 ap) sa (read ra) = (ac, Suc (length ap div 2))"
using a b c d e f
apply(rule_tac adjust_fetch0, simp_all)
done
@@ -1402,14 +1402,14 @@
(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))" by blast
hence "\<exists> stp. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
- (adjust t_twice_compile) stp
+ (adjust0 t_twice_compile) stp
= (Suc (length t_twice_compile div 2), Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(rn))"
apply(rule_tac stp = stp in adjust_halt_eq)
apply(simp add: t_twice_compile_def, auto)
done
then obtain stpb where
"steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
- (adjust t_twice_compile) stpb
+ (adjust0 t_twice_compile) stpb
= (Suc (length t_twice_compile div 2), Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(rn))" ..
thus "?thesis"
apply(simp add: t_twice_def t_twice_len_def)
@@ -2079,14 +2079,14 @@
(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))" by blast
hence "\<exists> stp. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
- (adjust t_fourtimes_compile) stp
+ (adjust0 t_fourtimes_compile) stp
= (Suc (length t_fourtimes_compile div 2), Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (4 * rs)) @ Bk\<up>(rn))"
apply(rule_tac stp = stp in adjust_halt_eq)
apply(simp add: t_fourtimes_compile_def, auto)
done
then obtain stpb where
"steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
- (adjust t_fourtimes_compile) stpb
+ (adjust0 t_fourtimes_compile) stpb
= (Suc (length t_fourtimes_compile div 2), Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (4 * rs)) @ Bk\<up>(rn))" ..
thus "?thesis"
apply(simp add: t_fourtimes_def t_fourtimes_len_def)
@@ -3356,7 +3356,7 @@
lemma tm_wf_change_termi: "tm_wf (tp, 0) \<Longrightarrow>
- list_all (\<lambda>(acn, st). (st \<le> Suc (length tp div 2))) (adjust tp)"
+ list_all (\<lambda>(acn, st). (st \<le> Suc (length tp div 2))) (adjust0 tp)"
apply(auto simp: tm_wf.simps List.list_all_length)
apply(case_tac "tp!n", auto simp: adjust.simps split: if_splits)
apply(erule_tac x = "(a, b)" in ballE, auto)
@@ -3376,28 +3376,36 @@
apply(auto simp: mopup.simps)
done
-lemma [elim]: "(a, b) \<in> set (shift (Turing.adjust t_twice_compile) 12) \<Longrightarrow>
+lemma [elim]: "(a, b) \<in> set (shift (adjust0 t_twice_compile) 12) \<Longrightarrow>
b \<le> (28 + (length t_twice_compile + length t_fourtimes_compile)) div 2"
apply(simp add: t_twice_compile_def t_fourtimes_compile_def)
proof -
- assume g: "(a, b) \<in> set (shift (Turing.adjust (tm_of abc_twice @ shift (mopup (Suc 0)) (length (tm_of abc_twice) div 2))) 12)"
+ assume g: "(a, b)
+ \<in> set (shift
+ (adjust
+ (tm_of abc_twice @
+ shift (mopup (Suc 0)) (length (tm_of abc_twice) div 2))
+ (Suc ((length (tm_of abc_twice) + 16) div 2)))
+ 12)"
moreover have "length (tm_of abc_twice) mod 2 = 0" by auto
moreover have "length (tm_of abc_fourtimes) mod 2 = 0" by auto
ultimately have "list_all (\<lambda>(acn, st). (st \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2))
- (shift (Turing.adjust t_twice_compile) 12)"
- proof(auto simp: mod_ex1)
+ (shift (adjust0 t_twice_compile) 12)"
+ proof(auto simp add: mod_ex1 del: adjust.simps)
fix q qa
assume h: "length (tm_of abc_twice) = 2 * q" "length (tm_of abc_fourtimes) = 2 * qa"
- hence "list_all (\<lambda>(acn, st). st \<le> (18 + (q + qa)) + 12) (shift (Turing.adjust t_twice_compile) 12)"
+ hence "list_all (\<lambda>(acn, st). st \<le> (18 + (q + qa)) + 12) (shift (adjust0 t_twice_compile) 12)"
proof(rule_tac tm_wf_shift t_twice_compile_def)
- have "list_all (\<lambda>(acn, st). st \<le> Suc (length t_twice_compile div 2)) (adjust t_twice_compile)"
+ have "list_all (\<lambda>(acn, st). st \<le> Suc (length t_twice_compile div 2)) (adjust0 t_twice_compile)"
by(rule_tac tm_wf_change_termi, auto)
- thus "list_all (\<lambda>(acn, st). st \<le> 18 + (q + qa)) (Turing.adjust t_twice_compile)"
+ thus "list_all (\<lambda>(acn, st). st \<le> 18 + (q + qa)) (adjust0 t_twice_compile)"
using h
apply(simp add: t_twice_compile_def, auto simp: List.list_all_length)
done
qed
- thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa)) (shift (Turing.adjust t_twice_compile) 12)"
+ thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa))
+ (shift
+ (adjust t_twice_compile (Suc (length t_twice_compile div 2))) 12)"
by simp
qed
thus "b \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2"
@@ -3408,37 +3416,50 @@
done
qed
-lemma [elim]: "(a, b) \<in> set (shift (Turing.adjust t_fourtimes_compile) (t_twice_len + 13))
+lemma [elim]: "(a, b) \<in> set (shift (adjust0 t_fourtimes_compile) (t_twice_len + 13))
\<Longrightarrow> b \<le> (28 + (length t_twice_compile + length t_fourtimes_compile)) div 2"
apply(simp add: t_twice_compile_def t_fourtimes_compile_def t_twice_len_def)
proof -
- assume g: "(a, b) \<in> set (shift (Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0))
- (length (tm_of abc_fourtimes) div 2))) (length t_twice div 2 + 13))"
+ assume g: "(a, b)
+ \<in> set (shift
+ (adjust
+ (tm_of abc_fourtimes @
+ shift (mopup (Suc 0)) (length (tm_of abc_fourtimes) div 2))
+ (Suc ((length (tm_of abc_fourtimes) + 16) div 2)))
+ (length t_twice div 2 + 13))"
moreover have "length (tm_of abc_twice) mod 2 = 0" by auto
moreover have "length (tm_of abc_fourtimes) mod 2 = 0" by auto
ultimately have "list_all (\<lambda>(acn, st). (st \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2))
- (shift (Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0))
+ (shift (adjust0 (tm_of abc_fourtimes @ shift (mopup (Suc 0))
(length (tm_of abc_fourtimes) div 2))) (length t_twice div 2 + 13))"
proof(auto simp: mod_ex1 t_twice_def t_twice_compile_def)
fix q qa
assume h: "length (tm_of abc_twice) = 2 * q" "length (tm_of abc_fourtimes) = 2 * qa"
hence "list_all (\<lambda>(acn, st). st \<le> (9 + qa + (21 + q)))
- (shift (Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)) (21 + q))"
+ (shift (adjust0 (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)) (21 + q))"
proof(rule_tac tm_wf_shift t_twice_compile_def)
have "list_all (\<lambda>(acn, st). st \<le> Suc (length (tm_of abc_fourtimes @ shift
- (mopup (Suc 0)) qa) div 2)) (adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa))"
+ (mopup (Suc 0)) qa) div 2)) (adjust0 (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa))"
apply(rule_tac tm_wf_change_termi)
using wf_fourtimes h
apply(simp add: t_fourtimes_compile_def)
- done
- thus "list_all (\<lambda>(acn, st). st \<le> 9 + qa) ((Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)))"
+ done
+ thus "list_all (\<lambda>(acn, st). st \<le> 9 + qa)
+ (adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)
+ (Suc (length (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa) div
+ 2)))"
using h
apply(simp)
done
qed
- thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa)) (shift (Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)) (21 + q))"
+ thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa))
+ (shift
+ (adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)
+ (9 + qa))
+ (21 + q))"
apply(subgoal_tac "qa + q = q + qa")
- apply(simp, simp)
+ apply(simp add: h)
+ apply(simp)
done
qed
thus "b \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2"
@@ -3515,7 +3536,7 @@
apply(auto simp: Hoare_halt_def)
apply(rule_tac x = n in exI)
apply(case_tac "(steps0 (Suc 0, [], <m # args>)
- (Turing.adjust t_wcode_prepare @ shift t_wcode_main (length t_wcode_prepare div 2)) n)")
+ (adjust0 t_wcode_prepare @ shift t_wcode_main (length t_wcode_prepare div 2)) n)")
apply(auto simp: tm_comp.simps)
done
qed
@@ -4613,7 +4634,7 @@
*}
definition t_wcode :: "instr list"
where
- "t_wcode = (t_wcode_prepare |+| t_wcode_main) |+| t_wcode_adjust"
+ "t_wcode = (t_wcode_prepare |+| t_wcode_main) |+| t_wcode_adjust "
text {*