84 |
84 |
85 subsection{*Absolute Value Function for the Hyperreals*} |
85 subsection{*Absolute Value Function for the Hyperreals*} |
86 |
86 |
87 declare abs_mult [simp] |
87 declare abs_mult [simp] |
88 |
88 |
89 lemma hrabs_add_less: "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)" |
89 lemma hrabs_add_less: |
90 apply (unfold hrabs_def) |
90 "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)" |
91 apply (simp split add: split_if_asm) |
91 by (simp add: abs_if split: split_if_asm) |
92 done |
|
93 |
92 |
94 text{*used once in NSA*} |
93 text{*used once in NSA*} |
95 lemma hrabs_less_gt_zero: "abs x < r ==> (0::hypreal) < r" |
94 lemma hrabs_less_gt_zero: "abs x < r ==> (0::hypreal) < r" |
96 by (blast intro!: order_le_less_trans abs_ge_zero) |
95 by (blast intro!: order_le_less_trans abs_ge_zero) |
97 |
96 |
98 lemma hrabs_disj: "abs x = (x::hypreal) | abs x = -x" |
97 lemma hrabs_disj: "abs x = (x::hypreal) | abs x = -x" |
99 by (simp add: hrabs_def) |
98 by (simp add: abs_if) |
100 |
99 |
101 (* Needed in Geom.ML *) |
100 (* Needed in Geom.ML *) |
102 lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y" |
101 lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y" |
103 by (simp add: hrabs_def split add: split_if_asm) |
102 by (simp add: abs_if split add: split_if_asm) |
104 |
103 |
105 lemma hypreal_of_real_hrabs: |
104 lemma hypreal_of_real_hrabs: |
106 "abs (hypreal_of_real r) = hypreal_of_real (abs r)" |
105 "abs (hypreal_of_real r) = hypreal_of_real (abs r)" |
107 apply (unfold hypreal_of_real_def) |
106 apply (unfold hypreal_of_real_def) |
108 apply (auto simp add: hypreal_hrabs) |
107 apply (auto simp add: hypreal_hrabs) |