Quelle Real_Mod.thy Sprache: Isabelle

(*
  File:     HOL/Library/Real_Mod.thy
  Authors:  Manuel Eberl, University of Innsbruck
*)
section \<open>Modulo and congruence on the reals\<close>
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\\ +
       \<lfloor>(x + y - (\<bar>z\<bar> * real_of_int \<lfloor>x / \<bar>z\<bar>\<rfloor> + \<bar>z\<bar> * real_of_int \<lfloor>y / \<bar>z\<bar>\<rfloor>)) / \<bar>z\<bar>\<rfloor>)"
    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\\ +
      \<lfloor>(x + \<bar>z\<bar> * real_of_int \<lfloor>y / \<bar>z\<bar>\<rfloor> - (y + \<bar>z\<bar> * real_of_int \<lfloor>x / \<bar>z\<bar>\<rfloor>)) / \<bar>z\<bar>\<rfloor> - \<lfloor>y / \<bar>z\<bar>\<rfloor>)"
    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"
    (\<open>(\<open>indent=1 notation=\<open>mixfix rcong\<close>\<close>[_ = _] '(' rmod _'))\<close>)
  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)) \
         (\<exists>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)) \
         (\<exists>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

quality100%

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.