Generalised polynomial lemmas from cring to ring.
authorballarin
Fri Aug 01 18:10:52 2008 +0200 (2008-08-01)
changeset 2771721bbd410ba04
parent 27716 96699d8eb49e
child 27718 3a85bc6bfd73
Generalised polynomial lemmas from cring to ring.
NEWS
src/HOL/Algebra/AbelCoset.thy
src/HOL/Algebra/Bij.thy
src/HOL/Algebra/Congruence.thy
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Divisibility.thy
src/HOL/Algebra/Exponent.thy
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Algebra/Ideal.thy
src/HOL/Algebra/IntRing.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/QuotRing.thy
src/HOL/Algebra/Ring.thy
src/HOL/Algebra/RingHom.thy
src/HOL/Algebra/Sylow.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Algebra/document/root.tex
src/HOL/IsaMakefile
     1.1 --- a/NEWS	Fri Aug 01 17:41:37 2008 +0200
     1.2 +++ b/NEWS	Fri Aug 01 18:10:52 2008 +0200
     1.3 @@ -142,7 +142,8 @@
     1.4  least_carrier ~> least_closed
     1.5  greatest_carrier ~> greatest_closed
     1.6  greatest_Lower_above ~> greatest_Lower_below
     1.7 -
     1.8 +one_zero ~> carrier_one_zero
     1.9 +one_not_zero ~> carrier_one_not_zero  (collision with assumption)
    1.10  
    1.11  *** HOL-NSA ***
    1.12  
     2.1 --- a/src/HOL/Algebra/AbelCoset.thy	Fri Aug 01 17:41:37 2008 +0200
     2.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Fri Aug 01 18:10:52 2008 +0200
     2.3 @@ -9,9 +9,9 @@
     2.4  begin
     2.5  
     2.6  
     2.7 -section {* More Lifting from Groups to Abelian Groups *}
     2.8 +subsection {* More Lifting from Groups to Abelian Groups *}
     2.9  
    2.10 -subsection {* Definitions *}
    2.11 +subsubsection {* Definitions *}
    2.12  
    2.13  text {* Hiding @{text "<+>"} from @{theory Sum_Type} until I come
    2.14    up with better syntax here *}
    2.15 @@ -102,7 +102,7 @@
    2.16  by (fold a_inv_def)
    2.17  
    2.18  
    2.19 -subsection {* Cosets *}
    2.20 +subsubsection {* Cosets *}
    2.21  
    2.22  lemma (in abelian_group) a_coset_add_assoc:
    2.23       "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
    2.24 @@ -178,7 +178,7 @@
    2.25  *)
    2.26  
    2.27  
    2.28 -subsection {* Subgroups *}
    2.29 +subsubsection {* Subgroups *}
    2.30  
    2.31  locale additive_subgroup = var H + struct G +
    2.32    assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    2.33 @@ -214,9 +214,7 @@
    2.34      folded a_inv_def, simplified monoid_record_simps])
    2.35  
    2.36  
    2.37 -subsection {* Normal additive subgroups *}
    2.38 -
    2.39 -subsubsection {* Definition of @{text "abelian_subgroup"} *}
    2.40 +subsubsection {* Additive subgroups are normal *}
    2.41  
    2.42  text {* Every subgroup of an @{text "abelian_group"} is normal *}
    2.43  
    2.44 @@ -385,7 +383,7 @@
    2.45      folded set_add_def A_RCOSETS_def, simplified monoid_record_simps])
    2.46  
    2.47  
    2.48 -subsection {* Congruence Relation *}
    2.49 +subsubsection {* Congruence Relation *}
    2.50  
    2.51  lemma (in abelian_subgroup) a_equiv_rcong:
    2.52     shows "equiv (carrier G) (racong H)"
    2.53 @@ -446,7 +444,7 @@
    2.54      (fast intro!: additive_subgroup.a_subgroup)+
    2.55  
    2.56  
    2.57 -subsection {* Factorization *}
    2.58 +subsubsection {* Factorization *}
    2.59  
    2.60  lemmas A_FactGroup_defs = A_FactGroup_def FactGroup_def
    2.61  
    2.62 @@ -518,7 +516,7 @@
    2.63  text {* The isomorphism theorems have been omitted from lifting, at
    2.64    least for now *}
    2.65  
    2.66 -subsection{*The First Isomorphism Theorem*}
    2.67 +subsubsection{*The First Isomorphism Theorem*}
    2.68  
    2.69  text{*The quotient by the kernel of a homomorphism is isomorphic to the 
    2.70    range of that homomorphism.*}
    2.71 @@ -531,7 +529,7 @@
    2.72  by (rule a_kernel_def[unfolded kernel_def, simplified ring_record_simps])
    2.73  
    2.74  
    2.75 -subsection {* Homomorphisms *}
    2.76 +subsubsection {* Homomorphisms *}
    2.77  
    2.78  lemma abelian_group_homI:
    2.79    assumes "abelian_group G"
    2.80 @@ -640,12 +638,10 @@
    2.81  by (rule group_hom.FactGroup_iso[OF a_group_hom,
    2.82      folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
    2.83  
    2.84 -section {* Lemmas Lifted from CosetExt.thy *}
    2.85 +subsubsection {* Cosets *}
    2.86  
    2.87  text {* Not eveything from \texttt{CosetExt.thy} is lifted here. *}
    2.88  
    2.89 -subsection {* General Lemmas from \texttt{AlgebraExt.thy} *}
    2.90 -
    2.91  lemma (in additive_subgroup) a_Hcarr [simp]:
    2.92    assumes hH: "h \<in> H"
    2.93    shows "h \<in> carrier G"
    2.94 @@ -653,8 +649,6 @@
    2.95      simplified monoid_record_simps]) (rule hH)
    2.96  
    2.97  
    2.98 -subsection {* Lemmas for Right Cosets *}
    2.99 -
   2.100  lemma (in abelian_subgroup) a_elemrcos_carrier:
   2.101    assumes acarr: "a \<in> carrier G"
   2.102        and a': "a' \<in> H +> a"
   2.103 @@ -722,8 +716,6 @@
   2.104      folded a_r_coset_def, simplified monoid_record_simps]) (rule ycarr, rule repr)
   2.105  
   2.106  
   2.107 -subsection {* Lemmas for the Set of Right Cosets *}
   2.108 -
   2.109  lemma (in abelian_subgroup) a_rcosets_carrier:
   2.110    "X \<in> a_rcosets H \<Longrightarrow> X \<subseteq> carrier G"
   2.111  by (rule subgroup.rcosets_carrier [OF a_subgroup a_group,
   2.112 @@ -731,7 +723,7 @@
   2.113  
   2.114  
   2.115  
   2.116 -subsection {* Addition of Subgroups *}
   2.117 +subsubsection {* Addition of Subgroups *}
   2.118  
   2.119  lemma (in abelian_monoid) set_add_closed:
   2.120    assumes Acarr: "A \<subseteq> carrier G"
     3.1 --- a/src/HOL/Algebra/Bij.thy	Fri Aug 01 17:41:37 2008 +0200
     3.2 +++ b/src/HOL/Algebra/Bij.thy	Fri Aug 01 18:10:52 2008 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  theory Bij imports Group begin
     3.5  
     3.6  
     3.7 -section {* Bijections of a Set, Permutation Groups and Automorphism Groups *}
     3.8 +section {* Bijections of a Set, Permutation and Automorphism Groups *}
     3.9  
    3.10  constdefs
    3.11    Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set"
     4.1 --- a/src/HOL/Algebra/Congruence.thy	Fri Aug 01 17:41:37 2008 +0200
     4.2 +++ b/src/HOL/Algebra/Congruence.thy	Fri Aug 01 18:10:52 2008 +0200
     4.3 @@ -9,12 +9,13 @@
     4.4  
     4.5  section {* Objects *}
     4.6  
     4.7 -text {* Structure with a carrier set. *}
     4.8 +subsection {* Structure with Carrier Set. *}
     4.9  
    4.10  record 'a partial_object =
    4.11    carrier :: "'a set"
    4.12  
    4.13 -text {* Dito with equivalence relation *}
    4.14 +
    4.15 +subsection {* Structure with Carrier and Equivalence Relation @{text eq} *}
    4.16  
    4.17  record 'a eq_object = "'a partial_object" +
    4.18    eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".=\<index>" 50)
    4.19 @@ -45,15 +46,14 @@
    4.20    "x .\<notin>\<index> A" == "~(x .\<in>\<index> A)"
    4.21    "A {.\<noteq>}\<index> B" == "~(A {.=}\<index> B)"
    4.22  
    4.23 -
    4.24 -section {* Equivalence Relations *}
    4.25 -
    4.26  locale equivalence =
    4.27    fixes S (structure)
    4.28    assumes refl [simp, intro]: "x \<in> carrier S \<Longrightarrow> x .= x"
    4.29      and sym [sym]: "\<lbrakk> x .= y; x \<in> carrier S; y \<in> carrier S \<rbrakk> \<Longrightarrow> y .= x"
    4.30      and trans [trans]: "\<lbrakk> x .= y; y .= z; x \<in> carrier S; y \<in> carrier S; z \<in> carrier S \<rbrakk> \<Longrightarrow> x .= z"
    4.31  
    4.32 +(* Lemmas by Stephan Hohe *)
    4.33 +
    4.34  lemma elemI:
    4.35    fixes R (structure)
    4.36    assumes "a' \<in> A" and "a .= a'"
    4.37 @@ -205,6 +205,7 @@
    4.38  by fast
    4.39  
    4.40  (* FIXME: the following two required in Isabelle 2008, not Isabelle 2007 *)
    4.41 +(* alternatively, could declare lemmas [trans] = ssubst [where 'a = "'a set"] *)
    4.42  
    4.43  lemma (in equivalence) equal_set_eq_trans [trans]:
    4.44    assumes AB: "A = B" and BC: "B {.=} C"
    4.45 @@ -216,6 +217,7 @@
    4.46    shows "A {.=} C"
    4.47    using AB BC by simp
    4.48  
    4.49 +
    4.50  lemma (in equivalence) set_eq_trans [trans]:
    4.51    assumes AB: "A {.=} B" and BC: "B {.=} C"
    4.52      and carr: "A \<subseteq> carrier S"  "B \<subseteq> carrier S"  "C \<subseteq> carrier S"
     5.1 --- a/src/HOL/Algebra/Coset.thy	Fri Aug 01 17:41:37 2008 +0200
     5.2 +++ b/src/HOL/Algebra/Coset.thy	Fri Aug 01 18:10:52 2008 +0200
     5.3 @@ -4,7 +4,7 @@
     5.4                  Stephan Hohe
     5.5  *)
     5.6  
     5.7 -theory Coset imports Group Exponent begin
     5.8 +theory Coset imports Group begin
     5.9  
    5.10  
    5.11  section {*Cosets and Quotient Groups*}
     6.1 --- a/src/HOL/Algebra/Divisibility.thy	Fri Aug 01 17:41:37 2008 +0200
     6.2 +++ b/src/HOL/Algebra/Divisibility.thy	Fri Aug 01 18:10:52 2008 +0200
     6.3 @@ -3,14 +3,16 @@
     6.4    Id:        $Id$
     6.5    Author:    Clemens Ballarin, started 18 July 2008
     6.6  
     6.7 -Based on work by Stefan Hohe.
     6.8 +Based on work by Stephan Hohe.
     6.9  *)
    6.10  
    6.11  theory Divisibility
    6.12  imports Permutation Coset Group
    6.13  begin
    6.14  
    6.15 -subsection {* Monoid with cancelation law *}
    6.16 +section {* Factorial Monoids *}
    6.17 +
    6.18 +subsection {* Monoids with Cancellation Law *}
    6.19  
    6.20  locale monoid_cancel = monoid +
    6.21    assumes l_cancel: 
    6.22 @@ -56,7 +58,7 @@
    6.23  by unfold_locales
    6.24  
    6.25  
    6.26 -subsection {* Products of units in monoids *}
    6.27 +subsection {* Products of Units in Monoids *}
    6.28  
    6.29  lemma (in monoid) Units_m_closed[simp, intro]:
    6.30    assumes h1unit: "h1 \<in> Units G" and h2unit: "h2 \<in> Units G"
    6.31 @@ -150,7 +152,7 @@
    6.32        show "a \<in> Units G" by (simp add: Units_def, fast)
    6.33  qed
    6.34  
    6.35 -subsection {* Divisibility and association *}
    6.36 +subsection {* Divisibility and Association *}
    6.37  
    6.38  subsubsection {* Function definitions *}
    6.39  
    6.40 @@ -811,7 +813,7 @@
    6.41  by (intro properfactor_trans2[OF ab] divides_prod_l, simp+)
    6.42  
    6.43  
    6.44 -subsection {* Irreducible elements and primes *}
    6.45 +subsection {* Irreducible Elements and Primes *}
    6.46  
    6.47  subsubsection {* Irreducible elements *}
    6.48  
    6.49 @@ -1031,11 +1033,7 @@
    6.50  qed
    6.51  
    6.52  
    6.53 -subsection {* Factorization and factorial monoids *}
    6.54 -
    6.55 -(*
    6.56 -hide (open) const mult     (* Multiset.mult, conflicting with monoid.mult *)
    6.57 -*)
    6.58 +subsection {* Factorization and Factorial Monoids *}
    6.59  
    6.60  subsubsection {* Function definitions *}
    6.61  
    6.62 @@ -1891,7 +1889,7 @@
    6.63  qed (blast intro: factors_wfactors wfactors_unique)
    6.64  
    6.65  
    6.66 -subsection {* Factorizations as multisets *}
    6.67 +subsection {* Factorizations as Multisets *}
    6.68  
    6.69  text {* Gives useful operations like intersection *}
    6.70  
    6.71 @@ -2370,7 +2368,7 @@
    6.72  qed
    6.73  
    6.74  
    6.75 -subsection {* Irreducible elements are prime *}
    6.76 +subsection {* Irreducible Elements are Prime *}
    6.77  
    6.78  lemma (in factorial_monoid) irreducible_is_prime:
    6.79    assumes pirr: "irreducible G p"
    6.80 @@ -2610,7 +2608,7 @@
    6.81  qed
    6.82  
    6.83  
    6.84 -subsection {* Greatest common divisors and lowest common multiples *}
    6.85 +subsection {* Greatest Common Divisors and Lowest Common Multiples *}
    6.86  
    6.87  subsubsection {* Definitions *}
    6.88  
    6.89 @@ -2907,7 +2905,7 @@
    6.90  qed
    6.91  
    6.92  
    6.93 -subsection {* Conditions for factoriality *}
    6.94 +subsection {* Conditions for Factoriality *}
    6.95  
    6.96  subsubsection {* Gcd condition *}
    6.97  
    6.98 @@ -3891,7 +3889,7 @@
    6.99  qed
   6.100  
   6.101  
   6.102 -subsection {* Factoriality theorems *}
   6.103 +subsection {* Factoriality Theorems *}
   6.104  
   6.105  theorem factorial_condition_one: (* Jacobson theorem 2.21 *)
   6.106    shows "(divisor_chain_condition_monoid G \<and> primeness_condition_monoid G) = 
     7.1 --- a/src/HOL/Algebra/Exponent.thy	Fri Aug 01 17:41:37 2008 +0200
     7.2 +++ b/src/HOL/Algebra/Exponent.thy	Fri Aug 01 18:10:52 2008 +0200
     7.3 @@ -9,12 +9,15 @@
     7.4  imports Main Primes Binomial
     7.5  begin
     7.6  
     7.7 -section {*The Combinatorial Argument Underlying the First Sylow Theorem*}
     7.8 +section {*Sylow's Theorem*}
     7.9 +
    7.10 +subsection {*The Combinatorial Argument Underlying the First Sylow Theorem*}
    7.11 +
    7.12  definition exponent :: "nat => nat => nat" where
    7.13  "exponent p s == if prime p then (GREATEST r. p^r dvd s) else 0"
    7.14  
    7.15  
    7.16 -subsection{*Prime Theorems*}
    7.17 +text{*Prime Theorems*}
    7.18  
    7.19  lemma prime_imp_one_less: "prime p ==> Suc 0 < p"
    7.20  by (unfold prime_def, force)
    7.21 @@ -106,7 +109,7 @@
    7.22  done
    7.23  
    7.24  
    7.25 -subsection{*Exponent Theorems*}
    7.26 +text{*Exponent Theorems*}
    7.27  
    7.28  lemma exponent_ge [rule_format]:
    7.29    "[|p^k dvd n;  prime p;  0<n|] ==> k <= exponent p n"
    7.30 @@ -186,7 +189,7 @@
    7.31  done
    7.32  
    7.33  
    7.34 -subsection{*Main Combinatorial Argument*}
    7.35 +text{*Main Combinatorial Argument*}
    7.36  
    7.37  lemma le_extend_mult: "[| c > 0; a <= b |] ==> a <= b * (c::nat)"
    7.38  apply (rule_tac P = "%x. x <= b * c" in subst)
     8.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Fri Aug 01 17:41:37 2008 +0200
     8.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Fri Aug 01 18:10:52 2008 +0200
     8.3 @@ -8,10 +8,9 @@
     8.4  theory FiniteProduct imports Group begin
     8.5  
     8.6  
     8.7 -section {* Product Operator for Commutative Monoids *}
     8.8 +subsection {* Product Operator for Commutative Monoids *}
     8.9  
    8.10 -
    8.11 -subsection {* Inductive Definition of a Relation for Products over Sets *}
    8.12 +subsubsection {* Inductive Definition of a Relation for Products over Sets *}
    8.13  
    8.14  text {* Instantiation of locale @{text LC} of theory @{text Finite_Set} is not
    8.15    possible, because here we have explicit typing rules like 
    8.16 @@ -62,7 +61,7 @@
    8.17  qed
    8.18  
    8.19  
    8.20 -subsection {* Left-Commutative Operations *}
    8.21 +text {* Left-Commutative Operations *}
    8.22  
    8.23  locale LCD =
    8.24    fixes B :: "'b set"
    8.25 @@ -231,7 +230,7 @@
    8.26    foldSetD_closed [rule del]
    8.27  
    8.28  
    8.29 -subsection {* Commutative Monoids *}
    8.30 +text {* Commutative Monoids *}
    8.31  
    8.32  text {*
    8.33    We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
    8.34 @@ -286,7 +285,7 @@
    8.35      left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff)
    8.36  
    8.37  
    8.38 -subsection {* Products over Finite Sets *}
    8.39 +subsubsection {* Products over Finite Sets *}
    8.40  
    8.41  constdefs (structure G)
    8.42    finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
     9.1 --- a/src/HOL/Algebra/Ideal.thy	Fri Aug 01 17:41:37 2008 +0200
     9.2 +++ b/src/HOL/Algebra/Ideal.thy	Fri Aug 01 18:10:52 2008 +0200
     9.3 @@ -10,7 +10,9 @@
     9.4  
     9.5  section {* Ideals *}
     9.6  
     9.7 -subsection {* General definition *}
     9.8 +subsection {* Definitions *}
     9.9 +
    9.10 +subsubsection {* General definition *}
    9.11  
    9.12  locale ideal = additive_subgroup I R + ring R +
    9.13    assumes I_l_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
    9.14 @@ -44,14 +46,14 @@
    9.15    done
    9.16  qed
    9.17  
    9.18 -subsection {* Ideals Generated by a Subset of @{term [locale=ring] "carrier R"} *}
    9.19 +subsubsection {* Ideals Generated by a Subset of @{term [locale=ring] "carrier R"} *}
    9.20  
    9.21  constdefs (structure R)
    9.22    genideal :: "('a, 'b) ring_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set"  ("Idl\<index> _" [80] 79)
    9.23    "genideal R S \<equiv> Inter {I. ideal I R \<and> S \<subseteq> I}"
    9.24  
    9.25  
    9.26 -subsection {* Principal Ideals *}
    9.27 +subsubsection {* Principal Ideals *}
    9.28  
    9.29  locale principalideal = ideal +
    9.30    assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"
    9.31 @@ -70,7 +72,7 @@
    9.32    show ?thesis  by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate)
    9.33  qed
    9.34  
    9.35 -subsection {* Maximal Ideals *}
    9.36 +subsubsection {* Maximal Ideals *}
    9.37  
    9.38  locale maximalideal = ideal +
    9.39    assumes I_notcarr: "carrier R \<noteq> I"
    9.40 @@ -92,7 +94,7 @@
    9.41      (rule is_ideal, rule I_notcarr, rule I_maximal)
    9.42  qed
    9.43  
    9.44 -subsection {* Prime Ideals *}
    9.45 +subsubsection {* Prime Ideals *}
    9.46  
    9.47  locale primeideal = ideal + cring +
    9.48    assumes I_notcarr: "carrier R \<noteq> I"
    9.49 @@ -138,8 +140,6 @@
    9.50      done
    9.51  qed
    9.52  
    9.53 -section {* Properties of Ideals *}
    9.54 -
    9.55  subsection {* Special Ideals *}
    9.56  
    9.57  lemma (in ring) zeroideal:
    9.58 @@ -223,8 +223,6 @@
    9.59  done
    9.60  qed
    9.61  
    9.62 -subsubsection {* Intersection of a Set of Ideals *}
    9.63 -
    9.64  text {* The intersection of any Number of Ideals is again
    9.65          an Ideal in @{term R} *}
    9.66  lemma (in ring) i_Intersect:
    9.67 @@ -352,8 +350,6 @@
    9.68  subsection {* Ideals generated by a subset of @{term [locale=ring]
    9.69    "carrier R"} *}
    9.70  
    9.71 -subsubsection {* Generation of Ideals in General Rings *}
    9.72 -
    9.73  text {* @{term genideal} generates an ideal *}
    9.74  lemma (in ring) genideal_ideal:
    9.75    assumes Scarr: "S \<subseteq> carrier R"
    9.76 @@ -455,7 +451,7 @@
    9.77  qed
    9.78  
    9.79  
    9.80 -subsubsection {* Generation of Principal Ideals in Commutative Rings *}
    9.81 +text {* Generation of Principal Ideals in Commutative Rings *}
    9.82  
    9.83  constdefs (structure R)
    9.84    cgenideal :: "('a, 'b) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a set"  ("PIdl\<index> _" [80] 79)
    9.85 @@ -873,7 +869,7 @@
    9.86    qed
    9.87  qed
    9.88  
    9.89 -subsection {* Derived Theorems Involving Ideals *}
    9.90 +subsection {* Derived Theorems *}
    9.91  
    9.92  --"A non-zero cring that has only the two trivial ideals is a field"
    9.93  lemma (in cring) trivialideals_fieldI:
    10.1 --- a/src/HOL/Algebra/IntRing.thy	Fri Aug 01 17:41:37 2008 +0200
    10.2 +++ b/src/HOL/Algebra/IntRing.thy	Fri Aug 01 18:10:52 2008 +0200
    10.3 @@ -5,7 +5,7 @@
    10.4  *)
    10.5  
    10.6  theory IntRing
    10.7 -imports QuotRing Int
    10.8 +imports QuotRing Int Primes
    10.9  begin
   10.10  
   10.11  
   10.12 @@ -62,10 +62,7 @@
   10.13  done
   10.14  
   10.15  
   10.16 -
   10.17 -subsection {* The Set of Integers as Algebraic Structure *}
   10.18 -
   10.19 -subsubsection {* Definition of @{text "\<Z>"} *}
   10.20 +subsection {* @{text "\<Z>"}: The Set of Integers as Algebraic Structure *}
   10.21  
   10.22  constdefs
   10.23    int_ring :: "int ring" ("\<Z>")
   10.24 @@ -94,7 +91,7 @@
   10.25   apply (unfold int_ring_def, simp+)
   10.26  done
   10.27  *)
   10.28 -subsubsection {* Interpretations *}
   10.29 +subsection {* Interpretations *}
   10.30  
   10.31  text {* Since definitions of derived operations are global, their
   10.32    interpretation needs to be done as early as possible --- that is,
   10.33 @@ -254,7 +251,7 @@
   10.34    by unfold_locales clarsimp
   10.35  
   10.36  
   10.37 -subsubsection {* Generated Ideals of @{text "\<Z>"} *}
   10.38 +subsection {* Generated Ideals of @{text "\<Z>"} *}
   10.39  
   10.40  lemma int_Idl:
   10.41    "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"
   10.42 @@ -342,7 +339,7 @@
   10.43  qed
   10.44  
   10.45  
   10.46 -subsubsection {* Ideals and Divisibility *}
   10.47 +subsection {* Ideals and Divisibility *}
   10.48  
   10.49  lemma int_Idl_subset_ideal:
   10.50    "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})"
   10.51 @@ -376,7 +373,7 @@
   10.52  done
   10.53  
   10.54  
   10.55 -subsubsection {* Ideals and the Modulus *}
   10.56 +subsection {* Ideals and the Modulus *}
   10.57  
   10.58  constdefs
   10.59     ZMod :: "int => int => int set"
   10.60 @@ -459,7 +456,7 @@
   10.61  by (rule, erule ZMod_imp_zmod, erule zmod_imp_ZMod)
   10.62  
   10.63  
   10.64 -subsubsection {* Factorization *}
   10.65 +subsection {* Factorization *}
   10.66  
   10.67  constdefs
   10.68    ZFact :: "int \<Rightarrow> int set ring"
    11.1 --- a/src/HOL/Algebra/Lattice.thy	Fri Aug 01 17:41:37 2008 +0200
    11.2 +++ b/src/HOL/Algebra/Lattice.thy	Fri Aug 01 18:10:52 2008 +0200
    11.3 @@ -4,7 +4,7 @@
    11.4    Author:    Clemens Ballarin, started 7 November 2003
    11.5    Copyright: Clemens Ballarin
    11.6  
    11.7 -Most congruence rules by Stefan Hohe.
    11.8 +Most congruence rules by Stephan Hohe.
    11.9  *)
   11.10  
   11.11  theory Lattice imports Congruence begin
   11.12 @@ -964,7 +964,7 @@
   11.13  qed
   11.14  
   11.15  
   11.16 -subsection {* Complete lattices *}
   11.17 +subsection {* Complete Lattices *}
   11.18  
   11.19  locale weak_complete_lattice = weak_lattice +
   11.20    assumes sup_exists:
   11.21 @@ -1115,12 +1115,7 @@
   11.22  end
   11.23  
   11.24  
   11.25 -subsubsection {* Upper and lower bounds of a set *}
   11.26 -
   11.27 -(* all relevant lemmas are global and already proved above *)
   11.28 -
   11.29 -
   11.30 -subsubsection {* Least and greatest, as predicate *}
   11.31 +text {* Least and greatest, as predicate *}
   11.32  
   11.33  lemma (in partial_order) least_unique:
   11.34    "[| least L x A; least L y A |] ==> x = y"
   11.35 @@ -1131,7 +1126,7 @@
   11.36    using weak_greatest_unique unfolding eq_is_equal .
   11.37  
   11.38  
   11.39 -subsection {* Lattices *}
   11.40 +text {* Lattices *}
   11.41  
   11.42  locale upper_semilattice = partial_order +
   11.43    assumes sup_of_two_exists:
   11.44 @@ -1150,7 +1145,7 @@
   11.45  locale lattice = upper_semilattice + lower_semilattice
   11.46  
   11.47  
   11.48 -subsubsection {* Supremum *}
   11.49 +text {* Supremum *}
   11.50  
   11.51  declare (in partial_order) weak_sup_of_singleton [simp del]
   11.52  
   11.53 @@ -1169,7 +1164,7 @@
   11.54    using weak_join_assoc L unfolding eq_is_equal .
   11.55  
   11.56  
   11.57 -subsubsection {* Infimum *}
   11.58 +text {* Infimum *}
   11.59  
   11.60  declare (in partial_order) weak_inf_of_singleton [simp del]
   11.61  
   11.62 @@ -1190,7 +1185,7 @@
   11.63    using weak_meet_assoc L unfolding eq_is_equal .
   11.64  
   11.65  
   11.66 -subsection {* Total Orders *}
   11.67 +text {* Total Orders *}
   11.68  
   11.69  locale total_order = partial_order +
   11.70    assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   11.71 @@ -1211,7 +1206,7 @@
   11.72    by unfold_locales (auto intro: sup_of_two_exists inf_of_two_exists)
   11.73  
   11.74  
   11.75 -subsection {* Complete lattices *}
   11.76 +text {* Complete lattices *}
   11.77  
   11.78  locale complete_lattice = lattice +
   11.79    assumes sup_exists:
   11.80 @@ -1280,7 +1275,7 @@
   11.81  
   11.82  subsection {* Examples *}
   11.83  
   11.84 -subsubsection {* Powerset of a Set is a Complete Lattice *}
   11.85 +subsubsection {* The Powerset of a Set is a Complete Lattice *}
   11.86  
   11.87  theorem powerset_is_complete_lattice:
   11.88    "complete_lattice (| carrier = Pow A, eq = op =, le = op \<subseteq> |)"
    12.1 --- a/src/HOL/Algebra/QuotRing.thy	Fri Aug 01 17:41:37 2008 +0200
    12.2 +++ b/src/HOL/Algebra/QuotRing.thy	Fri Aug 01 18:10:52 2008 +0200
    12.3 @@ -4,12 +4,12 @@
    12.4    Author:    Stephan Hohe
    12.5  *)
    12.6  
    12.7 -header {* Quotient Rings *}
    12.8 -
    12.9  theory QuotRing
   12.10  imports RingHom
   12.11  begin
   12.12  
   12.13 +section {* Quotient Rings *}
   12.14 +
   12.15  subsection {* Multiplication on Cosets *}
   12.16  
   12.17  constdefs (structure R)
    13.1 --- a/src/HOL/Algebra/Ring.thy	Fri Aug 01 17:41:37 2008 +0200
    13.2 +++ b/src/HOL/Algebra/Ring.thy	Fri Aug 01 18:10:52 2008 +0200
    13.3 @@ -9,7 +9,9 @@
    13.4  uses ("ringsimp.ML") begin
    13.5  
    13.6  
    13.7 -section {* Abelian Groups *}
    13.8 +section {* The Algebraic Hierarchy of Rings *}
    13.9 +
   13.10 +subsection {* Abelian Groups *}
   13.11  
   13.12  record 'a ring = "'a monoid" +
   13.13    zero :: 'a ("\<zero>\<index>")
   13.14 @@ -341,9 +343,7 @@
   13.15  *)
   13.16  
   13.17  
   13.18 -section {* The Algebraic Hierarchy of Rings *}
   13.19 -
   13.20 -subsection {* Basic Definitions *}
   13.21 +subsection {* Rings: Basic Definitions *}
   13.22  
   13.23  locale ring = abelian_group R + monoid R +
   13.24    assumes l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
   13.25 @@ -554,13 +554,13 @@
   13.26        show "\<one> = \<zero>" by simp
   13.27  qed
   13.28  
   13.29 -lemma (in ring) one_zero:
   13.30 +lemma (in ring) carrier_one_zero:
   13.31    shows "(carrier R = {\<zero>}) = (\<one> = \<zero>)"
   13.32    by (rule, erule one_zeroI, erule one_zeroD)
   13.33  
   13.34 -lemma (in ring) one_not_zero:
   13.35 +lemma (in ring) carrier_one_not_zero:
   13.36    shows "(carrier R \<noteq> {\<zero>}) = (\<one> \<noteq> \<zero>)"
   13.37 -  by (simp add: one_zero)
   13.38 +  by (simp add: carrier_one_zero)
   13.39  
   13.40  text {* Two examples for use of method algebra *}
   13.41  
   13.42 @@ -588,7 +588,7 @@
   13.43  
   13.44  subsubsection {* Sums over Finite Sets *}
   13.45  
   13.46 -lemma (in cring) finsum_ldistr:
   13.47 +lemma (in ring) finsum_ldistr:
   13.48    "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
   13.49     finsum R f A \<otimes> a = finsum R (%i. f i \<otimes> a) A"
   13.50  proof (induct set: finite)
   13.51 @@ -597,7 +597,7 @@
   13.52    case (insert x F) then show ?case by (simp add: Pi_def l_distr)
   13.53  qed
   13.54  
   13.55 -lemma (in cring) finsum_rdistr:
   13.56 +lemma (in ring) finsum_rdistr:
   13.57    "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
   13.58     a \<otimes> finsum R f A = finsum R (%i. a \<otimes> f i) A"
   13.59  proof (induct set: finite)
    14.1 --- a/src/HOL/Algebra/RingHom.thy	Fri Aug 01 17:41:37 2008 +0200
    14.2 +++ b/src/HOL/Algebra/RingHom.thy	Fri Aug 01 18:10:52 2008 +0200
    14.3 @@ -99,7 +99,7 @@
    14.4      (rule R.is_cring, rule S.is_cring, rule homh)
    14.5  qed
    14.6  
    14.7 -subsection {* The kernel of a ring homomorphism *}
    14.8 +subsection {* The Kernel of a Ring Homomorphism *}
    14.9  
   14.10  --"the kernel of a ring homomorphism is an ideal"
   14.11  lemma (in ring_hom_ring) kernel_is_ideal:
    15.1 --- a/src/HOL/Algebra/Sylow.thy	Fri Aug 01 17:41:37 2008 +0200
    15.2 +++ b/src/HOL/Algebra/Sylow.thy	Fri Aug 01 18:10:52 2008 +0200
    15.3 @@ -3,10 +3,7 @@
    15.4      Author:     Florian Kammueller, with new proofs by L C Paulson
    15.5  *)
    15.6  
    15.7 -theory Sylow imports Coset begin
    15.8 -
    15.9 -
   15.10 -section {* Sylow's Theorem *}
   15.11 +theory Sylow imports Coset Exponent begin
   15.12  
   15.13  text {*
   15.14    See also \cite{Kammueller-Paulson:1999}.
    16.1 --- a/src/HOL/Algebra/UnivPoly.thy	Fri Aug 01 17:41:37 2008 +0200
    16.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Fri Aug 01 18:10:52 2008 +0200
    16.3 @@ -3,9 +3,11 @@
    16.4    Id:        $Id$
    16.5    Author:    Clemens Ballarin, started 9 December 1996
    16.6    Copyright: Clemens Ballarin
    16.7 +
    16.8 +Contributions by Jesus Aransay.
    16.9  *)
   16.10  
   16.11 -theory UnivPoly imports Module begin
   16.12 +theory UnivPoly imports Module RingHom begin
   16.13  
   16.14  
   16.15  section {* Univariate Polynomials *}
   16.16 @@ -77,19 +79,16 @@
   16.17    "f \<in> up R ==> f n \<in> carrier R"
   16.18    by (simp add: up_def Pi_def)
   16.19  
   16.20 -lemma (in cring) bound_upD [dest]:
   16.21 -  "f \<in> up R ==> EX n. bound \<zero> n f"
   16.22 -  by (simp add: up_def)
   16.23 +context ring
   16.24 +begin
   16.25 +
   16.26 +lemma bound_upD [dest]: "f \<in> up R ==> EX n. bound \<zero> n f" by (simp add: up_def)
   16.27  
   16.28 -lemma (in cring) up_one_closed:
   16.29 -   "(%n. if n = 0 then \<one> else \<zero>) \<in> up R"
   16.30 -  using up_def by force
   16.31 +lemma up_one_closed: "(%n. if n = 0 then \<one> else \<zero>) \<in> up R" using up_def by force
   16.32  
   16.33 -lemma (in cring) up_smult_closed:
   16.34 -  "[| a \<in> carrier R; p \<in> up R |] ==> (%i. a \<otimes> p i) \<in> up R"
   16.35 -  by force
   16.36 +lemma up_smult_closed: "[| a \<in> carrier R; p \<in> up R |] ==> (%i. a \<otimes> p i) \<in> up R" by force
   16.37  
   16.38 -lemma (in cring) up_add_closed:
   16.39 +lemma up_add_closed:
   16.40    "[| p \<in> up R; q \<in> up R |] ==> (%i. p i \<oplus> q i) \<in> up R"
   16.41  proof
   16.42    fix n
   16.43 @@ -112,7 +111,7 @@
   16.44    qed
   16.45  qed
   16.46  
   16.47 -lemma (in cring) up_a_inv_closed:
   16.48 +lemma up_a_inv_closed:
   16.49    "p \<in> up R ==> (%i. \<ominus> (p i)) \<in> up R"
   16.50  proof
   16.51    assume R: "p \<in> up R"
   16.52 @@ -121,7 +120,7 @@
   16.53    then show "EX n. bound \<zero> n (%i. \<ominus> p i)" by auto
   16.54  qed auto
   16.55  
   16.56 -lemma (in cring) up_mult_closed:
   16.57 +lemma up_mult_closed:
   16.58    "[| p \<in> up R; q \<in> up R |] ==>
   16.59    (%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)) \<in> up R"
   16.60  proof
   16.61 @@ -161,6 +160,8 @@
   16.62    qed
   16.63  qed
   16.64  
   16.65 +end
   16.66 +
   16.67  
   16.68  subsection {* Effect of Operations on Coefficients *}
   16.69  
   16.70 @@ -168,19 +169,45 @@
   16.71    fixes R (structure) and P (structure)
   16.72    defines P_def: "P == UP R"
   16.73  
   16.74 +locale UP_ring = UP + ring R
   16.75 +
   16.76  locale UP_cring = UP + cring R
   16.77  
   16.78 -locale UP_domain = UP_cring + "domain" R
   16.79 +interpretation UP_cring < UP_ring
   16.80 +  by (rule P_def) intro_locales
   16.81 +
   16.82 +locale UP_domain = UP + "domain" R
   16.83  
   16.84 -text {*
   16.85 -  Temporarily declare @{thm [locale=UP] P_def} as simp rule.
   16.86 -*}
   16.87 +interpretation UP_domain < UP_cring
   16.88 +  by (rule P_def) intro_locales
   16.89 +
   16.90 +context UP
   16.91 +begin
   16.92 +
   16.93 +text {*Temporarily declare @{thm [locale=UP] P_def} as simp rule.*}
   16.94 +
   16.95 +declare P_def [simp]
   16.96  
   16.97 -declare (in UP) P_def [simp]
   16.98 +lemma up_eqI:
   16.99 +  assumes prem: "!!n. coeff P p n = coeff P q n" and R: "p \<in> carrier P" "q \<in> carrier P"
  16.100 +  shows "p = q"
  16.101 +proof
  16.102 +  fix x
  16.103 +  from prem and R show "p x = q x" by (simp add: UP_def)
  16.104 +qed
  16.105  
  16.106 -lemma (in UP_cring) coeff_monom [simp]:
  16.107 -  "a \<in> carrier R ==>
  16.108 -  coeff P (monom P a m) n = (if m=n then a else \<zero>)"
  16.109 +lemma coeff_closed [simp]:
  16.110 +  "p \<in> carrier P ==> coeff P p n \<in> carrier R" by (auto simp add: UP_def)
  16.111 +
  16.112 +end
  16.113 +
  16.114 +context UP_ring 
  16.115 +begin
  16.116 +
  16.117 +(* Theorems generalised to rings by Jesus Aransay. *)
  16.118 +
  16.119 +lemma coeff_monom [simp]:
  16.120 +  "a \<in> carrier R ==> coeff P (monom P a m) n = (if m=n then a else \<zero>)"
  16.121  proof -
  16.122    assume R: "a \<in> carrier R"
  16.123    then have "(%n. if n = m then a else \<zero>) \<in> up R"
  16.124 @@ -188,86 +215,69 @@
  16.125    with R show ?thesis by (simp add: UP_def)
  16.126  qed
  16.127  
  16.128 -lemma (in UP_cring) coeff_zero [simp]:
  16.129 -  "coeff P \<zero>\<^bsub>P\<^esub> n = \<zero>"
  16.130 -  by (auto simp add: UP_def)
  16.131 +lemma coeff_zero [simp]: "coeff P \<zero>\<^bsub>P\<^esub> n = \<zero>" by (auto simp add: UP_def)
  16.132  
  16.133 -lemma (in UP_cring) coeff_one [simp]:
  16.134 -  "coeff P \<one>\<^bsub>P\<^esub> n = (if n=0 then \<one> else \<zero>)"
  16.135 +lemma coeff_one [simp]: "coeff P \<one>\<^bsub>P\<^esub> n = (if n=0 then \<one> else \<zero>)"
  16.136    using up_one_closed by (simp add: UP_def)
  16.137  
  16.138 -lemma (in UP_cring) coeff_smult [simp]:
  16.139 -  "[| a \<in> carrier R; p \<in> carrier P |] ==>
  16.140 -  coeff P (a \<odot>\<^bsub>P\<^esub> p) n = a \<otimes> coeff P p n"
  16.141 +lemma coeff_smult [simp]:
  16.142 +  "[| a \<in> carrier R; p \<in> carrier P |] ==> coeff P (a \<odot>\<^bsub>P\<^esub> p) n = a \<otimes> coeff P p n"
  16.143    by (simp add: UP_def up_smult_closed)
  16.144  
  16.145 -lemma (in UP_cring) coeff_add [simp]:
  16.146 -  "[| p \<in> carrier P; q \<in> carrier P |] ==>
  16.147 -  coeff P (p \<oplus>\<^bsub>P\<^esub> q) n = coeff P p n \<oplus> coeff P q n"
  16.148 +lemma coeff_add [simp]:
  16.149 +  "[| p \<in> carrier P; q \<in> carrier P |] ==> coeff P (p \<oplus>\<^bsub>P\<^esub> q) n = coeff P p n \<oplus> coeff P q n"
  16.150    by (simp add: UP_def up_add_closed)
  16.151  
  16.152 -lemma (in UP_cring) coeff_mult [simp]:
  16.153 -  "[| p \<in> carrier P; q \<in> carrier P |] ==>
  16.154 -  coeff P (p \<otimes>\<^bsub>P\<^esub> q) n = (\<Oplus>i \<in> {..n}. coeff P p i \<otimes> coeff P q (n-i))"
  16.155 +lemma coeff_mult [simp]:
  16.156 +  "[| p \<in> carrier P; q \<in> carrier P |] ==> coeff P (p \<otimes>\<^bsub>P\<^esub> q) n = (\<Oplus>i \<in> {..n}. coeff P p i \<otimes> coeff P q (n-i))"
  16.157    by (simp add: UP_def up_mult_closed)
  16.158  
  16.159 -lemma (in UP) up_eqI:
  16.160 -  assumes prem: "!!n. coeff P p n = coeff P q n"
  16.161 -    and R: "p \<in> carrier P" "q \<in> carrier P"
  16.162 -  shows "p = q"
  16.163 -proof
  16.164 -  fix x
  16.165 -  from prem and R show "p x = q x" by (simp add: UP_def)
  16.166 -qed
  16.167 +end
  16.168  
  16.169  
  16.170 -subsection {* Polynomials Form a Commutative Ring. *}
  16.171 +subsection {* Polynomials Form a Ring. *}
  16.172 +
  16.173 +context UP_ring
  16.174 +begin
  16.175  
  16.176  text {* Operations are closed over @{term P}. *}
  16.177  
  16.178 -lemma (in UP_cring) UP_mult_closed [simp]:
  16.179 -  "[| p \<in> carrier P; q \<in> carrier P |] ==> p \<otimes>\<^bsub>P\<^esub> q \<in> carrier P"
  16.180 -  by (simp add: UP_def up_mult_closed)
  16.181 +lemma UP_mult_closed [simp]:
  16.182 +  "[| p \<in> carrier P; q \<in> carrier P |] ==> p \<otimes>\<^bsub>P\<^esub> q \<in> carrier P" by (simp add: UP_def up_mult_closed)
  16.183  
  16.184 -lemma (in UP_cring) UP_one_closed [simp]:
  16.185 -  "\<one>\<^bsub>P\<^esub> \<in> carrier P"
  16.186 -  by (simp add: UP_def up_one_closed)
  16.187 +lemma UP_one_closed [simp]:
  16.188 +  "\<one>\<^bsub>P\<^esub> \<in> carrier P" by (simp add: UP_def up_one_closed)
  16.189  
  16.190 -lemma (in UP_cring) UP_zero_closed [intro, simp]:
  16.191 -  "\<zero>\<^bsub>P\<^esub> \<in> carrier P"
  16.192 -  by (auto simp add: UP_def)
  16.193 +lemma UP_zero_closed [intro, simp]:
  16.194 +  "\<zero>\<^bsub>P\<^esub> \<in> carrier P" by (auto simp add: UP_def)
  16.195  
  16.196 -lemma (in UP_cring) UP_a_closed [intro, simp]:
  16.197 -  "[| p \<in> carrier P; q \<in> carrier P |] ==> p \<oplus>\<^bsub>P\<^esub> q \<in> carrier P"
  16.198 -  by (simp add: UP_def up_add_closed)
  16.199 -
  16.200 -lemma (in UP_cring) monom_closed [simp]:
  16.201 -  "a \<in> carrier R ==> monom P a n \<in> carrier P"
  16.202 -  by (auto simp add: UP_def up_def Pi_def)
  16.203 +lemma UP_a_closed [intro, simp]:
  16.204 +  "[| p \<in> carrier P; q \<in> carrier P |] ==> p \<oplus>\<^bsub>P\<^esub> q \<in> carrier P" by (simp add: UP_def up_add_closed)
  16.205  
  16.206 -lemma (in UP_cring) UP_smult_closed [simp]:
  16.207 -  "[| a \<in> carrier R; p \<in> carrier P |] ==> a \<odot>\<^bsub>P\<^esub> p \<in> carrier P"
  16.208 -  by (simp add: UP_def up_smult_closed)
  16.209 +lemma monom_closed [simp]:
  16.210 +  "a \<in> carrier R ==> monom P a n \<in> carrier P" by (auto simp add: UP_def up_def Pi_def)
  16.211  
  16.212 -lemma (in UP) coeff_closed [simp]:
  16.213 -  "p \<in> carrier P ==> coeff P p n \<in> carrier R"
  16.214 -  by (auto simp add: UP_def)
  16.215 +lemma UP_smult_closed [simp]:
  16.216 +  "[| a \<in> carrier R; p \<in> carrier P |] ==> a \<odot>\<^bsub>P\<^esub> p \<in> carrier P" by (simp add: UP_def up_smult_closed)
  16.217 +
  16.218 +end
  16.219  
  16.220  declare (in UP) P_def [simp del]
  16.221  
  16.222  text {* Algebraic ring properties *}
  16.223  
  16.224 -lemma (in UP_cring) UP_a_assoc:
  16.225 -  assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
  16.226 -  shows "(p \<oplus>\<^bsub>P\<^esub> q) \<oplus>\<^bsub>P\<^esub> r = p \<oplus>\<^bsub>P\<^esub> (q \<oplus>\<^bsub>P\<^esub> r)"
  16.227 -  by (rule up_eqI, simp add: a_assoc R, simp_all add: R)
  16.228 +context UP_ring
  16.229 +begin
  16.230  
  16.231 -lemma (in UP_cring) UP_l_zero [simp]:
  16.232 +lemma UP_a_assoc:
  16.233 +  assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
  16.234 +  shows "(p \<oplus>\<^bsub>P\<^esub> q) \<oplus>\<^bsub>P\<^esub> r = p \<oplus>\<^bsub>P\<^esub> (q \<oplus>\<^bsub>P\<^esub> r)" by (rule up_eqI, simp add: a_assoc R, simp_all add: R)
  16.235 +
  16.236 +lemma UP_l_zero [simp]:
  16.237    assumes R: "p \<in> carrier P"
  16.238 -  shows "\<zero>\<^bsub>P\<^esub> \<oplus>\<^bsub>P\<^esub> p = p"
  16.239 -  by (rule up_eqI, simp_all add: R)
  16.240 +  shows "\<zero>\<^bsub>P\<^esub> \<oplus>\<^bsub>P\<^esub> p = p" by (rule up_eqI, simp_all add: R)
  16.241  
  16.242 -lemma (in UP_cring) UP_l_neg_ex:
  16.243 +lemma UP_l_neg_ex:
  16.244    assumes R: "p \<in> carrier P"
  16.245    shows "EX q : carrier P. q \<oplus>\<^bsub>P\<^esub> p = \<zero>\<^bsub>P\<^esub>"
  16.246  proof -
  16.247 @@ -283,12 +293,17 @@
  16.248    qed (rule closed)
  16.249  qed
  16.250  
  16.251 -lemma (in UP_cring) UP_a_comm:
  16.252 +lemma UP_a_comm:
  16.253    assumes R: "p \<in> carrier P" "q \<in> carrier P"
  16.254 -  shows "p \<oplus>\<^bsub>P\<^esub> q = q \<oplus>\<^bsub>P\<^esub> p"
  16.255 -  by (rule up_eqI, simp add: a_comm R, simp_all add: R)
  16.256 +  shows "p \<oplus>\<^bsub>P\<^esub> q = q \<oplus>\<^bsub>P\<^esub> p" by (rule up_eqI, simp add: a_comm R, simp_all add: R)
  16.257 +
  16.258 +end
  16.259 +
  16.260  
  16.261 -lemma (in UP_cring) UP_m_assoc:
  16.262 +context UP_ring
  16.263 +begin
  16.264 +
  16.265 +lemma UP_m_assoc:
  16.266    assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
  16.267    shows "(p \<otimes>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>P\<^esub> r = p \<otimes>\<^bsub>P\<^esub> (q \<otimes>\<^bsub>P\<^esub> r)"
  16.268  proof (rule up_eqI)
  16.269 @@ -310,14 +325,51 @@
  16.270        with R show ?case
  16.271          by (simp cong: finsum_cong
  16.272               add: Suc_diff_le Pi_def l_distr r_distr m_assoc)
  16.273 -          (simp cong: finsum_cong add: Pi_def a_ac finsum_ldistr m_assoc)
  16.274 +           (simp cong: finsum_cong add: Pi_def a_ac finsum_ldistr m_assoc)
  16.275      qed
  16.276    }
  16.277    with R show "coeff P ((p \<otimes>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>P\<^esub> r) n = coeff P (p \<otimes>\<^bsub>P\<^esub> (q \<otimes>\<^bsub>P\<^esub> r)) n"
  16.278      by (simp add: Pi_def)
  16.279  qed (simp_all add: R)
  16.280  
  16.281 -lemma (in UP_cring) UP_l_one [simp]:
  16.282 +lemma UP_r_one [simp]:
  16.283 +  assumes R: "p \<in> carrier P" shows "p \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub> = p"
  16.284 +proof (rule up_eqI)
  16.285 +  fix n
  16.286 +  show "coeff P (p \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub>) n = coeff P p n"
  16.287 +  proof (cases n)
  16.288 +    case 0 
  16.289 +    {
  16.290 +      with R show ?thesis by simp
  16.291 +    }
  16.292 +  next
  16.293 +    case Suc
  16.294 +    {
  16.295 +      (*JE: in the locale UP_cring the proof was solved only with "by (simp del: finsum_Suc add: finsum_Suc2 Pi_def)", but I did not
  16.296 +      get it to work here*)
  16.297 +      fix nn assume Succ: "n = Suc nn"
  16.298 +      have "coeff P (p \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub>) (Suc nn) = coeff P p (Suc nn)"
  16.299 +      proof -
  16.300 +	have "coeff P (p \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub>) (Suc nn) = (\<Oplus>i\<in>{..Suc nn}. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))" using R by simp
  16.301 +	also have "\<dots> = coeff P p (Suc nn) \<otimes> (if Suc nn \<le> Suc nn then \<one> else \<zero>) \<oplus> (\<Oplus>i\<in>{..nn}. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))"
  16.302 +	  using finsum_Suc [of "(\<lambda>i::nat. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))" "nn"] unfolding Pi_def using R by simp
  16.303 +	also have "\<dots> = coeff P p (Suc nn) \<otimes> (if Suc nn \<le> Suc nn then \<one> else \<zero>)"
  16.304 +	proof -
  16.305 +	  have "(\<Oplus>i\<in>{..nn}. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>)) = (\<Oplus>i\<in>{..nn}. \<zero>)"
  16.306 +	    using finsum_cong [of "{..nn}" "{..nn}" "(\<lambda>i::nat. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))" "(\<lambda>i::nat. \<zero>)"] using R 
  16.307 +	    unfolding Pi_def by simp
  16.308 +	  also have "\<dots> = \<zero>" by simp
  16.309 +	  finally show ?thesis using r_zero R by simp
  16.310 +	qed
  16.311 +	also have "\<dots> = coeff P p (Suc nn)" using R by simp
  16.312 +	finally show ?thesis by simp
  16.313 +      qed
  16.314 +      then show ?thesis using Succ by simp
  16.315 +    }
  16.316 +  qed
  16.317 +qed (simp_all add: R)
  16.318 +  
  16.319 +lemma UP_l_one [simp]:
  16.320    assumes R: "p \<in> carrier P"
  16.321    shows "\<one>\<^bsub>P\<^esub> \<otimes>\<^bsub>P\<^esub> p = p"
  16.322  proof (rule up_eqI)
  16.323 @@ -331,22 +383,36 @@
  16.324    qed
  16.325  qed (simp_all add: R)
  16.326  
  16.327 -lemma (in UP_cring) UP_l_distr:
  16.328 +lemma UP_l_distr:
  16.329    assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
  16.330    shows "(p \<oplus>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>P\<^esub> r = (p \<otimes>\<^bsub>P\<^esub> r) \<oplus>\<^bsub>P\<^esub> (q \<otimes>\<^bsub>P\<^esub> r)"
  16.331    by (rule up_eqI) (simp add: l_distr R Pi_def, simp_all add: R)
  16.332  
  16.333 -lemma (in UP_cring) UP_m_comm:
  16.334 -  assumes R: "p \<in> carrier P" "q \<in> carrier P"
  16.335 -  shows "p \<otimes>\<^bsub>P\<^esub> q = q \<otimes>\<^bsub>P\<^esub> p"
  16.336 +lemma UP_r_distr:
  16.337 +  assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
  16.338 +  shows "r \<otimes>\<^bsub>P\<^esub> (p \<oplus>\<^bsub>P\<^esub> q) = (r \<otimes>\<^bsub>P\<^esub> p) \<oplus>\<^bsub>P\<^esub> (r \<otimes>\<^bsub>P\<^esub> q)"
  16.339 +  by (rule up_eqI) (simp add: r_distr R Pi_def, simp_all add: R)
  16.340 +
  16.341 +theorem UP_ring: "ring P"
  16.342 +  by (auto intro!: ringI abelian_groupI monoidI UP_a_assoc)
  16.343 +(auto intro: UP_a_comm UP_l_neg_ex UP_m_assoc UP_l_distr UP_r_distr)
  16.344 +
  16.345 +end
  16.346 +
  16.347 +subsection {* Polynomials form a commutative Ring. *}
  16.348 +
  16.349 +context UP_cring
  16.350 +begin
  16.351 +
  16.352 +lemma UP_m_comm:
  16.353 +  assumes R1: "p \<in> carrier P" and R2: "q \<in> carrier P" shows "p \<otimes>\<^bsub>P\<^esub> q = q \<otimes>\<^bsub>P\<^esub> p"
  16.354  proof (rule up_eqI)
  16.355    fix n
  16.356    {
  16.357      fix k and a b :: "nat=>'a"
  16.358      assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
  16.359      then have "k <= n ==>
  16.360 -      (\<Oplus>i \<in> {..k}. a i \<otimes> b (n-i)) =
  16.361 -      (\<Oplus>i \<in> {..k}. a (k-i) \<otimes> b (i+n-k))"
  16.362 +      (\<Oplus>i \<in> {..k}. a i \<otimes> b (n-i)) = (\<Oplus>i \<in> {..k}. a (k-i) \<otimes> b (i+n-k))"
  16.363        (is "_ \<Longrightarrow> ?eq k")
  16.364      proof (induct k)
  16.365        case 0 then show ?case by (simp add: Pi_def)
  16.366 @@ -356,31 +422,27 @@
  16.367      qed
  16.368    }
  16.369    note l = this
  16.370 -  from R show "coeff P (p \<otimes>\<^bsub>P\<^esub> q) n =  coeff P (q \<otimes>\<^bsub>P\<^esub> p) n"
  16.371 -    apply (simp add: Pi_def)
  16.372 -    apply (subst l)
  16.373 -    apply (auto simp add: Pi_def)
  16.374 -    apply (simp add: m_comm)
  16.375 -    done
  16.376 -qed (simp_all add: R)
  16.377 +  from R1 R2 show "coeff P (p \<otimes>\<^bsub>P\<^esub> q) n =  coeff P (q \<otimes>\<^bsub>P\<^esub> p) n"
  16.378 +    unfolding coeff_mult [OF R1 R2, of n] 
  16.379 +    unfolding coeff_mult [OF R2 R1, of n] 
  16.380 +    using l [of "(\<lambda>i. coeff P p i)" "(\<lambda>i. coeff P q i)" "n"] by (simp add: Pi_def m_comm)
  16.381 +qed (simp_all add: R1 R2)
  16.382  
  16.383 -theorem (in UP_cring) UP_cring:
  16.384 -  "cring P"
  16.385 -  by (auto intro!: cringI abelian_groupI comm_monoidI UP_a_assoc UP_l_zero
  16.386 -    UP_l_neg_ex UP_a_comm UP_m_assoc UP_l_one UP_m_comm UP_l_distr)
  16.387 +subsection{*Polynomials over a commutative ring for a commutative ring*}
  16.388 +
  16.389 +theorem UP_cring:
  16.390 +  "cring P" using UP_ring unfolding cring_def by (auto intro!: comm_monoidI UP_m_assoc UP_m_comm)
  16.391  
  16.392 -lemma (in UP_cring) UP_ring:
  16.393 -  (* preliminary,
  16.394 -     we want "UP_ring R P ==> ring P", not "UP_cring R P ==> ring P" *)
  16.395 -  "ring P"
  16.396 -  by (auto intro: ring.intro cring.axioms UP_cring)
  16.397 +end
  16.398 +
  16.399 +context UP_ring
  16.400 +begin
  16.401  
  16.402 -lemma (in UP_cring) UP_a_inv_closed [intro, simp]:
  16.403 +lemma UP_a_inv_closed [intro, simp]:
  16.404    "p \<in> carrier P ==> \<ominus>\<^bsub>P\<^esub> p \<in> carrier P"
  16.405 -  by (rule abelian_group.a_inv_closed
  16.406 -    [OF ring.is_abelian_group [OF UP_ring]])
  16.407 +  by (rule abelian_group.a_inv_closed [OF ring.is_abelian_group [OF UP_ring]])
  16.408  
  16.409 -lemma (in UP_cring) coeff_a_inv [simp]:
  16.410 +lemma coeff_a_inv [simp]:
  16.411    assumes R: "p \<in> carrier P"
  16.412    shows "coeff P (\<ominus>\<^bsub>P\<^esub> p) n = \<ominus> (coeff P p n)"
  16.413  proof -
  16.414 @@ -393,42 +455,47 @@
  16.415    finally show ?thesis .
  16.416  qed
  16.417  
  16.418 -text {*
  16.419 -  Interpretation of lemmas from @{term cring}.  Saves lifting 43
  16.420 -  lemmas manually.
  16.421 -*}
  16.422 +end
  16.423  
  16.424 -interpretation UP_cring < cring P
  16.425 -  by intro_locales
  16.426 -    (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms UP_cring)+
  16.427 +interpretation UP_ring < ring P using UP_ring .
  16.428 +interpretation UP_cring < cring P using UP_cring .
  16.429  
  16.430  
  16.431  subsection {* Polynomials Form an Algebra *}
  16.432  
  16.433 -lemma (in UP_cring) UP_smult_l_distr:
  16.434 +context UP_ring
  16.435 +begin
  16.436 +
  16.437 +lemma UP_smult_l_distr:
  16.438    "[| a \<in> carrier R; b \<in> carrier R; p \<in> carrier P |] ==>
  16.439    (a \<oplus> b) \<odot>\<^bsub>P\<^esub> p = a \<odot>\<^bsub>P\<^esub> p \<oplus>\<^bsub>P\<^esub> b \<odot>\<^bsub>P\<^esub> p"
  16.440    by (rule up_eqI) (simp_all add: R.l_distr)
  16.441  
  16.442 -lemma (in UP_cring) UP_smult_r_distr:
  16.443 +lemma UP_smult_r_distr:
  16.444    "[| a \<in> carrier R; p \<in> carrier P; q \<in> carrier P |] ==>
  16.445    a \<odot>\<^bsub>P\<^esub> (p \<oplus>\<^bsub>P\<^esub> q) = a \<odot>\<^bsub>P\<^esub> p \<oplus>\<^bsub>P\<^esub> a \<odot>\<^bsub>P\<^esub> q"
  16.446    by (rule up_eqI) (simp_all add: R.r_distr)
  16.447  
  16.448 -lemma (in UP_cring) UP_smult_assoc1:
  16.449 +lemma UP_smult_assoc1:
  16.450        "[| a \<in> carrier R; b \<in> carrier R; p \<in> carrier P |] ==>
  16.451        (a \<otimes> b) \<odot>\<^bsub>P\<^esub> p = a \<odot>\<^bsub>P\<^esub> (b \<odot>\<^bsub>P\<^esub> p)"
  16.452    by (rule up_eqI) (simp_all add: R.m_assoc)
  16.453  
  16.454 -lemma (in UP_cring) UP_smult_one [simp]:
  16.455 +lemma UP_smult_zero [simp]:
  16.456 +      "p \<in> carrier P ==> \<zero> \<odot>\<^bsub>P\<^esub> p = \<zero>\<^bsub>P\<^esub>"
  16.457 +  by (rule up_eqI) simp_all
  16.458 +
  16.459 +lemma UP_smult_one [simp]:
  16.460        "p \<in> carrier P ==> \<one> \<odot>\<^bsub>P\<^esub> p = p"
  16.461    by (rule up_eqI) simp_all
  16.462  
  16.463 -lemma (in UP_cring) UP_smult_assoc2:
  16.464 +lemma UP_smult_assoc2:
  16.465    "[| a \<in> carrier R; p \<in> carrier P; q \<in> carrier P |] ==>
  16.466    (a \<odot>\<^bsub>P\<^esub> p) \<otimes>\<^bsub>P\<^esub> q = a \<odot>\<^bsub>P\<^esub> (p \<otimes>\<^bsub>P\<^esub> q)"
  16.467    by (rule up_eqI) (simp_all add: R.finsum_rdistr R.m_assoc Pi_def)
  16.468  
  16.469 +end
  16.470 +
  16.471  text {*
  16.472    Interpretation of lemmas from @{term algebra}.
  16.473  *}
  16.474 @@ -438,44 +505,44 @@
  16.475    by unfold_locales
  16.476  
  16.477  lemma (in UP_cring) UP_algebra:
  16.478 -  "algebra R P"
  16.479 -  by (auto intro: algebraI R.cring UP_cring UP_smult_l_distr UP_smult_r_distr
  16.480 +  "algebra R P" by (auto intro!: algebraI R.cring UP_cring UP_smult_l_distr UP_smult_r_distr
  16.481      UP_smult_assoc1 UP_smult_assoc2)
  16.482  
  16.483 -interpretation UP_cring < algebra R P
  16.484 -  by intro_locales
  16.485 -    (rule module.axioms algebra.axioms UP_algebra)+
  16.486 +interpretation UP_cring < algebra R P using UP_algebra .
  16.487  
  16.488  
  16.489  subsection {* Further Lemmas Involving Monomials *}
  16.490  
  16.491 -lemma (in UP_cring) monom_zero [simp]:
  16.492 -  "monom P \<zero> n = \<zero>\<^bsub>P\<^esub>"
  16.493 -  by (simp add: UP_def P_def)
  16.494 +context UP_ring
  16.495 +begin
  16.496  
  16.497 -lemma (in UP_cring) monom_mult_is_smult:
  16.498 +lemma monom_zero [simp]:
  16.499 +  "monom P \<zero> n = \<zero>\<^bsub>P\<^esub>" by (simp add: UP_def P_def)
  16.500 +
  16.501 +lemma monom_mult_is_smult:
  16.502    assumes R: "a \<in> carrier R" "p \<in> carrier P"
  16.503    shows "monom P a 0 \<otimes>\<^bsub>P\<^esub> p = a \<odot>\<^bsub>P\<^esub> p"
  16.504  proof (rule up_eqI)
  16.505    fix n
  16.506 -  have "coeff P (p \<otimes>\<^bsub>P\<^esub> monom P a 0) n = coeff P (a \<odot>\<^bsub>P\<^esub> p) n"
  16.507 +  show "coeff P (monom P a 0 \<otimes>\<^bsub>P\<^esub> p) n = coeff P (a \<odot>\<^bsub>P\<^esub> p) n"
  16.508    proof (cases n)
  16.509 -    case 0 with R show ?thesis by (simp add: R.m_comm)
  16.510 +    case 0 with R show ?thesis by simp
  16.511    next
  16.512      case Suc with R show ?thesis
  16.513 -      by (simp cong: R.finsum_cong add: R.r_null Pi_def)
  16.514 -        (simp add: R.m_comm)
  16.515 +      using R.finsum_Suc2 by (simp del: R.finsum_Suc add: R.r_null Pi_def)
  16.516    qed
  16.517 -  with R show "coeff P (monom P a 0 \<otimes>\<^bsub>P\<^esub> p) n = coeff P (a \<odot>\<^bsub>P\<^esub> p) n"
  16.518 -    by (simp add: UP_m_comm)
  16.519  qed (simp_all add: R)
  16.520  
  16.521 -lemma (in UP_cring) monom_add [simp]:
  16.522 +lemma monom_one [simp]:
  16.523 +  "monom P \<one> 0 = \<one>\<^bsub>P\<^esub>"
  16.524 +  by (rule up_eqI) simp_all
  16.525 +
  16.526 +lemma monom_add [simp]:
  16.527    "[| a \<in> carrier R; b \<in> carrier R |] ==>
  16.528    monom P (a \<oplus> b) n = monom P a n \<oplus>\<^bsub>P\<^esub> monom P b n"
  16.529    by (rule up_eqI) simp_all
  16.530  
  16.531 -lemma (in UP_cring) monom_one_Suc:
  16.532 +lemma monom_one_Suc:
  16.533    "monom P \<one> (Suc n) = monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> 1"
  16.534  proof (rule up_eqI)
  16.535    fix k
  16.536 @@ -550,24 +617,59 @@
  16.537    qed
  16.538  qed (simp_all)
  16.539  
  16.540 -lemma (in UP_cring) monom_mult_smult:
  16.541 +lemma monom_one_Suc2:
  16.542 +  "monom P \<one> (Suc n) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> n"
  16.543 +proof (induct n)
  16.544 +  case 0 show ?case by simp
  16.545 +next
  16.546 +  case Suc
  16.547 +  {
  16.548 +    fix k:: nat
  16.549 +    assume hypo: "monom P \<one> (Suc k) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k"
  16.550 +    then show "monom P \<one> (Suc (Suc k)) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> (Suc k)"
  16.551 +    proof -
  16.552 +      have lhs: "monom P \<one> (Suc (Suc k)) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k \<otimes>\<^bsub>P\<^esub> monom P \<one> 1"
  16.553 +	unfolding monom_one_Suc [of "Suc k"] unfolding hypo ..
  16.554 +      note cl = monom_closed [OF R.one_closed, of 1]
  16.555 +      note clk = monom_closed [OF R.one_closed, of k]
  16.556 +      have rhs: "monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> (Suc k) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k \<otimes>\<^bsub>P\<^esub> monom P \<one> 1"
  16.557 +	unfolding monom_one_Suc [of k] unfolding sym [OF m_assoc  [OF cl clk cl]] ..
  16.558 +      from lhs rhs show ?thesis by simp
  16.559 +    qed
  16.560 +  }
  16.561 +qed
  16.562 +
  16.563 +text{*The following corollary follows from lemmas @{thm [locale=UP_ring] "monom_one_Suc"} 
  16.564 +  and @{thm [locale=UP_ring] "monom_one_Suc2"}, and is trivial in @{term UP_cring}*}
  16.565 +
  16.566 +corollary monom_one_comm: shows "monom P \<one> k \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k"
  16.567 +  unfolding monom_one_Suc [symmetric] monom_one_Suc2 [symmetric] ..
  16.568 +
  16.569 +lemma monom_mult_smult:
  16.570    "[| a \<in> carrier R; b \<in> carrier R |] ==> monom P (a \<otimes> b) n = a \<odot>\<^bsub>P\<^esub> monom P b n"
  16.571    by (rule up_eqI) simp_all
  16.572  
  16.573 -lemma (in UP_cring) monom_one [simp]:
  16.574 -  "monom P \<one> 0 = \<one>\<^bsub>P\<^esub>"
  16.575 -  by (rule up_eqI) simp_all
  16.576 -
  16.577 -lemma (in UP_cring) monom_one_mult:
  16.578 +lemma monom_one_mult:
  16.579    "monom P \<one> (n + m) = monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> m"
  16.580  proof (induct n)
  16.581    case 0 show ?case by simp
  16.582  next
  16.583    case Suc then show ?case
  16.584 -    by (simp only: add_Suc monom_one_Suc) (simp add: P.m_ac)
  16.585 +    unfolding add_Suc unfolding monom_one_Suc unfolding Suc.hyps
  16.586 +    using m_assoc monom_one_comm [of m] by simp
  16.587  qed
  16.588  
  16.589 -lemma (in UP_cring) monom_mult [simp]:
  16.590 +lemma monom_one_mult_comm: "monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> m = monom P \<one> m \<otimes>\<^bsub>P\<^esub> monom P \<one> n"
  16.591 +  unfolding monom_one_mult [symmetric] by (rule up_eqI) simp_all
  16.592 +
  16.593 +end
  16.594 +
  16.595 +context UP_cring
  16.596 +begin
  16.597 +
  16.598 +(* Could got to UP_ring?  *)
  16.599 +
  16.600 +lemma monom_mult [simp]:
  16.601    assumes R: "a \<in> carrier R" "b \<in> carrier R"
  16.602    shows "monom P (a \<otimes> b) (n + m) = monom P a n \<otimes>\<^bsub>P\<^esub> monom P b m"
  16.603  proof -
  16.604 @@ -579,11 +681,11 @@
  16.605    also from R have "... = a \<odot>\<^bsub>P\<^esub> (b \<odot>\<^bsub>P\<^esub> (monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> m))"
  16.606      by (simp add: UP_smult_assoc1)
  16.607    also from R have "... = a \<odot>\<^bsub>P\<^esub> (b \<odot>\<^bsub>P\<^esub> (monom P \<one> m \<otimes>\<^bsub>P\<^esub> monom P \<one> n))"
  16.608 -    by (simp add: P.m_comm)
  16.609 +    unfolding monom_one_mult_comm by simp
  16.610    also from R have "... = a \<odot>\<^bsub>P\<^esub> ((b \<odot>\<^bsub>P\<^esub> monom P \<one> m) \<otimes>\<^bsub>P\<^esub> monom P \<one> n)"
  16.611      by (simp add: UP_smult_assoc2)
  16.612    also from R have "... = a \<odot>\<^bsub>P\<^esub> (monom P \<one> n \<otimes>\<^bsub>P\<^esub> (b \<odot>\<^bsub>P\<^esub> monom P \<one> m))"
  16.613 -    by (simp add: P.m_comm)
  16.614 +    using monom_one_mult_comm [of n m] by (simp add: P.m_comm)
  16.615    also from R have "... = (a \<odot>\<^bsub>P\<^esub> monom P \<one> n) \<otimes>\<^bsub>P\<^esub> (b \<odot>\<^bsub>P\<^esub> monom P \<one> m)"
  16.616      by (simp add: UP_smult_assoc2)
  16.617    also from R have "... = monom P (a \<otimes> \<one>) n \<otimes>\<^bsub>P\<^esub> monom P (b \<otimes> \<one>) m"
  16.618 @@ -592,11 +694,16 @@
  16.619    finally show ?thesis .
  16.620  qed
  16.621  
  16.622 -lemma (in UP_cring) monom_a_inv [simp]:
  16.623 +end
  16.624 +
  16.625 +context UP_ring
  16.626 +begin
  16.627 +
  16.628 +lemma monom_a_inv [simp]:
  16.629    "a \<in> carrier R ==> monom P (\<ominus> a) n = \<ominus>\<^bsub>P\<^esub> monom P a n"
  16.630    by (rule up_eqI) simp_all
  16.631  
  16.632 -lemma (in UP_cring) monom_inj:
  16.633 +lemma monom_inj:
  16.634    "inj_on (%a. monom P a n) (carrier R)"
  16.635  proof (rule inj_onI)
  16.636    fix x y
  16.637 @@ -605,6 +712,8 @@
  16.638    with R show "x = y" by simp
  16.639  qed
  16.640  
  16.641 +end
  16.642 +
  16.643  
  16.644  subsection {* The Degree Function *}
  16.645  
  16.646 @@ -612,7 +721,10 @@
  16.647    deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
  16.648    "deg R p == LEAST n. bound \<zero> n (coeff (UP R) p)"
  16.649  
  16.650 -lemma (in UP_cring) deg_aboveI:
  16.651 +context UP_ring
  16.652 +begin
  16.653 +
  16.654 +lemma deg_aboveI:
  16.655    "[| (!!m. n < m ==> coeff P p m = \<zero>); p \<in> carrier P |] ==> deg R p <= n"
  16.656    by (unfold deg_def P_def) (fast intro: Least_le)
  16.657  
  16.658 @@ -633,7 +745,7 @@
  16.659  qed
  16.660  *)
  16.661  
  16.662 -lemma (in UP_cring) deg_aboveD:
  16.663 +lemma deg_aboveD:
  16.664    assumes "deg R p < m" and "p \<in> carrier P"
  16.665    shows "coeff P p m = \<zero>"
  16.666  proof -
  16.667 @@ -644,7 +756,7 @@
  16.668    from this and `deg R p < m` show ?thesis ..
  16.669  qed
  16.670  
  16.671 -lemma (in UP_cring) deg_belowI:
  16.672 +lemma deg_belowI:
  16.673    assumes non_zero: "n ~= 0 ==> coeff P p n ~= \<zero>"
  16.674      and R: "p \<in> carrier P"
  16.675    shows "n <= deg R p"
  16.676 @@ -658,7 +770,7 @@
  16.677    then show ?thesis by arith
  16.678  qed
  16.679  
  16.680 -lemma (in UP_cring) lcoeff_nonzero_deg:
  16.681 +lemma lcoeff_nonzero_deg:
  16.682    assumes deg: "deg R p ~= 0" and R: "p \<in> carrier P"
  16.683    shows "coeff P p (deg R p) ~= \<zero>"
  16.684  proof -
  16.685 @@ -666,9 +778,8 @@
  16.686    proof -
  16.687      have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)"
  16.688        by arith
  16.689 -(* TODO: why does simplification below not work with "1" *)
  16.690      from deg have "deg R p - 1 < (LEAST n. bound \<zero> n (coeff P p))"
  16.691 -      by (unfold deg_def P_def) arith
  16.692 +      by (unfold deg_def P_def) simp
  16.693      then have "~ bound \<zero> (deg R p - 1) (coeff P p)" by (rule not_less_Least)
  16.694      then have "EX m. deg R p - 1 < m & coeff P p m ~= \<zero>"
  16.695        by (unfold bound_def) fast
  16.696 @@ -679,7 +790,7 @@
  16.697    with m_coeff show ?thesis by simp
  16.698  qed
  16.699  
  16.700 -lemma (in UP_cring) lcoeff_nonzero_nonzero:
  16.701 +lemma lcoeff_nonzero_nonzero:
  16.702    assumes deg: "deg R p = 0" and nonzero: "p ~= \<zero>\<^bsub>P\<^esub>" and R: "p \<in> carrier P"
  16.703    shows "coeff P p 0 ~= \<zero>"
  16.704  proof -
  16.705 @@ -695,7 +806,7 @@
  16.706    with coeff show ?thesis by simp
  16.707  qed
  16.708  
  16.709 -lemma (in UP_cring) lcoeff_nonzero:
  16.710 +lemma lcoeff_nonzero:
  16.711    assumes neq: "p ~= \<zero>\<^bsub>P\<^esub>" and R: "p \<in> carrier P"
  16.712    shows "coeff P p (deg R p) ~= \<zero>"
  16.713  proof (cases "deg R p = 0")
  16.714 @@ -704,14 +815,14 @@
  16.715    case False with neq R show ?thesis by (simp add: lcoeff_nonzero_deg)
  16.716  qed
  16.717  
  16.718 -lemma (in UP_cring) deg_eqI:
  16.719 +lemma deg_eqI:
  16.720    "[| !!m. n < m ==> coeff P p m = \<zero>;
  16.721        !!n. n ~= 0 ==> coeff P p n ~= \<zero>; p \<in> carrier P |] ==> deg R p = n"
  16.722  by (fast intro: le_anti_sym deg_aboveI deg_belowI)
  16.723  
  16.724  text {* Degree and polynomial operations *}
  16.725  
  16.726 -lemma (in UP_cring) deg_add [simp]:
  16.727 +lemma deg_add [simp]:
  16.728    assumes R: "p \<in> carrier P" "q \<in> carrier P"
  16.729    shows "deg R (p \<oplus>\<^bsub>P\<^esub> q) <= max (deg R p) (deg R q)"
  16.730  proof (cases "deg R p <= deg R q")
  16.731 @@ -722,15 +833,15 @@
  16.732      by (rule deg_aboveI) (simp_all add: False R deg_aboveD)
  16.733  qed
  16.734  
  16.735 -lemma (in UP_cring) deg_monom_le:
  16.736 +lemma deg_monom_le:
  16.737    "a \<in> carrier R ==> deg R (monom P a n) <= n"
  16.738    by (intro deg_aboveI) simp_all
  16.739  
  16.740 -lemma (in UP_cring) deg_monom [simp]:
  16.741 +lemma deg_monom [simp]:
  16.742    "[| a ~= \<zero>; a \<in> carrier R |] ==> deg R (monom P a n) = n"
  16.743    by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI)
  16.744  
  16.745 -lemma (in UP_cring) deg_const [simp]:
  16.746 +lemma deg_const [simp]:
  16.747    assumes R: "a \<in> carrier R" shows "deg R (monom P a 0) = 0"
  16.748  proof (rule le_anti_sym)
  16.749    show "deg R (monom P a 0) <= 0" by (rule deg_aboveI) (simp_all add: R)
  16.750 @@ -738,7 +849,7 @@
  16.751    show "0 <= deg R (monom P a 0)" by (rule deg_belowI) (simp_all add: R)
  16.752  qed
  16.753  
  16.754 -lemma (in UP_cring) deg_zero [simp]:
  16.755 +lemma deg_zero [simp]:
  16.756    "deg R \<zero>\<^bsub>P\<^esub> = 0"
  16.757  proof (rule le_anti_sym)
  16.758    show "deg R \<zero>\<^bsub>P\<^esub> <= 0" by (rule deg_aboveI) simp_all
  16.759 @@ -746,7 +857,7 @@
  16.760    show "0 <= deg R \<zero>\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all
  16.761  qed
  16.762  
  16.763 -lemma (in UP_cring) deg_one [simp]:
  16.764 +lemma deg_one [simp]:
  16.765    "deg R \<one>\<^bsub>P\<^esub> = 0"
  16.766  proof (rule le_anti_sym)
  16.767    show "deg R \<one>\<^bsub>P\<^esub> <= 0" by (rule deg_aboveI) simp_all
  16.768 @@ -754,7 +865,7 @@
  16.769    show "0 <= deg R \<one>\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all
  16.770  qed
  16.771  
  16.772 -lemma (in UP_cring) deg_uminus [simp]:
  16.773 +lemma deg_uminus [simp]:
  16.774    assumes R: "p \<in> carrier P" shows "deg R (\<ominus>\<^bsub>P\<^esub> p) = deg R p"
  16.775  proof (rule le_anti_sym)
  16.776    show "deg R (\<ominus>\<^bsub>P\<^esub> p) <= deg R p" by (simp add: deg_aboveI deg_aboveD R)
  16.777 @@ -764,12 +875,20 @@
  16.778        inj_on_iff [OF R.a_inv_inj, of _ "\<zero>", simplified] R)
  16.779  qed
  16.780  
  16.781 -lemma (in UP_domain) deg_smult_ring:
  16.782 +text{*The following lemma is later \emph{overwritten} by the most
  16.783 +  specific one for domains, @{text deg_smult}.*}
  16.784 +
  16.785 +lemma deg_smult_ring [simp]:
  16.786    "[| a \<in> carrier R; p \<in> carrier P |] ==>
  16.787    deg R (a \<odot>\<^bsub>P\<^esub> p) <= (if a = \<zero> then 0 else deg R p)"
  16.788    by (cases "a = \<zero>") (simp add: deg_aboveI deg_aboveD)+
  16.789  
  16.790 -lemma (in UP_domain) deg_smult [simp]:
  16.791 +end
  16.792 +
  16.793 +context UP_domain
  16.794 +begin
  16.795 +
  16.796 +lemma deg_smult [simp]:
  16.797    assumes R: "a \<in> carrier R" "p \<in> carrier P"
  16.798    shows "deg R (a \<odot>\<^bsub>P\<^esub> p) = (if a = \<zero> then 0 else deg R p)"
  16.799  proof (rule le_anti_sym)
  16.800 @@ -781,7 +900,12 @@
  16.801    qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff R)
  16.802  qed
  16.803  
  16.804 -lemma (in UP_cring) deg_mult_cring:
  16.805 +end
  16.806 +
  16.807 +context UP_ring
  16.808 +begin
  16.809 +
  16.810 +lemma deg_mult_ring:
  16.811    assumes R: "p \<in> carrier P" "q \<in> carrier P"
  16.812    shows "deg R (p \<otimes>\<^bsub>P\<^esub> q) <= deg R p + deg R q"
  16.813  proof (rule deg_aboveI)
  16.814 @@ -801,12 +925,17 @@
  16.815    with boundm R show "coeff P (p \<otimes>\<^bsub>P\<^esub> q) m = \<zero>" by simp
  16.816  qed (simp add: R)
  16.817  
  16.818 -lemma (in UP_domain) deg_mult [simp]:
  16.819 +end
  16.820 +
  16.821 +context UP_domain
  16.822 +begin
  16.823 +
  16.824 +lemma deg_mult [simp]:
  16.825    "[| p ~= \<zero>\<^bsub>P\<^esub>; q ~= \<zero>\<^bsub>P\<^esub>; p \<in> carrier P; q \<in> carrier P |] ==>
  16.826    deg R (p \<otimes>\<^bsub>P\<^esub> q) = deg R p + deg R q"
  16.827  proof (rule le_anti_sym)
  16.828    assume "p \<in> carrier P" " q \<in> carrier P"
  16.829 -  then show "deg R (p \<otimes>\<^bsub>P\<^esub> q) <= deg R p + deg R q" by (rule deg_mult_cring)
  16.830 +  then show "deg R (p \<otimes>\<^bsub>P\<^esub> q) <= deg R p + deg R q" by (rule deg_mult_ring)
  16.831  next
  16.832    let ?s = "(%i. coeff P p i \<otimes> coeff P q (deg R p + deg R q - i))"
  16.833    assume R: "p \<in> carrier P" "q \<in> carrier P" and nz: "p ~= \<zero>\<^bsub>P\<^esub>" "q ~= \<zero>\<^bsub>P\<^esub>"
  16.834 @@ -828,16 +957,23 @@
  16.835        = coeff P p (deg R p) \<otimes> coeff P q (deg R q)" .
  16.836      with nz show "(\<Oplus>i \<in> {.. deg R p + deg R q}. ?s i) ~= \<zero>"
  16.837        by (simp add: integral_iff lcoeff_nonzero R)
  16.838 -    qed (simp add: R)
  16.839 -  qed
  16.840 +  qed (simp add: R)
  16.841 +qed
  16.842 +
  16.843 +end
  16.844  
  16.845 -lemma (in UP_cring) coeff_finsum:
  16.846 +text{*The following lemmas also can be lifted to @{term UP_ring}.*}
  16.847 +
  16.848 +context UP_ring
  16.849 +begin
  16.850 +
  16.851 +lemma coeff_finsum:
  16.852    assumes fin: "finite A"
  16.853    shows "p \<in> A -> carrier P ==>
  16.854      coeff P (finsum P p A) k = (\<Oplus>i \<in> A. coeff P (p i) k)"
  16.855    using fin by induct (auto simp: Pi_def)
  16.856  
  16.857 -lemma (in UP_cring) up_repr:
  16.858 +lemma up_repr:
  16.859    assumes R: "p \<in> carrier P"
  16.860    shows "(\<Oplus>\<^bsub>P\<^esub> i \<in> {..deg R p}. monom P (coeff P p i) i) = p"
  16.861  proof (rule up_eqI)
  16.862 @@ -874,7 +1010,7 @@
  16.863    qed
  16.864  qed (simp_all add: R Pi_def)
  16.865  
  16.866 -lemma (in UP_cring) up_repr_le:
  16.867 +lemma up_repr_le:
  16.868    "[| deg R p <= n; p \<in> carrier P |] ==>
  16.869    (\<Oplus>\<^bsub>P\<^esub> i \<in> {..n}. monom P (coeff P p i) i) = p"
  16.870  proof -
  16.871 @@ -889,6 +1025,8 @@
  16.872    finally show ?thesis .
  16.873  qed
  16.874  
  16.875 +end
  16.876 +
  16.877  
  16.878  subsection {* Polynomials over Integral Domains *}
  16.879  
  16.880 @@ -901,16 +1039,19 @@
  16.881    by (auto intro!: domain.intro domain_axioms.intro cring.axioms assms
  16.882      del: disjCI)
  16.883  
  16.884 -lemma (in UP_domain) UP_one_not_zero:
  16.885 +context UP_domain
  16.886 +begin
  16.887 +
  16.888 +lemma UP_one_not_zero:
  16.889    "\<one>\<^bsub>P\<^esub> ~= \<zero>\<^bsub>P\<^esub>"
  16.890  proof
  16.891    assume "\<one>\<^bsub>P\<^esub> = \<zero>\<^bsub>P\<^esub>"
  16.892    hence "coeff P \<one>\<^bsub>P\<^esub> 0 = (coeff P \<zero>\<^bsub>P\<^esub> 0)" by simp
  16.893    hence "\<one> = \<zero>" by simp
  16.894 -  with one_not_zero show "False" by contradiction
  16.895 +  with R.one_not_zero show "False" by contradiction
  16.896  qed
  16.897  
  16.898 -lemma (in UP_domain) UP_integral:
  16.899 +lemma UP_integral:
  16.900    "[| p \<otimes>\<^bsub>P\<^esub> q = \<zero>\<^bsub>P\<^esub>; p \<in> carrier P; q \<in> carrier P |] ==> p = \<zero>\<^bsub>P\<^esub> | q = \<zero>\<^bsub>P\<^esub>"
  16.901  proof -
  16.902    fix p q
  16.903 @@ -939,10 +1080,12 @@
  16.904    qed
  16.905  qed
  16.906  
  16.907 -theorem (in UP_domain) UP_domain:
  16.908 +theorem UP_domain:
  16.909    "domain P"
  16.910    by (auto intro!: domainI UP_cring UP_one_not_zero UP_integral del: disjCI)
  16.911  
  16.912 +end
  16.913 +
  16.914  text {*
  16.915    Interpretation of theorems from @{term domain}.
  16.916  *}
  16.917 @@ -959,7 +1102,14 @@
  16.918    !!i. i \<in> B ==> f i = g i |] ==> finsum G f A = finsum G g B"
  16.919    sorry*)
  16.920  
  16.921 -theorem (in cring) diagonal_sum:
  16.922 +lemma (in abelian_monoid) boundD_carrier:
  16.923 +  "[| bound \<zero> n f; n < m |] ==> f m \<in> carrier G"
  16.924 +  by auto
  16.925 +
  16.926 +context ring
  16.927 +begin
  16.928 +
  16.929 +theorem diagonal_sum:
  16.930    "[| f \<in> {..n + m::nat} -> carrier R; g \<in> {..n + m} -> carrier R |] ==>
  16.931    (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
  16.932    (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
  16.933 @@ -992,11 +1142,7 @@
  16.934    then show ?thesis by fast
  16.935  qed
  16.936  
  16.937 -lemma (in abelian_monoid) boundD_carrier:
  16.938 -  "[| bound \<zero> n f; n < m |] ==> f m \<in> carrier G"
  16.939 -  by auto
  16.940 -
  16.941 -theorem (in cring) cauchy_product:
  16.942 +theorem cauchy_product:
  16.943    assumes bf: "bound \<zero> n f" and bg: "bound \<zero> m g"
  16.944      and Rf: "f \<in> {..n} -> carrier R" and Rg: "g \<in> {..m} -> carrier R"
  16.945    shows "(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
  16.946 @@ -1034,7 +1180,9 @@
  16.947    finally show ?thesis .
  16.948  qed
  16.949  
  16.950 -lemma (in UP_cring) const_ring_hom:
  16.951 +end
  16.952 +
  16.953 +lemma (in UP_ring) const_ring_hom:
  16.954    "(%a. monom P a 0) \<in> ring_hom R P"
  16.955    by (auto intro!: ring_hom_memI intro: up_eqI simp: monom_mult_is_smult)
  16.956  
  16.957 @@ -1044,17 +1192,20 @@
  16.958    "eval R S phi s == \<lambda>p \<in> carrier (UP R).
  16.959      \<Oplus>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes> s (^) i"
  16.960  
  16.961 +context UP
  16.962 +begin
  16.963  
  16.964 -lemma (in UP) eval_on_carrier:
  16.965 +lemma eval_on_carrier:
  16.966    fixes S (structure)
  16.967    shows "p \<in> carrier P ==>
  16.968    eval R S phi s p = (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p}. phi (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
  16.969    by (unfold eval_def, fold P_def) simp
  16.970  
  16.971 -lemma (in UP) eval_extensional:
  16.972 +lemma eval_extensional:
  16.973    "eval R S phi p \<in> extensional (carrier P)"
  16.974    by (unfold eval_def, fold P_def) simp
  16.975  
  16.976 +end
  16.977  
  16.978  text {* The universal property of the polynomial ring *}
  16.979  
  16.980 @@ -1065,7 +1216,23 @@
  16.981    assumes indet_img_carrier [simp, intro]: "s \<in> carrier S"
  16.982    defines Eval_def: "Eval == eval R S h s"
  16.983  
  16.984 -theorem (in UP_pre_univ_prop) eval_ring_hom:
  16.985 +text{*JE: I have moved the following lemma from Ring.thy and lifted then to the locale @{term ring_hom_ring} from @{term ring_hom_cring}.*}
  16.986 +text{*JE: I was considering using it in @{text eval_ring_hom}, but that property does not hold for non commutative rings, so 
  16.987 +  maybe it is not that necessary.*}
  16.988 +
  16.989 +lemma (in ring_hom_ring) hom_finsum [simp]:
  16.990 +  "[| finite A; f \<in> A -> carrier R |] ==>
  16.991 +  h (finsum R f A) = finsum S (h o f) A"
  16.992 +proof (induct set: finite)
  16.993 +  case empty then show ?case by simp
  16.994 +next
  16.995 +  case insert then show ?case by (simp add: Pi_def)
  16.996 +qed
  16.997 +
  16.998 +context UP_pre_univ_prop
  16.999 +begin
 16.1000 +
 16.1001 +theorem eval_ring_hom:
 16.1002    assumes S: "s \<in> carrier S"
 16.1003    shows "eval R S h s \<in> ring_hom P S"
 16.1004  proof (rule ring_hom_memI)
 16.1005 @@ -1076,38 +1243,6 @@
 16.1006  next
 16.1007    fix p q
 16.1008    assume R: "p \<in> carrier P" "q \<in> carrier P"
 16.1009 -  then show "eval R S h s (p \<otimes>\<^bsub>P\<^esub> q) = eval R S h s p \<otimes>\<^bsub>S\<^esub> eval R S h s q"
 16.1010 -  proof (simp only: eval_on_carrier UP_mult_closed)
 16.1011 -    from R S have
 16.1012 -      "(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (p \<otimes>\<^bsub>P\<^esub> q)}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) =
 16.1013 -      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (p \<otimes>\<^bsub>P\<^esub> q)} \<union> {deg R (p \<otimes>\<^bsub>P\<^esub> q)<..deg R p + deg R q}.
 16.1014 -        h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
 16.1015 -      by (simp cong: S.finsum_cong
 16.1016 -        add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def
 16.1017 -        del: coeff_mult)
 16.1018 -    also from R have "... =
 16.1019 -      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p + deg R q}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
 16.1020 -      by (simp only: ivl_disj_un_one deg_mult_cring)
 16.1021 -    also from R S have "... =
 16.1022 -      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p + deg R q}.
 16.1023 -         \<Oplus>\<^bsub>S\<^esub> k \<in> {..i}.
 16.1024 -           h (coeff P p k) \<otimes>\<^bsub>S\<^esub> h (coeff P q (i - k)) \<otimes>\<^bsub>S\<^esub>
 16.1025 -           (s (^)\<^bsub>S\<^esub> k \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> (i - k)))"
 16.1026 -      by (simp cong: S.finsum_cong add: S.nat_pow_mult Pi_def
 16.1027 -        S.m_ac S.finsum_rdistr)
 16.1028 -    also from R S have "... =
 16.1029 -      (\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R p}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \<otimes>\<^bsub>S\<^esub>
 16.1030 -      (\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
 16.1031 -      by (simp add: S.cauchy_product [THEN sym] bound.intro deg_aboveD S.m_ac
 16.1032 -        Pi_def)
 16.1033 -    finally show
 16.1034 -      "(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (p \<otimes>\<^bsub>P\<^esub> q)}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) =
 16.1035 -      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \<otimes>\<^bsub>S\<^esub>
 16.1036 -      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" .
 16.1037 -  qed
 16.1038 -next
 16.1039 -  fix p q
 16.1040 -  assume R: "p \<in> carrier P" "q \<in> carrier P"
 16.1041    then show "eval R S h s (p \<oplus>\<^bsub>P\<^esub> q) = eval R S h s p \<oplus>\<^bsub>S\<^esub> eval R S h s q"
 16.1042    proof (simp only: eval_on_carrier P.a_closed)
 16.1043      from S R have
 16.1044 @@ -1115,8 +1250,7 @@
 16.1045        (\<Oplus>\<^bsub>S \<^esub>i\<in>{..deg R (p \<oplus>\<^bsub>P\<^esub> q)} \<union> {deg R (p \<oplus>\<^bsub>P\<^esub> q)<..max (deg R p) (deg R q)}.
 16.1046          h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
 16.1047        by (simp cong: S.finsum_cong
 16.1048 -        add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def
 16.1049 -        del: coeff_add)
 16.1050 +        add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def del: coeff_add)
 16.1051      also from R have "... =
 16.1052          (\<Oplus>\<^bsub>S\<^esub> i \<in> {..max (deg R p) (deg R q)}.
 16.1053            h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
 16.1054 @@ -1145,23 +1279,40 @@
 16.1055  next
 16.1056    show "eval R S h s \<one>\<^bsub>P\<^esub> = \<one>\<^bsub>S\<^esub>"
 16.1057      by (simp only: eval_on_carrier UP_one_closed) simp
 16.1058 +next
 16.1059 +  fix p q
 16.1060 +  assume R: "p \<in> carrier P" "q \<in> carrier P"
 16.1061 +  then show "eval R S h s (p \<otimes>\<^bsub>P\<^esub> q) = eval R S h s p \<otimes>\<^bsub>S\<^esub> eval R S h s q"
 16.1062 +  proof (simp only: eval_on_carrier UP_mult_closed)
 16.1063 +    from R S have
 16.1064 +      "(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (p \<otimes>\<^bsub>P\<^esub> q)}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) =
 16.1065 +      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (p \<otimes>\<^bsub>P\<^esub> q)} \<union> {deg R (p \<otimes>\<^bsub>P\<^esub> q)<..deg R p + deg R q}.
 16.1066 +        h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
 16.1067 +      by (simp cong: S.finsum_cong
 16.1068 +        add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def
 16.1069 +        del: coeff_mult)
 16.1070 +    also from R have "... =
 16.1071 +      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p + deg R q}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
 16.1072 +      by (simp only: ivl_disj_un_one deg_mult_ring)
 16.1073 +    also from R S have "... =
 16.1074 +      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p + deg R q}.
 16.1075 +         \<Oplus>\<^bsub>S\<^esub> k \<in> {..i}.
 16.1076 +           h (coeff P p k) \<otimes>\<^bsub>S\<^esub> h (coeff P q (i - k)) \<otimes>\<^bsub>S\<^esub>
 16.1077 +           (s (^)\<^bsub>S\<^esub> k \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> (i - k)))"
 16.1078 +      by (simp cong: S.finsum_cong add: S.nat_pow_mult Pi_def
 16.1079 +        S.m_ac S.finsum_rdistr)
 16.1080 +    also from R S have "... =
 16.1081 +      (\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R p}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \<otimes>\<^bsub>S\<^esub>
 16.1082 +      (\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
 16.1083 +      by (simp add: S.cauchy_product [THEN sym] bound.intro deg_aboveD S.m_ac
 16.1084 +        Pi_def)
 16.1085 +    finally show
 16.1086 +      "(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (p \<otimes>\<^bsub>P\<^esub> q)}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) =
 16.1087 +      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \<otimes>\<^bsub>S\<^esub>
 16.1088 +      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" .
 16.1089 +  qed
 16.1090  qed
 16.1091  
 16.1092 -text {* Interpretation of ring homomorphism lemmas. *}
 16.1093 -
 16.1094 -interpretation UP_univ_prop < ring_hom_cring P S Eval
 16.1095 -  apply (unfold Eval_def)
 16.1096 -  apply intro_locales
 16.1097 -  apply (rule ring_hom_cring.axioms)
 16.1098 -  apply (rule ring_hom_cring.intro)
 16.1099 -  apply unfold_locales
 16.1100 -  apply (rule eval_ring_hom)
 16.1101 -  apply rule
 16.1102 -  done
 16.1103 -
 16.1104 -
 16.1105 -text {* Further properties of the evaluation homomorphism. *}
 16.1106 -
 16.1107  text {*
 16.1108    The following lemma could be proved in @{text UP_cring} with the additional
 16.1109    assumption that @{text h} is closed. *}
 16.1110 @@ -1170,6 +1321,8 @@
 16.1111    "[| s \<in> carrier S; r \<in> carrier R |] ==> eval R S h s (monom P r 0) = h r"
 16.1112    by (simp only: eval_on_carrier monom_closed) simp
 16.1113  
 16.1114 +text {* Further properties of the evaluation homomorphism. *}
 16.1115 +
 16.1116  text {* The following proof is complicated by the fact that in arbitrary
 16.1117    rings one might have @{term "one R = zero R"}. *}
 16.1118  
 16.1119 @@ -1198,6 +1351,20 @@
 16.1120      h (coeff P (monom P \<one> 1) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) = s" .
 16.1121  qed
 16.1122  
 16.1123 +end
 16.1124 +
 16.1125 +text {* Interpretation of ring homomorphism lemmas. *}
 16.1126 +
 16.1127 +interpretation UP_univ_prop < ring_hom_cring P S Eval
 16.1128 +  apply (unfold Eval_def)
 16.1129 +  apply intro_locales
 16.1130 +  apply (rule ring_hom_cring.axioms)
 16.1131 +  apply (rule ring_hom_cring.intro)
 16.1132 +  apply unfold_locales
 16.1133 +  apply (rule eval_ring_hom)
 16.1134 +  apply rule
 16.1135 +  done
 16.1136 +
 16.1137  lemma (in UP_cring) monom_pow:
 16.1138    assumes R: "a \<in> carrier R"
 16.1139    shows "(monom P a n) (^)\<^bsub>P\<^esub> m = monom P (a (^) m) (n * m)"
 16.1140 @@ -1253,7 +1420,10 @@
 16.1141    by (fast intro: ring_hom_cring.intro ring_hom_cring_axioms.intro
 16.1142      cring.axioms assms)
 16.1143  
 16.1144 -lemma (in UP_pre_univ_prop) UP_hom_unique:
 16.1145 +context UP_pre_univ_prop
 16.1146 +begin
 16.1147 +
 16.1148 +lemma UP_hom_unique:
 16.1149    assumes "ring_hom_cring P S Phi"
 16.1150    assumes Phi: "Phi (monom P \<one> (Suc 0)) = s"
 16.1151        "!!r. r \<in> carrier R ==> Phi (monom P r 0) = h r"
 16.1152 @@ -1277,7 +1447,7 @@
 16.1153    finally show ?thesis .
 16.1154  qed
 16.1155  
 16.1156 -lemma (in UP_pre_univ_prop) ring_homD:
 16.1157 +lemma ring_homD:
 16.1158    assumes Phi: "Phi \<in> ring_hom P S"
 16.1159    shows "ring_hom_cring P S Phi"
 16.1160  proof (rule ring_hom_cring.intro)
 16.1161 @@ -1285,7 +1455,7 @@
 16.1162    by (rule ring_hom_cring_axioms.intro) (rule Phi)
 16.1163  qed unfold_locales
 16.1164  
 16.1165 -theorem (in UP_pre_univ_prop) UP_universal_property:
 16.1166 +theorem UP_universal_property:
 16.1167    assumes S: "s \<in> carrier S"
 16.1168    shows "EX! Phi. Phi \<in> ring_hom P S \<inter> extensional (carrier P) &
 16.1169      Phi (monom P \<one> 1) = s &
 16.1170 @@ -1296,6 +1466,8 @@
 16.1171    apply (auto intro: UP_hom_unique ring_homD)
 16.1172    done
 16.1173  
 16.1174 +end
 16.1175 +
 16.1176  
 16.1177  subsection {* Sample Application of Evaluation Homomorphism *}
 16.1178  
 16.1179 @@ -1308,9 +1480,8 @@
 16.1180    by (auto intro!: UP_pre_univ_prop.intro ring_hom_cring.intro
 16.1181      ring_hom_cring_axioms.intro UP_cring.intro)
 16.1182  
 16.1183 -constdefs
 16.1184 -  INTEG :: "int ring"
 16.1185 -  "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
 16.1186 +definition  INTEG :: "int ring"
 16.1187 +  where INTEG_def: "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
 16.1188  
 16.1189  lemma INTEG_cring:
 16.1190    "cring INTEG"
 16.1191 @@ -1327,11 +1498,7 @@
 16.1192    "UP INTEG"} globally.
 16.1193  *}
 16.1194  
 16.1195 -interpretation INTEG: UP_pre_univ_prop [INTEG INTEG id]
 16.1196 -  apply simp
 16.1197 -  using INTEG_id_eval
 16.1198 -  apply simp
 16.1199 -  done
 16.1200 +interpretation INTEG: UP_pre_univ_prop [INTEG INTEG id] using INTEG_id_eval by simp_all
 16.1201  
 16.1202  lemma INTEG_closed [intro, simp]:
 16.1203    "z \<in> carrier INTEG"
    17.1 --- a/src/HOL/Algebra/document/root.tex	Fri Aug 01 17:41:37 2008 +0200
    17.2 +++ b/src/HOL/Algebra/document/root.tex	Fri Aug 01 18:10:52 2008 +0200
    17.3 @@ -1,4 +1,3 @@
    17.4 -
    17.5  % $Id$
    17.6  
    17.7  \documentclass[11pt,a4paper]{article}
    17.8 @@ -7,23 +6,22 @@
    17.9  \usepackage{amssymb}
   17.10  \usepackage[latin1]{inputenc}
   17.11  \usepackage[only,bigsqcap]{stmaryrd}
   17.12 -%\usepackage{masmath}
   17.13 +%\usepackage{amsmath}
   17.14  
   17.15  % this should be the last package used
   17.16  \usepackage{pdfsetup}
   17.17  
   17.18  \urlstyle{rm}
   17.19 -\isabellestyle{it}
   17.20 +\isabellestyle{tt}
   17.21  \pagestyle{myheadings}
   17.22  
   17.23  \begin{document}
   17.24  
   17.25  \title{The Isabelle/HOL Algebra Library}
   17.26 -\author{
   17.27 -  Clemens Ballarin \\
   17.28 -  Florian Kammüller \\
   17.29 -  Lawrence C Paulson
   17.30 -}
   17.31 +\author{Clemens Ballarin (Editor)}
   17.32 +\date{With contributions by Jesús Aransay, Clemens Ballarin, Stephan Hohe,
   17.33 +  Florian Kammüller and Lawrence C Paulson \\
   17.34 +  \today}
   17.35  \maketitle
   17.36  
   17.37  \tableofcontents
   17.38 @@ -34,8 +32,8 @@
   17.39  
   17.40  \clearpage
   17.41  
   17.42 -\renewcommand{\isamarkupheader}[1]%
   17.43 -{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
   17.44 +%\renewcommand{\isamarkupheader}[1]%
   17.45 +%{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
   17.46  
   17.47  \parindent 0pt\parskip 0.5ex
   17.48  \input{session}
    18.1 --- a/src/HOL/IsaMakefile	Fri Aug 01 17:41:37 2008 +0200
    18.2 +++ b/src/HOL/IsaMakefile	Fri Aug 01 18:10:52 2008 +0200
    18.3 @@ -520,7 +520,7 @@
    18.4    Algebra/document/root.tex Algebra/poly/LongDiv.thy			\
    18.5    Algebra/poly/PolyHomo.thy Algebra/poly/Polynomial.thy			\
    18.6    Algebra/poly/UnivPoly2.thy Algebra/ringsimp.ML
    18.7 -	@cd Algebra; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Algebra
    18.8 +	@cd Algebra; $(ISATOOL) usedir -b -g true -V outline=/proof,/ML $(OUT)/HOL HOL-Algebra
    18.9  
   18.10  
   18.11  ## HOL-Auth