equal
deleted
inserted
replaced
179 val diff_simps = [@{thm diff_minus}, @{thm minus_add_distrib}, @{thm minus_minus}]; |
179 val diff_simps = [@{thm diff_minus}, @{thm minus_add_distrib}, @{thm minus_minus}]; |
180 |
180 |
181 (*To let us treat division as multiplication*) |
181 (*To let us treat division as multiplication*) |
182 val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}]; |
182 val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}]; |
183 |
183 |
184 (*push the unary minus down: - x * y = x * - y *) |
184 (*push the unary minus down*) |
185 val minus_mult_eq_1_to_2 = |
185 val minus_mult_eq_1_to_2 = @{lemma "- (a::'a::ring) * b = a * - b" by simp}; |
186 [@{thm mult_minus_left}, @{thm minus_mult_right}] MRS trans |> Drule.standard; |
|
187 |
186 |
188 (*to extract again any uncancelled minuses*) |
187 (*to extract again any uncancelled minuses*) |
189 val minus_from_mult_simps = |
188 val minus_from_mult_simps = |
190 [@{thm minus_minus}, @{thm mult_minus_left}, @{thm mult_minus_right}]; |
189 [@{thm minus_minus}, @{thm mult_minus_left}, @{thm mult_minus_right}]; |
191 |
190 |