src/HOL/Set_Interval.thy
 changeset 47317 432b29a96f61 parent 47222 1b7c909a6fad child 47988 e4b69e10b990
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Set_Interval.thy	Tue Apr 03 15:15:00 2012 +0200
1.3 @@ -0,0 +1,1439 @@
1.4 +(*  Title:      HOL/Set_Interval.thy
1.5 +    Author:     Tobias Nipkow
1.6 +    Author:     Clemens Ballarin
1.7 +    Author:     Jeremy Avigad
1.8 +
1.9 +lessThan, greaterThan, atLeast, atMost and two-sided intervals
1.10 +*)
1.11 +
1.12 +header {* Set intervals *}
1.13 +
1.14 +theory Set_Interval
1.15 +imports Int Nat_Transfer
1.16 +begin
1.17 +
1.18 +context ord
1.19 +begin
1.20 +
1.21 +definition
1.22 +  lessThan    :: "'a => 'a set" ("(1{..<_})") where
1.23 +  "{..<u} == {x. x < u}"
1.24 +
1.25 +definition
1.26 +  atMost      :: "'a => 'a set" ("(1{.._})") where
1.27 +  "{..u} == {x. x \<le> u}"
1.28 +
1.29 +definition
1.30 +  greaterThan :: "'a => 'a set" ("(1{_<..})") where
1.31 +  "{l<..} == {x. l<x}"
1.32 +
1.33 +definition
1.34 +  atLeast     :: "'a => 'a set" ("(1{_..})") where
1.35 +  "{l..} == {x. l\<le>x}"
1.36 +
1.37 +definition
1.38 +  greaterThanLessThan :: "'a => 'a => 'a set"  ("(1{_<..<_})") where
1.39 +  "{l<..<u} == {l<..} Int {..<u}"
1.40 +
1.41 +definition
1.42 +  atLeastLessThan :: "'a => 'a => 'a set"      ("(1{_..<_})") where
1.43 +  "{l..<u} == {l..} Int {..<u}"
1.44 +
1.45 +definition
1.46 +  greaterThanAtMost :: "'a => 'a => 'a set"    ("(1{_<.._})") where
1.47 +  "{l<..u} == {l<..} Int {..u}"
1.48 +
1.49 +definition
1.50 +  atLeastAtMost :: "'a => 'a => 'a set"        ("(1{_.._})") where
1.51 +  "{l..u} == {l..} Int {..u}"
1.52 +
1.53 +end
1.54 +
1.55 +
1.56 +text{* A note of warning when using @{term"{..<n}"} on type @{typ
1.57 +nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving
1.58 +@{term"{m..<n}"} may not exist in @{term"{..<n}"}-form as well. *}
1.59 +
1.60 +syntax
1.61 +  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3UN _<=_./ _)" [0, 0, 10] 10)
1.62 +  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3UN _<_./ _)" [0, 0, 10] 10)
1.63 +  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3INT _<=_./ _)" [0, 0, 10] 10)
1.64 +  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3INT _<_./ _)" [0, 0, 10] 10)
1.65 +
1.66 +syntax (xsymbols)
1.67 +  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _\<le>_./ _)" [0, 0, 10] 10)
1.68 +  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _<_./ _)" [0, 0, 10] 10)
1.69 +  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _\<le>_./ _)" [0, 0, 10] 10)
1.70 +  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" [0, 0, 10] 10)
1.71 +
1.72 +syntax (latex output)
1.73 +  "_UNION_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ \<le> _)/ _)" [0, 0, 10] 10)
1.74 +  "_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ < _)/ _)" [0, 0, 10] 10)
1.75 +  "_INTER_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ \<le> _)/ _)" [0, 0, 10] 10)
1.76 +  "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ < _)/ _)" [0, 0, 10] 10)
1.77 +
1.78 +translations
1.79 +  "UN i<=n. A"  == "UN i:{..n}. A"
1.80 +  "UN i<n. A"   == "UN i:{..<n}. A"
1.81 +  "INT i<=n. A" == "INT i:{..n}. A"
1.82 +  "INT i<n. A"  == "INT i:{..<n}. A"
1.83 +
1.84 +
1.85 +subsection {* Various equivalences *}
1.86 +
1.87 +lemma (in ord) lessThan_iff [iff]: "(i: lessThan k) = (i<k)"
1.88 +by (simp add: lessThan_def)
1.89 +
1.90 +lemma Compl_lessThan [simp]:
1.91 +    "!!k:: 'a::linorder. -lessThan k = atLeast k"
1.92 +apply (auto simp add: lessThan_def atLeast_def)
1.93 +done
1.94 +
1.95 +lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k} - lessThan k = {k}"
1.96 +by auto
1.97 +
1.98 +lemma (in ord) greaterThan_iff [iff]: "(i: greaterThan k) = (k<i)"
1.99 +by (simp add: greaterThan_def)
1.100 +
1.101 +lemma Compl_greaterThan [simp]:
1.102 +    "!!k:: 'a::linorder. -greaterThan k = atMost k"
1.103 +  by (auto simp add: greaterThan_def atMost_def)
1.104 +
1.105 +lemma Compl_atMost [simp]: "!!k:: 'a::linorder. -atMost k = greaterThan k"
1.106 +apply (subst Compl_greaterThan [symmetric])
1.107 +apply (rule double_complement)
1.108 +done
1.109 +
1.110 +lemma (in ord) atLeast_iff [iff]: "(i: atLeast k) = (k<=i)"
1.111 +by (simp add: atLeast_def)
1.112 +
1.113 +lemma Compl_atLeast [simp]:
1.114 +    "!!k:: 'a::linorder. -atLeast k = lessThan k"
1.115 +  by (auto simp add: lessThan_def atLeast_def)
1.116 +
1.117 +lemma (in ord) atMost_iff [iff]: "(i: atMost k) = (i<=k)"
1.118 +by (simp add: atMost_def)
1.119 +
1.120 +lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"
1.121 +by (blast intro: order_antisym)
1.122 +
1.123 +
1.124 +subsection {* Logical Equivalences for Set Inclusion and Equality *}
1.125 +
1.126 +lemma atLeast_subset_iff [iff]:
1.127 +     "(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))"
1.128 +by (blast intro: order_trans)
1.129 +
1.130 +lemma atLeast_eq_iff [iff]:
1.131 +     "(atLeast x = atLeast y) = (x = (y::'a::linorder))"
1.132 +by (blast intro: order_antisym order_trans)
1.133 +
1.134 +lemma greaterThan_subset_iff [iff]:
1.135 +     "(greaterThan x \<subseteq> greaterThan y) = (y \<le> (x::'a::linorder))"
1.136 +apply (auto simp add: greaterThan_def)
1.137 + apply (subst linorder_not_less [symmetric], blast)
1.138 +done
1.139 +
1.140 +lemma greaterThan_eq_iff [iff]:
1.141 +     "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))"
1.142 +apply (rule iffI)
1.143 + apply (erule equalityE)
1.144 + apply simp_all
1.145 +done
1.146 +
1.147 +lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))"
1.148 +by (blast intro: order_trans)
1.149 +
1.150 +lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))"
1.151 +by (blast intro: order_antisym order_trans)
1.152 +
1.153 +lemma lessThan_subset_iff [iff]:
1.154 +     "(lessThan x \<subseteq> lessThan y) = (x \<le> (y::'a::linorder))"
1.155 +apply (auto simp add: lessThan_def)
1.156 + apply (subst linorder_not_less [symmetric], blast)
1.157 +done
1.158 +
1.159 +lemma lessThan_eq_iff [iff]:
1.160 +     "(lessThan x = lessThan y) = (x = (y::'a::linorder))"
1.161 +apply (rule iffI)
1.162 + apply (erule equalityE)
1.163 + apply simp_all
1.164 +done
1.165 +
1.166 +lemma lessThan_strict_subset_iff:
1.167 +  fixes m n :: "'a::linorder"
1.168 +  shows "{..<m} < {..<n} \<longleftrightarrow> m < n"
1.169 +  by (metis leD lessThan_subset_iff linorder_linear not_less_iff_gr_or_eq psubset_eq)
1.170 +
1.171 +subsection {*Two-sided intervals*}
1.172 +
1.173 +context ord
1.174 +begin
1.175 +
1.176 +lemma greaterThanLessThan_iff [simp,no_atp]:
1.177 +  "(i : {l<..<u}) = (l < i & i < u)"
1.178 +by (simp add: greaterThanLessThan_def)
1.179 +
1.180 +lemma atLeastLessThan_iff [simp,no_atp]:
1.181 +  "(i : {l..<u}) = (l <= i & i < u)"
1.182 +by (simp add: atLeastLessThan_def)
1.183 +
1.184 +lemma greaterThanAtMost_iff [simp,no_atp]:
1.185 +  "(i : {l<..u}) = (l < i & i <= u)"
1.186 +by (simp add: greaterThanAtMost_def)
1.187 +
1.188 +lemma atLeastAtMost_iff [simp,no_atp]:
1.189 +  "(i : {l..u}) = (l <= i & i <= u)"
1.190 +by (simp add: atLeastAtMost_def)
1.191 +
1.192 +text {* The above four lemmas could be declared as iffs. Unfortunately this
1.193 +breaks many proofs. Since it only helps blast, it is better to leave well
1.194 +alone *}
1.195 +
1.196 +end
1.197 +
1.198 +subsubsection{* Emptyness, singletons, subset *}
1.199 +
1.200 +context order
1.201 +begin
1.202 +
1.203 +lemma atLeastatMost_empty[simp]:
1.204 +  "b < a \<Longrightarrow> {a..b} = {}"
1.205 +by(auto simp: atLeastAtMost_def atLeast_def atMost_def)
1.206 +
1.207 +lemma atLeastatMost_empty_iff[simp]:
1.208 +  "{a..b} = {} \<longleftrightarrow> (~ a <= b)"
1.209 +by auto (blast intro: order_trans)
1.210 +
1.211 +lemma atLeastatMost_empty_iff2[simp]:
1.212 +  "{} = {a..b} \<longleftrightarrow> (~ a <= b)"
1.213 +by auto (blast intro: order_trans)
1.214 +
1.215 +lemma atLeastLessThan_empty[simp]:
1.216 +  "b <= a \<Longrightarrow> {a..<b} = {}"
1.217 +by(auto simp: atLeastLessThan_def)
1.218 +
1.219 +lemma atLeastLessThan_empty_iff[simp]:
1.220 +  "{a..<b} = {} \<longleftrightarrow> (~ a < b)"
1.221 +by auto (blast intro: le_less_trans)
1.222 +
1.223 +lemma atLeastLessThan_empty_iff2[simp]:
1.224 +  "{} = {a..<b} \<longleftrightarrow> (~ a < b)"
1.225 +by auto (blast intro: le_less_trans)
1.226 +
1.227 +lemma greaterThanAtMost_empty[simp]: "l \<le> k ==> {k<..l} = {}"
1.228 +by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)
1.229 +
1.230 +lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \<longleftrightarrow> ~ k < l"
1.231 +by auto (blast intro: less_le_trans)
1.232 +
1.233 +lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \<longleftrightarrow> ~ k < l"
1.234 +by auto (blast intro: less_le_trans)
1.235 +
1.236 +lemma greaterThanLessThan_empty[simp]:"l \<le> k ==> {k<..<l} = {}"
1.237 +by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def)
1.238 +
1.239 +lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}"
1.240 +by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)
1.241 +
1.242 +lemma atLeastAtMost_singleton': "a = b \<Longrightarrow> {a .. b} = {a}" by simp
1.243 +
1.244 +lemma atLeastatMost_subset_iff[simp]:
1.245 +  "{a..b} <= {c..d} \<longleftrightarrow> (~ a <= b) | c <= a & b <= d"
1.246 +unfolding atLeastAtMost_def atLeast_def atMost_def
1.247 +by (blast intro: order_trans)
1.248 +
1.249 +lemma atLeastatMost_psubset_iff:
1.250 +  "{a..b} < {c..d} \<longleftrightarrow>
1.251 +   ((~ a <= b) | c <= a & b <= d & (c < a | b < d))  &  c <= d"
1.252 +by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans)
1.253 +
1.254 +lemma atLeastAtMost_singleton_iff[simp]:
1.255 +  "{a .. b} = {c} \<longleftrightarrow> a = b \<and> b = c"
1.256 +proof
1.257 +  assume "{a..b} = {c}"
1.258 +  hence "\<not> (\<not> a \<le> b)" unfolding atLeastatMost_empty_iff[symmetric] by simp
1.259 +  moreover with {a..b} = {c} have "c \<le> a \<and> b \<le> c" by auto
1.260 +  ultimately show "a = b \<and> b = c" by auto
1.261 +qed simp
1.262 +
1.263 +end
1.264 +
1.265 +context dense_linorder
1.266 +begin
1.267 +
1.268 +lemma greaterThanLessThan_empty_iff[simp]:
1.269 +  "{ a <..< b } = {} \<longleftrightarrow> b \<le> a"
1.270 +  using dense[of a b] by (cases "a < b") auto
1.271 +
1.272 +lemma greaterThanLessThan_empty_iff2[simp]:
1.273 +  "{} = { a <..< b } \<longleftrightarrow> b \<le> a"
1.274 +  using dense[of a b] by (cases "a < b") auto
1.275 +
1.276 +lemma atLeastLessThan_subseteq_atLeastAtMost_iff:
1.277 +  "{a ..< b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)"
1.278 +  using dense[of "max a d" "b"]
1.279 +  by (force simp: subset_eq Ball_def not_less[symmetric])
1.280 +
1.281 +lemma greaterThanAtMost_subseteq_atLeastAtMost_iff:
1.282 +  "{a <.. b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)"
1.283 +  using dense[of "a" "min c b"]
1.284 +  by (force simp: subset_eq Ball_def not_less[symmetric])
1.285 +
1.286 +lemma greaterThanLessThan_subseteq_atLeastAtMost_iff:
1.287 +  "{a <..< b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)"
1.288 +  using dense[of "a" "min c b"] dense[of "max a d" "b"]
1.289 +  by (force simp: subset_eq Ball_def not_less[symmetric])
1.290 +
1.291 +lemma atLeastAtMost_subseteq_atLeastLessThan_iff:
1.292 +  "{a .. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a \<le> b \<longrightarrow> c \<le> a \<and> b < d)"
1.293 +  using dense[of "max a d" "b"]
1.294 +  by (force simp: subset_eq Ball_def not_less[symmetric])
1.295 +
1.296 +lemma greaterThanAtMost_subseteq_atLeastLessThan_iff:
1.297 +  "{a <.. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b < d)"
1.298 +  using dense[of "a" "min c b"]
1.299 +  by (force simp: subset_eq Ball_def not_less[symmetric])
1.300 +
1.301 +lemma greaterThanLessThan_subseteq_atLeastLessThan_iff:
1.302 +  "{a <..< b} \<subseteq> { c ..< d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)"
1.303 +  using dense[of "a" "min c b"] dense[of "max a d" "b"]
1.304 +  by (force simp: subset_eq Ball_def not_less[symmetric])
1.305 +
1.306 +end
1.307 +
1.308 +lemma (in linorder) atLeastLessThan_subset_iff:
1.309 +  "{a..<b} <= {c..<d} \<Longrightarrow> b <= a | c<=a & b<=d"
1.310 +apply (auto simp:subset_eq Ball_def)
1.311 +apply(frule_tac x=a in spec)
1.312 +apply(erule_tac x=d in allE)
1.313 +apply (simp add: less_imp_le)
1.314 +done
1.315 +
1.316 +lemma atLeastLessThan_inj:
1.317 +  fixes a b c d :: "'a::linorder"
1.318 +  assumes eq: "{a ..< b} = {c ..< d}" and "a < b" "c < d"
1.319 +  shows "a = c" "b = d"
1.320 +using assms by (metis atLeastLessThan_subset_iff eq less_le_not_le linorder_antisym_conv2 subset_refl)+
1.321 +
1.322 +lemma atLeastLessThan_eq_iff:
1.323 +  fixes a b c d :: "'a::linorder"
1.324 +  assumes "a < b" "c < d"
1.325 +  shows "{a ..< b} = {c ..< d} \<longleftrightarrow> a = c \<and> b = d"
1.326 +  using atLeastLessThan_inj assms by auto
1.327 +
1.328 +subsubsection {* Intersection *}
1.329 +
1.330 +context linorder
1.331 +begin
1.332 +
1.333 +lemma Int_atLeastAtMost[simp]: "{a..b} Int {c..d} = {max a c .. min b d}"
1.334 +by auto
1.335 +
1.336 +lemma Int_atLeastAtMostR1[simp]: "{..b} Int {c..d} = {c .. min b d}"
1.337 +by auto
1.338 +
1.339 +lemma Int_atLeastAtMostR2[simp]: "{a..} Int {c..d} = {max a c .. d}"
1.340 +by auto
1.341 +
1.342 +lemma Int_atLeastAtMostL1[simp]: "{a..b} Int {..d} = {a .. min b d}"
1.343 +by auto
1.344 +
1.345 +lemma Int_atLeastAtMostL2[simp]: "{a..b} Int {c..} = {max a c .. b}"
1.346 +by auto
1.347 +
1.348 +lemma Int_atLeastLessThan[simp]: "{a..<b} Int {c..<d} = {max a c ..< min b d}"
1.349 +by auto
1.350 +
1.351 +lemma Int_greaterThanAtMost[simp]: "{a<..b} Int {c<..d} = {max a c <.. min b d}"
1.352 +by auto
1.353 +
1.354 +lemma Int_greaterThanLessThan[simp]: "{a<..<b} Int {c<..<d} = {max a c <..< min b d}"
1.355 +by auto
1.356 +
1.357 +end
1.358 +
1.359 +
1.360 +subsection {* Intervals of natural numbers *}
1.361 +
1.362 +subsubsection {* The Constant @{term lessThan} *}
1.363 +
1.364 +lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"
1.365 +by (simp add: lessThan_def)
1.366 +
1.367 +lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"
1.368 +by (simp add: lessThan_def less_Suc_eq, blast)
1.369 +
1.370 +text {* The following proof is convenient in induction proofs where
1.371 +new elements get indices at the beginning. So it is used to transform
1.372 +@{term "{..<Suc n}"} to @{term "0::nat"} and @{term "{..< n}"}. *}
1.373 +
1.374 +lemma lessThan_Suc_eq_insert_0: "{..<Suc n} = insert 0 (Suc  {..<n})"
1.375 +proof safe
1.376 +  fix x assume "x < Suc n" "x \<notin> Suc  {..<n}"
1.377 +  then have "x \<noteq> Suc (x - 1)" by auto
1.378 +  with x < Suc n show "x = 0" by auto
1.379 +qed
1.380 +
1.381 +lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"
1.382 +by (simp add: lessThan_def atMost_def less_Suc_eq_le)
1.383 +
1.384 +lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"
1.385 +by blast
1.386 +
1.387 +subsubsection {* The Constant @{term greaterThan} *}
1.388 +
1.389 +lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"
1.390 +apply (simp add: greaterThan_def)
1.391 +apply (blast dest: gr0_conv_Suc [THEN iffD1])
1.392 +done
1.393 +
1.394 +lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"
1.395 +apply (simp add: greaterThan_def)
1.396 +apply (auto elim: linorder_neqE)
1.397 +done
1.398 +
1.399 +lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"
1.400 +by blast
1.401 +
1.402 +subsubsection {* The Constant @{term atLeast} *}
1.403 +
1.404 +lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"
1.405 +by (unfold atLeast_def UNIV_def, simp)
1.406 +
1.407 +lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"
1.408 +apply (simp add: atLeast_def)
1.409 +apply (simp add: Suc_le_eq)
1.410 +apply (simp add: order_le_less, blast)
1.411 +done
1.412 +
1.413 +lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k"
1.414 +  by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le)
1.415 +
1.416 +lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"
1.417 +by blast
1.418 +
1.419 +subsubsection {* The Constant @{term atMost} *}
1.420 +
1.421 +lemma atMost_0 [simp]: "atMost (0::nat) = {0}"
1.422 +by (simp add: atMost_def)
1.423 +
1.424 +lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"
1.425 +apply (simp add: atMost_def)
1.426 +apply (simp add: less_Suc_eq order_le_less, blast)
1.427 +done
1.428 +
1.429 +lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
1.430 +by blast
1.431 +
1.432 +subsubsection {* The Constant @{term atLeastLessThan} *}
1.433 +
1.434 +text{*The orientation of the following 2 rules is tricky. The lhs is
1.435 +defined in terms of the rhs.  Hence the chosen orientation makes sense
1.436 +in this theory --- the reverse orientation complicates proofs (eg
1.437 +nontermination). But outside, when the definition of the lhs is rarely
1.438 +used, the opposite orientation seems preferable because it reduces a
1.439 +specific concept to a more general one. *}
1.440 +
1.441 +lemma atLeast0LessThan: "{0::nat..<n} = {..<n}"
1.442 +by(simp add:lessThan_def atLeastLessThan_def)
1.443 +
1.444 +lemma atLeast0AtMost: "{0..n::nat} = {..n}"
1.445 +by(simp add:atMost_def atLeastAtMost_def)
1.446 +
1.447 +declare atLeast0LessThan[symmetric, code_unfold]
1.448 +        atLeast0AtMost[symmetric, code_unfold]
1.449 +
1.450 +lemma atLeastLessThan0: "{m..<0::nat} = {}"
1.451 +by (simp add: atLeastLessThan_def)
1.452 +
1.453 +subsubsection {* Intervals of nats with @{term Suc} *}
1.454 +
1.455 +text{*Not a simprule because the RHS is too messy.*}
1.456 +lemma atLeastLessThanSuc:
1.457 +    "{m..<Suc n} = (if m \<le> n then insert n {m..<n} else {})"
1.458 +by (auto simp add: atLeastLessThan_def)
1.459 +
1.460 +lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}"
1.461 +by (auto simp add: atLeastLessThan_def)
1.462 +(*
1.463 +lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}"
1.464 +by (induct k, simp_all add: atLeastLessThanSuc)
1.465 +
1.466 +lemma atLeastSucLessThan [simp]: "{Suc n..<n} = {}"
1.467 +by (auto simp add: atLeastLessThan_def)
1.468 +*)
1.469 +lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}"
1.470 +  by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def)
1.471 +
1.472 +lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {l<..u}"
1.473 +  by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def
1.474 +    greaterThanAtMost_def)
1.475 +
1.476 +lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..<u} = {l<..<u}"
1.477 +  by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def
1.478 +    greaterThanLessThan_def)
1.479 +
1.480 +lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}"
1.481 +by (auto simp add: atLeastAtMost_def)
1.482 +
1.483 +lemma atLeastAtMost_insertL: "m \<le> n \<Longrightarrow> insert m {Suc m..n} = {m ..n}"
1.484 +by auto
1.485 +
1.486 +text {* The analogous result is useful on @{typ int}: *}
1.487 +(* here, because we don't have an own int section *)
1.488 +lemma atLeastAtMostPlus1_int_conv:
1.489 +  "m <= 1+n \<Longrightarrow> {m..1+n} = insert (1+n) {m..n::int}"
1.490 +  by (auto intro: set_eqI)
1.491 +
1.492 +lemma atLeastLessThan_add_Un: "i \<le> j \<Longrightarrow> {i..<j+k} = {i..<j} \<union> {j..<j+k::nat}"
1.493 +  apply (induct k)
1.494 +  apply (simp_all add: atLeastLessThanSuc)
1.495 +  done
1.496 +
1.497 +subsubsection {* Image *}
1.498 +
1.500 +  "(%n::nat. n+k)  {i..j} = {i+k..j+k}" (is "?A = ?B")
1.501 +proof
1.502 +  show "?A \<subseteq> ?B" by auto
1.503 +next
1.504 +  show "?B \<subseteq> ?A"
1.505 +  proof
1.506 +    fix n assume a: "n : ?B"
1.507 +    hence "n - k : {i..j}" by auto
1.508 +    moreover have "n = (n - k) + k" using a by auto
1.509 +    ultimately show "n : ?A" by blast
1.510 +  qed
1.511 +qed
1.512 +
1.514 +  "(%n::nat. n+k)  {i..<j} = {i+k..<j+k}" (is "?A = ?B")
1.515 +proof
1.516 +  show "?A \<subseteq> ?B" by auto
1.517 +next
1.518 +  show "?B \<subseteq> ?A"
1.519 +  proof
1.520 +    fix n assume a: "n : ?B"
1.521 +    hence "n - k : {i..<j}" by auto
1.522 +    moreover have "n = (n - k) + k" using a by auto
1.523 +    ultimately show "n : ?A" by blast
1.524 +  qed
1.525 +qed
1.526 +
1.527 +corollary image_Suc_atLeastAtMost[simp]:
1.528 +  "Suc  {i..j} = {Suc i..Suc j}"
1.529 +using image_add_atLeastAtMost[where k="Suc 0"] by simp
1.530 +
1.531 +corollary image_Suc_atLeastLessThan[simp]:
1.532 +  "Suc  {i..<j} = {Suc i..<Suc j}"
1.533 +using image_add_atLeastLessThan[where k="Suc 0"] by simp
1.534 +
1.536 +    "(%x. x + (l::int))  {0..<u-l} = {l..<u}"
1.537 +  apply (auto simp add: image_def)
1.538 +  apply (rule_tac x = "x - l" in bexI)
1.539 +  apply auto
1.540 +  done
1.541 +
1.542 +lemma image_minus_const_atLeastLessThan_nat:
1.543 +  fixes c :: nat
1.544 +  shows "(\<lambda>i. i - c)  {x ..< y} =
1.545 +      (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"
1.546 +    (is "_ = ?right")
1.547 +proof safe
1.548 +  fix a assume a: "a \<in> ?right"
1.549 +  show "a \<in> (\<lambda>i. i - c)  {x ..< y}"
1.550 +  proof cases
1.551 +    assume "c < y" with a show ?thesis
1.552 +      by (auto intro!: image_eqI[of _ _ "a + c"])
1.553 +  next
1.554 +    assume "\<not> c < y" with a show ?thesis
1.555 +      by (auto intro!: image_eqI[of _ _ x] split: split_if_asm)
1.556 +  qed
1.557 +qed auto
1.558 +
1.560 +begin
1.561 +
1.562 +lemma
1.563 +  fixes x :: 'a
1.564 +  shows image_uminus_greaterThan[simp]: "uminus  {x<..} = {..<-x}"
1.565 +  and image_uminus_atLeast[simp]: "uminus  {x..} = {..-x}"
1.566 +proof safe
1.567 +  fix y assume "y < -x"
1.568 +  hence *:  "x < -y" using neg_less_iff_less[of "-y" x] by simp
1.569 +  have "- (-y) \<in> uminus  {x<..}"
1.570 +    by (rule imageI) (simp add: *)
1.571 +  thus "y \<in> uminus  {x<..}" by simp
1.572 +next
1.573 +  fix y assume "y \<le> -x"
1.574 +  have "- (-y) \<in> uminus  {x..}"
1.575 +    by (rule imageI) (insert y \<le> -x[THEN le_imp_neg_le], simp)
1.576 +  thus "y \<in> uminus  {x..}" by simp
1.577 +qed simp_all
1.578 +
1.579 +lemma
1.580 +  fixes x :: 'a
1.581 +  shows image_uminus_lessThan[simp]: "uminus  {..<x} = {-x<..}"
1.582 +  and image_uminus_atMost[simp]: "uminus  {..x} = {-x..}"
1.583 +proof -
1.584 +  have "uminus  {..<x} = uminus  uminus  {-x<..}"
1.585 +    and "uminus  {..x} = uminus  uminus  {-x..}" by simp_all
1.586 +  thus "uminus  {..<x} = {-x<..}" and "uminus  {..x} = {-x..}"
1.587 +    by (simp_all add: image_image
1.588 +        del: image_uminus_greaterThan image_uminus_atLeast)
1.589 +qed
1.590 +
1.591 +lemma
1.592 +  fixes x :: 'a
1.593 +  shows image_uminus_atLeastAtMost[simp]: "uminus  {x..y} = {-y..-x}"
1.594 +  and image_uminus_greaterThanAtMost[simp]: "uminus  {x<..y} = {-y..<-x}"
1.595 +  and image_uminus_atLeastLessThan[simp]: "uminus  {x..<y} = {-y<..-x}"
1.596 +  and image_uminus_greaterThanLessThan[simp]: "uminus  {x<..<y} = {-y<..<-x}"
1.597 +  by (simp_all add: atLeastAtMost_def greaterThanAtMost_def atLeastLessThan_def
1.598 +      greaterThanLessThan_def image_Int[OF inj_uminus] Int_commute)
1.599 +end
1.600 +
1.601 +subsubsection {* Finiteness *}
1.602 +
1.603 +lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}"
1.604 +  by (induct k) (simp_all add: lessThan_Suc)
1.605 +
1.606 +lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}"
1.607 +  by (induct k) (simp_all add: atMost_Suc)
1.608 +
1.609 +lemma finite_greaterThanLessThan [iff]:
1.610 +  fixes l :: nat shows "finite {l<..<u}"
1.611 +by (simp add: greaterThanLessThan_def)
1.612 +
1.613 +lemma finite_atLeastLessThan [iff]:
1.614 +  fixes l :: nat shows "finite {l..<u}"
1.615 +by (simp add: atLeastLessThan_def)
1.616 +
1.617 +lemma finite_greaterThanAtMost [iff]:
1.618 +  fixes l :: nat shows "finite {l<..u}"
1.619 +by (simp add: greaterThanAtMost_def)
1.620 +
1.621 +lemma finite_atLeastAtMost [iff]:
1.622 +  fixes l :: nat shows "finite {l..u}"
1.623 +by (simp add: atLeastAtMost_def)
1.624 +
1.625 +text {* A bounded set of natural numbers is finite. *}
1.626 +lemma bounded_nat_set_is_finite:
1.627 +  "(ALL i:N. i < (n::nat)) ==> finite N"
1.628 +apply (rule finite_subset)
1.629 + apply (rule_tac [2] finite_lessThan, auto)
1.630 +done
1.631 +
1.632 +text {* A set of natural numbers is finite iff it is bounded. *}
1.633 +lemma finite_nat_set_iff_bounded:
1.634 +  "finite(N::nat set) = (EX m. ALL n:N. n<m)" (is "?F = ?B")
1.635 +proof
1.636 +  assume f:?F  show ?B
1.637 +    using Max_ge[OF ?F, simplified less_Suc_eq_le[symmetric]] by blast
1.638 +next
1.639 +  assume ?B show ?F using ?B by(blast intro:bounded_nat_set_is_finite)
1.640 +qed
1.641 +
1.642 +lemma finite_nat_set_iff_bounded_le:
1.643 +  "finite(N::nat set) = (EX m. ALL n:N. n<=m)"
1.645 +apply(blast dest:less_imp_le_nat le_imp_less_Suc)
1.646 +done
1.647 +
1.648 +lemma finite_less_ub:
1.649 +     "!!f::nat=>nat. (!!n. n \<le> f n) ==> finite {n. f n \<le> u}"
1.650 +by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)
1.651 +
1.652 +text{* Any subset of an interval of natural numbers the size of the
1.653 +subset is exactly that interval. *}
1.654 +
1.655 +lemma subset_card_intvl_is_intvl:
1.656 +  "A <= {k..<k+card A} \<Longrightarrow> A = {k..<k+card A}" (is "PROP ?P")
1.657 +proof cases
1.658 +  assume "finite A"
1.659 +  thus "PROP ?P"
1.660 +  proof(induct A rule:finite_linorder_max_induct)
1.661 +    case empty thus ?case by auto
1.662 +  next
1.663 +    case (insert b A)
1.664 +    moreover hence "b ~: A" by auto
1.665 +    moreover have "A <= {k..<k+card A}" and "b = k+card A"
1.666 +      using b ~: A insert by fastforce+
1.667 +    ultimately show ?case by auto
1.668 +  qed
1.669 +next
1.670 +  assume "~finite A" thus "PROP ?P" by simp
1.671 +qed
1.672 +
1.673 +
1.674 +subsubsection {* Proving Inclusions and Equalities between Unions *}
1.675 +
1.676 +lemma UN_le_eq_Un0:
1.677 +  "(\<Union>i\<le>n::nat. M i) = (\<Union>i\<in>{1..n}. M i) \<union> M 0" (is "?A = ?B")
1.678 +proof
1.679 +  show "?A <= ?B"
1.680 +  proof
1.681 +    fix x assume "x : ?A"
1.682 +    then obtain i where i: "i\<le>n" "x : M i" by auto
1.683 +    show "x : ?B"
1.684 +    proof(cases i)
1.685 +      case 0 with i show ?thesis by simp
1.686 +    next
1.687 +      case (Suc j) with i show ?thesis by auto
1.688 +    qed
1.689 +  qed
1.690 +next
1.691 +  show "?B <= ?A" by auto
1.692 +qed
1.693 +
1.695 +  "(\<Union>i\<le>n::nat. M(i+k)) = (\<Union>i\<in>{k..n+k}. M i)" (is "?A = ?B")
1.696 +proof
1.697 +  show "?A <= ?B" by fastforce
1.698 +next
1.699 +  show "?B <= ?A"
1.700 +  proof
1.701 +    fix x assume "x : ?B"
1.702 +    then obtain i where i: "i : {k..n+k}" "x : M(i)" by auto
1.703 +    hence "i-k\<le>n & x : M((i-k)+k)" by auto
1.704 +    thus "x : ?A" by blast
1.705 +  qed
1.706 +qed
1.707 +
1.708 +lemma UN_UN_finite_eq: "(\<Union>n::nat. \<Union>i\<in>{0..<n}. A i) = (\<Union>n. A n)"
1.709 +  by (auto simp add: atLeast0LessThan)
1.710 +
1.711 +lemma UN_finite_subset: "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> C) \<Longrightarrow> (\<Union>n. A n) \<subseteq> C"
1.712 +  by (subst UN_UN_finite_eq [symmetric]) blast
1.713 +
1.714 +lemma UN_finite2_subset:
1.715 +     "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n+k}. B i)) \<Longrightarrow> (\<Union>n. A n) \<subseteq> (\<Union>n. B n)"
1.716 +  apply (rule UN_finite_subset)
1.717 +  apply (subst UN_UN_finite_eq [symmetric, of B])
1.718 +  apply blast
1.719 +  done
1.720 +
1.721 +lemma UN_finite2_eq:
1.722 +  "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) = (\<Union>i\<in>{0..<n+k}. B i)) \<Longrightarrow> (\<Union>n. A n) = (\<Union>n. B n)"
1.723 +  apply (rule subset_antisym)
1.724 +   apply (rule UN_finite2_subset, blast)
1.725 + apply (rule UN_finite2_subset [where k=k])
1.726 + apply (force simp add: atLeastLessThan_add_Un [of 0])
1.727 + done
1.728 +
1.729 +
1.730 +subsubsection {* Cardinality *}
1.731 +
1.732 +lemma card_lessThan [simp]: "card {..<u} = u"
1.733 +  by (induct u, simp_all add: lessThan_Suc)
1.734 +
1.735 +lemma card_atMost [simp]: "card {..u} = Suc u"
1.736 +  by (simp add: lessThan_Suc_atMost [THEN sym])
1.737 +
1.738 +lemma card_atLeastLessThan [simp]: "card {l..<u} = u - l"
1.739 +  apply (subgoal_tac "card {l..<u} = card {..<u-l}")
1.740 +  apply (erule ssubst, rule card_lessThan)
1.741 +  apply (subgoal_tac "(%x. x + l)  {..<u-l} = {l..<u}")
1.742 +  apply (erule subst)
1.743 +  apply (rule card_image)
1.744 +  apply (simp add: inj_on_def)
1.745 +  apply (auto simp add: image_def atLeastLessThan_def lessThan_def)
1.746 +  apply (rule_tac x = "x - l" in exI)
1.747 +  apply arith
1.748 +  done
1.749 +
1.750 +lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l"
1.751 +  by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp)
1.752 +
1.753 +lemma card_greaterThanAtMost [simp]: "card {l<..u} = u - l"
1.754 +  by (subst atLeastSucAtMost_greaterThanAtMost [THEN sym], simp)
1.755 +
1.756 +lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u - Suc l"
1.757 +  by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp)
1.758 +
1.759 +lemma ex_bij_betw_nat_finite:
1.760 +  "finite M \<Longrightarrow> \<exists>h. bij_betw h {0..<card M} M"
1.761 +apply(drule finite_imp_nat_seg_image_inj_on)
1.762 +apply(auto simp:atLeast0LessThan[symmetric] lessThan_def[symmetric] card_image bij_betw_def)
1.763 +done
1.764 +
1.765 +lemma ex_bij_betw_finite_nat:
1.766 +  "finite M \<Longrightarrow> \<exists>h. bij_betw h M {0..<card M}"
1.767 +by (blast dest: ex_bij_betw_nat_finite bij_betw_inv)
1.768 +
1.769 +lemma finite_same_card_bij:
1.770 +  "finite A \<Longrightarrow> finite B \<Longrightarrow> card A = card B \<Longrightarrow> EX h. bij_betw h A B"
1.771 +apply(drule ex_bij_betw_finite_nat)
1.772 +apply(drule ex_bij_betw_nat_finite)
1.773 +apply(auto intro!:bij_betw_trans)
1.774 +done
1.775 +
1.776 +lemma ex_bij_betw_nat_finite_1:
1.777 +  "finite M \<Longrightarrow> \<exists>h. bij_betw h {1 .. card M} M"
1.778 +by (rule finite_same_card_bij) auto
1.779 +
1.780 +lemma bij_betw_iff_card:
1.781 +  assumes FIN: "finite A" and FIN': "finite B"
1.782 +  shows BIJ: "(\<exists>f. bij_betw f A B) \<longleftrightarrow> (card A = card B)"
1.783 +using assms
1.784 +proof(auto simp add: bij_betw_same_card)
1.785 +  assume *: "card A = card B"
1.786 +  obtain f where "bij_betw f A {0 ..< card A}"
1.787 +  using FIN ex_bij_betw_finite_nat by blast
1.788 +  moreover obtain g where "bij_betw g {0 ..< card B} B"
1.789 +  using FIN' ex_bij_betw_nat_finite by blast
1.790 +  ultimately have "bij_betw (g o f) A B"
1.791 +  using * by (auto simp add: bij_betw_trans)
1.792 +  thus "(\<exists>f. bij_betw f A B)" by blast
1.793 +qed
1.794 +
1.795 +lemma inj_on_iff_card_le:
1.796 +  assumes FIN: "finite A" and FIN': "finite B"
1.797 +  shows "(\<exists>f. inj_on f A \<and> f  A \<le> B) = (card A \<le> card B)"
1.798 +proof (safe intro!: card_inj_on_le)
1.799 +  assume *: "card A \<le> card B"
1.800 +  obtain f where 1: "inj_on f A" and 2: "f  A = {0 ..< card A}"
1.801 +  using FIN ex_bij_betw_finite_nat unfolding bij_betw_def by force
1.802 +  moreover obtain g where "inj_on g {0 ..< card B}" and 3: "g  {0 ..< card B} = B"
1.803 +  using FIN' ex_bij_betw_nat_finite unfolding bij_betw_def by force
1.804 +  ultimately have "inj_on g (f  A)" using subset_inj_on[of g _ "f  A"] * by force
1.805 +  hence "inj_on (g o f) A" using 1 comp_inj_on by blast
1.806 +  moreover
1.807 +  {have "{0 ..< card A} \<le> {0 ..< card B}" using * by force
1.808 +   with 2 have "f  A  \<le> {0 ..< card B}" by blast
1.809 +   hence "(g o f)  A \<le> B" unfolding comp_def using 3 by force
1.810 +  }
1.811 +  ultimately show "(\<exists>f. inj_on f A \<and> f  A \<le> B)" by blast
1.812 +qed (insert assms, auto)
1.813 +
1.814 +subsection {* Intervals of integers *}
1.815 +
1.816 +lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..<u+1} = {l..(u::int)}"
1.817 +  by (auto simp add: atLeastAtMost_def atLeastLessThan_def)
1.818 +
1.819 +lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}"
1.820 +  by (auto simp add: atLeastAtMost_def greaterThanAtMost_def)
1.821 +
1.822 +lemma atLeastPlusOneLessThan_greaterThanLessThan_int:
1.823 +    "{l+1..<u} = {l<..<u::int}"
1.824 +  by (auto simp add: atLeastLessThan_def greaterThanLessThan_def)
1.825 +
1.826 +subsubsection {* Finiteness *}
1.827 +
1.828 +lemma image_atLeastZeroLessThan_int: "0 \<le> u ==>
1.829 +    {(0::int)..<u} = int  {..<nat u}"
1.830 +  apply (unfold image_def lessThan_def)
1.831 +  apply auto
1.832 +  apply (rule_tac x = "nat x" in exI)
1.833 +  apply (auto simp add: zless_nat_eq_int_zless [THEN sym])
1.834 +  done
1.835 +
1.836 +lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}"
1.837 +  apply (case_tac "0 \<le> u")
1.838 +  apply (subst image_atLeastZeroLessThan_int, assumption)
1.839 +  apply (rule finite_imageI)
1.840 +  apply auto
1.841 +  done
1.842 +
1.843 +lemma finite_atLeastLessThan_int [iff]: "finite {l..<u::int}"
1.844 +  apply (subgoal_tac "(%x. x + l)  {0..<u-l} = {l..<u}")
1.845 +  apply (erule subst)
1.846 +  apply (rule finite_imageI)
1.847 +  apply (rule finite_atLeastZeroLessThan_int)
1.848 +  apply (rule image_add_int_atLeastLessThan)
1.849 +  done
1.850 +
1.851 +lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}"
1.852 +  by (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym], simp)
1.853 +
1.854 +lemma finite_greaterThanAtMost_int [iff]: "finite {l<..(u::int)}"
1.855 +  by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
1.856 +
1.857 +lemma finite_greaterThanLessThan_int [iff]: "finite {l<..<u::int}"
1.858 +  by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
1.859 +
1.860 +
1.861 +subsubsection {* Cardinality *}
1.862 +
1.863 +lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u"
1.864 +  apply (case_tac "0 \<le> u")
1.865 +  apply (subst image_atLeastZeroLessThan_int, assumption)
1.866 +  apply (subst card_image)
1.867 +  apply (auto simp add: inj_on_def)
1.868 +  done
1.869 +
1.870 +lemma card_atLeastLessThan_int [simp]: "card {l..<u} = nat (u - l)"
1.871 +  apply (subgoal_tac "card {l..<u} = card {0..<u-l}")
1.872 +  apply (erule ssubst, rule card_atLeastZeroLessThan_int)
1.873 +  apply (subgoal_tac "(%x. x + l)  {0..<u-l} = {l..<u}")
1.874 +  apply (erule subst)
1.875 +  apply (rule card_image)
1.876 +  apply (simp add: inj_on_def)
1.877 +  apply (rule image_add_int_atLeastLessThan)
1.878 +  done
1.879 +
1.880 +lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u - l + 1)"
1.881 +apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym])
1.882 +apply (auto simp add: algebra_simps)
1.883 +done
1.884 +
1.885 +lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u - l)"
1.886 +by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
1.887 +
1.888 +lemma card_greaterThanLessThan_int [simp]: "card {l<..<u} = nat (u - (l + 1))"
1.889 +by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
1.890 +
1.891 +lemma finite_M_bounded_by_nat: "finite {k. P k \<and> k < (i::nat)}"
1.892 +proof -
1.893 +  have "{k. P k \<and> k < i} \<subseteq> {..<i}" by auto
1.894 +  with finite_lessThan[of "i"] show ?thesis by (simp add: finite_subset)
1.895 +qed
1.896 +
1.897 +lemma card_less:
1.898 +assumes zero_in_M: "0 \<in> M"
1.899 +shows "card {k \<in> M. k < Suc i} \<noteq> 0"
1.900 +proof -
1.901 +  from zero_in_M have "{k \<in> M. k < Suc i} \<noteq> {}" by auto
1.902 +  with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff)
1.903 +qed
1.904 +
1.905 +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.906 +apply (rule card_bij_eq [of Suc _ _ "\<lambda>x. x - Suc 0"])
1.907 +apply simp
1.908 +apply fastforce
1.909 +apply auto
1.910 +apply (rule inj_on_diff_nat)
1.911 +apply auto
1.912 +apply (case_tac x)
1.913 +apply auto
1.914 +apply (case_tac xa)
1.915 +apply auto
1.916 +apply (case_tac xa)
1.917 +apply auto
1.918 +done
1.919 +
1.920 +lemma card_less_Suc:
1.921 +  assumes zero_in_M: "0 \<in> M"
1.922 +    shows "Suc (card {k. Suc k \<in> M \<and> k < i}) = card {k \<in> M. k < Suc i}"
1.923 +proof -
1.924 +  from assms have a: "0 \<in> {k \<in> M. k < Suc i}" by simp
1.925 +  hence c: "{k \<in> M. k < Suc i} = insert 0 ({k \<in> M. k < Suc i} - {0})"
1.926 +    by (auto simp only: insert_Diff)
1.927 +  have b: "{k \<in> M. k < Suc i} - {0} = {k \<in> M - {0}. k < Suc i}"  by auto
1.928 +  from finite_M_bounded_by_nat[of "\<lambda>x. x \<in> M" "Suc i"] have "Suc (card {k. Suc k \<in> M \<and> k < i}) = card (insert 0 ({k \<in> M. k < Suc i} - {0}))"
1.929 +    apply (subst card_insert)
1.930 +    apply simp_all
1.931 +    apply (subst b)
1.932 +    apply (subst card_less_Suc2[symmetric])
1.933 +    apply simp_all
1.934 +    done
1.935 +  with c show ?thesis by simp
1.936 +qed
1.937 +
1.938 +
1.939 +subsection {*Lemmas useful with the summation operator setsum*}
1.940 +
1.941 +text {* For examples, see Algebra/poly/UnivPoly2.thy *}
1.942 +
1.943 +subsubsection {* Disjoint Unions *}
1.944 +
1.945 +text {* Singletons and open intervals *}
1.946 +
1.947 +lemma ivl_disj_un_singleton:
1.948 +  "{l::'a::linorder} Un {l<..} = {l..}"
1.949 +  "{..<u} Un {u::'a::linorder} = {..u}"
1.950 +  "(l::'a::linorder) < u ==> {l} Un {l<..<u} = {l..<u}"
1.951 +  "(l::'a::linorder) < u ==> {l<..<u} Un {u} = {l<..u}"
1.952 +  "(l::'a::linorder) <= u ==> {l} Un {l<..u} = {l..u}"
1.953 +  "(l::'a::linorder) <= u ==> {l..<u} Un {u} = {l..u}"
1.954 +by auto
1.955 +
1.956 +text {* One- and two-sided intervals *}
1.957 +
1.958 +lemma ivl_disj_un_one:
1.959 +  "(l::'a::linorder) < u ==> {..l} Un {l<..<u} = {..<u}"
1.960 +  "(l::'a::linorder) <= u ==> {..<l} Un {l..<u} = {..<u}"
1.961 +  "(l::'a::linorder) <= u ==> {..l} Un {l<..u} = {..u}"
1.962 +  "(l::'a::linorder) <= u ==> {..<l} Un {l..u} = {..u}"
1.963 +  "(l::'a::linorder) <= u ==> {l<..u} Un {u<..} = {l<..}"
1.964 +  "(l::'a::linorder) < u ==> {l<..<u} Un {u..} = {l<..}"
1.965 +  "(l::'a::linorder) <= u ==> {l..u} Un {u<..} = {l..}"
1.966 +  "(l::'a::linorder) <= u ==> {l..<u} Un {u..} = {l..}"
1.967 +by auto
1.968 +
1.969 +text {* Two- and two-sided intervals *}
1.970 +
1.971 +lemma ivl_disj_un_two:
1.972 +  "[| (l::'a::linorder) < m; m <= u |] ==> {l<..<m} Un {m..<u} = {l<..<u}"
1.973 +  "[| (l::'a::linorder) <= m; m < u |] ==> {l<..m} Un {m<..<u} = {l<..<u}"
1.974 +  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..<m} Un {m..<u} = {l..<u}"
1.975 +  "[| (l::'a::linorder) <= m; m < u |] ==> {l..m} Un {m<..<u} = {l..<u}"
1.976 +  "[| (l::'a::linorder) < m; m <= u |] ==> {l<..<m} Un {m..u} = {l<..u}"
1.977 +  "[| (l::'a::linorder) <= m; m <= u |] ==> {l<..m} Un {m<..u} = {l<..u}"
1.978 +  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..<m} Un {m..u} = {l..u}"
1.979 +  "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {m<..u} = {l..u}"
1.980 +by auto
1.981 +
1.982 +lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two
1.983 +
1.984 +subsubsection {* Disjoint Intersections *}
1.985 +
1.986 +text {* One- and two-sided intervals *}
1.987 +
1.988 +lemma ivl_disj_int_one:
1.989 +  "{..l::'a::order} Int {l<..<u} = {}"
1.990 +  "{..<l} Int {l..<u} = {}"
1.991 +  "{..l} Int {l<..u} = {}"
1.992 +  "{..<l} Int {l..u} = {}"
1.993 +  "{l<..u} Int {u<..} = {}"
1.994 +  "{l<..<u} Int {u..} = {}"
1.995 +  "{l..u} Int {u<..} = {}"
1.996 +  "{l..<u} Int {u..} = {}"
1.997 +  by auto
1.998 +
1.999 +text {* Two- and two-sided intervals *}
1.1000 +
1.1001 +lemma ivl_disj_int_two:
1.1002 +  "{l::'a::order<..<m} Int {m..<u} = {}"
1.1003 +  "{l<..m} Int {m<..<u} = {}"
1.1004 +  "{l..<m} Int {m..<u} = {}"
1.1005 +  "{l..m} Int {m<..<u} = {}"
1.1006 +  "{l<..<m} Int {m..u} = {}"
1.1007 +  "{l<..m} Int {m<..u} = {}"
1.1008 +  "{l..<m} Int {m..u} = {}"
1.1009 +  "{l..m} Int {m<..u} = {}"
1.1010 +  by auto
1.1011 +
1.1012 +lemmas ivl_disj_int = ivl_disj_int_one ivl_disj_int_two
1.1013 +
1.1014 +subsubsection {* Some Differences *}
1.1015 +
1.1016 +lemma ivl_diff[simp]:
1.1017 + "i \<le> n \<Longrightarrow> {i..<m} - {i..<n} = {n..<(m::'a::linorder)}"
1.1018 +by(auto)
1.1019 +
1.1020 +
1.1021 +subsubsection {* Some Subset Conditions *}
1.1022 +
1.1023 +lemma ivl_subset [simp,no_atp]:
1.1024 + "({i..<j} \<subseteq> {m..<n}) = (j \<le> i | m \<le> i & j \<le> (n::'a::linorder))"
1.1025 +apply(auto simp:linorder_not_le)
1.1026 +apply(rule ccontr)
1.1027 +apply(insert linorder_le_less_linear[of i n])
1.1028 +apply(clarsimp simp:linorder_not_le)
1.1029 +apply(fastforce)
1.1030 +done
1.1031 +
1.1032 +
1.1033 +subsection {* Summation indexed over intervals *}
1.1034 +
1.1035 +syntax
1.1036 +  "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)
1.1037 +  "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)
1.1038 +  "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<_./ _)" [0,0,10] 10)
1.1039 +  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<=_./ _)" [0,0,10] 10)
1.1040 +syntax (xsymbols)
1.1041 +  "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
1.1042 +  "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10)
1.1043 +  "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10)
1.1044 +  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10)
1.1045 +syntax (HTML output)
1.1046 +  "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
1.1047 +  "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10)
1.1048 +  "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10)
1.1049 +  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10)
1.1050 +syntax (latex_sum output)
1.1051 +  "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
1.1052 + ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)
1.1053 +  "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
1.1054 + ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)
1.1055 +  "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
1.1056 + ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10)
1.1057 +  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
1.1058 + ("(3\<^raw:$\sum_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10)
1.1059 +
1.1060 +translations
1.1061 +  "\<Sum>x=a..b. t" == "CONST setsum (%x. t) {a..b}"
1.1062 +  "\<Sum>x=a..<b. t" == "CONST setsum (%x. t) {a..<b}"
1.1063 +  "\<Sum>i\<le>n. t" == "CONST setsum (\<lambda>i. t) {..n}"
1.1064 +  "\<Sum>i<n. t" == "CONST setsum (\<lambda>i. t) {..<n}"
1.1065 +
1.1066 +text{* The above introduces some pretty alternative syntaxes for
1.1067 +summation over intervals:
1.1068 +\begin{center}
1.1069 +\begin{tabular}{lll}
1.1070 +Old & New & \LaTeX\\
1.1071 +@{term[source]"\<Sum>x\<in>{a..b}. e"} & @{term"\<Sum>x=a..b. e"} & @{term[mode=latex_sum]"\<Sum>x=a..b. e"}\\
1.1072 +@{term[source]"\<Sum>x\<in>{a..<b}. e"} & @{term"\<Sum>x=a..<b. e"} & @{term[mode=latex_sum]"\<Sum>x=a..<b. e"}\\
1.1073 +@{term[source]"\<Sum>x\<in>{..b}. e"} & @{term"\<Sum>x\<le>b. e"} & @{term[mode=latex_sum]"\<Sum>x\<le>b. e"}\\
1.1074 +@{term[source]"\<Sum>x\<in>{..<b}. e"} & @{term"\<Sum>x<b. e"} & @{term[mode=latex_sum]"\<Sum>x<b. e"}
1.1075 +\end{tabular}
1.1076 +\end{center}
1.1077 +The left column shows the term before introduction of the new syntax,
1.1078 +the middle column shows the new (default) syntax, and the right column
1.1079 +shows a special syntax. The latter is only meaningful for latex output
1.1080 +and has to be activated explicitly by setting the print mode to
1.1081 +@{text latex_sum} (e.g.\ via @{text "mode = latex_sum"} in
1.1082 +antiquotations). It is not the default \LaTeX\ output because it only
1.1083 +works well with italic-style formulae, not tt-style.
1.1084 +
1.1085 +Note that for uniformity on @{typ nat} it is better to use
1.1086 +@{term"\<Sum>x::nat=0..<n. e"} rather than @{text"\<Sum>x<n. e"}: @{text setsum} may
1.1087 +not provide all lemmas available for @{term"{m..<n}"} also in the
1.1088 +special form for @{term"{..<n}"}. *}
1.1089 +
1.1090 +text{* This congruence rule should be used for sums over intervals as
1.1091 +the standard theorem @{text[source]setsum_cong} does not work well
1.1092 +with the simplifier who adds the unsimplified premise @{term"x:B"} to
1.1093 +the context. *}
1.1094 +
1.1095 +lemma setsum_ivl_cong:
1.1096 + "\<lbrakk>a = c; b = d; !!x. \<lbrakk> c \<le> x; x < d \<rbrakk> \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow>
1.1097 + setsum f {a..<b} = setsum g {c..<d}"
1.1098 +by(rule setsum_cong, simp_all)
1.1099 +
1.1100 +(* FIXME why are the following simp rules but the corresponding eqns
1.1101 +on intervals are not? *)
1.1102 +
1.1103 +lemma setsum_atMost_Suc[simp]: "(\<Sum>i \<le> Suc n. f i) = (\<Sum>i \<le> n. f i) + f(Suc n)"
1.1105 +
1.1106 +lemma setsum_lessThan_Suc[simp]: "(\<Sum>i < Suc n. f i) = (\<Sum>i < n. f i) + f n"
1.1108 +
1.1109 +lemma setsum_cl_ivl_Suc[simp]:
1.1110 +  "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"
1.1111 +by (auto simp:add_ac atLeastAtMostSuc_conv)
1.1112 +
1.1113 +lemma setsum_op_ivl_Suc[simp]:
1.1114 +  "setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))"
1.1115 +by (auto simp:add_ac atLeastLessThanSuc)
1.1116 +(*
1.1117 +lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==>
1.1118 +    (\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)"
1.1119 +by (auto simp:add_ac atLeastAtMostSuc_conv)
1.1120 +*)
1.1121 +
1.1123 +  fixes n :: nat
1.1124 +  assumes mn: "m <= n"
1.1125 +  shows "(\<Sum>x\<in>{m..n}. P x) = P m + (\<Sum>x\<in>{m<..n}. P x)" (is "?lhs = ?rhs")
1.1126 +proof -
1.1127 +  from mn
1.1128 +  have "{m..n} = {m} \<union> {m<..n}"
1.1129 +    by (auto intro: ivl_disj_un_singleton)
1.1130 +  hence "?lhs = (\<Sum>x\<in>{m} \<union> {m<..n}. P x)"
1.1131 +    by (simp add: atLeast0LessThan)
1.1132 +  also have "\<dots> = ?rhs" by simp
1.1133 +  finally show ?thesis .
1.1134 +qed
1.1135 +
1.1137 +  "m \<le> n \<Longrightarrow> setsum f {m..n} = f m + setsum f {Suc m..n}"
1.1139 +
1.1141 +  "m < n \<Longrightarrow> setsum f {m..<n} = f m + setsum f {Suc m..<n}"
1.1142 +apply(insert setsum_head_Suc[of m "n - Suc 0" f])
1.1143 +apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps)
1.1144 +done
1.1145 +
1.1146 +lemma setsum_ub_add_nat: assumes "(m::nat) \<le> n + 1"
1.1147 +  shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}"
1.1148 +proof-
1.1149 +  have "{m .. n+p} = {m..n} \<union> {n+1..n+p}" using m \<le> n+1 by auto
1.1150 +  thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint
1.1151 +    atLeastSucAtMost_greaterThanAtMost)
1.1152 +qed
1.1153 +
1.1154 +lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
1.1155 +  setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"
1.1156 +by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un)
1.1157 +
1.1158 +lemma setsum_diff_nat_ivl:
1.1159 +fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
1.1160 +shows "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
1.1161 +  setsum f {m..<p} - setsum f {m..<n} = setsum f {n..<p}"
1.1162 +using setsum_add_nat_ivl [of m n p f,symmetric]
1.1164 +done
1.1165 +
1.1166 +lemma setsum_natinterval_difff:
1.1167 +  fixes f:: "nat \<Rightarrow> ('a::ab_group_add)"
1.1168 +  shows  "setsum (\<lambda>k. f k - f(k + 1)) {(m::nat) .. n} =
1.1169 +          (if m <= n then f m - f(n + 1) else 0)"
1.1170 +by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)
1.1171 +
1.1172 +lemma setsum_restrict_set':
1.1173 +  "finite A \<Longrightarrow> setsum f {x \<in> A. x \<in> B} = (\<Sum>x\<in>A. if x \<in> B then f x else 0)"
1.1174 +  by (simp add: setsum_restrict_set [symmetric] Int_def)
1.1175 +
1.1176 +lemma setsum_restrict_set'':
1.1177 +  "finite A \<Longrightarrow> setsum f {x \<in> A. P x} = (\<Sum>x\<in>A. if P x  then f x else 0)"
1.1178 +  by (simp add: setsum_restrict_set' [of A f "{x. P x}", simplified mem_Collect_eq])
1.1179 +
1.1180 +lemma setsum_setsum_restrict:
1.1181 +  "finite S \<Longrightarrow> finite T \<Longrightarrow>
1.1182 +    setsum (\<lambda>x. setsum (\<lambda>y. f x y) {y. y \<in> T \<and> R x y}) S = setsum (\<lambda>y. setsum (\<lambda>x. f x y) {x. x \<in> S \<and> R x y}) T"
1.1183 +  by (simp add: setsum_restrict_set'') (rule setsum_commute)
1.1184 +
1.1185 +lemma setsum_image_gen: assumes fS: "finite S"
1.1186 +  shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f  S)"
1.1187 +proof-
1.1188 +  { fix x assume "x \<in> S" then have "{y. y\<in> fS \<and> f x = y} = {f x}" by auto }
1.1189 +  hence "setsum g S = setsum (\<lambda>x. setsum (\<lambda>y. g x) {y. y\<in> fS \<and> f x = y}) S"
1.1190 +    by simp
1.1191 +  also have "\<dots> = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f  S)"
1.1192 +    by (rule setsum_setsum_restrict[OF fS finite_imageI[OF fS]])
1.1193 +  finally show ?thesis .
1.1194 +qed
1.1195 +
1.1196 +lemma setsum_le_included:
1.1197 +  fixes f :: "'a \<Rightarrow> 'b::ordered_comm_monoid_add"
1.1198 +  assumes "finite s" "finite t"
1.1199 +  and "\<forall>y\<in>t. 0 \<le> g y" "(\<forall>x\<in>s. \<exists>y\<in>t. i y = x \<and> f x \<le> g y)"
1.1200 +  shows "setsum f s \<le> setsum g t"
1.1201 +proof -
1.1202 +  have "setsum f s \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) s"
1.1203 +  proof (rule setsum_mono)
1.1204 +    fix y assume "y \<in> s"
1.1205 +    with assms obtain z where z: "z \<in> t" "y = i z" "f y \<le> g z" by auto
1.1206 +    with assms show "f y \<le> setsum g {x \<in> t. i x = y}" (is "?A y \<le> ?B y")
1.1207 +      using order_trans[of "?A (i z)" "setsum g {z}" "?B (i z)", intro]
1.1208 +      by (auto intro!: setsum_mono2)
1.1209 +  qed
1.1210 +  also have "... \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) (i  t)"
1.1211 +    using assms(2-4) by (auto intro!: setsum_mono2 setsum_nonneg)
1.1212 +  also have "... \<le> setsum g t"
1.1213 +    using assms by (auto simp: setsum_image_gen[symmetric])
1.1214 +  finally show ?thesis .
1.1215 +qed
1.1216 +
1.1217 +lemma setsum_multicount_gen:
1.1218 +  assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)"
1.1219 +  shows "setsum (\<lambda>i. (card {j\<in>t. R i j})) s = setsum k t" (is "?l = ?r")
1.1220 +proof-
1.1221 +  have "?l = setsum (\<lambda>i. setsum (\<lambda>x.1) {j\<in>t. R i j}) s" by auto
1.1222 +  also have "\<dots> = ?r" unfolding setsum_setsum_restrict[OF assms(1-2)]
1.1223 +    using assms(3) by auto
1.1224 +  finally show ?thesis .
1.1225 +qed
1.1226 +
1.1227 +lemma setsum_multicount:
1.1228 +  assumes "finite S" "finite T" "\<forall>j\<in>T. (card {i\<in>S. R i j} = k)"
1.1229 +  shows "setsum (\<lambda>i. card {j\<in>T. R i j}) S = k * card T" (is "?l = ?r")
1.1230 +proof-
1.1231 +  have "?l = setsum (\<lambda>i. k) T" by(rule setsum_multicount_gen)(auto simp:assms)
1.1232 +  also have "\<dots> = ?r" by(simp add: mult_commute)
1.1233 +  finally show ?thesis by auto
1.1234 +qed
1.1235 +
1.1236 +
1.1237 +subsection{* Shifting bounds *}
1.1238 +
1.1239 +lemma setsum_shift_bounds_nat_ivl:
1.1240 +  "setsum f {m+k..<n+k} = setsum (%i. f(i + k)){m..<n::nat}"
1.1241 +by (induct "n", auto simp:atLeastLessThanSuc)
1.1242 +
1.1243 +lemma setsum_shift_bounds_cl_nat_ivl:
1.1244 +  "setsum f {m+k..n+k} = setsum (%i. f(i + k)){m..n::nat}"
1.1245 +apply (insert setsum_reindex[OF inj_on_add_nat, where h=f and B = "{m..n}"])
1.1247 +done
1.1248 +
1.1249 +corollary setsum_shift_bounds_cl_Suc_ivl:
1.1250 +  "setsum f {Suc m..Suc n} = setsum (%i. f(Suc i)){m..n}"
1.1251 +by (simp add:setsum_shift_bounds_cl_nat_ivl[where k="Suc 0", simplified])
1.1252 +
1.1253 +corollary setsum_shift_bounds_Suc_ivl:
1.1254 +  "setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}"
1.1255 +by (simp add:setsum_shift_bounds_nat_ivl[where k="Suc 0", simplified])
1.1256 +
1.1257 +lemma setsum_shift_lb_Suc0_0:
1.1258 +  "f(0::nat) = (0::nat) \<Longrightarrow> setsum f {Suc 0..k} = setsum f {0..k}"
1.1260 +
1.1261 +lemma setsum_shift_lb_Suc0_0_upt:
1.1262 +  "f(0::nat) = 0 \<Longrightarrow> setsum f {Suc 0..<k} = setsum f {0..<k}"
1.1263 +apply(cases k)apply simp
1.1265 +done
1.1266 +
1.1267 +subsection {* The formula for geometric sums *}
1.1268 +
1.1269 +lemma geometric_sum:
1.1270 +  assumes "x \<noteq> 1"
1.1271 +  shows "(\<Sum>i=0..<n. x ^ i) = (x ^ n - 1) / (x - 1::'a::field)"
1.1272 +proof -
1.1273 +  from assms obtain y where "y = x - 1" and "y \<noteq> 0" by simp_all
1.1274 +  moreover have "(\<Sum>i=0..<n. (y + 1) ^ i) = ((y + 1) ^ n - 1) / y"
1.1275 +  proof (induct n)
1.1276 +    case 0 then show ?case by simp
1.1277 +  next
1.1278 +    case (Suc n)
1.1279 +    moreover with y \<noteq> 0 have "(1 + y) ^ n = (y * inverse y) * (1 + y) ^ n" by simp
1.1280 +    ultimately show ?case by (simp add: field_simps divide_inverse)
1.1281 +  qed
1.1282 +  ultimately show ?thesis by simp
1.1283 +qed
1.1284 +
1.1285 +
1.1286 +subsection {* The formula for arithmetic sums *}
1.1287 +
1.1288 +lemma gauss_sum:
1.1289 +  "(2::'a::comm_semiring_1)*(\<Sum>i\<in>{1..n}. of_nat i) =
1.1290 +   of_nat n*((of_nat n)+1)"
1.1291 +proof (induct n)
1.1292 +  case 0
1.1293 +  show ?case by simp
1.1294 +next
1.1295 +  case (Suc n)
1.1296 +  then show ?case
1.1298 +      (* FIXME: make numeral cancellation simprocs work for semirings *)
1.1299 +qed
1.1300 +
1.1301 +theorem arith_series_general:
1.1302 +  "(2::'a::comm_semiring_1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
1.1303 +  of_nat n * (a + (a + of_nat(n - 1)*d))"
1.1304 +proof cases
1.1305 +  assume ngt1: "n > 1"
1.1306 +  let ?I = "\<lambda>i. of_nat i" and ?n = "of_nat n"
1.1307 +  have
1.1308 +    "(\<Sum>i\<in>{..<n}. a+?I i*d) =
1.1309 +     ((\<Sum>i\<in>{..<n}. a) + (\<Sum>i\<in>{..<n}. ?I i*d))"
1.1310 +    by (rule setsum_addf)
1.1311 +  also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp
1.1312 +  also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))"
1.1313 +    unfolding One_nat_def
1.1314 +    by (simp add: setsum_right_distrib atLeast0LessThan[symmetric] setsum_shift_lb_Suc0_0_upt mult_ac)
1.1315 +  also have "2*\<dots> = 2*?n*a + d*2*(\<Sum>i\<in>{1..<n}. ?I i)"
1.1316 +    by (simp add: algebra_simps)
1.1317 +  also from ngt1 have "{1..<n} = {1..n - 1}"
1.1318 +    by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)
1.1319 +  also from ngt1
1.1320 +  have "2*?n*a + d*2*(\<Sum>i\<in>{1..n - 1}. ?I i) = (2*?n*a + d*?I (n - 1)*?I n)"
1.1321 +    by (simp only: mult_ac gauss_sum [of "n - 1"], unfold One_nat_def)
1.1322 +       (simp add:  mult_ac trans [OF add_commute of_nat_Suc [symmetric]])
1.1323 +  finally show ?thesis
1.1324 +    unfolding mult_2 by (simp add: algebra_simps)
1.1325 +next
1.1326 +  assume "\<not>(n > 1)"
1.1327 +  hence "n = 1 \<or> n = 0" by auto
1.1328 +  thus ?thesis by (auto simp: mult_2)
1.1329 +qed
1.1330 +
1.1331 +lemma arith_series_nat:
1.1332 +  "(2::nat) * (\<Sum>i\<in>{..<n}. a+i*d) = n * (a + (a+(n - 1)*d))"
1.1333 +proof -
1.1334 +  have
1.1335 +    "2 * (\<Sum>i\<in>{..<n::nat}. a + of_nat(i)*d) =
1.1336 +    of_nat(n) * (a + (a + of_nat(n - 1)*d))"
1.1337 +    by (rule arith_series_general)
1.1338 +  thus ?thesis
1.1339 +    unfolding One_nat_def by auto
1.1340 +qed
1.1341 +
1.1342 +lemma arith_series_int:
1.1343 +  "2 * (\<Sum>i\<in>{..<n}. a + int i * d) = int n * (a + (a + int(n - 1)*d))"
1.1344 +  by (fact arith_series_general) (* FIXME: duplicate *)
1.1345 +
1.1346 +lemma sum_diff_distrib:
1.1347 +  fixes P::"nat\<Rightarrow>nat"
1.1348 +  shows
1.1349 +  "\<forall>x. Q x \<le> P x  \<Longrightarrow>
1.1350 +  (\<Sum>x<n. P x) - (\<Sum>x<n. Q x) = (\<Sum>x<n. P x - Q x)"
1.1351 +proof (induct n)
1.1352 +  case 0 show ?case by simp
1.1353 +next
1.1354 +  case (Suc n)
1.1355 +
1.1356 +  let ?lhs = "(\<Sum>x<n. P x) - (\<Sum>x<n. Q x)"
1.1357 +  let ?rhs = "\<Sum>x<n. P x - Q x"
1.1358 +
1.1359 +  from Suc have "?lhs = ?rhs" by simp
1.1360 +  moreover
1.1361 +  from Suc have "?lhs + P n - Q n = ?rhs + (P n - Q n)" by simp
1.1362 +  moreover
1.1363 +  from Suc have
1.1364 +    "(\<Sum>x<n. P x) + P n - ((\<Sum>x<n. Q x) + Q n) = ?rhs + (P n - Q n)"
1.1365 +    by (subst diff_diff_left[symmetric],
1.1366 +        subst diff_add_assoc2)
1.1367 +       (auto simp: diff_add_assoc2 intro: setsum_mono)
1.1368 +  ultimately
1.1369 +  show ?case by simp
1.1370 +qed
1.1371 +
1.1372 +subsection {* Products indexed over intervals *}
1.1373 +
1.1374 +syntax
1.1375 +  "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10)
1.1376 +  "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)
1.1377 +  "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<_./ _)" [0,0,10] 10)
1.1378 +  "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<=_./ _)" [0,0,10] 10)
1.1379 +syntax (xsymbols)
1.1380 +  "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
1.1381 +  "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10)
1.1382 +  "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10)
1.1383 +  "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
1.1384 +syntax (HTML output)
1.1385 +  "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
1.1386 +  "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10)
1.1387 +  "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10)
1.1388 +  "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
1.1389 +syntax (latex_prod output)
1.1390 +  "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
1.1391 + ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)
1.1392 +  "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
1.1393 + ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)
1.1394 +  "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
1.1395 + ("(3\<^raw:$\prod_{>_ < _\<^raw:}$> _)" [0,0,10] 10)
1.1396 +  "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
1.1397 + ("(3\<^raw:$\prod_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10)
1.1398 +
1.1399 +translations
1.1400 +  "\<Prod>x=a..b. t" == "CONST setprod (%x. t) {a..b}"
1.1401 +  "\<Prod>x=a..<b. t" == "CONST setprod (%x. t) {a..<b}"
1.1402 +  "\<Prod>i\<le>n. t" == "CONST setprod (\<lambda>i. t) {..n}"
1.1403 +  "\<Prod>i<n. t" == "CONST setprod (\<lambda>i. t) {..<n}"
1.1404 +
1.1405 +subsection {* Transfer setup *}
1.1406 +
1.1407 +lemma transfer_nat_int_set_functions:
1.1408 +    "{..n} = nat  {0..int n}"
1.1409 +    "{m..n} = nat  {int m..int n}"  (* need all variants of these! *)
1.1410 +  apply (auto simp add: image_def)
1.1411 +  apply (rule_tac x = "int x" in bexI)
1.1412 +  apply auto
1.1413 +  apply (rule_tac x = "int x" in bexI)
1.1414 +  apply auto
1.1415 +  done
1.1416 +
1.1417 +lemma transfer_nat_int_set_function_closures:
1.1418 +    "x >= 0 \<Longrightarrow> nat_set {x..y}"
1.1419 +  by (simp add: nat_set_def)
1.1420 +
1.1421 +declare transfer_morphism_nat_int[transfer add
1.1422 +  return: transfer_nat_int_set_functions
1.1423 +    transfer_nat_int_set_function_closures
1.1424 +]
1.1425 +
1.1426 +lemma transfer_int_nat_set_functions:
1.1427 +    "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int  {nat m..nat n}"
1.1428 +  by (simp only: is_nat_def transfer_nat_int_set_functions
1.1429 +    transfer_nat_int_set_function_closures
1.1430 +    transfer_nat_int_set_return_embed nat_0_le
1.1431 +    cong: transfer_nat_int_set_cong)
1.1432 +
1.1433 +lemma transfer_int_nat_set_function_closures:
1.1434 +    "is_nat x \<Longrightarrow> nat_set {x..y}"
1.1435 +  by (simp only: transfer_nat_int_set_function_closures is_nat_def)
1.1436 +
1.1437 +declare transfer_morphism_int_nat[transfer add
1.1438 +  return: transfer_int_nat_set_functions
1.1439 +    transfer_int_nat_set_function_closures
1.1440 +]
1.1441 +
1.1442 +end
`