28 let ?M = "\<lambda>f. Suc (Max (f ` prod_decode ` {..<n}))" |
28 let ?M = "\<lambda>f. Suc (Max (f ` prod_decode ` {..<n}))" |
29 { fix a b x assume "x < n" and [symmetric]: "(a, b) = prod_decode x" |
29 { fix a b x assume "x < n" and [symmetric]: "(a, b) = prod_decode x" |
30 then have "a < ?M fst" "b < ?M snd" |
30 then have "a < ?M fst" "b < ?M snd" |
31 by (auto intro!: Max_ge le_imp_less_Suc image_eqI) } |
31 by (auto intro!: Max_ge le_imp_less_Suc image_eqI) } |
32 then have "sum f (prod_decode ` {..<n}) \<le> sum f ({..<?M fst} \<times> {..<?M snd})" |
32 then have "sum f (prod_decode ` {..<n}) \<le> sum f ({..<?M fst} \<times> {..<?M snd})" |
33 by (auto intro!: sum_mono3) |
33 by (auto intro!: sum_mono2) |
34 then show "\<exists>a b. sum f (prod_decode ` {..<n}) \<le> sum f ({..<a} \<times> {..<b})" by auto |
34 then show "\<exists>a b. sum f (prod_decode ` {..<n}) \<le> sum f ({..<a} \<times> {..<b})" by auto |
35 next |
35 next |
36 fix a b |
36 fix a b |
37 let ?M = "prod_decode ` {..<Suc (Max (prod_encode ` ({..<a} \<times> {..<b})))}" |
37 let ?M = "prod_decode ` {..<Suc (Max (prod_encode ` ({..<a} \<times> {..<b})))}" |
38 { fix a' b' assume "a' < a" "b' < b" then have "(a', b') \<in> ?M" |
38 { fix a' b' assume "a' < a" "b' < b" then have "(a', b') \<in> ?M" |
39 by (auto intro!: Max_ge le_imp_less_Suc image_eqI[where x="prod_encode (a', b')"]) } |
39 by (auto intro!: Max_ge le_imp_less_Suc image_eqI[where x="prod_encode (a', b')"]) } |
40 then have "sum f ({..<a} \<times> {..<b}) \<le> sum f ?M" |
40 then have "sum f ({..<a} \<times> {..<b}) \<le> sum f ?M" |
41 by (auto intro!: sum_mono3) |
41 by (auto intro!: sum_mono2) |
42 then show "\<exists>n. sum f ({..<a} \<times> {..<b}) \<le> sum f (prod_decode ` {..<n})" |
42 then show "\<exists>n. sum f ({..<a} \<times> {..<b}) \<le> sum f (prod_decode ` {..<n})" |
43 by auto |
43 by auto |
44 qed |
44 qed |
45 also have "\<dots> = (SUP p. \<Sum>i<p. \<Sum>n. f (i, n))" |
45 also have "\<dots> = (SUP p. \<Sum>i<p. \<Sum>n. f (i, n))" |
46 unfolding suminf_sum[OF summableI, symmetric] |
46 unfolding suminf_sum[OF summableI, symmetric] |