src/HOL/SetInterval.thy
changeset 16733 236dfafbeb63
parent 16102 c5f6726d9bb1
child 17149 e2b19c92ef51
     1.1 --- a/src/HOL/SetInterval.thy	Thu Jul 07 12:36:56 2005 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Thu Jul 07 12:39:17 2005 +0200
     1.3 @@ -300,6 +300,52 @@
     1.4  lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}"
     1.5  by (auto simp add: atLeastAtMost_def)
     1.6  
     1.7 +subsubsection {* Image *}
     1.8 +
     1.9 +lemma image_add_atLeastAtMost:
    1.10 +  "(%n::nat. n+k) ` {i..j} = {i+k..j+k}" (is "?A = ?B")
    1.11 +proof
    1.12 +  show "?A \<subseteq> ?B" by auto
    1.13 +next
    1.14 +  show "?B \<subseteq> ?A"
    1.15 +  proof
    1.16 +    fix n assume a: "n : ?B"
    1.17 +    hence "n - k : {i..j}" by auto arith+
    1.18 +    moreover have "n = (n - k) + k" using a by auto
    1.19 +    ultimately show "n : ?A" by blast
    1.20 +  qed
    1.21 +qed
    1.22 +
    1.23 +lemma image_add_atLeastLessThan:
    1.24 +  "(%n::nat. n+k) ` {i..<j} = {i+k..<j+k}" (is "?A = ?B")
    1.25 +proof
    1.26 +  show "?A \<subseteq> ?B" by auto
    1.27 +next
    1.28 +  show "?B \<subseteq> ?A"
    1.29 +  proof
    1.30 +    fix n assume a: "n : ?B"
    1.31 +    hence "n - k : {i..<j}" by auto arith+
    1.32 +    moreover have "n = (n - k) + k" using a by auto
    1.33 +    ultimately show "n : ?A" by blast
    1.34 +  qed
    1.35 +qed
    1.36 +
    1.37 +corollary image_Suc_atLeastAtMost[simp]:
    1.38 +  "Suc ` {i..j} = {Suc i..Suc j}"
    1.39 +using image_add_atLeastAtMost[where k=1] by simp
    1.40 +
    1.41 +corollary image_Suc_atLeastLessThan[simp]:
    1.42 +  "Suc ` {i..<j} = {Suc i..<Suc j}"
    1.43 +using image_add_atLeastLessThan[where k=1] by simp
    1.44 +
    1.45 +lemma image_add_int_atLeastLessThan:
    1.46 +    "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
    1.47 +  apply (auto simp add: image_def)
    1.48 +  apply (rule_tac x = "x - l" in bexI)
    1.49 +  apply auto
    1.50 +  done
    1.51 +
    1.52 +
    1.53  subsubsection {* Finiteness *}
    1.54  
    1.55  lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}"
    1.56 @@ -390,19 +436,12 @@
    1.57    apply auto
    1.58    done
    1.59  
    1.60 -lemma image_atLeastLessThan_int_shift:
    1.61 -    "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
    1.62 -  apply (auto simp add: image_def)
    1.63 -  apply (rule_tac x = "x - l" in bexI)
    1.64 -  apply auto
    1.65 -  done
    1.66 -
    1.67  lemma finite_atLeastLessThan_int [iff]: "finite {l..<u::int}"
    1.68    apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}")
    1.69    apply (erule subst)
    1.70    apply (rule finite_imageI)
    1.71    apply (rule finite_atLeastZeroLessThan_int)
    1.72 -  apply (rule image_atLeastLessThan_int_shift)
    1.73 +  apply (rule image_add_int_atLeastLessThan)
    1.74    done
    1.75  
    1.76  lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}"
    1.77 @@ -430,7 +469,7 @@
    1.78    apply (erule subst)
    1.79    apply (rule card_image)
    1.80    apply (simp add: inj_on_def)
    1.81 -  apply (rule image_atLeastLessThan_int_shift)
    1.82 +  apply (rule image_add_int_atLeastLessThan)
    1.83    done
    1.84  
    1.85  lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u - l + 1)"
    1.86 @@ -607,8 +646,6 @@
    1.87  not provide all lemmas available for @{term"{m..<n}"} also in the
    1.88  special form for @{term"{..<n}"}. *}
    1.89  
    1.90 -(* FIXME change the simplifier's treatment of congruence rules?? *)
    1.91 -
    1.92  text{* This congruence rule should be used for sums over intervals as
    1.93  the standard theorem @{text[source]setsum_cong} does not work well
    1.94  with the simplifier who adds the unsimplified premise @{term"x:B"} to
    1.95 @@ -652,10 +689,26 @@
    1.96  apply (simp add: add_ac)
    1.97  done
    1.98  
    1.99 +subsection{* Shifting bounds *}
   1.100 +
   1.101  lemma setsum_shift_bounds_nat_ivl:
   1.102    "setsum f {m+k..<n+k} = setsum (%i. f(i + k)){m..<n::nat}"
   1.103  by (induct "n", auto simp:atLeastLessThanSuc)
   1.104  
   1.105 +lemma setsum_shift_bounds_cl_nat_ivl:
   1.106 +  "setsum f {m+k..n+k} = setsum (%i. f(i + k)){m..n::nat}"
   1.107 +apply (insert setsum_reindex[OF inj_on_add_nat, where h=f and B = "{m..n}"])
   1.108 +apply (simp add:image_add_atLeastAtMost o_def)
   1.109 +done
   1.110 +
   1.111 +corollary setsum_shift_bounds_cl_Suc_ivl:
   1.112 +  "setsum f {Suc m..Suc n} = setsum (%i. f(Suc i)){m..n}"
   1.113 +by (simp add:setsum_shift_bounds_cl_nat_ivl[where k=1,simplified])
   1.114 +
   1.115 +corollary setsum_shift_bounds_Suc_ivl:
   1.116 +  "setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}"
   1.117 +by (simp add:setsum_shift_bounds_nat_ivl[where k=1,simplified])
   1.118 +
   1.119  
   1.120  ML
   1.121  {*