author  nipkow 
Tue, 23 Feb 2016 16:25:08 +0100  
changeset 62390  842917225d56 
parent 62055  755fda743c49 
child 68406  6beb45f6cf67 
permissions  rwrr 
62055
755fda743c49
MultivariateAnalysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset

1 
(* Title: HOL/Library/Periodic_Fun.thy 
755fda743c49
MultivariateAnalysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset

2 
Author: Manuel Eberl, TU München 
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

3 
*) 
62055
755fda743c49
MultivariateAnalysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset

4 

755fda743c49
MultivariateAnalysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset

5 
section \<open>Periodic Functions\<close> 
755fda743c49
MultivariateAnalysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset

6 

62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

7 
theory Periodic_Fun 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

8 
imports Complex_Main 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

9 
begin 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

10 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

11 
text \<open> 
62055
755fda743c49
MultivariateAnalysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset

12 
A locale for periodic functions. The idea is that one proves $f(x + p) = f(x)$ 
755fda743c49
MultivariateAnalysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset

13 
for some period $p$ and gets derived results like $f(x  p) = f(x)$ and $f(x + 2p) = f(x)$ 
755fda743c49
MultivariateAnalysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset

14 
for free. 
755fda743c49
MultivariateAnalysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset

15 

62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

16 
@{term g} and @{term gm} are ``plus/minus k periods'' functions. 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

17 
@{term g1} and @{term gn1} are ``plus/minus one period'' functions. 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

18 
This is useful e.g. if the period is one; the lemmas one gets are then 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

19 
@{term "f (x + 1) = f x"} instead of @{term "f (x + 1 * 1) = f x"} etc. 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

20 
\<close> 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

21 
locale periodic_fun = 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

22 
fixes f :: "('a :: {ring_1}) \<Rightarrow> 'b" and g gm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" and g1 gn1 :: "'a \<Rightarrow> 'a" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

23 
assumes plus_1: "f (g1 x) = f x" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

24 
assumes periodic_arg_plus_0: "g x 0 = x" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

25 
assumes periodic_arg_plus_distrib: "g x (of_int (m + n)) = g (g x (of_int n)) (of_int m)" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

26 
assumes plus_1_eq: "g x 1 = g1 x" and minus_1_eq: "g x (1) = gn1 x" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

27 
and minus_eq: "g x (y) = gm x y" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

28 
begin 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

29 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

30 
lemma plus_of_nat: "f (g x (of_nat n)) = f x" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

31 
by (induction n) (insert periodic_arg_plus_distrib[of _ 1 "int n" for n], 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

32 
simp_all add: plus_1 periodic_arg_plus_0 plus_1_eq) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

33 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

34 
lemma minus_of_nat: "f (gm x (of_nat n)) = f x" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

35 
proof  
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

36 
have "f (g x ( of_nat n)) = f (g (g x ( of_nat n)) (of_nat n))" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

37 
by (rule plus_of_nat[symmetric]) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

38 
also have "\<dots> = f (g (g x (of_int ( of_nat n))) (of_int (of_nat n)))" by simp 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

39 
also have "\<dots> = f x" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

40 
by (subst periodic_arg_plus_distrib [symmetric]) (simp add: periodic_arg_plus_0) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

41 
finally show ?thesis by (simp add: minus_eq) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

42 
qed 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

43 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

44 
lemma plus_of_int: "f (g x (of_int n)) = f x" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

45 
by (induction n) (simp_all add: plus_of_nat minus_of_nat minus_eq del: of_nat_Suc) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

46 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

47 
lemma minus_of_int: "f (gm x (of_int n)) = f x" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

48 
using plus_of_int[of x "of_int (n)"] by (simp add: minus_eq) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

49 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

50 
lemma plus_numeral: "f (g x (numeral n)) = f x" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

51 
by (subst of_nat_numeral[symmetric], subst plus_of_nat) (rule refl) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

52 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

53 
lemma minus_numeral: "f (gm x (numeral n)) = f x" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

54 
by (subst of_nat_numeral[symmetric], subst minus_of_nat) (rule refl) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

55 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

56 
lemma minus_1: "f (gn1 x) = f x" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

57 
using minus_of_nat[of x 1] by (simp add: minus_1_eq minus_eq[symmetric]) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

58 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

59 
lemmas periodic_simps = plus_of_nat minus_of_nat plus_of_int minus_of_int 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

60 
plus_numeral minus_numeral plus_1 minus_1 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

61 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

62 
end 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

63 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

64 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

65 
text \<open> 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

66 
Specialised case of the @{term periodic_fun} locale for periods that are not 1. 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

67 
Gives lemmas @{term "f (x  period) = f x"} etc. 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

68 
\<close> 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

69 
locale periodic_fun_simple = 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

70 
fixes f :: "('a :: {ring_1}) \<Rightarrow> 'b" and period :: 'a 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

71 
assumes plus_period: "f (x + period) = f x" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

72 
begin 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

73 
sublocale periodic_fun f "\<lambda>z x. z + x * period" "\<lambda>z x. z  x * period" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

74 
"\<lambda>z. z + period" "\<lambda>z. z  period" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

75 
by standard (simp_all add: ring_distribs plus_period) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

76 
end 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

77 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

78 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

79 
text \<open> 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

80 
Specialised case of the @{term periodic_fun} locale for period 1. 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

81 
Gives lemmas @{term "f (x  1) = f x"} etc. 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

82 
\<close> 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

83 
locale periodic_fun_simple' = 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

84 
fixes f :: "('a :: {ring_1}) \<Rightarrow> 'b" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

85 
assumes plus_period: "f (x + 1) = f x" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

86 
begin 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

87 
sublocale periodic_fun f "\<lambda>z x. z + x" "\<lambda>z x. z  x" "\<lambda>z. z + 1" "\<lambda>z. z  1" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

88 
by standard (simp_all add: ring_distribs plus_period) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

89 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

90 
lemma of_nat: "f (of_nat n) = f 0" using plus_of_nat[of 0 n] by simp 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

91 
lemma uminus_of_nat: "f (of_nat n) = f 0" using minus_of_nat[of 0 n] by simp 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

92 
lemma of_int: "f (of_int n) = f 0" using plus_of_int[of 0 n] by simp 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

93 
lemma uminus_of_int: "f (of_int n) = f 0" using minus_of_int[of 0 n] by simp 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

94 
lemma of_numeral: "f (numeral n) = f 0" using plus_numeral[of 0 n] by simp 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

95 
lemma of_neg_numeral: "f (numeral n) = f 0" using minus_numeral[of 0 n] by simp 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

96 
lemma of_1: "f 1 = f 0" using plus_of_nat[of 0 1] by simp 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

97 
lemma of_neg_1: "f (1) = f 0" using minus_of_nat[of 0 1] by simp 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

98 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

99 
lemmas periodic_simps' = 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

100 
of_nat uminus_of_nat of_int uminus_of_int of_numeral of_neg_numeral of_1 of_neg_1 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

101 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

102 
end 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

103 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

104 
lemma sin_plus_pi: "sin ((z :: 'a :: {real_normed_field,banach}) + of_real pi) =  sin z" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

105 
by (simp add: sin_add) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

106 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

107 
lemma cos_plus_pi: "cos ((z :: 'a :: {real_normed_field,banach}) + of_real pi) =  cos z" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

108 
by (simp add: cos_add) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

109 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

110 
interpretation sin: periodic_fun_simple sin "2 * of_real pi :: 'a :: {real_normed_field,banach}" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

111 
proof 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

112 
fix z :: 'a 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

113 
have "sin (z + 2 * of_real pi) = sin (z + of_real pi + of_real pi)" by (simp add: ac_simps) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

114 
also have "\<dots> = sin z" by (simp only: sin_plus_pi) simp 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

115 
finally show "sin (z + 2 * of_real pi) = sin z" . 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

116 
qed 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

117 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

118 
interpretation cos: periodic_fun_simple cos "2 * of_real pi :: 'a :: {real_normed_field,banach}" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

119 
proof 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

120 
fix z :: 'a 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

121 
have "cos (z + 2 * of_real pi) = cos (z + of_real pi + of_real pi)" by (simp add: ac_simps) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

122 
also have "\<dots> = cos z" by (simp only: cos_plus_pi) simp 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

123 
finally show "cos (z + 2 * of_real pi) = cos z" . 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

124 
qed 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

125 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

126 
interpretation tan: periodic_fun_simple tan "2 * of_real pi :: 'a :: {real_normed_field,banach}" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

127 
by standard (simp only: tan_def [abs_def] sin.plus_1 cos.plus_1) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

128 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

129 
interpretation cot: periodic_fun_simple cot "2 * of_real pi :: 'a :: {real_normed_field,banach}" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

130 
by standard (simp only: cot_def [abs_def] sin.plus_1 cos.plus_1) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

131 

62390  132 
end 