160 val Root_crls = |
160 val Root_crls = |
161 Rule_Set.append_rules "Root_crls" Atools_erls [ |
161 Rule_Set.append_rules "Root_crls" Atools_erls [ |
162 \<^rule_thm>\<open>real_unari_minus\<close>, |
162 \<^rule_thm>\<open>real_unari_minus\<close>, |
163 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"), |
163 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"), |
164 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
164 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
165 \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"), |
165 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"), |
166 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
166 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
167 \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"), |
167 \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"), |
168 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
168 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"), |
169 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]; |
169 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]; |
170 |
170 |
171 val Root_erls = |
171 val Root_erls = |
172 Rule_Set.append_rules "Root_erls" Atools_erls [ |
172 Rule_Set.append_rules "Root_erls" Atools_erls [ |
173 \<^rule_thm>\<open>real_unari_minus\<close>, |
173 \<^rule_thm>\<open>real_unari_minus\<close>, |
174 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"), |
174 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"), |
175 \<^rule_eval>\<open>Rings.divide_class.divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
175 \<^rule_eval>\<open>Rings.divide_class.divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
176 \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"), |
176 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"), |
177 \<^rule_eval>\<open>Groups.plus_class.plus\<close> (**)(eval_binop "#add_"), |
177 \<^rule_eval>\<open>Groups.plus_class.plus\<close> (**)(Calc_Binop.numeric "#add_"), |
178 \<^rule_eval>\<open>Groups.minus_class.minus\<close> (**)(eval_binop "#sub_"), |
178 \<^rule_eval>\<open>Groups.minus_class.minus\<close> (**)(Calc_Binop.numeric "#sub_"), |
179 \<^rule_eval>\<open>Groups.times_class.times\<close> (**)(eval_binop "#mult_"), |
179 \<^rule_eval>\<open>Groups.times_class.times\<close> (**)(Calc_Binop.numeric "#mult_"), |
180 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]; |
180 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]; |
181 val Root_erls = |
181 val Root_erls = |
182 Rule_Set.append_erls_rules "Root_erls_erls" Root_erls [ |
182 Rule_Set.append_erls_rules "Root_erls_erls" Root_erls [ |
183 \<^rule_thm>\<open>not_false\<close>, |
183 \<^rule_thm>\<open>not_false\<close>, |
184 \<^rule_thm>\<open>not_true\<close>, |
184 \<^rule_thm>\<open>not_true\<close>, |
220 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==> l * n + m * n = (l + m) * n"*) |
220 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==> l * n + m * n = (l + m) * n"*) |
221 \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) = (l + m) * n + k"*) |
221 \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) = (l + m) * n + k"*) |
222 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*) |
222 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*) |
223 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*) |
223 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*) |
224 |
224 |
225 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
225 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
226 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
226 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"), |
227 \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")], |
227 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")], |
228 scr = Rule.Empty_Prog}); |
228 scr = Rule.Empty_Prog}); |
229 \<close> |
229 \<close> |
230 rule_set_knowledge make_rooteq = make_rooteq |
230 rule_set_knowledge make_rooteq = make_rooteq |
231 ML \<open> |
231 ML \<open> |
232 |
232 |
252 |
252 |
253 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*) |
253 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*) |
254 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*) |
254 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*) |
255 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*) |
255 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*) |
256 |
256 |
257 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
257 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
258 \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"), |
258 \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"), |
259 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
259 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"), |
260 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
260 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
261 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"), |
261 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"), |
262 \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"), |
262 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"), |
263 |
263 |
264 \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*) |
264 \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*) |
265 \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r \<up> n = r \<up> (n + 1)"*) |
265 \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r \<up> n = r \<up> (n + 1)"*) |
266 \<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*) |
266 \<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*) |
267 |
267 |
268 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |] ==>l * n + m * n = (l + m) * n"*) |
268 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |] ==>l * n + m * n = (l + m) * n"*) |
269 \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) = (l + m) * n + k"*) |
269 \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) = (l + m) * n + k"*) |
270 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*) |
270 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*) |
271 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*) |
271 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*) |
272 |
272 |
273 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
273 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
274 \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"), |
274 \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"), |
275 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
275 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"), |
276 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
276 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
277 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"), |
277 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"), |
278 \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")], |
278 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")], |
279 scr = Rule.Empty_Prog}); |
279 scr = Rule.Empty_Prog}); |
280 \<close> |
280 \<close> |
281 rule_set_knowledge expand_rootbinoms = expand_rootbinoms |
281 rule_set_knowledge expand_rootbinoms = expand_rootbinoms |
282 ML \<open> |
282 ML \<open> |
283 \<close> ML \<open> |
283 \<close> ML \<open> |