1.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Tue Jul 26 15:25:28 2011 +0200
1.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Tue Jul 26 16:09:08 2011 +0200
1.3 @@ -1,4 +1,3 @@
1.4 -
1.5 (* tests for IsacKnowledge/DiffApp
1.6 author Walther Neuper 000301
1.7 (c) due to copyright terms
1.8 @@ -473,62 +472,67 @@
1.9 \ in ((SubProblem (Reals_s,[find_values,tool],[Isac,find_values]) \
1.10 \ [REAL mx_x, REAL (Rhs t_t), REAL v_v, REAL m_m, \
1.11 \ BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list))";
1.12 -(*=== inhibit exn 110722=============================================================
1.13
1.14 val f_ix = (str2term "f_ix::bool list",
1.15 str2term "[r=Arbfix]");
1.16 -val m_ = (str2term "m_::real",
1.17 +val m_m = (str2term "m_m::real",
1.18 str2term "A");
1.19 -val r_s = (str2term "rs_::bool list",
1.20 +val r_s = (str2term "rs_s::bool list",
1.21 str2term "[A = a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]");
1.22 val v_v = (str2term "v_v::real",
1.23 str2term "b");
1.24 -val itv_ = (str2term "itv_v::real set",
1.25 +val itv_v = (str2term "itv_v::real set",
1.26 str2term "{x::real. 0 <= x & x <= 2*r}");
1.27 -val err_ = (str2term "err_::bool",
1.28 +val err_r = (str2term "err_r::bool",
1.29 str2term "eps=0");
1.30 -val env = [f_ix, m_, r_s ,v_, itv_, err_];
1.31 +val env = [f_ix, m_m, r_s ,v_v, itv_v, err_r];
1.32
1.33 (*--- 1.line in script ---*)
1.34 -val t = str2term "(hd o (filterVar m_)) (r_s::bool list)";
1.35 +val t = str2term "(hd o (filterVar m_m)) (r_s::bool list)";
1.36 val s = subst_atomic env t;
1.37 term2str s;
1.38 "(hd o filterVar A) [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";
1.39 +(*=== inhibit exn 110726=============================================================
1.40 val SOME (s',_) = rewrite_set_ thy false list_rls s;
1.41 val s'' = term2str s';
1.42 if s''="A = a * b" then () else error "new behaviour with list_rls 1.1.";
1.43 -val env = env @ [(str2term "e_::bool",str2term "A = a * b")];
1.44 +=== inhibit exn 110726=============================================================*)
1.45 +val env = env @ [(str2term "e_e::bool",str2term "A = a * b")];
1.46
1.47 (*--- 2.line: condition alone ---*)
1.48 -val t = str2term "1 < length_ (r_s::bool list)";
1.49 +val t = str2term "1 < length_h (r_s::bool list)";
1.50 val s = subst_atomic env t;
1.51 term2str s;
1.52 -"1 < length_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";
1.53 +"1 < length_h [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";
1.54 +(*=== inhibit exn 110726=============================================================
1.55 val SOME (s',_) = rewrite_set_ thy false list_rls s;
1.56 val s'' = term2str s';
1.57 if s''="HOL.True" then () else error "new behaviour with list_rls 1.2.";
1.58 +=== inhibit exn 110726=============================================================*)
1.59
1.60 (*--- 2.line in script ---*)
1.61 val t = str2term
1.62 - "(if 1 < length_ r_s \
1.63 - \ then (SubProblem (Reals_,[make,function],[no_met])\
1.64 - \ [REAL m_, REAL v_v, BOOL_LIST r_s])\
1.65 + "(if 1 < length_h r_s \
1.66 + \ then (SubProblem (Reals_s,[make,function],[no_met])\
1.67 + \ [REAL m_m, REAL v_v, BOOL_LIST r_s])\
1.68 \ else (hd r_s))";
1.69 val s = subst_atomic env t;
1.70 term2str s;
1.71 -"if 1 < length_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]\
1.72 -\then SubProblem (Reals_, [make, function], [no_met])\
1.73 +"if 1 < length_h [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]\
1.74 +\then SubProblem (Reals_s, [make, function], [no_met])\
1.75 \ [REAL A, REAL b,\
1.76 \ BOOL_LIST [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]\
1.77 \else hd [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";
1.78 +(*=== inhibit exn 110726=============================================================
1.79 val SOME (s',_) = rewrite_set_ thy false list_rls s;
1.80 val s'' = term2str s';
1.81 if s'' =
1.82 -"SubProblem (Reals_, [make, function], [no_met])\n\
1.83 +"SubProblem (Reals_s, [make, function], [no_met])\n\
1.84 \ [REAL A, REAL b,\n\
1.85 \ BOOL_LIST [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]" then ()
1.86 else error "new behaviour with list_rls 1.3.";
1.87 -val env = env @ [(str2term "t_::bool",
1.88 +=== inhibit exn 110726=============================================================*)
1.89 +val env = env @ [(str2term "t_t::bool",
1.90 str2term "A = (2*sqrt(r^^^2-(b/2)^^^2)) * b")];
1.91
1.92
1.93 @@ -539,14 +543,14 @@
1.94 str2term
1.95 "Script Make_fun_by_explicit (f_f::real) (v_v::real) \
1.96 \ (eqs::bool list) = \
1.97 - \ (let h_ = (hd o (filterVar f_)) eqs; \
1.98 - \ e_1 = hd (dropWhile (ident h_) eqs); \
1.99 - \ v_s = dropWhile (ident f_) (Vars h_); \
1.100 + \ (let h_h = (hd o (filterVar f_f)) eqs; \
1.101 + \ e_1 = hd (dropWhile (ident h_h) eqs); \
1.102 + \ v_s = dropWhile (ident f_f) (Vars h_h); \
1.103 \ v_1 = hd (dropWhile (ident v_v) v_s); \
1.104 - \ (s_1::bool list)=(SubProblem(Reals_,[univar,equation],[no_met])\
1.105 + \ (s_1::bool list)=(SubProblem(Reals_s,[univar,equation],[no_met])\
1.106 \ [BOOL e_1, REAL v_1])\
1.107 - \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)";
1.108 -val f_ = (str2term "f_f::real",
1.109 + \ in Substitute [(v_1 = (rhs o hd) s_1)] h_h)";
1.110 +val f_f = (str2term "f_f::real",
1.111 str2term "A");
1.112 val v_v = (str2term "v_v::real",
1.113 str2term "b");
1.114 @@ -562,66 +566,76 @@
1.115 "(hd o filterVar b) [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";
1.116 val SOME (t',_) = rewrite_set_ thy false list_rls t;
1.117 val s' = term2str t';
1.118 +(*=== inhibit exn 110726=============================================================
1.119 if s' = "A = a * b" then () else error "new behaviour with list_rls 2.1";
1.120 -val env = env @ [(str2term "h_::bool", str2term s')];
1.121 +=== inhibit exn 110726=============================================================*)
1.122 +val env = env @ [(str2term "h_h::bool", str2term s')];
1.123
1.124 (*--- 2.line in script ---*)
1.125 -val t = str2term "hd (dropWhile (ident h_) (eqs::bool list))";
1.126 +val t = str2term "hd (dropWhile (ident h_h) (eqs::bool list))";
1.127 val s = subst_atomic env t;
1.128 term2str s;
1.129 val t = str2term
1.130 "hd (dropWhile (ident (A = a * b))\
1.131 \ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2])";
1.132 +(*=== inhibit exn 110726=============================================================
1.133 mem_rls "dropWhile_Cons" list_rls;
1.134 mem_rls "Atools.ident" list_rls;
1.135 val SOME (t',_) = rewrite_set_ thy false list_rls t;
1.136 val s' = term2str t';
1.137 if s' = "(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2" then ()
1.138 else error "new behaviour with list_rls 2.2";
1.139 +=== inhibit exn 110726=============================================================*)
1.140 val env = env @ [(str2term "e_1::bool", str2term s')];
1.141
1.142 (*--- 3.line in script ---*)
1.143 -val t = str2term "dropWhile (ident f_) (Vars (h_::bool))";
1.144 +val t = str2term "dropWhile (ident f_f) (Vars (h_h::bool))";
1.145 val s = subst_atomic env t;
1.146 term2str s;
1.147 val t = str2term "dropWhile (ident A) (Vars (A = a * b))";
1.148 +(*=== inhibit exn 110726=============================================================
1.149 val SOME (t',_) = rewrite_set_ thy false list_rls t;
1.150 val s' = term2str t';
1.151 if s' = "[a, b]" then () else error "new behaviour with list_rls 2.3";
1.152 -val env = env @ [(str2term "vs_::real list", str2term s')];
1.153 +=== inhibit exn 110726=============================================================*)
1.154 +val env = env @ [(str2term "vs_s::real list", str2term s')];
1.155
1.156 (*--- 4.line in script ---*)
1.157 val t = str2term "hd (dropWhile (ident v_v) v_s)";
1.158 val s = subst_atomic env t;
1.159 term2str s;
1.160 val t = str2term "hd (dropWhile (ident b) [a, b])";
1.161 +(*=== inhibit exn 110726=============================================================
1.162 val SOME (t',_) = rewrite_set_ thy false list_rls t;
1.163 val s' = term2str t';
1.164 if s' = "a" then () else error "new behaviour with list_rls 2.4.";
1.165 +=== inhibit exn 110726=============================================================*)
1.166 val env = env @ [(str2term "v_1::real", str2term s')];
1.167
1.168 (*--- 5.line in script ---*)
1.169 -val t = str2term "(SubProblem(Reals_,[univar,equation],[no_met])\
1.170 +val t = str2term "(SubProblem(Reals_s,[univar,equation],[no_met])\
1.171 \ [BOOL e_1, REAL v_1])";
1.172 val s = subst_atomic env t;
1.173 term2str s;
1.174 -"SubProblem (Reals_, [univar, equation], [no_met])\n\
1.175 +"SubProblem (Reals_s, [univar, equation], [no_met])\n\
1.176 \ [BOOL ((a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2), REAL a]";
1.177 val env = env @ [(str2term "s_1::bool list",
1.178 str2term "[a = 2 * sqrt (r^^^2 - (b/2)^^^2)]")];
1.179
1.180 (*--- 6.line in script ---*)
1.181 -val t = str2term "Substitute [(v_1 = (rhs o hd) (s_1::bool list))] (h_::bool)";
1.182 +val t = str2term "Substitute [(v_1 = (rhs o hd) (s_1::bool list))] (h_h::bool)";
1.183 val s = subst_atomic env t;
1.184 term2str s;
1.185 val t = str2term
1.186 "Substitute [(a = (rhs o hd) [a = 2 * sqrt (r ^^^ 2 - (b / 2) ^^^ 2)])]\n\
1.187 \ (A = a * b)";
1.188 +(*=== inhibit exn 110726=============================================================
1.189 mem_rls "Tools.rhs" list_rls;
1.190 val SOME (t',_) = rewrite_set_ thy false list_rls t;
1.191 val s' = term2str t';
1.192 if s' = "Substitute [a = 2 * sqrt (r ^^^ 2 - (b / 2) ^^^ 2)] (A = a * b)"
1.193 then () else error "new behaviour with list_rls 2.6.";
1.194 +=== inhibit exn 110726=============================================================*)
1.195
1.196
1.197 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
1.198 @@ -630,18 +644,18 @@
1.199 str2term
1.200 "Script Make_fun_by_new_variable (f_f::real) (v_v::real) \
1.201 \ (eqs::bool list) = \
1.202 - \(let h_ = (hd o (filterVar f_)) eqs; \
1.203 - \ es_ = dropWhile (ident h_) eqs; \
1.204 - \ v_s = dropWhile (ident f_) (Vars h_); \
1.205 - \ v_1 = nth_ 1 v_s; \
1.206 - \ v_2 = nth_ 2 v_s; \
1.207 - \ e_1 = (hd o (filterVar v_1)) es_; \
1.208 - \ e_2 = (hd o (filterVar v_2)) es_; \
1.209 - \ (s_1::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\
1.210 + \(let h_h = (hd o (filterVar f_f)) eqs; \
1.211 + \ es_s = dropWhile (ident h_h) eqs; \
1.212 + \ v_s = dropWhile (ident f_f) (Vars h_h); \
1.213 + \ v_1 = nth_h 1 v_s; \
1.214 + \ v_2 = nth_h 2 v_s; \
1.215 + \ e_1 = (hd o (filterVar v_1)) es_s; \
1.216 + \ e_2 = (hd o (filterVar v_2)) es_s; \
1.217 + \ (s_1::bool list) = (SubProblem (Reals_s,[univar,equation],[no_met])\
1.218 \ [BOOL e_1, REAL v_1]);\
1.219 - \ (s_2::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\
1.220 + \ (s_2::bool list) = (SubProblem (Reals_s,[univar,equation],[no_met])\
1.221 \ [BOOL e_2, REAL v_2])\
1.222 - \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)";
1.223 + \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_h)";
1.224 val f_ = (str2term "f_f::real",
1.225 str2term "A");
1.226 val v_v = (str2term "v_v::real",
1.227 @@ -660,89 +674,103 @@
1.228 val SOME (t',_) = rewrite_set_ thy false list_rls t;
1.229 trace_rewrite:=false;
1.230 val s' = term2str t';
1.231 +(*=== inhibit exn 110726=============================================================
1.232 if s' = "A = a * b" then() else error "new behaviour with list_rls 3.1.";
1.233 -val env = env @ [(str2term "h_::bool", str2term s')];
1.234 +val env = env @ [(str2term "h_h::bool", str2term s')];
1.235 +=== inhibit exn 110726=============================================================*)
1.236
1.237 (*--- 2.line in script ---*)
1.238 -val t = str2term "dropWhile (ident (h_::bool)) (eqs::bool list)";
1.239 +val t = str2term "dropWhile (ident (h_h::bool)) (eqs::bool list)";
1.240 val s = subst_atomic env t;
1.241 term2str s;
1.242 val t = str2term
1.243 "dropWhile (ident (A = a * b))\
1.244 \ [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
1.245 +(*=== inhibit exn 110726=============================================================
1.246 val SOME (t',_) = rewrite_set_ thy false list_rls t;
1.247 val s' = term2str t';
1.248 if s' = "[a / 2 = r * sin alpha, b / 2 = r * cos alpha]"
1.249 then () else error "new behaviour with list_rls 3.2.";
1.250 -val env = env @ [(str2term "es_::bool list", str2term s')];
1.251 +=== inhibit exn 110726=============================================================*)
1.252 +val env = env @ [(str2term "es_s::bool list", str2term s')];
1.253
1.254 (*--- 3.line in script ---*)
1.255 -val t = str2term "dropWhile (ident (f_f::real)) (Vars (h_::bool))";
1.256 +val t = str2term "dropWhile (ident (f_f::real)) (Vars (h_h::bool))";
1.257 val s = subst_atomic env t;
1.258 term2str s;
1.259 val t = str2term "dropWhile (ident A) (Vars (A = a * b))";
1.260 +(*=== inhibit exn 110726=============================================================
1.261 val SOME (t',_) = rewrite_set_ thy false list_rls t;
1.262 val s' = term2str t';
1.263 if s' = "[a, b]" then () else error "new behaviour with list_rls 3.3.";
1.264 -val env = env @ [(str2term "vs_::real list", str2term s')];
1.265 +=== inhibit exn 110726=============================================================*)
1.266 +val env = env @ [(str2term "vs_s::real list", str2term s')];
1.267
1.268 (*--- 4.line in script ---*)
1.269 -val t = str2term "nth_ 1 v_s";
1.270 +val t = str2term "nth_h 1 v_s";
1.271 val s = subst_atomic env t;
1.272 term2str s;
1.273 -val t = str2term "nth_ 1 [a, b]";
1.274 +val t = str2term "nth_h 1 [a, b]";
1.275 +(*=== inhibit exn 110726=============================================================
1.276 val SOME (t',_) = rewrite_set_ thy false list_rls t;
1.277 val s' = term2str t';
1.278 if s' = "a" then () else error "new behaviour with list_rls 3.4.";
1.279 +=== inhibit exn 110726=============================================================*)
1.280 val env = env @ [(str2term "v_1", str2term s')];
1.281
1.282 (*--- 5.line in script ---*)
1.283 -val t = str2term "nth_ 2 v_s";
1.284 +val t = str2term "nth_h 2 v_s";
1.285 val s = subst_atomic env t;
1.286 term2str s;
1.287 -val t = str2term "nth_ 2 [a, b]";
1.288 +val t = str2term "nth_h 2 [a, b]";
1.289 +(*=== inhibit exn 110726=============================================================
1.290 val SOME (t',_) = rewrite_set_ thy false list_rls t;
1.291 val s' = term2str t';
1.292 if s' = "b" then () else error "new behaviour with list_rls 3.5.";
1.293 +=== inhibit exn 110726=============================================================*)
1.294 val env = env @ [(str2term "v_2", str2term s')];
1.295
1.296 (*--- 6.line in script ---*)
1.297 -val t = str2term "(hd o (filterVar v_1)) (es_::bool list)";
1.298 +val t = str2term "(hd o (filterVar v_1)) (es_s::bool list)";
1.299 val s = subst_atomic env t;
1.300 term2str s;
1.301 val t = str2term
1.302 "(hd o filterVar a) [a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
1.303 val SOME (t',_) = rewrite_set_ thy false list_rls t;
1.304 val s' = term2str t';
1.305 +(*=== inhibit exn 110726=============================================================
1.306 if s' = "a / 2 = r * sin alpha" then ()
1.307 else error "new behaviour with list_rls 3.6.";
1.308 +=== inhibit exn 110726=============================================================*)
1.309 val e_1 = str2term "e_1::bool";
1.310 val env = env @ [(e_1, str2term s')];
1.311
1.312 (*--- 7.line in script ---*)
1.313 -val t = str2term "(hd o (filterVar v_2)) (es_::bool list)";
1.314 +val t = str2term "(hd o (filterVar v_2)) (es_s::bool list)";
1.315 val s = subst_atomic env t;
1.316 term2str s;
1.317 val t = str2term
1.318 "(hd o filterVar b) [a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
1.319 val SOME (t',_) = rewrite_set_ thy false list_rls t;
1.320 val s' = term2str t';
1.321 +(*=== inhibit exn 110726=============================================================
1.322 if s' = "b / 2 = r * cos alpha" then ()
1.323 else error "new behaviour with list_rls 3.7.";
1.324 +=== inhibit exn 110726=============================================================*)
1.325 val env = env @ [(str2term "e_2::bool", str2term s')];
1.326
1.327 (*--- 8.line in script ---*)
1.328 -val t = str2term "(SubProblem (Reals_,[univar,equation],[no_met])\
1.329 +val t = str2term "(SubProblem (Reals_s,[univar,equation],[no_met])\
1.330 \ [BOOL e_1, REAL v_1])";
1.331 val s = subst_atomic env t;
1.332 term2str s;
1.333 -"SubProblem (Reals_, [univar, equation], [no_met])\
1.334 +"SubProblem (Reals_s, [univar, equation], [no_met])\
1.335 \ [BOOL (a / 2 = r * sin alpha), REAL a]";
1.336 val s_1 = str2term "[a = 2*r*sin alpha]";
1.337 val env = env @ [(str2term "s_1::bool list", s_1)];
1.338
1.339 (*--- 9.line in script ---*)
1.340 -val t = str2term "(SubProblem (Reals_,[univar,equation],[no_met])\
1.341 +val t = str2term "(SubProblem (Reals_s,[univar,equation],[no_met])\
1.342 \ [BOOL e_2, REAL v_2])";
1.343 val s = subst_atomic env t;
1.344 term2str s;
1.345 @@ -753,19 +781,16 @@
1.346
1.347 (*--- 10.line in script ---*)
1.348 val t = str2term
1.349 -"Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] (h_::bool)";
1.350 +"Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] (h_h::bool)";
1.351 val s = subst_atomic env t;
1.352 term2str s;
1.353 "Substitute\n [(a = (rhs o hd) [a = 2 * r * sin alpha]),\
1.354 \ (b = (rhs o hd) [b = 2 * r * cos alpha])] (A = a * b)";
1.355 val SOME (s',_) = rewrite_set_ thy false list_rls s;
1.356 val s'' = term2str s';
1.357 +(*=== inhibit exn 110726=============================================================
1.358 if s'' =
1.359 "Substitute [a = 2 * r * sin alpha, b = 2 * r * cos alpha] (A = a * b)"
1.360 then () else error "new behaviour with list_rls 3.10.";
1.361 -
1.362 -
1.363 -
1.364 ===== inhibit exn 110722===========================================================*)
1.365
1.366 -
2.1 --- a/test/Tools/isac/Test_Some.thy Tue Jul 26 15:25:28 2011 +0200
2.2 +++ b/test/Tools/isac/Test_Some.thy Tue Jul 26 16:09:08 2011 +0200
2.3 @@ -11,6 +11,8 @@
2.4
2.5 ML {*
2.6
2.7 +
2.8 +
2.9 *}
2.10 ML{*
2.11 *}