359 \<^rule_thm>\<open>rat_leq3\<close> |
359 \<^rule_thm>\<open>rat_leq3\<close> |
360 ]); |
360 ]); |
361 |
361 |
362 val cancel_leading_coeff = prep_rls'( |
362 val cancel_leading_coeff = prep_rls'( |
363 Rule_Def.Repeat {id = "cancel_leading_coeff", preconds = [], |
363 Rule_Def.Repeat {id = "cancel_leading_coeff", preconds = [], |
364 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), |
364 rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), |
365 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
365 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
366 rules = [ |
366 rules = [ |
367 \<^rule_thm>\<open>cancel_leading_coeff1\<close>, |
367 \<^rule_thm>\<open>cancel_leading_coeff1\<close>, |
368 \<^rule_thm>\<open>cancel_leading_coeff2\<close>, |
368 \<^rule_thm>\<open>cancel_leading_coeff2\<close>, |
369 \<^rule_thm>\<open>cancel_leading_coeff3\<close>, |
369 \<^rule_thm>\<open>cancel_leading_coeff3\<close>, |
382 val prep_rls' = Auto_Prog.prep_rls @{theory}; |
382 val prep_rls' = Auto_Prog.prep_rls @{theory}; |
383 \<close> |
383 \<close> |
384 ML\<open> |
384 ML\<open> |
385 val complete_square = prep_rls'( |
385 val complete_square = prep_rls'( |
386 Rule_Def.Repeat {id = "complete_square", preconds = [], |
386 Rule_Def.Repeat {id = "complete_square", preconds = [], |
387 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), |
387 rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), |
388 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
388 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
389 rules = [ |
389 rules = [ |
390 \<^rule_thm>\<open>complete_square1\<close>, |
390 \<^rule_thm>\<open>complete_square1\<close>, |
391 \<^rule_thm>\<open>complete_square2\<close>, |
391 \<^rule_thm>\<open>complete_square2\<close>, |
392 \<^rule_thm>\<open>complete_square3\<close>, |
392 \<^rule_thm>\<open>complete_square3\<close>, |
425 (* the subsequent rule-sets are caused by the lack of rewriting at the time of implementation *) |
425 (* the subsequent rule-sets are caused by the lack of rewriting at the time of implementation *) |
426 (* -- d0 -- *) |
426 (* -- d0 -- *) |
427 (*isolate the bound variable in an d0 equation; 'bdv' is a meta-constant*) |
427 (*isolate the bound variable in an d0 equation; 'bdv' is a meta-constant*) |
428 val d0_polyeq_simplify = prep_rls'( |
428 val d0_polyeq_simplify = prep_rls'( |
429 Rule_Def.Repeat {id = "d0_polyeq_simplify", preconds = [], |
429 Rule_Def.Repeat {id = "d0_polyeq_simplify", preconds = [], |
430 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), |
430 rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), |
431 erls = PolyEq_erls, |
431 erls = PolyEq_erls, |
432 srls = Rule_Set.Empty, |
432 srls = Rule_Set.Empty, |
433 calc = [], errpatts = [], |
433 calc = [], errpatts = [], |
434 rules = [ |
434 rules = [ |
435 \<^rule_thm>\<open>d0_true\<close>, |
435 \<^rule_thm>\<open>d0_true\<close>, |
438 |
438 |
439 (* -- d1 -- *) |
439 (* -- d1 -- *) |
440 (*isolate the bound variable in an d1 equation; 'bdv' is a meta-constant*) |
440 (*isolate the bound variable in an d1 equation; 'bdv' is a meta-constant*) |
441 val d1_polyeq_simplify = prep_rls'( |
441 val d1_polyeq_simplify = prep_rls'( |
442 Rule_Def.Repeat {id = "d1_polyeq_simplify", preconds = [], |
442 Rule_Def.Repeat {id = "d1_polyeq_simplify", preconds = [], |
443 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), |
443 rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), |
444 erls = PolyEq_erls, |
444 erls = PolyEq_erls, |
445 srls = Rule_Set.Empty, |
445 srls = Rule_Set.Empty, |
446 calc = [], errpatts = [], |
446 calc = [], errpatts = [], |
447 rules = [ |
447 rules = [ |
448 \<^rule_thm>\<open>d1_isolate_add1\<close>, (* a+bx=0 -> bx=-a *) |
448 \<^rule_thm>\<open>d1_isolate_add1\<close>, (* a+bx=0 -> bx=-a *) |
454 subsection \<open>degree 2\<close> |
454 subsection \<open>degree 2\<close> |
455 ML\<open> |
455 ML\<open> |
456 (* isolate the bound variable in an d2 equation with bdv only; |
456 (* isolate the bound variable in an d2 equation with bdv only; |
457 "bdv" is a meta-constant substituted for the "x" below by isac's rewriter. *) |
457 "bdv" is a meta-constant substituted for the "x" below by isac's rewriter. *) |
458 val d2_polyeq_bdv_only_simplify = prep_rls'( |
458 val d2_polyeq_bdv_only_simplify = prep_rls'( |
459 Rule_Def.Repeat {id = "d2_polyeq_bdv_only_simplify", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), |
459 Rule_Def.Repeat {id = "d2_polyeq_bdv_only_simplify", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), |
460 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
460 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
461 rules = [ |
461 rules = [ |
462 \<^rule_thm>\<open>d2_prescind1\<close>, (* ax+bx^2=0 -> x(a+bx)=0 *) |
462 \<^rule_thm>\<open>d2_prescind1\<close>, (* ax+bx^2=0 -> x(a+bx)=0 *) |
463 \<^rule_thm>\<open>d2_prescind2\<close>, (* ax+ x^2=0 -> x(a+ x)=0 *) |
463 \<^rule_thm>\<open>d2_prescind2\<close>, (* ax+ x^2=0 -> x(a+ x)=0 *) |
464 \<^rule_thm>\<open>d2_prescind3\<close>, (* x+bx^2=0 -> x(1+bx)=0 *) |
464 \<^rule_thm>\<open>d2_prescind3\<close>, (* x+bx^2=0 -> x(1+bx)=0 *) |
473 |
473 |
474 (* isolate the bound variable in an d2 equation with sqrt only; |
474 (* isolate the bound variable in an d2 equation with sqrt only; |
475 'bdv' is a meta-constant*) |
475 'bdv' is a meta-constant*) |
476 val d2_polyeq_sq_only_simplify = prep_rls'( |
476 val d2_polyeq_sq_only_simplify = prep_rls'( |
477 Rule_Def.Repeat {id = "d2_polyeq_sq_only_simplify", preconds = [], |
477 Rule_Def.Repeat {id = "d2_polyeq_sq_only_simplify", preconds = [], |
478 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), |
478 rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), |
479 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
479 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
480 rules = [ |
480 rules = [ |
481 \<^rule_thm>\<open>d2_isolate_add1\<close>,(* a+ bx^2=0 -> bx^2=(-1)a*) |
481 \<^rule_thm>\<open>d2_isolate_add1\<close>,(* a+ bx^2=0 -> bx^2=(-1)a*) |
482 \<^rule_thm>\<open>d2_isolate_add2\<close>, (* a+ x^2=0 -> x^2=(-1)a*) |
482 \<^rule_thm>\<open>d2_isolate_add2\<close>, (* a+ x^2=0 -> x^2=(-1)a*) |
483 \<^rule_thm>\<open>d2_sqrt_equation2\<close>, (* x^2=0 -> x=0 *) |
483 \<^rule_thm>\<open>d2_sqrt_equation2\<close>, (* x^2=0 -> x=0 *) |
489 ML\<open> |
489 ML\<open> |
490 (* isolate the bound variable in an d2 equation with pqFormula; |
490 (* isolate the bound variable in an d2 equation with pqFormula; |
491 'bdv' is a meta-constant*) |
491 'bdv' is a meta-constant*) |
492 val d2_polyeq_pqFormula_simplify = prep_rls'( |
492 val d2_polyeq_pqFormula_simplify = prep_rls'( |
493 Rule_Def.Repeat {id = "d2_polyeq_pqFormula_simplify", preconds = [], |
493 Rule_Def.Repeat {id = "d2_polyeq_pqFormula_simplify", preconds = [], |
494 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls, |
494 rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls, |
495 srls = Rule_Set.Empty, calc = [], errpatts = [], |
495 srls = Rule_Set.Empty, calc = [], errpatts = [], |
496 rules = [ |
496 rules = [ |
497 \<^rule_thm>\<open>d2_pqformula1\<close>, (* q+px+ x^2=0 *) |
497 \<^rule_thm>\<open>d2_pqformula1\<close>, (* q+px+ x^2=0 *) |
498 \<^rule_thm>\<open>d2_pqformula1_neg\<close>, (* q+px+ x^2=0 *) |
498 \<^rule_thm>\<open>d2_pqformula1_neg\<close>, (* q+px+ x^2=0 *) |
499 \<^rule_thm>\<open>d2_pqformula2\<close>, (* q+px+1x^2=0 *) |
499 \<^rule_thm>\<open>d2_pqformula2\<close>, (* q+px+1x^2=0 *) |
516 |
516 |
517 (* isolate the bound variable in an d2 equation with abcFormula; |
517 (* isolate the bound variable in an d2 equation with abcFormula; |
518 'bdv' is a meta-constant*) |
518 'bdv' is a meta-constant*) |
519 val d2_polyeq_abcFormula_simplify = prep_rls'( |
519 val d2_polyeq_abcFormula_simplify = prep_rls'( |
520 Rule_Def.Repeat {id = "d2_polyeq_abcFormula_simplify", preconds = [], |
520 Rule_Def.Repeat {id = "d2_polyeq_abcFormula_simplify", preconds = [], |
521 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls, |
521 rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls, |
522 srls = Rule_Set.Empty, calc = [], errpatts = [], |
522 srls = Rule_Set.Empty, calc = [], errpatts = [], |
523 rules = [ |
523 rules = [ |
524 \<^rule_thm>\<open>d2_abcformula1\<close>, (*c+bx+cx^2=0 *) |
524 \<^rule_thm>\<open>d2_abcformula1\<close>, (*c+bx+cx^2=0 *) |
525 \<^rule_thm>\<open>d2_abcformula1_neg\<close>, (*c+bx+cx^2=0 *) |
525 \<^rule_thm>\<open>d2_abcformula1_neg\<close>, (*c+bx+cx^2=0 *) |
526 \<^rule_thm>\<open>d2_abcformula2\<close>, (*c+ x+cx^2=0 *) |
526 \<^rule_thm>\<open>d2_abcformula2\<close>, (*c+ x+cx^2=0 *) |
543 |
543 |
544 (* isolate the bound variable in an d2 equation; |
544 (* isolate the bound variable in an d2 equation; |
545 'bdv' is a meta-constant*) |
545 'bdv' is a meta-constant*) |
546 val d2_polyeq_simplify = prep_rls'( |
546 val d2_polyeq_simplify = prep_rls'( |
547 Rule_Def.Repeat {id = "d2_polyeq_simplify", preconds = [], |
547 Rule_Def.Repeat {id = "d2_polyeq_simplify", preconds = [], |
548 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls, |
548 rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls, |
549 srls = Rule_Set.Empty, calc = [], errpatts = [], |
549 srls = Rule_Set.Empty, calc = [], errpatts = [], |
550 rules = [ |
550 rules = [ |
551 \<^rule_thm>\<open>d2_pqformula1\<close>, (* p+qx+ x^2=0 *) |
551 \<^rule_thm>\<open>d2_pqformula1\<close>, (* p+qx+ x^2=0 *) |
552 \<^rule_thm>\<open>d2_pqformula1_neg\<close>, (* p+qx+ x^2=0 *) |
552 \<^rule_thm>\<open>d2_pqformula1_neg\<close>, (* p+qx+ x^2=0 *) |
553 \<^rule_thm>\<open>d2_pqformula2\<close>, (* p+qx+1x^2=0 *) |
553 \<^rule_thm>\<open>d2_pqformula2\<close>, (* p+qx+1x^2=0 *) |
576 |
576 |
577 (* -- d3 -- *) |
577 (* -- d3 -- *) |
578 (* isolate the bound variable in an d3 equation; 'bdv' is a meta-constant *) |
578 (* isolate the bound variable in an d3 equation; 'bdv' is a meta-constant *) |
579 val d3_polyeq_simplify = prep_rls'( |
579 val d3_polyeq_simplify = prep_rls'( |
580 Rule_Def.Repeat {id = "d3_polyeq_simplify", preconds = [], |
580 Rule_Def.Repeat {id = "d3_polyeq_simplify", preconds = [], |
581 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls, |
581 rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls, |
582 srls = Rule_Set.Empty, calc = [], errpatts = [], |
582 srls = Rule_Set.Empty, calc = [], errpatts = [], |
583 rules = [ |
583 rules = [ |
584 \<^rule_thm>\<open>d3_reduce_equation1\<close>, (*a*bdv + b*bdv \<up> 2 + c*bdv \<up> 3=0) = (bdv=0 | (a + b*bdv + c*bdv \<up> 2=0)*) |
584 \<^rule_thm>\<open>d3_reduce_equation1\<close>, (*a*bdv + b*bdv \<up> 2 + c*bdv \<up> 3=0) = (bdv=0 | (a + b*bdv + c*bdv \<up> 2=0)*) |
585 \<^rule_thm>\<open>d3_reduce_equation2\<close>, (* bdv + b*bdv \<up> 2 + c*bdv \<up> 3=0) = (bdv=0 | (1 + b*bdv + c*bdv \<up> 2=0)*) |
585 \<^rule_thm>\<open>d3_reduce_equation2\<close>, (* bdv + b*bdv \<up> 2 + c*bdv \<up> 3=0) = (bdv=0 | (1 + b*bdv + c*bdv \<up> 2=0)*) |
586 \<^rule_thm>\<open>d3_reduce_equation3\<close>, (*a*bdv + bdv \<up> 2 + c*bdv \<up> 3=0) = (bdv=0 | (a + bdv + c*bdv \<up> 2=0)*) |
586 \<^rule_thm>\<open>d3_reduce_equation3\<close>, (*a*bdv + bdv \<up> 2 + c*bdv \<up> 3=0) = (bdv=0 | (a + bdv + c*bdv \<up> 2=0)*) |
606 |
606 |
607 (* -- d4 -- *) |
607 (* -- d4 -- *) |
608 (*isolate the bound variable in an d4 equation; 'bdv' is a meta-constant*) |
608 (*isolate the bound variable in an d4 equation; 'bdv' is a meta-constant*) |
609 val d4_polyeq_simplify = prep_rls'( |
609 val d4_polyeq_simplify = prep_rls'( |
610 Rule_Def.Repeat {id = "d4_polyeq_simplify", preconds = [], |
610 Rule_Def.Repeat {id = "d4_polyeq_simplify", preconds = [], |
611 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls, |
611 rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls, |
612 srls = Rule_Set.Empty, calc = [], errpatts = [], |
612 srls = Rule_Set.Empty, calc = [], errpatts = [], |
613 rules = [ |
613 rules = [ |
614 \<^rule_thm>\<open>d4_sub_u1\<close> (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *)], |
614 \<^rule_thm>\<open>d4_sub_u1\<close> (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *)], |
615 scr = Rule.Empty_Prog}); |
615 scr = Rule.Empty_Prog}); |
616 \<close> |
616 \<close> |
1126 |
1126 |
1127 \<close> |
1127 \<close> |
1128 ML\<open> |
1128 ML\<open> |
1129 val collect_bdv = prep_rls'( |
1129 val collect_bdv = prep_rls'( |
1130 Rule_Def.Repeat{id = "collect_bdv", preconds = [], |
1130 Rule_Def.Repeat{id = "collect_bdv", preconds = [], |
1131 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
1131 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
1132 erls = Rule_Set.empty,srls = Rule_Set.Empty, |
1132 erls = Rule_Set.empty,srls = Rule_Set.Empty, |
1133 calc = [], errpatts = [], |
1133 calc = [], errpatts = [], |
1134 rules = [\<^rule_thm>\<open>bdv_collect_1\<close>, |
1134 rules = [\<^rule_thm>\<open>bdv_collect_1\<close>, |
1135 \<^rule_thm>\<open>bdv_collect_2\<close>, |
1135 \<^rule_thm>\<open>bdv_collect_2\<close>, |
1136 \<^rule_thm>\<open>bdv_collect_3\<close>, |
1136 \<^rule_thm>\<open>bdv_collect_3\<close>, |
1161 ML\<open> |
1161 ML\<open> |
1162 (*.transforms an arbitrary term without roots to a polynomial [4] |
1162 (*.transforms an arbitrary term without roots to a polynomial [4] |
1163 according to knowledge/Poly.sml.*) |
1163 according to knowledge/Poly.sml.*) |
1164 val make_polynomial_in = prep_rls'( |
1164 val make_polynomial_in = prep_rls'( |
1165 Rule_Set.Sequence { |
1165 Rule_Set.Sequence { |
1166 id = "make_polynomial_in", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
1166 id = "make_polynomial_in", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
1167 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
1167 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
1168 rules = [ |
1168 rules = [ |
1169 Rule.Rls_ expand_poly, |
1169 Rule.Rls_ expand_poly, |
1170 Rule.Rls_ order_add_mult_in, |
1170 Rule.Rls_ order_add_mult_in, |
1171 Rule.Rls_ simplify_power, |
1171 Rule.Rls_ simplify_power, |
1187 WN051031 DOES NOT BELONG TO HERE*)]; |
1187 WN051031 DOES NOT BELONG TO HERE*)]; |
1188 \<close> |
1188 \<close> |
1189 ML\<open> |
1189 ML\<open> |
1190 val make_ratpoly_in = prep_rls'( |
1190 val make_ratpoly_in = prep_rls'( |
1191 Rule_Set.Sequence { |
1191 Rule_Set.Sequence { |
1192 id = "make_ratpoly_in", preconds = []:term list, rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
1192 id = "make_ratpoly_in", preconds = []:term list, rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
1193 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
1193 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
1194 rules = [ |
1194 rules = [ |
1195 Rule.Rls_ norm_Rational, |
1195 Rule.Rls_ norm_Rational, |
1196 Rule.Rls_ order_add_mult_in, |
1196 Rule.Rls_ order_add_mult_in, |
1197 Rule.Rls_ discard_parentheses, |
1197 Rule.Rls_ discard_parentheses, |