tm: comparison thys/UTM.thy

equal deleted inserted replaced

-:a63c3f8d7234
+:67063c5365e1
 theory UTM
-imports Main recursive abacus UF GCD turing_hoare
+imports Recursive Abacus UF GCD Turing_Hoare
 begin
 section {* Wang coding of input arguments *}
 text {*
 apply(case_tac [!] a, auto simp: fetch.simps nth_of.simps)
 done
 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)
 done
 thus "?case"
 by(simp add: steps.simps)
 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'')"
 by (metis prod_cases3)
 hence c:"0 < st''"
 using h g
 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"
 using assms a b h g
 apply(simp add: step_red)
 lemma [simp]: "length (mopup (Suc 0)) = 16"
 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"
 using g
 apply(auto simp:t_twice_compile_def)
 apply(simp add: Ball_set[THEN sym])
 apply(erule_tac x = "(a, b)" in ballE, simp, simp)
 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))"
 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_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
 qed
 thus "b \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2"
 qed
 thus "?thesis"
 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
 definition tinres :: "cell list \<Rightarrow> cell list \<Rightarrow> bool"
 definition wadjust_le :: "((nat \<times> config) \<times> nat \<times> config) set"
 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
+by(auto intro:wf_lex_prod simp: Abacus.lex_pair_def lex_square_def
-abacus.lex_triple_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)
 done
 apply(simp add: step.simps)
 apply(case_tac d, case_tac [2] aa, simp_all)
 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)"
 apply(simp add: steps.simps wadjust_inv.simps wadjust_start.simps, auto)
 done
 where
 "UTM_pre = t_wcode |+| t_utm"
 (*
 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>
 \<Longrightarrow> \<exists> stp m. abc_steps_l (0, [code tp, bl2wc (<lm>)]) (F_aprog) stp =
 (length (F_aprog), code tp # bl2wc (<lm>) # (rs - 1) # 0\<up>(m))"
 done
 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 =
 (0, Bk\<up>(m), Oc\<up>(rs) @ Bk\<up>(n))"
 apply(drule_tac  l = l in F_abc_halt_eq, simp, simp, simp)
 apply(rule_tac x = "n - na" in exI, simp)
 done
 *)
 (*
 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 =
 (0, Bk\<up>(m), Oc\<up>(rs) @ Bk\<up>(n))"
 apply(drule_tac t_utm_halt_eq', simp_all)

changeset 163	67063c5365e1
parent 145	38d8e0e37b7d
child 166	99a180fd4194