src/HOL/Library/Periodic_Fun.thy
changeset 62049 b0f941e207cf
child 62055 755fda743c49
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Periodic_Fun.thy	Mon Jan 04 17:45:36 2016 +0100
     1.3 @@ -0,0 +1,130 @@
     1.4 +(*
     1.5 +  Title:    HOL/Library/Periodic_Fun.thy
     1.6 +  Author:   Manuel Eberl, TU M√ľnchen
     1.7 +  
     1.8 +  A locale for periodic functions. The idea is that one proves $f(x + p) = f(x)$
     1.9 +  for some period $p$ and gets derived results like $f(x - p) = f(x)$ and $f(x + 2p) = f(x)$
    1.10 +  for free.
    1.11 +*)
    1.12 +theory Periodic_Fun
    1.13 +imports Complex_Main
    1.14 +begin
    1.15 +
    1.16 +text \<open>
    1.17 +  @{term g} and @{term gm} are ``plus/minus k periods'' functions. 
    1.18 +  @{term g1} and @{term gn1} are ``plus/minus one period'' functions.
    1.19 +  This is useful e.g. if the period is one; the lemmas one gets are then 
    1.20 +  @{term "f (x + 1) = f x"} instead of @{term "f (x + 1 * 1) = f x"} etc.
    1.21 +\<close>
    1.22 +locale periodic_fun = 
    1.23 +  fixes f :: "('a :: {ring_1}) \<Rightarrow> 'b" and g gm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" and g1 gn1 :: "'a \<Rightarrow> 'a"
    1.24 +  assumes plus_1: "f (g1 x) = f x"
    1.25 +  assumes periodic_arg_plus_0: "g x 0 = x"
    1.26 +  assumes periodic_arg_plus_distrib: "g x (of_int (m + n)) = g (g x (of_int n)) (of_int m)"
    1.27 +  assumes plus_1_eq: "g x 1 = g1 x" and minus_1_eq: "g x (-1) = gn1 x" 
    1.28 +          and minus_eq: "g x (-y) = gm x y"
    1.29 +begin
    1.30 +
    1.31 +lemma plus_of_nat: "f (g x (of_nat n)) = f x"
    1.32 +  by (induction n) (insert periodic_arg_plus_distrib[of _ 1 "int n" for n], 
    1.33 +                    simp_all add: plus_1 periodic_arg_plus_0 plus_1_eq)
    1.34 +
    1.35 +lemma minus_of_nat: "f (gm x (of_nat n)) = f x"
    1.36 +proof -
    1.37 +  have "f (g x (- of_nat n)) = f (g (g x (- of_nat n)) (of_nat n))"
    1.38 +    by (rule plus_of_nat[symmetric])
    1.39 +  also have "\<dots> = f (g (g x (of_int (- of_nat n))) (of_int (of_nat n)))" by simp
    1.40 +  also have "\<dots> = f x" 
    1.41 +    by (subst periodic_arg_plus_distrib [symmetric]) (simp add: periodic_arg_plus_0)
    1.42 +  finally show ?thesis by (simp add: minus_eq)
    1.43 +qed
    1.44 +
    1.45 +lemma plus_of_int: "f (g x (of_int n)) = f x"
    1.46 +  by (induction n) (simp_all add: plus_of_nat minus_of_nat minus_eq del: of_nat_Suc)
    1.47 +
    1.48 +lemma minus_of_int: "f (gm x (of_int n)) = f x"
    1.49 +  using plus_of_int[of x "of_int (-n)"] by (simp add: minus_eq)
    1.50 +
    1.51 +lemma plus_numeral: "f (g x (numeral n)) = f x"
    1.52 +  by (subst of_nat_numeral[symmetric], subst plus_of_nat) (rule refl)
    1.53 +
    1.54 +lemma minus_numeral: "f (gm x (numeral n)) = f x"
    1.55 +  by (subst of_nat_numeral[symmetric], subst minus_of_nat) (rule refl)
    1.56 +
    1.57 +lemma minus_1: "f (gn1 x) = f x"
    1.58 +  using minus_of_nat[of x 1] by (simp add: minus_1_eq minus_eq[symmetric])
    1.59 +
    1.60 +lemmas periodic_simps = plus_of_nat minus_of_nat plus_of_int minus_of_int 
    1.61 +                        plus_numeral minus_numeral plus_1 minus_1
    1.62 +
    1.63 +end
    1.64 +
    1.65 +
    1.66 +text \<open>
    1.67 +  Specialised case of the @{term periodic_fun} locale for periods that are not 1.
    1.68 +  Gives lemmas @{term "f (x - period) = f x"} etc.
    1.69 +\<close>
    1.70 +locale periodic_fun_simple = 
    1.71 +  fixes f :: "('a :: {ring_1}) \<Rightarrow> 'b" and period :: 'a
    1.72 +  assumes plus_period: "f (x + period) = f x"
    1.73 +begin
    1.74 +sublocale periodic_fun f "\<lambda>z x. z + x * period" "\<lambda>z x. z - x * period" 
    1.75 +  "\<lambda>z. z + period" "\<lambda>z. z - period"
    1.76 +  by standard (simp_all add: ring_distribs plus_period)
    1.77 +end
    1.78 +
    1.79 +
    1.80 +text \<open>
    1.81 +  Specialised case of the @{term periodic_fun} locale for period 1.
    1.82 +  Gives lemmas @{term "f (x - 1) = f x"} etc.
    1.83 +\<close>
    1.84 +locale periodic_fun_simple' = 
    1.85 +  fixes f :: "('a :: {ring_1}) \<Rightarrow> 'b"
    1.86 +  assumes plus_period: "f (x + 1) = f x"
    1.87 +begin
    1.88 +sublocale periodic_fun f "\<lambda>z x. z + x" "\<lambda>z x. z - x" "\<lambda>z. z + 1" "\<lambda>z. z - 1"
    1.89 +  by standard (simp_all add: ring_distribs plus_period)
    1.90 +
    1.91 +lemma of_nat: "f (of_nat n) = f 0" using plus_of_nat[of 0 n] by simp
    1.92 +lemma uminus_of_nat: "f (-of_nat n) = f 0" using minus_of_nat[of 0 n] by simp
    1.93 +lemma of_int: "f (of_int n) = f 0" using plus_of_int[of 0 n] by simp
    1.94 +lemma uminus_of_int: "f (-of_int n) = f 0" using minus_of_int[of 0 n] by simp
    1.95 +lemma of_numeral: "f (numeral n) = f 0" using plus_numeral[of 0 n] by simp
    1.96 +lemma of_neg_numeral: "f (-numeral n) = f 0" using minus_numeral[of 0 n] by simp
    1.97 +lemma of_1: "f 1 = f 0" using plus_of_nat[of 0 1] by simp
    1.98 +lemma of_neg_1: "f (-1) = f 0" using minus_of_nat[of 0 1] by simp
    1.99 +
   1.100 +lemmas periodic_simps' = 
   1.101 +  of_nat uminus_of_nat of_int uminus_of_int of_numeral of_neg_numeral of_1 of_neg_1
   1.102 +
   1.103 +end
   1.104 +
   1.105 +lemma sin_plus_pi: "sin ((z :: 'a :: {real_normed_field,banach}) + of_real pi) = - sin z"
   1.106 +  by (simp add: sin_add)
   1.107 +  
   1.108 +lemma cos_plus_pi: "cos ((z :: 'a :: {real_normed_field,banach}) + of_real pi) = - cos z"
   1.109 +  by (simp add: cos_add)
   1.110 +
   1.111 +interpretation sin: periodic_fun_simple sin "2 * of_real pi :: 'a :: {real_normed_field,banach}"
   1.112 +proof
   1.113 +  fix z :: 'a
   1.114 +  have "sin (z + 2 * of_real pi) = sin (z + of_real pi + of_real pi)" by (simp add: ac_simps)
   1.115 +  also have "\<dots> = sin z" by (simp only: sin_plus_pi) simp
   1.116 +  finally show "sin (z + 2 * of_real pi) = sin z" .
   1.117 +qed
   1.118 +
   1.119 +interpretation cos: periodic_fun_simple cos "2 * of_real pi :: 'a :: {real_normed_field,banach}"
   1.120 +proof
   1.121 +  fix z :: 'a
   1.122 +  have "cos (z + 2 * of_real pi) = cos (z + of_real pi + of_real pi)" by (simp add: ac_simps)
   1.123 +  also have "\<dots> = cos z" by (simp only: cos_plus_pi) simp
   1.124 +  finally show "cos (z + 2 * of_real pi) = cos z" .
   1.125 +qed
   1.126 +
   1.127 +interpretation tan: periodic_fun_simple tan "2 * of_real pi :: 'a :: {real_normed_field,banach}"
   1.128 +  by standard (simp only: tan_def [abs_def] sin.plus_1 cos.plus_1)
   1.129 +
   1.130 +interpretation cot: periodic_fun_simple cot "2 * of_real pi :: 'a :: {real_normed_field,banach}"
   1.131 +  by standard (simp only: cot_def [abs_def] sin.plus_1 cos.plus_1)
   1.132 +  
   1.133 +end
   1.134 \ No newline at end of file