1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Mon Aug 23 14:24:06 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Sun Sep 12 15:40:15 2021 +0200
1.3 @@ -22,7 +22,6 @@
1.4 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
1.5 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
1.6 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
1.7 -"------ polyeq- 2.sml ---------------------------------------------";
1.8 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
1.9 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
1.10 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
1.11 @@ -36,7 +35,7 @@
1.12 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
1.13 "----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1.14 "-----------------------------------------------------------------";
1.15 -"------ polyeq- 2.sml ---------------------------------------------";
1.16 +"------ polyeq-2.sml ---------------------------------------------";
1.17 "----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.18 "----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.19 "----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
2.1 --- a/test/Tools/isac/Knowledge/polyeq-2.sml Mon Aug 23 14:24:06 2021 +0200
2.2 +++ b/test/Tools/isac/Knowledge/polyeq-2.sml Sun Sep 12 15:40:15 2021 +0200
2.3 @@ -9,6 +9,8 @@
2.4 "-----------------------------------------------------------------";
2.5 "table of contents -----------------------------------------------";
2.6 "-----------------------------------------------------------------";
2.7 +"------ polyeq-2.sml ---------------------------------------------";
2.8 +"------ polyeq-1.sml ---------------------------------------------";
2.9 "----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
2.10 "----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
2.11 "----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
3.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon Aug 23 14:24:06 2021 +0200
3.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Sun Sep 12 15:40:15 2021 +0200
3.3 @@ -302,7 +302,7 @@
3.4 ML_file "Knowledge/diff.sml"
3.5 ML_file "Knowledge/integrate.sml"
3.6 ML_file "Knowledge/eqsystem-1.sml"
3.7 -(*ML_file "Knowledge/eqsystem-2.sml" broken by 8e46f61fdb15 *)
3.8 +(*ML_file "Knowledge/eqsystem-2.sml" broken by TOODOO 8e46f61fdb15 *)
3.9 ML_file "Knowledge/test.sml"
3.10 ML_file "Knowledge/polyminus.sml"
3.11 ML_file "Knowledge/vect.sml"
4.1 --- a/test/Tools/isac/Test_Some.thy Mon Aug 23 14:24:06 2021 +0200
4.2 +++ b/test/Tools/isac/Test_Some.thy Sun Sep 12 15:40:15 2021 +0200
4.3 @@ -107,318 +107,11 @@
4.4 section \<open>===================================================================================\<close>
4.5 ML \<open>
4.6 \<close> ML \<open>
4.7 -(* Title: Knowledge/polyeq- 1.sml
4.8 - testexamples for PolyEq, poynomial equations and equational systems
4.9 - Author: Richard Lang 2003
4.10 - (c) due to copyright terms
4.11 -WN030609: some expls dont work due to unfinished handling of 'expanded terms';
4.12 - others marked with TODO have to be checked, too.
4.13 -*)
4.14 -
4.15 -"-----------------------------------------------------------------";
4.16 -"table of contents -----------------------------------------------";
4.17 -"-----------------------------------------------------------------";
4.18 -"----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
4.19 -"----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
4.20 -"----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
4.21 -"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
4.22 -"----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
4.23 -"----------- rls make_polynomial_in ------------------------------";
4.24 -"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
4.25 -"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
4.26 -"-----------------------------------------------------------------";
4.27 -"-----------------------------------------------------------------";
4.28 -
4.29 -
4.30 -"----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
4.31 -"----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
4.32 -"----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
4.33 - val fmz = ["equality (a*b - (a+b)*x + x \<up> 2 = 0)",
4.34 - "solveFor x", "solutions L"];
4.35 - val (dI',pI',mI') =
4.36 - ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
4.37 - ["PolyEq", "complete_square"]);
4.38 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.39 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.40 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.41 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.42 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.43 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.44 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.45 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.46 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.47 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.48 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.49 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.50 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.51 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.52 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.53 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.54 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.55 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.56 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
4.57 -(*WN.2.5.03 TODO FIXME Matthias ?
4.58 - case f of
4.59 - Form'
4.60 - (Test_Out.FormKF
4.61 - (~1,EdUndef,0,Nundef,
4.62 - "[x = (a + b) / 2 + - 1 * sqrt ((a + b) \<up> 2 / 2 \<up> 2 - a * b),\n x = (a + b) / 2 + sqrt ((a + b) \<up> 2 / 2 \<up> 2 - a * b)]"))
4.63 - => ()
4.64 - | _ => error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x \<up> 2 = 0";
4.65 - this will be simplified [x = a, x = b] to by Factor.ML*)
4.66 -
4.67 -
4.68 -\<close> ML \<open>
4.69 -"----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
4.70 -"----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
4.71 -"----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
4.72 - val fmz = ["equality (-64 + x \<up> 2 = 0)",(*Schalk 2, S.66 Nr.1.a~*)
4.73 - "solveFor x", "solutions L"];
4.74 - val (dI',pI',mI') =
4.75 - ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
4.76 - ["PolyEq", "complete_square"]);
4.77 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.78 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.79 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.80 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.81 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.82 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.83 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.84 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.85 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.86 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.87 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.88 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.89 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.90 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
4.91 -(*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = - 1 * sqrt (0 - -64)]"
4.92 - case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => ()
4.93 - | _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]";
4.94 -*)
4.95 -
4.96 -\<close> ML \<open>
4.97 -"----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
4.98 -"----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
4.99 -"----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
4.100 -val fmz = ["equality (- 147 + 3*x \<up> 2 = 0)",(*Schalk 2, S.66 Nr.1.b*)
4.101 - "solveFor x", "solutions L"];
4.102 -val (dI',pI',mI') =
4.103 - ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
4.104 - ["PolyEq", "complete_square"]);
4.105 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.106 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.107 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.108 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.109 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.110 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.111 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.112 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.113 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.114 -(*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = - 1 * sqrt (0 - -49)]"
4.115 - case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
4.116 - | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
4.117 -*)
4.118 -if f2str f = "[x = sqrt (0 - - 49), x = - 1 * sqrt (0 - - 49)]" then ()
4.119 -else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]";
4.120 -
4.121 -
4.122 -\<close> ML \<open>
4.123 -"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
4.124 -"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
4.125 -"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
4.126 -(*EP- 17 Schalk_I_p86_n5*)
4.127 -val fmz = ["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = - 11)", "solveFor x", "solutions L"];
4.128 -(* Refine.refine fmz ["univariate", "equation"];
4.129 -*)
4.130 -val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
4.131 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.132 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.133 -(* val nxt =
4.134 - ("Model_Problem",
4.135 - Model_Problem ["normalise", "polynomial", "univariate", "equation"])
4.136 - : string * tac*)
4.137 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.138 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.139 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.140 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.141 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.142 -(* val nxt =
4.143 - ("Subproblem",
4.144 - Subproblem ("PolyEq",["polynomial", "univariate", "equation"]))
4.145 - : string * tac *)
4.146 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.147 -(*val nxt =
4.148 - ("Model_Problem",
4.149 - Model_Problem ["degree_1", "polynomial", "univariate", "equation"])
4.150 - : string * tac *)
4.151 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.152 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.153 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.154 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.155 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.156 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.157 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.158 -case f of Test_Out.FormKF "[x = 2]" => ()
4.159 - | _ => error "polyeq.sml: diff.behav. in [x = 2]";
4.160 -
4.161 -
4.162 -\<close> ML \<open>
4.163 -"----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
4.164 -"----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
4.165 -"----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
4.166 -(*is in rlang.sml, too*)
4.167 -val fmz = ["equality ((x+1)*(x+2) - (3*x - 2) \<up> 2=(2*x - 1) \<up> 2+(3*x - 1)*(x+1))",
4.168 - "solveFor x", "solutions L"];
4.169 -val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
4.170 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.171 -(*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate", "equation"])*)
4.172 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.173 -(* val nxt =
4.174 - ("Model_Problem",
4.175 - Model_Problem ["normalise", "polynomial", "univariate", "equation"])
4.176 - : string * tac *)
4.177 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.178 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.179 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.180 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.181 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.182 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.183 -(* val nxt =
4.184 - ("Subproblem",
4.185 - Subproblem ("PolyEq",["polynomial", "univariate", "equation"]))
4.186 - : string * tac*)
4.187 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.188 -(*val nxt =
4.189 - ("Model_Problem",
4.190 - Model_Problem ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])
4.191 - : string * tac*)
4.192 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.193 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.194 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.195 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.196 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.197 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.198 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.199 -case f of Test_Out.FormKF "[x = 2 / 15, x = 1]" => ()
4.200 - | _ => error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]";
4.201 -
4.202 -
4.203 -" -4 + x \<up> 2 =0 ";
4.204 -" -4 + x \<up> 2 =0 ";
4.205 -" -4 + x \<up> 2 =0 ";
4.206 -val fmz = ["equality ( -4 + x \<up> 2 =0)", "solveFor x", "solutions L"];
4.207 -(* val fmz = ["equality (1 + x \<up> 2 =0)", "solveFor x", "solutions L"];*)
4.208 -(*val fmz = ["equality (0 =0)", "solveFor x", "solutions L"];*)
4.209 -val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
4.210 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.211 -
4.212 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.213 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.214 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.215 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.216 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.217 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.218 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.219 -case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
4.220 - | _ => error "polyeq.sml: diff.behav. in [x = 2, x = - 2]";
4.221 -
4.222 -\<close> ML \<open>
4.223 -"----------- rls make_polynomial_in ------------------------------";
4.224 -"----------- rls make_polynomial_in ------------------------------";
4.225 -"----------- rls make_polynomial_in ------------------------------";
4.226 -val thy = @{theory};
4.227 -(*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
4.228 -(*WN.19.3.03 ---v-*)
4.229 -(*3(b)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "R1");
4.230 -val t = TermC.str2term "- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0";
4.231 -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
4.232 -if UnparseC.term t' = "- 1 * R * R2 + R2 * R1 + - 1 * R * R1 = 0" then ()
4.233 -else error "make_polynomial_in (- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0)";
4.234 -"- 1 * R * R2 + (R2 + - 1 * R) * R1 = 0";
4.235 -(*WN.19.3.03 ---^-*)
4.236 -
4.237 -(*3(c)*)val (bdv,v) = (TermC.str2term "bdv", TermC.str2term "p");
4.238 -val t = TermC.str2term "y \<up> 2 + - 2 * (x * p) = 0";
4.239 -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
4.240 -if UnparseC.term t' = "y \<up> 2 + - 2 * x * p = 0" then ()
4.241 -else error "make_polynomial_in (y \<up> 2 + - 2 * (x * p) = 0)";
4.242 -
4.243 -(*3(d)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "x2");
4.244 -val t = TermC.str2term
4.245 -"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";
4.246 -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
4.247 -if UnparseC.term t' =
4.248 -"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"
4.249 -then ()
4.250 -else error "make_polynomial_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + - 1...";
4.251 -"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";
4.252 -
4.253 -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t;
4.254 -if UnparseC.term t' =
4.255 -"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"
4.256 -then ()
4.257 -else error "make_ratpoly_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + - 1...";
4.258 -"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";
4.259 -
4.260 -(*3(e)*)val (bdv,v) = (TermC.str2term "bdv", TermC.str2term "a");
4.261 -val t = TermC.str2term
4.262 -"A \<up> 2 + c \<up> 2 * (c / d) \<up> 2 + (-4 * (c / d) \<up> 2) * a \<up> 2 = 0";
4.263 -val NONE = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
4.264 -(* the invisible parentheses are as expected *)
4.265 -
4.266 -val t = TermC.str2term "(x + 1) * (x + 2) - (3 * x - 2) \<up> 2 - ((2 * x - 1) \<up> 2 + (3 * x - 1) * (x + 1)) = 0";
4.267 -Rewrite.trace_on:= false; (*true false*)
4.268 -rewrite_set_ thy false expand_binoms t;
4.269 -Rewrite.trace_on:=false; (*true false*)
4.270 -
4.271 -
4.272 -\<close> ML \<open>
4.273 -"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
4.274 -"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
4.275 -"----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
4.276 -reset_states ();
4.277 -CalcTree
4.278 -[(["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = - 11)", "solveFor x", "solutions L"],
4.279 - ("PolyEq",["univariate", "equation"],["no_met"]))];
4.280 -Iterator 1;
4.281 -moveActiveRoot 1;
4.282 -
4.283 -autoCalculate 1 CompleteCalc;
4.284 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
4.285 -interSteps 1 ([1],Res)
4.286 -(*BEFORE Isabelle2002 --> 2011: <ERROR> no Rewrite_Set... </ERROR> ?see fun prep_rls?*);
4.287 -
4.288 -
4.289 -\<close> ML \<open>
4.290 -"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
4.291 -"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
4.292 -"----------- rls d2_polyeq_bdv_only_simplify ---------------------";
4.293 -val t = TermC.str2term "-6 * x + 5 * x \<up> 2 = (0::real)";
4.294 -val subst = [(TermC.str2term "(bdv::real)", TermC.str2term "(x::real)")];
4.295 -val SOME (t''''', _) = rewrite_set_inst_ thy true subst d2_polyeq_bdv_only_simplify t;
4.296 -(* steps in rls d2_polyeq_bdv_only_simplify:*)
4.297 -
4.298 -(*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1", "")) --> x * (-6 + 5 * x) = 0*)
4.299 -t |> UnparseC.term; t |> TermC.atomty;
4.300 -val thm = @{thm d2_prescind1};
4.301 -thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
4.302 -val SOME (t', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t; UnparseC.term t';
4.303 -
4.304 -(*x * (-6 + 5 * x) = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1", ""))
4.305 - --> x = 0 | -6 + 5 * x = 0*)
4.306 -t' |> UnparseC.term; t' |> TermC.atomty;
4.307 -val thm = @{thm d2_reduce_equation1};
4.308 -thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
4.309 -val SOME (t'', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t'; UnparseC.term t'';
4.310 -(* NONE with d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
4.311 - instead d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"
4.312 -*)
4.313 -if UnparseC.term t'' = "x = 0 \<or> - 6 + 5 * x = 0" then ()
4.314 -else error "rls d2_polyeq_bdv_only_simplify broken";
4.315 \<close> ML \<open>
4.316 \<close> ML \<open>
4.317 \<close>
4.318
4.319 +
4.320 section \<open>===================================================================================\<close>
4.321 ML \<open>
4.322 \<close> ML \<open>