# HG changeset patch # User ballarin # Date 1217607052 -7200 # Node ID 21bbd410ba0419d73330573af16b46bec2e7f1e0 # Parent 96699d8eb49e86a109cd65c193bddccac3356d25 Generalised polynomial lemmas from cring to ring. diff -r 96699d8eb49e -r 21bbd410ba04 NEWS --- a/NEWS Fri Aug 01 17:41:37 2008 +0200 +++ b/NEWS Fri Aug 01 18:10:52 2008 +0200 @@ -142,7 +142,8 @@ least_carrier ~> least_closed greatest_carrier ~> greatest_closed greatest_Lower_above ~> greatest_Lower_below - +one_zero ~> carrier_one_zero +one_not_zero ~> carrier_one_not_zero (collision with assumption) *** HOL-NSA *** diff -r 96699d8eb49e -r 21bbd410ba04 src/HOL/Algebra/AbelCoset.thy --- a/src/HOL/Algebra/AbelCoset.thy Fri Aug 01 17:41:37 2008 +0200 +++ b/src/HOL/Algebra/AbelCoset.thy Fri Aug 01 18:10:52 2008 +0200 @@ -9,9 +9,9 @@ begin -section {* More Lifting from Groups to Abelian Groups *} +subsection {* More Lifting from Groups to Abelian Groups *} -subsection {* Definitions *} +subsubsection {* Definitions *} text {* Hiding @{text "<+>"} from @{theory Sum_Type} until I come up with better syntax here *} @@ -102,7 +102,7 @@ by (fold a_inv_def) -subsection {* Cosets *} +subsubsection {* Cosets *} lemma (in abelian_group) a_coset_add_assoc: "[| M \ carrier G; g \ carrier G; h \ carrier G |] @@ -178,7 +178,7 @@ *) -subsection {* Subgroups *} +subsubsection {* Subgroups *} locale additive_subgroup = var H + struct G + assumes a_subgroup: "subgroup H \carrier = carrier G, mult = add G, one = zero G\" @@ -214,9 +214,7 @@ folded a_inv_def, simplified monoid_record_simps]) -subsection {* Normal additive subgroups *} - -subsubsection {* Definition of @{text "abelian_subgroup"} *} +subsubsection {* Additive subgroups are normal *} text {* Every subgroup of an @{text "abelian_group"} is normal *} @@ -385,7 +383,7 @@ folded set_add_def A_RCOSETS_def, simplified monoid_record_simps]) -subsection {* Congruence Relation *} +subsubsection {* Congruence Relation *} lemma (in abelian_subgroup) a_equiv_rcong: shows "equiv (carrier G) (racong H)" @@ -446,7 +444,7 @@ (fast intro!: additive_subgroup.a_subgroup)+ -subsection {* Factorization *} +subsubsection {* Factorization *} lemmas A_FactGroup_defs = A_FactGroup_def FactGroup_def @@ -518,7 +516,7 @@ text {* The isomorphism theorems have been omitted from lifting, at least for now *} -subsection{*The First Isomorphism Theorem*} +subsubsection{*The First Isomorphism Theorem*} text{*The quotient by the kernel of a homomorphism is isomorphic to the range of that homomorphism.*} @@ -531,7 +529,7 @@ by (rule a_kernel_def[unfolded kernel_def, simplified ring_record_simps]) -subsection {* Homomorphisms *} +subsubsection {* Homomorphisms *} lemma abelian_group_homI: assumes "abelian_group G" @@ -640,12 +638,10 @@ by (rule group_hom.FactGroup_iso[OF a_group_hom, folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) -section {* Lemmas Lifted from CosetExt.thy *} +subsubsection {* Cosets *} text {* Not eveything from \texttt{CosetExt.thy} is lifted here. *} -subsection {* General Lemmas from \texttt{AlgebraExt.thy} *} - lemma (in additive_subgroup) a_Hcarr [simp]: assumes hH: "h \ H" shows "h \ carrier G" @@ -653,8 +649,6 @@ simplified monoid_record_simps]) (rule hH) -subsection {* Lemmas for Right Cosets *} - lemma (in abelian_subgroup) a_elemrcos_carrier: assumes acarr: "a \ carrier G" and a': "a' \ H +> a" @@ -722,8 +716,6 @@ folded a_r_coset_def, simplified monoid_record_simps]) (rule ycarr, rule repr) -subsection {* Lemmas for the Set of Right Cosets *} - lemma (in abelian_subgroup) a_rcosets_carrier: "X \ a_rcosets H \ X \ carrier G" by (rule subgroup.rcosets_carrier [OF a_subgroup a_group, @@ -731,7 +723,7 @@ -subsection {* Addition of Subgroups *} +subsubsection {* Addition of Subgroups *} lemma (in abelian_monoid) set_add_closed: assumes Acarr: "A \ carrier G" diff -r 96699d8eb49e -r 21bbd410ba04 src/HOL/Algebra/Bij.thy --- a/src/HOL/Algebra/Bij.thy Fri Aug 01 17:41:37 2008 +0200 +++ b/src/HOL/Algebra/Bij.thy Fri Aug 01 18:10:52 2008 +0200 @@ -6,7 +6,7 @@ theory Bij imports Group begin -section {* Bijections of a Set, Permutation Groups and Automorphism Groups *} +section {* Bijections of a Set, Permutation and Automorphism Groups *} constdefs Bij :: "'a set \ ('a \ 'a) set" diff -r 96699d8eb49e -r 21bbd410ba04 src/HOL/Algebra/Congruence.thy --- a/src/HOL/Algebra/Congruence.thy Fri Aug 01 17:41:37 2008 +0200 +++ b/src/HOL/Algebra/Congruence.thy Fri Aug 01 18:10:52 2008 +0200 @@ -9,12 +9,13 @@ section {* Objects *} -text {* Structure with a carrier set. *} +subsection {* Structure with Carrier Set. *} record 'a partial_object = carrier :: "'a set" -text {* Dito with equivalence relation *} + +subsection {* Structure with Carrier and Equivalence Relation @{text eq} *} record 'a eq_object = "'a partial_object" + eq :: "'a \ 'a \ bool" (infixl ".=\" 50) @@ -45,15 +46,14 @@ "x .\\ A" == "~(x .\\ A)" "A {.\}\ B" == "~(A {.=}\ B)" - -section {* Equivalence Relations *} - locale equivalence = fixes S (structure) assumes refl [simp, intro]: "x \ carrier S \ x .= x" and sym [sym]: "\ x .= y; x \ carrier S; y \ carrier S \ \ y .= x" and trans [trans]: "\ x .= y; y .= z; x \ carrier S; y \ carrier S; z \ carrier S \ \ x .= z" +(* Lemmas by Stephan Hohe *) + lemma elemI: fixes R (structure) assumes "a' \ A" and "a .= a'" @@ -205,6 +205,7 @@ by fast (* FIXME: the following two required in Isabelle 2008, not Isabelle 2007 *) +(* alternatively, could declare lemmas [trans] = ssubst [where 'a = "'a set"] *) lemma (in equivalence) equal_set_eq_trans [trans]: assumes AB: "A = B" and BC: "B {.=} C" @@ -216,6 +217,7 @@ shows "A {.=} C" using AB BC by simp + lemma (in equivalence) set_eq_trans [trans]: assumes AB: "A {.=} B" and BC: "B {.=} C" and carr: "A \ carrier S" "B \ carrier S" "C \ carrier S" diff -r 96699d8eb49e -r 21bbd410ba04 src/HOL/Algebra/Coset.thy --- a/src/HOL/Algebra/Coset.thy Fri Aug 01 17:41:37 2008 +0200 +++ b/src/HOL/Algebra/Coset.thy Fri Aug 01 18:10:52 2008 +0200 @@ -4,7 +4,7 @@ Stephan Hohe *) -theory Coset imports Group Exponent begin +theory Coset imports Group begin section {*Cosets and Quotient Groups*} diff -r 96699d8eb49e -r 21bbd410ba04 src/HOL/Algebra/Divisibility.thy --- a/src/HOL/Algebra/Divisibility.thy Fri Aug 01 17:41:37 2008 +0200 +++ b/src/HOL/Algebra/Divisibility.thy Fri Aug 01 18:10:52 2008 +0200 @@ -3,14 +3,16 @@ Id: $Id$ Author: Clemens Ballarin, started 18 July 2008 -Based on work by Stefan Hohe. +Based on work by Stephan Hohe. *) theory Divisibility imports Permutation Coset Group begin -subsection {* Monoid with cancelation law *} +section {* Factorial Monoids *} + +subsection {* Monoids with Cancellation Law *} locale monoid_cancel = monoid + assumes l_cancel: @@ -56,7 +58,7 @@ by unfold_locales -subsection {* Products of units in monoids *} +subsection {* Products of Units in Monoids *} lemma (in monoid) Units_m_closed[simp, intro]: assumes h1unit: "h1 \ Units G" and h2unit: "h2 \ Units G" @@ -150,7 +152,7 @@ show "a \ Units G" by (simp add: Units_def, fast) qed -subsection {* Divisibility and association *} +subsection {* Divisibility and Association *} subsubsection {* Function definitions *} @@ -811,7 +813,7 @@ by (intro properfactor_trans2[OF ab] divides_prod_l, simp+) -subsection {* Irreducible elements and primes *} +subsection {* Irreducible Elements and Primes *} subsubsection {* Irreducible elements *} @@ -1031,11 +1033,7 @@ qed -subsection {* Factorization and factorial monoids *} - -(* -hide (open) const mult (* Multiset.mult, conflicting with monoid.mult *) -*) +subsection {* Factorization and Factorial Monoids *} subsubsection {* Function definitions *} @@ -1891,7 +1889,7 @@ qed (blast intro: factors_wfactors wfactors_unique) -subsection {* Factorizations as multisets *} +subsection {* Factorizations as Multisets *} text {* Gives useful operations like intersection *} @@ -2370,7 +2368,7 @@ qed -subsection {* Irreducible elements are prime *} +subsection {* Irreducible Elements are Prime *} lemma (in factorial_monoid) irreducible_is_prime: assumes pirr: "irreducible G p" @@ -2610,7 +2608,7 @@ qed -subsection {* Greatest common divisors and lowest common multiples *} +subsection {* Greatest Common Divisors and Lowest Common Multiples *} subsubsection {* Definitions *} @@ -2907,7 +2905,7 @@ qed -subsection {* Conditions for factoriality *} +subsection {* Conditions for Factoriality *} subsubsection {* Gcd condition *} @@ -3891,7 +3889,7 @@ qed -subsection {* Factoriality theorems *} +subsection {* Factoriality Theorems *} theorem factorial_condition_one: (* Jacobson theorem 2.21 *) shows "(divisor_chain_condition_monoid G \ primeness_condition_monoid G) = diff -r 96699d8eb49e -r 21bbd410ba04 src/HOL/Algebra/Exponent.thy --- a/src/HOL/Algebra/Exponent.thy Fri Aug 01 17:41:37 2008 +0200 +++ b/src/HOL/Algebra/Exponent.thy Fri Aug 01 18:10:52 2008 +0200 @@ -9,12 +9,15 @@ imports Main Primes Binomial begin -section {*The Combinatorial Argument Underlying the First Sylow Theorem*} +section {*Sylow's Theorem*} + +subsection {*The Combinatorial Argument Underlying the First Sylow Theorem*} + definition exponent :: "nat => nat => nat" where "exponent p s == if prime p then (GREATEST r. p^r dvd s) else 0" -subsection{*Prime Theorems*} +text{*Prime Theorems*} lemma prime_imp_one_less: "prime p ==> Suc 0 < p" by (unfold prime_def, force) @@ -106,7 +109,7 @@ done -subsection{*Exponent Theorems*} +text{*Exponent Theorems*} lemma exponent_ge [rule_format]: "[|p^k dvd n; prime p; 0 k <= exponent p n" @@ -186,7 +189,7 @@ done -subsection{*Main Combinatorial Argument*} +text{*Main Combinatorial Argument*} lemma le_extend_mult: "[| c > 0; a <= b |] ==> a <= b * (c::nat)" apply (rule_tac P = "%x. x <= b * c" in subst) diff -r 96699d8eb49e -r 21bbd410ba04 src/HOL/Algebra/FiniteProduct.thy --- a/src/HOL/Algebra/FiniteProduct.thy Fri Aug 01 17:41:37 2008 +0200 +++ b/src/HOL/Algebra/FiniteProduct.thy Fri Aug 01 18:10:52 2008 +0200 @@ -8,10 +8,9 @@ theory FiniteProduct imports Group begin -section {* Product Operator for Commutative Monoids *} +subsection {* Product Operator for Commutative Monoids *} - -subsection {* Inductive Definition of a Relation for Products over Sets *} +subsubsection {* Inductive Definition of a Relation for Products over Sets *} text {* Instantiation of locale @{text LC} of theory @{text Finite_Set} is not possible, because here we have explicit typing rules like @@ -62,7 +61,7 @@ qed -subsection {* Left-Commutative Operations *} +text {* Left-Commutative Operations *} locale LCD = fixes B :: "'b set" @@ -231,7 +230,7 @@ foldSetD_closed [rule del] -subsection {* Commutative Monoids *} +text {* Commutative Monoids *} text {* We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"} @@ -286,7 +285,7 @@ left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff) -subsection {* Products over Finite Sets *} +subsubsection {* Products over Finite Sets *} constdefs (structure G) finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b" diff -r 96699d8eb49e -r 21bbd410ba04 src/HOL/Algebra/Ideal.thy --- a/src/HOL/Algebra/Ideal.thy Fri Aug 01 17:41:37 2008 +0200 +++ b/src/HOL/Algebra/Ideal.thy Fri Aug 01 18:10:52 2008 +0200 @@ -10,7 +10,9 @@ section {* Ideals *} -subsection {* General definition *} +subsection {* Definitions *} + +subsubsection {* General definition *} locale ideal = additive_subgroup I R + ring R + assumes I_l_closed: "\a \ I; x \ carrier R\ \ x \ a \ I" @@ -44,14 +46,14 @@ done qed -subsection {* Ideals Generated by a Subset of @{term [locale=ring] "carrier R"} *} +subsubsection {* Ideals Generated by a Subset of @{term [locale=ring] "carrier R"} *} constdefs (structure R) genideal :: "('a, 'b) ring_scheme \ 'a set \ 'a set" ("Idl\ _" [80] 79) "genideal R S \ Inter {I. ideal I R \ S \ I}" -subsection {* Principal Ideals *} +subsubsection {* Principal Ideals *} locale principalideal = ideal + assumes generate: "\i \ carrier R. I = Idl {i}" @@ -70,7 +72,7 @@ show ?thesis by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate) qed -subsection {* Maximal Ideals *} +subsubsection {* Maximal Ideals *} locale maximalideal = ideal + assumes I_notcarr: "carrier R \ I" @@ -92,7 +94,7 @@ (rule is_ideal, rule I_notcarr, rule I_maximal) qed -subsection {* Prime Ideals *} +subsubsection {* Prime Ideals *} locale primeideal = ideal + cring + assumes I_notcarr: "carrier R \ I" @@ -138,8 +140,6 @@ done qed -section {* Properties of Ideals *} - subsection {* Special Ideals *} lemma (in ring) zeroideal: @@ -223,8 +223,6 @@ done qed -subsubsection {* Intersection of a Set of Ideals *} - text {* The intersection of any Number of Ideals is again an Ideal in @{term R} *} lemma (in ring) i_Intersect: @@ -352,8 +350,6 @@ subsection {* Ideals generated by a subset of @{term [locale=ring] "carrier R"} *} -subsubsection {* Generation of Ideals in General Rings *} - text {* @{term genideal} generates an ideal *} lemma (in ring) genideal_ideal: assumes Scarr: "S \ carrier R" @@ -455,7 +451,7 @@ qed -subsubsection {* Generation of Principal Ideals in Commutative Rings *} +text {* Generation of Principal Ideals in Commutative Rings *} constdefs (structure R) cgenideal :: "('a, 'b) monoid_scheme \ 'a \ 'a set" ("PIdl\ _" [80] 79) @@ -873,7 +869,7 @@ qed qed -subsection {* Derived Theorems Involving Ideals *} +subsection {* Derived Theorems *} --"A non-zero cring that has only the two trivial ideals is a field" lemma (in cring) trivialideals_fieldI: diff -r 96699d8eb49e -r 21bbd410ba04 src/HOL/Algebra/IntRing.thy --- a/src/HOL/Algebra/IntRing.thy Fri Aug 01 17:41:37 2008 +0200 +++ b/src/HOL/Algebra/IntRing.thy Fri Aug 01 18:10:52 2008 +0200 @@ -5,7 +5,7 @@ *) theory IntRing -imports QuotRing Int +imports QuotRing Int Primes begin @@ -62,10 +62,7 @@ done - -subsection {* The Set of Integers as Algebraic Structure *} - -subsubsection {* Definition of @{text "\"} *} +subsection {* @{text "\"}: The Set of Integers as Algebraic Structure *} constdefs int_ring :: "int ring" ("\") @@ -94,7 +91,7 @@ apply (unfold int_ring_def, simp+) done *) -subsubsection {* Interpretations *} +subsection {* Interpretations *} text {* Since definitions of derived operations are global, their interpretation needs to be done as early as possible --- that is, @@ -254,7 +251,7 @@ by unfold_locales clarsimp -subsubsection {* Generated Ideals of @{text "\"} *} +subsection {* Generated Ideals of @{text "\"} *} lemma int_Idl: "Idl\<^bsub>\\<^esub> {a} = {x * a | x. True}" @@ -342,7 +339,7 @@ qed -subsubsection {* Ideals and Divisibility *} +subsection {* Ideals and Divisibility *} lemma int_Idl_subset_ideal: "Idl\<^bsub>\\<^esub> {k} \ Idl\<^bsub>\\<^esub> {l} = (k \ Idl\<^bsub>\\<^esub> {l})" @@ -376,7 +373,7 @@ done -subsubsection {* Ideals and the Modulus *} +subsection {* Ideals and the Modulus *} constdefs ZMod :: "int => int => int set" @@ -459,7 +456,7 @@ by (rule, erule ZMod_imp_zmod, erule zmod_imp_ZMod) -subsubsection {* Factorization *} +subsection {* Factorization *} constdefs ZFact :: "int \ int set ring" diff -r 96699d8eb49e -r 21bbd410ba04 src/HOL/Algebra/Lattice.thy --- a/src/HOL/Algebra/Lattice.thy Fri Aug 01 17:41:37 2008 +0200 +++ b/src/HOL/Algebra/Lattice.thy Fri Aug 01 18:10:52 2008 +0200 @@ -4,7 +4,7 @@ Author: Clemens Ballarin, started 7 November 2003 Copyright: Clemens Ballarin -Most congruence rules by Stefan Hohe. +Most congruence rules by Stephan Hohe. *) theory Lattice imports Congruence begin @@ -964,7 +964,7 @@ qed -subsection {* Complete lattices *} +subsection {* Complete Lattices *} locale weak_complete_lattice = weak_lattice + assumes sup_exists: @@ -1115,12 +1115,7 @@ end -subsubsection {* Upper and lower bounds of a set *} - -(* all relevant lemmas are global and already proved above *) - - -subsubsection {* Least and greatest, as predicate *} +text {* Least and greatest, as predicate *} lemma (in partial_order) least_unique: "[| least L x A; least L y A |] ==> x = y" @@ -1131,7 +1126,7 @@ using weak_greatest_unique unfolding eq_is_equal . -subsection {* Lattices *} +text {* Lattices *} locale upper_semilattice = partial_order + assumes sup_of_two_exists: @@ -1150,7 +1145,7 @@ locale lattice = upper_semilattice + lower_semilattice -subsubsection {* Supremum *} +text {* Supremum *} declare (in partial_order) weak_sup_of_singleton [simp del] @@ -1169,7 +1164,7 @@ using weak_join_assoc L unfolding eq_is_equal . -subsubsection {* Infimum *} +text {* Infimum *} declare (in partial_order) weak_inf_of_singleton [simp del] @@ -1190,7 +1185,7 @@ using weak_meet_assoc L unfolding eq_is_equal . -subsection {* Total Orders *} +text {* Total Orders *} locale total_order = partial_order + assumes total: "[| x \ carrier L; y \ carrier L |] ==> x \ y | y \ x" @@ -1211,7 +1206,7 @@ by unfold_locales (auto intro: sup_of_two_exists inf_of_two_exists) -subsection {* Complete lattices *} +text {* Complete lattices *} locale complete_lattice = lattice + assumes sup_exists: @@ -1280,7 +1275,7 @@ subsection {* Examples *} -subsubsection {* Powerset of a Set is a Complete Lattice *} +subsubsection {* The Powerset of a Set is a Complete Lattice *} theorem powerset_is_complete_lattice: "complete_lattice (| carrier = Pow A, eq = op =, le = op \ |)" diff -r 96699d8eb49e -r 21bbd410ba04 src/HOL/Algebra/QuotRing.thy --- a/src/HOL/Algebra/QuotRing.thy Fri Aug 01 17:41:37 2008 +0200 +++ b/src/HOL/Algebra/QuotRing.thy Fri Aug 01 18:10:52 2008 +0200 @@ -4,12 +4,12 @@ Author: Stephan Hohe *) -header {* Quotient Rings *} - theory QuotRing imports RingHom begin +section {* Quotient Rings *} + subsection {* Multiplication on Cosets *} constdefs (structure R) diff -r 96699d8eb49e -r 21bbd410ba04 src/HOL/Algebra/Ring.thy --- a/src/HOL/Algebra/Ring.thy Fri Aug 01 17:41:37 2008 +0200 +++ b/src/HOL/Algebra/Ring.thy Fri Aug 01 18:10:52 2008 +0200 @@ -9,7 +9,9 @@ uses ("ringsimp.ML") begin -section {* Abelian Groups *} +section {* The Algebraic Hierarchy of Rings *} + +subsection {* Abelian Groups *} record 'a ring = "'a monoid" + zero :: 'a ("\\") @@ -341,9 +343,7 @@ *) -section {* The Algebraic Hierarchy of Rings *} - -subsection {* Basic Definitions *} +subsection {* Rings: Basic Definitions *} locale ring = abelian_group R + monoid R + assumes l_distr: "[| x \ carrier R; y \ carrier R; z \ carrier R |] @@ -554,13 +554,13 @@ show "\ = \" by simp qed -lemma (in ring) one_zero: +lemma (in ring) carrier_one_zero: shows "(carrier R = {\}) = (\ = \)" by (rule, erule one_zeroI, erule one_zeroD) -lemma (in ring) one_not_zero: +lemma (in ring) carrier_one_not_zero: shows "(carrier R \ {\}) = (\ \ \)" - by (simp add: one_zero) + by (simp add: carrier_one_zero) text {* Two examples for use of method algebra *} @@ -588,7 +588,7 @@ subsubsection {* Sums over Finite Sets *} -lemma (in cring) finsum_ldistr: +lemma (in ring) finsum_ldistr: "[| finite A; a \ carrier R; f \ A -> carrier R |] ==> finsum R f A \ a = finsum R (%i. f i \ a) A" proof (induct set: finite) @@ -597,7 +597,7 @@ case (insert x F) then show ?case by (simp add: Pi_def l_distr) qed -lemma (in cring) finsum_rdistr: +lemma (in ring) finsum_rdistr: "[| finite A; a \ carrier R; f \ A -> carrier R |] ==> a \ finsum R f A = finsum R (%i. a \ f i) A" proof (induct set: finite) diff -r 96699d8eb49e -r 21bbd410ba04 src/HOL/Algebra/RingHom.thy --- a/src/HOL/Algebra/RingHom.thy Fri Aug 01 17:41:37 2008 +0200 +++ b/src/HOL/Algebra/RingHom.thy Fri Aug 01 18:10:52 2008 +0200 @@ -99,7 +99,7 @@ (rule R.is_cring, rule S.is_cring, rule homh) qed -subsection {* The kernel of a ring homomorphism *} +subsection {* The Kernel of a Ring Homomorphism *} --"the kernel of a ring homomorphism is an ideal" lemma (in ring_hom_ring) kernel_is_ideal: diff -r 96699d8eb49e -r 21bbd410ba04 src/HOL/Algebra/Sylow.thy --- a/src/HOL/Algebra/Sylow.thy Fri Aug 01 17:41:37 2008 +0200 +++ b/src/HOL/Algebra/Sylow.thy Fri Aug 01 18:10:52 2008 +0200 @@ -3,10 +3,7 @@ Author: Florian Kammueller, with new proofs by L C Paulson *) -theory Sylow imports Coset begin - - -section {* Sylow's Theorem *} +theory Sylow imports Coset Exponent begin text {* See also \cite{Kammueller-Paulson:1999}. diff -r 96699d8eb49e -r 21bbd410ba04 src/HOL/Algebra/UnivPoly.thy --- a/src/HOL/Algebra/UnivPoly.thy Fri Aug 01 17:41:37 2008 +0200 +++ b/src/HOL/Algebra/UnivPoly.thy Fri Aug 01 18:10:52 2008 +0200 @@ -3,9 +3,11 @@ Id: $Id$ Author: Clemens Ballarin, started 9 December 1996 Copyright: Clemens Ballarin + +Contributions by Jesus Aransay. *) -theory UnivPoly imports Module begin +theory UnivPoly imports Module RingHom begin section {* Univariate Polynomials *} @@ -77,19 +79,16 @@ "f \ up R ==> f n \ carrier R" by (simp add: up_def Pi_def) -lemma (in cring) bound_upD [dest]: - "f \ up R ==> EX n. bound \ n f" - by (simp add: up_def) +context ring +begin + +lemma bound_upD [dest]: "f \ up R ==> EX n. bound \ n f" by (simp add: up_def) -lemma (in cring) up_one_closed: - "(%n. if n = 0 then \ else \) \ up R" - using up_def by force +lemma up_one_closed: "(%n. if n = 0 then \ else \) \ up R" using up_def by force -lemma (in cring) up_smult_closed: - "[| a \ carrier R; p \ up R |] ==> (%i. a \ p i) \ up R" - by force +lemma up_smult_closed: "[| a \ carrier R; p \ up R |] ==> (%i. a \ p i) \ up R" by force -lemma (in cring) up_add_closed: +lemma up_add_closed: "[| p \ up R; q \ up R |] ==> (%i. p i \ q i) \ up R" proof fix n @@ -112,7 +111,7 @@ qed qed -lemma (in cring) up_a_inv_closed: +lemma up_a_inv_closed: "p \ up R ==> (%i. \ (p i)) \ up R" proof assume R: "p \ up R" @@ -121,7 +120,7 @@ then show "EX n. bound \ n (%i. \ p i)" by auto qed auto -lemma (in cring) up_mult_closed: +lemma up_mult_closed: "[| p \ up R; q \ up R |] ==> (%n. \i \ {..n}. p i \ q (n-i)) \ up R" proof @@ -161,6 +160,8 @@ qed qed +end + subsection {* Effect of Operations on Coefficients *} @@ -168,19 +169,45 @@ fixes R (structure) and P (structure) defines P_def: "P == UP R" +locale UP_ring = UP + ring R + locale UP_cring = UP + cring R -locale UP_domain = UP_cring + "domain" R +interpretation UP_cring < UP_ring + by (rule P_def) intro_locales + +locale UP_domain = UP + "domain" R -text {* - Temporarily declare @{thm [locale=UP] P_def} as simp rule. -*} +interpretation UP_domain < UP_cring + by (rule P_def) intro_locales + +context UP +begin + +text {*Temporarily declare @{thm [locale=UP] P_def} as simp rule.*} + +declare P_def [simp] -declare (in UP) P_def [simp] +lemma up_eqI: + assumes prem: "!!n. coeff P p n = coeff P q n" and R: "p \ carrier P" "q \ carrier P" + shows "p = q" +proof + fix x + from prem and R show "p x = q x" by (simp add: UP_def) +qed -lemma (in UP_cring) coeff_monom [simp]: - "a \ carrier R ==> - coeff P (monom P a m) n = (if m=n then a else \)" +lemma coeff_closed [simp]: + "p \ carrier P ==> coeff P p n \ carrier R" by (auto simp add: UP_def) + +end + +context UP_ring +begin + +(* Theorems generalised to rings by Jesus Aransay. *) + +lemma coeff_monom [simp]: + "a \ carrier R ==> coeff P (monom P a m) n = (if m=n then a else \)" proof - assume R: "a \ carrier R" then have "(%n. if n = m then a else \) \ up R" @@ -188,86 +215,69 @@ with R show ?thesis by (simp add: UP_def) qed -lemma (in UP_cring) coeff_zero [simp]: - "coeff P \\<^bsub>P\<^esub> n = \" - by (auto simp add: UP_def) +lemma coeff_zero [simp]: "coeff P \\<^bsub>P\<^esub> n = \" by (auto simp add: UP_def) -lemma (in UP_cring) coeff_one [simp]: - "coeff P \\<^bsub>P\<^esub> n = (if n=0 then \ else \)" +lemma coeff_one [simp]: "coeff P \\<^bsub>P\<^esub> n = (if n=0 then \ else \)" using up_one_closed by (simp add: UP_def) -lemma (in UP_cring) coeff_smult [simp]: - "[| a \ carrier R; p \ carrier P |] ==> - coeff P (a \\<^bsub>P\<^esub> p) n = a \ coeff P p n" +lemma coeff_smult [simp]: + "[| a \ carrier R; p \ carrier P |] ==> coeff P (a \\<^bsub>P\<^esub> p) n = a \ coeff P p n" by (simp add: UP_def up_smult_closed) -lemma (in UP_cring) coeff_add [simp]: - "[| p \ carrier P; q \ carrier P |] ==> - coeff P (p \\<^bsub>P\<^esub> q) n = coeff P p n \ coeff P q n" +lemma coeff_add [simp]: + "[| p \ carrier P; q \ carrier P |] ==> coeff P (p \\<^bsub>P\<^esub> q) n = coeff P p n \ coeff P q n" by (simp add: UP_def up_add_closed) -lemma (in UP_cring) coeff_mult [simp]: - "[| p \ carrier P; q \ carrier P |] ==> - coeff P (p \\<^bsub>P\<^esub> q) n = (\i \ {..n}. coeff P p i \ coeff P q (n-i))" +lemma coeff_mult [simp]: + "[| p \ carrier P; q \ carrier P |] ==> coeff P (p \\<^bsub>P\<^esub> q) n = (\i \ {..n}. coeff P p i \ coeff P q (n-i))" by (simp add: UP_def up_mult_closed) -lemma (in UP) up_eqI: - assumes prem: "!!n. coeff P p n = coeff P q n" - and R: "p \ carrier P" "q \ carrier P" - shows "p = q" -proof - fix x - from prem and R show "p x = q x" by (simp add: UP_def) -qed +end -subsection {* Polynomials Form a Commutative Ring. *} +subsection {* Polynomials Form a Ring. *} + +context UP_ring +begin text {* Operations are closed over @{term P}. *} -lemma (in UP_cring) UP_mult_closed [simp]: - "[| p \ carrier P; q \ carrier P |] ==> p \\<^bsub>P\<^esub> q \ carrier P" - by (simp add: UP_def up_mult_closed) +lemma UP_mult_closed [simp]: + "[| p \ carrier P; q \ carrier P |] ==> p \\<^bsub>P\<^esub> q \ carrier P" by (simp add: UP_def up_mult_closed) -lemma (in UP_cring) UP_one_closed [simp]: - "\\<^bsub>P\<^esub> \ carrier P" - by (simp add: UP_def up_one_closed) +lemma UP_one_closed [simp]: + "\\<^bsub>P\<^esub> \ carrier P" by (simp add: UP_def up_one_closed) -lemma (in UP_cring) UP_zero_closed [intro, simp]: - "\\<^bsub>P\<^esub> \ carrier P" - by (auto simp add: UP_def) +lemma UP_zero_closed [intro, simp]: + "\\<^bsub>P\<^esub> \ carrier P" by (auto simp add: UP_def) -lemma (in UP_cring) UP_a_closed [intro, simp]: - "[| p \ carrier P; q \ carrier P |] ==> p \\<^bsub>P\<^esub> q \ carrier P" - by (simp add: UP_def up_add_closed) - -lemma (in UP_cring) monom_closed [simp]: - "a \ carrier R ==> monom P a n \ carrier P" - by (auto simp add: UP_def up_def Pi_def) +lemma UP_a_closed [intro, simp]: + "[| p \ carrier P; q \ carrier P |] ==> p \\<^bsub>P\<^esub> q \ carrier P" by (simp add: UP_def up_add_closed) -lemma (in UP_cring) UP_smult_closed [simp]: - "[| a \ carrier R; p \ carrier P |] ==> a \\<^bsub>P\<^esub> p \ carrier P" - by (simp add: UP_def up_smult_closed) +lemma monom_closed [simp]: + "a \ carrier R ==> monom P a n \ carrier P" by (auto simp add: UP_def up_def Pi_def) -lemma (in UP) coeff_closed [simp]: - "p \ carrier P ==> coeff P p n \ carrier R" - by (auto simp add: UP_def) +lemma UP_smult_closed [simp]: + "[| a \ carrier R; p \ carrier P |] ==> a \\<^bsub>P\<^esub> p \ carrier P" by (simp add: UP_def up_smult_closed) + +end declare (in UP) P_def [simp del] text {* Algebraic ring properties *} -lemma (in UP_cring) UP_a_assoc: - assumes R: "p \ carrier P" "q \ carrier P" "r \ carrier P" - shows "(p \\<^bsub>P\<^esub> q) \\<^bsub>P\<^esub> r = p \\<^bsub>P\<^esub> (q \\<^bsub>P\<^esub> r)" - by (rule up_eqI, simp add: a_assoc R, simp_all add: R) +context UP_ring +begin -lemma (in UP_cring) UP_l_zero [simp]: +lemma UP_a_assoc: + assumes R: "p \ carrier P" "q \ carrier P" "r \ carrier P" + shows "(p \\<^bsub>P\<^esub> q) \\<^bsub>P\<^esub> r = p \\<^bsub>P\<^esub> (q \\<^bsub>P\<^esub> r)" by (rule up_eqI, simp add: a_assoc R, simp_all add: R) + +lemma UP_l_zero [simp]: assumes R: "p \ carrier P" - shows "\\<^bsub>P\<^esub> \\<^bsub>P\<^esub> p = p" - by (rule up_eqI, simp_all add: R) + shows "\\<^bsub>P\<^esub> \\<^bsub>P\<^esub> p = p" by (rule up_eqI, simp_all add: R) -lemma (in UP_cring) UP_l_neg_ex: +lemma UP_l_neg_ex: assumes R: "p \ carrier P" shows "EX q : carrier P. q \\<^bsub>P\<^esub> p = \\<^bsub>P\<^esub>" proof - @@ -283,12 +293,17 @@ qed (rule closed) qed -lemma (in UP_cring) UP_a_comm: +lemma UP_a_comm: assumes R: "p \ carrier P" "q \ carrier P" - shows "p \\<^bsub>P\<^esub> q = q \\<^bsub>P\<^esub> p" - by (rule up_eqI, simp add: a_comm R, simp_all add: R) + shows "p \\<^bsub>P\<^esub> q = q \\<^bsub>P\<^esub> p" by (rule up_eqI, simp add: a_comm R, simp_all add: R) + +end + -lemma (in UP_cring) UP_m_assoc: +context UP_ring +begin + +lemma UP_m_assoc: assumes R: "p \ carrier P" "q \ carrier P" "r \ carrier P" shows "(p \\<^bsub>P\<^esub> q) \\<^bsub>P\<^esub> r = p \\<^bsub>P\<^esub> (q \\<^bsub>P\<^esub> r)" proof (rule up_eqI) @@ -310,14 +325,51 @@ with R show ?case by (simp cong: finsum_cong add: Suc_diff_le Pi_def l_distr r_distr m_assoc) - (simp cong: finsum_cong add: Pi_def a_ac finsum_ldistr m_assoc) + (simp cong: finsum_cong add: Pi_def a_ac finsum_ldistr m_assoc) qed } with R show "coeff P ((p \\<^bsub>P\<^esub> q) \\<^bsub>P\<^esub> r) n = coeff P (p \\<^bsub>P\<^esub> (q \\<^bsub>P\<^esub> r)) n" by (simp add: Pi_def) qed (simp_all add: R) -lemma (in UP_cring) UP_l_one [simp]: +lemma UP_r_one [simp]: + assumes R: "p \ carrier P" shows "p \\<^bsub>P\<^esub> \\<^bsub>P\<^esub> = p" +proof (rule up_eqI) + fix n + show "coeff P (p \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) n = coeff P p n" + proof (cases n) + case 0 + { + with R show ?thesis by simp + } + next + case Suc + { + (*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 + get it to work here*) + fix nn assume Succ: "n = Suc nn" + have "coeff P (p \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) (Suc nn) = coeff P p (Suc nn)" + proof - + have "coeff P (p \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) (Suc nn) = (\i\{..Suc nn}. coeff P p i \ (if Suc nn \ i then \ else \))" using R by simp + also have "\ = coeff P p (Suc nn) \ (if Suc nn \ Suc nn then \ else \) \ (\i\{..nn}. coeff P p i \ (if Suc nn \ i then \ else \))" + using finsum_Suc [of "(\i::nat. coeff P p i \ (if Suc nn \ i then \ else \))" "nn"] unfolding Pi_def using R by simp + also have "\ = coeff P p (Suc nn) \ (if Suc nn \ Suc nn then \ else \)" + proof - + have "(\i\{..nn}. coeff P p i \ (if Suc nn \ i then \ else \)) = (\i\{..nn}. \)" + using finsum_cong [of "{..nn}" "{..nn}" "(\i::nat. coeff P p i \ (if Suc nn \ i then \ else \))" "(\i::nat. \)"] using R + unfolding Pi_def by simp + also have "\ = \" by simp + finally show ?thesis using r_zero R by simp + qed + also have "\ = coeff P p (Suc nn)" using R by simp + finally show ?thesis by simp + qed + then show ?thesis using Succ by simp + } + qed +qed (simp_all add: R) + +lemma UP_l_one [simp]: assumes R: "p \ carrier P" shows "\\<^bsub>P\<^esub> \\<^bsub>P\<^esub> p = p" proof (rule up_eqI) @@ -331,22 +383,36 @@ qed qed (simp_all add: R) -lemma (in UP_cring) UP_l_distr: +lemma UP_l_distr: assumes R: "p \ carrier P" "q \ carrier P" "r \ carrier P" shows "(p \\<^bsub>P\<^esub> q) \\<^bsub>P\<^esub> r = (p \\<^bsub>P\<^esub> r) \\<^bsub>P\<^esub> (q \\<^bsub>P\<^esub> r)" by (rule up_eqI) (simp add: l_distr R Pi_def, simp_all add: R) -lemma (in UP_cring) UP_m_comm: - assumes R: "p \ carrier P" "q \ carrier P" - shows "p \\<^bsub>P\<^esub> q = q \\<^bsub>P\<^esub> p" +lemma UP_r_distr: + assumes R: "p \ carrier P" "q \ carrier P" "r \ carrier P" + shows "r \\<^bsub>P\<^esub> (p \\<^bsub>P\<^esub> q) = (r \\<^bsub>P\<^esub> p) \\<^bsub>P\<^esub> (r \\<^bsub>P\<^esub> q)" + by (rule up_eqI) (simp add: r_distr R Pi_def, simp_all add: R) + +theorem UP_ring: "ring P" + by (auto intro!: ringI abelian_groupI monoidI UP_a_assoc) +(auto intro: UP_a_comm UP_l_neg_ex UP_m_assoc UP_l_distr UP_r_distr) + +end + +subsection {* Polynomials form a commutative Ring. *} + +context UP_cring +begin + +lemma UP_m_comm: + assumes R1: "p \ carrier P" and R2: "q \ carrier P" shows "p \\<^bsub>P\<^esub> q = q \\<^bsub>P\<^esub> p" proof (rule up_eqI) fix n { fix k and a b :: "nat=>'a" assume R: "a \ UNIV -> carrier R" "b \ UNIV -> carrier R" then have "k <= n ==> - (\i \ {..k}. a i \ b (n-i)) = - (\i \ {..k}. a (k-i) \ b (i+n-k))" + (\i \ {..k}. a i \ b (n-i)) = (\i \ {..k}. a (k-i) \ b (i+n-k))" (is "_ \ ?eq k") proof (induct k) case 0 then show ?case by (simp add: Pi_def) @@ -356,31 +422,27 @@ qed } note l = this - from R show "coeff P (p \\<^bsub>P\<^esub> q) n = coeff P (q \\<^bsub>P\<^esub> p) n" - apply (simp add: Pi_def) - apply (subst l) - apply (auto simp add: Pi_def) - apply (simp add: m_comm) - done -qed (simp_all add: R) + from R1 R2 show "coeff P (p \\<^bsub>P\<^esub> q) n = coeff P (q \\<^bsub>P\<^esub> p) n" + unfolding coeff_mult [OF R1 R2, of n] + unfolding coeff_mult [OF R2 R1, of n] + using l [of "(\i. coeff P p i)" "(\i. coeff P q i)" "n"] by (simp add: Pi_def m_comm) +qed (simp_all add: R1 R2) -theorem (in UP_cring) UP_cring: - "cring P" - by (auto intro!: cringI abelian_groupI comm_monoidI UP_a_assoc UP_l_zero - UP_l_neg_ex UP_a_comm UP_m_assoc UP_l_one UP_m_comm UP_l_distr) +subsection{*Polynomials over a commutative ring for a commutative ring*} + +theorem UP_cring: + "cring P" using UP_ring unfolding cring_def by (auto intro!: comm_monoidI UP_m_assoc UP_m_comm) -lemma (in UP_cring) UP_ring: - (* preliminary, - we want "UP_ring R P ==> ring P", not "UP_cring R P ==> ring P" *) - "ring P" - by (auto intro: ring.intro cring.axioms UP_cring) +end + +context UP_ring +begin -lemma (in UP_cring) UP_a_inv_closed [intro, simp]: +lemma UP_a_inv_closed [intro, simp]: "p \ carrier P ==> \\<^bsub>P\<^esub> p \ carrier P" - by (rule abelian_group.a_inv_closed - [OF ring.is_abelian_group [OF UP_ring]]) + by (rule abelian_group.a_inv_closed [OF ring.is_abelian_group [OF UP_ring]]) -lemma (in UP_cring) coeff_a_inv [simp]: +lemma coeff_a_inv [simp]: assumes R: "p \ carrier P" shows "coeff P (\\<^bsub>P\<^esub> p) n = \ (coeff P p n)" proof - @@ -393,42 +455,47 @@ finally show ?thesis . qed -text {* - Interpretation of lemmas from @{term cring}. Saves lifting 43 - lemmas manually. -*} +end -interpretation UP_cring < cring P - by intro_locales - (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms UP_cring)+ +interpretation UP_ring < ring P using UP_ring . +interpretation UP_cring < cring P using UP_cring . subsection {* Polynomials Form an Algebra *} -lemma (in UP_cring) UP_smult_l_distr: +context UP_ring +begin + +lemma UP_smult_l_distr: "[| a \ carrier R; b \ carrier R; p \ carrier P |] ==> (a \ b) \\<^bsub>P\<^esub> p = a \\<^bsub>P\<^esub> p \\<^bsub>P\<^esub> b \\<^bsub>P\<^esub> p" by (rule up_eqI) (simp_all add: R.l_distr) -lemma (in UP_cring) UP_smult_r_distr: +lemma UP_smult_r_distr: "[| a \ carrier R; p \ carrier P; q \ carrier P |] ==> a \\<^bsub>P\<^esub> (p \\<^bsub>P\<^esub> q) = a \\<^bsub>P\<^esub> p \\<^bsub>P\<^esub> a \\<^bsub>P\<^esub> q" by (rule up_eqI) (simp_all add: R.r_distr) -lemma (in UP_cring) UP_smult_assoc1: +lemma UP_smult_assoc1: "[| a \ carrier R; b \ carrier R; p \