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/OLDTESTS/root-equ.sml
changeset 60565 f92963a33fe3
parent 60559 aba19e46dd84
child 60571 19a172de0bb5
equal deleted inserted replaced
60564:90ea835c07b3 60565:f92963a33fe3 
   184 val rls = norm_equation;	  
   184 val rls = norm_equation;	  
   185 val (t,_) = the (rewrite_set_ thy false rls t);
 
   185 val (t,_) = the (rewrite_set_ thy false rls t);
 
   186 val rls = Test_simplify;	  
   186 val rls = Test_simplify;	  
   187 val (t,_) = the (rewrite_set_ thy false rls t);
 
   187 val (t,_) = the (rewrite_set_ thy false rls t);
 
   188 val rls = isolate_bdv;
 
   188 val rls = isolate_bdv;
 
   189 val subst = [(TermC.str2term "bdv", TermC.str2term "x")];
 
   189 val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")];
 
   190 val (t,_) = the (rewrite_set_inst_ thy false subst rls t);
 
   190 val (t,_) = the (rewrite_set_inst_ thy false subst rls t);
 
   191 val rls = Test_simplify;
 
   191 val rls = Test_simplify;
 
   192 val (t,_) = the (rewrite_set_ thy false rls t);
 
   192 val (t,_) = the (rewrite_set_ thy false rls t);
 
   193 val t' = UnparseC.term t;
 
   193 val t' = UnparseC.term t;
 
   194 if t' = "x = 4" then ()
 
   194 if t' = "x = 4" then ()
 
   245 
   245 
   246 " _________________ rewrite + cappend _________________ ";
 
   246 " _________________ rewrite + cappend _________________ ";
 
   247 " _________________ rewrite + cappend _________________ ";
 
   247 " _________________ rewrite + cappend _________________ ";
 
   248 " _________________ rewrite + cappend _________________ ";
 
   248 " _________________ rewrite + cappend _________________ ";
 
   249 val thy' = "Test";
 
   249 val thy' = "Test";
 
   250 val ct = TermC.str2term"sqrt(9+4*x)=sqrt x + sqrt(5+x)";
 
   250 val ct = TermC.parse_test @{context}"sqrt(9+4*x)=sqrt x + sqrt(5+x)";
 
   251 val ctl = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)", "x::real", "0"];
 
   251 val ctl = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)", "x::real", "0"];
 
   252 val oris = O_Model.init thy ctl 
   252 val oris = O_Model.init thy ctl 
   253 		    ((#ppc o Problem.from_store)
 
   253 		    ((#ppc o Problem.from_store)
 
   254 			 ["sqroot-test", "univariate", "equation", "test"]);
 
   254 			 ["sqroot-test", "univariate", "equation", "test"]);
 
   255 val loc = Istate.empty;
 
   255 val loc = Istate.empty;
 
   288 val (pt,_) = cappend_parent pt pos loc ct (Tac "repeat") TransitiveB;
 
   288 val (pt,_) = cappend_parent pt pos loc ct (Tac "repeat") TransitiveB;
 
   289 
   289 
   290 val pos = (lev_on o lev_dn) pos;
 
   290 val pos = (lev_on o lev_dn) pos;
 
   291 val thm = ("square_equation_left", ""); val ctold = ct;
 
   291 val thm = ("square_equation_left", ""); val ctold = ct;
 
   292 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") true thm (UnparseC.term ct));
 
   292 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") true thm (UnparseC.term ct));
 
   293 val (pt,_) = cappend_atomic pt pos loc ctold (Tac (fst thm)) (TermC.str2term ct,[])Complete;
 
   293 val (pt,_) = cappend_atomic pt pos loc ctold (Tac (fst thm)) (TermC.parse_test @{context} ct,[])Complete;
 
   294 (*val pt = union_asm pt [] (map (rpair []) asm);*)
 
   294 (*val pt = union_asm pt [] (map (rpair []) asm);*)
 
   295 
   295 
   296 val pos = lev_on pos;
 
   296 val pos = lev_on pos;
 
   297 val rls = ("Test_simplify"); val ctold = TermC.str2term ct;
 
   297 val rls = ("Test_simplify"); val ctold = TermC.parse_test @{context} ct;
 
   298 val (ct,_) = the (rewrite_set thy'  false rls ct);
 
   298 val (ct,_) = the (rewrite_set thy'  false rls ct);
 
   299 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
 
   299 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
 
   300 
   300 
   301 val pos = lev_on pos;
 
   301 val pos = lev_on pos;
 
   302 val rls = ("rearrange_assoc"); val ctold = TermC.str2term ct;
 
   302 val rls = ("rearrange_assoc"); val ctold = TermC.parse_test @{context} ct;
 
   303 val (ct,_) = the (rewrite_set thy'  false rls ct);
 
   303 val (ct,_) = the (rewrite_set thy'  false rls ct);
 
   304 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
 
   304 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
 
   305 
   305 
   306 val pos = lev_on pos;
 
   306 val pos = lev_on pos;
 
   307 val rls = ("isolate_root"); val ctold = TermC.str2term ct;
 
   307 val rls = ("isolate_root"); val ctold = TermC.parse_test @{context} ct;
 
   308 val (ct,_) = the (rewrite_set thy'  false rls ct);
 
   308 val (ct,_) = the (rewrite_set thy'  false rls ct);
 
   309 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
 
   309 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
 
   310 
   310 
   311 val pos = lev_on pos;
 
   311 val pos = lev_on pos;
 
   312 val rls = ("Test_simplify"); val ctold = TermC.str2term ct;
 
   312 val rls = ("Test_simplify"); val ctold = TermC.parse_test @{context} ct;
 
   313 val (ct,_) = the (rewrite_set thy'  false rls ct);
 
   313 val (ct,_) = the (rewrite_set thy'  false rls ct);
 
   314 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
 
   314 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
 
   315 
   315 
   316 val pos = lev_on pos;
 
   316 val pos = lev_on pos;
 
   317 val thm = ("square_equation_left", ""); val ctold = TermC.str2term ct;
 
   317 val thm = ("square_equation_left", ""); val ctold = TermC.parse_test @{context} ct;
 
   318 val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
 
   318 val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
 
   319 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
 
   319 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
 
   320 (*val pt = union_asm pt [] (map (rpair []) asm);*)
 
   320 (*val pt = union_asm pt [] (map (rpair []) asm);*)
 
   321 
   321 
   322 val pos = lev_up pos;
 
   322 val pos = lev_up pos;
 
   323 val (pt,_) = append_result pt pos Istate.empty (TermC.str2term ct,[]) Complete;
 
   323 val (pt,_) = append_result pt pos Istate.empty (TermC.parse_test @{context} ct,[]) Complete;
 
   324 
   324 
   325 val pos = lev_on pos;
 
   325 val pos = lev_on pos;
 
   326 val rls = ("Test_simplify"); val ctold = TermC.str2term ct;
 
   326 val rls = ("Test_simplify"); val ctold = TermC.parse_test @{context} ct;
 
   327 val (ct,_) = the (rewrite_set thy'  false rls ct);
 
   327 val (ct,_) = the (rewrite_set thy'  false rls ct);
 
   328 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
 
   328 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
 
   329 
   329 
   330 val pos = lev_on pos;
 
   330 val pos = lev_on pos;
 
   331 val rls = ("norm_equation"); val ctold = TermC.str2term ct;
 
   331 val rls = ("norm_equation"); val ctold = TermC.parse_test @{context} ct;
 
   332 val (ct,_) = the (rewrite_set thy'  false rls ct);
 
   332 val (ct,_) = the (rewrite_set thy'  false rls ct);
 
   333 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
 
   333 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
 
   334 
   334 
   335 val pos = lev_on pos;
 
   335 val pos = lev_on pos;
 
   336 val rls = ("Test_simplify"); val ctold = TermC.str2term ct;
 
   336 val rls = ("Test_simplify"); val ctold = TermC.parse_test @{context} ct;
 
   337 val (ct,_) = the (rewrite_set thy'  false rls ct);
 
   337 val (ct,_) = the (rewrite_set thy'  false rls ct);
 
   338 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
 
   338 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
 
   339 
   339 
   340 (* --- see comments in interface_ME_ISA/instantiate''
 
   340 (* --- see comments in interface_ME_ISA/instantiate''
 
   341 val rlsdat' = instantiate_rls' thy' [("bdv", "x")] ("isolate_bdv");
 
   341 val rlsdat' = instantiate_rls' thy' [("bdv", "x")] ("isolate_bdv");
 
   342 val (ct,_) = the (rewrite_set thy'  false 
   342 val (ct,_) = the (rewrite_set thy'  false 
   343 		                 ("#isolate_bdv",rlsdat') ct);   *)
 
   343 		                 ("#isolate_bdv",rlsdat') ct);   *)
 
   344 val pos = lev_on pos;
 
   344 val pos = lev_on pos;
 
   345 val rls = ("isolate_bdv"); val ctold = TermC.str2term ct;
 
   345 val rls = ("isolate_bdv"); val ctold = TermC.parse_test @{context} ct;
 
   346 val (ct,_) = the (rewrite_set_inst thy'  false 
   346 val (ct,_) = the (rewrite_set_inst thy'  false 
   347 		  [("bdv", "x")] rls ct);
 
   347 		  [("bdv", "x")] rls ct);
 
   348 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
 
   348 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
 
   349 
   349 
   350 val pos = lev_on pos;
 
   350 val pos = lev_on pos;
 
   351 val rls = ("Test_simplify"); val ctold = TermC.str2term ct;  
   351 val rls = ("Test_simplify"); val ctold = TermC.parse_test @{context} ct;  
   352 val (ct,_) = the (rewrite_set thy'  false rls ct);
 
   352 val (ct,_) = the (rewrite_set thy'  false rls ct);
 
   353 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
 
   353 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
 
   354 
   354 
   355 val pos = lev_up pos;
 
   355 val pos = lev_up pos;
 
   356 val (pt,pos) = append_result pt pos Istate.empty (TermC.str2term ct,[]) Complete;
 
   356 val (pt,pos) = append_result pt pos Istate.empty (TermC.parse_test @{context} ct,[]) Complete;
 
   357 Ctree.get_assumptions pt ([],Res);
 
   357 Ctree.get_assumptions pt ([],Res);
 
   358 
   358 
   359 writeln (pr_ctree pr_short pt);
 
   359 writeln (pr_ctree pr_short pt);
 
   360 (* aus src.24-11-99:
 
   360 (* aus src.24-11-99:
 
   361 .   sqrt(9+4*x)=sqrt x + sqrt(5+x), x, (+0)
 
   361 .   sqrt(9+4*x)=sqrt x + sqrt(5+x), x, (+0)
 
   527 "--- 1 ---";
 
   527 "--- 1 ---";
 
   528 val nxt = ("Rewrite",Rewrite ("square_equation_left", ""));
 
   528 val nxt = ("Rewrite",Rewrite ("square_equation_left", ""));
 
   529 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   529 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   530 
   530 
   531 (*.9.6.03
 
   531 (*.9.6.03
 
   532  val t = TermC.str2term "sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)";
 
   532  val t = TermC.parse_test @{context} "sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)";
 
   533  val SOME (t',asm) = rewrite_set_ thy false rls t;
 
   533  val SOME (t',asm) = rewrite_set_ thy false rls t;
 
   534  UnparseC.term t';
 
   534  UnparseC.term t';
 
   535  Rewrite.trace_on:=false; (*true false*)
 
   535  Rewrite.trace_on:=false; (*true false*)
 
   536 *)
 
   536 *)
 
   537 
   537
wneuper/isa