diff -r d5a0e25c4742 -r a9003e6d0463 thys/Abacus_Mopup.thy
--- a/thys/Abacus_Mopup.thy	Wed Jan 14 09:08:51 2015 +0000
+++ b/thys/Abacus_Mopup.thy	Wed Dec 19 16:10:58 2018 +0100
@@ -2,7 +2,7 @@
    Author: Jian Xu, Xingyuan Zhang, and Christian Urban
 *)
 
-header {* Mopup Turing Machine that deletes all "registers", except one *}
+chapter {* Mopup Turing Machine that deletes all "registers", except one *}
 
 theory Abacus_Mopup
 imports Uncomputable
@@ -156,7 +156,7 @@
   "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = 0\<rbrakk> \<Longrightarrow> 
      (fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk) = (R, s - 1)"
 apply(subgoal_tac "\<exists> q. s = 2 * q", auto)
-apply(case_tac qa, simp, simp)
+apply(case_tac q, simp, simp)
 apply(auto simp: fetch.simps nth_of.simps nth_append)
 apply(subgoal_tac "mopup_a n ! (4 * nat + 2) = 
                      mopup_a (Suc nat) ! ((4 * nat) + 2)", 
@@ -290,12 +290,12 @@
 
 lemma tape_of_nl_cons: "<m # lm> = (if lm = [] then Oc\<up>(Suc m)
                     else Oc\<up>(Suc m) @ Bk # <lm>)"
-apply(case_tac lm, simp_all add: tape_of_nl_abv  tape_of_nat_abv split: if_splits)
-done
+  by(case_tac lm, simp_all add: tape_of_list_def  tape_of_nat_def split: if_splits)
 
 lemma drop_tape_of_cons: 
   "\<lbrakk>Suc q < length lm; x = lm ! q\<rbrakk> \<Longrightarrow> <drop q lm> = Oc # Oc \<up> x @ Bk # <drop (Suc q) lm>"
-by (metis Suc_lessD append_Cons list.simps(2) nth_drop' replicate_Suc tape_of_nl_cons)
+  using Suc_lessD append_Cons list.simps(2) Cons_nth_drop_Suc replicate_Suc tape_of_nl_cons
+  by metis
 
 lemma erase2jumpover1:
   "\<lbrakk>q < length list; 
@@ -307,8 +307,8 @@
 apply(rule_tac drop_tape_of_cons, simp_all)
 apply(subgoal_tac "length list = Suc q", auto)
 apply(subgoal_tac "drop q list = [list ! q]")
-apply(simp add: tape_of_nl_abv tape_of_nat_abv replicate_Suc)
-by (metis append_Nil2 append_eq_conv_conj drop_Suc_conv_tl lessI)
+apply(simp add: tape_of_nat_def tape_of_list_def replicate_Suc)
+by (metis append_Nil2 append_eq_conv_conj Cons_nth_drop_Suc lessI)
 
 lemma erase2jumpover2:
   "\<lbrakk>q < length list; \<forall>rn. <drop q list> @ Bk # Bk \<up> n \<noteq>
@@ -319,8 +319,8 @@
 apply(erule_tac notE, simp add: replicate_Suc)
 apply(rule_tac drop_tape_of_cons, simp_all)
 apply(subgoal_tac "length list = Suc q", auto)
-apply(erule_tac x = "n" in allE, simp add: tape_of_nl_abv)
-by (metis append_Nil2 append_eq_conv_conj drop_Suc_conv_tl lessI replicate_Suc tape_of_nl_abv tape_of_nl_cons)
+apply(erule_tac x = "n" in allE, simp add: tape_of_list_def)
+by (metis append_Nil2 append_eq_conv_conj Cons_nth_drop_Suc lessI replicate_Suc tape_of_list_def tape_of_nl_cons)
 
 lemma mod_ex1: "(a mod 2 = Suc 0) = (\<exists> q. a = Suc (2 * q))"
 by arith
@@ -449,12 +449,10 @@
 apply(rule mopup_jump_over1_2_aft_erase_a, simp)
 apply(auto simp: mopup_jump_over1.simps)
 apply(rule_tac x = ln in exI, rule_tac x = "Suc (lm ! n)" in exI, 
-      rule_tac x = 0 in exI, simp add: tape_of_nl_abv )
+      rule_tac x = 0 in exI, simp add: tape_of_list_def )
 done
 
-lemma [simp]: "<[]> = []"
-apply(simp add: tape_of_nl_abv)
-done
+lemma [simp]: "<[]> = []" by(simp add: tape_of_list_def)
 
 lemma [simp]: 
  "\<lbrakk>n < length lm; 
@@ -467,7 +465,7 @@
 apply(case_tac a, simp_all)
 apply(rule_tac x = rn in exI, rule_tac x = "[]" in exI, simp)
 apply(rule_tac x = rn in exI, rule_tac x = "[nat]" in exI, simp)
-apply(case_tac a, simp,  simp add: tape_of_nl_abv tape_of_nat_abv)
+apply(case_tac a, simp,  simp add: tape_of_list_def tape_of_nat_def)
 apply(case_tac a, simp_all)
 apply(rule_tac x = rn in exI, rule_tac x = "list" in exI, simp)
 apply(rule_tac x = rn in exI, simp)
@@ -519,7 +517,7 @@
 apply(case_tac a, simp_all)
 apply(rule_tac x = rn in exI, rule_tac x = "[]" in exI, simp)
 apply(rule_tac x = rn in exI, rule_tac x = "[nat]" in exI, simp)
-apply(simp add: tape_of_nl_abv tape_of_nat_abv)
+apply(simp add: tape_of_list_def tape_of_nat_def)
 done
 
 lemma [intro]: "\<exists>rna ml. Oc \<up> a @ Bk # <list::nat list> @ Bk \<up> rn = 
@@ -655,7 +653,7 @@
  "\<lbrakk>n < length lm; mopup_jump_over2 (2 * n + 6, l, Bk # xs) lm n ires\<rbrakk> 
   \<Longrightarrow> mopup_stop (0, Bk # l, xs) lm n ires"
 apply(auto simp: mopup_jump_over2.simps mopup_stop.simps)
-apply(simp_all add: tape_of_nat_abv exp_ind[THEN sym])
+apply(simp_all add: tape_of_nat_def exp_ind[THEN sym])
 done
 
 lemma [simp]: "mopup_jump_over2 (2 * n + 6, l, []) lm n ires = False"
@@ -791,8 +789,7 @@
     have "((step (a, b, c) (mopup_a n @ shift mopup_b (2 * n), 0), n), (a, b, c), n) \<in> abc_mopup_measure"
       apply(case_tac c, case_tac [2] aa)
       apply(auto split:if_splits simp add:step.simps mopup_inv.simps)
-      apply(simp_all add: mopupfetchs abc_mopup_measure_def)
-      done
+      by (auto split:if_splits simp: mopupfetchs abc_mopup_measure_def)
     thus "((step (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na) 
       (mopup_a n @ shift mopup_b (2 * n), 0), n),
       steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na, n)
@@ -840,7 +837,7 @@
       (mopup_a n @ shift mopup_b (2 * n), 0) stp")
     apply(simp add: mopup_inv.simps mopup_stop.simps rs)
     using rs
-    apply(simp add: tape_of_nat_abv)
+    apply(simp add: tape_of_nat_def)
     done
 qed