358 |
358 |
359 section \<open>rulesets\<close> |
359 section \<open>rulesets\<close> |
360 ML \<open> |
360 ML \<open> |
361 val testerls = |
361 val testerls = |
362 Rule_Def.Repeat {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI), |
362 Rule_Def.Repeat {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI), |
363 erls = Rule_Set.empty, srls = Rule_Set.Empty, |
363 erls = Rule_Set.empty, srls = Rule_Set.Empty, |
364 calc = [], errpatts = [], |
364 calc = [], errpatts = [], |
365 rules = [\<^rule_thm>\<open>refl\<close>, |
365 rules = [ |
366 \<^rule_thm>\<open>order_refl\<close>, |
366 \<^rule_thm>\<open>refl\<close>, |
367 \<^rule_thm>\<open>radd_left_cancel_le\<close>, |
367 \<^rule_thm>\<open>order_refl\<close>, |
368 \<^rule_thm>\<open>not_true\<close>, |
368 \<^rule_thm>\<open>radd_left_cancel_le\<close>, |
369 \<^rule_thm>\<open>not_false\<close>, |
369 \<^rule_thm>\<open>not_true\<close>, |
370 \<^rule_thm>\<open>and_true\<close>, |
370 \<^rule_thm>\<open>not_false\<close>, |
371 \<^rule_thm>\<open>and_false\<close>, |
371 \<^rule_thm>\<open>and_true\<close>, |
372 \<^rule_thm>\<open>or_true\<close>, |
372 \<^rule_thm>\<open>and_false\<close>, |
373 \<^rule_thm>\<open>or_false\<close>, |
373 \<^rule_thm>\<open>or_true\<close>, |
374 \<^rule_thm>\<open>and_commute\<close>, |
374 \<^rule_thm>\<open>or_false\<close>, |
375 \<^rule_thm>\<open>or_commute\<close>, |
375 \<^rule_thm>\<open>and_commute\<close>, |
376 |
376 \<^rule_thm>\<open>or_commute\<close>, |
377 \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"), |
377 |
378 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""), |
378 \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"), |
379 |
379 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""), |
380 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
380 |
381 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
381 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
382 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"), |
382 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
383 |
383 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"), |
384 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
384 |
385 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"), |
385 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
386 |
386 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"), |
387 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_")], |
387 |
388 scr = Rule.Empty_Prog |
388 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_")], |
389 }; |
389 scr = Rule.Empty_Prog}; |
390 \<close> |
390 \<close> |
391 ML \<open> |
391 ML \<open> |
392 (*.for evaluation of conditions in rewrite rules.*) |
392 (*.for evaluation of conditions in rewrite rules.*) |
393 (*FIXXXXXXME 10.8.02: handle like _simplify*) |
393 (*FIXXXXXXME 10.8.02: handle like _simplify*) |
394 val tval_rls = |
394 val tval_rls = |
395 Rule_Def.Repeat{id = "tval_rls", preconds = [], |
395 Rule_Def.Repeat{id = "tval_rls", preconds = [], |
396 rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}), |
396 rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}), |
397 erls=testerls,srls = Rule_Set.empty, |
397 erls=testerls,srls = Rule_Set.empty, |
398 calc=[], errpatts = [], |
398 calc=[], errpatts = [], |
399 rules = [\<^rule_thm>\<open>refl\<close>, |
399 rules = [ |
400 \<^rule_thm>\<open>order_refl\<close>, |
400 \<^rule_thm>\<open>refl\<close>, |
401 \<^rule_thm>\<open>radd_left_cancel_le\<close>, |
401 \<^rule_thm>\<open>order_refl\<close>, |
402 \<^rule_thm>\<open>not_true\<close>, |
402 \<^rule_thm>\<open>radd_left_cancel_le\<close>, |
403 \<^rule_thm>\<open>not_false\<close>, |
403 \<^rule_thm>\<open>not_true\<close>, |
404 \<^rule_thm>\<open>and_true\<close>, |
404 \<^rule_thm>\<open>not_false\<close>, |
405 \<^rule_thm>\<open>and_false\<close>, |
405 \<^rule_thm>\<open>and_true\<close>, |
406 \<^rule_thm>\<open>or_true\<close>, |
406 \<^rule_thm>\<open>and_false\<close>, |
407 \<^rule_thm>\<open>or_false\<close>, |
407 \<^rule_thm>\<open>or_true\<close>, |
408 \<^rule_thm>\<open>and_commute\<close>, |
408 \<^rule_thm>\<open>or_false\<close>, |
409 \<^rule_thm>\<open>or_commute\<close>, |
409 \<^rule_thm>\<open>and_commute\<close>, |
410 |
410 \<^rule_thm>\<open>or_commute\<close>, |
411 \<^rule_thm>\<open>real_diff_minus\<close>, |
411 |
412 |
412 \<^rule_thm>\<open>real_diff_minus\<close>, |
413 \<^rule_thm>\<open>root_ge0\<close>, |
413 |
414 \<^rule_thm>\<open>root_add_ge0\<close>, |
414 \<^rule_thm>\<open>root_ge0\<close>, |
415 \<^rule_thm>\<open>root_ge0_1\<close>, |
415 \<^rule_thm>\<open>root_add_ge0\<close>, |
416 \<^rule_thm>\<open>root_ge0_2\<close>, |
416 \<^rule_thm>\<open>root_ge0_1\<close>, |
417 |
417 \<^rule_thm>\<open>root_ge0_2\<close>, |
418 \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"), |
418 |
419 \<^rule_eval>\<open>contains_root\<close> (eval_contains_root "#eval_contains_root"), |
419 \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"), |
420 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""), |
420 \<^rule_eval>\<open>contains_root\<close> (eval_contains_root "#eval_contains_root"), |
421 \<^rule_eval>\<open>contains_root\<close> (eval_contains_root"#contains_root_"), |
421 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""), |
422 |
422 \<^rule_eval>\<open>contains_root\<close> (eval_contains_root"#contains_root_"), |
423 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
423 |
424 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
424 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
425 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"), |
425 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
426 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"), |
426 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"), |
427 |
427 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"), |
428 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
428 |
429 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"), |
429 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
430 |
430 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"), |
431 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_")], |
431 |
432 scr = Rule.Empty_Prog |
432 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_")], |
433 }; |
433 scr = Rule.Empty_Prog}; |
434 \<close> |
434 \<close> |
435 rule_set_knowledge testerls = \<open>prep_rls' testerls\<close> |
435 rule_set_knowledge testerls = \<open>prep_rls' testerls\<close> |
436 |
436 |
437 ML \<open> |
437 ML \<open> |
438 (*make () dissappear*) |
438 (*make () dissappear*) |
439 val rearrange_assoc = |
439 val rearrange_assoc = |
440 Rule_Def.Repeat{id = "rearrange_assoc", preconds = [], |
440 Rule_Def.Repeat{ |
441 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), |
441 id = "rearrange_assoc", preconds = [], |
442 erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [], |
442 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), |
443 rules = [\<^rule_thm_sym>\<open>add.assoc\<close>, \<^rule_thm_sym>\<open>rmult_assoc\<close>], |
443 erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [], |
444 scr = Rule.Empty_Prog |
444 rules = [ |
445 }; |
445 \<^rule_thm_sym>\<open>add.assoc\<close>, |
|
446 \<^rule_thm_sym>\<open>rmult_assoc\<close>], |
|
447 scr = Rule.Empty_Prog}; |
446 |
448 |
447 val ac_plus_times = |
449 val ac_plus_times = |
448 Rule_Def.Repeat{id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order), |
450 Rule_Def.Repeat{ |
449 erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [], |
451 id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order), |
450 rules = |
452 erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [], |
451 [\<^rule_thm>\<open>radd_commute\<close>, |
453 rules = [ |
452 \<^rule_thm>\<open>radd_left_commute\<close>, |
454 \<^rule_thm>\<open>radd_commute\<close>, |
453 \<^rule_thm>\<open>add.assoc\<close>, |
455 \<^rule_thm>\<open>radd_left_commute\<close>, |
454 \<^rule_thm>\<open>rmult_commute\<close>, |
456 \<^rule_thm>\<open>add.assoc\<close>, |
455 \<^rule_thm>\<open>rmult_left_commute\<close>, |
457 \<^rule_thm>\<open>rmult_commute\<close>, |
456 \<^rule_thm>\<open>rmult_assoc\<close>], |
458 \<^rule_thm>\<open>rmult_left_commute\<close>, |
457 scr = Rule.Empty_Prog |
459 \<^rule_thm>\<open>rmult_assoc\<close>], |
458 }; |
460 scr = Rule.Empty_Prog}; |
459 |
461 |
460 (*todo: replace by Rewrite("rnorm_equation_add", @{thm rnorm_equation_add)*) |
462 (*todo: replace by Rewrite("rnorm_equation_add", @{thm rnorm_equation_add)*) |
461 val norm_equation = |
463 val norm_equation = |
462 Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), |
464 Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), |
463 erls = tval_rls, srls = Rule_Set.empty, calc = [], errpatts = [], |
465 erls = tval_rls, srls = Rule_Set.empty, calc = [], errpatts = [], |
464 rules = [\<^rule_thm>\<open>rnorm_equation_add\<close> |
466 rules = [ |
465 ], |
467 \<^rule_thm>\<open>rnorm_equation_add\<close>], |
466 scr = Rule.Empty_Prog |
468 scr = Rule.Empty_Prog}; |
467 }; |
|
468 \<close> |
469 \<close> |
469 ML \<open> |
470 ML \<open> |
470 (* expects * distributed over + *) |
471 (* expects * distributed over + *) |
471 val Test_simplify = |
472 val Test_simplify = |
472 Rule_Def.Repeat{id = "Test_simplify", preconds = [], |
473 Rule_Def.Repeat{ |
473 rew_ord = ("sqrt_right", sqrt_right false @{theory "Pure"}), |
474 id = "Test_simplify", preconds = [], |
474 erls = tval_rls, srls = Rule_Set.empty, |
475 rew_ord = ("sqrt_right", sqrt_right false @{theory "Pure"}), |
475 calc=[(*since 040209 filled by prep_rls'*)], errpatts = [], |
476 erls = tval_rls, srls = Rule_Set.empty, |
476 rules = [ |
477 calc=[(*since 040209 filled by prep_rls'*)], errpatts = [], |
477 \<^rule_thm>\<open>real_diff_minus\<close>, |
478 rules = [ |
478 \<^rule_thm>\<open>radd_mult_distrib2\<close>, |
479 \<^rule_thm>\<open>real_diff_minus\<close>, |
479 \<^rule_thm>\<open>rdistr_right_assoc\<close>, |
480 \<^rule_thm>\<open>radd_mult_distrib2\<close>, |
480 \<^rule_thm>\<open>rdistr_right_assoc_p\<close>, |
481 \<^rule_thm>\<open>rdistr_right_assoc\<close>, |
481 \<^rule_thm>\<open>rdistr_div_right\<close>, |
482 \<^rule_thm>\<open>rdistr_right_assoc_p\<close>, |
482 \<^rule_thm>\<open>rbinom_power_2\<close>, |
483 \<^rule_thm>\<open>rdistr_div_right\<close>, |
483 |
484 \<^rule_thm>\<open>rbinom_power_2\<close>, |
484 \<^rule_thm>\<open>radd_commute\<close>, |
485 |
485 \<^rule_thm>\<open>radd_left_commute\<close>, |
486 \<^rule_thm>\<open>radd_commute\<close>, |
486 \<^rule_thm>\<open>add.assoc\<close>, |
487 \<^rule_thm>\<open>radd_left_commute\<close>, |
487 \<^rule_thm>\<open>rmult_commute\<close>, |
488 \<^rule_thm>\<open>add.assoc\<close>, |
488 \<^rule_thm>\<open>rmult_left_commute\<close>, |
489 \<^rule_thm>\<open>rmult_commute\<close>, |
489 \<^rule_thm>\<open>rmult_assoc\<close>, |
490 \<^rule_thm>\<open>rmult_left_commute\<close>, |
490 |
491 \<^rule_thm>\<open>rmult_assoc\<close>, |
491 \<^rule_thm>\<open>radd_real_const_eq\<close>, |
492 |
492 \<^rule_thm>\<open>radd_real_const\<close>, |
493 \<^rule_thm>\<open>radd_real_const_eq\<close>, |
493 (* these 2 rules are invers to distr_div_right wrt. termination. |
494 \<^rule_thm>\<open>radd_real_const\<close>, |
494 thus they MUST be done IMMEDIATELY before calc *) |
495 (* these 2 rules are invers to distr_div_right wrt. termination. |
495 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
496 thus they MUST be done IMMEDIATELY before calc *) |
496 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
497 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
497 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
498 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
498 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"), |
499 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"), |
499 |
500 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"), |
500 \<^rule_thm>\<open>rcollect_right\<close>, |
501 |
501 \<^rule_thm>\<open>rcollect_one_left\<close>, |
502 \<^rule_thm>\<open>rcollect_right\<close>, |
502 \<^rule_thm>\<open>rcollect_one_left_assoc\<close>, |
503 \<^rule_thm>\<open>rcollect_one_left\<close>, |
503 \<^rule_thm>\<open>rcollect_one_left_assoc_p\<close>, |
504 \<^rule_thm>\<open>rcollect_one_left_assoc\<close>, |
504 |
505 \<^rule_thm>\<open>rcollect_one_left_assoc_p\<close>, |
505 \<^rule_thm>\<open>rshift_nominator\<close>, |
506 |
506 \<^rule_thm>\<open>rcancel_den\<close>, |
507 \<^rule_thm>\<open>rshift_nominator\<close>, |
507 \<^rule_thm>\<open>rroot_square_inv\<close>, |
508 \<^rule_thm>\<open>rcancel_den\<close>, |
508 \<^rule_thm>\<open>rroot_times_root\<close>, |
509 \<^rule_thm>\<open>rroot_square_inv\<close>, |
509 \<^rule_thm>\<open>rroot_times_root_assoc_p\<close>, |
510 \<^rule_thm>\<open>rroot_times_root\<close>, |
510 \<^rule_thm>\<open>rsqare\<close>, |
511 \<^rule_thm>\<open>rroot_times_root_assoc_p\<close>, |
511 \<^rule_thm>\<open>power_1\<close>, |
512 \<^rule_thm>\<open>rsqare\<close>, |
512 \<^rule_thm>\<open>rtwo_of_the_same\<close>, |
513 \<^rule_thm>\<open>power_1\<close>, |
513 \<^rule_thm>\<open>rtwo_of_the_same_assoc_p\<close>, |
514 \<^rule_thm>\<open>rtwo_of_the_same\<close>, |
514 |
515 \<^rule_thm>\<open>rtwo_of_the_same_assoc_p\<close>, |
515 \<^rule_thm>\<open>rmult_1\<close>, |
516 |
516 \<^rule_thm>\<open>rmult_1_right\<close>, |
517 \<^rule_thm>\<open>rmult_1\<close>, |
517 \<^rule_thm>\<open>rmult_0\<close>, |
518 \<^rule_thm>\<open>rmult_1_right\<close>, |
518 \<^rule_thm>\<open>rmult_0_right\<close>, |
519 \<^rule_thm>\<open>rmult_0\<close>, |
519 \<^rule_thm>\<open>radd_0\<close>, |
520 \<^rule_thm>\<open>rmult_0_right\<close>, |
520 \<^rule_thm>\<open>radd_0_right\<close> |
521 \<^rule_thm>\<open>radd_0\<close>, |
521 ], |
522 \<^rule_thm>\<open>radd_0_right\<close>], |
522 scr = Rule.Empty_Prog |
523 scr = Rule.Empty_Prog}; |
523 (*since 040209 filled by prep_rls': STest_simplify*) |
|
524 }; |
|
525 \<close> |
524 \<close> |
526 ML \<open> |
525 ML \<open> |
527 (*isolate the root in a root-equation*) |
526 (*isolate the root in a root-equation*) |
528 val isolate_root = |
527 val isolate_root = |
529 Rule_Def.Repeat{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), |
528 Rule_Def.Repeat{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), |
530 erls=tval_rls,srls = Rule_Set.empty, calc=[], errpatts = [], |
529 erls=tval_rls,srls = Rule_Set.empty, calc=[], errpatts = [], |
531 rules = [\<^rule_thm>\<open>rroot_to_lhs\<close>, |
530 rules = [ |
532 \<^rule_thm>\<open>rroot_to_lhs_mult\<close>, |
531 \<^rule_thm>\<open>rroot_to_lhs\<close>, |
533 \<^rule_thm>\<open>rroot_to_lhs_add_mult\<close>, |
532 \<^rule_thm>\<open>rroot_to_lhs_mult\<close>, |
534 \<^rule_thm>\<open>risolate_root_add\<close>, |
533 \<^rule_thm>\<open>rroot_to_lhs_add_mult\<close>, |
535 \<^rule_thm>\<open>risolate_root_mult\<close>, |
534 \<^rule_thm>\<open>risolate_root_add\<close>, |
536 \<^rule_thm>\<open>risolate_root_div\<close> ], |
535 \<^rule_thm>\<open>risolate_root_mult\<close>, |
537 scr = Rule.Prog ((Thm.term_of o the o (TermC.parse \<^theory>)) |
536 \<^rule_thm>\<open>risolate_root_div\<close>], |
538 "empty_script") |
537 scr = Rule.Empty_Prog}; |
539 }; |
|
540 |
538 |
541 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*) |
539 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*) |
542 val isolate_bdv = |
540 val isolate_bdv = |
543 Rule_Def.Repeat{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), |
541 Rule_Def.Repeat{ |
544 erls=tval_rls,srls = Rule_Set.empty, calc= [], errpatts = [], |
542 id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), |
545 rules = |
543 erls=tval_rls,srls = Rule_Set.empty, calc= [], errpatts = [], |
546 [\<^rule_thm>\<open>risolate_bdv_add\<close>, |
544 rules = [ |
547 \<^rule_thm>\<open>risolate_bdv_mult_add\<close>, |
545 \<^rule_thm>\<open>risolate_bdv_add\<close>, |
548 \<^rule_thm>\<open>risolate_bdv_mult\<close>, |
546 \<^rule_thm>\<open>risolate_bdv_mult_add\<close>, |
549 \<^rule_thm>\<open>mult_square\<close>, |
547 \<^rule_thm>\<open>risolate_bdv_mult\<close>, |
550 \<^rule_thm>\<open>constant_square\<close>, |
548 \<^rule_thm>\<open>mult_square\<close>, |
551 \<^rule_thm>\<open>constant_mult_square\<close> |
549 \<^rule_thm>\<open>constant_square\<close>, |
552 ], |
550 \<^rule_thm>\<open>constant_mult_square\<close>], |
553 scr = Rule.Prog ((Thm.term_of o the o (TermC.parse \<^theory>)) |
551 scr = Rule.Empty_Prog}; |
554 "empty_script") |
|
555 }; |
|
556 \<close> |
552 \<close> |
557 ML \<open>val prep_rls' = Auto_Prog.prep_rls @{theory};\<close> |
553 ML \<open>val prep_rls' = Auto_Prog.prep_rls @{theory};\<close> |
558 rule_set_knowledge |
554 rule_set_knowledge |
559 Test_simplify = \<open>prep_rls' Test_simplify\<close> and |
555 Test_simplify = \<open>prep_rls' Test_simplify\<close> and |
560 tval_rls = \<open>prep_rls' tval_rls\<close> and |
556 tval_rls = \<open>prep_rls' tval_rls\<close> and |
599 ("ord_make_polytest", ord_make_polytest false \<^theory>) |
595 ("ord_make_polytest", ord_make_polytest false \<^theory>) |
600 ]); |
596 ]); |
601 |
597 |
602 val make_polytest = |
598 val make_polytest = |
603 Rule_Def.Repeat{id = "make_polytest", preconds = []:term list, |
599 Rule_Def.Repeat{id = "make_polytest", preconds = []:term list, |
604 rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}), |
600 rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}), |
605 erls = testerls, srls = Rule_Set.Empty, |
601 erls = testerls, srls = Rule_Set.Empty, |
606 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")), |
602 calc = [ |
607 ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")), |
603 ("PLUS" , (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")), |
608 ("POWER", (\<^const_name>\<open>powr\<close>, (**)eval_binop "#power_")) |
604 ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")), |
609 ], errpatts = [], |
605 ("POWER", (\<^const_name>\<open>powr\<close>, (**)eval_binop "#power_"))], |
610 rules = [\<^rule_thm>\<open>real_diff_minus\<close>, |
606 errpatts = [], |
611 (*"a - b = a + (-1) * b"*) |
607 rules = [ |
612 \<^rule_thm>\<open>distrib_right\<close>, |
608 \<^rule_thm>\<open>real_diff_minus\<close>, (*"a - b = a + (-1) * b"*) |
613 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
609 \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
614 \<^rule_thm>\<open>distrib_left\<close>, |
610 \<^rule_thm>\<open>distrib_left\<close>, (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) |
615 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) |
611 \<^rule_thm>\<open>left_diff_distrib\<close>, (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*) |
616 \<^rule_thm>\<open>left_diff_distrib\<close>, |
612 \<^rule_thm>\<open>right_diff_distrib\<close>, (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*) |
617 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*) |
613 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*) |
618 \<^rule_thm>\<open>right_diff_distrib\<close>, |
614 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*) |
619 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*) |
615 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*) |
620 \<^rule_thm>\<open>mult_1_left\<close>, |
616 (*AC-rewriting*) |
621 (*"1 * z = z"*) |
617 \<^rule_thm>\<open>mult.commute\<close>, (* z * w = w * z *) |
622 \<^rule_thm>\<open>mult_zero_left\<close>, |
618 \<^rule_thm>\<open>real_mult_left_commute\<close>, (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*) |
623 (*"0 * z = 0"*) |
619 \<^rule_thm>\<open>mult.assoc\<close>, (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*) |
624 \<^rule_thm>\<open>add_0_left\<close>, |
620 \<^rule_thm>\<open>add.commute\<close>, (*z + w = w + z*) |
625 (*"0 + z = z"*) |
621 \<^rule_thm>\<open>add.left_commute\<close>, (*x + (y + z) = y + (x + z)*) |
626 |
622 \<^rule_thm>\<open>add.assoc\<close>, (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*) |
627 (*AC-rewriting*) |
623 |
628 \<^rule_thm>\<open>mult.commute\<close>, |
624 \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*) |
629 (* z * w = w * z *) |
625 \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r \<up> n = r \<up> (n + 1)"*) |
630 \<^rule_thm>\<open>real_mult_left_commute\<close>, |
626 \<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*) |
631 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*) |
627 \<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*) |
632 \<^rule_thm>\<open>mult.assoc\<close>, |
628 |
633 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*) |
629 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*) |
634 \<^rule_thm>\<open>add.commute\<close>, |
630 \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*) |
635 (*z + w = w + z*) |
631 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_const ==> n + m * n = (1 + m) * n"*) |
636 \<^rule_thm>\<open>add.left_commute\<close>, |
632 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) |
637 (*x + (y + z) = y + (x + z)*) |
633 |
638 \<^rule_thm>\<open>add.assoc\<close>, |
634 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
639 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*) |
635 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
640 |
636 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")], |
641 \<^rule_thm_sym>\<open>realpow_twoI\<close>, |
637 scr = Rule.Empty_Prog}; |
642 (*"r1 * r1 = r1 \<up> 2"*) |
|
643 \<^rule_thm>\<open>realpow_plus_1\<close>, |
|
644 (*"r * r \<up> n = r \<up> (n + 1)"*) |
|
645 \<^rule_thm_sym>\<open>real_mult_2\<close>, |
|
646 (*"z1 + z1 = 2 * z1"*) |
|
647 \<^rule_thm>\<open>real_mult_2_assoc\<close>, |
|
648 (*"z1 + (z1 + k) = 2 * z1 + k"*) |
|
649 |
|
650 \<^rule_thm>\<open>real_num_collect\<close>, |
|
651 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*) |
|
652 \<^rule_thm>\<open>real_num_collect_assoc\<close>, |
|
653 (*"[| l is_const; m is_const |] ==> |
|
654 l * n + (m * n + k) = (l + m) * n + k"*) |
|
655 \<^rule_thm>\<open>real_one_collect\<close>, |
|
656 (*"m is_const ==> n + m * n = (1 + m) * n"*) |
|
657 \<^rule_thm>\<open>real_one_collect_assoc\<close>, |
|
658 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) |
|
659 |
|
660 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
|
661 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
|
662 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_") |
|
663 ], |
|
664 scr = Rule.Empty_Prog(*Rule.Prog ((Thm.term_of o the o (parse thy)) |
|
665 scr_make_polytest)*) |
|
666 }; |
|
667 |
638 |
668 val expand_binomtest = |
639 val expand_binomtest = |
669 Rule_Def.Repeat{id = "expand_binomtest", preconds = [], |
640 Rule_Def.Repeat{id = "expand_binomtest", preconds = [], |
670 rew_ord = ("termlessI",termlessI), |
641 rew_ord = ("termlessI",termlessI), erls = testerls, srls = Rule_Set.Empty, |
671 erls = testerls, srls = Rule_Set.Empty, |
642 calc = [ |
672 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")), |
643 ("PLUS" , (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")), |
673 ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")), |
644 ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")), |
674 ("POWER", (\<^const_name>\<open>powr\<close>, (**)eval_binop "#power_")) |
645 ("POWER", (\<^const_name>\<open>powr\<close>, (**)eval_binop "#power_")) |
675 ], errpatts = [], |
646 ], |
676 rules = |
647 errpatts = [], |
677 [\<^rule_thm>\<open>real_plus_binom_pow2\<close>, |
648 rules = [ |
678 (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*) |
649 \<^rule_thm>\<open>real_plus_binom_pow2\<close>, (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*) |
679 \<^rule_thm>\<open>real_plus_binom_times\<close>, |
650 \<^rule_thm>\<open>real_plus_binom_times\<close>, (*"(a + b)*(a + b) = ...*) |
680 (*"(a + b)*(a + b) = ...*) |
651 \<^rule_thm>\<open>real_minus_binom_pow2\<close>, (*"(a - b) \<up> 2 = a \<up> 2 - 2 * a * b + b \<up> 2"*) |
681 \<^rule_thm>\<open>real_minus_binom_pow2\<close>, |
652 \<^rule_thm>\<open>real_minus_binom_times\<close>, (*"(a - b)*(a - b) = ...*) |
682 (*"(a - b) \<up> 2 = a \<up> 2 - 2 * a * b + b \<up> 2"*) |
653 \<^rule_thm>\<open>real_plus_minus_binom1\<close>, (*"(a + b) * (a - b) = a \<up> 2 - b \<up> 2"*) |
683 \<^rule_thm>\<open>real_minus_binom_times\<close>, |
654 \<^rule_thm>\<open>real_plus_minus_binom2\<close>, (*"(a - b) * (a + b) = a \<up> 2 - b \<up> 2"*) |
684 (*"(a - b)*(a - b) = ...*) |
655 (*RL 020915*) |
685 \<^rule_thm>\<open>real_plus_minus_binom1\<close>, |
656 \<^rule_thm>\<open>real_pp_binom_times\<close>, (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*) |
686 (*"(a + b) * (a - b) = a \<up> 2 - b \<up> 2"*) |
657 \<^rule_thm>\<open>real_pm_binom_times\<close>, (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*) |
687 \<^rule_thm>\<open>real_plus_minus_binom2\<close>, |
658 \<^rule_thm>\<open>real_mp_binom_times\<close>, (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*) |
688 (*"(a - b) * (a + b) = a \<up> 2 - b \<up> 2"*) |
659 \<^rule_thm>\<open>real_mm_binom_times\<close>, (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*) |
689 (*RL 020915*) |
660 \<^rule_thm>\<open>realpow_multI\<close>, (*(a*b) \<up> n = a \<up> n * b \<up> n*) |
690 \<^rule_thm>\<open>real_pp_binom_times\<close>, |
661 \<^rule_thm>\<open>real_plus_binom_pow3\<close>, (* (a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3 *) |
691 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*) |
662 \<^rule_thm>\<open>real_minus_binom_pow3\<close>, (* (a - b) \<up> 3 = a \<up> 3 - 3*a \<up> 2*b + 3*a*b \<up> 2 - b \<up> 3 *) |
692 \<^rule_thm>\<open>real_pm_binom_times\<close>, |
663 |
693 (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*) |
664 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*) |
694 \<^rule_thm>\<open>real_mp_binom_times\<close>, |
665 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*) |
695 (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*) |
666 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*) |
696 \<^rule_thm>\<open>real_mm_binom_times\<close>, |
667 |
697 (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*) |
668 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
698 \<^rule_thm>\<open>realpow_multI\<close>, |
669 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
699 (*(a*b) \<up> n = a \<up> n * b \<up> n*) |
670 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"), |
700 \<^rule_thm>\<open>real_plus_binom_pow3\<close>, |
671 |
701 (* (a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3 *) |
672 \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*) |
702 \<^rule_thm>\<open>real_minus_binom_pow3\<close>, |
673 \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r \<up> n = r \<up> (n + 1)"*) |
703 (* (a - b) \<up> 3 = a \<up> 3 - 3*a \<up> 2*b + 3*a*b \<up> 2 - b \<up> 3 *) |
674 (*\<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)*) |
704 |
675 \<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*) |
705 |
676 |
706 (* \<^rule_thm>\<open>distrib_right\<close>, |
677 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*) |
707 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
678 \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*) |
708 \<^rule_thm>\<open>distrib_left\<close>, |
679 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_const ==> n + m * n = (1 + m) * n"*) |
709 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) |
680 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) |
710 \<^rule_thm>\<open>left_diff_distrib\<close>, |
681 |
711 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*) |
682 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
712 \<^rule_thm>\<open>right_diff_distrib\<close>, |
683 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
713 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*) |
684 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")], |
714 *) |
685 scr = Rule.Empty_Prog}; |
715 |
|
716 \<^rule_thm>\<open>mult_1_left\<close>, |
|
717 (*"1 * z = z"*) |
|
718 \<^rule_thm>\<open>mult_zero_left\<close>, |
|
719 (*"0 * z = 0"*) |
|
720 \<^rule_thm>\<open>add_0_left\<close>, |
|
721 (*"0 + z = z"*) |
|
722 |
|
723 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
|
724 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
|
725 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"), |
|
726 (* |
|
727 \<^rule_thm>\<open>mult.commute\<close>, |
|
728 (*AC-rewriting*) |
|
729 \<^rule_thm>\<open>real_mult_left_commute\<close>, |
|
730 \<^rule_thm>\<open>mult.assoc\<close>, |
|
731 \<^rule_thm>\<open>add.commute\<close>, |
|
732 \<^rule_thm>\<open>add.left_commute\<close>, |
|
733 \<^rule_thm>\<open>add.assoc\<close>, |
|
734 *) |
|
735 |
|
736 \<^rule_thm_sym>\<open>realpow_twoI\<close>, |
|
737 (*"r1 * r1 = r1 \<up> 2"*) |
|
738 \<^rule_thm>\<open>realpow_plus_1\<close>, |
|
739 (*"r * r \<up> n = r \<up> (n + 1)"*) |
|
740 (*\<^rule_thm_sym>\<open>real_mult_2\<close>, |
|
741 (*"z1 + z1 = 2 * z1"*)*) |
|
742 \<^rule_thm>\<open>real_mult_2_assoc\<close>, |
|
743 (*"z1 + (z1 + k) = 2 * z1 + k"*) |
|
744 |
|
745 \<^rule_thm>\<open>real_num_collect\<close>, |
|
746 (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*) |
|
747 \<^rule_thm>\<open>real_num_collect_assoc\<close>, |
|
748 (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*) |
|
749 \<^rule_thm>\<open>real_one_collect\<close>, |
|
750 (*"m is_const ==> n + m * n = (1 + m) * n"*) |
|
751 \<^rule_thm>\<open>real_one_collect_assoc\<close>, |
|
752 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) |
|
753 |
|
754 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
|
755 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
|
756 \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_") |
|
757 ], |
|
758 scr = Rule.Empty_Prog |
|
759 (*Program ((Thm.term_of o the o (parse thy)) scr_expand_binomtest)*) |
|
760 }; |
|
761 \<close> |
686 \<close> |
762 rule_set_knowledge |
687 rule_set_knowledge |
763 make_polytest = \<open>prep_rls' make_polytest\<close> and |
688 make_polytest = \<open>prep_rls' make_polytest\<close> and |
764 expand_binomtest = \<open>prep_rls' expand_binomtest\<close> |
689 expand_binomtest = \<open>prep_rls' expand_binomtest\<close> |
765 rule_set_knowledge |
690 rule_set_knowledge |