Theory Algebraic_Auxiliaries

(*
  File:     Algebraic_Auxiliaries.thy
  Authors:  Daniel Stüwe

  Miscellaneous facts about algebra and number theory
*)
section ‹Auxiliary Material›
theory Algebraic_Auxiliaries
  imports 
    "HOL-Algebra.Algebra"
    "HOL-Computational_Algebra.Squarefree"
    "HOL-Number_Theory.Number_Theory"
begin
          
hide_const (open) Divisibility.prime

lemma sum_of_bool_eq_card:
  assumes "finite S"
  shows "(a  S. of_bool (P a)) = real (card {a  S . P a })"
proof -
  have "(a  S. of_bool (P a) :: real) = (a  {xS. P x}. 1)"
    using assms by (intro sum.mono_neutral_cong_right) auto
  thus ?thesis by simp
qed

lemma mod_natE:
  fixes a n b :: nat
  assumes "a mod n = b"
  shows " l. a = n * l + b"
  using assms mod_mult_div_eq[of a n] by (metis add.commute)

lemma (in group) r_coset_is_image: "H #> a = (λ x. x  a) ` H"
  unfolding r_coset_def image_def
  by blast

lemma (in group) FactGroup_order:
  assumes "subgroup H G" "finite H"
  shows "order G = order (G Mod H) * card H"
using lagrange assms unfolding FactGroup_def order_def by simp

corollary (in group) FactGroup_order_div:
  assumes "subgroup H G" "finite H"
  shows "order (G Mod H) = order G div card H" 
using assms FactGroup_order subgroupE(2)[OF subgroup H G] by (auto simp: order_def)

lemma group_hom_imp_group_hom_image:
  assumes "group_hom G G h"
  shows "group_hom G (Gcarrier := h  ` carrier G) h"
  using group_hom.axioms[OF assms] group_hom.img_is_subgroup[OF assms] group.subgroup_imp_group
  by(auto intro!: group_hom.intro simp: group_hom_axioms_def hom_def)

theorem homomorphism_thm:
  assumes "group_hom G G h"
  shows "G Mod kernel G (Gcarrier := h ` carrier G) h  G carrier := h ` carrier G"
  by (intro group_hom.FactGroup_iso group_hom_imp_group_hom_image assms) simp

lemma is_iso_imp_same_card:
  assumes "H  G "
  shows "order H = order G"
proof -
  from assms obtain h where "bij_betw h (carrier H) (carrier G)"
    unfolding is_iso_def iso_def
    by blast

  then show ?thesis
    unfolding order_def 
    by (rule bij_betw_same_card)
qed

corollary homomorphism_thm_order:
  assumes "group_hom G G h" 
  shows "order (Gcarrier := h ` carrier G) * card (kernel G (Gcarrier := h ` carrier G) h) = order G "
proof -
  have "order (Gcarrier := h ` carrier G) = order (G Mod (kernel G (Gcarrier := h ` carrier G) h))"
    using is_iso_imp_same_card[OF homomorphism_thm] group_hom G G h
    by fastforce

  moreover have "group G" using group_hom G G h group_hom.axioms by blast

  ultimately show ?thesis
    using group_hom G G h and group_hom_imp_group_hom_image[OF group_hom G G h] 
    unfolding FactGroup_def
    by (simp add: group.lagrange group_hom.subgroup_kernel order_def)
qed

lemma (in group_hom) kernel_subset: "kernel G H h  carrier G"
  using subgroup_kernel G.subgroupE(1) by blast

lemma (in group) proper_subgroup_imp_bound_on_card:
  assumes "H  carrier G" "subgroup H G" "finite (carrier G)"
  shows "card H  order G div 2"
proof -
  from finite (carrier G) have "finite (rcosets H)"
    by (simp add: RCOSETS_def)

  note subgroup.subgroup_in_rcosets[OF subgroup H G is_group]
  then obtain J where "J  H" "J  rcosets H"
    using rcosets_part_G[OF subgroup H G] and H  carrier G
    by (metis Sup_le_iff inf.absorb_iff2 inf.idem inf.strict_order_iff)

  then have "2  card (rcosets H)"
    using H  rcosets H card_mono[OF finite (rcosets H), of "{H, J}"]
    by simp

  then show ?thesis
    using mult_le_mono[of 2 "card (rcosets H)" "card H" "card H"]  
    unfolding lagrange[OF subgroup H G]
    by force
qed

lemma cong_exp_trans[trans]: 
  "[a ^ b = c] (mod n)  [a = d] (mod n)  [d ^ b = c] (mod n)"
  "[c = a ^ b] (mod n)  [a = d] (mod n)  [c = d ^ b] (mod n)"
  using cong_pow cong_sym cong_trans by blast+

lemma cong_exp_mod[simp]: 
  "[(a mod n) ^ b = c] (mod n)  [a ^ b = c] (mod n)"
  "[c = (a mod n) ^ b] (mod n)  [c = a ^ b] (mod n)"
  by (auto simp add: cong_def mod_simps)

lemma cong_mult_mod[simp]:
  "[(a mod n) * b = c] (mod n)  [a * b = c] (mod n)"
  "[a * (b mod n) = c] (mod n)  [a * b = c] (mod n)"
  by (auto simp add: cong_def mod_simps)

lemma cong_add_mod[simp]:
  "[(a mod n) + b = c] (mod n)  [a + b = c] (mod n)"
  "[a + (b mod n) = c] (mod n)  [a + b = c] (mod n)"
  "[iA. f i mod n = c] (mod n)  [iA. f i = c] (mod n)"
  by (auto simp add: cong_def mod_simps)

lemma cong_add_trans[trans]:
  "[a = b + x] (mod n)  [x = y] (mod n)  [a = b + y] (mod n)"
  "[a = x + b] (mod n)  [x = y] (mod n)  [a = y + b] (mod n)"
  "[b + x = a] (mod n)  [x = y] (mod n)  [b + y = a] (mod n)"
  "[x + b = a] (mod n)  [x = y] (mod n)  [y + b = a] (mod n)"
  unfolding cong_def
  using mod_simps(1, 2)
  by metis+

lemma cong_mult_trans[trans]:
  "[a = b * x] (mod n)  [x = y] (mod n)  [a = b * y] (mod n)"
  "[a = x * b] (mod n)  [x = y] (mod n)  [a = y * b] (mod n)"
  "[b * x = a] (mod n)  [x = y] (mod n)  [b * y = a] (mod n)"
  "[x * b = a] (mod n)  [x = y] (mod n)  [y * b = a] (mod n)"
  unfolding cong_def
  using mod_simps(4, 5)
  by metis+

lemma cong_diff_trans[trans]:
  "[a = b - x] (mod n)  [x = y] (mod n)  [a = b - y] (mod n)" 
  "[a = x - b] (mod n)  [x = y] (mod n)  [a = y - b] (mod n)" 
  "[b - x = a] (mod n)  [x = y] (mod n)  [b - y = a] (mod n)"
  "[x - b = a] (mod n)  [x = y] (mod n)  [y - b = a] (mod n)"
  for a :: "'a :: {unique_euclidean_semiring, euclidean_ring_cancel}"
  unfolding cong_def
  by (metis mod_diff_eq)+

lemma eq_imp_eq_mod_int: "a = b  [a = b] (mod m)" for a b :: int by simp
lemma eq_imp_eq_mod_nat: "a = b  [a = b] (mod m)" for a b :: nat by simp

lemma cong_pow_I: "a = b  [x^a = x^b](mod n)" by simp

lemma gre1I: "(n = 0  False)  (1 :: nat)  n"
  by presburger

lemma gre1I_nat: "(n = 0  False)  (Suc 0 :: nat)  n"
  by presburger

lemma totient_less_not_prime:
  assumes "¬ prime n" "1 < n"
  shows "totient n < n - 1"
  using totient_imp_prime totient_less assms
  by (metis One_nat_def Suc_pred le_less_trans less_SucE zero_le_one)

lemma power2_diff_nat: "x  y  (x - y)2 = x2 + y2 - 2 * x * y" for x y :: nat
  by (simp add: algebra_simps power2_eq_square mult_2_right)
     (meson Nat.diff_diff_right le_add2 le_trans mult_le_mono order_refl)

lemma square_inequality: "1 < n  (n + n)  (n * n)" for n :: nat
  by (metis Suc_eq_plus1_left Suc_leI mult_le_mono1 semiring_normalization_rules(4))

lemma square_one_cong_one:
  assumes "[x = 1](mod n)"
  shows "[x^2 = 1](mod n)"
  using assms cong_pow by fastforce 

lemma cong_square_alt_int:
  "prime p  [a * a = 1] (mod p)  [a = 1] (mod p)  [a = p - 1] (mod p)"
  for a p :: "'a :: {normalization_semidom, linordered_idom, unique_euclidean_ring}"
  using dvd_add_triv_right_iff[of p "a - (p - 1)"]
  by (auto simp add: cong_iff_dvd_diff square_diff_one_factored dest!: prime_dvd_multD)

lemma cong_square_alt:
  "prime p  [a * a = 1] (mod p)  [a = 1] (mod p)  [a = p - 1] (mod p)"
  for a p :: nat
  using cong_square_alt_int[of "int p" "int a"] prime_nat_int_transfer[of p] prime_gt_1_nat[of p]
  by (simp flip: cong_int_iff add: of_nat_diff)  

lemma square_minus_one_cong_one:
  fixes n x :: nat
  assumes "1 < n" "[x = n - 1](mod n)"
  shows "[x^2 = 1](mod n)"
proof -
  have "[x^2 = (n - 1) * (n - 1)] (mod n)"
    using cong_mult[OF assms(2) assms(2)]
    by (simp add: algebra_simps power2_eq_square)

  also have "[(n - 1) * (n - 1) = Suc (n * n) - (n + n)] (mod n)" 
    using power2_diff_nat[of 1 n] 1 < n
    by (simp add: algebra_simps power2_eq_square)

  also have "[Suc (n * n) - (n + n) = Suc (n * n)] (mod n)"
  proof -
    have "n * n + 0 * n = n * n" by linarith
    moreover have "n * n - (n + n) + (n + n) = n * n"
      using square_inequality[OF 1 < n] le_add_diff_inverse2 by blast
    moreover have "(Suc 0 + 1) * n = n + n"
      by simp
    ultimately show ?thesis
      using square_inequality[OF 1 < n] 
      by (metis (no_types) Suc_diff_le add_Suc cong_iff_lin_nat)
  qed

  also have "[Suc (n * n) = 1] (mod n)"
    using cong_to_1'_nat by auto

  finally show ?thesis .
qed

lemma odd_prime_gt_2_int:
 "2 < p" if "odd p" "prime p" for p :: int
  using prime_ge_2_int[OF prime p] odd p
  by (cases "p = 2") auto

lemma odd_prime_gt_2_nat:
 "2 < p" if "odd p" "prime p" for p :: nat
  using prime_ge_2_nat[OF prime p] odd p
  by (cases "p = 2") auto

lemma gt_one_imp_gt_one_power_if_coprime:
  "1  x  1 < n  coprime x n  1  x ^ (n - 1) mod n"
  by (rule gre1I) (auto simp: coprime_commute dest: coprime_absorb_left)

lemma residue_one_dvd: "a mod n = 1  n dvd a - 1" for a n :: nat
  by (fastforce intro!: cong_to_1_nat simp: cong_def)

lemma coprimeI_power_mod:
  fixes x r n :: nat
  assumes "x ^ r mod n = 1" "r  0" "n  0"
  shows "coprime x n"
proof -
  have "coprime (x ^ r mod n) n"
    using coprime_1_right x ^ r mod n = 1
    by (simp add: coprime_commute)
  thus ?thesis using r  0 n  0 by simp
qed


(* MOVE - EXTRA *)
lemma prime_dvd_choose:
  assumes "0 < k" "k < p" "prime p" 
  shows "p dvd (p choose k)"
proof -
  have "k  p" using k < p by auto 

  have "p dvd fact p" using prime p by (simp add: prime_dvd_fact_iff)   
  
  moreover have "¬ p dvd fact k * fact (p - k)"
    unfolding prime_dvd_mult_iff[OF prime p] prime_dvd_fact_iff[OF prime p] 
    using assms by simp
  
  ultimately show ?thesis
    unfolding binomial_fact_lemma[OF k  p, symmetric]
    using assms prime_dvd_multD by blast
qed

lemma cong_eq_0_I: "(iA. [f i mod n = 0] (mod n))  [iA. f i = 0] (mod n)"
  using cong_sum by fastforce

lemma power_mult_cong:
  assumes "[x^n = a](mod m)" "[y^n = b](mod m)"
  shows "[(x*y)^n = a*b](mod m)"
  using assms cong_mult[of "x^n" a m "y^n" b] power_mult_distrib
  by metis

lemma
  fixes n :: nat
  assumes "n > 1"
  shows odd_pow_cong: "odd m  [(n - 1) ^ m = n - 1] (mod n)"
  and even_pow_cong: "even m  [(n - 1) ^ m = 1] (mod n)"
proof (induction m)
  case (Suc m)
  case 1
  with Suc have IH: "[(n - 1) ^ m = 1] (mod n)" by auto
  show ?case using 1 < n cong_mult[OF cong_refl IH] by simp
next
  case (Suc m)
  case 2
  with Suc have IH: "[(n - 1) ^ m = n - 1] (mod n)" by auto
  show ?case 
    using cong_mult[OF cong_refl IH, of "(n - 1)"] and square_minus_one_cong_one[OF 1 < n, of "n - 1"]
    by (auto simp: power2_eq_square intro: cong_trans)
qed simp_all

lemma cong_mult_uneq':
  fixes a :: "'a::{unique_euclidean_ring, ring_gcd}"
  assumes "coprime d a"
  shows "[b  c] (mod a)  [d = e] (mod a)  [b * d  c * e] (mod a)"
  using cong_mult_rcancel[OF assms]
  using cong_trans[of "b*d" "c*e" a "c*d"]
  using cong_scalar_left cong_sym by blast

lemma p_coprime_right_nat: "prime p  coprime a p = (¬ p dvd a)" for p a :: nat
  by (meson coprime_absorb_left coprime_commute not_prime_unit prime_imp_coprime_nat)


lemma squarefree_mult_imp_coprime:
  assumes "squarefree (a * b :: 'a :: semiring_gcd)"
  shows   "coprime a b"
proof (rule coprimeI)
  fix l assume "l dvd a" "l dvd b"
  then obtain a' b' where "a = l * a'" "b = l * b'"
    by (auto elim!: dvdE)
  with assms have "squarefree (l2 * (a' * b'))"
    by (simp add: power2_eq_square mult_ac)
  thus "l dvd 1" by (rule squarefreeD) auto
qed

lemma prime_divisor_exists_strong:
  fixes m :: int
  assumes "m > 1" "¬prime m"
  shows   "n k. m = n * k  1 < n  n < m  1 < k  k < m"
proof -
  from assms obtain n k where nk: "n * k > 1" "n  0" "m = n * k" "n  1" "n  0" "k  1"
    using assms unfolding prime_int_iff dvd_def by auto
  from nk have "n > 1" by linarith

  from nk assms have "n * k > 0" by simp
  with n  0 have "k > 0"
    using zero_less_mult_pos by force
  with k  1 have "k > 1" by linarith
  from nk have "n > 1" by linarith

  from k > 1 nk have "n < m" "k < m" by simp_all
  with nk k > 1 n > 1 show ?thesis by blast
qed

lemma prime_divisor_exists_strong_nat:
  fixes m :: nat
  assumes "1 < m" "¬prime m"
  shows   "p k. m = p * k  1 < p  p < m  1 < k  k < m  prime p"
proof -
  obtain p where p_def: "prime p" "p dvd m" "p  m" "1 < p" 
    using assms prime_prime_factor and prime_gt_1_nat
    by blast

  moreover define k where "k = m div p"
  with p dvd m have "m = p * k" by simp

  moreover have "p < m" 
    using p  m dvd_imp_le[OF p dvd m] and m > 1
    by simp

  moreover have "1 < k" "k < m"
    using 1 < m 1 < p and p  m
    unfolding m = p * k
    by (force intro: Suc_lessI Nat.gr0I)+

  ultimately show ?thesis using 1 < m by blast
qed

(* TODO Remove *)
lemma prime_factorization_eqI:
  assumes "p. p ∈# P  prime p" "prod_mset P = n"
  shows   "prime_factorization n = P"
  using prime_factorization_prod_mset_primes[of P] assms by simp

lemma prime_factorization_prime_elem:
  assumes "prime_elem p"
  shows   "prime_factorization p = {#normalize p#}"
proof -
  have "prime_factorization p = prime_factorization (normalize p)"
    by (metis normalize_idem prime_factorization_cong)
  also have " = {#normalize p#}"
    by (rule prime_factorization_prime) (use assms in auto)
  finally show ?thesis .
qed

lemma size_prime_factorization_eq_Suc_0_iff [simp]:
  fixes n :: "'a :: factorial_semiring_multiplicative"
  shows "size (prime_factorization n) = Suc 0  prime_elem n"
proof
  assume size: "size (prime_factorization n) = Suc 0"
  hence [simp]: "n  0" by auto
  from size obtain p where *: "prime_factorization n = {#p#}"
    by (auto elim!: size_mset_SucE)
  hence p: "p  prime_factors n" by auto

  have "prime_elem (normalize p)"
    using p by (auto simp: in_prime_factors_iff)
  also have "p = prod_mset (prime_factorization n)"
    using * by simp
  also have "normalize  = normalize n"
    by (rule prod_mset_prime_factorization_weak) auto
  finally show "prime_elem n" by simp
qed (auto simp: prime_factorization_prime_elem)
(* END TODO *)

(* TODO Move *)
lemma squarefree_prime_elem [simp, intro]:
  fixes p :: "'a :: algebraic_semidom"
  assumes "prime_elem p"
  shows   "squarefree p"
proof (rule squarefreeI)
  fix x assume "x2 dvd p"
  show "is_unit x"
  proof (rule ccontr)
    assume "¬is_unit x"
    hence "¬is_unit (x2)"
      by (simp add: is_unit_power_iff)
    from assms and this and x2 dvd p have "prime_elem (x2)"
      by (rule prime_elem_mono)
    thus False by (simp add: prime_elem_power_iff)
  qed
qed

lemma squarefree_prime [simp, intro]: "prime p  squarefree p"
  by auto

lemma not_squarefree_primepow:
  assumes "primepow n"
  shows   "squarefree n  prime n"
  using assms by (auto simp: primepow_def squarefree_power_iff prime_power_iff)

lemma prime_factorization_normalize [simp]:
  "prime_factorization (normalize n) = prime_factorization n"
  by (rule prime_factorization_cong) auto

lemma one_prime_factor_iff_primepow:
  fixes n :: "'a :: factorial_semiring_multiplicative"
  shows "card (prime_factors n) = Suc 0  primepow (normalize n)"
proof
  assume "primepow (normalize n)"
  then obtain p k where pk: "prime p" "normalize n = p ^ k" "k > 0"
    by (auto simp: primepow_def)
  hence "card (prime_factors (normalize n)) = Suc 0"
    by (subst pk) (simp add: prime_factors_power prime_factorization_prime)
  thus "card (prime_factors n) = Suc 0"
    by simp
next
  assume *: "card (prime_factors n) = Suc 0"
  from * have "(pprime_factors n. p ^ multiplicity p n) = normalize n"
    by (intro prod_prime_factors) auto
  also from * have "card (prime_factors n) = 1" by simp
  then obtain p where p: "prime_factors n = {p}"
    by (elim card_1_singletonE)
  finally have "normalize n = p ^ multiplicity p n"
    by simp
  moreover from p have "prime p" "multiplicity p n > 0"
    by (auto simp: prime_factors_multiplicity)
  ultimately show "primepow (normalize n)"
    unfolding primepow_def by blast
qed

lemma squarefree_imp_prod_prime_factors_eq:
  fixes x :: "'a :: factorial_semiring_multiplicative"
  assumes "squarefree x"
  shows   "(prime_factors x) = normalize x"
proof -
  from assms have [simp]: "x  0" by auto
  have "(pprime_factors x. p ^ multiplicity p x) = normalize x"
    by (intro prod_prime_factors) auto
  also have "(pprime_factors x. p ^ multiplicity p x) = (pprime_factors x. p)"
    using assms by (intro prod.cong refl) (auto simp: squarefree_factorial_semiring')
  finally show ?thesis by simp
qed
(* END TODO *)

end