1.1 --- a/test/Tools/isac/Knowledge/polyeq-2.sml Tue May 19 12:33:35 2020 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-2.sml Wed May 20 12:52:09 2020 +0200
1.3 @@ -25,10 +25,10 @@
1.4 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.5 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.6 val fmz = ["equality (a*b - (a+b)*x + x^^^2 = 0)",
1.7 - "solveFor x","solutions L"];
1.8 + "solveFor x", "solutions L"];
1.9 val (dI',pI',mI') =
1.10 - ("PolyEq",["degree_2","expanded","univariate","equation"],
1.11 - ["PolyEq","complete_square"]);
1.12 + ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
1.13 + ["PolyEq", "complete_square"]);
1.14 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.15 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.16 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.17 @@ -63,10 +63,10 @@
1.18 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.19 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.20 val fmz = ["equality (-64 + x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.a~*)
1.21 - "solveFor x","solutions L"];
1.22 + "solveFor x", "solutions L"];
1.23 val (dI',pI',mI') =
1.24 - ("PolyEq",["degree_2","expanded","univariate","equation"],
1.25 - ["PolyEq","complete_square"]);
1.26 + ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
1.27 + ["PolyEq", "complete_square"]);
1.28 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.29 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.30 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.31 @@ -90,10 +90,10 @@
1.32 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.33 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.34 val fmz = ["equality (-147 + 3*x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.b*)
1.35 - "solveFor x","solutions L"];
1.36 + "solveFor x", "solutions L"];
1.37 val (dI',pI',mI') =
1.38 - ("PolyEq",["degree_2","expanded","univariate","equation"],
1.39 - ["PolyEq","complete_square"]);
1.40 + ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
1.41 + ["PolyEq", "complete_square"]);
1.42 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.43 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.44 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.45 @@ -115,15 +115,15 @@
1.46 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1.47 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1.48 (*EP-17 Schalk_I_p86_n5*)
1.49 -val fmz = ["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"];
1.50 -(* Refine.refine fmz ["univariate","equation"];
1.51 +val fmz = ["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = -11)", "solveFor x", "solutions L"];
1.52 +(* Refine.refine fmz ["univariate", "equation"];
1.53 *)
1.54 -val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.55 +val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
1.56 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.57 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.58 (* val nxt =
1.59 ("Model_Problem",
1.60 - Model_Problem ["normalise","polynomial","univariate","equation"])
1.61 + Model_Problem ["normalise", "polynomial", "univariate", "equation"])
1.62 : string * tac*)
1.63 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.64 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.65 @@ -132,12 +132,12 @@
1.66 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.67 (* val nxt =
1.68 ("Subproblem",
1.69 - Subproblem ("PolyEq",["polynomial","univariate","equation"]))
1.70 + Subproblem ("PolyEq",["polynomial", "univariate", "equation"]))
1.71 : string * tac *)
1.72 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.73 (*val nxt =
1.74 ("Model_Problem",
1.75 - Model_Problem ["degree_1","polynomial","univariate","equation"])
1.76 + Model_Problem ["degree_1", "polynomial", "univariate", "equation"])
1.77 : string * tac *)
1.78 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.79 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.80 @@ -155,14 +155,14 @@
1.81 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1.82 (*is in rlang.sml, too*)
1.83 val fmz = ["equality ((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1))",
1.84 - "solveFor x","solutions L"];
1.85 -val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.86 + "solveFor x", "solutions L"];
1.87 +val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
1.88 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.89 -(*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*)
1.90 +(*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate", "equation"])*)
1.91 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.92 (* val nxt =
1.93 ("Model_Problem",
1.94 - Model_Problem ["normalise","polynomial","univariate","equation"])
1.95 + Model_Problem ["normalise", "polynomial", "univariate", "equation"])
1.96 : string * tac *)
1.97 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.98 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.99 @@ -172,12 +172,12 @@
1.100 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.101 (* val nxt =
1.102 ("Subproblem",
1.103 - Subproblem ("PolyEq",["polynomial","univariate","equation"]))
1.104 + Subproblem ("PolyEq",["polynomial", "univariate", "equation"]))
1.105 : string * tac*)
1.106 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.107 (*val nxt =
1.108 ("Model_Problem",
1.109 - Model_Problem ["abcFormula","degree_2","polynomial","univariate","equation"])
1.110 + Model_Problem ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])
1.111 : string * tac*)
1.112 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.113 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.114 @@ -193,10 +193,10 @@
1.115 " -4 + x^^^2 =0 ";
1.116 " -4 + x^^^2 =0 ";
1.117 " -4 + x^^^2 =0 ";
1.118 -val fmz = ["equality ( -4 + x^^^2 =0)", "solveFor x","solutions L"];
1.119 -(* val fmz = ["equality (1 + x^^^2 =0)", "solveFor x","solutions L"];*)
1.120 -(*val fmz = ["equality (0 =0)", "solveFor x","solutions L"];*)
1.121 -val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.122 +val fmz = ["equality ( -4 + x^^^2 =0)", "solveFor x", "solutions L"];
1.123 +(* val fmz = ["equality (1 + x^^^2 =0)", "solveFor x", "solutions L"];*)
1.124 +(*val fmz = ["equality (0 =0)", "solveFor x", "solutions L"];*)
1.125 +val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
1.126 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.127
1.128 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.129 @@ -262,8 +262,8 @@
1.130 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1.131 reset_states ();
1.132 CalcTree
1.133 -[(["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"],
1.134 - ("PolyEq",["univariate","equation"],["no_met"]))];
1.135 +[(["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = -11)", "solveFor x", "solutions L"],
1.136 + ("PolyEq",["univariate", "equation"],["no_met"]))];
1.137 Iterator 1;
1.138 moveActiveRoot 1;
1.139
1.140 @@ -281,13 +281,13 @@
1.141 val SOME (t''''', _) = rewrite_set_inst_ thy true subst d2_polyeq_bdv_only_simplify t;
1.142 (* steps in rls d2_polyeq_bdv_only_simplify:*)
1.143
1.144 -(*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1","")) --> x * (-6 + 5 * x) = 0*)
1.145 +(*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1", "")) --> x * (-6 + 5 * x) = 0*)
1.146 t |> UnparseC.term; t |> atomty;
1.147 val thm = ThmC.numerals_to_Free @{thm d2_prescind1};
1.148 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> atomty;
1.149 val SOME (t', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t; UnparseC.term t';
1.150
1.151 -(*x * (-6 + 5 * x) = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1",""))
1.152 +(*x * (-6 + 5 * x) = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1", ""))
1.153 --> x = 0 | -6 + 5 * x = 0*)
1.154 t' |> UnparseC.term; t' |> atomty;
1.155 val thm = ThmC.numerals_to_Free @{thm d2_reduce_equation1};