1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Algebra/poly/PolyHomo.ML Fri Nov 05 11:14:26 1999 +0100
1.3 @@ -0,0 +1,127 @@
1.4 +(*
1.5 + Universal property and evaluation homomorphism of univariate polynomials
1.6 + $Id$
1.7 + Author: Clemens Ballarin, started 16 April 1997
1.8 +*)
1.9 +
1.10 +(* Ring homomorphisms and polynomials *)
1.11 +
1.12 +Goal "homo (const::'a::ring=>'a up)";
1.13 +by (auto_tac (claset() addSIs [homoI], simpset()));
1.14 +qed "const_homo";
1.15 +
1.16 +Delsimps [const_add, const_mult, const_one, const_zero];
1.17 +Addsimps [const_homo];
1.18 +
1.19 +Goal
1.20 + "!!f::'a::ring up=>'b::ring. homo f ==> f (a *s p) = f (const a) * f p";
1.21 +by (asm_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1);
1.22 +qed "homo_smult";
1.23 +
1.24 +Addsimps [homo_smult];
1.25 +
1.26 +(* Evaluation homomorphism *)
1.27 +
1.28 +Goal
1.29 + "!! phi::('a::ring=>'b::ring). homo phi ==> homo (EVAL2 phi a)";
1.30 +by (rtac homoI 1);
1.31 +by (rewtac EVAL2_def);
1.32 +(* + commutes *)
1.33 +(* degree estimations:
1.34 + bound of all sums can be extended to max (deg aa) (deg b) *)
1.35 +by (res_inst_tac [("m", "deg (aa + b)"), ("n", "max (deg aa) (deg b)")]
1.36 + SUM_shrink 1);
1.37 +by (rtac deg_add 1);
1.38 +by (asm_simp_tac (simpset() delsimps [coeff_add] addsimps [deg_aboveD]) 1);
1.39 +by (res_inst_tac [("m", "deg aa"), ("n", "max (deg aa) (deg b)")]
1.40 + SUM_shrink 1);
1.41 +by (rtac le_maxI1 1);
1.42 +by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
1.43 +by (res_inst_tac [("m", "deg b"), ("n", "max (deg aa) (deg b)")]
1.44 + SUM_shrink 1);
1.45 +by (rtac le_maxI2 1);
1.46 +by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
1.47 +(* actual homom property + *)
1.48 +by (asm_simp_tac (simpset() addsimps [l_distr, SUM_add]) 1);
1.49 +
1.50 +(* * commutes *)
1.51 +by (res_inst_tac [("m", "deg (aa * b)"), ("n", "deg aa + deg b")]
1.52 + SUM_shrink 1);
1.53 +by (rtac deg_mult_ring 1);
1.54 +by (asm_simp_tac (simpset() delsimps [coeff_mult] addsimps [deg_aboveD]) 1);
1.55 +by (rtac trans 1);
1.56 +by (rtac CauchySum 2);
1.57 +by (asm_simp_tac (simpset() addsimps [boundI, deg_aboveD]) 2);
1.58 +by (asm_simp_tac (simpset() addsimps [boundI, deg_aboveD]) 2);
1.59 +(* getting a^i and a^(k-i) together is difficult, so we do is manually *)
1.60 +by (res_inst_tac [("s",
1.61 +" SUM (deg aa + deg b) \
1.62 +\ (%k. SUM k \
1.63 +\ (%i. phi (coeff i aa) * (phi (coeff (k - i) b) * \
1.64 +\ (a ^ i * a ^ (k - i)))))")] trans 1);
1.65 +by (asm_simp_tac (simpset()
1.66 + addsimps [power_mult, leD RS add_diff_inverse, SUM_ldistr]) 1);
1.67 +by (simp_tac (simpset() addsimps m_ac) 1);
1.68 +by (simp_tac (simpset() addsimps m_ac) 1);
1.69 +(* <1> commutes *)
1.70 +by (Asm_simp_tac 1);
1.71 +qed "EVAL2_homo";
1.72 +
1.73 +Goalw [EVAL2_def]
1.74 + "!! phi::'a::ring=>'b::ring. EVAL2 phi a (const b) = phi b";
1.75 +by (Simp_tac 1);
1.76 +qed "EVAL2_const";
1.77 +
1.78 +(* This is probably redundant *)
1.79 +Goalw [EVAL2_def]
1.80 + "!! phi::'a::ring=>'b::ring. homo phi ==> EVAL2 phi a (monom 1) = a";
1.81 +by (Asm_simp_tac 1);
1.82 +qed "EVAL2_monom1";
1.83 +
1.84 +Goalw [EVAL2_def]
1.85 + "!! phi::'a::ring=>'b::ring. homo phi ==> EVAL2 phi a (monom n) = a ^ n";
1.86 +by (Simp_tac 1);
1.87 +by (nat_ind_tac "n" 1); (* really a case split *)
1.88 +by (Asm_simp_tac 1);
1.89 +by (Asm_simp_tac 1);
1.90 +qed "EVAL2_monom";
1.91 +
1.92 +Goal
1.93 + "!! phi::'a::ring=>'b::ring. \
1.94 +\ homo phi ==> EVAL2 phi a (b *s p) = phi b * EVAL2 phi a p";
1.95 +by (asm_simp_tac
1.96 + (simpset() addsimps [const_mult_is_smult RS sym, EVAL2_homo, EVAL2_const]) 1);
1.97 +qed "EVAL2_smult";
1.98 +
1.99 +Goalw [EVAL_def] "!! a::'a::ring. homo (EVAL a)";
1.100 +by (asm_simp_tac (simpset() addsimps [EVAL2_homo, id_homo]) 1);
1.101 +qed "EVAL_homo";
1.102 +
1.103 +Goalw [EVAL_def] "!! a::'a::ring. EVAL a (const b) = b";
1.104 +by (asm_simp_tac (simpset() addsimps [EVAL2_const]) 1);
1.105 +qed "EVAL_const";
1.106 +
1.107 +Goalw [EVAL_def] "!! a::'a::ring. EVAL a (monom n) = a ^ n";
1.108 +by (asm_simp_tac (simpset() addsimps [EVAL2_monom]) 1);
1.109 +qed "EVAL_monom";
1.110 +
1.111 +Goalw [EVAL_def] "!! a::'a::ring. EVAL a (b *s p) = b * EVAL a p";
1.112 +by (asm_simp_tac (simpset() addsimps [EVAL2_smult]) 1);
1.113 +qed "EVAL_smult";
1.114 +
1.115 +(* Examples *)
1.116 +
1.117 +Goal
1.118 + "EVAL (x::'a::ring) (a*X^2 + b*X^1 + c*X^0) = a * x ^ 2 + b * x ^ 1 + c";
1.119 +by (asm_simp_tac (simpset() delsimps [power_Suc]
1.120 + addsimps [EVAL_homo, EVAL_monom, EVAL_smult]) 1);
1.121 +result();
1.122 +
1.123 +Goal
1.124 + "EVAL (y::'a::ring) \
1.125 +\ (EVAL (const x) (monom 1 + const (a*X^2 + b*X^1 + c*X^0))) = \
1.126 +\ x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)";
1.127 +by (asm_simp_tac (simpset() delsimps [power_Suc]
1.128 + addsimps [EVAL_homo, EVAL_monom, EVAL_smult, EVAL_const]) 1);
1.129 +result();
1.130 +