src/real/realScript.sml

2104 (* Now define finite sums; NB: sum(m,n) f = f(m) + f(m+1) + ... + f(m+n-1)   *)
2107 val sum = Lib.with_flag (boolLib.def_suffix, "") Define`
2108    (sum (n,0) f = 0) /\
2109    (sum (n,SUC m) f = sum (n,m) f + f (n + m): real)`
2116   ���!f n p. sum(0,n) f + sum(n,p) f = sum(0,n + p) f���,
2118   REWRITE_TAC[sum, REAL_ADD_RID, ADD_CLAUSES] THEN
2122   ���!f m n. sum(m,n) f = sum(0,m + n) f - sum(0,m) f���,
2127   ���!f m n. abs(sum(m,n) f) <= sum(m,n) (\n. abs(f n))���,
2129   REWRITE_TAC[sum, ABS_0, REAL_LE_REFL] THEN BETA_TAC THEN
2131   EXISTS_TAC ���abs(sum(m,n) f) + abs(f(m + n))��� THEN
2136         ==> (sum(m,n) f <= sum(m,n) g)���,
2138   INDUCT_TAC THEN REWRITE_TAC[sum, REAL_LE_REFL] THEN
2149         ==> (sum(m,n) f = sum(m,n) g)���,
2156   ���!f. (!n. 0 <= f(n)) ==> !m n. 0 <= sum(m,n) f���,
2158   REWRITE_TAC[sum, REAL_LE_REFL] THEN
2163         !n. 0 <= sum(m,n) f���,
2165   REWRITE_TAC[sum, REAL_LE_REFL] THEN
2171   ���!f m n. abs(sum(m,n) (\m. abs(f m))) = sum(m,n) (\m. abs(f m))���,
2177   ���!f m n. abs(sum(m,n) f) <= sum(m,n)(\n. abs(f n))���,
2179   REWRITE_TAC[sum, ABS_0, REAL_LE_REFL] THEN
2181   EXISTS_TAC ���abs(sum(m,n) f) + abs(f(m + n))��� THEN
2188             (!m n. m >= N ==> (sum(m,n) f = 0))���,
2194   SPEC_TAC(���n:num���,���n:num���) THEN INDUCT_TAC THEN REWRITE_TAC[sum]
2201       sum(m,n) (\n. f(n) + g(n))
2203       sum(m,n) f + sum(m,n) g���,
2205   ASM_REWRITE_TAC[sum, REAL_ADD_LID] THEN BETA_TAC THEN
2209   ���!f c m n. sum(m,n) (\n. c * f(n)) = c * sum(m,n) f���,
2211   ASM_REWRITE_TAC[sum, REAL_MUL_RZERO] THEN BETA_TAC THEN
2215   ���!f n d. sum(n,d) (\n. ~(f n)) = ~(sum(n,d) f)���,
2217   ASM_REWRITE_TAC[sum, REAL_NEG_0] THEN
2222       sum(m,n)(\n. (f n) - (g n))
2223     = sum(m,n) f - sum(m,n) g���,
2229         ==> (sum(m,n) f = sum(m,n) g)���,
2230   EVERY [GEN_TAC, GEN_TAC, GEN_TAC] THEN INDUCT_TAC THEN REWRITE_TAC[sum] THEN
2242       sum(0,n) f - (&n * c)
2244       sum(0,n)(\p. f(p) - c)���,
2245   INDUCT_TAC THEN REWRITE_TAC[sum, REAL_MUL_LZERO, REAL_SUB_REFL] THEN
2253         ==> (sum(m,n) f <= (&n * k))���,
2255   REWRITE_TAC[sum, REAL_MUL_LZERO, REAL_LE_REFL] THEN
2267   ���!n k f. sum(0,n)(\m. sum(m * k,k) f) = sum(0,n * k) f���,
2268   INDUCT_TAC THEN REWRITE_TAC[sum, MULT_CLAUSES] THEN
2273   ���!f n. sum(n,1) f = f(n)���,
2275   REWRITE_TAC[num_CONV ���1:num���, sum, ADD_CLAUSES, REAL_ADD_LID]);
2278   ���!f n. sum(n,2) f = f(n) + f(n + 1)���,
2280   REWRITE_TAC[sum, ADD_CLAUSES, REAL_ADD_LID]);
2284       sum(0,n)(\m. f(m + k))
2285     = sum(0,n + k) f - sum(0,k) f���,
2290   INDUCT_TAC THEN REWRITE_TAC[sum] THEN
2295   ���!f m k n. sum(m + k,n) f = sum(m,n)(\r. f(r + k))���,
2296   EVERY [GEN_TAC, GEN_TAC, GEN_TAC] THEN INDUCT_TAC THEN REWRITE_TAC[sum] THEN
2301   ���!m n. sum(m,n)(\r. 0) = 0���,
2302   GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[sum] THEN
2307         ==> !f. sum(0,n)(\n. f(p n)) = sum(0,n) f���,
2308   INDUCT_TAC THEN GEN_TAC THEN TRY(REWRITE_TAC[sum] THEN NO_TAC) THEN
2314   GEN_REWR_TAC RAND_CONV  [sum] THEN
2391     REWRITE_TAC[GSYM SUM_TWO, sum, ADD_CLAUSES] THEN BETA_TAC THEN
2405       sum(n,d) (\n. f(SUC n) - f(n))
2408   ASM_REWRITE_TAC[sum, ADD_CLAUSES, REAL_SUB_REFL] THEN