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/eqsystem.sml
branchisac-update-Isa09-2
changeset 37995 fac82f29f143
parent 37991 028442673981
child 38014 3e11e3c2dc42
equal deleted inserted replaced
37994:eb4c556a525b 37995:fac82f29f143 
    99 atomty (term_of t);
 
    99 atomty (term_of t);
 
   100 val SOME t = parse Biegelinie.thy "solution L";
 
   100 val SOME t = parse Biegelinie.thy "solution L";
 
   101 atomty (term_of t);
 
   101 atomty (term_of t);
 
   102 
   102 
   103 val t = str2term 
   103 val t = str2term 
   104 "(tl (tl (tl vs_))) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))";
 
   104 "(tl (tl (tl v_s))) from_ v_s occur_exactly_in (nth_ 1 (es_::bool list))";
 
   105 atomty t;
 
   105 atomty t;
 
   106 val t = str2term 
   106 val t = str2term 
   107 "(tl (tl (tl [c,c_2,c_3,c_4]))) from_ [c,c_2,c_3,c_4] occur_exactly_in \
 
   107 "(tl (tl (tl [c,c_2,c_3,c_4]))) from_ [c,c_2,c_3,c_4] occur_exactly_in \
 
   108 \(nth_ 1 [c_4 = 1, 2=2,3=3,4=4])";
 
   108 \(nth_ 1 [c_4 = 1, 2=2,3=3,4=4])";
 
   109 val SOME (t,_) = 
   109 val SOME (t,_) = 
   282 
   282 
   283 "----------- script [EqSystem,normalize,2x2] ---------------------";
 
   283 "----------- script [EqSystem,normalize,2x2] ---------------------";
 
   284 "----------- script [EqSystem,normalize,2x2] ---------------------";
 
   284 "----------- script [EqSystem,normalize,2x2] ---------------------";
 
   285 "----------- script [EqSystem,normalize,2x2] ---------------------";
 
   285 "----------- script [EqSystem,normalize,2x2] ---------------------";
 
   286 val str = 
   286 val str = 
   287 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   287 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   288 \  (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   288 \  (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   289 \                                simplify_System_parenthesized False) es_  \
 
   289 \                                simplify_System_parenthesized False) es_  \
 
   290 \   in ([]))";
 
   290 \   in ([]))";
 
   291 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   291 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   292 val str = 
   292 val str = 
   293 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   293 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   294 \  (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   294 \  (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   295 \                                 simplify_System_parenthesized False) es_  \
 
   295 \                                 simplify_System_parenthesized False) es_  \
 
   296 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\
 
   296 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\
 
   297 \                  []))";
 
   297 \                  []))";
 
   298 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   298 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   299 val str = 
   299 val str = 
   300 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   300 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   301 \  (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   301 \  (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   302 \                                 simplify_System_parenthesized False) es_  \
 
   302 \                                 simplify_System_parenthesized False) es_  \
 
   303 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\
 
   303 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\
 
   304 \                  [BOOL_LIST es__, REAL_LIST vs_]))"
 
   304 \                  [BOOL_LIST es__, REAL_LIST v_s]))"
 
   305 ;
 
   305 ;
 
   306 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   306 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   307 val str = 
   307 val str = 
   308 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   308 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   309 \  (let es__ = Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   309 \  (let es__ = Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   310 \                                 simplify_System_parenthesized False) es_  \
 
   310 \                                 simplify_System_parenthesized False) es_  \
 
   311 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\
 
   311 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\
 
   312 \                  [BOOL_LIST es__, REAL_LIST vs_]))"
 
   312 \                  [BOOL_LIST es__, REAL_LIST v_s]))"
 
   313 ;
 
   313 ;
 
   314 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   314 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   315 val str = 
   315 val str = 
   316 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   316 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   317 \  (let es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   317 \  (let es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   318 \                                 simplify_System_parenthesized False)) es_  \
 
   318 \                                 simplify_System_parenthesized False)) es_  \
 
   319 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\
 
   319 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\
 
   320 \                  [BOOL_LIST es__, REAL_LIST vs_]))"
 
   320 \                  [BOOL_LIST es__, REAL_LIST v_s]))"
 
   321 ;
 
   321 ;
 
   322 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   322 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   323 val str = 
   323 val str = 
   324 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   324 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   325 \  (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   325 \  (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   326 \                                 simplify_System_parenthesized False)) @@\
 
   326 \                                 simplify_System_parenthesized False)) @@\
 
   327 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   327 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   328 \                                 simplify_System_parenthesized False))) es_\
 
   328 \                                 simplify_System_parenthesized False))) es_\
 
   329 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\
 
   329 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\
 
   330 \                  [BOOL_LIST es__, REAL_LIST vs_]))"
 
   330 \                  [BOOL_LIST es__, REAL_LIST v_s]))"
 
   331 ;
 
   331 ;
 
   332 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   332 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   333 val str = 
   333 val str = 
   334 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   334 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   335 \  (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   335 \  (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   336 \                                 simplify_System_parenthesized False)) @@\
 
   336 \                                 simplify_System_parenthesized False)) @@\
 
   337 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   337 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   338 \                                 simplify_System_parenthesized False)) @@\
 
   338 \                                 simplify_System_parenthesized False)) @@\
 
   339 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   339 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   340 \                                 simplify_System_parenthesized False))) es_\
 
   340 \                                 simplify_System_parenthesized False))) es_\
 
   341 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\
 
   341 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\
 
   342 \                  [BOOL_LIST es__, REAL_LIST vs_]))"
 
   342 \                  [BOOL_LIST es__, REAL_LIST v_s]))"
 
   343 ;
 
   343 ;
 
   344 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   344 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   345 val str = 
   345 val str = 
   346 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   346 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   347 \  (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   347 \  (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   348 \                                 simplify_System_parenthesized False)) @@\
 
   348 \                                 simplify_System_parenthesized False)) @@\
 
   349 \               (Try (Rewrite_Set_Inst [] isolate_bdvs False)) @@\
 
   349 \               (Try (Rewrite_Set_Inst [] isolate_bdvs False)) @@\
 
   350 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   350 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   351 \                                 simplify_System_parenthesized False)) @@\
 
   351 \                                 simplify_System_parenthesized False)) @@\
 
   352 \               (Try (Rewrite_Set order_system False))) es_\
 
   352 \               (Try (Rewrite_Set order_system False))) es_\
 
   353 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\
 
   353 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\
 
   354 \                  [BOOL_LIST es__, REAL_LIST vs_]))"
 
   354 \                  [BOOL_LIST es__, REAL_LIST v_s]))"
 
   355 ;
 
   355 ;
 
   356 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   356 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   357 val str = 
   357 val str = 
   358 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   358 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   359 \  (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   359 \  (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   360 \                                 simplify_System_parenthesized False)) @@\
 
   360 \                                 simplify_System_parenthesized False)) @@\
 
   361 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_)]\
 
   361 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s)]\
 
   362 \                                                    isolate_bdvs False)) @@\
 
   362 \                                                    isolate_bdvs False)) @@\
 
   363 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   363 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   364 \                                 simplify_System_parenthesized False)) @@\
 
   364 \                                 simplify_System_parenthesized False)) @@\
 
   365 \               (Try (Rewrite_Set order_system False))) es_\
 
   365 \               (Try (Rewrite_Set order_system False))) es_\
 
   366 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\
 
   366 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\
 
   367 \                  [BOOL_LIST es__, REAL_LIST vs_]))"
 
   367 \                  [BOOL_LIST es__, REAL_LIST v_s]))"
 
   368 ;
 
   368 ;
 
   369 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   369 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   370 val str = 
   370 val str = 
   371 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   371 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   372 \  (let es__ = ((Try (Rewrite_Set simplify_System_parenthesized False)) @@\
 
   372 \  (let es__ = ((Try (Rewrite_Set simplify_System_parenthesized False)) @@\
 
   373 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   373 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   374 \                                                    isolate_bdvs False)) @@\
 
   374 \                                                    isolate_bdvs False)) @@\
 
   375 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   375 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   376 \                                 simplify_System_parenthesized False)) @@\
 
   376 \                                 simplify_System_parenthesized False)) @@\
 
   377 \               (Try (Rewrite_Set order_system False))) es_\
 
   377 \               (Try (Rewrite_Set order_system False))) es_\
 
   378 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\
 
   378 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\
 
   379 \                  [BOOL_LIST es__, REAL_LIST vs_]))"
 
   379 \                  [BOOL_LIST es__, REAL_LIST v_s]))"
 
   380 ;
 
   380 ;
 
   381 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   381 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   382 (*---^^^-OK-----------------------------------------------------------------*)
 
   382 (*---^^^-OK-----------------------------------------------------------------*)
 
   383 (*---vvv-NOT ok-------------------------------------------------------------*)
 
   383 (*---vvv-NOT ok-------------------------------------------------------------*)
 
   384 
   384 
   385 
   385 
   386 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
 
   386 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
 
   387 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
 
   387 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
 
   388 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
 
   388 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
 
   389 val str = 
   389 val str = 
   390 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   390 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   391 \  (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   391 \  (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   392 \                                 simplify_System_parenthesized False) es_  \
 
   392 \                                 simplify_System_parenthesized False) es_  \
 
   393 \   in ([]))";
 
   393 \   in ([]))";
 
   394 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   394 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   395 val str = 
   395 val str = 
   396 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   396 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   397 \  (let e1__ = Take (hd es_)                \
 
   397 \  (let e1__ = Take (hd es_)                \
 
   398 \   in ([]))";
 
   398 \   in ([]))";
 
   399 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   399 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   400 val str = 
   400 val str = 
   401 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   401 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   402 \  (let e1__ = Take (hd es_);               \
 
   402 \  (let e1__ = Take (hd es_);               \
 
   403 \       e1__ = Take (hd es_)                \
 
   403 \       e1__ = Take (hd es_)                \
 
   404 \   in ([]))";
 
   404 \   in ([]))";
 
   405 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   405 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   406 val str = 
   406 val str = 
   407 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   407 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   408 \  (let e1__ = Take (hd es_);               \
 
   408 \  (let e1__ = Take (hd es_);               \
 
   409 \       e1__ = (Take (hd es_))\
 
   409 \       e1__ = (Take (hd es_))\
 
   410 \   in ([]))";
 
   410 \   in ([]))";
 
   411 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   411 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   412 val str = 
   412 val str = 
   413 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   413 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   414 \  (let e1__ = Take (hd es_);               \
 
   414 \  (let e1__ = Take (hd es_);               \
 
   415 \       e1__ = ((Rewrite_Set order_system False)) e1__\
 
   415 \       e1__ = ((Rewrite_Set order_system False)) e1__\
 
   416 \   in ([]))";
 
   416 \   in ([]))";
 
   417 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   417 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   418 (*--------------------------------------------------------------------------*)
 
   418 (*--------------------------------------------------------------------------*)
 
   419 val str = 
   419 val str = 
   420 "(Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   420 "(Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   421 \                                           isolate_bdvs False) (e1__::bool)";
 
   421 \                                           isolate_bdvs False) (e1__::bool)";
 
   422 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   422 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   423 (*--------------------------------------------------------------------------*)
 
   423 (*--------------------------------------------------------------------------*)
 
   424 val str = 
   424 val str = 
   425 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   425 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   426 \  (let e1__ = Take (hd es_);               \
 
   426 \  (let e1__ = Take (hd es_);               \
 
   427 \       e1__ = ((Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   427 \       e1__ = ((Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   428 \                                           isolate_bdvs False)) e1__\
 
   428 \                                           isolate_bdvs False)) e1__\
 
   429 \   in ([]))";
 
   429 \   in ([]))";
 
   430 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   430 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   431 val str = 
   431 val str = 
   432 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   432 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   433 \  (let e1__ = Take (hd es_);               \
 
   433 \  (let e1__ = Take (hd es_);               \
 
   434 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   434 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   435 \                                           isolate_bdvs False)) @@\
 
   435 \                                           isolate_bdvs False)) @@\
 
   436 \               (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   436 \               (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   437 \                                 simplify_System False)) e1__\
 
   437 \                                 simplify_System False)) e1__\
 
   438 \   in ([]))";
 
   438 \   in ([]))";
 
   439 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   439 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   440 val str = 
   440 val str = 
   441 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   441 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   442 \  (let e1__ = Take (hd es_);               \
 
   442 \  (let e1__ = Take (hd es_);               \
 
   443 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   443 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   444 \                                           isolate_bdvs False)) @@\
 
   444 \                                           isolate_bdvs False)) @@\
 
   445 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   445 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   446 \                                 simplify_System False))) e1__\
 
   446 \                                 simplify_System False))) e1__\
 
   447 \   in ([]))";
 
   447 \   in ([]))";
 
   448 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   448 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   449 val str = 
   449 val str = 
   450 "Script SolveSystemScript (es_::bool list) (vs_::real list) =                \
 
   450 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                \
 
   451 \  (let e1__ = Take (hd es_);                                                \
 
   451 \  (let e1__ = Take (hd es_);                                                \
 
   452 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   452 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   453 \                                           isolate_bdvs False)) @@          \
 
   453 \                                           isolate_bdvs False)) @@          \
 
   454 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   454 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   455 \                                 simplify_System False))) e1__;           \
 
   455 \                                 simplify_System False))) e1__;           \
 
   456 \       e2__ = Take (hd (tl es_))                                            \
 
   456 \       e2__ = Take (hd (tl es_))                                            \
 
   457 \   in ([]))";
 
   457 \   in ([]))";
 
   458 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   458 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   459 val str = 
   459 val str = 
   460 "Script SolveSystemScript (es_::bool list) (vs_::real list) =                \
 
   460 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                \
 
   461 \  (let e1__ = Take (hd es_);                                                \
 
   461 \  (let e1__ = Take (hd es_);                                                \
 
   462 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   462 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   463 \                                           isolate_bdvs False)) @@          \
 
   463 \                                           isolate_bdvs False)) @@          \
 
   464 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   464 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   465 \                                 simplify_System False))) e1__;           \
 
   465 \                                 simplify_System False))) e1__;           \
 
   466 \       e2__ = Take (hd (tl es_));                                           \
 
   466 \       e2__ = Take (hd (tl es_));                                           \
 
   467 \       e2__ = Substitute [e1__] e2__                                       \
 
   467 \       e2__ = Substitute [e1__] e2__                                       \
 
   468 \   in ([]))";
 
   468 \   in ([]))";
 
   469 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   469 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   470 val str = 
   470 val str = 
   471 "Script SolveSystemScript (es_::bool list) (vs_::real list) =                \
 
   471 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                \
 
   472 \  (let e1__ = Take (hd es_);                                                \
 
   472 \  (let e1__ = Take (hd es_);                                                \
 
   473 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   473 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   474 \                                           isolate_bdvs False)) @@          \
 
   474 \                                           isolate_bdvs False)) @@          \
 
   475 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   475 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   476 \                                 simplify_System False))) e1__;           \
 
   476 \                                 simplify_System False))) e1__;           \
 
   477 \       e2__ = Take (hd (tl es_));                                           \
 
   477 \       e2__ = Take (hd (tl es_));                                           \
 
   478 \       e2__ = ((Substitute [e1__])) e2__                                  \
 
   478 \       e2__ = ((Substitute [e1__])) e2__                                  \
 
   479 \   in ([]))";
 
   479 \   in ([]))";
 
   480 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   480 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   481 val str = 
   481 val str = 
   482 "Script SolveSystemScript (es_::bool list) (vs_::real list) =                \
 
   482 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                \
 
   483 \  (let e1__ = Take (hd es_);                                                \
 
   483 \  (let e1__ = Take (hd es_);                                                \
 
   484 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   484 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   485 \                                      isolate_bdvs False)) @@               \
 
   485 \                                      isolate_bdvs False)) @@               \
 
   486 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   486 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   487 \                                 simplify_System False))) e1__;           \
 
   487 \                                 simplify_System False))) e1__;           \
 
   488 \       e2__ = Take (hd (tl es_));                                           \
 
   488 \       e2__ = Take (hd (tl es_));                                           \
 
   489 \       e2__ = ((Substitute [e1__]) @@                                       \
 
   489 \       e2__ = ((Substitute [e1__]) @@                                       \
 
   490 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   490 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   491 \                                      isolate_bdvs False)) @@               \
 
   491 \                                      isolate_bdvs False)) @@               \
 
   492 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   492 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   493 \                                 simplify_System False))) e2__            \
 
   493 \                                 simplify_System False))) e2__            \
 
   494 \   in [e1__, e2__])"
 
   494 \   in [e1__, e2__])"
 
   495 ;
 
   495 ;
 
   496 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   496 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   497 val str = 
   497 val str = 
   498 "Script SolveSystemScript (es_::bool list) (vs_::real list) =                \
 
   498 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                \
 
   499 \  (let e1__ = Take (hd es_);                                                \
 
   499 \  (let e1__ = Take (hd es_);                                                \
 
   500 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   500 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   501 \                                      isolate_bdvs False)) @@               \
 
   501 \                                      isolate_bdvs False)) @@               \
 
   502 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   502 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   503 \                                 simplify_System False))) e1__;           \
 
   503 \                                 simplify_System False))) e1__;           \
 
   504 \       e2__ = Take (hd (tl es_));                                           \
 
   504 \       e2__ = Take (hd (tl es_));                                           \
 
   505 \       e2__ = ((Substitute [e1__]) @@                                       \
 
   505 \       e2__ = ((Substitute [e1__]) @@                                       \
 
   506 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   506 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   507 \                                 simplify_System_parenthesized False)) @@ \
 
   507 \                                 simplify_System_parenthesized False)) @@ \
 
   508 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   508 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   509 \                                      isolate_bdvs False)) @@               \
 
   509 \                                      isolate_bdvs False)) @@               \
 
   510 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   510 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   511 \                                 simplify_System False)) @@               \
 
   511 \                                 simplify_System False)) @@               \
 
   512 \               (Try (Rewrite_Set order_system False))) e2__                 \
 
   512 \               (Try (Rewrite_Set order_system False))) e2__                 \
 
   513 \   in [e1__, e2__])"
 
   513 \   in [e1__, e2__])"
 
   514 ;
 
   514 ;
 
   515 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   515 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   516 (*---^^^-OK-----------------------------------------------------------------*)
 
   516 (*---^^^-OK-----------------------------------------------------------------*)
 
   517 val str = 
   517 val str = 
   518 "Script SolveSystemScript (es_::bool list) (vs_::real list) =                \
 
   518 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                \
 
   519 \  (let e1__ = Take (hd es_);                                                \
 
   519 \  (let e1__ = Take (hd es_);                                                \
 
   520 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   520 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   521 \                                      isolate_bdvs False)) @@               \
 
   521 \                                      isolate_bdvs False)) @@               \
 
   522 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   522 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   523 \                                 simplify_System False))) e1__;           \
 
   523 \                                 simplify_System False))) e1__;           \
 
   524 \       e2__ = Take (hd (tl es_));                                           \
 
   524 \       e2__ = Take (hd (tl es_));                                           \
 
   525 \       e2__ = ((Substitute [e1__]) @@                                       \
 
   525 \       e2__ = ((Substitute [e1__]) @@                                       \
 
   526 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   526 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   527 \                                 simplify_System_parenthesized False)) @@ \
 
   527 \                                 simplify_System_parenthesized False)) @@ \
 
   528 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   528 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   529 \                                      isolate_bdvs False)) @@               \
 
   529 \                                      isolate_bdvs False)) @@               \
 
   530 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   530 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   531 \                                 simplify_System False))) e2__;           \
 
   531 \                                 simplify_System False))) e2__;           \
 
   532 \       es__ = Take [e1__, e2__]\
 
   532 \       es__ = Take [e1__, e2__]\
 
   533 \   in (Try (Rewrite_Set order_system False)) es__)"
 
   533 \   in (Try (Rewrite_Set order_system False)) es__)"
 
   534 ;
 
   534 ;
 
   535 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   535 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   538 
   538 
   539 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
 
   539 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
 
   540 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
 
   540 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
 
   541 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
 
   541 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
 
   542 val str = 
   542 val str = 
   543 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   543 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   544 \  (let es__ = Take es_;   \
 
   544 \  (let es__ = Take es_;   \
 
   545 \       e1__ = hd es__\
 
   545 \       e1__ = hd es__\
 
   546 \   in ([]))"
 
   546 \   in ([]))"
 
   547 ;
 
   547 ;
 
   548 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   548 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   549 val str = 
   549 val str = 
   550 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   550 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   551 \  (let es__ = Take es_;   \
 
   551 \  (let es__ = Take es_;   \
 
   552 \       e1__ = hd es__;    \
 
   552 \       e1__ = hd es__;    \
 
   553 \       e2__ = hd (tl es__)\
 
   553 \       e2__ = hd (tl es__)\
 
   554 \   in ([]))"
 
   554 \   in ([]))"
 
   555 ;
 
   555 ;
 
   556 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   556 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   557 val str = 
   557 val str = 
   558 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   558 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   559 \  (let es__ = Take es_;   \
 
   559 \  (let es__ = Take es_;   \
 
   560 \       e1__ = hd es__;    \
 
   560 \       e1__ = hd es__;    \
 
   561 \       e2__ = hd (tl es__);\
 
   561 \       e2__ = hd (tl es__);\
 
   562 \       es__ = [1=2,3=4]\
 
   562 \       es__ = [1=2,3=4]\
 
   563 \   in ([]))"
 
   563 \   in ([]))"
 
   564 ;
 
   564 ;
 
   565 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   565 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   566 val str = 
   566 val str = 
   567 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   567 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   568 \  (let es__ = Take es_;   \
 
   568 \  (let es__ = Take es_;   \
 
   569 \       e1__ = hd es__;    \
 
   569 \       e1__ = hd es__;    \
 
   570 \       e2__ = hd (tl es__);\
 
   570 \       e2__ = hd (tl es__);\
 
   571 \       es__ = [e1__,e2__]\
 
   571 \       es__ = [e1__,e2__]\
 
   572 \   in ([]))"
 
   572 \   in ([]))"
 
   573 ;
 
   573 ;
 
   574 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   574 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   575 val str = 
   575 val str = 
   576 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   576 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   577 \  (let es__ = Take es_;   \
 
   577 \  (let es__ = Take es_;   \
 
   578 \       e1__ = hd es__;    \
 
   578 \       e1__ = hd es__;    \
 
   579 \       e2__ = hd (tl es__);\
 
   579 \       e2__ = hd (tl es__);\
 
   580 \       es__ = [e1__, Substitute [e1__] e2__];\
 
   580 \       es__ = [e1__, Substitute [e1__] e2__];\
 
   581 \       es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   581 \       es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   582 \                                 simplify_System False)) es__            \
 
   582 \                                 simplify_System False)) es__            \
 
   583 \   in ([]))"
 
   583 \   in ([]))"
 
   584 ;
 
   584 ;
 
   585 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   585 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   586 val str = 
   586 val str = 
   587 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   587 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   588 \  (let es__ = Take es_;   \
 
   588 \  (let es__ = Take es_;   \
 
   589 \       e1__ = hd es__;    \
 
   589 \       e1__ = hd es__;    \
 
   590 \       e2__ = hd (tl es__);\
 
   590 \       e2__ = hd (tl es__);\
 
   591 \       es__ = [e1__, Substitute [e1__] e2__];\
 
   591 \       es__ = [e1__, Substitute [e1__] e2__];\
 
   592 \       es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   592 \       es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   593 \                                      isolate_bdvs False)) @@               \
 
   593 \                                      isolate_bdvs False)) @@               \
 
   594 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   594 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   595 \                                 simplify_System False))) es__            \
 
   595 \                                 simplify_System False))) es__            \
 
   596 \   in ([]))"
 
   596 \   in ([]))"
 
   597 ;
 
   597 ;
 
   598 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   598 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   599 val str = 
   599 val str = 
   600 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   600 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   601 \  (let es__ = Take es_;   \
 
   601 \  (let es__ = Take es_;   \
 
   602 \       e1__ = hd es__;    \
 
   602 \       e1__ = hd es__;    \
 
   603 \       e2__ = hd (tl es__);\
 
   603 \       e2__ = hd (tl es__);\
 
   604 \       es__ = [e1__, Substitute [e1__] e2__];\
 
   604 \       es__ = [e1__, Substitute [e1__] e2__];\
 
   605 \       es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   605 \       es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   606 \                                 simplify_System_parenthesized False)) @@  \
 
   606 \                                 simplify_System_parenthesized False)) @@  \
 
   607 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   607 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   608 \                                      isolate_bdvs False)) @@               \
 
   608 \                                      isolate_bdvs False)) @@               \
 
   609 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   609 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   610 \                                 simplify_System False))) es__            \
 
   610 \                                 simplify_System False))) es__            \
 
   611 \   in ([]))"
 
   611 \   in ([]))"
 
   612 ;
 
   612 ;
 
   613 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   613 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   614 val str = 
   614 val str = 
   615 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
 
   615 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \
 
   616 \  (let es__ = Take es_;                                                     \
 
   616 \  (let es__ = Take es_;                                                     \
 
   617 \       e1__ = hd es__;                                                      \
 
   617 \       e1__ = hd es__;                                                      \
 
   618 \       e2__ = hd (tl es__);                                                 \
 
   618 \       e2__ = hd (tl es__);                                                 \
 
   619 \       es__ = [e1__, Substitute [e1__] e2__];                               \
 
   619 \       es__ = [e1__, Substitute [e1__] e2__];                               \
 
   620 \       es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   620 \       es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   621 \                                 simplify_System_parenthesized False)) @@  \
 
   621 \                                 simplify_System_parenthesized False)) @@  \
 
   622 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   622 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   623 \                                      isolate_bdvs False))              @@  \
 
   623 \                                      isolate_bdvs False))              @@  \
 
   624 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   624 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   625 \                                 simplify_System False))) es__            \
 
   625 \                                 simplify_System False))) es__            \
 
   626 \   in es__)"
 
   626 \   in es__)"
 
   627 ;
 
   627 ;
 
   628 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   628 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   629 val str = 
   629 val str = 
   630 "Script SolveSystemScript (es_::bool list) (vs_::real list) =         \
 
   630 "Script SolveSystemScript (es_::bool list) (v_s::real list) =         \
 
   631 \  (let es__ = Take es_;                                              \
 
   631 \  (let es__ = Take es_;                                              \
 
   632 \       e1__ = hd es__;                                               \
 
   632 \       e1__ = hd es__;                                               \
 
   633 \       e2__ = hd (tl es__);                                          \
 
   633 \       e2__ = hd (tl es__);                                          \
 
   634 \       es__ = [e1__, Substitute [e1__] e2__]                         \
 
   634 \       es__ = [e1__, Substitute [e1__] e2__]                         \
 
   635 \   in ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   635 \   in ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   636 \                                 simplify_System_parenthesized False)) @@   \
 
   636 \                                 simplify_System_parenthesized False)) @@   \
 
   637 \       (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))] \
 
   637 \       (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))] \
 
   638 \                              isolate_bdvs False))              @@   \
 
   638 \                              isolate_bdvs False))              @@   \
 
   639 \       (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   639 \       (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   640 \                                 simplify_System False))) es__)"
 
   640 \                                 simplify_System False))) es__)"
 
   641 ;
 
   641 ;
 
   642 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   642 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   643 (*---^^^-OK-----------------------------------------------------------------*)
 
   643 (*---^^^-OK-----------------------------------------------------------------*)
 
   644 val str = 
   644 val str = 
   645 "Script SolveSystemScript (es_::bool list) (vs_::real list) =         \
 
   645 "Script SolveSystemScript (es_::bool list) (v_s::real list) =         \
 
   646 \  (let es__ = Take es_;                                              \
 
   646 \  (let es__ = Take es_;                                              \
 
   647 \       e1__ = hd es__;                                               \
 
   647 \       e1__ = hd es__;                                               \
 
   648 \       e2__ = hd (tl es__);                                          \
 
   648 \       e2__ = hd (tl es__);                                          \
 
   649 \       es__ = [e1__, Substitute [e1__] e2__]                         "^
 
   649 \       es__ = [e1__, Substitute [e1__] e2__]                         "^
 
   650 (* this        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ is a script-'Expr'
 
   650 (* this        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ is a script-'Expr'
 
   651    which is not yet searched for 'STac's; thus this script does not yet work*)
 
   651    which is not yet searched for 'STac's; thus this script does not yet work*)
 
   652 "   in ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   652 "   in ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   653 \                                 simplify_System_parenthesized False)) @@   \
 
   653 \                                 simplify_System_parenthesized False)) @@   \
 
   654 \       (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))] \
 
   654 \       (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))] \
 
   655 \                              isolate_bdvs False))              @@   \
 
   655 \                              isolate_bdvs False))              @@   \
 
   656 \       (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
   656 \       (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
   657 \                                 simplify_System False))) es__)"
 
   657 \                                 simplify_System False))) es__)"
 
   658 ;
 
   658 ;
 
   659 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   659 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
   660 (*---vvv-NOT ok-------------------------------------------------------------*)
 
   660 (*---vvv-NOT ok-------------------------------------------------------------*)
 
   661 atomty sc;
 
   661 atomty sc;
 
   789 =========================================================================\
 
   789 =========================================================================\
 
   790 -------fun prep_pbt
 
   790 -------fun prep_pbt
 
   791 (* val (thy, (pblID, dsc_dats: (string * (string list)) list, 
   791 (* val (thy, (pblID, dsc_dats: (string * (string list)) list, 
   792 		  ev:rls, ca: string option, metIDs:metID list)) =
 
   792 		  ev:rls, ca: string option, metIDs:metID list)) =
 
   793        (EqSystem.thy, (["system"],
 
   793        (EqSystem.thy, (["system"],
 
   794 		       [("#Given" ,["equalities es_", "solveForVars vs_"]),
 
   794 		       [("#Given" ,["equalities es_", "solveForVars v_s"]),
 
   795 			("#Find"  ,["solution ss___"](*___ is copy-named*))
 
   795 			("#Find"  ,["solution ss___"](*___ is copy-named*))
 
   796 			],
 
   796 			],
 
   797 		       append_rls "e_rls" e_rls [(*for preds in where_*)], 
   797 		       append_rls "e_rls" e_rls [(*for preds in where_*)], 
   798 		       SOME "solveSystem es_ vs_", 
   798 		       SOME "solveSystem es_ v_s", 
   799 		       []));
 
   799 		       []));
 
   800    *)
 
   800    *)
 
   801 > val [("#Given", [equalities_es_, "solveForVars vs_"])] = gi;
 
   801 > val [("#Given", [equalities_es_, "solveForVars v_s"])] = gi;
 
   802 val equalities_es_ = "equalities es_" : string
 
   802 val equalities_es_ = "equalities es_" : string
 
   803 > val (dd, ii) = (split_did o term_of o the o (parse thy)) equalities_es_;
 
   803 > val (dd, ii) = (split_did o term_of o the o (parse thy)) equalities_es_;
 
   804 > show_types:=true; term2str ii; show_types:=false;
 
   804 > show_types:=true; term2str ii; show_types:=false;
 
   805 val it = "es_::bool list" : string
 
   805 val it = "es_::bool list" : string
 
   806 ~~~~~~~~~~~~~~~^^^^^^^^^ OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
   806 ~~~~~~~~~~~~~~~^^^^^^^^^ OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
   817 [
 
   817 [
 
   818 (1 ,[1] ,true ,#Given ,Cor equalities
 
   818 (1 ,[1] ,true ,#Given ,Cor equalities
 
   819  [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
 
   819  [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
 
   820   0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2] ,(es_, [[0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
 
   820   0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2] ,(es_, [[0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
 
   821  0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]])),
 
   821  0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]])),
 
   822 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])),
 
   822 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
 
   823 (3 ,[1] ,true ,#Find ,Cor solution L ,(ss___, [L]))]
 
   823 (3 ,[1] ,true ,#Find ,Cor solution L ,(ss___, [L]))]
 
   824 
   824 
   825 > (writeln o pres2str) pre';
 
   825 > (writeln o pres2str) pre';
 
   826 [
 
   826 [
 
   827 (false, length_ es_ = 2),
 
   827 (false, length_ es_ = 2),
 
   835 ----- fun check_preconds'
 
   835 ----- fun check_preconds'
 
   836 > (writeln o env2str) env;
 
   836 > (writeln o env2str) env;
 
   837 ["
 
   837 ["
 
   838 (es_, [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
 
   838 (es_, [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
 
   839  0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2])","
 
   839  0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2])","
 
   840 (vs_, [c, c_2])","
 
   840 (v_s, [c, c_2])","
 
   841 (ss___, L)"]
 
   841 (ss___, L)"]
 
   842 
   842 
   843 > val es_ = (fst o hd) env;
 
   843 > val es_ = (fst o hd) env;
 
   844 val es_ = Free ("es_", "bool List.list") : Term.term
 
   844 val es_ = Free ("es_", "bool List.list") : Term.term
 
   845 
   845 
   897 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   897 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   898 val PblObj {probl,...} = get_obj I pt [5];
 
   898 val PblObj {probl,...} = get_obj I pt [5];
 
   899     (writeln o (itms2str_ (thy2ctxt "Isac"))) probl;
 
   899     (writeln o (itms2str_ (thy2ctxt "Isac"))) probl;
 
   900 (*[
 
   900 (*[
 
   901 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])),
 
   901 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])),
 
   902 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])),
 
   902 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
 
   903 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
 
   903 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
 
   904 *)
 
   904 *)
 
   905 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 
   905 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 
   906 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 
   906 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 
   907 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 
   907 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 
   966 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   966 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   967 val PblObj {probl,...} = get_obj I pt [5];
 
   967 val PblObj {probl,...} = get_obj I pt [5];
 
   968     (writeln o (itms2str_ (thy2ctxt "Isac"))) probl;
 
   968     (writeln o (itms2str_ (thy2ctxt "Isac"))) probl;
 
   969 (*[
 
   969 (*[
 
   970 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])),
 
   970 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])),
 
   971 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])),
 
   971 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
 
   972 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
 
   972 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
 
   973 *)
 
   973 *)
 
   974 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 
   974 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 
   975 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 
   975 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 
   976 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 
   976 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
 
  1153 
  1153 
  1154 "----- 7.70 with met top_down_: ";
 
  1154 "----- 7.70 with met top_down_: ";
 
  1155 "--- scr [EqSystem,top_down_substitution,4x4] -- a saved trial";
 
  1155 "--- scr [EqSystem,top_down_substitution,4x4] -- a saved trial";
 
  1156 (*---vvv-this script failed with if ?!?-------------------------------------*) 
  1156 (*---vvv-this script failed with if ?!?-------------------------------------*) 
  1157 val str = 
  1157 val str = 
  1158 "Script SolveSystemScript (es_::bool list) (vs_::real list) =          \
 
  1158 "Script SolveSystemScript (es_::bool list) (v_s::real list) =          \
 
  1159 \  (let e1_ = hd es_;                                                  \
 
  1159 \  (let e1_ = hd es_;                                                  \
 
  1160 \       v1_ = hd vs_;                                                  \
 
  1160 \       v1_ = hd v_s;                                                  \
 
  1161 \       xxx = if lhs e1_ =!= v1_                                       \
 
  1161 \       xxx = if lhs e1_ =!= v1_                                       \
 
  1162 \             then 0=0                                                 \
 
  1162 \             then 0=0                                                 \
 
  1163 \             else let e1_ = Take e1_;                                 \
 
  1163 \             else let e1_ = Take e1_;                                 \
 
  1164 \                      e1_ = (Rewrite_Set_Inst [(bdv_1, hd vs_),       \
 
  1164 \                      e1_ = (Rewrite_Set_Inst [(bdv_1, hd v_s),       \
 
  1165 \                                               (bdv_2, hd (tl vs_))]  \
 
  1165 \                                               (bdv_2, hd (tl v_s))]  \
 
  1166 \                                  isolate_bdvs False) e1_;            \
 
  1166 \                                  isolate_bdvs False) e1_;            \
 
  1167 \       e2_ = Take (hd (tl es_));                                      \
 
  1167 \       e2_ = Take (hd (tl es_));                                      \
 
  1168 \       e2_ = (Substitute [e1__]) e2_                                  \
 
  1168 \       e2_ = (Substitute [e1__]) e2_                                  \
 
  1169 \    in [e1_, e2_])";
 
  1169 \    in [e1_, e2_])";
 
  1170 (*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*)
 
  1170 (*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*)
 
  1171 val str = 
  1171 val str = 
  1172 "Script SolveSystemScript (es_::bool list) (vs_::real list) =          \
 
  1172 "Script SolveSystemScript (es_::bool list) (v_s::real list) =          \
 
  1173 \  (let e1_ = hd es_;                                                  \
 
  1173 \  (let e1_ = hd es_;                                                  \
 
  1174 \       v1_ = hd vs_;                                                  \
 
  1174 \       v1_ = hd v_s;                                                  \
 
  1175 \       e2_ = Take (hd (tl es_));                                      \
 
  1175 \       e2_ = Take (hd (tl es_));                                      \
 
  1176 \       e2_ = (Substitute [e1__]) e2_                                  \
 
  1176 \       e2_ = (Substitute [e1__]) e2_                                  \
 
  1177 \    in [e1_, e2_])";
 
  1177 \    in [e1_, e2_])";
 
  1178 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
  1178 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
  1179 (*---^^^-OK-----------------------------------------------------------------*)
 
  1179 (*---^^^-OK-----------------------------------------------------------------*)
 
  1180 (*---vvv-NOT ok-------------------------------------------------------------*)
 
  1180 (*---vvv-NOT ok-------------------------------------------------------------*)
 
  1181 val str = 
  1181 val str = 
  1182 "Script SolveSystemScript (es_::bool list) (vs_::real list) =          \
 
  1182 "Script SolveSystemScript (es_::bool list) (v_s::real list) =          \
 
  1183 \  (let e1_ = hd es_;                                                  \
 
  1183 \  (let e1_ = hd es_;                                                  \
 
  1184 \       v1_ = hd vs_;                                                  \
 
  1184 \       v1_ = hd v_s;                                                  \
 
  1185 \       xxx = if ((lhs e1_) =!= v1_) then 1 else 2; \
 
  1185 \       xxx = if ((lhs e1_) =!= v1_) then 1 else 2; \
 
  1186 \       e2_ = Take (hd (tl es_));                                      \
 
  1186 \       e2_ = Take (hd (tl es_));                                      \
 
  1187 \       e2_ = (Substitute [e1__]) e2_                                  \
 
  1187 \       e2_ = (Substitute [e1__]) e2_                                  \
 
  1188 \    in [e1_, e2_])";
 
  1188 \    in [e1_, e2_])";
 
  1189 (*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*)
 
  1189 (*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*)
 
  1194 (*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*)
 
  1194 (*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*)
 
  1195 atomty sc; term2str sc;
 
  1195 atomty sc; term2str sc;
 
  1196 
  1196 
  1197 "--- scr [EqSystem,top_down_substitution,4x4] -- adapted only to 7.70";
 
  1197 "--- scr [EqSystem,top_down_substitution,4x4] -- adapted only to 7.70";
 
  1198 val str = 
  1198 val str = 
  1199 "Script SolveSystemScript (es_::bool list) (vs_::real list) =                \
 
  1199 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                \
 
  1200 \  (let e2__ = Take (hd (tl es_));                                           \
 
  1200 \  (let e2__ = Take (hd (tl es_));                                           \
 
  1201 \       e2__ = ((Substitute [e1__]) @@                                       \
 
  1201 \       e2__ = ((Substitute [e1__]) @@                                       \
 
  1202 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
  1202 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
  1203 \                                  simplify_System_parenthesized False)) @@  \
 
  1203 \                                  simplify_System_parenthesized False)) @@  \
 
  1204 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
  1204 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
  1205 \                                  isolate_bdvs False))                  @@  \
 
  1205 \                                  isolate_bdvs False))                  @@  \
 
  1206 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
  1206 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
  1207 \                                  simplify_System False)))             e2__;\
 
  1207 \                                  simplify_System False)))             e2__;\
 
  1208 \       es__ = Take [e1__, e2__]                                             \
 
  1208 \       es__ = Take [e1__, e2__]                                             \
 
  1209 \   in (Try (Rewrite_Set order_system False)) es__)"
 
  1209 \   in (Try (Rewrite_Set order_system False)) es__)"
 
  1210 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
  1210 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
  1211 val str = 
  1211 val str = 
  1212 "Script SolveSystemScript (es_::bool list) (vs_::real list) =                \
 
  1212 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                \
 
  1213 \  (let e2__ = Take (nth_ 2 es_);                                           \
 
  1213 \  (let e2__ = Take (nth_ 2 es_);                                           \
 
  1214 \       e2__ = ((Substitute [e1__]) @@                                       \
 
  1214 \       e2__ = ((Substitute [e1__]) @@                                       \
 
  1215 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
  1215 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
  1216 \                                  simplify_System_parenthesized False)) @@  \
 
  1216 \                                  simplify_System_parenthesized False)) @@  \
 
  1217 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
  1217 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
  1218 \                                  isolate_bdvs False))                  @@  \
 
  1218 \                                  isolate_bdvs False))                  @@  \
 
  1219 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
 
  1219 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
 
  1220 \                                  simplify_System False)))             e2__;\
 
  1220 \                                  simplify_System False)))             e2__;\
 
  1221 \       es__ = Take [e1__, e2__]                                             \
 
  1221 \       es__ = Take [e1__, e2__]                                             \
 
  1222 \   in (Try (Rewrite_Set order_system False)) es__)"
 
  1222 \   in (Try (Rewrite_Set order_system False)) es__)"
 
  1223 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
  1223 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
  1224 val str = 
  1224 val str = 
  1225 "Script SolveSystemScript (es_::bool list) (vs_::real list) =                \
 
  1225 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                \
 
  1226 \  (let e2__ = Take (nth_ 2 es_);                                            \
 
  1226 \  (let e2__ = Take (nth_ 2 es_);                                            \
 
  1227 \       e2__ = ((Substitute [e1__]) @@                                       \
 
  1227 \       e2__ = ((Substitute [e1__]) @@                                       \
 
  1228 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
 
  1228 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)] \
 
  1229 \                                  simplify_System_parenthesized False)) @@  \
 
  1229 \                                  simplify_System_parenthesized False)) @@  \
 
  1230 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)]\
 
  1230 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)]\
 
  1231 \                                  isolate_bdvs False))                  @@  \
 
  1231 \                                  isolate_bdvs False))                  @@  \
 
  1232 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)]\
 
  1232 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)]\
 
  1233 \                                  simplify_System False)))             e2__;\
 
  1233 \                                  simplify_System False)))             e2__;\
 
  1234 \       es__ = Take [e1__, e2__]                                             \
 
  1234 \       es__ = Take [e1__, e2__]                                             \
 
  1235 \   in (Try (Rewrite_Set order_system False)) es__)"
 
  1235 \   in (Try (Rewrite_Set order_system False)) es__)"
 
  1236 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
  1236 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
  1237 val str = 
  1237 val str = 
  1238 "Script SolveSystemScript (es_::bool list) (vs_::real list) =                 \
 
  1238 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                 \
 
  1239 \  (let e2__ = Take (nth_ 2 es_);                                             \
 
  1239 \  (let e2__ = Take (nth_ 2 es_);                                             \
 
  1240 \       e2__ = ((Substitute [e1__]) @@                                        \
 
  1240 \       e2__ = ((Substitute [e1__]) @@                                        \
 
  1241 \               (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
 
  1241 \               (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
 
  1242 \                                       (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
 
  1242 \                                       (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
 
  1243 \                                  simplify_System_parenthesized False)) @@   \
 
  1243 \                                  simplify_System_parenthesized False)) @@   \
 
  1244 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)]  \
 
  1244 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)]  \
 
  1245 \                                  isolate_bdvs False))                  @@   \
 
  1245 \                                  isolate_bdvs False))                  @@   \
 
  1246 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)]  \
 
  1246 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)]  \
 
  1247 \                                  norm_Rational False)))             e2__;   \
 
  1247 \                                  norm_Rational False)))             e2__;   \
 
  1248 \       es__ = Take [e1__, e2__]                                              \
 
  1248 \       es__ = Take [e1__, e2__]                                              \
 
  1249 \   in [])"
 
  1249 \   in [])"
 
  1250 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
  1250 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
  1251 val str = 
  1251 val str = 
  1252 "Script SolveSystemScript (es_::bool list) (vs_::real list) =                 \
 
  1252 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                 \
 
  1253 \  (let e2_ = Take (nth_ 2 es_);                                             \
 
  1253 \  (let e2_ = Take (nth_ 2 es_);                                             \
 
  1254 \       e2_ = ((Substitute [e1_]) @@                                        \
 
  1254 \       e2_ = ((Substitute [e1_]) @@                                        \
 
  1255 \               (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
 
  1255 \               (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
 
  1256 \                                       (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
 
  1256 \                                       (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
 
  1257 \                                  simplify_System_parenthesized False)) @@   \
 
  1257 \                                  simplify_System_parenthesized False)) @@   \
 
  1258 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)]  \
 
  1258 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)]  \
 
  1259 \                                  isolate_bdvs False))                  @@   \
 
  1259 \                                  isolate_bdvs False))                  @@   \
 
  1260 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)]  \
 
  1260 \               (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)]  \
 
  1261 \                                  norm_Rational False)))             e2_;   \
 
  1261 \                                  norm_Rational False)))             e2_;   \
 
  1262 \       es_ = Take [e1_, e2_]                                              \
 
  1262 \       es_ = Take [e1_, e2_]                                              \
 
  1263 \   in [e1_, e2_,e3_, e4_])"
 
  1263 \   in [e1_, e2_,e3_, e4_])"
 
  1264 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
  1264 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
  1265 val str = 
  1265 val str = 
  1266 "Script SolveSystemScript (es_::bool list) (vs_::real list) =                 \
 
  1266 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                 \
 
  1267 \  (let e2_ = Take (nth_ 2 es_);                                              \
 
  1267 \  (let e2_ = Take (nth_ 2 es_);                                              \
 
  1268 \       e2_ = ((Substitute [e1_]) @@                                          \
 
  1268 \       e2_ = ((Substitute [e1_]) @@                                          \
 
  1269 \               (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
 
  1269 \               (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
 
  1270 \                                       (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
 
  1270 \                                       (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
 
  1271 \                                  simplify_System_parenthesized False)) @@   \
 
  1271 \                                  simplify_System_parenthesized False)) @@   \
 
  1272 \               (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
 
  1272 \               (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
 
  1273 \                                       (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
 
  1273 \                                       (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
 
  1274 \                                  isolate_bdvs False))                  @@   \
 
  1274 \                                  isolate_bdvs False))                  @@   \
 
  1275 \               (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
 
  1275 \               (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
 
  1276 \                                       (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
 
  1276 \                                       (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
 
  1277 \                                  norm_Rational False)))             e2_;    \
 
  1277 \                                  norm_Rational False)))             e2_;    \
 
  1278 \       es_ = Take [e1_, e2_]                                                 \
 
  1278 \       es_ = Take [e1_, e2_]                                                 \
 
  1279 \   in [e1_, e2_,e3_, e4_])"
 
  1279 \   in [e1_, e2_,e3_, e4_])"
 
  1280 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
  1280 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
  1281 (*---^^^-OK-----------------------------------------------------------------*)
 
  1281 (*---^^^-OK-----------------------------------------------------------------*)
 
  1282 val str = 
  1282 val str = 
  1283 "Script SolveSystemScript (es_::bool list) (vs_::real list) =                 \
 
  1283 "Script SolveSystemScript (es_::bool list) (v_s::real list) =                 \
 
  1284 \  (let e2_ = Take (nth_ 2 es_);                                              \
 
  1284 \  (let e2_ = Take (nth_ 2 es_);                                              \
 
  1285 \       e2_ = ((Substitute [e1_]) @@                                          \
 
  1285 \       e2_ = ((Substitute [e1_]) @@                                          \
 
  1286 \               (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
 
  1286 \               (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
 
  1287 \                                       (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
 
  1287 \                                       (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
 
  1288 \                                  simplify_System_parenthesized False)) @@   \
 
  1288 \                                  simplify_System_parenthesized False)) @@   \
 
  1289 \               (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
 
  1289 \               (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
 
  1290 \                                       (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
 
  1290 \                                       (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
 
  1291 \                                  isolate_bdvs False))                  @@   \
 
  1291 \                                  isolate_bdvs False))                  @@   \
 
  1292 \               (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
 
  1292 \               (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
 
  1293 \                                       (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
 
  1293 \                                       (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
 
  1294 \                                  norm_Rational False)))             e2_     \
 
  1294 \                                  norm_Rational False)))             e2_     \
 
  1295 \   in [e1_, e2_, nth_ 3 es_, nth_ 4 es_])"
 
  1295 \   in [e1_, e2_, nth_ 3 es_, nth_ 4 es_])"
 
  1296 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
  1296 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 
  1297 (*---vvv-NOT ok-------------------------------------------------------------*)
 
  1297 (*---vvv-NOT ok-------------------------------------------------------------*)
 
  1298 atomty sc; term2str sc;
 
  1298 atomty sc; term2str sc;
wneuper/isa