Quelle  Algebra_Aux.thy

(*  Title:      HOL/Decision_Procs/Algebra_Aux.thy
  Author: Stefan Berghofer
*)

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🪙 = ((⊕🪙R🪙) 1🪙R🪙 ^^ n) 0🪙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¬🪙ℕ = 0"
  by (simp add: of_natural_def)

lemma of_nat_Suc [simp]: "«Suc n¬🪙ℕ = 1 ⊕ «n¬🪙ℕ"
  by (simp add: of_natural_def)

lemma of_int_0 [simp]: "«0¬ = 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 0
  then show ?case by (simp add: minus_eq)
next
  case Suc': (Suc m)
  show ?case
  proof (cases n)
    case 0
    then show ?thesis
      by (simp add: minus_eq)
  next
    case (Suc k)
    with Suc' have "«Suc m - Suc k¬🪙ℕ = «m¬🪙ℕ ⊖ «k¬🪙ℕ" by simp
    also have "… = 1 ⊕ ⊖ 1 ⊕ («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
qed

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¬ = 1"
  by (simp add: of_integer_def)

lemma of_int_2: "«2¬ = 1 ⊕ 1"
  by (simp add: of_integer_def numeral_2_eq_2)

lemma minus_0_r [simp]: "x ∈ carrier R ==> x ⊖ 0 = x"
  by (simp add: minus_eq)

lemma minus_0_l [simp]: "x ∈ carrier R ==> 0 ⊖ x = ⊖ x"
  by (simp add: minus_eq)

lemma eq_diff0:
  assumes "x ∈ carrier R" "y ∈ carrier R"
  shows "x ⊖ y = 0 ⟷ x = y"
proof
  assume "x ⊖ y = 0"
  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 = 0" 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 = 0"
proof
  assume "x = ⊖ y"
  with assms show "x ⊕ y = 0" by (simp add: l_neg)
next
  assume "x ⊕ y = 0"
  with assms have "x ⊕ (y ⊕ ⊖ y) = 0 ⊕ ⊖ 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 = (*), one = 1, zero = 0, add = (+))"

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: "0🪙cring_class_ops🪙 = 0"
  by (simp add: cring_class_ops_def)

lemma one_class: "1🪙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"
proof -
  have "(THE y::'a. x + y = 0 ∧ y + x = 0) = - x"
    by (rule the_equality) (simp_all add: eq_neg_iff_add_eq_0)
  then show ?thesis
    by (simp add: a_inv_def m_inv_def cring_class_ops_def)
qed

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 "(0🪙cring_class_ops🪙::'a) = 0"
    and "(1🪙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) = 0) = (a = 0 ∧ 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 = 0🪙G🪙 then 0🪙G🪙 else x ⊗🪙G🪙 inv🪙G🪙 y)"

context field
begin

lemma inv_closed [simp]: "x ∈ carrier R ==> x ≠ 0 ==> inv x ∈ carrier R"
  by (simp add: field_Units)

lemma l_inv [simp]: "x ∈ carrier R ==> x ≠ 0 ==> inv x ⊗ x = 1"
  by (simp add: field_Units)

lemma r_inv [simp]: "x ∈ carrier R ==> x ≠ 0 ==> x ⊗ inv x = 1"
  by (simp add: field_Units)

lemma inverse_unique:
  assumes a: "a ∈ carrier R"
    and b: "b ∈ carrier R"
    and ab: "a ⊗ b = 1"
  shows "inv a = b"
proof -
  from ab b have *: "a ≠ 0"
    by (cases "a = 0") simp_all
  with a have "inv a ⊗ (a ⊗ b) = inv a"
    by (simp add: ab)
  with a b * show ?thesis
    by (simp add: m_assoc [symmetric])
qed

lemma nonzero_inverse_inverse_eq: "a ∈ carrier R ==> a ≠ 0 ==> inv (inv a) = a"
  by (rule inverse_unique) simp_all

lemma inv_1 [simp]: "inv 1 = 1"
  by (rule inverse_unique) simp_all

lemma nonzero_inverse_mult_distrib:
  assumes "a ∈ carrier R" "b ∈ carrier R"
    and "a ≠ 0" "b ≠ 0"
  shows "inv (a ⊗ b) = inv b ⊗ inv a"
proof -
  from assms have "a ⊗ (b ⊗ inv b) ⊗ inv a = 1"
    by simp
  with assms have eq: "a ⊗ b ⊗ (inv b ⊗ inv a) = 1"
    by (simp only: m_assoc m_closed inv_closed assms)
  from assms show ?thesis
    using inverse_unique [OF _ _ eq] by simp
qed

lemma nonzero_imp_inverse_nonzero:
  assumes "a ∈ carrier R" and "a ≠ 0"
  shows "inv a ≠ 0"
proof
  assume *: "inv a = 0"
  from assms have **: "1 = a ⊗ inv a"
    by simp
  also from assms have "… = 0" by (simp add: *)
  finally have "1 = 0" .
  then show False by (simp add: eq_commute)
qed

lemma nonzero_divide_divide_eq_left:
  "a ∈ carrier R ==> b ∈ carrier R ==> c ∈ carrier R ==> b ≠ 0 ==> c ≠ 0 ==>
    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 ≠ 0 ==> d ≠ 0 ==> (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 ≠ 0 ==> c ≠ 0 ==> d ≠ 0 ==> (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 ⊘ 1 = x"
  by (simp add: m_div_def)

lemma add_frac_eq:
  assumes "x ∈ carrier R" "y ∈ carrier R" "z ∈ carrier R" "w ∈ carrier R"
    and "y ≠ 0" "z ≠ 0"
  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 ≠ 0 ==> x ⊘ y ∈ carrier R"
  by (simp add: m_div_def)

lemma minus_divide_left [simp]:
  "a ∈ carrier R ==> b ∈ carrier R ==> b ≠ 0 ==> ⊖ (a ⊘ b) = ⊖ a ⊘ b"
  by (simp add: m_div_def l_minus)

lemma diff_frac_eq:
  assumes "x ∈ carrier R" "y ∈ carrier R" "z ∈ carrier R" "w ∈ carrier R"
    and "y ≠ 0" "z ≠ 0"
  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" "b ∈ carrier R" "c ∈ carrier R"
    and "b ≠ 0" "c ≠ 0"
  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 ≠ 0 ==>
    (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 ≠ 0 ==>
    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 ≠ 0 ==>
    (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 ≠ 0 ==> 0 ⊘ a = 0"
  by (simp add: m_div_def)

lemma divide_self: "a ∈ carrier R ==> a ≠ 0 ==> a ⊘ a = 1"
  by (simp add: m_div_def)

lemma divide_eq_0_iff:
  assumes "a ∈ carrier R" "b ∈ carrier R"
    and "b ≠ 0"
  shows "a ⊘ b = 0 ⟷ a = 0"
proof
  assume "a = 0"
  with assms show "a ⊘ b = 0" by simp
next
  assume "a ⊘ b = 0"
  with assms have "b ⊗ (a ⊘ b) = b ⊗ 0" 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 = 1" by (simp add: divide_self)
  finally show "a = 0" 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)
  using field_class.field_inverse by (force simp add: Units_def)

lemma div_class: "(x::'a::field) ⊘🪙cring_class_ops🪙 y = x / y"
  by (simp add: carrier_class class_simps cring_class.comm_inv_char
      field_class.field_divide_inverse m_div_def)

interpretation field_class: field "cring_class_ops::'a::field ring"
  rewrites "(0🪙cring_class_ops🪙::'a) = 0"
    and "(1🪙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