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