# HG changeset patch # User paulson # Date 1530473327 -3600 # Node ID 5e85cda58af6e3367ce2fbbc542b65b174efdce8 # Parent fcffdcb8f5067c3e75a909f4840c0e61b9375fc8 new lemmas, de-applying, etc. diff -r fcffdcb8f506 -r 5e85cda58af6 src/HOL/Algebra/IntRing.thy --- a/src/HOL/Algebra/IntRing.thy Sun Jul 01 16:46:28 2018 +0100 +++ b/src/HOL/Algebra/IntRing.thy Sun Jul 01 20:28:47 2018 +0100 @@ -14,10 +14,7 @@ lemma dvds_eq_abseq: fixes k :: int shows "l dvd k \ k dvd l \ \l\ = \k\" -apply rule - apply (simp add: zdvd_antisym_abs) -apply (simp add: dvd_if_abs_eq) -done + by (metis dvd_if_abs_eq lcm.commute lcm_proj1_iff_int) subsection \\\\: The Set of Integers as Algebraic Structure\ @@ -29,22 +26,12 @@ by simp lemma int_is_cring: "cring \" -apply (rule cringI) - apply (rule abelian_groupI, simp_all) - defer 1 - apply (rule comm_monoidI, simp_all) - apply (rule distrib_right) -apply (fast intro: left_minus) -done - -(* -lemma int_is_domain: - "domain \" -apply (intro domain.intro domain_axioms.intro) - apply (rule int_is_cring) - apply (unfold int_ring_def, simp+) -done -*) +proof (rule cringI) + show "abelian_group \" + by (rule abelian_groupI) (auto intro: left_minus) + show "Group.comm_monoid \" + by (simp add: Group.monoid.intro monoid.monoid_comm_monoidI) +qed (auto simp: distrib_right) subsection \Interpretations\ @@ -195,22 +182,14 @@ let ?Z = "\carrier = UNIV::int set, eq = (=), le = (\)\" show "lattice ?Z" apply unfold_locales - apply (simp add: least_def Upper_def) - apply arith - apply (simp add: greatest_def Lower_def) - apply arith + apply (simp_all add: least_def Upper_def greatest_def Lower_def) + apply arith+ done then interpret int: lattice "?Z" . show "join ?Z x y = max x y" - apply (rule int.joinI) - apply (simp_all add: least_def Upper_def) - apply arith - done + by (metis int.le_iff_meet iso_tuple_UNIV_I join_comm linear max.absorb_iff2 max_def) show "meet ?Z x y = min x y" - apply (rule int.meetI) - apply (simp_all add: greatest_def Lower_def) - apply arith - done + using int.meet_le int.meet_left int.meet_right by auto qed interpretation int (* [unfolded UNIV] *) : @@ -221,9 +200,7 @@ subsection \Generated Ideals of \\\\ lemma int_Idl: "Idl\<^bsub>\\<^esub> {a} = {x * a | x. True}" - apply (subst int.cgenideal_eq_genideal[symmetric]) apply simp - apply (simp add: cgenideal_def) - done + by (simp_all add: cgenideal_def int.cgenideal_eq_genideal[symmetric]) lemma multiples_principalideal: "principalideal {x * a | x. True } \" by (metis UNIV_I int.cgenideal_eq_genideal int.cgenideal_is_principalideal int_Idl) @@ -231,43 +208,35 @@ lemma prime_primeideal: assumes prime: "Factorial_Ring.prime p" shows "primeideal (Idl\<^bsub>\\<^esub> {p}) \" -apply (rule primeidealI) - apply (rule int.genideal_ideal, simp) - apply (rule int_is_cring) - apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def) - apply clarsimp defer 1 - apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def) - apply (elim exE) -proof - - fix a b x - assume "a * b = x * p" - then have "p dvd a * b" by simp - then have "p dvd a \ p dvd b" - by (metis prime prime_dvd_mult_eq_int) - then show "(\x. a = x * p) \ (\x. b = x * p)" - by (metis dvd_def mult.commute) -next - assume "UNIV = {uu. \x. uu = x * p}" - then obtain x where "1 = x * p" - by best - then have "\p * x\ = 1" - by (simp add: ac_simps) - then show False using prime - by (auto simp add: abs_mult zmult_eq_1_iff) +proof (rule primeidealI) + show "ideal (Idl\<^bsub>\\<^esub> {p}) \" + by (rule int.genideal_ideal, simp) + show "cring \" + by (rule int_is_cring) + have False if "UNIV = {v::int. \x. v = x * p}" + proof - + from that + obtain i where "1 = i * p" + by (blast intro: elim: ) + then show False + using prime by (auto simp add: abs_mult zmult_eq_1_iff) + qed + then show "carrier \ \ Idl\<^bsub>\\<^esub> {p}" + by (auto simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def) + have "p dvd a \ p dvd b" if "a * b = x * p" for a b x + by (simp add: prime prime_dvd_multD that) + then show "\a b. \a \ carrier \; b \ carrier \; a \\<^bsub>\\<^esub> b \ Idl\<^bsub>\\<^esub> {p}\ + \ a \ Idl\<^bsub>\\<^esub> {p} \ b \ Idl\<^bsub>\\<^esub> {p}" + by (auto simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def dvd_def mult.commute) qed - subsection \Ideals and Divisibility\ lemma int_Idl_subset_ideal: "Idl\<^bsub>\\<^esub> {k} \ Idl\<^bsub>\\<^esub> {l} = (k \ Idl\<^bsub>\\<^esub> {l})" by (rule int.Idl_subset_ideal') simp_all lemma Idl_subset_eq_dvd: "Idl\<^bsub>\\<^esub> {k} \ Idl\<^bsub>\\<^esub> {l} \ l dvd k" - apply (subst int_Idl_subset_ideal, subst int_Idl, simp) - apply (rule, clarify) - apply (simp add: dvd_def) - apply (simp add: dvd_def ac_simps) - done + by (subst int_Idl_subset_ideal) (auto simp: dvd_def int_Idl) lemma dvds_eq_Idl: "l dvd k \ k dvd l \ Idl\<^bsub>\\<^esub> {k} = Idl\<^bsub>\\<^esub> {l}" proof - @@ -380,35 +349,25 @@ lemmas ZFact_defs = ZFact_def FactRing_def lemma ZFact_is_cring: "cring (ZFact k)" - apply (unfold ZFact_def) - apply (rule ideal.quotient_is_cring) - apply (intro ring.genideal_ideal) - apply (simp add: cring.axioms[OF int_is_cring] ring.intro) - apply simp - apply (rule int_is_cring) - done + by (simp add: ZFact_def ideal.quotient_is_cring int.cring_axioms int.genideal_ideal) lemma ZFact_zero: "carrier (ZFact 0) = (\a. {{a}})" - apply (insert int.genideal_zero) - apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def) - done + by (simp add: ZFact_defs A_RCOSETS_defs r_coset_def int.genideal_zero) lemma ZFact_one: "carrier (ZFact 1) = {UNIV}" - apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def ring_record_simps) - apply (subst int.genideal_one) - apply (rule, rule, clarsimp) - apply (rule, rule, clarsimp) - apply (rule, clarsimp, arith) - apply (rule, clarsimp) - apply (rule exI[of _ "0"], clarsimp) - done + unfolding ZFact_defs A_RCOSETS_defs r_coset_def ring_record_simps int.genideal_one +proof + have "\a b::int. \x. b = x + a" + by presburger + then show "(\a::int. {\h. {h + a}}) \ {UNIV}" + by force + then show "{UNIV} \ (\a::int. {\h. {h + a}})" + by (metis (no_types, lifting) UNIV_I UN_I singletonD singletonI subset_iff) +qed lemma ZFact_prime_is_domain: assumes pprime: "Factorial_Ring.prime p" shows "domain (ZFact p)" - apply (unfold ZFact_def) - apply (rule primeideal.quotient_is_domain) - apply (rule prime_primeideal[OF pprime]) - done + by (simp add: ZFact_def pprime prime_primeideal primeideal.quotient_is_domain) end diff -r fcffdcb8f506 -r 5e85cda58af6 src/HOL/Algebra/Multiplicative_Group.thy --- a/src/HOL/Algebra/Multiplicative_Group.thy Sun Jul 01 16:46:28 2018 +0100 +++ b/src/HOL/Algebra/Multiplicative_Group.thy Sun Jul 01 20:28:47 2018 +0100 @@ -596,6 +596,11 @@ lemma mult_of_is_Units: "mult_of R = units_of R" unfolding mult_of_def units_of_def using field_Units by auto +lemma m_inv_mult_of : +"\x. x \ carrier (mult_of R) \ m_inv (mult_of R) x = m_inv R x" + using mult_of_is_Units units_of_inv unfolding units_of_def + by simp + lemma field_mult_group : shows "group (mult_of R)" apply (rule groupI) diff -r fcffdcb8f506 -r 5e85cda58af6 src/HOL/Algebra/Sylow.thy --- a/src/HOL/Algebra/Sylow.thy Sun Jul 01 16:46:28 2018 +0100 +++ b/src/HOL/Algebra/Sylow.thy Sun Jul 01 20:28:47 2018 +0100 @@ -8,7 +8,7 @@ text \See also @{cite "Kammueller-Paulson:1999"}.\ -text \The combinatorial argument is in theory @{theory "HOL-Algebra.Exponent"}.\ +text \The combinatorial argument is in theory @{text "Exponent"}.\ lemma le_extend_mult: "\0 < c; a \ b\ \ a \ b * c" for c :: nat