# HG changeset patch
# User nipkow
# Date 1410277854 -7200
# Node ID 98d0f85d247f0dac82f4157409ebced0bbab84c8
# Parent  7e54225acef1f929714e1a3f187f80872381a532
enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc

diff -r 7e54225acef1 -r 98d0f85d247f NEWS
--- a/NEWS	Mon Sep 08 23:09:37 2014 +0200
+++ b/NEWS	Tue Sep 09 17:50:54 2014 +0200
@@ -78,6 +78,8 @@
   - The 'smt2' method has been renamed 'smt'.
     INCOMPATIBILITY.
 
+* List: renamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
+
 
 *** ML ***
 
diff -r 7e54225acef1 -r 98d0f85d247f src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Mon Sep 08 23:09:37 2014 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Tue Sep 09 17:50:54 2014 +0200
@@ -3412,7 +3412,7 @@
 
     from len
       have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"
-      by (simp add: drop_Suc_conv_tl)
+      by (simp add: Cons_nth_drop_Suc)
     with carr
       have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
       by simp
diff -r 7e54225acef1 -r 98d0f85d247f src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Sep 08 23:09:37 2014 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue Sep 09 17:50:54 2014 +0200
@@ -2296,7 +2296,7 @@
   def xsa \<equiv> "take j xs' @ drop (Suc j) xs'" 
   have "multiset_of xs' = {#x#} + multiset_of xsa"
     unfolding xsa_def using j_len nth_j
-    by (metis (no_types) ab_semigroup_add_class.add_ac(1) append_take_drop_id drop_Suc_conv_tl
+    by (metis (no_types) ab_semigroup_add_class.add_ac(1) append_take_drop_id Cons_nth_drop_Suc
       multiset_of.simps(2) union_code union_commute)
   hence ms_x: "multiset_of xsa = multiset_of xs"
     by (metis Cons.prems add.commute add_right_imp_eq multiset_of.simps(2))
@@ -2307,7 +2307,7 @@
   def ys' \<equiv> "take j ysa @ y # drop j ysa"
   have xs': "xs' = take j xsa @ x # drop j xsa"
     using ms_x j_len nth_j Cons.prems xsa_def
-    by (metis append_eq_append_conv append_take_drop_id diff_Suc_Suc drop_Suc_conv_tl length_Cons
+    by (metis append_eq_append_conv append_take_drop_id diff_Suc_Suc Cons_nth_drop_Suc length_Cons
       length_drop mcard_multiset_of)
   have j_len': "j \<le> length xsa"
     using j_len xs' xsa_def
diff -r 7e54225acef1 -r 98d0f85d247f src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Sep 08 23:09:37 2014 +0200
+++ b/src/HOL/List.thy	Tue Sep 09 17:50:54 2014 +0200
@@ -2009,7 +2009,7 @@
 apply (case_tac i, auto)
 done
 
-lemma drop_Suc_conv_tl:
+lemma Cons_nth_drop_Suc:
   "i < length xs \<Longrightarrow> (xs!i) # (drop (Suc i) xs) = drop i xs"
 apply (induct xs arbitrary: i, simp)
 apply (case_tac i, auto)
@@ -2200,16 +2200,6 @@
   finally show ?thesis .
 qed
 
-lemma nth_drop':
-  "i < length xs \<Longrightarrow> xs ! i # drop (Suc i) xs = drop i xs"
-apply (induct i arbitrary: xs)
-apply (simp add: neq_Nil_conv)
-apply (erule exE)+
-apply simp
-apply (case_tac xs)
-apply simp_all
-done
-
 
 subsubsection {* @{const takeWhile} and @{const dropWhile} *}
 
@@ -5264,9 +5254,9 @@
   apply (rule_tac x ="x ! i" in exI) 
   apply (rule_tac x ="y ! i" in exI, safe) 
   apply (rule_tac x="drop (Suc i) x" in exI)
-  apply (drule sym, simp add: drop_Suc_conv_tl) 
+  apply (drule sym, simp add: Cons_nth_drop_Suc) 
   apply (rule_tac x="drop (Suc i) y" in exI)
-  by (simp add: drop_Suc_conv_tl) 
+  by (simp add: Cons_nth_drop_Suc) 
 
 -- {* lexord is extension of partial ordering List.lex *} 
 lemma lexord_lex: "(x,y) \<in> lex r = ((x,y) \<in> lexord r \<and> length x = length y)"
diff -r 7e54225acef1 -r 98d0f85d247f src/HOL/ex/Gauge_Integration.thy
--- a/src/HOL/ex/Gauge_Integration.thy	Mon Sep 08 23:09:37 2014 +0200
+++ b/src/HOL/ex/Gauge_Integration.thy	Tue Sep 09 17:50:54 2014 +0200
@@ -436,7 +436,7 @@
     note rsum1 = I1[OF this]
 
     have drop_split: "drop N D = [D ! N] @ drop (Suc N) D"
-      using nth_drop'[OF `N < length D`] by simp
+      using Cons_nth_drop_Suc[OF `N < length D`] by simp
 
     have fine2: "fine \<delta>2 (e,c) (drop (Suc N) D)"
     proof (cases "drop (Suc N) D = []")
@@ -472,7 +472,7 @@
     note rsum2 = I2[OF this]
 
     have "rsum D f = rsum (take N D) f + rsum [D ! N] f + rsum (drop (Suc N) D) f"
-      using rsum_append[symmetric] nth_drop'[OF `N < length D`] by auto
+      using rsum_append[symmetric] Cons_nth_drop_Suc[OF `N < length D`] by auto
     also have "\<dots> = rsum D1 f + rsum D2 f"
       by (cases "b = e", auto simp add: D1_def D2_def D_eq rsum_append algebra_simps)
     finally have "\<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>"