1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Sep 08 17:20:03 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Sep 08 17:49:36 2010 +0200
1.3 @@ -415,28 +415,28 @@
1.4 store_pbt
1.5 (prep_pbt thy "pbl_equsys" [] e_pblID
1.6 (["system"],
1.7 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.8 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
1.9 ("#Find" ,["solution ss___"](*___ is copy-named*))
1.10 ],
1.11 append_rls "e_rls" e_rls [(*for preds in where_*)],
1.12 - SOME "solveSystem es_ vs_",
1.13 + SOME "solveSystem es_ v_s",
1.14 []));
1.15 store_pbt
1.16 (prep_pbt thy "pbl_equsys_lin" [] e_pblID
1.17 (["linear", "system"],
1.18 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.19 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
1.20 (*TODO.WN050929 check linearity*)
1.21 ("#Find" ,["solution ss___"])
1.22 ],
1.23 append_rls "e_rls" e_rls [(*for preds in where_*)],
1.24 - SOME "solveSystem es_ vs_",
1.25 + SOME "solveSystem es_ v_s",
1.26 []));
1.27 store_pbt
1.28 (prep_pbt thy "pbl_equsys_lin_2x2" [] e_pblID
1.29 (["2x2", "linear", "system"],
1.30 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.31 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.32 - ("#Where" ,["length_ (es_:: bool list) = 2", "length_ vs_ = 2"]),
1.33 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
1.34 + ("#Where" ,["length_ (es_:: bool list) = 2", "length_ v_s = 2"]),
1.35 ("#Find" ,["solution ss___"])
1.36 ],
1.37 append_rls "prls_2x2_linear_system" e_rls
1.38 @@ -445,35 +445,35 @@
1.39 Calc ("op +", eval_binop "#add_"),
1.40 Calc ("op =",eval_equal "#equal_")
1.41 ],
1.42 - SOME "solveSystem es_ vs_",
1.43 + SOME "solveSystem es_ v_s",
1.44 []));
1.45 store_pbt
1.46 (prep_pbt thy "pbl_equsys_lin_2x2_tri" [] e_pblID
1.47 (["triangular", "2x2", "linear", "system"],
1.48 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.49 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
1.50 ("#Where" ,
1.51 - ["(tl vs_) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))",
1.52 - " vs_ from_ vs_ occur_exactly_in (nth_ 2 (es_::bool list))"]),
1.53 + ["(tl v_s) from_ v_s occur_exactly_in (nth_ 1 (es_::bool list))",
1.54 + " v_s from_ v_s occur_exactly_in (nth_ 2 (es_::bool list))"]),
1.55 ("#Find" ,["solution ss___"])
1.56 ],
1.57 prls_triangular,
1.58 - SOME "solveSystem es_ vs_",
1.59 + SOME "solveSystem es_ v_s",
1.60 [["EqSystem","top_down_substitution","2x2"]]));
1.61 store_pbt
1.62 (prep_pbt thy "pbl_equsys_lin_2x2_norm" [] e_pblID
1.63 (["normalize", "2x2", "linear", "system"],
1.64 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.65 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
1.66 ("#Find" ,["solution ss___"])
1.67 ],
1.68 append_rls "e_rls" e_rls [(*for preds in where_*)],
1.69 - SOME "solveSystem es_ vs_",
1.70 + SOME "solveSystem es_ v_s",
1.71 [["EqSystem","normalize","2x2"]]));
1.72 store_pbt
1.73 (prep_pbt thy "pbl_equsys_lin_3x3" [] e_pblID
1.74 (["3x3", "linear", "system"],
1.75 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.76 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.77 - ("#Where" ,["length_ (es_:: bool list) = 3", "length_ vs_ = 3"]),
1.78 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
1.79 + ("#Where" ,["length_ (es_:: bool list) = 3", "length_ v_s = 3"]),
1.80 ("#Find" ,["solution ss___"])
1.81 ],
1.82 append_rls "prls_3x3_linear_system" e_rls
1.83 @@ -482,14 +482,14 @@
1.84 Calc ("op +", eval_binop "#add_"),
1.85 Calc ("op =",eval_equal "#equal_")
1.86 ],
1.87 - SOME "solveSystem es_ vs_",
1.88 + SOME "solveSystem es_ v_s",
1.89 []));
1.90 store_pbt
1.91 (prep_pbt thy "pbl_equsys_lin_4x4" [] e_pblID
1.92 (["4x4", "linear", "system"],
1.93 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.94 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.95 - ("#Where" ,["length_ (es_:: bool list) = 4", "length_ vs_ = 4"]),
1.96 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
1.97 + ("#Where" ,["length_ (es_:: bool list) = 4", "length_ v_s = 4"]),
1.98 ("#Find" ,["solution ss___"])
1.99 ],
1.100 append_rls "prls_4x4_linear_system" e_rls
1.101 @@ -498,34 +498,34 @@
1.102 Calc ("op +", eval_binop "#add_"),
1.103 Calc ("op =",eval_equal "#equal_")
1.104 ],
1.105 - SOME "solveSystem es_ vs_",
1.106 + SOME "solveSystem es_ v_s",
1.107 []));
1.108 store_pbt
1.109 (prep_pbt thy "pbl_equsys_lin_4x4_tri" [] e_pblID
1.110 (["triangular", "4x4", "linear", "system"],
1.111 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.112 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
1.113 ("#Where" , (*accepts missing variables up to diagional form*)
1.114 - ["(nth_ 1 (vs_::real list)) occurs_in (nth_ 1 (es_::bool list))",
1.115 - "(nth_ 2 (vs_::real list)) occurs_in (nth_ 2 (es_::bool list))",
1.116 - "(nth_ 3 (vs_::real list)) occurs_in (nth_ 3 (es_::bool list))",
1.117 - "(nth_ 4 (vs_::real list)) occurs_in (nth_ 4 (es_::bool list))"
1.118 + ["(nth_ 1 (v_s::real list)) occurs_in (nth_ 1 (es_::bool list))",
1.119 + "(nth_ 2 (v_s::real list)) occurs_in (nth_ 2 (es_::bool list))",
1.120 + "(nth_ 3 (v_s::real list)) occurs_in (nth_ 3 (es_::bool list))",
1.121 + "(nth_ 4 (v_s::real list)) occurs_in (nth_ 4 (es_::bool list))"
1.122 ]),
1.123 ("#Find" ,["solution ss___"])
1.124 ],
1.125 append_rls "prls_tri_4x4_lin_sys" prls_triangular
1.126 [Calc ("Atools.occurs'_in",eval_occurs_in "")],
1.127 - SOME "solveSystem es_ vs_",
1.128 + SOME "solveSystem es_ v_s",
1.129 [["EqSystem","top_down_substitution","4x4"]]));
1.130
1.131 store_pbt
1.132 (prep_pbt thy "pbl_equsys_lin_4x4_norm" [] e_pblID
1.133 (["normalize", "4x4", "linear", "system"],
1.134 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.135 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
1.136 (*length_ is checked 1 level above*)
1.137 ("#Find" ,["solution ss___"])
1.138 ],
1.139 append_rls "e_rls" e_rls [(*for preds in where_*)],
1.140 - SOME "solveSystem es_ vs_",
1.141 + SOME "solveSystem es_ v_s",
1.142 [["EqSystem","normalize","4x4"]]));
1.143
1.144
1.145 @@ -553,10 +553,10 @@
1.146 store_met
1.147 (prep_met thy "met_eqsys_topdown_2x2" [] e_metID
1.148 (["EqSystem","top_down_substitution","2x2"],
1.149 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.150 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
1.151 ("#Where" ,
1.152 - ["(tl vs_) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))",
1.153 - " vs_ from_ vs_ occur_exactly_in (nth_ 2 (es_::bool list))"]),
1.154 + ["(tl v_s) from_ v_s occur_exactly_in (nth_ 1 (es_::bool list))",
1.155 + " v_s from_ v_s occur_exactly_in (nth_ 2 (es_::bool list))"]),
1.156 ("#Find" ,["solution ss___"])
1.157 ],
1.158 {rew_ord'="ord_simplify_System", rls' = Erls, calc = [],
1.159 @@ -566,19 +566,19 @@
1.160 Thm ("tl_Nil",num_str @{thm tl_Nil})
1.161 ],
1.162 prls = prls_triangular, crls = Erls, nrls = Erls},
1.163 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^
1.164 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^
1.165 " (let e1__ = Take (hd es_); " ^
1.166 -" e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^
1.167 +" e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
1.168 " isolate_bdvs False)) @@ " ^
1.169 -" (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^
1.170 +" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
1.171 " simplify_System False))) e1__; " ^
1.172 " e2__ = Take (hd (tl es_)); " ^
1.173 " e2__ = ((Substitute [e1__]) @@ " ^
1.174 -" (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^
1.175 +" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
1.176 " simplify_System_parenthesized False)) @@ " ^
1.177 -" (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^
1.178 +" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
1.179 " isolate_bdvs False)) @@ " ^
1.180 -" (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^
1.181 +" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
1.182 " simplify_System False))) e2__; " ^
1.183 " es__ = Take [e1__, e2__] " ^
1.184 " in (Try (Rewrite_Set order_system False)) es__)"
1.185 @@ -587,16 +587,16 @@
1.186 but it does not yet work due to preliminary script-interpreter,
1.187 see eqsystem.sml 'script [EqSystem,top_down_substitution,2x2] Vers.2'
1.188
1.189 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^
1.190 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^
1.191 " (let es__ = Take es_; " ^
1.192 " e1__ = hd es__; " ^
1.193 " e2__ = hd (tl es__); " ^
1.194 " es__ = [e1__, Substitute [e1__] e2__] " ^
1.195 -" in ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^
1.196 +" in ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
1.197 " simplify_System_parenthesized False)) @@ " ^
1.198 -" (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))] " ^
1.199 +" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))] " ^
1.200 " isolate_bdvs False)) @@ " ^
1.201 -" (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^
1.202 +" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
1.203 " simplify_System False))) es__)"
1.204 ---------------------------------------------------------------------------*)
1.205 ));
1.206 @@ -611,7 +611,7 @@
1.207 store_met
1.208 (prep_met thy "met_eqsys_norm_2x2" [] e_metID
1.209 (["EqSystem","normalize","2x2"],
1.210 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.211 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
1.212 ("#Find" ,["solution ss___"])],
1.213 {rew_ord'="tless_true", rls' = Erls, calc = [],
1.214 srls = append_rls "srls_normalize_2x2" e_rls
1.215 @@ -620,17 +620,17 @@
1.216 Thm ("tl_Nil",num_str @{thm tl_Nil})
1.217 ],
1.218 prls = Erls, crls = Erls, nrls = Erls},
1.219 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^
1.220 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^
1.221 " (let es__ = ((Try (Rewrite_Set norm_Rational False)) @@ " ^
1.222 -" (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^
1.223 +" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
1.224 " simplify_System_parenthesized False)) @@ " ^
1.225 -" (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^
1.226 +" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
1.227 " isolate_bdvs False)) @@ " ^
1.228 -" (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^
1.229 +" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
1.230 " simplify_System_parenthesized False)) @@ " ^
1.231 " (Try (Rewrite_Set order_system False))) es_ " ^
1.232 " in (SubProblem (EqSystem_,[linear,system],[no_met]) " ^
1.233 -" [BOOL_LIST es__, REAL_LIST vs_]))"
1.234 +" [BOOL_LIST es__, REAL_LIST v_s]))"
1.235 ));
1.236
1.237 (*this is for nth_ only*)
1.238 @@ -651,7 +651,7 @@
1.239 store_met
1.240 (prep_met thy "met_eqsys_norm_4x4" [] e_metID
1.241 (["EqSystem","normalize","4x4"],
1.242 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.243 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
1.244 ("#Find" ,["solution ss___"])],
1.245 {rew_ord'="tless_true", rls' = Erls, calc = [],
1.246 srls = append_rls "srls_normalize_4x4" srls
1.247 @@ -661,32 +661,32 @@
1.248 ],
1.249 prls = Erls, crls = Erls, nrls = Erls},
1.250 (*GOON met ["EqSystem","normalize","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
1.251 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^
1.252 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^
1.253 " (let es__ = " ^
1.254 " ((Try (Rewrite_Set norm_Rational False)) @@ " ^
1.255 " (Repeat (Rewrite commute_0_equality False)) @@ " ^
1.256 -" (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), " ^
1.257 -" (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] " ^
1.258 +" (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 v_s),(bdv_2, nth_ 2 v_s ), " ^
1.259 +" (bdv_3, nth_ 3 v_s),(bdv_3, nth_ 4 v_s )] " ^
1.260 " simplify_System_parenthesized False)) @@ " ^
1.261 -" (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), " ^
1.262 -" (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] " ^
1.263 +" (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 v_s),(bdv_2, nth_ 2 v_s ), " ^
1.264 +" (bdv_3, nth_ 3 v_s),(bdv_3, nth_ 4 v_s )] " ^
1.265 " isolate_bdvs_4x4 False)) @@ " ^
1.266 -" (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), " ^
1.267 -" (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] " ^
1.268 +" (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 v_s),(bdv_2, nth_ 2 v_s ), " ^
1.269 +" (bdv_3, nth_ 3 v_s),(bdv_3, nth_ 4 v_s )] " ^
1.270 " simplify_System_parenthesized False)) @@ " ^
1.271 " (Try (Rewrite_Set order_system False))) es_ " ^
1.272 " in (SubProblem (EqSystem_,[linear,system],[no_met]) " ^
1.273 -" [BOOL_LIST es__, REAL_LIST vs_]))"
1.274 +" [BOOL_LIST es__, REAL_LIST v_s]))"
1.275 ));
1.276 store_met
1.277 (prep_met thy "met_eqsys_topdown_4x4" [] e_metID
1.278 (["EqSystem","top_down_substitution","4x4"],
1.279 - [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.280 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
1.281 ("#Where" , (*accepts missing variables up to diagonal form*)
1.282 - ["(nth_ 1 (vs_::real list)) occurs_in (nth_ 1 (es_::bool list))",
1.283 - "(nth_ 2 (vs_::real list)) occurs_in (nth_ 2 (es_::bool list))",
1.284 - "(nth_ 3 (vs_::real list)) occurs_in (nth_ 3 (es_::bool list))",
1.285 - "(nth_ 4 (vs_::real list)) occurs_in (nth_ 4 (es_::bool list))"
1.286 + ["(nth_ 1 (v_s::real list)) occurs_in (nth_ 1 (es_::bool list))",
1.287 + "(nth_ 2 (v_s::real list)) occurs_in (nth_ 2 (es_::bool list))",
1.288 + "(nth_ 3 (v_s::real list)) occurs_in (nth_ 3 (es_::bool list))",
1.289 + "(nth_ 4 (v_s::real list)) occurs_in (nth_ 4 (es_::bool list))"
1.290 ]),
1.291 ("#Find" ,["solution ss___"])
1.292 ],
1.293 @@ -696,18 +696,18 @@
1.294 [Calc ("Atools.occurs'_in",eval_occurs_in "")],
1.295 crls = Erls, nrls = Erls},
1.296 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*)
1.297 -"Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^
1.298 +"Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^
1.299 " (let e1_ = nth_ 1 es_; " ^
1.300 " e2_ = Take (nth_ 2 es_); " ^
1.301 " e2_ = ((Substitute [e1_]) @@ " ^
1.302 -" (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_)," ^
1.303 -" (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]" ^
1.304 +" (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s)," ^
1.305 +" (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]" ^
1.306 " simplify_System_parenthesized False)) @@ " ^
1.307 -" (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_)," ^
1.308 -" (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]" ^
1.309 +" (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s)," ^
1.310 +" (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]" ^
1.311 " isolate_bdvs False)) @@ " ^
1.312 -" (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_)," ^
1.313 -" (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]" ^
1.314 +" (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s)," ^
1.315 +" (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]" ^
1.316 " norm_Rational False))) e2_ " ^
1.317 " in [e1_, e2_, nth_ 3 es_, nth_ 4 es_])"
1.318 ));