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