diff -r 6e1c03614d36 -r 93db7414931d thys/Abacus.thy
--- a/thys/Abacus.thy	Fri Dec 21 12:31:36 2018 +0100
+++ b/thys/Abacus.thy	Fri Dec 21 15:30:24 2018 +0100
@@ -362,10 +362,6 @@
     done
 qed
 
-lemma startof_not0[simp]: "0 < start_of ly as"
-apply(simp add: start_of.simps)
-done
-
 lemma startof_ge1[simp]: "Suc 0 \<le> start_of ly as"
 apply(simp add: start_of.simps)
 done
@@ -423,11 +419,6 @@
 apply(subgoal_tac "take (Suc as) xs = take as xs @ [xs ! as]", simp)
 by auto
 
-lemma concat_take_suc_iff: "Suc n \<le> length tps \<Longrightarrow> 
-       concat (take n tps) @ (tps ! n) = concat (take (Suc n) tps)"
-apply(drule_tac concat_suc, simp)
-done
-
 lemma concat_drop_suc_iff: 
    "Suc n < length tps \<Longrightarrow> concat (drop (Suc n) tps) = 
            tps ! Suc n @ concat (drop (Suc (Suc n)) tps)"
@@ -458,9 +449,6 @@
 
 declare append_assoc[simp]
 
-lemma map_of:  "n < length xs \<Longrightarrow> (map f xs) ! n = f (xs ! n)"
-by(auto)
-
 lemma length_tms_of[simp]: "length (tms_of aprog) = length aprog"
 apply(auto simp: tms_of.simps tpairs_of.simps)
 done
@@ -470,7 +458,7 @@
   abc_fetch as aprog = Some ins\<rbrakk>
   \<Longrightarrow> ci ly (start_of ly as) ins = tms_of aprog ! as"
 apply(simp add: tms_of.simps tpairs_of.simps 
-      abc_fetch.simps  map_of del: map_append split: if_splits)
+      abc_fetch.simps del: map_append split: if_splits)
 done
 
 lemma t_split:"\<lbrakk>
@@ -488,41 +476,13 @@
 apply(rule_tac ci_nth, auto)
 done
 
-lemma math_sub: "\<lbrakk>x >= Suc 0; x - 1 = z\<rbrakk> \<Longrightarrow> x + y - Suc 0 = z + y"
-by auto
-
-lemma start_more_one: "as \<noteq> 0 \<Longrightarrow> start_of ly as >= Suc 0"
-apply(induct as, simp add: start_of.simps)
-apply(case_tac as, auto simp: start_of.simps)
-done
-
 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"
   by(auto)
 
-lemma div_apart_iff: "\<lbrakk>x mod (2::nat) = 0; y mod 2 = 0\<rbrakk> \<Longrightarrow> 
-           (x + y) mod 2 = 0"
-by(auto)
-
 lemma length_layout_of[simp]: "length (layout_of aprog) = length aprog"
 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"
-  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)"
-  using concat_suc.
-
-lemma ci_in_set[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)"
-  by(insert ci_nth[of "layout_of aprog" aprog as], simp)
-
 lemma length_tms_of_elem_even[intro]:  "n < length ap \<Longrightarrow> length (tms_of ap ! n) mod 2 = 0"
   apply(cases "ap ! n")
   by (auto simp: tms_of.simps tpairs_of.simps ci.simps length_findnth tinc_b_def tdec_b_def)
@@ -1247,10 +1207,6 @@
 apply(simp add: tape_of_nat_def tape_of_list_def)
 done
 
-lemma tape_empty_list[simp]: " <([]::nat list)> = []"
-apply(simp add: tape_of_list_def)
-done
-
 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)
@@ -1338,9 +1294,6 @@
 
 (*inv: from locate_b to after_write*)
 
-lemma not_even_then_odd[simp]: "(a mod 2 \<noteq> 0) = (a mod 2 = Suc 0)  "
-by arith
-
 lemma div_rounding_down[simp]: "(2*q - Suc 0) div 2 = (q - 1)" "(Suc (2*q)) div 2 = q"
 by arith+
 
@@ -1399,10 +1352,7 @@
       done
   qed
 qed
-            
-lemma inv_locate_aI[intro]: "inv_locate_a (as, lm) (0, Bk # Bk # ires, <lm> @ Bk \<up> x) ires"
-apply(auto simp: crsp.simps inv_locate_a.simps at_begin_norm.simps)
-done
+
 lemma inv_locate_a_via_crsp[simp]:
  "crsp ly (as, lm) (s, l, r) ires \<Longrightarrow> inv_locate_a (as, lm) (0, l, r) ires"
 apply(auto simp: crsp.simps inv_locate_a.simps at_begin_norm.simps)
@@ -1524,14 +1474,6 @@
   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 inv_after_write_via_locate_b[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))) 
-                     (s, aaa, [Oc]) ires"
-apply(insert inv_locate_b_2_after_write [of as am n aaa "[]"])
-by(simp)
-
-
-
 (*inv: from after_write to after_move*)
 lemma inv_after_move_Oc_via_write[simp]: "inv_after_write (as, lm) (x, l, Oc # r) ires
                 \<Longrightarrow> inv_after_move (as, lm) (y, Oc # l, r) ires"
@@ -1608,15 +1550,6 @@
 apply(case_tac [!] rn, simp_all)
 done
 
-lemma inv_after_clear_singleton_Bk[simp]: "inv_after_clear (as, lm) (x, l, []) ires\<Longrightarrow> 
-               inv_after_clear (as, lm) (y, l, [Bk]) ires" 
-by(auto simp: inv_after_clear.simps)
-
-lemma inv_on_right_moving_Bk[simp]: "inv_after_clear (as, lm) (x, l, []) ires
-             \<Longrightarrow> inv_on_right_moving (as, lm) (y, Bk # l, []) ires"
-by(insert 
-    inv_after_clear_2_inv_on_right_moving[of as lm n l "[]"], simp)
-
 (*inv: from on_right_moving to on_right_movign*)
 lemma inv_on_right_moving_Oc[simp]: "inv_on_right_moving (as, lm) (x, l, Oc # r) ires
       \<Longrightarrow> inv_on_right_moving (as, lm) (y, Oc # l, r) ires"
@@ -1646,12 +1579,6 @@
 apply(rule_tac x = lm1 in exI, rule_tac x = "[]" in exI, simp)
 done
 
-(*inv: from on_right_moving to after_write*)
-lemma inv_after_write_singleton_Oc[simp]: "inv_on_right_moving (as, lm) (x, l, []) ires
-       \<Longrightarrow> inv_after_write (as, lm) (y, l, [Oc]) ires"
-apply(rule_tac inv_on_right_moving_2_inv_on_right_moving, simp)
-done
-
 (*inv: from on_left_moving to on_left_moving*)
 lemma no_inv_on_left_moving_in_middle_B_Oc[simp]: "inv_on_left_moving_in_middle_B (as, lm) 
                (s, l, Oc # r) ires = False"
@@ -1750,22 +1677,11 @@
 apply(auto simp: inv_on_left_moving_norm.simps)
 done
 
-lemma inv_on_left_moving_Bk[simp]: "inv_on_left_moving (as, lm) (s, l, []) ires\<Longrightarrow> 
-     inv_on_left_moving (as, lm) (6 + 2 * n, l, [Bk]) ires"
-apply(simp add: inv_on_left_moving.simps)
-apply(auto simp: inv_on_left_moving_in_middle_B.simps)
-done
-
 lemma inv_on_left_moving_no_empty[simp]: "inv_on_left_moving (as, lm) (s, l, []) ires = False"
 apply(simp add: inv_on_left_moving.simps)
 apply(simp add: inv_on_left_moving_in_middle_B.simps)
 done
 
-lemma inv_on_left_moving_cases_left[simp]: "inv_on_left_moving (as, lm) (s, l, []) ires
- \<Longrightarrow> (l = [] \<longrightarrow> inv_check_left_moving (as, lm) (s', [], [Bk]) ires) \<and>
-    (l \<noteq> [] \<longrightarrow> inv_check_left_moving (as, lm) (s', tl l, [hd l]) ires)"
-by simp
-
 lemma Bk_plus_one[intro]: "\<exists>rna. Bk # Bk \<up> rn = Bk \<up> rna"
   apply(rule_tac x = "Suc rn" in exI, simp)
   done
@@ -1792,13 +1708,6 @@
      inv_check_left_moving_in_middle (as, lm) (s', [Bk], Oc # r) ires"
 apply(auto simp: inv_check_left_moving_in_middle.simps )
 done
-lemma inv_on_left_moving_in_middle_B_Bk_Oc_via_check[simp]: 
- "inv_check_left_moving_in_middle (as, lm) (s, [], Oc # r) ires
-   \<Longrightarrow> inv_on_left_moving_in_middle_B (as, lm) (s', [], Bk # Oc # r) ires"
-apply(insert 
-inv_check_left_moving_in_middle_2_on_left_moving_in_middle_B[of 
-                  as lm n "[]" r], simp)
-done 
 
 lemma inv_on_left_moving_norm_Oc_Oc_via_middle[simp]: "inv_check_left_moving_in_middle (as, lm) 
                        (s, Oc # list, Oc # r) ires
@@ -2280,31 +2189,8 @@
     by arith
 qed
     
-lemma abc_fetch_contrE[elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e); as < e; 
-  Suc (start_of (layout_of ap) as + 2 * n) = start_of (layout_of ap) e\<rbrakk> \<Longrightarrow> RR"
-  by(drule_tac start_of_ge, auto)
-
-lemma abc_fetch_contrE2[elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e); as > e;
-  Suc (start_of (layout_of ap) as + 2 * n) = start_of (layout_of ap) e\<rbrakk> \<Longrightarrow> RR"
-apply(drule_tac ly = "layout_of ap" in start_of_less[of])
-apply(arith)
-done
-
-lemma abc_fetch_contrE3[elim]: "\<lbrakk>abc_fetch as ap = Some (Dec n e);
-  Suc (start_of (layout_of ap) as + 2 * n) = start_of (layout_of ap) e\<rbrakk> \<Longrightarrow> RR"
-apply(subgoal_tac "as = e \<or> as < e \<or> as > e", auto)
-done
-
-lemma fetch_c_Oc[simp]:"fetch (ci (ly) (start_of ly as) (Dec n e)) (Suc (2 * n))  Oc
-  = (R, start_of ly as + 2*n + 1)"
-apply(auto simp: ci.simps findnth.simps fetch.simps
-                  nth_of.simps shift.simps nth_append tdec_b_def length_findnth adjust.simps)
-done
-
-
 declare dec_inv_1.simps[simp del]
 
-
 lemma start_of_ineq1[simp]: 
  "\<lbrakk>abc_fetch as aprog = Some (Dec n e); ly = layout_of aprog\<rbrakk>
    \<Longrightarrow> (start_of ly e \<noteq> Suc (start_of ly as + 2 * n) \<and>
@@ -2424,11 +2310,6 @@
 apply(auto simp: dec_after_clear.simps dec_right_move.simps split: if_splits)
 done
 
-lemma dec_right_move_Bk_via_clear_empty[simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, []) ires\<rbrakk>
-             \<Longrightarrow> dec_right_move (as, am) (s', Bk # l, []) ires"
-apply(auto simp: dec_after_clear.simps dec_right_move.simps )
-done
-
 lemma dec_right_move_Bk_Bk_via_clear[simp]: "\<lbrakk>dec_after_clear (as, am) (s, l, []) ires\<rbrakk>
              \<Longrightarrow> dec_right_move (as, am) (s', Bk # l, [Bk]) ires"
 apply(auto simp: dec_after_clear.simps dec_right_move.simps split: if_splits)
@@ -2454,12 +2335,6 @@
 apply(simp add: dec_right_move.simps)
 done
 
-lemma dec_check_right_move_Bk_via_move[simp]: "\<lbrakk>dec_right_move (as, am) (s, l, []) ires\<rbrakk>
-             \<Longrightarrow> dec_check_right_move (as, am) (s, Bk # l, []) ires"
-apply(insert dec_right_move_2_check_right_move[of as am s l "[]" s'], 
-      simp)
-done
-
 lemma dec_check_right_move_nonempty[simp]: "dec_check_right_move (as, am) (s, l, r) ires\<Longrightarrow> l \<noteq> []"
 apply(auto simp: dec_check_right_move.simps split: if_splits)
 done
@@ -2504,11 +2379,6 @@
 apply(rule_tac x = "[m]" in exI, auto)
 done
 
-lemma inv_on_left_moving_in_middle_B_Oc_Bk_Bk[simp]: "inv_on_left_moving_in_middle_B (as, [m])
-  (s', Oc # Oc\<up>m @ Bk # Bk # ires, [Bk]) ires"
-apply(simp add: inv_on_left_moving_in_middle_B.simps)
-done
-
 
 lemma inv_on_left_moving_in_middle_B_Oc_Bk_Bks_rev[simp]: "lm1 \<noteq> [] \<Longrightarrow> 
   inv_on_left_moving_in_middle_B (as, lm1 @ [m]) (s', 
@@ -2518,14 +2388,6 @@
 apply(simp add: tape_of_nl_cons split: if_splits)
 done
 
-lemma inv_on_left_moving_in_middle_B_Oc_Bk_Bk_rev[simp]: "lm1 \<noteq> [] \<Longrightarrow> 
-  inv_on_left_moving_in_middle_B (as, lm1 @ [m]) (s', 
-  Oc # Oc\<up> m @ Bk # <rev lm1> @ Bk # Bk # ires, [Bk]) ires"
-apply(simp only: inv_on_left_moving_in_middle_B.simps)
-apply(rule_tac x = "lm1 @ [m ]" in exI, rule_tac x = "[]" in exI, simp)
-apply(simp add: tape_of_nl_cons split: if_splits)
-done
-
 lemma inv_on_left_moving_Bk_tail[simp]: "dec_left_move (as, am) (s, l, Bk # r) ires
        \<Longrightarrow> inv_on_left_moving (as, am) (s', tl l, hd l # Bk # r) ires"
 apply(auto simp: dec_left_move.simps inv_on_left_moving.simps split: if_splits)
@@ -2583,11 +2445,6 @@
 apply(rule_tac x = lm1 in exI, simp)
 done
 
-lemma inv_stop_abc_lm_s_nonempty[simp]: 
- "inv_stop (as, abc_lm_s am n (abc_lm_v am n)) (s, l, r) ires \<Longrightarrow> l \<noteq> []"
-apply(auto simp: inv_stop.simps)
-done
-
 lemma dec_false_1[simp]:
  "\<lbrakk>abc_lm_v am n = 0; inv_locate_b (as, am) (n, aaa, Oc # xs) ires\<rbrakk>
   \<Longrightarrow> False"
@@ -2647,63 +2504,12 @@
 apply(simp_all only: exp_ind Nat.Suc_diff_le del: replicate_Suc, simp_all)
 apply(auto simp: inv_on_left_moving_in_middle_B.simps split: if_splits)
 apply(case_tac [!] m, simp_all)
-done
-
-lemma update_zero_to_zero[simp]: "\<lbrakk>am ! n = (0::nat); n < length am\<rbrakk> \<Longrightarrow> am[n := 0] = am"
-apply(simp add: list_update_same_conv)
-done
-
-lemma abc_lm_v_zero: "\<lbrakk>abc_lm_v (a # list) 0 = 0\<rbrakk> \<Longrightarrow> a = 0"
-apply(simp add: abc_lm_v.simps split: if_splits)
-done
-
-lemma inv_locate_a_via_stop[simp]: 
- "inv_stop (as, abc_lm_s am n 0) 
-          (start_of (layout_of aprog) e, aaa, Oc # xs) ires
-  \<Longrightarrow> inv_locate_a (as, abc_lm_s am n 0) (0, aaa, Oc # xs) ires"
-apply(simp add: inv_locate_a.simps)
-apply(rule disjI1)
-apply(auto simp: inv_stop.simps at_begin_norm.simps)
-done
-
-lemma inv_locate_b_cases_via_stop[simp]: 
- "\<lbrakk>inv_stop (as, abc_lm_s am n 0) 
-          (start_of (layout_of aprog) e, aaa, Oc # xs) ires\<rbrakk>
-  \<Longrightarrow> inv_locate_b (as, am) (0, Oc # aaa, xs) ires \<or> 
-      inv_locate_b (as, abc_lm_s am n 0) (0, Oc # aaa, xs) ires"
-apply(simp)
-done
-
-lemma dec_false2: 
- "inv_stop (as, abc_lm_s am n 0) 
-  (start_of (layout_of aprog) e, aaa, Bk # xs) ires = False"
-apply(auto simp: inv_stop.simps abc_lm_s.simps)
-apply(case_tac [!] am, auto)
-apply(case_tac [!] n, auto simp: tape_of_nl_cons split: if_splits)
-done
-
-lemma dec_false3:
-   "inv_stop (as, abc_lm_s am n 0) 
-              (start_of (layout_of aprog) e, aaa, []) ires = False"
-apply(auto simp: inv_stop.simps abc_lm_s.simps)
-done
+  done
 
 declare dec_inv_1.simps[simp del]
 
 declare inv_locate_n_b.simps [simp del]
-
-lemma inv_locate_n_b_Oc_via_at_begin_fst_bwtn[simp]:
-  "\<lbrakk>0 < abc_lm_v am n; 0 < n; 
-    at_begin_fst_bwtn (as, am) (n, aaa, Oc # xs) ires\<rbrakk>
- \<Longrightarrow> inv_locate_n_b (as, am) (n, Oc # aaa, xs) ires"
-apply(simp add: at_begin_fst_bwtn.simps inv_locate_n_b.simps )
-done
  
-lemma Suc_minus:"length am + tn = n
-       \<Longrightarrow> Suc tn = Suc n - length am "
-apply(arith)
-done
-
 lemma dec_first_on_right_moving_Oc_via_inv_locate_n_b[simp]:
  "\<lbrakk>inv_locate_n_b (as, am) (n, aaa, Oc # xs) ires\<rbrakk>
  \<Longrightarrow> dec_first_on_right_moving n (as, abc_lm_s am n (abc_lm_v am n))  
@@ -3037,10 +2843,6 @@
 apply(simp add: inv_check_left_moving.simps inv_check_left_moving_in_middle.simps)
 done
 
-lemma inv_check_left_moving_nonempty[simp]:
-  "inv_check_left_moving (as, lm) (s, [], Oc # list) ires = False"
-  by auto
-
 lemma inv_locate_n_b_Oc_via_at_begin_norm[simp]:
 "\<lbrakk>0 < abc_lm_v am n; 
   at_begin_norm (as, am) (n, aaa, Oc # xs) ires\<rbrakk>
@@ -3376,14 +3178,6 @@
     done
 qed
 
-lemma fetch_Nops[simp]: 
-  "\<lbrakk>ly = layout_of ap; tp = tm_of ap\<rbrakk> \<Longrightarrow>
-        fetch (tp @ [(Nop, 0), (Nop, 0)]) (start_of ly (length ap)) b = 
-       (Nop, 0)"
-apply(case_tac b)
-apply(simp_all add: start_of.simps fetch.simps nth_append)
-done
-
 lemma length_tp:
   "\<lbrakk>ly = layout_of ap; tp = tm_of ap\<rbrakk> \<Longrightarrow> 
   start_of ly (length ap) = Suc (length tp div 2)"
@@ -3511,7 +3305,7 @@
     by(rule_tac tm_append_first_steps_eq, simp_all add: crsp.simps)
   from b have d: "s' > 0 \<and> stpa \<ge> stp"
     by(simp add: crsp.simps)
-  then obtain diff where e: "stpa = stp + diff"   by (metis le_iff_add)
+  then obtain diff where e: "stpa = stp + diff" by (metis le_iff_add)
   obtain s'' l'' r'' where f:
     "steps (1, l, r) (tp @ shift (mopup n) off, 0) stp = (s'', l'', r'') \<and> is_final (s'', l'', r'')"
     using h