472 ("#Find" ,["solutions v_v'i'"])], |
472 ("#Find" ,["solutions v_v'i'"])], |
473 RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq", "norm_sq_root_equation"]]))]\<close> |
473 RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq", "norm_sq_root_equation"]]))]\<close> |
474 |
474 |
475 subsection \<open>methods\<close> |
475 subsection \<open>methods\<close> |
476 setup \<open>KEStore_Elems.add_mets |
476 setup \<open>KEStore_Elems.add_mets |
477 [Method.prep_input thy "met_rooteq" [] Method.id_empty |
477 [MethodC.prep_input thy "met_rooteq" [] MethodC.id_empty |
478 (["RootEq"], [], |
478 (["RootEq"], [], |
479 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, |
479 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, |
480 crls=RootEq_crls, errpats = [], nrls = norm_Poly}, @{thm refl})] |
480 crls=RootEq_crls, errpats = [], nrls = norm_Poly}, @{thm refl})] |
481 \<close> |
481 \<close> |
482 (*-- normalise 20.10.02 --*) |
482 (*-- normalise 20.10.02 --*) |
493 ) e_e |
493 ) e_e |
494 in |
494 in |
495 SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met'']) |
495 SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met'']) |
496 [BOOL e_e, REAL v_v])" |
496 [BOOL e_e, REAL v_v])" |
497 setup \<open>KEStore_Elems.add_mets |
497 setup \<open>KEStore_Elems.add_mets |
498 [Method.prep_input thy "met_rooteq_norm" [] Method.id_empty |
498 [MethodC.prep_input thy "met_rooteq_norm" [] MethodC.id_empty |
499 (["RootEq", "norm_sq_root_equation"], |
499 (["RootEq", "norm_sq_root_equation"], |
500 [("#Given" ,["equality e_e", "solveFor v_v"]), |
500 [("#Given" ,["equality e_e", "solveFor v_v"]), |
501 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
501 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
502 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^ |
502 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^ |
503 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
503 "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ |
526 else |
526 else |
527 SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met'']) |
527 SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met'']) |
528 [BOOL e_e, REAL v_v]) |
528 [BOOL e_e, REAL v_v]) |
529 in Check_elementwise L_L {(v_v::real). Assumptions})" |
529 in Check_elementwise L_L {(v_v::real). Assumptions})" |
530 setup \<open>KEStore_Elems.add_mets |
530 setup \<open>KEStore_Elems.add_mets |
531 [Method.prep_input thy "met_rooteq_sq" [] Method.id_empty |
531 [MethodC.prep_input thy "met_rooteq_sq" [] MethodC.id_empty |
532 (["RootEq", "solve_sq_root_equation"], |
532 (["RootEq", "solve_sq_root_equation"], |
533 [("#Given" ,["equality e_e", "solveFor v_v"]), |
533 [("#Given" ,["equality e_e", "solveFor v_v"]), |
534 ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real)) & " ^ |
534 ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real)) & " ^ |
535 " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^ |
535 " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^ |
536 "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^ |
536 "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^ |
558 [BOOL e_e, REAL v_v] |
558 [BOOL e_e, REAL v_v] |
559 else |
559 else |
560 SubProblem (''RootEq'',[''univariate'', ''equation''], [''no_met'']) |
560 SubProblem (''RootEq'',[''univariate'', ''equation''], [''no_met'']) |
561 [BOOL e_e, REAL v_v])" |
561 [BOOL e_e, REAL v_v])" |
562 setup \<open>KEStore_Elems.add_mets |
562 setup \<open>KEStore_Elems.add_mets |
563 [Method.prep_input thy "met_rooteq_sq_right" [] Method.id_empty |
563 [MethodC.prep_input thy "met_rooteq_sq_right" [] MethodC.id_empty |
564 (["RootEq", "solve_right_sq_root_equation"], |
564 (["RootEq", "solve_right_sq_root_equation"], |
565 [("#Given" ,["equality e_e", "solveFor v_v"]), |
565 [("#Given" ,["equality e_e", "solveFor v_v"]), |
566 ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]), |
566 ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]), |
567 ("#Find" ,["solutions v_v'i'"])], |
567 ("#Find" ,["solutions v_v'i'"])], |
568 {rew_ord' = "termlessI", rls' = RootEq_erls, srls = Rule_Set.empty, prls = RootEq_prls, calc = [], |
568 {rew_ord' = "termlessI", rls' = RootEq_erls, srls = Rule_Set.empty, prls = RootEq_prls, calc = [], |
587 [BOOL e_e, REAL v_v] |
587 [BOOL e_e, REAL v_v] |
588 else |
588 else |
589 SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met'']) |
589 SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met'']) |
590 [BOOL e_e, REAL v_v])" |
590 [BOOL e_e, REAL v_v])" |
591 setup \<open>KEStore_Elems.add_mets |
591 setup \<open>KEStore_Elems.add_mets |
592 [Method.prep_input thy "met_rooteq_sq_left" [] Method.id_empty |
592 [MethodC.prep_input thy "met_rooteq_sq_left" [] MethodC.id_empty |
593 (["RootEq", "solve_left_sq_root_equation"], |
593 (["RootEq", "solve_left_sq_root_equation"], |
594 [("#Given" ,["equality e_e", "solveFor v_v"]), |
594 [("#Given" ,["equality e_e", "solveFor v_v"]), |
595 ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]), |
595 ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]), |
596 ("#Find" ,["solutions v_v'i'"])], |
596 ("#Find" ,["solutions v_v'i'"])], |
597 {rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule_Set.empty, prls=RootEq_prls, calc=[], |
597 {rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule_Set.empty, prls=RootEq_prls, calc=[], |