diff -r 6e1c03614d36 -r 93db7414931d thys/Recursive.thy
--- a/thys/Recursive.thy	Fri Dec 21 12:31:36 2018 +0100
+++ b/thys/Recursive.thy	Fri Dec 21 15:30:24 2018 +0100
@@ -170,33 +170,26 @@
 
 declare addition_inv.simps[simp del]
 
+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 addition_inv_init: 
   "\<lbrakk>m \<noteq> n; max m n < p; length lm > p; lm ! p = 0\<rbrakk> \<Longrightarrow>
                                    addition_inv (0, lm) m n p lm"
-apply(simp add: addition_inv.simps Let_def)
+apply(simp add: addition_inv.simps Let_def )
 apply(rule_tac x = "lm ! m" in exI, simp)
 done
 
-lemma abs_fetch_0[simp]: "abc_fetch 0 (addition m n p) = Some (Dec m 4)"
-by(simp add: abc_fetch.simps addition.simps)
-
-lemma abs_fetch_1[simp]: "abc_fetch (Suc 0) (addition m n p) = Some (Inc n)"
-by(simp add: abc_fetch.simps addition.simps)
-
-lemma abs_fetch_2[simp]: "abc_fetch 2 (addition m n p) = Some (Inc p)"
-by(simp add: abc_fetch.simps addition.simps)
-
-lemma abs_fetch_3[simp]: "abc_fetch 3 (addition m n p) = Some (Goto 0)"
-by(simp add: abc_fetch.simps addition.simps)
-
-lemma abs_fetch_4[simp]: "abc_fetch 4 (addition m n p) = Some (Dec p 7)"
-by(simp add: abc_fetch.simps addition.simps)
-
-lemma abs_fetch_5[simp]: "abc_fetch 5 (addition m n p) = Some (Inc m)"
-by(simp add: abc_fetch.simps addition.simps)
-
-lemma abs_fetch_6[simp]: "abc_fetch 6 (addition m n p) = Some (Goto 4)"
-by(simp add: abc_fetch.simps addition.simps)
+lemma abs_fetch[simp]:
+  "abc_fetch 0 (addition m n p) = Some (Dec m 4)"
+  "abc_fetch (Suc 0) (addition m n p) = Some (Inc n)"
+  "abc_fetch 2 (addition m n p) = Some (Inc p)"
+  "abc_fetch 3 (addition m n p) = Some (Goto 0)"
+  "abc_fetch 4 (addition m n p) = Some (Dec p 7)"
+  "abc_fetch 5 (addition m n p) = Some (Inc m)"
+  "abc_fetch 6 (addition m n p) = Some (Goto 4)"
+by(simp_all add: abc_fetch.simps addition.simps)
 
 lemma exists_small_list_elem1[simp]:
   "\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p; x \<le> lm ! m; 0 < x\<rbrakk>
@@ -288,7 +281,7 @@
                      abc_step_l.simps addition_inv.simps 
                      abc_lm_v.simps abc_lm_s.simps nth_append
                 split: if_splits)
-apply(rule_tac [!] x = x in exI, simp_all add: list_update_overwrite Suc_diff_Suc)
+apply(rule_tac [!] x = x in exI, simp_all add: list_update_overwrite Suc_diff_Suc )
 by (metis list_update_overwrite list_update_swap nat_neq_iff)
 
 lemma  addition_correct': 
@@ -479,21 +472,12 @@
       rule_tac x = "initlm ! n" in exI, simp)
 done
 
-lemma abc_fetch_0[simp]: "abc_fetch 0 (mv_box m n) = Some (Dec m 3)"
-apply(simp add: mv_box.simps abc_fetch.simps)
-done
-
-lemma abc_fetch_1[simp]: "abc_fetch (Suc 0) (mv_box m n) =
-               Some (Inc n)"
-apply(simp add: mv_box.simps abc_fetch.simps)
-done
-
-lemma abc_fetch_2[simp]: "abc_fetch 2 (mv_box m n) = Some (Goto 0)"
-apply(simp add: mv_box.simps abc_fetch.simps)
-done
-
-lemma abc_fetch_3[simp]: "abc_fetch 3 (mv_box m n) = None"
-apply(simp add: mv_box.simps abc_fetch.simps)
+lemma abc_fetch[simp]:
+  "abc_fetch 0 (mv_box m n) = Some (Dec m 3)"
+  "abc_fetch (Suc 0) (mv_box m n) = Some (Inc n)"
+  "abc_fetch 2 (mv_box m n) = Some (Goto 0)"
+  "abc_fetch 3 (mv_box m n) = None"
+apply(simp_all add: mv_box.simps abc_fetch.simps)
 done
 
 lemma replicate_Suc_iff_anywhere: "x # x\<up>b @ ys = x\<up>(Suc b) @ ys"
@@ -2584,7 +2568,7 @@
 apply(arith)
 apply(case_tac "Suc k = length ap", simp)
 apply(rule_tac start_of_less, simp)
-apply(auto simp: tinc_b_def shift.simps start_of_suc_inc length_of.simps startof_not0)
+apply(auto simp: tinc_b_def shift.simps start_of_suc_inc length_of.simps )
 done
 
 lemma findnth_le[elim]: 
@@ -2607,7 +2591,7 @@
 apply(rule_tac start_of_less, simp)
 apply(subgoal_tac "b \<le> start_of (layout_of ap) k + 2*n + 1 \<and> 
      start_of (layout_of ap) k + 2*n + 1 \<le>  start_of (layout_of ap) (Suc k)", auto)
-apply(auto simp: tinc_b_def shift.simps length_of.simps startof_not0 start_of_suc_inc)
+apply(auto simp: tinc_b_def shift.simps length_of.simps  start_of_suc_inc)
 done
 
 lemma start_of_eq: "length ap < as \<Longrightarrow> start_of (layout_of ap) as = start_of (layout_of ap) (length ap)"
@@ -2646,7 +2630,7 @@
 prefer 2
 apply(subgoal_tac "start_of (layout_of ap) (Suc k) = start_of (layout_of ap) k + 2*n + 16
                  \<and> start_of (layout_of ap) (Suc k) \<le> start_of (layout_of ap) (length ap)")
-apply(simp add: startof_not0, rule_tac conjI)
+apply(simp, rule_tac conjI)
 apply(simp add: start_of_suc_dec)
 apply(rule_tac start_of_all_le)
 apply(auto simp: tdec_b_def shift.simps)
@@ -2795,6 +2779,4 @@
     by simp
 qed
 
-unused_thms
-
 end
\ No newline at end of file