Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Knowledge/polyeq-2.sml
changeset 60660 c4b24621077e
parent 60650 06ec8abfd3bc
child 60665 fad0cbfb586d
equal deleted inserted replaced
60659:873f40b097bb 60660:c4b24621077e 
   216 "----------- rls make_polynomial_in ------------------------------";
 
   216 "----------- rls make_polynomial_in ------------------------------";
 
   217 val thy = @{theory};
 
   217 val thy = @{theory};
 
   218 val ctxt = @{context};
 
   218 val ctxt = @{context};
 
   219 (*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
 
   219 (*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
 
   220 (*WN.19.3.03 ---v-*)
 
   220 (*WN.19.3.03 ---v-*)
 
   221 (*3(b)*)val (bdv,v) = (TermC.parse_test @{context} "''bdv''", TermC.parse_test @{context} "R1");
 
   221 (*3(b)*)val (bdv,v) = (ParseC.parse_test @{context} "''bdv''", ParseC.parse_test @{context} "R1");
 
   222 val t = TermC.parse_test @{context} "- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0";
 
   222 val t = ParseC.parse_test @{context} "- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0";
 
   223 val SOME (t',_) = rewrite_set_inst_ ctxt false [(bdv,v)] make_polynomial_in t;
 
   223 val SOME (t',_) = rewrite_set_inst_ ctxt false [(bdv,v)] make_polynomial_in t;
 
   224 if UnparseC.term t' = "- 1 * R * R2 + R2 * R1 + - 1 * R * R1 = 0" then ()
 
   224 if UnparseC.term t' = "- 1 * R * R2 + R2 * R1 + - 1 * R * R1 = 0" then ()
 
   225 else error "make_polynomial_in (- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0)";
 
   225 else error "make_polynomial_in (- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0)";
 
   226 "- 1 * R * R2 + (R2 + - 1 * R) * R1 = 0";
 
   226 "- 1 * R * R2 + (R2 + - 1 * R) * R1 = 0";
 
   227 (*WN.19.3.03 ---^-*)
 
   227 (*WN.19.3.03 ---^-*)
 
   228 
   228 
   229 (*3(c)*)val (bdv,v) = (TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "p");
 
   229 (*3(c)*)val (bdv,v) = (ParseC.parse_test @{context} "bdv", ParseC.parse_test @{context} "p");
 
   230 val t = TermC.parse_test @{context} "y \<up> 2 + - 2 * (x * p) = 0";
 
   230 val t = ParseC.parse_test @{context} "y \<up> 2 + - 2 * (x * p) = 0";
 
   231 val SOME (t',_) = rewrite_set_inst_ ctxt false [(bdv,v)] make_polynomial_in t;
 
   231 val SOME (t',_) = rewrite_set_inst_ ctxt false [(bdv,v)] make_polynomial_in t;
 
   232 if UnparseC.term t' = "y \<up> 2 + - 2 * x * p = 0" then ()
 
   232 if UnparseC.term t' = "y \<up> 2 + - 2 * x * p = 0" then ()
 
   233 else error "make_polynomial_in (y \<up> 2 + - 2 * (x * p) = 0)";
 
   233 else error "make_polynomial_in (y \<up> 2 + - 2 * (x * p) = 0)";
 
   234 
   234 
   235 (*3(d)*)val (bdv,v) = (TermC.parse_test @{context} "''bdv''", TermC.parse_test @{context} "x2");
 
   235 (*3(d)*)val (bdv,v) = (ParseC.parse_test @{context} "''bdv''", ParseC.parse_test @{context} "x2");
 
   236 val t = TermC.parse_test @{context} 
   236 val t = ParseC.parse_test @{context} 
   237 "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";
 
   237 "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";
 
   238 val SOME (t',_) = rewrite_set_inst_ ctxt false [(bdv,v)] make_polynomial_in t;
 
   238 val SOME (t',_) = rewrite_set_inst_ ctxt false [(bdv,v)] make_polynomial_in t;
 
   239 if UnparseC.term t' =
 
   239 if UnparseC.term t' =
 
   240 "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"
 
   240 "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"
 
   241 then ()
 
   241 then ()
 
   247 "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"
 
   247 "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"
 
   248 then ()
 
   248 then ()
 
   249 else error "make_ratpoly_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + - 1...";
 
   249 else error "make_ratpoly_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + - 1...";
 
   250 "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";
 
   250 "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";
 
   251 
   251 
   252 (*3(e)*)val (bdv,v) = (TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "a");
 
   252 (*3(e)*)val (bdv,v) = (ParseC.parse_test @{context} "bdv", ParseC.parse_test @{context} "a");
 
   253 val t = TermC.parse_test @{context} 
   253 val t = ParseC.parse_test @{context} 
   254 "A \<up> 2 + c \<up> 2 * (c / d) \<up> 2 + (-4 * (c / d) \<up> 2) * a \<up> 2 = 0";
 
   254 "A \<up> 2 + c \<up> 2 * (c / d) \<up> 2 + (-4 * (c / d) \<up> 2) * a \<up> 2 = 0";
 
   255 val NONE = rewrite_set_inst_ ctxt false [(bdv,v)] make_polynomial_in t;
 
   255 val NONE = rewrite_set_inst_ ctxt false [(bdv,v)] make_polynomial_in t;
 
   256 (* the invisible parentheses are as expected *)
 
   256 (* the invisible parentheses are as expected *)
 
   257 
   257 
   258 val t = TermC.parse_test @{context} "(x + 1) * (x + 2) - (3 * x - 2) \<up> 2 - ((2 * x - 1) \<up> 2 + (3 * x - 1) * (x + 1)) = 0";
 
   258 val t = ParseC.parse_test @{context} "(x + 1) * (x + 2) - (3 * x - 2) \<up> 2 - ((2 * x - 1) \<up> 2 + (3 * x - 1) * (x + 1)) = 0";
 
   259 rewrite_set_ ctxt false expand_binoms t;
 
   259 rewrite_set_ ctxt false expand_binoms t;
 
   260 
   260 
   261 
   261 
   262 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
 
   262 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
 
   263 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
 
   263 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
 
   276 
   276 
   277 
   277 
   278 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
 
   278 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
 
   279 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
 
   279 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
 
   280 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
 
   280 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
 
   281 val t = TermC.parse_test @{context} "-6 * x + 5 * x \<up> 2 = (0::real)";
 
   281 val t = ParseC.parse_test @{context} "-6 * x + 5 * x \<up> 2 = (0::real)";
 
   282 val subst = [(TermC.parse_test @{context} "(bdv::real)", TermC.parse_test @{context} "(x::real)")];
 
   282 val subst = [(ParseC.parse_test @{context} "(bdv::real)", ParseC.parse_test @{context} "(x::real)")];
 
   283 val SOME (t''''', _) = rewrite_set_inst_ ctxt true subst d2_polyeq_bdv_only_simplify t;
 
   283 val SOME (t''''', _) = rewrite_set_inst_ ctxt true subst d2_polyeq_bdv_only_simplify t;
 
   284 (* steps in rls d2_polyeq_bdv_only_simplify:*)
 
   284 (* steps in rls d2_polyeq_bdv_only_simplify:*)
 
   285 
   285 
   286 (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1", "")) --> x * (-6 + 5 * x) = 0*)
 
   286 (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1", "")) --> x * (-6 + 5 * x) = 0*)
 
   287 t |> UnparseC.term; t |> TermC.atom_trace_detail @{context};
 
   287 t |> UnparseC.term; t |> TermC.atom_trace_detail @{context};
wneuper/isa