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