1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Algebra/poly/Degree.ML	Fri Nov 05 11:14:26 1999 +0100
     1.3 @@ -0,0 +1,363 @@
     1.4 +(*
     1.5 +    Degree of polynomials
     1.6 +    $Id$
     1.7 +    written by Clemens Ballarin, started 22 January 1997
     1.8 +*)
     1.9 +
    1.10 +(* Relating degree and bound *)
    1.11 +
    1.12 +goal ProtoPoly.thy
    1.13 +  "!! f. [| bound m f; f n ~= <0> |] ==> n <= m";
    1.14 +by (rtac classical 1);
    1.15 +by (dtac not_leE 1);
    1.16 +by (dtac boundD 1 THEN atac 1);
    1.17 +by (etac notE 1);
    1.18 +by (assume_tac 1);
    1.19 +qed "below_bound";
    1.20 +
    1.21 +goal UnivPoly.thy "bound (LEAST n. bound n (Rep_UP p)) (Rep_UP p)";
    1.22 +by (rtac exE 1);
    1.23 +by (rtac LeastI 2);
    1.24 +by (assume_tac 2);
    1.25 +by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
    1.26 +by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
    1.27 +qed "Least_is_bound";
    1.28 +
    1.29 +Goalw [coeff_def, deg_def]
    1.30 +  "!! p. ALL m. n < m --> coeff m p = <0> ==> deg p <= n";
    1.31 +by (rtac Least_le 1);
    1.32 +by (Fast_tac 1);
    1.33 +qed "deg_aboveI";
    1.34 +
    1.35 +Goalw [coeff_def, deg_def]
    1.36 +  "!! p. (n ~= 0 --> coeff n p ~= <0>) ==> n <= deg p";
    1.37 +by (case_tac "n = 0" 1);
    1.38 +(* Case n=0 *)
    1.39 +by (Asm_simp_tac 1);
    1.40 +(* Case n~=0 *)
    1.41 +by (rotate_tac 1 1);
    1.42 +by (Asm_full_simp_tac 1);
    1.43 +by (rtac below_bound 1);
    1.44 +by (assume_tac 2);
    1.45 +by (rtac Least_is_bound 1);
    1.46 +qed "deg_belowI";
    1.47 +
    1.48 +Goalw [coeff_def, deg_def]
    1.49 +  "!! p. deg p < m ==> coeff m p = <0>";
    1.50 +by (rtac exE 1); (* create !! x. *)
    1.51 +by (rtac boundD 2);
    1.52 +by (assume_tac 3);
    1.53 +by (rtac LeastI 2);
    1.54 +by (assume_tac 2);
    1.55 +by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
    1.56 +by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
    1.57 +qed "deg_aboveD";
    1.58 +
    1.59 +Goalw [deg_def]
    1.60 +  "!! p. deg p = Suc y ==> ~ bound y (Rep_UP p)";
    1.61 +by (rtac not_less_Least 1);
    1.62 +by (Asm_simp_tac 1);
    1.63 +val lemma1 = result();
    1.64 +
    1.65 +Goalw [deg_def, coeff_def]
    1.66 +  "!! p. deg p = Suc y ==> coeff (deg p) p ~= <0>";
    1.67 +by (rtac classical 1);
    1.68 +by (dtac notnotD 1);
    1.69 +by (cut_inst_tac [("p", "p")] Least_is_bound 1);
    1.70 +by (subgoal_tac "bound y (Rep_UP p)" 1);
    1.71 +(* prove subgoal *)
    1.72 +by (rtac boundI 2);  
    1.73 +by (case_tac "Suc y < m" 2);
    1.74 +(* first case *)
    1.75 +by (rtac boundD 2);  
    1.76 +by (assume_tac 2);
    1.77 +by (Asm_simp_tac 2);
    1.78 +(* second case *)
    1.79 +by (dtac leI 2);
    1.80 +by (dtac Suc_leI 2);
    1.81 +by (dtac le_anti_sym 2);
    1.82 +by (assume_tac 2);
    1.83 +by (Asm_full_simp_tac 2);
    1.84 +(* end prove subgoal *)
    1.85 +by (fold_goals_tac [deg_def]);
    1.86 +by (dtac lemma1 1);
    1.87 +by (etac notE 1);
    1.88 +by (assume_tac 1);
    1.89 +val lemma2 = result();
    1.90 +
    1.91 +Goal
    1.92 +  "!! p. deg p ~= 0 ==> coeff (deg p) p ~= <0>";
    1.93 +by (rtac lemma2 1);
    1.94 +by (Full_simp_tac 1);
    1.95 +by (dtac Suc_pred 1);
    1.96 +by (rtac sym 1);
    1.97 +by (Asm_simp_tac 1);
    1.98 +qed "deg_lcoeff";
    1.99 +
   1.100 +Goal
   1.101 +  "!! p. p ~= <0> ==> coeff (deg p) p ~= <0>";
   1.102 +by (etac contrapos 1);
   1.103 +by (ftac contrapos2 1);
   1.104 +by (rtac deg_lcoeff 1);
   1.105 +by (assume_tac 1);
   1.106 +by (rtac up_eqI 1);
   1.107 +by (case_tac "n=0" 1);
   1.108 +by (rotate_tac ~2 1);
   1.109 +by (Asm_full_simp_tac 1);
   1.110 +by (asm_full_simp_tac (simpset() addsimps [deg_aboveD]) 1);
   1.111 +qed "nonzero_lcoeff";
   1.112 +
   1.113 +Goal "(deg p <= n) = bound n (Rep_UP p)";
   1.114 +by (rtac iffI 1);
   1.115 +(* ==> *)
   1.116 +by (rtac boundI 1);
   1.117 +by (fold_goals_tac [coeff_def]);
   1.118 +by (rtac deg_aboveD 1);
   1.119 +by (fast_arith_tac 1);
   1.120 +(* <== *)
   1.121 +by (rtac deg_aboveI 1);
   1.122 +by (rewtac coeff_def);
   1.123 +by (Fast_tac 1);
   1.124 +qed "deg_above_is_bound";
   1.125 +
   1.126 +(* Lemmas on the degree function *)
   1.127 +
   1.128 +Goalw [max_def]
   1.129 +  "!! p::'a::ring up. deg (p + q) <= max (deg p) (deg q)";
   1.130 +by (case_tac "deg p <= deg q" 1);
   1.131 +(* case deg p <= deg q *)
   1.132 +by (rtac deg_aboveI 1);
   1.133 +by (Asm_simp_tac 1);
   1.134 +by (strip_tac 1);
   1.135 +by (dtac le_less_trans 1);
   1.136 +by (assume_tac 1);
   1.137 +by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
   1.138 +(* case deg p > deg q *)
   1.139 +by (rtac deg_aboveI 1);
   1.140 +by (Asm_simp_tac 1);
   1.141 +by (dtac not_leE 1);
   1.142 +by (strip_tac 1);
   1.143 +by (dtac less_trans 1);
   1.144 +by (assume_tac 1);
   1.145 +by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
   1.146 +qed "deg_add";
   1.147 +
   1.148 +Goal "!!p::('a::ring up). deg p < deg q ==> deg (p + q) = deg q";
   1.149 +by (rtac order_antisym 1);
   1.150 +by (rtac le_trans 1);
   1.151 +by (rtac deg_add 1);
   1.152 +by (Asm_simp_tac 1);
   1.153 +by (rtac deg_belowI 1);
   1.154 +by (asm_simp_tac (simpset() addsimps [deg_aboveD, deg_lcoeff]) 1);
   1.155 +qed "deg_add_equal";
   1.156 +
   1.157 +Goal "deg (monom m::'a::ring up) = m";
   1.158 +by (rtac le_anti_sym 1);
   1.159 +(* <= *)
   1.160 +by (asm_simp_tac 
   1.161 +  (simpset() addsimps [deg_aboveI, less_not_refl2 RS not_sym]) 1);
   1.162 +(* >= *)
   1.163 +by (asm_simp_tac 
   1.164 +  (simpset() addsimps [deg_belowI, less_not_refl2 RS not_sym]) 1);
   1.165 +qed "deg_monom";
   1.166 +
   1.167 +Goal "!! a::'a::ring. deg (const a) = 0";
   1.168 +by (rtac le_anti_sym 1);
   1.169 +by (rtac deg_aboveI 1);
   1.170 +by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
   1.171 +by (rtac deg_belowI 1);
   1.172 +by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
   1.173 +qed "deg_const";
   1.174 +
   1.175 +Goal "deg (<0>::'a::ringS up) = 0";
   1.176 +by (rtac le_anti_sym 1);
   1.177 +by (rtac deg_aboveI 1);
   1.178 +by (Simp_tac 1);
   1.179 +by (rtac deg_belowI 1);
   1.180 +by (Simp_tac 1);
   1.181 +qed "deg_zero";
   1.182 +
   1.183 +Goal "deg (<1>::'a::ring up) = 0";
   1.184 +by (rtac le_anti_sym 1);
   1.185 +by (rtac deg_aboveI 1);
   1.186 +by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
   1.187 +by (rtac deg_belowI 1);
   1.188 +by (Simp_tac 1);
   1.189 +qed "deg_one";
   1.190 +
   1.191 +Goal "!!p::('a::ring) up. deg (-p) = deg p";
   1.192 +by (rtac le_anti_sym 1);
   1.193 +(* <= *)
   1.194 +by (simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1);
   1.195 +by (simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff, uminus_monom_neq]) 1);
   1.196 +qed "deg_uminus";
   1.197 +
   1.198 +Addsimps [deg_monom, deg_const, deg_zero, deg_one, deg_uminus];
   1.199 +
   1.200 +Goal
   1.201 +  "!! a::'a::ring. deg (a *s p) <= (if a = <0> then 0 else deg p)";
   1.202 +by (case_tac "a = <0>" 1);
   1.203 +by (REPEAT (asm_simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1));
   1.204 +qed "deg_smult_ring";
   1.205 +
   1.206 +Goal
   1.207 +  "!! a::'a::domain. deg (a *s p) = (if a = <0> then 0 else deg p)";
   1.208 +by (rtac le_anti_sym 1);
   1.209 +by (rtac deg_smult_ring 1);
   1.210 +by (case_tac "a = <0>" 1);
   1.211 +by (REPEAT (asm_simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff]) 1));
   1.212 +qed "deg_smult";
   1.213 +
   1.214 +Goal
   1.215 +  "!! p::'a::ring up. [| deg p + deg q < k |] ==> \
   1.216 +\       coeff i p * coeff (k - i) q = <0>";
   1.217 +by (simp_tac (simpset() addsimps [coeff_def]) 1);
   1.218 +by (rtac bound_mult_zero 1);
   1.219 +by (assume_tac 3);
   1.220 +by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
   1.221 +by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
   1.222 +qed "deg_above_mult_zero";
   1.223 +
   1.224 +Goal
   1.225 +  "!! p::'a::ring up. deg (p * q) <= deg p + deg q";
   1.226 +by (rtac deg_aboveI 1);
   1.227 +by (asm_simp_tac (simpset() addsimps [deg_above_mult_zero]) 1);
   1.228 +qed "deg_mult_ring";
   1.229 +
   1.230 +goal Main.thy 
   1.231 +  "!!k::nat. k < n ==> m < n + m - k";
   1.232 +by (arith_tac 1);
   1.233 +qed "less_add_diff";
   1.234 +
   1.235 +Goal "!!p. coeff n p ~= <0> ==> n <= deg p";
   1.236 +(* More general than deg_belowI, and simplifies the next proof! *)
   1.237 +by (rtac deg_belowI 1);
   1.238 +by (Fast_tac 1);
   1.239 +qed "deg_below2I";
   1.240 +
   1.241 +Goal
   1.242 +  "!! p::'a::domain up. \
   1.243 +\    [| p ~= <0>; q ~= <0> |] ==> deg (p * q) = deg p + deg q";
   1.244 +by (rtac le_anti_sym 1);
   1.245 +by (rtac deg_mult_ring 1);
   1.246 +(* deg p + deg q <= deg (p * q) *)
   1.247 +by (rtac deg_below2I 1);
   1.248 +by (Simp_tac 1);
   1.249 +(*
   1.250 +by (rtac conjI 1);
   1.251 +by (rtac impI 1);
   1.252 +*)
   1.253 +by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
   1.254 +by (rtac le_add1 1);
   1.255 +by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
   1.256 +by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
   1.257 +by (rtac le_refl 1);
   1.258 +by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
   1.259 +by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
   1.260 +(*
   1.261 +by (rtac impI 1);
   1.262 +by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
   1.263 +by (rtac le_add1 1);
   1.264 +by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
   1.265 +by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
   1.266 +by (rtac le_refl 1);
   1.267 +by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
   1.268 +by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
   1.269 +*)
   1.270 +qed "deg_mult";
   1.271 +
   1.272 +Addsimps [deg_smult, deg_mult];
   1.273 +
   1.274 +(* Representation theorems about polynomials *)
   1.275 +
   1.276 +goal PolyRing.thy
   1.277 +  "!! p::nat=>'a::ring up. coeff k (SUM n p) = SUM n (%i. coeff k (p i))";
   1.278 +by (nat_ind_tac "n" 1);
   1.279 +(* Base case *)
   1.280 +by (Simp_tac 1);
   1.281 +(* Induction step *)
   1.282 +by (Asm_simp_tac 1);
   1.283 +qed "coeff_SUM";
   1.284 +
   1.285 +goal UnivPoly.thy
   1.286 +  "!! f::(nat=>'a::ring). \
   1.287 +\    bound n f ==> SUM n (%i. if i = x then f i else <0>) = f x";
   1.288 +by (simp_tac (simpset() addsimps [SUM_if_singleton]) 1);
   1.289 +by (auto_tac
   1.290 +  (claset() addDs [not_leE],
   1.291 +   simpset() setloop (split_tac [expand_if])));
   1.292 +qed "bound_SUM_if";
   1.293 +
   1.294 +Goal
   1.295 +  "!! p::'a::ring up. deg p <= n ==> SUM n (%i. coeff i p *s monom i) = p";
   1.296 +by (rtac up_eqI 1);
   1.297 +by (simp_tac (simpset() addsimps [coeff_SUM]) 1);
   1.298 +by (rtac trans 1);
   1.299 +by (res_inst_tac [("x", "na")] bound_SUM_if 2);
   1.300 +by (full_simp_tac (simpset() addsimps [deg_above_is_bound, coeff_def]) 2);
   1.301 +by (rtac SUM_cong 1);
   1.302 +by (rtac refl 1);
   1.303 +by (asm_simp_tac 
   1.304 +  (simpset() setloop (split_tac [expand_if])) 1);
   1.305 +qed "up_repr";
   1.306 +
   1.307 +Goal
   1.308 +  "!! p::'a::ring up. [| deg p <= n; P p |] ==> \
   1.309 +\  P (SUM n (%i. coeff i p *s monom i))";
   1.310 +by (asm_simp_tac (simpset() addsimps [up_repr]) 1);
   1.311 +qed "up_reprD";
   1.312 +
   1.313 +Goal
   1.314 +  "!! p::'a::ring up. [| deg p <= n; P (SUM n (%i. coeff i p *s monom i)) |] \
   1.315 +\    ==> P p";
   1.316 +by (asm_full_simp_tac (simpset() addsimps [up_repr]) 1);
   1.317 +qed "up_repr2D";
   1.318 +
   1.319 +(*
   1.320 +Goal
   1.321 +  "!! p::'a::ring up. [| deg p <= n; deg q <= m |] ==> \
   1.322 +\    (SUM n (%i. coeff i p *s monom i) = SUM m (%i. coeff i q *s monom i)) \
   1.323 +\    = (coeff k f = coeff k g)
   1.324 +...
   1.325 +qed "up_unique";
   1.326 +*)
   1.327 +
   1.328 +(* Polynomials over integral domains are again integral domains *)
   1.329 +
   1.330 +Goal "!!p::'a::domain up. p * q = <0> ==> p = <0> | q = <0>";
   1.331 +by (rtac classical 1);
   1.332 +by (subgoal_tac "deg p = 0 & deg q = 0" 1);
   1.333 +by (res_inst_tac [("p", "p"), ("n", "0")] up_repr2D 1);
   1.334 +by (Asm_simp_tac 1);
   1.335 +by (res_inst_tac [("p", "q"), ("n", "0")] up_repr2D 1);
   1.336 +by (Asm_simp_tac 1);
   1.337 +by (subgoal_tac "coeff 0 p = <0> | coeff 0 q = <0>" 1);
   1.338 +by (SELECT_GOAL (auto_tac (claset() addIs [up_eqI], simpset())) 1);
   1.339 +by (rtac integral 1);
   1.340 +by (subgoal_tac "coeff 0 (p * q) = <0>" 1);
   1.341 +by (Full_simp_tac 1);
   1.342 +by (Asm_simp_tac 1);
   1.343 +
   1.344 +by (dres_inst_tac [("f", "deg")] arg_cong 1);
   1.345 +by (Asm_full_simp_tac 1);
   1.346 +qed "up_integral";
   1.347 +
   1.348 +Goal "!! a::'a::domain. a *s p = <0> ==> a = <0> | p = <0>";
   1.349 +by (full_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1);
   1.350 +by (dtac up_integral 1);
   1.351 +by Auto_tac;
   1.352 +by (rtac (const_inj RS injD) 1);
   1.353 +by (Simp_tac 1);
   1.354 +qed "smult_integral";
   1.355 +
   1.356 +(* Divisibility and degree *)
   1.357 +
   1.358 +Goalw [dvd_def]
   1.359 +  "!! p::'a::domain up. [| p dvd q; q ~= <0> |] ==> deg p <= deg q";
   1.360 +by (etac exE 1);
   1.361 +by (hyp_subst_tac 1);
   1.362 +by (case_tac "p = <0>" 1);
   1.363 +by (Asm_simp_tac 1);
   1.364 +by (dtac r_nullD 1);
   1.365 +by (asm_simp_tac (simpset() addsimps [le_add1]) 1);
   1.366 +qed "dvd_imp_deg";