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--
New theory header syntax.
     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