1.1 --- a/test/Tools/isac/Knowledge/polyeq-2.sml Thu Jul 28 11:43:27 2022 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-2.sml Sat Jul 30 16:47:45 2022 +0200
1.3 @@ -215,11 +215,12 @@
1.4 "----------- rls make_polynomial_in ------------------------------";
1.5 "----------- rls make_polynomial_in ------------------------------";
1.6 val thy = @{theory};
1.7 +val ctxt = @{context};
1.8 (*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
1.9 (*WN.19.3.03 ---v-*)
1.10 (*3(b)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "R1");
1.11 val t = TermC.str2term "- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0";
1.12 -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.13 +val SOME (t',_) = rewrite_set_inst_ ctxt false [(bdv,v)] make_polynomial_in t;
1.14 if UnparseC.term t' = "- 1 * R * R2 + R2 * R1 + - 1 * R * R1 = 0" then ()
1.15 else error "make_polynomial_in (- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0)";
1.16 "- 1 * R * R2 + (R2 + - 1 * R) * R1 = 0";
1.17 @@ -227,21 +228,21 @@
1.18
1.19 (*3(c)*)val (bdv,v) = (TermC.str2term "bdv", TermC.str2term "p");
1.20 val t = TermC.str2term "y \<up> 2 + - 2 * (x * p) = 0";
1.21 -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.22 +val SOME (t',_) = rewrite_set_inst_ ctxt false [(bdv,v)] make_polynomial_in t;
1.23 if UnparseC.term t' = "y \<up> 2 + - 2 * x * p = 0" then ()
1.24 else error "make_polynomial_in (y \<up> 2 + - 2 * (x * p) = 0)";
1.25
1.26 (*3(d)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "x2");
1.27 val t = TermC.str2term
1.28 "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.29 -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.30 +val SOME (t',_) = rewrite_set_inst_ ctxt false [(bdv,v)] make_polynomial_in t;
1.31 if UnparseC.term t' =
1.32 "A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + - 1 * x1 * y2 * (1 / 2) +\n- 1 * x3 * y1 * (1 / 2) +\ny1 * (1 / 2) * x2 +\n- 1 * y3 * (1 / 2) * x2 =\n0"
1.33 then ()
1.34 else error "make_polynomial_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + - 1...";
1.35 "A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + - x1 * y2 * (1 / 2) + - x3 * y1 * (1 / 2) + (y1 * (1 / 2) + - y3 * (1 / 2)) * x2 = 0";
1.36
1.37 -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t;
1.38 +val SOME (t',_) = rewrite_set_inst_ ctxt false [(bdv,v)] make_ratpoly_in t;
1.39 if UnparseC.term t' =
1.40 "A / 1 + x1 * y3 / 2 + x3 * y2 / 2 + - 1 * x1 * y2 / 2 + - 1 * x3 * y1 / 2 +\ny1 * x2 / 2 +\n- 1 * y3 * x2 / 2 =\n0"
1.41 then ()
1.42 @@ -251,13 +252,11 @@
1.43 (*3(e)*)val (bdv,v) = (TermC.str2term "bdv", TermC.str2term "a");
1.44 val t = TermC.str2term
1.45 "A \<up> 2 + c \<up> 2 * (c / d) \<up> 2 + (-4 * (c / d) \<up> 2) * a \<up> 2 = 0";
1.46 -val NONE = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.47 +val NONE = rewrite_set_inst_ ctxt false [(bdv,v)] make_polynomial_in t;
1.48 (* the invisible parentheses are as expected *)
1.49
1.50 val t = TermC.str2term "(x + 1) * (x + 2) - (3 * x - 2) \<up> 2 - ((2 * x - 1) \<up> 2 + (3 * x - 1) * (x + 1)) = 0";
1.51 -Rewrite.trace_on:= false; (*true false*)
1.52 -rewrite_set_ thy false expand_binoms t;
1.53 -Rewrite.trace_on:=false; (*true false*)
1.54 +rewrite_set_ ctxt false expand_binoms t;
1.55
1.56
1.57 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1.58 @@ -281,21 +280,21 @@
1.59 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
1.60 val t = TermC.str2term "-6 * x + 5 * x \<up> 2 = (0::real)";
1.61 val subst = [(TermC.str2term "(bdv::real)", TermC.str2term "(x::real)")];
1.62 -val SOME (t''''', _) = rewrite_set_inst_ thy true subst d2_polyeq_bdv_only_simplify t;
1.63 +val SOME (t''''', _) = rewrite_set_inst_ ctxt true subst d2_polyeq_bdv_only_simplify t;
1.64 (* steps in rls d2_polyeq_bdv_only_simplify:*)
1.65
1.66 (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1", "")) --> x * (-6 + 5 * x) = 0*)
1.67 t |> UnparseC.term; t |> TermC.atomty;
1.68 val thm = @{thm d2_prescind1};
1.69 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
1.70 -val SOME (t', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t; UnparseC.term t';
1.71 +val SOME (t', _) = rewrite_inst_ ctxt e_rew_ord Rule_Set.empty true subst thm t; UnparseC.term t';
1.72
1.73 (*x * (-6 + 5 * x) = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1", ""))
1.74 --> x = 0 | -6 + 5 * x = 0*)
1.75 t' |> UnparseC.term; t' |> TermC.atomty;
1.76 val thm = @{thm d2_reduce_equation1};
1.77 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
1.78 -val SOME (t'', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t'; UnparseC.term t'';
1.79 +val SOME (t'', _) = rewrite_inst_ ctxt e_rew_ord Rule_Set.empty true subst thm t'; UnparseC.term t'';
1.80 (* NONE with d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
1.81 instead d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"
1.82 *)