src/HOL/Set_Interval.thy
author hoelzl
Thu Jan 31 11:31:27 2013 +0100 (2013-01-31)
changeset 50999 3de230ed0547
parent 50417 f18b92f91818
child 51152 b52cc015429a
permissions -rw-r--r--
introduce order topology
     1 (*  Title:      HOL/Set_Interval.thy
     2     Author:     Tobias Nipkow
     3     Author:     Clemens Ballarin
     4     Author:     Jeremy Avigad
     5 
     6 lessThan, greaterThan, atLeast, atMost and two-sided intervals
     7 *)
     8 
     9 header {* Set intervals *}
    10 
    11 theory Set_Interval
    12 imports Int Nat_Transfer
    13 begin
    14 
    15 context ord
    16 begin
    17 
    18 definition
    19   lessThan    :: "'a => 'a set" ("(1{..<_})") where
    20   "{..<u} == {x. x < u}"
    21 
    22 definition
    23   atMost      :: "'a => 'a set" ("(1{.._})") where
    24   "{..u} == {x. x \<le> u}"
    25 
    26 definition
    27   greaterThan :: "'a => 'a set" ("(1{_<..})") where
    28   "{l<..} == {x. l<x}"
    29 
    30 definition
    31   atLeast     :: "'a => 'a set" ("(1{_..})") where
    32   "{l..} == {x. l\<le>x}"
    33 
    34 definition
    35   greaterThanLessThan :: "'a => 'a => 'a set"  ("(1{_<..<_})") where
    36   "{l<..<u} == {l<..} Int {..<u}"
    37 
    38 definition
    39   atLeastLessThan :: "'a => 'a => 'a set"      ("(1{_..<_})") where
    40   "{l..<u} == {l..} Int {..<u}"
    41 
    42 definition
    43   greaterThanAtMost :: "'a => 'a => 'a set"    ("(1{_<.._})") where
    44   "{l<..u} == {l<..} Int {..u}"
    45 
    46 definition
    47   atLeastAtMost :: "'a => 'a => 'a set"        ("(1{_.._})") where
    48   "{l..u} == {l..} Int {..u}"
    49 
    50 end
    51 
    52 
    53 text{* A note of warning when using @{term"{..<n}"} on type @{typ
    54 nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving
    55 @{term"{m..<n}"} may not exist in @{term"{..<n}"}-form as well. *}
    56 
    57 syntax
    58   "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3UN _<=_./ _)" [0, 0, 10] 10)
    59   "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3UN _<_./ _)" [0, 0, 10] 10)
    60   "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3INT _<=_./ _)" [0, 0, 10] 10)
    61   "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3INT _<_./ _)" [0, 0, 10] 10)
    62 
    63 syntax (xsymbols)
    64   "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _\<le>_./ _)" [0, 0, 10] 10)
    65   "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Union> _<_./ _)" [0, 0, 10] 10)
    66   "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _\<le>_./ _)" [0, 0, 10] 10)
    67   "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" [0, 0, 10] 10)
    68 
    69 syntax (latex output)
    70   "_UNION_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ \<le> _)/ _)" [0, 0, 10] 10)
    71   "_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ < _)/ _)" [0, 0, 10] 10)
    72   "_INTER_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ \<le> _)/ _)" [0, 0, 10] 10)
    73   "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ < _)/ _)" [0, 0, 10] 10)
    74 
    75 translations
    76   "UN i<=n. A"  == "UN i:{..n}. A"
    77   "UN i<n. A"   == "UN i:{..<n}. A"
    78   "INT i<=n. A" == "INT i:{..n}. A"
    79   "INT i<n. A"  == "INT i:{..<n}. A"
    80 
    81 
    82 subsection {* Various equivalences *}
    83 
    84 lemma (in ord) lessThan_iff [iff]: "(i: lessThan k) = (i<k)"
    85 by (simp add: lessThan_def)
    86 
    87 lemma Compl_lessThan [simp]:
    88     "!!k:: 'a::linorder. -lessThan k = atLeast k"
    89 apply (auto simp add: lessThan_def atLeast_def)
    90 done
    91 
    92 lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k} - lessThan k = {k}"
    93 by auto
    94 
    95 lemma (in ord) greaterThan_iff [iff]: "(i: greaterThan k) = (k<i)"
    96 by (simp add: greaterThan_def)
    97 
    98 lemma Compl_greaterThan [simp]:
    99     "!!k:: 'a::linorder. -greaterThan k = atMost k"
   100   by (auto simp add: greaterThan_def atMost_def)
   101 
   102 lemma Compl_atMost [simp]: "!!k:: 'a::linorder. -atMost k = greaterThan k"
   103 apply (subst Compl_greaterThan [symmetric])
   104 apply (rule double_complement)
   105 done
   106 
   107 lemma (in ord) atLeast_iff [iff]: "(i: atLeast k) = (k<=i)"
   108 by (simp add: atLeast_def)
   109 
   110 lemma Compl_atLeast [simp]:
   111     "!!k:: 'a::linorder. -atLeast k = lessThan k"
   112   by (auto simp add: lessThan_def atLeast_def)
   113 
   114 lemma (in ord) atMost_iff [iff]: "(i: atMost k) = (i<=k)"
   115 by (simp add: atMost_def)
   116 
   117 lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"
   118 by (blast intro: order_antisym)
   119 
   120 lemma (in linorder) lessThan_Int_lessThan: "{ a <..} \<inter> { b <..} = { max a b <..}"
   121   by auto
   122 
   123 lemma (in linorder) greaterThan_Int_greaterThan: "{..< a} \<inter> {..< b} = {..< min a b}"
   124   by auto
   125 
   126 subsection {* Logical Equivalences for Set Inclusion and Equality *}
   127 
   128 lemma atLeast_subset_iff [iff]:
   129      "(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))"
   130 by (blast intro: order_trans)
   131 
   132 lemma atLeast_eq_iff [iff]:
   133      "(atLeast x = atLeast y) = (x = (y::'a::linorder))"
   134 by (blast intro: order_antisym order_trans)
   135 
   136 lemma greaterThan_subset_iff [iff]:
   137      "(greaterThan x \<subseteq> greaterThan y) = (y \<le> (x::'a::linorder))"
   138 apply (auto simp add: greaterThan_def)
   139  apply (subst linorder_not_less [symmetric], blast)
   140 done
   141 
   142 lemma greaterThan_eq_iff [iff]:
   143      "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))"
   144 apply (rule iffI)
   145  apply (erule equalityE)
   146  apply simp_all
   147 done
   148 
   149 lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))"
   150 by (blast intro: order_trans)
   151 
   152 lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))"
   153 by (blast intro: order_antisym order_trans)
   154 
   155 lemma lessThan_subset_iff [iff]:
   156      "(lessThan x \<subseteq> lessThan y) = (x \<le> (y::'a::linorder))"
   157 apply (auto simp add: lessThan_def)
   158  apply (subst linorder_not_less [symmetric], blast)
   159 done
   160 
   161 lemma lessThan_eq_iff [iff]:
   162      "(lessThan x = lessThan y) = (x = (y::'a::linorder))"
   163 apply (rule iffI)
   164  apply (erule equalityE)
   165  apply simp_all
   166 done
   167 
   168 lemma lessThan_strict_subset_iff:
   169   fixes m n :: "'a::linorder"
   170   shows "{..<m} < {..<n} \<longleftrightarrow> m < n"
   171   by (metis leD lessThan_subset_iff linorder_linear not_less_iff_gr_or_eq psubset_eq)
   172 
   173 subsection {*Two-sided intervals*}
   174 
   175 context ord
   176 begin
   177 
   178 lemma greaterThanLessThan_iff [simp,no_atp]:
   179   "(i : {l<..<u}) = (l < i & i < u)"
   180 by (simp add: greaterThanLessThan_def)
   181 
   182 lemma atLeastLessThan_iff [simp,no_atp]:
   183   "(i : {l..<u}) = (l <= i & i < u)"
   184 by (simp add: atLeastLessThan_def)
   185 
   186 lemma greaterThanAtMost_iff [simp,no_atp]:
   187   "(i : {l<..u}) = (l < i & i <= u)"
   188 by (simp add: greaterThanAtMost_def)
   189 
   190 lemma atLeastAtMost_iff [simp,no_atp]:
   191   "(i : {l..u}) = (l <= i & i <= u)"
   192 by (simp add: atLeastAtMost_def)
   193 
   194 text {* The above four lemmas could be declared as iffs. Unfortunately this
   195 breaks many proofs. Since it only helps blast, it is better to leave well
   196 alone *}
   197 
   198 lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} \<inter> {..< b }"
   199   by auto
   200 
   201 end
   202 
   203 subsubsection{* Emptyness, singletons, subset *}
   204 
   205 context order
   206 begin
   207 
   208 lemma atLeastatMost_empty[simp]:
   209   "b < a \<Longrightarrow> {a..b} = {}"
   210 by(auto simp: atLeastAtMost_def atLeast_def atMost_def)
   211 
   212 lemma atLeastatMost_empty_iff[simp]:
   213   "{a..b} = {} \<longleftrightarrow> (~ a <= b)"
   214 by auto (blast intro: order_trans)
   215 
   216 lemma atLeastatMost_empty_iff2[simp]:
   217   "{} = {a..b} \<longleftrightarrow> (~ a <= b)"
   218 by auto (blast intro: order_trans)
   219 
   220 lemma atLeastLessThan_empty[simp]:
   221   "b <= a \<Longrightarrow> {a..<b} = {}"
   222 by(auto simp: atLeastLessThan_def)
   223 
   224 lemma atLeastLessThan_empty_iff[simp]:
   225   "{a..<b} = {} \<longleftrightarrow> (~ a < b)"
   226 by auto (blast intro: le_less_trans)
   227 
   228 lemma atLeastLessThan_empty_iff2[simp]:
   229   "{} = {a..<b} \<longleftrightarrow> (~ a < b)"
   230 by auto (blast intro: le_less_trans)
   231 
   232 lemma greaterThanAtMost_empty[simp]: "l \<le> k ==> {k<..l} = {}"
   233 by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)
   234 
   235 lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \<longleftrightarrow> ~ k < l"
   236 by auto (blast intro: less_le_trans)
   237 
   238 lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \<longleftrightarrow> ~ k < l"
   239 by auto (blast intro: less_le_trans)
   240 
   241 lemma greaterThanLessThan_empty[simp]:"l \<le> k ==> {k<..<l} = {}"
   242 by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def)
   243 
   244 lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}"
   245 by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)
   246 
   247 lemma atLeastAtMost_singleton': "a = b \<Longrightarrow> {a .. b} = {a}" by simp
   248 
   249 lemma atLeastatMost_subset_iff[simp]:
   250   "{a..b} <= {c..d} \<longleftrightarrow> (~ a <= b) | c <= a & b <= d"
   251 unfolding atLeastAtMost_def atLeast_def atMost_def
   252 by (blast intro: order_trans)
   253 
   254 lemma atLeastatMost_psubset_iff:
   255   "{a..b} < {c..d} \<longleftrightarrow>
   256    ((~ a <= b) | c <= a & b <= d & (c < a | b < d))  &  c <= d"
   257 by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans)
   258 
   259 lemma atLeastAtMost_singleton_iff[simp]:
   260   "{a .. b} = {c} \<longleftrightarrow> a = b \<and> b = c"
   261 proof
   262   assume "{a..b} = {c}"
   263   hence "\<not> (\<not> a \<le> b)" unfolding atLeastatMost_empty_iff[symmetric] by simp
   264   moreover with `{a..b} = {c}` have "c \<le> a \<and> b \<le> c" by auto
   265   ultimately show "a = b \<and> b = c" by auto
   266 qed simp
   267 
   268 end
   269 
   270 context dense_linorder
   271 begin
   272 
   273 lemma greaterThanLessThan_empty_iff[simp]:
   274   "{ a <..< b } = {} \<longleftrightarrow> b \<le> a"
   275   using dense[of a b] by (cases "a < b") auto
   276 
   277 lemma greaterThanLessThan_empty_iff2[simp]:
   278   "{} = { a <..< b } \<longleftrightarrow> b \<le> a"
   279   using dense[of a b] by (cases "a < b") auto
   280 
   281 lemma atLeastLessThan_subseteq_atLeastAtMost_iff:
   282   "{a ..< b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)"
   283   using dense[of "max a d" "b"]
   284   by (force simp: subset_eq Ball_def not_less[symmetric])
   285 
   286 lemma greaterThanAtMost_subseteq_atLeastAtMost_iff:
   287   "{a <.. b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)"
   288   using dense[of "a" "min c b"]
   289   by (force simp: subset_eq Ball_def not_less[symmetric])
   290 
   291 lemma greaterThanLessThan_subseteq_atLeastAtMost_iff:
   292   "{a <..< b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)"
   293   using dense[of "a" "min c b"] dense[of "max a d" "b"]
   294   by (force simp: subset_eq Ball_def not_less[symmetric])
   295 
   296 lemma atLeastAtMost_subseteq_atLeastLessThan_iff:
   297   "{a .. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a \<le> b \<longrightarrow> c \<le> a \<and> b < d)"
   298   using dense[of "max a d" "b"]
   299   by (force simp: subset_eq Ball_def not_less[symmetric])
   300 
   301 lemma greaterThanAtMost_subseteq_atLeastLessThan_iff:
   302   "{a <.. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b < d)"
   303   using dense[of "a" "min c b"]
   304   by (force simp: subset_eq Ball_def not_less[symmetric])
   305 
   306 lemma greaterThanLessThan_subseteq_atLeastLessThan_iff:
   307   "{a <..< b} \<subseteq> { c ..< d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)"
   308   using dense[of "a" "min c b"] dense[of "max a d" "b"]
   309   by (force simp: subset_eq Ball_def not_less[symmetric])
   310 
   311 end
   312 
   313 lemma (in linorder) atLeastLessThan_subset_iff:
   314   "{a..<b} <= {c..<d} \<Longrightarrow> b <= a | c<=a & b<=d"
   315 apply (auto simp:subset_eq Ball_def)
   316 apply(frule_tac x=a in spec)
   317 apply(erule_tac x=d in allE)
   318 apply (simp add: less_imp_le)
   319 done
   320 
   321 lemma atLeastLessThan_inj:
   322   fixes a b c d :: "'a::linorder"
   323   assumes eq: "{a ..< b} = {c ..< d}" and "a < b" "c < d"
   324   shows "a = c" "b = d"
   325 using assms by (metis atLeastLessThan_subset_iff eq less_le_not_le linorder_antisym_conv2 subset_refl)+
   326 
   327 lemma atLeastLessThan_eq_iff:
   328   fixes a b c d :: "'a::linorder"
   329   assumes "a < b" "c < d"
   330   shows "{a ..< b} = {c ..< d} \<longleftrightarrow> a = c \<and> b = d"
   331   using atLeastLessThan_inj assms by auto
   332 
   333 subsubsection {* Intersection *}
   334 
   335 context linorder
   336 begin
   337 
   338 lemma Int_atLeastAtMost[simp]: "{a..b} Int {c..d} = {max a c .. min b d}"
   339 by auto
   340 
   341 lemma Int_atLeastAtMostR1[simp]: "{..b} Int {c..d} = {c .. min b d}"
   342 by auto
   343 
   344 lemma Int_atLeastAtMostR2[simp]: "{a..} Int {c..d} = {max a c .. d}"
   345 by auto
   346 
   347 lemma Int_atLeastAtMostL1[simp]: "{a..b} Int {..d} = {a .. min b d}"
   348 by auto
   349 
   350 lemma Int_atLeastAtMostL2[simp]: "{a..b} Int {c..} = {max a c .. b}"
   351 by auto
   352 
   353 lemma Int_atLeastLessThan[simp]: "{a..<b} Int {c..<d} = {max a c ..< min b d}"
   354 by auto
   355 
   356 lemma Int_greaterThanAtMost[simp]: "{a<..b} Int {c<..d} = {max a c <.. min b d}"
   357 by auto
   358 
   359 lemma Int_greaterThanLessThan[simp]: "{a<..<b} Int {c<..<d} = {max a c <..< min b d}"
   360 by auto
   361 
   362 lemma Int_atMost[simp]: "{..a} \<inter> {..b} = {.. min a b}"
   363   by (auto simp: min_def)
   364 
   365 end
   366 
   367 
   368 subsection {* Intervals of natural numbers *}
   369 
   370 subsubsection {* The Constant @{term lessThan} *}
   371 
   372 lemma lessThan_0 [simp]: "lessThan (0::nat) = {}"
   373 by (simp add: lessThan_def)
   374 
   375 lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"
   376 by (simp add: lessThan_def less_Suc_eq, blast)
   377 
   378 text {* The following proof is convenient in induction proofs where
   379 new elements get indices at the beginning. So it is used to transform
   380 @{term "{..<Suc n}"} to @{term "0::nat"} and @{term "{..< n}"}. *}
   381 
   382 lemma lessThan_Suc_eq_insert_0: "{..<Suc n} = insert 0 (Suc ` {..<n})"
   383 proof safe
   384   fix x assume "x < Suc n" "x \<notin> Suc ` {..<n}"
   385   then have "x \<noteq> Suc (x - 1)" by auto
   386   with `x < Suc n` show "x = 0" by auto
   387 qed
   388 
   389 lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"
   390 by (simp add: lessThan_def atMost_def less_Suc_eq_le)
   391 
   392 lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"
   393 by blast
   394 
   395 subsubsection {* The Constant @{term greaterThan} *}
   396 
   397 lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc"
   398 apply (simp add: greaterThan_def)
   399 apply (blast dest: gr0_conv_Suc [THEN iffD1])
   400 done
   401 
   402 lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}"
   403 apply (simp add: greaterThan_def)
   404 apply (auto elim: linorder_neqE)
   405 done
   406 
   407 lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"
   408 by blast
   409 
   410 subsubsection {* The Constant @{term atLeast} *}
   411 
   412 lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV"
   413 by (unfold atLeast_def UNIV_def, simp)
   414 
   415 lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}"
   416 apply (simp add: atLeast_def)
   417 apply (simp add: Suc_le_eq)
   418 apply (simp add: order_le_less, blast)
   419 done
   420 
   421 lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k"
   422   by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le)
   423 
   424 lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"
   425 by blast
   426 
   427 subsubsection {* The Constant @{term atMost} *}
   428 
   429 lemma atMost_0 [simp]: "atMost (0::nat) = {0}"
   430 by (simp add: atMost_def)
   431 
   432 lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"
   433 apply (simp add: atMost_def)
   434 apply (simp add: less_Suc_eq order_le_less, blast)
   435 done
   436 
   437 lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
   438 by blast
   439 
   440 subsubsection {* The Constant @{term atLeastLessThan} *}
   441 
   442 text{*The orientation of the following 2 rules is tricky. The lhs is
   443 defined in terms of the rhs.  Hence the chosen orientation makes sense
   444 in this theory --- the reverse orientation complicates proofs (eg
   445 nontermination). But outside, when the definition of the lhs is rarely
   446 used, the opposite orientation seems preferable because it reduces a
   447 specific concept to a more general one. *}
   448 
   449 lemma atLeast0LessThan: "{0::nat..<n} = {..<n}"
   450 by(simp add:lessThan_def atLeastLessThan_def)
   451 
   452 lemma atLeast0AtMost: "{0..n::nat} = {..n}"
   453 by(simp add:atMost_def atLeastAtMost_def)
   454 
   455 declare atLeast0LessThan[symmetric, code_unfold]
   456         atLeast0AtMost[symmetric, code_unfold]
   457 
   458 lemma atLeastLessThan0: "{m..<0::nat} = {}"
   459 by (simp add: atLeastLessThan_def)
   460 
   461 subsubsection {* Intervals of nats with @{term Suc} *}
   462 
   463 text{*Not a simprule because the RHS is too messy.*}
   464 lemma atLeastLessThanSuc:
   465     "{m..<Suc n} = (if m \<le> n then insert n {m..<n} else {})"
   466 by (auto simp add: atLeastLessThan_def)
   467 
   468 lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}"
   469 by (auto simp add: atLeastLessThan_def)
   470 (*
   471 lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}"
   472 by (induct k, simp_all add: atLeastLessThanSuc)
   473 
   474 lemma atLeastSucLessThan [simp]: "{Suc n..<n} = {}"
   475 by (auto simp add: atLeastLessThan_def)
   476 *)
   477 lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}"
   478   by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def)
   479 
   480 lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {l<..u}"
   481   by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def
   482     greaterThanAtMost_def)
   483 
   484 lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..<u} = {l<..<u}"
   485   by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def
   486     greaterThanLessThan_def)
   487 
   488 lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}"
   489 by (auto simp add: atLeastAtMost_def)
   490 
   491 lemma atLeastAtMost_insertL: "m \<le> n \<Longrightarrow> insert m {Suc m..n} = {m ..n}"
   492 by auto
   493 
   494 text {* The analogous result is useful on @{typ int}: *}
   495 (* here, because we don't have an own int section *)
   496 lemma atLeastAtMostPlus1_int_conv:
   497   "m <= 1+n \<Longrightarrow> {m..1+n} = insert (1+n) {m..n::int}"
   498   by (auto intro: set_eqI)
   499 
   500 lemma atLeastLessThan_add_Un: "i \<le> j \<Longrightarrow> {i..<j+k} = {i..<j} \<union> {j..<j+k::nat}"
   501   apply (induct k) 
   502   apply (simp_all add: atLeastLessThanSuc)   
   503   done
   504 
   505 subsubsection {* Image *}
   506 
   507 lemma image_add_atLeastAtMost:
   508   "(%n::nat. n+k) ` {i..j} = {i+k..j+k}" (is "?A = ?B")
   509 proof
   510   show "?A \<subseteq> ?B" by auto
   511 next
   512   show "?B \<subseteq> ?A"
   513   proof
   514     fix n assume a: "n : ?B"
   515     hence "n - k : {i..j}" by auto
   516     moreover have "n = (n - k) + k" using a by auto
   517     ultimately show "n : ?A" by blast
   518   qed
   519 qed
   520 
   521 lemma image_add_atLeastLessThan:
   522   "(%n::nat. n+k) ` {i..<j} = {i+k..<j+k}" (is "?A = ?B")
   523 proof
   524   show "?A \<subseteq> ?B" by auto
   525 next
   526   show "?B \<subseteq> ?A"
   527   proof
   528     fix n assume a: "n : ?B"
   529     hence "n - k : {i..<j}" by auto
   530     moreover have "n = (n - k) + k" using a by auto
   531     ultimately show "n : ?A" by blast
   532   qed
   533 qed
   534 
   535 corollary image_Suc_atLeastAtMost[simp]:
   536   "Suc ` {i..j} = {Suc i..Suc j}"
   537 using image_add_atLeastAtMost[where k="Suc 0"] by simp
   538 
   539 corollary image_Suc_atLeastLessThan[simp]:
   540   "Suc ` {i..<j} = {Suc i..<Suc j}"
   541 using image_add_atLeastLessThan[where k="Suc 0"] by simp
   542 
   543 lemma image_add_int_atLeastLessThan:
   544     "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
   545   apply (auto simp add: image_def)
   546   apply (rule_tac x = "x - l" in bexI)
   547   apply auto
   548   done
   549 
   550 lemma image_minus_const_atLeastLessThan_nat:
   551   fixes c :: nat
   552   shows "(\<lambda>i. i - c) ` {x ..< y} =
   553       (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"
   554     (is "_ = ?right")
   555 proof safe
   556   fix a assume a: "a \<in> ?right"
   557   show "a \<in> (\<lambda>i. i - c) ` {x ..< y}"
   558   proof cases
   559     assume "c < y" with a show ?thesis
   560       by (auto intro!: image_eqI[of _ _ "a + c"])
   561   next
   562     assume "\<not> c < y" with a show ?thesis
   563       by (auto intro!: image_eqI[of _ _ x] split: split_if_asm)
   564   qed
   565 qed auto
   566 
   567 context ordered_ab_group_add
   568 begin
   569 
   570 lemma
   571   fixes x :: 'a
   572   shows image_uminus_greaterThan[simp]: "uminus ` {x<..} = {..<-x}"
   573   and image_uminus_atLeast[simp]: "uminus ` {x..} = {..-x}"
   574 proof safe
   575   fix y assume "y < -x"
   576   hence *:  "x < -y" using neg_less_iff_less[of "-y" x] by simp
   577   have "- (-y) \<in> uminus ` {x<..}"
   578     by (rule imageI) (simp add: *)
   579   thus "y \<in> uminus ` {x<..}" by simp
   580 next
   581   fix y assume "y \<le> -x"
   582   have "- (-y) \<in> uminus ` {x..}"
   583     by (rule imageI) (insert `y \<le> -x`[THEN le_imp_neg_le], simp)
   584   thus "y \<in> uminus ` {x..}" by simp
   585 qed simp_all
   586 
   587 lemma
   588   fixes x :: 'a
   589   shows image_uminus_lessThan[simp]: "uminus ` {..<x} = {-x<..}"
   590   and image_uminus_atMost[simp]: "uminus ` {..x} = {-x..}"
   591 proof -
   592   have "uminus ` {..<x} = uminus ` uminus ` {-x<..}"
   593     and "uminus ` {..x} = uminus ` uminus ` {-x..}" by simp_all
   594   thus "uminus ` {..<x} = {-x<..}" and "uminus ` {..x} = {-x..}"
   595     by (simp_all add: image_image
   596         del: image_uminus_greaterThan image_uminus_atLeast)
   597 qed
   598 
   599 lemma
   600   fixes x :: 'a
   601   shows image_uminus_atLeastAtMost[simp]: "uminus ` {x..y} = {-y..-x}"
   602   and image_uminus_greaterThanAtMost[simp]: "uminus ` {x<..y} = {-y..<-x}"
   603   and image_uminus_atLeastLessThan[simp]: "uminus ` {x..<y} = {-y<..-x}"
   604   and image_uminus_greaterThanLessThan[simp]: "uminus ` {x<..<y} = {-y<..<-x}"
   605   by (simp_all add: atLeastAtMost_def greaterThanAtMost_def atLeastLessThan_def
   606       greaterThanLessThan_def image_Int[OF inj_uminus] Int_commute)
   607 end
   608 
   609 subsubsection {* Finiteness *}
   610 
   611 lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}"
   612   by (induct k) (simp_all add: lessThan_Suc)
   613 
   614 lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}"
   615   by (induct k) (simp_all add: atMost_Suc)
   616 
   617 lemma finite_greaterThanLessThan [iff]:
   618   fixes l :: nat shows "finite {l<..<u}"
   619 by (simp add: greaterThanLessThan_def)
   620 
   621 lemma finite_atLeastLessThan [iff]:
   622   fixes l :: nat shows "finite {l..<u}"
   623 by (simp add: atLeastLessThan_def)
   624 
   625 lemma finite_greaterThanAtMost [iff]:
   626   fixes l :: nat shows "finite {l<..u}"
   627 by (simp add: greaterThanAtMost_def)
   628 
   629 lemma finite_atLeastAtMost [iff]:
   630   fixes l :: nat shows "finite {l..u}"
   631 by (simp add: atLeastAtMost_def)
   632 
   633 text {* A bounded set of natural numbers is finite. *}
   634 lemma bounded_nat_set_is_finite:
   635   "(ALL i:N. i < (n::nat)) ==> finite N"
   636 apply (rule finite_subset)
   637  apply (rule_tac [2] finite_lessThan, auto)
   638 done
   639 
   640 text {* A set of natural numbers is finite iff it is bounded. *}
   641 lemma finite_nat_set_iff_bounded:
   642   "finite(N::nat set) = (EX m. ALL n:N. n<m)" (is "?F = ?B")
   643 proof
   644   assume f:?F  show ?B
   645     using Max_ge[OF `?F`, simplified less_Suc_eq_le[symmetric]] by blast
   646 next
   647   assume ?B show ?F using `?B` by(blast intro:bounded_nat_set_is_finite)
   648 qed
   649 
   650 lemma finite_nat_set_iff_bounded_le:
   651   "finite(N::nat set) = (EX m. ALL n:N. n<=m)"
   652 apply(simp add:finite_nat_set_iff_bounded)
   653 apply(blast dest:less_imp_le_nat le_imp_less_Suc)
   654 done
   655 
   656 lemma finite_less_ub:
   657      "!!f::nat=>nat. (!!n. n \<le> f n) ==> finite {n. f n \<le> u}"
   658 by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)
   659 
   660 text{* Any subset of an interval of natural numbers the size of the
   661 subset is exactly that interval. *}
   662 
   663 lemma subset_card_intvl_is_intvl:
   664   "A <= {k..<k+card A} \<Longrightarrow> A = {k..<k+card A}" (is "PROP ?P")
   665 proof cases
   666   assume "finite A"
   667   thus "PROP ?P"
   668   proof(induct A rule:finite_linorder_max_induct)
   669     case empty thus ?case by auto
   670   next
   671     case (insert b A)
   672     moreover hence "b ~: A" by auto
   673     moreover have "A <= {k..<k+card A}" and "b = k+card A"
   674       using `b ~: A` insert by fastforce+
   675     ultimately show ?case by auto
   676   qed
   677 next
   678   assume "~finite A" thus "PROP ?P" by simp
   679 qed
   680 
   681 
   682 subsubsection {* Proving Inclusions and Equalities between Unions *}
   683 
   684 lemma UN_le_eq_Un0:
   685   "(\<Union>i\<le>n::nat. M i) = (\<Union>i\<in>{1..n}. M i) \<union> M 0" (is "?A = ?B")
   686 proof
   687   show "?A <= ?B"
   688   proof
   689     fix x assume "x : ?A"
   690     then obtain i where i: "i\<le>n" "x : M i" by auto
   691     show "x : ?B"
   692     proof(cases i)
   693       case 0 with i show ?thesis by simp
   694     next
   695       case (Suc j) with i show ?thesis by auto
   696     qed
   697   qed
   698 next
   699   show "?B <= ?A" by auto
   700 qed
   701 
   702 lemma UN_le_add_shift:
   703   "(\<Union>i\<le>n::nat. M(i+k)) = (\<Union>i\<in>{k..n+k}. M i)" (is "?A = ?B")
   704 proof
   705   show "?A <= ?B" by fastforce
   706 next
   707   show "?B <= ?A"
   708   proof
   709     fix x assume "x : ?B"
   710     then obtain i where i: "i : {k..n+k}" "x : M(i)" by auto
   711     hence "i-k\<le>n & x : M((i-k)+k)" by auto
   712     thus "x : ?A" by blast
   713   qed
   714 qed
   715 
   716 lemma UN_UN_finite_eq: "(\<Union>n::nat. \<Union>i\<in>{0..<n}. A i) = (\<Union>n. A n)"
   717   by (auto simp add: atLeast0LessThan) 
   718 
   719 lemma UN_finite_subset: "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> C) \<Longrightarrow> (\<Union>n. A n) \<subseteq> C"
   720   by (subst UN_UN_finite_eq [symmetric]) blast
   721 
   722 lemma UN_finite2_subset: 
   723      "(!!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)"
   724   apply (rule UN_finite_subset)
   725   apply (subst UN_UN_finite_eq [symmetric, of B]) 
   726   apply blast
   727   done
   728 
   729 lemma UN_finite2_eq:
   730   "(!!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)"
   731   apply (rule subset_antisym)
   732    apply (rule UN_finite2_subset, blast)
   733  apply (rule UN_finite2_subset [where k=k])
   734  apply (force simp add: atLeastLessThan_add_Un [of 0])
   735  done
   736 
   737 
   738 subsubsection {* Cardinality *}
   739 
   740 lemma card_lessThan [simp]: "card {..<u} = u"
   741   by (induct u, simp_all add: lessThan_Suc)
   742 
   743 lemma card_atMost [simp]: "card {..u} = Suc u"
   744   by (simp add: lessThan_Suc_atMost [THEN sym])
   745 
   746 lemma card_atLeastLessThan [simp]: "card {l..<u} = u - l"
   747   apply (subgoal_tac "card {l..<u} = card {..<u-l}")
   748   apply (erule ssubst, rule card_lessThan)
   749   apply (subgoal_tac "(%x. x + l) ` {..<u-l} = {l..<u}")
   750   apply (erule subst)
   751   apply (rule card_image)
   752   apply (simp add: inj_on_def)
   753   apply (auto simp add: image_def atLeastLessThan_def lessThan_def)
   754   apply (rule_tac x = "x - l" in exI)
   755   apply arith
   756   done
   757 
   758 lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l"
   759   by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp)
   760 
   761 lemma card_greaterThanAtMost [simp]: "card {l<..u} = u - l"
   762   by (subst atLeastSucAtMost_greaterThanAtMost [THEN sym], simp)
   763 
   764 lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u - Suc l"
   765   by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp)
   766 
   767 lemma ex_bij_betw_nat_finite:
   768   "finite M \<Longrightarrow> \<exists>h. bij_betw h {0..<card M} M"
   769 apply(drule finite_imp_nat_seg_image_inj_on)
   770 apply(auto simp:atLeast0LessThan[symmetric] lessThan_def[symmetric] card_image bij_betw_def)
   771 done
   772 
   773 lemma ex_bij_betw_finite_nat:
   774   "finite M \<Longrightarrow> \<exists>h. bij_betw h M {0..<card M}"
   775 by (blast dest: ex_bij_betw_nat_finite bij_betw_inv)
   776 
   777 lemma finite_same_card_bij:
   778   "finite A \<Longrightarrow> finite B \<Longrightarrow> card A = card B \<Longrightarrow> EX h. bij_betw h A B"
   779 apply(drule ex_bij_betw_finite_nat)
   780 apply(drule ex_bij_betw_nat_finite)
   781 apply(auto intro!:bij_betw_trans)
   782 done
   783 
   784 lemma ex_bij_betw_nat_finite_1:
   785   "finite M \<Longrightarrow> \<exists>h. bij_betw h {1 .. card M} M"
   786 by (rule finite_same_card_bij) auto
   787 
   788 lemma bij_betw_iff_card:
   789   assumes FIN: "finite A" and FIN': "finite B"
   790   shows BIJ: "(\<exists>f. bij_betw f A B) \<longleftrightarrow> (card A = card B)"
   791 using assms
   792 proof(auto simp add: bij_betw_same_card)
   793   assume *: "card A = card B"
   794   obtain f where "bij_betw f A {0 ..< card A}"
   795   using FIN ex_bij_betw_finite_nat by blast
   796   moreover obtain g where "bij_betw g {0 ..< card B} B"
   797   using FIN' ex_bij_betw_nat_finite by blast
   798   ultimately have "bij_betw (g o f) A B"
   799   using * by (auto simp add: bij_betw_trans)
   800   thus "(\<exists>f. bij_betw f A B)" by blast
   801 qed
   802 
   803 lemma inj_on_iff_card_le:
   804   assumes FIN: "finite A" and FIN': "finite B"
   805   shows "(\<exists>f. inj_on f A \<and> f ` A \<le> B) = (card A \<le> card B)"
   806 proof (safe intro!: card_inj_on_le)
   807   assume *: "card A \<le> card B"
   808   obtain f where 1: "inj_on f A" and 2: "f ` A = {0 ..< card A}"
   809   using FIN ex_bij_betw_finite_nat unfolding bij_betw_def by force
   810   moreover obtain g where "inj_on g {0 ..< card B}" and 3: "g ` {0 ..< card B} = B"
   811   using FIN' ex_bij_betw_nat_finite unfolding bij_betw_def by force
   812   ultimately have "inj_on g (f ` A)" using subset_inj_on[of g _ "f ` A"] * by force
   813   hence "inj_on (g o f) A" using 1 comp_inj_on by blast
   814   moreover
   815   {have "{0 ..< card A} \<le> {0 ..< card B}" using * by force
   816    with 2 have "f ` A  \<le> {0 ..< card B}" by blast
   817    hence "(g o f) ` A \<le> B" unfolding comp_def using 3 by force
   818   }
   819   ultimately show "(\<exists>f. inj_on f A \<and> f ` A \<le> B)" by blast
   820 qed (insert assms, auto)
   821 
   822 subsection {* Intervals of integers *}
   823 
   824 lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..<u+1} = {l..(u::int)}"
   825   by (auto simp add: atLeastAtMost_def atLeastLessThan_def)
   826 
   827 lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}"
   828   by (auto simp add: atLeastAtMost_def greaterThanAtMost_def)
   829 
   830 lemma atLeastPlusOneLessThan_greaterThanLessThan_int:
   831     "{l+1..<u} = {l<..<u::int}"
   832   by (auto simp add: atLeastLessThan_def greaterThanLessThan_def)
   833 
   834 subsubsection {* Finiteness *}
   835 
   836 lemma image_atLeastZeroLessThan_int: "0 \<le> u ==>
   837     {(0::int)..<u} = int ` {..<nat u}"
   838   apply (unfold image_def lessThan_def)
   839   apply auto
   840   apply (rule_tac x = "nat x" in exI)
   841   apply (auto simp add: zless_nat_eq_int_zless [THEN sym])
   842   done
   843 
   844 lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}"
   845   apply (cases "0 \<le> u")
   846   apply (subst image_atLeastZeroLessThan_int, assumption)
   847   apply (rule finite_imageI)
   848   apply auto
   849   done
   850 
   851 lemma finite_atLeastLessThan_int [iff]: "finite {l..<u::int}"
   852   apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}")
   853   apply (erule subst)
   854   apply (rule finite_imageI)
   855   apply (rule finite_atLeastZeroLessThan_int)
   856   apply (rule image_add_int_atLeastLessThan)
   857   done
   858 
   859 lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}"
   860   by (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym], simp)
   861 
   862 lemma finite_greaterThanAtMost_int [iff]: "finite {l<..(u::int)}"
   863   by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
   864 
   865 lemma finite_greaterThanLessThan_int [iff]: "finite {l<..<u::int}"
   866   by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
   867 
   868 
   869 subsubsection {* Cardinality *}
   870 
   871 lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u"
   872   apply (cases "0 \<le> u")
   873   apply (subst image_atLeastZeroLessThan_int, assumption)
   874   apply (subst card_image)
   875   apply (auto simp add: inj_on_def)
   876   done
   877 
   878 lemma card_atLeastLessThan_int [simp]: "card {l..<u} = nat (u - l)"
   879   apply (subgoal_tac "card {l..<u} = card {0..<u-l}")
   880   apply (erule ssubst, rule card_atLeastZeroLessThan_int)
   881   apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}")
   882   apply (erule subst)
   883   apply (rule card_image)
   884   apply (simp add: inj_on_def)
   885   apply (rule image_add_int_atLeastLessThan)
   886   done
   887 
   888 lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u - l + 1)"
   889 apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym])
   890 apply (auto simp add: algebra_simps)
   891 done
   892 
   893 lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u - l)"
   894 by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
   895 
   896 lemma card_greaterThanLessThan_int [simp]: "card {l<..<u} = nat (u - (l + 1))"
   897 by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
   898 
   899 lemma finite_M_bounded_by_nat: "finite {k. P k \<and> k < (i::nat)}"
   900 proof -
   901   have "{k. P k \<and> k < i} \<subseteq> {..<i}" by auto
   902   with finite_lessThan[of "i"] show ?thesis by (simp add: finite_subset)
   903 qed
   904 
   905 lemma card_less:
   906 assumes zero_in_M: "0 \<in> M"
   907 shows "card {k \<in> M. k < Suc i} \<noteq> 0"
   908 proof -
   909   from zero_in_M have "{k \<in> M. k < Suc i} \<noteq> {}" by auto
   910   with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff)
   911 qed
   912 
   913 lemma card_less_Suc2: "0 \<notin> M \<Longrightarrow> card {k. Suc k \<in> M \<and> k < i} = card {k \<in> M. k < Suc i}"
   914 apply (rule card_bij_eq [of Suc _ _ "\<lambda>x. x - Suc 0"])
   915 apply simp
   916 apply fastforce
   917 apply auto
   918 apply (rule inj_on_diff_nat)
   919 apply auto
   920 apply (case_tac x)
   921 apply auto
   922 apply (case_tac xa)
   923 apply auto
   924 apply (case_tac xa)
   925 apply auto
   926 done
   927 
   928 lemma card_less_Suc:
   929   assumes zero_in_M: "0 \<in> M"
   930     shows "Suc (card {k. Suc k \<in> M \<and> k < i}) = card {k \<in> M. k < Suc i}"
   931 proof -
   932   from assms have a: "0 \<in> {k \<in> M. k < Suc i}" by simp
   933   hence c: "{k \<in> M. k < Suc i} = insert 0 ({k \<in> M. k < Suc i} - {0})"
   934     by (auto simp only: insert_Diff)
   935   have b: "{k \<in> M. k < Suc i} - {0} = {k \<in> M - {0}. k < Suc i}"  by auto
   936   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}))"
   937     apply (subst card_insert)
   938     apply simp_all
   939     apply (subst b)
   940     apply (subst card_less_Suc2[symmetric])
   941     apply simp_all
   942     done
   943   with c show ?thesis by simp
   944 qed
   945 
   946 
   947 subsection {*Lemmas useful with the summation operator setsum*}
   948 
   949 text {* For examples, see Algebra/poly/UnivPoly2.thy *}
   950 
   951 subsubsection {* Disjoint Unions *}
   952 
   953 text {* Singletons and open intervals *}
   954 
   955 lemma ivl_disj_un_singleton:
   956   "{l::'a::linorder} Un {l<..} = {l..}"
   957   "{..<u} Un {u::'a::linorder} = {..u}"
   958   "(l::'a::linorder) < u ==> {l} Un {l<..<u} = {l..<u}"
   959   "(l::'a::linorder) < u ==> {l<..<u} Un {u} = {l<..u}"
   960   "(l::'a::linorder) <= u ==> {l} Un {l<..u} = {l..u}"
   961   "(l::'a::linorder) <= u ==> {l..<u} Un {u} = {l..u}"
   962 by auto
   963 
   964 text {* One- and two-sided intervals *}
   965 
   966 lemma ivl_disj_un_one:
   967   "(l::'a::linorder) < u ==> {..l} Un {l<..<u} = {..<u}"
   968   "(l::'a::linorder) <= u ==> {..<l} Un {l..<u} = {..<u}"
   969   "(l::'a::linorder) <= u ==> {..l} Un {l<..u} = {..u}"
   970   "(l::'a::linorder) <= u ==> {..<l} Un {l..u} = {..u}"
   971   "(l::'a::linorder) <= u ==> {l<..u} Un {u<..} = {l<..}"
   972   "(l::'a::linorder) < u ==> {l<..<u} Un {u..} = {l<..}"
   973   "(l::'a::linorder) <= u ==> {l..u} Un {u<..} = {l..}"
   974   "(l::'a::linorder) <= u ==> {l..<u} Un {u..} = {l..}"
   975 by auto
   976 
   977 text {* Two- and two-sided intervals *}
   978 
   979 lemma ivl_disj_un_two:
   980   "[| (l::'a::linorder) < m; m <= u |] ==> {l<..<m} Un {m..<u} = {l<..<u}"
   981   "[| (l::'a::linorder) <= m; m < u |] ==> {l<..m} Un {m<..<u} = {l<..<u}"
   982   "[| (l::'a::linorder) <= m; m <= u |] ==> {l..<m} Un {m..<u} = {l..<u}"
   983   "[| (l::'a::linorder) <= m; m < u |] ==> {l..m} Un {m<..<u} = {l..<u}"
   984   "[| (l::'a::linorder) < m; m <= u |] ==> {l<..<m} Un {m..u} = {l<..u}"
   985   "[| (l::'a::linorder) <= m; m <= u |] ==> {l<..m} Un {m<..u} = {l<..u}"
   986   "[| (l::'a::linorder) <= m; m <= u |] ==> {l..<m} Un {m..u} = {l..u}"
   987   "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {m<..u} = {l..u}"
   988 by auto
   989 
   990 lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two
   991 
   992 subsubsection {* Disjoint Intersections *}
   993 
   994 text {* One- and two-sided intervals *}
   995 
   996 lemma ivl_disj_int_one:
   997   "{..l::'a::order} Int {l<..<u} = {}"
   998   "{..<l} Int {l..<u} = {}"
   999   "{..l} Int {l<..u} = {}"
  1000   "{..<l} Int {l..u} = {}"
  1001   "{l<..u} Int {u<..} = {}"
  1002   "{l<..<u} Int {u..} = {}"
  1003   "{l..u} Int {u<..} = {}"
  1004   "{l..<u} Int {u..} = {}"
  1005   by auto
  1006 
  1007 text {* Two- and two-sided intervals *}
  1008 
  1009 lemma ivl_disj_int_two:
  1010   "{l::'a::order<..<m} Int {m..<u} = {}"
  1011   "{l<..m} Int {m<..<u} = {}"
  1012   "{l..<m} Int {m..<u} = {}"
  1013   "{l..m} Int {m<..<u} = {}"
  1014   "{l<..<m} Int {m..u} = {}"
  1015   "{l<..m} Int {m<..u} = {}"
  1016   "{l..<m} Int {m..u} = {}"
  1017   "{l..m} Int {m<..u} = {}"
  1018   by auto
  1019 
  1020 lemmas ivl_disj_int = ivl_disj_int_one ivl_disj_int_two
  1021 
  1022 subsubsection {* Some Differences *}
  1023 
  1024 lemma ivl_diff[simp]:
  1025  "i \<le> n \<Longrightarrow> {i..<m} - {i..<n} = {n..<(m::'a::linorder)}"
  1026 by(auto)
  1027 
  1028 
  1029 subsubsection {* Some Subset Conditions *}
  1030 
  1031 lemma ivl_subset [simp,no_atp]:
  1032  "({i..<j} \<subseteq> {m..<n}) = (j \<le> i | m \<le> i & j \<le> (n::'a::linorder))"
  1033 apply(auto simp:linorder_not_le)
  1034 apply(rule ccontr)
  1035 apply(insert linorder_le_less_linear[of i n])
  1036 apply(clarsimp simp:linorder_not_le)
  1037 apply(fastforce)
  1038 done
  1039 
  1040 
  1041 subsection {* Summation indexed over intervals *}
  1042 
  1043 syntax
  1044   "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)
  1045   "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)
  1046   "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<_./ _)" [0,0,10] 10)
  1047   "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<=_./ _)" [0,0,10] 10)
  1048 syntax (xsymbols)
  1049   "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
  1050   "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10)
  1051   "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10)
  1052   "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10)
  1053 syntax (HTML output)
  1054   "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
  1055   "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10)
  1056   "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10)
  1057   "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10)
  1058 syntax (latex_sum output)
  1059   "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
  1060  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)
  1061   "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
  1062  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)
  1063   "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
  1064  ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10)
  1065   "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
  1066  ("(3\<^raw:$\sum_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10)
  1067 
  1068 translations
  1069   "\<Sum>x=a..b. t" == "CONST setsum (%x. t) {a..b}"
  1070   "\<Sum>x=a..<b. t" == "CONST setsum (%x. t) {a..<b}"
  1071   "\<Sum>i\<le>n. t" == "CONST setsum (\<lambda>i. t) {..n}"
  1072   "\<Sum>i<n. t" == "CONST setsum (\<lambda>i. t) {..<n}"
  1073 
  1074 text{* The above introduces some pretty alternative syntaxes for
  1075 summation over intervals:
  1076 \begin{center}
  1077 \begin{tabular}{lll}
  1078 Old & New & \LaTeX\\
  1079 @{term[source]"\<Sum>x\<in>{a..b}. e"} & @{term"\<Sum>x=a..b. e"} & @{term[mode=latex_sum]"\<Sum>x=a..b. e"}\\
  1080 @{term[source]"\<Sum>x\<in>{a..<b}. e"} & @{term"\<Sum>x=a..<b. e"} & @{term[mode=latex_sum]"\<Sum>x=a..<b. e"}\\
  1081 @{term[source]"\<Sum>x\<in>{..b}. e"} & @{term"\<Sum>x\<le>b. e"} & @{term[mode=latex_sum]"\<Sum>x\<le>b. e"}\\
  1082 @{term[source]"\<Sum>x\<in>{..<b}. e"} & @{term"\<Sum>x<b. e"} & @{term[mode=latex_sum]"\<Sum>x<b. e"}
  1083 \end{tabular}
  1084 \end{center}
  1085 The left column shows the term before introduction of the new syntax,
  1086 the middle column shows the new (default) syntax, and the right column
  1087 shows a special syntax. The latter is only meaningful for latex output
  1088 and has to be activated explicitly by setting the print mode to
  1089 @{text latex_sum} (e.g.\ via @{text "mode = latex_sum"} in
  1090 antiquotations). It is not the default \LaTeX\ output because it only
  1091 works well with italic-style formulae, not tt-style.
  1092 
  1093 Note that for uniformity on @{typ nat} it is better to use
  1094 @{term"\<Sum>x::nat=0..<n. e"} rather than @{text"\<Sum>x<n. e"}: @{text setsum} may
  1095 not provide all lemmas available for @{term"{m..<n}"} also in the
  1096 special form for @{term"{..<n}"}. *}
  1097 
  1098 text{* This congruence rule should be used for sums over intervals as
  1099 the standard theorem @{text[source]setsum_cong} does not work well
  1100 with the simplifier who adds the unsimplified premise @{term"x:B"} to
  1101 the context. *}
  1102 
  1103 lemma setsum_ivl_cong:
  1104  "\<lbrakk>a = c; b = d; !!x. \<lbrakk> c \<le> x; x < d \<rbrakk> \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow>
  1105  setsum f {a..<b} = setsum g {c..<d}"
  1106 by(rule setsum_cong, simp_all)
  1107 
  1108 (* FIXME why are the following simp rules but the corresponding eqns
  1109 on intervals are not? *)
  1110 
  1111 lemma setsum_atMost_Suc[simp]: "(\<Sum>i \<le> Suc n. f i) = (\<Sum>i \<le> n. f i) + f(Suc n)"
  1112 by (simp add:atMost_Suc add_ac)
  1113 
  1114 lemma setsum_lessThan_Suc[simp]: "(\<Sum>i < Suc n. f i) = (\<Sum>i < n. f i) + f n"
  1115 by (simp add:lessThan_Suc add_ac)
  1116 
  1117 lemma setsum_cl_ivl_Suc[simp]:
  1118   "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"
  1119 by (auto simp:add_ac atLeastAtMostSuc_conv)
  1120 
  1121 lemma setsum_op_ivl_Suc[simp]:
  1122   "setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))"
  1123 by (auto simp:add_ac atLeastLessThanSuc)
  1124 (*
  1125 lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==>
  1126     (\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)"
  1127 by (auto simp:add_ac atLeastAtMostSuc_conv)
  1128 *)
  1129 
  1130 lemma setsum_head:
  1131   fixes n :: nat
  1132   assumes mn: "m <= n" 
  1133   shows "(\<Sum>x\<in>{m..n}. P x) = P m + (\<Sum>x\<in>{m<..n}. P x)" (is "?lhs = ?rhs")
  1134 proof -
  1135   from mn
  1136   have "{m..n} = {m} \<union> {m<..n}"
  1137     by (auto intro: ivl_disj_un_singleton)
  1138   hence "?lhs = (\<Sum>x\<in>{m} \<union> {m<..n}. P x)"
  1139     by (simp add: atLeast0LessThan)
  1140   also have "\<dots> = ?rhs" by simp
  1141   finally show ?thesis .
  1142 qed
  1143 
  1144 lemma setsum_head_Suc:
  1145   "m \<le> n \<Longrightarrow> setsum f {m..n} = f m + setsum f {Suc m..n}"
  1146 by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost)
  1147 
  1148 lemma setsum_head_upt_Suc:
  1149   "m < n \<Longrightarrow> setsum f {m..<n} = f m + setsum f {Suc m..<n}"
  1150 apply(insert setsum_head_Suc[of m "n - Suc 0" f])
  1151 apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps)
  1152 done
  1153 
  1154 lemma setsum_ub_add_nat: assumes "(m::nat) \<le> n + 1"
  1155   shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}"
  1156 proof-
  1157   have "{m .. n+p} = {m..n} \<union> {n+1..n+p}" using `m \<le> n+1` by auto
  1158   thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint
  1159     atLeastSucAtMost_greaterThanAtMost)
  1160 qed
  1161 
  1162 lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
  1163   setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"
  1164 by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un)
  1165 
  1166 lemma setsum_diff_nat_ivl:
  1167 fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
  1168 shows "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
  1169   setsum f {m..<p} - setsum f {m..<n} = setsum f {n..<p}"
  1170 using setsum_add_nat_ivl [of m n p f,symmetric]
  1171 apply (simp add: add_ac)
  1172 done
  1173 
  1174 lemma setsum_natinterval_difff:
  1175   fixes f:: "nat \<Rightarrow> ('a::ab_group_add)"
  1176   shows  "setsum (\<lambda>k. f k - f(k + 1)) {(m::nat) .. n} =
  1177           (if m <= n then f m - f(n + 1) else 0)"
  1178 by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)
  1179 
  1180 lemma setsum_restrict_set':
  1181   "finite A \<Longrightarrow> setsum f {x \<in> A. x \<in> B} = (\<Sum>x\<in>A. if x \<in> B then f x else 0)"
  1182   by (simp add: setsum_restrict_set [symmetric] Int_def)
  1183 
  1184 lemma setsum_restrict_set'':
  1185   "finite A \<Longrightarrow> setsum f {x \<in> A. P x} = (\<Sum>x\<in>A. if P x  then f x else 0)"
  1186   by (simp add: setsum_restrict_set' [of A f "{x. P x}", simplified mem_Collect_eq])
  1187 
  1188 lemma setsum_setsum_restrict:
  1189   "finite S \<Longrightarrow> finite T \<Longrightarrow>
  1190     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"
  1191   by (simp add: setsum_restrict_set'') (rule setsum_commute)
  1192 
  1193 lemma setsum_image_gen: assumes fS: "finite S"
  1194   shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"
  1195 proof-
  1196   { fix x assume "x \<in> S" then have "{y. y\<in> f`S \<and> f x = y} = {f x}" by auto }
  1197   hence "setsum g S = setsum (\<lambda>x. setsum (\<lambda>y. g x) {y. y\<in> f`S \<and> f x = y}) S"
  1198     by simp
  1199   also have "\<dots> = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"
  1200     by (rule setsum_setsum_restrict[OF fS finite_imageI[OF fS]])
  1201   finally show ?thesis .
  1202 qed
  1203 
  1204 lemma setsum_le_included:
  1205   fixes f :: "'a \<Rightarrow> 'b::ordered_comm_monoid_add"
  1206   assumes "finite s" "finite t"
  1207   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)"
  1208   shows "setsum f s \<le> setsum g t"
  1209 proof -
  1210   have "setsum f s \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) s"
  1211   proof (rule setsum_mono)
  1212     fix y assume "y \<in> s"
  1213     with assms obtain z where z: "z \<in> t" "y = i z" "f y \<le> g z" by auto
  1214     with assms show "f y \<le> setsum g {x \<in> t. i x = y}" (is "?A y \<le> ?B y")
  1215       using order_trans[of "?A (i z)" "setsum g {z}" "?B (i z)", intro]
  1216       by (auto intro!: setsum_mono2)
  1217   qed
  1218   also have "... \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) (i ` t)"
  1219     using assms(2-4) by (auto intro!: setsum_mono2 setsum_nonneg)
  1220   also have "... \<le> setsum g t"
  1221     using assms by (auto simp: setsum_image_gen[symmetric])
  1222   finally show ?thesis .
  1223 qed
  1224 
  1225 lemma setsum_multicount_gen:
  1226   assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)"
  1227   shows "setsum (\<lambda>i. (card {j\<in>t. R i j})) s = setsum k t" (is "?l = ?r")
  1228 proof-
  1229   have "?l = setsum (\<lambda>i. setsum (\<lambda>x.1) {j\<in>t. R i j}) s" by auto
  1230   also have "\<dots> = ?r" unfolding setsum_setsum_restrict[OF assms(1-2)]
  1231     using assms(3) by auto
  1232   finally show ?thesis .
  1233 qed
  1234 
  1235 lemma setsum_multicount:
  1236   assumes "finite S" "finite T" "\<forall>j\<in>T. (card {i\<in>S. R i j} = k)"
  1237   shows "setsum (\<lambda>i. card {j\<in>T. R i j}) S = k * card T" (is "?l = ?r")
  1238 proof-
  1239   have "?l = setsum (\<lambda>i. k) T" by(rule setsum_multicount_gen)(auto simp:assms)
  1240   also have "\<dots> = ?r" by(simp add: mult_commute)
  1241   finally show ?thesis by auto
  1242 qed
  1243 
  1244 
  1245 subsection{* Shifting bounds *}
  1246 
  1247 lemma setsum_shift_bounds_nat_ivl:
  1248   "setsum f {m+k..<n+k} = setsum (%i. f(i + k)){m..<n::nat}"
  1249 by (induct "n", auto simp:atLeastLessThanSuc)
  1250 
  1251 lemma setsum_shift_bounds_cl_nat_ivl:
  1252   "setsum f {m+k..n+k} = setsum (%i. f(i + k)){m..n::nat}"
  1253 apply (insert setsum_reindex[OF inj_on_add_nat, where h=f and B = "{m..n}"])
  1254 apply (simp add:image_add_atLeastAtMost o_def)
  1255 done
  1256 
  1257 corollary setsum_shift_bounds_cl_Suc_ivl:
  1258   "setsum f {Suc m..Suc n} = setsum (%i. f(Suc i)){m..n}"
  1259 by (simp add:setsum_shift_bounds_cl_nat_ivl[where k="Suc 0", simplified])
  1260 
  1261 corollary setsum_shift_bounds_Suc_ivl:
  1262   "setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}"
  1263 by (simp add:setsum_shift_bounds_nat_ivl[where k="Suc 0", simplified])
  1264 
  1265 lemma setsum_shift_lb_Suc0_0:
  1266   "f(0::nat) = (0::nat) \<Longrightarrow> setsum f {Suc 0..k} = setsum f {0..k}"
  1267 by(simp add:setsum_head_Suc)
  1268 
  1269 lemma setsum_shift_lb_Suc0_0_upt:
  1270   "f(0::nat) = 0 \<Longrightarrow> setsum f {Suc 0..<k} = setsum f {0..<k}"
  1271 apply(cases k)apply simp
  1272 apply(simp add:setsum_head_upt_Suc)
  1273 done
  1274 
  1275 subsection {* The formula for geometric sums *}
  1276 
  1277 lemma geometric_sum:
  1278   assumes "x \<noteq> 1"
  1279   shows "(\<Sum>i=0..<n. x ^ i) = (x ^ n - 1) / (x - 1::'a::field)"
  1280 proof -
  1281   from assms obtain y where "y = x - 1" and "y \<noteq> 0" by simp_all
  1282   moreover have "(\<Sum>i=0..<n. (y + 1) ^ i) = ((y + 1) ^ n - 1) / y"
  1283   proof (induct n)
  1284     case 0 then show ?case by simp
  1285   next
  1286     case (Suc n)
  1287     moreover with `y \<noteq> 0` have "(1 + y) ^ n = (y * inverse y) * (1 + y) ^ n" by simp 
  1288     ultimately show ?case by (simp add: field_simps divide_inverse)
  1289   qed
  1290   ultimately show ?thesis by simp
  1291 qed
  1292 
  1293 
  1294 subsection {* The formula for arithmetic sums *}
  1295 
  1296 lemma gauss_sum:
  1297   "(2::'a::comm_semiring_1)*(\<Sum>i\<in>{1..n}. of_nat i) =
  1298    of_nat n*((of_nat n)+1)"
  1299 proof (induct n)
  1300   case 0
  1301   show ?case by simp
  1302 next
  1303   case (Suc n)
  1304   then show ?case
  1305     by (simp add: algebra_simps add: one_add_one [symmetric] del: one_add_one)
  1306       (* FIXME: make numeral cancellation simprocs work for semirings *)
  1307 qed
  1308 
  1309 theorem arith_series_general:
  1310   "(2::'a::comm_semiring_1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
  1311   of_nat n * (a + (a + of_nat(n - 1)*d))"
  1312 proof cases
  1313   assume ngt1: "n > 1"
  1314   let ?I = "\<lambda>i. of_nat i" and ?n = "of_nat n"
  1315   have
  1316     "(\<Sum>i\<in>{..<n}. a+?I i*d) =
  1317      ((\<Sum>i\<in>{..<n}. a) + (\<Sum>i\<in>{..<n}. ?I i*d))"
  1318     by (rule setsum_addf)
  1319   also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp
  1320   also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))"
  1321     unfolding One_nat_def
  1322     by (simp add: setsum_right_distrib atLeast0LessThan[symmetric] setsum_shift_lb_Suc0_0_upt mult_ac)
  1323   also have "2*\<dots> = 2*?n*a + d*2*(\<Sum>i\<in>{1..<n}. ?I i)"
  1324     by (simp add: algebra_simps)
  1325   also from ngt1 have "{1..<n} = {1..n - 1}"
  1326     by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)
  1327   also from ngt1
  1328   have "2*?n*a + d*2*(\<Sum>i\<in>{1..n - 1}. ?I i) = (2*?n*a + d*?I (n - 1)*?I n)"
  1329     by (simp only: mult_ac gauss_sum [of "n - 1"], unfold One_nat_def)
  1330        (simp add:  mult_ac trans [OF add_commute of_nat_Suc [symmetric]])
  1331   finally show ?thesis
  1332     unfolding mult_2 by (simp add: algebra_simps)
  1333 next
  1334   assume "\<not>(n > 1)"
  1335   hence "n = 1 \<or> n = 0" by auto
  1336   thus ?thesis by (auto simp: mult_2)
  1337 qed
  1338 
  1339 lemma arith_series_nat:
  1340   "(2::nat) * (\<Sum>i\<in>{..<n}. a+i*d) = n * (a + (a+(n - 1)*d))"
  1341 proof -
  1342   have
  1343     "2 * (\<Sum>i\<in>{..<n::nat}. a + of_nat(i)*d) =
  1344     of_nat(n) * (a + (a + of_nat(n - 1)*d))"
  1345     by (rule arith_series_general)
  1346   thus ?thesis
  1347     unfolding One_nat_def by auto
  1348 qed
  1349 
  1350 lemma arith_series_int:
  1351   "2 * (\<Sum>i\<in>{..<n}. a + int i * d) = int n * (a + (a + int(n - 1)*d))"
  1352   by (fact arith_series_general) (* FIXME: duplicate *)
  1353 
  1354 lemma sum_diff_distrib:
  1355   fixes P::"nat\<Rightarrow>nat"
  1356   shows
  1357   "\<forall>x. Q x \<le> P x  \<Longrightarrow>
  1358   (\<Sum>x<n. P x) - (\<Sum>x<n. Q x) = (\<Sum>x<n. P x - Q x)"
  1359 proof (induct n)
  1360   case 0 show ?case by simp
  1361 next
  1362   case (Suc n)
  1363 
  1364   let ?lhs = "(\<Sum>x<n. P x) - (\<Sum>x<n. Q x)"
  1365   let ?rhs = "\<Sum>x<n. P x - Q x"
  1366 
  1367   from Suc have "?lhs = ?rhs" by simp
  1368   moreover
  1369   from Suc have "?lhs + P n - Q n = ?rhs + (P n - Q n)" by simp
  1370   moreover
  1371   from Suc have
  1372     "(\<Sum>x<n. P x) + P n - ((\<Sum>x<n. Q x) + Q n) = ?rhs + (P n - Q n)"
  1373     by (subst diff_diff_left[symmetric],
  1374         subst diff_add_assoc2)
  1375        (auto simp: diff_add_assoc2 intro: setsum_mono)
  1376   ultimately
  1377   show ?case by simp
  1378 qed
  1379 
  1380 subsection {* Products indexed over intervals *}
  1381 
  1382 syntax
  1383   "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10)
  1384   "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)
  1385   "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<_./ _)" [0,0,10] 10)
  1386   "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<=_./ _)" [0,0,10] 10)
  1387 syntax (xsymbols)
  1388   "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
  1389   "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10)
  1390   "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10)
  1391   "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
  1392 syntax (HTML output)
  1393   "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
  1394   "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10)
  1395   "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10)
  1396   "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
  1397 syntax (latex_prod output)
  1398   "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
  1399  ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)
  1400   "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
  1401  ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)
  1402   "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
  1403  ("(3\<^raw:$\prod_{>_ < _\<^raw:}$> _)" [0,0,10] 10)
  1404   "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
  1405  ("(3\<^raw:$\prod_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10)
  1406 
  1407 translations
  1408   "\<Prod>x=a..b. t" == "CONST setprod (%x. t) {a..b}"
  1409   "\<Prod>x=a..<b. t" == "CONST setprod (%x. t) {a..<b}"
  1410   "\<Prod>i\<le>n. t" == "CONST setprod (\<lambda>i. t) {..n}"
  1411   "\<Prod>i<n. t" == "CONST setprod (\<lambda>i. t) {..<n}"
  1412 
  1413 subsection {* Transfer setup *}
  1414 
  1415 lemma transfer_nat_int_set_functions:
  1416     "{..n} = nat ` {0..int n}"
  1417     "{m..n} = nat ` {int m..int n}"  (* need all variants of these! *)
  1418   apply (auto simp add: image_def)
  1419   apply (rule_tac x = "int x" in bexI)
  1420   apply auto
  1421   apply (rule_tac x = "int x" in bexI)
  1422   apply auto
  1423   done
  1424 
  1425 lemma transfer_nat_int_set_function_closures:
  1426     "x >= 0 \<Longrightarrow> nat_set {x..y}"
  1427   by (simp add: nat_set_def)
  1428 
  1429 declare transfer_morphism_nat_int[transfer add
  1430   return: transfer_nat_int_set_functions
  1431     transfer_nat_int_set_function_closures
  1432 ]
  1433 
  1434 lemma transfer_int_nat_set_functions:
  1435     "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
  1436   by (simp only: is_nat_def transfer_nat_int_set_functions
  1437     transfer_nat_int_set_function_closures
  1438     transfer_nat_int_set_return_embed nat_0_le
  1439     cong: transfer_nat_int_set_cong)
  1440 
  1441 lemma transfer_int_nat_set_function_closures:
  1442     "is_nat x \<Longrightarrow> nat_set {x..y}"
  1443   by (simp only: transfer_nat_int_set_function_closures is_nat_def)
  1444 
  1445 declare transfer_morphism_int_nat[transfer add
  1446   return: transfer_int_nat_set_functions
  1447     transfer_int_nat_set_function_closures
  1448 ]
  1449 
  1450 end