src/HOL/Algebra/UnivPoly.thy
 changeset 14399 dc677b35e54f parent 13975 c8e9a89883ce child 14553 4740fc2da7bb
```     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Thu Feb 19 15:57:34 2004 +0100
1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Thu Feb 19 16:44:21 2004 +0100
1.3 @@ -370,10 +370,14 @@
1.4    by (auto intro!: cringI abelian_groupI comm_monoidI UP_a_assoc UP_l_zero
1.5      UP_l_neg_ex UP_a_comm UP_m_assoc UP_l_one UP_m_comm UP_l_distr)
1.6
1.7 +lemma (in UP_cring) UP_ring:  (* preliminary *)
1.8 +  "ring P"
1.9 +  by (auto intro: ring.intro cring.axioms UP_cring)
1.10 +
1.11  lemma (in UP_cring) UP_a_inv_closed [intro, simp]:
1.12    "p \<in> carrier P ==> \<ominus>\<^sub>2 p \<in> carrier P"
1.13    by (rule abelian_group.a_inv_closed
1.14 -    [OF cring.is_abelian_group [OF UP_cring]])
1.15 +    [OF ring.is_abelian_group [OF UP_ring]])
1.16
1.17  lemma (in UP_cring) coeff_a_inv [simp]:
1.18    assumes R: "p \<in> carrier P"
1.19 @@ -384,7 +388,7 @@
1.20      by algebra
1.21    also from R have "... =  \<ominus> (coeff P p n)"
1.23 -      abelian_group.r_neg [OF cring.is_abelian_group [OF UP_cring]])
1.24 +      abelian_group.r_neg [OF ring.is_abelian_group [OF UP_ring]])
1.25    finally show ?thesis .
1.26  qed
1.27
1.28 @@ -409,11 +413,11 @@
1.29
1.30  lemma (in UP_cring) UP_abelian_monoid:
1.31    "abelian_monoid P"
1.32 -  by (fast intro!: abelian_group.axioms cring.is_abelian_group UP_cring)
1.33 +  by (fast intro!: abelian_group.axioms ring.is_abelian_group UP_ring)
1.34
1.35  lemma (in UP_cring) UP_abelian_group:
1.36    "abelian_group P"
1.37 -  by (fast intro!: cring.is_abelian_group UP_cring)
1.38 +  by (fast intro!: ring.is_abelian_group UP_ring)
1.39
1.40  lemmas (in UP_cring) UP_r_one [simp] =
1.41    monoid.r_one [OF UP_monoid]
1.42 @@ -521,19 +525,19 @@
1.43    abelian_group.r_neg1 [OF UP_abelian_group]
1.44
1.45  lemmas (in UP_cring) UP_r_distr =
1.46 -  cring.r_distr [OF UP_cring]
1.47 +  ring.r_distr [OF UP_ring]
1.48
1.49  lemmas (in UP_cring) UP_l_null [simp] =
1.50 -  cring.l_null [OF UP_cring]
1.51 +  ring.l_null [OF UP_ring]
1.52
1.53  lemmas (in UP_cring) UP_r_null [simp] =
1.54 -  cring.r_null [OF UP_cring]
1.55 +  ring.r_null [OF UP_ring]
1.56
1.57  lemmas (in UP_cring) UP_l_minus =
1.58 -  cring.l_minus [OF UP_cring]
1.59 +  ring.l_minus [OF UP_ring]
1.60
1.61  lemmas (in UP_cring) UP_r_minus =
1.62 -  cring.r_minus [OF UP_cring]
1.63 +  ring.r_minus [OF UP_ring]
1.64
1.65  lemmas (in UP_cring) UP_finsum_ldistr =
1.66    cring.finsum_ldistr [OF UP_cring]
```