# HG changeset patch
# User ballarin
# Date 1051689695 -7200
# Node ID d3671b87882871607794b7b97101efa7e2c3c4ec
# Parent  4822d9597d1e4a5d40eb7f49fa7428480c83de5b
Greatly extended CRing.  Added Module.

diff -r 4822d9597d1e -r d3671b878828 src/HOL/Algebra/CRing.thy
--- a/src/HOL/Algebra/CRing.thy	Tue Apr 29 12:36:49 2003 +0200
+++ b/src/HOL/Algebra/CRing.thy	Wed Apr 30 10:01:35 2003 +0200
@@ -5,41 +5,294 @@
   Copyright: Clemens Ballarin
 *)
 
-theory CRing = Summation
+theory CRing = FiniteProduct
 files ("ringsimp.ML"):
 
+section {* Abelian Groups *}
+
+record 'a ring = "'a monoid" +
+  zero :: 'a ("\<zero>\<index>")
+  add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)
+
+text {* Derived operations. *}
+
+constdefs
+  a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
+  "a_inv R == m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
+
+  minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
+  "[| x \<in> carrier R; y \<in> carrier R |] ==> minus R x y == add R x (a_inv R y)"
+
+locale abelian_monoid = struct G +
+  assumes a_comm_monoid: "comm_monoid (| carrier = carrier G,
+      mult = add G, one = zero G |)"
+
+text {*
+  The following definition is redundant but simple to use.
+*}
+
+locale abelian_group = abelian_monoid +
+  assumes a_comm_group: "comm_group (| carrier = carrier G,
+      mult = add G, one = zero G |)"
+
+subsection {* Basic Properties *}
+
+lemma abelian_monoidI:
+  assumes a_closed:
+      "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> add R x y \<in> carrier R"
+    and zero_closed: "zero R \<in> carrier R"
+    and a_assoc:
+      "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |] ==>
+      add R (add R x y) z = add R x (add R y z)"
+    and l_zero: "!!x. x \<in> carrier R ==> add R (zero R) x = x"
+    and a_comm:
+      "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> add R x y = add R y x"
+  shows "abelian_monoid R"
+  by (auto intro!: abelian_monoid.intro comm_monoidI intro: prems)
+
+lemma abelian_groupI:
+  assumes a_closed:
+      "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> add R x y \<in> carrier R"
+    and zero_closed: "zero R \<in> carrier R"
+    and a_assoc:
+      "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |] ==>
+      add R (add R x y) z = add R x (add R y z)"
+    and a_comm:
+      "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> add R x y = add R y x"
+    and l_zero: "!!x. x \<in> carrier R ==> add R (zero R) x = x"
+    and l_inv_ex: "!!x. x \<in> carrier R ==> EX y : carrier R. add R y x = zero R"
+  shows "abelian_group R"
+  by (auto intro!: abelian_group.intro abelian_monoidI
+      abelian_group_axioms.intro comm_monoidI comm_groupI
+    intro: prems)
+
+(* TODO: The following thms are probably unnecessary. *)
+
+lemma (in abelian_monoid) a_magma:
+  "magma (| carrier = carrier G, mult = add G, one = zero G |)"
+  by (rule comm_monoid.axioms) (rule a_comm_monoid)
+
+lemma (in abelian_monoid) a_semigroup:
+  "semigroup (| carrier = carrier G, mult = add G, one = zero G |)"
+  by (unfold semigroup_def) (fast intro: comm_monoid.axioms a_comm_monoid)
+
+lemma (in abelian_monoid) a_monoid:
+  "monoid (| carrier = carrier G, mult = add G, one = zero G |)"
+  by (unfold monoid_def) (fast intro: a_comm_monoid comm_monoid.axioms)
+
+lemma (in abelian_group) a_group:
+  "group (| carrier = carrier G, mult = add G, one = zero G |)"
+  by (unfold group_def semigroup_def)
+    (fast intro: comm_group.axioms a_comm_group)
+
+lemma (in abelian_monoid) a_comm_semigroup:
+  "comm_semigroup (| carrier = carrier G, mult = add G, one = zero G |)"
+  by (unfold comm_semigroup_def semigroup_def)
+    (fast intro: comm_monoid.axioms a_comm_monoid)
+
+lemmas monoid_record_simps = semigroup.simps monoid.simps
+
+lemma (in abelian_monoid) a_closed [intro, simp]:
+  "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> y \<in> carrier G"
+  by (rule magma.m_closed [OF a_magma, simplified monoid_record_simps]) 
+
+lemma (in abelian_monoid) zero_closed [intro, simp]:
+  "\<zero> \<in> carrier G"
+  by (rule monoid.one_closed [OF a_monoid, simplified monoid_record_simps])
+
+lemma (in abelian_group) a_inv_closed [intro, simp]:
+  "x \<in> carrier G ==> \<ominus> x \<in> carrier G"
+  by (simp add: a_inv_def
+    group.inv_closed [OF a_group, simplified monoid_record_simps])
+
+lemma (in abelian_group) minus_closed [intro, simp]:
+  "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<ominus> y \<in> carrier G"
+  by (simp add: minus_def)
+
+lemma (in abelian_group) a_l_cancel [simp]:
+  "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
+   (x \<oplus> y = x \<oplus> z) = (y = z)"
+  by (rule group.l_cancel [OF a_group, simplified monoid_record_simps])
+
+lemma (in abelian_group) a_r_cancel [simp]:
+  "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
+   (y \<oplus> x = z \<oplus> x) = (y = z)"
+  by (rule group.r_cancel [OF a_group, simplified monoid_record_simps])
+
+lemma (in abelian_monoid) a_assoc:
+  "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
+  (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
+  by (rule semigroup.m_assoc [OF a_semigroup, simplified monoid_record_simps])
+
+lemma (in abelian_monoid) l_zero [simp]:
+  "x \<in> carrier G ==> \<zero> \<oplus> x = x"
+  by (rule monoid.l_one [OF a_monoid, simplified monoid_record_simps])
+
+lemma (in abelian_group) l_neg:
+  "x \<in> carrier G ==> \<ominus> x \<oplus> x = \<zero>"
+  by (simp add: a_inv_def
+    group.l_inv [OF a_group, simplified monoid_record_simps])
+
+lemma (in abelian_monoid) a_comm:
+  "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> y = y \<oplus> x"
+  by (rule comm_semigroup.m_comm [OF a_comm_semigroup,
+    simplified monoid_record_simps])
+
+lemma (in abelian_monoid) a_lcomm:
+  "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
+   x \<oplus> (y \<oplus> z) = y \<oplus> (x \<oplus> z)"
+  by (rule comm_semigroup.m_lcomm [OF a_comm_semigroup,
+    simplified monoid_record_simps])
+
+lemma (in abelian_monoid) r_zero [simp]:
+  "x \<in> carrier G ==> x \<oplus> \<zero> = x"
+  using monoid.r_one [OF a_monoid]
+  by simp
+
+lemma (in abelian_group) r_neg:
+  "x \<in> carrier G ==> x \<oplus> (\<ominus> x) = \<zero>"
+  using group.r_inv [OF a_group]
+  by (simp add: a_inv_def)
+
+lemma (in abelian_group) minus_zero [simp]:
+  "\<ominus> \<zero> = \<zero>"
+  by (simp add: a_inv_def
+    group.inv_one [OF a_group, simplified monoid_record_simps])
+
+lemma (in abelian_group) minus_minus [simp]:
+  "x \<in> carrier G ==> \<ominus> (\<ominus> x) = x"
+  using group.inv_inv [OF a_group, simplified monoid_record_simps]
+  by (simp add: a_inv_def)
+
+lemma (in abelian_group) a_inv_inj:
+  "inj_on (a_inv G) (carrier G)"
+  using group.inv_inj [OF a_group, simplified monoid_record_simps]
+  by (simp add: a_inv_def)
+
+lemma (in abelian_group) minus_add:
+  "[| x \<in> carrier G; y \<in> carrier G |] ==> \<ominus> (x \<oplus> y) = \<ominus> x \<oplus> \<ominus> y"
+  using comm_group.inv_mult [OF a_comm_group]
+  by (simp add: a_inv_def)
+
+lemmas (in abelian_monoid) a_ac = a_assoc a_comm a_lcomm
+
+subsection {* Sums over Finite Sets *}
+
+text {*
+  This definition makes it easy to lift lemmas from @{term finprod}.
+*}
+
+constdefs
+  finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b"
+  "finsum G f A == finprod (| carrier = carrier G,
+     mult = add G, one = zero G |) f A"
+
+(*
+  lemmas (in abelian_monoid) finsum_empty [simp] =
+    comm_monoid.finprod_empty [OF a_comm_monoid, simplified]
+  is dangeous, because attributes (like simplified) are applied upon opening
+  the locale, simplified refers to the simpset at that time!!!
+
+  lemmas (in abelian_monoid) finsum_empty [simp] =
+    abelian_monoid.finprod_empty [OF a_abelian_monoid, folded finsum_def,
+      simplified monoid_record_simps]
+makes the locale slow, because proofs are repeated for every
+"lemma (in abelian_monoid)" command.
+When lemma is used time in UnivPoly.thy from beginning to UP_cring goes down
+from 110 secs to 60 secs.
+*)
+
+lemma (in abelian_monoid) finsum_empty [simp]:
+  "finsum G f {} = \<zero>"
+  by (rule comm_monoid.finprod_empty [OF a_comm_monoid,
+    folded finsum_def, simplified monoid_record_simps])
+
+lemma (in abelian_monoid) finsum_insert [simp]:
+  "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |]
+  ==> finsum G f (insert a F) = f a \<oplus> finsum G f F"
+  by (rule comm_monoid.finprod_insert [OF a_comm_monoid,
+    folded finsum_def, simplified monoid_record_simps])
+
+lemma (in abelian_monoid) finsum_zero [simp]:
+  "finite A ==> finsum G (%i. \<zero>) A = \<zero>"
+  by (rule comm_monoid.finprod_one [OF a_comm_monoid, folded finsum_def,
+    simplified monoid_record_simps])
+
+lemma (in abelian_monoid) finsum_closed [simp]:
+  fixes A
+  assumes fin: "finite A" and f: "f \<in> A -> carrier G" 
+  shows "finsum G f A \<in> carrier G"
+  by (rule comm_monoid.finprod_closed [OF a_comm_monoid,
+    folded finsum_def, simplified monoid_record_simps])
+
+lemma (in abelian_monoid) finsum_Un_Int:
+  "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
+     finsum G g (A Un B) \<oplus> finsum G g (A Int B) =
+     finsum G g A \<oplus> finsum G g B"
+  by (rule comm_monoid.finprod_Un_Int [OF a_comm_monoid,
+    folded finsum_def, simplified monoid_record_simps])
+
+lemma (in abelian_monoid) finsum_Un_disjoint:
+  "[| finite A; finite B; A Int B = {};
+      g \<in> A -> carrier G; g \<in> B -> carrier G |]
+   ==> finsum G g (A Un B) = finsum G g A \<oplus> finsum G g B"
+  by (rule comm_monoid.finprod_Un_disjoint [OF a_comm_monoid,
+    folded finsum_def, simplified monoid_record_simps])
+
+lemma (in abelian_monoid) finsum_addf:
+  "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
+   finsum G (%x. f x \<oplus> g x) A = (finsum G f A \<oplus> finsum G g A)"
+  by (rule comm_monoid.finprod_multf [OF a_comm_monoid,
+    folded finsum_def, simplified monoid_record_simps])
+
+lemma (in abelian_monoid) finsum_cong':
+  "[| A = B; g : B -> carrier G;
+      !!i. i : B ==> f i = g i |] ==> finsum G f A = finsum G g B"
+  by (rule comm_monoid.finprod_cong' [OF a_comm_monoid,
+    folded finsum_def, simplified monoid_record_simps]) auto
+
+lemma (in abelian_monoid) finsum_0 [simp]:
+  "f : {0::nat} -> carrier G ==> finsum G f {..0} = f 0"
+  by (rule comm_monoid.finprod_0 [OF a_comm_monoid, folded finsum_def,
+    simplified monoid_record_simps])
+
+lemma (in abelian_monoid) finsum_Suc [simp]:
+  "f : {..Suc n} -> carrier G ==>
+   finsum G f {..Suc n} = (f (Suc n) \<oplus> finsum G f {..n})"
+  by (rule comm_monoid.finprod_Suc [OF a_comm_monoid, folded finsum_def,
+    simplified monoid_record_simps])
+
+lemma (in abelian_monoid) finsum_Suc2:
+  "f : {..Suc n} -> carrier G ==>
+   finsum G f {..Suc n} = (finsum G (%i. f (Suc i)) {..n} \<oplus> f 0)"
+  by (rule comm_monoid.finprod_Suc2 [OF a_comm_monoid, folded finsum_def,
+    simplified monoid_record_simps])
+
+lemma (in abelian_monoid) finsum_add [simp]:
+  "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==>
+     finsum G (%i. f i \<oplus> g i) {..n::nat} =
+     finsum G f {..n} \<oplus> finsum G g {..n}"
+  by (rule comm_monoid.finprod_mult [OF a_comm_monoid, folded finsum_def,
+    simplified monoid_record_simps])
+
+lemma (in abelian_monoid) finsum_cong:
+  "[| A = B; !!i. i : B ==> f i = g i;
+      g : B -> carrier G = True |] ==> finsum G f A = finsum G g B"
+  by (rule comm_monoid.finprod_cong [OF a_comm_monoid, folded finsum_def,
+    simplified monoid_record_simps]) auto
+
+text {*Usually, if this rule causes a failed congruence proof error,
+   the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
+   Adding @{thm [source] Pi_def} to the simpset is often useful. *}
+
 section {* The Algebraic Hierarchy of Rings *}
 
 subsection {* Basic Definitions *}
 
-record 'a ring = "'a group" +
-  zero :: 'a ("\<zero>\<index>")
-  add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)
-  a_inv :: "'a => 'a" ("\<ominus>\<index> _" [81] 80)
-
-locale cring = abelian_monoid R +
-  assumes a_abelian_group: "abelian_group (| carrier = carrier R,
-      mult = add R, one = zero R, m_inv = a_inv R |)"
-    and m_inv_def: "[| EX y. y \<in> carrier R & x \<otimes> y = \<one>; x \<in> carrier R |]
-      ==> inv x = (THE y. y \<in> carrier R & x \<otimes> y = \<one>)"
-    and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
+locale cring = abelian_group R + comm_monoid R +
+  assumes l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
       ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
 
-text {* Derived operation. *}
-
-constdefs
-  minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
-  "[| x \<in> carrier R; y \<in> carrier R |] ==> minus R x y == add R x (a_inv R y)"
-
-(*
-  -- {* Definition of derived operations *}
-
-  minus_def:    "a - b = a + (-b)"
-  inverse_def:  "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
-  divide_def:   "a / b = a * inverse b"
-  power_def:    "a ^ n = nat_rec 1 (%u b. b * a) n"
-*)
-
 locale "domain" = cring +
   assumes one_not_zero [simp]: "\<one> ~= \<zero>"
     and integral: "[| a \<otimes> b = \<zero>; a \<in> carrier R; b \<in> carrier R |] ==>
@@ -47,117 +300,41 @@
 
 subsection {* Basic Facts of Rings *}
 
-lemma (in cring) a_magma [simp, intro]:
-  "magma (| carrier = carrier R,
-     mult = add R, one = zero R, m_inv = a_inv R |)"
-  using a_abelian_group by (simp only: abelian_group_def)
-
-lemma (in cring) a_l_one [simp, intro]:
-  "l_one (| carrier = carrier R,
-     mult = add R, one = zero R, m_inv = a_inv R |)"
-  using a_abelian_group by (simp only: abelian_group_def)
-
-lemma (in cring) a_abelian_group_parts [simp, intro]:
-  "semigroup_axioms (| carrier = carrier R,
-     mult = add R, one = zero R, m_inv = a_inv R |)"
-  "group_axioms (| carrier = carrier R,
-     mult = add R, one = zero R, m_inv = a_inv R |)"
-  "abelian_semigroup_axioms (| carrier = carrier R,
-     mult = add R, one = zero R, m_inv = a_inv R |)"
-  using a_abelian_group by (simp_all only: abelian_group_def)
-
-lemma (in cring) a_semigroup:
-  "semigroup (| carrier = carrier R,
-     mult = add R, one = zero R, m_inv = a_inv R |)"
-  by (simp add: semigroup_def)
-
-lemma (in cring) a_group:
-  "group (| carrier = carrier R,
-     mult = add R, one = zero R, m_inv = a_inv R |)"
-  by (simp add: group_def)
-
-lemma (in cring) a_abelian_semigroup:
-  "abelian_semigroup (| carrier = carrier R,
-     mult = add R, one = zero R, m_inv = a_inv R |)"
-  by (simp add: abelian_semigroup_def)
-
-lemmas group_record_simps = semigroup.simps monoid.simps group.simps
-
-lemmas (in cring) a_closed [intro, simp] =
-  magma.m_closed [OF a_magma, simplified group_record_simps]
-
-lemmas (in cring) zero_closed [intro, simp] = 
-  l_one.one_closed [OF a_l_one, simplified group_record_simps]
-
-lemmas (in cring) a_inv_closed [intro, simp] =
-  group.inv_closed [OF a_group, simplified group_record_simps]
+lemma cringI:
+  assumes abelian_group: "abelian_group R"
+    and comm_monoid: "comm_monoid R"
+    and l_distr: "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
+      ==> mult R (add R x y) z = add R (mult R x z) (mult R y z)"
+  shows "cring R"
+  by (auto intro: cring.intro
+    abelian_group.axioms comm_monoid.axioms cring_axioms.intro prems)
 
-lemma (in cring) minus_closed [intro, simp]:
-  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y \<in> carrier R"
-  by (simp add: minus_def)
-
-lemmas (in cring) a_l_cancel [simp] =
-  group.l_cancel [OF a_group, simplified group_record_simps]
-
-lemmas (in cring) a_r_cancel [simp] =
-  group.r_cancel [OF a_group, simplified group_record_simps]
-
-lemmas (in cring) a_assoc =
-  semigroup.m_assoc [OF a_semigroup, simplified group_record_simps]
-
-lemmas (in cring) l_zero [simp] =
-  l_one.l_one [OF a_l_one, simplified group_record_simps]
-
-lemmas (in cring) l_neg =
-  group.l_inv [OF a_group, simplified group_record_simps]
-
-lemmas (in cring) a_comm =
-  abelian_semigroup.m_comm [OF a_abelian_semigroup,
-  simplified group_record_simps]
+lemma (in cring) is_abelian_group:
+  "abelian_group R"
+  by (auto intro!: abelian_groupI a_assoc a_comm l_neg)
 
-lemmas (in cring) a_lcomm =
-  abelian_semigroup.m_lcomm [OF a_abelian_semigroup, simplified group_record_simps]
-
-lemma (in cring) r_zero [simp]:
-  "x \<in> carrier R ==> x \<oplus> \<zero> = x"
-  using group.r_one [OF a_group]
-  by simp
-
-lemma (in cring) r_neg:
-  "x \<in> carrier R ==> x \<oplus> (\<ominus> x) = \<zero>"
-  using group.r_inv [OF a_group]
-  by simp
-
-lemmas (in cring) minus_zero [simp] =
-  group.inv_one [OF a_group, simplified group_record_simps]
-
-lemma (in cring) minus_minus [simp]:
-  "x \<in> carrier R ==> \<ominus> (\<ominus> x) = x"
-  using group.inv_inv [OF a_group, simplified group_record_simps]
-  by simp
-
-lemma (in cring) minus_add:
-  "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> (x \<oplus> y) = \<ominus> x \<oplus> \<ominus> y"
-  using abelian_group.inv_mult [OF a_abelian_group]
-  by simp
-
-lemmas (in cring) a_ac = a_assoc a_comm a_lcomm
+lemma (in cring) is_comm_monoid:
+  "comm_monoid R"
+  by (auto intro!: comm_monoidI m_assoc m_comm)
 
 subsection {* Normaliser for Commutative Rings *}
 
-lemma (in cring) r_neg2:
-  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> (\<ominus> x \<oplus> y) = y"
+lemma (in abelian_group) r_neg2:
+  "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> (\<ominus> x \<oplus> y) = y"
 proof -
-  assume G: "x \<in> carrier R" "y \<in> carrier R"
-  then have "(x \<oplus> \<ominus> x) \<oplus> y = y" by (simp only: r_neg l_zero)
-  with G show ?thesis by (simp add: a_ac)
+  assume G: "x \<in> carrier G" "y \<in> carrier G"
+  then have "(x \<oplus> \<ominus> x) \<oplus> y = y"
+    by (simp only: r_neg l_zero)
+  with G show ?thesis 
+    by (simp add: a_ac)
 qed
 
-lemma (in cring) r_neg1:
-  "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> x \<oplus> (x \<oplus> y) = y"
+lemma (in abelian_group) r_neg1:
+  "[| x \<in> carrier G; y \<in> carrier G |] ==> \<ominus> x \<oplus> (x \<oplus> y) = y"
 proof -
-  assume G: "x \<in> carrier R" "y \<in> carrier R"
-  then have "(\<ominus> x \<oplus> x) \<oplus> y = y" by (simp only: l_neg l_zero)
+  assume G: "x \<in> carrier G" "y \<in> carrier G"
+  then have "(\<ominus> x \<oplus> x) \<oplus> y = y" 
+    by (simp only: l_neg l_zero)
   with G show ?thesis by (simp add: a_ac)
 qed
 
@@ -165,10 +342,10 @@
   "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
   ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
 proof -
-  assume G: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
+  assume R: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
   then have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z" by (simp add: m_comm)
-  also from G have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
-  also from G have "... = z \<otimes> x \<oplus> z \<otimes> y" by (simp add: m_comm)
+  also from R have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
+  also from R have "... = z \<otimes> x \<oplus> z \<otimes> y" by (simp add: m_comm)
   finally show ?thesis .
 qed
 
@@ -191,7 +368,7 @@
   "x \<in> carrier R ==> x \<otimes> \<zero> = \<zero>"
 proof -
   assume R: "x \<in> carrier R"
-  then have "x \<otimes> \<zero> = \<zero> \<otimes> x" by (simp add: ac)
+  then have "x \<otimes> \<zero> = \<zero> \<otimes> x" by (simp add: m_ac)
   also from R have "... = \<zero>" by simp
   finally show ?thesis .
 qed
@@ -211,15 +388,19 @@
   "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<otimes> \<ominus> y = \<ominus> (x \<otimes> y)"
 proof -
   assume R: "x \<in> carrier R" "y \<in> carrier R"
-  then have "x \<otimes> \<ominus> y = \<ominus> y \<otimes> x" by (simp add: ac)
+  then have "x \<otimes> \<ominus> y = \<ominus> y \<otimes> x" by (simp add: m_ac)
   also from R have "... = \<ominus> (y \<otimes> x)" by (simp add: l_minus)
-  also from R have "... = \<ominus> (x \<otimes> y)" by (simp add: ac)
+  also from R have "... = \<ominus> (x \<otimes> y)" by (simp add: m_ac)
   finally show ?thesis .
 qed
 
+lemma (in cring) minus_eq:
+  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y = x \<oplus> \<ominus> y"
+  by (simp only: minus_def)
+
 lemmas (in cring) cring_simprules =
   a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
-  a_assoc l_zero l_neg a_comm m_assoc l_one l_distr m_comm minus_def
+  a_assoc l_zero l_neg a_comm m_assoc l_one l_distr m_comm minus_eq
   r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero
   a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus
 
@@ -227,7 +408,11 @@
 
 method_setup algebra =
   {* Method.ctxt_args cring_normalise *}
-  {* computes distributive normal form in commutative rings (locales version) *}
+  {* computes distributive normal form in locale context cring *}
+
+lemma (in cring) nat_pow_zero:
+  "(n::nat) ~= 0 ==> \<zero> (^) n = \<zero>"
+  by (induct n) simp_all
 
 text {* Two examples for use of method algebra *}
 
@@ -244,83 +429,6 @@
 
 subsection {* Sums over Finite Sets *}
 
-text {*
-  This definition makes it easy to lift lemmas from @{term finprod}.
-*}
-
-constdefs
-  finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b"
-  "finsum R f A == finprod (| carrier = carrier R,
-     mult = add R, one = zero R, m_inv = a_inv R |) f A"
-
-lemma (in cring) a_abelian_monoid:
-  "abelian_monoid (| carrier = carrier R,
-     mult = add R, one = zero R, m_inv = a_inv R |)"
-  by (simp add: abelian_monoid_def)
-
-(*
-  lemmas (in cring) finsum_empty [simp] =
-    abelian_monoid.finprod_empty [OF a_abelian_monoid, simplified]
-  is dangeous, because attributes (like simplified) are applied upon opening
-  the locale, simplified refers to the simpset at that time!!!
-*)
-
-lemmas (in cring) finsum_empty [simp] =
-  abelian_monoid.finprod_empty [OF a_abelian_monoid, folded finsum_def,
-    simplified group_record_simps]
-
-lemmas (in cring) finsum_insert [simp] =
-  abelian_monoid.finprod_insert [OF a_abelian_monoid, folded finsum_def,
-    simplified group_record_simps]
-
-lemmas (in cring) finsum_zero =
-  abelian_monoid.finprod_one [OF a_abelian_monoid, folded finsum_def,
-    simplified group_record_simps]
-
-lemmas (in cring) finsum_closed [simp] =
-  abelian_monoid.finprod_closed [OF a_abelian_monoid, folded finsum_def,
-    simplified group_record_simps]
-
-lemmas (in cring) finsum_Un_Int =
-  abelian_monoid.finprod_Un_Int [OF a_abelian_monoid, folded finsum_def,
-    simplified group_record_simps]
-
-lemmas (in cring) finsum_Un_disjoint =
-  abelian_monoid.finprod_Un_disjoint [OF a_abelian_monoid, folded finsum_def,
-    simplified group_record_simps]
-
-lemmas (in cring) finsum_addf =
-  abelian_monoid.finprod_multf [OF a_abelian_monoid, folded finsum_def,
-    simplified group_record_simps]
-
-lemmas (in cring) finsum_cong' =
-  abelian_monoid.finprod_cong' [OF a_abelian_monoid, folded finsum_def,
-    simplified group_record_simps]
-
-lemmas (in cring) finsum_0 [simp] =
-  abelian_monoid.finprod_0 [OF a_abelian_monoid, folded finsum_def,
-    simplified group_record_simps]
-
-lemmas (in cring) finsum_Suc [simp] =
-  abelian_monoid.finprod_Suc [OF a_abelian_monoid, folded finsum_def,
-    simplified group_record_simps]
-
-lemmas (in cring) finsum_Suc2 =
-  abelian_monoid.finprod_Suc2 [OF a_abelian_monoid, folded finsum_def,
-    simplified group_record_simps]
-
-lemmas (in cring) finsum_add [simp] =
-  abelian_monoid.finprod_mult [OF a_abelian_monoid, folded finsum_def,
-    simplified group_record_simps]
-
-lemmas (in cring) finsum_cong =
-  abelian_monoid.finprod_cong [OF a_abelian_monoid, folded finsum_def,
-    simplified group_record_simps]
-
-text {*Usually, if this rule causes a failed congruence proof error,
-   the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
-   Adding @{thm [source] Pi_def} to the simpset is often useful. *}
-
 lemma (in cring) finsum_ldistr:
   "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
    finsum R f A \<otimes> a = finsum R (%i. f i \<otimes> a) A"
@@ -380,4 +488,90 @@
   with R show ?thesis by algebra
 qed
 
+subsection {* Morphisms *}
+
+constdefs
+  ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set"
+  "ring_hom R S == {h. h \<in> carrier R -> carrier S &
+      (ALL x y. x \<in> carrier R & y \<in> carrier R -->
+        h (mult R x y) = mult S (h x) (h y) &
+        h (add R x y) = add S (h x) (h y)) &
+      h (one R) = one S}"
+
+lemma ring_hom_memI:
+  assumes hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
+    and hom_mult: "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==>
+      h (mult R x y) = mult S (h x) (h y)"
+    and hom_add: "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==>
+      h (add R x y) = add S (h x) (h y)"
+    and hom_one: "h (one R) = one S"
+  shows "h \<in> ring_hom R S"
+  by (auto simp add: ring_hom_def prems Pi_def)
+
+lemma ring_hom_closed:
+  "[| h \<in> ring_hom R S; x \<in> carrier R |] ==> h x \<in> carrier S"
+  by (auto simp add: ring_hom_def funcset_mem)
+
+lemma ring_hom_mult:
+  "[| h \<in> ring_hom R S; x \<in> carrier R; y \<in> carrier R |] ==>
+  h (mult R x y) = mult S (h x) (h y)"
+  by (simp add: ring_hom_def)
+
+lemma ring_hom_add:
+  "[| h \<in> ring_hom R S; x \<in> carrier R; y \<in> carrier R |] ==>
+  h (add R x y) = add S (h x) (h y)"
+  by (simp add: ring_hom_def)
+
+lemma ring_hom_one:
+  "h \<in> ring_hom R S ==> h (one R) = one S"
+  by (simp add: ring_hom_def)
+
+locale ring_hom_cring = cring R + cring S + var h +
+  assumes homh [simp, intro]: "h \<in> ring_hom R S"
+  notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
+    and hom_mult [simp] = ring_hom_mult [OF homh]
+    and hom_add [simp] = ring_hom_add [OF homh]
+    and hom_one [simp] = ring_hom_one [OF homh]
+
+lemma (in ring_hom_cring) hom_zero [simp]:
+  "h \<zero> = \<zero>\<^sub>2"
+proof -
+  have "h \<zero> \<oplus>\<^sub>2 h \<zero> = h \<zero> \<oplus>\<^sub>2 \<zero>\<^sub>2"
+    by (simp add: hom_add [symmetric] del: hom_add)
+  then show ?thesis by (simp del: S.r_zero)
+qed
+
+lemma (in ring_hom_cring) hom_a_inv [simp]:
+  "x \<in> carrier R ==> h (\<ominus> x) = \<ominus>\<^sub>2 h x"
+proof -
+  assume R: "x \<in> carrier R"
+  then have "h x \<oplus>\<^sub>2 h (\<ominus> x) = h x \<oplus>\<^sub>2 (\<ominus>\<^sub>2 h x)"
+    by (simp add: hom_add [symmetric] R.r_neg S.r_neg del: hom_add)
+  with R show ?thesis by simp
+qed
+
+lemma (in ring_hom_cring) hom_finsum [simp]:
+  "[| finite A; f \<in> A -> carrier R |] ==>
+  h (finsum R f A) = finsum S (h o f) A"
+proof (induct set: Finites)
+  case empty then show ?case by simp
+next
+  case insert then show ?case by (simp add: Pi_def)
+qed
+
+lemma (in ring_hom_cring) hom_finprod:
+  "[| finite A; f \<in> A -> carrier R |] ==>
+  h (finprod R f A) = finprod S (h o f) A"
+proof (induct set: Finites)
+  case empty then show ?case by simp
+next
+  case insert then show ?case by (simp add: Pi_def)
+qed
+
+declare ring_hom_cring.hom_finprod [simp]
+
+lemma id_ring_hom [simp]:
+  "id \<in> ring_hom R R"
+  by (auto intro!: ring_hom_memI)
+
 end
diff -r 4822d9597d1e -r d3671b878828 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Tue Apr 29 12:36:49 2003 +0200
+++ b/src/HOL/Algebra/Coset.thy	Wed Apr 30 10:01:35 2003 +0200
@@ -10,27 +10,27 @@
 declare (in group) l_inv [simp]  r_inv [simp] 
 
 constdefs
-  r_coset    :: "[('a,'b) group_scheme,'a set, 'a] => 'a set"    
+  r_coset    :: "[('a,'b) monoid_scheme,'a set, 'a] => 'a set"    
    "r_coset G H a == (% x. (mult G) x a) ` H"
 
-  l_coset    :: "[('a,'b) group_scheme, 'a, 'a set] => 'a set"
+  l_coset    :: "[('a,'b) monoid_scheme, 'a, 'a set] => 'a set"
    "l_coset G a H == (% x. (mult G) a x) ` H"
 
-  rcosets  :: "[('a,'b) group_scheme,'a set] => ('a set)set"
+  rcosets  :: "[('a,'b) monoid_scheme,'a set] => ('a set)set"
    "rcosets G H == r_coset G H ` (carrier G)"
 
-  set_mult  :: "[('a,'b) group_scheme,'a set,'a set] => 'a set"
+  set_mult  :: "[('a,'b) monoid_scheme,'a set,'a set] => 'a set"
    "set_mult G H K == (%(x,y). (mult G) x y) ` (H \<times> K)"
 
-  set_inv   :: "[('a,'b) group_scheme,'a set] => 'a set"
+  set_inv   :: "[('a,'b) monoid_scheme,'a set] => 'a set"
    "set_inv G H == (m_inv G) ` H"
 
-  normal     :: "['a set, ('a,'b) group_scheme] => bool"       (infixl "<|" 60)
+  normal     :: "['a set, ('a,'b) monoid_scheme] => bool"       (infixl "<|" 60)
    "normal H G == subgroup H G & 
                   (\<forall>x \<in> carrier G. r_coset G H x = l_coset G x H)"
 
 syntax (xsymbols)
-  normal  :: "['a set, ('a,'b) group_scheme] => bool" (infixl "\<lhd>" 60)
+  normal  :: "['a set, ('a,'b) monoid_scheme] => bool" (infixl "\<lhd>" 60)
 
 locale coset = group G +
   fixes rcos      :: "['a set, 'a] => 'a set"     (infixl "#>" 60)
@@ -153,7 +153,7 @@
 subsection{*normal subgroups*}
 
 (*????????????????
-text{*Allows use of theorems proved in the locale coset*}
+text "Allows use of theorems proved in the locale coset"
 lemma subgroup_imp_coset: "subgroup H G ==> coset G"
 apply (drule subgroup_imp_group)
 apply (simp add: group_def coset_def)  
@@ -406,13 +406,13 @@
 subsection {*Factorization of a Group*}
 
 constdefs
-  FactGroup :: "[('a,'b) group_scheme, 'a set] => ('a set) group"
+  FactGroup :: "[('a,'b) monoid_scheme, 'a set] => ('a set) monoid"
      (infixl "Mod" 60)
    "FactGroup G H ==
       (| carrier = rcosets G H,
 	 mult = (%X: rcosets G H. %Y: rcosets G H. set_mult G X Y),
-	 one = H,
-	 m_inv = (%X: rcosets G H. set_inv G X) |)"
+	 one = H (*,
+	 m_inv = (%X: rcosets G H. set_inv G X) *) |)"
 
 lemma (in coset) setmult_closed:
      "[| H <| G; K1 \<in> rcosets G H; K2 \<in> rcosets G H |] 
@@ -482,18 +482,13 @@
   "H <| G ==> group (G Mod H)"
 apply (insert is_coset) 
 apply (simp add: FactGroup_def) 
-apply (rule group.intro)
-   apply (rule magma.intro) 
-   apply (simp add: coset.setmult_closed)
-  apply (rule semigroup_axioms.intro)
+apply (rule groupI)
+    apply (simp add: coset.setmult_closed)
+   apply (simp add: normal_imp_subgroup subgroup_in_rcosets)
   apply (simp add: restrictI coset.setmult_closed coset.setrcos_assoc)
- apply (rule l_one.intro)
-  apply (simp add: normal_imp_subgroup subgroup_in_rcosets)
  apply (simp add: normal_imp_subgroup
    subgroup_in_rcosets coset.setrcos_mult_eq)
-apply (rule group_axioms.intro)
- apply (simp add: restrictI setinv_closed)
-apply (simp add: setinv_closed coset.setrcos_inv_mult_group_eq)
+apply (auto dest: coset.setrcos_inv_mult_group_eq simp add: setinv_closed)
 done
 
 (*????????????????
diff -r 4822d9597d1e -r d3671b878828 src/HOL/Algebra/FiniteProduct.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/FiniteProduct.thy	Wed Apr 30 10:01:35 2003 +0200
@@ -0,0 +1,483 @@
+(*  Title:      Product Operator for Commutative Monoids
+    ID:         $Id$
+    Author:     Clemens Ballarin, started 19 November 2002
+
+This file is largely based on HOL/Finite_Set.thy.
+*)
+
+header {* Product Operator *}
+
+theory FiniteProduct = Group:
+
+(* Instantiation of LC from Finite_Set.thy is not possible,
+   because here we have explicit typing rules like x : carrier G.
+   We introduce an explicit argument for the domain D *)
+
+consts
+  foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set"
+
+inductive "foldSetD D f e"
+  intros
+    emptyI [intro]: "e : D ==> ({}, e) : foldSetD D f e"
+    insertI [intro]: "[| x ~: A; f x y : D; (A, y) : foldSetD D f e |] ==>
+                      (insert x A, f x y) : foldSetD D f e"
+
+inductive_cases empty_foldSetDE [elim!]: "({}, x) : foldSetD D f e"
+
+constdefs
+  foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a"
+  "foldD D f e A == THE x. (A, x) : foldSetD D f e"
+
+lemma foldSetD_closed:
+  "[| (A, z) : foldSetD D f e ; e : D; !!x y. [| x : A; y : D |] ==> f x y : D 
+      |] ==> z : D";
+  by (erule foldSetD.elims) auto
+
+lemma Diff1_foldSetD:
+  "[| (A - {x}, y) : foldSetD D f e; x : A; f x y : D |] ==>
+   (A, f x y) : foldSetD D f e"
+  apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
+    apply auto
+  done
+
+lemma foldSetD_imp_finite [simp]: "(A, x) : foldSetD D f e ==> finite A"
+  by (induct set: foldSetD) auto
+
+lemma finite_imp_foldSetD:
+  "[| finite A; e : D; !!x y. [| x : A; y : D |] ==> f x y : D |] ==>
+   EX x. (A, x) : foldSetD D f e"
+proof (induct set: Finites)
+  case empty then show ?case by auto
+next
+  case (insert F x)
+  then obtain y where y: "(F, y) : foldSetD D f e" by auto
+  with insert have "y : D" by (auto dest: foldSetD_closed)
+  with y and insert have "(insert x F, f x y) : foldSetD D f e"
+    by (intro foldSetD.intros) auto
+  then show ?case ..
+qed
+
+subsection {* Left-commutative operations *}
+
+locale LCD =
+  fixes B :: "'b set"
+  and D :: "'a set"
+  and f :: "'b => 'a => 'a"    (infixl "\<cdot>" 70)
+  assumes left_commute:
+    "[| x : B; y : B; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
+  and f_closed [simp, intro!]: "!!x y. [| x : B; y : D |] ==> f x y : D"
+
+lemma (in LCD) foldSetD_closed [dest]:
+  "(A, z) : foldSetD D f e ==> z : D";
+  by (erule foldSetD.elims) auto
+
+lemma (in LCD) Diff1_foldSetD:
+  "[| (A - {x}, y) : foldSetD D f e; x : A; A <= B |] ==>
+  (A, f x y) : foldSetD D f e"
+  apply (subgoal_tac "x : B")
+   prefer 2 apply fast
+  apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
+    apply auto
+  done
+
+lemma (in LCD) foldSetD_imp_finite [simp]:
+  "(A, x) : foldSetD D f e ==> finite A"
+  by (induct set: foldSetD) auto
+
+lemma (in LCD) finite_imp_foldSetD:
+  "[| finite A; A <= B; e : D |] ==> EX x. (A, x) : foldSetD D f e"
+proof (induct set: Finites)
+  case empty then show ?case by auto
+next
+  case (insert F x)
+  then obtain y where y: "(F, y) : foldSetD D f e" by auto
+  with insert have "y : D" by auto
+  with y and insert have "(insert x F, f x y) : foldSetD D f e"
+    by (intro foldSetD.intros) auto
+  then show ?case ..
+qed
+
+lemma (in LCD) foldSetD_determ_aux:
+  "e : D ==> ALL A x. A <= B & card A < n --> (A, x) : foldSetD D f e -->
+    (ALL y. (A, y) : foldSetD D f e --> y = x)"
+  apply (induct n)
+   apply (auto simp add: less_Suc_eq) (* slow *)
+  apply (erule foldSetD.cases)
+   apply blast
+  apply (erule foldSetD.cases)
+   apply blast
+  apply clarify
+  txt {* force simplification of @{text "card A < card (insert ...)"}. *}
+  apply (erule rev_mp)
+  apply (simp add: less_Suc_eq_le)
+  apply (rule impI)
+  apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb")
+   apply (subgoal_tac "Aa = Ab")
+    prefer 2 apply (blast elim!: equalityE)
+   apply blast
+  txt {* case @{prop "xa \<notin> xb"}. *}
+  apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab")
+   prefer 2 apply (blast elim!: equalityE)
+  apply clarify
+  apply (subgoal_tac "Aa = insert xb Ab - {xa}")
+   prefer 2 apply blast
+  apply (subgoal_tac "card Aa <= card Ab")
+   prefer 2
+   apply (rule Suc_le_mono [THEN subst])
+   apply (simp add: card_Suc_Diff1)
+  apply (rule_tac A1 = "Aa - {xb}" in finite_imp_foldSetD [THEN exE])
+     apply (blast intro: foldSetD_imp_finite finite_Diff)
+    apply best
+   apply assumption
+  apply (frule (1) Diff1_foldSetD)
+   apply best
+  apply (subgoal_tac "ya = f xb x")
+   prefer 2
+   apply (subgoal_tac "Aa <= B")
+    prefer 2 apply best (* slow *)
+   apply (blast del: equalityCE)
+  apply (subgoal_tac "(Ab - {xa}, x) : foldSetD D f e")
+   prefer 2 apply simp
+  apply (subgoal_tac "yb = f xa x")
+   prefer 2 
+   apply (blast del: equalityCE dest: Diff1_foldSetD)
+  apply (simp (no_asm_simp))
+  apply (rule left_commute)
+    apply assumption
+   apply best (* slow *)
+  apply best
+  done
+
+lemma (in LCD) foldSetD_determ:
+  "[| (A, x) : foldSetD D f e; (A, y) : foldSetD D f e; e : D; A <= B |]
+  ==> y = x"
+  by (blast intro: foldSetD_determ_aux [rule_format])
+
+lemma (in LCD) foldD_equality:
+  "[| (A, y) : foldSetD D f e; e : D; A <= B |] ==> foldD D f e A = y"
+  by (unfold foldD_def) (blast intro: foldSetD_determ)
+
+lemma foldD_empty [simp]:
+  "e : D ==> foldD D f e {} = e"
+  by (unfold foldD_def) blast
+
+lemma (in LCD) foldD_insert_aux:
+  "[| x ~: A; x : B; e : D; A <= B |] ==>
+    ((insert x A, v) : foldSetD D f e) =
+    (EX y. (A, y) : foldSetD D f e & v = f x y)"
+  apply auto
+  apply (rule_tac A1 = A in finite_imp_foldSetD [THEN exE])
+     apply (fastsimp dest: foldSetD_imp_finite)
+    apply assumption
+   apply assumption
+  apply (blast intro: foldSetD_determ)
+  done
+
+lemma (in LCD) foldD_insert:
+    "[| finite A; x ~: A; x : B; e : D; A <= B |] ==>
+     foldD D f e (insert x A) = f x (foldD D f e A)"
+  apply (unfold foldD_def)
+  apply (simp add: foldD_insert_aux)
+  apply (rule the_equality)
+   apply (auto intro: finite_imp_foldSetD
+     cong add: conj_cong simp add: foldD_def [symmetric] foldD_equality)
+  done
+
+lemma (in LCD) foldD_closed [simp]:
+  "[| finite A; e : D; A <= B |] ==> foldD D f e A : D"
+proof (induct set: Finites)
+  case empty then show ?case by (simp add: foldD_empty)
+next
+  case insert then show ?case by (simp add: foldD_insert)
+qed
+
+lemma (in LCD) foldD_commute:
+  "[| finite A; x : B; e : D; A <= B |] ==>
+   f x (foldD D f e A) = foldD D f (f x e) A"
+  apply (induct set: Finites)
+   apply simp
+  apply (auto simp add: left_commute foldD_insert)
+  done
+
+lemma Int_mono2:
+  "[| A <= C; B <= C |] ==> A Int B <= C"
+  by blast
+
+lemma (in LCD) foldD_nest_Un_Int:
+  "[| finite A; finite C; e : D; A <= B; C <= B |] ==>
+   foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)"
+  apply (induct set: Finites)
+   apply simp
+  apply (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb
+    Int_mono2 Un_subset_iff)
+  done
+
+lemma (in LCD) foldD_nest_Un_disjoint:
+  "[| finite A; finite B; A Int B = {}; e : D; A <= B; C <= B |]
+    ==> foldD D f e (A Un B) = foldD D f (foldD D f e B) A"
+  by (simp add: foldD_nest_Un_Int)
+
+-- {* Delete rules to do with @{text foldSetD} relation. *}
+
+declare foldSetD_imp_finite [simp del]
+  empty_foldSetDE [rule del]
+  foldSetD.intros [rule del]
+declare (in LCD)
+  foldSetD_closed [rule del]
+
+subsection {* Commutative monoids *}
+
+text {*
+  We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
+  instead of @{text "'b => 'a => 'a"}.
+*}
+
+locale ACeD =
+  fixes D :: "'a set"
+    and f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
+    and e :: 'a
+  assumes ident [simp]: "x : D ==> x \<cdot> e = x"
+    and commute: "[| x : D; y : D |] ==> x \<cdot> y = y \<cdot> x"
+    and assoc: "[| x : D; y : D; z : D |] ==> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
+    and e_closed [simp]: "e : D"
+    and f_closed [simp]: "[| x : D; y : D |] ==> x \<cdot> y : D"
+
+lemma (in ACeD) left_commute:
+  "[| x : D; y : D; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
+proof -
+  assume D: "x : D" "y : D" "z : D"
+  then have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp add: commute)
+  also from D have "... = y \<cdot> (z \<cdot> x)" by (simp add: assoc)
+  also from D have "z \<cdot> x = x \<cdot> z" by (simp add: commute)
+  finally show ?thesis .
+qed
+
+lemmas (in ACeD) AC = assoc commute left_commute
+
+lemma (in ACeD) left_ident [simp]: "x : D ==> e \<cdot> x = x"
+proof -
+  assume D: "x : D"
+  have "x \<cdot> e = x" by (rule ident)
+  with D show ?thesis by (simp add: commute)
+qed
+
+lemma (in ACeD) foldD_Un_Int:
+  "[| finite A; finite B; A <= D; B <= D |] ==>
+    foldD D f e A \<cdot> foldD D f e B =
+    foldD D f e (A Un B) \<cdot> foldD D f e (A Int B)"
+  apply (induct set: Finites)
+   apply (simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]])
+  apply (simp add: AC insert_absorb Int_insert_left
+    LCD.foldD_insert [OF LCD.intro [of D]]
+    LCD.foldD_closed [OF LCD.intro [of D]]
+    Int_mono2 Un_subset_iff)
+  done
+
+lemma (in ACeD) foldD_Un_disjoint:
+  "[| finite A; finite B; A Int B = {}; A <= D; B <= D |] ==>
+    foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B"
+  by (simp add: foldD_Un_Int
+    left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff)
+
+subsection {* Products over Finite Sets *}
+
+constdefs
+  finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
+  "finprod G f A == if finite A
+      then foldD (carrier G) (mult G o f) (one G) A
+      else arbitrary"
+
+(* TODO: nice syntax for the summation operator inside the locale
+   like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *)
+
+ML_setup {* 
+  Context.>> (fn thy => (simpset_ref_of thy :=
+    simpset_of thy setsubgoaler asm_full_simp_tac; thy))
+*}
+
+lemma (in comm_monoid) finprod_empty [simp]: 
+  "finprod G f {} = \<one>"
+  by (simp add: finprod_def)
+
+ML_setup {* 
+  Context.>> (fn thy => (simpset_ref_of thy :=
+    simpset_of thy setsubgoaler asm_simp_tac; thy))
+*}
+
+declare funcsetI [intro]
+  funcset_mem [dest]
+
+lemma (in comm_monoid) finprod_insert [simp]:
+  "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |] ==>
+   finprod G f (insert a F) = f a \<otimes> finprod G f F"
+  apply (rule trans)
+   apply (simp add: finprod_def)
+  apply (rule trans)
+   apply (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]])
+         apply simp
+         apply (rule m_lcomm)
+           apply fast
+          apply fast
+         apply assumption
+        apply (fastsimp intro: m_closed)
+       apply simp+
+   apply fast
+  apply (auto simp add: finprod_def)
+  done
+
+lemma (in comm_monoid) finprod_one [simp]:
+  "finite A ==> finprod G (%i. \<one>) A = \<one>"
+proof (induct set: Finites)
+  case empty show ?case by simp
+next
+  case (insert A a)
+  have "(%i. \<one>) \<in> A -> carrier G" by auto
+  with insert show ?case by simp
+qed
+
+lemma (in comm_monoid) finprod_closed [simp]:
+  fixes A
+  assumes fin: "finite A" and f: "f \<in> A -> carrier G" 
+  shows "finprod G f A \<in> carrier G"
+using fin f
+proof induct
+  case empty show ?case by simp
+next
+  case (insert A a)
+  then have a: "f a \<in> carrier G" by fast
+  from insert have A: "f \<in> A -> carrier G" by fast
+  from insert A a show ?case by simp
+qed
+
+lemma funcset_Int_left [simp, intro]:
+  "[| f \<in> A -> C; f \<in> B -> C |] ==> f \<in> A Int B -> C"
+  by fast
+
+lemma funcset_Un_left [iff]:
+  "(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)"
+  by fast
+
+lemma (in comm_monoid) finprod_Un_Int:
+  "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
+     finprod G g (A Un B) \<otimes> finprod G g (A Int B) =
+     finprod G g A \<otimes> finprod G g B"
+-- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
+proof (induct set: Finites)
+  case empty then show ?case by (simp add: finprod_closed)
+next
+  case (insert A a)
+  then have a: "g a \<in> carrier G" by fast
+  from insert have A: "g \<in> A -> carrier G" by fast
+  from insert A a show ?case
+    by (simp add: m_ac Int_insert_left insert_absorb finprod_closed
+          Int_mono2 Un_subset_iff) 
+qed
+
+lemma (in comm_monoid) finprod_Un_disjoint:
+  "[| finite A; finite B; A Int B = {};
+      g \<in> A -> carrier G; g \<in> B -> carrier G |]
+   ==> finprod G g (A Un B) = finprod G g A \<otimes> finprod G g B"
+  apply (subst finprod_Un_Int [symmetric])
+      apply (auto simp add: finprod_closed)
+  done
+
+lemma (in comm_monoid) finprod_multf:
+  "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
+   finprod G (%x. f x \<otimes> g x) A = (finprod G f A \<otimes> finprod G g A)"
+proof (induct set: Finites)
+  case empty show ?case by simp
+next
+  case (insert A a) then
+  have fA: "f : A -> carrier G" by fast
+  from insert have fa: "f a : carrier G" by fast
+  from insert have gA: "g : A -> carrier G" by fast
+  from insert have ga: "g a : carrier G" by fast
+  from insert have fgA: "(%x. f x \<otimes> g x) : A -> carrier G"
+    by (simp add: Pi_def)
+  show ?case  (* check if all simps are really necessary *)
+    by (simp add: insert fA fa gA ga fgA m_ac Int_insert_left insert_absorb
+      Int_mono2 Un_subset_iff)
+qed
+
+lemma (in comm_monoid) finprod_cong':
+  "[| A = B; g : B -> carrier G;
+      !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B"
+proof -
+  assume prems: "A = B" "g : B -> carrier G"
+    "!!i. i : B ==> f i = g i"
+  show ?thesis
+  proof (cases "finite B")
+    case True
+    then have "!!A. [| A = B; g : B -> carrier G;
+      !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B"
+    proof induct
+      case empty thus ?case by simp
+    next
+      case (insert B x)
+      then have "finprod G f A = finprod G f (insert x B)" by simp
+      also from insert have "... = f x \<otimes> finprod G f B"
+      proof (intro finprod_insert)
+	show "finite B" .
+      next
+	show "x ~: B" .
+      next
+	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
+	  "g \<in> insert x B \<rightarrow> carrier G"
+	thus "f : B -> carrier G" by fastsimp
+      next
+	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
+	  "g \<in> insert x B \<rightarrow> carrier G"
+	thus "f x \<in> carrier G" by fastsimp
+      qed
+      also from insert have "... = g x \<otimes> finprod G g B" by fastsimp
+      also from insert have "... = finprod G g (insert x B)"
+      by (intro finprod_insert [THEN sym]) auto
+      finally show ?case .
+    qed
+    with prems show ?thesis by simp
+  next
+    case False with prems show ?thesis by (simp add: finprod_def)
+  qed
+qed
+
+lemma (in comm_monoid) finprod_cong:
+  "[| A = B; !!i. i : B ==> f i = g i;
+      g : B -> carrier G = True |] ==> finprod G f A = finprod G g B"
+  by (rule finprod_cong') fast+
+
+text {*Usually, if this rule causes a failed congruence proof error,
+  the reason is that the premise @{text "g : B -> carrier G"} cannot be shown.
+  Adding @{thm [source] Pi_def} to the simpset is often useful.
+  For this reason, @{thm [source] comm_monoid.finprod_cong}
+  is not added to the simpset by default.
+*}
+
+declare funcsetI [rule del]
+  funcset_mem [rule del]
+
+lemma (in comm_monoid) finprod_0 [simp]:
+  "f : {0::nat} -> carrier G ==> finprod G f {..0} = f 0"
+by (simp add: Pi_def)
+
+lemma (in comm_monoid) finprod_Suc [simp]:
+  "f : {..Suc n} -> carrier G ==>
+   finprod G f {..Suc n} = (f (Suc n) \<otimes> finprod G f {..n})"
+by (simp add: Pi_def atMost_Suc)
+
+lemma (in comm_monoid) finprod_Suc2:
+  "f : {..Suc n} -> carrier G ==>
+   finprod G f {..Suc n} = (finprod G (%i. f (Suc i)) {..n} \<otimes> f 0)"
+proof (induct n)
+  case 0 thus ?case by (simp add: Pi_def)
+next
+  case Suc thus ?case by (simp add: m_assoc Pi_def)
+qed
+
+lemma (in comm_monoid) finprod_mult [simp]:
+  "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==>
+     finprod G (%i. f i \<otimes> g i) {..n::nat} =
+     finprod G f {..n} \<otimes> finprod G g {..n}"
+  by (induct n) (simp_all add: m_ac Pi_def)
+
+end
+
diff -r 4822d9597d1e -r d3671b878828 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Tue Apr 29 12:36:49 2003 +0200
+++ b/src/HOL/Algebra/Group.thy	Wed Apr 30 10:01:35 2003 +0200
@@ -6,18 +6,23 @@
 Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
 *)
 
-header {* Algebraic Structures up to Abelian Groups *}
+header {* Algebraic Structures up to Commutative Groups *}
 
 theory Group = FuncSet:
 
+axclass number < type
+
+instance nat :: number ..
+instance int :: number ..
+
+section {* From Magmas to Groups *}
+
 text {*
   Definitions follow Jacobson, Basic Algebra I, Freeman, 1985; with
   the exception of \emph{magma} which, following Bourbaki, is a set
   together with a binary, closed operation.
 *}
 
-section {* From Magmas to Groups *}
-
 subsection {* Definitions *}
 
 record 'a semigroup =
@@ -27,8 +32,23 @@
 record 'a monoid = "'a semigroup" +
   one :: 'a ("\<one>\<index>")
 
-record 'a group = "'a monoid" +
-  m_inv :: "'a => 'a" ("inv\<index> _" [81] 80)
+constdefs
+  m_inv :: "[('a, 'm) monoid_scheme, 'a] => 'a" ("inv\<index> _" [81] 80)
+  "m_inv G x == (THE y. y \<in> carrier G &
+                  mult G x y = one G & mult G y x = one G)"
+
+  Units :: "('a, 'm) monoid_scheme => 'a set"
+  "Units G == {y. y \<in> carrier G &
+                  (EX x : carrier G. mult G x y = one G & mult G y x = one G)}"
+
+consts
+  pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
+
+defs (overloaded)
+  nat_pow_def: "pow G a n == nat_rec (one G) (%u b. mult G b a) n"
+  int_pow_def: "pow G a z ==
+    let p = nat_rec (one G) (%u b. mult G b a)
+    in if neg z then m_inv G (p (nat (-z))) else p (nat z)"
 
 locale magma = struct G +
   assumes m_closed [intro, simp]:
@@ -37,32 +57,237 @@
 locale semigroup = magma +
   assumes m_assoc:
     "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
-     (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
+    (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
 
-locale l_one = struct G +
+locale monoid = semigroup +
   assumes one_closed [intro, simp]: "\<one> \<in> carrier G"
     and l_one [simp]: "x \<in> carrier G ==> \<one> \<otimes> x = x"
+    and r_one [simp]: "x \<in> carrier G ==> x \<otimes> \<one> = x"
 
-locale group = semigroup + l_one +
-  assumes inv_closed [intro, simp]: "x \<in> carrier G ==> inv x \<in> carrier G"
-    and l_inv: "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
+lemma monoidI:
+  assumes m_closed:
+      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
+    and one_closed: "one G \<in> carrier G"
+    and m_assoc:
+      "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
+      mult G (mult G x y) z = mult G x (mult G y z)"
+    and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
+    and r_one: "!!x. x \<in> carrier G ==> mult G x (one G) = x"
+  shows "monoid G"
+  by (fast intro!: monoid.intro magma.intro semigroup_axioms.intro
+    semigroup.intro monoid_axioms.intro
+    intro: prems)
+
+lemma (in monoid) Units_closed [dest]:
+  "x \<in> Units G ==> x \<in> carrier G"
+  by (unfold Units_def) fast
+
+lemma (in monoid) inv_unique:
+  assumes eq: "y \<otimes> x = \<one>" "x \<otimes> y' = \<one>"
+    and G: "x \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G"
+  shows "y = y'"
+proof -
+  from G eq have "y = y \<otimes> (x \<otimes> y')" by simp
+  also from G have "... = (y \<otimes> x) \<otimes> y'" by (simp add: m_assoc)
+  also from G eq have "... = y'" by simp
+  finally show ?thesis .
+qed
+
+lemma (in monoid) Units_inv_closed [intro, simp]:
+  "x \<in> Units G ==> inv x \<in> carrier G"
+  apply (unfold Units_def m_inv_def)
+  apply auto
+  apply (rule theI2, fast)
+   apply (fast intro: inv_unique)
+  apply fast
+  done
+
+lemma (in monoid) Units_l_inv:
+  "x \<in> Units G ==> inv x \<otimes> x = \<one>"
+  apply (unfold Units_def m_inv_def)
+  apply auto
+  apply (rule theI2, fast)
+   apply (fast intro: inv_unique)
+  apply fast
+  done
+
+lemma (in monoid) Units_r_inv:
+  "x \<in> Units G ==> x \<otimes> inv x = \<one>"
+  apply (unfold Units_def m_inv_def)
+  apply auto
+  apply (rule theI2, fast)
+   apply (fast intro: inv_unique)
+  apply fast
+  done
+
+lemma (in monoid) Units_inv_Units [intro, simp]:
+  "x \<in> Units G ==> inv x \<in> Units G"
+proof -
+  assume x: "x \<in> Units G"
+  show "inv x \<in> Units G"
+    by (auto simp add: Units_def
+      intro: Units_l_inv Units_r_inv x Units_closed [OF x])
+qed
+
+lemma (in monoid) Units_l_cancel [simp]:
+  "[| x \<in> Units G; y \<in> carrier G; z \<in> carrier G |] ==>
+   (x \<otimes> y = x \<otimes> z) = (y = z)"
+proof
+  assume eq: "x \<otimes> y = x \<otimes> z"
+    and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G"
+  then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z"
+    by (simp add: m_assoc Units_closed)
+  with G show "y = z" by (simp add: Units_l_inv)
+next
+  assume eq: "y = z"
+    and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G"
+  then show "x \<otimes> y = x \<otimes> z" by simp
+qed
+
+lemma (in monoid) Units_inv_inv [simp]:
+  "x \<in> Units G ==> inv (inv x) = x"
+proof -
+  assume x: "x \<in> Units G"
+  then have "inv x \<otimes> inv (inv x) = inv x \<otimes> x"
+    by (simp add: Units_l_inv Units_r_inv)
+  with x show ?thesis by (simp add: Units_closed)
+qed
+
+lemma (in monoid) inv_inj_on_Units:
+  "inj_on (m_inv G) (Units G)"
+proof (rule inj_onI)
+  fix x y
+  assume G: "x \<in> Units G" "y \<in> Units G" and eq: "inv x = inv y"
+  then have "inv (inv x) = inv (inv y)" by simp
+  with G show "x = y" by simp
+qed
+
+text {* Power *}
+
+lemma (in monoid) nat_pow_closed [intro, simp]:
+  "x \<in> carrier G ==> x (^) (n::nat) \<in> carrier G"
+  by (induct n) (simp_all add: nat_pow_def)
+
+lemma (in monoid) nat_pow_0 [simp]:
+  "x (^) (0::nat) = \<one>"
+  by (simp add: nat_pow_def)
+
+lemma (in monoid) nat_pow_Suc [simp]:
+  "x (^) (Suc n) = x (^) n \<otimes> x"
+  by (simp add: nat_pow_def)
+
+lemma (in monoid) nat_pow_one [simp]:
+  "\<one> (^) (n::nat) = \<one>"
+  by (induct n) simp_all
+
+lemma (in monoid) nat_pow_mult:
+  "x \<in> carrier G ==> x (^) (n::nat) \<otimes> x (^) m = x (^) (n + m)"
+  by (induct m) (simp_all add: m_assoc [THEN sym])
+
+lemma (in monoid) nat_pow_pow:
+  "x \<in> carrier G ==> (x (^) n) (^) m = x (^) (n * m::nat)"
+  by (induct m) (simp, simp add: nat_pow_mult add_commute)
+
+text {*
+  A group is a monoid all of whose elements are invertible.
+*}
+
+locale group = monoid +
+  assumes Units: "carrier G <= Units G"
+
+theorem groupI:
+  assumes m_closed [simp]:
+      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
+    and one_closed [simp]: "one G \<in> carrier G"
+    and m_assoc:
+      "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
+      mult G (mult G x y) z = mult G x (mult G y z)"
+    and l_one [simp]: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
+    and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G"
+  shows "group G"
+proof -
+  have l_cancel [simp]:
+    "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
+    (mult G x y = mult G x z) = (y = z)"
+  proof
+    fix x y z
+    assume eq: "mult G x y = mult G x z"
+      and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
+    with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G"
+      and l_inv: "mult G x_inv x = one G" by fast
+    from G eq xG have "mult G (mult G x_inv x) y = mult G (mult G x_inv x) z"
+      by (simp add: m_assoc)
+    with G show "y = z" by (simp add: l_inv)
+  next
+    fix x y z
+    assume eq: "y = z"
+      and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
+    then show "mult G x y = mult G x z" by simp
+  qed
+  have r_one:
+    "!!x. x \<in> carrier G ==> mult G x (one G) = x"
+  proof -
+    fix x
+    assume x: "x \<in> carrier G"
+    with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G"
+      and l_inv: "mult G x_inv x = one G" by fast
+    from x xG have "mult G x_inv (mult G x (one G)) = mult G x_inv x"
+      by (simp add: m_assoc [symmetric] l_inv)
+    with x xG show "mult G x (one G) = x" by simp 
+  qed
+  have inv_ex:
+    "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G &
+      mult G x y = one G"
+  proof -
+    fix x
+    assume x: "x \<in> carrier G"
+    with l_inv_ex obtain y where y: "y \<in> carrier G"
+      and l_inv: "mult G y x = one G" by fast
+    from x y have "mult G y (mult G x y) = mult G y (one G)"
+      by (simp add: m_assoc [symmetric] l_inv r_one)
+    with x y have r_inv: "mult G x y = one G"
+      by simp
+    from x y show "EX y : carrier G. mult G y x = one G &
+      mult G x y = one G"
+      by (fast intro: l_inv r_inv)
+  qed
+  then have carrier_subset_Units: "carrier G <= Units G"
+    by (unfold Units_def) fast
+  show ?thesis
+    by (fast intro!: group.intro magma.intro semigroup_axioms.intro
+      semigroup.intro monoid_axioms.intro group_axioms.intro
+      carrier_subset_Units intro: prems r_one)
+qed
+
+lemma (in monoid) monoid_groupI:
+  assumes l_inv_ex:
+    "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G"
+  shows "group G"
+  by (rule groupI) (auto intro: m_assoc l_inv_ex)
+
+lemma (in group) Units_eq [simp]:
+  "Units G = carrier G"
+proof
+  show "Units G <= carrier G" by fast
+next
+  show "carrier G <= Units G" by (rule Units)
+qed
+
+lemma (in group) inv_closed [intro, simp]:
+  "x \<in> carrier G ==> inv x \<in> carrier G"
+  using Units_inv_closed by simp
+
+lemma (in group) l_inv:
+  "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
+  using Units_l_inv by simp
 
 subsection {* Cancellation Laws and Basic Properties *}
 
 lemma (in group) l_cancel [simp]:
   "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    (x \<otimes> y = x \<otimes> z) = (y = z)"
-proof
-  assume eq: "x \<otimes> y = x \<otimes> z"
-    and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
-  then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z" by (simp add: m_assoc)
-  with G show "y = z" by (simp add: l_inv)
-next
-  assume eq: "y = z"
-    and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
-  then show "x \<otimes> y = x \<otimes> z" by simp
-qed
-
+  using Units_l_inv by simp
+(*
 lemma (in group) r_one [simp]:  
   "x \<in> carrier G ==> x \<otimes> \<one> = x"
 proof -
@@ -71,7 +296,7 @@
     by (simp add: m_assoc [symmetric] l_inv)
   with x show ?thesis by simp 
 qed
-
+*)
 lemma (in group) r_inv:
   "x \<in> carrier G ==> x \<otimes> inv x = \<one>"
 proof -
@@ -106,11 +331,11 @@
 
 lemma (in group) inv_inv [simp]:
   "x \<in> carrier G ==> inv (inv x) = x"
-proof -
-  assume x: "x \<in> carrier G"
-  then have "inv x \<otimes> inv (inv x) = inv x \<otimes> x" by (simp add: l_inv r_inv)
-  with x show ?thesis by simp
-qed
+  using Units_inv_inv by simp
+
+lemma (in group) inv_inj:
+  "inj_on (m_inv G) (carrier G)"
+  using inv_inj_on_Units by simp
 
 lemma (in group) inv_mult_group:
   "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv y \<otimes> inv x"
@@ -121,6 +346,20 @@
   with G show ?thesis by simp
 qed
 
+text {* Power *}
+
+lemma (in group) int_pow_def2:
+  "a (^) (z::int) = (if neg z then inv (a (^) (nat (-z))) else a (^) (nat z))"
+  by (simp add: int_pow_def nat_pow_def Let_def)
+
+lemma (in group) int_pow_0 [simp]:
+  "x (^) (0::int) = \<one>"
+  by (simp add: int_pow_def2)
+
+lemma (in group) int_pow_one [simp]:
+  "\<one> (^) (z::int) = \<one>"
+  by (simp add: int_pow_def2)
+
 subsection {* Substructures *}
 
 locale submagma = var H + struct G +
@@ -128,7 +367,7 @@
     and m_closed [intro, simp]: "[| x \<in> H; y \<in> H |] ==> x \<otimes> y \<in> H"
 
 declare (in submagma) magma.intro [intro] semigroup.intro [intro]
-
+  semigroup_axioms.intro [intro]
 (*
 alternative definition of submagma
 
@@ -167,21 +406,21 @@
     and m_inv_closed [intro, simp]: "x \<in> H ==> inv x \<in> H"
 
 declare (in subgroup) group.intro [intro]
-
+(*
 lemma (in subgroup) l_oneI [intro]:
   includes l_one G
   shows "l_one (G(| carrier := H |))"
   by rule simp_all
-
+*)
 lemma (in subgroup) group_axiomsI [intro]:
   includes group G
   shows "group_axioms (G(| carrier := H |))"
-  by rule (simp_all add: l_inv)
+  by rule (auto intro: l_inv r_inv simp add: Units_def)
 
 lemma (in subgroup) groupI [intro]:
   includes group G
   shows "group (G(| carrier := H |))"
-  using prems by fast
+  by (rule groupI) (auto intro: m_assoc l_inv)
 
 text {*
   Since @{term H} is nonempty, it contains some element @{term x}.  Since
@@ -223,8 +462,8 @@
 
 declare magma.m_closed [simp]
 
-declare l_one.one_closed [iff] group.inv_closed [simp]
-  l_one.l_one [simp] group.r_one [simp] group.inv_inv [simp]
+declare monoid.one_closed [iff] group.inv_closed [simp]
+  monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp]
 
 lemma subgroup_nonempty:
   "~ subgroup {} G"
@@ -241,6 +480,11 @@
   with subgroup_nonempty show ?thesis by contradiction
 qed
 
+(*
+lemma (in monoid) Units_subgroup:
+  "subgroup (Units G) G"
+*)
+
 subsection {* Direct Products *}
 
 constdefs
@@ -251,13 +495,13 @@
   "G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H,
     mult = (%(xg, xh) (yg, yh). (mult G xg yg, mult H xh yh)) |)"
 
-  DirProdMonoid ::
+  DirProdGroup ::
     "[('a, 'm) monoid_scheme, ('b, 'n) monoid_scheme] => ('a \<times> 'b) monoid"
-    (infixr "\<times>\<^sub>m" 80)
-  "G \<times>\<^sub>m H == (| carrier = carrier (G \<times>\<^sub>s H),
+    (infixr "\<times>\<^sub>g" 80)
+  "G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>s H),
     mult = mult (G \<times>\<^sub>s H),
     one = (one G, one H) |)"
-
+(*
   DirProdGroup ::
     "[('a, 'm) group_scheme, ('b, 'n) group_scheme] => ('a \<times> 'b) group"
     (infixr "\<times>\<^sub>g" 80)
@@ -265,6 +509,7 @@
     mult = mult (G \<times>\<^sub>m H),
     one = one (G \<times>\<^sub>m H),
     m_inv = (%(g, h). (m_inv G g, m_inv H h)) |)"
+*)
 
 lemma DirProdSemigroup_magma:
   includes magma G + magma H
@@ -287,13 +532,13 @@
   includes magma G + magma H
   shows "magma (G \<times>\<^sub>g H)"
   by rule
-    (auto simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def)
+    (auto simp add: DirProdGroup_def DirProdSemigroup_def)
 
 lemma DirProdGroup_semigroup_axioms:
   includes semigroup G + semigroup H
   shows "semigroup_axioms (G \<times>\<^sub>g H)"
   by rule
-    (auto simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def
+    (auto simp add: DirProdGroup_def DirProdSemigroup_def
       G.m_assoc H.m_assoc)
 
 lemma DirProdGroup_semigroup:
@@ -308,11 +553,9 @@
 lemma DirProdGroup_group:
   includes group G + group H
   shows "group (G \<times>\<^sub>g H)"
-by rule
-  (auto intro: magma.intro l_one.intro
-      semigroup_axioms.intro group_axioms.intro
-    simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def
-      G.m_assoc H.m_assoc G.l_inv H.l_inv)
+  by (rule groupI)
+    (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
+      simp add: DirProdGroup_def DirProdSemigroup_def)
 
 subsection {* Homomorphisms *}
 
@@ -376,14 +619,20 @@
   with x show ?thesis by simp
 qed
 
-section {* Abelian Structures *}
+section {* Commutative Structures *}
+
+text {*
+  Naming convention: multiplicative structures that are commutative
+  are called \emph{commutative}, additive structures are called
+  \emph{Abelian}.
+*}
 
 subsection {* Definition *}
 
-locale abelian_semigroup = semigroup +
+locale comm_semigroup = semigroup +
   assumes m_comm: "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
 
-lemma (in abelian_semigroup) m_lcomm:
+lemma (in comm_semigroup) m_lcomm:
   "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
 proof -
@@ -394,11 +643,33 @@
   finally show ?thesis .
 qed
 
-lemmas (in abelian_semigroup) ac = m_assoc m_comm m_lcomm
+lemmas (in comm_semigroup) m_ac = m_assoc m_comm m_lcomm
+
+locale comm_monoid = comm_semigroup + monoid
 
-locale abelian_monoid = abelian_semigroup + l_one
+lemma comm_monoidI:
+  assumes m_closed:
+      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
+    and one_closed: "one G \<in> carrier G"
+    and m_assoc:
+      "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
+      mult G (mult G x y) z = mult G x (mult G y z)"
+    and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
+    and m_comm:
+      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y = mult G y x"
+  shows "comm_monoid G"
+  using l_one
+  by (auto intro!: comm_monoid.intro magma.intro semigroup_axioms.intro
+    comm_semigroup_axioms.intro monoid_axioms.intro
+    intro: prems simp: m_closed one_closed m_comm)
 
-lemma (in abelian_monoid) l_one [simp]:
+lemma (in monoid) monoid_comm_monoidI:
+  assumes m_comm:
+      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y = mult G y x"
+  shows "comm_monoid G"
+  by (rule comm_monoidI) (auto intro: m_assoc m_comm)
+(*
+lemma (in comm_monoid) r_one [simp]:
   "x \<in> carrier G ==> x \<otimes> \<one> = x"
 proof -
   assume G: "x \<in> carrier G"
@@ -406,11 +677,38 @@
   also from G have "... = x" by simp
   finally show ?thesis .
 qed
+*)
 
-locale abelian_group = abelian_monoid + group
+lemma (in comm_monoid) nat_pow_distr:
+  "[| x \<in> carrier G; y \<in> carrier G |] ==>
+  (x \<otimes> y) (^) (n::nat) = x (^) n \<otimes> y (^) n"
+  by (induct n) (simp, simp add: m_ac)
+
+locale comm_group = comm_monoid + group
+
+lemma (in group) group_comm_groupI:
+  assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
+      mult G x y = mult G y x"
+  shows "comm_group G"
+  by (fast intro: comm_group.intro comm_semigroup_axioms.intro
+    group.axioms prems)
 
-lemma (in abelian_group) inv_mult:
+lemma comm_groupI:
+  assumes m_closed:
+      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
+    and one_closed: "one G \<in> carrier G"
+    and m_assoc:
+      "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
+      mult G (mult G x y) z = mult G x (mult G y z)"
+    and m_comm:
+      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y = mult G y x"
+    and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
+    and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G"
+  shows "comm_group G"
+  by (fast intro: group.group_comm_groupI groupI prems)
+
+lemma (in comm_group) inv_mult:
   "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
-  by (simp add: ac inv_mult_group)
+  by (simp add: m_ac inv_mult_group)
 
 end
diff -r 4822d9597d1e -r d3671b878828 src/HOL/Algebra/Module.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Module.thy	Wed Apr 30 10:01:35 2003 +0200
@@ -0,0 +1,161 @@
+(*  Title:      HOL/Algebra/Module
+    ID:         $Id$
+    Author:     Clemens Ballarin, started 15 April 2003
+    Copyright:  Clemens Ballarin
+*)
+
+theory Module = CRing:
+
+section {* Modules over an Abelian Group *}
+
+record ('a, 'b) module = "'b ring" +
+  smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
+
+locale module = cring R + abelian_group M +
+  assumes smult_closed [simp, intro]:
+      "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^sub>2 x \<in> carrier M"
+    and smult_l_distr:
+      "[| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
+      (a \<oplus> b) \<odot>\<^sub>2 x = a \<odot>\<^sub>2 x \<oplus>\<^sub>2 b \<odot>\<^sub>2 x"
+    and smult_r_distr:
+      "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
+      a \<odot>\<^sub>2 (x \<oplus>\<^sub>2 y) = a \<odot>\<^sub>2 x \<oplus>\<^sub>2 a \<odot>\<^sub>2 y"
+    and smult_assoc1:
+      "[| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
+      (a \<otimes> b) \<odot>\<^sub>2 x = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 x)"
+    and smult_one [simp]:
+      "x \<in> carrier M ==> \<one> \<odot>\<^sub>2 x = x"
+
+locale algebra = module R M + cring M +
+  assumes smult_assoc2:
+      "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
+      (a \<odot>\<^sub>2 x) \<otimes>\<^sub>2 y = a \<odot>\<^sub>2 (x \<otimes>\<^sub>2 y)"
+
+lemma moduleI:
+  assumes cring: "cring R"
+    and abelian_group: "abelian_group M"
+    and smult_closed:
+      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> smult M a x \<in> carrier M"
+    and smult_l_distr:
+      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
+      smult M (add R a b) x = add M (smult M a x) (smult M b x)"
+    and smult_r_distr:
+      "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
+      smult M a (add M x y) = add M (smult M a x) (smult M a y)"
+    and smult_assoc1:
+      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
+      smult M (mult R a b) x = smult M a (smult M b x)"
+    and smult_one:
+      "!!x. x \<in> carrier M ==> smult M (one R) x = x"
+  shows "module R M"
+  by (auto intro: module.intro cring.axioms abelian_group.axioms
+    module_axioms.intro prems)
+
+lemma algebraI:
+  assumes R_cring: "cring R"
+    and M_cring: "cring M"
+    and smult_closed:
+      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> smult M a x \<in> carrier M"
+    and smult_l_distr:
+      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
+      smult M (add R a b) x = add M (smult M a x) (smult M b x)"
+    and smult_r_distr:
+      "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
+      smult M a (add M x y) = add M (smult M a x) (smult M a y)"
+    and smult_assoc1:
+      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
+      smult M (mult R a b) x = smult M a (smult M b x)"
+    and smult_one:
+      "!!x. x \<in> carrier M ==> smult M (one R) x = x"
+    and smult_assoc2:
+      "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
+      mult M (smult M a x) y = smult M a (mult M x y)"
+  shows "algebra R M"
+  by (auto intro!: algebra.intro algebra_axioms.intro cring.axioms 
+    module_axioms.intro prems)
+
+lemma (in algebra) R_cring:
+  "cring R"
+  by (rule cring.intro) assumption+
+
+lemma (in algebra) M_cring:
+  "cring M"
+  by (rule cring.intro) assumption+
+
+lemma (in algebra) module:
+  "module R M"
+  by (auto intro: moduleI R_cring is_abelian_group
+    smult_l_distr smult_r_distr smult_assoc1)
+
+subsection {* Basic Properties of Algebras *}
+
+lemma (in algebra) smult_l_null [simp]:
+  "x \<in> carrier M ==> \<zero> \<odot>\<^sub>2 x = \<zero>\<^sub>2"
+proof -
+  assume M: "x \<in> carrier M"
+  note facts = M smult_closed
+  from facts have "\<zero> \<odot>\<^sub>2 x = (\<zero> \<odot>\<^sub>2 x \<oplus>\<^sub>2 \<zero> \<odot>\<^sub>2 x) \<oplus>\<^sub>2 \<ominus>\<^sub>2 (\<zero> \<odot>\<^sub>2 x)" by algebra
+  also from M have "... = (\<zero> \<oplus> \<zero>) \<odot>\<^sub>2 x \<oplus>\<^sub>2 \<ominus>\<^sub>2 (\<zero> \<odot>\<^sub>2 x)"
+    by (simp add: smult_l_distr del: R.l_zero R.r_zero)
+  also from facts have "... = \<zero>\<^sub>2" by algebra
+  finally show ?thesis .
+qed
+
+lemma (in algebra) smult_r_null [simp]:
+  "a \<in> carrier R ==> a \<odot>\<^sub>2 \<zero>\<^sub>2 = \<zero>\<^sub>2";
+proof -
+  assume R: "a \<in> carrier R"
+  note facts = R smult_closed
+  from facts have "a \<odot>\<^sub>2 \<zero>\<^sub>2 = (a \<odot>\<^sub>2 \<zero>\<^sub>2 \<oplus>\<^sub>2 a \<odot>\<^sub>2 \<zero>\<^sub>2) \<oplus>\<^sub>2 \<ominus>\<^sub>2 (a \<odot>\<^sub>2 \<zero>\<^sub>2)"
+    by algebra
+  also from R have "... = a \<odot>\<^sub>2 (\<zero>\<^sub>2 \<oplus>\<^sub>2 \<zero>\<^sub>2) \<oplus>\<^sub>2 \<ominus>\<^sub>2 (a \<odot>\<^sub>2 \<zero>\<^sub>2)"
+    by (simp add: smult_r_distr del: M.l_zero M.r_zero)
+  also from facts have "... = \<zero>\<^sub>2" by algebra
+  finally show ?thesis .
+qed
+
+lemma (in algebra) smult_l_minus:
+  "[| a \<in> carrier R; x \<in> carrier M |] ==> (\<ominus>a) \<odot>\<^sub>2 x = \<ominus>\<^sub>2 (a \<odot>\<^sub>2 x)"
+proof -
+  assume RM: "a \<in> carrier R" "x \<in> carrier M"
+  note facts = RM smult_closed
+  from facts have "(\<ominus>a) \<odot>\<^sub>2 x = (\<ominus>a \<odot>\<^sub>2 x \<oplus>\<^sub>2 a \<odot>\<^sub>2 x) \<oplus>\<^sub>2 \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)" by algebra
+  also from RM have "... = (\<ominus>a \<oplus> a) \<odot>\<^sub>2 x \<oplus>\<^sub>2 \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)"
+    by (simp add: smult_l_distr)
+  also from facts smult_l_null have "... = \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)" by algebra
+  finally show ?thesis .
+qed
+
+lemma (in algebra) smult_r_minus:
+  "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^sub>2 (\<ominus>\<^sub>2x) = \<ominus>\<^sub>2 (a \<odot>\<^sub>2 x)"
+proof -
+  assume RM: "a \<in> carrier R" "x \<in> carrier M"
+  note facts = RM smult_closed
+  from facts have "a \<odot>\<^sub>2 (\<ominus>\<^sub>2x) = (a \<odot>\<^sub>2 \<ominus>\<^sub>2x \<oplus>\<^sub>2 a \<odot>\<^sub>2 x) \<oplus>\<^sub>2 \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)"
+    by algebra
+  also from RM have "... = a \<odot>\<^sub>2 (\<ominus>\<^sub>2x \<oplus>\<^sub>2 x) \<oplus>\<^sub>2 \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)"
+    by (simp add: smult_r_distr)
+  also from facts smult_r_null have "... = \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)" by algebra
+  finally show ?thesis .
+qed
+
+subsection {* Every Abelian Group is a $\mathbb{Z}$-module *}
+
+text {* Not finished. *}
+
+constdefs
+  INTEG :: "int ring"
+  "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
+
+(*
+  INTEG_MODULE :: "('a, 'm) ring_scheme => (int, 'a) module"
+  "INTEG_MODULE R == (| carrier = carrier R, mult = mult R, one = one R,
+    zero = zero R, add = add R, smult = (%n. %x:carrier R. ... ) |)"
+*)
+
+lemma cring_INTEG:
+  "cring INTEG"
+  by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
+    zadd_zminus_inverse2 zadd_zmult_distrib)
+
+end
diff -r 4822d9597d1e -r d3671b878828 src/HOL/Algebra/ROOT.ML
--- a/src/HOL/Algebra/ROOT.ML	Tue Apr 29 12:36:49 2003 +0200
+++ b/src/HOL/Algebra/ROOT.ML	Wed Apr 30 10:01:35 2003 +0200
@@ -1,9 +1,16 @@
 (*
-    Polynomials
+    The Isabelle Algebraic Library
     $Id$
     Author: Clemens Ballarin, started 24 September 1999
 *)
 
+(* New development, based on explicit structures *)
+
+use_thy "Sylow";		(* Groups *)
+(* use_thy "UnivPoly"; *)	(* Rings and polynomials *)
+
+(* Old development, based on axiomatic type classes.
+   Will be withdrawn in future. *)
+
 with_path "abstract" time_use_thy "Abstract";        (*The ring theory*)
 with_path "poly"     time_use_thy "Polynomial";      (*The full theory*)
-use_thy "Sylow";
diff -r 4822d9597d1e -r d3671b878828 src/HOL/Algebra/Summation.thy
--- a/src/HOL/Algebra/Summation.thy	Tue Apr 29 12:36:49 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,500 +0,0 @@
-(*  Title:      Summation Operator for Abelian Groups
-    ID:         $Id$
-    Author:     Clemens Ballarin, started 19 November 2002
-
-This file is largely based on HOL/Finite_Set.thy.
-*)
-
-header {* Summation Operator *}
-
-theory Summation = Group:
-
-(* Instantiation of LC from Finite_Set.thy is not possible,
-   because here we have explicit typing rules like x : carrier G.
-   We introduce an explicit argument for the domain D *)
-
-consts
-  foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set"
-
-inductive "foldSetD D f e"
-  intros
-    emptyI [intro]: "e : D ==> ({}, e) : foldSetD D f e"
-    insertI [intro]: "[| x ~: A; f x y : D; (A, y) : foldSetD D f e |] ==>
-                      (insert x A, f x y) : foldSetD D f e"
-
-inductive_cases empty_foldSetDE [elim!]: "({}, x) : foldSetD D f e"
-
-constdefs
-  foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a"
-  "foldD D f e A == THE x. (A, x) : foldSetD D f e"
-
-lemma foldSetD_closed:
-  "[| (A, z) : foldSetD D f e ; e : D; !!x y. [| x : A; y : D |] ==> f x y : D 
-      |] ==> z : D";
-  by (erule foldSetD.elims) auto
-
-lemma Diff1_foldSetD:
-  "[| (A - {x}, y) : foldSetD D f e; x : A; f x y : D |] ==>
-   (A, f x y) : foldSetD D f e"
-  apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
-   apply auto
-  done
-
-lemma foldSetD_imp_finite [simp]: "(A, x) : foldSetD D f e ==> finite A"
-  by (induct set: foldSetD) auto
-
-lemma finite_imp_foldSetD:
-  "[| finite A; e : D; !!x y. [| x : A; y : D |] ==> f x y : D |] ==>
-   EX x. (A, x) : foldSetD D f e"
-proof (induct set: Finites)
-  case empty then show ?case by auto
-next
-  case (insert F x)
-  then obtain y where y: "(F, y) : foldSetD D f e" by auto
-  with insert have "y : D" by (auto dest: foldSetD_closed)
-  with y and insert have "(insert x F, f x y) : foldSetD D f e"
-    by (intro foldSetD.intros) auto
-  then show ?case ..
-qed
-
-subsection {* Left-commutative operations *}
-
-locale LCD =
-  fixes B :: "'b set"
-  and D :: "'a set"
-  and f :: "'b => 'a => 'a"    (infixl "\<cdot>" 70)
-  assumes left_commute: "[| x : B; y : B; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
-  and f_closed [simp, intro!]: "!!x y. [| x : B; y : D |] ==> f x y : D"
-
-lemma (in LCD) foldSetD_closed [dest]:
-  "(A, z) : foldSetD D f e ==> z : D";
-  by (erule foldSetD.elims) auto
-
-lemma (in LCD) Diff1_foldSetD:
-  "[| (A - {x}, y) : foldSetD D f e; x : A; A <= B |] ==>
-   (A, f x y) : foldSetD D f e"
-  apply (subgoal_tac "x : B")
-  prefer 2 apply fast
-  apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
-   apply auto
-  done
-
-lemma (in LCD) foldSetD_imp_finite [simp]:
-  "(A, x) : foldSetD D f e ==> finite A"
-  by (induct set: foldSetD) auto
-
-lemma (in LCD) finite_imp_foldSetD:
-  "[| finite A; A <= B; e : D |] ==> EX x. (A, x) : foldSetD D f e"
-proof (induct set: Finites)
-  case empty then show ?case by auto
-next
-  case (insert F x)
-  then obtain y where y: "(F, y) : foldSetD D f e" by auto
-  with insert have "y : D" by auto
-  with y and insert have "(insert x F, f x y) : foldSetD D f e"
-    by (intro foldSetD.intros) auto
-  then show ?case ..
-qed
-
-lemma (in LCD) foldSetD_determ_aux:
-  "e : D ==> ALL A x. A <= B & card A < n --> (A, x) : foldSetD D f e -->
-    (ALL y. (A, y) : foldSetD D f e --> y = x)"
-  apply (induct n)
-   apply (auto simp add: less_Suc_eq)
-  apply (erule foldSetD.cases)
-   apply blast
-  apply (erule foldSetD.cases)
-   apply blast
-  apply clarify
-  txt {* force simplification of @{text "card A < card (insert ...)"}. *}
-  apply (erule rev_mp)
-  apply (simp add: less_Suc_eq_le)
-  apply (rule impI)
-  apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb")
-   apply (subgoal_tac "Aa = Ab")
-    prefer 2 apply (blast elim!: equalityE)
-   apply blast
-  txt {* case @{prop "xa \<notin> xb"}. *}
-  apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab")
-   prefer 2 apply (blast elim!: equalityE)
-  apply clarify
-  apply (subgoal_tac "Aa = insert xb Ab - {xa}")
-   prefer 2 apply blast
-  apply (subgoal_tac "card Aa <= card Ab")
-   prefer 2
-   apply (rule Suc_le_mono [THEN subst])
-   apply (simp add: card_Suc_Diff1)
-  apply (rule_tac A1 = "Aa - {xb}" in finite_imp_foldSetD [THEN exE])
-  apply (blast intro: foldSetD_imp_finite finite_Diff)
-(* new subgoal from finite_imp_foldSetD *)
-    apply best (* blast doesn't seem to solve this *)
-   apply assumption
-  apply (frule (1) Diff1_foldSetD)
-(* new subgoal from Diff1_foldSetD *)
-    apply best
-(*
-apply (best del: foldSetD_closed elim: foldSetD_closed)
-    apply (rule f_closed) apply assumption apply (rule foldSetD_closed)
-    prefer 3 apply assumption apply (rule e_closed)
-    apply (rule f_closed) apply force apply assumption
-*)
-  apply (subgoal_tac "ya = f xb x")
-   prefer 2
-(* new subgoal to make IH applicable *) 
-  apply (subgoal_tac "Aa <= B")
-   prefer 2 apply best
-   apply (blast del: equalityCE)
-  apply (subgoal_tac "(Ab - {xa}, x) : foldSetD D f e")
-   prefer 2 apply simp
-  apply (subgoal_tac "yb = f xa x")
-   prefer 2 
-(*   apply (drule_tac x = xa in Diff1_foldSetD)
-     apply assumption
-     apply (rule f_closed) apply best apply (rule foldSetD_closed)
-     prefer 3 apply assumption apply (rule e_closed)
-     apply (rule f_closed) apply best apply assumption
-*)
-   apply (blast del: equalityCE dest: Diff1_foldSetD)
-   apply (simp (no_asm_simp))
-   apply (rule left_commute)
-   apply assumption apply best apply best
- done
-
-lemma (in LCD) foldSetD_determ:
-  "[| (A, x) : foldSetD D f e; (A, y) : foldSetD D f e; e : D; A <= B |]
-   ==> y = x"
-  by (blast intro: foldSetD_determ_aux [rule_format])
-
-lemma (in LCD) foldD_equality:
-  "[| (A, y) : foldSetD D f e; e : D; A <= B |] ==> foldD D f e A = y"
-  by (unfold foldD_def) (blast intro: foldSetD_determ)
-
-lemma foldD_empty [simp]:
-  "e : D ==> foldD D f e {} = e"
-  by (unfold foldD_def) blast
-
-lemma (in LCD) foldD_insert_aux:
-  "[| x ~: A; x : B; e : D; A <= B |] ==>
-    ((insert x A, v) : foldSetD D f e) =
-    (EX y. (A, y) : foldSetD D f e & v = f x y)"
-  apply auto
-  apply (rule_tac A1 = A in finite_imp_foldSetD [THEN exE])
-   apply (fastsimp dest: foldSetD_imp_finite)
-(* new subgoal by finite_imp_foldSetD *)
-    apply assumption
-    apply assumption
-  apply (blast intro: foldSetD_determ)
-  done
-
-lemma (in LCD) foldD_insert:
-    "[| finite A; x ~: A; x : B; e : D; A <= B |] ==>
-     foldD D f e (insert x A) = f x (foldD D f e A)"
-  apply (unfold foldD_def)
-  apply (simp add: foldD_insert_aux)
-  apply (rule the_equality)
-  apply (auto intro: finite_imp_foldSetD
-    cong add: conj_cong simp add: foldD_def [symmetric] foldD_equality)
-  done
-
-lemma (in LCD) foldD_closed [simp]:
-  "[| finite A; e : D; A <= B |] ==> foldD D f e A : D"
-proof (induct set: Finites)
-  case empty then show ?case by (simp add: foldD_empty)
-next
-  case insert then show ?case by (simp add: foldD_insert)
-qed
-
-lemma (in LCD) foldD_commute:
-  "[| finite A; x : B; e : D; A <= B |] ==>
-   f x (foldD D f e A) = foldD D f (f x e) A"
-  apply (induct set: Finites)
-   apply simp
-  apply (auto simp add: left_commute foldD_insert)
-  done
-
-lemma Int_mono2:
-  "[| A <= C; B <= C |] ==> A Int B <= C"
-  by blast
-
-lemma (in LCD) foldD_nest_Un_Int:
-  "[| finite A; finite C; e : D; A <= B; C <= B |] ==>
-   foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)"
-  apply (induct set: Finites)
-   apply simp
-  apply (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb
-    Int_mono2 Un_subset_iff)
-  done
-
-lemma (in LCD) foldD_nest_Un_disjoint:
-  "[| finite A; finite B; A Int B = {}; e : D; A <= B; C <= B |]
-    ==> foldD D f e (A Un B) = foldD D f (foldD D f e B) A"
-  by (simp add: foldD_nest_Un_Int)
-
--- {* Delete rules to do with @{text foldSetD} relation. *}
-
-declare foldSetD_imp_finite [simp del]
-  empty_foldSetDE [rule del]
-  foldSetD.intros [rule del]
-declare (in LCD)
-  foldSetD_closed [rule del]
-
-subsection {* Commutative monoids *}
-
-text {*
-  We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
-  instead of @{text "'b => 'a => 'a"}.
-*}
-
-locale ACeD =
-  fixes D :: "'a set"
-    and f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
-    and e :: 'a
-  assumes ident [simp]: "x : D ==> x \<cdot> e = x"
-    and commute: "[| x : D; y : D |] ==> x \<cdot> y = y \<cdot> x"
-    and assoc: "[| x : D; y : D; z : D |] ==> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
-    and e_closed [simp]: "e : D"
-    and f_closed [simp]: "[| x : D; y : D |] ==> x \<cdot> y : D"
-
-lemma (in ACeD) left_commute:
-  "[| x : D; y : D; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
-proof -
-  assume D: "x : D" "y : D" "z : D"
-  then have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp add: commute)
-  also from D have "... = y \<cdot> (z \<cdot> x)" by (simp add: assoc)
-  also from D have "z \<cdot> x = x \<cdot> z" by (simp add: commute)
-  finally show ?thesis .
-qed
-
-lemmas (in ACeD) AC = assoc commute left_commute
-
-lemma (in ACeD) left_ident [simp]: "x : D ==> e \<cdot> x = x"
-proof -
-  assume D: "x : D"
-  have "x \<cdot> e = x" by (rule ident)
-  with D show ?thesis by (simp add: commute)
-qed
-
-lemma (in ACeD) foldD_Un_Int:
-  "[| finite A; finite B; A <= D; B <= D |] ==>
-    foldD D f e A \<cdot> foldD D f e B =
-    foldD D f e (A Un B) \<cdot> foldD D f e (A Int B)"
-  apply (induct set: Finites)
-   apply (simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]])
-(* left_commute is required to show premise of LCD.intro *)
-  apply (simp add: AC insert_absorb Int_insert_left
-    LCD.foldD_insert [OF LCD.intro [of D]]
-    LCD.foldD_closed [OF LCD.intro [of D]]
-    Int_mono2 Un_subset_iff)
-  done
-
-lemma (in ACeD) foldD_Un_disjoint:
-  "[| finite A; finite B; A Int B = {}; A <= D; B <= D |] ==>
-    foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B"
-  by (simp add: foldD_Un_Int
-    left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff)
-
-subsection {* Products over Finite Sets *}
-
-constdefs
-  finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
-  "finprod G f A == if finite A
-      then foldD (carrier G) (mult G o f) (one G) A
-      else arbitrary"
-
-(*
-locale finite_prod = abelian_monoid + var prod +
-  defines "prod == (%f A. if finite A
-      then foldD (carrier G) (op \<otimes> o f) \<one> A
-      else arbitrary)"
-*)
-(* TODO: nice syntax for the summation operator inside the locale
-   like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *)
-
-ML_setup {* 
-
-Context.>> (fn thy => (simpset_ref_of thy :=
-  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
-
-lemma (in abelian_monoid) finprod_empty [simp]: 
-  "finprod G f {} = \<one>"
-  by (simp add: finprod_def)
-
-ML_setup {* 
-
-Context.>> (fn thy => (simpset_ref_of thy :=
-  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
-
-declare funcsetI [intro]
-  funcset_mem [dest]
-
-lemma (in abelian_monoid) finprod_insert [simp]:
-  "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |] ==>
-   finprod G f (insert a F) = f a \<otimes> finprod G f F"
-  apply (rule trans)
-  apply (simp add: finprod_def)
-  apply (rule trans)
-  apply (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]])
-    apply simp
-    apply (rule m_lcomm)
-      apply fast apply fast apply assumption
-    apply (fastsimp intro: m_closed)
-    apply simp+ apply fast
-  apply (auto simp add: finprod_def)
-  done
-
-lemma (in abelian_monoid) finprod_one:
-  "finite A ==> finprod G (%i. \<one>) A = \<one>"
-proof (induct set: Finites)
-  case empty show ?case by simp
-next
-  case (insert A a)
-  have "(%i. \<one>) \<in> A -> carrier G" by auto
-  with insert show ?case by simp
-qed
-
-lemma (in abelian_monoid) finprod_closed [simp]:
-  fixes A
-  assumes fin: "finite A" and f: "f \<in> A -> carrier G" 
-  shows "finprod G f A \<in> carrier G"
-using fin f
-proof induct
-  case empty show ?case by simp
-next
-  case (insert A a)
-  then have a: "f a \<in> carrier G" by fast
-  from insert have A: "f \<in> A -> carrier G" by fast
-  from insert A a show ?case by simp
-qed
-
-lemma funcset_Int_left [simp, intro]:
-  "[| f \<in> A -> C; f \<in> B -> C |] ==> f \<in> A Int B -> C"
-  by fast
-
-lemma funcset_Un_left [iff]:
-  "(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)"
-  by fast
-
-lemma (in abelian_monoid) finprod_Un_Int:
-  "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
-     finprod G g (A Un B) \<otimes> finprod G g (A Int B) =
-     finprod G g A \<otimes> finprod G g B"
-  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
-proof (induct set: Finites)
-  case empty then show ?case by (simp add: finprod_closed)
-next
-  case (insert A a)
-  then have a: "g a \<in> carrier G" by fast
-  from insert have A: "g \<in> A -> carrier G" by fast
-  from insert A a show ?case
-    by (simp add: ac Int_insert_left insert_absorb finprod_closed
-          Int_mono2 Un_subset_iff) 
-qed
-
-lemma (in abelian_monoid) finprod_Un_disjoint:
-  "[| finite A; finite B; A Int B = {};
-      g \<in> A -> carrier G; g \<in> B -> carrier G |]
-   ==> finprod G g (A Un B) = finprod G g A \<otimes> finprod G g B"
-  apply (subst finprod_Un_Int [symmetric])
-    apply (auto simp add: finprod_closed)
-  done
-
-lemma (in abelian_monoid) finprod_multf:
-  "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
-   finprod G (%x. f x \<otimes> g x) A = (finprod G f A \<otimes> finprod G g A)"
-proof (induct set: Finites)
-  case empty show ?case by simp
-next
-  case (insert A a) then
-  have fA: "f : A -> carrier G" by fast
-  from insert have fa: "f a : carrier G" by fast
-  from insert have gA: "g : A -> carrier G" by fast
-  from insert have ga: "g a : carrier G" by fast
-  from insert have fga: "(%x. f x \<otimes> g x) a : carrier G" by (simp add: Pi_def)
-  from insert have fgA: "(%x. f x \<otimes> g x) : A -> carrier G"
-    by (simp add: Pi_def)
-  show ?case  (* check if all simps are really necessary *)
-    by (simp add: insert fA fa gA ga fgA fga ac finprod_closed Int_insert_left insert_absorb Int_mono2 Un_subset_iff)
-qed
-
-lemma (in abelian_monoid) finprod_cong':
-  "[| A = B; g : B -> carrier G;
-      !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B"
-proof -
-  assume prems: "A = B" "g : B -> carrier G"
-    "!!i. i : B ==> f i = g i"
-  show ?thesis
-  proof (cases "finite B")
-    case True
-    then have "!!A. [| A = B; g : B -> carrier G;
-      !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B"
-    proof induct
-      case empty thus ?case by simp
-    next
-      case (insert B x)
-      then have "finprod G f A = finprod G f (insert x B)" by simp
-      also from insert have "... = f x \<otimes> finprod G f B"
-      proof (intro finprod_insert)
-	show "finite B" .
-      next
-	show "x ~: B" .
-      next
-	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
-	  "g \<in> insert x B \<rightarrow> carrier G"
-	thus "f : B -> carrier G" by fastsimp
-      next
-	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
-	  "g \<in> insert x B \<rightarrow> carrier G"
-	thus "f x \<in> carrier G" by fastsimp
-      qed
-      also from insert have "... = g x \<otimes> finprod G g B" by fastsimp
-      also from insert have "... = finprod G g (insert x B)"
-      by (intro finprod_insert [THEN sym]) auto
-      finally show ?case .
-    qed
-    with prems show ?thesis by simp
-  next
-    case False with prems show ?thesis by (simp add: finprod_def)
-  qed
-qed
-
-lemma (in abelian_monoid) finprod_cong:
-  "[| A = B; !!i. i : B ==> f i = g i;
-      g : B -> carrier G = True |] ==> finprod G f A = finprod G g B"
-  by (rule finprod_cong') fast+
-
-text {*Usually, if this rule causes a failed congruence proof error,
-  the reason is that the premise @{text "g : B -> carrier G"} cannot be shown.
-  Adding @{thm [source] Pi_def} to the simpset is often useful.
-  For this reason, @{thm [source] abelian_monoid.finprod_cong}
-  is not added to the simpset by default.
-*}
-
-declare funcsetI [rule del]
-  funcset_mem [rule del]
-
-lemma (in abelian_monoid) finprod_0 [simp]:
-  "f : {0::nat} -> carrier G ==> finprod G f {..0} = f 0"
-by (simp add: Pi_def)
-
-lemma (in abelian_monoid) finprod_Suc [simp]:
-  "f : {..Suc n} -> carrier G ==>
-   finprod G f {..Suc n} = (f (Suc n) \<otimes> finprod G f {..n})"
-by (simp add: Pi_def atMost_Suc)
-
-lemma (in abelian_monoid) finprod_Suc2:
-  "f : {..Suc n} -> carrier G ==>
-   finprod G f {..Suc n} = (finprod G (%i. f (Suc i)) {..n} \<otimes> f 0)"
-proof (induct n)
-  case 0 thus ?case by (simp add: Pi_def)
-next
-  case Suc thus ?case by (simp add: m_assoc Pi_def finprod_closed)
-qed
-
-lemma (in abelian_monoid) finprod_mult [simp]:
-  "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==>
-     finprod G (%i. f i \<otimes> g i) {..n::nat} =
-     finprod G f {..n} \<otimes> finprod G g {..n}"
-  by (induct n) (simp_all add: ac Pi_def finprod_closed)
-
-end
-
diff -r 4822d9597d1e -r d3671b878828 src/HOL/Algebra/poly/PolyHomo.thy
--- a/src/HOL/Algebra/poly/PolyHomo.thy	Tue Apr 29 12:36:49 2003 +0200
+++ b/src/HOL/Algebra/poly/PolyHomo.thy	Wed Apr 30 10:01:35 2003 +0200
@@ -4,7 +4,7 @@
     Author: Clemens Ballarin, started 15 April 1997
 *)
 
-PolyHomo = UnivPoly +
+PolyHomo = UnivPoly2 +
 
 consts
   EVAL2	:: "['a::ring => 'b, 'b, 'a up] => 'b::ring"
diff -r 4822d9597d1e -r d3671b878828 src/HOL/Algebra/poly/UnivPoly.ML
--- a/src/HOL/Algebra/poly/UnivPoly.ML	Tue Apr 29 12:36:49 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,359 +0,0 @@
-(*
-    Degree of polynomials
-    $Id$
-    written by Clemens Ballarin, started 22 January 1997
-*)
-
-(*
-(* Relating degree and bound *)
-
-Goal "[| bound m f; f n ~= 0 |] ==> n <= m";
-by (force_tac (claset() addDs [inst "m" "n" boundD], 
-               simpset()) 1); 
-qed "below_bound";
-
-goal UnivPoly.thy "bound (LEAST n. bound n (Rep_UP p)) (Rep_UP p)";
-by (rtac exE 1);
-by (rtac LeastI 2);
-by (assume_tac 2);
-by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
-by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
-qed "Least_is_bound";
-
-Goalw [coeff_def, deg_def]
-  "!! p. ALL m. n < m --> coeff m p = 0 ==> deg p <= n";
-by (rtac Least_le 1);
-by (Fast_tac 1);
-qed "deg_aboveI";
-
-Goalw [coeff_def, deg_def]
-  "(n ~= 0 --> coeff n p ~= 0) ==> n <= deg p";
-by (case_tac "n = 0" 1);
-(* Case n=0 *)
-by (Asm_simp_tac 1);
-(* Case n~=0 *)
-by (rotate_tac 1 1);
-by (Asm_full_simp_tac 1);
-by (rtac below_bound 1);
-by (assume_tac 2);
-by (rtac Least_is_bound 1);
-qed "deg_belowI";
-
-Goalw [coeff_def, deg_def]
-  "deg p < m ==> coeff m p = 0";
-by (rtac exE 1); (* create !! x. *)
-by (rtac boundD 2);
-by (assume_tac 3);
-by (rtac LeastI 2);
-by (assume_tac 2);
-by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
-by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
-qed "deg_aboveD";
-
-Goalw [deg_def]
-  "deg p = Suc y ==> ~ bound y (Rep_UP p)";
-by (rtac not_less_Least 1);
-by (Asm_simp_tac 1);
-val lemma1 = result();
-
-Goalw [deg_def, coeff_def]
-  "deg p = Suc y ==> coeff (deg p) p ~= 0";
-by (rtac ccontr 1);
-by (dtac notnotD 1);
-by (cut_inst_tac [("p", "p")] Least_is_bound 1);
-by (subgoal_tac "bound y (Rep_UP p)" 1);
-(* prove subgoal *)
-by (rtac boundI 2);  
-by (case_tac "Suc y < m" 2);
-(* first case *)
-by (rtac boundD 2);  
-by (assume_tac 2);
-by (Asm_simp_tac 2);
-(* second case *)
-by (dtac leI 2);
-by (dtac Suc_leI 2);
-by (dtac le_anti_sym 2);
-by (assume_tac 2);
-by (Asm_full_simp_tac 2);
-(* end prove subgoal *)
-by (fold_goals_tac [deg_def]);
-by (dtac lemma1 1);
-by (etac notE 1);
-by (assume_tac 1);
-val lemma2 = result();
-
-Goal "deg p ~= 0 ==> coeff (deg p) p ~= 0";
-by (rtac lemma2 1);
-by (Full_simp_tac 1);
-by (dtac Suc_pred 1);
-by (rtac sym 1);
-by (Asm_simp_tac 1);
-qed "deg_lcoeff";
-
-Goal "p ~= 0 ==> coeff (deg p) p ~= 0";
-by (etac contrapos_np 1); 
-by (case_tac "deg p = 0" 1);
-by (blast_tac (claset() addSDs [deg_lcoeff]) 2); 
-by (rtac up_eqI 1);
-by (case_tac "n=0" 1);
-by (rotate_tac ~2 1);
-by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [deg_aboveD]) 1);
-qed "nonzero_lcoeff";
-
-Goal "(deg p <= n) = bound n (Rep_UP p)";
-by (rtac iffI 1);
-(* ==> *)
-by (rtac boundI 1);
-by (fold_goals_tac [coeff_def]);
-by (rtac deg_aboveD 1);
-by (fast_arith_tac 1);
-(* <== *)
-by (rtac deg_aboveI 1);
-by (rewtac coeff_def);
-by (Fast_tac 1);
-qed "deg_above_is_bound";
-
-(* Lemmas on the degree function *)
-
-Goalw [max_def]
-  "!! p::'a::ring up. deg (p + q) <= max (deg p) (deg q)";
-by (case_tac "deg p <= deg q" 1);
-(* case deg p <= deg q *)
-by (rtac deg_aboveI 1);
-by (Asm_simp_tac 1);
-by (strip_tac 1);
-by (dtac le_less_trans 1);
-by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
-(* case deg p > deg q *)
-by (rtac deg_aboveI 1);
-by (Asm_simp_tac 1);
-by (dtac not_leE 1);
-by (strip_tac 1);
-by (dtac less_trans 1);
-by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
-qed "deg_add";
-
-Goal "!!p::('a::ring up). deg p < deg q ==> deg (p + q) = deg q";
-by (rtac order_antisym 1);
-by (rtac le_trans 1);
-by (rtac deg_add 1);
-by (Asm_simp_tac 1);
-by (rtac deg_belowI 1);
-by (asm_simp_tac (simpset() addsimps [deg_aboveD, deg_lcoeff]) 1);
-qed "deg_add_equal";
-
-Goal "deg (monom m::'a::ring up) <= m";
-by (asm_simp_tac 
-  (simpset() addsimps [deg_aboveI, less_not_refl2 RS not_sym]) 1);
-qed "deg_monom_ring";
-
-Goal "deg (monom m::'a::domain up) = m";
-by (rtac le_anti_sym 1);
-(* <= *)
-by (rtac deg_monom_ring 1);
-(* >= *)
-by (asm_simp_tac 
-  (simpset() addsimps [deg_belowI, less_not_refl2 RS not_sym]) 1);
-qed "deg_monom";
-
-Goal "!! a::'a::ring. deg (const a) = 0";
-by (rtac le_anti_sym 1);
-by (rtac deg_aboveI 1);
-by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
-by (rtac deg_belowI 1);
-by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
-qed "deg_const";
-
-Goal "deg (0::'a::ringS up) = 0";
-by (rtac le_anti_sym 1);
-by (rtac deg_aboveI 1);
-by (Simp_tac 1);
-by (rtac deg_belowI 1);
-by (Simp_tac 1);
-qed "deg_zero";
-
-Goal "deg (<1>::'a::ring up) = 0";
-by (rtac le_anti_sym 1);
-by (rtac deg_aboveI 1);
-by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
-by (rtac deg_belowI 1);
-by (Simp_tac 1);
-qed "deg_one";
-
-Goal "!!p::('a::ring) up. deg (-p) = deg p";
-by (rtac le_anti_sym 1);
-(* <= *)
-by (simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1);
-by (simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff, uminus_monom_neq]) 1);
-qed "deg_uminus";
-
-Addsimps [deg_monom, deg_const, deg_zero, deg_one, deg_uminus];
-
-Goal
-  "!! a::'a::ring. deg (a *s p) <= (if a = 0 then 0 else deg p)";
-by (case_tac "a = 0" 1);
-by (REPEAT (asm_simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1));
-qed "deg_smult_ring";
-
-Goal
-  "!! a::'a::domain. deg (a *s p) = (if a = 0 then 0 else deg p)";
-by (rtac le_anti_sym 1);
-by (rtac deg_smult_ring 1);
-by (case_tac "a = 0" 1);
-by (REPEAT (asm_simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff]) 1));
-qed "deg_smult";
-
-Goal
-  "!! p::'a::ring up. [| deg p + deg q < k |] ==> \
-\       coeff i p * coeff (k - i) q = 0";
-by (simp_tac (simpset() addsimps [coeff_def]) 1);
-by (rtac bound_mult_zero 1);
-by (assume_tac 3);
-by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
-by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
-qed "deg_above_mult_zero";
-
-Goal
-  "!! p::'a::ring up. deg (p * q) <= deg p + deg q";
-by (rtac deg_aboveI 1);
-by (asm_simp_tac (simpset() addsimps [deg_above_mult_zero]) 1);
-qed "deg_mult_ring";
-
-goal Main.thy 
-  "!!k::nat. k < n ==> m < n + m - k";
-by (arith_tac 1);
-qed "less_add_diff";
-
-Goal "!!p. coeff n p ~= 0 ==> n <= deg p";
-(* More general than deg_belowI, and simplifies the next proof! *)
-by (rtac deg_belowI 1);
-by (Fast_tac 1);
-qed "deg_below2I";
-
-Goal
-  "!! p::'a::domain up. \
-\    [| p ~= 0; q ~= 0 |] ==> deg (p * q) = deg p + deg q";
-by (rtac le_anti_sym 1);
-by (rtac deg_mult_ring 1);
-(* deg p + deg q <= deg (p * q) *)
-by (rtac deg_below2I 1);
-by (Simp_tac 1);
-(*
-by (rtac conjI 1);
-by (rtac impI 1);
-*)
-by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
-by (rtac le_add1 1);
-by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
-by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
-by (rtac le_refl 1);
-by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
-by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
-(*
-by (rtac impI 1);
-by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
-by (rtac le_add1 1);
-by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
-by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
-by (rtac le_refl 1);
-by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
-by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
-*)
-qed "deg_mult";
-
-Addsimps [deg_smult, deg_mult];
-
-(* Representation theorems about polynomials *)
-
-goal PolyRing.thy
-  "!! p::nat=>'a::ring up. \
-\    coeff k (setsum p {..n}) = setsum (%i. coeff k (p i)) {..n}";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "coeff_SUM";
-
-goal UnivPoly.thy
-  "!! f::(nat=>'a::ring). \
-\    bound n f ==> setsum (%i. if i = x then f i else 0) {..n} = f x";
-by (simp_tac (simpset() addsimps [SUM_if_singleton]) 1);
-by (auto_tac
-    (claset() addDs [not_leE],
-     simpset()));
-qed "bound_SUM_if";
-
-Goal
-  "!! p::'a::ring up. deg p <= n ==> \
-\  setsum (%i. coeff i p *s monom i) {..n} = p";
-by (rtac up_eqI 1);
-by (simp_tac (simpset() addsimps [coeff_SUM]) 1);
-by (rtac trans 1);
-by (res_inst_tac [("x", "na")] bound_SUM_if 2);
-by (full_simp_tac (simpset() addsimps [deg_above_is_bound, coeff_def]) 2);
-by (rtac SUM_cong 1);
-by (rtac refl 1);
-by (Asm_simp_tac 1);
-qed "up_repr";
-
-Goal
-  "!! p::'a::ring up. [| deg p <= n; P p |] ==> \
-\  P (setsum (%i. coeff i p *s monom i) {..n})";
-by (asm_simp_tac (simpset() addsimps [up_repr]) 1);
-qed "up_reprD";
-
-Goal
-  "!! p::'a::ring up. \
-\  [| deg p <= n; P (setsum (%i. coeff i p *s monom i) {..n}) |] \
-\    ==> P p";
-by (asm_full_simp_tac (simpset() addsimps [up_repr]) 1);
-qed "up_repr2D";
-
-(*
-Goal
-  "!! p::'a::ring up. [| deg p <= n; deg q <= m |] ==> \
-\    (SUM n (%i. coeff i p *s monom i) = SUM m (%i. coeff i q *s monom i)) \
-\    = (coeff k f = coeff k g)
-...
-qed "up_unique";
-*)
-
-(* Polynomials over integral domains are again integral domains *)
-
-Goal "!!p::'a::domain up. p * q = 0 ==> p = 0 | q = 0";
-by (rtac classical 1);
-by (subgoal_tac "deg p = 0 & deg q = 0" 1);
-by (res_inst_tac [("p", "p"), ("n", "0")] up_repr2D 1);
-by (Asm_simp_tac 1);
-by (res_inst_tac [("p", "q"), ("n", "0")] up_repr2D 1);
-by (Asm_simp_tac 1);
-by (subgoal_tac "coeff 0 p = 0 | coeff 0 q = 0" 1);
-by (force_tac (claset() addIs [up_eqI], simpset()) 1);
-by (rtac integral 1);
-by (subgoal_tac "coeff 0 (p * q) = 0" 1);
-by (Asm_simp_tac 2);
-by (Full_simp_tac 1);
-by (dres_inst_tac [("f", "deg")] arg_cong 1);
-by (Asm_full_simp_tac 1);
-qed "up_integral";
-
-Goal "!! a::'a::domain. a *s p = 0 ==> a = 0 | p = 0";
-by (full_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1);
-by (dtac up_integral 1);
-by Auto_tac;
-by (rtac (const_inj RS injD) 1);
-by (Simp_tac 1);
-qed "smult_integral";
-*)
-
-(* Divisibility and degree *)
-
-Goalw [dvd_def]
-  "!! p::'a::domain up. [| p dvd q; q ~= 0 |] ==> deg p <= deg q";
-by (etac exE 1);
-by (hyp_subst_tac 1);
-by (case_tac "p = 0" 1);
-by (case_tac "k = 0" 2);
-by Auto_tac;
-qed "dvd_imp_deg";
diff -r 4822d9597d1e -r d3671b878828 src/HOL/Algebra/poly/UnivPoly.thy
--- a/src/HOL/Algebra/poly/UnivPoly.thy	Tue Apr 29 12:36:49 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,779 +0,0 @@
-(*
-  Title:     Univariate Polynomials
-  Id:        $Id$
-  Author:    Clemens Ballarin, started 9 December 1996
-  Copyright: Clemens Ballarin
-*)
-
-header {* Univariate Polynomials *}
-
-theory UnivPoly = Abstract:
-
-(* already proved in Finite_Set.thy
-
-lemma setsum_cong:
-  "[| A = B; !!i. i : B ==> f i = g i |] ==> setsum f A = setsum g B"
-proof -
-  assume prems: "A = B" "!!i. i : B ==> f i = g i"
-  show ?thesis
-  proof (cases "finite B")
-    case True
-    then have "!!A. [| A = B; !!i. i : B ==> f i = g i |] ==>
-      setsum f A = setsum g B"
-    proof induct
-      case empty thus ?case by simp
-    next
-      case insert thus ?case by simp
-    qed
-    with prems show ?thesis by simp
-  next
-    case False with prems show ?thesis by (simp add: setsum_def)
-  qed
-qed
-*)
-
-(* Instruct simplifier to simplify assumptions introduced by congs.
-   This makes setsum_cong more convenient to use, because assumptions
-   like i:{m..n} get simplified (to m <= i & i <= n). *)
-
-ML_setup {* 
-
-Addcongs [thm "setsum_cong"];
-Context.>> (fn thy => (simpset_ref_of thy :=
-  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
-
-section {* Definition of type up *}
-
-constdefs
-  bound  :: "[nat, nat => 'a::zero] => bool"
-  "bound n f == (ALL i. n < i --> f i = 0)"
-
-lemma boundI [intro!]: "[| !! m. n < m ==> f m = 0 |] ==> bound n f"
-proof (unfold bound_def)
-qed fast
-
-lemma boundE [elim?]: "[| bound n f; (!! m. n < m ==> f m = 0) ==> P |] ==> P"
-proof (unfold bound_def)
-qed fast
-
-lemma boundD [dest]: "[| bound n f; n < m |] ==> f m = 0"
-proof (unfold bound_def)
-qed fast
-
-lemma bound_below:
-  assumes bound: "bound m f" and nonzero: "f n ~= 0" shows "n <= m"
-proof (rule classical)
-  assume "~ ?thesis"
-  then have "m < n" by arith
-  with bound have "f n = 0" ..
-  with nonzero show ?thesis by contradiction
-qed
-
-typedef (UP)
-  ('a) up = "{f :: nat => 'a::zero. EX n. bound n f}"
-by (rule+)   (* Question: what does trace_rule show??? *)
-
-section {* Constants *}
-
-consts
-  coeff  :: "['a up, nat] => ('a::zero)"
-  monom  :: "['a::zero, nat] => 'a up"              ("(3_*X^/_)" [71, 71] 70)
-  "*s"   :: "['a::{zero, times}, 'a up] => 'a up"   (infixl 70)
-
-defs
-  coeff_def: "coeff p n == Rep_UP p n"
-  monom_def: "monom a n == Abs_UP (%i. if i=n then a else 0)"
-  smult_def: "a *s p == Abs_UP (%i. a * Rep_UP p i)"
-
-lemma coeff_bound_ex: "EX n. bound n (coeff p)"
-proof -
-  have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
-  then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
-  then show ?thesis ..
-qed
-  
-lemma bound_coeff_obtain:
-  assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P"
-proof -
-  have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
-  then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
-  with prem show P .
-qed
-
-text {* Ring operations *}
-
-instance up :: (zero) zero ..
-instance up :: (one) one ..
-instance up :: (plus) plus ..
-instance up :: (minus) minus ..
-instance up :: (times) times ..
-instance up :: (inverse) inverse ..
-instance up :: (power) power ..
-
-defs
-  up_add_def:	"p + q == Abs_UP (%n. Rep_UP p n + Rep_UP q n)"
-  up_mult_def:  "p * q == Abs_UP (%n::nat. setsum
-		     (%i. Rep_UP p i * Rep_UP q (n-i)) {..n})"
-  up_zero_def:  "0 == monom 0 0"
-  up_one_def:   "1 == monom 1 0"
-  up_uminus_def:"- p == (- 1) *s p"
-                (* easier to use than "Abs_UP (%i. - Rep_UP p i)" *)
-                (* note: - 1 is different from -1; latter is of class number *)
-
-  up_minus_def:   "(a::'a::{plus, minus} up) - b == a + (-b)"
-  up_inverse_def: "inverse (a::'a::{zero, one, times, inverse} up) == 
-                     (if a dvd 1 then THE x. a*x = 1 else 0)"
-  up_divide_def:  "(a::'a::{times, inverse} up) / b == a * inverse b"
-  up_power_def:   "(a::'a::{one, times, power} up) ^ n ==
-                     nat_rec 1 (%u b. b * a) n"
-
-subsection {* Effect of operations on coefficients *}
-
-lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)"
-proof -
-  have "(%n. if n = m then a else 0) : UP"
-    using UP_def by force
-  from this show ?thesis
-    by (simp add: coeff_def monom_def Abs_UP_inverse Rep_UP)
-qed
-
-lemma coeff_zero [simp]: "coeff 0 n = 0"
-proof (unfold up_zero_def)
-qed simp
-
-lemma coeff_one [simp]: "coeff 1 n = (if n=0 then 1 else 0)"
-proof (unfold up_one_def)
-qed simp
-
-(* term order
-lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n"
-proof -
-  have "!!f. f : UP ==> (%n. a * f n) : UP"
-    by (unfold UP_def) (force simp add: ring_simps)
-*)      (* this force step is slow *)
-(*  then show ?thesis
-    apply (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP)
-qed
-*)
-lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n"
-proof -
-  have "Rep_UP p : UP ==> (%n. a * Rep_UP p n) : UP"
-    by (unfold UP_def) (force simp add: ring_simps)
-      (* this force step is slow *)
-  then show ?thesis
-    by (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP)
-qed
-
-lemma coeff_add [simp]: "coeff (p+q) n = (coeff p n + coeff q n::'a::ring)"
-proof -
-  {
-    fix f g
-    assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP"
-    have "(%i. f i + g i) : UP"
-    proof -
-      from fup obtain n where boundn: "bound n f"
-	by (unfold UP_def) fast
-      from gup obtain m where boundm: "bound m g"
-	by (unfold UP_def) fast
-      have "bound (max n m) (%i. (f i + g i))"
-      proof
-	fix i
-	assume "max n m < i"
-	with boundn and boundm show "f i + g i = 0"
-          by (fastsimp simp add: ring_simps)
-      qed
-      then show "(%i. (f i + g i)) : UP"
-	by (unfold UP_def) fast
-    qed
-  }
-  then show ?thesis
-    by (simp add: coeff_def up_add_def Abs_UP_inverse Rep_UP)
-qed
-
-lemma coeff_mult [simp]:
-  "coeff (p * q) n = (setsum (%i. coeff p i * coeff q (n-i)) {..n}::'a::ring)"
-proof -
-  {
-    fix f g
-    assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP"
-    have "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP"
-    proof -
-      from fup obtain n where "bound n f"
-	by (unfold UP_def) fast
-      from gup obtain m where "bound m g"
-	by (unfold UP_def) fast
-      have "bound (n + m) (%n. setsum (%i. f i * g (n-i)) {..n})"
-      proof
-	fix k
-	assume bound: "n + m < k"
-	{
-	  fix i
-	  have "f i * g (k-i) = 0"
-	  proof cases
-	    assume "n < i"
-	    show ?thesis by (auto! simp add: ring_simps)
-	  next
-	    assume "~ (n < i)"
-	    with bound have "m < k-i" by arith
-	    then show ?thesis by (auto! simp add: ring_simps)
-	  qed
-	}
-	then show "setsum (%i. f i * g (k-i)) {..k} = 0"
-	  by (simp add: ring_simps)
-      qed
-      then show "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP"
-	by (unfold UP_def) fast
-    qed
-  }
-  then show ?thesis
-    by (simp add: coeff_def up_mult_def Abs_UP_inverse Rep_UP)
-qed
-
-lemma coeff_uminus [simp]: "coeff (-p) n = (-coeff p n::'a::ring)"
-by (unfold up_uminus_def) (simp add: ring_simps)
-
-(* Other lemmas *)
-
-lemma up_eqI: assumes prem: "(!! n. coeff p n = coeff q n)" shows "p = q"
-proof -
-  have "p = Abs_UP (%u. Rep_UP p u)" by (simp add: Rep_UP_inverse)
-  also from prem have "... = Abs_UP (Rep_UP q)" by (simp only: coeff_def)
-  also have "... = q" by (simp add: Rep_UP_inverse)
-  finally show ?thesis .
-qed
-
-(* ML_setup {* Addsimprocs [ring_simproc] *} *)
-
-instance up :: (ring) ring
-proof
-  fix p q r :: "'a::ring up"
-  fix n
-  show "(p + q) + r = p + (q + r)"
-    by (rule up_eqI) simp
-  show "0 + p = p"
-    by (rule up_eqI) simp
-  show "(-p) + p = 0"
-    by (rule up_eqI) simp
-  show "p + q = q + p"
-    by (rule up_eqI) simp
-  show "(p * q) * r = p * (q * r)"
-  proof (rule up_eqI)
-    fix n 
-    {
-      fix k and a b c :: "nat=>'a::ring"
-      have "k <= n ==> 
-	setsum (%j. setsum (%i. a i * b (j-i)) {..j} * c (n-j)) {..k} = 
-	setsum (%j. a j * setsum  (%i. b i * c (n-j-i)) {..k-j}) {..k}"
-	(is "_ ==> ?eq k")
-      proof (induct k)
-	case 0 show ?case by simp
-      next
-	case (Suc k)
-	then have "k <= n" by arith
-	then have "?eq k" by (rule Suc)
-	then show ?case
-	  by (simp add: Suc_diff_le natsum_ldistr)
-      qed
-    }
-    then show "coeff ((p * q) * r) n = coeff (p * (q * r)) n"
-      by simp
-  qed
-  show "1 * p = p"
-  proof (rule up_eqI)
-    fix n
-    show "coeff (1 * p) n = coeff p n"
-    proof (cases n)
-      case 0 then show ?thesis by simp
-    next
-      case Suc then show ?thesis by (simp del: natsum_Suc add: natsum_Suc2)
-    qed
-  qed
-  show "(p + q) * r = p * r + q * r"
-    by (rule up_eqI) simp
-  show "p * q = q * p"
-  proof (rule up_eqI)
-    fix n 
-    {
-      fix k
-      fix a b :: "nat=>'a::ring"
-      have "k <= n ==> 
-	setsum (%i. a i * b (n-i)) {..k} =
-	setsum (%i. a (k-i) * b (i+n-k)) {..k}"
-	(is "_ ==> ?eq k")
-      proof (induct k)
-	case 0 show ?case by simp
-      next
-	case (Suc k) then show ?case by (subst natsum_Suc2) simp
-      qed
-    }
-    then show "coeff (p * q) n = coeff (q * p) n"
-      by simp
-  qed
-
-  show "p - q = p + (-q)"
-    by (simp add: up_minus_def)
-  show "inverse p = (if p dvd 1 then THE x. p*x = 1 else 0)"
-    by (simp add: up_inverse_def)
-  show "p / q = p * inverse q"
-    by (simp add: up_divide_def)
-  show "p ^ n = nat_rec 1 (%u b. b * p) n"
-    by (simp add: up_power_def)
-  qed
-
-(* Further properties of monom *)
-
-lemma monom_zero [simp]:
-  "monom 0 n = 0"
-  by (simp add: monom_def up_zero_def)
-(* term order: application of coeff_mult goes wrong: rule not symmetric
-lemma monom_mult_is_smult:
-  "monom (a::'a::ring) 0 * p = a *s p"
-proof (rule up_eqI)
-  fix k
-  show "coeff (monom a 0 * p) k = coeff (a *s p) k"
-  proof (cases k)
-    case 0 then show ?thesis by simp
-  next
-    case Suc then show ?thesis by simp
-  qed
-qed
-*)
-ML_setup {* Delsimprocs [ring_simproc] *}
-
-lemma monom_mult_is_smult:
-  "monom (a::'a::ring) 0 * p = a *s p"
-proof (rule up_eqI)
-  fix k
-  have "coeff (p * monom a 0) k = coeff (a *s p) k"
-  proof (cases k)
-    case 0 then show ?thesis by simp ring
-  next
-    case Suc then show ?thesis by (simp add: ring_simps) ring
-  qed
-  then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring
-qed
-
-ML_setup {* Addsimprocs [ring_simproc] *}
-
-lemma monom_add [simp]:
-  "monom (a + b) n = monom (a::'a::ring) n + monom b n"
-by (rule up_eqI) simp
-
-lemma monom_mult_smult:
-  "monom (a * b) n = a *s monom (b::'a::ring) n"
-by (rule up_eqI) simp
-
-lemma monom_uminus [simp]:
-  "monom (-a) n = - monom (a::'a::ring) n"
-by (rule up_eqI) simp
-
-lemma monom_one [simp]:
-  "monom 1 0 = 1"
-by (simp add: up_one_def)
-
-lemma monom_inj:
-  "(monom a n = monom b n) = (a = b)"
-proof
-  assume "monom a n = monom b n"
-  then have "coeff (monom a n) n = coeff (monom b n) n" by simp
-  then show "a = b" by simp
-next
-  assume "a = b" then show "monom a n = monom b n" by simp
-qed
-
-(* Properties of *s:
-   Polynomials form a module *)
-
-lemma smult_l_distr:
-  "(a + b::'a::ring) *s p = a *s p + b *s p"
-by (rule up_eqI) simp
-
-lemma smult_r_distr:
-  "(a::'a::ring) *s (p + q) = a *s p + a *s q"
-by (rule up_eqI) simp
-
-lemma smult_assoc1:
-  "(a * b::'a::ring) *s p = a *s (b *s p)"
-by (rule up_eqI) simp
-
-lemma smult_one [simp]:
-  "(1::'a::ring) *s p = p"
-by (rule up_eqI) simp
-
-(* Polynomials form an algebra *)
-
-ML_setup {* Delsimprocs [ring_simproc] *}
-
-lemma smult_assoc2:
-  "(a *s p) * q = (a::'a::ring) *s (p * q)"
-by (rule up_eqI) (simp add: natsum_rdistr m_assoc)
-(* Simproc fails. *)
-
-ML_setup {* Addsimprocs [ring_simproc] *}
-
-(* the following can be derived from the above ones,
-   for generality reasons, it is therefore done *)
-
-lemma smult_l_null [simp]:
-  "(0::'a::ring) *s p = 0"
-proof -
-  fix a
-  have "0 *s p = (0 *s p + a *s p) + - (a *s p)" by simp
-  also have "... = (0 + a) *s p + - (a *s p)" by (simp only: smult_l_distr)
-  also have "... = 0" by simp
-  finally show ?thesis .
-qed
-
-lemma smult_r_null [simp]:
-  "(a::'a::ring) *s 0 = 0";
-proof -
-  fix p
-  have "a *s 0 = (a *s 0 + a *s p) + - (a *s p)" by simp
-  also have "... = a *s (0 + p) + - (a *s p)" by (simp only: smult_r_distr)
-  also have "... = 0" by simp
-  finally show ?thesis .
-qed
-
-lemma smult_l_minus:
-  "(-a::'a::ring) *s p = - (a *s p)"
-proof -
-  have "(-a) *s p = (-a *s p + a *s p) + -(a *s p)" by simp 
-  also have "... = (-a + a) *s p + -(a *s p)" by (simp only: smult_l_distr)
-  also have "... = -(a *s p)" by simp
-  finally show ?thesis .
-qed
-
-lemma smult_r_minus:
-  "(a::'a::ring) *s (-p) = - (a *s p)"
-proof -
-  have "a *s (-p) = (a *s -p + a *s p) + -(a *s p)" by simp
-  also have "... = a *s (-p + p) + -(a *s p)" by (simp only: smult_r_distr)
-  also have "... = -(a *s p)" by simp
-  finally show ?thesis .
-qed
-
-section {* The degree function *}
-
-constdefs
-  deg :: "('a::zero) up => nat"
-  "deg p == LEAST n. bound n (coeff p)"
-
-lemma deg_aboveI:
-  "(!!m. n < m ==> coeff p m = 0) ==> deg p <= n"
-by (unfold deg_def) (fast intro: Least_le)
-
-lemma deg_aboveD:
-  assumes prem: "deg p < m" shows "coeff p m = 0"
-proof -
-  obtain n where "bound n (coeff p)" by (rule bound_coeff_obtain)
-  then have "bound (deg p) (coeff p)" by (unfold deg_def, rule LeastI)
-  then show "coeff p m = 0" by (rule boundD)
-qed
-
-lemma deg_belowI:
-  assumes prem: "n ~= 0 ==> coeff p n ~= 0" shows "n <= deg p"
-(* logically, this is a slightly stronger version of deg_aboveD *)
-proof (cases "n=0")
-  case True then show ?thesis by simp
-next
-  case False then have "coeff p n ~= 0" by (rule prem)
-  then have "~ deg p < n" by (fast dest: deg_aboveD)
-  then show ?thesis by arith
-qed
-
-lemma lcoeff_nonzero_deg:
-  assumes deg: "deg p ~= 0" shows "coeff p (deg p) ~= 0"
-proof -
-  obtain m where "deg p <= m" and m_coeff: "coeff p m ~= 0"
-  proof -
-    have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)"
-      by arith (* make public?, why does proof not work with "1" *)
-    from deg have "deg p - 1 < (LEAST n. bound n (coeff p))"
-      by (unfold deg_def) arith
-    then have "~ bound (deg p - 1) (coeff p)" by (rule not_less_Least)
-    then have "EX m. deg p - 1 < m & coeff p m ~= 0"
-      by (unfold bound_def) fast
-    then have "EX m. deg p <= m & coeff p m ~= 0" by (simp add: deg minus)
-    then show ?thesis by auto 
-  qed
-  with deg_belowI have "deg p = m" by fastsimp
-  with m_coeff show ?thesis by simp
-qed
-
-lemma lcoeff_nonzero_nonzero:
-  assumes deg: "deg p = 0" and nonzero: "p ~= 0" shows "coeff p 0 ~= 0"
-proof -
-  have "EX m. coeff p m ~= 0"
-  proof (rule classical)
-    assume "~ ?thesis"
-    then have "p = 0" by (auto intro: up_eqI)
-    with nonzero show ?thesis by contradiction
-  qed
-  then obtain m where coeff: "coeff p m ~= 0" ..
-  then have "m <= deg p" by (rule deg_belowI)
-  then have "m = 0" by (simp add: deg)
-  with coeff show ?thesis by simp
-qed
-
-lemma lcoeff_nonzero:
-  "p ~= 0 ==> coeff p (deg p) ~= 0"
-proof (cases "deg p = 0")
-  case True
-  assume "p ~= 0"
-  with True show ?thesis by (simp add: lcoeff_nonzero_nonzero)
-next
-  case False
-  assume "p ~= 0"
-  with False show ?thesis by (simp add: lcoeff_nonzero_deg)
-qed
-
-lemma deg_eqI:
-  "[| !!m. n < m ==> coeff p m = 0;
-      !!n. n ~= 0 ==> coeff p n ~= 0|] ==> deg p = n"
-by (fast intro: le_anti_sym deg_aboveI deg_belowI)
-
-(* Degree and polynomial operations *)
-
-lemma deg_add [simp]:
-  "deg ((p::'a::ring up) + q) <= max (deg p) (deg q)"
-proof (cases "deg p <= deg q")
-  case True show ?thesis by (rule deg_aboveI) (simp add: True deg_aboveD) 
-next
-  case False show ?thesis by (rule deg_aboveI) (simp add: False deg_aboveD)
-qed
-
-lemma deg_monom_ring:
-  "deg (monom a n::'a::ring up) <= n"
-by (rule deg_aboveI) simp
-
-lemma deg_monom [simp]:
-  "a ~= 0 ==> deg (monom a n::'a::ring up) = n"
-by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI)
-
-lemma deg_const [simp]:
-  "deg (monom (a::'a::ring) 0) = 0"
-proof (rule le_anti_sym)
-  show "deg (monom a 0) <= 0" by (rule deg_aboveI) simp
-next
-  show "0 <= deg (monom a 0)" by (rule deg_belowI) simp
-qed
-
-lemma deg_zero [simp]:
-  "deg 0 = 0"
-proof (rule le_anti_sym)
-  show "deg 0 <= 0" by (rule deg_aboveI) simp
-next
-  show "0 <= deg 0" by (rule deg_belowI) simp
-qed
-
-lemma deg_one [simp]:
-  "deg 1 = 0"
-proof (rule le_anti_sym)
-  show "deg 1 <= 0" by (rule deg_aboveI) simp
-next
-  show "0 <= deg 1" by (rule deg_belowI) simp
-qed
-
-lemma uminus_monom:
-  "!!a::'a::ring. (-a = 0) = (a = 0)"
-proof
-  fix a::"'a::ring"
-  assume "a = 0"
-  then show "-a = 0" by simp
-next
-  fix a::"'a::ring"
-  assume "- a = 0"
-  then have "-(- a) = 0" by simp
-  then show "a = 0" by simp
-qed
-
-lemma deg_uminus [simp]:
-  "deg (-p::('a::ring) up) = deg p"
-proof (rule le_anti_sym)
-  show "deg (- p) <= deg p" by (simp add: deg_aboveI deg_aboveD)
-next
-  show "deg p <= deg (- p)" 
-  by (simp add: deg_belowI lcoeff_nonzero_deg uminus_monom)
-qed
-
-lemma deg_smult_ring:
-  "deg ((a::'a::ring) *s p) <= (if a = 0 then 0 else deg p)"
-proof (cases "a = 0")
-qed (simp add: deg_aboveI deg_aboveD)+
-
-lemma deg_smult [simp]:
-  "deg ((a::'a::domain) *s p) = (if a = 0 then 0 else deg p)"
-proof (rule le_anti_sym)
-  show "deg (a *s p) <= (if a = 0 then 0 else deg p)" by (rule deg_smult_ring)
-next
-  show "(if a = 0 then 0 else deg p) <= deg (a *s p)"
-  proof (cases "a = 0")
-  qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff)
-qed
-
-lemma deg_mult_ring:
-  "deg (p * q::'a::ring up) <= deg p + deg q"
-proof (rule deg_aboveI)
-  fix m
-  assume boundm: "deg p + deg q < m"
-  {
-    fix k i
-    assume boundk: "deg p + deg q < k"
-    then have "coeff p i * coeff q (k - i) = 0"
-    proof (cases "deg p < i")
-      case True then show ?thesis by (simp add: deg_aboveD)
-    next
-      case False with boundk have "deg q < k - i" by arith
-      then show ?thesis by (simp add: deg_aboveD)
-    qed
-  }
-      (* This is similar to bound_mult_zero and deg_above_mult_zero in the old
-         proofs. *)
-  with boundm show "coeff (p * q) m = 0" by simp
-qed
-
-lemma deg_mult [simp]:
-  "[| (p::'a::domain up) ~= 0; q ~= 0|] ==> deg (p * q) = deg p + deg q"
-proof (rule le_anti_sym)
-  show "deg (p * q) <= deg p + deg q" by (rule deg_mult_ring)
-next
-  let ?s = "(%i. coeff p i * coeff q (deg p + deg q - i))"
-  assume nz: "p ~= 0" "q ~= 0"
-  have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith
-  show "deg p + deg q <= deg (p * q)"
-  proof (rule deg_belowI, simp)
-    have "setsum ?s {.. deg p + deg q}
-      = setsum ?s ({.. deg p(} Un {deg p .. deg p + deg q})"
-      by (simp only: ivl_disj_un_one)
-    also have "... = setsum ?s {deg p .. deg p + deg q}"
-      by (simp add: setsum_Un_disjoint ivl_disj_int_one
-        setsum_0 deg_aboveD less_add_diff)
-    also have "... = setsum ?s ({deg p} Un {)deg p .. deg p + deg q})"
-      by (simp only: ivl_disj_un_singleton)
-    also have "... = coeff p (deg p) * coeff q (deg q)" 
-      by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
-        setsum_0 deg_aboveD)
-    finally have "setsum ?s {.. deg p + deg q} 
-      = coeff p (deg p) * coeff q (deg q)" .
-    with nz show "setsum ?s {.. deg p + deg q} ~= 0"
-      by (simp add: integral_iff lcoeff_nonzero)
-    qed
-  qed
-
-lemma coeff_natsum:
-  "((coeff (setsum p A) k)::'a::ring) = 
-   setsum (%i. coeff (p i) k) A"
-proof (cases "finite A")
-  case True then show ?thesis by induct auto
-next
-  case False then show ?thesis by (simp add: setsum_def)
-qed
-(* Instance of a more general result!!! *)
-
-(*
-lemma coeff_natsum:
-  "((coeff (setsum p {..n::nat}) k)::'a::ring) = 
-   setsum (%i. coeff (p i) k) {..n}"
-by (induct n) auto
-*)
-
-lemma up_repr:
-  "setsum (%i. monom (coeff p i) i) {..deg (p::'a::ring up)} = p"
-proof (rule up_eqI)
-  let ?s = "(%i. monom (coeff p i) i)"
-  fix k
-  show "coeff (setsum ?s {..deg p}) k = coeff p k"
-  proof (cases "k <= deg p")
-    case True
-    hence "coeff (setsum ?s {..deg p}) k = 
-          coeff (setsum ?s ({..k} Un {)k..deg p})) k"
-      by (simp only: ivl_disj_un_one)
-    also from True
-    have "... = coeff (setsum ?s {..k}) k"
-      by (simp add: setsum_Un_disjoint ivl_disj_int_one order_less_imp_not_eq2
-        setsum_0 coeff_natsum )
-    also
-    have "... = coeff (setsum ?s ({..k(} Un {k})) k"
-      by (simp only: ivl_disj_un_singleton)
-    also have "... = coeff p k"
-      by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
-        setsum_0 coeff_natsum deg_aboveD)
-    finally show ?thesis .
-  next
-    case False
-    hence "coeff (setsum ?s {..deg p}) k = 
-          coeff (setsum ?s ({..deg p(} Un {deg p})) k"
-      by (simp only: ivl_disj_un_singleton)
-    also from False have "... = coeff p k"
-      by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
-        setsum_0 coeff_natsum deg_aboveD)
-    finally show ?thesis .
-  qed
-qed
-
-lemma up_repr_le:
-  "deg (p::'a::ring up) <= n ==> setsum (%i. monom (coeff p i) i) {..n} = p"
-proof -
-  let ?s = "(%i. monom (coeff p i) i)"
-  assume "deg p <= n"
-  then have "setsum ?s {..n} = setsum ?s ({..deg p} Un {)deg p..n})"
-    by (simp only: ivl_disj_un_one)
-  also have "... = setsum ?s {..deg p}"
-    by (simp add: setsum_Un_disjoint ivl_disj_int_one
-      setsum_0 deg_aboveD)
-  also have "... = p" by (rule up_repr)
-  finally show ?thesis .
-qed
-
-instance up :: ("domain") "domain"
-proof
-  show "1 ~= (0::'a up)"
-  proof (* notI is applied here *)
-    assume "1 = (0::'a up)"
-    hence "coeff 1 0 = (coeff 0 0::'a)" by simp
-    hence "1 = (0::'a)" by simp
-    with one_not_zero show "False" by contradiction
-  qed
-next
-  fix p q :: "'a::domain up"
-  assume pq: "p * q = 0"
-  show "p = 0 | q = 0"
-  proof (rule classical)
-    assume c: "~ (p = 0 | q = 0)"
-    then have "deg p + deg q = deg (p * q)" by simp
-    also from pq have "... = 0" by simp
-    finally have "deg p + deg q = 0" .
-    then have f1: "deg p = 0 & deg q = 0" by simp
-    from f1 have "p = setsum (%i. (monom (coeff p i) i)) {..0}"
-      by (simp only: up_repr_le)
-    also have "... = monom (coeff p 0) 0" by simp
-    finally have p: "p = monom (coeff p 0) 0" .
-    from f1 have "q = setsum (%i. (monom (coeff q i) i)) {..0}"
-      by (simp only: up_repr_le)
-    also have "... = monom (coeff q 0) 0" by simp
-    finally have q: "q = monom (coeff q 0) 0" .
-    have "coeff p 0 * coeff q 0 = coeff (p * q) 0" by simp
-    also from pq have "... = 0" by simp
-    finally have "coeff p 0 * coeff q 0 = 0" .
-    then have "coeff p 0 = 0 | coeff q 0 = 0" by (simp only: integral_iff)
-    with p q show "p = 0 | q = 0" by fastsimp
-  qed
-qed
-
-lemma monom_inj_zero:
-  "(monom a n = 0) = (a = 0)"
-proof -
-  have "(monom a n = 0) = (monom a n = monom 0 n)" by simp
-  also have "... = (a = 0)" by (simp add: monom_inj del: monom_zero)
-  finally show ?thesis .
-qed
-(* term order: makes this simpler!!!
-lemma smult_integral:
-  "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
-by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero) fast
-*)
-lemma smult_integral:
-  "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
-by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero)
-
-end
\ No newline at end of file
diff -r 4822d9597d1e -r d3671b878828 src/HOL/Algebra/poly/UnivPoly2.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/poly/UnivPoly2.ML	Wed Apr 30 10:01:35 2003 +0200
@@ -0,0 +1,359 @@
+(*
+    Degree of polynomials
+    $Id$
+    written by Clemens Ballarin, started 22 January 1997
+*)
+
+(*
+(* Relating degree and bound *)
+
+Goal "[| bound m f; f n ~= 0 |] ==> n <= m";
+by (force_tac (claset() addDs [inst "m" "n" boundD], 
+               simpset()) 1); 
+qed "below_bound";
+
+goal UnivPoly2.thy "bound (LEAST n. bound n (Rep_UP p)) (Rep_UP p)";
+by (rtac exE 1);
+by (rtac LeastI 2);
+by (assume_tac 2);
+by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
+by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
+qed "Least_is_bound";
+
+Goalw [coeff_def, deg_def]
+  "!! p. ALL m. n < m --> coeff m p = 0 ==> deg p <= n";
+by (rtac Least_le 1);
+by (Fast_tac 1);
+qed "deg_aboveI";
+
+Goalw [coeff_def, deg_def]
+  "(n ~= 0 --> coeff n p ~= 0) ==> n <= deg p";
+by (case_tac "n = 0" 1);
+(* Case n=0 *)
+by (Asm_simp_tac 1);
+(* Case n~=0 *)
+by (rotate_tac 1 1);
+by (Asm_full_simp_tac 1);
+by (rtac below_bound 1);
+by (assume_tac 2);
+by (rtac Least_is_bound 1);
+qed "deg_belowI";
+
+Goalw [coeff_def, deg_def]
+  "deg p < m ==> coeff m p = 0";
+by (rtac exE 1); (* create !! x. *)
+by (rtac boundD 2);
+by (assume_tac 3);
+by (rtac LeastI 2);
+by (assume_tac 2);
+by (res_inst_tac [("a", "Rep_UP p")] CollectD 1);
+by (rtac (rewrite_rule [UP_def] Rep_UP) 1);
+qed "deg_aboveD";
+
+Goalw [deg_def]
+  "deg p = Suc y ==> ~ bound y (Rep_UP p)";
+by (rtac not_less_Least 1);
+by (Asm_simp_tac 1);
+val lemma1 = result();
+
+Goalw [deg_def, coeff_def]
+  "deg p = Suc y ==> coeff (deg p) p ~= 0";
+by (rtac ccontr 1);
+by (dtac notnotD 1);
+by (cut_inst_tac [("p", "p")] Least_is_bound 1);
+by (subgoal_tac "bound y (Rep_UP p)" 1);
+(* prove subgoal *)
+by (rtac boundI 2);  
+by (case_tac "Suc y < m" 2);
+(* first case *)
+by (rtac boundD 2);  
+by (assume_tac 2);
+by (Asm_simp_tac 2);
+(* second case *)
+by (dtac leI 2);
+by (dtac Suc_leI 2);
+by (dtac le_anti_sym 2);
+by (assume_tac 2);
+by (Asm_full_simp_tac 2);
+(* end prove subgoal *)
+by (fold_goals_tac [deg_def]);
+by (dtac lemma1 1);
+by (etac notE 1);
+by (assume_tac 1);
+val lemma2 = result();
+
+Goal "deg p ~= 0 ==> coeff (deg p) p ~= 0";
+by (rtac lemma2 1);
+by (Full_simp_tac 1);
+by (dtac Suc_pred 1);
+by (rtac sym 1);
+by (Asm_simp_tac 1);
+qed "deg_lcoeff";
+
+Goal "p ~= 0 ==> coeff (deg p) p ~= 0";
+by (etac contrapos_np 1); 
+by (case_tac "deg p = 0" 1);
+by (blast_tac (claset() addSDs [deg_lcoeff]) 2); 
+by (rtac up_eqI 1);
+by (case_tac "n=0" 1);
+by (rotate_tac ~2 1);
+by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [deg_aboveD]) 1);
+qed "nonzero_lcoeff";
+
+Goal "(deg p <= n) = bound n (Rep_UP p)";
+by (rtac iffI 1);
+(* ==> *)
+by (rtac boundI 1);
+by (fold_goals_tac [coeff_def]);
+by (rtac deg_aboveD 1);
+by (fast_arith_tac 1);
+(* <== *)
+by (rtac deg_aboveI 1);
+by (rewtac coeff_def);
+by (Fast_tac 1);
+qed "deg_above_is_bound";
+
+(* Lemmas on the degree function *)
+
+Goalw [max_def]
+  "!! p::'a::ring up. deg (p + q) <= max (deg p) (deg q)";
+by (case_tac "deg p <= deg q" 1);
+(* case deg p <= deg q *)
+by (rtac deg_aboveI 1);
+by (Asm_simp_tac 1);
+by (strip_tac 1);
+by (dtac le_less_trans 1);
+by (assume_tac 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
+(* case deg p > deg q *)
+by (rtac deg_aboveI 1);
+by (Asm_simp_tac 1);
+by (dtac not_leE 1);
+by (strip_tac 1);
+by (dtac less_trans 1);
+by (assume_tac 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
+qed "deg_add";
+
+Goal "!!p::('a::ring up). deg p < deg q ==> deg (p + q) = deg q";
+by (rtac order_antisym 1);
+by (rtac le_trans 1);
+by (rtac deg_add 1);
+by (Asm_simp_tac 1);
+by (rtac deg_belowI 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD, deg_lcoeff]) 1);
+qed "deg_add_equal";
+
+Goal "deg (monom m::'a::ring up) <= m";
+by (asm_simp_tac 
+  (simpset() addsimps [deg_aboveI, less_not_refl2 RS not_sym]) 1);
+qed "deg_monom_ring";
+
+Goal "deg (monom m::'a::domain up) = m";
+by (rtac le_anti_sym 1);
+(* <= *)
+by (rtac deg_monom_ring 1);
+(* >= *)
+by (asm_simp_tac 
+  (simpset() addsimps [deg_belowI, less_not_refl2 RS not_sym]) 1);
+qed "deg_monom";
+
+Goal "!! a::'a::ring. deg (const a) = 0";
+by (rtac le_anti_sym 1);
+by (rtac deg_aboveI 1);
+by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
+by (rtac deg_belowI 1);
+by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
+qed "deg_const";
+
+Goal "deg (0::'a::ringS up) = 0";
+by (rtac le_anti_sym 1);
+by (rtac deg_aboveI 1);
+by (Simp_tac 1);
+by (rtac deg_belowI 1);
+by (Simp_tac 1);
+qed "deg_zero";
+
+Goal "deg (<1>::'a::ring up) = 0";
+by (rtac le_anti_sym 1);
+by (rtac deg_aboveI 1);
+by (simp_tac (simpset() addsimps [less_not_refl2]) 1);
+by (rtac deg_belowI 1);
+by (Simp_tac 1);
+qed "deg_one";
+
+Goal "!!p::('a::ring) up. deg (-p) = deg p";
+by (rtac le_anti_sym 1);
+(* <= *)
+by (simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1);
+by (simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff, uminus_monom_neq]) 1);
+qed "deg_uminus";
+
+Addsimps [deg_monom, deg_const, deg_zero, deg_one, deg_uminus];
+
+Goal
+  "!! a::'a::ring. deg (a *s p) <= (if a = 0 then 0 else deg p)";
+by (case_tac "a = 0" 1);
+by (REPEAT (asm_simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1));
+qed "deg_smult_ring";
+
+Goal
+  "!! a::'a::domain. deg (a *s p) = (if a = 0 then 0 else deg p)";
+by (rtac le_anti_sym 1);
+by (rtac deg_smult_ring 1);
+by (case_tac "a = 0" 1);
+by (REPEAT (asm_simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff]) 1));
+qed "deg_smult";
+
+Goal
+  "!! p::'a::ring up. [| deg p + deg q < k |] ==> \
+\       coeff i p * coeff (k - i) q = 0";
+by (simp_tac (simpset() addsimps [coeff_def]) 1);
+by (rtac bound_mult_zero 1);
+by (assume_tac 3);
+by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
+by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1);
+qed "deg_above_mult_zero";
+
+Goal
+  "!! p::'a::ring up. deg (p * q) <= deg p + deg q";
+by (rtac deg_aboveI 1);
+by (asm_simp_tac (simpset() addsimps [deg_above_mult_zero]) 1);
+qed "deg_mult_ring";
+
+goal Main.thy 
+  "!!k::nat. k < n ==> m < n + m - k";
+by (arith_tac 1);
+qed "less_add_diff";
+
+Goal "!!p. coeff n p ~= 0 ==> n <= deg p";
+(* More general than deg_belowI, and simplifies the next proof! *)
+by (rtac deg_belowI 1);
+by (Fast_tac 1);
+qed "deg_below2I";
+
+Goal
+  "!! p::'a::domain up. \
+\    [| p ~= 0; q ~= 0 |] ==> deg (p * q) = deg p + deg q";
+by (rtac le_anti_sym 1);
+by (rtac deg_mult_ring 1);
+(* deg p + deg q <= deg (p * q) *)
+by (rtac deg_below2I 1);
+by (Simp_tac 1);
+(*
+by (rtac conjI 1);
+by (rtac impI 1);
+*)
+by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
+by (rtac le_add1 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
+by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
+by (rtac le_refl 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
+by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
+(*
+by (rtac impI 1);
+by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1);
+by (rtac le_add1 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
+by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1);
+by (rtac le_refl 1);
+by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1);
+by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1);
+*)
+qed "deg_mult";
+
+Addsimps [deg_smult, deg_mult];
+
+(* Representation theorems about polynomials *)
+
+goal PolyRing.thy
+  "!! p::nat=>'a::ring up. \
+\    coeff k (setsum p {..n}) = setsum (%i. coeff k (p i)) {..n}";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "coeff_SUM";
+
+goal UnivPoly2.thy
+  "!! f::(nat=>'a::ring). \
+\    bound n f ==> setsum (%i. if i = x then f i else 0) {..n} = f x";
+by (simp_tac (simpset() addsimps [SUM_if_singleton]) 1);
+by (auto_tac
+    (claset() addDs [not_leE],
+     simpset()));
+qed "bound_SUM_if";
+
+Goal
+  "!! p::'a::ring up. deg p <= n ==> \
+\  setsum (%i. coeff i p *s monom i) {..n} = p";
+by (rtac up_eqI 1);
+by (simp_tac (simpset() addsimps [coeff_SUM]) 1);
+by (rtac trans 1);
+by (res_inst_tac [("x", "na")] bound_SUM_if 2);
+by (full_simp_tac (simpset() addsimps [deg_above_is_bound, coeff_def]) 2);
+by (rtac SUM_cong 1);
+by (rtac refl 1);
+by (Asm_simp_tac 1);
+qed "up_repr";
+
+Goal
+  "!! p::'a::ring up. [| deg p <= n; P p |] ==> \
+\  P (setsum (%i. coeff i p *s monom i) {..n})";
+by (asm_simp_tac (simpset() addsimps [up_repr]) 1);
+qed "up_reprD";
+
+Goal
+  "!! p::'a::ring up. \
+\  [| deg p <= n; P (setsum (%i. coeff i p *s monom i) {..n}) |] \
+\    ==> P p";
+by (asm_full_simp_tac (simpset() addsimps [up_repr]) 1);
+qed "up_repr2D";
+
+(*
+Goal
+  "!! p::'a::ring up. [| deg p <= n; deg q <= m |] ==> \
+\    (SUM n (%i. coeff i p *s monom i) = SUM m (%i. coeff i q *s monom i)) \
+\    = (coeff k f = coeff k g)
+...
+qed "up_unique";
+*)
+
+(* Polynomials over integral domains are again integral domains *)
+
+Goal "!!p::'a::domain up. p * q = 0 ==> p = 0 | q = 0";
+by (rtac classical 1);
+by (subgoal_tac "deg p = 0 & deg q = 0" 1);
+by (res_inst_tac [("p", "p"), ("n", "0")] up_repr2D 1);
+by (Asm_simp_tac 1);
+by (res_inst_tac [("p", "q"), ("n", "0")] up_repr2D 1);
+by (Asm_simp_tac 1);
+by (subgoal_tac "coeff 0 p = 0 | coeff 0 q = 0" 1);
+by (force_tac (claset() addIs [up_eqI], simpset()) 1);
+by (rtac integral 1);
+by (subgoal_tac "coeff 0 (p * q) = 0" 1);
+by (Asm_simp_tac 2);
+by (Full_simp_tac 1);
+by (dres_inst_tac [("f", "deg")] arg_cong 1);
+by (Asm_full_simp_tac 1);
+qed "up_integral";
+
+Goal "!! a::'a::domain. a *s p = 0 ==> a = 0 | p = 0";
+by (full_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1);
+by (dtac up_integral 1);
+by Auto_tac;
+by (rtac (const_inj RS injD) 1);
+by (Simp_tac 1);
+qed "smult_integral";
+*)
+
+(* Divisibility and degree *)
+
+Goalw [dvd_def]
+  "!! p::'a::domain up. [| p dvd q; q ~= 0 |] ==> deg p <= deg q";
+by (etac exE 1);
+by (hyp_subst_tac 1);
+by (case_tac "p = 0" 1);
+by (case_tac "k = 0" 2);
+by Auto_tac;
+qed "dvd_imp_deg";
diff -r 4822d9597d1e -r d3671b878828 src/HOL/Algebra/poly/UnivPoly2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Apr 30 10:01:35 2003 +0200
@@ -0,0 +1,779 @@
+(*
+  Title:     Univariate Polynomials
+  Id:        $Id$
+  Author:    Clemens Ballarin, started 9 December 1996
+  Copyright: Clemens Ballarin
+*)
+
+header {* Univariate Polynomials *}
+
+theory UnivPoly2 = Abstract:
+
+(* already proved in Finite_Set.thy
+
+lemma setsum_cong:
+  "[| A = B; !!i. i : B ==> f i = g i |] ==> setsum f A = setsum g B"
+proof -
+  assume prems: "A = B" "!!i. i : B ==> f i = g i"
+  show ?thesis
+  proof (cases "finite B")
+    case True
+    then have "!!A. [| A = B; !!i. i : B ==> f i = g i |] ==>
+      setsum f A = setsum g B"
+    proof induct
+      case empty thus ?case by simp
+    next
+      case insert thus ?case by simp
+    qed
+    with prems show ?thesis by simp
+  next
+    case False with prems show ?thesis by (simp add: setsum_def)
+  qed
+qed
+*)
+
+(* Instruct simplifier to simplify assumptions introduced by congs.
+   This makes setsum_cong more convenient to use, because assumptions
+   like i:{m..n} get simplified (to m <= i & i <= n). *)
+
+ML_setup {* 
+
+Addcongs [thm "setsum_cong"];
+Context.>> (fn thy => (simpset_ref_of thy :=
+  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
+
+section {* Definition of type up *}
+
+constdefs
+  bound  :: "[nat, nat => 'a::zero] => bool"
+  "bound n f == (ALL i. n < i --> f i = 0)"
+
+lemma boundI [intro!]: "[| !! m. n < m ==> f m = 0 |] ==> bound n f"
+proof (unfold bound_def)
+qed fast
+
+lemma boundE [elim?]: "[| bound n f; (!! m. n < m ==> f m = 0) ==> P |] ==> P"
+proof (unfold bound_def)
+qed fast
+
+lemma boundD [dest]: "[| bound n f; n < m |] ==> f m = 0"
+proof (unfold bound_def)
+qed fast
+
+lemma bound_below:
+  assumes bound: "bound m f" and nonzero: "f n ~= 0" shows "n <= m"
+proof (rule classical)
+  assume "~ ?thesis"
+  then have "m < n" by arith
+  with bound have "f n = 0" ..
+  with nonzero show ?thesis by contradiction
+qed
+
+typedef (UP)
+  ('a) up = "{f :: nat => 'a::zero. EX n. bound n f}"
+by (rule+)   (* Question: what does trace_rule show??? *)
+
+section {* Constants *}
+
+consts
+  coeff  :: "['a up, nat] => ('a::zero)"
+  monom  :: "['a::zero, nat] => 'a up"              ("(3_*X^/_)" [71, 71] 70)
+  "*s"   :: "['a::{zero, times}, 'a up] => 'a up"   (infixl 70)
+
+defs
+  coeff_def: "coeff p n == Rep_UP p n"
+  monom_def: "monom a n == Abs_UP (%i. if i=n then a else 0)"
+  smult_def: "a *s p == Abs_UP (%i. a * Rep_UP p i)"
+
+lemma coeff_bound_ex: "EX n. bound n (coeff p)"
+proof -
+  have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
+  then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
+  then show ?thesis ..
+qed
+  
+lemma bound_coeff_obtain:
+  assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P"
+proof -
+  have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
+  then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
+  with prem show P .
+qed
+
+text {* Ring operations *}
+
+instance up :: (zero) zero ..
+instance up :: (one) one ..
+instance up :: (plus) plus ..
+instance up :: (minus) minus ..
+instance up :: (times) times ..
+instance up :: (inverse) inverse ..
+instance up :: (power) power ..
+
+defs
+  up_add_def:	"p + q == Abs_UP (%n. Rep_UP p n + Rep_UP q n)"
+  up_mult_def:  "p * q == Abs_UP (%n::nat. setsum
+		     (%i. Rep_UP p i * Rep_UP q (n-i)) {..n})"
+  up_zero_def:  "0 == monom 0 0"
+  up_one_def:   "1 == monom 1 0"
+  up_uminus_def:"- p == (- 1) *s p"
+                (* easier to use than "Abs_UP (%i. - Rep_UP p i)" *)
+                (* note: - 1 is different from -1; latter is of class number *)
+
+  up_minus_def:   "(a::'a::{plus, minus} up) - b == a + (-b)"
+  up_inverse_def: "inverse (a::'a::{zero, one, times, inverse} up) == 
+                     (if a dvd 1 then THE x. a*x = 1 else 0)"
+  up_divide_def:  "(a::'a::{times, inverse} up) / b == a * inverse b"
+  up_power_def:   "(a::'a::{one, times, power} up) ^ n ==
+                     nat_rec 1 (%u b. b * a) n"
+
+subsection {* Effect of operations on coefficients *}
+
+lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)"
+proof -
+  have "(%n. if n = m then a else 0) : UP"
+    using UP_def by force
+  from this show ?thesis
+    by (simp add: coeff_def monom_def Abs_UP_inverse Rep_UP)
+qed
+
+lemma coeff_zero [simp]: "coeff 0 n = 0"
+proof (unfold up_zero_def)
+qed simp
+
+lemma coeff_one [simp]: "coeff 1 n = (if n=0 then 1 else 0)"
+proof (unfold up_one_def)
+qed simp
+
+(* term order
+lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n"
+proof -
+  have "!!f. f : UP ==> (%n. a * f n) : UP"
+    by (unfold UP_def) (force simp add: ring_simps)
+*)      (* this force step is slow *)
+(*  then show ?thesis
+    apply (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP)
+qed
+*)
+lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n"
+proof -
+  have "Rep_UP p : UP ==> (%n. a * Rep_UP p n) : UP"
+    by (unfold UP_def) (force simp add: ring_simps)
+      (* this force step is slow *)
+  then show ?thesis
+    by (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP)
+qed
+
+lemma coeff_add [simp]: "coeff (p+q) n = (coeff p n + coeff q n::'a::ring)"
+proof -
+  {
+    fix f g
+    assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP"
+    have "(%i. f i + g i) : UP"
+    proof -
+      from fup obtain n where boundn: "bound n f"
+	by (unfold UP_def) fast
+      from gup obtain m where boundm: "bound m g"
+	by (unfold UP_def) fast
+      have "bound (max n m) (%i. (f i + g i))"
+      proof
+	fix i
+	assume "max n m < i"
+	with boundn and boundm show "f i + g i = 0"
+          by (fastsimp simp add: ring_simps)
+      qed
+      then show "(%i. (f i + g i)) : UP"
+	by (unfold UP_def) fast
+    qed
+  }
+  then show ?thesis
+    by (simp add: coeff_def up_add_def Abs_UP_inverse Rep_UP)
+qed
+
+lemma coeff_mult [simp]:
+  "coeff (p * q) n = (setsum (%i. coeff p i * coeff q (n-i)) {..n}::'a::ring)"
+proof -
+  {
+    fix f g
+    assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP"
+    have "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP"
+    proof -
+      from fup obtain n where "bound n f"
+	by (unfold UP_def) fast
+      from gup obtain m where "bound m g"
+	by (unfold UP_def) fast
+      have "bound (n + m) (%n. setsum (%i. f i * g (n-i)) {..n})"
+      proof
+	fix k
+	assume bound: "n + m < k"
+	{
+	  fix i
+	  have "f i * g (k-i) = 0"
+	  proof cases
+	    assume "n < i"
+	    show ?thesis by (auto! simp add: ring_simps)
+	  next
+	    assume "~ (n < i)"
+	    with bound have "m < k-i" by arith
+	    then show ?thesis by (auto! simp add: ring_simps)
+	  qed
+	}
+	then show "setsum (%i. f i * g (k-i)) {..k} = 0"
+	  by (simp add: ring_simps)
+      qed
+      then show "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP"
+	by (unfold UP_def) fast
+    qed
+  }
+  then show ?thesis
+    by (simp add: coeff_def up_mult_def Abs_UP_inverse Rep_UP)
+qed
+
+lemma coeff_uminus [simp]: "coeff (-p) n = (-coeff p n::'a::ring)"
+by (unfold up_uminus_def) (simp add: ring_simps)
+
+(* Other lemmas *)
+
+lemma up_eqI: assumes prem: "(!! n. coeff p n = coeff q n)" shows "p = q"
+proof -
+  have "p = Abs_UP (%u. Rep_UP p u)" by (simp add: Rep_UP_inverse)
+  also from prem have "... = Abs_UP (Rep_UP q)" by (simp only: coeff_def)
+  also have "... = q" by (simp add: Rep_UP_inverse)
+  finally show ?thesis .
+qed
+
+(* ML_setup {* Addsimprocs [ring_simproc] *} *)
+
+instance up :: (ring) ring
+proof
+  fix p q r :: "'a::ring up"
+  fix n
+  show "(p + q) + r = p + (q + r)"
+    by (rule up_eqI) simp
+  show "0 + p = p"
+    by (rule up_eqI) simp
+  show "(-p) + p = 0"
+    by (rule up_eqI) simp
+  show "p + q = q + p"
+    by (rule up_eqI) simp
+  show "(p * q) * r = p * (q * r)"
+  proof (rule up_eqI)
+    fix n 
+    {
+      fix k and a b c :: "nat=>'a::ring"
+      have "k <= n ==> 
+	setsum (%j. setsum (%i. a i * b (j-i)) {..j} * c (n-j)) {..k} = 
+	setsum (%j. a j * setsum  (%i. b i * c (n-j-i)) {..k-j}) {..k}"
+	(is "_ ==> ?eq k")
+      proof (induct k)
+	case 0 show ?case by simp
+      next
+	case (Suc k)
+	then have "k <= n" by arith
+	then have "?eq k" by (rule Suc)
+	then show ?case
+	  by (simp add: Suc_diff_le natsum_ldistr)
+      qed
+    }
+    then show "coeff ((p * q) * r) n = coeff (p * (q * r)) n"
+      by simp
+  qed
+  show "1 * p = p"
+  proof (rule up_eqI)
+    fix n
+    show "coeff (1 * p) n = coeff p n"
+    proof (cases n)
+      case 0 then show ?thesis by simp
+    next
+      case Suc then show ?thesis by (simp del: natsum_Suc add: natsum_Suc2)
+    qed
+  qed
+  show "(p + q) * r = p * r + q * r"
+    by (rule up_eqI) simp
+  show "p * q = q * p"
+  proof (rule up_eqI)
+    fix n 
+    {
+      fix k
+      fix a b :: "nat=>'a::ring"
+      have "k <= n ==> 
+	setsum (%i. a i * b (n-i)) {..k} =
+	setsum (%i. a (k-i) * b (i+n-k)) {..k}"
+	(is "_ ==> ?eq k")
+      proof (induct k)
+	case 0 show ?case by simp
+      next
+	case (Suc k) then show ?case by (subst natsum_Suc2) simp
+      qed
+    }
+    then show "coeff (p * q) n = coeff (q * p) n"
+      by simp
+  qed
+
+  show "p - q = p + (-q)"
+    by (simp add: up_minus_def)
+  show "inverse p = (if p dvd 1 then THE x. p*x = 1 else 0)"
+    by (simp add: up_inverse_def)
+  show "p / q = p * inverse q"
+    by (simp add: up_divide_def)
+  show "p ^ n = nat_rec 1 (%u b. b * p) n"
+    by (simp add: up_power_def)
+  qed
+
+(* Further properties of monom *)
+
+lemma monom_zero [simp]:
+  "monom 0 n = 0"
+  by (simp add: monom_def up_zero_def)
+(* term order: application of coeff_mult goes wrong: rule not symmetric
+lemma monom_mult_is_smult:
+  "monom (a::'a::ring) 0 * p = a *s p"
+proof (rule up_eqI)
+  fix k
+  show "coeff (monom a 0 * p) k = coeff (a *s p) k"
+  proof (cases k)
+    case 0 then show ?thesis by simp
+  next
+    case Suc then show ?thesis by simp
+  qed
+qed
+*)
+ML_setup {* Delsimprocs [ring_simproc] *}
+
+lemma monom_mult_is_smult:
+  "monom (a::'a::ring) 0 * p = a *s p"
+proof (rule up_eqI)
+  fix k
+  have "coeff (p * monom a 0) k = coeff (a *s p) k"
+  proof (cases k)
+    case 0 then show ?thesis by simp ring
+  next
+    case Suc then show ?thesis by (simp add: ring_simps) ring
+  qed
+  then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring
+qed
+
+ML_setup {* Addsimprocs [ring_simproc] *}
+
+lemma monom_add [simp]:
+  "monom (a + b) n = monom (a::'a::ring) n + monom b n"
+by (rule up_eqI) simp
+
+lemma monom_mult_smult:
+  "monom (a * b) n = a *s monom (b::'a::ring) n"
+by (rule up_eqI) simp
+
+lemma monom_uminus [simp]:
+  "monom (-a) n = - monom (a::'a::ring) n"
+by (rule up_eqI) simp
+
+lemma monom_one [simp]:
+  "monom 1 0 = 1"
+by (simp add: up_one_def)
+
+lemma monom_inj:
+  "(monom a n = monom b n) = (a = b)"
+proof
+  assume "monom a n = monom b n"
+  then have "coeff (monom a n) n = coeff (monom b n) n" by simp
+  then show "a = b" by simp
+next
+  assume "a = b" then show "monom a n = monom b n" by simp
+qed
+
+(* Properties of *s:
+   Polynomials form a module *)
+
+lemma smult_l_distr:
+  "(a + b::'a::ring) *s p = a *s p + b *s p"
+by (rule up_eqI) simp
+
+lemma smult_r_distr:
+  "(a::'a::ring) *s (p + q) = a *s p + a *s q"
+by (rule up_eqI) simp
+
+lemma smult_assoc1:
+  "(a * b::'a::ring) *s p = a *s (b *s p)"
+by (rule up_eqI) simp
+
+lemma smult_one [simp]:
+  "(1::'a::ring) *s p = p"
+by (rule up_eqI) simp
+
+(* Polynomials form an algebra *)
+
+ML_setup {* Delsimprocs [ring_simproc] *}
+
+lemma smult_assoc2:
+  "(a *s p) * q = (a::'a::ring) *s (p * q)"
+by (rule up_eqI) (simp add: natsum_rdistr m_assoc)
+(* Simproc fails. *)
+
+ML_setup {* Addsimprocs [ring_simproc] *}
+
+(* the following can be derived from the above ones,
+   for generality reasons, it is therefore done *)
+
+lemma smult_l_null [simp]:
+  "(0::'a::ring) *s p = 0"
+proof -
+  fix a
+  have "0 *s p = (0 *s p + a *s p) + - (a *s p)" by simp
+  also have "... = (0 + a) *s p + - (a *s p)" by (simp only: smult_l_distr)
+  also have "... = 0" by simp
+  finally show ?thesis .
+qed
+
+lemma smult_r_null [simp]:
+  "(a::'a::ring) *s 0 = 0";
+proof -
+  fix p
+  have "a *s 0 = (a *s 0 + a *s p) + - (a *s p)" by simp
+  also have "... = a *s (0 + p) + - (a *s p)" by (simp only: smult_r_distr)
+  also have "... = 0" by simp
+  finally show ?thesis .
+qed
+
+lemma smult_l_minus:
+  "(-a::'a::ring) *s p = - (a *s p)"
+proof -
+  have "(-a) *s p = (-a *s p + a *s p) + -(a *s p)" by simp 
+  also have "... = (-a + a) *s p + -(a *s p)" by (simp only: smult_l_distr)
+  also have "... = -(a *s p)" by simp
+  finally show ?thesis .
+qed
+
+lemma smult_r_minus:
+  "(a::'a::ring) *s (-p) = - (a *s p)"
+proof -
+  have "a *s (-p) = (a *s -p + a *s p) + -(a *s p)" by simp
+  also have "... = a *s (-p + p) + -(a *s p)" by (simp only: smult_r_distr)
+  also have "... = -(a *s p)" by simp
+  finally show ?thesis .
+qed
+
+section {* The degree function *}
+
+constdefs
+  deg :: "('a::zero) up => nat"
+  "deg p == LEAST n. bound n (coeff p)"
+
+lemma deg_aboveI:
+  "(!!m. n < m ==> coeff p m = 0) ==> deg p <= n"
+by (unfold deg_def) (fast intro: Least_le)
+
+lemma deg_aboveD:
+  assumes prem: "deg p < m" shows "coeff p m = 0"
+proof -
+  obtain n where "bound n (coeff p)" by (rule bound_coeff_obtain)
+  then have "bound (deg p) (coeff p)" by (unfold deg_def, rule LeastI)
+  then show "coeff p m = 0" by (rule boundD)
+qed
+
+lemma deg_belowI:
+  assumes prem: "n ~= 0 ==> coeff p n ~= 0" shows "n <= deg p"
+(* logically, this is a slightly stronger version of deg_aboveD *)
+proof (cases "n=0")
+  case True then show ?thesis by simp
+next
+  case False then have "coeff p n ~= 0" by (rule prem)
+  then have "~ deg p < n" by (fast dest: deg_aboveD)
+  then show ?thesis by arith
+qed
+
+lemma lcoeff_nonzero_deg:
+  assumes deg: "deg p ~= 0" shows "coeff p (deg p) ~= 0"
+proof -
+  obtain m where "deg p <= m" and m_coeff: "coeff p m ~= 0"
+  proof -
+    have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)"
+      by arith (* make public?, why does proof not work with "1" *)
+    from deg have "deg p - 1 < (LEAST n. bound n (coeff p))"
+      by (unfold deg_def) arith
+    then have "~ bound (deg p - 1) (coeff p)" by (rule not_less_Least)
+    then have "EX m. deg p - 1 < m & coeff p m ~= 0"
+      by (unfold bound_def) fast
+    then have "EX m. deg p <= m & coeff p m ~= 0" by (simp add: deg minus)
+    then show ?thesis by auto 
+  qed
+  with deg_belowI have "deg p = m" by fastsimp
+  with m_coeff show ?thesis by simp
+qed
+
+lemma lcoeff_nonzero_nonzero:
+  assumes deg: "deg p = 0" and nonzero: "p ~= 0" shows "coeff p 0 ~= 0"
+proof -
+  have "EX m. coeff p m ~= 0"
+  proof (rule classical)
+    assume "~ ?thesis"
+    then have "p = 0" by (auto intro: up_eqI)
+    with nonzero show ?thesis by contradiction
+  qed
+  then obtain m where coeff: "coeff p m ~= 0" ..
+  then have "m <= deg p" by (rule deg_belowI)
+  then have "m = 0" by (simp add: deg)
+  with coeff show ?thesis by simp
+qed
+
+lemma lcoeff_nonzero:
+  "p ~= 0 ==> coeff p (deg p) ~= 0"
+proof (cases "deg p = 0")
+  case True
+  assume "p ~= 0"
+  with True show ?thesis by (simp add: lcoeff_nonzero_nonzero)
+next
+  case False
+  assume "p ~= 0"
+  with False show ?thesis by (simp add: lcoeff_nonzero_deg)
+qed
+
+lemma deg_eqI:
+  "[| !!m. n < m ==> coeff p m = 0;
+      !!n. n ~= 0 ==> coeff p n ~= 0|] ==> deg p = n"
+by (fast intro: le_anti_sym deg_aboveI deg_belowI)
+
+(* Degree and polynomial operations *)
+
+lemma deg_add [simp]:
+  "deg ((p::'a::ring up) + q) <= max (deg p) (deg q)"
+proof (cases "deg p <= deg q")
+  case True show ?thesis by (rule deg_aboveI) (simp add: True deg_aboveD) 
+next
+  case False show ?thesis by (rule deg_aboveI) (simp add: False deg_aboveD)
+qed
+
+lemma deg_monom_ring:
+  "deg (monom a n::'a::ring up) <= n"
+by (rule deg_aboveI) simp
+
+lemma deg_monom [simp]:
+  "a ~= 0 ==> deg (monom a n::'a::ring up) = n"
+by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI)
+
+lemma deg_const [simp]:
+  "deg (monom (a::'a::ring) 0) = 0"
+proof (rule le_anti_sym)
+  show "deg (monom a 0) <= 0" by (rule deg_aboveI) simp
+next
+  show "0 <= deg (monom a 0)" by (rule deg_belowI) simp
+qed
+
+lemma deg_zero [simp]:
+  "deg 0 = 0"
+proof (rule le_anti_sym)
+  show "deg 0 <= 0" by (rule deg_aboveI) simp
+next
+  show "0 <= deg 0" by (rule deg_belowI) simp
+qed
+
+lemma deg_one [simp]:
+  "deg 1 = 0"
+proof (rule le_anti_sym)
+  show "deg 1 <= 0" by (rule deg_aboveI) simp
+next
+  show "0 <= deg 1" by (rule deg_belowI) simp
+qed
+
+lemma uminus_monom:
+  "!!a::'a::ring. (-a = 0) = (a = 0)"
+proof
+  fix a::"'a::ring"
+  assume "a = 0"
+  then show "-a = 0" by simp
+next
+  fix a::"'a::ring"
+  assume "- a = 0"
+  then have "-(- a) = 0" by simp
+  then show "a = 0" by simp
+qed
+
+lemma deg_uminus [simp]:
+  "deg (-p::('a::ring) up) = deg p"
+proof (rule le_anti_sym)
+  show "deg (- p) <= deg p" by (simp add: deg_aboveI deg_aboveD)
+next
+  show "deg p <= deg (- p)" 
+  by (simp add: deg_belowI lcoeff_nonzero_deg uminus_monom)
+qed
+
+lemma deg_smult_ring:
+  "deg ((a::'a::ring) *s p) <= (if a = 0 then 0 else deg p)"
+proof (cases "a = 0")
+qed (simp add: deg_aboveI deg_aboveD)+
+
+lemma deg_smult [simp]:
+  "deg ((a::'a::domain) *s p) = (if a = 0 then 0 else deg p)"
+proof (rule le_anti_sym)
+  show "deg (a *s p) <= (if a = 0 then 0 else deg p)" by (rule deg_smult_ring)
+next
+  show "(if a = 0 then 0 else deg p) <= deg (a *s p)"
+  proof (cases "a = 0")
+  qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff)
+qed
+
+lemma deg_mult_ring:
+  "deg (p * q::'a::ring up) <= deg p + deg q"
+proof (rule deg_aboveI)
+  fix m
+  assume boundm: "deg p + deg q < m"
+  {
+    fix k i
+    assume boundk: "deg p + deg q < k"
+    then have "coeff p i * coeff q (k - i) = 0"
+    proof (cases "deg p < i")
+      case True then show ?thesis by (simp add: deg_aboveD)
+    next
+      case False with boundk have "deg q < k - i" by arith
+      then show ?thesis by (simp add: deg_aboveD)
+    qed
+  }
+      (* This is similar to bound_mult_zero and deg_above_mult_zero in the old
+         proofs. *)
+  with boundm show "coeff (p * q) m = 0" by simp
+qed
+
+lemma deg_mult [simp]:
+  "[| (p::'a::domain up) ~= 0; q ~= 0|] ==> deg (p * q) = deg p + deg q"
+proof (rule le_anti_sym)
+  show "deg (p * q) <= deg p + deg q" by (rule deg_mult_ring)
+next
+  let ?s = "(%i. coeff p i * coeff q (deg p + deg q - i))"
+  assume nz: "p ~= 0" "q ~= 0"
+  have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith
+  show "deg p + deg q <= deg (p * q)"
+  proof (rule deg_belowI, simp)
+    have "setsum ?s {.. deg p + deg q}
+      = setsum ?s ({.. deg p(} Un {deg p .. deg p + deg q})"
+      by (simp only: ivl_disj_un_one)
+    also have "... = setsum ?s {deg p .. deg p + deg q}"
+      by (simp add: setsum_Un_disjoint ivl_disj_int_one
+        setsum_0 deg_aboveD less_add_diff)
+    also have "... = setsum ?s ({deg p} Un {)deg p .. deg p + deg q})"
+      by (simp only: ivl_disj_un_singleton)
+    also have "... = coeff p (deg p) * coeff q (deg q)" 
+      by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
+        setsum_0 deg_aboveD)
+    finally have "setsum ?s {.. deg p + deg q} 
+      = coeff p (deg p) * coeff q (deg q)" .
+    with nz show "setsum ?s {.. deg p + deg q} ~= 0"
+      by (simp add: integral_iff lcoeff_nonzero)
+    qed
+  qed
+
+lemma coeff_natsum:
+  "((coeff (setsum p A) k)::'a::ring) = 
+   setsum (%i. coeff (p i) k) A"
+proof (cases "finite A")
+  case True then show ?thesis by induct auto
+next
+  case False then show ?thesis by (simp add: setsum_def)
+qed
+(* Instance of a more general result!!! *)
+
+(*
+lemma coeff_natsum:
+  "((coeff (setsum p {..n::nat}) k)::'a::ring) = 
+   setsum (%i. coeff (p i) k) {..n}"
+by (induct n) auto
+*)
+
+lemma up_repr:
+  "setsum (%i. monom (coeff p i) i) {..deg (p::'a::ring up)} = p"
+proof (rule up_eqI)
+  let ?s = "(%i. monom (coeff p i) i)"
+  fix k
+  show "coeff (setsum ?s {..deg p}) k = coeff p k"
+  proof (cases "k <= deg p")
+    case True
+    hence "coeff (setsum ?s {..deg p}) k = 
+          coeff (setsum ?s ({..k} Un {)k..deg p})) k"
+      by (simp only: ivl_disj_un_one)
+    also from True
+    have "... = coeff (setsum ?s {..k}) k"
+      by (simp add: setsum_Un_disjoint ivl_disj_int_one order_less_imp_not_eq2
+        setsum_0 coeff_natsum )
+    also
+    have "... = coeff (setsum ?s ({..k(} Un {k})) k"
+      by (simp only: ivl_disj_un_singleton)
+    also have "... = coeff p k"
+      by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
+        setsum_0 coeff_natsum deg_aboveD)
+    finally show ?thesis .
+  next
+    case False
+    hence "coeff (setsum ?s {..deg p}) k = 
+          coeff (setsum ?s ({..deg p(} Un {deg p})) k"
+      by (simp only: ivl_disj_un_singleton)
+    also from False have "... = coeff p k"
+      by (simp add: setsum_Un_disjoint ivl_disj_int_singleton 
+        setsum_0 coeff_natsum deg_aboveD)
+    finally show ?thesis .
+  qed
+qed
+
+lemma up_repr_le:
+  "deg (p::'a::ring up) <= n ==> setsum (%i. monom (coeff p i) i) {..n} = p"
+proof -
+  let ?s = "(%i. monom (coeff p i) i)"
+  assume "deg p <= n"
+  then have "setsum ?s {..n} = setsum ?s ({..deg p} Un {)deg p..n})"
+    by (simp only: ivl_disj_un_one)
+  also have "... = setsum ?s {..deg p}"
+    by (simp add: setsum_Un_disjoint ivl_disj_int_one
+      setsum_0 deg_aboveD)
+  also have "... = p" by (rule up_repr)
+  finally show ?thesis .
+qed
+
+instance up :: ("domain") "domain"
+proof
+  show "1 ~= (0::'a up)"
+  proof (* notI is applied here *)
+    assume "1 = (0::'a up)"
+    hence "coeff 1 0 = (coeff 0 0::'a)" by simp
+    hence "1 = (0::'a)" by simp
+    with one_not_zero show "False" by contradiction
+  qed
+next
+  fix p q :: "'a::domain up"
+  assume pq: "p * q = 0"
+  show "p = 0 | q = 0"
+  proof (rule classical)
+    assume c: "~ (p = 0 | q = 0)"
+    then have "deg p + deg q = deg (p * q)" by simp
+    also from pq have "... = 0" by simp
+    finally have "deg p + deg q = 0" .
+    then have f1: "deg p = 0 & deg q = 0" by simp
+    from f1 have "p = setsum (%i. (monom (coeff p i) i)) {..0}"
+      by (simp only: up_repr_le)
+    also have "... = monom (coeff p 0) 0" by simp
+    finally have p: "p = monom (coeff p 0) 0" .
+    from f1 have "q = setsum (%i. (monom (coeff q i) i)) {..0}"
+      by (simp only: up_repr_le)
+    also have "... = monom (coeff q 0) 0" by simp
+    finally have q: "q = monom (coeff q 0) 0" .
+    have "coeff p 0 * coeff q 0 = coeff (p * q) 0" by simp
+    also from pq have "... = 0" by simp
+    finally have "coeff p 0 * coeff q 0 = 0" .
+    then have "coeff p 0 = 0 | coeff q 0 = 0" by (simp only: integral_iff)
+    with p q show "p = 0 | q = 0" by fastsimp
+  qed
+qed
+
+lemma monom_inj_zero:
+  "(monom a n = 0) = (a = 0)"
+proof -
+  have "(monom a n = 0) = (monom a n = monom 0 n)" by simp
+  also have "... = (a = 0)" by (simp add: monom_inj del: monom_zero)
+  finally show ?thesis .
+qed
+(* term order: makes this simpler!!!
+lemma smult_integral:
+  "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
+by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero) fast
+*)
+lemma smult_integral:
+  "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
+by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero)
+
+end
\ No newline at end of file
diff -r 4822d9597d1e -r d3671b878828 src/HOL/Algebra/ringsimp.ML
--- a/src/HOL/Algebra/ringsimp.ML	Tue Apr 29 12:36:49 2003 +0200
+++ b/src/HOL/Algebra/ringsimp.ML	Wed Apr 30 10:01:35 2003 +0200
@@ -56,8 +56,8 @@
 (*** Term order for commutative rings ***)
 
 fun ring_ord a =
-  find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "Cring.ring.a_inv",
-  "CRing.ring.minus", "Group.monoid.one", "Group.semigroup.mult"];
+  find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "CRing.a_inv",
+  "CRing.minus", "Group.monoid.one", "Group.semigroup.mult"];
 
 fun termless_ring (a, b) = (term_lpo ring_ord (a, b) = LESS);