wneuper/isa: src/HOL/Algebra/abstract/NatSum.ML@299127ded09d

     1 (*

     2     Sums with naturals as index domain

     3     $Id$

     4     Author: Clemens Ballarin, started 12 December 1996

     5 *)

     7 section "Basic Properties";

     9 Goalw [SUM_def] "SUM 0 f = (f 0::'a::ring)";

    10 by (Asm_simp_tac 1);

    11 qed "SUM_0";

    13 Goalw [SUM_def]

    14   "SUM (Suc n) f = (f (Suc n) + SUM n f::'a::ring)";

    15 by (Simp_tac 1);

    16 qed "SUM_Suc";

    18 Addsimps [SUM_0, SUM_Suc];

    20 Goal

    21   "SUM (Suc n) f = (SUM n (%i. f (Suc i)) + f 0::'a::ring)";

    22 by (nat_ind_tac "n" 1);

    23 (* Base case *)

    24 by (Simp_tac 1);

    25 (* Induction step *)

    26 by (asm_full_simp_tac (simpset() addsimps [a_assoc]) 1);

    27 qed "SUM_Suc2";

    29 (* Congruence rules *)

    31 val [p_equal, p_context] = goal NatSum.thy

    32   "[| m = n; !!i. i <= n ==> f i = g i |] ==> SUM m f = (SUM n g::'a::ring)";

    33 by (simp_tac (simpset() addsimps [p_equal]) 1);

    34 by (cut_inst_tac [("n", "n")] le_refl 1);

    35 by (etac rev_mp 1);

    36 by (res_inst_tac [("P", "%k. k <= n --> SUM k f = SUM k g")] nat_induct 1);

    37 (* Base case *)

    38 by (simp_tac (simpset() addsimps [p_context]) 1);

    39 (* Induction step *)

    40 by (rtac impI 1);

    41 by (etac impE 1);

    42 by (rtac Suc_leD 1);

    43 by (assume_tac 1);

    44 by (asm_simp_tac (simpset() addsimps [p_context]) 1);

    45 qed "SUM_cong";

    47 Addcongs [SUM_cong];

    49 (* Results needed for the development of polynomials *)

    51 section "Ring Properties";

    53 Goal "SUM n (%i. <0>) = (<0>::'a::ring)";

    54 by (nat_ind_tac "n" 1);

    55 by (Simp_tac 1);

    56 by (Asm_simp_tac 1);

    57 qed "SUM_zero";

    59 Addsimps [SUM_zero];

    61 Goal

    62   "!!f::nat=>'a::ring. SUM n (%i. f i + g i) = SUM n f + SUM n g";

    63 by (nat_ind_tac "n" 1);

    64 (* Base case *)

    65 by (Simp_tac 1);

    66 (* Induction step *)

    67 by (asm_simp_tac (simpset() addsimps a_ac) 1);

    68 qed "SUM_add";

    70 Goal

    71   "!!a::'a::ring. SUM n f * a = SUM n (%i. f i * a)";

    72 by (nat_ind_tac "n" 1);

    73 (* Base case *)

    74 by (Simp_tac 1);

    75 (* Induction step *)

    76 by (asm_simp_tac (simpset() addsimps [l_distr]) 1);

    77 qed "SUM_ldistr";

    79 Goal

    80   "!!a::'a::ring. a * SUM n f = SUM n (%i. a * f i)";

    81 by (nat_ind_tac "n" 1);

    82 (* Base case *)

    83 by (Simp_tac 1);

    84 (* Induction step *)

    85 by (asm_simp_tac (simpset() addsimps [r_distr]) 1);

    86 qed "SUM_rdistr";

    88 section "Results for the Construction of Polynomials";

    90 goal Main.thy (* could go to Arith *)

    91   "!!j::nat. [| m <= j; Suc j <= n |] ==> (n - m) - Suc (j - m) = n - Suc j";

    92 by (asm_simp_tac (simpset() addsimps [Suc_diff_le RS sym]) 1);

    93 by (asm_simp_tac (simpset() addsimps [diff_right_cancel, less_imp_le]) 1);

    94 qed "Suc_diff_lemma";

    96 Goal

    97   "!!a::nat=>'a::ring. k <= n --> \

    98 \  SUM k (%j. SUM j (%i. a i * b (j-i)) * c (n-j)) = \

    99 \  SUM k (%j. a j * SUM (k-j) (%i. b i * c (n-j-i)))";

   100 by (nat_ind_tac "k" 1);

   101 (* Base case *)

   102 by (simp_tac (simpset() addsimps [m_assoc]) 1);

   103 (* Induction step *)

   104 by (rtac impI 1);

   105 by (etac impE 1);

   106 by (rtac Suc_leD 1);

   107 by (assume_tac 1);

   108 by (asm_simp_tac (simpset() addsimps a_ac@[Suc_diff_le, l_distr, r_distr, m_assoc, SUM_add]) 1);

   109 by (asm_simp_tac (simpset() addsimps a_ac@[Suc_diff_lemma, SUM_ldistr, m_assoc]) 1);

   110 qed "poly_assoc_lemma1";

   112 Goal

   113   "!!a::nat=>'a::ring. \

   114 \  SUM n (%j. SUM j (%i. a i * b (j-i)) * c (n-j)) = \

   115 \  SUM n (%j. a j * SUM (n-j) (%i. b i * c (n-j-i)))";

   116 by (rtac (poly_assoc_lemma1 RS mp) 1);

   117 by (rtac le_refl 1);

   118 qed "poly_assoc_lemma";

   120 goal Main.thy (* could go to Arith *)

   121   "!! n. Suc i <= n ==> Suc (a + (n - Suc i)) = a + (n - i)";

   122 by (asm_simp_tac (simpset() delsimps [add_Suc] addsimps [add_Suc_right RS sym, Suc_diff_Suc]) 1);

   123 qed "Suc_add_diff_Suc";

   125 goal Main.thy (* could go to Arith *)

   126   "!! n. [| Suc j <= n; i <= j |] ==> \

   127 \    n - Suc i - (n - Suc j) = n - i - (n - j)";

   128 by (res_inst_tac [("m1", "n - Suc i"), ("n1", "n - Suc j")]

   129   (diff_Suc_Suc RS subst) 1);

   130 by (subgoal_tac "Suc i <= n" 1);

   131 by (asm_simp_tac (simpset() delsimps [diff_Suc_Suc] addsimps [Suc_diff_Suc]) 1);

   132 by (fast_arith_tac 1);

   133 qed "diff_lemma2";

   135 Goal

   136   "!! a::nat=>'a::ring. j <= n --> \

   137 \    SUM j (%i. a i * b (n-i)) = SUM j (%i. a (n-i-(n-j)) * b (i+(n-j)))";

   138 by (nat_ind_tac "j" 1);

   139 (* Base case *)

   140 by (Simp_tac 1);

   141 (* Induction step *)

   142 by (rtac impI 1);

   143 by (etac impE 1);

   144 by (rtac Suc_leD 1);

   145 by (assume_tac 1);

   146 by (stac SUM_Suc2 1);

   147 by (stac SUM_Suc 1);

   148 by (asm_simp_tac (simpset()

   149     addsimps [a_comm, Suc_add_diff_Suc, diff_diff_cancel, diff_lemma2]) 1);

   150 qed "poly_comm_lemma1";

   152 Goal

   153  "!!a::nat=>'a::ring. SUM n (%i. a i * b (n-i)) = SUM n (%i. a (n-i) * b i)";

   154 by (cut_inst_tac [("j", "n"), ("n", "n")] poly_comm_lemma1 1);

   155 by (Asm_full_simp_tac 1);

   156 qed "poly_comm_lemma";

   158 section "Changing the Range of Summation";

   160 Goal

   161   "!! f::(nat=>'a::ring). \

   162 \    SUM n (%i. if i = x then f i else <0>) = (if x <= n then f x else <0>)";

   163 by (nat_ind_tac "n" 1);

   164 (* Base case *)

   165 by (Simp_tac 1);

   166 (* Induction step *)

   167 by (Asm_simp_tac 1);

   168 by (Clarify_tac 1);

   169 by (res_inst_tac [("f", "f")] arg_cong 1);

   170 by (arith_tac 1);

   171 qed "SUM_if_singleton";

   173 Goal

   174   "!! f::(nat=>'a::ring). \

   175 \    m <= n & (ALL i. m < i & i <= n --> f i = <0>) --> \

   176 \    SUM m f = SUM n f";

   177 by (nat_ind_tac "n" 1);

   178 (* Base case *)

   179 by (Simp_tac 1);

   180 (* Induction step *)

   181 by (case_tac "m <= n" 1);

   182 by (rtac impI 1);

   183 by (etac impE 1);

   184 by (SELECT_GOAL Auto_tac 1);

   185 by (etac conjE 1);

   186 by (dres_inst_tac [("x", "Suc n")] spec 1);

   187 by (asm_simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);

   188 (* case n < m, in fact m = Suc n *)

   189 by (rtac impI 1);

   190 by (etac conjE 1);

   191 by (subgoal_tac "m = Suc n" 1);

   192 by (Asm_simp_tac 1);

   193 by (fast_arith_tac 1);

   194 val SUM_shrink_lemma = result();

   196 Goal

   197   "!! f::(nat=>'a::ring). \

   198 \    [| m <= n; !!i. [| m < i; i <= n |] ==> f i = <0>; P (SUM n f) |] ==> \

   199 \      P (SUM m f)";

   200 by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1);

   201 by (Asm_full_simp_tac 1);

   202 qed "SUM_shrink";

   204 Goal

   205   "!! f::(nat=>'a::ring). \

   206 \    [| m <= n; !!i. [| m < i; i <= n |] ==> f i = <0>; P (SUM m f) |] ==> \

   207 \      P (SUM n f)";

   208 by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1);

   209 by (Asm_full_simp_tac 1);

   210 qed "SUM_extend";

   212 Goal

   213   "!! f::(nat=>'a::ring). \

   214 \    (ALL i. i < m --> f i = <0>) --> SUM d (%i. f (i+m)) = SUM (m+d) f";

   215 by (nat_ind_tac "d" 1);

   216 (* Base case *)

   217 by (nat_ind_tac "m" 1);

   218 by (Simp_tac 1);

   219 by (rtac impI 1);

   220 by (etac impE 1);

   221 by (Asm_simp_tac 1);

   222 by (subgoal_tac "SUM m f = <0>" 1);

   223 by (Asm_simp_tac 1);

   224 by (Asm_full_simp_tac 1);

   225 (* Induction step *)

   226 by (asm_simp_tac (simpset() addsimps add_ac) 1);

   227 val SUM_shrink_below_lemma = result();

   229 Goal

   230   "!! f::(nat=>'a::ring). \

   231 \    [| m <= n; !!i. i < m ==> f i = <0>; P (SUM (n-m) (%i. f (i+m))) |] ==> \

   232 \    P (SUM n f)";

   233 by (asm_full_simp_tac (simpset() addsimps

   234   [SUM_shrink_below_lemma, add_diff_inverse, leD]) 1);

   235 qed "SUM_extend_below";

   237 section "Result for the Univeral Property of Polynomials";

   239 Goal

   240   "!!f::nat=>'a::ring. j <= n + m --> \

   241 \    SUM j (%k. SUM k (%i. f i * g (k - i))) = \

   242 \    SUM j (%k. SUM (j - k) (%i. f k * g i))";

   243 by (nat_ind_tac "j" 1);

   244 (* Base case *)

   245 by (Simp_tac 1);

   246 (* Induction step *)

   247 by (simp_tac (simpset() addsimps [Suc_diff_le]) 1);

   248 by (simp_tac (simpset() addsimps [SUM_add]) 1);

   249 by (rtac impI 1);

   250 by (etac impE 1);

   251 by (dtac Suc_leD 1);

   252 by (assume_tac 1);

   253 by (asm_simp_tac (simpset() addsimps a_ac) 1);

   254 val DiagSum_lemma = result();

   256 Goal

   257   "!!f::nat=>'a::ring. \

   258 \    SUM (n + m) (%k. SUM k (%i. f i * g (k - i))) = \

   259 \    SUM (n + m) (%k. SUM (n + m - k) (%i. f k * g i))";

   260 by (rtac (DiagSum_lemma RS mp) 1);

   261 by (rtac le_refl 1);

   262 qed "DiagSum";

author	paulson
	Thu, 11 Nov 1999 10:25:29 +0100
changeset 8006	299127ded09d
parent 7998	3d0c34795831
child 8707	5de763446504
permissions	-rw-r--r--