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 60393 070aa3b448d6
parent 60330 e5e9a6c45597
child 60394 41cdbf7d5e6e
equal deleted inserted replaced
60392:e9a69b881f22 60393:070aa3b448d6 
   105 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   105 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 
   106 (*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = - 1 * sqrt (0 - -49)]"
 
   106 (*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = - 1 * sqrt (0 - -49)]"
 
   107  case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
 
   107  case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
 
   108 	 | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
 
   108 	 | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
 
   109 *)
 
   109 *)
 
   110 if f2str f = "[x = sqrt (0 - -49), x = - 1 * sqrt (0 - -49)]" then ()
 
   110 if f2str f = "[x = sqrt (0 - - 49), x = - 1 * sqrt (0 - - 49)]" then ()
 
   111 else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]";
 
   111 else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]";
 
   112 
   112 
   113 
   113 
   114 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
 
   114 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
 
   115 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
 
   115 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
 
   210 	 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = - 2]";
 
   210 	 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = - 2]";
 
   211 
   211 
   212 "----------- rls make_polynomial_in ------------------------------";
 
   212 "----------- rls make_polynomial_in ------------------------------";
 
   213 "----------- rls make_polynomial_in ------------------------------";
 
   213 "----------- rls make_polynomial_in ------------------------------";
 
   214 "----------- rls make_polynomial_in ------------------------------";
 
   214 "----------- rls make_polynomial_in ------------------------------";
 
       
   215 val thy = @{theory};
 
   215 (*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
 
   216 (*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
 
   216 (*WN.19.3.03 ---v-*)
 
   217 (*WN.19.3.03 ---v-*)
 
   217 (*3(b)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "R1");
 
   218 (*3(b)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "R1");
 
   218 val t = TermC.str2term "- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0";
 
   219 val t = TermC.str2term "- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0";
 
   219 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
 
   220 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
 
   281 val SOME (t''''', _) = rewrite_set_inst_ thy true subst d2_polyeq_bdv_only_simplify t;
 
   282 val SOME (t''''', _) = rewrite_set_inst_ thy true subst d2_polyeq_bdv_only_simplify t;
 
   282 (* steps in rls d2_polyeq_bdv_only_simplify:*)
 
   283 (* steps in rls d2_polyeq_bdv_only_simplify:*)
 
   283 
   284 
   284 (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1", "")) --> x * (-6 + 5 * x) = 0*)
 
   285 (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1", "")) --> x * (-6 + 5 * x) = 0*)
 
   285 t |> UnparseC.term; t |> TermC.atomty;
 
   286 t |> UnparseC.term; t |> TermC.atomty;
 
   286 val thm = ThmC.numerals_to_Free @{thm d2_prescind1};
 
   287 val thm = @{thm d2_prescind1};
 
   287 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
 
   288 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
 
   288 val SOME (t', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t; UnparseC.term t';
 
   289 val SOME (t', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t; UnparseC.term t';
 
   289 
   290 
   290 (*x * (-6 + 5 * x) = 0   : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1", "")) 
   291 (*x * (-6 + 5 * x) = 0   : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1", "")) 
   291                                                                         --> x = 0 | -6 + 5 * x = 0*)
 
   292                                                                         --> x = 0 | -6 + 5 * x = 0*)
 
   292 t' |> UnparseC.term; t' |> TermC.atomty;
 
   293 t' |> UnparseC.term; t' |> TermC.atomty;
 
   293 val thm = ThmC.numerals_to_Free @{thm d2_reduce_equation1};
 
   294 val thm = @{thm d2_reduce_equation1};
 
   294 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
 
   295 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
 
   295 val SOME (t'', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t'; UnparseC.term t'';
 
   296 val SOME (t'', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t'; UnparseC.term t'';
 
   296 (* NONE with d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
 
   297 (* NONE with d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
 
   297    instead   d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"
 
   298    instead   d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"
 
   298 *)
 
   299 *)
 
   299 if UnparseC.term t'' = "x = 0 \<or> -6 + 5 * x = 0" then ()
 
   300 if UnparseC.term t'' = "x = 0 \<or> - 6 + 5 * x = 0" then ()
 
   300 else error "rls d2_polyeq_bdv_only_simplify broken";
 
   301 else error "rls d2_polyeq_bdv_only_simplify broken";
wneuper/isa