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