src/Tools/isac/Knowledge/RootEq.thy
branchisac-update-Isa09-2
changeset 37987 bf83d30839c7
parent 37986 7b1d2366c191
child 37991 028442673981
equal deleted inserted replaced
37986:7b1d2366c191 37987:bf83d30839c7
   540     "(let e_e = ((Repeat(Try (Rewrite     makex1_x            False))) @@  " ^
   540     "(let e_e = ((Repeat(Try (Rewrite     makex1_x            False))) @@  " ^
   541     "           (Try (Repeat (Rewrite_Set expand_rootbinoms  False))) @@  " ^ 
   541     "           (Try (Repeat (Rewrite_Set expand_rootbinoms  False))) @@  " ^ 
   542     "           (Try (Rewrite_Set rooteq_simplify              True)) @@  " ^ 
   542     "           (Try (Rewrite_Set rooteq_simplify              True)) @@  " ^ 
   543     "           (Try (Repeat (Rewrite_Set make_rooteq        False))) @@  " ^
   543     "           (Try (Repeat (Rewrite_Set make_rooteq        False))) @@  " ^
   544     "           (Try (Rewrite_Set rooteq_simplify              True))) e_e " ^
   544     "           (Try (Rewrite_Set rooteq_simplify              True))) e_e " ^
   545     " in ((SubProblem (RootEq_',[univariate,equation],                     " ^
   545     " in ((SubProblem (RootEq',[univariate,equation],                     " ^
   546     "      [no_met]) [BOOL e_e, REAL v_v])))"
   546     "      [no_met]) [BOOL e_e, REAL v_v])))"
   547    ));
   547    ));
   548 
   548 
   549 *}
   549 *}
   550 
   550 
   569 "   (Try (Repeat (Rewrite_Set expand_rootbinoms         False))) @@      " ^
   569 "   (Try (Repeat (Rewrite_Set expand_rootbinoms         False))) @@      " ^
   570 "   (Try (Repeat (Rewrite_Set make_rooteq               False))) @@      " ^
   570 "   (Try (Repeat (Rewrite_Set make_rooteq               False))) @@      " ^
   571 "   (Try (Rewrite_Set rooteq_simplify                    True)) ) e_e;   " ^
   571 "   (Try (Rewrite_Set rooteq_simplify                    True)) ) e_e;   " ^
   572 " (L_L::bool list) =                                                     " ^
   572 " (L_L::bool list) =                                                     " ^
   573 "   (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^
   573 "   (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^
   574 "    then (SubProblem (RootEq_',[normalize,root',univariate,equation],   " ^
   574 "    then (SubProblem (RootEq',[normalize,root',univariate,equation],   " ^
   575 "                      [no_met]) [BOOL e_e, REAL v_v])                   " ^
   575 "                      [no_met]) [BOOL e_e, REAL v_v])                   " ^
   576 "    else (SubProblem (RootEq_',[univariate,equation], [no_met])         " ^
   576 "    else (SubProblem (RootEq',[univariate,equation], [no_met])         " ^
   577 "                     [BOOL e_e, REAL v_v]))                             " ^
   577 "                     [BOOL e_e, REAL v_v]))                             " ^
   578 "in Check_elementwise L_L {(v_v::real). Assumptions})"
   578 "in Check_elementwise L_L {(v_v::real). Assumptions})"
   579  ));
   579  ));
   580 *}
   580 *}
   581 
   581 
   596    "    (Try (Rewrite_Set                       rooteq_simplify False)) @@   " ^
   596    "    (Try (Rewrite_Set                       rooteq_simplify False)) @@   " ^
   597    "    (Try (Repeat (Rewrite_Set expand_rootbinoms            False))) @@   " ^
   597    "    (Try (Repeat (Rewrite_Set expand_rootbinoms            False))) @@   " ^
   598    "    (Try (Repeat (Rewrite_Set make_rooteq                  False))) @@   " ^
   598    "    (Try (Repeat (Rewrite_Set make_rooteq                  False))) @@   " ^
   599    "    (Try (Rewrite_Set rooteq_simplify                       False))) e_e " ^
   599    "    (Try (Rewrite_Set rooteq_simplify                       False))) e_e " ^
   600    " in if ((rhs e_e) is_sqrtTerm_in v_v)                                    " ^
   600    " in if ((rhs e_e) is_sqrtTerm_in v_v)                                    " ^
   601    " then (SubProblem (RootEq_',[normalize,root',univariate,equation],       " ^
   601    " then (SubProblem (RootEq',[normalize,root',univariate,equation],       " ^
   602    "       [no_met]) [BOOL e_e, REAL v_v])                                   " ^
   602    "       [no_met]) [BOOL e_e, REAL v_v])                                   " ^
   603    " else ((SubProblem (RootEq_',[univariate,equation],                      " ^
   603    " else ((SubProblem (RootEq',[univariate,equation],                      " ^
   604    "        [no_met]) [BOOL e_e, REAL v_v])))"
   604    "        [no_met]) [BOOL e_e, REAL v_v])))"
   605  ));
   605  ));
   606 val --------------------------------------------------+++ = "33333";
   606 val --------------------------------------------------+++ = "33333";
   607 
   607 
   608 (*-- left 28.08.02 --*)
   608 (*-- left 28.08.02 --*)
   625     "  (Try (Rewrite_Set                       rooteq_simplify False)) @@  " ^
   625     "  (Try (Rewrite_Set                       rooteq_simplify False)) @@  " ^
   626     "  (Try (Repeat (Rewrite_Set expand_rootbinoms            False))) @@  " ^
   626     "  (Try (Repeat (Rewrite_Set expand_rootbinoms            False))) @@  " ^
   627     "  (Try (Repeat (Rewrite_Set make_rooteq                  False))) @@  " ^
   627     "  (Try (Repeat (Rewrite_Set make_rooteq                  False))) @@  " ^
   628     "  (Try (Rewrite_Set rooteq_simplify                       False))) e_e " ^
   628     "  (Try (Rewrite_Set rooteq_simplify                       False))) e_e " ^
   629     " in if ((lhs e_e) is_sqrtTerm_in v_v)                                   " ^ 
   629     " in if ((lhs e_e) is_sqrtTerm_in v_v)                                   " ^ 
   630     " then (SubProblem (RootEq_',[normalize,root',univariate,equation],      " ^
   630     " then (SubProblem (RootEq',[normalize,root',univariate,equation],      " ^
   631     "       [no_met]) [BOOL e_e, REAL v_v])                                " ^
   631     "       [no_met]) [BOOL e_e, REAL v_v])                                " ^
   632     " else ((SubProblem (RootEq_',[univariate,equation],                    " ^
   632     " else ((SubProblem (RootEq',[univariate,equation],                    " ^
   633     "        [no_met]) [BOOL e_e, REAL v_v])))"
   633     "        [no_met]) [BOOL e_e, REAL v_v])))"
   634    ));
   634    ));
   635 val --------------------------------------------------++++ = "44444";
   635 val --------------------------------------------------++++ = "44444";
   636 
   636 
   637 calclist':= overwritel (!calclist', 
   637 calclist':= overwritel (!calclist',