Theory HOL-Library.Real_Mod

(*
  File:     HOL/Library/Real_Mod.thy
  Authors:  Manuel Eberl, University of Innsbruck
*)
section ‹Modulo and congruence on the reals›
theory Real_Mod
  imports Complex_Main
begin

(* MOVED TO HOL-Library ON 20.03.2024 *)

definition rmod :: "real ⇒ real ⇒ real" (infixl ‹rmod› 70) where
  "x rmod y = x - ¦y¦ * of_int ⌊x / ¦y¦⌋"

lemma rmod_conv_frac: "y ≠ 0 ⟹ x rmod y = frac (x / ¦y¦) * ¦y¦"
  by (simp add: rmod_def frac_def algebra_simps)

lemma rmod_conv_frac': "x rmod y = (if y = 0 then x else frac (x / ¦y¦) * ¦y¦)"
  by (simp add: rmod_def frac_def algebra_simps)

lemma rmod_rmod [simp]: "(x rmod y) rmod y = x rmod y"
  by (simp add: rmod_conv_frac')

lemma rmod_0_right [simp]: "x rmod 0 = x"
  by (simp add: rmod_def)

lemma rmod_less: "m > 0 ⟹ x rmod m < m"
  by (simp add: rmod_conv_frac' frac_lt_1)

lemma rmod_less_abs: "m ≠ 0 ⟹ x rmod m < ¦m¦"
  by (simp add: rmod_conv_frac' frac_lt_1)

lemma rmod_le: "m > 0 ⟹ x rmod m ≤ m"
  by (intro less_imp_le rmod_less)

lemma rmod_nonneg: "m ≠ 0 ⟹ x rmod m ≥ 0"
  unfolding rmod_def
  by (metis abs_le_zero_iff diff_ge_0_iff_ge floor_divide_lower linorder_not_le mult.commute)

lemma rmod_unique:
  assumes "z ∈ {0..<¦y¦}" "x = z + of_int n * y"
  shows   "x rmod y = z"
proof -
  have "(x - z) / y = of_int n"
    using assms by auto
  hence "(x - z) / ¦y¦ = of_int ((if y > 0 then 1 else -1) * n)"
    using assms(1) by (cases y "0 :: real" rule: linorder_cases) (auto split: if_splits)
  also have "… ∈ ℤ"
    by auto
  finally have "frac (x / ¦y¦) = z / ¦y¦"
    using assms(1) by (subst frac_unique_iff) (auto simp: field_simps)
  thus ?thesis
    using assms(1) by (auto simp: rmod_conv_frac')
qed

lemma rmod_0 [simp]: "0 rmod z = 0"
  by (simp add: rmod_def)

lemma rmod_add: "(x rmod z + y rmod z) rmod z = (x + y) rmod z"
proof (cases "z = 0")
  case [simp]: False
  show ?thesis
  proof (rule sym, rule rmod_unique)
    define n where "n = (if z > 0 then 1 else -1) * (⌊x / ¦z¦⌋ + ⌊y / ¦z¦⌋ +
       ⌊(x + y - (¦z¦ * real_of_int ⌊x / ¦z¦⌋ + ¦z¦ * real_of_int ⌊y / ¦z¦⌋)) / ¦z¦⌋)"
    show "x + y = (x rmod z + y rmod z) rmod z + real_of_int n * z"
      by (simp add: rmod_def algebra_simps n_def)
  qed (auto simp: rmod_less_abs rmod_nonneg)
qed auto

lemma rmod_diff: "(x rmod z - y rmod z) rmod z = (x - y) rmod z"
proof (cases "z = 0")
  case [simp]: False
  show ?thesis
  proof (rule sym, rule rmod_unique)
    define n where "n = (if z > 0 then 1 else -1) * (⌊x / ¦z¦⌋ +
      ⌊(x + ¦z¦ * real_of_int ⌊y / ¦z¦⌋ - (y + ¦z¦ * real_of_int ⌊x / ¦z¦⌋)) / ¦z¦⌋ - ⌊y / ¦z¦⌋)"
    show "x - y = (x rmod z - y rmod z) rmod z + real_of_int n * z"
      by (simp add: rmod_def algebra_simps n_def)
  qed (auto simp: rmod_less_abs rmod_nonneg)
qed auto

lemma rmod_self [simp]: "x rmod x = 0"
  by (cases x "0 :: real" rule: linorder_cases) (auto simp: rmod_conv_frac)

lemma rmod_self_multiple_int [simp]: "(of_int n * x) rmod x = 0"
  by (cases x "0 :: real" rule: linorder_cases) (auto simp: rmod_conv_frac)

lemma rmod_self_multiple_nat [simp]: "(of_nat n * x) rmod x = 0"
  by (cases x "0 :: real" rule: linorder_cases) (auto simp: rmod_conv_frac)

lemma rmod_self_multiple_numeral [simp]: "(numeral n * x) rmod x = 0"
  by (cases x "0 :: real" rule: linorder_cases) (auto simp: rmod_conv_frac)

lemma rmod_self_multiple_int' [simp]: "(x * of_int n) rmod x = 0"
  by (cases x "0 :: real" rule: linorder_cases) (auto simp: rmod_conv_frac)

lemma rmod_self_multiple_nat' [simp]: "(x * of_nat n) rmod x = 0"
  by (cases x "0 :: real" rule: linorder_cases) (auto simp: rmod_conv_frac)

lemma rmod_self_multiple_numeral' [simp]: "(x * numeral n) rmod x = 0"
  by (cases x "0 :: real" rule: linorder_cases) (auto simp: rmod_conv_frac)

lemma rmod_idem [simp]: "x ∈ {0..<¦y¦} ⟹ x rmod y = x"
  by (rule rmod_unique[of _ _ _ 0]) auto



definition rcong :: "real ⇒ real ⇒ real ⇒ bool"
    (‹(‹indent=1 notation=‹mixfix rcong››[_ = _] '(' rmod _'))›)
  where "[x = y] (rmod m) ⟷ x rmod m = y rmod m"

named_theorems rcong_intros

lemma rcong_0_right [simp]: "[x = y] (rmod 0) ⟷ x = y"
  by (simp add: rcong_def)

lemma rcong_0_iff: "[x = 0] (rmod m) ⟷ x rmod m = 0"
  and rcong_0_iff': "[0 = x] (rmod m) ⟷ x rmod m = 0"
  by (simp_all add: rcong_def)

lemma rcong_refl [simp, intro!, rcong_intros]: "[x = x] (rmod m)"
  by (simp add: rcong_def)

lemma rcong_sym: "[y = x] (rmod m) ⟹ [x = y] (rmod m)"
  by (simp add: rcong_def)

lemma rcong_sym_iff: "[y = x] (rmod m) ⟷ [x = y] (rmod m)"
  unfolding rcong_def by (simp add: eq_commute del: rmod_idem)

lemma rcong_trans [trans]: "[x = y] (rmod m) ⟹ [y = z] (rmod m) ⟹ [x = z] (rmod m)"
  by (simp add: rcong_def)

lemma rcong_add [rcong_intros]:
  "[a = b] (rmod m) ⟹ [c = d] (rmod m) ⟹ [a + c = b + d] (rmod m)"
  unfolding rcong_def using rmod_add by metis

lemma rcong_diff [rcong_intros]:
  "[a = b] (rmod m) ⟹ [c = d] (rmod m) ⟹ [a - c = b - d] (rmod m)"
  unfolding rcong_def using rmod_diff by metis

lemma rcong_uminus [rcong_intros]:
  "[a = b] (rmod m) ⟹ [-a = -b] (rmod m)"
  using rcong_diff[of 0 0 m a b] by simp

lemma rcong_uminus_uminus_iff [simp]: "[-x = -y] (rmod m) ⟷ [x = y] (rmod m)"
  using rcong_uminus minus_minus by metis

lemma rcong_uminus_left_iff: "[-x = y] (rmod m) ⟷ [x = -y] (rmod m)"
  using rcong_uminus minus_minus by metis

lemma rcong_add_right_cancel [simp]: "[a + c = b + c] (rmod m) ⟷ [a = b] (rmod m)"
  using rcong_add[of a b m c c] rcong_add[of "a + c" "b + c" m "-c" "-c"] by auto

lemma rcong_add_left_cancel [simp]: "[c + a = c + b] (rmod m) ⟷ [a = b] (rmod m)"
  by (subst (1 2) add.commute) simp

lemma rcong_diff_right_cancel [simp]: "[a - c = b - c] (rmod m) ⟷ [a = b] (rmod m)"
  by (metis rcong_add_left_cancel uminus_add_conv_diff)

lemma rcong_diff_left_cancel [simp]: "[c - a = c - b] (rmod m) ⟷ [a = b] (rmod m)"
  by (metis minus_diff_eq rcong_diff_right_cancel rcong_uminus_uminus_iff)

lemma rcong_rmod_right_iff [simp]: "[a = (b rmod m)] (rmod m) ⟷ [a = b] (rmod m)"
  and rcong_rmod_left_iff [simp]: "[(a rmod m) = b] (rmod m) ⟷ [a = b] (rmod m)"
  by (simp_all add: rcong_def)

lemma rcong_rmod_left [rcong_intros]: "[a = b] (rmod m) ⟹ [(a rmod m) = b] (rmod m)"
  and rcong_rmod_right [rcong_intros]: "[a = b] (rmod m) ⟹ [a = (b rmod m)] (rmod m)"
  by simp_all

lemma rcong_mult_of_int_0_left_left [rcong_intros]: "[0 = of_int n * m] (rmod m)"
  and rcong_mult_of_int_0_right_left [rcong_intros]: "[0 = m * of_int n] (rmod m)"
  and rcong_mult_of_int_0_left_right [rcong_intros]: "[of_int n * m = 0] (rmod m)"
  and rcong_mult_of_int_0_right_right [rcong_intros]: "[m * of_int n = 0] (rmod m)"
  by (simp_all add: rcong_def)

lemma rcong_altdef: "[a = b] (rmod m) ⟷ (∃n. b = a + of_int n * m)"
proof (cases "m = 0")
  case False
  show ?thesis
  proof
    assume "[a = b] (rmod m)"
    hence "[a - b = b - b] (rmod m)"
      by (intro rcong_intros)
    hence "(a - b) rmod m = 0"
      by (simp add: rcong_def)
    then obtain n where "of_int n = (a - b) / ¦m¦"
      using False by (auto simp: rmod_conv_frac elim!: Ints_cases)
    thus "∃n. b = a + of_int n * m" using False
      by (intro exI[of _ "if m > 0 then -n else n"]) (auto simp: field_simps)
  next
    assume "∃n. b = a + of_int n * m"
    then obtain n where n: "b = a + of_int n * m"
      by auto
    have "[a + 0 = a + of_int n * m] (rmod m)"
      by (intro rcong_intros)
    with n show "[a = b] (rmod m)"
      by simp
  qed
qed auto

lemma rcong_conv_diff_rmod_eq_0: "[x = y] (rmod m) ⟷ (x - y) rmod m = 0"
  by (metis cancel_comm_monoid_add_class.diff_cancel rcong_0_iff rcong_diff_right_cancel)

lemma rcong_imp_eq:
  assumes "[x = y] (rmod m)" "¦x - y¦ < ¦m¦"
  shows   "x = y"
proof -
  from assms obtain n where n: "y = x + of_int n * m"
    unfolding rcong_altdef by blast
  have "of_int ¦n¦ * ¦m¦ = ¦x - y¦"
    by (simp add: n abs_mult)
  also have "… < 1 * ¦m¦"
    using assms(2) by simp
  finally have "n = 0"
    by (subst (asm) mult_less_cancel_right) auto
  with n show ?thesis
    by simp
qed

lemma rcong_mult_modulus:
  assumes "[a = b] (rmod (m / c))" "c ≠ 0"
  shows   "[a * c = b * c] (rmod m)"
proof -
  from assms obtain k where k: "b = a + of_int k * (m / c)"
    by (auto simp: rcong_altdef)
  have "b * c = (a + of_int k * (m / c)) * c"
    by (simp only: k)
  also have "… = a * c + of_int k * m"
    using assms(2) by (auto simp: divide_simps)
  finally show ?thesis
    unfolding rcong_altdef by blast
qed

lemma rcong_divide_modulus:
  assumes "[a = b] (rmod (m * c))" "c ≠ 0"
  shows   "[a / c = b / c] (rmod m)"
  using rcong_mult_modulus[of a b m "1 / c"] assms by (auto simp: field_simps)

lemma sin_rmod [simp]: "sin (x rmod (2*pi)) = sin x"
  and cos_rmod [simp]: "cos (x rmod (2*pi)) = cos x"
  by (simp_all add: rmod_def sin_diff cos_diff)

lemma tan_rmod [simp]: "tan (x rmod (2*pi)) = tan x"
  and cot_rmod [simp]: "cot (x rmod (2*pi)) = cot x"
  and cis_rmod [simp]: "cis (x rmod (2*pi)) = cis x"
  and rcis_rmod [simp]: "rcis r (x rmod (2*pi)) = rcis r x"
  by (simp_all add: tan_def cot_def complex_eq_iff)

lemma cis_eq_iff: "cis a = cis b ⟷ [a = b] (rmod (2 * pi))"
proof -
  have "cis a = cis b ⟷ sin a = sin b ∧ cos a = cos b"
    by (auto simp: complex_eq_iff)
  also have "… ⟷ (∃x. a = b + 2 * pi * real_of_int x)"
    by (rule sin_cos_eq_iff)
  also have "… ⟷ [b = a] (rmod (2 * pi))"
    by (simp add: rcong_altdef mult_ac)
  finally show ?thesis
    by (simp add: rcong_sym_iff)
qed

lemma cis_eq_1_iff: "cis a = 1 ⟷ (∃n. a = of_int n * (2 * pi))"
proof -
  have "cis 0 = cis a ⟷ [0 = a] (rmod (2 * pi))"
    by (rule cis_eq_iff)
  also have "… ⟷ (∃n. a = of_int n * (2 * pi))"
    unfolding rcong_altdef by simp
  finally show ?thesis
    by simp
qed

lemma cis_cong:
  assumes "[a = b] (rmod 2 * pi)"
  shows   "cis a = cis b"
  using cis_eq_iff assms by blast

lemma rcis_cong:
  assumes "[a = b] (rmod 2 * pi)"
  shows   "rcis r a = rcis r b"
  using assms by (auto simp: rcis_def intro!: cis_cong)

lemma sin_rcong: "[x = y] (rmod (2 * pi)) ⟹ sin x = sin y"
  and cos_rcong: "[x = y] (rmod (2 * pi)) ⟹ cos x = cos y"
  using cis_cong[of x y] by (simp_all add: complex_eq_iff)

lemma sin_eq_sin_conv_rmod:
  assumes "sin x = sin y"
  shows   "[x = y] (rmod 2 * pi) ∨ [x = pi - y] (rmod 2 * pi)"
proof -
  have "0 = sin y - sin x"
    using assms by simp
  hence "sin ((y - x) / 2) = 0 ∨ cos ((y + x) / 2) = 0"
    unfolding sin_diff_sin by simp
  hence "(∃i. y = x + real_of_int i * (2 * pi)) ∨
         (∃i. pi - y = x + real_of_int (-i) * (2 * pi))"
    unfolding sin_zero_iff_int2 cos_zero_iff_int2
    by (auto simp: algebra_simps)
  thus ?thesis
    unfolding rcong_altdef by blast
qed

lemma cos_eq_cos_conv_rmod:
  assumes "cos x = cos y"
  shows   "[x = y] (rmod 2 * pi) ∨ [x = -y] (rmod 2 * pi)"
proof -
  have "0 = cos y - cos x"
    using assms by simp
  hence "sin ((y + x) / 2) = 0 ∨ sin ((x - y) / 2) = 0"
    unfolding cos_diff_cos by simp
  hence "(∃i. -y = x + real_of_int (-i) * (2 * pi)) ∨
         (∃i. y = x + real_of_int (-i) * (2 * pi))"
    unfolding sin_zero_iff_int2
    by (auto simp: algebra_simps)
  thus ?thesis
    unfolding rcong_altdef by blast
qed

lemma sin_eq_sin_conv_rmod_iff:
  "sin x = sin y ⟷ [x = y] (rmod 2 * pi) ∨ [x = pi - y] (rmod 2 * pi)"
  by (metis sin_eq_sin_conv_rmod sin_pi_minus sin_rcong)

lemma cos_eq_cos_conv_rmod_iff:
  "cos x = cos y ⟷ [x = y] (rmod 2 * pi) ∨ [x = -y] (rmod 2 * pi)"
  by (metis cos_eq_cos_conv_rmod cos_minus cos_rcong)

end