equal
deleted
inserted
replaced
49 |
49 |
50 lemma real_divide_minus1 [simp]: "x/-1 = -(x::real)" |
50 lemma real_divide_minus1 [simp]: "x/-1 = -(x::real)" |
51 by simp |
51 by simp |
52 |
52 |
53 lemma real_minus1_divide [simp]: "-1/(x::real) = - (1/x)" |
53 lemma real_minus1_divide [simp]: "-1/(x::real) = - (1/x)" |
54 by (simp add: real_divide_def real_minus_inverse) |
54 by (simp add: real_divide_def inverse_minus_eq) |
55 |
55 |
56 lemma real_lbound_gt_zero: |
56 lemma real_lbound_gt_zero: |
57 "[| (0::real) < d1; 0 < d2 |] ==> \<exists>e. 0 < e & e < d1 & e < d2" |
57 "[| (0::real) < d1; 0 < d2 |] ==> \<exists>e. 0 < e & e < d1 & e < d2" |
58 apply (rule_tac x = " (min d1 d2) /2" in exI) |
58 apply (rule_tac x = " (min d1 d2) /2" in exI) |
59 apply (simp add: min_def) |
59 apply (simp add: min_def) |
114 |
114 |
115 lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)" |
115 lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)" |
116 by (auto intro: abs_eqI1 simp add: real_of_nat_ge_zero) |
116 by (auto intro: abs_eqI1 simp add: real_of_nat_ge_zero) |
117 |
117 |
118 lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x" |
118 lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x" |
119 apply (rule real_leD) |
119 apply (simp add: linorder_not_less) |
120 apply (auto intro: abs_ge_self [THEN order_trans]) |
120 apply (auto intro: abs_ge_self [THEN order_trans]) |
121 done |
121 done |
122 |
122 |
123 text{*Used only in Hyperreal/Lim.ML*} |
123 text{*Used only in Hyperreal/Lim.ML*} |
124 lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)" |
124 lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)" |
125 apply (simp add: real_add_assoc) |
125 apply (simp add: real_add_assoc) |
126 apply (rule_tac x1 = y in real_add_left_commute [THEN ssubst]) |
126 apply (rule_tac a1 = y in add_left_commute [THEN ssubst]) |
127 apply (rule real_add_assoc [THEN subst]) |
127 apply (rule real_add_assoc [THEN subst]) |
128 apply (rule abs_triangle_ineq) |
128 apply (rule abs_triangle_ineq) |
129 done |
129 done |
130 |
130 |
131 |
131 |