equal
deleted
inserted
replaced
138 |
138 |
139 subsection{*Various Other Theorems*} |
139 subsection{*Various Other Theorems*} |
140 |
140 |
141 text{*Used several times in Hyperreal/Transcendental.ML*} |
141 text{*Used several times in Hyperreal/Transcendental.ML*} |
142 lemma real_sum_squares_cancel_a: "x * x = -(y * y) ==> x = (0::real) & y=0" |
142 lemma real_sum_squares_cancel_a: "x * x = -(y * y) ==> x = (0::real) & y=0" |
143 by (auto intro: real_sum_squares_cancel) |
143 apply (auto dest: real_sum_squares_cancel simp add: real_add_eq_0_iff [symmetric]) |
|
144 apply (auto dest: real_sum_squares_cancel simp add: add_commute) |
|
145 done |
144 |
146 |
145 lemma real_squared_diff_one_factored: "x*x - (1::real) = (x + 1)*(x - 1)" |
147 lemma real_squared_diff_one_factored: "x*x - (1::real) = (x + 1)*(x - 1)" |
146 by (auto simp add: left_distrib right_distrib real_diff_def) |
148 by (auto simp add: left_distrib right_distrib real_diff_def) |
147 |
149 |
148 lemma real_mult_is_one [simp]: "(x*x = (1::real)) = (x = 1 | x = - 1)" |
150 lemma real_mult_is_one [simp]: "(x*x = (1::real)) = (x = 1 | x = - 1)" |