492 subsection \<open>methods\<close> |
492 subsection \<open>methods\<close> |
493 setup \<open>KEStore_Elems.add_mets |
493 setup \<open>KEStore_Elems.add_mets |
494 [Specify.prep_met thy "met_rooteq" [] Celem.e_metID |
494 [Specify.prep_met thy "met_rooteq" [] Celem.e_metID |
495 (["RootEq"], [], |
495 (["RootEq"], [], |
496 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule.e_rls, prls=Rule.e_rls, |
496 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule.e_rls, prls=Rule.e_rls, |
497 crls=RootEq_crls, errpats = [], nrls = norm_Poly}, "empty_script")] |
497 crls=RootEq_crls, errpats = [], nrls = norm_Poly}, @{thm refl})] |
498 \<close> |
498 \<close> |
499 (*-- normalise 20.10.02 --*) |
499 (*-- normalise 20.10.02 --*) |
500 (*ok |
|
501 partial_function (tailrec) norm_sqrt_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
500 partial_function (tailrec) norm_sqrt_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
502 where |
501 where |
503 "norm_sqrt_equ e_e v_v = |
502 "norm_sqrt_equ e_e v_v = |
504 (let e_e = ((Repeat(Try (Rewrite ''makex1_x'' False))) @@ |
503 (let e_e = ((Repeat(Try (Rewrite ''makex1_x'' False))) @@ |
505 (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ |
504 (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ |
506 (Try (Rewrite_Set ''rooteq_simplify'' True)) @@ |
505 (Try (Rewrite_Set ''rooteq_simplify'' True)) @@ |
507 (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@ |
506 (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@ |
508 (Try (Rewrite_Set ''rooteq_simplify'' True))) e_e |
507 (Try (Rewrite_Set ''rooteq_simplify'' True))) e_e |
509 in SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met'']) |
508 in SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met'']) |
510 [BOOL e_e, REAL v_v])" |
509 [BOOL e_e, REAL v_v])" |
511 *) |
|
512 setup \<open>KEStore_Elems.add_mets |
510 setup \<open>KEStore_Elems.add_mets |
513 [Specify.prep_met thy "met_rooteq_norm" [] Celem.e_metID |
511 [Specify.prep_met thy "met_rooteq_norm" [] Celem.e_metID |
514 (["RootEq","norm_sq_root_equation"], |
512 (["RootEq","norm_sq_root_equation"], |
515 [("#Given" ,["equality e_e","solveFor v_v"]), |
513 [("#Given" ,["equality e_e","solveFor v_v"]), |
516 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
514 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
518 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
516 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
519 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]), |
517 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]), |
520 ("#Find" ,["solutions v_v'i'"])], |
518 ("#Find" ,["solutions v_v'i'"])], |
521 {rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule.e_rls, prls=RootEq_prls, calc=[], |
519 {rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule.e_rls, prls=RootEq_prls, calc=[], |
522 crls=RootEq_crls, errpats = [], nrls = norm_Poly}, |
520 crls=RootEq_crls, errpats = [], nrls = norm_Poly}, |
523 "Script Norm_sq_root_equation (e_e::bool) (v_v::real) = " ^ |
521 @{thm norm_sqrt_equ.simps} |
|
522 (*"Script Norm_sq_root_equation (e_e::bool) (v_v::real) = " ^ |
524 "(let e_e = ((Repeat(Try (Rewrite ''makex1_x'' False))) @@ " ^ |
523 "(let e_e = ((Repeat(Try (Rewrite ''makex1_x'' False))) @@ " ^ |
525 " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^ |
524 " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^ |
526 " (Try (Rewrite_Set ''rooteq_simplify'' True)) @@ " ^ |
525 " (Try (Rewrite_Set ''rooteq_simplify'' True)) @@ " ^ |
527 " (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@ " ^ |
526 " (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@ " ^ |
528 " (Try (Rewrite_Set ''rooteq_simplify'' True))) e_e " ^ |
527 " (Try (Rewrite_Set ''rooteq_simplify'' True))) e_e " ^ |
529 " in ((SubProblem (''RootEq'',[''univariate'',''equation''], " ^ |
528 " in ((SubProblem (''RootEq'',[''univariate'',''equation''], " ^ |
530 " [''no_met'']) [BOOL e_e, REAL v_v])))")] |
529 " [''no_met'']) [BOOL e_e, REAL v_v])))"*))] |
531 \<close> |
530 \<close> |
532 (*ok |
531 |
533 partial_function (tailrec) solve_sqrt_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
532 partial_function (tailrec) solve_sqrt_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
534 where |
533 where |
535 "solve_sqrt_equ e_e v_v = |
534 "solve_sqrt_equ e_e v_v = |
536 (let |
535 (let |
537 e_e = |
536 e_e = |
545 then SubProblem (''RootEq'', [''normalise'', ''rootX'', ''univariate'', ''equation''], |
544 then SubProblem (''RootEq'', [''normalise'', ''rootX'', ''univariate'', ''equation''], |
546 [''no_met'']) [BOOL e_e, REAL v_v] |
545 [''no_met'']) [BOOL e_e, REAL v_v] |
547 else SubProblem (''RootEq'',[''univariate'',''equation''], |
546 else SubProblem (''RootEq'',[''univariate'',''equation''], |
548 [''no_met'']) [BOOL e_e, REAL v_v]) |
547 [''no_met'']) [BOOL e_e, REAL v_v]) |
549 in Check_elementwise L_L {(v_v::real). Assumptions})" |
548 in Check_elementwise L_L {(v_v::real). Assumptions})" |
550 *) |
|
551 setup \<open>KEStore_Elems.add_mets |
549 setup \<open>KEStore_Elems.add_mets |
552 [Specify.prep_met thy "met_rooteq_sq" [] Celem.e_metID |
550 [Specify.prep_met thy "met_rooteq_sq" [] Celem.e_metID |
553 (["RootEq","solve_sq_root_equation"], |
551 (["RootEq","solve_sq_root_equation"], |
554 [("#Given" ,["equality e_e", "solveFor v_v"]), |
552 [("#Given" ,["equality e_e", "solveFor v_v"]), |
555 ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real)) & " ^ |
553 ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real)) & " ^ |
557 "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^ |
555 "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^ |
558 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]), |
556 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]), |
559 ("#Find" ,["solutions v_v'i'"])], |
557 ("#Find" ,["solutions v_v'i'"])], |
560 {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls, prls = RootEq_prls, calc = [], |
558 {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls, prls = RootEq_prls, calc = [], |
561 crls=RootEq_crls, errpats = [], nrls = norm_Poly}, |
559 crls=RootEq_crls, errpats = [], nrls = norm_Poly}, |
562 "Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^ |
560 @{thm solve_sqrt_equ.simps} |
|
561 (*"Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^ |
563 "(let e_e = " ^ |
562 "(let e_e = " ^ |
564 " ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''sqrt_isolate'' True)) @@ " ^ |
563 " ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''sqrt_isolate'' True)) @@ " ^ |
565 " (Try (Rewrite_Set ''rooteq_simplify'' True)) @@ " ^ |
564 " (Try (Rewrite_Set ''rooteq_simplify'' True)) @@ " ^ |
566 " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^ |
565 " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^ |
567 " (Try (Repeat (Rewrite_Set ''make_rooteq '' False))) @@ " ^ |
566 " (Try (Repeat (Rewrite_Set ''make_rooteq '' False))) @@ " ^ |
570 " (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^ |
569 " (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^ |
571 " then (SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], " ^ |
570 " then (SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], " ^ |
572 " [''no_met'']) [BOOL e_e, REAL v_v]) " ^ |
571 " [''no_met'']) [BOOL e_e, REAL v_v]) " ^ |
573 " else (SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met'']) " ^ |
572 " else (SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met'']) " ^ |
574 " [BOOL e_e, REAL v_v])) " ^ |
573 " [BOOL e_e, REAL v_v])) " ^ |
575 "in Check_elementwise L_L {(v_v::real). Assumptions})")] |
574 "in Check_elementwise L_L {(v_v::real). Assumptions})"*))] |
576 \<close> |
575 \<close> |
577 (*-- right 28.08.02 --*) |
576 (*-- right 28.08.02 --*) |
578 (*ok |
|
579 partial_function (tailrec) solve_sqrt_equ_right :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
577 partial_function (tailrec) solve_sqrt_equ_right :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
580 where "solve_sqrt_equ_right e_e v_v = |
578 where "solve_sqrt_equ_right e_e v_v = |
581 (let e_e = |
579 (let e_e = |
582 ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''r_sqrt_isolate'' False)) @@ |
580 ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''r_sqrt_isolate'' False)) @@ |
583 (Try (Rewrite_Set ''rooteq_simplify'' False)) @@ |
581 (Try (Rewrite_Set ''rooteq_simplify'' False)) @@ |
588 if (rhs e_e) is_sqrtTerm_in v_v |
586 if (rhs e_e) is_sqrtTerm_in v_v |
589 then SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], |
587 then SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], |
590 [''no_met'']) [BOOL e_e, REAL v_v] |
588 [''no_met'']) [BOOL e_e, REAL v_v] |
591 else SubProblem (''RootEq'',[''univariate'', ''equation''], |
589 else SubProblem (''RootEq'',[''univariate'', ''equation''], |
592 [''no_met'']) [BOOL e_e, REAL v_v])" |
590 [''no_met'']) [BOOL e_e, REAL v_v])" |
593 *) |
|
594 setup \<open>KEStore_Elems.add_mets |
591 setup \<open>KEStore_Elems.add_mets |
595 [Specify.prep_met thy "met_rooteq_sq_right" [] Celem.e_metID |
592 [Specify.prep_met thy "met_rooteq_sq_right" [] Celem.e_metID |
596 (["RootEq","solve_right_sq_root_equation"], |
593 (["RootEq","solve_right_sq_root_equation"], |
597 [("#Given" ,["equality e_e","solveFor v_v"]), |
594 [("#Given" ,["equality e_e","solveFor v_v"]), |
598 ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]), |
595 ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]), |
599 ("#Find" ,["solutions v_v'i'"])], |
596 ("#Find" ,["solutions v_v'i'"])], |
600 {rew_ord' = "termlessI", rls' = RootEq_erls, srls = Rule.e_rls, prls = RootEq_prls, calc = [], |
597 {rew_ord' = "termlessI", rls' = RootEq_erls, srls = Rule.e_rls, prls = RootEq_prls, calc = [], |
601 crls = RootEq_crls, errpats = [], nrls = norm_Poly}, |
598 crls = RootEq_crls, errpats = [], nrls = norm_Poly}, |
602 "Script Solve_right_sq_root_equation (e_e::bool) (v_v::real) = " ^ |
599 @{thm solve_sqrt_equ_right.simps} |
|
600 (*"Script Solve_right_sq_root_equation (e_e::bool) (v_v::real) = " ^ |
603 "(let e_e = " ^ |
601 "(let e_e = " ^ |
604 " ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''r_sqrt_isolate'' False)) @@ " ^ |
602 " ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''r_sqrt_isolate'' False)) @@ " ^ |
605 " (Try (Rewrite_Set ''rooteq_simplify'' False)) @@ " ^ |
603 " (Try (Rewrite_Set ''rooteq_simplify'' False)) @@ " ^ |
606 " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^ |
604 " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^ |
607 " (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@ " ^ |
605 " (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@ " ^ |
608 " (Try (Rewrite_Set ''rooteq_simplify'' False))) e_e " ^ |
606 " (Try (Rewrite_Set ''rooteq_simplify'' False))) e_e " ^ |
609 " in if ((rhs e_e) is_sqrtTerm_in v_v) " ^ |
607 " in if ((rhs e_e) is_sqrtTerm_in v_v) " ^ |
610 " then (SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], " ^ |
608 " then (SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], " ^ |
611 " [''no_met'']) [BOOL e_e, REAL v_v]) " ^ |
609 " [''no_met'']) [BOOL e_e, REAL v_v]) " ^ |
612 " else ((SubProblem (''RootEq'',[''univariate'',equation''], " ^ |
610 " else ((SubProblem (''RootEq'',[''univariate'',equation''], " ^ |
613 " [''no_met'']) [BOOL e_e, REAL v_v])))")] |
611 " [''no_met'']) [BOOL e_e, REAL v_v])))"*))] |
614 \<close> |
612 \<close> |
615 (*-- left 28.08.02 --*) |
613 (*-- left 28.08.02 --*) |
616 (*ok |
|
617 partial_function (tailrec) solve_sqrt_equ_left :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
614 partial_function (tailrec) solve_sqrt_equ_left :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
618 where |
615 where |
619 "solve_sqrt_equ_left e_e v_v = |
616 "solve_sqrt_equ_left e_e v_v = |
620 (let e_e = |
617 (let e_e = |
621 ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''l_sqrt_isolate'' False)) @@ |
618 ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''l_sqrt_isolate'' False)) @@ |
627 if (lhs e_e) is_sqrtTerm_in v_v |
624 if (lhs e_e) is_sqrtTerm_in v_v |
628 then SubProblem (''RootEq'', [''normalise'',''rootX'',''univariate'',''equation''], |
625 then SubProblem (''RootEq'', [''normalise'',''rootX'',''univariate'',''equation''], |
629 [''no_met'']) [BOOL e_e, REAL v_v] |
626 [''no_met'']) [BOOL e_e, REAL v_v] |
630 else SubProblem (''RootEq'',[''univariate'',''equation''], |
627 else SubProblem (''RootEq'',[''univariate'',''equation''], |
631 [''no_met'']) [BOOL e_e, REAL v_v])" |
628 [''no_met'']) [BOOL e_e, REAL v_v])" |
632 *) |
|
633 setup \<open>KEStore_Elems.add_mets |
629 setup \<open>KEStore_Elems.add_mets |
634 [Specify.prep_met thy "met_rooteq_sq_left" [] Celem.e_metID |
630 [Specify.prep_met thy "met_rooteq_sq_left" [] Celem.e_metID |
635 (["RootEq","solve_left_sq_root_equation"], |
631 (["RootEq","solve_left_sq_root_equation"], |
636 [("#Given" ,["equality e_e","solveFor v_v"]), |
632 [("#Given" ,["equality e_e","solveFor v_v"]), |
637 ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]), |
633 ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]), |
638 ("#Find" ,["solutions v_v'i'"])], |
634 ("#Find" ,["solutions v_v'i'"])], |
639 {rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule.e_rls, prls=RootEq_prls, calc=[], |
635 {rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule.e_rls, prls=RootEq_prls, calc=[], |
640 crls=RootEq_crls, errpats = [], nrls = norm_Poly}, |
636 crls=RootEq_crls, errpats = [], nrls = norm_Poly}, |
641 "Script Solve_left_sq_root_equation (e_e::bool) (v_v::real) = " ^ |
637 @{thm solve_sqrt_equ_left.simps} |
|
638 (*"Script Solve_left_sq_root_equation (e_e::bool) (v_v::real) = " ^ |
642 "(let e_e = " ^ |
639 "(let e_e = " ^ |
643 " ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''l_sqrt_isolate'' False)) @@ " ^ |
640 " ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''l_sqrt_isolate'' False)) @@ " ^ |
644 " (Try (Rewrite_Set ''rooteq_simplify'' False)) @@ " ^ |
641 " (Try (Rewrite_Set ''rooteq_simplify'' False)) @@ " ^ |
645 " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^ |
642 " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^ |
646 " (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@ " ^ |
643 " (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@ " ^ |
647 " (Try (Rewrite_Set ''rooteq_simplify'' False))) e_e " ^ |
644 " (Try (Rewrite_Set ''rooteq_simplify'' False))) e_e " ^ |
648 " in if ((lhs e_e) is_sqrtTerm_in v_v) " ^ |
645 " in if ((lhs e_e) is_sqrtTerm_in v_v) " ^ |
649 " then (SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], " ^ |
646 " then (SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], " ^ |
650 " [''no_met'']) [BOOL e_e, REAL v_v]) " ^ |
647 " [''no_met'']) [BOOL e_e, REAL v_v]) " ^ |
651 " else ((SubProblem (''RootEq'',[''univariate'',''equation''], " ^ |
648 " else ((SubProblem (''RootEq'',[''univariate'',''equation''], " ^ |
652 " [''no_met'']) [BOOL e_e, REAL v_v])))")] |
649 " [''no_met'']) [BOOL e_e, REAL v_v])))"*))] |
653 \<close> |
650 \<close> |
654 ML \<open> |
651 ML \<open> |
655 \<close> ML \<open> |
652 \<close> ML \<open> |
656 \<close> |
653 \<close> |
657 end |
654 end |