src/HOL/Complex/CSeries.ML
author paulson
Tue, 03 Feb 2004 11:06:36 +0100
changeset 14373 67a628beb981
parent 14334 6137d24eef79
permissions -rw-r--r--
tidying of the complex numbers
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13957
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
     1
(*  Title       : CSeries.ML
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
     2
    Author      : Jacques D. Fleuriot
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
     3
    Copyright   : 2002  University of Edinburgh
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
     4
    Description : Finite summation and infinite series for complex numbers
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
     5
*)
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
     6
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
     7
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
     8
Goal "sumc (Suc n) n f = 0";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
     9
by (induct_tac "n" 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    10
by (Auto_tac);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    11
qed "sumc_Suc_zero";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    12
Addsimps [sumc_Suc_zero];
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    13
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    14
Goal "sumc m m f = 0";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    15
by (induct_tac "m" 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    16
by (Auto_tac);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    17
qed "sumc_eq_bounds";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    18
Addsimps [sumc_eq_bounds];
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    19
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    20
Goal "sumc m (Suc m) f = f(m)";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    21
by (Auto_tac);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    22
qed "sumc_Suc_eq";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    23
Addsimps [sumc_Suc_eq];
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    24
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    25
Goal "sumc (m+k) k f = 0";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    26
by (induct_tac "k" 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    27
by (Auto_tac);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    28
qed "sumc_add_lbound_zero";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    29
Addsimps [sumc_add_lbound_zero];
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    30
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    31
Goal "sumc m n f + sumc m n g = sumc m n (%n. f n + g n)";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    32
by (induct_tac "n" 1);
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 13957
diff changeset
    33
by (auto_tac (claset(),simpset() addsimps add_ac));
13957
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    34
qed "sumc_add";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    35
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    36
Goal "r * sumc m n f = sumc m n (%n. r * f n)";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    37
by (induct_tac "n" 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    38
by (Auto_tac);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    39
by (auto_tac (claset(),simpset() addsimps 
14373
67a628beb981 tidying of the complex numbers
paulson
parents: 14334
diff changeset
    40
    [right_distrib]));
13957
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    41
qed "sumc_mult";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    42
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    43
Goal "n < p --> sumc 0 n f + sumc n p f = sumc 0 p f";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    44
by (induct_tac "p" 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    45
by (auto_tac (claset() addSDs [CLAIM "n < Suc na ==> n <= na",
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    46
    leI] addDs [le_anti_sym], simpset()));
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    47
qed_spec_mp "sumc_split_add";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    48
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    49
Goal "n < p ==> sumc 0 p f + \
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    50
\                - sumc 0 n f = sumc n p f";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    51
by (dres_inst_tac [("f1","f")] (sumc_split_add RS sym) 1);
14373
67a628beb981 tidying of the complex numbers
paulson
parents: 14334
diff changeset
    52
by (asm_simp_tac (simpset() addsimps add_ac) 1);
13957
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    53
qed "sumc_split_add_minus";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    54
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    55
Goal "cmod(sumc m n f) <= sumr m n (%i. cmod(f i))";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    56
by (induct_tac "n" 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    57
by (auto_tac (claset() addIs [complex_mod_triangle_ineq RS order_trans], 
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    58
              simpset()));
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    59
qed "sumc_cmod";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    60
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    61
Goal "!!f g. (ALL r. m <= r & r < n --> f r = g r) \
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    62
\                --> sumc m n f = sumc m n g";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    63
by (induct_tac "n" 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    64
by (Auto_tac);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    65
qed_spec_mp "sumc_fun_eq";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    66
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    67
Goal "sumc 0 n (%i. r) = complex_of_real (real n) * r";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    68
by (induct_tac "n" 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    69
by (auto_tac (claset(),
14373
67a628beb981 tidying of the complex numbers
paulson
parents: 14334
diff changeset
    70
              simpset() addsimps [left_distrib,
13957
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    71
                                  complex_of_real_add RS sym,
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    72
                                  real_of_nat_Suc]));
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    73
qed "sumc_const";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    74
Addsimps [sumc_const];
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    75
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    76
Goal "sumc 0 n f + -(complex_of_real(real n) * r) = sumc 0 n (%i. f i + -r)";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    77
by (full_simp_tac (simpset() addsimps [sumc_add RS sym]) 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    78
qed "sumc_add_mult_const";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    79
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    80
Goalw [complex_diff_def] 
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    81
     "sumc 0 n f - (complex_of_real(real n)*r) = sumc 0 n (%i. f i - r)";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    82
by (full_simp_tac (simpset() addsimps [sumc_add_mult_const]) 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    83
qed "sumc_diff_mult_const";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    84
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    85
Goal "n < m --> sumc m n f = 0";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    86
by (induct_tac "n" 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    87
by Auto_tac;
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    88
qed_spec_mp "sumc_less_bounds_zero";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    89
Addsimps [sumc_less_bounds_zero];
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    90
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    91
Goal "sumc m n (%i. - f i) = - sumc m n f";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    92
by (induct_tac "n" 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    93
by Auto_tac;
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    94
qed "sumc_minus";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    95
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    96
Goal "sumc (m+k) (n+k) f = sumc m n (%i. f(i + k))";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    97
by (induct_tac "n" 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    98
by (Auto_tac);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
    99
qed "sumc_shift_bounds";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   100
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   101
Goal "sumc 0 (2*n) (%i. (-1) ^ Suc i) = 0";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   102
by (induct_tac "n" 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   103
by (Auto_tac);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   104
qed "sumc_minus_one_complexpow_zero";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   105
Addsimps [sumc_minus_one_complexpow_zero];
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   106
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   107
Goal "(ALL n. m <= Suc n --> f n = r) & m <= na \
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   108
\                --> sumc m na f = (complex_of_real(real (na - m)) * r)";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   109
by (induct_tac "na" 1);
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 13957
diff changeset
   110
by (auto_tac (claset(),simpset() addsimps [left_distrib, Suc_diff_n,
13957
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   111
                                      real_of_nat_Suc,complex_of_real_add RS sym,
14373
67a628beb981 tidying of the complex numbers
paulson
parents: 14334
diff changeset
   112
                                      left_distrib]));
13957
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   113
qed_spec_mp "sumc_interval_const";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   114
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   115
Goal "(ALL n. m <= n --> f n = r) & m <= na \
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   116
\     --> sumc m na f = (complex_of_real(real (na - m)) * r)";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   117
by (induct_tac "na" 1);
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 13957
diff changeset
   118
by (auto_tac (claset(),simpset() addsimps [left_distrib, Suc_diff_n,
13957
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   119
                                      real_of_nat_Suc,complex_of_real_add RS sym,
14373
67a628beb981 tidying of the complex numbers
paulson
parents: 14334
diff changeset
   120
                                      left_distrib]));
13957
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   121
qed_spec_mp "sumc_interval_const2";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   122
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   123
(*** 
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   124
Goal "(ALL n. m <= n --> 0 <= cmod(f n)) & m < k --> cmod(sumc 0 m f) <= cmod(sumc 0 k f)";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   125
by (induct_tac "k" 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   126
by (Step_tac 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   127
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [less_Suc_eq_le])));
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   128
by (ALLGOALS(dres_inst_tac [("x","n")] spec));
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   129
by (Step_tac 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   130
by (dtac le_imp_less_or_eq 1 THEN Step_tac 1);
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 13957
diff changeset
   131
by (dtac add_mono 2);
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 13957
diff changeset
   132
by (dres_inst_tac [("i","sumr 0 m f")] (order_refl RS add_mono) 1);
13957
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   133
by (Auto_tac);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   134
qed_spec_mp "sumc_le";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   135
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   136
Goal "!!f g. (ALL r. m <= r & r < n --> f r <= g r) \
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   137
\                --> sumc m n f <= sumc m n g";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   138
by (induct_tac "n" 1);
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 13957
diff changeset
   139
by (auto_tac (claset() addIs [add_mono],
13957
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   140
    simpset() addsimps [le_def]));
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   141
qed_spec_mp "sumc_le2";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   142
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   143
Goal "(ALL n. 0 <= f n) --> 0 <= sumc m n f";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   144
by (induct_tac "n" 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   145
by Auto_tac;
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   146
by (dres_inst_tac [("x","n")] spec 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   147
by (arith_tac 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   148
qed_spec_mp "sumc_ge_zero";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   149
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   150
Goal "(ALL n. m <= n --> 0 <= f n) --> 0 <= sumc m n f";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   151
by (induct_tac "n" 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   152
by Auto_tac;
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   153
by (dres_inst_tac [("x","n")] spec 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   154
by (arith_tac 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   155
qed_spec_mp "sumc_ge_zero2";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   156
***)
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   157
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   158
Goal "0 <= sumr m n (%n. cmod (f n))";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   159
by (induct_tac "n" 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   160
by Auto_tac;
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   161
by (res_inst_tac [("j","0")] real_le_trans 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   162
by Auto_tac;
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   163
qed "sumr_cmod_ge_zero";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   164
Addsimps [sumr_cmod_ge_zero];
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   165
AddSIs [sumr_cmod_ge_zero]; 
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   166
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   167
Goal "abs (sumr m n (%n. cmod (f n))) = (sumr m n (%n. cmod (f n)))";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   168
by (rtac (abs_eqI1 RS ssubst) 1 THEN Auto_tac);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   169
qed "rabs_sumc_cmod_cancel";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   170
Addsimps [rabs_sumc_cmod_cancel];
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   171
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   172
Goal "ALL n. N <= n --> f n = 0 \
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   173
\     ==> ALL m n. N <= m --> sumc m n f = 0";   
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   174
by (Step_tac 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   175
by (induct_tac "n" 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   176
by (Auto_tac);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   177
qed "sumc_zero";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   178
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   179
Goal "ALL n. N <= n --> f (Suc n) = 0 \
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   180
\     ==> ALL m n. Suc N <= m --> sumc m n f = 0";   
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   181
by (rtac sumc_zero 1 THEN Step_tac 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   182
by (dres_inst_tac [("x","n - 1")] spec 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   183
by Auto_tac;
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   184
by (arith_tac 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   185
qed "fun_zero_sumc_zero";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   186
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   187
Goal "sumc 1 n (%n. f(n) * 0 ^ n) = 0";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   188
by (induct_tac "n" 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   189
by (case_tac "n" 2);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   190
by Auto_tac;
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   191
qed "sumc_one_lb_complexpow_zero";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   192
Addsimps [sumc_one_lb_complexpow_zero];
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   193
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   194
Goalw [complex_diff_def] "sumc m n f - sumc m n g = sumc m n (%n. f n - g n)";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   195
by (simp_tac (simpset() addsimps [sumc_add RS sym,sumc_minus]) 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   196
qed "sumc_diff";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   197
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   198
Goal "(ALL p. (m <= p & p < m + n --> (f p = g p))) --> sumc m n f = sumc m n g";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   199
by (induct_tac "n" 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   200
by (Auto_tac);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   201
qed_spec_mp "sumc_subst";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   202
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   203
Goal "sumc 0 n (%m. sumc (m * k) (m*k + k) f) = sumc 0 (n * k) f";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   204
by (subgoal_tac "k = 0 | 0 < k" 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   205
by (Auto_tac);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   206
by (induct_tac "n" 1);
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   207
by (auto_tac (claset(),simpset() addsimps [sumc_split_add,add_commute]));
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   208
qed "sumc_group";
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   209
Addsimps [sumc_group];
10dbf16be15f new session Complex for the complex numbers
paulson
parents:
diff changeset
   210