Quelle Periodic_Fun.thy Sprache: Isabelle

(*  Title:    HOL/Library/Periodic_Fun.thy
    Author:   Manuel Eberl, TU München
*)

section \<open>Periodic Functions\<close>

theory Periodic_Fun
imports Complex_Main
begin

text \<open>
  A locale for periodic functions. The idea is that one proves $f(x + p) = f(x)$
  for some period $p$ and gets derived results like $f(x - p) = f(x)$ and $f(x + 2p) = f(x)$
  for free.

  \<^term>\<open>g\<close> and \<^term>\<open>gm\<close> are ``plus/minus k periods'' functions.
  \<^term>\<open>g1\<close> and \<^term>\<open>gn1\<close> are ``plus/minus one period'' functions.
  This is useful e.g. if the period is one; the lemmas one gets are then
  \<^term>\<open>f (x + 1) = f x\<close> instead of \<^term>\<open>f (x + 1 * 1) = f x\<close> etc.
\<close>
locale periodic_fun =
  fixes f :: "('a :: {ring_1}) \ 'b" and g gm :: "'a \ 'a \ 'a" and g1 gn1 :: "'a \ 'a"
  assumes plus_1: "f (g1 x) = f x"
  assumes periodic_arg_plus_0: "g x 0 = x"
  assumes periodic_arg_plus_distrib: "g x (of_int (m + n)) = g (g x (of_int n)) (of_int m)"
  assumes plus_1_eq: "g x 1 = g1 x" and minus_1_eq: "g x (-1) = gn1 x"
          and minus_eq: "g x (-y) = gm x y"
begin

lemma plus_of_nat: "f (g x (of_nat n)) = f x"
  by (induction n) (insert periodic_arg_plus_distrib[of _ 1 "int n" for n],
                    simp_all add: plus_1 periodic_arg_plus_0 plus_1_eq)

lemma minus_of_nat: "f (gm x (of_nat n)) = f x"
proof -
  have "f (g x (- of_nat n)) = f (g (g x (- of_nat n)) (of_nat n))"
    by (rule plus_of_nat[symmetric])
  also have "\ = f (g (g x (of_int (- of_nat n))) (of_int (of_nat n)))" by simp
  also have "\ = f x"
    by (subst periodic_arg_plus_distrib [symmetric]) (simp add: periodic_arg_plus_0)
  finally show ?thesis by (simp add: minus_eq)
qed

lemma plus_of_int: "f (g x (of_int n)) = f x"
  by (induction n) (simp_all add: plus_of_nat minus_of_nat minus_eq del: of_nat_Suc)

lemma minus_of_int: "f (gm x (of_int n)) = f x"
  using plus_of_int[of x "of_int (-n)"] by (simp add: minus_eq)

lemma plus_numeral: "f (g x (numeral n)) = f x"
  by (subst of_nat_numeral[symmetric], subst plus_of_nat) (rule refl)

lemma minus_numeral: "f (gm x (numeral n)) = f x"
  by (subst of_nat_numeral[symmetric], subst minus_of_nat) (rule refl)

lemma minus_1: "f (gn1 x) = f x"
  using minus_of_nat[of x 1] by (simp flip: minus_1_eq minus_eq)

lemmas periodic_simps = plus_of_nat minus_of_nat plus_of_int minus_of_int
                        plus_numeral minus_numeral plus_1 minus_1

end

text \<open>
  Specialised case of the \<^term>\<open>periodic_fun\<close> locale for periods that are not 1.
  Gives lemmas \<^term>\<open>f (x - period) = f x\<close> etc.
\<close>
locale periodic_fun_simple =
  fixes f :: "('a :: {ring_1}) \ 'b" and period :: 'a
  assumes plus_period: "f (x + period) = f x"
begin
sublocale periodic_fun f "\z x. z + x * period" "\z x. z - x * period"
  "\z. z + period" "\z. z - period"
  by standard (simp_all add: ring_distribs plus_period)
end

text \<open>
  Specialised case of the \<^term>\<open>periodic_fun\<close> locale for period 1.
  Gives lemmas \<^term>\<open>f (x - 1) = f x\<close> etc.
\<close>
locale periodic_fun_simple' =
  fixes f :: "('a :: {ring_1}) \ 'b"
  assumes plus_period: "f (x + 1) = f x"
begin
sublocale periodic_fun f "\z x. z + x" "\z x. z - x" "\z. z + 1" "\z. z - 1"
  by standard (simp_all add: ring_distribs plus_period)

lemma of_nat: "f (of_nat n) = f 0" using plus_of_nat[of 0 n] by simp
lemma uminus_of_nat: "f (-of_nat n) = f 0" using minus_of_nat[of 0 n] by simp
lemma of_int: "f (of_int n) = f 0" using plus_of_int[of 0 n] by simp
lemma uminus_of_int: "f (-of_int n) = f 0" using minus_of_int[of 0 n] by simp
lemma of_numeral: "f (numeral n) = f 0" using plus_numeral[of 0 n] by simp
lemma of_neg_numeral: "f (-numeral n) = f 0" using minus_numeral[of 0 n] by simp
lemma of_1: "f 1 = f 0" using plus_of_nat[of 0 1] by simp
lemma of_neg_1: "f (-1) = f 0" using minus_of_nat[of 0 1] by simp

lemmas periodic_simps' =
  of_nat uminus_of_nat of_int uminus_of_int of_numeral of_neg_numeral of_1 of_neg_1

end

lemma sin_plus_pi: "sin ((z :: 'a :: {real_normed_field,banach}) + of_real pi) = - sin z"
  by (simp add: sin_add)

lemma cos_plus_pi: "cos ((z :: 'a :: {real_normed_field,banach}) + of_real pi) = - cos z"
  by (simp add: cos_add)

interpretation sin: periodic_fun_simple sin "2 * of_real pi :: 'a :: {real_normed_field,banach}"
proof
  fix z :: 'a
  have "sin (z + 2 * of_real pi) = sin (z + of_real pi + of_real pi)" by (simp add: ac_simps)
  also have "\ = sin z" by (simp only: sin_plus_pi) simp
  finally show "sin (z + 2 * of_real pi) = sin z" .
qed

interpretation cos: periodic_fun_simple cos "2 * of_real pi :: 'a :: {real_normed_field,banach}"
proof
  fix z :: 'a
  have "cos (z + 2 * of_real pi) = cos (z + of_real pi + of_real pi)" by (simp add: ac_simps)
  also have "\ = cos z" by (simp only: cos_plus_pi) simp
  finally show "cos (z + 2 * of_real pi) = cos z" .
qed

interpretation tan: periodic_fun_simple tan "2 * of_real pi :: 'a :: {real_normed_field,banach}"
  by standard (simp only: tan_def [abs_def] sin.plus_1 cos.plus_1)

interpretation cot: periodic_fun_simple cot "2 * of_real pi :: 'a :: {real_normed_field,banach}"
  by standard (simp only: cot_def [abs_def] sin.plus_1 cos.plus_1)

lemma cos_eq_neg_periodic_intro:
  assumes "x - y = 2*(of_int k)*pi + pi \ x + y = 2*(of_int k)*pi + pi"
  shows "cos x = - cos y" using assms
proof
  assume "x - y = 2 * (of_int k) * pi + pi"
  then show ?thesis
    using cos.periodic_simps[of "y+pi"]
    by (auto simp add:algebra_simps)
next
  assume "x + y = 2 * real_of_int k * pi + pi "
  then show ?thesis
    using cos.periodic_simps[of "-y+pi"]
    by (clarsimp simp add: algebra_simps) (smt (verit))
qed

lemma cos_eq_periodic_intro:
  assumes "x - y = 2*(of_int k)*pi \ x + y = 2*(of_int k)*pi"
  shows "cos x = cos y"
  by (smt (verit, best) assms cos_eq_neg_periodic_intro cos_minus_pi cos_periodic_pi)

lemma cos_eq_arccos_Ex:
  "cos x = y \ -1\y \ y\1 \ (\k::int. x = arccos y + 2*k*pi \ x = - arccos y + 2*k*pi)" (is "?L=?R")
proof
  assume ?R then show "cos x = y"
    by (metis cos.plus_of_int cos_arccos cos_minus id_apply mult.assoc mult.left_commute of_real_eq_id)
next
  assume L: ?L
  let ?goal = "(\k::int. x = arccos y + 2*k*pi \ x = - arccos y + 2*k*pi)"
  obtain k::int where k: "-pi < x - k*(2*pi)" "x - k*(2*pi) \ pi"
    using ceiling_divide_lower [of "2*pi" "x-pi"] ceiling_divide_upper [of "2*pi" "x-pi"]
    by (simp add: divide_simps algebra_simps) (metis mult.commute)
  have *: "cos (x - k * 2*pi) = y"
    using cos.periodic_simps(3)[of x "-k"] L by (auto simp add:field_simps)
  then have **: ?goal when "x-k*2*pi \ 0"
    using arccos_cos k that by force
  then show "-1\y \ y\1 \ ?goal"
    using "*" arccos_cos2 k(1) by force
qed

end

quality98%

¤ 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.