src/HOL/Library/Periodic_Fun.thy
 author hoelzl Tue Jan 05 13:35:06 2016 +0100 (2016-01-05) changeset 62055 755fda743c49 parent 62049 b0f941e207cf child 62390 842917225d56 permissions -rw-r--r--
Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
```     1 (*  Title:    HOL/Library/Periodic_Fun.thy
```
```     2     Author:   Manuel Eberl, TU München
```
```     3 *)
```
```     4
```
```     5 section \<open>Periodic Functions\<close>
```
```     6
```
```     7 theory Periodic_Fun
```
```     8 imports Complex_Main
```
```     9 begin
```
```    10
```
```    11 text \<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>
```
```    21 locale 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"
```
```    28 begin
```
```    29
```
```    30 lemma 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
```
```    34 lemma minus_of_nat: "f (gm x (of_nat n)) = f x"
```
```    35 proof -
```
```    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)
```
```    42 qed
```
```    43
```
```    44 lemma 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
```
```    47 lemma 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
```
```    50 lemma plus_numeral: "f (g x (numeral n)) = f x"
```
```    51   by (subst of_nat_numeral[symmetric], subst plus_of_nat) (rule refl)
```
```    52
```
```    53 lemma minus_numeral: "f (gm x (numeral n)) = f x"
```
```    54   by (subst of_nat_numeral[symmetric], subst minus_of_nat) (rule refl)
```
```    55
```
```    56 lemma minus_1: "f (gn1 x) = f x"
```
```    57   using minus_of_nat[of x 1] by (simp add: minus_1_eq minus_eq[symmetric])
```
```    58
```
```    59 lemmas periodic_simps = plus_of_nat minus_of_nat plus_of_int minus_of_int
```
```    60                         plus_numeral minus_numeral plus_1 minus_1
```
```    61
```
```    62 end
```
```    63
```
```    64
```
```    65 text \<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>
```
```    69 locale periodic_fun_simple =
```
```    70   fixes f :: "('a :: {ring_1}) \<Rightarrow> 'b" and period :: 'a
```
```    71   assumes plus_period: "f (x + period) = f x"
```
```    72 begin
```
```    73 sublocale 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)
```
```    76 end
```
```    77
```
```    78
```
```    79 text \<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>
```
```    83 locale periodic_fun_simple' =
```
```    84   fixes f :: "('a :: {ring_1}) \<Rightarrow> 'b"
```
```    85   assumes plus_period: "f (x + 1) = f x"
```
```    86 begin
```
```    87 sublocale 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
```
```    90 lemma of_nat: "f (of_nat n) = f 0" using plus_of_nat[of 0 n] by simp
```
```    91 lemma uminus_of_nat: "f (-of_nat n) = f 0" using minus_of_nat[of 0 n] by simp
```
```    92 lemma of_int: "f (of_int n) = f 0" using plus_of_int[of 0 n] by simp
```
```    93 lemma uminus_of_int: "f (-of_int n) = f 0" using minus_of_int[of 0 n] by simp
```
```    94 lemma of_numeral: "f (numeral n) = f 0" using plus_numeral[of 0 n] by simp
```
```    95 lemma of_neg_numeral: "f (-numeral n) = f 0" using minus_numeral[of 0 n] by simp
```
```    96 lemma of_1: "f 1 = f 0" using plus_of_nat[of 0 1] by simp
```
```    97 lemma of_neg_1: "f (-1) = f 0" using minus_of_nat[of 0 1] by simp
```
```    98
```
```    99 lemmas periodic_simps' =
```
```   100   of_nat uminus_of_nat of_int uminus_of_int of_numeral of_neg_numeral of_1 of_neg_1
```
```   101
```
```   102 end
```
```   103
```
```   104 lemma sin_plus_pi: "sin ((z :: 'a :: {real_normed_field,banach}) + of_real pi) = - sin z"
```
```   105   by (simp add: sin_add)
```
```   106
```
```   107 lemma cos_plus_pi: "cos ((z :: 'a :: {real_normed_field,banach}) + of_real pi) = - cos z"
```
```   108   by (simp add: cos_add)
```
```   109
```
```   110 interpretation sin: periodic_fun_simple sin "2 * of_real pi :: 'a :: {real_normed_field,banach}"
```
```   111 proof
```
```   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" .
```
```   116 qed
```
```   117
```
```   118 interpretation cos: periodic_fun_simple cos "2 * of_real pi :: 'a :: {real_normed_field,banach}"
```
```   119 proof
```
```   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" .
```
```   124 qed
```
```   125
```
```   126 interpretation 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
```
```   129 interpretation 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
```
`   132 end`