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