# File UnivPoly2.ML

    (*
        Degree of polynomials
        $Id: UnivPoly2.ML,v 1.1 2003/04/30 08:01:35 ballarin Exp $
        written by Clemens Ballarin, started 22 January 1997
    *)

    (*
    (* Relating degree and bound *)

    Goal "[| bound m f; f n ~= 0 |] ==> n <= m";
    by (force_tac (claset() addDs [inst "m" "n" boundD],
                   simpset()) 1);
    qed "below_bound";

    goal UnivPoly2.thy "bound (LEAST n. bound n (Rep_UP p)) (Rep_UP p)";
    by (rtac exE 1);
    by (rtac LeastI 2);
    by (assume_tac 2);
    by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
    by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
    qed "Least_is_bound";

    Goalw [coeff_def, deg_def]
      "!! p. ALL m. n < m --> coeff m p = 0 ==> deg p <= n";
    by (rtac Least_le 1);
    by (Fast_tac 1);
    qed "deg_aboveI";

    Goalw [coeff_def, deg_def]
      "(n ~= 0 --> coeff n p ~= 0) ==> n <= deg p";
    by (case_tac "n = 0" 1);
    (* Case n=0 *)
    by (Asm_simp_tac 1);
    (* Case n~=0 *)
    by (rotate_tac 1 1);
    by (Asm_full_simp_tac 1);
    by (rtac below_bound 1);
    by (assume_tac 2);
    by (rtac Least_is_bound 1);
    qed "deg_belowI";

    Goalw [coeff_def, deg_def]
      "deg p < m ==> coeff m p = 0";
    by (rtac exE 1); (* create !! x. *)
    by (rtac boundD 2);
    by (assume_tac 3);
    by (rtac LeastI 2);
    by (assume_tac 2);
    by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
    by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
    qed "deg_aboveD";

    Goalw [deg_def]
      "deg p = Suc y ==> ~ bound y (Rep_UP p)";
    by (rtac not_less_Least 1);
    by (Asm_simp_tac 1);
    val lemma1 = result();

    Goalw [deg_def, coeff_def]
      "deg p = Suc y ==> coeff (deg p) p ~= 0";
    by (rtac ccontr 1);
    by (dtac notnotD 1);
    by (cut_inst_tac [("p", "p")] Least_is_bound 1);
    by (subgoal_tac "bound y (Rep_UP p)" 1);
    (* prove subgoal *)
    by (rtac boundI 2);
    by (case_tac "Suc y < m" 2);
    (* first case *)
    by (rtac boundD 2);
    by (assume_tac 2);
    by (Asm_simp_tac 2);
    (* second case *)
    by (dtac leI 2);
    by (dtac Suc_leI 2);
    by (dtac le_anti_sym 2);
    by (assume_tac 2);
    by (Asm_full_simp_tac 2);
    (* end prove subgoal *)
    by (fold_goals_tac [deg_def]);
    by (dtac lemma1 1);
    by (etac notE 1);
    by (assume_tac 1);
    val lemma2 = result();

    Goal "deg p ~= 0 ==> coeff (deg p) p ~= 0";
    by (rtac lemma2 1);
    by (Full_simp_tac 1);
    by (dtac Suc_pred 1);
    by (rtac sym 1);
    by (Asm_simp_tac 1);
    qed "deg_lcoeff";

    Goal "p ~= 0 ==> coeff (deg p) p ~= 0";
    by (etac contrapos_np 1);
    by (case_tac "deg p = 0" 1);
    by (blast_tac (claset() addSDs [deg_lcoeff]) 2);
    by (rtac up_eqI 1);
    by (case_tac "n=0" 1);
    by (rotate_tac ~2 1);
    by (Asm_full_simp_tac 1);
    by (asm_full_simp_tac (simpset() addsimps [deg_aboveD]) 1);
    qed "nonzero_lcoeff";

    Goal "(deg p <= n) = bound n (Rep_UP p)";
    by (rtac iffI 1);
    (* ==> *)
    by (rtac boundI 1);
    by (fold_goals_tac [coeff_def]);
    by (rtac deg_aboveD 1);
    by (fast_arith_tac 1);
    (* <== *)
    by (rtac deg_aboveI 1);
    by (rewtac coeff_def);
    by (Fast_tac 1);
    qed "deg_above_is_bound";

    (* Lemmas on the degree function *)

    Goalw [max_def]
      "!! p::'a::ring up. deg (p + q) <= max (deg p) (deg q)";
    by (case_tac "deg p <= deg q" 1);
    (* case deg p <= deg q *)
    by (rtac deg_aboveI 1);
    by (Asm_simp_tac 1);
    by (strip_tac 1);
    by (dtac le_less_trans 1);
    by (assume_tac 1);
    by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
    (* case deg p > deg q *)
    by (rtac deg_aboveI 1);
    by (Asm_simp_tac 1);
    by (dtac not_leE 1);
    by (strip_tac 1);
    by (dtac less_trans 1);
    by (assume_tac 1);
    by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
    qed "deg_add";

    Goal "!!p::('a::ring up). deg p < deg q ==> deg (p + q) = deg q";
    by (rtac order_antisym 1);
    by (rtac le_trans 1);
    by (rtac deg_add 1);
    by (Asm_simp_tac 1);
    by (rtac deg_belowI 1);
    by (asm_simp_tac (simpset() addsimps [deg_aboveD, deg_lcoeff]) 1);
    qed "deg_add_equal";

    Goal "deg (monom m::'a::ring up) <= m";
    by (asm_simp_tac
      (simpset() addsimps [deg_aboveI, less_not_refl2 RS not_sym]) 1);
    qed "deg_monom_ring";

    Goal "deg (monom m::'a::domain up) = m";
    by (rtac le_anti_sym 1);
    (* <= *)
    by (rtac deg_monom_ring 1);
    (* >= *)
    by (asm_simp_tac
      (simpset() addsimps [deg_belowI, less_not_refl2 RS not_sym]) 1);
    qed "deg_monom";

    Goal "!! a::'a::ring. deg (const a) = 0";
    by (rtac le_anti_sym 1);
    by (rtac deg_aboveI 1);
    by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
    by (rtac deg_belowI 1);
    by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
    qed "deg_const";

    Goal "deg (0::'a::ringS up) = 0";
    by (rtac le_anti_sym 1);
    by (rtac deg_aboveI 1);
    by (Simp_tac 1);
    by (rtac deg_belowI 1);
    by (Simp_tac 1);
    qed "deg_zero";

    Goal "deg (<1>::'a::ring up) = 0";
    by (rtac le_anti_sym 1);
    by (rtac deg_aboveI 1);
    by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
    by (rtac deg_belowI 1);
    by (Simp_tac 1);
    qed "deg_one";

    Goal "!!p::('a::ring) up. deg (-p) = deg p";
    by (rtac le_anti_sym 1);
    (* <= *)
    by (simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1);
    by (simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff, uminus_monom_neq]) 1);
    qed "deg_uminus";

    Addsimps [deg_monom, deg_const, deg_zero, deg_one, deg_uminus];

    Goal
      "!! a::'a::ring. deg (a *s p) <= (if a = 0 then 0 else deg p)";
    by (case_tac "a = 0" 1);
    by (REPEAT (asm_simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1));
    qed "deg_smult_ring";

    Goal
      "!! a::'a::domain. deg (a *s p) = (if a = 0 then 0 else deg p)";
    by (rtac le_anti_sym 1);
    by (rtac deg_smult_ring 1);
    by (case_tac "a = 0" 1);
    by (REPEAT (asm_simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff]) 1));
    qed "deg_smult";

    Goal
      "!! p::'a::ring up. [| deg p + deg q < k |] ==> \
    \       coeff i p * coeff (k - i) q = 0";
    by (simp_tac (simpset() addsimps [coeff_def]) 1);
    by (rtac bound_mult_zero 1);
    by (assume_tac 3);
    by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
    by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
    qed "deg_above_mult_zero";

    Goal
      "!! p::'a::ring up. deg (p * q) <= deg p + deg q";
    by (rtac deg_aboveI 1);
    by (asm_simp_tac (simpset() addsimps [deg_above_mult_zero]) 1);
    qed "deg_mult_ring";

    goal Main.thy
      "!!k::nat. k < n ==> m < n + m - k";
    by (arith_tac 1);
    qed "less_add_diff";

    Goal "!!p. coeff n p ~= 0 ==> n <= deg p";
    (* More general than deg_belowI, and simplifies the next proof! *)
    by (rtac deg_belowI 1);
    by (Fast_tac 1);
    qed "deg_below2I";

    Goal
      "!! p::'a::domain up. \
    \    [| p ~= 0; q ~= 0 |] ==> deg (p * q) = deg p + deg q";
    by (rtac le_anti_sym 1);
    by (rtac deg_mult_ring 1);
    (* deg p + deg q <= deg (p * q) *)
    by (rtac deg_below2I 1);
    by (Simp_tac 1);
    (*
    by (rtac conjI 1);
    by (rtac impI 1);
    *)
    by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
    by (rtac le_add1 1);
    by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
    by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
    by (rtac le_refl 1);
    by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
    by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
    (*
    by (rtac impI 1);
    by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
    by (rtac le_add1 1);
    by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
    by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
    by (rtac le_refl 1);
    by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
    by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
    *)
    qed "deg_mult";

    Addsimps [deg_smult, deg_mult];

    (* Representation theorems about polynomials *)

    goal PolyRing.thy
      "!! p::nat=>'a::ring up. \
    \    coeff k (setsum p {..n}) = setsum (%i. coeff k (p i)) {..n}";
    by (induct_tac "n" 1);
    by Auto_tac;
    qed "coeff_SUM";

    goal UnivPoly2.thy
      "!! f::(nat=>'a::ring). \
    \    bound n f ==> setsum (%i. if i = x then f i else 0) {..n} = f x";
    by (simp_tac (simpset() addsimps [SUM_if_singleton]) 1);
    by (auto_tac
        (claset() addDs [not_leE],
         simpset()));
    qed "bound_SUM_if";

    Goal
      "!! p::'a::ring up. deg p <= n ==> \
    \  setsum (%i. coeff i p *s monom i) {..n} = p";
    by (rtac up_eqI 1);
    by (simp_tac (simpset() addsimps [coeff_SUM]) 1);
    by (rtac trans 1);
    by (res_inst_tac [("x", "na")] bound_SUM_if 2);
    by (full_simp_tac (simpset() addsimps [deg_above_is_bound, coeff_def]) 2);
    by (rtac SUM_cong 1);
    by (rtac refl 1);
    by (Asm_simp_tac 1);
    qed "up_repr";

    Goal
      "!! p::'a::ring up. [| deg p <= n; P p |] ==> \
    \  P (setsum (%i. coeff i p *s monom i) {..n})";
    by (asm_simp_tac (simpset() addsimps [up_repr]) 1);
    qed "up_reprD";

    Goal
      "!! p::'a::ring up. \
    \  [| deg p <= n; P (setsum (%i. coeff i p *s monom i) {..n}) |] \
    \    ==> P p";
    by (asm_full_simp_tac (simpset() addsimps [up_repr]) 1);
    qed "up_repr2D";

    (*
    Goal
      "!! p::'a::ring up. [| deg p <= n; deg q <= m |] ==> \
    \    (SUM n (%i. coeff i p *s monom i) = SUM m (%i. coeff i q *s monom i)) \
    \    = (coeff k f = coeff k g)
    ...
    qed "up_unique";
    *)

    (* Polynomials over integral domains are again integral domains *)

    Goal "!!p::'a::domain up. p * q = 0 ==> p = 0 | q = 0";
    by (rtac classical 1);
    by (subgoal_tac "deg p = 0 & deg q = 0" 1);
    by (res_inst_tac [("p", "p"), ("n", "0")] up_repr2D 1);
    by (Asm_simp_tac 1);
    by (res_inst_tac [("p", "q"), ("n", "0")] up_repr2D 1);
    by (Asm_simp_tac 1);
    by (subgoal_tac "coeff 0 p = 0 | coeff 0 q = 0" 1);
    by (force_tac (claset() addIs [up_eqI], simpset()) 1);
    by (rtac integral 1);
    by (subgoal_tac "coeff 0 (p * q) = 0" 1);
    by (Asm_simp_tac 2);
    by (Full_simp_tac 1);
    by (dres_inst_tac [("f", "deg")] arg_cong 1);
    by (Asm_full_simp_tac 1);
    qed "up_integral";

    Goal "!! a::'a::domain. a *s p = 0 ==> a = 0 | p = 0";
    by (full_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1);
    by (dtac up_integral 1);
    by Auto_tac;
    by (rtac (const_inj RS injD) 1);
    by (Simp_tac 1);
    qed "smult_integral";
    *)

    (* Divisibility and degree *)

    Goalw [dvd_def]
      "!! p::'a::domain up. [| p dvd q; q ~= 0 |] ==> deg p <= deg q";
    by (etac exE 1);
    by (hyp_subst_tac 1);
    by (case_tac "p = 0" 1);
    by (case_tac "k = 0" 2);
    by Auto_tac;
    qed "dvd_imp_deg";