1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Fri Aug 06 18:27:05 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Sun Aug 08 15:21:33 2021 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4                 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
     1.5    | is_ratpolyexp (Const (\<^const_name>\<open>divide\<close>,_) $ t1 $ t2) = 
     1.6                 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
     1.7 -  | is_ratpolyexp _ = false;
     1.8 +  | is_ratpolyexp t = if TermC.is_num t then true else false;
     1.9  
    1.10  (*("is_ratpolyexp", ("Rational.is_ratpolyexp", eval_is_ratpolyexp ""))*)
    1.11  fun eval_is_ratpolyexp (thmid:string) _ 

     2.1 --- a/test/Tools/isac/Knowledge/rational-1.sml	Fri Aug 06 18:27:05 2021 +0200
     2.2 +++ b/test/Tools/isac/Knowledge/rational-1.sml	Sun Aug 08 15:21:33 2021 +0200
     2.3 @@ -11,6 +11,7 @@
     2.4  "-----------------------------------------------------------------------------------------------";
     2.5  "-------- fun poly_of_term ---------------------------------------------------------------------";
     2.6  "-------- fun is_poly --------------------------------------------------------------------------";
     2.7 +"-------- fun is_ratpolyexp --------------------------------------------------------------------";
     2.8  "-------- fun term_of_poly ---------------------------------------------------------------------";
     2.9  "-------- fun cancel_p special cases -----------------------------------------------------------";
    2.10  "-------- complex examples: rls norm_Rational --------------------------------------------------";
    2.11 @@ -103,6 +104,20 @@
    2.12  if not (is_poly (TermC.str2term "2 * (x \<up> 3 * y \<up> 4 * z \<up> 6 + 7) * y \<up> 8 + 1"))
    2.13  then () else error "is_poly 2 changed";
    2.14  
    2.15 +"-------- fun is_ratpolyexp --------------------------------------------------------------------";
    2.16 +"-------- fun is_ratpolyexp --------------------------------------------------------------------";
    2.17 +"-------- fun is_ratpolyexp --------------------------------------------------------------------";
    2.18 +if is_ratpolyexp @{term "14 * x * y / (x * y)"}
    2.19 +then () else error "is_ratpolyexp (14 * x * y / (x * y)) CHANGED";
    2.20 +if is_ratpolyexp @{term "2 * (x \<up> 3 * y \<up> 4 * z \<up> 6 + 7) * y \<up> 8 + 1"}
    2.21 +then () else error "is_ratpolyexp (2 * (x \<up> 3 * y \<up> 4 * z \<up> 6 + 7) * y \<up> 8 + 1) CHANGED";
    2.22 +
    2.23 +if is_ratpolyexp @{term "((sin x) \<up> 2 - (cos x) \<up> 2)/ ((sin x)+ (cos x))"}
    2.24 +then error "is_ratpolyexp (((sin x) \<up> 2 - (cos x) \<up> 2)/ ((sin x)+ (cos x)) CHANGED" else ();
    2.25 +if is_ratpolyexp @{term "1 + sqrt x + sqrt y"}
    2.26 +then error "is_ratpolyexp (1 + sqrt x + sqrt y) CHANGED" else ();
    2.27 +
    2.28 +
    2.29  "-------- fun term_of_poly ---------------------------------------------------------------------";
    2.30  "-------- fun term_of_poly ---------------------------------------------------------------------";
    2.31  "-------- fun term_of_poly ---------------------------------------------------------------------";

     3.1 --- a/test/Tools/isac/Knowledge/simplify.sml	Fri Aug 06 18:27:05 2021 +0200
     3.2 +++ b/test/Tools/isac/Knowledge/simplify.sml	Sun Aug 08 15:21:33 2021 +0200
     3.3 @@ -1,5 +1,5 @@
     3.4 -(* tests on simplification
     3.5 -   author: Walther Neuper 061019
     3.6 +(* Title: \<open>\<close>
     3.7 +   Author: Walther Neuper 061019
     3.8     (c) due to copyright terms
     3.9  *)
    3.10  
    3.11 @@ -39,13 +39,81 @@
    3.12  Iterator 1;
    3.13  moveActiveRoot 1;
    3.14  autoCalculate 1 CompleteCalcHead;
    3.15 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; 
    3.16 -(*[
    3.17 +val ((pt,p),_) = get_calc 1; 
    3.18 +Test_Tool.show_pt pt; (*[
    3.19  (([], Frm), Simplify (14 * x * y / (x * y)))] *)
    3.20  ME_Misc.pt_extract (pt, p); (*determines SOME (Apply_Method ["simplification", "of_rationals"])*)
    3.21  
    3.22 -autoCalculate 1 (Steps 1);
    3.23 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
    3.24 +(*/------------------- step into autoCalculate 1 (Steps 1) \<longrightarrow> Apply_Method ----------------\*)
    3.25 +"~~~~~ fun autoCalculate , args:"; val (cI, auto) = (1, Steps 1);
    3.26 +     val pold = get_pos cI 1
    3.27 +
    3.28 +(** )val ("ok", [], (_, ([], Met))) =    (*case*)                                      ( *isa*)
    3.29 +(**)val ("ok", [], (_, ([1], Frm))) =   (*case*)                                     (*isa2*)
    3.30 +Math_Engine.autocalc [] pold (get_calc cI) auto (*of*);
    3.31 +"~~~~~  fun autocalc , args:"; val (c, ip, cs, (Solve.Steps s)) = ([], pold, (get_calc cI), auto);
    3.32 +    (*if*) s <= 1 (*then*);
    3.33 +
    3.34 +(** )  val ("ok", (                                                                    (*isa*)
    3.35 +        [(Specify_Method ["simplification", "of_rationals"], _, (([], Met), (Uistate, _)))],
    3.36 +           [], (_, ([], Met)))) = ( **)
    3.37 +(**)  val ("ok", (                                                                      (*isa2*)
    3.38 +        [(Apply_Method ["simplification", "of_rationals"], _, (([1], Frm), (pstate, _)))],
    3.39 +           [], (_, ([1], Frm)))) = (**)
    3.40 +      Step.do_next ip cs;
    3.41 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (ip, cs);
    3.42 +  (*if*) Pos.on_calc_end ip (*else*);
    3.43 +      val ("Rational", probl_id as ["rational", "simplification"], ["simplification", "of_rationals"]) =
    3.44 +  Calc.references (pt, p);                                                        (*isa == isa2*)
    3.45 +val _ =
    3.46 +      (*case*) tacis (*of*);
    3.47 +        (*if*) probl_id = Problem.id_empty (*else*);
    3.48 +
    3.49 +(** )  val ("ok", (                                                                     (*isa*)
    3.50 +        [(Specify_Method ["simplification", "of_rationals"], _, (([], Met), (Uistate, _)))],
    3.51 +           [], (_, ([], Met)))) = ( **)
    3.52 +(**)  val ("ok", (                                                                      (*isa2*)
    3.53 +        [(Apply_Method ["simplification", "of_rationals"], _, (([1], Frm), (pstate, _)))],
    3.54 +           [], (_, ([1], Frm)))) = (**)
    3.55 +           switch_specify_solve p_ (pt, ip);
    3.56 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
    3.57 +      (*if*) Pos.on_specification ([], state_pos) (*then*);
    3.58 +
    3.59 +(** )  val ("ok", (                                                                     (*isa*)
    3.60 +        [(Specify_Method ["simplification", "of_rationals"], _, (([], Met), (Uistate, _)))],
    3.61 +           [], (_, ([], Met)))) = ( **)
    3.62 +(**)  val ("ok", (                                                                      (*isa2*)
    3.63 +        [(Apply_Method ["simplification", "of_rationals"], _, (([1], Frm), (pstate, _)))],
    3.64 +           [], (_, ([1], Frm)))) = (**)
    3.65 +           specify_do_next (pt, input_pos);
    3.66 +"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
    3.67 +    val (_, (p_', tac)) = Specify.find_next_step ptp
    3.68 +
    3.69 +(** ) val (_, (Met, Specify_Method ["simplification", "of_rationals"])) =             ( *isa*)
    3.70 +(**) val (_, (Met, Apply_Method ["simplification", "of_rationals"])) =               (*isa2*)
    3.71 +   Specify.find_next_step ptp;
    3.72 +"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
    3.73 +    val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
    3.74 +      spec = refs, ...} = Calc.specify_data (pt, pos);
    3.75 +      (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
    3.76 +        (*if*) p_ = Pos.Pbl (*else*);
    3.77 +
    3.78 +(** ) val (_, (Met, Specify_Method ["simplification", "of_rationals"])) =             ( *isa*)
    3.79 +(**) val (_, (Met, Apply_Method ["simplification", "of_rationals"])) =               (*isa2*)
    3.80 +           for_method oris (o_refs, refs) (pbl, met);
    3.81 +"~~~~~ fun for_method , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
    3.82 +  (oris, (o_refs, refs), (pbl, met));
    3.83 +    val cmI = if mI = MethodC.id_empty then mI' else mI;
    3.84 +    val {ppc = mpc, prls, pre, ...} = MethodC.from_store cmI;    (*..MethodC ?*)
    3.85 +
    3.86 +(*+*)Rewrite.trace_on := false; (*false true*)
    3.87 +(** ) val (preok as false, _) = Pre_Conds.check prls pre pbl 0;                       ( *isa*)
    3.88 +(**) val (preok as true, _) = Pre_Conds.check prls pre pbl 0;                        (*isa2*)
    3.89 + (*####  eval asms: "14 * x * y / (x * y) is_ratpolyexp = False"                       (*isa*)
    3.90 +                                                         True                        ( *isa2*)
    3.91 +(*\------------------- step into autoCalculate 1 (Steps 1) \<longrightarrow> Apply_Method ----------------/*)
    3.92 +val ((pt,p),_) = get_calc 1;  
    3.93 +Test_Tool.show_pt pt;
    3.94  (*[
    3.95  (([], Frm), Simplify (14 * x * y / (x * y))),
    3.96  (([1], Frm), 14 * x * y / (x * y))] *)
    3.97 @@ -73,10 +141,7 @@
    3.98  (([1], Res), 14),
    3.99  (([], Res), 14)] *)
   3.100  val Form res = (#1 o ME_Misc.pt_extract) (pt, ([],Res));
   3.101 -p;
   3.102 -UnparseC.term res = "??.empty"; (*TOODOO*)
   3.103 -(** )
   3.104 +
   3.105  if p = ([], Res) andalso UnparseC.term res = "14" then ()
   3.106  else error "simplify.sml: append inform with final result changed";
   3.107 -( **)
   3.108