equal
deleted
inserted
replaced
12 begin |
12 begin |
13 |
13 |
14 constdefs |
14 constdefs |
15 sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal" |
15 sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal" |
16 "sumhr == |
16 "sumhr == |
17 %(M,N,f). Ifun2_of (%m n. setsum f {m..<n}) M N" |
17 %(M,N,f). starfun2 (%m n. setsum f {m..<n}) M N" |
18 (* |
|
19 "sumhr p == |
|
20 (%(M,N,f). Abs_star(\<Union>X \<in> Rep_star(M). \<Union>Y \<in> Rep_star(N). |
|
21 starrel ``{%n::nat. setsum f {X n..<Y n}})) p" |
|
22 *) |
|
23 |
18 |
24 NSsums :: "[nat=>real,real] => bool" (infixr "NSsums" 80) |
19 NSsums :: "[nat=>real,real] => bool" (infixr "NSsums" 80) |
25 "f NSsums s == (%n. setsum f {0..<n}) ----NS> s" |
20 "f NSsums s == (%n. setsum f {0..<n}) ----NS> s" |
26 |
21 |
27 NSsummable :: "(nat=>real) => bool" |
22 NSsummable :: "(nat=>real) => bool" |
32 |
27 |
33 |
28 |
34 lemma sumhr: |
29 lemma sumhr: |
35 "sumhr(star_n M, star_n N, f) = |
30 "sumhr(star_n M, star_n N, f) = |
36 star_n (%n. setsum f {M n..<N n})" |
31 star_n (%n. setsum f {M n..<N n})" |
37 by (simp add: sumhr_def Ifun2_of_def star_of_def Ifun_star_n) |
32 by (simp add: sumhr_def starfun2_star_n) |
38 |
33 |
39 text{*Base case in definition of @{term sumr}*} |
34 text{*Base case in definition of @{term sumr}*} |
40 lemma sumhr_zero [simp]: "sumhr (m,0,f) = 0" |
35 lemma sumhr_zero [simp]: "sumhr (m,0,f) = 0" |
41 apply (cases m) |
36 apply (cases m) |
42 apply (simp add: star_n_zero_num sumhr symmetric) |
37 apply (simp add: star_n_zero_num sumhr symmetric) |