531 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^ |
532 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^ |
532 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
533 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
533 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]), |
534 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]), |
534 ("#Find" ,["solutions v_i"]) |
535 ("#Find" ,["solutions v_i"]) |
535 ], |
536 ], |
536 {rew_ord'="termlessI", |
537 {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls, |
537 rls'=RootEq_erls, |
538 calc=[], crls=RootEq_crls, nrls=norm_Poly}, |
538 srls=e_rls, |
|
539 prls=RootEq_prls, |
|
540 calc=[], |
|
541 crls=RootEq_crls, nrls=norm_Poly(*, |
|
542 asm_rls=[], |
|
543 asm_thm=[("sqrt_square_1","")]*)}, |
|
544 "Script Norm_sq_root_equation (e_e::bool) (v_v::real) = " ^ |
539 "Script Norm_sq_root_equation (e_e::bool) (v_v::real) = " ^ |
545 "(let e_e = ((Repeat(Try (Rewrite makex1_x False))) @@ " ^ |
540 "(let e_e = ((Repeat(Try (Rewrite makex1_x False))) @@ " ^ |
546 " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^ |
541 " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^ |
547 " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^ |
542 " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^ |
548 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^ |
543 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^ |
549 " (Try (Rewrite_Set rooteq_simplify True))) e_e " ^ |
544 " (Try (Rewrite_Set rooteq_simplify True))) e_e " ^ |
550 " in ((SubProblem (RootEq_,[univariate,equation], " ^ |
545 " in ((SubProblem (RootEq_',[univariate,equation], " ^ |
551 " [no_met]) [BOOL e_e, REAL v_])))" |
546 " [no_met]) [BOOL e_e, REAL v_v])))" |
552 )); |
547 )); |
553 |
548 |
|
549 *} |
|
550 |
|
551 ML {* (*-----del------------------------------------------------del-----*) |
|
552 Toplevel.debug := true; |
|
553 val scr = |
|
554 "Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^ |
|
555 "(let e_e = " ^ |
|
556 " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] sqrt_isolate True)) @@ " ^ |
|
557 " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^ |
|
558 " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^ |
|
559 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^ |
|
560 " (Try (Rewrite_Set rooteq_simplify True)) ) e_e; " ^ |
|
561 " (L_L::bool list) = " ^ |
|
562 " (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^ |
|
563 " then (SubProblem (RootEq_',[normalize,root',univariate,equation], " ^ |
|
564 " [no_met]) [BOOL e_e, REAL v_v]) " ^ |
|
565 " else (SubProblem (RootEq_',[univariate,equation], [no_met]) " ^ |
|
566 " [BOOL e_e, REAL v_v])) " ^ |
|
567 "in Check_elementwise L_L {(v_v::real). Assumptions})"; |
|
568 val sss = ( term_of o the o (parse thy)) scr; |
|
569 *} |
|
570 |
|
571 ML {* |
|
572 val -------------------------------------------------- = "00000"; |
554 store_met |
573 store_met |
555 (prep_met thy "met_rooteq_sq" [] e_metID |
574 (prep_met thy "met_rooteq_sq" [] e_metID |
556 (["RootEq","solve_sq_root_equation"], |
575 (["RootEq","solve_sq_root_equation"], |
557 [("#Given" ,["equality e_e","solveFor v_v"]), |
576 [("#Given" ,["equality e_e", "solveFor v_v"]), |
558 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
577 ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real)) & " ^ |
559 " ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |" ^ |
578 " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^ |
560 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
579 "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^ |
561 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"]), |
580 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]), |
562 ("#Find" ,["solutions v_i"]) |
581 ("#Find" ,["solutions v_i"]) |
563 ], |
582 ], |
564 {rew_ord'="termlessI", |
583 {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls, |
565 rls'=RootEq_erls, |
584 prls = RootEq_prls, calc = [], crls=RootEq_crls, nrls=norm_Poly}, |
566 srls = rooteq_srls, |
585 "Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^ |
567 prls = RootEq_prls, |
586 "(let e_e = " ^ |
568 calc = [], |
587 " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] sqrt_isolate True)) @@ " ^ |
569 crls=RootEq_crls, nrls=norm_Poly}, |
588 " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^ |
570 "Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^ |
589 " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^ |
571 "(let e_e = " ^ |
590 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^ |
572 " ((Try (Rewrite_Set_Inst [(bdv,v_::real)] sqrt_isolate True)) @@ " ^ |
591 " (Try (Rewrite_Set rooteq_simplify True)) ) e_e; " ^ |
573 " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^ |
592 " (L_L::bool list) = " ^ |
574 " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^ |
593 " (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^ |
575 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^ |
594 " then (SubProblem (RootEq_',[normalize,root',univariate,equation], " ^ |
576 " (Try (Rewrite_Set rooteq_simplify True))) e_;" ^ |
595 " [no_met]) [BOOL e_e, REAL v_v]) " ^ |
577 " (L_::bool list) = " ^ |
596 " else (SubProblem (RootEq_',[univariate,equation], [no_met]) " ^ |
578 " (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^ |
597 " [BOOL e_e, REAL v_v])) " ^ |
579 " then (SubProblem (RootEq_,[normalize,root,univariate,equation], " ^ |
598 "in Check_elementwise L_L {(v_v::real). Assumptions})" |
580 " [no_met]) [BOOL e_e, REAL v_]) " ^ |
|
581 " else (SubProblem (RootEq_,[univariate,equation], " ^ |
|
582 " [no_met]) [BOOL e_e, REAL v_])) " ^ |
|
583 " in Check_elementwise L_ {(v_v::real). Assumptions})" |
|
584 )); |
599 )); |
585 |
600 *} |
|
601 |
|
602 ML {* |
586 (*-- right 28.08.02 --*) |
603 (*-- right 28.08.02 --*) |
587 store_met |
604 store_met |
588 (prep_met thy "met_rooteq_sq_right" [] e_metID |
605 (prep_met thy "met_rooteq_sq_right" [] e_metID |
589 (["RootEq","solve_right_sq_root_equation"], |
606 (["RootEq","solve_right_sq_root_equation"], |
590 [("#Given" ,["equality e_e","solveFor v_v"]), |
607 [("#Given" ,["equality e_e","solveFor v_v"]), |
591 ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]), |
608 ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]), |
592 ("#Find" ,["solutions v_i"]) |
609 ("#Find" ,["solutions v_i"]) |
593 ], |
610 ], |
594 {rew_ord'="termlessI", |
611 {rew_ord' = "termlessI", rls' = RootEq_erls, srls = e_rls, |
595 rls'=RootEq_erls, |
612 prls = RootEq_prls, calc = [], crls = RootEq_crls, nrls = norm_Poly}, |
596 srls=e_rls, |
613 "Script Solve_right_sq_root_equation (e_e::bool) (v_v::real) = " ^ |
597 prls=RootEq_prls, |
614 "(let e_e = " ^ |
598 calc=[], |
615 " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] r_sqrt_isolate False)) @@ " ^ |
599 crls=RootEq_crls, nrls=norm_Poly}, |
616 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^ |
600 "Script Solve_right_sq_root_equation (e_e::bool) (v_v::real) = " ^ |
617 " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^ |
601 "(let e_e = " ^ |
618 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^ |
602 " ((Try (Rewrite_Set_Inst [(bdv,v_::real)] r_sqrt_isolate False)) @@ " ^ |
|
603 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^ |
|
604 " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^ |
|
605 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^ |
|
606 " (Try (Rewrite_Set rooteq_simplify False))) e_e " ^ |
619 " (Try (Rewrite_Set rooteq_simplify False))) e_e " ^ |
607 " in if ((rhs e_e) is_sqrtTerm_in v_v) " ^ |
620 " in if ((rhs e_e) is_sqrtTerm_in v_v) " ^ |
608 " then (SubProblem (RootEq_,[normalize,root,univariate,equation], " ^ |
621 " then (SubProblem (RootEq_',[normalize,root',univariate,equation], " ^ |
609 " [no_met]) [BOOL e_e, REAL v_]) " ^ |
622 " [no_met]) [BOOL e_e, REAL v_v]) " ^ |
610 " else ((SubProblem (RootEq_,[univariate,equation], " ^ |
623 " else ((SubProblem (RootEq_',[univariate,equation], " ^ |
611 " [no_met]) [BOOL e_e, REAL v_])))" |
624 " [no_met]) [BOOL e_e, REAL v_v])))" |
612 )); |
625 )); |
|
626 val --------------------------------------------------+++ = "33333"; |
613 |
627 |
614 (*-- left 28.08.02 --*) |
628 (*-- left 28.08.02 --*) |
615 store_met |
629 store_met |
616 (prep_met thy "met_rooteq_sq_left" [] e_metID |
630 (prep_met thy "met_rooteq_sq_left" [] e_metID |
617 (["RootEq","solve_left_sq_root_equation"], |
631 (["RootEq","solve_left_sq_root_equation"], |
625 prls=RootEq_prls, |
639 prls=RootEq_prls, |
626 calc=[], |
640 calc=[], |
627 crls=RootEq_crls, nrls=norm_Poly}, |
641 crls=RootEq_crls, nrls=norm_Poly}, |
628 "Script Solve_left_sq_root_equation (e_e::bool) (v_v::real) = " ^ |
642 "Script Solve_left_sq_root_equation (e_e::bool) (v_v::real) = " ^ |
629 "(let e_e = " ^ |
643 "(let e_e = " ^ |
630 " ((Try (Rewrite_Set_Inst [(bdv,v_::real)] l_sqrt_isolate False)) @@ " ^ |
644 " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] l_sqrt_isolate False)) @@ " ^ |
631 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^ |
645 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^ |
632 " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^ |
646 " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^ |
633 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^ |
647 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^ |
634 " (Try (Rewrite_Set rooteq_simplify False))) e_e " ^ |
648 " (Try (Rewrite_Set rooteq_simplify False))) e_e " ^ |
635 " in if ((lhs e_e) is_sqrtTerm_in v_v) " ^ |
649 " in if ((lhs e_e) is_sqrtTerm_in v_v) " ^ |
636 " then (SubProblem (RootEq_,[normalize,root,univariate,equation], " ^ |
650 " then (SubProblem (RootEq_',[normalize,root',univariate,equation], " ^ |
637 " [no_met]) [BOOL e_e, REAL v_]) " ^ |
651 " [no_met]) [BOOL e_e, REAL v_v]) " ^ |
638 " else ((SubProblem (RootEq_,[univariate,equation], " ^ |
652 " else ((SubProblem (RootEq_',[univariate,equation], " ^ |
639 " [no_met]) [BOOL e_e, REAL v_])))" |
653 " [no_met]) [BOOL e_e, REAL v_v])))" |
640 )); |
654 )); |
|
655 val --------------------------------------------------++++ = "44444"; |
641 |
656 |
642 calclist':= overwritel (!calclist', |
657 calclist':= overwritel (!calclist', |
643 [("is_rootTerm_in", ("RootEq.is'_rootTerm'_in", |
658 [("is_rootTerm_in", ("RootEq.is'_rootTerm'_in", |
644 eval_is_rootTerm_in"")), |
659 eval_is_rootTerm_in"")), |
645 ("is_sqrtTerm_in", ("RootEq.is'_sqrtTerm'_in", |
660 ("is_sqrtTerm_in", ("RootEq.is'_sqrtTerm'_in", |