
diff -r d5a0e25c4742 -r a9003e6d0463 thys/Abacus.thy
--- a/thys/Abacus.thy	Wed Jan 14 09:08:51 2015 +0000
+++ b/thys/Abacus.thy	Wed Dec 19 16:10:58 2018 +0100
@@ -2,7 +2,7 @@
    Author: Jian Xu, Xingyuan Zhang, and Christian Urban
 *)
 
-header {* Abacus Machines *}
+chapter {* Abacus Machines *}
 
 theory Abacus
 imports Turing_Hoare Abacus_Mopup
@@ -203,7 +203,7 @@
 
 fun start_of :: "nat list \<Rightarrow> nat \<Rightarrow> nat"
   where
-  "start_of ly x = (Suc (listsum (take x ly))) "
+  "start_of ly x = (Suc (sum_list (take x ly))) "
 
 text {*
   @{text "ci lo ss i"} complies Abacus instruction @{text "i"}
@@ -451,10 +451,10 @@
                concat (take (Suc n) tps)")
 apply(simp only: append_assoc[THEN sym], simp only: append_assoc)
 apply(subgoal_tac " concat (drop (Suc n) tps) = tps ! Suc n @ 
-                  concat (drop (Suc (Suc n)) tps)", simp)
-apply(rule_tac concat_drop_suc_iff, simp)
-apply(rule_tac concat_take_suc_iff, simp)
-done
+                  concat (drop (Suc (Suc n)) tps)")
+  apply (metis append_take_drop_id concat_append)
+   apply(rule concat_drop_suc_iff,force)
+  by (simp add: concat_suc)
 
 declare append_assoc[simp]
 
@@ -498,59 +498,48 @@
 
 lemma div_apart: "\<lbrakk>x mod (2::nat) = 0; y mod 2 = 0\<rbrakk> 
           \<Longrightarrow> (x + y) div 2 = x div 2 + y div 2"
-apply(drule mod_eqD)+
-apply(auto)
-done
+  by(auto)
 
 lemma div_apart_iff: "\<lbrakk>x mod (2::nat) = 0; y mod 2 = 0\<rbrakk> \<Longrightarrow> 
            (x + y) mod 2 = 0"
-apply(auto)
-done
+by(auto)
 
 lemma [simp]: "length (layout_of aprog) = length aprog"
-apply(auto simp: layout_of.simps)
-done
+by(auto simp: layout_of.simps)
 
 lemma start_of_ind: "\<lbrakk>as < length aprog; ly = layout_of aprog\<rbrakk> \<Longrightarrow> 
        start_of ly (Suc as) = start_of ly as + 
                           length ((tms_of aprog) ! as) div 2"
-apply(simp only: start_of.simps, simp)
-apply(auto simp: start_of.simps tms_of.simps layout_of.simps 
-                 tpairs_of.simps)
-apply(simp add: ci_length take_Suc take_Suc_conv_app_nth)
-done
+  by (auto simp: start_of.simps tms_of.simps layout_of.simps 
+                 tpairs_of.simps ci_length take_Suc take_Suc_conv_app_nth)
 
 lemma concat_take_suc: "Suc n \<le> length xs \<Longrightarrow>
   concat (take (Suc n) xs) = concat (take n xs) @ (xs ! n)"
-apply(subgoal_tac "take (Suc n) xs =
-                   take n xs @ [xs ! n]")
-apply(auto)
-done
+  using concat_suc.
 
 lemma [simp]: 
   "\<lbrakk>as < length aprog; (abc_fetch as aprog) = Some ins\<rbrakk>
   \<Longrightarrow> ci (layout_of aprog) 
   (start_of (layout_of aprog) as) (ins) \<in> set (tms_of aprog)"
-apply(insert ci_nth[of "layout_of aprog" aprog as], simp)
-done
+  by(insert ci_nth[of "layout_of aprog" aprog as], simp)
 
 lemma [simp]: "length (tms_of ap) = length ap"
 by(auto simp: tms_of.simps tpairs_of.simps)
 
 lemma [intro]:  "n < length ap \<Longrightarrow> length (tms_of ap ! n) mod 2 = 0"
-apply(auto simp: tms_of.simps tpairs_of.simps)
-apply(case_tac "ap ! n", auto simp: ci.simps length_findnth tinc_b_def tdec_b_def)
-apply arith
-by arith
+  apply(cases "ap ! n")
+  by (auto simp: tms_of.simps tpairs_of.simps ci.simps length_findnth tinc_b_def tdec_b_def)
 
 lemma compile_mod2: "length (concat (take n (tms_of ap))) mod 2 = 0"
-apply(induct n, auto)
-apply(case_tac "n < length (tms_of ap)", simp add: take_Suc_conv_app_nth, auto)
-(*apply(subgoal_tac "length (tms_of ap ! n) mod 2 = 0")
-apply arith
-by auto
-*)
-done
+proof(induct n)
+  case 0
+  then show ?case by (auto simp add: take_Suc_conv_app_nth)
+next
+  case (Suc n)
+  hence "n < length (tms_of ap) \<Longrightarrow> is_even (length (concat (take (Suc n) (tms_of ap))))"
+    unfolding take_Suc_conv_app_nth by fastforce
+  with Suc show ?case by(cases "n < length (tms_of ap)", auto)
+qed
 
 lemma tpa_states:
   "\<lbrakk>tp = concat (take as (tms_of ap));
@@ -615,8 +604,7 @@
     tp1 = concat (take as (tms_of ap)) \<and> tp2 = concat (drop (Suc as) (tms_of ap))" by blast
   then have b: "start_of (layout_of ap) as = Suc (length tp1 div 2)"
     using fetch
-    apply(rule_tac tpa_states, simp, simp add: abc_fetch.simps split: if_splits)
-    done
+    by(rule_tac tpa_states, simp, simp add: abc_fetch.simps split: if_splits)
   have "fetch (tp1 @ (ci ly (start_of ly as) ins) @ tp2)  s b = 
         fetch (ci ly (start_of ly as) ins) (s - length tp1 div 2) b"
   proof(rule_tac append_append_fetch)
@@ -625,8 +613,7 @@
       by(auto, rule_tac compile_mod2)
   next
     show "length (ci ly (start_of ly as) ins) mod 2 = 0"
-      apply(case_tac ins, auto simp: ci.simps length_findnth tinc_b_def tdec_b_def)
-      by(arith, arith)
+      by(case_tac ins, auto simp: ci.simps length_findnth tinc_b_def tdec_b_def)
   next
     show "length tp1 div 2 < s \<and> s \<le> 
       length tp1 div 2 + length (ci ly (start_of ly as) ins) div 2"
@@ -694,17 +681,12 @@
       using abc_fetch layout
       apply(case_tac b, simp_all add: Suc_diff_le)
       apply(case_tac [!] ins, simp_all add: start_of_Suc2 start_of_Suc1 start_of_Suc3)
-      apply(simp_all only: length_ci_inc length_ci_dec length_ci_goto, auto)
-      using layout
-      apply(subgoal_tac [!] "start_of ly (Suc as) = start_of ly as + 2*nat1 + 16", simp_all)
-      apply(rule_tac [!] start_of_Suc2, auto)
-      done
+      by (simp_all only: length_ci_inc length_ci_dec length_ci_goto, auto)
     from fetch and notfinal this show "?thesis"by simp
   qed
   ultimately show "?thesis"
     using assms
-    apply(drule_tac b= b and ins = ins in step_eq_fetch', auto)
-    done
+    by(drule_tac b= b and ins = ins in step_eq_fetch', auto)
 qed
 
 
@@ -1245,8 +1227,7 @@
     (is "\<exists>lm1 tn rn. ?P lm1 tn rn")
   proof -
     from k have "?P lm1 tn (rn - 1)"
-      apply(auto simp: Oc_def)
-      by(case_tac [!] "rn::nat", auto)
+      by (auto simp: Cons_replicate_eq)
     thus ?thesis by blast
   qed
 next
@@ -1264,21 +1245,20 @@
     (is "\<exists>lm1 tn rn. ?P lm1 tn rn")
   proof -
     from h1 and h2  have "?P lm1 0 (rn - 1)"
-      apply(auto simp: Oc_def
-                      tape_of_nl_abv tape_of_nat_list.simps)
+      apply(auto simp:tape_of_nat_def)
       by(case_tac "rn::nat", simp, simp)
     thus ?thesis by blast
   qed
 qed
 
-lemma [simp]: "inv_locate_a (as, am) (q, aaa, []) ires \<Longrightarrow> 
+lemma inv_locate_a[simp]: "inv_locate_a (as, am) (q, aaa, []) ires \<Longrightarrow> 
                inv_locate_a (as, am) (q, aaa, [Oc]) ires"
 apply(insert locate_a_2_locate_a [of as am q aaa "[]"])
 apply(subgoal_tac "inv_locate_a (as, am) (q, aaa, [Bk]) ires", auto)
 done
 
 (*inv: from locate_b to locate_b*)
-lemma [simp]: "inv_locate_b (as, am) (q, aaa, Oc # xs) ires
+lemma inv_locate_b[simp]: "inv_locate_b (as, am) (q, aaa, Oc # xs) ires
          \<Longrightarrow> inv_locate_b (as, am) (q, Oc # aaa, xs) ires"
 apply(simp only: inv_locate_b.simps in_middle.simps)
 apply(erule exE)+
@@ -1289,15 +1269,15 @@
 apply(case_tac mr, simp_all, auto)
 done
 
-lemma [simp]:  "<[x::nat]> = Oc\<up>(Suc x)"
-apply(simp add: tape_of_nat_abv tape_of_nl_abv)
+lemma tape_nat[simp]:  "<[x::nat]> = Oc\<up>(Suc x)"
+apply(simp add: tape_of_nat_def tape_of_list_def)
 done
 
-lemma [simp]: " <([]::nat list)> = []"
-apply(simp add: tape_of_nl_abv)
+lemma tape_empty_list[simp]: " <([]::nat list)> = []"
+apply(simp add: tape_of_list_def)
 done
 
-lemma [simp]: "\<lbrakk>inv_locate_b (as, am) (q, aaa, Bk # xs) ires; \<exists>n. xs = Bk\<up>n\<rbrakk>
+lemma inv_locate[simp]: "\<lbrakk>inv_locate_b (as, am) (q, aaa, Bk # xs) ires; \<exists>n. xs = Bk\<up>n\<rbrakk>
             \<Longrightarrow> inv_locate_a (as, am) (Suc q, Bk # aaa, xs) ires"
 apply(simp add: inv_locate_b.simps inv_locate_a.simps)
 apply(rule_tac disjI2, rule_tac disjI1)
@@ -1628,8 +1608,8 @@
 apply(rule_tac x = "lm2" in exI, simp)
 apply(simp only: Suc_diff_le exp_ind)
 apply(subgoal_tac "lm2 = []", simp)
-apply(drule_tac length_equal, simp)
-done
+  apply(drule_tac length_equal, simp)
+  by (metis (no_types, lifting) add_diff_inverse_nat append.assoc append_eq_append_conv length_append length_replicate list.inject)
 
 lemma [simp]: "inv_locate_b (as, am) (n, aaa, []) ires \<Longrightarrow> 
      inv_after_write (as, abc_lm_s am n (Suc (abc_lm_v am n))) 
@@ -1819,15 +1799,14 @@
 apply(case_tac "hd l", simp, simp, simp)
 done
 
-(*inv: from on_left_moving to check_left_moving*)
-lemma [simp]: "inv_on_left_moving_in_middle_B (as, lm) 
+lemma from_on_left_moving_to_check_left_moving[simp]: "inv_on_left_moving_in_middle_B (as, lm) 
                                       (s, Bk # list, Bk # r) ires
           \<Longrightarrow> inv_check_left_moving_on_leftmost (as, lm) 
                                       (s', list, Bk # Bk # r) ires"
 apply(auto simp: inv_on_left_moving_in_middle_B.simps 
                  inv_check_left_moving_on_leftmost.simps split: if_splits)
 apply(case_tac [!] "rev lm1", simp_all)
-apply(case_tac [!] lista, simp_all add: tape_of_nl_abv tape_of_nat_abv tape_of_nat_list.simps)
+apply(case_tac [!] lista, simp_all add: tape_of_nat_def tape_of_list_def)
 done
 
 lemma [simp]:
@@ -1895,11 +1874,11 @@
 apply(erule_tac exE)+
 apply(rule_tac x = "rev (tl (rev lm1))" in exI, 
       rule_tac x = "[hd (rev lm1)] @ lm2" in exI, auto)
-apply(case_tac [!] "rev lm1",simp_all add: tape_of_nat_abv tape_of_nl_abv tape_of_nat_list.simps)
+apply(case_tac [!] "rev lm1",simp_all add: tape_of_nat_def tape_of_list_def tape_of_nat_list.simps)
 apply(case_tac [!] a, simp_all)
-apply(case_tac [1] lm2, simp_all add: tape_of_nat_list.simps tape_of_nat_abv, auto)
-apply(case_tac [3] lm2, simp_all add: tape_of_nat_list.simps tape_of_nat_abv, auto)
-apply(case_tac [!] lista, simp_all add: tape_of_nat_abv tape_of_nat_list.simps)
+apply(case_tac [1] lm2, auto simp:tape_of_nat_def)
+apply(case_tac [3] lm2, auto simp:tape_of_nat_def)
+apply(case_tac [!] lista, simp_all add: tape_of_nat_def)
 done
 
 lemma [simp]: 
@@ -3320,7 +3299,7 @@
 by(auto intro:wf_inv_image simp:abc_dec_2_LE_def lex_square_def lex_triple_def lex_pair_def)
 
 lemma fix_add: "fetch ap ((x::nat) + 2*n) b = fetch ap (2*n + x) b"
-by (metis Suc_1 mult_2 nat_add_commute)
+  using Suc_1 add.commute by metis
 
 lemma [elim]: 
  "\<lbrakk>0 < abc_lm_v am n; inv_locate_n_b (as, am) (n, aaa, Bk # xs) ires\<rbrakk> 
@@ -3486,9 +3465,7 @@
    abc_fetch as ap = Some (Dec n e)\<rbrakk>
   \<Longrightarrow> crsp (layout_of ap) (abc_step_l (as, lm) (Some (Dec n e))) 
   (start_of (layout_of ap) as + 2 * n + 16, a, b) ires"
-apply(auto simp: inv_stop.simps crsp.simps  abc_step_l.simps startof_Suc2)
-apply(drule_tac startof_Suc2, simp)
-done
+  by(auto simp: inv_stop.simps crsp.simps  abc_step_l.simps startof_Suc2)
   
 lemma crsp_step_dec_b_suc:
   assumes layout: "ly = layout_of ap"
@@ -3693,7 +3670,7 @@
 
 lemma length_tp'[simp]: 
   "\<lbrakk>ly = layout_of ap; tp = tm_of ap\<rbrakk> \<Longrightarrow>
-       length tp = 2 * listsum (take (length ap) (layout_of ap))"
+       length tp = 2 * sum_list (take (length ap) (layout_of ap))"
 proof(induct ap arbitrary: ly tp rule: rev_induct)
   case Nil
   thus "?case"
@@ -3701,18 +3678,18 @@
 next
   fix x xs ly tp
   assume ind: "\<And>ly tp. \<lbrakk>ly = layout_of xs; tp = tm_of xs\<rbrakk> \<Longrightarrow> 
-    length tp = 2 * listsum (take (length xs) (layout_of xs))"
+    length tp = 2 * sum_list (take (length xs) (layout_of xs))"
   and layout: "ly = layout_of (xs @ [x])"
   and tp: "tp = tm_of (xs @ [x])"
   obtain ly' where a: "ly' = layout_of xs"
     by metis
   obtain tp' where b: "tp' = tm_of xs"
     by metis
-  have c: "length tp' = 2 * listsum (take (length xs) (layout_of xs))"
+  have c: "length tp' = 2 * sum_list (take (length xs) (layout_of xs))"
     using a b
     by(erule_tac ind, simp)
   thus "length tp = 2 * 
-    listsum (take (length (xs @ [x])) (layout_of (xs @ [x])))"
+    sum_list (take (length (xs @ [x])) (layout_of (xs @ [x])))"
     using tp b
     apply(auto simp: layout_id_cons tm_of.simps tms_of.simps length_concat tpairs_id_cons map_length_ci)
     apply(case_tac x)




