--- 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 ***
--- 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
--- 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
--- 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)"
--- 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>"