1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Algebra/poly/PolyRing.ML	Fri Nov 05 11:14:26 1999 +0100
     1.3 @@ -0,0 +1,96 @@
     1.4 +(*
     1.5 +    Instantiate polynomials to form a ring and prove further properties
     1.6 +    $Id$
     1.7 +    Author: Clemens Ballarin, started 22 January 1997
     1.8 +*)
     1.9 +
    1.10 +open PolyRing;
    1.11 +
    1.12 +(* Properties of *s:
    1.13 +   Polynomials form a module *)
    1.14 +
    1.15 +goal UnivPoly.thy "!!a::'a::ring. (a + b) *s p = a *s p + b *s p";
    1.16 +by (rtac up_eqI 1);
    1.17 +by (simp_tac (simpset() addsimps [l_distr]) 1);
    1.18 +qed "smult_l_distr";
    1.19 +
    1.20 +goal UnivPoly.thy "!!a::'a::ring. a *s (p + q) = a *s p + a *s q";
    1.21 +by (rtac up_eqI 1);
    1.22 +by (simp_tac (simpset() addsimps [r_distr]) 1);
    1.23 +qed "smult_r_distr";
    1.24 +
    1.25 +goal UnivPoly.thy "!!a::'a::ring. (a * b) *s p = a *s (b *s p)";
    1.26 +by (rtac up_eqI 1);
    1.27 +by (simp_tac (simpset() addsimps [m_assoc]) 1);
    1.28 +qed "smult_assoc1";
    1.29 +
    1.30 +goal UnivPoly.thy "(<1>::'a::ring) *s p = p";
    1.31 +by (rtac up_eqI 1);
    1.32 +by (Simp_tac 1);
    1.33 +qed "smult_one";
    1.34 +
    1.35 +(* Polynomials form an algebra *)
    1.36 +
    1.37 +goal UnivPoly.thy "!!a::'a::ring. (a *s p) * q = a *s (p * q)";
    1.38 +by (rtac up_eqI 1);
    1.39 +by (simp_tac (simpset() addsimps [SUM_rdistr, m_assoc]) 1);
    1.40 +qed "smult_assoc2";
    1.41 +
    1.42 +(* the following can be derived from the above ones,
    1.43 +   for generality reasons, it is therefore done *)
    1.44 +
    1.45 +Goal "(<0>::'a::ring) *s p = <0>";
    1.46 +by (rtac a_lcancel 1);
    1.47 +by (rtac (smult_l_distr RS sym RS trans) 1);
    1.48 +by (Simp_tac 1);
    1.49 +qed "smult_l_null";
    1.50 +
    1.51 +Goal "!!a::'a::ring. a *s <0> = <0>";
    1.52 +by (rtac a_lcancel 1);
    1.53 +by (rtac (smult_r_distr RS sym RS trans) 1);
    1.54 +by (Simp_tac 1);
    1.55 +qed "smult_r_null";
    1.56 +
    1.57 +Goal "!!a::'a::ring. (-a) *s p = - (a *s p)";
    1.58 +by (rtac a_lcancel 1);
    1.59 +by (rtac (r_neg RS sym RSN (2, trans)) 1);
    1.60 +by (rtac (smult_l_distr RS sym RS trans) 1);
    1.61 +by (simp_tac (simpset() addsimps [smult_l_null, r_neg]) 1);
    1.62 +qed "smult_l_minus";
    1.63 +
    1.64 +Goal "!!a::'a::ring. a *s (-p) = - (a *s p)";
    1.65 +by (rtac a_lcancel 1);
    1.66 +by (rtac (r_neg RS sym RSN (2, trans)) 1);
    1.67 +by (rtac (smult_r_distr RS sym RS trans) 1);
    1.68 +by (simp_tac (simpset() addsimps [smult_r_null, r_neg]) 1);
    1.69 +qed "smult_r_minus";
    1.70 +
    1.71 +val smult_minus = [smult_l_minus, smult_r_minus];
    1.72 +
    1.73 +(* Integrity of smult *)
    1.74 +(*
    1.75 +Goal
    1.76 +  "!! a::'a::domain. a *s b = <0> ==> a = <0> | b = <0>";
    1.77 +by (simp_tac (simpset() addsimps [disj_commute]) 1);
    1.78 +
    1.79 +by (rtac (disj_commute RS trans) 1);
    1.80 +by (rtac contrapos2 1);
    1.81 +by (assume_tac 1);
    1.82 +by (rtac up_neqI 1);
    1.83 +by (Full_simp_tac 1);
    1.84 +by (etac conjE 1);
    1.85 +by (rtac not_integral 1);
    1.86 +by (assume_tac 1);
    1.87 +by (etac contrapos 1);
    1.88 +back();
    1.89 +by (rtac up_eqI 1);
    1.90 +by (Simp_tac 1);
    1.91 +
    1.92 +by (rtac integral 1);
    1.93 +
    1.94 +by (etac conjE 1);
    1.95 +
    1.96 +by (rtac disjCI 1);
    1.97 +*)
    1.98 +
    1.99 +Addsimps [smult_one, smult_l_null, smult_r_null];