--- a/src/HOL/Algebra/Algebra.thy Tue Jul 03 10:07:24 2018 +0100
+++ b/src/HOL/Algebra/Algebra.thy Tue Jul 03 10:07:35 2018 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Algebra/Algebra *)
+(* Title: HOL/Algebra/Algebra.thy *)
theory Algebra
imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields
--- a/src/HOL/Algebra/Chinese_Remainder.thy Tue Jul 03 10:07:24 2018 +0100
+++ b/src/HOL/Algebra/Chinese_Remainder.thy Tue Jul 03 10:07:35 2018 +0100
@@ -1,11 +1,9 @@
-(* ************************************************************************** *)
-(* Title: Chinese_Remainder.thy *)
-(* Author: Paulo Emílio de Vilhena *)
-(* ************************************************************************** *)
+(* Title: HOL/Algebra/Chinese_Remainder.thy
+ Author: Paulo Emílio de Vilhena
+*)
theory Chinese_Remainder
imports QuotRing Ideal_Product
-
begin
section \<open>Chinese Remainder Theorem\<close>
@@ -1204,4 +1202,4 @@
is_ring by (simp add: ring_hom_ringI2)
qed
-end
\ No newline at end of file
+end
--- a/src/HOL/Algebra/Coset.thy Tue Jul 03 10:07:24 2018 +0100
+++ b/src/HOL/Algebra/Coset.thy Tue Jul 03 10:07:35 2018 +0100
@@ -1,5 +1,6 @@
(* Title: HOL/Algebra/Coset.thy
- Authors: Florian Kammueller, L C Paulson, Stephan Hohe
+ Authors: Florian Kammueller, L C Paulson, Stephan Hohe
+
With additional contributions from Martin Baillon and Paulo Emílio de Vilhena.
*)
--- a/src/HOL/Algebra/Cycles.thy Tue Jul 03 10:07:24 2018 +0100
+++ b/src/HOL/Algebra/Cycles.thy Tue Jul 03 10:07:35 2018 +0100
@@ -1,11 +1,9 @@
-(* ************************************************************************** *)
-(* Title: Cycles.thy *)
-(* Author: Paulo Emílio de Vilhena *)
-(* ************************************************************************** *)
+(* Title: HOL/Algebra/Cycles.thy
+ Author: Paulo Emílio de Vilhena
+*)
theory Cycles
imports "HOL-Library.Permutations" "HOL-Library.FuncSet"
-
begin
section \<open>Cycles\<close>
@@ -753,4 +751,4 @@
shows "cycle_decomp S p"
using assms cycle_decomposition_aux by blast
-end
\ No newline at end of file
+end
--- a/src/HOL/Algebra/Embedded_Algebras.thy Tue Jul 03 10:07:24 2018 +0100
+++ b/src/HOL/Algebra/Embedded_Algebras.thy Tue Jul 03 10:07:35 2018 +0100
@@ -1,11 +1,9 @@
-(* ************************************************************************** *)
-(* Title: Embedded_Algebras.thy *)
-(* Author: Paulo Emílio de Vilhena *)
-(* ************************************************************************** *)
+(* Title: HOL/Algebra/Embedded_Algebras.thy
+ Author: Paulo Emílio de Vilhena
+*)
theory Embedded_Algebras
imports Subrings Generated_Groups
-
begin
section \<open>Definitions\<close>
@@ -1315,4 +1313,4 @@
qed
*)
-end
\ No newline at end of file
+end
--- a/src/HOL/Algebra/Exact_Sequence.thy Tue Jul 03 10:07:24 2018 +0100
+++ b/src/HOL/Algebra/Exact_Sequence.thy Tue Jul 03 10:07:35 2018 +0100
@@ -1,11 +1,9 @@
-(* ************************************************************************** *)
-(* Title: Exact_Sequence.thy *)
-(* Author: Martin Baillon *)
-(* ************************************************************************** *)
+(* Title: HOL/Algebra/Exact_Sequence.thy
+ Author: Martin Baillon
+*)
theory Exact_Sequence
imports Group Coset Solvable_Groups
-
begin
section \<open>Exact Sequences\<close>
@@ -176,4 +174,3 @@
using exact_seq_solvable_recip exact_seq_solvable_imp assms by blast
end
-
\ No newline at end of file
--- a/src/HOL/Algebra/Generated_Fields.thy Tue Jul 03 10:07:24 2018 +0100
+++ b/src/HOL/Algebra/Generated_Fields.thy Tue Jul 03 10:07:35 2018 +0100
@@ -1,12 +1,9 @@
-(* ************************************************************************** *)
-(* Title: Generated_Fields.thy *)
-(* Author: Martin Baillon *)
-(* ************************************************************************** *)
+(* Title: HOL/Algebra/Generated_Fields.thy
+ Author: Martin Baillon
+*)
theory Generated_Fields
-
imports Generated_Rings Subrings Multiplicative_Group
-
begin
inductive_set
@@ -184,7 +181,4 @@
subfield_gen_incl[OF carrier_is_subfield assms(1) _ assms(2)] subfieldE(1)[OF assms(1)]
by force
-
-
end
-
--- a/src/HOL/Algebra/Generated_Groups.thy Tue Jul 03 10:07:24 2018 +0100
+++ b/src/HOL/Algebra/Generated_Groups.thy Tue Jul 03 10:07:35 2018 +0100
@@ -1,11 +1,9 @@
-(* ************************************************************************** *)
-(* Title: Generated_Groups.thy *)
-(* Author: Paulo Emílio de Vilhena *)
-(* ************************************************************************** *)
+(* Title: HOL/Algebra/Generated_Groups.thy
+ Author: Paulo Emílio de Vilhena
+*)
theory Generated_Groups
imports Group Coset
-
begin
section\<open>Generated Groups\<close>
--- a/src/HOL/Algebra/Group_Action.thy Tue Jul 03 10:07:24 2018 +0100
+++ b/src/HOL/Algebra/Group_Action.thy Tue Jul 03 10:07:35 2018 +0100
@@ -1,9 +1,9 @@
-(* Title: Group_Action.thy *)
-(* Author: Paulo Emílio de Vilhena *)
+(* Title: HOL/Algebra/Group_Action.thy
+ Author: Paulo Emílio de Vilhena
+*)
theory Group_Action
imports Bij Coset Congruence
-
begin
section \<open>Group Actions\<close>
@@ -922,4 +922,4 @@
using induced_homomorphism assms group.subgroup_imp_group group_BijGroup
group_hom group_hom.axioms(1) group_hom_axioms_def by blast
-end
\ No newline at end of file
+end
--- a/src/HOL/Algebra/Ideal_Product.thy Tue Jul 03 10:07:24 2018 +0100
+++ b/src/HOL/Algebra/Ideal_Product.thy Tue Jul 03 10:07:35 2018 +0100
@@ -1,11 +1,9 @@
-(* ************************************************************************** *)
-(* Title: Ideal_Product.thy *)
-(* Author: Paulo Emílio de Vilhena *)
-(* ************************************************************************** *)
+(* Title: HOL/Algebra/Ideal_Product.thy
+ Author: Paulo Emílio de Vilhena
+*)
theory Ideal_Product
imports Ideal
-
begin
section \<open>Product of Ideals\<close>
@@ -587,4 +585,4 @@
using assms is_cring by (simp add: primeidealI)
qed
-end
\ No newline at end of file
+end
--- a/src/HOL/Algebra/Module.thy Tue Jul 03 10:07:24 2018 +0100
+++ b/src/HOL/Algebra/Module.thy Tue Jul 03 10:07:35 2018 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Algebra/Module.thy
Author: Clemens Ballarin, started 15 April 2003
- with contributions by Martin Baillon
+ with contributions by Martin Baillon
*)
theory Module
--- a/src/HOL/Algebra/Polynomials.thy Tue Jul 03 10:07:24 2018 +0100
+++ b/src/HOL/Algebra/Polynomials.thy Tue Jul 03 10:07:35 2018 +0100
@@ -1,11 +1,9 @@
-(* ************************************************************************** *)
-(* Title: Polynomials.thy *)
-(* Author: Paulo Emílio de Vilhena *)
-(* ************************************************************************** *)
+(* Title: HOL/Algebra/Polynomials.thy
+ Author: Paulo Emílio de Vilhena
+*)
theory Polynomials
imports Ring Ring_Divisibility Subrings
-
begin
section \<open>Polynomials\<close>
@@ -127,7 +125,7 @@
using degree_def[of "a # p"] by auto
also have " ... = a # p"
using Cons by simp
- finally show ?case .
+ finally show ?case .
qed
lemma coeff_nth: "i < length p \<Longrightarrow> (coeff p) i = p ! (length p - 1 - i)"
@@ -228,7 +226,7 @@
assume "p1 \<noteq> [] \<and> p2 \<noteq> []"
hence "length p1 = length p2"
using deg_eq unfolding degree_def
- by (simp add: Nitpick.size_list_simp(2))
+ by (simp add: Nitpick.size_list_simp(2))
thus ?thesis
using coeff_iff_length_cond[of p1 p2] coeff_eq by simp
next
@@ -681,7 +679,7 @@
proof -
let ?len = length and ?norm = normalize
obtain a p' where p: "p = a # p'"
- using assms(2) list.exhaust_sel by blast
+ using assms(2) list.exhaust_sel by blast
hence a: "a \<in> carrier R - { \<zero> }" and p': "set p' \<subseteq> carrier R"
using assms(1) unfolding p by (auto simp add: polynomial_def)
hence "dense_repr p = (lead_coeff p, degree p) # dense_repr p'"
@@ -742,7 +740,7 @@
next
case (Cons a p1)
let ?a_p2 = "(map (\<lambda>b. a \<otimes> b) p2) @ (replicate (degree (a # p1)) \<zero>)"
-
+
have "set (poly_mult p1 p2) \<subseteq> carrier R"
using Cons unfolding polynomial_def by auto
@@ -775,7 +773,7 @@
lemma poly_mult_coeff:
assumes "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
shows "coeff (poly_mult p1 p2) = (\<lambda>i. \<Oplus> k \<in> {..i}. (coeff p1) k \<otimes> (coeff p2) (i - k))"
- using assms(1)
+ using assms(1)
proof (induction p1)
case Nil thus ?case using assms(2) by auto
next
@@ -823,7 +821,7 @@
have "\<And>k. k \<in> {..i} \<Longrightarrow>
?f2 k \<otimes>\<^bsub>R\<^esub> ?f3 (i - k) = (if length p1 = k then a \<otimes> coeff p2 (i - k) else \<zero>)"
using in_carrier by auto
- hence "(\<Oplus> k \<in> {..i}. ?f2 k \<otimes> ?f3 (i - k)) =
+ hence "(\<Oplus> k \<in> {..i}. ?f2 k \<otimes> ?f3 (i - k)) =
(\<Oplus> k \<in> {..i}. (if length p1 = k then a \<otimes> coeff p2 (i - k) else \<zero>))"
using in_carrier
add.finprod_cong'[of "{..i}" "{..i}" "\<lambda>k. ?f2 k \<otimes> ?f3 (i - k)"
@@ -848,7 +846,7 @@
using in_carrier(1) assms(2) by auto
moreover have "set (poly_mult p1 p2) \<subseteq> carrier R"
- using poly_mult_is_polynomial[of p1 p2] polynomial_in_carrier assms(2) Cons(2) by auto
+ using poly_mult_is_polynomial[of p1 p2] polynomial_in_carrier assms(2) Cons(2) by auto
ultimately
have "coeff (poly_mult (a # p1) p2) = (\<lambda>i. ((coeff ?a_p2) i) \<oplus> ((coeff (poly_mult p1 p2)) i))"
@@ -910,7 +908,7 @@
and "polynomial R (poly_add (poly_mult p1 p3) (poly_mult p2 p3))"
using assms poly_add_is_polynomial poly_mult_is_polynomial polynomial_in_carrier by auto
ultimately show ?thesis
- using coeff_iff_polynomial_cond by auto
+ using coeff_iff_polynomial_cond by auto
qed
lemma poly_mult_l_distr:
@@ -938,7 +936,7 @@
normalize_replicate_zero[of "length p2 + length p1" "[]"] by auto
finally show ?thesis by auto
qed } note aux_lemma = this
-
+
from assms show ?thesis
proof (induction n)
case 0 thus ?case by simp
@@ -988,7 +986,7 @@
using inj_on_def by force
moreover have "(\<lambda>k. i - k) ` {..i} \<subseteq> {..i}" by auto
hence "(\<lambda>k. i - k) ` {..i} = {..i}"
- using reindex_inj endo_inj_surj[of "{..i}" "\<lambda>k. i - k"] by simp
+ using reindex_inj endo_inj_surj[of "{..i}" "\<lambda>k. i - k"] by simp
ultimately have "(\<Oplus>k \<in> {..i}. ?f k) = (\<Oplus>k \<in> {..i}. ?f (i - k))"
using add.finprod_reindex[of ?f "\<lambda>k. i - k" "{..i}"] in_carrier by auto
@@ -1041,7 +1039,7 @@
using poly_add_normalize(1)[of "replicate (length p + n) \<zero>" "[]"]
normalize_replicate_zero[of "length p + n" "[]"] by auto
also have " ... = []" by simp
- finally show ?case .
+ finally show ?case .
qed
thus "poly_mult p (replicate n \<zero>) = []"
using poly_mult_comm[OF assms in_carrier] by simp
@@ -1061,9 +1059,9 @@
next
case (Cons b ps)
hence "a \<otimes> lead_coeff p \<noteq> \<zero>"
- using assms integral[of a "lead_coeff p"] unfolding polynomial_def by auto
+ using assms integral[of a "lead_coeff p"] unfolding polynomial_def by auto
thus ?thesis
- using Cons polynomial_in_carrier[OF assms(1)] assms(2) unfolding polynomial_def by auto
+ using Cons polynomial_in_carrier[OF assms(1)] assms(2) unfolding polynomial_def by auto
qed
ultimately show ?thesis
using poly_add_zero(1)[of "map (\<lambda>b. a \<otimes> b) p"] by simp
@@ -1086,7 +1084,7 @@
hence "lead_coeff ((map (\<lambda>b. a \<otimes> b) p) @ (replicate n \<zero>)) \<noteq> \<zero>"
using Cons assms integral[of a b] unfolding polynomial_def by auto
moreover have "set ((map (\<lambda>b. a \<otimes> b) p) @ (replicate n \<zero>)) \<subseteq> carrier R"
- using polynomial_in_carrier[OF assms(1)] assms(2) DiffD1 by auto
+ using polynomial_in_carrier[OF assms(1)] assms(2) DiffD1 by auto
ultimately have is_polynomial: "polynomial R ((map (\<lambda>b. a \<otimes> b) p) @ (replicate n \<zero>))"
using Cons unfolding polynomial_def by auto
@@ -1107,7 +1105,7 @@
shows "poly_mult [ \<one> ] p = p" and "poly_mult p [ \<one> ] = p"
proof -
have "map (\<lambda>a. \<one> \<otimes> a) p = p"
- using polynomial_in_carrier[OF assms] by (meson assms l_one map_idI subsetCE)
+ using polynomial_in_carrier[OF assms] by (meson assms l_one map_idI subsetCE)
thus "poly_mult [ \<one> ] p = p" and "poly_mult p [ \<one> ] = p"
using poly_mult_const[OF assms, of \<one>] by auto
qed
@@ -1119,7 +1117,7 @@
have p1: "lead_coeff p1 \<in> carrier R - { \<zero> }" and p2: "lead_coeff p2 \<in> carrier R - { \<zero> }"
using assms unfolding polynomial_def by auto
- have "(coeff (poly_mult p1 p2)) (degree p1 + degree p2) =
+ have "(coeff (poly_mult p1 p2)) (degree p1 + degree p2) =
(\<Oplus> k \<in> {..((degree p1) + (degree p2))}.
(coeff p1) k \<otimes> (coeff p2) ((degree p1) + (degree p2) - k))"
using poly_mult_coeff assms(1-2) polynomial_in_carrier by auto
@@ -1299,7 +1297,7 @@
also have " ... = (\<Oplus>i \<in> {..n - ?len}. (a \<otimes> ?c2 i) \<otimes> ?c3 (n - (i + ?len)))"
unfolding h_def by simp
also have " ... = (\<Oplus>i \<in> {..n - ?len}. a \<otimes> (?c2 i \<otimes> ?c3 (n - (i + ?len))))"
- using in_carrier assms(3) by (simp add: m_assoc)
+ using in_carrier assms(3) by (simp add: m_assoc)
also have " ... = a \<otimes> (\<Oplus>i \<in> {..n - ?len}. ?c2 i \<otimes> ?c3 (n - (i + ?len)))"
using finsum_rdistr[of "{..n - ?len}" a "\<lambda>i. ?c2 i \<otimes> ?c3 (n - (i + ?len))"]
in_carrier(2-3) assms(3) by simp
@@ -1427,10 +1425,10 @@
proof (auto)
fix p assume p: "polynomial R p"
have "polynomial R [ \<ominus> \<one> ]"
- unfolding polynomial_def using r_neg by fastforce
+ unfolding polynomial_def using r_neg by fastforce
hence cond0: "polynomial R (poly_mult [ \<ominus> \<one> ] p)"
using poly_mult_closed[of "[ \<ominus> \<one> ]" p] p by simp
-
+
have "poly_add p (poly_mult [ \<ominus> \<one> ] p) = poly_add (poly_mult [ \<one> ] p) (poly_mult [ \<ominus> \<one> ] p)"
using poly_mult_one[OF p] by simp
also have " ... = poly_mult (poly_add [ \<one> ] [ \<ominus> \<one> ]) p"
@@ -1498,51 +1496,6 @@
(auto simp add: univ_poly_def domain.poly_mult_integral[OF assms])
qed
-lemma (in domain) univ_poly_a_inv_def':
- assumes "p \<in> carrier (univ_poly R)"
- shows "\<ominus>\<^bsub>(univ_poly R)\<^esub> p = map (\<lambda>a. \<ominus> a) p"
-proof -
- have aux_lemma:
- "\<And>p. p \<in> carrier (univ_poly R) \<Longrightarrow> p \<oplus>\<^bsub>(univ_poly R)\<^esub> (map (\<lambda>a. \<ominus> a) p) = []"
- "\<And>p. p \<in> carrier (univ_poly R) \<Longrightarrow> (map (\<lambda>a. \<ominus> a) p) \<in> carrier (univ_poly R)"
- proof -
- fix p assume p: "p \<in> carrier (univ_poly R)"
- hence set_p: "set p \<subseteq> carrier R"
- unfolding univ_poly_def polynomial_def by auto
- show "(map (\<lambda>a. \<ominus> a) p) \<in> carrier (univ_poly R)"
- proof (cases "p = []")
- assume "p = []" thus ?thesis
- unfolding univ_poly_def polynomial_def by auto
- next
- assume not_nil: "p \<noteq> []"
- hence "lead_coeff p \<noteq> \<zero>"
- using p unfolding univ_poly_def polynomial_def by auto
- moreover have "lead_coeff (map (\<lambda>a. \<ominus> a) p) = \<ominus> (lead_coeff p)"
- using not_nil by (simp add: hd_map)
- ultimately have "lead_coeff (map (\<lambda>a. \<ominus> a) p) \<noteq> \<zero>"
- using hd_in_set local.minus_zero not_nil set_p by force
- moreover have "set (map (\<lambda>a. \<ominus> a) p) \<subseteq> carrier R"
- using set_p by (induct p) (auto)
- ultimately show ?thesis
- unfolding univ_poly_def polynomial_def by auto
- qed
-
- have "map2 (\<oplus>) p (map (\<lambda>a. \<ominus> a) p) = replicate (length p) \<zero>"
- using set_p by (induct p) (auto simp add: r_neg)
- thus "p \<oplus>\<^bsub>(univ_poly R)\<^esub> (map (\<lambda>a. \<ominus> a) p) = []"
- unfolding univ_poly_def using normalize_replicate_zero[of "length p" "[]"] by auto
- qed
-
- interpret UP: ring "univ_poly R"
- using univ_poly_is_ring[OF domain_axioms] .
-
- from aux_lemma
- have "\<And>p. p \<in> carrier (univ_poly R) \<Longrightarrow> \<ominus>\<^bsub>(univ_poly R)\<^esub> p = map (\<lambda>a. \<ominus> a) p"
- by (metis Nil_is_map_conv UP.add.inv_closed UP.l_zero UP.r_neg1 UP.r_zero UP.zero_closed)
- thus ?thesis
- using assms by simp
-qed
-
subsection \<open>Long Division Theorem\<close>
@@ -1564,7 +1517,7 @@
proof (cases "length b > length p")
assume "length b > length p"
hence "p = [] \<or> degree p < degree b" unfolding degree_def
- by (meson diff_less_mono length_0_conv less_one not_le)
+ by (meson diff_less_mono length_0_conv less_one not_le)
hence "?long_division p [] p"
using poly_add_zero[OF less(2)] less(2) zero_is_polynomial
poly_mult_zero[OF less(3)] by simp
@@ -1591,7 +1544,7 @@
hence s_coeff: "lead_coeff s = (\<ominus> a)"
using poly_mult_lead_coeff[OF monon_is_polynomial[OF in_carrier] less(3)] a c
unfolding monon_def s_def b using m_assoc by force
-
+
have "degree s = degree (monon ((\<ominus> a) \<otimes> inv c) (?len p - ?len b)) + degree b"
using poly_mult_degree_eq[OF monon_is_polynomial[OF in_carrier] less(3)]
unfolding s_def b monon_def by auto
@@ -1605,7 +1558,7 @@
by (simp add: Nitpick.size_list_simp(2) local.Cons)
obtain s' where s: "s = (\<ominus> a) # s'"
- using s_coeff len_eq by (metis \<open>s \<noteq> []\<close> hd_Cons_tl)
+ using s_coeff len_eq by (metis \<open>s \<noteq> []\<close> hd_Cons_tl)
define p_diff where "p_diff = poly_add p s"
hence "?len p_diff < ?len p"
@@ -1623,7 +1576,7 @@
using s_def monon_is_polynomial[OF in_carrier(1)] by auto
have in_univ_carrier:
"p \<in> carrier (univ_poly R)" "m \<in> carrier (univ_poly R)" "b \<in> carrier (univ_poly R)"
- "r' \<in> carrier (univ_poly R)" "q' \<in> carrier (univ_poly R)"
+ "r' \<in> carrier (univ_poly R)" "q' \<in> carrier (univ_poly R)"
using r' q' less(2-3) m(1) unfolding univ_poly_def by auto
hence "poly_add p (poly_mult m b) = poly_add (poly_mult b q') r'"
@@ -1634,7 +1587,7 @@
"(p \<oplus>\<^bsub>(univ_poly R)\<^esub> (m \<otimes>\<^bsub>(univ_poly R)\<^esub> b)) \<ominus>\<^bsub>(univ_poly R)\<^esub> (m \<otimes>\<^bsub>(univ_poly R)\<^esub> b) =
((b \<otimes>\<^bsub>(univ_poly R)\<^esub>q') \<oplus>\<^bsub>(univ_poly R)\<^esub> r') \<ominus>\<^bsub>(univ_poly R)\<^esub> (m \<otimes>\<^bsub>(univ_poly R)\<^esub> b)"
by simp
- hence "p = (b \<otimes>\<^bsub>(univ_poly R)\<^esub> (q' \<ominus>\<^bsub>(univ_poly R)\<^esub> m)) \<oplus>\<^bsub>(univ_poly R)\<^esub> r'"
+ hence "p = (b \<otimes>\<^bsub>(univ_poly R)\<^esub> (q' \<ominus>\<^bsub>(univ_poly R)\<^esub> m)) \<oplus>\<^bsub>(univ_poly R)\<^esub> r'"
using in_univ_carrier by algebra
hence "p = poly_add (poly_mult b (q' \<ominus>\<^bsub>(univ_poly R)\<^esub> m)) r'"
unfolding univ_poly_def by simp
@@ -1656,7 +1609,7 @@
using long_division_theorem[OF assms] assms lead_coeff_not_zero[of "hd b" "tl b"]
by (simp add: field_Units)
-theorem univ_poly_is_euclidean:
+lemma univ_poly_is_euclidean_domain:
assumes "field R"
shows "euclidean_domain (univ_poly R) degree"
proof -
@@ -1668,16 +1621,6 @@
using field.field_long_division_theorem[OF assms] by auto
qed
-corollary univ_poly_is_principal:
- assumes "field R"
- shows "principal_domain (univ_poly R)"
-proof -
- interpret UP: euclidean_domain "univ_poly R" degree
- using univ_poly_is_euclidean[OF assms] .
- show ?thesis
- using UP.principal_domain_axioms .
-qed
-
subsection \<open>Consistency Rules\<close>
@@ -1707,7 +1650,7 @@
qed
lemma (in ring) poly_add_consistent [simp]:
- assumes "subring K R" shows "ring.poly_add (R \<lparr> carrier := K \<rparr>) = poly_add"
+ assumes "subring K R" shows "ring.poly_add (R \<lparr> carrier := K \<rparr>) = poly_add"
proof -
have "\<And>p q. ring.poly_add (R \<lparr> carrier := K \<rparr>) p q = poly_add p q"
proof -
@@ -1721,7 +1664,7 @@
assumes "subring K R" shows "ring.poly_mult (R \<lparr> carrier := K \<rparr>) = poly_mult"
proof -
have "\<And>p q. ring.poly_mult (R \<lparr> carrier := K \<rparr>) p q = poly_mult p q"
- proof -
+ proof -
fix p q show "ring.poly_mult (R \<lparr> carrier := K \<rparr>) p q = poly_mult p q"
using ring.poly_mult.simps[OF subring_is_ring[OF assms]] poly_add_consistent[OF assms]
by (induct p) (auto)
@@ -1729,7 +1672,7 @@
thus ?thesis by auto
qed
-lemma (in ring) univ_poly_subring_def':
+lemma (in ring) univ_poly_carrier_change_def':
assumes "subring K R"
shows "univ_poly (R \<lparr> carrier := K \<rparr>) = (univ_poly R) \<lparr> carrier := { p. polynomial R p \<and> set p \<subseteq> K } \<rparr>"
unfolding univ_poly_def polynomial_def
@@ -1738,26 +1681,6 @@
subringE(1)[OF assms]
by auto
-lemma (in domain) univ_poly_subring_is_domain:
- assumes "subring K R"
- shows "domain (univ_poly (R \<lparr> carrier := K \<rparr>))"
-proof -
- have "domain (R \<lparr> carrier := K \<rparr>)"
- using subdomainI'[OF assms] unfolding subdomain_iff[OF subringE(1)[OF assms]] .
- thus ?thesis
- using univ_poly_is_domain[of "R \<lparr> carrier := K \<rparr>"] by simp
-qed
-
-lemma (in domain) univ_poly_subfield_is_euclidean:
- assumes "subfield K R"
- shows "euclidean_domain (univ_poly (R \<lparr> carrier := K \<rparr>)) degree"
- using univ_poly_is_euclidean[OF subfield_iff(2)[OF assms]] .
-
-lemma (in domain) univ_poly_subfield_is_principal:
- assumes "subfield K R"
- shows "principal_domain (univ_poly (R \<lparr> carrier := K \<rparr>))"
- using univ_poly_is_principal[OF subfield_iff(2)[OF assms]] .
-
subsection \<open>The Evaluation Homomorphism\<close>
@@ -1886,7 +1809,7 @@
hence "set (map ((\<otimes>) b) q) \<subseteq> carrier R" and "set (replicate n \<zero>) \<subseteq> carrier R"
using assms(2) by (induct q) (auto)
hence "eval ((map ((\<otimes>) b) q) @ (replicate n \<zero>)) a = (eval ((map ((\<otimes>) b) q)) a) \<otimes> (a [^] n) \<oplus> \<zero>"
- using eval_append[OF _ _ assms(3), of "map ((\<otimes>) b) q" "replicate n \<zero>"]
+ using eval_append[OF _ _ assms(3), of "map ((\<otimes>) b) q" "replicate n \<zero>"]
eval_replicate[OF _ assms(3), of "[]"] by auto
moreover have "eval (map ((\<otimes>) b) q) a = b \<otimes> eval q a"
using assms(2-3) eval_in_carrier b by(induct q) (auto simp add: degree_def m_assoc r_distr)
@@ -1920,309 +1843,10 @@
proposition (in cring) eval_is_hom:
assumes "subring K R" and "a \<in> carrier R"
shows "(\<lambda>p. (eval p) a) \<in> ring_hom (univ_poly (R \<lparr> carrier := K \<rparr>)) R"
- unfolding univ_poly_subring_def'[OF assms(1)]
+ unfolding univ_poly_carrier_change_def'[OF assms(1)]
using polynomial_in_carrier eval_in_carrier eval_poly_add eval_poly_mult assms(2)
by (auto intro!: ring_hom_memI
simp add: univ_poly_def degree_def
simp del: poly_add.simps poly_mult.simps)
-theorem (in domain) eval_cring_hom:
- assumes "subring K R" and "a \<in> carrier R"
- shows "ring_hom_cring (univ_poly (R \<lparr> carrier := K \<rparr>)) R (\<lambda>p. (eval p) a)"
- unfolding ring_hom_cring_def ring_hom_cring_axioms_def
- using domain.axioms(1)[OF univ_poly_subring_is_domain[OF assms(1)]]
- eval_is_hom[OF assms] cring_axioms by auto
-
-corollary (in domain) eval_ring_hom:
- assumes "subring K R" and "a \<in> carrier R"
- shows "ring_hom_ring (univ_poly (R \<lparr> carrier := K \<rparr>)) R (\<lambda>p. (eval p) a)"
- using eval_cring_hom[OF assms] ring_hom_ringI2
- unfolding ring_hom_cring_def ring_hom_cring_axioms_def cring_def by auto
-
-
-subsection \<open>The Reduction Map and Uniqueness of The Evaluation Homomorphism\<close>
-
-definition (in ring) reduction_map :: "('c \<Rightarrow> 'a) \<Rightarrow> 'c list \<Rightarrow> 'a list"
- where "reduction_map h = (\<lambda>p. normalize (map h p))"
-
-(*
-lemma (in ring_hom_ring)
- "(reduction_map h) \<in> ring_hom (univ_poly R) (univ_poly S)"
- sorry
-*)
-
-
-subsection \<open>Divisibility of Polynomials\<close>
-
-definition pirreducible :: "_ \<Rightarrow> 'a list \<Rightarrow> bool"
- where "pirreducible R p \<longleftrightarrow> irreducible (mult_of (univ_poly R)) p"
-
-definition pprime :: "_ \<Rightarrow> 'a list \<Rightarrow> bool"
- where "pprime R p \<longleftrightarrow> prime (mult_of (univ_poly R)) p"
-
-definition rupture :: "_ \<Rightarrow> 'a list \<Rightarrow> _"
- where "rupture R p = (univ_poly R) Quot (PIdl\<^bsub>(univ_poly R)\<^esub> p)"
-
-
-text \<open>Be aware of Nil!\<close>
-lemma (in domain) Nil_is_pirreducible: "pirreducible R []"
- unfolding pirreducible_def using poly_mult_integral
- by (auto intro!: irreducibleI simp add: Units_def univ_poly_def properfactor_def factor_def, force)
-
-lemma (in field) pprime_iff_ppirreducible:
- assumes "polynomial R p" and "p \<noteq> []"
- shows "pprime R p \<longleftrightarrow> pirreducible R p"
-proof -
- have "p \<in> carrier (mult_of (univ_poly R))"
- using assms unfolding univ_poly_def by auto
- thus ?thesis
- using principal_domain.primeness_condition[OF univ_poly_is_principal[OF field_axioms]]
- unfolding pprime_def pirreducible_def by simp
-qed
-
-lemma (in field) rupture_field:
- assumes "polynomial R p" and "p \<noteq> []"
- shows "field (rupture R p) \<longleftrightarrow> pirreducible R p"
-proof -
- have "p \<in> carrier (mult_of (univ_poly R))"
- using assms(1-2) unfolding univ_poly_def by auto
- thus ?thesis
- using principal_domain.field_iff_prime[OF univ_poly_is_principal[OF field_axioms]]
- pprime_iff_ppirreducible[OF assms]
- unfolding pprime_def rupture_def by simp
-qed
-
-lemma (in field) univ_poly_units:
- "Units (univ_poly R) = { [ k ] | k. k \<in> carrier R - { \<zero> } }"
-proof
- show "Units (univ_poly R) \<subseteq> { [ k ] | k. k \<in> carrier R - { \<zero> } }"
- proof
- fix p assume "p \<in> Units (univ_poly R)"
- then obtain q where p: "polynomial R p" and q: "polynomial R q" and pq: "poly_mult p q = [ \<one> ]"
- unfolding Units_def univ_poly_def by auto
- hence not_nil: "p \<noteq> []" and "q \<noteq> []"
- using poly_mult_integral[OF p q] poly_mult_zero[OF p] by auto
- hence "degree p = 0"
- using poly_mult_degree_eq[OF p q] unfolding pq degree_def by simp
- hence "length p = 1"
- using not_nil unfolding degree_def by (metis One_nat_def Suc_pred length_greater_0_conv)
- then obtain k where k: "p = [ k ]"
- by (metis One_nat_def length_0_conv length_Suc_conv)
- hence "k \<in> carrier R - { \<zero> }"
- using p unfolding polynomial_def by auto
- thus "p \<in> { [ k ] | k. k \<in> carrier R - { \<zero> } }"
- unfolding k by blast
- qed
-next
- show "{ [ k ] | k. k \<in> carrier R - { \<zero> } } \<subseteq> Units (univ_poly R)"
- proof (auto)
- fix k assume k: "k \<in> carrier R" "k \<noteq> \<zero>"
- hence inv_k: "inv k \<in> carrier R" "inv k \<noteq> \<zero>" and "k \<otimes> inv k = \<one>" "inv k \<otimes> k = \<one>"
- using subfield_m_inv[OF carrier_is_subfield, of k] by auto
- hence "poly_mult [ k ] [ inv k ] = [ \<one> ]" and "poly_mult [ inv k ] [ k ] = [ \<one> ]"
- by (auto simp add: degree_def k)
- moreover have "polynomial R [ k ]" and "polynomial R [ inv k ]"
- using const_is_polynomial k inv_k by auto
- ultimately show "[ k ] \<in> Units (univ_poly R)"
- unfolding Units_def univ_poly_def by (auto simp del: poly_mult.simps)
- qed
-qed
-
-corollary (in field) univ_poly_not_field: "\<not> field (univ_poly R)"
-proof -
- have "[ \<one>, \<zero> ] \<in> carrier (univ_poly R) - { \<zero>\<^bsub>(univ_poly R)\<^esub> }"
- and "[ \<one>, \<zero> ] \<notin> { [ k ] | k. k \<in> carrier R - { \<zero> } }"
- unfolding univ_poly_def polynomial_def by auto
- thus ?thesis
- using field.field_Units[of "univ_poly R"]
- unfolding univ_poly_units by blast
-qed
-
-text \<open>A stronger version for one sense of rupture_field lemma.\<close>
-corollary (in field) rupture_field_imp_pirreducible:
- assumes "polynomial R p" and "field (rupture R p)"
- shows "p \<noteq> []" and "pirreducible R p"
-proof -
- interpret UP: domain "univ_poly R"
- using univ_poly_is_domain[OF domain_axioms] .
-
- show "p \<noteq> []"
- proof (rule ccontr)
- assume "\<not> p \<noteq> []"
- hence nil: "p = []" "p = \<zero>\<^bsub>(univ_poly R)\<^esub>"
- unfolding univ_poly_def by simp+
- hence "rupture R p = (univ_poly R) Quot { \<zero>\<^bsub>(univ_poly R)\<^esub> }"
- unfolding rupture_def
- using UP.genideal_zero UP.cgenideal_eq_genideal[OF UP.zero_closed] by simp
- hence "rupture R p \<simeq> univ_poly R"
- using UP.FactRing_zeroideal(1) by simp
- then obtain h where h: "h \<in> ring_iso (rupture R p) (univ_poly R)"
- unfolding is_ring_iso_def by blast
- moreover have "ring (rupture R p)"
- using assms(2) by (simp add: cring_def domain_def field_def)
- ultimately interpret ring_hom_ring "rupture R p" "univ_poly R" h
- unfolding ring_hom_ring_def ring_hom_ring_axioms_def ring_iso_def
- using UP.is_ring by simp
- have "field (univ_poly R)"
- using field.ring_iso_imp_img_field[OF assms(2) h] by simp
- thus False
- using univ_poly_not_field by simp
- qed
- thus "pirreducible R p"
- using rupture_field assms by simp
-qed
-
-lemma (in field) associated_polynomials_iff:
- assumes "polynomial R p" and "polynomial R q"
- shows "p \<sim>\<^bsub>(univ_poly R)\<^esub> q \<longleftrightarrow> (\<exists>k \<in> carrier R - { \<zero> }. p = map (\<lambda>a. k \<otimes> a) q)"
-proof
- interpret UP: principal_domain "univ_poly R"
- using univ_poly_is_principal[OF field_axioms] .
-
- assume A: "p \<sim>\<^bsub>(univ_poly R)\<^esub> q"
- then obtain r1 r2
- where r1: "polynomial R r1" "p = poly_mult q r1"
- and r2: "polynomial R r2" "q = poly_mult p r2"
- unfolding associated_def factor_def univ_poly_def by auto
-
- show "\<exists>k \<in> carrier R - { \<zero> }. p = map (\<lambda>a. k \<otimes> a) q"
- proof (cases "p = []")
- assume "p = []" thus ?thesis
- using poly_mult_zero[OF r2(1)] r2(2) by auto
- next
- assume p: "p \<noteq> []" hence q: "q \<noteq> []"
- using poly_mult_zero[OF r1(1)] r1(2) by auto
- hence "p \<in> carrier (mult_of (univ_poly R))" and "q \<in> carrier (mult_of (univ_poly R))"
- using p assms unfolding univ_poly_def by auto
- moreover have "p \<sim>\<^bsub>mult_of (univ_poly R)\<^esub> q"
- using p UP.assoc_imp_assoc_mult[OF _ _ A] assms unfolding univ_poly_def by auto
- ultimately obtain r where r: "r \<in> Units (univ_poly R)" "p = q \<otimes>\<^bsub>(univ_poly R)\<^esub> r"
- using UP.mult_of.associatedD2[of p q] UP.Units_mult_eq_Units by blast
- then obtain k where k: "k \<in> carrier R - { \<zero> }" "r = [ k ]"
- using univ_poly_units UP.m_comm[of q r] by auto
- moreover have "p = poly_mult r q"
- using r UP.m_comm[of q r] q assms unfolding Units_def univ_poly_def by auto
- ultimately show ?thesis
- using poly_mult_const(1)[OF assms(2) k(1)] unfolding k(2) by auto
- qed
-next
- assume "\<exists>k \<in> carrier R - { \<zero> }. p = map (\<lambda>a. k \<otimes> a) q"
- then obtain k where k: "k \<in> carrier R - { \<zero> }" "p = map (\<lambda>a. k \<otimes> a) q"
- by blast
- hence inv_k: "inv k \<in> carrier R - { \<zero> }" "inv k \<otimes> k = \<one>"
- using subfield_m_inv[OF carrier_is_subfield k(1)] by simp+
- moreover have "map (\<lambda>a. inv k \<otimes> a) (map (\<lambda>a. k \<otimes> a) q) = q"
- using inv_k polynomial_in_carrier[OF assms(2)] k(1) m_assoc m_comm by (induct q) (auto)
- hence "q = map (\<lambda>a. inv k \<otimes> a) p"
- using k(2) by simp
- ultimately have "p = poly_mult q [ k ]" and "q = poly_mult p [ inv k ]"
- using poly_mult_const(2)[OF assms(2) k(1)]
- poly_mult_const(2)[OF assms(1) inv_k(1)] k(2) by auto
- moreover have "polynomial R [ k ]" and "polynomial R [ inv k ]"
- using const_is_polynomial k inv_k by auto
- ultimately show "p \<sim>\<^bsub>(univ_poly R)\<^esub> q"
- unfolding univ_poly_def associated_def factor_def
- by (auto simp del: poly_mult.simps)
-qed
-
-lemma (in cring) ideal_eq_carrier_iff: (* <- Move to Ideal.thy *)
- assumes "a \<in> carrier R"
- shows "carrier R = PIdl a \<longleftrightarrow> a \<in> Units R"
-proof
- assume "carrier R = PIdl a"
- hence "\<one> \<in> PIdl a"
- by auto
- then obtain b where "b \<in> carrier R" "\<one> = a \<otimes> b" "\<one> = b \<otimes> a"
- unfolding cgenideal_def using m_comm[OF assms] by auto
- thus "a \<in> Units R"
- using assms unfolding Units_def by auto
-next
- assume "a \<in> Units R"
- then have inv_a: "inv a \<in> carrier R" "inv a \<otimes> a = \<one>"
- by auto
- have "carrier R \<subseteq> PIdl a"
- proof
- fix b assume "b \<in> carrier R"
- hence "(b \<otimes> inv a) \<otimes> a = b" and "b \<otimes> inv a \<in> carrier R"
- using m_assoc[OF _ inv_a(1) assms] inv_a by auto
- thus "b \<in> PIdl a"
- unfolding cgenideal_def by force
- qed
- thus "carrier R = PIdl a"
- using assms by (simp add: cgenideal_eq_rcos r_coset_subset_G subset_antisym)
-qed
-
-text \<open>We don't suppose that x is algebraic, because, in our definition, [] is pirreducible.\<close>
-lemma (in field) exists_ker_generator_pirreducible:
- assumes "x \<in> carrier R - { \<zero> }"
- shows "\<exists>p. polynomial R p \<and>
- pirreducible R p \<and>
- a_kernel (univ_poly R) R (\<lambda>p. eval p x) = PIdl\<^bsub>(univ_poly R)\<^esub> p"
- (is "\<exists>p. polynomial R p \<and> ?pirr R p \<and> ?a_ker p = ?PIdl p")
-proof -
- interpret UP: principal_domain "univ_poly R"
- using univ_poly_is_principal[OF field_axioms] by simp
-
- have ker: "ideal (a_kernel (univ_poly R) R (\<lambda>p. eval p x)) (univ_poly R)"
- using ring_hom_ring.kernel_is_ideal[OF eval_ring_hom[OF carrier_is_subring]] assms by simp
- obtain p where in_carrier: "p \<in> carrier (univ_poly R)" and p: "?a_ker p = ?PIdl p"
- using principalideal.generate[OF UP.principal_I[OF ker]] UP.cgenideal_eq_genideal by auto
- hence poly: "polynomial R p"
- unfolding univ_poly_def by simp
-
- show ?thesis
- proof (cases "p = []")
- assume "p = []" thus ?thesis
- using poly Nil_is_pirreducible p by auto
- next
- assume not_Nil: "p \<noteq> []"
-
- have "eval (monon \<one> (Suc 0)) x = x"
- using assms eval_monon[of \<one> x "Suc 0"] by auto
- moreover have "monon \<one> (Suc 0) \<in> carrier (univ_poly R)"
- using monon_is_polynomial unfolding univ_poly_def by auto
- ultimately have "?a_ker p \<noteq> carrier (univ_poly R)"
- unfolding a_kernel_def' using assms by force
- hence not_unit: "p \<notin> Units (mult_of (univ_poly R))"
- using p UP.ideal_eq_carrier_iff by auto
-
- have "pprime R p"
- unfolding pprime_def
- proof (rule primeI[OF not_unit])
- fix a b
- assume "a \<in> carrier (mult_of (univ_poly R))"
- and "b \<in> carrier (mult_of (univ_poly R))"
- and "p divides\<^bsub>mult_of (univ_poly R)\<^esub> (a \<otimes>\<^bsub>mult_of (univ_poly R)\<^esub> b)"
- then obtain c
- where a: "polynomial R a" "a \<noteq> []" and b: "polynomial R b" "b \<noteq> []" and c: "polynomial R c" "c \<noteq> []"
- and dvd: "poly_mult a b = poly_mult p c"
- unfolding univ_poly_def factor_def by auto
- hence "(eval a x) \<otimes> (eval b x) = (eval p x) \<otimes> (eval c x)"
- using eval_poly_mult[of a b x] eval_poly_mult[of p c x] poly
- polynomial_in_carrier assms by auto
- moreover have "eval p x = \<zero>"
- using p UP.cgenideal_self[OF in_carrier] unfolding a_kernel_def' by auto
- ultimately have "(eval a x) \<otimes> (eval b x) = \<zero>"
- using eval_in_carrier[OF polynomial_in_carrier[OF c(1)]] assms by auto
- hence "(eval a x) = \<zero> \<or> (eval b x) = \<zero>"
- using integral eval_in_carrier polynomial_in_carrier a b assms by auto
- moreover
- have "\<And>a. \<lbrakk> polynomial R a; a \<noteq> []; (eval a x) = \<zero> \<rbrakk> \<Longrightarrow> p divides\<^bsub>mult_of (univ_poly R)\<^esub> a"
- proof -
- fix a assume a: "polynomial R a" "a \<noteq> []" "(eval a x) = \<zero>"
- hence "a \<in> ?PIdl p"
- using p unfolding a_kernel_def' univ_poly_def by auto
- hence "p divides\<^bsub>(univ_poly R)\<^esub> a"
- using UP.m_comm[OF in_carrier] unfolding cgenideal_def factor_def by auto
- thus "p divides\<^bsub>mult_of (univ_poly R)\<^esub> a"
- using UP.divides_imp_divides_mult[OF in_carrier] a unfolding univ_poly_def by auto
- qed
- ultimately show "p divides\<^bsub>mult_of (univ_poly R)\<^esub> a \<or> p divides\<^bsub>mult_of (univ_poly R)\<^esub> b"
- using a b by blast
- qed
- thus ?thesis
- using poly p unfolding pprime_iff_ppirreducible[OF poly not_Nil] by auto
- qed
-qed
-
end
--- a/src/HOL/Algebra/QuotRing.thy Tue Jul 03 10:07:24 2018 +0100
+++ b/src/HOL/Algebra/QuotRing.thy Tue Jul 03 10:07:35 2018 +0100
@@ -1,7 +1,6 @@
(* Title: HOL/Algebra/QuotRing.thy
Author: Stephan Hohe
Author: Paulo Emílio de Vilhena
-
*)
theory QuotRing
--- a/src/HOL/Algebra/Ring.thy Tue Jul 03 10:07:24 2018 +0100
+++ b/src/HOL/Algebra/Ring.thy Tue Jul 03 10:07:35 2018 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/Algebra/Ring.thy
Author: Clemens Ballarin, started 9 December 1996
-With contributions by Martin Baillon
+With contributions by Martin Baillon.
*)
theory Ring
--- a/src/HOL/Algebra/Ring_Divisibility.thy Tue Jul 03 10:07:24 2018 +0100
+++ b/src/HOL/Algebra/Ring_Divisibility.thy Tue Jul 03 10:07:35 2018 +0100
@@ -1,12 +1,30 @@
-(* ************************************************************************** *)
-(* Title: Ring_Divisibility.thy *)
-(* Author: Paulo Emílio de Vilhena *)
-(* ************************************************************************** *)
+(* Title: HOL/Algebra/Ring_Divisibility.thy
+ Author: Paulo Emílio de Vilhena
+*)
theory Ring_Divisibility
-imports Ideal Divisibility QuotRing Multiplicative_Group
+imports Ideal Divisibility QuotRing
+begin
+
+section \<open>Definitions ported from @{text "Multiplicative_Group.thy"}\<close>
+
+definition mult_of :: "('a, 'b) ring_scheme \<Rightarrow> 'a monoid" where
+ "mult_of R \<equiv> \<lparr> carrier = carrier R - { \<zero>\<^bsub>R\<^esub> }, mult = mult R, one = \<one>\<^bsub>R\<^esub> \<rparr>"
+
+lemma carrier_mult_of [simp]: "carrier (mult_of R) = carrier R - { \<zero>\<^bsub>R\<^esub> }"
+ by (simp add: mult_of_def)
-begin
+lemma mult_mult_of [simp]: "mult (mult_of R) = mult R"
+ by (simp add: mult_of_def)
+
+lemma nat_pow_mult_of: "([^]\<^bsub>mult_of R\<^esub>) = (([^]\<^bsub>R\<^esub>) :: _ \<Rightarrow> nat \<Rightarrow> _)"
+ by (simp add: mult_of_def fun_eq_iff nat_pow_def)
+
+lemma one_mult_of [simp]: "\<one>\<^bsub>mult_of R\<^esub> = \<one>\<^bsub>R\<^esub>"
+ by (simp add: mult_of_def)
+
+lemmas mult_of_simps = carrier_mult_of mult_mult_of nat_pow_mult_of one_mult_of
+
section \<open>The Arithmetic of Rings\<close>
@@ -107,14 +125,14 @@
lemma (in cring) to_contain_is_to_divide:
assumes "a \<in> carrier R" "b \<in> carrier R"
shows "(PIdl b \<subseteq> PIdl a) = (a divides b)"
-proof
+proof
show "PIdl b \<subseteq> PIdl a \<Longrightarrow> a divides b"
proof -
assume "PIdl b \<subseteq> PIdl a"
hence "b \<in> PIdl a"
by (meson assms(2) local.ring_axioms ring.cgenideal_self subsetCE)
thus ?thesis
- unfolding factor_def cgenideal_def using m_comm assms(1) by blast
+ unfolding factor_def cgenideal_def using m_comm assms(1) by blast
qed
show "a divides b \<Longrightarrow> PIdl b \<subseteq> PIdl a"
proof -
@@ -146,23 +164,15 @@
lemma (in domain) divides_imp_divides_mult [simp]:
"\<lbrakk> a \<in> carrier R; b \<in> carrier R - { \<zero> } \<rbrakk> \<Longrightarrow>
a divides\<^bsub>R\<^esub> b \<Longrightarrow> a divides\<^bsub>(mult_of R)\<^esub> b"
- unfolding factor_def using integral_iff by auto
+ unfolding factor_def using integral_iff by auto
lemma assoc_mult_imp_assoc [simp]: "a \<sim>\<^bsub>(mult_of R)\<^esub> b \<Longrightarrow> a \<sim>\<^bsub>R\<^esub> b"
unfolding associated_def by simp
lemma (in domain) assoc_imp_assoc_mult [simp]:
- assumes "a \<in> carrier R - { \<zero> }" and "b \<in> carrier R"
- shows "a \<sim>\<^bsub>R\<^esub> b \<Longrightarrow> a \<sim>\<^bsub>(mult_of R)\<^esub> b"
-proof -
- assume A: "a \<sim>\<^bsub>R\<^esub> b"
- then obtain c where "c \<in> carrier R" "a = b \<otimes> c"
- unfolding associated_def factor_def by auto
- hence "b \<in> carrier R - { \<zero> }"
- using assms integral by auto
- thus "a \<sim>\<^bsub>(mult_of R)\<^esub> b"
- using A assms(1) unfolding associated_def by simp
-qed
+ "\<lbrakk> a \<in> carrier R - { \<zero> } ; b \<in> carrier R - { \<zero> } \<rbrakk> \<Longrightarrow>
+ a \<sim>\<^bsub>R\<^esub> b \<Longrightarrow> a \<sim>\<^bsub>(mult_of R)\<^esub> b"
+ unfolding associated_def by simp
lemma (in domain) Units_mult_eq_Units [simp]: "Units (mult_of R) = Units R"
unfolding Units_def using insert_Diff integral_iff by auto
@@ -186,7 +196,7 @@
using c A integral_iff by auto
thus "properfactor R b a"
using A divides_imp_divides_mult[of a b] unfolding properfactor_def
- by (meson DiffI divides_mult_imp_divides empty_iff insert_iff)
+ by (meson DiffI divides_mult_imp_divides empty_iff insert_iff)
qed
lemma (in domain) properfactor_imp_properfactor_mult:
@@ -257,7 +267,7 @@
qed
qed
moreover have "PIdl p \<noteq> carrier R" using A primeideal.I_notcarr by auto
- ultimately show False by simp
+ ultimately show False by simp
qed
next
{ fix a assume "a \<in> PIdl p" and a: "a \<noteq> \<zero>"
@@ -321,12 +331,12 @@
from \<open>finite S\<close> and \<open>S \<subseteq> (\<Union>i. I i)\<close> have "\<exists>n. S \<subseteq> I n"
proof (induct S set: "finite")
- case empty thus ?case by simp
+ case empty thus ?case by simp
next
case (insert x S')
then obtain n m where m: "S' \<subseteq> I m" and n: "x \<in> I n" by blast
hence "insert x S' \<subseteq> I (max m n)"
- by (meson assms(2) insert_subsetI max.cobounded1 max.cobounded2 rev_subsetD subset_trans)
+ by (meson assms(2) insert_subsetI max.cobounded1 max.cobounded2 rev_subsetD subset_trans)
thus ?case by blast
qed
then obtain n where "S \<subseteq> I n" by blast
@@ -415,7 +425,7 @@
using S_builder_incl[of R J] J S_def I_def
by (meson additive_subgroup.a_subset dual_order.trans ideal.axioms(1) subset_Idl_subset)
ultimately obtain n where "\<And>k. k \<ge> n \<Longrightarrow> I k = I n"
- using assms increasing_set_seq_iff[of I] by (metis lift_Suc_mono_le)
+ using assms increasing_set_seq_iff[of I] by (metis lift_Suc_mono_le)
hence "J = Idl (S_builder R J n)"
using S_builder_const1[OF J, of n] S_builder_const2[OF J, of n] I_def S_def
by (meson Suc_n_not_le_n le_cases)
@@ -424,7 +434,7 @@
by (meson J S_builder_incl ideal.Icarr set_rev_mp subsetI)
qed
thus ?thesis
- by (simp add: local.ring_axioms noetherian_ring_axioms_def noetherian_ring_def)
+ by (simp add: local.ring_axioms noetherian_ring_axioms_def noetherian_ring_def)
qed
lemma (in noetherian_domain) wfactors_exists:
@@ -438,7 +448,7 @@
have "\<not> irreducible (mult_of R) x"
proof (rule ccontr)
assume "\<not> (\<not> irreducible (mult_of R) x)" hence "irreducible (mult_of R) x" by simp
- hence "wfactors (mult_of R) [ x ] x" unfolding wfactors_def using A by auto
+ hence "wfactors (mult_of R) [ x ] x" unfolding wfactors_def using A by auto
thus False using A by auto
qed
moreover have "\<not> x \<in> Units (mult_of R)"
@@ -460,11 +470,11 @@
using fs_a fs_b a b mult_of.wfactors_mult by simp
moreover have "set (fs_a @ fs_b) \<subseteq> carrier (mult_of R)"
using fs_a fs_b by auto
- ultimately show False using A by blast
+ ultimately show False using A by blast
qed
thus ?thesis using a b b_properfactor mult_of.m_comm by blast
qed } note aux_lemma = this
-
+
assume A: "\<not> ?P x"
define f :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
@@ -473,7 +483,7 @@
where "factor_seq = rec_nat x (\<lambda>n y. (SOME a. f a y))"
define I where "I = (\<lambda>i. PIdl (factor_seq i))"
have factor_seq_props:
- "\<And>n. properfactor (mult_of R) (factor_seq (Suc n)) (factor_seq n) \<and>
+ "\<And>n. properfactor (mult_of R) (factor_seq (Suc n)) (factor_seq n) \<and>
(factor_seq n) \<in> carrier (mult_of R) \<and> \<not> ?P (factor_seq n)" (is "\<And>n. ?Q n")
proof -
fix n show "?Q n"
@@ -507,7 +517,7 @@
qed
have in_carrier: "\<And>i. factor_seq i \<in> carrier R"
- using factor_seq_props by simp
+ using factor_seq_props by simp
hence "\<And>i. ideal (I i) R"
using I_def by (simp add: cgenideal_ideal)
@@ -570,12 +580,11 @@
hence "q divides p"
using to_contain_is_to_divide[of q p] using assms(1) J(1-2) by simp
hence q_div_p: "q divides\<^bsub>(mult_of R)\<^esub> p"
- using assms(1) divides_imp_divides_mult[OF q(1), of p] by (simp add: \<open>q divides p\<close>)
+ using assms(1) divides_imp_divides_mult[OF q(1), of p] by (simp add: \<open>q divides p\<close>)
show "J = PIdl p \<or> J = carrier R"
proof (cases "q \<in> Units R")
case True thus ?thesis
- by (metis J(3) Unit_eq_dividesone cgenideal_eq_genideal genideal_one one_closed q
- subset_antisym to_contain_is_to_divide)
+ by (metis J(1) Units_r_inv_ex cgenideal_self ideal.I_r_closed ideal.one_imp_carrier q(1) q(2))
next
case False
have q_in_carr: "q \<in> carrier (mult_of R)"
@@ -738,12 +747,12 @@
next
fix I assume I: "ideal I R" show "principalideal I R"
proof (cases "I = { \<zero> }")
- case True thus ?thesis by (simp add: zeropideal)
+ case True thus ?thesis by (simp add: zeropideal)
next
case False hence A: "I - { \<zero> } \<noteq> {}"
- using I additive_subgroup.zero_closed ideal.axioms(1) by auto
+ using I additive_subgroup.zero_closed ideal.axioms(1) by auto
define phi_img :: "nat set" where "phi_img = (\<phi> ` (I - { \<zero> }))"
- hence "phi_img \<noteq> {}" using A by simp
+ hence "phi_img \<noteq> {}" using A by simp
then obtain m where "m \<in> phi_img" "\<And>k. k \<in> phi_img \<Longrightarrow> m \<le> k"
using exists_least_iff[of "\<lambda>n. n \<in> phi_img"] not_less by force
then obtain a where a: "a \<in> I - { \<zero> }" "\<And>b. b \<in> I - { \<zero> } \<Longrightarrow> \<phi> a \<le> \<phi> b"
@@ -762,7 +771,7 @@
unfolding cgenideal_def using m_comm[of a] ideal.Icarr[OF I] a(1) by auto
hence 1: "\<phi> r < \<phi> a \<and> r \<noteq> \<zero>"
using eucl_div(4) b(2) by auto
-
+
have "r = (\<ominus> (a \<otimes> q)) \<oplus> b"
using eucl_div(1-3) a(1) b(1) ideal.Icarr[OF I] r_neg1 by auto
moreover have "\<ominus> (a \<otimes> q) \<in> I"
--- a/src/HOL/Algebra/Solvable_Groups.thy Tue Jul 03 10:07:24 2018 +0100
+++ b/src/HOL/Algebra/Solvable_Groups.thy Tue Jul 03 10:07:35 2018 +0100
@@ -1,11 +1,9 @@
-(* ************************************************************************** *)
-(* Title: Solvable_Groups.thy *)
-(* Author: Paulo Emílio de Vilhena *)
-(* ************************************************************************** *)
+(* Title: HOL/Algebra/Solvable_Groups.thy
+ Author: Paulo Emílio de Vilhena
+*)
theory Solvable_Groups
imports Group Coset Generated_Groups
-
begin
inductive solvable_seq :: "('a, 'b) monoid_scheme \<Rightarrow> 'a set \<Rightarrow> bool" for G where
@@ -428,4 +426,4 @@
unfolding solvable_def group_hom_def by (simp add: group.subgroup_self)
qed
-end
\ No newline at end of file
+end
--- a/src/HOL/Algebra/Subrings.thy Tue Jul 03 10:07:24 2018 +0100
+++ b/src/HOL/Algebra/Subrings.thy Tue Jul 03 10:07:35 2018 +0100
@@ -1,11 +1,9 @@
-(* ************************************************************************** *)
-(* Title: Subrings.thy *)
-(* Authors: Martin Baillon and Paulo Emílio de Vilhena *)
-(* ************************************************************************** *)
+(* Title: HOL/Algebra/Subrings.thy
+ Authors: Martin Baillon and Paulo Emílio de Vilhena
+*)
theory Subrings
imports Ring RingHom QuotRing Multiplicative_Group
-
begin
section \<open>Subrings\<close>
@@ -425,4 +423,4 @@
using S.subfield_iff[of "h ` K"] K(1) ring_hom_memE(1)[OF homh] by blast
qed
-end
\ No newline at end of file
+end
--- a/src/HOL/Algebra/Sym_Groups.thy Tue Jul 03 10:07:24 2018 +0100
+++ b/src/HOL/Algebra/Sym_Groups.thy Tue Jul 03 10:07:35 2018 +0100
@@ -1,11 +1,9 @@
-(* ************************************************************************** *)
-(* Title: Sym_Groups.th *)
-(* Author: Paulo Emílio de Vilhena *)
-(* ************************************************************************** *)
+(* Title: HOL/Algebra/Sym_Groups.thy
+ Author: Paulo Emílio de Vilhena
+*)
theory Sym_Groups
imports Cycles Group Coset Generated_Groups Solvable_Groups
-
begin
abbreviation inv' :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
@@ -661,4 +659,4 @@
alt_group_not_solvable[OF assms] inj_on_id by blast
qed
-end
\ No newline at end of file
+end