--- a/thys/UTM.thy Thu Feb 07 06:39:06 2013 +0000
+++ b/thys/UTM.thy Sun Feb 10 19:49:07 2013 +0000
@@ -1,5 +1,5 @@
theory UTM
-imports Main recursive abacus UF GCD turing_hoare
+imports Recursive Abacus UF GCD Turing_Hoare
begin
section {* Wang coding of input arguments *}
@@ -1247,7 +1247,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_basic.adjust ap) st b = (aa, ns)"
+ \<Longrightarrow> fetch (Turing.adjust 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)
@@ -1299,7 +1299,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_basic.adjust ap) stp = (st', l', r')" by fact
+ \<Longrightarrow> steps0 (st, l, r) (Turing.adjust 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'')"
@@ -1309,7 +1309,7 @@
apply(simp add: step_red)
apply(case_tac st'', auto)
done
- hence b: "steps0 (st, l, r) (turing_basic.adjust ap) stp = (st'', l'', r'')"
+ hence b: "steps0 (st, l, r) (Turing.adjust ap) stp = (st'', l'', r'')"
using a
by(rule_tac ind, simp_all)
thus "?case"
@@ -3373,28 +3373,28 @@
apply(auto simp: mopup.simps)
done
-lemma [elim]: "(a, b) \<in> set (shift (turing_basic.adjust t_twice_compile) 12) \<Longrightarrow>
+lemma [elim]: "(a, b) \<in> set (shift (Turing.adjust 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_basic.adjust (tm_of abc_twice @ shift (mopup (Suc 0)) (length (tm_of abc_twice) div 2))) 12)"
+ 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)"
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_basic.adjust t_twice_compile) 12)"
+ (shift (Turing.adjust t_twice_compile) 12)"
proof(auto simp: mod_ex1)
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_basic.adjust t_twice_compile) 12)"
+ hence "list_all (\<lambda>(acn, st). st \<le> (18 + (q + qa)) + 12) (shift (Turing.adjust 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)"
by(rule_tac tm_wf_change_termi, auto)
- thus "list_all (\<lambda>(acn, st). st \<le> 18 + (q + qa)) (turing_basic.adjust t_twice_compile)"
+ thus "list_all (\<lambda>(acn, st). st \<le> 18 + (q + qa)) (Turing.adjust 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_basic.adjust t_twice_compile) 12)"
+ thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa)) (shift (Turing.adjust t_twice_compile) 12)"
by simp
qed
thus "b \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2"
@@ -3405,22 +3405,22 @@
done
qed
-lemma [elim]: "(a, b) \<in> set (shift (turing_basic.adjust t_fourtimes_compile) (t_twice_len + 13))
+lemma [elim]: "(a, b) \<in> set (shift (Turing.adjust 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_basic.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0))
+ 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))"
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_basic.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0))
+ (shift (Turing.adjust (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_basic.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)) (21 + q))"
+ (shift (Turing.adjust (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))"
@@ -3428,12 +3428,12 @@
using wf_fourtimes h
apply(simp add: t_fourtimes_compile_def)
done
- thus "list_all (\<lambda>(acn, st). st \<le> 9 + qa) ((turing_basic.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)))"
+ thus "list_all (\<lambda>(acn, st). st \<le> 9 + qa) ((Turing.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)))"
using h
apply(simp)
done
qed
- thus "list_all (\<lambda>(acn, st). st \<le> 30 + (q + qa)) (shift (turing_basic.adjust (tm_of abc_fourtimes @ shift (mopup (Suc 0)) qa)) (21 + q))"
+ 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))"
apply(subgoal_tac "qa + q = q + qa")
apply(simp, simp)
done
@@ -3512,7 +3512,7 @@
apply(auto simp: Hoare_halt_def)
apply(rule_tac x = n in exI)
apply(case_tac "(steps0 (Suc 0, [], <m # args>)
- (turing_basic.adjust t_wcode_prepare @ shift t_wcode_main (length t_wcode_prepare div 2)) n)")
+ (Turing.adjust t_wcode_prepare @ shift t_wcode_main (length t_wcode_prepare div 2)) n)")
apply(auto simp: tm_comp.simps)
done
qed
@@ -3919,12 +3919,12 @@
where "wadjust_le \<equiv> (inv_image lex_square wadjust_measure)"
lemma [intro]: "wf lex_square"
-by(auto intro:wf_lex_prod simp: abacus.lex_pair_def lex_square_def
- abacus.lex_triple_def)
+by(auto intro:wf_lex_prod simp: Abacus.lex_pair_def lex_square_def
+ Abacus.lex_triple_def)
lemma wf_wadjust_le[intro]: "wf wadjust_le"
by(auto intro:wf_inv_image simp: wadjust_le_def
- abacus.lex_triple_def abacus.lex_pair_def)
+ Abacus.lex_triple_def Abacus.lex_pair_def)
lemma [simp]: "wadjust_start m rs (c, []) = False"
apply(auto simp: wadjust_start.simps)
@@ -4518,7 +4518,7 @@
apply(simp_all only: wadjust_inv.simps split: if_splits)
apply(simp_all)
apply(simp_all add: wadjust_inv.simps wadjust_le_def
- abacus.lex_triple_def abacus.lex_pair_def lex_square_def split: if_splits)
+ Abacus.lex_triple_def Abacus.lex_pair_def lex_square_def split: if_splits)
done
next
show "?Q (?f 0)"
@@ -4667,7 +4667,7 @@
(*
lemma F_abc_halt_eq:
- "\<lbrakk>turing_basic.t_correct tp;
+ "\<lbrakk>Turing.t_correct tp;
length lm = k;
steps (Suc 0, Bk\<up>(l), <lm>) tp stp = (0, Bk\<up>(m), Oc\<up>(rs)@Bk\<up>(n));
rs > 0\<rbrakk>
@@ -4701,7 +4701,7 @@
declare tape_of_nl_abv_cons[simp del]
lemma t_utm_halt_eq':
- "\<lbrakk>turing_basic.t_correct tp;
+ "\<lbrakk>Turing.t_correct tp;
0 < rs;
steps (Suc 0, Bk\<up>(l), <lm::nat list>) tp stp = (0, Bk\<up>(m), Oc\<up>(rs)@Bk\<up>(n))\<rbrakk>
\<Longrightarrow> \<exists>stp m n. steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stp =
@@ -4729,7 +4729,7 @@
*)
(*
lemma t_utm_halt_eq'':
- "\<lbrakk>turing_basic.t_correct tp;
+ "\<lbrakk>Turing.t_correct tp;
0 < rs;
steps (Suc 0, Bk\<up>(l), <lm::nat list>) tp stp = (0, Bk\<up>(m), Oc\<up>(rs)@Bk\<up>(n))\<rbrakk>
\<Longrightarrow> \<exists>stp m n. steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>(i)) t_utm stp =