# Theory Generated_Rings

```(* ************************************************************************** *)
(* Title:      Generated_Rings.thy                                            *)
(* Author:     Martin Baillon                                                 *)
(* ************************************************************************** *)

theory Generated_Rings
imports Subrings
begin

sectionβΉGenerated RingsβΊ

inductive_set
generate_ring :: "('a, 'b) ring_scheme β 'a set β 'a set"
for R and H where
one:   "π­βRβ β generate_ring R H"
| incl:  "h β H βΉ h β generate_ring R H"
| a_inv: "h β generate_ring R H βΉ ββRβ h β generate_ring R H"
| eng_add : "β¦ h1 β generate_ring R H; h2 β generate_ring R H β§ βΉ h1 ββRβ h2 β generate_ring R H"
| eng_mult: "β¦ h1 β generate_ring R H; h2 β generate_ring R H β§ βΉ h1 ββRβ h2 β generate_ring R H"

subsectionβΉBasic Properties of Generated Rings - First PartβΊ

lemma (in ring) generate_ring_in_carrier:
assumes "H β carrier R"
shows "h β generate_ring R H βΉ h β carrier R"
apply (induction rule: generate_ring.induct) using assms
by blast+

lemma (in ring) generate_ring_incl:
assumes "H β carrier R"
shows "generate_ring R H β carrier R"
using generate_ring_in_carrier[OF assms] by auto

lemma (in ring) zero_in_generate: "π¬βRβ β generate_ring R H"
using one a_inv by (metis generate_ring.eng_add one_closed r_neg)

lemma (in ring) generate_ring_is_subring:
assumes "H β carrier R"
shows "subring (generate_ring R H) R"
by (auto intro!: subringI[of "generate_ring R H"]

lemma (in ring) generate_ring_is_ring:
assumes "H β carrier R"
shows "ring (R β¦ carrier := generate_ring R H β¦)"
using subring_iff[OF generate_ring_incl[OF assms]] generate_ring_is_subring[OF assms] by simp

lemma (in ring) generate_ring_min_subring1:
assumes "H β carrier R" and "subring E R" "H β E"
shows "generate_ring R H β E"
proof
fix h assume h: "h β generate_ring R H"
show "h β E"
using h and assms(3)
by (induct rule: generate_ring.induct)
qed

lemma (in ring) generate_ringI:
assumes "H β carrier R"
and "subring E R" "H β E"
and "βK. β¦ subring K R; H β K β§ βΉ E β K"
shows "E = generate_ring R H"
proof
show "E β generate_ring R H"
using assms generate_ring_is_subring generate_ring.incl by (metis subset_iff)
show "generate_ring R H β E"
using generate_ring_min_subring1[OF assms(1-3)] by simp
qed

lemma (in ring) generate_ringE:
assumes "H β carrier R" and "E = generate_ring R H"
shows "subring E R" and "H β E" and "βK. β¦ subring K R; H β K β§ βΉ E β K"
proof -
show "subring E R" using assms generate_ring_is_subring by simp
show "H β E" using assms(2) by (simp add: generate_ring.incl subsetI)
show "βK. subring K R  βΉ H β K βΉ E β K"
using assms generate_ring_min_subring1 by auto
qed

lemma (in ring) generate_ring_min_subring2:
assumes "H β carrier R"
shows "generate_ring R H = β{K. subring K R β§ H β K}"
proof
have "subring (generate_ring R H) R β§ H β generate_ring R H"
by (simp add: assms generate_ringE(2) generate_ring_is_subring)
thus "β{K. subring K R β§ H β K} β generate_ring R H" by blast
next
have "βK. subring K R β§ H β K βΉ generate_ring R H β K"
thus "generate_ring R H β β{K. subring K R β§ H β K}" by blast
qed

lemma (in ring) mono_generate_ring:
assumes "I β J" and "J β carrier R"
shows "generate_ring R I β generate_ring R J"
proof-
have "I β generate_ring R J "
using assms generate_ringE(2) by blast
thus "generate_ring R I β generate_ring R J"
using generate_ring_min_subring1[of I "generate_ring R J"] assms generate_ring_is_subring[OF assms(2)]
by blast
qed

lemma (in ring) subring_gen_incl :
assumes "subring H R"
and  "subring K R"
and "I β H"
and "I β K"
shows "generate_ring (Rβ¦carrier := Kβ¦) I β generate_ring (Rβ¦carrier := Hβ¦) I"
proof
{fix J assume J_def : "subring J R" "I β J"
have "generate_ring (R β¦ carrier := J β¦) I β J"
using ring.mono_generate_ring[of "(Rβ¦carrier := Jβ¦)" I J ] subring_is_ring[OF J_def(1)]
ring.generate_ring_in_carrier[of "Rβ¦carrier := Jβ¦"]  ring_axioms J_def(2)
by auto}
note incl_HK = this
{fix x have "x β generate_ring (Rβ¦carrier := Kβ¦) I βΉ x β generate_ring (Rβ¦carrier := Hβ¦) I"
proof (induction  rule : generate_ring.induct)
case one
have "π­βRβ¦carrier := Hβ¦β β π­βRβ¦carrier := Kβ¦β = π­βRβ¦carrier := Hβ¦β" by simp
moreover have "π­βRβ¦carrier := Hβ¦β β π­βRβ¦carrier := Kβ¦β = π­βRβ¦carrier := Kβ¦β" 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β¦carrier := Kβ¦) 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β¦carrier := Hβ¦) 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
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. x β generate_ring (Rβ¦carrier := Kβ¦) I βΉ x β generate_ring (Rβ¦carrier := Hβ¦) I"
by auto
qed

lemma (in ring) subring_gen_equality:
assumes "subring H R" "K β H"
shows "generate_ring R K = generate_ring (R β¦ carrier := H β¦) K"
using subring_gen_incl[OF assms(1)carrier_is_subring assms(2)] assms subringE(1)
subring_gen_incl[OF carrier_is_subring assms(1) _ assms(2)]
by force

end
```