author  hoelzl 
Tue, 09 Feb 2016 06:39:31 +0100  
changeset 62369  acfc4ad7b76a 
parent 62343  24106dc44def 
child 62371  7c288c0c7300 
permissions  rwrr 
43920  1 
(* Title: HOL/Library/Extended_Real.thy 
41983  2 
Author: Johannes Hölzl, TU München 
3 
Author: Robert Himmelmann, TU München 

4 
Author: Armin Heller, TU München 

5 
Author: Bogdan Grechuk, University of Edinburgh 

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

6 
Author: Manuel Eberl, TU München 
41983  7 
*) 
41973  8 

60500  9 
section \<open>Extended real number line\<close> 
41973  10 

43920  11 
theory Extended_Real 
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60580
diff
changeset

12 
imports Complex_Main Extended_Nat Liminf_Limsup 
41973  13 
begin 
14 

60500  15 
text \<open> 
51022
78de6c7e8a58
replace open_interval with the rule open_tendstoI; generalize Liminf/Limsup rules
hoelzl
parents:
51000
diff
changeset

16 

60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

17 
This should be part of @{theory Extended_Nat} or @{theory Order_Continuity}, but then the 
61585  18 
AFPentry \<open>Jinja_Thread\<close> fails, as it does overload certain named from @{theory Complex_Main}. 
59115
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

19 

60500  20 
\<close> 
59115
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

21 

60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

22 
lemma continuous_at_left_imp_sup_continuous: 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

23 
fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology}" 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

24 
assumes "mono f" "\<And>x. continuous (at_left x) f" 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

25 
shows "sup_continuous f" 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

26 
unfolding sup_continuous_def 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

27 
proof safe 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

28 
fix M :: "nat \<Rightarrow> 'a" assume "incseq M" then show "f (SUP i. M i) = (SUP i. f (M i))" 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

29 
using continuous_at_Sup_mono[OF assms, of "range M"] by simp 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

30 
qed 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

31 

423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

32 
lemma sup_continuous_at_left: 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

33 
fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology, first_countable_topology}" 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

34 
assumes f: "sup_continuous f" 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

35 
shows "continuous (at_left x) f" 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

36 
proof cases 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

37 
assume "x = bot" then show ?thesis 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

38 
by (simp add: trivial_limit_at_left_bot) 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

39 
next 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61631
diff
changeset

40 
assume x: "x \<noteq> bot" 
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

41 
show ?thesis 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

42 
unfolding continuous_within 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

43 
proof (intro tendsto_at_left_sequentially[of bot]) 
61969  44 
fix S :: "nat \<Rightarrow> 'a" assume S: "incseq S" and S_x: "S \<longlonglongrightarrow> x" 
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

45 
from S_x have x_eq: "x = (SUP i. S i)" 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

46 
by (rule LIMSEQ_unique) (intro LIMSEQ_SUP S) 
61969  47 
show "(\<lambda>n. f (S n)) \<longlonglongrightarrow> f x" 
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

48 
unfolding x_eq sup_continuousD[OF f S] 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

49 
using S sup_continuous_mono[OF f] by (intro LIMSEQ_SUP) (auto simp: mono_def) 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

50 
qed (insert x, auto simp: bot_less) 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

51 
qed 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

52 

423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

53 
lemma sup_continuous_iff_at_left: 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

54 
fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology, first_countable_topology}" 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

55 
shows "sup_continuous f \<longleftrightarrow> (\<forall>x. continuous (at_left x) f) \<and> mono f" 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

56 
using sup_continuous_at_left[of f] continuous_at_left_imp_sup_continuous[of f] 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

57 
sup_continuous_mono[of f] by auto 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61631
diff
changeset

58 

60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

59 
lemma continuous_at_right_imp_inf_continuous: 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

60 
fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology}" 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

61 
assumes "mono f" "\<And>x. continuous (at_right x) f" 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

62 
shows "inf_continuous f" 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

63 
unfolding inf_continuous_def 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

64 
proof safe 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

65 
fix M :: "nat \<Rightarrow> 'a" assume "decseq M" then show "f (INF i. M i) = (INF i. f (M i))" 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

66 
using continuous_at_Inf_mono[OF assms, of "range M"] by simp 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

67 
qed 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

68 

423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

69 
lemma inf_continuous_at_right: 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

70 
fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology, first_countable_topology}" 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

71 
assumes f: "inf_continuous f" 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

72 
shows "continuous (at_right x) f" 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

73 
proof cases 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

74 
assume "x = top" then show ?thesis 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

75 
by (simp add: trivial_limit_at_right_top) 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

76 
next 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61631
diff
changeset

77 
assume x: "x \<noteq> top" 
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

78 
show ?thesis 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

79 
unfolding continuous_within 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

80 
proof (intro tendsto_at_right_sequentially[of _ top]) 
61969  81 
fix S :: "nat \<Rightarrow> 'a" assume S: "decseq S" and S_x: "S \<longlonglongrightarrow> x" 
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

82 
from S_x have x_eq: "x = (INF i. S i)" 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

83 
by (rule LIMSEQ_unique) (intro LIMSEQ_INF S) 
61969  84 
show "(\<lambda>n. f (S n)) \<longlonglongrightarrow> f x" 
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

85 
unfolding x_eq inf_continuousD[OF f S] 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

86 
using S inf_continuous_mono[OF f] by (intro LIMSEQ_INF) (auto simp: mono_def antimono_def) 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

87 
qed (insert x, auto simp: less_top) 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

88 
qed 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

89 

423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

90 
lemma inf_continuous_iff_at_right: 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

91 
fixes f :: "'a \<Rightarrow> 'a::{complete_linorder, linorder_topology, first_countable_topology}" 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

92 
shows "inf_continuous f \<longleftrightarrow> (\<forall>x. continuous (at_right x) f) \<and> mono f" 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

93 
using inf_continuous_at_right[of f] continuous_at_right_imp_inf_continuous[of f] 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

94 
inf_continuous_mono[of f] by auto 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

95 

59115
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

96 
instantiation enat :: linorder_topology 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

97 
begin 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

98 

f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

99 
definition open_enat :: "enat set \<Rightarrow> bool" where 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

100 
"open_enat = generate_topology (range lessThan \<union> range greaterThan)" 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

101 

f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

102 
instance 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

103 
proof qed (rule open_enat_def) 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

104 

f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

105 
end 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

106 

f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

107 
lemma open_enat: "open {enat n}" 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

108 
proof (cases n) 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

109 
case 0 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

110 
then have "{enat n} = {..< eSuc 0}" 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

111 
by (auto simp: enat_0) 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

112 
then show ?thesis 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

113 
by simp 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

114 
next 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

115 
case (Suc n') 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

116 
then have "{enat n} = {enat n' <..< enat (Suc n)}" 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

117 
apply auto 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

118 
apply (case_tac x) 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

119 
apply auto 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

120 
done 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

121 
then show ?thesis 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

122 
by simp 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

123 
qed 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

124 

f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

125 
lemma open_enat_iff: 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

126 
fixes A :: "enat set" 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

127 
shows "open A \<longleftrightarrow> (\<infinity> \<in> A \<longrightarrow> (\<exists>n::nat. {n <..} \<subseteq> A))" 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

128 
proof safe 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

129 
assume "\<infinity> \<notin> A" 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

130 
then have "A = (\<Union>n\<in>{n. enat n \<in> A}. {enat n})" 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

131 
apply auto 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

132 
apply (case_tac x) 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

133 
apply auto 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

134 
done 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

135 
moreover have "open \<dots>" 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

136 
by (auto intro: open_enat) 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

137 
ultimately show "open A" 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

138 
by simp 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

139 
next 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

140 
fix n assume "{enat n <..} \<subseteq> A" 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

141 
then have "A = (\<Union>n\<in>{n. enat n \<in> A}. {enat n}) \<union> {enat n <..}" 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

142 
apply auto 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

143 
apply (case_tac x) 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

144 
apply auto 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

145 
done 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

146 
moreover have "open \<dots>" 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

147 
by (intro open_Un open_UN ballI open_enat open_greaterThan) 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

148 
ultimately show "open A" 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

149 
by simp 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

150 
next 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

151 
assume "open A" "\<infinity> \<in> A" 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

152 
then have "generate_topology (range lessThan \<union> range greaterThan) A" "\<infinity> \<in> A" 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

153 
unfolding open_enat_def by auto 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

154 
then show "\<exists>n::nat. {n <..} \<subseteq> A" 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

155 
proof induction 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

156 
case (Int A B) 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

157 
then obtain n m where "{enat n<..} \<subseteq> A" "{enat m<..} \<subseteq> B" 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

158 
by auto 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

159 
then have "{enat (max n m) <..} \<subseteq> A \<inter> B" 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

160 
by (auto simp add: subset_eq Ball_def max_def enat_ord_code(1)[symmetric] simp del: enat_ord_code(1)) 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

161 
then show ?case 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

162 
by auto 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

163 
next 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

164 
case (UN K) 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

165 
then obtain k where "k \<in> K" "\<infinity> \<in> k" 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

166 
by auto 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

167 
with UN.IH[OF this] show ?case 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

168 
by auto 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

169 
qed auto 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

170 
qed 
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

171 

62369  172 
lemma nhds_enat: "nhds x = (if x = \<infinity> then INF i. principal {enat i..} else principal {x})" 
173 
proof auto 

174 
show "nhds \<infinity> = (INF i. principal {enat i..})" 

175 
unfolding nhds_def 

176 
apply (auto intro!: antisym INF_greatest simp add: open_enat_iff cong: rev_conj_cong) 

177 
apply (auto intro!: INF_lower Ioi_le_Ico) [] 

178 
subgoal for x i 

179 
by (auto intro!: INF_lower2[of "Suc i"] simp: subset_eq Ball_def eSuc_enat Suc_ile_eq) 

180 
done 

181 
show "nhds (enat i) = principal {enat i}" for i 

182 
by (simp add: nhds_discrete_open open_enat) 

183 
qed 

184 

185 
instance enat :: topological_comm_monoid_add 

186 
proof 

187 
have [simp]: "enat i \<le> aa \<Longrightarrow> enat i \<le> aa + ba" for aa ba i 

188 
by (rule order_trans[OF _ add_mono[of aa aa 0 ba]]) auto 

189 
then have [simp]: "enat i \<le> ba \<Longrightarrow> enat i \<le> aa + ba" for aa ba i 

190 
by (metis add.commute) 

191 
fix a b :: enat show "((\<lambda>x. fst x + snd x) \<longlongrightarrow> a + b) (nhds a \<times>\<^sub>F nhds b)" 

192 
apply (auto simp: nhds_enat filterlim_INF prod_filter_INF1 prod_filter_INF2 

193 
filterlim_principal principal_prod_principal eventually_principal) 

194 
subgoal for i 

195 
by (auto intro!: eventually_INF1[of i] simp: eventually_principal) 

196 
subgoal for j i 

197 
by (auto intro!: eventually_INF1[of i] simp: eventually_principal) 

198 
subgoal for j i 

199 
by (auto intro!: eventually_INF1[of i] simp: eventually_principal) 

200 
done 

201 
qed 

59115
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

202 

60500  203 
text \<open> 
59115
f65ac77f7e07
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
hoelzl
parents:
59023
diff
changeset

204 

51022
78de6c7e8a58
replace open_interval with the rule open_tendstoI; generalize Liminf/Limsup rules
hoelzl
parents:
51000
diff
changeset

205 
For more lemmas about the extended real numbers go to 
78de6c7e8a58
replace open_interval with the rule open_tendstoI; generalize Liminf/Limsup rules
hoelzl
parents:
51000
diff
changeset

206 
@{file "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"} 
78de6c7e8a58
replace open_interval with the rule open_tendstoI; generalize Liminf/Limsup rules
hoelzl
parents:
51000
diff
changeset

207 

60500  208 
\<close> 
209 

210 
subsection \<open>Definition and basic properties\<close> 

41973  211 

58310  212 
datatype ereal = ereal real  PInfty  MInfty 
41973  213 

43920  214 
instantiation ereal :: uminus 
41973  215 
begin 
53873  216 

217 
fun uminus_ereal where 

218 
" (ereal r) = ereal ( r)" 

219 
 " PInfty = MInfty" 

220 
 " MInfty = PInfty" 

221 

222 
instance .. 

223 

41973  224 
end 
225 

43923  226 
instantiation ereal :: infinity 
227 
begin 

53873  228 

229 
definition "(\<infinity>::ereal) = PInfty" 

230 
instance .. 

231 

43923  232 
end 
41973  233 

43923  234 
declare [[coercion "ereal :: real \<Rightarrow> ereal"]] 
41973  235 

43920  236 
lemma ereal_uminus_uminus[simp]: 
53873  237 
fixes a :: ereal 
238 
shows " ( a) = a" 

41973  239 
by (cases a) simp_all 
240 

43923  241 
lemma 
242 
shows PInfty_eq_infinity[simp]: "PInfty = \<infinity>" 

243 
and MInfty_eq_minfinity[simp]: "MInfty =  \<infinity>" 

244 
and MInfty_neq_PInfty[simp]: "\<infinity> \<noteq>  (\<infinity>::ereal)" " \<infinity> \<noteq> (\<infinity>::ereal)" 

245 
and MInfty_neq_ereal[simp]: "ereal r \<noteq>  \<infinity>" " \<infinity> \<noteq> ereal r" 

246 
and PInfty_neq_ereal[simp]: "ereal r \<noteq> \<infinity>" "\<infinity> \<noteq> ereal r" 

247 
and PInfty_cases[simp]: "(case \<infinity> of ereal r \<Rightarrow> f r  PInfty \<Rightarrow> y  MInfty \<Rightarrow> z) = y" 

248 
and MInfty_cases[simp]: "(case  \<infinity> of ereal r \<Rightarrow> f r  PInfty \<Rightarrow> y  MInfty \<Rightarrow> z) = z" 

249 
by (simp_all add: infinity_ereal_def) 

41973  250 

43933  251 
declare 
252 
PInfty_eq_infinity[code_post] 

253 
MInfty_eq_minfinity[code_post] 

254 

255 
lemma [code_unfold]: 

256 
"\<infinity> = PInfty" 

53873  257 
" PInfty = MInfty" 
43933  258 
by simp_all 
259 

43923  260 
lemma inj_ereal[simp]: "inj_on ereal A" 
261 
unfolding inj_on_def by auto 

41973  262 

55913  263 
lemma ereal_cases[cases type: ereal]: 
264 
obtains (real) r where "x = ereal r" 

265 
 (PInf) "x = \<infinity>" 

266 
 (MInf) "x = \<infinity>" 

41973  267 
using assms by (cases x) auto 
268 

43920  269 
lemmas ereal2_cases = ereal_cases[case_product ereal_cases] 
270 
lemmas ereal3_cases = ereal2_cases[case_product ereal_cases] 

41973  271 

57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57025
diff
changeset

272 
lemma ereal_all_split: "\<And>P. (\<forall>x::ereal. P x) \<longleftrightarrow> P \<infinity> \<and> (\<forall>x. P (ereal x)) \<and> P (\<infinity>)" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57025
diff
changeset

273 
by (metis ereal_cases) 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57025
diff
changeset

274 

87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57025
diff
changeset

275 
lemma ereal_ex_split: "\<And>P. (\<exists>x::ereal. P x) \<longleftrightarrow> P \<infinity> \<or> (\<exists>x. P (ereal x)) \<or> P (\<infinity>)" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57025
diff
changeset

276 
by (metis ereal_cases) 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57025
diff
changeset

277 

43920  278 
lemma ereal_uminus_eq_iff[simp]: 
53873  279 
fixes a b :: ereal 
280 
shows "a = b \<longleftrightarrow> a = b" 

43920  281 
by (cases rule: ereal2_cases[of a b]) simp_all 
41973  282 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61245
diff
changeset

283 
function real_of_ereal :: "ereal \<Rightarrow> real" where 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61245
diff
changeset

284 
"real_of_ereal (ereal r) = r" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61245
diff
changeset

285 
 "real_of_ereal \<infinity> = 0" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61245
diff
changeset

286 
 "real_of_ereal (\<infinity>) = 0" 
43920  287 
by (auto intro: ereal_cases) 
60679  288 
termination by standard (rule wf_empty) 
41973  289 

43920  290 
lemma real_of_ereal[simp]: 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61245
diff
changeset

291 
"real_of_ereal ( x :: ereal) =  (real_of_ereal x)" 
58042
ffa9e39763e3
introduce real_of typeclass for real :: 'a => real
hoelzl
parents:
57512
diff
changeset

292 
by (cases x) simp_all 
41973  293 

43920  294 
lemma range_ereal[simp]: "range ereal = UNIV  {\<infinity>, \<infinity>}" 
41973  295 
proof safe 
53873  296 
fix x 
297 
assume "x \<notin> range ereal" "x \<noteq> \<infinity>" 

298 
then show "x = \<infinity>" 

299 
by (cases x) auto 

41973  300 
qed auto 
301 

43920  302 
lemma ereal_range_uminus[simp]: "range uminus = (UNIV::ereal set)" 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

303 
proof safe 
53873  304 
fix x :: ereal 
305 
show "x \<in> range uminus" 

306 
by (intro image_eqI[of _ _ "x"]) auto 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

307 
qed auto 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

308 

43920  309 
instantiation ereal :: abs 
41976  310 
begin 
53873  311 

312 
function abs_ereal where 

313 
"\<bar>ereal r\<bar> = ereal \<bar>r\<bar>" 

314 
 "\<bar>\<infinity>\<bar> = (\<infinity>::ereal)" 

315 
 "\<bar>\<infinity>\<bar> = (\<infinity>::ereal)" 

316 
by (auto intro: ereal_cases) 

317 
termination proof qed (rule wf_empty) 

318 

319 
instance .. 

320 

41976  321 
end 
322 

53873  323 
lemma abs_eq_infinity_cases[elim!]: 
324 
fixes x :: ereal 

325 
assumes "\<bar>x\<bar> = \<infinity>" 

326 
obtains "x = \<infinity>"  "x = \<infinity>" 

327 
using assms by (cases x) auto 

41976  328 

53873  329 
lemma abs_neq_infinity_cases[elim!]: 
330 
fixes x :: ereal 

331 
assumes "\<bar>x\<bar> \<noteq> \<infinity>" 

332 
obtains r where "x = ereal r" 

333 
using assms by (cases x) auto 

334 

335 
lemma abs_ereal_uminus[simp]: 

336 
fixes x :: ereal 

337 
shows "\<bar> x\<bar> = \<bar>x\<bar>" 

41976  338 
by (cases x) auto 
339 

53873  340 
lemma ereal_infinity_cases: 
341 
fixes a :: ereal 

342 
shows "a \<noteq> \<infinity> \<Longrightarrow> a \<noteq> \<infinity> \<Longrightarrow> \<bar>a\<bar> \<noteq> \<infinity>" 

343 
by auto 

41976  344 

41973  345 
subsubsection "Addition" 
346 

54408  347 
instantiation ereal :: "{one,comm_monoid_add,zero_neq_one}" 
41973  348 
begin 
349 

43920  350 
definition "0 = ereal 0" 
51351  351 
definition "1 = ereal 1" 
41973  352 

43920  353 
function plus_ereal where 
53873  354 
"ereal r + ereal p = ereal (r + p)" 
355 
 "\<infinity> + a = (\<infinity>::ereal)" 

356 
 "a + \<infinity> = (\<infinity>::ereal)" 

357 
 "ereal r + \<infinity> =  \<infinity>" 

358 
 "\<infinity> + ereal p = (\<infinity>::ereal)" 

359 
 "\<infinity> + \<infinity> = (\<infinity>::ereal)" 

61166
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61120
diff
changeset

360 
proof goal_cases 
60580  361 
case prems: (1 P x) 
53873  362 
then obtain a b where "x = (a, b)" 
363 
by (cases x) auto 

60580  364 
with prems show P 
43920  365 
by (cases rule: ereal2_cases[of a b]) auto 
41973  366 
qed auto 
60679  367 
termination by standard (rule wf_empty) 
41973  368 

369 
lemma Infty_neq_0[simp]: 

43923  370 
"(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> (\<infinity>::ereal)" 
371 
"(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> (\<infinity>::ereal)" 

43920  372 
by (simp_all add: zero_ereal_def) 
41973  373 

43920  374 
lemma ereal_eq_0[simp]: 
375 
"ereal r = 0 \<longleftrightarrow> r = 0" 

376 
"0 = ereal r \<longleftrightarrow> r = 0" 

377 
unfolding zero_ereal_def by simp_all 

41973  378 

54416  379 
lemma ereal_eq_1[simp]: 
380 
"ereal r = 1 \<longleftrightarrow> r = 1" 

381 
"1 = ereal r \<longleftrightarrow> r = 1" 

382 
unfolding one_ereal_def by simp_all 

383 

41973  384 
instance 
385 
proof 

47082  386 
fix a b c :: ereal 
387 
show "0 + a = a" 

43920  388 
by (cases a) (simp_all add: zero_ereal_def) 
47082  389 
show "a + b = b + a" 
43920  390 
by (cases rule: ereal2_cases[of a b]) simp_all 
47082  391 
show "a + b + c = a + (b + c)" 
43920  392 
by (cases rule: ereal3_cases[of a b c]) simp_all 
54408  393 
show "0 \<noteq> (1::ereal)" 
394 
by (simp add: one_ereal_def zero_ereal_def) 

41973  395 
qed 
53873  396 

41973  397 
end 
398 

60060  399 
lemma ereal_0_plus [simp]: "ereal 0 + x = x" 
400 
and plus_ereal_0 [simp]: "x + ereal 0 = x" 

401 
by(simp_all add: zero_ereal_def[symmetric]) 

402 

51351  403 
instance ereal :: numeral .. 
404 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61245
diff
changeset

405 
lemma real_of_ereal_0[simp]: "real_of_ereal (0::ereal) = 0" 
58042
ffa9e39763e3
introduce real_of typeclass for real :: 'a => real
hoelzl
parents:
57512
diff
changeset

406 
unfolding zero_ereal_def by simp 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

407 

43920  408 
lemma abs_ereal_zero[simp]: "\<bar>0\<bar> = (0::ereal)" 
409 
unfolding zero_ereal_def abs_ereal.simps by simp 

41976  410 

53873  411 
lemma ereal_uminus_zero[simp]: " 0 = (0::ereal)" 
43920  412 
by (simp add: zero_ereal_def) 
41973  413 

43920  414 
lemma ereal_uminus_zero_iff[simp]: 
53873  415 
fixes a :: ereal 
416 
shows "a = 0 \<longleftrightarrow> a = 0" 

41973  417 
by (cases a) simp_all 
418 

43920  419 
lemma ereal_plus_eq_PInfty[simp]: 
53873  420 
fixes a b :: ereal 
421 
shows "a + b = \<infinity> \<longleftrightarrow> a = \<infinity> \<or> b = \<infinity>" 

43920  422 
by (cases rule: ereal2_cases[of a b]) auto 
41973  423 

43920  424 
lemma ereal_plus_eq_MInfty[simp]: 
53873  425 
fixes a b :: ereal 
426 
shows "a + b = \<infinity> \<longleftrightarrow> (a = \<infinity> \<or> b = \<infinity>) \<and> a \<noteq> \<infinity> \<and> b \<noteq> \<infinity>" 

43920  427 
by (cases rule: ereal2_cases[of a b]) auto 
41973  428 

43920  429 
lemma ereal_add_cancel_left: 
53873  430 
fixes a b :: ereal 
431 
assumes "a \<noteq> \<infinity>" 

432 
shows "a + b = a + c \<longleftrightarrow> a = \<infinity> \<or> b = c" 

43920  433 
using assms by (cases rule: ereal3_cases[of a b c]) auto 
41973  434 

43920  435 
lemma ereal_add_cancel_right: 
53873  436 
fixes a b :: ereal 
437 
assumes "a \<noteq> \<infinity>" 

438 
shows "b + a = c + a \<longleftrightarrow> a = \<infinity> \<or> b = c" 

43920  439 
using assms by (cases rule: ereal3_cases[of a b c]) auto 
41973  440 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61245
diff
changeset

441 
lemma ereal_real: "ereal (real_of_ereal x) = (if \<bar>x\<bar> = \<infinity> then 0 else x)" 
41973  442 
by (cases x) simp_all 
443 

43920  444 
lemma real_of_ereal_add: 
445 
fixes a b :: ereal 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61245
diff
changeset

446 
shows "real_of_ereal (a + b) = 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61245
diff
changeset

447 
(if (\<bar>a\<bar> = \<infinity>) \<and> (\<bar>b\<bar> = \<infinity>) \<or> (\<bar>a\<bar> \<noteq> \<infinity>) \<and> (\<bar>b\<bar> \<noteq> \<infinity>) then real_of_ereal a + real_of_ereal b else 0)" 
43920  448 
by (cases rule: ereal2_cases[of a b]) auto 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

449 

53873  450 

43920  451 
subsubsection "Linear order on @{typ ereal}" 
41973  452 

43920  453 
instantiation ereal :: linorder 
41973  454 
begin 
455 

47082  456 
function less_ereal 
457 
where 

458 
" ereal x < ereal y \<longleftrightarrow> x < y" 

459 
 "(\<infinity>::ereal) < a \<longleftrightarrow> False" 

460 
 " a < (\<infinity>::ereal) \<longleftrightarrow> False" 

461 
 "ereal x < \<infinity> \<longleftrightarrow> True" 

462 
 " \<infinity> < ereal r \<longleftrightarrow> True" 

463 
 " \<infinity> < (\<infinity>::ereal) \<longleftrightarrow> True" 

61166
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61120
diff
changeset

464 
proof goal_cases 
60580  465 
case prems: (1 P x) 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset

466 
then obtain a b where "x = (a,b)" by (cases x) auto 
60580  467 
with prems show P by (cases rule: ereal2_cases[of a b]) auto 
41973  468 
qed simp_all 
469 
termination by (relation "{}") simp 

470 

43920  471 
definition "x \<le> (y::ereal) \<longleftrightarrow> x < y \<or> x = y" 
41973  472 

43920  473 
lemma ereal_infty_less[simp]: 
43923  474 
fixes x :: ereal 
475 
shows "x < \<infinity> \<longleftrightarrow> (x \<noteq> \<infinity>)" 

476 
"\<infinity> < x \<longleftrightarrow> (x \<noteq> \<infinity>)" 

41973  477 
by (cases x, simp_all) (cases x, simp_all) 
478 

43920  479 
lemma ereal_infty_less_eq[simp]: 
43923  480 
fixes x :: ereal 
481 
shows "\<infinity> \<le> x \<longleftrightarrow> x = \<infinity>" 

53873  482 
and "x \<le> \<infinity> \<longleftrightarrow> x = \<infinity>" 
43920  483 
by (auto simp add: less_eq_ereal_def) 
41973  484 

43920  485 
lemma ereal_less[simp]: 
486 
"ereal r < 0 \<longleftrightarrow> (r < 0)" 

487 
"0 < ereal r \<longleftrightarrow> (0 < r)" 

54416  488 
"ereal r < 1 \<longleftrightarrow> (r < 1)" 
489 
"1 < ereal r \<longleftrightarrow> (1 < r)" 

43923  490 
"0 < (\<infinity>::ereal)" 
491 
"(\<infinity>::ereal) < 0" 

54416  492 
by (simp_all add: zero_ereal_def one_ereal_def) 
41973  493 

43920  494 
lemma ereal_less_eq[simp]: 
43923  495 
"x \<le> (\<infinity>::ereal)" 
496 
"(\<infinity>::ereal) \<le> x" 

43920  497 
"ereal r \<le> ereal p \<longleftrightarrow> r \<le> p" 
498 
"ereal r \<le> 0 \<longleftrightarrow> r \<le> 0" 

499 
"0 \<le> ereal r \<longleftrightarrow> 0 \<le> r" 

54416  500 
"ereal r \<le> 1 \<longleftrightarrow> r \<le> 1" 
501 
"1 \<le> ereal r \<longleftrightarrow> 1 \<le> r" 

502 
by (auto simp add: less_eq_ereal_def zero_ereal_def one_ereal_def) 

41973  503 

43920  504 
lemma ereal_infty_less_eq2: 
43923  505 
"a \<le> b \<Longrightarrow> a = \<infinity> \<Longrightarrow> b = (\<infinity>::ereal)" 
506 
"a \<le> b \<Longrightarrow> b = \<infinity> \<Longrightarrow> a = (\<infinity>::ereal)" 

41973  507 
by simp_all 
508 

509 
instance 

510 
proof 

47082  511 
fix x y z :: ereal 
512 
show "x \<le> x" 

41973  513 
by (cases x) simp_all 
47082  514 
show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x" 
43920  515 
by (cases rule: ereal2_cases[of x y]) auto 
41973  516 
show "x \<le> y \<or> y \<le> x " 
43920  517 
by (cases rule: ereal2_cases[of x y]) auto 
53873  518 
{ 
519 
assume "x \<le> y" "y \<le> x" 

520 
then show "x = y" 

521 
by (cases rule: ereal2_cases[of x y]) auto 

522 
} 

523 
{ 

524 
assume "x \<le> y" "y \<le> z" 

525 
then show "x \<le> z" 

526 
by (cases rule: ereal3_cases[of x y z]) auto 

527 
} 

41973  528 
qed 
47082  529 

41973  530 
end 
531 

51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

532 
lemma ereal_dense2: "x < y \<Longrightarrow> \<exists>z. x < ereal z \<and> ereal z < y" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

533 
using lt_ex gt_ex dense by (cases x y rule: ereal2_cases) auto 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

534 

53216  535 
instance ereal :: dense_linorder 
60679  536 
by standard (blast dest: ereal_dense2) 
51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

537 

43920  538 
instance ereal :: ordered_ab_semigroup_add 
41978  539 
proof 
53873  540 
fix a b c :: ereal 
541 
assume "a \<le> b" 

542 
then show "c + a \<le> c + b" 

43920  543 
by (cases rule: ereal3_cases[of a b c]) auto 
41978  544 
qed 
545 

43920  546 
lemma real_of_ereal_positive_mono: 
53873  547 
fixes x y :: ereal 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61245
diff
changeset

548 
shows "0 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<noteq> \<infinity> \<Longrightarrow> real_of_ereal x \<le> real_of_ereal y" 
43920  549 
by (cases rule: ereal2_cases[of x y]) auto 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

550 

43920  551 
lemma ereal_MInfty_lessI[intro, simp]: 
53873  552 
fixes a :: ereal 
553 
shows "a \<noteq> \<infinity> \<Longrightarrow> \<infinity> < a" 

41973  554 
by (cases a) auto 
555 

43920  556 
lemma ereal_less_PInfty[intro, simp]: 
53873  557 
fixes a :: ereal 
558 
shows "a \<noteq> \<infinity> \<Longrightarrow> a < \<infinity>" 

41973  559 
by (cases a) auto 
560 

43920  561 
lemma ereal_less_ereal_Ex: 
562 
fixes a b :: ereal 

563 
shows "x < ereal r \<longleftrightarrow> x = \<infinity> \<or> (\<exists>p. p < r \<and> x = ereal p)" 

41973  564 
by (cases x) auto 
565 

43920  566 
lemma less_PInf_Ex_of_nat: "x \<noteq> \<infinity> \<longleftrightarrow> (\<exists>n::nat. x < ereal (real n))" 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

567 
proof (cases x) 
53873  568 
case (real r) 
569 
then show ?thesis 

41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
41979
diff
changeset

570 
using reals_Archimedean2[of r] by simp 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

571 
qed simp_all 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

572 

43920  573 
lemma ereal_add_mono: 
53873  574 
fixes a b c d :: ereal 
575 
assumes "a \<le> b" 

576 
and "c \<le> d" 

577 
shows "a + c \<le> b + d" 

41973  578 
using assms 
579 
apply (cases a) 

43920  580 
apply (cases rule: ereal3_cases[of b c d], auto) 
581 
apply (cases rule: ereal3_cases[of b c d], auto) 

41973  582 
done 
583 

43920  584 
lemma ereal_minus_le_minus[simp]: 
53873  585 
fixes a b :: ereal 
586 
shows " a \<le>  b \<longleftrightarrow> b \<le> a" 

43920  587 
by (cases rule: ereal2_cases[of a b]) auto 
41973  588 

43920  589 
lemma ereal_minus_less_minus[simp]: 
53873  590 
fixes a b :: ereal 
591 
shows " a <  b \<longleftrightarrow> b < a" 

43920  592 
by (cases rule: ereal2_cases[of a b]) auto 
41973  593 

43920  594 
lemma ereal_le_real_iff: 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61245
diff
changeset

595 
"x \<le> real_of_ereal y \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> ereal x \<le> y) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> x \<le> 0)" 
41973  596 
by (cases y) auto 
597 

43920  598 
lemma real_le_ereal_iff: 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61245
diff
changeset

599 
"real_of_ereal y \<le> x \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y \<le> ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 \<le> x)" 
41973  600 
by (cases y) auto 
601 

43920  602 
lemma ereal_less_real_iff: 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61245
diff
changeset

603 
"x < real_of_ereal y \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> ereal x < y) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> x < 0)" 
41973  604 
by (cases y) auto 
605 

43920  606 
lemma real_less_ereal_iff: 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61245
diff
changeset

607 
"real_of_ereal y < x \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y < ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 < x)" 
41973  608 
by (cases y) auto 
609 

43920  610 
lemma real_of_ereal_pos: 
53873  611 
fixes x :: ereal 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61245
diff
changeset

612 
shows "0 \<le> x \<Longrightarrow> 0 \<le> real_of_ereal x" by (cases x) auto 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

613 

43920  614 
lemmas real_of_ereal_ord_simps = 
615 
ereal_le_real_iff real_le_ereal_iff ereal_less_real_iff real_less_ereal_iff 

41973  616 

43920  617 
lemma abs_ereal_ge0[simp]: "0 \<le> x \<Longrightarrow> \<bar>x :: ereal\<bar> = x" 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

618 
by (cases x) auto 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

619 

43920  620 
lemma abs_ereal_less0[simp]: "x < 0 \<Longrightarrow> \<bar>x :: ereal\<bar> = x" 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

621 
by (cases x) auto 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

622 

43920  623 
lemma abs_ereal_pos[simp]: "0 \<le> \<bar>x :: ereal\<bar>" 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

624 
by (cases x) auto 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

625 

61631
4f7ef088c4ed
add lemmas for extended nats and reals
Andreas Lochbihler
parents:
61610
diff
changeset

626 
lemma ereal_abs_leI: 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61631
diff
changeset

627 
fixes x y :: ereal 
61631
4f7ef088c4ed
add lemmas for extended nats and reals
Andreas Lochbihler
parents:
61610
diff
changeset

628 
shows "\<lbrakk> x \<le> y; x \<le> y \<rbrakk> \<Longrightarrow> \<bar>x\<bar> \<le> y" 
4f7ef088c4ed
add lemmas for extended nats and reals
Andreas Lochbihler
parents:
61610
diff
changeset

629 
by(cases x y rule: ereal2_cases)(simp_all) 
4f7ef088c4ed
add lemmas for extended nats and reals
Andreas Lochbihler
parents:
61610
diff
changeset

630 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61245
diff
changeset

631 
lemma real_of_ereal_le_0[simp]: "real_of_ereal (x :: ereal) \<le> 0 \<longleftrightarrow> x \<le> 0 \<or> x = \<infinity>" 
43923  632 
by (cases x) auto 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

633 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61245
diff
changeset

634 
lemma abs_real_of_ereal[simp]: "\<bar>real_of_ereal (x :: ereal)\<bar> = real_of_ereal \<bar>x\<bar>" 
43923  635 
by (cases x) auto 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

636 

43923  637 
lemma zero_less_real_of_ereal: 
53873  638 
fixes x :: ereal 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61245
diff
changeset

639 
shows "0 < real_of_ereal x \<longleftrightarrow> 0 < x \<and> x \<noteq> \<infinity>" 
43923  640 
by (cases x) auto 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

641 

43920  642 
lemma ereal_0_le_uminus_iff[simp]: 
53873  643 
fixes a :: ereal 
644 
shows "0 \<le>  a \<longleftrightarrow> a \<le> 0" 

43920  645 
by (cases rule: ereal2_cases[of a]) auto 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

646 

43920  647 
lemma ereal_uminus_le_0_iff[simp]: 
53873  648 
fixes a :: ereal 
649 
shows " a \<le> 0 \<longleftrightarrow> 0 \<le> a" 

43920  650 
by (cases rule: ereal2_cases[of a]) auto 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

651 

43920  652 
lemma ereal_add_strict_mono: 
653 
fixes a b c d :: ereal 

56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56927
diff
changeset

654 
assumes "a \<le> b" 
53873  655 
and "0 \<le> a" 
656 
and "a \<noteq> \<infinity>" 

657 
and "c < d" 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

658 
shows "a + c < b + d" 
53873  659 
using assms 
660 
by (cases rule: ereal3_cases[case_product ereal_cases, of a b c d]) auto 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

661 

53873  662 
lemma ereal_less_add: 
663 
fixes a b c :: ereal 

664 
shows "\<bar>a\<bar> \<noteq> \<infinity> \<Longrightarrow> c < b \<Longrightarrow> a + c < a + b" 

43920  665 
by (cases rule: ereal2_cases[of b c]) auto 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

666 

54416  667 
lemma ereal_add_nonneg_eq_0_iff: 
668 
fixes a b :: ereal 

669 
shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a + b = 0 \<longleftrightarrow> a = 0 \<and> b = 0" 

670 
by (cases a b rule: ereal2_cases) auto 

671 

53873  672 
lemma ereal_uminus_eq_reorder: " a = b \<longleftrightarrow> a = (b::ereal)" 
673 
by auto 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

674 

43920  675 
lemma ereal_uminus_less_reorder: " a < b \<longleftrightarrow> b < (a::ereal)" 
676 
by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_less_minus) 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

677 

59452
2538b2c51769
ereal: tuned proofs concerning continuity and suprema
hoelzl
parents:
59425
diff
changeset

678 
lemma ereal_less_uminus_reorder: "a <  b \<longleftrightarrow> b <  (a::ereal)" 
2538b2c51769
ereal: tuned proofs concerning continuity and suprema
hoelzl
parents:
59425
diff
changeset

679 
by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_less_minus) 
2538b2c51769
ereal: tuned proofs concerning continuity and suprema
hoelzl
parents:
59425
diff
changeset

680 

43920  681 
lemma ereal_uminus_le_reorder: " a \<le> b \<longleftrightarrow> b \<le> (a::ereal)" 
682 
by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_le_minus) 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

683 

43920  684 
lemmas ereal_uminus_reorder = 
685 
ereal_uminus_eq_reorder ereal_uminus_less_reorder ereal_uminus_le_reorder 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

686 

43920  687 
lemma ereal_bot: 
53873  688 
fixes x :: ereal 
689 
assumes "\<And>B. x \<le> ereal B" 

690 
shows "x =  \<infinity>" 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

691 
proof (cases x) 
53873  692 
case (real r) 
693 
with assms[of "r  1"] show ?thesis 

694 
by auto 

47082  695 
next 
53873  696 
case PInf 
697 
with assms[of 0] show ?thesis 

698 
by auto 

47082  699 
next 
53873  700 
case MInf 
701 
then show ?thesis 

702 
by simp 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

703 
qed 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

704 

43920  705 
lemma ereal_top: 
53873  706 
fixes x :: ereal 
707 
assumes "\<And>B. x \<ge> ereal B" 

708 
shows "x = \<infinity>" 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

709 
proof (cases x) 
53873  710 
case (real r) 
711 
with assms[of "r + 1"] show ?thesis 

712 
by auto 

47082  713 
next 
53873  714 
case MInf 
715 
with assms[of 0] show ?thesis 

716 
by auto 

47082  717 
next 
53873  718 
case PInf 
719 
then show ?thesis 

720 
by simp 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

721 
qed 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

722 

b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

723 
lemma 
43920  724 
shows ereal_max[simp]: "ereal (max x y) = max (ereal x) (ereal y)" 
725 
and ereal_min[simp]: "ereal (min x y) = min (ereal x) (ereal y)" 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

726 
by (simp_all add: min_def max_def) 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

727 

43920  728 
lemma ereal_max_0: "max 0 (ereal r) = ereal (max 0 r)" 
729 
by (auto simp: zero_ereal_def) 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

730 

41978  731 
lemma 
43920  732 
fixes f :: "nat \<Rightarrow> ereal" 
54416  733 
shows ereal_incseq_uminus[simp]: "incseq (\<lambda>x.  f x) \<longleftrightarrow> decseq f" 
734 
and ereal_decseq_uminus[simp]: "decseq (\<lambda>x.  f x) \<longleftrightarrow> incseq f" 

41978  735 
unfolding decseq_def incseq_def by auto 
736 

43920  737 
lemma incseq_ereal: "incseq f \<Longrightarrow> incseq (\<lambda>x. ereal (f x))" 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

738 
unfolding incseq_def by auto 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

739 

56537  740 
lemma ereal_add_nonneg_nonneg[simp]: 
53873  741 
fixes a b :: ereal 
742 
shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b" 

41978  743 
using add_mono[of 0 a 0 b] by simp 
744 

53873  745 
lemma image_eqD: "f ` A = B \<Longrightarrow> \<forall>x\<in>A. f x \<in> B" 
41978  746 
by auto 
747 

748 
lemma incseq_setsumI: 

53873  749 
fixes f :: "nat \<Rightarrow> 'a::{comm_monoid_add,ordered_ab_semigroup_add}" 
41978  750 
assumes "\<And>i. 0 \<le> f i" 
751 
shows "incseq (\<lambda>i. setsum f {..< i})" 

752 
proof (intro incseq_SucI) 

53873  753 
fix n 
754 
have "setsum f {..< n} + 0 \<le> setsum f {..<n} + f n" 

41978  755 
using assms by (rule add_left_mono) 
756 
then show "setsum f {..< n} \<le> setsum f {..< Suc n}" 

757 
by auto 

758 
qed 

759 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

760 
lemma incseq_setsumI2: 
53873  761 
fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::{comm_monoid_add,ordered_ab_semigroup_add}" 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

762 
assumes "\<And>n. n \<in> A \<Longrightarrow> incseq (f n)" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

763 
shows "incseq (\<lambda>i. \<Sum>n\<in>A. f n i)" 
53873  764 
using assms 
765 
unfolding incseq_def by (auto intro: setsum_mono) 

766 

59000  767 
lemma setsum_ereal[simp]: "(\<Sum>x\<in>A. ereal (f x)) = ereal (\<Sum>x\<in>A. f x)" 
768 
proof (cases "finite A") 

769 
case True 

770 
then show ?thesis by induct auto 

771 
next 

772 
case False 

773 
then show ?thesis by simp 

774 
qed 

775 

776 
lemma setsum_Pinfty: 

777 
fixes f :: "'a \<Rightarrow> ereal" 

778 
shows "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> finite P \<and> (\<exists>i\<in>P. f i = \<infinity>)" 

779 
proof safe 

780 
assume *: "setsum f P = \<infinity>" 

781 
show "finite P" 

782 
proof (rule ccontr) 

783 
assume "\<not> finite P" 

784 
with * show False 

785 
by auto 

786 
qed 

787 
show "\<exists>i\<in>P. f i = \<infinity>" 

788 
proof (rule ccontr) 

789 
assume "\<not> ?thesis" 

790 
then have "\<And>i. i \<in> P \<Longrightarrow> f i \<noteq> \<infinity>" 

791 
by auto 

60500  792 
with \<open>finite P\<close> have "setsum f P \<noteq> \<infinity>" 
59000  793 
by induct auto 
794 
with * show False 

795 
by auto 

796 
qed 

797 
next 

798 
fix i 

799 
assume "finite P" and "i \<in> P" and "f i = \<infinity>" 

800 
then show "setsum f P = \<infinity>" 

801 
proof induct 

802 
case (insert x A) 

803 
show ?case using insert by (cases "x = i") auto 

804 
qed simp 

805 
qed 

806 

807 
lemma setsum_Inf: 

808 
fixes f :: "'a \<Rightarrow> ereal" 

809 
shows "\<bar>setsum f A\<bar> = \<infinity> \<longleftrightarrow> finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)" 

810 
proof 

811 
assume *: "\<bar>setsum f A\<bar> = \<infinity>" 

812 
have "finite A" 

813 
by (rule ccontr) (insert *, auto) 

814 
moreover have "\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>" 

815 
proof (rule ccontr) 

816 
assume "\<not> ?thesis" 

817 
then have "\<forall>i\<in>A. \<exists>r. f i = ereal r" 

818 
by auto 

819 
from bchoice[OF this] obtain r where "\<forall>x\<in>A. f x = ereal (r x)" .. 

820 
with * show False 

821 
by auto 

822 
qed 

823 
ultimately show "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)" 

824 
by auto 

825 
next 

826 
assume "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)" 

827 
then obtain i where "finite A" "i \<in> A" and "\<bar>f i\<bar> = \<infinity>" 

828 
by auto 

829 
then show "\<bar>setsum f A\<bar> = \<infinity>" 

830 
proof induct 

831 
case (insert j A) 

832 
then show ?case 

833 
by (cases rule: ereal3_cases[of "f i" "f j" "setsum f A"]) auto 

834 
qed simp 

835 
qed 

836 

837 
lemma setsum_real_of_ereal: 

838 
fixes f :: "'i \<Rightarrow> ereal" 

839 
assumes "\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>" 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61245
diff
changeset

840 
shows "(\<Sum>x\<in>S. real_of_ereal (f x)) = real_of_ereal (setsum f S)" 
59000  841 
proof  
842 
have "\<forall>x\<in>S. \<exists>r. f x = ereal r" 

843 
proof 

844 
fix x 

845 
assume "x \<in> S" 

846 
from assms[OF this] show "\<exists>r. f x = ereal r" 

847 
by (cases "f x") auto 

848 
qed 

849 
from bchoice[OF this] obtain r where "\<forall>x\<in>S. f x = ereal (r x)" .. 

850 
then show ?thesis 

851 
by simp 

852 
qed 

853 

854 
lemma setsum_ereal_0: 

855 
fixes f :: "'a \<Rightarrow> ereal" 

856 
assumes "finite A" 

857 
and "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i" 

858 
shows "(\<Sum>x\<in>A. f x) = 0 \<longleftrightarrow> (\<forall>i\<in>A. f i = 0)" 

859 
proof 

860 
assume "setsum f A = 0" with assms show "\<forall>i\<in>A. f i = 0" 

861 
proof (induction A) 

862 
case (insert a A) 

863 
then have "f a = 0 \<and> (\<Sum>a\<in>A. f a) = 0" 

864 
by (subst ereal_add_nonneg_eq_0_iff[symmetric]) (simp_all add: setsum_nonneg) 

865 
with insert show ?case 

866 
by simp 

867 
qed simp 

868 
qed auto 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

869 

41973  870 
subsubsection "Multiplication" 
871 

53873  872 
instantiation ereal :: "{comm_monoid_mult,sgn}" 
41973  873 
begin 
874 

51351  875 
function sgn_ereal :: "ereal \<Rightarrow> ereal" where 
43920  876 
"sgn (ereal r) = ereal (sgn r)" 
43923  877 
 "sgn (\<infinity>::ereal) = 1" 
878 
 "sgn (\<infinity>::ereal) = 1" 

43920  879 
by (auto intro: ereal_cases) 
60679  880 
termination by standard (rule wf_empty) 
41976  881 

43920  882 
function times_ereal where 
53873  883 
"ereal r * ereal p = ereal (r * p)" 
884 
 "ereal r * \<infinity> = (if r = 0 then 0 else if r > 0 then \<infinity> else \<infinity>)" 

885 
 "\<infinity> * ereal r = (if r = 0 then 0 else if r > 0 then \<infinity> else \<infinity>)" 

886 
 "ereal r * \<infinity> = (if r = 0 then 0 else if r > 0 then \<infinity> else \<infinity>)" 

887 
 "\<infinity> * ereal r = (if r = 0 then 0 else if r > 0 then \<infinity> else \<infinity>)" 

888 
 "(\<infinity>::ereal) * \<infinity> = \<infinity>" 

889 
 "(\<infinity>::ereal) * \<infinity> = \<infinity>" 

890 
 "(\<infinity>::ereal) * \<infinity> = \<infinity>" 

891 
 "(\<infinity>::ereal) * \<infinity> = \<infinity>" 

61166
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61120
diff
changeset

892 
proof goal_cases 
60580  893 
case prems: (1 P x) 
53873  894 
then obtain a b where "x = (a, b)" 
895 
by (cases x) auto 

60580  896 
with prems show P 
53873  897 
by (cases rule: ereal2_cases[of a b]) auto 
41973  898 
qed simp_all 
899 
termination by (relation "{}") simp 

900 

901 
instance 

902 
proof 

53873  903 
fix a b c :: ereal 
904 
show "1 * a = a" 

43920  905 
by (cases a) (simp_all add: one_ereal_def) 
47082  906 
show "a * b = b * a" 
43920  907 
by (cases rule: ereal2_cases[of a b]) simp_all 
47082  908 
show "a * b * c = a * (b * c)" 
43920  909 
by (cases rule: ereal3_cases[of a b c]) 
910 
(simp_all add: zero_ereal_def zero_less_mult_iff) 

41973  911 
qed 
53873  912 

41973  913 
end 
914 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61631
diff
changeset

915 
lemma [simp]: 
61631
4f7ef088c4ed
add lemmas for extended nats and reals
Andreas Lochbihler
parents:
61610
diff
changeset

916 
shows ereal_1_times: "ereal 1 * x = x" 
4f7ef088c4ed
add lemmas for extended nats and reals
Andreas Lochbihler
parents:
61610
diff
changeset

917 
and times_ereal_1: "x * ereal 1 = x" 
4f7ef088c4ed
add lemmas for extended nats and reals
Andreas Lochbihler
parents:
61610
diff
changeset

918 
by(simp_all add: one_ereal_def[symmetric]) 
4f7ef088c4ed
add lemmas for extended nats and reals
Andreas Lochbihler
parents:
61610
diff
changeset

919 

59000  920 
lemma one_not_le_zero_ereal[simp]: "\<not> (1 \<le> (0::ereal))" 
921 
by (simp add: one_ereal_def zero_ereal_def) 

922 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61245
diff
changeset

923 
lemma real_ereal_1[simp]: "real_of_ereal (1::ereal) = 1" 
50104  924 
unfolding one_ereal_def by simp 
925 

43920  926 
lemma real_of_ereal_le_1: 
53873  927 
fixes a :: ereal 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61245
diff
changeset

928 
shows "a \<le> 1 \<Longrightarrow> real_of_ereal a \<le> 1" 
43920  929 
by (cases a) (auto simp: one_ereal_def) 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

930 

43920  931 
lemma abs_ereal_one[simp]: "\<bar>1\<bar> = (1::ereal)" 
932 
unfolding one_ereal_def by simp 

41976  933 

43920  934 
lemma ereal_mult_zero[simp]: 
53873  935 
fixes a :: ereal 
936 
shows "a * 0 = 0" 

43920  937 
by (cases a) (simp_all add: zero_ereal_def) 
41973  938 

43920  939 
lemma ereal_zero_mult[simp]: 
53873  940 
fixes a :: ereal 
941 
shows "0 * a = 0" 

43920  942 
by (cases a) (simp_all add: zero_ereal_def) 
41973  943 

53873  944 
lemma ereal_m1_less_0[simp]: "(1::ereal) < 0" 
43920  945 
by (simp add: zero_ereal_def one_ereal_def) 
41973  946 

43920  947 
lemma ereal_times[simp]: 
43923  948 
"1 \<noteq> (\<infinity>::ereal)" "(\<infinity>::ereal) \<noteq> 1" 
949 
"1 \<noteq> (\<infinity>::ereal)" "(\<infinity>::ereal) \<noteq> 1" 

61120  950 
by (auto simp: one_ereal_def) 
41973  951 

43920  952 
lemma ereal_plus_1[simp]: 
53873  953 
"1 + ereal r = ereal (r + 1)" 
954 
"ereal r + 1 = ereal (r + 1)" 

955 
"1 + (\<infinity>::ereal) = \<infinity>" 

956 
"(\<infinity>::ereal) + 1 = \<infinity>" 

43920  957 
unfolding one_ereal_def by auto 
41973  958 

43920  959 
lemma ereal_zero_times[simp]: 
53873  960 
fixes a b :: ereal 
961 
shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0" 

43920  962 
by (cases rule: ereal2_cases[of a b]) auto 
41973  963 

43920  964 
lemma ereal_mult_eq_PInfty[simp]: 
53873  965 
"a * b = (\<infinity>::ereal) \<longleftrightarrow> 
41973  966 
(a = \<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = \<infinity>) \<or> (a = \<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = \<infinity>)" 
43920  967 
by (cases rule: ereal2_cases[of a b]) auto 
41973  968 

43920  969 
lemma ereal_mult_eq_MInfty[simp]: 
53873  970 
"a * b = (\<infinity>::ereal) \<longleftrightarrow> 
41973  971 
(a = \<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = \<infinity>) \<or> (a = \<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = \<infinity>)" 
43920  972 
by (cases rule: ereal2_cases[of a b]) auto 
41973  973 

54416  974 
lemma ereal_abs_mult: "\<bar>x * y :: ereal\<bar> = \<bar>x\<bar> * \<bar>y\<bar>" 
975 
by (cases x y rule: ereal2_cases) (auto simp: abs_mult) 

976 

43920  977 
lemma ereal_0_less_1[simp]: "0 < (1::ereal)" 
978 
by (simp_all add: zero_ereal_def one_ereal_def) 

41973  979 

43920  980 
lemma ereal_mult_minus_left[simp]: 
53873  981 
fixes a b :: ereal 
982 
shows "a * b =  (a * b)" 

43920  983 
by (cases rule: ereal2_cases[of a b]) auto 
41973  984 

43920  985 
lemma ereal_mult_minus_right[simp]: 
53873  986 
fixes a b :: ereal 
987 
shows "a * b =  (a * b)" 

43920  988 
by (cases rule: ereal2_cases[of a b]) auto 
41973  989 

43920  990 
lemma ereal_mult_infty[simp]: 
43923  991 
"a * (\<infinity>::ereal) = (if a = 0 then 0 else if 0 < a then \<infinity> else  \<infinity>)" 
41973  992 
by (cases a) auto 
993 

43920  994 
lemma ereal_infty_mult[simp]: 
43923  995 
"(\<infinity>::ereal) * a = (if a = 0 then 0 else if 0 < a then \<infinity> else  \<infinity>)" 
41973  996 
by (cases a) auto 
997 

43920  998 
lemma ereal_mult_strict_right_mono: 
53873  999 
assumes "a < b" 
1000 
and "0 < c" 

1001 
and "c < (\<infinity>::ereal)" 

41973  1002 
shows "a * c < b * c" 
1003 
using assms 

53873  1004 
by (cases rule: ereal3_cases[of a b c]) (auto simp: zero_le_mult_iff) 
41973  1005 

43920  1006 
lemma ereal_mult_strict_left_mono: 
53873  1007 
"a < b \<Longrightarrow> 0 < c \<Longrightarrow> c < (\<infinity>::ereal) \<Longrightarrow> c * a < c * b" 
1008 
using ereal_mult_strict_right_mono 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57447
diff
changeset

1009 
by (simp add: mult.commute[of c]) 
41973  1010 

43920  1011 
lemma ereal_mult_right_mono: 
53873  1012 
fixes a b c :: ereal 
1013 
shows "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c" 

41973  1014 
using assms 
53873  1015 
apply (cases "c = 0") 
1016 
apply simp 

1017 
apply (cases rule: ereal3_cases[of a b c]) 

1018 
apply (auto simp: zero_le_mult_iff) 

1019 
done 

41973  1020 

43920  1021 
lemma ereal_mult_left_mono: 
53873  1022 
fixes a b c :: ereal 
1023 
shows "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" 

1024 
using ereal_mult_right_mono 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57447
diff
changeset

1025 
by (simp add: mult.commute[of c]) 
41973  1026 

43920  1027 
lemma zero_less_one_ereal[simp]: "0 \<le> (1::ereal)" 
1028 
by (simp add: one_ereal_def zero_ereal_def) 

41978  1029 

43920  1030 
lemma ereal_0_le_mult[simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * (b :: ereal)" 
56536  1031 
by (cases rule: ereal2_cases[of a b]) auto 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1032 

43920  1033 
lemma ereal_right_distrib: 
53873  1034 
fixes r a b :: ereal 
1035 
shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> r * (a + b) = r * a + r * b" 

43920  1036 
by (cases rule: ereal3_cases[of r a b]) (simp_all add: field_simps) 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1037 

43920  1038 
lemma ereal_left_distrib: 
53873  1039 
fixes r a b :: ereal 
1040 
shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> (a + b) * r = a * r + b * r" 

43920  1041 
by (cases rule: ereal3_cases[of r a b]) (simp_all add: field_simps) 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1042 

43920  1043 
lemma ereal_mult_le_0_iff: 
1044 
fixes a b :: ereal 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1045 
shows "a * b \<le> 0 \<longleftrightarrow> (0 \<le> a \<and> b \<le> 0) \<or> (a \<le> 0 \<and> 0 \<le> b)" 
43920  1046 
by (cases rule: ereal2_cases[of a b]) (simp_all add: mult_le_0_iff) 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1047 

43920  1048 
lemma ereal_zero_le_0_iff: 
1049 
fixes a b :: ereal 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1050 
shows "0 \<le> a * b \<longleftrightarrow> (0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0)" 
43920  1051 
by (cases rule: ereal2_cases[of a b]) (simp_all add: zero_le_mult_iff) 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1052 

43920  1053 
lemma ereal_mult_less_0_iff: 
1054 
fixes a b :: ereal 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1055 
shows "a * b < 0 \<longleftrightarrow> (0 < a \<and> b < 0) \<or> (a < 0 \<and> 0 < b)" 
43920  1056 
by (cases rule: ereal2_cases[of a b]) (simp_all add: mult_less_0_iff) 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1057 

43920  1058 
lemma ereal_zero_less_0_iff: 
1059 
fixes a b :: ereal 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1060 
shows "0 < a * b \<longleftrightarrow> (0 < a \<and> 0 < b) \<or> (a < 0 \<and> b < 0)" 
43920  1061 
by (cases rule: ereal2_cases[of a b]) (simp_all add: zero_less_mult_iff) 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1062 

50104  1063 
lemma ereal_left_mult_cong: 
1064 
fixes a b c :: ereal 

59002
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset

1065 
shows "c = d \<Longrightarrow> (d \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> a * c = b * d" 
50104  1066 
by (cases "c = 0") simp_all 
1067 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61631
diff
changeset

1068 
lemma ereal_right_mult_cong: 
59002
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset

1069 
fixes a b c :: ereal 
59000  1070 
shows "c = d \<Longrightarrow> (d \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> c * a = d * b" 
59002
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset

1071 
by (cases "c = 0") simp_all 
50104  1072 

43920  1073 
lemma ereal_distrib: 
1074 
fixes a b c :: ereal 

53873  1075 
assumes "a \<noteq> \<infinity> \<or> b \<noteq> \<infinity>" 
1076 
and "a \<noteq> \<infinity> \<or> b \<noteq> \<infinity>" 

1077 
and "\<bar>c\<bar> \<noteq> \<infinity>" 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1078 
shows "(a + b) * c = a * c + b * c" 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1079 
using assms 
43920  1080 
by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps) 
41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1081 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47082
diff
changeset

1082 
lemma numeral_eq_ereal [simp]: "numeral w = ereal (numeral w)" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47082
diff
changeset

1083 
apply (induct w rule: num_induct) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47082
diff
changeset

1084 
apply (simp only: numeral_One one_ereal_def) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47082
diff
changeset

1085 
apply (simp only: numeral_inc ereal_plus_1) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47082
diff
changeset

1086 
done 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47082
diff
changeset

1087 

61631
4f7ef088c4ed
add lemmas for extended nats and reals
Andreas Lochbihler
parents:
61610
diff
changeset

1088 
lemma distrib_left_ereal_nn: 
4f7ef088c4ed
add lemmas for extended nats and reals
Andreas Lochbihler
parents:
61610
diff
changeset

1089 
"c \<ge> 0 \<Longrightarrow> (x + y) * ereal c = x * ereal c + y * ereal c" 
4f7ef088c4ed
add lemmas for extended nats and reals
Andreas Lochbihler
parents:
61610
diff
changeset

1090 
by(cases x y rule: ereal2_cases)(simp_all add: ring_distribs) 
4f7ef088c4ed
add lemmas for extended nats and reals
Andreas Lochbihler
parents:
61610
diff
changeset

1091 

59000  1092 
lemma setsum_ereal_right_distrib: 
1093 
fixes f :: "'a \<Rightarrow> ereal" 

1094 
shows "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> r * setsum f A = (\<Sum>n\<in>A. r * f n)" 

1095 
by (induct A rule: infinite_finite_induct) (auto simp: ereal_right_distrib setsum_nonneg) 

1096 

59002
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset

1097 
lemma setsum_ereal_left_distrib: 
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset

1098 
"(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> setsum f A * r = (\<Sum>n\<in>A. f n * r :: ereal)" 
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset

1099 
using setsum_ereal_right_distrib[of A f r] by (simp add: mult_ac) 
2c8b2fb54b88
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
hoelzl
parents:
59000
diff
changeset

1100 

61631
4f7ef088c4ed
add lemmas for extended nats and reals
Andreas Lochbihler
parents:
61610
diff
changeset

1101 
lemma setsum_left_distrib_ereal: 
4f7ef088c4ed
add lemmas for extended nats and reals
Andreas Lochbihler
parents:
61610
diff
changeset

1102 
"c \<ge> 0 \<Longrightarrow> setsum f A * ereal c = (\<Sum>x\<in>A. f x * c :: ereal)" 
4f7ef088c4ed
add lemmas for extended nats and reals
Andreas Lochbihler
parents:
61610
diff
changeset

1103 
by(subst setsum_comp_morphism[where h="\<lambda>x. x * ereal c", symmetric])(simp_all add: distrib_left_ereal_nn) 
4f7ef088c4ed
add lemmas for extended nats and reals
Andreas Lochbihler
parents:
61610
diff
changeset

1104 

43920  1105 
lemma ereal_le_epsilon: 
1106 
fixes x y :: ereal 

53873  1107 
assumes "\<forall>e. 0 < e \<longrightarrow> x \<le> y + e" 
1108 
shows "x \<le> y" 

1109 
proof  

1110 
{ 

1111 
assume a: "\<exists>r. y = ereal r" 

1112 
then obtain r where r_def: "y = ereal r" 

1113 
by auto 

1114 
{ 

1115 
assume "x = \<infinity>" 

1116 
then have ?thesis by auto 

1117 
} 

1118 
moreover 

1119 
{ 

1120 
assume "x \<noteq> \<infinity>" 

1121 
then obtain p where p_def: "x = ereal p" 

1122 
using a assms[rule_format, of 1] 

1123 
by (cases x) auto 

1124 
{ 

1125 
fix e 

1126 
have "0 < e \<longrightarrow> p \<le> r + e" 

1127 
using assms[rule_format, of "ereal e"] p_def r_def by auto 

1128 
} 

1129 
then have "p \<le> r" 

1130 
apply (subst field_le_epsilon) 

1131 
apply auto 

1132 
done 

1133 
then have ?thesis 

1134 
using r_def p_def by auto 

1135 
} 

1136 
ultimately have ?thesis 

1137 
by blast 

1138 
} 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1139 
moreover 
53873  1140 
{ 
1141 
assume "y = \<infinity>  y = \<infinity>" 

1142 
then have ?thesis 

1143 
using assms[rule_format, of 1] by (cases x) auto 

1144 
} 

1145 
ultimately show ?thesis 

1146 
by (cases y) auto 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1147 
qed 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1148 

43920  1149 
lemma ereal_le_epsilon2: 
1150 
fixes x y :: ereal 

53873  1151 
assumes "\<forall>e. 0 < e \<longrightarrow> x \<le> y + ereal e" 
1152 
shows "x \<le> y" 

1153 
proof  

1154 
{ 

1155 
fix e :: ereal 

1156 
assume "e > 0" 

1157 
{ 

1158 
assume "e = \<infinity>" 

1159 
then have "x \<le> y + e" 

1160 
by auto 

1161 
} 

1162 
moreover 

1163 
{ 

1164 
assume "e \<noteq> \<infinity>" 

1165 
then obtain r where "e = ereal r" 

60500  1166 
using \<open>e > 0\<close> by (cases e) auto 
53873  1167 
then have "x \<le> y + e" 
60500  1168 
using assms[rule_format, of r] \<open>e>0\<close> by auto 
53873  1169 
} 
1170 
ultimately have "x \<le> y + e" 

1171 
by blast 

1172 
} 

1173 
then show ?thesis 

1174 
using ereal_le_epsilon by auto 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1175 
qed 
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1176 

43920  1177 
lemma ereal_le_real: 
1178 
fixes x y :: ereal 

53873  1179 
assumes "\<forall>z. x \<le> ereal z \<longrightarrow> y \<le> ereal z" 
1180 
shows "y \<le> x" 

1181 
by (metis assms ereal_bot ereal_cases ereal_infty_less_eq(2) ereal_less_eq(1) linorder_le_cases) 

41979
b10ec1f5e9d5
lemmas about addition, SUP on countable sets and infinite sums for extreal
hoelzl
parents:
41978
diff
changeset

1182 

43920  1183 
lemma setprod_ereal_0: 
1184 
fixes f :: "'a \<Rightarrow> ereal" 

53873  1185 
shows "(\<Prod>i\<in>A. f i) = 0 \<longleftrightarrow> finite A \<and> (\<exists>i\<in>A. f i = 0)" 
1186 
proof (cases "finite A") 

1187 
case True 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

1188 
then show ?thesis by (induct A) auto 
53873  1189 
next 
1190 
case False 

1191 
then show ?thesis by auto 

1192 
qed 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

1193 

43920  1194 
lemma setprod_ereal_pos: 
53873  1195 
fixes f :: "'a \<Rightarrow> ereal" 
1196 
assumes pos: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" 

1197 
shows "0 \<le> (\<Prod>i\<in>I. f i)" 

1198 
proof (cases "finite I") 

1199 
case True 

1200 
from this pos show ?thesis 

1201 
by induct auto 

1202 
next 

1203 
case False 

1204 
then show ?thesis by simp 

1205 
qed 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

1206 

6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

1207 
lemma setprod_PInf: 
43923  1208 
fixes f :: "'a \<Rightarrow> ereal" 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

1209 
assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

1210 
shows "(\<Prod>i\<in>I. f i) = \<infinity> \<longleftrightarrow> finite I \<and> (\<exists>i\<in>I. f i = \<infinity>) \<and> (\<forall>i\<in>I. f i \<noteq> 0)" 
53873  1211 
proof (cases "finite I") 
1212 
case True 

1213 
from this assms show ?thesis 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

1214 
proof (induct I) 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

1215 
case (insert i I) 
53873  1216 
then have pos: "0 \<le> f i" "0 \<le> setprod f I" 
1217 
by (auto intro!: setprod_ereal_pos) 

1218 
from insert have "(\<Prod>j\<in>insert i I. f j) = \<infinity> \<longleftrightarrow> setprod f I * f i = \<infinity>" 

1219 
by auto 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

1220 
also have "\<dots> \<longleftrightarrow> (setprod f I = \<infinity> \<or> f i = \<infinity>) \<and> f i \<noteq> 0 \<and> setprod f I \<noteq> 0" 
43920  1221 
using setprod_ereal_pos[of I f] pos 
1222 
by (cases rule: ereal2_cases[of "f i" "setprod f I"]) auto 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

1223 
also have "\<dots> \<longleftrightarrow> finite (insert i I) \<and> (\<exists>j\<in>insert i I. f j = \<infinity>) \<and> (\<forall>j\<in>insert i I. f j \<noteq> 0)" 
43920  1224 
using insert by (auto simp: setprod_ereal_0) 
42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

1225 
finally show ?case . 
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

1226 
qed simp 
53873  1227 
next 
1228 
case False 

1229 
then show ?thesis by simp 

1230 
qed 

42950
6e5c2a3c69da
move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents:
42600
diff
changeset

1231 

43920  1232 
lemma setprod_ereal: "(\<Prod>i\<in>A. ereal (f i)) = ereal (setprod f A)" 
53873  1233 
proof (cases "finite A") 
1234 
case True 

1235 
then show ?thesis 

43920  1236 
by induct (auto simp: one_ereal_def) 
53873  12 