# HG changeset patch
# User nipkow
# Date 1220289400 -7200
# Node ID f6b2d19951710840d2fc8747c4550b5b5dd78e7b
# Parent  4b6783d3f0d99415235d1014c8964994b7024217
cleaned up code generation for {.._} and {..<_}
moved lemmas into SetInterval where they belong

diff -r 4b6783d3f0d9 -r f6b2d1995171 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Sep 01 10:28:04 2008 +0200
+++ b/src/HOL/List.thy	Mon Sep 01 19:16:40 2008 +0200
@@ -3626,14 +3626,6 @@
 
 text {* Code for bounded quantification and summation over nats. *}
 
-lemma atMost_upto [code unfold]:
-  "{..n} = set [0..<Suc n]"
-by auto
-
-lemma atLeast_upt [code unfold]:
-  "{..<n} = set [0..<n]"
-by auto
-
 lemma greaterThanLessThan_upt [code unfold]:
   "{n<..<m} = set [Suc n..<m]"
 by auto
diff -r 4b6783d3f0d9 -r f6b2d1995171 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Mon Sep 01 10:28:04 2008 +0200
+++ b/src/HOL/SetInterval.thy	Mon Sep 01 19:16:40 2008 +0200
@@ -48,32 +48,7 @@
   "{l..u} == {l..} Int {..u}"
 
 end
-(*
-constdefs
-  lessThan    :: "('a::ord) => 'a set"	("(1{..<_})")
-  "{..<u} == {x. x<u}"
 
-  atMost      :: "('a::ord) => 'a set"	("(1{.._})")
-  "{..u} == {x. x<=u}"
-
-  greaterThan :: "('a::ord) => 'a set"	("(1{_<..})")
-  "{l<..} == {x. l<x}"
-
-  atLeast     :: "('a::ord) => 'a set"	("(1{_..})")
-  "{l..} == {x. l<=x}"
-
-  greaterThanLessThan :: "['a::ord, 'a] => 'a set"  ("(1{_<..<_})")
-  "{l<..<u} == {l<..} Int {..<u}"
-
-  atLeastLessThan :: "['a::ord, 'a] => 'a set"      ("(1{_..<_})")
-  "{l..<u} == {l..} Int {..<u}"
-
-  greaterThanAtMost :: "['a::ord, 'a] => 'a set"    ("(1{_<.._})")
-  "{l<..u} == {l<..} Int {..u}"
-
-  atLeastAtMost :: "['a::ord, 'a] => 'a set"        ("(1{_.._})")
-  "{l..u} == {l..} Int {..u}"
-*)
 
 text{* A note of warning when using @{term"{..<n}"} on type @{typ
 nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving
@@ -297,16 +272,21 @@
 
 subsubsection {* The Constant @{term atLeastLessThan} *}
 
-text{*The orientation of the following rule is tricky. The lhs is
+text{*The orientation of the following 2 rules is tricky. The lhs is
 defined in terms of the rhs.  Hence the chosen orientation makes sense
 in this theory --- the reverse orientation complicates proofs (eg
 nontermination). But outside, when the definition of the lhs is rarely
 used, the opposite orientation seems preferable because it reduces a
 specific concept to a more general one. *}
+
 lemma atLeast0LessThan: "{0::nat..<n} = {..<n}"
 by(simp add:lessThan_def atLeastLessThan_def)
 
+lemma atLeast0AtMost: "{0..n::nat} = {..n}"
+by(simp add:atMost_def atLeastAtMost_def)
+
 declare atLeast0LessThan[symmetric, code unfold]
+        atLeast0AtMost[symmetric, code unfold]
 
 lemma atLeastLessThan0: "{m..<0::nat} = {}"
 by (simp add: atLeastLessThan_def)
@@ -411,12 +391,16 @@
   fixes l :: nat shows "finite {l..u}"
 by (simp add: atLeastAtMost_def)
 
+text {* A bounded set of natural numbers is finite. *}
 lemma bounded_nat_set_is_finite:
   "(ALL i:N. i < (n::nat)) ==> finite N"
-  -- {* A bounded set of natural numbers is finite. *}
-  apply (rule finite_subset)
-   apply (rule_tac [2] finite_lessThan, auto)
-  done
+apply (rule finite_subset)
+ apply (rule_tac [2] finite_lessThan, auto)
+done
+
+lemma finite_less_ub:
+     "!!f::nat=>nat. (!!n. n \<le> f n) ==> finite {n. f n \<le> u}"
+by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)
 
 text{* Any subset of an interval of natural numbers the size of the
 subset is exactly that interval. *}
@@ -800,6 +784,32 @@
     (\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)"
 by (auto simp:add_ac atLeastAtMostSuc_conv)
 *)
+
+lemma setsum_head:
+  fixes n :: nat
+  assumes mn: "m <= n" 
+  shows "(\<Sum>x\<in>{m..n}. P x) = P m + (\<Sum>x\<in>{m<..n}. P x)" (is "?lhs = ?rhs")
+proof -
+  from mn
+  have "{m..n} = {m} \<union> {m<..n}"
+    by (auto intro: ivl_disj_un_singleton)
+  hence "?lhs = (\<Sum>x\<in>{m} \<union> {m<..n}. P x)"
+    by (simp add: atLeast0LessThan)
+  also have "\<dots> = ?rhs" by simp
+  finally show ?thesis .
+qed
+
+lemma setsum_head_Suc:
+  "m \<le> n \<Longrightarrow> setsum f {m..n} = f m + setsum f {Suc m..n}"
+by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost)
+
+lemma setsum_head_upt_Suc:
+  "m < n \<Longrightarrow> setsum f {m..<n} = f m + setsum f {Suc m..<n}"
+apply(insert setsum_head_Suc[of m "n - 1" f])
+apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] ring_simps)
+done
+
+
 lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
   setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"
 by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un)
@@ -812,6 +822,7 @@
 apply (simp add: add_ac)
 done
 
+
 subsection{* Shifting bounds *}
 
 lemma setsum_shift_bounds_nat_ivl:
@@ -832,40 +843,15 @@
   "setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}"
 by (simp add:setsum_shift_bounds_nat_ivl[where k=1,simplified])
 
-lemma setsum_head:
-  fixes n :: nat
-  assumes mn: "m <= n" 
-  shows "(\<Sum>x\<in>{m..n}. P x) = P m + (\<Sum>x\<in>{m<..n}. P x)" (is "?lhs = ?rhs")
-proof -
-  from mn
-  have "{m..n} = {m} \<union> {m<..n}"
-    by (auto intro: ivl_disj_un_singleton)
-  hence "?lhs = (\<Sum>x\<in>{m} \<union> {m<..n}. P x)"
-    by (simp add: atLeast0LessThan)
-  also have "\<dots> = ?rhs" by simp
-  finally show ?thesis .
-qed
+lemma setsum_shift_lb_Suc0_0:
+  "f(0::nat) = (0::nat) \<Longrightarrow> setsum f {Suc 0..k} = setsum f {0..k}"
+by(simp add:setsum_head_Suc)
 
-lemma setsum_head_upt:
-  fixes m::nat
-  assumes m: "0 < m"
-  shows "(\<Sum>x<m. P x) = P 0 + (\<Sum>x\<in>{1..<m}. P x)"
-proof -
-  have "(\<Sum>x<m. P x) = (\<Sum>x\<in>{0..<m}. P x)" 
-    by (simp add: atLeast0LessThan)
-  also 
-  from m 
-  have "\<dots> = (\<Sum>x\<in>{0..m - 1}. P x)"
-    by (cases m) (auto simp add: atLeastLessThanSuc_atLeastAtMost)
-  also
-  have "\<dots> = P 0 + (\<Sum>x\<in>{0<..m - 1}. P x)"
-    by (simp add: setsum_head)
-  also 
-  from m 
-  have "{0<..m - 1} = {1..<m}" 
-    by (cases m) (auto simp add: atLeastLessThanSuc_atLeastAtMost)
-  finally show ?thesis .
-qed
+lemma setsum_shift_lb_Suc0_0_upt:
+  "f(0::nat) = 0 \<Longrightarrow> setsum f {Suc 0..<k} = setsum f {0..<k}"
+apply(cases k)apply simp
+apply(simp add:setsum_head_upt_Suc)
+done
 
 subsection {* The formula for geometric sums *}
 
@@ -899,12 +885,12 @@
     by (rule setsum_addf)
   also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp
   also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))"
-    by (simp add: setsum_right_distrib setsum_head_upt mult_ac)
+    by (simp add: setsum_right_distrib atLeast0LessThan[symmetric] setsum_shift_lb_Suc0_0_upt mult_ac)
   also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)"
     by (simp add: left_distrib right_distrib)
   also from ngt1 have "{1..<n} = {1..n - 1}"
-    by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)    
-  also from ngt1 
+    by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)
+  also from ngt1
   have "(1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..n - 1}. ?I i) = ((1+1)*?n*a + d*?I (n - 1)*?I n)"
     by (simp only: mult_ac gauss_sum [of "n - 1"])
        (simp add:  mult_ac trans [OF add_commute of_nat_Suc [symmetric]])