--- 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