Mercurial Mercurial > hg > tm / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
UTM.thy
changeset 35 839e37b75d9a
parent 0 aa8656a8dbef 
--- a/UTM.thy	Sat Jan 12 01:05:01 2013 +0000
+++ b/UTM.thy	Sat Jan 12 01:33:20 2013 +0000
@@ -1148,12 +1148,12 @@
 qed
     
 lemma [elim]: "t_ncorrect tp
-    \<Longrightarrow> t_ncorrect (abacus.tshift tp a)"
+    \<Longrightarrow> t_ncorrect (tshift tp a)"
 apply(simp add: t_ncorrect.simps shift_length)
 done
 
 lemma tshift_fetch: "\<lbrakk> fetch tp a b = (aa, st'); 0 < st'\<rbrakk>
-       \<Longrightarrow> fetch (abacus.tshift tp (length tp1 div 2)) a b 
+       \<Longrightarrow> fetch (tshift tp (length tp1 div 2)) a b 
           = (aa, st' + length tp1 div 2)"
 apply(subgoal_tac "a > 0")
 apply(auto simp: fetch.simps nth_of.simps shift_length nth_map
@@ -1176,22 +1176,22 @@
   assume ind: "\<And>st' l' r'.
     \<lbrakk>a = st' \<and> b = l' \<and> c = r'; 0 < st'\<rbrakk>
     \<Longrightarrow> t_steps (st + length tp1 div 2, l, r) 
-    (abacus.tshift tp (length tp1 div 2), length tp1 div 2) stp = 
+    (tshift tp (length tp1 div 2), length tp1 div 2) stp = 
      (st' + length tp1 div 2, l', r')"
   and h: "tstep (a, b, c) tp = (st', l', r')" "0 < st'" "t_ncorrect tp1"  "t_ncorrect tp"
-  have k: "t_steps (st + length tp1 div 2, l, r) (abacus.tshift tp (length tp1 div 2),
+  have k: "t_steps (st + length tp1 div 2, l, r) (tshift tp (length tp1 div 2),
          length tp1 div 2) stp = (a + length tp1 div 2, b, c)"
     apply(rule_tac ind, simp)
     using h
     apply(case_tac a, simp_all add: tstep.simps fetch.simps)
     done
-  from h and this show "t_step (t_steps (st + length tp1 div 2, l, r) (abacus.tshift tp (length tp1 div 2), length tp1 div 2) stp)
-           (abacus.tshift tp (length tp1 div 2), length tp1 div 2) =
+  from h and this show "t_step (t_steps (st + length tp1 div 2, l, r) (tshift tp (length tp1 div 2), length tp1 div 2) stp)
+           (tshift tp (length tp1 div 2), length tp1 div 2) =
           (st' + length tp1 div 2, l', r')"
     apply(simp add: k)
     apply(simp add: tstep.simps t_step.simps)
     apply(case_tac "fetch tp a (case c of [] \<Rightarrow> Bk | x # xs \<Rightarrow> x)", simp)
-    apply(subgoal_tac "fetch (abacus.tshift tp (length tp1 div 2)) a
+    apply(subgoal_tac "fetch (tshift tp (length tp1 div 2)) a
                        (case c of [] \<Rightarrow> Bk | x # xs \<Rightarrow> x) = (aa, st' + length tp1 div 2)", simp)
     apply(simp add: tshift_fetch)
     done
@@ -1215,7 +1215,7 @@
     "t_ncorrect tp"
     "t_ncorrect tp2"
   from h have 
-    "\<exists>stp>0. t_steps (st + length tp1 div 2, l, r) (tp1 @ abacus.tshift tp (length tp1 div 2) @ tp2, 0) stp = 
+    "\<exists>stp>0. t_steps (st + length tp1 div 2, l, r) (tp1 @ tshift tp (length tp1 div 2) @ tp2, 0) stp = 
                             (st' + length tp1 div 2, l', r')"
     apply(rule_tac stp = stp in turing_shift, simp_all add: shift_length)
     apply(simp add: t_steps_steps_eq)
@@ -1225,7 +1225,7 @@
                   = (st' + length tp1 div 2, l', r')"
     apply(erule_tac exE)
     apply(rule_tac x = stp in exI, simp)
-    apply(subgoal_tac "length (tp1 @ abacus.tshift tp (length tp1 div 2) @ tp2) mod 2 = 0")
+    apply(subgoal_tac "length (tp1 @ tshift tp (length tp1 div 2) @ tp2) mod 2 = 0")
     apply(simp only: steps_eq)
     using h
     apply(auto simp: t_ncorrect.simps shift_length)
@@ -1407,7 +1407,7 @@
     done
 next
   show "t_ncorrect ((L, Suc 0) # (L, Suc 0) #
-       abacus.tshift t_fourtimes (t_twice_len + 13) @ [(L, Suc 0), (L, Suc 0)])"
+       tshift t_fourtimes (t_twice_len + 13) @ [(L, Suc 0), (L, Suc 0)])"
     using length_tm_even[of abc_fourtimes]
     apply(simp add: t_ncorrect.simps shift_length t_fourtimes_def)
     apply arith
@@ -2081,7 +2081,7 @@
     done
 next
   show "t_ncorrect (t_wcode_main_first_part @ 
-    abacus.tshift t_twice (length t_wcode_main_first_part div 2) @ 
+    tshift t_twice (length t_wcode_main_first_part div 2) @ 
     [(L, Suc 0), (L, Suc 0)])"
     apply(simp add: t_ncorrect.simps t_wcode_main_first_part_def shift_length
                     t_twice_def)
@@ -2107,13 +2107,13 @@
 apply(simp add: t_twice_def)
 done
 
-lemma [simp]: "((26 + length (abacus.tshift t_twice 12)) div 2)
-             = (length (abacus.tshift t_twice 12) div 2 + 13)"
+lemma [simp]: "((26 + length (tshift t_twice 12)) div 2)
+             = (length (tshift t_twice 12) div 2 + 13)"
 using tm_even[of abc_twice]
 apply(simp add: t_twice_def)
 done 
 
-lemma [simp]: "t_twice_len + 14 =  14 + length (abacus.tshift t_twice 12) div 2"
+lemma [simp]: "t_twice_len + 14 =  14 + length (tshift t_twice 12) div 2"
 using tm_even[of abc_twice]
 apply(simp add: t_twice_def t_twice_len_def shift_length)
 done
@@ -3351,13 +3351,13 @@
     done
   hence "list_all (\<lambda>(acn, s). s \<le>  Suc (length (tm_of abc_twice @ tMp (Suc 0)
     (start_of twice_ly (length abc_twice) - Suc 0)) div 2) + 12)
-     (abacus.tshift (change_termi_state (tm_of abc_twice @ tMp (Suc 0) 
+     (tshift (change_termi_state (tm_of abc_twice @ tMp (Suc 0) 
            (start_of twice_ly (length abc_twice) - Suc 0))) 12)"
     apply(rule_tac t_correct_shift, simp)
     done
   thus  "list_all (\<lambda>(acn, s). s \<le> 
            (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2)
-     (abacus.tshift (change_termi_state (tm_of abc_twice @ tMp (Suc 0)
+     (tshift (change_termi_state (tm_of abc_twice @ tMp (Suc 0)
                  (start_of twice_ly (length abc_twice) - Suc 0))) 12)"
     apply(simp)
     apply(simp add: list_all_length, auto)
@@ -3371,12 +3371,12 @@
     done
   hence "list_all (\<lambda>(acn, s). s \<le> Suc (length (tm_of abc_fourtimes @ tMp (Suc 0) 
     (start_of fourtimes_ly (length abc_fourtimes) - Suc 0)) div 2) + (t_twice_len + 13))
-    (abacus.tshift (change_termi_state (tm_of abc_fourtimes @ tMp (Suc 0) 
+    (tshift (change_termi_state (tm_of abc_fourtimes @ tMp (Suc 0) 
     (start_of fourtimes_ly (length abc_fourtimes) - Suc 0))) (t_twice_len + 13))"
     apply(rule_tac t_correct_shift, simp)
     done
   thus "list_all (\<lambda>(acn, s). s \<le> (60 + (length (tm_of abc_twice) + length (tm_of abc_fourtimes))) div 2)
-    (abacus.tshift (change_termi_state (tm_of abc_fourtimes @ tMp (Suc 0)
+    (tshift (change_termi_state (tm_of abc_fourtimes @ tMp (Suc 0)
     (start_of fourtimes_ly (length abc_fourtimes) - Suc 0))) (t_twice_len + 13))"
     apply(simp add: t_twice_len_def t_twice_def)
     using twice_len_even fourtimes_len_even
tm