merged

--- a/src/HOL/Algebra/IntRing.thy	Sun Jul 01 19:51:04 2018 +0200
+++ b/src/HOL/Algebra/IntRing.thy	Sun Jul 01 20:29:23 2018 +0100
@@ -14,10 +14,7 @@
 lemma dvds_eq_abseq:
   fixes k :: int
   shows "l dvd k \<and> k dvd l \<longleftrightarrow> \<bar>l\<bar> = \<bar>k\<bar>"
-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 \<open>\<open>\<Z>\<close>: The Set of Integers as Algebraic Structure\<close>
@@ -29,22 +26,12 @@
   by simp
 
 lemma int_is_cring: "cring \<Z>"
-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 \<Z>"
-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 \<Z>"
+    by (rule abelian_groupI) (auto intro: left_minus)
+  show "Group.comm_monoid \<Z>"
+    by (simp add: Group.monoid.intro monoid.monoid_comm_monoidI)
+qed (auto simp: distrib_right)
 
 
 subsection \<open>Interpretations\<close>
@@ -195,22 +182,14 @@
   let ?Z = "\<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>"
   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 \<open>Generated Ideals of \<open>\<Z>\<close>\<close>
 
 lemma int_Idl: "Idl\<^bsub>\<Z>\<^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 } \<Z>"
   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>\<Z>\<^esub> {p}) \<Z>"
-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 \<or> p dvd b"
-    by (metis prime prime_dvd_mult_eq_int)
-  then show "(\<exists>x. a = x * p) \<or> (\<exists>x. b = x * p)"
-    by (metis dvd_def mult.commute)
-next
-  assume "UNIV = {uu. \<exists>x. uu = x * p}"
-  then obtain x where "1 = x * p"
-    by best
-  then have "\<bar>p * x\<bar> = 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>\<Z>\<^esub> {p}) \<Z>"
+    by (rule int.genideal_ideal, simp)
+  show "cring \<Z>"
+    by (rule int_is_cring)
+  have False if "UNIV = {v::int. \<exists>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 \<Z> \<noteq> Idl\<^bsub>\<Z>\<^esub> {p}"
+    by (auto simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
+  have "p dvd a \<or> p dvd b" if "a * b = x * p" for a b x
+    by (simp add: prime prime_dvd_multD that)
+  then show "\<And>a b. \<lbrakk>a \<in> carrier \<Z>; b \<in> carrier \<Z>; a \<otimes>\<^bsub>\<Z>\<^esub> b \<in> Idl\<^bsub>\<Z>\<^esub> {p}\<rbrakk>
+           \<Longrightarrow> a \<in> Idl\<^bsub>\<Z>\<^esub> {p} \<or> b \<in> Idl\<^bsub>\<Z>\<^esub> {p}"
+    by (auto simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def dvd_def mult.commute)
 qed
 
-
 subsection \<open>Ideals and Divisibility\<close>
 
 lemma int_Idl_subset_ideal: "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})"
   by (rule int.Idl_subset_ideal') simp_all
 
 lemma Idl_subset_eq_dvd: "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} \<longleftrightarrow> 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 \<and> k dvd l \<longleftrightarrow> Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^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) = (\<Union>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 "\<And>a b::int. \<exists>x. b = x + a"
+    by presburger
+  then show "(\<Union>a::int. {\<Union>h. {h + a}}) \<subseteq> {UNIV}"
+    by force
+  then show "{UNIV} \<subseteq> (\<Union>a::int. {\<Union>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

--- a/src/HOL/Algebra/Multiplicative_Group.thy	Sun Jul 01 19:51:04 2018 +0200
+++ b/src/HOL/Algebra/Multiplicative_Group.thy	Sun Jul 01 20:29:23 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 :
+"\<And>x. x \<in> carrier (mult_of R) \<Longrightarrow> 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)

--- a/src/HOL/Algebra/Sylow.thy	Sun Jul 01 19:51:04 2018 +0200
+++ b/src/HOL/Algebra/Sylow.thy	Sun Jul 01 20:29:23 2018 +0100
@@ -8,7 +8,7 @@
 
 text \<open>See also @{cite "Kammueller-Paulson:1999"}.\<close>
 
-text \<open>The combinatorial argument is in theory @{theory "HOL-Algebra.Exponent"}.\<close>
+text \<open>The combinatorial argument is in theory @{text "Exponent"}.\<close>
 
 lemma le_extend_mult: "\<lbrakk>0 < c; a \<le> b\<rbrakk> \<Longrightarrow> a \<le> b * c"
   for c :: nat