src/HOL/SetInterval.thy
changeset 15542 ee6cd48cf840
parent 15539 333a88244569
child 15554 03d4347b071d
     1.1 --- a/src/HOL/SetInterval.thy	Mon Feb 21 18:04:28 2005 +0100
     1.2 +++ b/src/HOL/SetInterval.thy	Mon Feb 21 19:23:46 2005 +0100
     1.3 @@ -534,6 +534,24 @@
     1.4  
     1.5  lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two
     1.6  
     1.7 +subsubsection {* Some Differences *}
     1.8 +
     1.9 +lemma ivl_diff[simp]:
    1.10 + "i \<le> n \<Longrightarrow> {i..<m} - {i..<n} = {n..<(m::'a::linorder)}"
    1.11 +by(auto)
    1.12 +
    1.13 +
    1.14 +subsubsection {* Some Subset Conditions *}
    1.15 +
    1.16 +lemma ivl_subset[simp]:
    1.17 + "({i..<j} \<subseteq> {m..<n}) = (j \<le> i | m \<le> i & j \<le> (n::'a::linorder))"
    1.18 +apply(auto simp:linorder_not_le)
    1.19 +apply(rule ccontr)
    1.20 +apply(insert linorder_le_less_linear[of i n])
    1.21 +apply(clarsimp simp:linorder_not_le)
    1.22 +apply(fastsimp)
    1.23 +done
    1.24 +
    1.25  
    1.26  subsection {* Summation indexed over intervals *}
    1.27  
    1.28 @@ -585,6 +603,17 @@
    1.29  not provide all lemmas available for @{term"{m..<n}"} also in the
    1.30  special form for @{term"{..<n}"}. *}
    1.31  
    1.32 +(* FIXME change the simplifier's treatment of congruence rules?? *)
    1.33 +
    1.34 +text{* This congruence rule should be used for sums over intervals as
    1.35 +the standard theorem @{text[source]setsum_cong} does not work well
    1.36 +with the simplifier who adds the unsimplified premise @{term"x:B"} to
    1.37 +the context. *}
    1.38 +
    1.39 +lemma setsum_ivl_cong:
    1.40 + "\<lbrakk>a = c; b = d; !!x. \<lbrakk> c \<le> x; x < d \<rbrakk> \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow>
    1.41 + setsum f {a..<b} = setsum g {c..<d}"
    1.42 +by(rule setsum_cong, simp_all)
    1.43  
    1.44  lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
    1.45  by (simp add:lessThan_Suc)