1(* Title: HOL/Library/Periodic_Fun.thy 2 Author: Manuel Eberl, TU M��nchen 3*) 4 5section \<open>Periodic Functions\<close> 6 7theory Periodic_Fun 8imports Complex_Main 9begin 10 11text \<open> 12 A locale for periodic functions. The idea is that one proves $f(x + p) = f(x)$ 13 for some period $p$ and gets derived results like $f(x - p) = f(x)$ and $f(x + 2p) = f(x)$ 14 for free. 15 16 @{term g} and @{term gm} are ``plus/minus k periods'' functions. 17 @{term g1} and @{term gn1} are ``plus/minus one period'' functions. 18 This is useful e.g. if the period is one; the lemmas one gets are then 19 @{term "f (x + 1) = f x"} instead of @{term "f (x + 1 * 1) = f x"} etc. 20\<close> 21locale periodic_fun = 22 fixes f :: "('a :: {ring_1}) \<Rightarrow> 'b" and g gm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" and g1 gn1 :: "'a \<Rightarrow> 'a" 23 assumes plus_1: "f (g1 x) = f x" 24 assumes periodic_arg_plus_0: "g x 0 = x" 25 assumes periodic_arg_plus_distrib: "g x (of_int (m + n)) = g (g x (of_int n)) (of_int m)" 26 assumes plus_1_eq: "g x 1 = g1 x" and minus_1_eq: "g x (-1) = gn1 x" 27 and minus_eq: "g x (-y) = gm x y" 28begin 29 30lemma plus_of_nat: "f (g x (of_nat n)) = f x" 31 by (induction n) (insert periodic_arg_plus_distrib[of _ 1 "int n" for n], 32 simp_all add: plus_1 periodic_arg_plus_0 plus_1_eq) 33 34lemma minus_of_nat: "f (gm x (of_nat n)) = f x" 35proof - 36 have "f (g x (- of_nat n)) = f (g (g x (- of_nat n)) (of_nat n))" 37 by (rule plus_of_nat[symmetric]) 38 also have "\<dots> = f (g (g x (of_int (- of_nat n))) (of_int (of_nat n)))" by simp 39 also have "\<dots> = f x" 40 by (subst periodic_arg_plus_distrib [symmetric]) (simp add: periodic_arg_plus_0) 41 finally show ?thesis by (simp add: minus_eq) 42qed 43 44lemma plus_of_int: "f (g x (of_int n)) = f x" 45 by (induction n) (simp_all add: plus_of_nat minus_of_nat minus_eq del: of_nat_Suc) 46 47lemma minus_of_int: "f (gm x (of_int n)) = f x" 48 using plus_of_int[of x "of_int (-n)"] by (simp add: minus_eq) 49 50lemma plus_numeral: "f (g x (numeral n)) = f x" 51 by (subst of_nat_numeral[symmetric], subst plus_of_nat) (rule refl) 52 53lemma minus_numeral: "f (gm x (numeral n)) = f x" 54 by (subst of_nat_numeral[symmetric], subst minus_of_nat) (rule refl) 55 56lemma minus_1: "f (gn1 x) = f x" 57 using minus_of_nat[of x 1] by (simp flip: minus_1_eq minus_eq) 58 59lemmas periodic_simps = plus_of_nat minus_of_nat plus_of_int minus_of_int 60 plus_numeral minus_numeral plus_1 minus_1 61 62end 63 64 65text \<open> 66 Specialised case of the @{term periodic_fun} locale for periods that are not 1. 67 Gives lemmas @{term "f (x - period) = f x"} etc. 68\<close> 69locale periodic_fun_simple = 70 fixes f :: "('a :: {ring_1}) \<Rightarrow> 'b" and period :: 'a 71 assumes plus_period: "f (x + period) = f x" 72begin 73sublocale periodic_fun f "\<lambda>z x. z + x * period" "\<lambda>z x. z - x * period" 74 "\<lambda>z. z + period" "\<lambda>z. z - period" 75 by standard (simp_all add: ring_distribs plus_period) 76end 77 78 79text \<open> 80 Specialised case of the @{term periodic_fun} locale for period 1. 81 Gives lemmas @{term "f (x - 1) = f x"} etc. 82\<close> 83locale periodic_fun_simple' = 84 fixes f :: "('a :: {ring_1}) \<Rightarrow> 'b" 85 assumes plus_period: "f (x + 1) = f x" 86begin 87sublocale periodic_fun f "\<lambda>z x. z + x" "\<lambda>z x. z - x" "\<lambda>z. z + 1" "\<lambda>z. z - 1" 88 by standard (simp_all add: ring_distribs plus_period) 89 90lemma of_nat: "f (of_nat n) = f 0" using plus_of_nat[of 0 n] by simp 91lemma uminus_of_nat: "f (-of_nat n) = f 0" using minus_of_nat[of 0 n] by simp 92lemma of_int: "f (of_int n) = f 0" using plus_of_int[of 0 n] by simp 93lemma uminus_of_int: "f (-of_int n) = f 0" using minus_of_int[of 0 n] by simp 94lemma of_numeral: "f (numeral n) = f 0" using plus_numeral[of 0 n] by simp 95lemma of_neg_numeral: "f (-numeral n) = f 0" using minus_numeral[of 0 n] by simp 96lemma of_1: "f 1 = f 0" using plus_of_nat[of 0 1] by simp 97lemma of_neg_1: "f (-1) = f 0" using minus_of_nat[of 0 1] by simp 98 99lemmas periodic_simps' = 100 of_nat uminus_of_nat of_int uminus_of_int of_numeral of_neg_numeral of_1 of_neg_1 101 102end 103 104lemma sin_plus_pi: "sin ((z :: 'a :: {real_normed_field,banach}) + of_real pi) = - sin z" 105 by (simp add: sin_add) 106 107lemma cos_plus_pi: "cos ((z :: 'a :: {real_normed_field,banach}) + of_real pi) = - cos z" 108 by (simp add: cos_add) 109 110interpretation sin: periodic_fun_simple sin "2 * of_real pi :: 'a :: {real_normed_field,banach}" 111proof 112 fix z :: 'a 113 have "sin (z + 2 * of_real pi) = sin (z + of_real pi + of_real pi)" by (simp add: ac_simps) 114 also have "\<dots> = sin z" by (simp only: sin_plus_pi) simp 115 finally show "sin (z + 2 * of_real pi) = sin z" . 116qed 117 118interpretation cos: periodic_fun_simple cos "2 * of_real pi :: 'a :: {real_normed_field,banach}" 119proof 120 fix z :: 'a 121 have "cos (z + 2 * of_real pi) = cos (z + of_real pi + of_real pi)" by (simp add: ac_simps) 122 also have "\<dots> = cos z" by (simp only: cos_plus_pi) simp 123 finally show "cos (z + 2 * of_real pi) = cos z" . 124qed 125 126interpretation tan: periodic_fun_simple tan "2 * of_real pi :: 'a :: {real_normed_field,banach}" 127 by standard (simp only: tan_def [abs_def] sin.plus_1 cos.plus_1) 128 129interpretation cot: periodic_fun_simple cot "2 * of_real pi :: 'a :: {real_normed_field,banach}" 130 by standard (simp only: cot_def [abs_def] sin.plus_1 cos.plus_1) 131 132end 133