Theory 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" (‹(1[_ = _] '(' 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)

end