section ‹Things that can be added to the Algebra library›
theory Algebra_Aux
imports "HOL-Algebra.Ring"
begin
definition of_natural :: "('a, 'm) ring_scheme ⇒ nat ⇒ 'a" ("«_»⇩ℕı") where
"«n»⇩ℕ⇘R⇙ = (op ⊕⇘R⇙ 𝟭⇘R⇙ ^^ n) 𝟬⇘R⇙"
definition of_integer :: "('a, 'm) ring_scheme ⇒ int ⇒ 'a" ("«_»ı") where
"«i»⇘R⇙ = (if 0 ≤ i then «nat i»⇩ℕ⇘R⇙ else ⊖⇘R⇙ «nat (- i)»⇩ℕ⇘R⇙)"
context ring begin
lemma of_nat_0 [simp]: "«0»⇩ℕ = 𝟬"
by (simp add: of_natural_def)
lemma of_nat_Suc [simp]: "«Suc n»⇩ℕ = 𝟭 ⊕ «n»⇩ℕ"
by (simp add: of_natural_def)
lemma of_int_0 [simp]: "«0» = 𝟬"
by (simp add: of_integer_def)
lemma of_nat_closed [simp]: "«n»⇩ℕ ∈ carrier R"
by (induct n) simp_all
lemma of_int_closed [simp]: "«i» ∈ carrier R"
by (simp add: of_integer_def)
lemma of_int_minus [simp]: "«- i» = ⊖ «i»"
by (simp add: of_integer_def)
lemma of_nat_add [simp]: "«m + n»⇩ℕ = «m»⇩ℕ ⊕ «n»⇩ℕ"
by (induct m) (simp_all add: a_ac)
lemma of_nat_diff [simp]: "n ≤ m ⟹ «m - n»⇩ℕ = «m»⇩ℕ ⊖ «n»⇩ℕ"
proof (induct m arbitrary: n)
case (Suc m)
note Suc' = this
show ?case
proof (cases n)
case (Suc k)
with Suc' have "«Suc m - Suc k»⇩ℕ = «m»⇩ℕ ⊖ «k»⇩ℕ" by simp
also have "… = 𝟭 ⊕ ⊖ 𝟭 ⊕ («m»⇩ℕ ⊖ «k»⇩ℕ)"
by (simp add: r_neg)
also have "… = «Suc m»⇩ℕ ⊖ «Suc k»⇩ℕ"
by (simp add: minus_eq minus_add a_ac)
finally show ?thesis using Suc by simp
qed (simp add: minus_eq)
qed (simp add: minus_eq)
lemma of_int_add [simp]: "«i + j» = «i» ⊕ «j»"
proof (cases "0 ≤ i")
case True
show ?thesis
proof (cases "0 ≤ j")
case True
with ‹0 ≤ i› show ?thesis by (simp add: of_integer_def nat_add_distrib)
next
case False
show ?thesis
proof (cases "0 ≤ i + j")
case True
then have "«i + j» = «nat (i - (- j))»⇩ℕ"
by (simp add: of_integer_def)
also from True ‹0 ≤ i› ‹¬ 0 ≤ j›
have "nat (i - (- j)) = nat i - nat (- j)"
by (simp add: nat_diff_distrib)
finally show ?thesis using True ‹0 ≤ i› ‹¬ 0 ≤ j›
by (simp add: minus_eq of_integer_def)
next
case False
then have "«i + j» = ⊖ «nat (- j - i)»⇩ℕ"
by (simp add: of_integer_def) (simp only: diff_conv_add_uminus add_ac)
also from False ‹0 ≤ i› ‹¬ 0 ≤ j›
have "nat (- j - i) = nat (- j) - nat i"
by (simp add: nat_diff_distrib)
finally show ?thesis using False ‹0 ≤ i› ‹¬ 0 ≤ j›
by (simp add: minus_eq minus_add a_ac of_integer_def)
qed
qed
next
case False
show ?thesis
proof (cases "0 ≤ j")
case True
show ?thesis
proof (cases "0 ≤ i + j")
case True
then have "«i + j» = «nat (j - (- i))»⇩ℕ"
by (simp add: of_integer_def add_ac)
also from True ‹¬ 0 ≤ i› ‹0 ≤ j›
have "nat (j - (- i)) = nat j - nat (- i)"
by (simp add: nat_diff_distrib)
finally show ?thesis using True ‹¬ 0 ≤ i› ‹0 ≤ j›
by (simp add: minus_eq minus_add a_ac of_integer_def)
next
case False
then have "«i + j» = ⊖ «nat (- i - j)»⇩ℕ"
by (simp add: of_integer_def)
also from False ‹¬ 0 ≤ i› ‹0 ≤ j›
have "nat (- i - j) = nat (- i) - nat j"
by (simp add: nat_diff_distrib)
finally show ?thesis using False ‹¬ 0 ≤ i› ‹0 ≤ j›
by (simp add: minus_eq minus_add of_integer_def)
qed
next
case False
with ‹¬ 0 ≤ i› show ?thesis
by (simp add: of_integer_def nat_add_distrib minus_add diff_conv_add_uminus
del: add_uminus_conv_diff uminus_add_conv_diff)
qed
qed
lemma of_int_diff [simp]: "«i - j» = «i» ⊖ «j»"
by (simp only: diff_conv_add_uminus of_int_add) (simp add: minus_eq)
lemma of_nat_mult [simp]: "«i * j»⇩ℕ = «i»⇩ℕ ⊗ «j»⇩ℕ"
by (induct i) (simp_all add: l_distr)
lemma of_int_mult [simp]: "«i * j» = «i» ⊗ «j»"
proof (cases "0 ≤ i")
case True
show ?thesis
proof (cases "0 ≤ j")
case True
with ‹0 ≤ i› show ?thesis
by (simp add: of_integer_def nat_mult_distrib zero_le_mult_iff)
next
case False
with ‹0 ≤ i› show ?thesis
by (simp add: of_integer_def zero_le_mult_iff
minus_mult_right nat_mult_distrib r_minus
del: minus_mult_right [symmetric])
qed
next
case False
show ?thesis
proof (cases "0 ≤ j")
case True
with ‹¬ 0 ≤ i› show ?thesis
by (simp add: of_integer_def zero_le_mult_iff
minus_mult_left nat_mult_distrib l_minus
del: minus_mult_left [symmetric])
next
case False
with ‹¬ 0 ≤ i› show ?thesis
by (simp add: of_integer_def zero_le_mult_iff
minus_mult_minus [of i j, symmetric] nat_mult_distrib
l_minus r_minus
del: minus_mult_minus
minus_mult_left [symmetric] minus_mult_right [symmetric])
qed
qed
lemma of_int_1 [simp]: "«1» = 𝟭"
by (simp add: of_integer_def)
lemma of_int_2: "«2» = 𝟭 ⊕ 𝟭"
by (simp add: of_integer_def numeral_2_eq_2)
lemma minus_0_r [simp]: "x ∈ carrier R ⟹ x ⊖ 𝟬 = x"
by (simp add: minus_eq)
lemma minus_0_l [simp]: "x ∈ carrier R ⟹ 𝟬 ⊖ x = ⊖ x"
by (simp add: minus_eq)
lemma eq_diff0:
assumes "x ∈ carrier R" "y ∈ carrier R"
shows "(x ⊖ y = 𝟬) = (x = y)"
proof
assume "x ⊖ y = 𝟬"
with assms have "x ⊕ (⊖ y ⊕ y) = y"
by (simp add: minus_eq a_assoc [symmetric])
with assms show "x = y" by (simp add: l_neg)
next
assume "x = y"
with assms show "x ⊖ y = 𝟬" by (simp add: minus_eq r_neg)
qed
lemma power2_eq_square: "x ∈ carrier R ⟹ x (^) (2::nat) = x ⊗ x"
by (simp add: numeral_eq_Suc)
lemma eq_neg_iff_add_eq_0:
assumes "x ∈ carrier R" "y ∈ carrier R"
shows "(x = ⊖ y) = (x ⊕ y = 𝟬)"
proof
assume "x = ⊖ y"
with assms show "x ⊕ y = 𝟬" by (simp add: l_neg)
next
assume "x ⊕ y = 𝟬"
with assms have "x ⊕ (y ⊕ ⊖ y) = 𝟬 ⊕ ⊖ y"
by (simp add: a_assoc [symmetric])
with assms show "x = ⊖ y"
by (simp add: r_neg)
qed
lemma neg_equal_iff_equal:
assumes x: "x ∈ carrier R" and y: "y ∈ carrier R"
shows "(⊖ x = ⊖ y) = (x = y)"
proof
assume "⊖ x = ⊖ y"
then have "⊖ (⊖ x) = ⊖ (⊖ y)" by simp
with x y show "x = y" by simp
next
assume "x = y"
then show "⊖ x = ⊖ y" by simp
qed
lemma neg_equal_swap:
assumes x: "x ∈ carrier R" and y: "y ∈ carrier R"
shows "(⊖ x = y) = (x = ⊖ y)"
using assms neg_equal_iff_equal [of x "⊖ y"]
by simp
lemma mult2: "x ∈ carrier R ⟹ x ⊕ x = «2» ⊗ x"
by (simp add: of_int_2 l_distr)
end
lemma (in cring) of_int_power [simp]: "«i ^ n» = «i» (^) n"
by (induct n) (simp_all add: m_ac)
definition cring_class_ops :: "'a::comm_ring_1 ring" where
"cring_class_ops ≡ ⦇carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +⦈"
lemma cring_class: "cring cring_class_ops"
apply unfold_locales
apply (auto simp add: cring_class_ops_def ring_distribs Units_def)
apply (rule_tac x="- x" in exI)
apply simp
done
lemma carrier_class: "x ∈ carrier cring_class_ops"
by (simp add: cring_class_ops_def)
lemma zero_class: "𝟬⇘cring_class_ops⇙ = 0"
by (simp add: cring_class_ops_def)
lemma one_class: "𝟭⇘cring_class_ops⇙ = 1"
by (simp add: cring_class_ops_def)
lemma plus_class: "x ⊕⇘cring_class_ops⇙ y = x + y"
by (simp add: cring_class_ops_def)
lemma times_class: "x ⊗⇘cring_class_ops⇙ y = x * y"
by (simp add: cring_class_ops_def)
lemma uminus_class: "⊖⇘cring_class_ops⇙ x = - x"
apply (simp add: a_inv_def m_inv_def cring_class_ops_def)
apply (rule the_equality)
apply (simp_all add: eq_neg_iff_add_eq_0)
done
lemma minus_class: "x ⊖⇘cring_class_ops⇙ y = x - y"
by (simp add: a_minus_def carrier_class plus_class uminus_class)
lemma power_class: "x (^)⇘cring_class_ops⇙ n = x ^ n"
by (induct n) (simp_all add: one_class times_class
monoid.nat_pow_0 [OF comm_monoid.axioms(1) [OF cring.axioms(2) [OF cring_class]]]
monoid.nat_pow_Suc [OF comm_monoid.axioms(1) [OF cring.axioms(2) [OF cring_class]]])
lemma of_nat_class: "«n»⇩ℕ⇘cring_class_ops⇙ = of_nat n"
by (induct n) (simp_all add: cring_class_ops_def of_natural_def)
lemma of_int_class: "«i»⇘cring_class_ops⇙ = of_int i"
by (simp add: of_integer_def of_nat_class uminus_class)
lemmas class_simps = zero_class one_class plus_class minus_class uminus_class
times_class power_class of_nat_class of_int_class carrier_class
interpretation cring_class: cring "cring_class_ops::'a::comm_ring_1 ring"
rewrites
"(𝟬⇘cring_class_ops⇙::'a) = 0" and
"(𝟭⇘cring_class_ops⇙::'a) = 1" and
"(x::'a) ⊕⇘cring_class_ops⇙ y = x + y" and
"(x::'a) ⊗⇘cring_class_ops⇙ y = x * y" and
"⊖⇘cring_class_ops⇙ (x::'a) = - x" and
"(x::'a) ⊖⇘cring_class_ops⇙ y = x - y" and
"(x::'a) (^)⇘cring_class_ops⇙ n = x ^ n" and
"«n»⇩ℕ⇘cring_class_ops⇙ = of_nat n" and
"((«i»⇘cring_class_ops⇙)::'a) = of_int i" and
"(Int.of_int (numeral m)::'a) = numeral m"
by (simp_all add: cring_class class_simps)
lemma (in domain) nat_pow_eq_0_iff [simp]:
"a ∈ carrier R ⟹ (a (^) (n::nat) = 𝟬) = (a = 𝟬 ∧ n ≠ 0)"
by (induct n) (auto simp add: integral_iff)
lemma (in domain) square_eq_iff:
assumes "x ∈ carrier R" "y ∈ carrier R"
shows "(x ⊗ x = y ⊗ y) = (x = y ∨ x = ⊖ y)"
proof
assume "x ⊗ x = y ⊗ y"
with assms have "(x ⊖ y) ⊗ (x ⊕ y) = x ⊗ y ⊕ ⊖ (x ⊗ y) ⊕ (y ⊗ y ⊕ ⊖ (y ⊗ y))"
by (simp add: r_distr l_distr minus_eq r_minus m_comm a_ac)
with assms show "x = y ∨ x = ⊖ y"
by (simp add: integral_iff eq_neg_iff_add_eq_0 eq_diff0 r_neg)
next
assume "x = y ∨ x = ⊖ y"
with assms show "x ⊗ x = y ⊗ y" by (auto simp add: l_minus r_minus)
qed
definition
m_div :: "('a, 'b) ring_scheme ⇒ 'a ⇒ 'a ⇒ 'a" (infixl "⊘ı" 70) where
"x ⊘⇘G⇙ y = (if y = 𝟬⇘G⇙ then 𝟬⇘G⇙ else x ⊗⇘G⇙ inv⇘G⇙ y)"
context field
begin
lemma inv_closed [simp]: "x ∈ carrier R ⟹ x ≠ 𝟬 ⟹ inv x ∈ carrier R"
by (simp add: field_Units)
lemma l_inv [simp]: "x ∈ carrier R ⟹ x ≠ 𝟬 ⟹ inv x ⊗ x = 𝟭"
by (simp add: field_Units)
lemma r_inv [simp]: "x ∈ carrier R ⟹ x ≠ 𝟬 ⟹ x ⊗ inv x = 𝟭"
by (simp add: field_Units)
lemma inverse_unique:
assumes a: "a ∈ carrier R"
and b: "b ∈ carrier R"
and ab: "a ⊗ b = 𝟭"
shows "inv a = b"
proof -
have "a ≠ 𝟬" using ab b by (cases "a = 𝟬") simp_all
moreover with a have "inv a ⊗ (a ⊗ b) = inv a" by (simp add: ab)
ultimately show ?thesis using a b by (simp add: m_assoc [symmetric])
qed
lemma nonzero_inverse_inverse_eq:
"a ∈ carrier R ⟹ a ≠ 𝟬 ⟹ inv (inv a) = a"
by (rule inverse_unique) simp_all
lemma inv_1 [simp]: "inv 𝟭 = 𝟭"
by (rule inverse_unique) simp_all
lemma nonzero_inverse_mult_distrib:
assumes "a ∈ carrier R" and "b ∈ carrier R" and "a ≠ 𝟬" and "b ≠ 𝟬"
shows "inv (a ⊗ b) = inv b ⊗ inv a"
proof -
have "a ⊗ (b ⊗ inv b) ⊗ inv a = 𝟭" using assms by simp
hence eq: "a ⊗ b ⊗ (inv b ⊗ inv a) = 𝟭" using assms
by (simp only: m_assoc m_closed inv_closed assms)
from inverse_unique [OF _ _ eq] assms
show ?thesis by simp
qed
lemma nonzero_imp_inverse_nonzero:
assumes "a ∈ carrier R" and "a ≠ 𝟬"
shows "inv a ≠ 𝟬"
proof
assume ianz: "inv a = 𝟬"
from assms
have "𝟭 = a ⊗ inv a" by simp
also with assms have "... = 𝟬" by (simp add: ianz)
finally have "𝟭 = 𝟬" .
thus False by (simp add: eq_commute)
qed
lemma nonzero_divide_divide_eq_left:
"a ∈ carrier R ⟹ b ∈ carrier R ⟹ c ∈ carrier R ⟹ b ≠ 𝟬 ⟹ c ≠ 𝟬 ⟹
a ⊘ b ⊘ c = a ⊘ (b ⊗ c)"
by (simp add: m_div_def nonzero_inverse_mult_distrib m_ac integral_iff)
lemma nonzero_times_divide_eq:
"a ∈ carrier R ⟹ b ∈ carrier R ⟹ c ∈ carrier R ⟹ d ∈ carrier R ⟹
b ≠ 𝟬 ⟹ d ≠ 𝟬 ⟹ (a ⊘ b) ⊗ (c ⊘ d) = (a ⊗ c) ⊘ (b ⊗ d)"
by (simp add: m_div_def nonzero_inverse_mult_distrib m_ac integral_iff)
lemma nonzero_divide_divide_eq:
"a ∈ carrier R ⟹ b ∈ carrier R ⟹ c ∈ carrier R ⟹ d ∈ carrier R ⟹
b ≠ 𝟬 ⟹ c ≠ 𝟬 ⟹ d ≠ 𝟬 ⟹ (a ⊘ b) ⊘ (c ⊘ d) = (a ⊗ d) ⊘ (b ⊗ c)"
by (simp add: m_div_def nonzero_inverse_mult_distrib
nonzero_imp_inverse_nonzero nonzero_inverse_inverse_eq m_ac integral_iff)
lemma divide_1 [simp]: "x ∈ carrier R ⟹ x ⊘ 𝟭 = x"
by (simp add: m_div_def)
lemma add_frac_eq:
assumes "x ∈ carrier R" and "y ∈ carrier R" and "z ∈ carrier R" and "w ∈ carrier R"
and "y ≠ 𝟬" and "z ≠ 𝟬"
shows "x ⊘ y ⊕ w ⊘ z = (x ⊗ z ⊕ w ⊗ y) ⊘ (y ⊗ z)"
proof -
from assms
have "x ⊘ y ⊕ w ⊘ z = x ⊗ inv y ⊗ (z ⊗ inv z) ⊕ w ⊗ inv z ⊗ (y ⊗ inv y)"
by (simp add: m_div_def)
also from assms have "… = (x ⊗ z ⊕ w ⊗ y) ⊘ (y ⊗ z)"
by (simp add: m_div_def nonzero_inverse_mult_distrib r_distr m_ac integral_iff del: r_inv)
finally show ?thesis .
qed
lemma div_closed [simp]:
"x ∈ carrier R ⟹ y ∈ carrier R ⟹ y ≠ 𝟬 ⟹ x ⊘ y ∈ carrier R"
by (simp add: m_div_def)
lemma minus_divide_left [simp]:
"a ∈ carrier R ⟹ b ∈ carrier R ⟹ b ≠ 𝟬 ⟹ ⊖ (a ⊘ b) = ⊖ a ⊘ b"
by (simp add: m_div_def l_minus)
lemma diff_frac_eq:
assumes "x ∈ carrier R" and "y ∈ carrier R" and "z ∈ carrier R" and "w ∈ carrier R"
and "y ≠ 𝟬" and "z ≠ 𝟬"
shows "x ⊘ y ⊖ w ⊘ z = (x ⊗ z ⊖ w ⊗ y) ⊘ (y ⊗ z)"
using assms
by (simp add: minus_eq l_minus add_frac_eq)
lemma nonzero_mult_divide_mult_cancel_left [simp]:
assumes "a ∈ carrier R" and "b ∈ carrier R" and "c ∈ carrier R"
and "b ≠ 𝟬" and "c ≠ 𝟬"
shows "(c ⊗ a) ⊘ (c ⊗ b) = a ⊘ b"
proof -
from assms have "(c ⊗ a) ⊘ (c ⊗ b) = c ⊗ a ⊗ (inv b ⊗ inv c)"
by (simp add: m_div_def nonzero_inverse_mult_distrib integral_iff)
also from assms have "… = a ⊗ inv b ⊗ (inv c ⊗ c)"
by (simp add: m_ac)
also from assms have "… = a ⊗ inv b" by simp
finally show ?thesis using assms by (simp add: m_div_def)
qed
lemma times_divide_eq_left [simp]:
"a ∈ carrier R ⟹ b ∈ carrier R ⟹ c ∈ carrier R ⟹ c ≠ 𝟬 ⟹
(b ⊘ c) ⊗ a = b ⊗ a ⊘ c"
by (simp add: m_div_def m_ac)
lemma times_divide_eq_right [simp]:
"a ∈ carrier R ⟹ b ∈ carrier R ⟹ c ∈ carrier R ⟹ c ≠ 𝟬 ⟹
a ⊗ (b ⊘ c) = a ⊗ b ⊘ c"
by (simp add: m_div_def m_ac)
lemma nonzero_power_divide:
"a ∈ carrier R ⟹ b ∈ carrier R ⟹ b ≠ 𝟬 ⟹
(a ⊘ b) (^) (n::nat) = a (^) n ⊘ b (^) n"
by (induct n) (simp_all add: nonzero_divide_divide_eq_left)
lemma r_diff_distr:
"x ∈ carrier R ⟹ y ∈ carrier R ⟹ z ∈ carrier R ⟹
z ⊗ (x ⊖ y) = z ⊗ x ⊖ z ⊗ y"
by (simp add: minus_eq r_distr r_minus)
lemma divide_zero_left [simp]:
"a ∈ carrier R ⟹ a ≠ 𝟬 ⟹ 𝟬 ⊘ a = 𝟬"
by (simp add: m_div_def)
lemma divide_self: "a ∈ carrier R ⟹ a ≠ 𝟬 ⟹ a ⊘ a = 𝟭"
by (simp add: m_div_def)
lemma divide_eq_0_iff:
assumes "a ∈ carrier R"
and "b ∈ carrier R"
and "b ≠ 𝟬"
shows "(a ⊘ b = 𝟬) = (a = 𝟬)"
proof
assume "a = 𝟬"
with assms show "a ⊘ b = 𝟬" by simp
next
assume "a ⊘ b = 𝟬"
with assms have "b ⊗ (a ⊘ b) = b ⊗ 𝟬" by simp
also from assms have "b ⊗ (a ⊘ b) = b ⊗ a ⊘ b" by simp
also from assms have "b ⊗ a = a ⊗ b" by (simp add: m_comm)
also from assms have "a ⊗ b ⊘ b = a ⊗ (b ⊘ b)" by simp
also from assms have "b ⊘ b = 𝟭" by (simp add: divide_self)
finally show "a = 𝟬" using assms by simp
qed
end
lemma field_class: "field (cring_class_ops::'a::field ring)"
apply unfold_locales
apply (simp_all add: cring_class_ops_def)
apply (auto simp add: Units_def)
apply (rule_tac x="1 / x" in exI)
apply simp
done
lemma div_class: "(x::'a::field) ⊘⇘cring_class_ops⇙ y = x / y"
apply (simp add: m_div_def m_inv_def class_simps)
apply (rule impI)
apply (rule ssubst [OF the_equality, of _ "1 / y"])
apply simp_all
apply (drule conjunct2)
apply (drule_tac f="λx. x / y" in arg_cong)
apply simp
done
interpretation field_class: field "cring_class_ops::'a::field ring"
rewrites
"(𝟬⇘cring_class_ops⇙::'a) = 0" and
"(𝟭⇘cring_class_ops⇙::'a) = 1" and
"(x::'a) ⊕⇘cring_class_ops⇙ y = x + y" and
"(x::'a) ⊗⇘cring_class_ops⇙ y = x * y" and
"⊖⇘cring_class_ops⇙ (x::'a) = - x" and
"(x::'a) ⊖⇘cring_class_ops⇙ y = x - y" and
"(x::'a) (^)⇘cring_class_ops⇙ n = x ^ n" and
"«n»⇩ℕ⇘cring_class_ops⇙ = of_nat n" and
"((«i»⇘cring_class_ops⇙)::'a) = of_int i" and
"(x::'a) ⊘⇘cring_class_ops⇙ y = x / y" and
"(Int.of_int (numeral m)::'a) = numeral m"
by (simp_all add: field_class class_simps div_class)
end