--- a/src/HOL/Algebra/Chinese_Remainder.thy Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Chinese_Remainder.thy Wed Nov 13 20:10:34 2024 +0100
@@ -231,11 +231,13 @@
shows "(canonical_proj I J) ` carrier R = carrier (RDirProd (R Quot I) (R Quot J))"
unfolding RDirProd_def DirProd_def FactRing_def A_RCOSETS_def'
proof (auto simp add: monoid.defs)
- { fix I i assume "ideal I R" "i \<in> I" hence "I +> i = \<zero>\<^bsub>R Quot I\<^esub>"
- using a_rcos_zero by (simp add: FactRing_def)
- } note aux_lemma1 = this
+ have aux_lemma1: "I +> i = \<zero>\<^bsub>R Quot I\<^esub>" if "ideal I R" "i \<in> I" for I i
+ using that a_rcos_zero by (simp add: FactRing_def)
- { fix I i j assume A: "ideal I R" "i \<in> I" "j \<in> carrier R" "i \<oplus> j = \<one>"
+ have aux_lemma2: "I +> j = \<one>\<^bsub>R Quot I\<^esub>"
+ if A: "ideal I R" "i \<in> I" "j \<in> carrier R" "i \<oplus> j = \<one>"
+ for I i j
+ proof -
have "(I +> i) \<oplus>\<^bsub>R Quot I\<^esub> (I +> j) = I +> \<one>"
using ring_hom_memE(3)[OF ideal.rcos_ring_hom ideal.Icarr[OF _ A(2)] A(3)] A(1,4) by simp
moreover have "I +> i = I"
@@ -243,9 +245,9 @@
by (simp add: A(1-2) abelian_subgroup.a_rcos_const)
moreover have "I +> j \<in> carrier (R Quot I)" and "I = \<zero>\<^bsub>R Quot I\<^esub>" and "I +> \<one> = \<one>\<^bsub>R Quot I\<^esub>"
by (auto simp add: FactRing_def A_RCOSETS_def' A(3))
- ultimately have "I +> j = \<one>\<^bsub>R Quot I\<^esub>"
+ ultimately show ?thesis
using ring.ring_simprules(8)[OF ideal.quotient_is_ring[OF A(1)]] by simp
- } note aux_lemma2 = this
+ qed
interpret I: ring "R Quot I" + J: ring "R Quot J"
using assms(1-2)[THEN ideal.quotient_is_ring] by auto
@@ -418,33 +420,33 @@
case 0 show ?case
by (auto simp add: RDirProd_list_carrier FactRing_def A_RCOSETS_def')
next
- { fix S :: "'c ring" and T :: "'d ring" and f g
- assume A: "ring T" "f \<in> ring_hom R S" "g \<in> ring_hom R T" "f ` carrier R \<subseteq> f ` (a_kernel R T g)"
- have "(\<lambda>a. (f a, g a)) ` carrier R = (f ` carrier R) \<times> (g ` carrier R)"
+ have aux_lemma: "(\<lambda>a. (f a, g a)) ` carrier R = (f ` carrier R) \<times> (g ` carrier R)"
+ if A: "ring T" "f \<in> ring_hom R S" "g \<in> ring_hom R T" "f ` carrier R \<subseteq> f ` (a_kernel R T g)"
+ for S :: "'c ring" and T :: "'d ring" and f g
+ proof
+ show "(\<lambda>a. (f a, g a)) ` carrier R \<subseteq> (f ` carrier R) \<times> (g ` carrier R)"
+ by blast
+ next
+ show "(f ` carrier R) \<times> (g ` carrier R) \<subseteq> (\<lambda>a. (f a, g a)) ` carrier R"
proof
- show "(\<lambda>a. (f a, g a)) ` carrier R \<subseteq> (f ` carrier R) \<times> (g ` carrier R)"
+ fix t assume "t \<in> (f ` carrier R) \<times> (g ` carrier R)"
+ then obtain a b where a: "a \<in> carrier R" "f a = fst t" and b: "b \<in> carrier R" "g b = snd t"
+ by auto
+ obtain c where c: "c \<in> a_kernel R T g" "f c = f (a \<ominus> b)"
+ using A(4) minus_closed[OF a(1) b (1)] by auto
+ have "f (c \<oplus> b) = f (a \<ominus> b) \<oplus>\<^bsub>S\<^esub> f b"
+ using ring_hom_memE(3)[OF A(2)] b c unfolding a_kernel_def' by auto
+ hence "f (c \<oplus> b) = f a"
+ using ring_hom_memE(3)[OF A(2) minus_closed[of a b], of b] a b by algebra
+ moreover have "g (c \<oplus> b) = g b"
+ using ring_hom_memE(1,3)[OF A(3)] b(1) c ring.ring_simprules(8)[OF A(1)]
+ unfolding a_kernel_def' by auto
+ ultimately have "(\<lambda>a. (f a, g a)) (c \<oplus> b) = t" and "c \<oplus> b \<in> carrier R"
+ using a b c unfolding a_kernel_def' by auto
+ thus "t \<in> (\<lambda>a. (f a, g a)) ` carrier R"
by blast
- next
- show "(f ` carrier R) \<times> (g ` carrier R) \<subseteq> (\<lambda>a. (f a, g a)) ` carrier R"
- proof
- fix t assume "t \<in> (f ` carrier R) \<times> (g ` carrier R)"
- then obtain a b where a: "a \<in> carrier R" "f a = fst t" and b: "b \<in> carrier R" "g b = snd t"
- by auto
- obtain c where c: "c \<in> a_kernel R T g" "f c = f (a \<ominus> b)"
- using A(4) minus_closed[OF a(1) b (1)] by auto
- have "f (c \<oplus> b) = f (a \<ominus> b) \<oplus>\<^bsub>S\<^esub> f b"
- using ring_hom_memE(3)[OF A(2)] b c unfolding a_kernel_def' by auto
- hence "f (c \<oplus> b) = f a"
- using ring_hom_memE(3)[OF A(2) minus_closed[of a b], of b] a b by algebra
- moreover have "g (c \<oplus> b) = g b"
- using ring_hom_memE(1,3)[OF A(3)] b(1) c ring.ring_simprules(8)[OF A(1)]
- unfolding a_kernel_def' by auto
- ultimately have "(\<lambda>a. (f a, g a)) (c \<oplus> b) = t" and "c \<oplus> b \<in> carrier R"
- using a b c unfolding a_kernel_def' by auto
- thus "t \<in> (\<lambda>a. (f a, g a)) ` carrier R"
- by blast
- qed
- qed } note aux_lemma = this
+ qed
+ qed
let ?map_Quot = "\<lambda>I n. map (\<lambda>i. R Quot (I i)) [0..< Suc n]"
let ?DirProd = "\<lambda>I n. RDirProd_list (?map_Quot I n)"
--- a/src/HOL/Algebra/Coset.thy Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Coset.thy Wed Nov 13 20:10:34 2024 +0100
@@ -1914,9 +1914,10 @@
interpret Anormal: normal A "(G Mod H)" using assms by simp
show "{x \<in> carrier G. H #> x \<in> A} #> x = x <# {x \<in> carrier G. H #> x \<in> A}" if x: "x \<in> carrier G" for x
proof -
- { fix y
- assume y: "y \<in> {x \<in> carrier G. H #> x \<in> A} #> x"
- then obtain x' where x': "x' \<in> carrier G" "H #> x' \<in> A" "y = x' \<otimes> x"
+ have "y \<in> x <# {x \<in> carrier G. H #> x \<in> A}"
+ if y: "y \<in> {x \<in> carrier G. H #> x \<in> A} #> x" for y
+ proof -
+ from that obtain x' where x': "x' \<in> carrier G" "H #> x' \<in> A" "y = x' \<otimes> x"
unfolding r_coset_def by auto
from x(1) have Hx: "H #> x \<in> carrier (G Mod H)"
unfolding FactGroup_def RCOSETS_def by force
@@ -1937,11 +1938,12 @@
also have "\<dots> = y"
by (simp add: x x')
finally have "x \<otimes> (inv x \<otimes> x' \<otimes> x) = y" .
- with xcoset have "y \<in> x <# {x \<in> carrier G. H #> x \<in> A}" by auto}
- moreover
- { fix y
- assume y: "y \<in> x <# {x \<in> carrier G. H #> x \<in> A}"
- then obtain x' where x': "x' \<in> carrier G" "H #> x' \<in> A" "y = x \<otimes> x'" unfolding l_coset_def by auto
+ with xcoset show ?thesis by auto
+ qed
+ moreover have "y \<in> {x \<in> carrier G. H #> x \<in> A} #> x"
+ if y: "y \<in> x <# {x \<in> carrier G. H #> x \<in> A}" for y
+ proof -
+ from that obtain x' where x': "x' \<in> carrier G" "H #> x' \<in> A" "y = x \<otimes> x'" unfolding l_coset_def by auto
from x(1) have invx: "inv x \<in> carrier G"
by (rule inv_closed)
hence Hinvx: "H #> (inv x) \<in> carrier (G Mod H)"
@@ -1960,7 +1962,8 @@
also have "\<dots> = y"
by (simp add: x x')
finally have "x \<otimes> x' \<otimes> inv x \<otimes> x = y".
- with xcoset have "y \<in> {x \<in> carrier G. H #> x \<in> A} #> x" by auto }
+ with xcoset show ?thesis by auto
+ qed
ultimately show ?thesis
by auto
qed
--- a/src/HOL/Algebra/Embedded_Algebras.thy Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Embedded_Algebras.thy Wed Nov 13 20:10:34 2024 +0100
@@ -1123,14 +1123,14 @@
assumes "dimension n K E" and "dimension m K E"
shows "n = m"
proof -
- { fix n m assume n: "dimension n K E" and m: "dimension m K E"
- then obtain Vs
+ have aux_lemma: "n \<le> m" if n: "dimension n K E" and m: "dimension m K E" for n m
+ proof -
+ from that obtain Vs
where Vs: "set Vs \<subseteq> carrier R" "independent K Vs" "length Vs = n" "Span K Vs = E"
using exists_base by meson
- hence "n \<le> m"
+ then show ?thesis
using independent_length_le_dimension[OF m Vs(2)] Span_base_incl[OF Vs(1)] by auto
- } note aux_lemma = this
-
+ qed
show ?thesis
using aux_lemma[OF assms] aux_lemma[OF assms(2,1)] by simp
qed
@@ -1166,28 +1166,28 @@
assumes "dimension n K E" and "independent K Us" "set Us \<subseteq> E"
shows "\<exists>Vs. length (Vs @ Us) = n \<and> independent K (Vs @ Us) \<and> Span K (Vs @ Us) = E"
proof -
- { fix Us k assume "k \<le> n" "independent K Us" "set Us \<subseteq> E" "length Us = k"
- hence "\<exists>Vs. length (Vs @ Us) = n \<and> independent K (Vs @ Us) \<and> Span K (Vs @ Us) = E"
- proof (induct arbitrary: Us rule: inc_induct)
- case base thus ?case
- using independent_length_eq_dimension[OF assms(1) base(1-2)] by auto
- next
- case (step m)
- have "Span K Us \<subseteq> E"
- using mono_Span_subset step(4-6) exists_base[OF assms(1)] by blast
- hence "Span K Us \<subset> E"
- using independent_length_eq_dimension[OF assms(1) step(4-5)] step(2,6) assms(1) by blast
- then obtain v where v: "v \<in> E" "v \<notin> Span K Us"
- using Span_strict_incl exists_base[OF assms(1)] by blast
- hence "independent K (v # Us)"
- using space_subgroup_props(1)[OF assms(1)] li_Cons[OF _ v(2) step(4)] by auto
- then obtain Vs
- where "length (Vs @ (v # Us)) = n" "independent K (Vs @ (v # Us))" "Span K (Vs @ (v # Us)) = E"
- using step(3)[of "v # Us"] step(1-2,4-6) v by auto
- thus ?case
- by (metis append.assoc append_Cons append_Nil)
- qed } note aux_lemma = this
-
+ have aux_lemma: "\<exists>Vs. length (Vs @ Us) = n \<and> independent K (Vs @ Us) \<and> Span K (Vs @ Us) = E"
+ if "k \<le> n" "independent K Us" "set Us \<subseteq> E" "length Us = k" for Us k
+ using that
+ proof (induct arbitrary: Us rule: inc_induct)
+ case base
+ thus ?case using independent_length_eq_dimension[OF assms(1) base(1-2)] by auto
+ next
+ case (step m)
+ have "Span K Us \<subseteq> E"
+ using mono_Span_subset step(4-6) exists_base[OF assms(1)] by blast
+ hence "Span K Us \<subset> E"
+ using independent_length_eq_dimension[OF assms(1) step(4-5)] step(2,6) assms(1) by blast
+ then obtain v where v: "v \<in> E" "v \<notin> Span K Us"
+ using Span_strict_incl exists_base[OF assms(1)] by blast
+ hence "independent K (v # Us)"
+ using space_subgroup_props(1)[OF assms(1)] li_Cons[OF _ v(2) step(4)] by auto
+ then obtain Vs
+ where "length (Vs @ (v # Us)) = n" "independent K (Vs @ (v # Us))" "Span K (Vs @ (v # Us)) = E"
+ using step(3)[of "v # Us"] step(1-2,4-6) v by auto
+ thus ?case
+ by (metis append.assoc append_Cons append_Nil)
+ qed
have "length Us \<le> n"
using independent_length_le_dimension[OF assms] .
thus ?thesis
--- a/src/HOL/Algebra/Exact_Sequence.thy Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Exact_Sequence.thy Wed Nov 13 20:10:34 2024 +0100
@@ -38,24 +38,23 @@
assumes "exact_seq (G, F)" and "(i :: nat) < length F"
shows "exact_seq (drop i G, drop i F)"
proof-
- { fix t i assume "exact_seq t" "i < length (snd t)"
- hence "exact_seq (drop i (fst t), drop i (snd t))"
- proof (induction arbitrary: i)
- case (unity G1 G2 f) thus ?case
- by (simp add: exact_seq.unity)
+ have "exact_seq (drop i (fst t), drop i (snd t))" if "exact_seq t" "i < length (snd t)" for t i
+ using that
+ proof (induction arbitrary: i)
+ case (unity G1 G2 f) thus ?case
+ by (simp add: exact_seq.unity)
+ next
+ case (extension G K l g q H h) show ?case
+ proof (cases)
+ assume "i = 0" thus ?case
+ using exact_seq.extension[OF extension.hyps] by simp
next
- case (extension G K l g q H h) show ?case
- proof (cases)
- assume "i = 0" thus ?case
- using exact_seq.extension[OF extension.hyps] by simp
- next
- assume "i \<noteq> 0" hence "i \<ge> Suc 0" by simp
- then obtain k where "k < length (snd (G # K # l, g # q))" "i = Suc k"
- using Suc_le_D extension.prems by auto
- thus ?thesis using extension.IH by simp
- qed
- qed }
-
+ assume "i \<noteq> 0" hence "i \<ge> Suc 0" by simp
+ then obtain k where "k < length (snd (G # K # l, g # q))" "i = Suc k"
+ using Suc_le_D extension.prems by auto
+ thus ?thesis using extension.IH by simp
+ qed
+ qed
thus ?thesis using assms by auto
qed
@@ -68,18 +67,19 @@
lemma exact_seq_imp_exact_hom:
assumes "exact_seq (G1 # l,q) \<longlongrightarrow>\<^bsub>g1\<^esub> G2 \<longlongrightarrow>\<^bsub>g2\<^esub> G3"
shows "g1 ` (carrier G1) = kernel G2 G3 g2"
-proof-
- { fix t assume "exact_seq t" and "length (fst t) \<ge> 3 \<and> length (snd t) \<ge> 2"
- hence "(hd (tl (snd t))) ` (carrier (hd (tl (tl (fst t))))) =
+proof -
+ have "(hd (tl (snd t))) ` (carrier (hd (tl (tl (fst t))))) =
kernel (hd (tl (fst t))) (hd (fst t)) (hd (snd t))"
- proof (induction)
- case (unity G1 G2 f)
- then show ?case by auto
- next
- case (extension G l g q H h)
- then show ?case by auto
- qed }
- thus ?thesis using assms by fastforce
+ if "exact_seq t" and "length (fst t) \<ge> 3 \<and> length (snd t) \<ge> 2" for t
+ using that
+ proof (induction)
+ case (unity G1 G2 f)
+ then show ?case by auto
+ next
+ case (extension G l g q H h)
+ then show ?case by auto
+ qed
+ with assms show ?thesis by fastforce
qed
lemma exact_seq_imp_exact_hom_arbitrary:
@@ -103,16 +103,15 @@
assumes "exact_seq ((G # l, q)) \<longlongrightarrow>\<^bsub>g\<^esub> H"
shows "group_hom G H g"
proof-
- { fix t assume "exact_seq t"
- hence "group_hom (hd (tl (fst t))) (hd (fst t)) (hd(snd t))"
- proof (induction)
- case (unity G1 G2 f)
- then show ?case by auto
- next
- case (extension G l g q H h)
- then show ?case unfolding group_hom_def group_hom_axioms_def by auto
- qed }
- note aux_lemma = this
+ have aux_lemma: "group_hom (hd (tl (fst t))) (hd (fst t)) (hd(snd t))" if "exact_seq t" for t
+ using that
+ proof (induction)
+ case (unity G1 G2 f)
+ then show ?case by auto
+ next
+ case (extension G l g q H h)
+ then show ?case unfolding group_hom_def group_hom_axioms_def by auto
+ qed
show ?thesis using aux_lemma[OF assms]
by simp
qed
--- a/src/HOL/Algebra/FiniteProduct.thy Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy Wed Nov 13 20:10:34 2024 +0100
@@ -115,8 +115,7 @@
then show ?thesis
using \<open>(A,y) \<in> foldSetD D (\<cdot>) e\<close> by auto
next
- case (2 x' A' y')
- note A' = this
+ case A': (2 x' A' y')
show ?thesis
using foldSetD.cases [OF \<open>(A,y) \<in> foldSetD D (\<cdot>) e\<close>]
proof cases
@@ -124,8 +123,7 @@
then show ?thesis
using \<open>(A,x) \<in> foldSetD D (\<cdot>) e\<close> by auto
next
- case (2 x'' A'' y'')
- note A'' = this
+ case A'': (2 x'' A'' y'')
show ?thesis
proof (cases "x' = x''")
case True
--- a/src/HOL/Algebra/Generated_Fields.thy Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Generated_Fields.thy Wed Nov 13 20:10:34 2024 +0100
@@ -121,56 +121,56 @@
and "I \<subseteq> K"
shows "generate_field (R\<lparr>carrier := K\<rparr>) I \<subseteq> generate_field (R\<lparr>carrier := H\<rparr>) I"
proof
- {fix J assume J_def : "subfield J R" "I \<subseteq> J"
- have "generate_field (R \<lparr> carrier := J \<rparr>) I \<subseteq> J"
- using field.mono_generate_field[of "(R\<lparr>carrier := J\<rparr>)" I J] subfield_iff(2)[OF J_def(1)]
- field.generate_field_in_carrier[of "R\<lparr>carrier := J\<rparr>"] field_axioms J_def
- by auto}
- note incl_HK = this
- {fix x have "x \<in> generate_field (R\<lparr>carrier := K\<rparr>) I \<Longrightarrow> x \<in> generate_field (R\<lparr>carrier := H\<rparr>) I"
- proof (induction rule : generate_field.induct)
- case one
- have "\<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub> \<otimes> \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub> = \<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub>" by simp
- moreover have "\<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub> \<otimes> \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub> = \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub>" by simp
- ultimately show ?case using assms generate_field.one by metis
- next
- case (incl h) thus ?case using generate_field.incl by force
- next
- case (a_inv h)
- note hyp = this
- have "a_inv (R\<lparr>carrier := K\<rparr>) h = a_inv R h"
- using assms group.m_inv_consistent[of "add_monoid R" K] a_comm_group incl_HK[of K] hyp
- subring.axioms(1)[OF subfieldE(1)[OF assms(2)]]
- unfolding comm_group_def a_inv_def by auto
- moreover have "a_inv (R\<lparr>carrier := H\<rparr>) h = a_inv R h"
- using assms group.m_inv_consistent[of "add_monoid R" H] a_comm_group incl_HK[of H] hyp
- subring.axioms(1)[OF subfieldE(1)[OF assms(1)]]
- unfolding comm_group_def a_inv_def by auto
- ultimately show ?case using generate_field.a_inv a_inv.IH by fastforce
- next
- case (m_inv h)
- note hyp = this
- have h_K : "h \<in> (K - {\<zero>})" using incl_HK[OF assms(2) assms(4)] hyp by auto
- hence "m_inv (R\<lparr>carrier := K\<rparr>) h = m_inv R h"
- using field.m_inv_mult_of[OF subfield_iff(2)[OF assms(2)]]
- group.m_inv_consistent[of "mult_of R" "K - {\<zero>}"] field_mult_group units_of_inv
- subgroup_mult_of subfieldE[OF assms(2)] unfolding mult_of_def apply simp
- by (metis h_K mult_of_def mult_of_is_Units subgroup.mem_carrier units_of_carrier assms(2))
- moreover have h_H : "h \<in> (H - {\<zero>})" using incl_HK[OF assms(1) assms(3)] hyp by auto
- hence "m_inv (R\<lparr>carrier := H\<rparr>) h = m_inv R h"
- using field.m_inv_mult_of[OF subfield_iff(2)[OF assms(1)]]
- group.m_inv_consistent[of "mult_of R" "H - {\<zero>}"] field_mult_group
- subgroup_mult_of[OF assms(1)] unfolding mult_of_def apply simp
- by (metis h_H field_Units m_inv_mult_of mult_of_is_Units subgroup.mem_carrier units_of_def)
- ultimately show ?case using generate_field.m_inv m_inv.IH h_H by fastforce
- next
- case (eng_add h1 h2)
- thus ?case using incl_HK assms generate_field.eng_add by force
- next
- case (eng_mult h1 h2)
- thus ?case using generate_field.eng_mult by force
- qed}
- thus "\<And>x. x \<in> generate_field (R\<lparr>carrier := K\<rparr>) I \<Longrightarrow> x \<in> generate_field (R\<lparr>carrier := H\<rparr>) I"
+ have incl_HK: "generate_field (R \<lparr> carrier := J \<rparr>) I \<subseteq> J"
+ if J_def : "subfield J R" "I \<subseteq> J" for J
+ using field.mono_generate_field[of "(R\<lparr>carrier := J\<rparr>)" I J] subfield_iff(2)[OF J_def(1)]
+ field.generate_field_in_carrier[of "R\<lparr>carrier := J\<rparr>"] field_axioms J_def
+ by auto
+
+ fix x
+ have "x \<in> generate_field (R\<lparr>carrier := K\<rparr>) I \<Longrightarrow> x \<in> generate_field (R\<lparr>carrier := H\<rparr>) I"
+ proof (induction rule : generate_field.induct)
+ case one
+ have "\<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub> \<otimes> \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub> = \<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub>" by simp
+ moreover have "\<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub> \<otimes> \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub> = \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub>" by simp
+ ultimately show ?case using assms generate_field.one by metis
+ next
+ case (incl h)
+ thus ?case using generate_field.incl by force
+ next
+ case (a_inv h)
+ have "a_inv (R\<lparr>carrier := K\<rparr>) h = a_inv R h"
+ using assms group.m_inv_consistent[of "add_monoid R" K] a_comm_group incl_HK[of K] a_inv
+ subring.axioms(1)[OF subfieldE(1)[OF assms(2)]]
+ unfolding comm_group_def a_inv_def by auto
+ moreover have "a_inv (R\<lparr>carrier := H\<rparr>) h = a_inv R h"
+ using assms group.m_inv_consistent[of "add_monoid R" H] a_comm_group incl_HK[of H] a_inv
+ subring.axioms(1)[OF subfieldE(1)[OF assms(1)]]
+ unfolding comm_group_def a_inv_def by auto
+ ultimately show ?case using generate_field.a_inv a_inv.IH by fastforce
+ next
+ case (m_inv h)
+ have h_K : "h \<in> (K - {\<zero>})" using incl_HK[OF assms(2) assms(4)] m_inv by auto
+ hence "m_inv (R\<lparr>carrier := K\<rparr>) h = m_inv R h"
+ using field.m_inv_mult_of[OF subfield_iff(2)[OF assms(2)]]
+ group.m_inv_consistent[of "mult_of R" "K - {\<zero>}"] field_mult_group units_of_inv
+ subgroup_mult_of subfieldE[OF assms(2)] unfolding mult_of_def apply simp
+ by (metis h_K mult_of_def mult_of_is_Units subgroup.mem_carrier units_of_carrier assms(2))
+ moreover have h_H : "h \<in> (H - {\<zero>})" using incl_HK[OF assms(1) assms(3)] m_inv by auto
+ hence "m_inv (R\<lparr>carrier := H\<rparr>) h = m_inv R h"
+ using field.m_inv_mult_of[OF subfield_iff(2)[OF assms(1)]]
+ group.m_inv_consistent[of "mult_of R" "H - {\<zero>}"] field_mult_group
+ subgroup_mult_of[OF assms(1)] unfolding mult_of_def apply simp
+ by (metis h_H field_Units m_inv_mult_of mult_of_is_Units subgroup.mem_carrier units_of_def)
+ ultimately show ?case using generate_field.m_inv m_inv.IH h_H by fastforce
+ next
+ case (eng_add h1 h2)
+ thus ?case using incl_HK assms generate_field.eng_add by force
+ next
+ case (eng_mult h1 h2)
+ thus ?case using generate_field.eng_mult by force
+ qed
+ thus "x \<in> generate_field (R\<lparr>carrier := K\<rparr>) I \<Longrightarrow> x \<in> generate_field (R\<lparr>carrier := H\<rparr>) I"
by auto
qed
--- a/src/HOL/Algebra/Generated_Groups.thy Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Generated_Groups.thy Wed Nov 13 20:10:34 2024 +0100
@@ -344,23 +344,23 @@
by (simp add: DG.rcos_sum)
also have " ... = derived G (carrier G) #> (g2 \<otimes> g1)"
proof -
- { fix g1 g2 assume g1: "g1 \<in> carrier G" and g2: "g2 \<in> carrier G"
- have "derived G (carrier G) #> (g1 \<otimes> g2) \<subseteq> derived G (carrier G) #> (g2 \<otimes> g1)"
- proof
- fix h assume "h \<in> derived G (carrier G) #> (g1 \<otimes> g2)"
- then obtain g' where h: "g' \<in> carrier G" "g' \<in> derived G (carrier G)" "h = g' \<otimes> (g1 \<otimes> g2)"
- using DG.subset unfolding r_coset_def by auto
- hence "h = g' \<otimes> (g1 \<otimes> g2) \<otimes> (inv g1 \<otimes> inv g2 \<otimes> g2 \<otimes> g1)"
- using g1 g2 by (simp add: m_assoc)
- hence "h = (g' \<otimes> (g1 \<otimes> g2 \<otimes> inv g1 \<otimes> inv g2)) \<otimes> (g2 \<otimes> g1)"
- using h(1) g1 g2 inv_closed m_assoc m_closed by presburger
- moreover have "g1 \<otimes> g2 \<otimes> inv g1 \<otimes> inv g2 \<in> derived G (carrier G)"
- using incl[of _ "derived_set G (carrier G)"] g1 g2 unfolding derived_def by blast
- hence "g' \<otimes> (g1 \<otimes> g2 \<otimes> inv g1 \<otimes> inv g2) \<in> derived G (carrier G)"
- using DG.m_closed[OF h(2)] by simp
- ultimately show "h \<in> derived G (carrier G) #> (g2 \<otimes> g1)"
- unfolding r_coset_def by blast
- qed }
+ have "derived G (carrier G) #> (g1 \<otimes> g2) \<subseteq> derived G (carrier G) #> (g2 \<otimes> g1)"
+ if g1: "g1 \<in> carrier G" and g2: "g2 \<in> carrier G" for g1 g2
+ proof
+ fix h assume "h \<in> derived G (carrier G) #> (g1 \<otimes> g2)"
+ then obtain g' where h: "g' \<in> carrier G" "g' \<in> derived G (carrier G)" "h = g' \<otimes> (g1 \<otimes> g2)"
+ using DG.subset unfolding r_coset_def by auto
+ hence "h = g' \<otimes> (g1 \<otimes> g2) \<otimes> (inv g1 \<otimes> inv g2 \<otimes> g2 \<otimes> g1)"
+ using g1 g2 by (simp add: m_assoc)
+ hence "h = (g' \<otimes> (g1 \<otimes> g2 \<otimes> inv g1 \<otimes> inv g2)) \<otimes> (g2 \<otimes> g1)"
+ using h(1) g1 g2 inv_closed m_assoc m_closed by presburger
+ moreover have "g1 \<otimes> g2 \<otimes> inv g1 \<otimes> inv g2 \<in> derived G (carrier G)"
+ using incl[of _ "derived_set G (carrier G)"] g1 g2 unfolding derived_def by blast
+ hence "g' \<otimes> (g1 \<otimes> g2 \<otimes> inv g1 \<otimes> inv g2) \<in> derived G (carrier G)"
+ using DG.m_closed[OF h(2)] by simp
+ ultimately show "h \<in> derived G (carrier G) #> (g2 \<otimes> g1)"
+ unfolding r_coset_def by blast
+ qed
thus ?thesis
using g1(1) g2(1) by auto
qed
--- a/src/HOL/Algebra/Generated_Rings.thy Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Generated_Rings.thy Wed Nov 13 20:10:34 2024 +0100
@@ -109,38 +109,37 @@
and "I \<subseteq> K"
shows "generate_ring (R\<lparr>carrier := K\<rparr>) I \<subseteq> generate_ring (R\<lparr>carrier := H\<rparr>) I"
proof
- {fix J assume J_def : "subring J R" "I \<subseteq> J"
- have "generate_ring (R \<lparr> carrier := J \<rparr>) I \<subseteq> J"
- using ring.mono_generate_ring[of "(R\<lparr>carrier := J\<rparr>)" I J ] subring_is_ring[OF J_def(1)]
- ring.generate_ring_in_carrier[of "R\<lparr>carrier := J\<rparr>"] ring_axioms J_def(2)
- by auto}
- note incl_HK = this
- {fix x have "x \<in> generate_ring (R\<lparr>carrier := K\<rparr>) I \<Longrightarrow> x \<in> generate_ring (R\<lparr>carrier := H\<rparr>) I"
- proof (induction rule : generate_ring.induct)
- case one
- have "\<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub> \<otimes> \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub> = \<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub>" by simp
- moreover have "\<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub> \<otimes> \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub> = \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub>" by simp
- ultimately show ?case using assms generate_ring.one by metis
- next
- case (incl h) thus ?case using generate_ring.incl by force
- next
- case (a_inv h)
- note hyp = this
- have "a_inv (R\<lparr>carrier := K\<rparr>) h = a_inv R h"
- using assms group.m_inv_consistent[of "add_monoid R" K] a_comm_group incl_HK[of K] hyp
- unfolding subring_def comm_group_def a_inv_def by auto
- moreover have "a_inv (R\<lparr>carrier := H\<rparr>) h = a_inv R h"
- using assms group.m_inv_consistent[of "add_monoid R" H] a_comm_group incl_HK[of H] hyp
- unfolding subring_def comm_group_def a_inv_def by auto
- ultimately show ?case using generate_ring.a_inv a_inv.IH by fastforce
- next
- case (eng_add h1 h2)
- thus ?case using incl_HK assms generate_ring.eng_add by force
- next
- case (eng_mult h1 h2)
- thus ?case using generate_ring.eng_mult by force
- qed}
- thus "\<And>x. x \<in> generate_ring (R\<lparr>carrier := K\<rparr>) I \<Longrightarrow> x \<in> generate_ring (R\<lparr>carrier := H\<rparr>) I"
+ have incl_HK: "generate_ring (R \<lparr> carrier := J \<rparr>) I \<subseteq> J" if J_def : "subring J R" "I \<subseteq> J" for J
+ using ring.mono_generate_ring[of "(R\<lparr>carrier := J\<rparr>)" I J ] subring_is_ring[OF J_def(1)]
+ ring.generate_ring_in_carrier[of "R\<lparr>carrier := J\<rparr>"] ring_axioms J_def(2)
+ by auto
+
+ fix x
+ have "x \<in> generate_ring (R\<lparr>carrier := K\<rparr>) I \<Longrightarrow> x \<in> generate_ring (R\<lparr>carrier := H\<rparr>) I"
+ proof (induction rule : generate_ring.induct)
+ case one
+ have "\<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub> \<otimes> \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub> = \<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub>" by simp
+ moreover have "\<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub> \<otimes> \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub> = \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub>" by simp
+ ultimately show ?case using assms generate_ring.one by metis
+ next
+ case (incl h) thus ?case using generate_ring.incl by force
+ next
+ case (a_inv h)
+ have "a_inv (R\<lparr>carrier := K\<rparr>) h = a_inv R h"
+ using assms group.m_inv_consistent[of "add_monoid R" K] a_comm_group incl_HK[of K] a_inv
+ unfolding subring_def comm_group_def a_inv_def by auto
+ moreover have "a_inv (R\<lparr>carrier := H\<rparr>) h = a_inv R h"
+ using assms group.m_inv_consistent[of "add_monoid R" H] a_comm_group incl_HK[of H] a_inv
+ unfolding subring_def comm_group_def a_inv_def by auto
+ ultimately show ?case using generate_ring.a_inv a_inv.IH by fastforce
+ next
+ case (eng_add h1 h2)
+ thus ?case using incl_HK assms generate_ring.eng_add by force
+ next
+ case (eng_mult h1 h2)
+ thus ?case using generate_ring.eng_mult by force
+ qed
+ thus "x \<in> generate_ring (R\<lparr>carrier := K\<rparr>) I \<Longrightarrow> x \<in> generate_ring (R\<lparr>carrier := H\<rparr>) I"
by auto
qed
--- a/src/HOL/Algebra/Ideal.thy Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Ideal.thy Wed Nov 13 20:10:34 2024 +0100
@@ -102,8 +102,8 @@
lemma (in ring) set_add_comm:
assumes "I \<subseteq> carrier R" "J \<subseteq> carrier R" shows "I <+> J = J <+> I"
proof -
- { fix I J assume "I \<subseteq> carrier R" "J \<subseteq> carrier R" hence "I <+> J \<subseteq> J <+> I"
- using a_comm unfolding set_add_def' by (auto, blast) }
+ have "I <+> J \<subseteq> J <+> I" if "I \<subseteq> carrier R" "J \<subseteq> carrier R" for I J
+ using that a_comm unfolding set_add_def' by (auto, blast)
thus ?thesis
using assms by auto
qed
@@ -262,35 +262,33 @@
assumes Sideals: "\<And>I. I \<in> S \<Longrightarrow> ideal I R" and notempty: "S \<noteq> {}"
shows "ideal (\<Inter>S) R"
proof -
- { fix x y J
- assume "\<forall>I\<in>S. x \<in> I" "\<forall>I\<in>S. y \<in> I" and JS: "J \<in> S"
+ have "x \<oplus> y \<in> J" if "\<forall>I\<in>S. x \<in> I" "\<forall>I\<in>S. y \<in> I" and JS: "J \<in> S" for x y J
+ proof -
interpret ideal J R by (rule Sideals[OF JS])
- have "x \<oplus> y \<in> J"
- by (simp add: JS \<open>\<forall>I\<in>S. x \<in> I\<close> \<open>\<forall>I\<in>S. y \<in> I\<close>) }
- moreover
- have "\<zero> \<in> J" if "J \<in> S" for J
- by (simp add: that Sideals additive_subgroup.zero_closed ideal.axioms(1))
- moreover
- { fix x J
- assume "\<forall>I\<in>S. x \<in> I" and JS: "J \<in> S"
+ show ?thesis by (simp add: JS \<open>\<forall>I\<in>S. x \<in> I\<close> \<open>\<forall>I\<in>S. y \<in> I\<close>)
+ qed
+ moreover have "\<zero> \<in> J" if "J \<in> S" for J
+ by (simp add: that Sideals additive_subgroup.zero_closed ideal.axioms(1))
+ moreover have "\<ominus> x \<in> J" if "\<forall>I\<in>S. x \<in> I" and JS: "J \<in> S" for x J
+ proof -
interpret ideal J R by (rule Sideals[OF JS])
- have "\<ominus> x \<in> J"
- by (simp add: JS \<open>\<forall>I\<in>S. x \<in> I\<close>) }
- moreover
- { fix x y J
- assume "\<forall>I\<in>S. x \<in> I" and ycarr: "y \<in> carrier R" and JS: "J \<in> S"
+ show ?thesis by (simp add: JS \<open>\<forall>I\<in>S. x \<in> I\<close>)
+ qed
+ moreover have "y \<otimes> x \<in> J" "x \<otimes> y \<in> J"
+ if "\<forall>I\<in>S. x \<in> I" and ycarr: "y \<in> carrier R" and JS: "J \<in> S" for x y J
+ proof -
interpret ideal J R by (rule Sideals[OF JS])
- have "y \<otimes> x \<in> J" "x \<otimes> y \<in> J"
- using I_l_closed I_r_closed JS \<open>\<forall>I\<in>S. x \<in> I\<close> ycarr by blast+ }
- moreover
- { fix x
- assume "\<forall>I\<in>S. x \<in> I"
+ show "y \<otimes> x \<in> J" "x \<otimes> y \<in> J" using I_l_closed I_r_closed JS \<open>\<forall>I\<in>S. x \<in> I\<close> ycarr by blast+
+ qed
+ moreover have "x \<in> carrier R" if "\<forall>I\<in>S. x \<in> I" for x
+ proof -
obtain I0 where I0S: "I0 \<in> S"
using notempty by blast
interpret ideal I0 R by (rule Sideals[OF I0S])
have "x \<in> I0"
by (simp add: I0S \<open>\<forall>I\<in>S. x \<in> I\<close>)
- with a_subset have "x \<in> carrier R" by fast }
+ with a_subset show ?thesis by fast
+ qed
ultimately show ?thesis
by unfold_locales (auto simp: Inter_eq simp flip: a_inv_def)
qed
@@ -308,17 +306,14 @@
by (rule ring_axioms)
show "ideal_axioms (I <+> J) R"
proof -
- { fix x i j
- assume xcarr: "x \<in> carrier R" and iI: "i \<in> I" and jJ: "j \<in> J"
- from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ]
- have "\<exists>h\<in>I. \<exists>k\<in>J. (i \<oplus> j) \<otimes> x = h \<oplus> k"
- by (meson iI ideal.I_r_closed idealJ jJ l_distr local.idealI) }
- moreover
- { fix x i j
- assume xcarr: "x \<in> carrier R" and iI: "i \<in> I" and jJ: "j \<in> J"
- from xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ]
- have "\<exists>h\<in>I. \<exists>k\<in>J. x \<otimes> (i \<oplus> j) = h \<oplus> k"
- by (meson iI ideal.I_l_closed idealJ jJ local.idealI r_distr) }
+ have "\<exists>h\<in>I. \<exists>k\<in>J. (i \<oplus> j) \<otimes> x = h \<oplus> k"
+ if xcarr: "x \<in> carrier R" and iI: "i \<in> I" and jJ: "j \<in> J" for x i j
+ using xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ]
+ by (meson iI ideal.I_r_closed idealJ jJ l_distr local.idealI)
+ moreover have "\<exists>h\<in>I. \<exists>k\<in>J. x \<otimes> (i \<oplus> j) = h \<oplus> k"
+ if xcarr: "x \<in> carrier R" and iI: "i \<in> I" and jJ: "j \<in> J" for x i j
+ using xcarr ideal.Icarr[OF idealI iI] ideal.Icarr[OF idealJ jJ]
+ by (meson iI ideal.I_l_closed idealJ jJ local.idealI r_distr)
ultimately show "ideal_axioms (I <+> J) R"
by (intro ideal_axioms.intro) (auto simp: set_add_defs)
qed
--- a/src/HOL/Algebra/Ideal_Product.thy Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Ideal_Product.thy Wed Nov 13 20:10:34 2024 +0100
@@ -273,26 +273,25 @@
local.ring_axioms ring.ideal_prod_is_ideal)
qed
qed
-next
- { fix s J K assume A: "ideal J R" "ideal K R" "s \<in> I \<cdot> J"
- have "s \<in> I \<cdot> (J <+> K) \<and> s \<in> I \<cdot> (K <+> J)"
- proof -
- from \<open>s \<in> I \<cdot> J\<close> have "s \<in> I \<cdot> (J <+> K)"
- proof (induct s rule: ideal_prod.induct)
- case (prod i j)
- hence "(j \<oplus> \<zero>) \<in> J <+> K"
- using set_add_def'[of R J K]
- additive_subgroup.zero_closed[OF ideal.axioms(1), of K R] A(2) by auto
- thus ?case
- by (metis A(1) additive_subgroup.a_Hcarr ideal.axioms(1) ideal_prod.prod prod r_zero)
- next
- case (sum s1 s2) thus ?case
- by (simp add: ideal_prod.sum)
- qed
- thus ?thesis
- by (metis A(1) A(2) ideal_def ring.union_genideal sup_commute)
- qed } note aux_lemma = this
+ have aux_lemma: "s \<in> I \<cdot> (J <+> K) \<and> s \<in> I \<cdot> (K <+> J)"
+ if A: "ideal J R" "ideal K R" "s \<in> I \<cdot> J" for s J K
+ proof -
+ from \<open>s \<in> I \<cdot> J\<close> have "s \<in> I \<cdot> (J <+> K)"
+ proof (induct s rule: ideal_prod.induct)
+ case (prod i j)
+ hence "(j \<oplus> \<zero>) \<in> J <+> K"
+ using set_add_def'[of R J K]
+ additive_subgroup.zero_closed[OF ideal.axioms(1), of K R] A(2) by auto
+ thus ?case
+ by (metis A(1) additive_subgroup.a_Hcarr ideal.axioms(1) ideal_prod.prod prod r_zero)
+ next
+ case (sum s1 s2) thus ?case
+ by (simp add: ideal_prod.sum)
+ qed
+ thus ?thesis
+ by (metis A(1) A(2) ideal_def ring.union_genideal sup_commute)
+ qed
show "I \<cdot> J <+> I \<cdot> K \<subseteq> I \<cdot> (J <+> K)"
proof
fix s assume "s \<in> I \<cdot> J <+> I \<cdot> K"
@@ -308,19 +307,22 @@
assumes "ideal I R" "ideal J R"
shows "I \<cdot> J = J \<cdot> I"
proof -
- { fix I J assume A: "ideal I R" "ideal J R"
- have "I \<cdot> J \<subseteq> J \<cdot> I"
- proof
- fix s assume "s \<in> I \<cdot> J" thus "s \<in> J \<cdot> I"
- proof (induct s rule: ideal_prod.induct)
- case (prod i j) thus ?case
- using m_comm[OF ideal.Icarr[OF A(1) prod(1)] ideal.Icarr[OF A(2) prod(2)]]
- by (simp add: ideal_prod.prod)
- next
- case (sum s1 s2) thus ?case by (simp add: ideal_prod.sum)
- qed
- qed }
- thus ?thesis using assms by blast
+ have "I \<cdot> J \<subseteq> J \<cdot> I" if A: "ideal I R" "ideal J R" for I J
+ proof
+ fix s
+ assume "s \<in> I \<cdot> J"
+ thus "s \<in> J \<cdot> I"
+ proof (induct s rule: ideal_prod.induct)
+ case (prod i j)
+ thus ?case
+ using m_comm[OF ideal.Icarr[OF A(1) prod(1)] ideal.Icarr[OF A(2) prod(2)]]
+ by (simp add: ideal_prod.prod)
+ next
+ case (sum s1 s2)
+ thus ?case by (simp add: ideal_prod.sum)
+ qed
+ qed
+ with assms show ?thesis by blast
qed
text \<open>The following result would also be true for locale ring\<close>
--- a/src/HOL/Algebra/Indexed_Polynomials.thy Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Indexed_Polynomials.thy Wed Nov 13 20:10:34 2024 +0100
@@ -285,23 +285,22 @@
assumes "\<And>P. P \<in> carrier L \<Longrightarrow> carrier_coeff P" and "\<And>P. P \<in> carrier L \<Longrightarrow> index_free P i" and "\<zero>\<^bsub>L\<^esub> = indexed_const \<zero>"
shows "inj_on (\<lambda>Ps. indexed_eval Ps i) (carrier (poly_ring L))"
proof -
- { fix Ps
- assume "Ps \<in> carrier (poly_ring L)" and "indexed_eval Ps i = indexed_const \<zero>"
- have "Ps = []"
- proof (rule ccontr)
- assume "Ps \<noteq> []"
- then obtain P' Ps' where Ps: "Ps = P' # Ps'"
- using list.exhaust by blast
- with \<open>Ps \<in> carrier (poly_ring L)\<close>
- have "P' \<noteq> indexed_const \<zero>" and "list_all carrier_coeff Ps" and "list_all (\<lambda>P. index_free P i) Ps"
- using assms unfolding sym[OF univ_poly_carrier[of L "carrier L"]] polynomial_def
- by (simp add: list.pred_set subset_code(1))+
- then obtain m where "(indexed_eval Ps i) m \<noteq> \<zero>"
- using exists_indexed_eval_monomial'[of P' Ps'] unfolding Ps by auto
- hence "indexed_eval Ps i \<noteq> indexed_const \<zero>"
- unfolding indexed_const_def by auto
- with \<open>indexed_eval Ps i = indexed_const \<zero>\<close> show False by simp
- qed } note aux_lemma = this
+ have aux_lemma: "Ps = []"
+ if "Ps \<in> carrier (poly_ring L)" and "indexed_eval Ps i = indexed_const \<zero>" for Ps
+ proof (rule ccontr)
+ assume "\<not> ?thesis"
+ then obtain P' Ps' where Ps: "Ps = P' # Ps'"
+ using list.exhaust by blast
+ with \<open>Ps \<in> carrier (poly_ring L)\<close>
+ have "P' \<noteq> indexed_const \<zero>" and "list_all carrier_coeff Ps" and "list_all (\<lambda>P. index_free P i) Ps"
+ using assms unfolding sym[OF univ_poly_carrier[of L "carrier L"]] polynomial_def
+ by (simp add: list.pred_set subset_code(1))+
+ then obtain m where "(indexed_eval Ps i) m \<noteq> \<zero>"
+ using exists_indexed_eval_monomial'[of P' Ps'] unfolding Ps by auto
+ hence "indexed_eval Ps i \<noteq> indexed_const \<zero>"
+ unfolding indexed_const_def by auto
+ with \<open>indexed_eval Ps i = indexed_const \<zero>\<close> show False by simp
+ qed
show ?thesis
proof (rule inj_onI)
@@ -356,9 +355,9 @@
lemma (in ring) indexed_eval_index_free:
assumes "list_all (\<lambda>P. index_free P j) Ps" and "i \<noteq> j" shows "index_free (indexed_eval Ps i) j"
proof -
- { fix Ps assume "list_all (\<lambda>P. index_free P j) Ps" hence "index_free (indexed_eval_aux Ps i) j"
- using indexed_padd_index_free[OF indexed_pmult_index_free[OF _ assms(2)]]
- by (induct Ps) (auto simp add: indexed_zero_def index_free_def) }
+ have "index_free (indexed_eval_aux Ps i) j" if "list_all (\<lambda>P. index_free P j) Ps" for Ps
+ using that indexed_padd_index_free[OF indexed_pmult_index_free[OF _ assms(2)]]
+ by (induct Ps) (auto simp add: indexed_zero_def index_free_def)
thus ?thesis
using assms(1) by auto
qed
--- a/src/HOL/Algebra/IntRing.thy Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/IntRing.thy Wed Nov 13 20:10:34 2024 +0100
@@ -54,7 +54,7 @@
show "carrier \<Z> = UNIV" by simp
\<comment> \<open>Operations\<close>
- { fix x y show "mult \<Z> x y = x * y" by simp }
+ show "mult \<Z> x y = x * y" for x y by simp
show "one \<Z> = 1" by simp
show "pow \<Z> x n = x^n" by (induct n) simp_all
qed
@@ -67,11 +67,8 @@
then interpret int: comm_monoid \<Z> .
\<comment> \<open>Operations\<close>
- { fix x y have "mult \<Z> x y = x * y" by simp }
- note mult = this
- have one: "one \<Z> = 1" by simp
show "finprod \<Z> f A = prod f A"
- by (induct A rule: infinite_finite_induct, auto)
+ by (induct A rule: infinite_finite_induct) auto
qed
interpretation int: abelian_monoid \<Z>
@@ -88,12 +85,10 @@
show "carrier \<Z> = UNIV" by simp
\<comment> \<open>Operations\<close>
- { fix x y show "add \<Z> x y = x + y" by simp }
- note add = this
- show zero: "zero \<Z> = 0"
- by simp
+ show "add \<Z> x y = x + y" for x y by simp
+ show zero: "zero \<Z> = 0" by simp
show "finsum \<Z> f A = sum f A"
- by (induct A rule: infinite_finite_induct, auto)
+ by (induct A rule: infinite_finite_induct) auto
qed
interpretation int: abelian_group \<Z>
@@ -118,17 +113,15 @@
qed auto
then interpret int: abelian_group \<Z> .
\<comment> \<open>Operations\<close>
- { fix x y have "add \<Z> x y = x + y" by simp }
- note add = this
+ have add: "add \<Z> x y = x + y" for x y by simp
have zero: "zero \<Z> = 0" by simp
- {
- fix x
+ show a_inv: "a_inv \<Z> x = - x" for x
+ proof -
have "add \<Z> (- x) x = zero \<Z>"
by (simp add: add zero)
- then show "a_inv \<Z> x = - x"
+ then show ?thesis
by (simp add: int.minus_equality)
- }
- note a_inv = this
+ qed
show "a_minus \<Z> x y = x - y"
by (simp add: int.minus_eq add a_inv)
qed (simp add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq)+
--- a/src/HOL/Algebra/Multiplicative_Group.thy Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Multiplicative_Group.thy Wed Nov 13 20:10:34 2024 +0100
@@ -216,37 +216,43 @@
assumes "n > 0"
shows "(\<Sum>d | d dvd n. phi' d) = n"
proof -
- { fix d assume "d dvd n" then obtain q where q: "n = d * q" ..
- have "card {a. 1 \<le> a \<and> a \<le> d \<and> coprime a d} = card {m \<in> {1 .. n}. n div gcd m n = d}"
- (is "card ?RF = card ?F")
- proof (rule card_bij_eq)
- { fix a b assume "a * n div d = b * n div d"
- hence "a * (n div d) = b * (n div d)"
- using dvd_div_mult[OF \<open>d dvd n\<close>] by (fastforce simp add: mult.commute)
- hence "a = b" using dvd_div_ge_1[OF _ \<open>d dvd n\<close>] \<open>n>0\<close>
- by (simp add: mult.commute nat_mult_eq_cancel1)
- } thus "inj_on (\<lambda>a. a*n div d) ?RF" unfolding inj_on_def by blast
- { fix a assume a: "a\<in>?RF"
- hence "a * (n div d) \<ge> 1" using \<open>n>0\<close> dvd_div_ge_1[OF _ \<open>d dvd n\<close>] by simp
- hence ge_1: "a * n div d \<ge> 1" by (simp add: \<open>d dvd n\<close> div_mult_swap)
- have le_n: "a * n div d \<le> n" using div_mult_mono a by simp
- have "gcd (a * n div d) n = n div d * gcd a d"
- by (simp add: gcd_mult_distrib_nat q ac_simps)
- hence "n div gcd (a * n div d) n = d*n div (d*(n div d))" using a by simp
- hence "a * n div d \<in> ?F"
- using ge_1 le_n by (fastforce simp add: \<open>d dvd n\<close>)
- } thus "(\<lambda>a. a*n div d) ` ?RF \<subseteq> ?F" by blast
- { fix m l assume A: "m \<in> ?F" "l \<in> ?F" "m div gcd m n = l div gcd l n"
- hence "gcd m n = gcd l n" using dvd_div_eq_2[OF assms] by fastforce
- hence "m = l" using dvd_div_eq_1[of "gcd m n" m l] A(3) by fastforce
- } thus "inj_on (\<lambda>a. a div gcd a n) ?F" unfolding inj_on_def by blast
- { fix m assume "m \<in> ?F"
- hence "m div gcd m n \<in> ?RF" using dvd_div_ge_1
- by (fastforce simp add: div_le_mono div_gcd_coprime)
- } thus "(\<lambda>a. a div gcd a n) ` ?F \<subseteq> ?RF" by blast
- qed force+
- } hence phi'_eq: "\<And>d. d dvd n \<Longrightarrow> phi' d = card {m \<in> {1 .. n}. n div gcd m n = d}"
- unfolding phi'_def by presburger
+ have "card {a. 1 \<le> a \<and> a \<le> d \<and> coprime a d} = card {m \<in> {1 .. n}. n div gcd m n = d}"
+ (is "card ?RF = card ?F")
+ if "d dvd n" for d
+ proof (rule card_bij_eq)
+ from that obtain q where q: "n = d * q" ..
+ have "a = b" if "a * n div d = b * n div d" for a b
+ proof -
+ from that have "a * (n div d) = b * (n div d)"
+ using dvd_div_mult[OF \<open>d dvd n\<close>] by (fastforce simp add: mult.commute)
+ then show ?thesis using dvd_div_ge_1[OF _ \<open>d dvd n\<close>] \<open>n>0\<close>
+ by (simp add: mult.commute nat_mult_eq_cancel1)
+ qed
+ thus "inj_on (\<lambda>a. a*n div d) ?RF" unfolding inj_on_def by blast
+ have "a * n div d \<in> ?F" if a: "a\<in>?RF" for a
+ proof -
+ from that have "a * (n div d) \<ge> 1" using \<open>n>0\<close> dvd_div_ge_1[OF _ \<open>d dvd n\<close>] by simp
+ hence ge_1: "a * n div d \<ge> 1" by (simp add: \<open>d dvd n\<close> div_mult_swap)
+ have le_n: "a * n div d \<le> n" using div_mult_mono a by simp
+ have "gcd (a * n div d) n = n div d * gcd a d"
+ by (simp add: gcd_mult_distrib_nat q ac_simps)
+ hence "n div gcd (a * n div d) n = d*n div (d*(n div d))" using a by simp
+ then show ?thesis
+ using ge_1 le_n by (fastforce simp add: \<open>d dvd n\<close>)
+ qed
+ thus "(\<lambda>a. a*n div d) ` ?RF \<subseteq> ?F" by blast
+ have "m = l" if A: "m \<in> ?F" "l \<in> ?F" "m div gcd m n = l div gcd l n" for m l
+ proof -
+ from that have "gcd m n = gcd l n" using dvd_div_eq_2[OF assms] by fastforce
+ then show ?thesis using dvd_div_eq_1[of "gcd m n" m l] A(3) by fastforce
+ qed
+ thus "inj_on (\<lambda>a. a div gcd a n) ?F" unfolding inj_on_def by blast
+ have "m div gcd m n \<in> ?RF" if "m \<in> ?F" for m
+ using that dvd_div_ge_1 by (fastforce simp add: div_le_mono div_gcd_coprime)
+ thus "(\<lambda>a. a div gcd a n) ` ?F \<subseteq> ?RF" by blast
+ qed force+
+ hence phi'_eq: "\<And>d. d dvd n \<Longrightarrow> phi' d = card {m \<in> {1 .. n}. n div gcd m n = d}"
+ unfolding phi'_def by presburger
have fin: "finite {d. d dvd n}" using dvd_nat_bounds[OF \<open>n>0\<close>] by force
have "(\<Sum>d | d dvd n. phi' d)
= card (\<Union>d \<in> {d. d dvd n}. {m \<in> {1 .. n}. n div gcd m n = d})"
@@ -419,22 +425,23 @@
proof (rule inj_onI, rule ccontr)
fix x y :: nat
assume A: "x \<in> {1 .. ord a}" "y \<in> {1 .. ord a}" "a [^] x = a [^] y" "x\<noteq>y"
- { assume "x < ord a" "y < ord a"
- hence False using ord_inj[OF assms] A unfolding inj_on_def by fastforce
- }
- moreover
- { assume "x = ord a" "y < ord a"
+ then consider "x < ord a" "y < ord a" | "x = ord a" "y < ord a" | "y = ord a" "x < ord a"
+ by force
+ then show False
+ proof cases
+ case 1
+ then show ?thesis using ord_inj[OF assms] A unfolding inj_on_def by fastforce
+ next
+ case 2
hence "a [^] y = a [^] (0::nat)" using pow_ord_eq_1 A by (simp add: a)
hence "y=0" using ord_inj[OF assms] \<open>y < ord a\<close> unfolding inj_on_def by force
- hence False using A by fastforce
- }
- moreover
- { assume "y = ord a" "x < ord a"
+ with A show ?thesis by fastforce
+ next
+ case 3
hence "a [^] x = a [^] (0::nat)" using pow_ord_eq_1 A by (simp add: a)
hence "x=0" using ord_inj[OF assms] \<open>x < ord a\<close> unfolding inj_on_def by force
- hence False using A by fastforce
- }
- ultimately show False using A by force
+ with A show ?thesis by fastforce
+ qed
qed
lemma (in group) ord_ge_1:
@@ -462,8 +469,9 @@
shows "{a[^]x | x. x \<in> (UNIV :: nat set)} = {a[^]x | x. x \<in> {0 .. ord a - 1}}" (is "?L = ?R")
proof
show "?R \<subseteq> ?L" by blast
- { fix y assume "y \<in> ?L"
- then obtain x::nat where x: "y = a[^]x" by auto
+ have "y \<in> {a[^]x | x. x \<in> {0 .. ord a - 1}}" if "y \<in> ?L" for y
+ proof -
+ from that obtain x::nat where x: "y = a[^]x" by auto
define r q where "r = x mod ord a" and "q = x div ord a"
then have "x = q * ord a + r"
by (simp add: div_mult_mod_eq)
@@ -472,8 +480,8 @@
hence "y = a[^]r" using assms by (simp add: pow_ord_eq_1)
have "r < ord a" using ord_ge_1[OF assms] by (simp add: r_def)
hence "r \<in> {0 .. ord a - 1}" by (force simp: r_def)
- hence "y \<in> {a[^]x | x. x \<in> {0 .. ord a - 1}}" using \<open>y=a[^]r\<close> by blast
- }
+ thus ?thesis using \<open>y=a[^]r\<close> by blast
+ qed
thus "?L \<subseteq> ?R" by auto
qed
@@ -598,20 +606,21 @@
assumes "a \<in> carrier G" "ord a \<noteq> 0"
shows "{a[^]x | x. x \<in> (UNIV :: nat set)} = {a[^]x | x. x \<in> {0 .. ord a - 1}}" (is "?L = ?R")
proof
- show "?R \<subseteq> ?L" by blast
- { fix y assume "y \<in> ?L"
- then obtain x::nat where x: "y = a[^]x" by auto
- define r q where "r = x mod ord a" and "q = x div ord a"
- then have "x = q * ord a + r"
- by (simp add: div_mult_mod_eq)
- hence "y = (a[^]ord a)[^]q \<otimes> a[^]r"
- using x assms by (metis mult.commute nat_pow_mult nat_pow_pow)
- hence "y = a[^]r" using assms by simp
- have "r < ord a" using assms by (simp add: r_def)
- hence "r \<in> {0 .. ord a - 1}" by (force simp: r_def)
- hence "y \<in> {a[^]x | x. x \<in> {0 .. ord a - 1}}" using \<open>y=a[^]r\<close> by blast
- }
- thus "?L \<subseteq> ?R" by auto
+ show "?R \<subseteq> ?L" by blast
+ have "y \<in> {a[^]x | x. x \<in> {0 .. ord a - 1}}" if "y \<in> ?L" for y
+ proof -
+ from that obtain x::nat where x: "y = a[^]x" by auto
+ define r q where "r = x mod ord a" and "q = x div ord a"
+ then have "x = q * ord a + r"
+ by (simp add: div_mult_mod_eq)
+ hence "y = (a[^]ord a)[^]q \<otimes> a[^]r"
+ using x assms by (metis mult.commute nat_pow_mult nat_pow_pow)
+ hence "y = a[^]r" using assms by simp
+ have "r < ord a" using assms by (simp add: r_def)
+ hence "r \<in> {0 .. ord a - 1}" by (force simp: r_def)
+ then show ?thesis using \<open>y=a[^]r\<close> by blast
+ qed
+ thus "?L \<subseteq> ?R" by auto
qed
lemma generate_pow_nat:
@@ -669,8 +678,7 @@
then show ?thesis
using \<open>ord a = 0\<close> by auto
next
- case False
- note finite_subgroup = this
+ case finite_subgroup: False
then have "generate G { a } = (([^]) a) ` {0..ord a - 1}"
using generate_pow_nat ord_elems_inf_carrier a by auto
hence "card (generate G {a}) = card {0..ord a - 1}"
@@ -952,12 +960,14 @@
have set_eq2: "{x \<in> carrier (mult_of R) . group.ord (mult_of R) x = d}
= (\<lambda> n . a[^]n) ` {n \<in> {1 .. d}. group.ord (mult_of R) (a[^]n) = d}" (is "?L = ?R")
proof
- { fix x assume x: "x \<in> (carrier (mult_of R)) \<and> group.ord (mult_of R) x = d"
- hence "x \<in> {x \<in> carrier (mult_of R). x [^] d = \<one>}"
+ have "x \<in> ?R" if x: "x \<in> (carrier (mult_of R)) \<and> group.ord (mult_of R) x = d" for x
+ proof -
+ from that have "x \<in> {x \<in> carrier (mult_of R). x [^] d = \<one>}"
by (simp add: G.pow_ord_eq_1[of x, symmetric])
then obtain n where n: "x = a[^]n \<and> n \<in> {1 .. d}" using set_eq1 by blast
- hence "x \<in> ?R" using x by fast
- } thus "?L \<subseteq> ?R" by blast
+ then show ?thesis using x by fast
+ qed
+ thus "?L \<subseteq> ?R" by blast
show "?R \<subseteq> ?L" using a by (auto simp add: carrier_mult_of[symmetric] simp del: carrier_mult_of)
qed
have "inj_on (\<lambda> n . a[^]n) {n \<in> {1 .. d}. group.ord (mult_of R) (a[^]n) = d}"
@@ -994,27 +1004,30 @@
using fin finite by (subst card_UN_disjoint) auto
also have "?U = carrier (mult_of R)"
proof
- { fix x assume x: "x \<in> carrier (mult_of R)"
- hence x': "x\<in>carrier (mult_of R)" by simp
+ have "x \<in> ?U" if x: "x \<in> carrier (mult_of R)" for x
+ proof -
+ from that have x': "x\<in>carrier (mult_of R)" by simp
then have "group.ord (mult_of R) x dvd order (mult_of R)"
using G.ord_dvd_group_order by blast
- hence "x \<in> ?U" using dvd_nat_bounds[of "order (mult_of R)" "group.ord (mult_of R) x"] x by blast
- } thus "carrier (mult_of R) \<subseteq> ?U" by blast
+ then show ?thesis
+ using dvd_nat_bounds[of "order (mult_of R)" "group.ord (mult_of R) x"] x by blast
+ qed
+ thus "carrier (mult_of R) \<subseteq> ?U" by blast
qed auto
also have "card ... = order (mult_of R)"
using order_mult_of finite' by (simp add: order_def)
finally have sum_Ns_eq: "(\<Sum>d | d dvd order (mult_of R). ?N d) = order (mult_of R)" .
- { fix d assume d: "d dvd order (mult_of R)"
- have "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} \<le> phi' d"
- proof cases
- assume "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} = 0" thus ?thesis by presburger
- next
- assume "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} \<noteq> 0"
- hence "\<exists>a \<in> carrier (mult_of R). group.ord (mult_of R) a = d" by (auto simp: card_eq_0_iff)
- thus ?thesis using num_elems_of_ord_eq_phi'[OF finite d] by auto
- qed
- }
+ have "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} \<le> phi' d"
+ if d: "d dvd order (mult_of R)" for d
+ proof (cases "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} = 0")
+ case True
+ thus ?thesis by presburger
+ next
+ case False
+ hence "\<exists>a \<in> carrier (mult_of R). group.ord (mult_of R) a = d" by (auto simp: card_eq_0_iff)
+ thus ?thesis using num_elems_of_ord_eq_phi'[OF finite d] by auto
+ qed
hence all_le: "\<And>i. i \<in> {d. d dvd order (mult_of R) }
\<Longrightarrow> (\<lambda>i. card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = i}) i \<le> (\<lambda>i. phi' i) i" by fast
hence le: "(\<Sum>i | i dvd order (mult_of R). ?N i)
--- a/src/HOL/Algebra/Polynomial_Divisibility.thy Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Polynomial_Divisibility.thy Wed Nov 13 20:10:34 2024 +0100
@@ -735,27 +735,25 @@
assumes "subring K R" and "p \<in> carrier (K[X])" and "q \<in> carrier (K[X])"
shows "p \<sim>\<^bsub>K[X]\<^esub> q \<Longrightarrow> length p = length q"
proof -
- { fix p q
- assume p: "p \<in> carrier (K[X])" and q: "q \<in> carrier (K[X])" and "p \<sim>\<^bsub>K[X]\<^esub> q"
- have "length p \<le> length q"
- proof (cases "q = []")
- case True with \<open>p \<sim>\<^bsub>K[X]\<^esub> q\<close> have "p = []"
- unfolding associated_def True factor_def univ_poly_def by auto
- thus ?thesis
- using True by simp
- next
- case False
- from \<open>p \<sim>\<^bsub>K[X]\<^esub> q\<close> have "p divides\<^bsub>K [X]\<^esub> q"
- unfolding associated_def by simp
- hence "p divides\<^bsub>poly_ring R\<^esub> q"
- using carrier_polynomial[OF assms(1)]
- unfolding factor_def univ_poly_carrier univ_poly_mult by auto
- with \<open>q \<noteq> []\<close> have "degree p \<le> degree q"
- using pdivides_imp_degree_le[OF assms(1) p q] unfolding pdivides_def by simp
- with \<open>q \<noteq> []\<close> show ?thesis
- by (cases "p = []", auto simp add: Suc_leI le_diff_iff)
- qed
- } note aux_lemma = this
+ have aux_lemma: "length p \<le> length q"
+ if p: "p \<in> carrier (K[X])" and q: "q \<in> carrier (K[X])" and "p \<sim>\<^bsub>K[X]\<^esub> q" for p q
+ proof (cases "q = []")
+ case True with \<open>p \<sim>\<^bsub>K[X]\<^esub> q\<close> have "p = []"
+ unfolding associated_def True factor_def univ_poly_def by auto
+ thus ?thesis
+ using True by simp
+ next
+ case False
+ from \<open>p \<sim>\<^bsub>K[X]\<^esub> q\<close> have "p divides\<^bsub>K [X]\<^esub> q"
+ unfolding associated_def by simp
+ hence "p divides\<^bsub>poly_ring R\<^esub> q"
+ using carrier_polynomial[OF assms(1)]
+ unfolding factor_def univ_poly_carrier univ_poly_mult by auto
+ with \<open>q \<noteq> []\<close> have "degree p \<le> degree q"
+ using pdivides_imp_degree_le[OF assms(1) p q] unfolding pdivides_def by simp
+ with \<open>q \<noteq> []\<close> show ?thesis
+ by (cases "p = []", auto simp add: Suc_leI le_diff_iff)
+ qed
interpret UP: domain "K[X]"
using univ_poly_is_domain[OF assms(1)] .
@@ -896,21 +894,23 @@
interpret UP: domain "K[X]"
using univ_poly_is_domain[OF assms(1)] .
- { fix q r
- assume q: "q \<in> carrier (K[X])" and r: "r \<in> carrier (K[X])" and "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r"
- hence not_zero: "q \<noteq> []" "r \<noteq> []"
+ have aux_lemma1: "degree q + degree r = 1" "q \<noteq> []" "r \<noteq> []"
+ if q: "q \<in> carrier (K[X])" and r: "r \<in> carrier (K[X])" and "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r" for q r
+ proof -
+ from that have not_zero: "q \<noteq> []" "r \<noteq> []"
by (metis UP.integral_iff list.distinct(1) univ_poly_zero)+
have "degree (q \<otimes>\<^bsub>K[X]\<^esub> r) = degree q + degree r"
using not_zero poly_mult_degree_eq[OF assms(1)] q r
by (simp add: univ_poly_carrier univ_poly_mult)
- with sym[OF \<open>[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r\<close>] have "degree q + degree r = 1" and "q \<noteq> []" "r \<noteq> []"
+ with sym[OF \<open>[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r\<close>] show "degree q + degree r = 1" and "q \<noteq> []" "r \<noteq> []"
using not_zero by auto
- } note aux_lemma1 = this
+ qed
- { fix q r
- assume q: "q \<in> carrier (K[X])" "q \<noteq> []" and r: "r \<in> carrier (K[X])" "r \<noteq> []"
- and "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r" and "degree q = 1" and "degree r = 0"
- hence "length q = Suc (Suc 0)" and "length r = Suc 0"
+ have aux_lemma2: "r \<in> Units (K[X])"
+ if q: "q \<in> carrier (K[X])" "q \<noteq> []" and r: "r \<in> carrier (K[X])" "r \<noteq> []"
+ and "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r" and "degree q = 1" and "degree r = 0" for q r
+ proof -
+ from that have "length q = Suc (Suc 0)" and "length r = Suc 0"
by (linarith, metis add.right_neutral add_eq_if length_0_conv)
from \<open>length q = Suc (Suc 0)\<close> obtain c d where q_def: "q = [ c, d ]"
by (metis length_0_conv length_Cons list.exhaust nat.inject)
@@ -933,9 +933,9 @@
moreover have "[ c \<otimes> inv_a ] \<otimes>\<^bsub>K[X]\<^esub> r = [ \<one> ]"
using \<open>a = c \<otimes> e\<close> a inv_a c e subsetD[OF subringE(1)[OF assms(1)]]
unfolding r_def univ_poly_mult by (auto) (simp add: m_assoc m_lcomm integral_iff)+
- ultimately have "r \<in> Units (K[X])"
+ ultimately show ?thesis
using r(1) UP.m_comm[OF in_carrier r(1)] unfolding sym[OF univ_poly_one[of R K]] Units_def by auto
- } note aux_lemma2 = this
+ qed
fix q r
assume q: "q \<in> carrier (K[X])" and r: "r \<in> carrier (K[X])" and qr: "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r"
@@ -1264,24 +1264,24 @@
interpret UP: domain "poly_ring R"
using univ_poly_is_domain[OF carrier_is_subring] .
- { fix p q
- assume p: "p \<in> carrier (poly_ring R)" and q: "q \<in> carrier (poly_ring R)" and pq: "p \<sim>\<^bsub>poly_ring R\<^esub> q"
- have "is_root p x \<Longrightarrow> is_root q x"
- proof -
- assume is_root: "is_root p x"
- then have "[ \<one>, \<ominus> x ] pdivides p" and "p \<noteq> []" and "x \<in> carrier R"
- using is_root_imp_pdivides[OF p] unfolding is_root_def by auto
- moreover have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
- using is_root unfolding is_root_def sym[OF univ_poly_carrier] polynomial_def by simp
- ultimately have "[ \<one>, \<ominus> x ] pdivides q"
- using UP.divides_cong_r[OF _ pq ] unfolding pdivides_def by simp
- with \<open>p \<noteq> []\<close> and \<open>x \<in> carrier R\<close> show ?thesis
- using associated_polynomials_imp_same_length[OF carrier_is_subring p q pq]
- pdivides_imp_is_root[of q x]
- by fastforce
- qed
- }
-
+ have "is_root q x"
+ if p: "p \<in> carrier (poly_ring R)"
+ and q: "q \<in> carrier (poly_ring R)"
+ and pq: "p \<sim>\<^bsub>poly_ring R\<^esub> q"
+ and is_root: "is_root p x"
+ for p q
+ proof -
+ from is_root have "[ \<one>, \<ominus> x ] pdivides p" and "p \<noteq> []" and "x \<in> carrier R"
+ using is_root_imp_pdivides[OF p] unfolding is_root_def by auto
+ moreover have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
+ using is_root unfolding is_root_def sym[OF univ_poly_carrier] polynomial_def by simp
+ ultimately have "[ \<one>, \<ominus> x ] pdivides q"
+ using UP.divides_cong_r[OF _ pq ] unfolding pdivides_def by simp
+ with \<open>p \<noteq> []\<close> and \<open>x \<in> carrier R\<close> show ?thesis
+ using associated_polynomials_imp_same_length[OF carrier_is_subring p q pq]
+ pdivides_imp_is_root[of q x]
+ by fastforce
+ qed
then show ?thesis
using assms UP.associated_sym[OF assms(3)] by blast
qed
--- a/src/HOL/Algebra/Polynomials.thy Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Polynomials.thy Wed Nov 13 20:10:34 2024 +0100
@@ -217,29 +217,30 @@
hence deg_eq: "degree p1 = degree p2"
using degree_def'[OF assms(1)] degree_def'[OF assms(2)] by auto
thus "p1 = p2"
- proof (cases)
- assume "p1 \<noteq> [] \<and> p2 \<noteq> []"
+ proof (cases "p1 \<noteq> [] \<and> p2 \<noteq> []")
+ case True
hence "length p1 = length p2"
using deg_eq by (simp add: Nitpick.size_list_simp(2))
thus ?thesis
using coeff_iff_length_cond[of p1 p2] coeff_eq by simp
next
- { fix p1 p2 assume A: "p1 = []" "coeff p1 = coeff p2" "polynomial K p2"
- have "p2 = []"
- proof (rule ccontr)
- assume "p2 \<noteq> []"
- hence "(coeff p2) (degree p2) \<noteq> \<zero>"
- using A(3) unfolding polynomial_def
- by (metis coeff.simps(2) list.collapse)
- moreover have "(coeff p1) ` UNIV = { \<zero> }"
- using A(1) by auto
- hence "(coeff p2) ` UNIV = { \<zero> }"
- using A(2) by simp
- ultimately show False
- by blast
- qed } note aux_lemma = this
- assume "\<not> (p1 \<noteq> [] \<and> p2 \<noteq> [])"
- hence "p1 = [] \<or> p2 = []" by simp
+ case False
+ have aux_lemma: "p2 = []"
+ if A: "p1 = []" "coeff p1 = coeff p2" "polynomial K p2"
+ for p1 p2
+ proof (rule ccontr)
+ assume "p2 \<noteq> []"
+ hence "(coeff p2) (degree p2) \<noteq> \<zero>"
+ using A(3) unfolding polynomial_def
+ by (metis coeff.simps(2) list.collapse)
+ moreover have "(coeff p1) ` UNIV = { \<zero> }"
+ using A(1) by auto
+ hence "(coeff p2) ` UNIV = { \<zero> }"
+ using A(2) by simp
+ ultimately show False
+ by blast
+ qed
+ from False have "p1 = [] \<or> p2 = []" by simp
thus ?thesis
using assms coeff_eq aux_lemma[of p1 p2] aux_lemma[of p2 p1] by auto
qed
@@ -409,20 +410,19 @@
assumes "set p1 \<subseteq> K" and "set p2 \<subseteq> K"
shows "polynomial K (poly_add p1 p2)"
proof -
- { fix p1 p2 assume A: "set p1 \<subseteq> K" "set p2 \<subseteq> K" "length p1 \<ge> length p2"
- hence "polynomial K (poly_add p1 p2)"
- proof -
- define p2' where "p2' = (replicate (length p1 - length p2) \<zero>) @ p2"
- hence "set p2' \<subseteq> K" and "length p1 = length p2'"
- using A(2-3) subringE(2)[OF K] by auto
- hence "set (map2 (\<oplus>) p1 p2') \<subseteq> K"
- using A(1) subringE(7)[OF K]
- by (induct p1) (auto, metis set_ConsD subsetD set_zip_leftD set_zip_rightD)
- thus ?thesis
- unfolding p2'_def using normalize_gives_polynomial A(3) by simp
- qed }
- thus ?thesis
- using assms by auto
+ have "polynomial K (poly_add p1 p2)"
+ if A: "set p1 \<subseteq> K" "set p2 \<subseteq> K" "length p1 \<ge> length p2" for p1 p2
+ proof -
+ define p2' where "p2' = (replicate (length p1 - length p2) \<zero>) @ p2"
+ hence "set p2' \<subseteq> K" and "length p1 = length p2'"
+ using A(2-3) subringE(2)[OF K] by auto
+ hence "set (map2 (\<oplus>) p1 p2') \<subseteq> K"
+ using A(1) subringE(7)[OF K]
+ by (induct p1) (auto, metis set_ConsD subsetD set_zip_leftD set_zip_rightD)
+ thus ?thesis
+ unfolding p2'_def using normalize_gives_polynomial A(3) by simp
+ qed
+ thus ?thesis using assms by auto
qed
lemma poly_add_closed: "\<lbrakk> polynomial K p1; polynomial K p2 \<rbrakk> \<Longrightarrow> polynomial K (poly_add p1 p2)"
@@ -432,29 +432,28 @@
assumes "polynomial K p1" "polynomial K p2" and "length p1 \<noteq> length p2"
shows "length (poly_add p1 p2) = max (length p1) (length p2)"
proof -
- { fix p1 p2 assume A: "polynomial K p1" "polynomial K p2" "length p1 > length p2"
- hence "length (poly_add p1 p2) = max (length p1) (length p2)"
- proof -
- let ?p2 = "(replicate (length p1 - length p2) \<zero>) @ p2"
- have p1: "p1 \<noteq> []" and p2: "?p2 \<noteq> []"
- using A(3) by auto
- then have "zip p1 (replicate (length p1 - length p2) \<zero> @ p2) = zip (lead_coeff p1 # tl p1) (lead_coeff (replicate (length p1 - length p2) \<zero> @ p2) # tl (replicate (length p1 - length p2) \<zero> @ p2))"
- by auto
- hence "lead_coeff (map2 (\<oplus>) p1 ?p2) = lead_coeff p1 \<oplus> lead_coeff ?p2"
- by simp
- moreover have "lead_coeff p1 \<in> carrier R"
- using p1 A(1) lead_coeff_in_carrier[OF K, of "hd p1" "tl p1"] by auto
- ultimately have "lead_coeff (map2 (\<oplus>) p1 ?p2) = lead_coeff p1"
- using A(3) by auto
- moreover have "lead_coeff p1 \<noteq> \<zero>"
- using p1 A(1) unfolding polynomial_def by simp
- ultimately have "length (normalize (map2 (\<oplus>) p1 ?p2)) = length p1"
- using normalize_length_eq by auto
- thus ?thesis
- using A(3) by auto
- qed }
- thus ?thesis
- using assms by auto
+ have "length (poly_add p1 p2) = max (length p1) (length p2)"
+ if A: "polynomial K p1" "polynomial K p2" "length p1 > length p2" for p1 p2
+ proof -
+ let ?p2 = "(replicate (length p1 - length p2) \<zero>) @ p2"
+ have p1: "p1 \<noteq> []" and p2: "?p2 \<noteq> []"
+ using A(3) by auto
+ then have "zip p1 (replicate (length p1 - length p2) \<zero> @ p2) =
+ zip (lead_coeff p1 # tl p1) (lead_coeff (replicate (length p1 - length p2) \<zero> @ p2) # tl (replicate (length p1 - length p2) \<zero> @ p2))"
+ by auto
+ hence "lead_coeff (map2 (\<oplus>) p1 ?p2) = lead_coeff p1 \<oplus> lead_coeff ?p2"
+ by simp
+ moreover have "lead_coeff p1 \<in> carrier R"
+ using p1 A(1) lead_coeff_in_carrier[OF K, of "hd p1" "tl p1"] by auto
+ ultimately have "lead_coeff (map2 (\<oplus>) p1 ?p2) = lead_coeff p1"
+ using A(3) by auto
+ moreover have "lead_coeff p1 \<noteq> \<zero>"
+ using p1 A(1) unfolding polynomial_def by simp
+ ultimately have "length (normalize (map2 (\<oplus>) p1 ?p2)) = length p1"
+ using normalize_length_eq by auto
+ thus ?thesis using A(3) by auto
+ qed
+ thus ?thesis using assms by auto
qed
lemma poly_add_degree_eq:
@@ -471,10 +470,10 @@
lemma poly_add_length_le: "length (poly_add p1 p2) \<le> max (length p1) (length p2)"
proof -
- { fix p1 p2 :: "'a list" assume A: "length p1 \<ge> length p2"
- let ?p2 = "(replicate (length p1 - length p2) \<zero>) @ p2"
- have "length (poly_add p1 p2) \<le> max (length p1) (length p2)"
- using normalize_length_le[of "map2 (\<oplus>) p1 ?p2"] A by auto }
+ have "length (poly_add p1 p2) \<le> max (length p1) (length p2)"
+ if "length p1 \<ge> length p2" for p1 p2 :: "'a list"
+ using normalize_length_le[of "map2 (\<oplus>) p1 ((replicate (length p1 - length p2) \<zero>) @ p2)"] that
+ by auto
thus ?thesis
by (metis le_cases max.commute poly_add.simps)
qed
@@ -582,57 +581,58 @@
assumes "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
shows "poly_add p1 p2 = poly_add (normalize p1) p2"
proof -
- { fix n p1 p2 assume "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
- hence "poly_add p1 p2 = poly_add ((replicate n \<zero>) @ p1) p2"
- proof (induction n)
- case 0 thus ?case by simp
- next
- { fix p1 p2 :: "'a list"
- assume in_carrier: "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
- have "poly_add p1 p2 = poly_add (\<zero> # p1) p2"
- proof -
- have "length p1 \<ge> length p2 \<Longrightarrow> ?thesis"
- proof -
- assume A: "length p1 \<ge> length p2"
- let ?p2 = "\<lambda>n. (replicate n \<zero>) @ p2"
- have "poly_add p1 p2 = normalize (map2 (\<oplus>) (\<zero> # p1) (\<zero> # ?p2 (length p1 - length p2)))"
- using A by simp
- also have " ... = normalize (map2 (\<oplus>) (\<zero> # p1) (?p2 (length (\<zero> # p1) - length p2)))"
- by (simp add: A Suc_diff_le)
- also have " ... = poly_add (\<zero> # p1) p2"
- using A by simp
- finally show ?thesis .
- qed
+ have aux_lemma: "poly_add p1 p2 = poly_add ((replicate n \<zero>) @ p1) p2"
+ if "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
+ for n p1 p2
+ using that
+ proof (induction n)
+ case 0
+ thus ?case by simp
+ next
+ case (Suc n)
+ have aux_lemma: "poly_add p1 p2 = poly_add (\<zero> # p1) p2"
+ if in_carrier: "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
+ for p1 p2
+ proof -
+ have "length p1 \<ge> length p2 \<Longrightarrow> ?thesis"
+ proof -
+ assume A: "length p1 \<ge> length p2"
+ let ?p2 = "\<lambda>n. (replicate n \<zero>) @ p2"
+ have "poly_add p1 p2 = normalize (map2 (\<oplus>) (\<zero> # p1) (\<zero> # ?p2 (length p1 - length p2)))"
+ using A by simp
+ also have " ... = normalize (map2 (\<oplus>) (\<zero> # p1) (?p2 (length (\<zero> # p1) - length p2)))"
+ by (simp add: A Suc_diff_le)
+ also have " ... = poly_add (\<zero> # p1) p2"
+ using A by simp
+ finally show ?thesis .
+ qed
+ moreover have "length p2 > length p1 \<Longrightarrow> ?thesis"
+ proof -
+ assume A: "length p2 > length p1"
+ let ?f = "\<lambda>n p. (replicate n \<zero>) @ p"
+ have "poly_add p1 p2 = poly_add p2 p1"
+ using A by simp
+ also have " ... = normalize (map2 (\<oplus>) p2 (?f (length p2 - length p1) p1))"
+ using A by simp
+ also have " ... = normalize (map2 (\<oplus>) p2 (?f (length p2 - Suc (length p1)) (\<zero> # p1)))"
+ by (metis A Suc_diff_Suc append_Cons replicate_Suc replicate_app_Cons_same)
+ also have " ... = poly_add p2 (\<zero> # p1)"
+ using A by simp
+ also have " ... = poly_add (\<zero> # p1) p2"
+ using poly_add_comm[of p2 "\<zero> # p1"] in_carrier by auto
+ finally show ?thesis .
+ qed
+ ultimately show ?thesis by auto
+ qed
- moreover have "length p2 > length p1 \<Longrightarrow> ?thesis"
- proof -
- assume A: "length p2 > length p1"
- let ?f = "\<lambda>n p. (replicate n \<zero>) @ p"
- have "poly_add p1 p2 = poly_add p2 p1"
- using A by simp
- also have " ... = normalize (map2 (\<oplus>) p2 (?f (length p2 - length p1) p1))"
- using A by simp
- also have " ... = normalize (map2 (\<oplus>) p2 (?f (length p2 - Suc (length p1)) (\<zero> # p1)))"
- by (metis A Suc_diff_Suc append_Cons replicate_Suc replicate_app_Cons_same)
- also have " ... = poly_add p2 (\<zero> # p1)"
- using A by simp
- also have " ... = poly_add (\<zero> # p1) p2"
- using poly_add_comm[of p2 "\<zero> # p1"] in_carrier by auto
- finally show ?thesis .
- qed
-
- ultimately show ?thesis by auto
- qed } note aux_lemma = this
-
- case (Suc n)
- hence in_carrier: "set (replicate n \<zero> @ p1) \<subseteq> carrier R"
- by auto
- have "poly_add p1 p2 = poly_add (replicate n \<zero> @ p1) p2"
- using Suc by simp
- also have " ... = poly_add (replicate (Suc n) \<zero> @ p1) p2"
- using aux_lemma[OF in_carrier Suc(3)] by simp
- finally show ?case .
- qed } note aux_lemma = this
+ from Suc have in_carrier: "set (replicate n \<zero> @ p1) \<subseteq> carrier R"
+ by auto
+ have "poly_add p1 p2 = poly_add (replicate n \<zero> @ p1) p2"
+ using Suc by simp
+ also have " ... = poly_add (replicate (Suc n) \<zero> @ p1) p2"
+ using aux_lemma[OF in_carrier Suc(3)] by simp
+ finally show ?case .
+ qed
have "poly_add p1 p2 =
poly_add ((replicate (length p1 - length (normalize p1)) \<zero>) @ normalize p1) p2"
@@ -935,29 +935,29 @@
assumes "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
shows "poly_mult p1 p2 = poly_mult ((replicate n \<zero>) @ p1) p2"
proof -
- { fix p1 p2 assume A: "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
- hence "poly_mult p1 p2 = poly_mult (\<zero> # p1) p2"
- proof -
- let ?a_p2 = "(map ((\<otimes>) \<zero>) p2) @ (replicate (length p1) \<zero>)"
- have "?a_p2 = replicate (length p2 + length p1) \<zero>"
- using A(2) by (induction p2) (auto)
- hence "poly_mult (\<zero> # p1) p2 = poly_add (replicate (length p2 + length p1) \<zero>) (poly_mult p1 p2)"
- by simp
- also have " ... = poly_add (normalize (replicate (length p2 + length p1) \<zero>)) (poly_mult p1 p2)"
- using poly_add_normalize(1)[of "replicate (length p2 + length p1) \<zero>" "poly_mult p1 p2"]
- poly_mult_in_carrier[OF A] by force
- also have " ... = poly_mult p1 p2"
- using poly_add_zero(2)[OF _ poly_mult_is_polynomial[OF _ A]] carrier_is_subring
- normalize_replicate_zero[of "length p2 + length p1" "[]"] by simp
- finally show ?thesis by auto
- qed } note aux_lemma = this
-
+ have aux_lemma: "poly_mult p1 p2 = poly_mult (\<zero> # p1) p2"
+ if A: "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R" for p1 p2
+ proof -
+ let ?a_p2 = "(map ((\<otimes>) \<zero>) p2) @ (replicate (length p1) \<zero>)"
+ have "?a_p2 = replicate (length p2 + length p1) \<zero>"
+ using A(2) by (induction p2) (auto)
+ hence "poly_mult (\<zero> # p1) p2 = poly_add (replicate (length p2 + length p1) \<zero>) (poly_mult p1 p2)"
+ by simp
+ also have " ... = poly_add (normalize (replicate (length p2 + length p1) \<zero>)) (poly_mult p1 p2)"
+ using poly_add_normalize(1)[of "replicate (length p2 + length p1) \<zero>" "poly_mult p1 p2"]
+ poly_mult_in_carrier[OF A] by force
+ also have " ... = poly_mult p1 p2"
+ using poly_add_zero(2)[OF _ poly_mult_is_polynomial[OF _ A]] carrier_is_subring
+ normalize_replicate_zero[of "length p2 + length p1" "[]"] by simp
+ finally show ?thesis by auto
+ qed
from assms show ?thesis
proof (induction n)
- case 0 thus ?case by simp
+ case 0
+ thus ?case by simp
next
- case (Suc n) thus ?case
- using aux_lemma[of "replicate n \<zero> @ p1" p2] by force
+ case (Suc n)
+ thus ?case using aux_lemma[of "replicate n \<zero> @ p1" p2] by force
qed
qed
@@ -1896,14 +1896,15 @@
assumes "set p \<subseteq> carrier R" "set q \<subseteq> carrier R" and "a \<in> carrier R"
shows "eval (poly_add p q) a = (eval p a) \<oplus> (eval q a)"
proof -
- { fix p q assume A: "set p \<subseteq> carrier R" "set q \<subseteq> carrier R" "length p \<ge> length q"
- hence "eval (poly_add p ((replicate (length p - length q) \<zero>) @ q)) a =
+ have aux_lemma: "eval (poly_add p q) a = (eval p a) \<oplus> (eval q a)"
+ if A: "set p \<subseteq> carrier R" "set q \<subseteq> carrier R" "length p \<ge> length q" for p q
+ proof -
+ from that have "eval (poly_add p ((replicate (length p - length q) \<zero>) @ q)) a =
(eval p a) \<oplus> (eval ((replicate (length p - length q) \<zero>) @ q) a)"
using eval_poly_add_aux[OF A(1) _ _ assms(3), of "(replicate (length p - length q) \<zero>) @ q"] by force
- hence "eval (poly_add p q) a = (eval p a) \<oplus> (eval q a)"
- using eval_replicate[OF A(2) assms(3)] A(3) by auto }
- note aux_lemma = this
-
+ then show "eval (poly_add p q) a = (eval p a) \<oplus> (eval q a)"
+ using eval_replicate[OF A(2) assms(3)] A(3) by auto
+ qed
have ?thesis if "length q \<ge> length p"
using assms(1-2)[THEN eval_in_carrier[OF _ assms(3)]] poly_add_comm[OF assms(1-2)]
aux_lemma[OF assms(2,1) that]
@@ -1978,8 +1979,12 @@
case Nil thus ?case
using eval_in_carrier[OF assms(2-3)] by simp
next
- { fix n b assume b: "b \<in> carrier R"
- hence "set (map ((\<otimes>) b) q) \<subseteq> carrier R" and "set (replicate n \<zero>) \<subseteq> carrier R"
+ case (Cons b p)
+
+ have aux_lemma: "eval ((map ((\<otimes>) b) q) @ (replicate n \<zero>)) a = (eval (monom b n) a) \<otimes> (eval q a)"
+ if b: "b \<in> carrier R" for n b
+ proof -
+ from that have "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>"]
@@ -1990,12 +1995,11 @@
by simp
also have " ... = (b \<otimes> (a [^] n)) \<otimes> (eval q a)"
using eval_in_carrier[OF assms(2-3)] b assms(3) m_assoc m_comm by auto
- finally have "eval ((map ((\<otimes>) b) q) @ (replicate n \<zero>)) a = (eval (monom b n) a) \<otimes> (eval q a)"
- using eval_monom[OF b assms(3)] by simp }
- note aux_lemma = this
+ finally show ?thesis
+ using eval_monom[OF b assms(3)] by simp
+ qed
- case (Cons b p)
- hence in_carrier:
+ from Cons have in_carrier:
"eval (monom b (length p)) a \<in> carrier R" "eval p a \<in> carrier R" "eval q a \<in> carrier R" "b \<in> carrier R"
using eval_in_carrier monom_in_carrier assms by auto
have set_map: "set ((map ((\<otimes>) b) q) @ (replicate (length p) \<zero>)) \<subseteq> carrier R"
@@ -2183,43 +2187,52 @@
interpret UP: domain "K[X]"
using univ_poly_is_domain[OF assms(1)] .
- { fix l assume "set l \<subseteq> K"
- hence "poly_of_const a \<in> carrier (K[X])" if "a \<in> set l" for a
+ have aux_lemma1: "set (?map_norm l) \<subseteq> carrier (K[X])" if "set l \<subseteq> K" for l
+ proof -
+ from that have "poly_of_const a \<in> carrier (K[X])" if "a \<in> set l" for a
using that normalize_gives_polynomial[of "[ a ]" K]
unfolding univ_poly_carrier poly_of_const_def by auto
- hence "set (?map_norm l) \<subseteq> carrier (K[X])"
- by auto }
- note aux_lemma1 = this
+ then show ?thesis by auto
+ qed
- { fix q l assume set_l: "set l \<subseteq> K" and q: "q \<in> carrier (K[X])"
- from set_l have "UP.eval (?map_norm l) q = UP.eval (?map_norm ((replicate n \<zero>) @ l)) q" for n
- proof (induct n, simp)
- case (Suc n)
- from \<open>set l \<subseteq> K\<close> have set_replicate: "set ((replicate n \<zero>) @ l) \<subseteq> K"
- using subringE(2)[OF assms(1)] by (induct n) (auto)
- have step: "UP.eval (?map_norm l') q = UP.eval (?map_norm (\<zero> # l')) q" if "set l' \<subseteq> K" for l'
- using UP.eval_in_carrier[OF aux_lemma1[OF that]] q unfolding poly_of_const_def
- by (simp, simp add: sym[OF univ_poly_zero[of R K]])
- have "UP.eval (?map_norm l) q = UP.eval (?map_norm ((replicate n \<zero>) @ l)) q"
- using Suc by simp
- also have " ... = UP.eval (map poly_of_const ((replicate (Suc n) \<zero>) @ l)) q"
- using step[OF set_replicate] by simp
- finally show ?case .
- qed }
- note aux_lemma2 = this
+ have aux_lemma2: "UP.eval (?map_norm l) q = UP.eval (?map_norm ((replicate n \<zero>) @ l)) q"
+ if set_l: "set l \<subseteq> K" and q: "q \<in> carrier (K[X])"
+ for n q l
+ using set_l
+ proof (induct n)
+ case 0
+ then show ?case by simp
+ next
+ case (Suc n)
+ from \<open>set l \<subseteq> K\<close> have set_replicate: "set ((replicate n \<zero>) @ l) \<subseteq> K"
+ using subringE(2)[OF assms(1)] by (induct n) (auto)
+ have step: "UP.eval (?map_norm l') q = UP.eval (?map_norm (\<zero> # l')) q" if "set l' \<subseteq> K" for l'
+ using UP.eval_in_carrier[OF aux_lemma1[OF that]] q unfolding poly_of_const_def
+ by (simp, simp add: sym[OF univ_poly_zero[of R K]])
+ have "UP.eval (?map_norm l) q = UP.eval (?map_norm ((replicate n \<zero>) @ l)) q"
+ using Suc by simp
+ also have " ... = UP.eval (map poly_of_const ((replicate (Suc n) \<zero>) @ l)) q"
+ using step[OF set_replicate] by simp
+ finally show ?case .
+ qed
- { fix q l assume "set l \<subseteq> K" and q: "q \<in> carrier (K[X])"
+ have aux_lemma3: "UP.eval (?map_norm l) q = UP.eval (?map_norm (normalize l)) q"
+ if "set l \<subseteq> K" and q: "q \<in> carrier (K[X])" for q l
+ proof -
from \<open>set l \<subseteq> K\<close> have set_norm: "set (normalize l) \<subseteq> K"
by (induct l) (auto)
- have "UP.eval (?map_norm l) q = UP.eval (?map_norm (normalize l)) q"
+ show ?thesis
using aux_lemma2[OF set_norm q, of "length l - length (local.normalize l)"]
- unfolding sym[OF normalize_trick[of l]] .. }
- note aux_lemma3 = this
+ unfolding sym[OF normalize_trick[of l]] ..
+ qed
from \<open>p \<in> carrier (K[X])\<close> show ?thesis
proof (induct "length p" arbitrary: p rule: less_induct)
case less thus ?case
- proof (cases p, simp add: univ_poly_zero)
+ proof (cases p)
+ case Nil
+ then show ?thesis by (simp add: univ_poly_zero)
+ next
case (Cons a l)
hence a: "a \<in> carrier R - { \<zero> }" and set_l: "set l \<subseteq> carrier R" "set l \<subseteq> K"
using less(2) subringE(1)[OF assms(1)] unfolding sym[OF univ_poly_carrier] polynomial_def by auto
--- a/src/HOL/Algebra/Ring_Divisibility.thy Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Ring_Divisibility.thy Wed Nov 13 20:10:34 2024 +0100
@@ -518,22 +518,22 @@
assumes "C \<noteq> {}" "subset.chain { I. ideal I R } C"
shows "\<Union>C \<in> C"
proof -
- { fix S assume "finite S" "S \<subseteq> \<Union>C"
- hence "\<exists>I. I \<in> C \<and> S \<subseteq> I"
- proof (induct S)
- case empty thus ?case
- using assms(1) by blast
- next
- case (insert s S)
- then obtain I where I: "I \<in> C" "S \<subseteq> I"
- by blast
- moreover obtain I' where I': "I' \<in> C" "s \<in> I'"
- using insert(4) by blast
- ultimately have "I \<subseteq> I' \<or> I' \<subseteq> I"
- using assms unfolding pred_on.chain_def by blast
- thus ?case
- using I I' by blast
- qed } note aux_lemma = this
+ have aux_lemma: "\<exists>I. I \<in> C \<and> S \<subseteq> I" if "finite S" "S \<subseteq> \<Union>C" for S
+ using that
+ proof (induct S)
+ case empty
+ thus ?case using assms(1) by blast
+ next
+ case (insert s S)
+ then obtain I where I: "I \<in> C" "S \<subseteq> I"
+ by blast
+ moreover obtain I' where I': "I' \<in> C" "s \<in> I'"
+ using insert(4) by blast
+ ultimately have "I \<subseteq> I' \<or> I' \<subseteq> I"
+ using assms unfolding pred_on.chain_def by blast
+ thus ?case
+ using I I' by blast
+ qed
obtain S where S: "finite S" "S \<subseteq> carrier R" "\<Union>C = Idl S"
using finetely_gen[OF chain_Union_is_ideal[OF assms(2)]] assms(1) by auto
@@ -805,27 +805,27 @@
assumes "a \<in> carrier R" "b \<in> carrier R" "d \<in> carrier R"
shows "PIdl d = PIdl a <+>\<^bsub>R\<^esub> PIdl b \<longleftrightarrow> d gcdof a b"
proof -
- { fix a b d
- assume in_carrier: "a \<in> carrier R" "b \<in> carrier R" "d \<in> carrier R"
- and ideal_eq: "PIdl d = PIdl a <+>\<^bsub>R\<^esub> PIdl b"
- have "d gcdof a b"
- proof (auto simp add: isgcd_def)
- have "a \<in> PIdl d" and "b \<in> PIdl d"
- using in_carrier(1-2)[THEN cgenideal_ideal] additive_subgroup.zero_closed[OF ideal.axioms(1)]
- in_carrier(1-2)[THEN cgenideal_self] in_carrier(1-2)
- unfolding ideal_eq set_add_def' by force+
- thus "d divides a" and "d divides b"
- using in_carrier(1,2)[THEN to_contain_is_to_divide[OF in_carrier(3)]]
- cgenideal_minimal[OF cgenideal_ideal[OF in_carrier(3)]] by simp+
- next
- fix c assume c: "c \<in> carrier R" "c divides a" "c divides b"
- hence "PIdl a \<subseteq> PIdl c" and "PIdl b \<subseteq> PIdl c"
- using to_contain_is_to_divide in_carrier by auto
- hence "PIdl a <+>\<^bsub>R\<^esub> PIdl b \<subseteq> PIdl c"
- by (metis Un_subset_iff c(1) in_carrier(1-2) cgenideal_ideal genideal_minimal union_genideal)
- thus "c divides d"
- using ideal_eq to_contain_is_to_divide[OF c(1) in_carrier(3)] by simp
- qed } note aux_lemma = this
+ have aux_lemma: "d gcdof a b"
+ if in_carrier: "a \<in> carrier R" "b \<in> carrier R" "d \<in> carrier R"
+ and ideal_eq: "PIdl d = PIdl a <+>\<^bsub>R\<^esub> PIdl b"
+ for a b d
+ proof (auto simp add: isgcd_def)
+ have "a \<in> PIdl d" and "b \<in> PIdl d"
+ using in_carrier(1-2)[THEN cgenideal_ideal] additive_subgroup.zero_closed[OF ideal.axioms(1)]
+ in_carrier(1-2)[THEN cgenideal_self] in_carrier(1-2)
+ unfolding ideal_eq set_add_def' by force+
+ thus "d divides a" and "d divides b"
+ using in_carrier(1,2)[THEN to_contain_is_to_divide[OF in_carrier(3)]]
+ cgenideal_minimal[OF cgenideal_ideal[OF in_carrier(3)]] by simp+
+ next
+ fix c assume c: "c \<in> carrier R" "c divides a" "c divides b"
+ hence "PIdl a \<subseteq> PIdl c" and "PIdl b \<subseteq> PIdl c"
+ using to_contain_is_to_divide in_carrier by auto
+ hence "PIdl a <+>\<^bsub>R\<^esub> PIdl b \<subseteq> PIdl c"
+ by (metis Un_subset_iff c(1) in_carrier(1-2) cgenideal_ideal genideal_minimal union_genideal)
+ thus "c divides d"
+ using ideal_eq to_contain_is_to_divide[OF c(1) in_carrier(3)] by simp
+ qed
have "PIdl d = PIdl a <+>\<^bsub>R\<^esub> PIdl b \<Longrightarrow> d gcdof a b"
using aux_lemma assms by simp
--- a/src/HOL/Algebra/SndIsomorphismGrp.thy Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/SndIsomorphismGrp.thy Wed Nov 13 20:10:34 2024 +0100
@@ -119,15 +119,14 @@
have "group ((G\<lparr>carrier := H <#> S\<rparr>) Mod H)"
by (simp add: H_contained_in_set_mult normal.factorgroup_is_group normal_axioms
normal_restrict_supergroup normal_set_mult_subgroup)
- moreover
- { fix g
- assume g: "g \<in> S"
- with g have "g \<in> H <#> S"
+ moreover have "H #> g \<in> carrier ((G\<lparr>carrier := H <#> S\<rparr>) Mod H)" if g: "g \<in> S" for g
+ proof -
+ from g that have "g \<in> H <#> S"
using S_contained_in_set_mult by blast
- hence "H #> g \<in> carrier ((G\<lparr>carrier := H <#> S\<rparr>) Mod H)"
- unfolding FactGroup_def RCOSETS_def r_coset_def by auto }
- moreover
- have "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> H #> x \<otimes> y = H #> x <#> (H #> y)"
+ thus "H #> g \<in> carrier ((G\<lparr>carrier := H <#> S\<rparr>) Mod H)"
+ unfolding FactGroup_def RCOSETS_def r_coset_def by auto
+ qed
+ moreover have "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> H #> x \<otimes> y = H #> x <#> (H #> y)"
using normal.rcos_sum normal_axioms subgroup.mem_carrier subgrpS by fastforce
ultimately show ?thesis
by (auto simp: group_hom_def group_hom_axioms_def hom_def)
--- a/src/HOL/Algebra/Sym_Groups.thy Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/Sym_Groups.thy Wed Nov 13 20:10:34 2024 +0100
@@ -207,19 +207,22 @@
shows "\<exists>a b A' p'. a \<noteq> b \<and> A = (insert a (insert b A')) \<and>
swapidseq_ext A' n p' \<and> p = (transpose a b) \<circ> p'"
proof -
- { fix A n k and p :: "'a \<Rightarrow> 'a"
- assume "swapidseq_ext A n p" "n = Suc k"
- hence "\<exists>a b A' p'. a \<noteq> b \<and> A = (insert a (insert b A')) \<and>
- swapidseq_ext A' k p' \<and> p = (transpose a b) \<circ> p'"
- proof (induction, simp)
- case single thus ?case
- by (metis Un_insert_right insert_iff insert_is_Un swapidseq_ext.single)
- next
- case comp thus ?case
- by blast
- qed }
- thus ?thesis
- using assms by simp
+ have "\<exists>a b A' p'. a \<noteq> b \<and> A = (insert a (insert b A')) \<and>
+ swapidseq_ext A' k p' \<and> p = (transpose a b) \<circ> p'"
+ if "swapidseq_ext A n p" "n = Suc k"
+ for A n k and p :: "'a \<Rightarrow> 'a"
+ using that
+ proof (induction)
+ case empty
+ thus ?case by simp
+ next
+ case single
+ thus ?case by (metis Un_insert_right insert_iff insert_is_Un swapidseq_ext.single)
+ next
+ case comp
+ thus ?case by blast
+ qed
+ thus ?thesis using assms by simp
qed
lemma swapidseq_ext_backwards':
@@ -369,61 +372,61 @@
proof
show "generate (alt_group n) (three_cycles n) \<subseteq> carrier (alt_group n)"
using A.generate_subgroup_incl[OF three_cycles_incl A.subgroup_self] .
- next
show "carrier (alt_group n) \<subseteq> generate (alt_group n) (three_cycles n)"
proof
- { fix q :: "nat \<Rightarrow> nat" and a b c
- assume "a \<noteq> b" "b \<noteq> c" "{ a, b, c } \<subseteq> {1..n}"
- have "cycle_of_list [a, b, c] \<in> generate (alt_group n) (three_cycles n)"
- proof (cases)
- assume "c = a"
- hence "cycle_of_list [ a, b, c ] = id"
- by (simp add: swap_commute)
- thus "cycle_of_list [ a, b, c ] \<in> generate (alt_group n) (three_cycles n)"
- using one[of "alt_group n"] unfolding alt_group_one by simp
- next
- assume "c \<noteq> a"
- have "distinct [a, b, c]"
- using \<open>a \<noteq> b\<close> and \<open>b \<noteq> c\<close> and \<open>c \<noteq> a\<close> by auto
- with \<open>{ a, b, c } \<subseteq> {1..n}\<close>
- show "cycle_of_list [ a, b, c ] \<in> generate (alt_group n) (three_cycles n)"
- by (intro incl, fastforce)
- qed } note aux_lemma1 = this
+ have aux_lemma1: "cycle_of_list [a, b, c] \<in> generate (alt_group n) (three_cycles n)"
+ if "a \<noteq> b" "b \<noteq> c" "{ a, b, c } \<subseteq> {1..n}"
+ for q :: "nat \<Rightarrow> nat" and a b c
+ proof (cases)
+ assume "c = a"
+ hence "cycle_of_list [ a, b, c ] = id"
+ by (simp add: swap_commute)
+ thus "cycle_of_list [ a, b, c ] \<in> generate (alt_group n) (three_cycles n)"
+ using one[of "alt_group n"] unfolding alt_group_one by simp
+ next
+ assume "c \<noteq> a"
+ have "distinct [a, b, c]"
+ using \<open>a \<noteq> b\<close> and \<open>b \<noteq> c\<close> and \<open>c \<noteq> a\<close> by auto
+ with \<open>{ a, b, c } \<subseteq> {1..n}\<close>
+ show "cycle_of_list [ a, b, c ] \<in> generate (alt_group n) (three_cycles n)"
+ by (intro incl) fastforce
+ qed
- { fix S :: "nat set" and q :: "nat \<Rightarrow> nat"
- assume seq: "swapidseq_ext S (Suc (Suc 0)) q" and S: "S \<subseteq> {1..n}"
- have "q \<in> generate (alt_group n) (three_cycles n)"
- proof -
- obtain a b q' where ab: "a \<noteq> b" "a \<in> S" "b \<in> S"
- and q': "swapidseq_ext S (Suc 0) q'" "q = (transpose a b) \<circ> q'"
- using swapidseq_ext_backwards'[OF seq] by auto
- obtain c d where cd: "c \<noteq> d" "c \<in> S" "d \<in> S"
- and q: "q = (transpose a b) \<circ> (Fun.swap c d id)"
- using swapidseq_ext_backwards'[OF q'(1)]
- swapidseq_ext_zero_imp_id
- unfolding q'(2)
- by fastforce
+ have aux_lemma2: "q \<in> generate (alt_group n) (three_cycles n)"
+ if seq: "swapidseq_ext S (Suc (Suc 0)) q" and S: "S \<subseteq> {1..n}"
+ for S :: "nat set" and q :: "nat \<Rightarrow> nat"
+ proof -
+ obtain a b q' where ab: "a \<noteq> b" "a \<in> S" "b \<in> S"
+ and q': "swapidseq_ext S (Suc 0) q'" "q = (transpose a b) \<circ> q'"
+ using swapidseq_ext_backwards'[OF seq] by auto
+ obtain c d where cd: "c \<noteq> d" "c \<in> S" "d \<in> S"
+ and q: "q = (transpose a b) \<circ> (Fun.swap c d id)"
+ using swapidseq_ext_backwards'[OF q'(1)]
+ swapidseq_ext_zero_imp_id
+ unfolding q'(2)
+ by fastforce
- consider (eq) "b = c" | (ineq) "b \<noteq> c" by auto
- thus ?thesis
- proof cases
- case eq then have "q = cycle_of_list [ a, b, d ]"
- unfolding q by simp
- moreover have "{ a, b, d } \<subseteq> {1..n}"
- using ab cd S by blast
- ultimately show ?thesis
- using aux_lemma1[OF ab(1)] cd(1) eq by simp
- next
- case ineq
- hence "q = cycle_of_list [ a, b, c ] \<circ> cycle_of_list [ b, c, d ]"
- unfolding q by (simp add: swap_nilpotent o_assoc)
- moreover have "{ a, b, c } \<subseteq> {1..n}" and "{ b, c, d } \<subseteq> {1..n}"
- using ab cd S by blast+
- ultimately show ?thesis
- using eng[OF aux_lemma1[OF ab(1) ineq] aux_lemma1[OF ineq cd(1)]]
- unfolding alt_group_mult by simp
- qed
- qed } note aux_lemma2 = this
+ consider (eq) "b = c" | (ineq) "b \<noteq> c" by auto
+ thus ?thesis
+ proof cases
+ case eq
+ then have "q = cycle_of_list [ a, b, d ]"
+ unfolding q by simp
+ moreover have "{ a, b, d } \<subseteq> {1..n}"
+ using ab cd S by blast
+ ultimately show ?thesis
+ using aux_lemma1[OF ab(1)] cd(1) eq by simp
+ next
+ case ineq
+ hence "q = cycle_of_list [ a, b, c ] \<circ> cycle_of_list [ b, c, d ]"
+ unfolding q by (simp add: swap_nilpotent o_assoc)
+ moreover have "{ a, b, c } \<subseteq> {1..n}" and "{ b, c, d } \<subseteq> {1..n}"
+ using ab cd S by blast+
+ ultimately show ?thesis
+ using eng[OF aux_lemma1[OF ab(1) ineq] aux_lemma1[OF ineq cd(1)]]
+ unfolding alt_group_mult by simp
+ qed
+ qed
fix p assume "p \<in> carrier (alt_group n)" then have p: "p permutes {1..n}" "evenperm p"
unfolding alt_group_carrier by auto
@@ -464,66 +467,67 @@
show "derived (alt_group n) (carrier (alt_group n)) \<subseteq> carrier (alt_group n)"
using group.derived_in_carrier[OF alt_group_is_group] by simp
next
- { fix p assume "p \<in> three_cycles n" have "p \<in> derived (alt_group n) (carrier (alt_group n))"
- proof -
- obtain cs where cs: "p = cycle_of_list cs" "cycle cs" "length cs = 3" "set cs \<subseteq> {1..n}"
- using \<open>p \<in> three_cycles n\<close> by auto
- then obtain a b c where cs_def: "cs = [ a, b, c ]"
- using stupid_lemma[OF cs(3)] by blast
- have "card (set cs) = 3"
- using cs(2-3)
- by (simp add: distinct_card)
+ have aux_lemma: "p \<in> derived (alt_group n) (carrier (alt_group n))"
+ if "p \<in> three_cycles n" for p
+ proof -
+ obtain cs where cs: "p = cycle_of_list cs" "cycle cs" "length cs = 3" "set cs \<subseteq> {1..n}"
+ using \<open>p \<in> three_cycles n\<close> by auto
+ then obtain a b c where cs_def: "cs = [ a, b, c ]"
+ using stupid_lemma[OF cs(3)] by blast
+ have "card (set cs) = 3"
+ using cs(2-3)
+ by (simp add: distinct_card)
- have "set cs \<noteq> {1..n}"
- using assms cs(3) unfolding sym[OF distinct_card[OF cs(2)]] by auto
- then obtain d where d: "d \<notin> set cs" "d \<in> {1..n}"
- using cs(4) by blast
+ have "set cs \<noteq> {1..n}"
+ using assms cs(3) unfolding sym[OF distinct_card[OF cs(2)]] by auto
+ then obtain d where d: "d \<notin> set cs" "d \<in> {1..n}"
+ using cs(4) by blast
- hence "cycle (d # cs)" and "length (d # cs) = 4" and "card {1..n} = n"
- using cs(2-3) by auto
- hence "set (d # cs) \<noteq> {1..n}"
- using assms unfolding sym[OF distinct_card[OF \<open>cycle (d # cs)\<close>]]
- by (metis Suc_n_not_le_n eval_nat_numeral(3))
- then obtain e where e: "e \<notin> set (d # cs)" "e \<in> {1..n}"
- using d cs(4) by (metis insert_subset list.simps(15) subsetI subset_antisym)
+ hence "cycle (d # cs)" and "length (d # cs) = 4" and "card {1..n} = n"
+ using cs(2-3) by auto
+ hence "set (d # cs) \<noteq> {1..n}"
+ using assms unfolding sym[OF distinct_card[OF \<open>cycle (d # cs)\<close>]]
+ by (metis Suc_n_not_le_n eval_nat_numeral(3))
+ then obtain e where e: "e \<notin> set (d # cs)" "e \<in> {1..n}"
+ using d cs(4) by (metis insert_subset list.simps(15) subsetI subset_antisym)
- define q where "q = (Fun.swap d e id) \<circ> (Fun.swap b c id)"
- hence "bij q"
- by (simp add: bij_comp)
- moreover have "q b = c" and "q c = b"
- using d(1) e(1) unfolding q_def cs_def by simp+
- moreover have "q a = a"
- using d(1) e(1) cs(2) unfolding q_def cs_def by auto
- ultimately have "q \<circ> p \<circ> (inv' q) = cycle_of_list [ a, c, b ]"
- using conjugation_of_cycle[OF cs(2), of q]
- unfolding sym[OF cs(1)] unfolding cs_def by simp
- also have " ... = p \<circ> p"
- using cs(2) unfolding cs(1) cs_def
- by (simp add: comp_swap swap_commute transpose_comp_triple)
- finally have "q \<circ> p \<circ> (inv' q) = p \<circ> p" .
- moreover have "bij p"
- unfolding cs(1) cs_def by (simp add: bij_comp)
- ultimately have p: "q \<circ> p \<circ> (inv' q) \<circ> (inv' p) = p"
- by (simp add: bijection.intro bijection.inv_comp_right comp_assoc)
+ define q where "q = (Fun.swap d e id) \<circ> (Fun.swap b c id)"
+ hence "bij q"
+ by (simp add: bij_comp)
+ moreover have "q b = c" and "q c = b"
+ using d(1) e(1) unfolding q_def cs_def by simp+
+ moreover have "q a = a"
+ using d(1) e(1) cs(2) unfolding q_def cs_def by auto
+ ultimately have "q \<circ> p \<circ> (inv' q) = cycle_of_list [ a, c, b ]"
+ using conjugation_of_cycle[OF cs(2), of q]
+ unfolding sym[OF cs(1)] unfolding cs_def by simp
+ also have " ... = p \<circ> p"
+ using cs(2) unfolding cs(1) cs_def
+ by (simp add: comp_swap swap_commute transpose_comp_triple)
+ finally have "q \<circ> p \<circ> (inv' q) = p \<circ> p" .
+ moreover have "bij p"
+ unfolding cs(1) cs_def by (simp add: bij_comp)
+ ultimately have p: "q \<circ> p \<circ> (inv' q) \<circ> (inv' p) = p"
+ by (simp add: bijection.intro bijection.inv_comp_right comp_assoc)
- have "swapidseq (Suc (Suc 0)) q"
- using comp_Suc[OF comp_Suc[OF id], of b c d e] e(1) cs(2) unfolding q_def cs_def by auto
- hence "evenperm q"
- using even_Suc_Suc_iff evenperm_unique by blast
- moreover have "q permutes { d, e, b, c }"
- unfolding q_def by (simp add: permutes_compose permutes_swap_id)
- hence "q permutes {1..n}"
- using cs(4) d(2) e(2) permutes_subset unfolding cs_def by fastforce
- ultimately have "q \<in> carrier (alt_group n)"
- unfolding alt_group_carrier by simp
- moreover have "p \<in> carrier (alt_group n)"
- using \<open>p \<in> three_cycles n\<close> three_cycles_incl by blast
- ultimately have "p \<in> derived_set (alt_group n) (carrier (alt_group n))"
- using p alt_group_inv_equality unfolding alt_group_mult
- by (metis (no_types, lifting) UN_iff singletonI)
- thus "p \<in> derived (alt_group n) (carrier (alt_group n))"
- unfolding derived_def by (rule incl)
- qed } note aux_lemma = this
+ have "swapidseq (Suc (Suc 0)) q"
+ using comp_Suc[OF comp_Suc[OF id], of b c d e] e(1) cs(2) unfolding q_def cs_def by auto
+ hence "evenperm q"
+ using even_Suc_Suc_iff evenperm_unique by blast
+ moreover have "q permutes { d, e, b, c }"
+ unfolding q_def by (simp add: permutes_compose permutes_swap_id)
+ hence "q permutes {1..n}"
+ using cs(4) d(2) e(2) permutes_subset unfolding cs_def by fastforce
+ ultimately have "q \<in> carrier (alt_group n)"
+ unfolding alt_group_carrier by simp
+ moreover have "p \<in> carrier (alt_group n)"
+ using \<open>p \<in> three_cycles n\<close> three_cycles_incl by blast
+ ultimately have "p \<in> derived_set (alt_group n) (carrier (alt_group n))"
+ using p alt_group_inv_equality unfolding alt_group_mult
+ by (metis (no_types, lifting) UN_iff singletonI)
+ thus "p \<in> derived (alt_group n) (carrier (alt_group n))"
+ unfolding derived_def by (rule incl)
+ qed
interpret A: group "alt_group n"
using alt_group_is_group .
--- a/src/HOL/Algebra/UnivPoly.thy Wed Nov 13 15:14:48 2024 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy Wed Nov 13 20:10:34 2024 +0100
@@ -408,20 +408,16 @@
assumes R1: "p \<in> carrier P" and R2: "q \<in> carrier P" shows "p \<otimes>\<^bsub>P\<^esub> q = q \<otimes>\<^bsub>P\<^esub> p"
proof (rule up_eqI)
fix n
- {
- fix k and a b :: "nat=>'a"
- assume R: "a \<in> UNIV \<rightarrow> carrier R" "b \<in> UNIV \<rightarrow> carrier R"
- then have "k <= n ==>
- (\<Oplus>i \<in> {..k}. a i \<otimes> b (n-i)) = (\<Oplus>i \<in> {..k}. a (k-i) \<otimes> b (i+n-k))"
- (is "_ \<Longrightarrow> ?eq k")
- proof (induct k)
- case 0 then show ?case by (simp add: Pi_def)
- next
- case (Suc k) then show ?case
- by (subst (2) finsum_Suc2) (simp add: Pi_def a_comm)+
- qed
- }
- note l = this
+ have l: "(\<Oplus>i \<in> {..k}. a i \<otimes> b (n-i)) = (\<Oplus>i \<in> {..k}. a (k-i) \<otimes> b (i+n-k))" (is "?eq k")
+ if "a \<in> UNIV \<rightarrow> carrier R" "b \<in> UNIV \<rightarrow> carrier R" and "k <= n"
+ for k and a b :: "nat=>'a"
+ using that
+ proof (induct k)
+ case 0 then show ?case by (simp add: Pi_def)
+ next
+ case (Suc k) then show ?case
+ by (subst (2) finsum_Suc2) (simp add: Pi_def a_comm)+
+ qed
from R1 R2 show "coeff P (p \<otimes>\<^bsub>P\<^esub> q) n = coeff P (q \<otimes>\<^bsub>P\<^esub> p) n"
unfolding coeff_mult [OF R1 R2, of n]
unfolding coeff_mult [OF R2 R1, of n]