Theory Schoenhage_Strassen_Ring_Lemmas

theory Schoenhage_Strassen_Ring_Lemmas
  imports "HOL-Algebra.Ring" "HOL-Algebra.Multiplicative_Group"
begin

context cring
begin

lemma diff_diff:
  assumes "a ∈ carrier R" "b ∈ carrier R" "c ∈ carrier R"
  shows "a ⊖ (b ⊖ c) = a ⊖ b ⊕ c"
  using assms by algebra
lemma minus_eq_mult_one:
  assumes "a ∈ carrier R"
  shows "⊖ a = (⊖ 𝟭) ⊗ a"
  using assms by algebra
lemma diff_eq_add_mult_one:
  assumes "a ∈ carrier R" "b ∈ carrier R"
  shows "a ⊖ b = a ⊕ (⊖ 𝟭) ⊗ b"
  using assms by algebra
lemma minus_cancel:
  assumes "a ∈ carrier R" "b ∈ carrier R"
  shows "a ⊖ b ⊕ b = a"
  using assms by algebra
lemma assoc4:
  assumes "a ∈ carrier R" "b ∈ carrier R" "c ∈ carrier R" "d ∈ carrier R"
  shows "a ⊗ (b ⊗ (c ⊗ d)) = a ⊗ b ⊗ c ⊗ d"
  using assms by algebra
lemma diff_sum:
  assumes "a ∈ carrier R" "b ∈ carrier R" "c ∈ carrier R" "d ∈ carrier R"
  shows "(a ⊖ c) ⊕ (b ⊖ d) = (a ⊕ b) ⊖ (c ⊕ d)"
  using assms by algebra

end

lemma (in ring) inv_cancel_left:
  assumes "x ∈ carrier R"
  assumes "y ∈ carrier R"
  assumes "z ∈ Units R"
  assumes "x = z ⊗ y"
  shows "inv z ⊗ x = y"
  using assms
  by (metis Units_closed Units_inv_closed Units_l_inv l_one m_assoc)

lemma (in ring) r_distr_diff:
  assumes "x ∈ carrier R"
  assumes "y ∈ carrier R"
  assumes "z ∈ carrier R"
  shows "x ⊗ (y ⊖ z) = x ⊗ y ⊖ x ⊗ z"
  using assms by algebra

lemma (in group)
  assumes "x ∈ carrier G"
  shows "⋀i. i ∈ {1..<ord x} ⟹ x [^] i ≠ 𝟭"
  using assms using pow_eq_id by auto

subsection "Multiplicative Subgroups"
locale multiplicative_subgroup = cring +
  fixes X
  fixes M
  assumes Units_subset: "X ⊆ Units R"
  assumes M_def: "M = ⦇ carrier = X, monoid.mult = (⊗), one = 𝟭 ⦈"
  assumes M_group: "group M"
begin

lemma carrier_M[simp]: "carrier M = X" using M_def by auto

lemma one_eq: "𝟭⇘M⇙ = 𝟭" using M_def by simp

lemma mult_eq: "a ⊗⇘M⇙ b = a ⊗ b" using M_def by simp

lemma inv_eq:
  assumes "x ∈ X"
  shows "inv⇘M⇙ x = inv x"
proof (intro comm_inv_char[symmetric])
  show "x ∈ carrier R" using assms Units_subset by blast
  from assms have "inv⇘M⇙ x ∈ X" using group.inv_closed[OF M_group] by simp
  then show "inv⇘M⇙ x ∈ carrier R" using Units_subset by blast
  have "x ⊗⇘M⇙ inv⇘M⇙ x = 𝟭⇘M⇙"
    using group.Units_eq[OF M_group] monoid.Units_r_inv[OF group.is_monoid[OF M_group]]
    using assms by simp
  then show "x ⊗ inv⇘M⇙ x = 𝟭" using M_def by simp
qed

lemma nat_pow_eq: "x [^]⇘M⇙ (m :: nat) = x [^] m"
  by (induction m) (simp_all add: M_def)

lemma int_pow_eq:
  assumes "x ∈ X"
  shows "x [^]⇘M⇙ (i :: int) = x [^] i"
proof (cases "i ≥ 0")
  case True
  then have "x [^]⇘M⇙ i = x [^]⇘M⇙ (nat i)"
    by simp
  also have "... = x [^] (nat i)"
    using nat_pow_eq by simp
  also have "... = x [^] i"
    using True by simp
  finally show ?thesis .
next
  case False
  then have "x [^]⇘M⇙ i = inv⇘M⇙ (x [^]⇘M⇙ (nat (- i)))"
    using int_pow_def2[of M] by presburger
  also have "... = inv (x [^]⇘M⇙ (nat (- i)))"
    apply (intro inv_eq)
    using monoid.nat_pow_closed[OF group.is_monoid[OF M_group]] assms by simp
  also have "... = inv (x [^] (nat (- i)))"
    by (simp add: nat_pow_eq)
  also have "... = x [^] i"
    using int_pow_def2 False by (metis leI)
  finally show ?thesis .
qed

end

context cring
begin

interpretation units_group: group "units_of R"
  by (rule units_group)

lemma units_subgroup: "multiplicative_subgroup R (Units R) (units_of R)"
  apply unfold_locales unfolding units_of_def by simp_all

interpretation units_subgroup: multiplicative_subgroup R "Units R" "units_of R"
  by (rule units_subgroup)

lemma inv_nat_pow:
  assumes "a ∈ Units R"
  shows "inv (a [^] (b :: nat)) = inv a [^] b"
proof -
  have "inv (a [^] b) = inv⇘units_of R⇙ (a [^]⇘units_of R⇙ b)"
    using assms units_subgroup.nat_pow_eq units_subgroup.inv_eq Units_pow_closed by simp
  also have "... = inv⇘units_of R⇙ a [^]⇘units_of R⇙ b"
    apply (intro group.nat_pow_inv[OF units_group, symmetric])
    using assms units_subgroup.carrier_M by argo
  also have "... = inv a [^] b"
    using assms units_subgroup.nat_pow_eq units_subgroup.inv_eq by simp
  finally show ?thesis .
qed
lemma int_pow_mult:
  fixes m1 m2 :: int
  assumes "x ∈ Units R"
  shows "x [^] m1 ⊗ x [^] m2 = x [^] (m1 + m2)"
  using units_group.int_pow_mult[of x]
  unfolding units_subgroup.carrier_M
  using assms units_subgroup.int_pow_eq[OF assms]
  by (simp add: units_subgroup.mult_eq)
lemma int_pow_pow:
  fixes m1 m2 :: int
  assumes "x ∈ Units R"
  shows "(x [^] m1) [^] m2 = x [^] (m1 * m2)"
  using units_group.int_pow_pow[of x] assms
  unfolding units_subgroup.carrier_M
  using units_group.int_pow_closed units_subgroup.int_pow_eq by auto
lemma int_pow_one:
  "𝟭 [^] (i :: int) = 𝟭"
  using units_group.int_pow_one[of i]
  using units_subgroup.int_pow_eq[OF Units_one_closed] units_subgroup.one_eq by simp
lemma int_pow_closed:
  assumes "x ∈ Units R"
  shows "x [^] (i :: int) ∈ Units R"
  using units_group.int_pow_closed units_subgroup.carrier_M assms units_subgroup.int_pow_eq
  by simp

lemma units_of_int_pow: "μ ∈ Units R ⟹ μ [^]⇘(units_of R)⇙ i = μ [^] (i :: int)"
  using units_of_pow[of μ]
  apply (simp add: int_pow_def)
  by (metis Units_pow_closed nat_pow_def units_of_inv)

lemma units_int_pow_neg: "μ ∈ Units R ⟹ (inv μ) [^] (n :: int) = μ [^] (- n)"
  by (metis Units_inv_Units units_of_int_pow units_group.int_pow_inv units_group.int_pow_neg units_of_carrier units_of_inv)

lemma units_inv_int_pow: "μ ∈ Units R ⟹ inv μ = μ [^] (- (1 :: int))"
  using units_int_pow_neg[of μ "1 :: int"]
  by (simp add: int_pow_def2)

lemma inv_prod: "μ ∈ Units R ⟹ ν ∈ Units R ⟹ inv (μ ⊗ ν) = inv ν ⊗ inv μ"
  by (metis Units_m_closed group.inv_mult_group units_group units_of_carrier units_of_inv units_of_mult)

lemma powers_of_negative:
  fixes r :: nat
  assumes "x ∈ carrier R"
  shows "even r ⟹ (⊖ x) [^] r = x [^] r" "odd r ⟹ (⊖ x) [^] r = ⊖ (x [^] r)"
   using assms by (induction r) (simp_all add: l_minus r_minus)

end

subsection "Additive Subgroups"

locale additive_subgroup = cring + 
  fixes X
  fixes M
  assumes Units_subset: "X ⊆ carrier R"
  assumes M_def: "M = ⦇ carrier = X, monoid.mult = (⊕), one = 𝟬 ⦈"
  assumes M_group: "group M"
begin

lemma carrier_M[simp]: "carrier M = X"
  unfolding M_def by simp

lemma one_eq: "𝟭⇘M⇙ = 𝟬" unfolding M_def by simp

lemma mult_eq: "a ⊗⇘M⇙ b = a ⊕ b"
  unfolding M_def by simp

lemma inv_eq:
  assumes "a ∈ X"
  shows "inv⇘M⇙ a = ⊖ a"
  apply (intro sum_zero_eq_neg set_mp[OF Units_subset] assms)
  subgoal using group.inv_closed[OF M_group] assms unfolding carrier_M by simp
  subgoal
    unfolding mult_eq[symmetric] one_eq[symmetric]
    apply (intro group.l_inv M_group)
    unfolding carrier_M using assms .
  done

end

end