1.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Wed Sep 08 17:20:03 2010 +0200
1.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Wed Sep 08 17:49:36 2010 +0200
1.3 @@ -101,7 +101,7 @@
1.4 atomty (term_of t);
1.5
1.6 val t = str2term
1.7 -"(tl (tl (tl vs_))) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))";
1.8 +"(tl (tl (tl v_s))) from_ v_s occur_exactly_in (nth_ 1 (es_::bool list))";
1.9 atomty t;
1.10 val t = str2term
1.11 "(tl (tl (tl [c,c_2,c_3,c_4]))) from_ [c,c_2,c_3,c_4] occur_exactly_in \
1.12 @@ -284,99 +284,99 @@
1.13 "----------- script [EqSystem,normalize,2x2] ---------------------";
1.14 "----------- script [EqSystem,normalize,2x2] ---------------------";
1.15 val str =
1.16 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.17 -\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.18 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.19 +\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.20 \ simplify_System_parenthesized False) es_ \
1.21 \ in ([]))";
1.22 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.23 val str =
1.24 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.25 -\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.26 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.27 +\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.28 \ simplify_System_parenthesized False) es_ \
1.29 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
1.30 \ []))";
1.31 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.32 val str =
1.33 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.34 -\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.35 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.36 +\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.37 \ simplify_System_parenthesized False) es_ \
1.38 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
1.39 -\ [BOOL_LIST es__, REAL_LIST vs_]))"
1.40 +\ [BOOL_LIST es__, REAL_LIST v_s]))"
1.41 ;
1.42 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.43 val str =
1.44 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.45 -\ (let es__ = Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.46 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.47 +\ (let es__ = Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.48 \ simplify_System_parenthesized False) es_ \
1.49 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
1.50 -\ [BOOL_LIST es__, REAL_LIST vs_]))"
1.51 +\ [BOOL_LIST es__, REAL_LIST v_s]))"
1.52 ;
1.53 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.54 val str =
1.55 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.56 -\ (let es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.57 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.58 +\ (let es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.59 \ simplify_System_parenthesized False)) es_ \
1.60 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
1.61 -\ [BOOL_LIST es__, REAL_LIST vs_]))"
1.62 +\ [BOOL_LIST es__, REAL_LIST v_s]))"
1.63 ;
1.64 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.65 val str =
1.66 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.67 -\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.68 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.69 +\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.70 \ simplify_System_parenthesized False)) @@\
1.71 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.72 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.73 \ simplify_System_parenthesized False))) es_\
1.74 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
1.75 -\ [BOOL_LIST es__, REAL_LIST vs_]))"
1.76 +\ [BOOL_LIST es__, REAL_LIST v_s]))"
1.77 ;
1.78 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.79 val str =
1.80 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.81 -\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.82 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.83 +\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.84 \ simplify_System_parenthesized False)) @@\
1.85 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.86 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.87 \ simplify_System_parenthesized False)) @@\
1.88 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.89 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.90 \ simplify_System_parenthesized False))) es_\
1.91 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
1.92 -\ [BOOL_LIST es__, REAL_LIST vs_]))"
1.93 +\ [BOOL_LIST es__, REAL_LIST v_s]))"
1.94 ;
1.95 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.96 val str =
1.97 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.98 -\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.99 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.100 +\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.101 \ simplify_System_parenthesized False)) @@\
1.102 \ (Try (Rewrite_Set_Inst [] isolate_bdvs False)) @@\
1.103 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.104 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.105 \ simplify_System_parenthesized False)) @@\
1.106 \ (Try (Rewrite_Set order_system False))) es_\
1.107 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
1.108 -\ [BOOL_LIST es__, REAL_LIST vs_]))"
1.109 +\ [BOOL_LIST es__, REAL_LIST v_s]))"
1.110 ;
1.111 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.112 val str =
1.113 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.114 -\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.115 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.116 +\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.117 \ simplify_System_parenthesized False)) @@\
1.118 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_)]\
1.119 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s)]\
1.120 \ isolate_bdvs False)) @@\
1.121 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.122 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.123 \ simplify_System_parenthesized False)) @@\
1.124 \ (Try (Rewrite_Set order_system False))) es_\
1.125 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
1.126 -\ [BOOL_LIST es__, REAL_LIST vs_]))"
1.127 +\ [BOOL_LIST es__, REAL_LIST v_s]))"
1.128 ;
1.129 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.130 val str =
1.131 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.132 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.133 \ (let es__ = ((Try (Rewrite_Set simplify_System_parenthesized False)) @@\
1.134 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.135 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.136 \ isolate_bdvs False)) @@\
1.137 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.138 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.139 \ simplify_System_parenthesized False)) @@\
1.140 \ (Try (Rewrite_Set order_system False))) es_\
1.141 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
1.142 -\ [BOOL_LIST es__, REAL_LIST vs_]))"
1.143 +\ [BOOL_LIST es__, REAL_LIST v_s]))"
1.144 ;
1.145 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.146 (*---^^^-OK-----------------------------------------------------------------*)
1.147 @@ -387,127 +387,127 @@
1.148 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
1.149 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
1.150 val str =
1.151 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.152 -\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.153 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.154 +\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.155 \ simplify_System_parenthesized False) es_ \
1.156 \ in ([]))";
1.157 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.158 val str =
1.159 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.160 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.161 \ (let e1__ = Take (hd es_) \
1.162 \ in ([]))";
1.163 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.164 val str =
1.165 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.166 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.167 \ (let e1__ = Take (hd es_); \
1.168 \ e1__ = Take (hd es_) \
1.169 \ in ([]))";
1.170 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.171 val str =
1.172 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.173 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.174 \ (let e1__ = Take (hd es_); \
1.175 \ e1__ = (Take (hd es_))\
1.176 \ in ([]))";
1.177 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.178 val str =
1.179 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.180 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.181 \ (let e1__ = Take (hd es_); \
1.182 \ e1__ = ((Rewrite_Set order_system False)) e1__\
1.183 \ in ([]))";
1.184 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.185 (*--------------------------------------------------------------------------*)
1.186 val str =
1.187 -"(Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.188 +"(Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.189 \ isolate_bdvs False) (e1__::bool)";
1.190 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.191 (*--------------------------------------------------------------------------*)
1.192 val str =
1.193 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.194 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.195 \ (let e1__ = Take (hd es_); \
1.196 -\ e1__ = ((Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.197 +\ e1__ = ((Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.198 \ isolate_bdvs False)) e1__\
1.199 \ in ([]))";
1.200 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.201 val str =
1.202 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.203 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.204 \ (let e1__ = Take (hd es_); \
1.205 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.206 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.207 \ isolate_bdvs False)) @@\
1.208 -\ (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.209 +\ (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.210 \ simplify_System False)) e1__\
1.211 \ in ([]))";
1.212 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.213 val str =
1.214 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.215 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.216 \ (let e1__ = Take (hd es_); \
1.217 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.218 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.219 \ isolate_bdvs False)) @@\
1.220 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.221 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.222 \ simplify_System False))) e1__\
1.223 \ in ([]))";
1.224 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.225 val str =
1.226 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.227 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.228 \ (let e1__ = Take (hd es_); \
1.229 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.230 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.231 \ isolate_bdvs False)) @@ \
1.232 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.233 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.234 \ simplify_System False))) e1__; \
1.235 \ e2__ = Take (hd (tl es_)) \
1.236 \ in ([]))";
1.237 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.238 val str =
1.239 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.240 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.241 \ (let e1__ = Take (hd es_); \
1.242 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.243 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.244 \ isolate_bdvs False)) @@ \
1.245 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.246 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.247 \ simplify_System False))) e1__; \
1.248 \ e2__ = Take (hd (tl es_)); \
1.249 \ e2__ = Substitute [e1__] e2__ \
1.250 \ in ([]))";
1.251 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.252 val str =
1.253 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.254 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.255 \ (let e1__ = Take (hd es_); \
1.256 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.257 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.258 \ isolate_bdvs False)) @@ \
1.259 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.260 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.261 \ simplify_System False))) e1__; \
1.262 \ e2__ = Take (hd (tl es_)); \
1.263 \ e2__ = ((Substitute [e1__])) e2__ \
1.264 \ in ([]))";
1.265 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.266 val str =
1.267 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.268 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.269 \ (let e1__ = Take (hd es_); \
1.270 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.271 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.272 \ isolate_bdvs False)) @@ \
1.273 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.274 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.275 \ simplify_System False))) e1__; \
1.276 \ e2__ = Take (hd (tl es_)); \
1.277 \ e2__ = ((Substitute [e1__]) @@ \
1.278 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.279 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.280 \ isolate_bdvs False)) @@ \
1.281 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.282 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.283 \ simplify_System False))) e2__ \
1.284 \ in [e1__, e2__])"
1.285 ;
1.286 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.287 val str =
1.288 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.289 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.290 \ (let e1__ = Take (hd es_); \
1.291 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.292 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.293 \ isolate_bdvs False)) @@ \
1.294 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.295 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.296 \ simplify_System False))) e1__; \
1.297 \ e2__ = Take (hd (tl es_)); \
1.298 \ e2__ = ((Substitute [e1__]) @@ \
1.299 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.300 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.301 \ simplify_System_parenthesized False)) @@ \
1.302 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.303 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.304 \ isolate_bdvs False)) @@ \
1.305 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.306 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.307 \ simplify_System False)) @@ \
1.308 \ (Try (Rewrite_Set order_system False))) e2__ \
1.309 \ in [e1__, e2__])"
1.310 @@ -515,19 +515,19 @@
1.311 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.312 (*---^^^-OK-----------------------------------------------------------------*)
1.313 val str =
1.314 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.315 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.316 \ (let e1__ = Take (hd es_); \
1.317 -\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.318 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.319 \ isolate_bdvs False)) @@ \
1.320 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.321 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.322 \ simplify_System False))) e1__; \
1.323 \ e2__ = Take (hd (tl es_)); \
1.324 \ e2__ = ((Substitute [e1__]) @@ \
1.325 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.326 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.327 \ simplify_System_parenthesized False)) @@ \
1.328 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.329 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.330 \ isolate_bdvs False)) @@ \
1.331 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.332 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.333 \ simplify_System False))) e2__; \
1.334 \ es__ = Take [e1__, e2__]\
1.335 \ in (Try (Rewrite_Set order_system False)) es__)"
1.336 @@ -540,14 +540,14 @@
1.337 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
1.338 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
1.339 val str =
1.340 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.341 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.342 \ (let es__ = Take es_; \
1.343 \ e1__ = hd es__\
1.344 \ in ([]))"
1.345 ;
1.346 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.347 val str =
1.348 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.349 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.350 \ (let es__ = Take es_; \
1.351 \ e1__ = hd es__; \
1.352 \ e2__ = hd (tl es__)\
1.353 @@ -555,7 +555,7 @@
1.354 ;
1.355 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.356 val str =
1.357 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.358 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.359 \ (let es__ = Take es_; \
1.360 \ e1__ = hd es__; \
1.361 \ e2__ = hd (tl es__);\
1.362 @@ -564,7 +564,7 @@
1.363 ;
1.364 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.365 val str =
1.366 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.367 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.368 \ (let es__ = Take es_; \
1.369 \ e1__ = hd es__; \
1.370 \ e2__ = hd (tl es__);\
1.371 @@ -573,87 +573,87 @@
1.372 ;
1.373 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.374 val str =
1.375 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.376 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.377 \ (let es__ = Take es_; \
1.378 \ e1__ = hd es__; \
1.379 \ e2__ = hd (tl es__);\
1.380 \ es__ = [e1__, Substitute [e1__] e2__];\
1.381 -\ es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.382 +\ es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.383 \ simplify_System False)) es__ \
1.384 \ in ([]))"
1.385 ;
1.386 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.387 val str =
1.388 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.389 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.390 \ (let es__ = Take es_; \
1.391 \ e1__ = hd es__; \
1.392 \ e2__ = hd (tl es__);\
1.393 \ es__ = [e1__, Substitute [e1__] e2__];\
1.394 -\ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.395 +\ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.396 \ isolate_bdvs False)) @@ \
1.397 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.398 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.399 \ simplify_System False))) es__ \
1.400 \ in ([]))"
1.401 ;
1.402 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.403 val str =
1.404 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.405 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.406 \ (let es__ = Take es_; \
1.407 \ e1__ = hd es__; \
1.408 \ e2__ = hd (tl es__);\
1.409 \ es__ = [e1__, Substitute [e1__] e2__];\
1.410 -\ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.411 +\ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.412 \ simplify_System_parenthesized False)) @@ \
1.413 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.414 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.415 \ isolate_bdvs False)) @@ \
1.416 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.417 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.418 \ simplify_System False))) es__ \
1.419 \ in ([]))"
1.420 ;
1.421 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.422 val str =
1.423 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.424 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.425 \ (let es__ = Take es_; \
1.426 \ e1__ = hd es__; \
1.427 \ e2__ = hd (tl es__); \
1.428 \ es__ = [e1__, Substitute [e1__] e2__]; \
1.429 -\ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.430 +\ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.431 \ simplify_System_parenthesized False)) @@ \
1.432 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.433 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.434 \ isolate_bdvs False)) @@ \
1.435 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.436 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.437 \ simplify_System False))) es__ \
1.438 \ in es__)"
1.439 ;
1.440 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.441 val str =
1.442 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.443 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.444 \ (let es__ = Take es_; \
1.445 \ e1__ = hd es__; \
1.446 \ e2__ = hd (tl es__); \
1.447 \ es__ = [e1__, Substitute [e1__] e2__] \
1.448 -\ in ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.449 +\ in ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.450 \ simplify_System_parenthesized False)) @@ \
1.451 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))] \
1.452 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))] \
1.453 \ isolate_bdvs False)) @@ \
1.454 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.455 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.456 \ simplify_System False))) es__)"
1.457 ;
1.458 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.459 (*---^^^-OK-----------------------------------------------------------------*)
1.460 val str =
1.461 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.462 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.463 \ (let es__ = Take es_; \
1.464 \ e1__ = hd es__; \
1.465 \ e2__ = hd (tl es__); \
1.466 \ es__ = [e1__, Substitute [e1__] e2__] "^
1.467 (* this ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ is a script-'Expr'
1.468 which is not yet searched for 'STac's; thus this script does not yet work*)
1.469 -" in ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.470 +" in ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.471 \ simplify_System_parenthesized False)) @@ \
1.472 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))] \
1.473 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))] \
1.474 \ isolate_bdvs False)) @@ \
1.475 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.476 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.477 \ simplify_System False))) es__)"
1.478 ;
1.479 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.480 @@ -791,14 +791,14 @@
1.481 (* val (thy, (pblID, dsc_dats: (string * (string list)) list,
1.482 ev:rls, ca: string option, metIDs:metID list)) =
1.483 (EqSystem.thy, (["system"],
1.484 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.485 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
1.486 ("#Find" ,["solution ss___"](*___ is copy-named*))
1.487 ],
1.488 append_rls "e_rls" e_rls [(*for preds in where_*)],
1.489 - SOME "solveSystem es_ vs_",
1.490 + SOME "solveSystem es_ v_s",
1.491 []));
1.492 *)
1.493 -> val [("#Given", [equalities_es_, "solveForVars vs_"])] = gi;
1.494 +> val [("#Given", [equalities_es_, "solveForVars v_s"])] = gi;
1.495 val equalities_es_ = "equalities es_" : string
1.496 > val (dd, ii) = (split_did o term_of o the o (parse thy)) equalities_es_;
1.497 > show_types:=true; term2str ii; show_types:=false;
1.498 @@ -819,7 +819,7 @@
1.499 [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
1.500 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2] ,(es_, [[0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
1.501 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]])),
1.502 -(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])),
1.503 +(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
1.504 (3 ,[1] ,true ,#Find ,Cor solution L ,(ss___, [L]))]
1.505
1.506 > (writeln o pres2str) pre';
1.507 @@ -837,7 +837,7 @@
1.508 ["
1.509 (es_, [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
1.510 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2])","
1.511 -(vs_, [c, c_2])","
1.512 +(v_s, [c, c_2])","
1.513 (ss___, L)"]
1.514
1.515 > val es_ = (fst o hd) env;
1.516 @@ -899,7 +899,7 @@
1.517 (writeln o (itms2str_ (thy2ctxt "Isac"))) probl;
1.518 (*[
1.519 (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]])),
1.520 -(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])),
1.521 +(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
1.522 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
1.523 *)
1.524 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.525 @@ -968,7 +968,7 @@
1.526 (writeln o (itms2str_ (thy2ctxt "Isac"))) probl;
1.527 (*[
1.528 (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]])),
1.529 -(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])),
1.530 +(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
1.531 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
1.532 *)
1.533 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.534 @@ -1155,23 +1155,23 @@
1.535 "--- scr [EqSystem,top_down_substitution,4x4] -- a saved trial";
1.536 (*---vvv-this script failed with if ?!?-------------------------------------*)
1.537 val str =
1.538 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.539 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.540 \ (let e1_ = hd es_; \
1.541 -\ v1_ = hd vs_; \
1.542 +\ v1_ = hd v_s; \
1.543 \ xxx = if lhs e1_ =!= v1_ \
1.544 \ then 0=0 \
1.545 \ else let e1_ = Take e1_; \
1.546 -\ e1_ = (Rewrite_Set_Inst [(bdv_1, hd vs_), \
1.547 -\ (bdv_2, hd (tl vs_))] \
1.548 +\ e1_ = (Rewrite_Set_Inst [(bdv_1, hd v_s), \
1.549 +\ (bdv_2, hd (tl v_s))] \
1.550 \ isolate_bdvs False) e1_; \
1.551 \ e2_ = Take (hd (tl es_)); \
1.552 \ e2_ = (Substitute [e1__]) e2_ \
1.553 \ in [e1_, e2_])";
1.554 (*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*)
1.555 val str =
1.556 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.557 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.558 \ (let e1_ = hd es_; \
1.559 -\ v1_ = hd vs_; \
1.560 +\ v1_ = hd v_s; \
1.561 \ e2_ = Take (hd (tl es_)); \
1.562 \ e2_ = (Substitute [e1__]) e2_ \
1.563 \ in [e1_, e2_])";
1.564 @@ -1179,9 +1179,9 @@
1.565 (*---^^^-OK-----------------------------------------------------------------*)
1.566 (*---vvv-NOT ok-------------------------------------------------------------*)
1.567 val str =
1.568 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.569 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.570 \ (let e1_ = hd es_; \
1.571 -\ v1_ = hd vs_; \
1.572 +\ v1_ = hd v_s; \
1.573 \ xxx = if ((lhs e1_) =!= v1_) then 1 else 2; \
1.574 \ e2_ = Take (hd (tl es_)); \
1.575 \ e2_ = (Substitute [e1__]) e2_ \
1.576 @@ -1196,101 +1196,101 @@
1.577
1.578 "--- scr [EqSystem,top_down_substitution,4x4] -- adapted only to 7.70";
1.579 val str =
1.580 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.581 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.582 \ (let e2__ = Take (hd (tl es_)); \
1.583 \ e2__ = ((Substitute [e1__]) @@ \
1.584 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.585 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.586 \ simplify_System_parenthesized False)) @@ \
1.587 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.588 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.589 \ isolate_bdvs False)) @@ \
1.590 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.591 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.592 \ simplify_System False))) e2__;\
1.593 \ es__ = Take [e1__, e2__] \
1.594 \ in (Try (Rewrite_Set order_system False)) es__)"
1.595 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.596 val str =
1.597 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.598 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.599 \ (let e2__ = Take (nth_ 2 es_); \
1.600 \ e2__ = ((Substitute [e1__]) @@ \
1.601 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.602 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.603 \ simplify_System_parenthesized False)) @@ \
1.604 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.605 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.606 \ isolate_bdvs False)) @@ \
1.607 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1.608 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\
1.609 \ simplify_System False))) e2__;\
1.610 \ es__ = Take [e1__, e2__] \
1.611 \ in (Try (Rewrite_Set order_system False)) es__)"
1.612 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.613 val str =
1.614 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.615 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.616 \ (let e2__ = Take (nth_ 2 es_); \
1.617 \ e2__ = ((Substitute [e1__]) @@ \
1.618 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
1.619 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)] \
1.620 \ simplify_System_parenthesized False)) @@ \
1.621 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)]\
1.622 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)]\
1.623 \ isolate_bdvs False)) @@ \
1.624 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)]\
1.625 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)]\
1.626 \ simplify_System False))) e2__;\
1.627 \ es__ = Take [e1__, e2__] \
1.628 \ in (Try (Rewrite_Set order_system False)) es__)"
1.629 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.630 val str =
1.631 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.632 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.633 \ (let e2__ = Take (nth_ 2 es_); \
1.634 \ e2__ = ((Substitute [e1__]) @@ \
1.635 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
1.636 -\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
1.637 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
1.638 +\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
1.639 \ simplify_System_parenthesized False)) @@ \
1.640 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
1.641 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)] \
1.642 \ isolate_bdvs False)) @@ \
1.643 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
1.644 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)] \
1.645 \ norm_Rational False))) e2__; \
1.646 \ es__ = Take [e1__, e2__] \
1.647 \ in [])"
1.648 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.649 val str =
1.650 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.651 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.652 \ (let e2_ = Take (nth_ 2 es_); \
1.653 \ e2_ = ((Substitute [e1_]) @@ \
1.654 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
1.655 -\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
1.656 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
1.657 +\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
1.658 \ simplify_System_parenthesized False)) @@ \
1.659 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
1.660 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)] \
1.661 \ isolate_bdvs False)) @@ \
1.662 -\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
1.663 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, nth_ 2 v_s)] \
1.664 \ norm_Rational False))) e2_; \
1.665 \ es_ = Take [e1_, e2_] \
1.666 \ in [e1_, e2_,e3_, e4_])"
1.667 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.668 val str =
1.669 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.670 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.671 \ (let e2_ = Take (nth_ 2 es_); \
1.672 \ e2_ = ((Substitute [e1_]) @@ \
1.673 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
1.674 -\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
1.675 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
1.676 +\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
1.677 \ simplify_System_parenthesized False)) @@ \
1.678 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
1.679 -\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
1.680 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
1.681 +\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
1.682 \ isolate_bdvs False)) @@ \
1.683 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
1.684 -\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
1.685 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
1.686 +\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
1.687 \ norm_Rational False))) e2_; \
1.688 \ es_ = Take [e1_, e2_] \
1.689 \ in [e1_, e2_,e3_, e4_])"
1.690 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.691 (*---^^^-OK-----------------------------------------------------------------*)
1.692 val str =
1.693 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1.694 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = \
1.695 \ (let e2_ = Take (nth_ 2 es_); \
1.696 \ e2_ = ((Substitute [e1_]) @@ \
1.697 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
1.698 -\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
1.699 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
1.700 +\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
1.701 \ simplify_System_parenthesized False)) @@ \
1.702 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
1.703 -\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
1.704 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
1.705 +\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
1.706 \ isolate_bdvs False)) @@ \
1.707 -\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
1.708 -\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
1.709 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s),\
1.710 +\ (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]\
1.711 \ norm_Rational False))) e2_ \
1.712 \ in [e1_, e2_, nth_ 3 es_, nth_ 4 es_])"
1.713 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;