Got rid of Summation and made it a translation into setsum instead.
authornipkow
Tue Jul 13 12:32:01 2004 +0200 (2004-07-13)
changeset 15041a6b1f0cef7b3
parent 15040 ed574b4f7e70
child 15042 fa7d27ef7e59
Got rid of Summation and made it a translation into setsum instead.
src/HOL/HoareParallel/OG_Examples.thy
src/HOL/HoareParallel/RG_Examples.thy
src/HOL/NatArith.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/HoareParallel/OG_Examples.thy	Mon Jul 12 19:56:58 2004 +0200
     1.2 +++ b/src/HOL/HoareParallel/OG_Examples.thy	Tue Jul 13 12:32:01 2004 +0200
     1.3 @@ -507,16 +507,16 @@
     1.4  lemma Example2_lemma2_aux2: 
     1.5    "!!b. j\<le> s \<Longrightarrow> (\<Sum>i<j. (b (s:=t)) i) = (\<Sum>i<j. b i)"
     1.6  apply(induct j)
     1.7 - apply simp_all
     1.8 + apply (simp_all cong:setsum_cong)
     1.9  done
    1.10  
    1.11  lemma Example2_lemma2: 
    1.12   "!!b. \<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i< n. b i)=(\<Sum>i< n. (b (j := Suc 0)) i)"
    1.13  apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
    1.14 -apply(erule_tac  t="Summation (b(j := (Suc 0))) n" in ssubst)
    1.15 +apply(erule_tac  t="setsum (b(j := (Suc 0))) {..n(}" in ssubst)
    1.16  apply(frule_tac b=b in Example2_lemma2_aux)
    1.17 -apply(erule_tac  t="Summation b n" in ssubst)
    1.18 -apply(subgoal_tac "Suc (Summation b j + b j + (\<Sum>i<n - Suc j. b (Suc j + i)))=(Summation b j + Suc (b j) + (\<Sum>i<n - Suc j. b (Suc j + i)))")
    1.19 +apply(erule_tac  t="setsum b {..n(}" in ssubst)
    1.20 +apply(subgoal_tac "Suc (setsum b {..j(} + b j + (\<Sum>i<n - Suc j. b (Suc j + i)))=(setsum b {..j(} + Suc (b j) + (\<Sum>i<n - Suc j. b (Suc j + i)))")
    1.21  apply(rotate_tac -1)
    1.22  apply(erule ssubst)
    1.23  apply(subgoal_tac "j\<le>j")
    1.24 @@ -548,7 +548,6 @@
    1.25  apply simp_all
    1.26  apply (tactic {* ALLGOALS Clarify_tac *})
    1.27  apply simp_all
    1.28 -    apply(force elim:Example2_lemma1)
    1.29     apply(erule Example2_lemma2)
    1.30     apply simp
    1.31    apply(erule Example2_lemma2)
     2.1 --- a/src/HOL/HoareParallel/RG_Examples.thy	Mon Jul 12 19:56:58 2004 +0200
     2.2 +++ b/src/HOL/HoareParallel/RG_Examples.thy	Tue Jul 13 12:32:01 2004 +0200
     2.3 @@ -206,21 +206,22 @@
     2.4  
     2.5  lemma Example2_lemma2_aux2: "j\<le> s \<Longrightarrow> (\<Sum>i<j. (b (s:=t)) i) = (\<Sum>i<j. b i)"
     2.6  apply(induct j)
     2.7 - apply simp_all
     2.8 + apply (simp_all cong:setsum_cong)
     2.9  done
    2.10  
    2.11 -lemma Example2_lemma2: "\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i< n. b i)=(\<Sum>i< n. (b (j:=1)) i)"
    2.12 -apply(frule_tac b="(b (j:=1))" in Example2_lemma2_aux)
    2.13 -apply(erule_tac  t="Summation (b(j := 1)) n" in ssubst)
    2.14 +lemma Example2_lemma2: 
    2.15 + "!!b. \<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i< n. b i)=(\<Sum>i< n. (b (j := Suc 0)) i)"
    2.16 +apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
    2.17 +apply(erule_tac  t="setsum (b(j := (Suc 0))) {..n(}" in ssubst)
    2.18  apply(frule_tac b=b in Example2_lemma2_aux)
    2.19 -apply(erule_tac  t="Summation b n" in ssubst)
    2.20 -apply(subgoal_tac "Suc (Summation b j + b j + (\<Sum>i<n - Suc j. b (Suc j + i)))=(Summation b j + Suc (b j) + (\<Sum>i<n - Suc j. b (Suc j + i)))")
    2.21 - apply(rotate_tac -1)
    2.22 - apply(erule ssubst)
    2.23 - apply(subgoal_tac "j\<le>j")
    2.24 -  apply(drule_tac b="b" and t=1 in Example2_lemma2_aux2)
    2.25 -  apply(rotate_tac -1)
    2.26 -  apply(erule ssubst)
    2.27 +apply(erule_tac  t="setsum b {..n(}" in ssubst)
    2.28 +apply(subgoal_tac "Suc (setsum b {..j(} + b j + (\<Sum>i<n - Suc j. b (Suc j + i)))=(setsum b {..j(} + Suc (b j) + (\<Sum>i<n - Suc j. b (Suc j + i)))")
    2.29 +apply(rotate_tac -1)
    2.30 +apply(erule ssubst)
    2.31 +apply(subgoal_tac "j\<le>j")
    2.32 + apply(drule_tac b="b" and t="(Suc 0)" in Example2_lemma2_aux2)
    2.33 +apply(rotate_tac -1)
    2.34 +apply(erule ssubst)
    2.35  apply simp_all
    2.36  done
    2.37  
     3.1 --- a/src/HOL/NatArith.thy	Mon Jul 12 19:56:58 2004 +0200
     3.2 +++ b/src/HOL/NatArith.thy	Tue Jul 13 12:32:01 2004 +0200
     3.3 @@ -36,7 +36,7 @@
     3.4  
     3.5  lemmas [arith_split] = nat_diff_split split_min split_max
     3.6  
     3.7 -
     3.8 +(*
     3.9  subsection {* Generic summation indexed over natural numbers *}
    3.10  
    3.11  consts
    3.12 @@ -53,5 +53,5 @@
    3.13  theorem Summation_step:
    3.14      "0 < n ==> (\<Sum>i < n. f i) = (\<Sum>i < n - 1. f i) + f (n - 1)"
    3.15    by (induct n) simp_all
    3.16 -
    3.17 +*)
    3.18  end
     4.1 --- a/src/HOL/SetInterval.thy	Mon Jul 12 19:56:58 2004 +0200
     4.2 +++ b/src/HOL/SetInterval.thy	Tue Jul 13 12:32:01 2004 +0200
     4.3 @@ -477,4 +477,19 @@
     4.4  
     4.5  lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two
     4.6  
     4.7 +
     4.8 +subsection {* Summation indexed over natural numbers *}
     4.9 +
    4.10 +text{* Legacy, only used in HoareParallel and Isar-Examples. Really
    4.11 +needed? Probably better to replace it with a more generic operator
    4.12 +like ``SUM i = m..n. b''. *}
    4.13 +
    4.14 +syntax
    4.15 +  "_Summation" :: "id => nat => 'a => nat"    ("\<Sum>_<_. _" [0, 51, 10] 10)
    4.16 +translations
    4.17 +  "\<Sum>i < n. b" == "setsum (\<lambda>i::nat. b) {..n(}"
    4.18 +
    4.19 +lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
    4.20 +by (simp add:lessThan_Suc)
    4.21 +
    4.22  end