src/HOL/Algebra/poly/PolyRing.ML

final tuning;

(*
    Instantiate polynomials to form a ring and prove further properties
    $Id$
    Author: Clemens Ballarin, started 22 January 1997
*)

open PolyRing;

(* Properties of *s:
   Polynomials form a module *)

goal UnivPoly.thy "!!a::'a::ring. (a + b) *s p = a *s p + b *s p";
by (rtac up_eqI 1);
by (simp_tac (simpset() addsimps [l_distr]) 1);
qed "smult_l_distr";

goal UnivPoly.thy "!!a::'a::ring. a *s (p + q) = a *s p + a *s q";
by (rtac up_eqI 1);
by (simp_tac (simpset() addsimps [r_distr]) 1);
qed "smult_r_distr";

goal UnivPoly.thy "!!a::'a::ring. (a * b) *s p = a *s (b *s p)";
by (rtac up_eqI 1);
by (simp_tac (simpset() addsimps [m_assoc]) 1);
qed "smult_assoc1";

goal UnivPoly.thy "(<1>::'a::ring) *s p = p";
by (rtac up_eqI 1);
by (Simp_tac 1);
qed "smult_one";

(* Polynomials form an algebra *)

goal UnivPoly.thy "!!a::'a::ring. (a *s p) * q = a *s (p * q)";
by (rtac up_eqI 1);
by (simp_tac (simpset() addsimps [SUM_rdistr, m_assoc]) 1);
qed "smult_assoc2";

(* the following can be derived from the above ones,
   for generality reasons, it is therefore done *)

Goal "(<0>::'a::ring) *s p = <0>";
by (rtac a_lcancel 1);
by (rtac (smult_l_distr RS sym RS trans) 1);
by (Simp_tac 1);
qed "smult_l_null";

Goal "!!a::'a::ring. a *s <0> = <0>";
by (rtac a_lcancel 1);
by (rtac (smult_r_distr RS sym RS trans) 1);
by (Simp_tac 1);
qed "smult_r_null";

Goal "!!a::'a::ring. (-a) *s p = - (a *s p)";
by (rtac a_lcancel 1);
by (rtac (r_neg RS sym RSN (2, trans)) 1);
by (rtac (smult_l_distr RS sym RS trans) 1);
by (simp_tac (simpset() addsimps [smult_l_null, r_neg]) 1);
qed "smult_l_minus";

Goal "!!a::'a::ring. a *s (-p) = - (a *s p)";
by (rtac a_lcancel 1);
by (rtac (r_neg RS sym RSN (2, trans)) 1);
by (rtac (smult_r_distr RS sym RS trans) 1);
by (simp_tac (simpset() addsimps [smult_r_null, r_neg]) 1);
qed "smult_r_minus";

val smult_minus = [smult_l_minus, smult_r_minus];

(* Integrity of smult *)
(*
Goal
  "!! a::'a::domain. a *s b = <0> ==> a = <0> | b = <0>";
by (simp_tac (simpset() addsimps [disj_commute]) 1);

by (rtac (disj_commute RS trans) 1);
by (rtac contrapos2 1);
by (assume_tac 1);
by (rtac up_neqI 1);
by (Full_simp_tac 1);
by (etac conjE 1);
by (rtac not_integral 1);
by (assume_tac 1);
by (etac contrapos 1);
back();
by (rtac up_eqI 1);
by (Simp_tac 1);

by (rtac integral 1);

by (etac conjE 1);

by (rtac disjCI 1);
*)

Addsimps [smult_one, smult_l_null, smult_r_null];