equal
deleted
inserted
replaced
101 done |
101 done |
102 |
102 |
103 lemma hypreal_sqrt_ge_zero: "0 \<le> x ==> 0 \<le> ( *f* sqrt)(x)" |
103 lemma hypreal_sqrt_ge_zero: "0 \<le> x ==> 0 \<le> ( *f* sqrt)(x)" |
104 by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less) |
104 by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less) |
105 |
105 |
106 lemma hypreal_sqrt_hrabs [simp]: "!!x. ( *f* sqrt)(x\<^sup>2) = abs(x)" |
106 lemma hypreal_sqrt_hrabs [simp]: "!!x. ( *f* sqrt)(x\<^sup>2) = \<bar>x\<bar>" |
107 by (transfer, simp) |
107 by (transfer, simp) |
108 |
108 |
109 lemma hypreal_sqrt_hrabs2 [simp]: "!!x. ( *f* sqrt)(x*x) = abs(x)" |
109 lemma hypreal_sqrt_hrabs2 [simp]: "!!x. ( *f* sqrt)(x*x) = \<bar>x\<bar>" |
110 by (transfer, simp) |
110 by (transfer, simp) |
111 |
111 |
112 lemma hypreal_sqrt_hyperpow_hrabs [simp]: |
112 lemma hypreal_sqrt_hyperpow_hrabs [simp]: |
113 "!!x. ( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)" |
113 "!!x. ( *f* sqrt)(x pow (hypnat_of_nat 2)) = \<bar>x\<bar>" |
114 by (transfer, simp) |
114 by (transfer, simp) |
115 |
115 |
116 lemma star_sqrt_HFinite: "\<lbrakk>x \<in> HFinite; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> HFinite" |
116 lemma star_sqrt_HFinite: "\<lbrakk>x \<in> HFinite; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> HFinite" |
117 apply (rule HFinite_square_iff [THEN iffD1]) |
117 apply (rule HFinite_square_iff [THEN iffD1]) |
118 apply (simp only: hypreal_sqrt_mult_distrib2 [symmetric], simp) |
118 apply (simp only: hypreal_sqrt_mult_distrib2 [symmetric], simp) |