Theory More_Ring

(*  Title:      HOL/Algebra/More_Ring.thy
    Author:     Jeremy Avigad
*)

section ‹More on rings etc.›

theory More_Ring
imports
  Ring
begin

lemma (in cring) field_intro2: "𝟬⇘R⇙ ~= 𝟭⇘R⇙ ⟹ ∀x ∈ carrier R - {𝟬⇘R⇙}. x ∈ Units R ⟹ field R"
  apply (unfold_locales)
  apply (insert cring_axioms, auto)
  apply (rule trans)
  apply (subgoal_tac "a = (a ⊗ b) ⊗ inv b")
  apply assumption
  apply (subst m_assoc)
  apply auto
  apply (unfold Units_def)
  apply auto
  done

lemma (in monoid) inv_char: "x : carrier G ⟹ y : carrier G ⟹
    x ⊗ y = 𝟭 ⟹ y ⊗ x = 𝟭 ⟹ inv x = y"
  apply (subgoal_tac "x : Units G")
  apply (subgoal_tac "y = inv x ⊗ 𝟭")
  apply simp
  apply (erule subst)
  apply (subst m_assoc [symmetric])
  apply auto
  apply (unfold Units_def)
  apply auto
  done

lemma (in comm_monoid) comm_inv_char: "x : carrier G ⟹ y : carrier G ⟹
  x ⊗ y = 𝟭 ⟹ inv x = y"
  apply (rule inv_char)
  apply auto
  apply (subst m_comm, auto)
  done

lemma (in ring) inv_neg_one [simp]: "inv (⊖ 𝟭) = ⊖ 𝟭"
  apply (rule inv_char)
  apply (auto simp add: l_minus r_minus)
  done

lemma (in monoid) inv_eq_imp_eq: "x : Units G ⟹ y : Units G ⟹
    inv x = inv y ⟹ x = y"
  apply (subgoal_tac "inv(inv x) = inv(inv y)")
  apply (subst (asm) Units_inv_inv)+
  apply auto
  done

lemma (in ring) Units_minus_one_closed [intro]: "⊖ 𝟭 : Units R"
  apply (unfold Units_def)
  apply auto
  apply (rule_tac x = "⊖ 𝟭" in bexI)
  apply auto
  apply (simp add: l_minus r_minus)
  done

lemma (in monoid) inv_one [simp]: "inv 𝟭 = 𝟭"
  apply (rule inv_char)
  apply auto
  done

lemma (in ring) inv_eq_neg_one_eq: "x : Units R ⟹ (inv x = ⊖ 𝟭) = (x = ⊖ 𝟭)"
  apply auto
  apply (subst Units_inv_inv [symmetric])
  apply auto
  done

lemma (in monoid) inv_eq_one_eq: "x : Units G ⟹ (inv x = 𝟭) = (x = 𝟭)"
  by (metis Units_inv_inv inv_one)

end