author paulson Sun, 01 Jul 2018 20:29:23 +0100 changeset 68562 1ab1f1681263 parent 68560 ad079be4f21c (current diff) parent 68561 5e85cda58af6 (diff) child 68563 05fb05f94686
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
-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
-  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"
-  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 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 @@