enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
authornipkow
Tue Sep 09 17:50:54 2014 +0200 (2014-09-09)
changeset 5824798d0f85d247f
parent 58245 7e54225acef1
child 58248 25af24e1f37b
enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
NEWS
src/HOL/Algebra/Divisibility.thy
src/HOL/Library/Multiset.thy
src/HOL/List.thy
src/HOL/ex/Gauge_Integration.thy
     1.1 --- a/NEWS	Mon Sep 08 23:09:37 2014 +0200
     1.2 +++ b/NEWS	Tue Sep 09 17:50:54 2014 +0200
     1.3 @@ -78,6 +78,8 @@
     1.4    - The 'smt2' method has been renamed 'smt'.
     1.5      INCOMPATIBILITY.
     1.6  
     1.7 +* List: renamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
     1.8 +
     1.9  
    1.10  *** ML ***
    1.11  
     2.1 --- a/src/HOL/Algebra/Divisibility.thy	Mon Sep 08 23:09:37 2014 +0200
     2.2 +++ b/src/HOL/Algebra/Divisibility.thy	Tue Sep 09 17:50:54 2014 +0200
     2.3 @@ -3412,7 +3412,7 @@
     2.4  
     2.5      from len
     2.6        have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"
     2.7 -      by (simp add: drop_Suc_conv_tl)
     2.8 +      by (simp add: Cons_nth_drop_Suc)
     2.9      with carr
    2.10        have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
    2.11        by simp
     3.1 --- a/src/HOL/Library/Multiset.thy	Mon Sep 08 23:09:37 2014 +0200
     3.2 +++ b/src/HOL/Library/Multiset.thy	Tue Sep 09 17:50:54 2014 +0200
     3.3 @@ -2296,7 +2296,7 @@
     3.4    def xsa \<equiv> "take j xs' @ drop (Suc j) xs'" 
     3.5    have "multiset_of xs' = {#x#} + multiset_of xsa"
     3.6      unfolding xsa_def using j_len nth_j
     3.7 -    by (metis (no_types) ab_semigroup_add_class.add_ac(1) append_take_drop_id drop_Suc_conv_tl
     3.8 +    by (metis (no_types) ab_semigroup_add_class.add_ac(1) append_take_drop_id Cons_nth_drop_Suc
     3.9        multiset_of.simps(2) union_code union_commute)
    3.10    hence ms_x: "multiset_of xsa = multiset_of xs"
    3.11      by (metis Cons.prems add.commute add_right_imp_eq multiset_of.simps(2))
    3.12 @@ -2307,7 +2307,7 @@
    3.13    def ys' \<equiv> "take j ysa @ y # drop j ysa"
    3.14    have xs': "xs' = take j xsa @ x # drop j xsa"
    3.15      using ms_x j_len nth_j Cons.prems xsa_def
    3.16 -    by (metis append_eq_append_conv append_take_drop_id diff_Suc_Suc drop_Suc_conv_tl length_Cons
    3.17 +    by (metis append_eq_append_conv append_take_drop_id diff_Suc_Suc Cons_nth_drop_Suc length_Cons
    3.18        length_drop mcard_multiset_of)
    3.19    have j_len': "j \<le> length xsa"
    3.20      using j_len xs' xsa_def
     4.1 --- a/src/HOL/List.thy	Mon Sep 08 23:09:37 2014 +0200
     4.2 +++ b/src/HOL/List.thy	Tue Sep 09 17:50:54 2014 +0200
     4.3 @@ -2009,7 +2009,7 @@
     4.4  apply (case_tac i, auto)
     4.5  done
     4.6  
     4.7 -lemma drop_Suc_conv_tl:
     4.8 +lemma Cons_nth_drop_Suc:
     4.9    "i < length xs \<Longrightarrow> (xs!i) # (drop (Suc i) xs) = drop i xs"
    4.10  apply (induct xs arbitrary: i, simp)
    4.11  apply (case_tac i, auto)
    4.12 @@ -2200,16 +2200,6 @@
    4.13    finally show ?thesis .
    4.14  qed
    4.15  
    4.16 -lemma nth_drop':
    4.17 -  "i < length xs \<Longrightarrow> xs ! i # drop (Suc i) xs = drop i xs"
    4.18 -apply (induct i arbitrary: xs)
    4.19 -apply (simp add: neq_Nil_conv)
    4.20 -apply (erule exE)+
    4.21 -apply simp
    4.22 -apply (case_tac xs)
    4.23 -apply simp_all
    4.24 -done
    4.25 -
    4.26  
    4.27  subsubsection {* @{const takeWhile} and @{const dropWhile} *}
    4.28  
    4.29 @@ -5264,9 +5254,9 @@
    4.30    apply (rule_tac x ="x ! i" in exI) 
    4.31    apply (rule_tac x ="y ! i" in exI, safe) 
    4.32    apply (rule_tac x="drop (Suc i) x" in exI)
    4.33 -  apply (drule sym, simp add: drop_Suc_conv_tl) 
    4.34 +  apply (drule sym, simp add: Cons_nth_drop_Suc) 
    4.35    apply (rule_tac x="drop (Suc i) y" in exI)
    4.36 -  by (simp add: drop_Suc_conv_tl) 
    4.37 +  by (simp add: Cons_nth_drop_Suc) 
    4.38  
    4.39  -- {* lexord is extension of partial ordering List.lex *} 
    4.40  lemma lexord_lex: "(x,y) \<in> lex r = ((x,y) \<in> lexord r \<and> length x = length y)"
     5.1 --- a/src/HOL/ex/Gauge_Integration.thy	Mon Sep 08 23:09:37 2014 +0200
     5.2 +++ b/src/HOL/ex/Gauge_Integration.thy	Tue Sep 09 17:50:54 2014 +0200
     5.3 @@ -436,7 +436,7 @@
     5.4      note rsum1 = I1[OF this]
     5.5  
     5.6      have drop_split: "drop N D = [D ! N] @ drop (Suc N) D"
     5.7 -      using nth_drop'[OF `N < length D`] by simp
     5.8 +      using Cons_nth_drop_Suc[OF `N < length D`] by simp
     5.9  
    5.10      have fine2: "fine \<delta>2 (e,c) (drop (Suc N) D)"
    5.11      proof (cases "drop (Suc N) D = []")
    5.12 @@ -472,7 +472,7 @@
    5.13      note rsum2 = I2[OF this]
    5.14  
    5.15      have "rsum D f = rsum (take N D) f + rsum [D ! N] f + rsum (drop (Suc N) D) f"
    5.16 -      using rsum_append[symmetric] nth_drop'[OF `N < length D`] by auto
    5.17 +      using rsum_append[symmetric] Cons_nth_drop_Suc[OF `N < length D`] by auto
    5.18      also have "\<dots> = rsum D1 f + rsum D2 f"
    5.19        by (cases "b = e", auto simp add: D1_def D2_def D_eq rsum_append algebra_simps)
    5.20      finally have "\<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>"