src/HOL/Complex/CSeries.thy
 author nipkow Mon Aug 16 14:22:27 2004 +0200 (2004-08-16) changeset 15131 c69542757a4d parent 15085 5693a977a767 child 15140 322485b816ac permissions -rw-r--r--
```     1 (*  Title       : CSeries.thy
```
```     2     Author      : Jacques D. Fleuriot
```
```     3     Copyright   : 2002  University of Edinburgh
```
```     4 *)
```
```     5
```
```     6 header{*Finite Summation and Infinite Series for Complex Numbers*}
```
```     7
```
```     8 theory CSeries
```
```     9 import CStar
```
```    10 begin
```
```    11
```
```    12 consts sumc :: "[nat,nat,(nat=>complex)] => complex"
```
```    13 primrec
```
```    14    sumc_0:   "sumc m 0 f = 0"
```
```    15    sumc_Suc: "sumc m (Suc n) f = (if n < m then 0 else sumc m n f + f(n))"
```
```    16
```
```    17 (*
```
```    18 constdefs
```
```    19
```
```    20    needs convergence of complex sequences
```
```    21
```
```    22   csums  :: [nat=>complex,complex] => bool     (infixr 80)
```
```    23    "f sums s  == (%n. sumr 0 n f) ----C> s"
```
```    24
```
```    25    csummable :: (nat=>complex) => bool
```
```    26    "csummable f == (EX s. f csums s)"
```
```    27
```
```    28    csuminf   :: (nat=>complex) => complex
```
```    29    "csuminf f == (@s. f csums s)"
```
```    30 *)
```
```    31
```
```    32 lemma sumc_Suc_zero [simp]: "sumc (Suc n) n f = 0"
```
```    33 by (induct_tac "n", auto)
```
```    34
```
```    35 lemma sumc_eq_bounds [simp]: "sumc m m f = 0"
```
```    36 by (induct_tac "m", auto)
```
```    37
```
```    38 lemma sumc_Suc_eq [simp]: "sumc m (Suc m) f = f(m)"
```
```    39 by auto
```
```    40
```
```    41 lemma sumc_add_lbound_zero [simp]: "sumc (m+k) k f = 0"
```
```    42 by (induct_tac "k", auto)
```
```    43
```
```    44 lemma sumc_add: "sumc m n f + sumc m n g = sumc m n (%n. f n + g n)"
```
```    45 apply (induct_tac "n")
```
```    46 apply (auto simp add: add_ac)
```
```    47 done
```
```    48
```
```    49 lemma sumc_mult: "r * sumc m n f = sumc m n (%n. r * f n)"
```
```    50 apply (induct_tac "n", auto)
```
```    51 apply (auto simp add: right_distrib)
```
```    52 done
```
```    53
```
```    54 lemma sumc_split_add [rule_format]:
```
```    55      "n < p --> sumc 0 n f + sumc n p f = sumc 0 p f"
```
```    56 apply (induct_tac "p")
```
```    57 apply (auto dest!: leI dest: le_anti_sym)
```
```    58 done
```
```    59
```
```    60 lemma sumc_split_add_minus:
```
```    61      "n < p ==> sumc 0 p f + - sumc 0 n f = sumc n p f"
```
```    62 apply (drule_tac f1 = f in sumc_split_add [symmetric])
```
```    63 apply (simp add: add_ac)
```
```    64 done
```
```    65
```
```    66 lemma sumc_cmod: "cmod(sumc m n f) \<le> sumr m n (%i. cmod(f i))"
```
```    67 apply (induct_tac "n")
```
```    68 apply (auto intro: complex_mod_triangle_ineq [THEN order_trans])
```
```    69 done
```
```    70
```
```    71 lemma sumc_fun_eq [rule_format (no_asm)]:
```
```    72      "(\<forall>r. m \<le> r & r < n --> f r = g r) --> sumc m n f = sumc m n g"
```
```    73 by (induct_tac "n", auto)
```
```    74
```
```    75 lemma sumc_const [simp]: "sumc 0 n (%i. r) = complex_of_real (real n) * r"
```
```    76 apply (induct_tac "n")
```
```    77 apply (auto simp add: left_distrib real_of_nat_Suc)
```
```    78 done
```
```    79
```
```    80 lemma sumc_add_mult_const:
```
```    81      "sumc 0 n f + -(complex_of_real(real n) * r) = sumc 0 n (%i. f i + -r)"
```
```    82 by (simp add: sumc_add [symmetric])
```
```    83
```
```    84 lemma sumc_diff_mult_const:
```
```    85      "sumc 0 n f - (complex_of_real(real n)*r) = sumc 0 n (%i. f i - r)"
```
```    86 by (simp add: diff_minus sumc_add_mult_const)
```
```    87
```
```    88 lemma sumc_less_bounds_zero [rule_format]: "n < m --> sumc m n f = 0"
```
```    89 by (induct_tac "n", auto)
```
```    90
```
```    91 lemma sumc_minus: "sumc m n (%i. - f i) = - sumc m n f"
```
```    92 by (induct_tac "n", auto)
```
```    93
```
```    94 lemma sumc_shift_bounds: "sumc (m+k) (n+k) f = sumc m n (%i. f(i + k))"
```
```    95 by (induct_tac "n", auto)
```
```    96
```
```    97 lemma sumc_minus_one_complexpow_zero [simp]:
```
```    98      "sumc 0 (2*n) (%i. (-1) ^ Suc i) = 0"
```
```    99 by (induct_tac "n", auto)
```
```   100
```
```   101 lemma sumc_interval_const [rule_format (no_asm)]:
```
```   102      "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na
```
```   103       --> sumc m na f = (complex_of_real(real (na - m)) * r)"
```
```   104 apply (induct_tac "na")
```
```   105 apply (auto simp add: Suc_diff_le real_of_nat_Suc left_distrib)
```
```   106 done
```
```   107
```
```   108 lemma sumc_interval_const2 [rule_format (no_asm)]:
```
```   109      "(\<forall>n. m \<le> n --> f n = r) & m \<le> na
```
```   110       --> sumc m na f = (complex_of_real(real (na - m)) * r)"
```
```   111 apply (induct_tac "na")
```
```   112 apply (auto simp add: left_distrib Suc_diff_le real_of_nat_Suc)
```
```   113 done
```
```   114
```
```   115 (***
```
```   116 Goal "(\<forall>n. m \<le> n --> 0 \<le> cmod(f n)) & m < k --> cmod(sumc 0 m f) \<le> cmod(sumc 0 k f)"
```
```   117 by (induct_tac "k" 1)
```
```   118 by (Step_tac 1)
```
```   119 by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [less_Suc_eq_le])));
```
```   120 by (ALLGOALS(dres_inst_tac [("x","n")] spec));
```
```   121 by (Step_tac 1)
```
```   122 by (dtac le_imp_less_or_eq 1 THEN Step_tac 1)
```
```   123 by (dtac add_mono 2)
```
```   124 by (dres_inst_tac [("i","sumr 0 m f")] (order_refl RS add_mono) 1);
```
```   125 by Auto_tac
```
```   126 qed_spec_mp "sumc_le";
```
```   127
```
```   128 Goal "!!f g. (\<forall>r. m \<le> r & r < n --> f r \<le> g r) \
```
```   129 \                --> sumc m n f \<le> sumc m n g";
```
```   130 by (induct_tac "n" 1)
```
```   131 by (auto_tac (claset() addIs [add_mono],
```
```   132     simpset() addsimps [le_def]));
```
```   133 qed_spec_mp "sumc_le2";
```
```   134
```
```   135 Goal "(\<forall>n. 0 \<le> f n) --> 0 \<le> sumc m n f";
```
```   136 by (induct_tac "n" 1)
```
```   137 by Auto_tac
```
```   138 by (dres_inst_tac [("x","n")] spec 1);
```
```   139 by (arith_tac 1)
```
```   140 qed_spec_mp "sumc_ge_zero";
```
```   141
```
```   142 Goal "(\<forall>n. m \<le> n --> 0 \<le> f n) --> 0 \<le> sumc m n f";
```
```   143 by (induct_tac "n" 1)
```
```   144 by Auto_tac
```
```   145 by (dres_inst_tac [("x","n")] spec 1);
```
```   146 by (arith_tac 1)
```
```   147 qed_spec_mp "sumc_ge_zero2";
```
```   148 ***)
```
```   149
```
```   150 lemma sumr_cmod_ge_zero [iff]: "0 \<le> sumr m n (%n. cmod (f n))"
```
```   151 by (induct_tac "n", auto simp add: add_increasing)
```
```   152
```
```   153 lemma rabs_sumc_cmod_cancel [simp]:
```
```   154      "abs (sumr m n (%n. cmod (f n))) = (sumr m n (%n. cmod (f n)))"
```
```   155 by (simp add: abs_if linorder_not_less)
```
```   156
```
```   157 lemma sumc_one_lb_complexpow_zero [simp]: "sumc 1 n (%n. f(n) * 0 ^ n) = 0"
```
```   158 apply (induct_tac "n")
```
```   159 apply (case_tac [2] "n", auto)
```
```   160 done
```
```   161
```
```   162 lemma sumc_diff: "sumc m n f - sumc m n g = sumc m n (%n. f n - g n)"
```
```   163 by (simp add: diff_minus sumc_add [symmetric] sumc_minus)
```
```   164
```
```   165 lemma sumc_subst [rule_format (no_asm)]:
```
```   166      "(\<forall>p. (m \<le> p & p < m + n --> (f p = g p))) --> sumc m n f = sumc m n g"
```
```   167 by (induct_tac "n", auto)
```
```   168
```
```   169 lemma sumc_group [simp]:
```
```   170      "sumc 0 n (%m. sumc (m * k) (m*k + k) f) = sumc 0 (n * k) f"
```
```   171 apply (subgoal_tac "k = 0 | 0 < k", auto)
```
```   172 apply (induct_tac "n")
```
```   173 apply (auto simp add: sumc_split_add add_commute)
```
```   174 done
```
```   175
```
```   176 ML
```
```   177 {*
```
```   178 val sumc_Suc_zero = thm "sumc_Suc_zero";
```
```   179 val sumc_eq_bounds = thm "sumc_eq_bounds";
```
```   180 val sumc_Suc_eq = thm "sumc_Suc_eq";
```
```   181 val sumc_add_lbound_zero = thm "sumc_add_lbound_zero";
```
```   182 val sumc_add = thm "sumc_add";
```
```   183 val sumc_mult = thm "sumc_mult";
```
```   184 val sumc_split_add = thm "sumc_split_add";
```
```   185 val sumc_split_add_minus = thm "sumc_split_add_minus";
```
```   186 val sumc_cmod = thm "sumc_cmod";
```
```   187 val sumc_fun_eq = thm "sumc_fun_eq";
```
```   188 val sumc_const = thm "sumc_const";
```
```   189 val sumc_add_mult_const = thm "sumc_add_mult_const";
```
```   190 val sumc_diff_mult_const = thm "sumc_diff_mult_const";
```
```   191 val sumc_less_bounds_zero = thm "sumc_less_bounds_zero";
```
```   192 val sumc_minus = thm "sumc_minus";
```
```   193 val sumc_shift_bounds = thm "sumc_shift_bounds";
```
```   194 val sumc_minus_one_complexpow_zero = thm "sumc_minus_one_complexpow_zero";
```
```   195 val sumc_interval_const = thm "sumc_interval_const";
```
```   196 val sumc_interval_const2 = thm "sumc_interval_const2";
```
```   197 val sumr_cmod_ge_zero = thm "sumr_cmod_ge_zero";
```
```   198 val rabs_sumc_cmod_cancel = thm "rabs_sumc_cmod_cancel";
```
```   199 val sumc_one_lb_complexpow_zero = thm "sumc_one_lb_complexpow_zero";
```
```   200 val sumc_diff = thm "sumc_diff";
```
```   201 val sumc_subst = thm "sumc_subst";
```
```   202 val sumc_group = thm "sumc_group";
```
```   203 *}
```
```   204
```
```   205 end
```
```   206
```