author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 64272  f76b6dda2e56 
child 65680  378a2f11bec9 
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 

62626
de25474ce728
Contractible sets. Also removal of obsolete theorems and refactoring
paulson <lp15@cam.ac.uk>
parents:
62390
diff
changeset

15 
text \<open>This should be part of @{theory Extended_Nat} or @{theory Order_Continuity}, but then the 
de25474ce728
Contractible sets. Also removal of obsolete theorems and refactoring
paulson <lp15@cam.ac.uk>
parents:
62390
diff
changeset

16 
AFPentry \<open>Jinja_Thread\<close> fails, as it does overload certain named from @{theory Complex_Main}.\<close> 
62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62371
diff
changeset

17 

64267  18 
lemma incseq_sumI2: 
62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62371
diff
changeset

19 
fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::ordered_comm_monoid_add" 
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62371
diff
changeset

20 
shows "(\<And>n. n \<in> A \<Longrightarrow> mono (f n)) \<Longrightarrow> mono (\<lambda>i. \<Sum>n\<in>A. f n i)" 
64267  21 
unfolding incseq_def by (auto intro: sum_mono) 
22 

23 
lemma incseq_sumI: 

62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62371
diff
changeset

24 
fixes f :: "nat \<Rightarrow> 'a::ordered_comm_monoid_add" 
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62371
diff
changeset

25 
assumes "\<And>i. 0 \<le> f i" 
64267  26 
shows "incseq (\<lambda>i. sum f {..< i})" 
62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62371
diff
changeset

27 
proof (intro incseq_SucI) 
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62371
diff
changeset

28 
fix n 
64267  29 
have "sum f {..< n} + 0 \<le> sum f {..<n} + f n" 
62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62371
diff
changeset

30 
using assms by (rule add_left_mono) 
64267  31 
then show "sum f {..< n} \<le> sum f {..< Suc n}" 
62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62371
diff
changeset

32 
by auto 
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62371
diff
changeset

33 
qed 
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62371
diff
changeset

34 

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

35 
lemma continuous_at_left_imp_sup_continuous: 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

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

37 
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

38 
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

39 
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

40 
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

41 
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

42 
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

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

44 

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

45 
lemma sup_continuous_at_left: 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

46 
fixes f :: "'a::{complete_linorder, linorder_topology, first_countable_topology} \<Rightarrow> 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

47 
'b::{complete_linorder, linorder_topology}" 
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 
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

49 
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

50 
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

51 
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

52 
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

53 
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

54 
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

55 
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

56 
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

57 
proof (intro tendsto_at_left_sequentially[of bot]) 
61969  58 
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

59 
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

60 
by (rule LIMSEQ_unique) (intro LIMSEQ_SUP S) 
61969  61 
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

62 
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

63 
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

64 
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

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

66 

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

67 
lemma sup_continuous_iff_at_left: 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

68 
fixes f :: "'a::{complete_linorder, linorder_topology, first_countable_topology} \<Rightarrow> 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

69 
'b::{complete_linorder, linorder_topology}" 
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

70 
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

71 
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

72 
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

73 

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

74 
lemma continuous_at_right_imp_inf_continuous: 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

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

76 
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

77 
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

78 
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

79 
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

80 
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

81 
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

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

83 

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

84 
lemma inf_continuous_at_right: 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

85 
fixes f :: "'a::{complete_linorder, linorder_topology, first_countable_topology} \<Rightarrow> 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

86 
'b::{complete_linorder, linorder_topology}" 
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

87 
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

88 
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

89 
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

90 
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

91 
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

92 
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

93 
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

94 
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

95 
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

96 
proof (intro tendsto_at_right_sequentially[of _ top]) 
61969  97 
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

98 
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

99 
by (rule LIMSEQ_unique) (intro LIMSEQ_INF S) 
61969  100 
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

101 
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

102 
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

103 
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

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

105 

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

106 
lemma inf_continuous_iff_at_right: 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

107 
fixes f :: "'a::{complete_linorder, linorder_topology, first_countable_topology} \<Rightarrow> 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

108 
'b::{complete_linorder, linorder_topology}" 
60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
60060
diff
changeset

109 
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

110 
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

111 
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

112 

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

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

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

115 

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

116 
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

117 
"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

118 

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

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

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

121 

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

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

123 

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

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

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

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

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

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

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

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

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

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

133 
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

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

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

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

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

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

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

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

141 

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

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

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

144 
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

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

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

147 
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

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

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

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

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

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

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

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

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

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

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

158 
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

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

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

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

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

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

164 
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

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

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

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

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

169 
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

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

171 
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

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

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

174 
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

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

176 
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

177 
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

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

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

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

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

182 
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

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

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

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

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

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

188 

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

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

192 
unfolding nhds_def 

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

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

195 
subgoal for x i 

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

197 
done 

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

199 
by (simp add: nhds_discrete_open open_enat) 

200 
qed 

201 

202 
instance enat :: topological_comm_monoid_add 

203 
proof 

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

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

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

207 
by (metis add.commute) 

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

209 
apply (auto simp: nhds_enat filterlim_INF prod_filter_INF1 prod_filter_INF2 

210 
filterlim_principal principal_prod_principal eventually_principal) 

211 
subgoal for i 

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

213 
subgoal for j i 

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

215 
subgoal for j i 

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

217 
done 

218 
qed 

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

219 

60500  220 
text \<open> 
63680  221 
For more lemmas about the extended real numbers see 
222 
\<^file>\<open>~~/src/HOL/Analysis/Extended_Real_Limits.thy\<close>. 

60500  223 
\<close> 
224 

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

41973  226 

58310  227 
datatype ereal = ereal real  PInfty  MInfty 
41973  228 

63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

229 
lemma ereal_cong: "x = y \<Longrightarrow> ereal x = ereal y" by simp 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

230 

43920  231 
instantiation ereal :: uminus 
41973  232 
begin 
53873  233 

234 
fun uminus_ereal where 

235 
" (ereal r) = ereal ( r)" 

236 
 " PInfty = MInfty" 

237 
 " MInfty = PInfty" 

238 

239 
instance .. 

240 

41973  241 
end 
242 

43923  243 
instantiation ereal :: infinity 
244 
begin 

53873  245 

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

247 
instance .. 

248 

43923  249 
end 
41973  250 

43923  251 
declare [[coercion "ereal :: real \<Rightarrow> ereal"]] 
41973  252 

43920  253 
lemma ereal_uminus_uminus[simp]: 
53873  254 
fixes a :: ereal 
255 
shows " ( a) = a" 

41973  256 
by (cases a) simp_all 
257 

43923  258 
lemma 
259 
shows PInfty_eq_infinity[simp]: "PInfty = \<infinity>" 

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

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

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

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

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

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

266 
by (simp_all add: infinity_ereal_def) 

41973  267 

43933  268 
declare 
269 
PInfty_eq_infinity[code_post] 

270 
MInfty_eq_minfinity[code_post] 

271 

272 
lemma [code_unfold]: 

273 
"\<infinity> = PInfty" 

53873  274 
" PInfty = MInfty" 
43933  275 
by simp_all 
276 

43923  277 
lemma inj_ereal[simp]: "inj_on ereal A" 
278 
unfolding inj_on_def by auto 

41973  279 

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

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

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

63092  284 
by (cases x) auto 
41973  285 

43920  286 
lemmas ereal2_cases = ereal_cases[case_product ereal_cases] 
287 
lemmas ereal3_cases = ereal2_cases[case_product ereal_cases] 

41973  288 

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

289 
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

290 
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

291 

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

292 
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

293 
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

294 

43920  295 
lemma ereal_uminus_eq_iff[simp]: 
53873  296 
fixes a b :: ereal 
297 
shows "a = b \<longleftrightarrow> a = b" 

43920  298 
by (cases rule: ereal2_cases[of a b]) simp_all 
41973  299 

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

300 
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

301 
"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

302 
 "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

303 
 "real_of_ereal (\<infinity>) = 0" 
43920  304 
by (auto intro: ereal_cases) 
60679  305 
termination by standard (rule wf_empty) 
41973  306 

43920  307 
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

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

309 
by (cases x) simp_all 
41973  310 

43920  311 
lemma range_ereal[simp]: "range ereal = UNIV  {\<infinity>, \<infinity>}" 
41973  312 
proof safe 
53873  313 
fix x 
314 
assume "x \<notin> range ereal" "x \<noteq> \<infinity>" 

315 
then show "x = \<infinity>" 

316 
by (cases x) auto 

41973  317 
qed auto 
318 

43920  319 
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

320 
proof safe 
53873  321 
fix x :: ereal 
322 
show "x \<in> range uminus" 

323 
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

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

325 

43920  326 
instantiation ereal :: abs 
41976  327 
begin 
53873  328 

329 
function abs_ereal where 

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

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

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

333 
by (auto intro: ereal_cases) 

334 
termination proof qed (rule wf_empty) 

335 

336 
instance .. 

337 

41976  338 
end 
339 

53873  340 
lemma abs_eq_infinity_cases[elim!]: 
341 
fixes x :: ereal 

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

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

344 
using assms by (cases x) auto 

41976  345 

53873  346 
lemma abs_neq_infinity_cases[elim!]: 
347 
fixes x :: ereal 

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

349 
obtains r where "x = ereal r" 

350 
using assms by (cases x) auto 

351 

352 
lemma abs_ereal_uminus[simp]: 

353 
fixes x :: ereal 

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

41976  355 
by (cases x) auto 
356 

53873  357 
lemma ereal_infinity_cases: 
358 
fixes a :: ereal 

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

360 
by auto 

41976  361 

41973  362 
subsubsection "Addition" 
363 

54408  364 
instantiation ereal :: "{one,comm_monoid_add,zero_neq_one}" 
41973  365 
begin 
366 

43920  367 
definition "0 = ereal 0" 
51351  368 
definition "1 = ereal 1" 
41973  369 

43920  370 
function plus_ereal where 
53873  371 
"ereal r + ereal p = ereal (r + p)" 
372 
 "\<infinity> + a = (\<infinity>::ereal)" 

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

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

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

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

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

377 
proof goal_cases 
60580  378 
case prems: (1 P x) 
53873  379 
then obtain a b where "x = (a, b)" 
380 
by (cases x) auto 

60580  381 
with prems show P 
43920  382 
by (cases rule: ereal2_cases[of a b]) auto 
41973  383 
qed auto 
60679  384 
termination by standard (rule wf_empty) 
41973  385 

386 
lemma Infty_neq_0[simp]: 

43923  387 
"(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> (\<infinity>::ereal)" 
388 
"(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> (\<infinity>::ereal)" 

43920  389 
by (simp_all add: zero_ereal_def) 
41973  390 

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

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

394 
unfolding zero_ereal_def by simp_all 

41973  395 

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

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

399 
unfolding one_ereal_def by simp_all 

400 

41973  401 
instance 
402 
proof 

47082  403 
fix a b c :: ereal 
404 
show "0 + a = a" 

43920  405 
by (cases a) (simp_all add: zero_ereal_def) 
47082  406 
show "a + b = b + a" 
43920  407 
by (cases rule: ereal2_cases[of a b]) simp_all 
47082  408 
show "a + b + c = a + (b + c)" 
43920  409 
by (cases rule: ereal3_cases[of a b c]) simp_all 
54408  410 
show "0 \<noteq> (1::ereal)" 
411 
by (simp add: one_ereal_def zero_ereal_def) 

41973  412 
qed 
53873  413 

41973  414 
end 
415 

60060  416 
lemma ereal_0_plus [simp]: "ereal 0 + x = x" 
417 
and plus_ereal_0 [simp]: "x + ereal 0 = x" 

418 
by(simp_all add: zero_ereal_def[symmetric]) 

419 

51351  420 
instance ereal :: numeral .. 
421 

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

422 
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

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

424 

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

41976  427 

53873  428 
lemma ereal_uminus_zero[simp]: " 0 = (0::ereal)" 
43920  429 
by (simp add: zero_ereal_def) 
41973  430 

43920  431 
lemma ereal_uminus_zero_iff[simp]: 
53873  432 
fixes a :: ereal 
433 
shows "a = 0 \<longleftrightarrow> a = 0" 

41973  434 
by (cases a) simp_all 
435 

43920  436 
lemma ereal_plus_eq_PInfty[simp]: 
53873  437 
fixes a b :: ereal 
438 
shows "a + b = \<infinity> \<longleftrightarrow> a = \<infinity> \<or> b = \<infinity>" 

43920  439 
by (cases rule: ereal2_cases[of a b]) auto 
41973  440 

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

43920  444 
by (cases rule: ereal2_cases[of a b]) auto 
41973  445 

43920  446 
lemma ereal_add_cancel_left: 
53873  447 
fixes a b :: ereal 
448 
assumes "a \<noteq> \<infinity>" 

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

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

43920  452 
lemma ereal_add_cancel_right: 
53873  453 
fixes a b :: ereal 
454 
assumes "a \<noteq> \<infinity>" 

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

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

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

458 
lemma ereal_real: "ereal (real_of_ereal x) = (if \<bar>x\<bar> = \<infinity> then 0 else x)" 
41973  459 
by (cases x) simp_all 
460 

43920  461 
lemma real_of_ereal_add: 
462 
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

463 
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

464 
(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  465 
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

466 

53873  467 

43920  468 
subsubsection "Linear order on @{typ ereal}" 
41973  469 

43920  470 
instantiation ereal :: linorder 
41973  471 
begin 
472 

47082  473 
function less_ereal 
474 
where 

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

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

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

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

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

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

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

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

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

487 

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

43920  490 
lemma ereal_infty_less[simp]: 
43923  491 
fixes x :: ereal 
492 
shows "x < \<infinity> \<longleftrightarrow> (x \<noteq> \<infinity>)" 

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

41973  494 
by (cases x, simp_all) (cases x, simp_all) 
495 

43920  496 
lemma ereal_infty_less_eq[simp]: 
43923  497 
fixes x :: ereal 
498 
shows "\<infinity> \<le> x \<longleftrightarrow> x = \<infinity>" 

53873  499 
and "x \<le> \<infinity> \<longleftrightarrow> x = \<infinity>" 
43920  500 
by (auto simp add: less_eq_ereal_def) 
41973  501 

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

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

54416  505 
"ereal r < 1 \<longleftrightarrow> (r < 1)" 
506 
"1 < ereal r \<longleftrightarrow> (1 < r)" 

43923  507 
"0 < (\<infinity>::ereal)" 
508 
"(\<infinity>::ereal) < 0" 

54416  509 
by (simp_all add: zero_ereal_def one_ereal_def) 
41973  510 

43920  511 
lemma ereal_less_eq[simp]: 
43923  512 
"x \<le> (\<infinity>::ereal)" 
513 
"(\<infinity>::ereal) \<le> x" 

43920  514 
"ereal r \<le> ereal p \<longleftrightarrow> r \<le> p" 
515 
"ereal r \<le> 0 \<longleftrightarrow> r \<le> 0" 

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

54416  517 
"ereal r \<le> 1 \<longleftrightarrow> r \<le> 1" 
518 
"1 \<le> ereal r \<longleftrightarrow> 1 \<le> r" 

519 
by (auto simp add: less_eq_ereal_def zero_ereal_def one_ereal_def) 

41973  520 

43920  521 
lemma ereal_infty_less_eq2: 
43923  522 
"a \<le> b \<Longrightarrow> a = \<infinity> \<Longrightarrow> b = (\<infinity>::ereal)" 
523 
"a \<le> b \<Longrightarrow> b = \<infinity> \<Longrightarrow> a = (\<infinity>::ereal)" 

41973  524 
by simp_all 
525 

526 
instance 

527 
proof 

47082  528 
fix x y z :: ereal 
529 
show "x \<le> x" 

41973  530 
by (cases x) simp_all 
47082  531 
show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x" 
43920  532 
by (cases rule: ereal2_cases[of x y]) auto 
41973  533 
show "x \<le> y \<or> y \<le> x " 
43920  534 
by (cases rule: ereal2_cases[of x y]) auto 
53873  535 
{ 
536 
assume "x \<le> y" "y \<le> x" 

537 
then show "x = y" 

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

539 
} 

540 
{ 

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

542 
then show "x \<le> z" 

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

544 
} 

41973  545 
qed 
47082  546 

41973  547 
end 
548 

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

549 
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

550 
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

551 

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

554 

62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62371
diff
changeset

555 
instance ereal :: ordered_comm_monoid_add 
41978  556 
proof 
53873  557 
fix a b c :: ereal 
558 
assume "a \<le> b" 

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

43920  560 
by (cases rule: ereal3_cases[of a b c]) auto 
41978  561 
qed 
562 

62648  563 
lemma ereal_one_not_less_zero_ereal[simp]: "\<not> 1 < (0::ereal)" 
564 
by (simp add: zero_ereal_def) 

565 

43920  566 
lemma real_of_ereal_positive_mono: 
53873  567 
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

568 
shows "0 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<noteq> \<infinity> \<Longrightarrow> real_of_ereal x \<le> real_of_ereal y" 
43920  569 
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

570 

43920  571 
lemma ereal_MInfty_lessI[intro, simp]: 
53873  572 
fixes a :: ereal 
573 
shows "a \<noteq> \<infinity> \<Longrightarrow> \<infinity> < a" 

41973  574 
by (cases a) auto 
575 

43920  576 
lemma ereal_less_PInfty[intro, simp]: 
53873  577 
fixes a :: ereal 
578 
shows "a \<noteq> \<infinity> \<Longrightarrow> a < \<infinity>" 

41973  579 
by (cases a) auto 
580 

43920  581 
lemma ereal_less_ereal_Ex: 
582 
fixes a b :: ereal 

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

41973  584 
by (cases x) auto 
585 

43920  586 
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

587 
proof (cases x) 
53873  588 
case (real r) 
589 
then show ?thesis 

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

590 
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

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

592 

43920  593 
lemma ereal_add_mono: 
53873  594 
fixes a b c d :: ereal 
595 
assumes "a \<le> b" 

596 
and "c \<le> d" 

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

41973  598 
using assms 
599 
apply (cases a) 

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

41973  602 
done 
603 

43920  604 
lemma ereal_minus_le_minus[simp]: 
53873  605 
fixes a b :: ereal 
606 
shows " a \<le>  b \<longleftrightarrow> b \<le> a" 

43920  607 
by (cases rule: ereal2_cases[of a b]) auto 
41973  608 

43920  609 
lemma ereal_minus_less_minus[simp]: 
53873  610 
fixes a b :: ereal 
611 
shows " a <  b \<longleftrightarrow> b < a" 

43920  612 
by (cases rule: ereal2_cases[of a b]) auto 
41973  613 

43920  614 
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

615 
"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  616 
by (cases y) auto 
617 

43920  618 
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

619 
"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  620 
by (cases y) auto 
621 

43920  622 
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

623 
"x < real_of_ereal y \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> ereal x < y) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> x < 0)" 
41973  624 
by (cases y) auto 
625 

43920  626 
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

627 
"real_of_ereal y < x \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y < ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 < x)" 
41973  628 
by (cases y) auto 
629 

43920  630 
lemma real_of_ereal_pos: 
53873  631 
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

632 
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

633 

43920  634 
lemmas real_of_ereal_ord_simps = 
635 
ereal_le_real_iff real_le_ereal_iff ereal_less_real_iff real_less_ereal_iff 

41973  636 

43920  637 
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

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

639 

43920  640 
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

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

642 

43920  643 
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

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

645 

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

646 
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

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

648 
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

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

650 

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

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

653 

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

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

656 

43923  657 
lemma zero_less_real_of_ereal: 
53873  658 
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

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

661 

43920  662 
lemma ereal_0_le_uminus_iff[simp]: 
53873  663 
fixes a :: ereal 
664 
shows "0 \<le>  a \<longleftrightarrow> a \<le> 0" 

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

666 

43920  667 
lemma ereal_uminus_le_0_iff[simp]: 
53873  668 
fixes a :: ereal 
669 
shows " a \<le> 0 \<longleftrightarrow> 0 \<le> a" 

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

671 

43920  672 
lemma ereal_add_strict_mono: 
673 
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

674 
assumes "a \<le> b" 
53873  675 
and "0 \<le> a" 
676 
and "a \<noteq> \<infinity>" 

677 
and "c < d" 

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

678 
shows "a + c < b + d" 
53873  679 
using assms 
680 
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

681 

53873  682 
lemma ereal_less_add: 
683 
fixes a b c :: ereal 

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

43920  685 
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

686 

54416  687 
lemma ereal_add_nonneg_eq_0_iff: 
688 
fixes a b :: ereal 

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

690 
by (cases a b rule: ereal2_cases) auto 

691 

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

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

694 

43920  695 
lemma ereal_uminus_less_reorder: " a < b \<longleftrightarrow> b < (a::ereal)" 
696 
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

697 

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

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

699 
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

700 

43920  701 
lemma ereal_uminus_le_reorder: " a \<le> b \<longleftrightarrow> b \<le> (a::ereal)" 
702 
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

703 

43920  704 
lemmas ereal_uminus_reorder = 
705 
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

706 

43920  707 
lemma ereal_bot: 
53873  708 
fixes x :: ereal 
709 
assumes "\<And>B. x \<le> ereal B" 

710 
shows "x =  \<infinity>" 

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

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

714 
by auto 

47082  715 
next 
53873  716 
case PInf 
717 
with assms[of 0] show ?thesis 

718 
by auto 

47082  719 
next 
53873  720 
case MInf 
721 
then show ?thesis 

722 
by simp 

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

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

724 

43920  725 
lemma ereal_top: 
53873  726 
fixes x :: ereal 
727 
assumes "\<And>B. x \<ge> ereal B" 

728 
shows "x = \<infinity>" 

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

729 
proof (cases x) 
53873  730 
case (real r) 
731 
with assms[of "r + 1"] show ?thesis 

732 
by auto 

47082  733 
next 
53873  734 
case MInf 
735 
with assms[of 0] show ?thesis 

736 
by auto 

47082  737 
next 
53873  738 
case PInf 
739 
then show ?thesis 

740 
by simp 

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

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

742 

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

743 
lemma 
43920  744 
shows ereal_max[simp]: "ereal (max x y) = max (ereal x) (ereal y)" 
745 
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

746 
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

747 

43920  748 
lemma ereal_max_0: "max 0 (ereal r) = ereal (max 0 r)" 
749 
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

750 

41978  751 
lemma 
43920  752 
fixes f :: "nat \<Rightarrow> ereal" 
54416  753 
shows ereal_incseq_uminus[simp]: "incseq (\<lambda>x.  f x) \<longleftrightarrow> decseq f" 
754 
and ereal_decseq_uminus[simp]: "decseq (\<lambda>x.  f x) \<longleftrightarrow> incseq f" 

41978  755 
unfolding decseq_def incseq_def by auto 
756 

43920  757 
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

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

759 

56537  760 
lemma ereal_add_nonneg_nonneg[simp]: 
53873  761 
fixes a b :: ereal 
762 
shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b" 

41978  763 
using add_mono[of 0 a 0 b] by simp 
764 

64267  765 
lemma sum_ereal[simp]: "(\<Sum>x\<in>A. ereal (f x)) = ereal (\<Sum>x\<in>A. f x)" 
59000  766 
proof (cases "finite A") 
767 
case True 

768 
then show ?thesis by induct auto 

769 
next 

770 
case False 

771 
then show ?thesis by simp 

772 
qed 

773 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63680
diff
changeset

774 
lemma sum_list_ereal [simp]: "sum_list (map (\<lambda>x. ereal (f x)) xs) = ereal (sum_list (map f xs))" 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

775 
by (induction xs) simp_all 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63092
diff
changeset

776 

64267  777 
lemma sum_Pinfty: 
59000  778 
fixes f :: "'a \<Rightarrow> ereal" 
779 
shows "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> finite P \<and> (\<exists>i\<in>P. f i = \<infinity>)" 

780 
proof safe 

64267  781 
assume *: "sum f P = \<infinity>" 
59000  782 
show "finite P" 
783 
proof (rule ccontr) 

784 
assume "\<not> finite P" 

785 
with * show False 

786 
by auto 

787 
qed 

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

789 
proof (rule ccontr) 

790 
assume "\<not> ?thesis" 

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

792 
by auto 

64267  793 
with \<open>finite P\<close> have "sum f P \<noteq> \<infinity>" 
59000  794 
by induct auto 
795 
with * show False 

796 
by auto 

797 
qed 

798 
next 

799 
fix i 

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

64267  801 
then show "sum f P = \<infinity>" 
59000  802 
proof induct 
803 
case (insert x A) 

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

805 
qed simp 

806 
qed 

807 

64267  808 
lemma sum_Inf: 
59000  809 
fixes f :: "'a \<Rightarrow> ereal" 
64267  810 
shows "\<bar>sum f A\<bar> = \<infinity> \<longleftrightarrow> finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)" 
59000  811 
proof 
64267  812 
assume *: "\<bar>sum f A\<bar> = \<infinity>" 
59000  813 
have "finite A" 
814 
by (rule ccontr) (insert *, auto) 

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

816 
proof (rule ccontr) 

817 
assume "\<not> ?thesis" 

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

819 
by auto 

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

821 
with * show False 

822 
by auto 

823 
qed 

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

825 
by auto 

826 
next 

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

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

829 
by auto 

64267  830 
then show "\<bar>sum f A\<bar> = \<infinity>" 
59000  831 
proof induct 
832 
case (insert j A) 

833 
then show ?case 

64267  834 
by (cases rule: ereal3_cases[of "f i" "f j" "sum f A"]) auto 
59000  835 
qed simp 
836 
qed 

837 

64267  838 
lemma sum_real_of_ereal: 
59000  839 
fixes f :: "'i \<Rightarrow> ereal" 
840 
assumes "\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>" 

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

844 
proof 

845 
fix x 

846 
assume "x \<in> S" 

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

848 
by (cases "f x") auto 

849 
qed 

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

851 
then show ?thesis 

852 
by simp 

853 
qed 

854 

64267  855 
lemma sum_ereal_0: 
59000  856 
fixes f :: "'a \<Rightarrow> ereal" 
857 
assumes "finite A" 

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

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

860 
proof 

64267  861 
assume "sum f A = 0" with assms show "\<forall>i\<in>A. f i = 0" 
59000  862 
proof (induction A) 
863 
case (insert a A) 

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

64267  865 
by (subst ereal_add_nonneg_eq_0_iff[symmetric]) (simp_all add: sum_nonneg) 
59000  866 
with insert show ?case 
867 
by simp 

868 
qed simp 

869 
qed auto 

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

870 

41973  871 
subsubsection "Multiplication" 
872 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

901 

902 
instance 

903 
proof 

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

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

41973  912 
qed 
53873  913 

41973  914 
end 
915 

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

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

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

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

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

920 

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

923 

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

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

43920  927 
lemma real_of_ereal_le_1: 
53873  928 
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

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

931 

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

41976  934 

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

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

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

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

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

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

61120  951 
by (auto simp: one_ereal_def) 
41973  952 

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

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

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

43920  958 
unfolding one_ereal_def by auto 
41973  959 

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

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

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

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

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

977 

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

41973  980 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 

64267  1092 
lemma sum_ereal_right_distrib: 
59000  1093 
fixes f :: "'a \<Rightarrow> ereal" 
64267  1094 
shows "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> r * sum f A = (\<Sum>n\<in>A. r * f n)" 
1095 
by (induct A rule: infinite_finite_induct) (auto simp: ereal_right_distrib sum_nonneg) 

1096 

1097 
lemma sum_ereal_left_distrib: 

1098 
"(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> sum f A * r = (\<Sum>n\<in>A. f n * r :: ereal)" 

1099 
using sum_ereal_right_distrib[of A f r] by (simp add: mult_ac) 

1100 

1101 
lemma sum_distrib_right_ereal: 

1102 
"c \<ge> 0 \<Longrightarrow> sum f A * ereal c = (\<Sum>x\<in>A. f x * c :: ereal)" 

1103 
by(subst sum_comp_morphism[where h="\<lambda>x. x * ereal c", symmetric])(simp_all add: distrib_left_ereal_nn) 

61631
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 

64272  1183 
lemma prod_ereal_0: 
43920  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 

64272  1194 
lemma prod_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 

64272  1207 
lemma prod_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) 
64272  1216 
then have pos: "0 \<le> f i" "0 \<le> prod f I" 
1217 
by (auto intro!: prod_ereal_pos) 

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

53873  1219 
by auto 
64272  1220 
also have "\<dots> \<longleftrightarrow> (prod f I = \<infinity> \<or> f i = \<infinity>) \<and> f i \<noteq> 0 \<and> prod f I \<noteq> 0" 
1221 
using prod_ereal_pos[of I f] pos 

1222 
by (cases rule: ereal2_cases[of "f i" "prod 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)" 
64272  1224 
using insert by (auto simp: prod_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 

64272  1232 
lemma prod_ereal: "(\<Prod>i\<in>A. ereal (f i)) = ereal (prod f A)" 
53873
08594daabcd9
tuned proofs;
wenzelm 