1.1 --- a/test/Tools/isac/Knowledge/polyeq-2.sml Mon Apr 19 11:45:43 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-2.sml Mon Apr 19 15:02:00 2021 +0200
1.3 @@ -214,22 +214,22 @@
1.4 "----------- rls make_polynomial_in ------------------------------";
1.5 (*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
1.6 (*WN.19.3.03 ---v-*)
1.7 -(*3(b)*)val (bdv,v) = (str2term "''bdv''", str2term "R1");
1.8 -val t = str2term "-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0";
1.9 +(*3(b)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "R1");
1.10 +val t = TermC.str2term "-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0";
1.11 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.12 if UnparseC.term t' = "-1 * R * R2 + R2 * R1 + -1 * R * R1 = 0" then ()
1.13 else error "make_polynomial_in (-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0)";
1.14 "-1 * R * R2 + (R2 + -1 * R) * R1 = 0";
1.15 (*WN.19.3.03 ---^-*)
1.16
1.17 -(*3(c)*)val (bdv,v) = (str2term "bdv", str2term "p");
1.18 -val t = str2term "y ^^^ 2 + -2 * (x * p) = 0";
1.19 +(*3(c)*)val (bdv,v) = (TermC.str2term "bdv", TermC.str2term "p");
1.20 +val t = TermC.str2term "y ^^^ 2 + -2 * (x * p) = 0";
1.21 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.22 if UnparseC.term t' = "y ^^^ 2 + -2 * x * p = 0" then ()
1.23 else error "make_polynomial_in (y ^^^ 2 + -2 * (x * p) = 0)";
1.24
1.25 -(*3(d)*)val (bdv,v) = (str2term "''bdv''", str2term "x2");
1.26 -val t = str2term
1.27 +(*3(d)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "x2");
1.28 +val t = TermC.str2term
1.29 "A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1 * (x1 * (y2 * (1 / 2))) + -1 * (x3 * (y1 * (1 / 2 ))) + y1 * (1 / 2 * x2) + -1 * (y3 * (1 / 2 * x2)) = 0";
1.30 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.31 if UnparseC.term t' =
1.32 @@ -245,13 +245,13 @@
1.33 else error "make_ratpoly_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1...";
1.34 "A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + -1 * x1 * y2 * (1 / 2) + -1 * x3 * y1 * (1 / 2) + (y1 * (1 / 2) + -1 * y3 * (1 / 2)) * x2 = 0";
1.35
1.36 -(*3(e)*)val (bdv,v) = (str2term "bdv", str2term "a");
1.37 -val t = str2term
1.38 +(*3(e)*)val (bdv,v) = (TermC.str2term "bdv", TermC.str2term "a");
1.39 +val t = TermC.str2term
1.40 "A ^^^ 2 + c ^^^ 2 * (c / d) ^^^ 2 + (-4 * (c / d) ^^^ 2) * a ^^^ 2 = 0";
1.41 val NONE = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.42 (* the invisible parentheses are as expected *)
1.43
1.44 -val t = str2term "(x + 1) * (x + 2) - (3 * x - 2) ^^^ 2 - ((2 * x - 1) ^^^ 2 + (3 * x - 1) * (x + 1)) = 0";
1.45 +val t = TermC.str2term "(x + 1) * (x + 2) - (3 * x - 2) ^^^ 2 - ((2 * x - 1) ^^^ 2 + (3 * x - 1) * (x + 1)) = 0";
1.46 Rewrite.trace_on:=(*true*)false;
1.47 rewrite_set_ thy false expand_binoms t;
1.48 Rewrite.trace_on:=false;
1.49 @@ -276,22 +276,22 @@
1.50 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
1.51 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
1.52 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
1.53 -val t = str2term "-6 * x + 5 * x ^^^ 2 = (0::real)";
1.54 -val subst = [(str2term "(bdv::real)", str2term "(x::real)")];
1.55 +val t = TermC.str2term "-6 * x + 5 * x ^^^ 2 = (0::real)";
1.56 +val subst = [(TermC.str2term "(bdv::real)", TermC.str2term "(x::real)")];
1.57 val SOME (t''''', _) = rewrite_set_inst_ thy true subst d2_polyeq_bdv_only_simplify t;
1.58 (* steps in rls d2_polyeq_bdv_only_simplify:*)
1.59
1.60 (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1", "")) --> x * (-6 + 5 * x) = 0*)
1.61 -t |> UnparseC.term; t |> atomty;
1.62 +t |> UnparseC.term; t |> TermC.atomty;
1.63 val thm = ThmC.numerals_to_Free @{thm d2_prescind1};
1.64 -thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> atomty;
1.65 +thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
1.66 val SOME (t', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t; UnparseC.term t';
1.67
1.68 (*x * (-6 + 5 * x) = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1", ""))
1.69 --> x = 0 | -6 + 5 * x = 0*)
1.70 -t' |> UnparseC.term; t' |> atomty;
1.71 +t' |> UnparseC.term; t' |> TermC.atomty;
1.72 val thm = ThmC.numerals_to_Free @{thm d2_reduce_equation1};
1.73 -thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> atomty;
1.74 +thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
1.75 val SOME (t'', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t'; UnparseC.term t'';
1.76 (* NONE with d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
1.77 instead d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"