486 show_ptyps(); |
486 show_ptyps(); |
487 *) |
487 *) |
488 *} |
488 *} |
489 setup {* KEStore_Elems.add_pbts |
489 setup {* KEStore_Elems.add_pbts |
490 (* ---------root----------- *) |
490 (* ---------root----------- *) |
491 [(prep_pbt thy "pbl_equ_univ_root" [] e_pblID |
491 [(Specify.prep_pbt thy "pbl_equ_univ_root" [] e_pblID |
492 (["root'","univariate","equation"], |
492 (["root'","univariate","equation"], |
493 [("#Given" ,["equality e_e","solveFor v_v"]), |
493 [("#Given" ,["equality e_e","solveFor v_v"]), |
494 ("#Where" ,["(lhs e_e) is_rootTerm_in (v_v::real) | " ^ |
494 ("#Where" ,["(lhs e_e) is_rootTerm_in (v_v::real) | " ^ |
495 "(rhs e_e) is_rootTerm_in (v_v::real)"]), |
495 "(rhs e_e) is_rootTerm_in (v_v::real)"]), |
496 ("#Find" ,["solutions v_v'i'"])], |
496 ("#Find" ,["solutions v_v'i'"])], |
497 RootEq_prls, SOME "solve (e_e::bool, v_v)", [])), |
497 RootEq_prls, SOME "solve (e_e::bool, v_v)", [])), |
498 (* ---------sqrt----------- *) |
498 (* ---------sqrt----------- *) |
499 (prep_pbt thy "pbl_equ_univ_root_sq" [] e_pblID |
499 (Specify.prep_pbt thy "pbl_equ_univ_root_sq" [] e_pblID |
500 (["sq","root'","univariate","equation"], |
500 (["sq","root'","univariate","equation"], |
501 [("#Given" ,["equality e_e","solveFor v_v"]), |
501 [("#Given" ,["equality e_e","solveFor v_v"]), |
502 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
502 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
503 " ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |" ^ |
503 " ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |" ^ |
504 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
504 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
505 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"]), |
505 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"]), |
506 ("#Find" ,["solutions v_v'i'"])], |
506 ("#Find" ,["solutions v_v'i'"])], |
507 RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq","solve_sq_root_equation"]])), |
507 RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq","solve_sq_root_equation"]])), |
508 (* ---------normalize----------- *) |
508 (* ---------normalize----------- *) |
509 (prep_pbt thy "pbl_equ_univ_root_norm" [] e_pblID |
509 (Specify.prep_pbt thy "pbl_equ_univ_root_norm" [] e_pblID |
510 (["normalize","root'","univariate","equation"], |
510 (["normalize","root'","univariate","equation"], |
511 [("#Given" ,["equality e_e","solveFor v_v"]), |
511 [("#Given" ,["equality e_e","solveFor v_v"]), |
512 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
512 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
513 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^ |
513 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^ |
514 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
514 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
518 |
518 |
519 |
519 |
520 (*-------------------------methods-----------------------*) |
520 (*-------------------------methods-----------------------*) |
521 setup {* KEStore_Elems.add_mets |
521 setup {* KEStore_Elems.add_mets |
522 [(* ---- root 20.8.02 ---*) |
522 [(* ---- root 20.8.02 ---*) |
523 prep_met thy "met_rooteq" [] e_metID |
523 Specify.prep_met thy "met_rooteq" [] e_metID |
524 (["RootEq"], [], |
524 (["RootEq"], [], |
525 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, |
525 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, |
526 crls=RootEq_crls, errpats = [], nrls = norm_Poly}, "empty_script"), |
526 crls=RootEq_crls, errpats = [], nrls = norm_Poly}, "empty_script"), |
527 (*-- normalize 20.10.02 --*) |
527 (*-- normalize 20.10.02 --*) |
528 prep_met thy "met_rooteq_norm" [] e_metID |
528 Specify.prep_met thy "met_rooteq_norm" [] e_metID |
529 (["RootEq","norm_sq_root_equation"], |
529 (["RootEq","norm_sq_root_equation"], |
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)) &" ^ |
541 " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^ |
541 " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^ |
542 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^ |
542 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^ |
543 " (Try (Rewrite_Set rooteq_simplify True))) e_e " ^ |
543 " (Try (Rewrite_Set rooteq_simplify True))) e_e " ^ |
544 " in ((SubProblem (RootEq',[univariate,equation], " ^ |
544 " in ((SubProblem (RootEq',[univariate,equation], " ^ |
545 " [no_met]) [BOOL e_e, REAL v_v])))"), |
545 " [no_met]) [BOOL e_e, REAL v_v])))"), |
546 prep_met thy "met_rooteq_sq" [] e_metID |
546 Specify.prep_met thy "met_rooteq_sq" [] e_metID |
547 (["RootEq","solve_sq_root_equation"], |
547 (["RootEq","solve_sq_root_equation"], |
548 [("#Given" ,["equality e_e", "solveFor v_v"]), |
548 [("#Given" ,["equality e_e", "solveFor v_v"]), |
549 ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real)) & " ^ |
549 ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real)) & " ^ |
550 " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^ |
550 " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^ |
551 "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^ |
551 "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^ |
566 " [no_met]) [BOOL e_e, REAL v_v]) " ^ |
566 " [no_met]) [BOOL e_e, REAL v_v]) " ^ |
567 " else (SubProblem (RootEq',[univariate,equation], [no_met]) " ^ |
567 " else (SubProblem (RootEq',[univariate,equation], [no_met]) " ^ |
568 " [BOOL e_e, REAL v_v])) " ^ |
568 " [BOOL e_e, REAL v_v])) " ^ |
569 "in Check_elementwise L_L {(v_v::real). Assumptions})"), |
569 "in Check_elementwise L_L {(v_v::real). Assumptions})"), |
570 (*-- right 28.08.02 --*) |
570 (*-- right 28.08.02 --*) |
571 prep_met thy "met_rooteq_sq_right" [] e_metID |
571 Specify.prep_met thy "met_rooteq_sq_right" [] e_metID |
572 (["RootEq","solve_right_sq_root_equation"], |
572 (["RootEq","solve_right_sq_root_equation"], |
573 [("#Given" ,["equality e_e","solveFor v_v"]), |
573 [("#Given" ,["equality e_e","solveFor v_v"]), |
574 ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]), |
574 ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]), |
575 ("#Find" ,["solutions v_v'i'"])], |
575 ("#Find" ,["solutions v_v'i'"])], |
576 {rew_ord' = "termlessI", rls' = RootEq_erls, srls = e_rls, prls = RootEq_prls, calc = [], |
576 {rew_ord' = "termlessI", rls' = RootEq_erls, srls = e_rls, prls = RootEq_prls, calc = [], |
586 " then (SubProblem (RootEq',[normalize,root',univariate,equation], " ^ |
586 " then (SubProblem (RootEq',[normalize,root',univariate,equation], " ^ |
587 " [no_met]) [BOOL e_e, REAL v_v]) " ^ |
587 " [no_met]) [BOOL e_e, REAL v_v]) " ^ |
588 " else ((SubProblem (RootEq',[univariate,equation], " ^ |
588 " else ((SubProblem (RootEq',[univariate,equation], " ^ |
589 " [no_met]) [BOOL e_e, REAL v_v])))"), |
589 " [no_met]) [BOOL e_e, REAL v_v])))"), |
590 (*-- left 28.08.02 --*) |
590 (*-- left 28.08.02 --*) |
591 prep_met thy "met_rooteq_sq_left" [] e_metID |
591 Specify.prep_met thy "met_rooteq_sq_left" [] e_metID |
592 (["RootEq","solve_left_sq_root_equation"], |
592 (["RootEq","solve_left_sq_root_equation"], |
593 [("#Given" ,["equality e_e","solveFor v_v"]), |
593 [("#Given" ,["equality e_e","solveFor v_v"]), |
594 ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]), |
594 ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]), |
595 ("#Find" ,["solutions v_v'i'"])], |
595 ("#Find" ,["solutions v_v'i'"])], |
596 {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls, calc=[], |
596 {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls, calc=[], |