cleaned up code generation for {.._} and {..<_}
authornipkow
Mon Sep 01 19:16:40 2008 +0200 (2008-09-01)
changeset 28068f6b2d1995171
parent 28067 4b6783d3f0d9
child 28069 ba4de3022862
cleaned up code generation for {.._} and {..<_}
moved lemmas into SetInterval where they belong
src/HOL/List.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/List.thy	Mon Sep 01 10:28:04 2008 +0200
     1.2 +++ b/src/HOL/List.thy	Mon Sep 01 19:16:40 2008 +0200
     1.3 @@ -3626,14 +3626,6 @@
     1.4  
     1.5  text {* Code for bounded quantification and summation over nats. *}
     1.6  
     1.7 -lemma atMost_upto [code unfold]:
     1.8 -  "{..n} = set [0..<Suc n]"
     1.9 -by auto
    1.10 -
    1.11 -lemma atLeast_upt [code unfold]:
    1.12 -  "{..<n} = set [0..<n]"
    1.13 -by auto
    1.14 -
    1.15  lemma greaterThanLessThan_upt [code unfold]:
    1.16    "{n<..<m} = set [Suc n..<m]"
    1.17  by auto
     2.1 --- a/src/HOL/SetInterval.thy	Mon Sep 01 10:28:04 2008 +0200
     2.2 +++ b/src/HOL/SetInterval.thy	Mon Sep 01 19:16:40 2008 +0200
     2.3 @@ -48,32 +48,7 @@
     2.4    "{l..u} == {l..} Int {..u}"
     2.5  
     2.6  end
     2.7 -(*
     2.8 -constdefs
     2.9 -  lessThan    :: "('a::ord) => 'a set"	("(1{..<_})")
    2.10 -  "{..<u} == {x. x<u}"
    2.11  
    2.12 -  atMost      :: "('a::ord) => 'a set"	("(1{.._})")
    2.13 -  "{..u} == {x. x<=u}"
    2.14 -
    2.15 -  greaterThan :: "('a::ord) => 'a set"	("(1{_<..})")
    2.16 -  "{l<..} == {x. l<x}"
    2.17 -
    2.18 -  atLeast     :: "('a::ord) => 'a set"	("(1{_..})")
    2.19 -  "{l..} == {x. l<=x}"
    2.20 -
    2.21 -  greaterThanLessThan :: "['a::ord, 'a] => 'a set"  ("(1{_<..<_})")
    2.22 -  "{l<..<u} == {l<..} Int {..<u}"
    2.23 -
    2.24 -  atLeastLessThan :: "['a::ord, 'a] => 'a set"      ("(1{_..<_})")
    2.25 -  "{l..<u} == {l..} Int {..<u}"
    2.26 -
    2.27 -  greaterThanAtMost :: "['a::ord, 'a] => 'a set"    ("(1{_<.._})")
    2.28 -  "{l<..u} == {l<..} Int {..u}"
    2.29 -
    2.30 -  atLeastAtMost :: "['a::ord, 'a] => 'a set"        ("(1{_.._})")
    2.31 -  "{l..u} == {l..} Int {..u}"
    2.32 -*)
    2.33  
    2.34  text{* A note of warning when using @{term"{..<n}"} on type @{typ
    2.35  nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving
    2.36 @@ -297,16 +272,21 @@
    2.37  
    2.38  subsubsection {* The Constant @{term atLeastLessThan} *}
    2.39  
    2.40 -text{*The orientation of the following rule is tricky. The lhs is
    2.41 +text{*The orientation of the following 2 rules is tricky. The lhs is
    2.42  defined in terms of the rhs.  Hence the chosen orientation makes sense
    2.43  in this theory --- the reverse orientation complicates proofs (eg
    2.44  nontermination). But outside, when the definition of the lhs is rarely
    2.45  used, the opposite orientation seems preferable because it reduces a
    2.46  specific concept to a more general one. *}
    2.47 +
    2.48  lemma atLeast0LessThan: "{0::nat..<n} = {..<n}"
    2.49  by(simp add:lessThan_def atLeastLessThan_def)
    2.50  
    2.51 +lemma atLeast0AtMost: "{0..n::nat} = {..n}"
    2.52 +by(simp add:atMost_def atLeastAtMost_def)
    2.53 +
    2.54  declare atLeast0LessThan[symmetric, code unfold]
    2.55 +        atLeast0AtMost[symmetric, code unfold]
    2.56  
    2.57  lemma atLeastLessThan0: "{m..<0::nat} = {}"
    2.58  by (simp add: atLeastLessThan_def)
    2.59 @@ -411,12 +391,16 @@
    2.60    fixes l :: nat shows "finite {l..u}"
    2.61  by (simp add: atLeastAtMost_def)
    2.62  
    2.63 +text {* A bounded set of natural numbers is finite. *}
    2.64  lemma bounded_nat_set_is_finite:
    2.65    "(ALL i:N. i < (n::nat)) ==> finite N"
    2.66 -  -- {* A bounded set of natural numbers is finite. *}
    2.67 -  apply (rule finite_subset)
    2.68 -   apply (rule_tac [2] finite_lessThan, auto)
    2.69 -  done
    2.70 +apply (rule finite_subset)
    2.71 + apply (rule_tac [2] finite_lessThan, auto)
    2.72 +done
    2.73 +
    2.74 +lemma finite_less_ub:
    2.75 +     "!!f::nat=>nat. (!!n. n \<le> f n) ==> finite {n. f n \<le> u}"
    2.76 +by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)
    2.77  
    2.78  text{* Any subset of an interval of natural numbers the size of the
    2.79  subset is exactly that interval. *}
    2.80 @@ -800,6 +784,32 @@
    2.81      (\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)"
    2.82  by (auto simp:add_ac atLeastAtMostSuc_conv)
    2.83  *)
    2.84 +
    2.85 +lemma setsum_head:
    2.86 +  fixes n :: nat
    2.87 +  assumes mn: "m <= n" 
    2.88 +  shows "(\<Sum>x\<in>{m..n}. P x) = P m + (\<Sum>x\<in>{m<..n}. P x)" (is "?lhs = ?rhs")
    2.89 +proof -
    2.90 +  from mn
    2.91 +  have "{m..n} = {m} \<union> {m<..n}"
    2.92 +    by (auto intro: ivl_disj_un_singleton)
    2.93 +  hence "?lhs = (\<Sum>x\<in>{m} \<union> {m<..n}. P x)"
    2.94 +    by (simp add: atLeast0LessThan)
    2.95 +  also have "\<dots> = ?rhs" by simp
    2.96 +  finally show ?thesis .
    2.97 +qed
    2.98 +
    2.99 +lemma setsum_head_Suc:
   2.100 +  "m \<le> n \<Longrightarrow> setsum f {m..n} = f m + setsum f {Suc m..n}"
   2.101 +by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost)
   2.102 +
   2.103 +lemma setsum_head_upt_Suc:
   2.104 +  "m < n \<Longrightarrow> setsum f {m..<n} = f m + setsum f {Suc m..<n}"
   2.105 +apply(insert setsum_head_Suc[of m "n - 1" f])
   2.106 +apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] ring_simps)
   2.107 +done
   2.108 +
   2.109 +
   2.110  lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
   2.111    setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"
   2.112  by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un)
   2.113 @@ -812,6 +822,7 @@
   2.114  apply (simp add: add_ac)
   2.115  done
   2.116  
   2.117 +
   2.118  subsection{* Shifting bounds *}
   2.119  
   2.120  lemma setsum_shift_bounds_nat_ivl:
   2.121 @@ -832,40 +843,15 @@
   2.122    "setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}"
   2.123  by (simp add:setsum_shift_bounds_nat_ivl[where k=1,simplified])
   2.124  
   2.125 -lemma setsum_head:
   2.126 -  fixes n :: nat
   2.127 -  assumes mn: "m <= n" 
   2.128 -  shows "(\<Sum>x\<in>{m..n}. P x) = P m + (\<Sum>x\<in>{m<..n}. P x)" (is "?lhs = ?rhs")
   2.129 -proof -
   2.130 -  from mn
   2.131 -  have "{m..n} = {m} \<union> {m<..n}"
   2.132 -    by (auto intro: ivl_disj_un_singleton)
   2.133 -  hence "?lhs = (\<Sum>x\<in>{m} \<union> {m<..n}. P x)"
   2.134 -    by (simp add: atLeast0LessThan)
   2.135 -  also have "\<dots> = ?rhs" by simp
   2.136 -  finally show ?thesis .
   2.137 -qed
   2.138 +lemma setsum_shift_lb_Suc0_0:
   2.139 +  "f(0::nat) = (0::nat) \<Longrightarrow> setsum f {Suc 0..k} = setsum f {0..k}"
   2.140 +by(simp add:setsum_head_Suc)
   2.141  
   2.142 -lemma setsum_head_upt:
   2.143 -  fixes m::nat
   2.144 -  assumes m: "0 < m"
   2.145 -  shows "(\<Sum>x<m. P x) = P 0 + (\<Sum>x\<in>{1..<m}. P x)"
   2.146 -proof -
   2.147 -  have "(\<Sum>x<m. P x) = (\<Sum>x\<in>{0..<m}. P x)" 
   2.148 -    by (simp add: atLeast0LessThan)
   2.149 -  also 
   2.150 -  from m 
   2.151 -  have "\<dots> = (\<Sum>x\<in>{0..m - 1}. P x)"
   2.152 -    by (cases m) (auto simp add: atLeastLessThanSuc_atLeastAtMost)
   2.153 -  also
   2.154 -  have "\<dots> = P 0 + (\<Sum>x\<in>{0<..m - 1}. P x)"
   2.155 -    by (simp add: setsum_head)
   2.156 -  also 
   2.157 -  from m 
   2.158 -  have "{0<..m - 1} = {1..<m}" 
   2.159 -    by (cases m) (auto simp add: atLeastLessThanSuc_atLeastAtMost)
   2.160 -  finally show ?thesis .
   2.161 -qed
   2.162 +lemma setsum_shift_lb_Suc0_0_upt:
   2.163 +  "f(0::nat) = 0 \<Longrightarrow> setsum f {Suc 0..<k} = setsum f {0..<k}"
   2.164 +apply(cases k)apply simp
   2.165 +apply(simp add:setsum_head_upt_Suc)
   2.166 +done
   2.167  
   2.168  subsection {* The formula for geometric sums *}
   2.169  
   2.170 @@ -899,12 +885,12 @@
   2.171      by (rule setsum_addf)
   2.172    also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp
   2.173    also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))"
   2.174 -    by (simp add: setsum_right_distrib setsum_head_upt mult_ac)
   2.175 +    by (simp add: setsum_right_distrib atLeast0LessThan[symmetric] setsum_shift_lb_Suc0_0_upt mult_ac)
   2.176    also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)"
   2.177      by (simp add: left_distrib right_distrib)
   2.178    also from ngt1 have "{1..<n} = {1..n - 1}"
   2.179 -    by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)    
   2.180 -  also from ngt1 
   2.181 +    by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)
   2.182 +  also from ngt1
   2.183    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)"
   2.184      by (simp only: mult_ac gauss_sum [of "n - 1"])
   2.185         (simp add:  mult_ac trans [OF add_commute of_nat_Suc [symmetric]])