480 (prep_pbt thy "pbl_equ_univ_root" [] e_pblID |
480 (prep_pbt thy "pbl_equ_univ_root" [] e_pblID |
481 (["root'","univariate","equation"], |
481 (["root'","univariate","equation"], |
482 [("#Given" ,["equality e_e","solveFor v_v"]), |
482 [("#Given" ,["equality e_e","solveFor v_v"]), |
483 ("#Where" ,["(lhs e_e) is_rootTerm_in (v_v::real) | " ^ |
483 ("#Where" ,["(lhs e_e) is_rootTerm_in (v_v::real) | " ^ |
484 "(rhs e_e) is_rootTerm_in (v_v::real)"]), |
484 "(rhs e_e) is_rootTerm_in (v_v::real)"]), |
485 ("#Find" ,["solutions v_i'''"]) |
485 ("#Find" ,["solutions v'i'"]) |
486 ], |
486 ], |
487 RootEq_prls, SOME "solve (e_e::bool, v_v)", |
487 RootEq_prls, SOME "solve (e_e::bool, v_v)", |
488 [])); |
488 [])); |
489 (* ---------sqrt----------- *) |
489 (* ---------sqrt----------- *) |
490 store_pbt |
490 store_pbt |
493 [("#Given" ,["equality e_e","solveFor v_v"]), |
493 [("#Given" ,["equality e_e","solveFor v_v"]), |
494 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
494 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
495 " ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |" ^ |
495 " ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |" ^ |
496 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
496 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
497 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"]), |
497 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"]), |
498 ("#Find" ,["solutions v_i'''"]) |
498 ("#Find" ,["solutions v'i'"]) |
499 ], |
499 ], |
500 RootEq_prls, SOME "solve (e_e::bool, v_v)", |
500 RootEq_prls, SOME "solve (e_e::bool, v_v)", |
501 [["RootEq","solve_sq_root_equation"]])); |
501 [["RootEq","solve_sq_root_equation"]])); |
502 (* ---------normalize----------- *) |
502 (* ---------normalize----------- *) |
503 store_pbt |
503 store_pbt |
506 [("#Given" ,["equality e_e","solveFor v_v"]), |
506 [("#Given" ,["equality e_e","solveFor v_v"]), |
507 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
507 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
508 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^ |
508 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^ |
509 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
509 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
510 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]), |
510 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]), |
511 ("#Find" ,["solutions v_i'''"]) |
511 ("#Find" ,["solutions v'i'"]) |
512 ], |
512 ], |
513 RootEq_prls, SOME "solve (e_e::bool, v_v)", |
513 RootEq_prls, SOME "solve (e_e::bool, v_v)", |
514 [["RootEq","norm_sq_root_equation"]])); |
514 [["RootEq","norm_sq_root_equation"]])); |
515 |
515 |
516 (*-------------------------methods-----------------------*) |
516 (*-------------------------methods-----------------------*) |
530 [("#Given" ,["equality e_e","solveFor v_v"]), |
530 [("#Given" ,["equality e_e","solveFor v_v"]), |
531 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
531 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
532 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^ |
532 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^ |
533 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
533 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
534 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]), |
534 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]), |
535 ("#Find" ,["solutions v_i'''"]) |
535 ("#Find" ,["solutions v'i'"]) |
536 ], |
536 ], |
537 {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls, |
537 {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls, |
538 calc=[], crls=RootEq_crls, nrls=norm_Poly}, |
538 calc=[], crls=RootEq_crls, nrls=norm_Poly}, |
539 "Script Norm_sq_root_equation (e_e::bool) (v_v::real) = " ^ |
539 "Script Norm_sq_root_equation (e_e::bool) (v_v::real) = " ^ |
540 "(let e_e = ((Repeat(Try (Rewrite makex1_x False))) @@ " ^ |
540 "(let e_e = ((Repeat(Try (Rewrite makex1_x False))) @@ " ^ |
556 [("#Given" ,["equality e_e", "solveFor v_v"]), |
556 [("#Given" ,["equality e_e", "solveFor v_v"]), |
557 ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real)) & " ^ |
557 ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real)) & " ^ |
558 " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^ |
558 " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^ |
559 "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^ |
559 "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^ |
560 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]), |
560 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]), |
561 ("#Find" ,["solutions v_i'''"]) |
561 ("#Find" ,["solutions v'i'"]) |
562 ], |
562 ], |
563 {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls, |
563 {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls, |
564 prls = RootEq_prls, calc = [], crls=RootEq_crls, nrls=norm_Poly}, |
564 prls = RootEq_prls, calc = [], crls=RootEq_crls, nrls=norm_Poly}, |
565 "Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^ |
565 "Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^ |
566 "(let e_e = " ^ |
566 "(let e_e = " ^ |
584 store_met |
584 store_met |
585 (prep_met thy "met_rooteq_sq_right" [] e_metID |
585 (prep_met thy "met_rooteq_sq_right" [] e_metID |
586 (["RootEq","solve_right_sq_root_equation"], |
586 (["RootEq","solve_right_sq_root_equation"], |
587 [("#Given" ,["equality e_e","solveFor v_v"]), |
587 [("#Given" ,["equality e_e","solveFor v_v"]), |
588 ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]), |
588 ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]), |
589 ("#Find" ,["solutions v_i'''"]) |
589 ("#Find" ,["solutions v'i'"]) |
590 ], |
590 ], |
591 {rew_ord' = "termlessI", rls' = RootEq_erls, srls = e_rls, |
591 {rew_ord' = "termlessI", rls' = RootEq_erls, srls = e_rls, |
592 prls = RootEq_prls, calc = [], crls = RootEq_crls, nrls = norm_Poly}, |
592 prls = RootEq_prls, calc = [], crls = RootEq_crls, nrls = norm_Poly}, |
593 "Script Solve_right_sq_root_equation (e_e::bool) (v_v::real) = " ^ |
593 "Script Solve_right_sq_root_equation (e_e::bool) (v_v::real) = " ^ |
594 "(let e_e = " ^ |
594 "(let e_e = " ^ |
609 store_met |
609 store_met |
610 (prep_met thy "met_rooteq_sq_left" [] e_metID |
610 (prep_met thy "met_rooteq_sq_left" [] e_metID |
611 (["RootEq","solve_left_sq_root_equation"], |
611 (["RootEq","solve_left_sq_root_equation"], |
612 [("#Given" ,["equality e_e","solveFor v_v"]), |
612 [("#Given" ,["equality e_e","solveFor v_v"]), |
613 ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]), |
613 ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]), |
614 ("#Find" ,["solutions v_i'''"]) |
614 ("#Find" ,["solutions v'i'"]) |
615 ], |
615 ], |
616 {rew_ord'="termlessI", |
616 {rew_ord'="termlessI", |
617 rls'=RootEq_erls, |
617 rls'=RootEq_erls, |
618 srls=e_rls, |
618 srls=e_rls, |
619 prls=RootEq_prls, |
619 prls=RootEq_prls, |