src/HOL/SetInterval.thy
changeset 30079 293b896b9c25
parent 29960 9d5c6f376768
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/SetInterval.thy	Mon Feb 23 13:55:36 2009 -0800
     1.2 +++ b/src/HOL/SetInterval.thy	Mon Feb 23 16:25:52 2009 -0800
     1.3 @@ -352,11 +352,11 @@
     1.4  
     1.5  corollary image_Suc_atLeastAtMost[simp]:
     1.6    "Suc ` {i..j} = {Suc i..Suc j}"
     1.7 -using image_add_atLeastAtMost[where k=1] by simp
     1.8 +using image_add_atLeastAtMost[where k="Suc 0"] by simp
     1.9  
    1.10  corollary image_Suc_atLeastLessThan[simp]:
    1.11    "Suc ` {i..<j} = {Suc i..<Suc j}"
    1.12 -using image_add_atLeastLessThan[where k=1] by simp
    1.13 +using image_add_atLeastLessThan[where k="Suc 0"] by simp
    1.14  
    1.15  lemma image_add_int_atLeastLessThan:
    1.16      "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
    1.17 @@ -556,7 +556,7 @@
    1.18  qed
    1.19  
    1.20  lemma card_less_Suc2: "0 \<notin> M \<Longrightarrow> card {k. Suc k \<in> M \<and> k < i} = card {k \<in> M. k < Suc i}"
    1.21 -apply (rule card_bij_eq [of "Suc" _ _ "\<lambda>x. x - 1"])
    1.22 +apply (rule card_bij_eq [of "Suc" _ _ "\<lambda>x. x - Suc 0"])
    1.23  apply simp
    1.24  apply fastsimp
    1.25  apply auto
    1.26 @@ -803,7 +803,7 @@
    1.27  
    1.28  lemma setsum_head_upt_Suc:
    1.29    "m < n \<Longrightarrow> setsum f {m..<n} = f m + setsum f {Suc m..<n}"
    1.30 -apply(insert setsum_head_Suc[of m "n - 1" f])
    1.31 +apply(insert setsum_head_Suc[of m "n - Suc 0" f])
    1.32  apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps)
    1.33  done
    1.34  
    1.35 @@ -835,11 +835,11 @@
    1.36  
    1.37  corollary setsum_shift_bounds_cl_Suc_ivl:
    1.38    "setsum f {Suc m..Suc n} = setsum (%i. f(Suc i)){m..n}"
    1.39 -by (simp add:setsum_shift_bounds_cl_nat_ivl[where k=1,simplified])
    1.40 +by (simp add:setsum_shift_bounds_cl_nat_ivl[where k="Suc 0", simplified])
    1.41  
    1.42  corollary setsum_shift_bounds_Suc_ivl:
    1.43    "setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}"
    1.44 -by (simp add:setsum_shift_bounds_nat_ivl[where k=1,simplified])
    1.45 +by (simp add:setsum_shift_bounds_nat_ivl[where k="Suc 0", simplified])
    1.46  
    1.47  lemma setsum_shift_lb_Suc0_0:
    1.48    "f(0::nat) = (0::nat) \<Longrightarrow> setsum f {Suc 0..k} = setsum f {0..k}"
    1.49 @@ -883,6 +883,7 @@
    1.50      by (rule setsum_addf)
    1.51    also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp
    1.52    also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))"
    1.53 +    unfolding One_nat_def
    1.54      by (simp add: setsum_right_distrib atLeast0LessThan[symmetric] setsum_shift_lb_Suc0_0_upt mult_ac)
    1.55    also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)"
    1.56      by (simp add: left_distrib right_distrib)
    1.57 @@ -890,7 +891,7 @@
    1.58      by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)
    1.59    also from ngt1
    1.60    have "(1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..n - 1}. ?I i) = ((1+1)*?n*a + d*?I (n - 1)*?I n)"
    1.61 -    by (simp only: mult_ac gauss_sum [of "n - 1"])
    1.62 +    by (simp only: mult_ac gauss_sum [of "n - 1"], unfold One_nat_def)
    1.63         (simp add:  mult_ac trans [OF add_commute of_nat_Suc [symmetric]])
    1.64    finally show ?thesis by (simp add: algebra_simps)
    1.65  next
    1.66 @@ -906,7 +907,8 @@
    1.67      "((1::nat) + 1) * (\<Sum>i\<in>{..<n::nat}. a + of_nat(i)*d) =
    1.68      of_nat(n) * (a + (a + of_nat(n - 1)*d))"
    1.69      by (rule arith_series_general)
    1.70 -  thus ?thesis by (auto simp add: of_nat_id)
    1.71 +  thus ?thesis
    1.72 +    unfolding One_nat_def by (auto simp add: of_nat_id)
    1.73  qed
    1.74  
    1.75  lemma arith_series_int: