Theory Supplementary_Ring_Facts

theory Supplementary_Ring_Facts
imports "HOL-Algebra.Ring" 
        "HOL-Algebra.UnivPoly"
        "HOL-Algebra.Subrings"

begin

section‹Supplementary Ring Facts›

text‹The nonzero elements of a ring.›

definition nonzero :: "('a, 'b) ring_scheme ⇒ 'a set" where
"nonzero R = {a ∈ carrier R. a ≠ 𝟬⇘R⇙}"


lemma zero_not_in_nonzero:
"𝟬⇘R⇙ ∉ nonzero R"
  unfolding nonzero_def by blast 

lemma(in domain) nonzero_memI:
  assumes "a ∈ carrier R"
  assumes "a ≠ 𝟬"
  shows "a ∈ nonzero R"
  using assms by(simp add: nonzero_def)

lemma(in domain) nonzero_memE:
  assumes "a ∈ nonzero R"
  shows "a ∈ carrier R" "a ≠𝟬"
  using assms by(auto simp: nonzero_def)

lemma(in domain) not_nonzero_memE:
  assumes "a ∉ nonzero R"
  assumes "a ∈ carrier R"
  shows "a = 𝟬"
  using assms 
  by (simp add: nonzero_def)

lemma(in domain) not_nonzero_memI:
  assumes "a = 𝟬"
  shows "a ∉ nonzero R"
  using assms nonzero_memE(2) by auto

lemma(in domain) nonzero_closed:
  assumes "a ∈ nonzero R"
  shows "a ∈ carrier R"
  using assms 
  by (simp add: nonzero_def)

lemma(in domain) nonzero_mult_in_car:
  assumes "a ∈ nonzero R"
  assumes "b ∈ nonzero R"
  shows "a ⊗ b ∈ carrier R"
  using assms 
  by (simp add: nonzero_def)

lemma(in domain) nonzero_mult_closed:
  assumes "a ∈ nonzero R"
  assumes "b ∈ nonzero R"
  shows "a ⊗ b ∈ nonzero R"
  apply(rule nonzero_memI)
  using assms nonzero_memE apply blast
    using assms nonzero_memE 
    by (simp add: integral_iff)    

lemma(in domain) nonzero_one_closed:
"𝟭 ∈ nonzero R"
  by (simp add: nonzero_def)

lemma(in domain) one_nonzero:
"𝟭 ∈ nonzero R"
  by (simp add: nonzero_one_closed)

lemma(in domain) nat_pow_nonzero:
  assumes "x ∈nonzero R"
  shows "x[^](n::nat) ∈ nonzero R"
  unfolding nonzero_def 
  apply(induction n)
  using assms integral_iff nonzero_closed zero_not_in_nonzero by auto

lemma(in monoid) Units_int_pow_closed:
  assumes "x ∈ Units G"
  shows "x[^](n::int) ∈ Units G"
  by (metis Units_pow_closed assms int_pow_def2 monoid.Units_inv_Units monoid_axioms)

lemma(in comm_monoid) UnitsI:
  assumes "a ∈ carrier G"
  assumes "b ∈ carrier G"
  assumes "a ⊗ b = 𝟭"
  shows "a ∈ Units G" "b ∈ Units G" 
  unfolding Units_def using comm_monoid_axioms_def assms m_comm[of a b] 
  by auto 

lemma(in comm_monoid) is_invI:
  assumes "a ∈ carrier G"
  assumes "b ∈ carrier G"
  assumes "a ⊗ b = 𝟭"
  shows "inv⇘G⇙ b = a" "inv⇘G⇙ a = b"
  using assms inv_char m_comm 
  by auto

lemma(in ring) ring_in_Units_imp_not_zero:
  assumes "𝟭 ≠ 𝟬"
  assumes "a ∈ Units R"
  shows "a ≠ 𝟬"
  using assms monoid.Units_l_cancel
  by (metis l_null  monoid_axioms one_closed zero_closed)

lemma(in ring) Units_nonzero:
  assumes "u ∈ Units R"
  assumes "𝟭⇘R⇙ ≠ 𝟬⇘R⇙"
  shows "u ∈ nonzero R"
proof-
  have "u ∈carrier R" 
    using Units_closed assms by auto
  have "u ≠𝟬" 
    using Units_r_inv_ex assms(1) assms(2) 
    by force 
  thus ?thesis 
    by (simp add: ‹u ∈ carrier R› nonzero_def)
qed


lemma(in ring) Units_inverse:
  assumes "u ∈ Units R"
  shows "inv u ∈ Units R"
  by (simp add: assms)

lemma(in cring) invI:  
  assumes "x ∈ carrier R"
  assumes "y ∈ carrier R"
  assumes "x ⊗⇘R⇙ y = 𝟭⇘R⇙"
  shows "y = inv ⇘R⇙ x"
        "x = inv ⇘R⇙ y"
  using assms(1) assms(2) assms(3) is_invI 
  by auto 

lemma(in cring) inv_cancelR:
  assumes "x ∈ Units R"
  assumes "y ∈ carrier R"
  assumes "z ∈ carrier R"
  assumes "y = x ⊗⇘R⇙ z"
  shows "inv⇘R⇙ x ⊗⇘R⇙ y = z"
        "y ⊗⇘R⇙ (inv⇘R⇙ x)  = z"
  apply (metis Units_closed assms(1) assms(3) assms(4) cring.cring_simprules(12) 
    is_cring m_assoc monoid.Units_inv_closed monoid.Units_l_inv monoid_axioms)
  by (metis Units_closed assms(1) assms(3) assms(4) m_assoc m_comm monoid.Units_inv_closed 
      monoid.Units_r_inv monoid.r_one monoid_axioms)
   
lemma(in cring) inv_cancelL:
  assumes "x ∈ Units R"
  assumes "y ∈ carrier R"
  assumes "z ∈ carrier R"
  assumes "y = z ⊗⇘R⇙ x"
  shows "inv⇘R⇙ x ⊗⇘R⇙ y = z"
        "y ⊗⇘R⇙ (inv⇘R⇙ x)  = z"
  apply (simp add: Units_closed assms(1) assms(3) assms(4) m_lcomm)
  by (simp add: Units_closed assms(1) assms(3) assms(4) m_assoc)


end