# File PolyHomo.ML

    (*
        Universal property and evaluation homomorphism of univariate polynomials
        $Id: PolyHomo.ML,v 1.7 2005/09/17 18:49:15 wenzelm Exp $
        Author: Clemens Ballarin, started 16 April 1997
    *)

    (* Summation result for tactic-style proofs *)

    val natsum_add = thm "natsum_add";
    val natsum_ldistr = thm "natsum_ldistr";
    val natsum_rdistr = thm "natsum_rdistr";

    Goal
      "!! f::(nat=>'a::ring). \
    \    m <= n & (ALL i. m < i & i <= n --> f i = 0) --> \
    \    setsum f {..m} = setsum f {..n}";
    by (induct_tac "n" 1);
    (* Base case *)
    by (Simp_tac 1);
    (* Induction step *)
    by (case_tac "m <= n" 1);
    by Auto_tac;
    by (subgoal_tac "m = Suc n" 1);
    by (Asm_simp_tac 1);
    by (fast_arith_tac 1);
    val SUM_shrink_lemma = result();

    Goal
      "!! f::(nat=>'a::ring). \
    \    [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..n}) |] \
    \  ==> P (setsum f {..m})";
    by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1);
    by (Asm_full_simp_tac 1);
    qed "SUM_shrink";

    Goal
      "!! f::(nat=>'a::ring). \
    \    [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..m}) |] \
    \    ==> P (setsum f {..n})";
    by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1);
    by (Asm_full_simp_tac 1);
    qed "SUM_extend";

    Goal
      "!!f::nat=>'a::ring. j <= n + m --> \
    \    setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..j} = \
    \    setsum (%k. setsum (%i. f k * g i) {..j - k}) {..j}";
    by (induct_tac "j" 1);
    (* Base case *)
    by (Simp_tac 1);
    (* Induction step *)
    by (simp_tac (simpset() addsimps [Suc_diff_le, natsum_add]) 1);
    (*
    by (asm_simp_tac (simpset() addsimps a_ac) 1);
    *)
    by (Asm_simp_tac 1);
    val DiagSum_lemma = result();

    Goal
      "!!f::nat=>'a::ring. \
    \    setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..n + m} = \
    \    setsum (%k. setsum (%i. f k * g i) {..n + m - k}) {..n + m}";
    by (rtac (DiagSum_lemma RS mp) 1);
    by (rtac le_refl 1);
    qed "DiagSum";

    Goal
      "!! f::nat=>'a::ring. [| bound n f; bound m g|] ==> \
    \    setsum (%k. setsum (%i. f i * g (k-i)) {..k}) {..n + m} = \
    \    setsum f {..n} * setsum g {..m}";
    by (simp_tac (simpset() addsimps [natsum_ldistr, DiagSum]) 1);
    (* SUM_rdistr must be applied after SUM_ldistr ! *)
    by (simp_tac (simpset() addsimps [natsum_rdistr]) 1);
    by (res_inst_tac [("m", "n"), ("n", "n+m")] SUM_extend 1);
    by (rtac le_add1 1);
    by (Force_tac 1);
    by (rtac (thm "natsum_cong") 1);
    by (rtac refl 1);
    by (res_inst_tac [("m", "m"), ("n", "n+m-i")] SUM_shrink 1);
    by (asm_simp_tac (simpset() addsimps [le_add_diff]) 1);
    by Auto_tac;
    qed "CauchySum";

    (* Ring homomorphisms and polynomials *)
    (*
    Goal "homo (const::'a::ring=>'a up)";
    by (auto_tac (claset() addSIs [homoI], simpset()));
    qed "const_homo";

    Delsimps [const_add, const_mult, const_one, const_zero];
    Addsimps [const_homo];

    Goal
      "!!f::'a::ring up=>'b::ring. homo f ==> f (a *s p) = f (const a) * f p";
    by (asm_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1);
    qed "homo_smult";

    Addsimps [homo_smult];
    *)

    val deg_add = thm "deg_add";
    val deg_mult_ring = thm "deg_mult_ring";
    val deg_aboveD = thm "deg_aboveD";
    val coeff_add = thm "coeff_add";
    val coeff_mult = thm "coeff_mult";
    val boundI = thm "boundI";
    val monom_mult_is_smult = thm "monom_mult_is_smult";

    (* Evaluation homomorphism *)

    Goal
      "!! phi::('a::ring=>'b::ring). homo phi ==> homo (EVAL2 phi a)";
    by (rtac homoI 1);
    by (rewtac (thm "EVAL2_def"));
    (* + commutes *)
    (* degree estimations:
      bound of all sums can be extended to max (deg aa) (deg b) *)
    by (res_inst_tac [("m", "deg (aa + b)"), ("n", "max (deg aa) (deg b)")]
      SUM_shrink 1);
    by (rtac deg_add 1);
    by (asm_simp_tac (simpset() delsimps [coeff_add] addsimps [deg_aboveD]) 1);
    by (res_inst_tac [("m", "deg aa"), ("n", "max (deg aa) (deg b)")]
      SUM_shrink 1);
    by (rtac le_maxI1 1);
    by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
    by (res_inst_tac [("m", "deg b"), ("n", "max (deg aa) (deg b)")]
      SUM_shrink 1);
    by (rtac le_maxI2 1);
    by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
    (* actual homom property + *)
    by (asm_simp_tac (simpset() addsimps [l_distr, natsum_add]) 1);

    (* * commutes *)
    by (res_inst_tac [("m", "deg (aa * b)"), ("n", "deg aa + deg b")]
      SUM_shrink 1);
    by (rtac deg_mult_ring 1);
    by (asm_simp_tac (simpset() delsimps [coeff_mult] addsimps [deg_aboveD]) 1);
    by (rtac trans 1);
    by (rtac CauchySum 2);
    by (asm_simp_tac (simpset() addsimps [boundI, deg_aboveD]) 2);
    by (asm_simp_tac (simpset() addsimps [boundI, deg_aboveD]) 2);
    (* getting a^i and a^(k-i) together is difficult, so we do it manually *)
    by (res_inst_tac [("s",
    "        setsum  \
    \           (%k. setsum \
    \                 (%i. phi (coeff aa i) * (phi (coeff b (k - i)) * \
    \                      (a ^ i * a ^ (k - i)))) {..k}) \
    \           {..deg aa + deg b}")] trans 1);
    by (asm_simp_tac (simpset()
        addsimps [power_mult, leD RS add_diff_inverse, natsum_ldistr]) 1);
    by (Simp_tac 1);
    (* 1 commutes *)
    by (Asm_simp_tac 1);
    qed "EVAL2_homo";

    Goalw [thm "EVAL2_def"]
      "!! phi::'a::ring=>'b::ring. EVAL2 phi a (monom b 0) = phi b";
    by (Simp_tac 1);
    qed "EVAL2_const";

    Goalw [thm "EVAL2_def"]
      "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 1) = a";
    (* Must be able to distinguish 0 from 1, hence 'a::domain *)
    by (Asm_simp_tac 1);
    qed "EVAL2_monom1";

    Goalw [thm "EVAL2_def"]
      "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 n) = a ^ n";
    by (Simp_tac 1);
    by (case_tac "n" 1);
    by Auto_tac;
    qed "EVAL2_monom";

    Goal
      "!! phi::'a::ring=>'b::ring. \
    \    homo phi ==> EVAL2 phi a (b *s p) = phi b * EVAL2 phi a p";
    by (asm_simp_tac (simpset()
        addsimps [monom_mult_is_smult RS sym, EVAL2_homo, EVAL2_const]) 1);
    qed "EVAL2_smult";

    val up_eqI = thm "up_eqI";

    Goal "monom (a::'a::ring) n = monom a 0 * monom 1 n";
    by (simp_tac (simpset() addsimps [monom_mult_is_smult]) 1);
    by (rtac up_eqI 1);
    by (Simp_tac 1);
    qed "monom_decomp";

    Goal
      "!! phi::'a::domain=>'b::ring. \
    \    homo phi ==> EVAL2 phi a (monom b n) = phi b * a ^ n";
    by (stac monom_decomp 1);
    by (asm_simp_tac (simpset()
        addsimps [EVAL2_homo, EVAL2_const, EVAL2_monom]) 1);
    qed "EVAL2_monom_n";

    Goalw [thm "EVAL_def"] "!! a::'a::ring. homo (EVAL a)";
    by (asm_simp_tac (simpset() addsimps [EVAL2_homo]) 1);
    qed "EVAL_homo";

    Goalw [thm "EVAL_def"] "!! a::'a::ring. EVAL a (monom b 0) = b";
    by (asm_simp_tac (simpset() addsimps [EVAL2_const]) 1);
    qed "EVAL_const";

    Goalw [thm "EVAL_def"] "!! a::'a::domain. EVAL a (monom 1 n) = a ^ n";
    by (asm_simp_tac (simpset() addsimps [EVAL2_monom]) 1);
    qed "EVAL_monom";

    Goalw [thm "EVAL_def"] "!! a::'a::ring. EVAL a (b *s p) = b * EVAL a p";
    by (asm_simp_tac (simpset() addsimps [EVAL2_smult]) 1);
    qed "EVAL_smult";

    Goalw [thm "EVAL_def"] "!! a::'a::domain. EVAL a (monom b n) = b * a ^ n";
    by (asm_simp_tac (simpset() addsimps [EVAL2_monom_n]) 1);
    qed "EVAL_monom_n";

    (* Examples *)

    Goal
      "EVAL (x::'a::domain) (a*X^2 + b*X^1 + c*X^0) = a * x ^ 2 + b * x ^ 1 + c";
    by (asm_simp_tac (simpset() delsimps [power_Suc]
        addsimps [EVAL_homo, EVAL_monom, EVAL_monom_n]) 1);
    result();

    Goal
      "EVAL (y::'a::domain) \
    \    (EVAL (monom x 0) (monom 1 1 + monom (a*X^2 + b*X^1 + c*X^0) 0)) = \
    \  x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)";
    by (asm_simp_tac (simpset() delsimps [power_Suc]
        addsimps [EVAL_homo, EVAL_monom, EVAL_monom_n, EVAL_const]) 1);
    result();