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 59868 d77aa0992e0f
parent 59861 65ec9f679c3f
child 59871 82428ca0d23e
equal deleted inserted replaced
59867:bb153a08645b 59868:d77aa0992e0f 
   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) = (str2term "''bdv''", str2term "R1");
 
   221 (*3(b)*)val (bdv,v) = (str2term "''bdv''", str2term "R1");
 
   222 val t = str2term "-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0";
 
   222 val t = str2term "-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0";
 
   223 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
 
   223 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
 
   224 if UnparseC.term2str 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) = (str2term "bdv", str2term "p");
 
   229 (*3(c)*)val (bdv,v) = (str2term "bdv", str2term "p");
 
   230 val t = str2term "y ^^^ 2 + -2 * (x * p) = 0";
 
   230 val t = str2term "y ^^^ 2 + -2 * (x * p) = 0";
 
   231 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
 
   231 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
 
   232 if UnparseC.term2str t' = "y ^^^ 2 + -2 * x * p = 0" then ()
 
   232 if UnparseC.term t' = "y ^^^ 2 + -2 * x * p = 0" then ()
 
   233 else error "make_polynomial_in (y ^^^ 2 + -2 * (x * p) = 0)";
 
   233 else error "make_polynomial_in (y ^^^ 2 + -2 * (x * p) = 0)";
 
   234 
   234 
   235 (*3(d)*)val (bdv,v) = (str2term "''bdv''", str2term "x2");
 
   235 (*3(d)*)val (bdv,v) = (str2term "''bdv''", str2term "x2");
 
   236 val t = str2term 
   236 val t = str2term 
   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_ thy false [(bdv,v)] make_polynomial_in t;
 
   238 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
 
   239 if UnparseC.term2str 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 ()
 
   242 else error "make_polynomial_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1...";
 
   242 else error "make_polynomial_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1...";
 
   243 "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";
 
   243 "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";
 
   244 
   244 
   245 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t;
 
   245 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t;
 
   246 if UnparseC.term2str t' = 
   246 if UnparseC.term t' = 
   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 
   284 val subst = [(str2term "(bdv::real)", str2term "(x::real)")];
 
   284 val subst = [(str2term "(bdv::real)", str2term "(x::real)")];
 
   285 val SOME (t''''', _) = rewrite_set_inst_ thy true subst d2_polyeq_bdv_only_simplify t;
 
   285 val SOME (t''''', _) = rewrite_set_inst_ thy true subst d2_polyeq_bdv_only_simplify t;
 
   286 (* steps in rls d2_polyeq_bdv_only_simplify:*)
 
   286 (* steps in rls d2_polyeq_bdv_only_simplify:*)
 
   287 
   287 
   288 (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1","")) --> x * (-6 + 5 * x) = 0*)
 
   288 (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1","")) --> x * (-6 + 5 * x) = 0*)
 
   289 t |> UnparseC.term2str; t |> atomty;
 
   289 t |> UnparseC.term; t |> atomty;
 
   290 val thm = num_str @{thm d2_prescind1};
 
   290 val thm = num_str @{thm d2_prescind1};
 
   291 thm |> Thm.prop_of |> UnparseC.term2str; thm |> Thm.prop_of |> atomty;
 
   291 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> atomty;
 
   292 val SOME (t', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t; UnparseC.term2str t';
 
   292 val SOME (t', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t; UnparseC.term t';
 
   293 
   293 
   294 (*x * (-6 + 5 * x) = 0   : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1","")) 
   294 (*x * (-6 + 5 * x) = 0   : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1","")) 
   295                                                                         --> x = 0 | -6 + 5 * x = 0*)
 
   295                                                                         --> x = 0 | -6 + 5 * x = 0*)
 
   296 t' |> UnparseC.term2str; t' |> atomty;
 
   296 t' |> UnparseC.term; t' |> atomty;
 
   297 val thm = num_str @{thm d2_reduce_equation1};
 
   297 val thm = num_str @{thm d2_reduce_equation1};
 
   298 thm |> Thm.prop_of |> UnparseC.term2str; thm |> Thm.prop_of |> atomty;
 
   298 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> atomty;
 
   299 val SOME (t'', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t'; UnparseC.term2str t'';
 
   299 val SOME (t'', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t'; UnparseC.term t'';
 
   300 (* NONE with d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
 
   300 (* NONE with d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
 
   301    instead   d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"
 
   301    instead   d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"
 
   302 *)
 
   302 *)
 
   303 if UnparseC.term2str t'' = "x = 0 \<or> -6 + 5 * x = 0" then ()
 
   303 if UnparseC.term t'' = "x = 0 \<or> -6 + 5 * x = 0" then ()
 
   304 else error "rls d2_polyeq_bdv_only_simplify broken";
 
   304 else error "rls d2_polyeq_bdv_only_simplify broken";
wneuper/isa