1.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Sun Feb 09 16:21:26 2020 +0100
1.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Sun Feb 09 16:55:41 2020 +0100
1.3 @@ -16,7 +16,7 @@
1.4 "--------- me .. scripts for maximum-example ---------------------";
1.5 "--------- autoCalc .. scripts for maximum-example ---------------";
1.6
1.7 -"--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------";
1.8 +"--------------------- 30.4.03: maximum .. rewrite_set_ prog_expr ---------";
1.9 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
1.10 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
1.11
1.12 @@ -456,9 +456,9 @@
1.13
1.14
1.15
1.16 -"--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------";
1.17 -"--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------";
1.18 -"--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------";
1.19 +"--------------------- 30.4.03: maximum .. rewrite_set_ prog_expr ---------";
1.20 +"--------------------- 30.4.03: maximum .. rewrite_set_ prog_expr ---------";
1.21 +"--------------------- 30.4.03: maximum .. rewrite_set_ prog_expr ---------";
1.22 str2term
1.23 "Program Maximum_value(f_ix::bool list)(m_m::real) (r_s::bool list)\
1.24 \ (v_v::real) (itv_v::real set) (err_r::bool) = \
1.25 @@ -494,9 +494,9 @@
1.26 term2str s;
1.27 "(hd o filterVar A) [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";
1.28 (*=== inhibit exn 110726=============================================================
1.29 -val SOME (s',_) = rewrite_set_ thy false list_rls s;
1.30 +val SOME (s',_) = rewrite_set_ thy false prog_expr s;
1.31 val s'' = term2str s';
1.32 -if s''="A = a * b" then () else error "new behaviour with list_rls 1.1.";
1.33 +if s''="A = a * b" then () else error "new behaviour with prog_expr 1.1.";
1.34 === inhibit exn 110726=============================================================*)
1.35 val env = env @ [(str2term "e_e::bool",str2term "A = a * b")];
1.36
1.37 @@ -506,9 +506,9 @@
1.38 term2str s;
1.39 "1 < length_h [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";
1.40 (*=== inhibit exn 110726=============================================================
1.41 -val SOME (s',_) = rewrite_set_ thy false list_rls s;
1.42 +val SOME (s',_) = rewrite_set_ thy false prog_expr s;
1.43 val s'' = term2str s';
1.44 -if s''="HOL.True" then () else error "new behaviour with list_rls 1.2.";
1.45 +if s''="HOL.True" then () else error "new behaviour with prog_expr 1.2.";
1.46 === inhibit exn 110726=============================================================*)
1.47
1.48 (*--- 2.line in script ---*)
1.49 @@ -525,13 +525,13 @@
1.50 \ BOOL_LIST [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]\
1.51 \else hd [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";
1.52 (*=== inhibit exn 110726=============================================================
1.53 -val SOME (s',_) = rewrite_set_ thy false list_rls s;
1.54 +val SOME (s',_) = rewrite_set_ thy false prog_expr s;
1.55 val s'' = term2str s';
1.56 if s'' =
1.57 "SubProblem (Reals_s, [make, function], [no_met])\n\
1.58 \ [REAL A, REAL b,\n\
1.59 \ BOOL_LIST [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]" then ()
1.60 -else error "new behaviour with list_rls 1.3.";
1.61 +else error "new behaviour with prog_expr 1.3.";
1.62 === inhibit exn 110726=============================================================*)
1.63 val env = env @ [(str2term "t_t::bool",
1.64 str2term "A = (2*sqrt(r^^^2-(b/2)^^^2)) * b")];
1.65 @@ -565,10 +565,10 @@
1.66 term2str s;
1.67 val t = str2term
1.68 "(hd o filterVar b) [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";
1.69 -val SOME (t',_) = rewrite_set_ thy false list_rls t;
1.70 +val SOME (t',_) = rewrite_set_ thy false prog_expr t;
1.71 val s' = term2str t';
1.72 (*=== inhibit exn 110726=============================================================
1.73 -if s' = "A = a * b" then () else error "new behaviour with list_rls 2.1";
1.74 +if s' = "A = a * b" then () else error "new behaviour with prog_expr 2.1";
1.75 === inhibit exn 110726=============================================================*)
1.76 val env = env @ [(str2term "h_h::bool", str2term s')];
1.77
1.78 @@ -580,12 +580,12 @@
1.79 "hd (dropWhile (ident (A = a * b))\
1.80 \ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2])";
1.81 (*=== inhibit exn 110726=============================================================
1.82 -mem_rls "dropWhile_Cons" list_rls;
1.83 -mem_rls "Prog_Expr.ident" list_rls;
1.84 -val SOME (t',_) = rewrite_set_ thy false list_rls t;
1.85 +mem_rls "dropWhile_Cons" prog_expr;
1.86 +mem_rls "Prog_Expr.ident" prog_expr;
1.87 +val SOME (t',_) = rewrite_set_ thy false prog_expr t;
1.88 val s' = term2str t';
1.89 if s' = "(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2" then ()
1.90 -else error "new behaviour with list_rls 2.2";
1.91 +else error "new behaviour with prog_expr 2.2";
1.92 === inhibit exn 110726=============================================================*)
1.93 val env = env @ [(str2term "e_1::bool", str2term s')];
1.94
1.95 @@ -595,9 +595,9 @@
1.96 term2str s;
1.97 val t = str2term "dropWhile (ident A) (Vars (A = a * b))";
1.98 (*=== inhibit exn 110726=============================================================
1.99 -val SOME (t',_) = rewrite_set_ thy false list_rls t;
1.100 +val SOME (t',_) = rewrite_set_ thy false prog_expr t;
1.101 val s' = term2str t';
1.102 -if s' = "[a, b]" then () else error "new behaviour with list_rls 2.3";
1.103 +if s' = "[a, b]" then () else error "new behaviour with prog_expr 2.3";
1.104 === inhibit exn 110726=============================================================*)
1.105 val env = env @ [(str2term "vs_s::real list", str2term s')];
1.106
1.107 @@ -607,9 +607,9 @@
1.108 term2str s;
1.109 val t = str2term "hd (dropWhile (ident b) [a, b])";
1.110 (*=== inhibit exn 110726=============================================================
1.111 -val SOME (t',_) = rewrite_set_ thy false list_rls t;
1.112 +val SOME (t',_) = rewrite_set_ thy false prog_expr t;
1.113 val s' = term2str t';
1.114 -if s' = "a" then () else error "new behaviour with list_rls 2.4.";
1.115 +if s' = "a" then () else error "new behaviour with prog_expr 2.4.";
1.116 === inhibit exn 110726=============================================================*)
1.117 val env = env @ [(str2term "v_1::real", str2term s')];
1.118
1.119 @@ -631,11 +631,11 @@
1.120 "Substitute [(a = (rhs o hd) [a = 2 * sqrt (r ^^^ 2 - (b / 2) ^^^ 2)])]\n\
1.121 \ (A = a * b)";
1.122 (*=== inhibit exn 110726=============================================================
1.123 -mem_rls "Prog_Expr.rhs" list_rls;
1.124 -val SOME (t',_) = rewrite_set_ thy false list_rls t;
1.125 +mem_rls "Prog_Expr.rhs" prog_expr;
1.126 +val SOME (t',_) = rewrite_set_ thy false prog_expr t;
1.127 val s' = term2str t';
1.128 if s' = "Substitute [a = 2 * sqrt (r ^^^ 2 - (b / 2) ^^^ 2)] (A = a * b)"
1.129 -then () else error "new behaviour with list_rls 2.6.";
1.130 +then () else error "new behaviour with prog_expr 2.6.";
1.131 === inhibit exn 110726=============================================================*)
1.132
1.133
1.134 @@ -672,11 +672,11 @@
1.135 val t = str2term
1.136 "(hd o filterVar A) [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
1.137 trace_rewrite := false;
1.138 -val SOME (t',_) = rewrite_set_ thy false list_rls t;
1.139 +val SOME (t',_) = rewrite_set_ thy false prog_expr t;
1.140 trace_rewrite:=false;
1.141 val s' = term2str t';
1.142 (*=== inhibit exn 110726=============================================================
1.143 -if s' = "A = a * b" then() else error "new behaviour with list_rls 3.1.";
1.144 +if s' = "A = a * b" then() else error "new behaviour with prog_expr 3.1.";
1.145 val env = env @ [(str2term "h_h::bool", str2term s')];
1.146 === inhibit exn 110726=============================================================*)
1.147
1.148 @@ -688,10 +688,10 @@
1.149 "dropWhile (ident (A = a * b))\
1.150 \ [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
1.151 (*=== inhibit exn 110726=============================================================
1.152 -val SOME (t',_) = rewrite_set_ thy false list_rls t;
1.153 +val SOME (t',_) = rewrite_set_ thy false prog_expr t;
1.154 val s' = term2str t';
1.155 if s' = "[a / 2 = r * sin alpha, b / 2 = r * cos alpha]"
1.156 -then () else error "new behaviour with list_rls 3.2.";
1.157 +then () else error "new behaviour with prog_expr 3.2.";
1.158 === inhibit exn 110726=============================================================*)
1.159 val env = env @ [(str2term "es_s::bool list", str2term s')];
1.160
1.161 @@ -701,9 +701,9 @@
1.162 term2str s;
1.163 val t = str2term "dropWhile (ident A) (Vars (A = a * b))";
1.164 (*=== inhibit exn 110726=============================================================
1.165 -val SOME (t',_) = rewrite_set_ thy false list_rls t;
1.166 +val SOME (t',_) = rewrite_set_ thy false prog_expr t;
1.167 val s' = term2str t';
1.168 -if s' = "[a, b]" then () else error "new behaviour with list_rls 3.3.";
1.169 +if s' = "[a, b]" then () else error "new behaviour with prog_expr 3.3.";
1.170 === inhibit exn 110726=============================================================*)
1.171 val env = env @ [(str2term "vs_s::real list", str2term s')];
1.172
1.173 @@ -713,9 +713,9 @@
1.174 term2str s;
1.175 val t = str2term "nth_h 1 [a, b]";
1.176 (*=== inhibit exn 110726=============================================================
1.177 -val SOME (t',_) = rewrite_set_ thy false list_rls t;
1.178 +val SOME (t',_) = rewrite_set_ thy false prog_expr t;
1.179 val s' = term2str t';
1.180 -if s' = "a" then () else error "new behaviour with list_rls 3.4.";
1.181 +if s' = "a" then () else error "new behaviour with prog_expr 3.4.";
1.182 === inhibit exn 110726=============================================================*)
1.183 val env = env @ [(str2term "v_1", str2term s')];
1.184
1.185 @@ -725,9 +725,9 @@
1.186 term2str s;
1.187 val t = str2term "nth_h 2 [a, b]";
1.188 (*=== inhibit exn 110726=============================================================
1.189 -val SOME (t',_) = rewrite_set_ thy false list_rls t;
1.190 +val SOME (t',_) = rewrite_set_ thy false prog_expr t;
1.191 val s' = term2str t';
1.192 -if s' = "b" then () else error "new behaviour with list_rls 3.5.";
1.193 +if s' = "b" then () else error "new behaviour with prog_expr 3.5.";
1.194 === inhibit exn 110726=============================================================*)
1.195 val env = env @ [(str2term "v_2", str2term s')];
1.196
1.197 @@ -737,11 +737,11 @@
1.198 term2str s;
1.199 val t = str2term
1.200 "(hd o filterVar a) [a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
1.201 -val SOME (t',_) = rewrite_set_ thy false list_rls t;
1.202 +val SOME (t',_) = rewrite_set_ thy false prog_expr t;
1.203 val s' = term2str t';
1.204 (*=== inhibit exn 110726=============================================================
1.205 if s' = "a / 2 = r * sin alpha" then ()
1.206 -else error "new behaviour with list_rls 3.6.";
1.207 +else error "new behaviour with prog_expr 3.6.";
1.208 === inhibit exn 110726=============================================================*)
1.209 val e_1 = str2term "e_1::bool";
1.210 val env = env @ [(e_1, str2term s')];
1.211 @@ -752,11 +752,11 @@
1.212 term2str s;
1.213 val t = str2term
1.214 "(hd o filterVar b) [a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
1.215 -val SOME (t',_) = rewrite_set_ thy false list_rls t;
1.216 +val SOME (t',_) = rewrite_set_ thy false prog_expr t;
1.217 val s' = term2str t';
1.218 (*=== inhibit exn 110726=============================================================
1.219 if s' = "b / 2 = r * cos alpha" then ()
1.220 -else error "new behaviour with list_rls 3.7.";
1.221 +else error "new behaviour with prog_expr 3.7.";
1.222 === inhibit exn 110726=============================================================*)
1.223 val env = env @ [(str2term "e_2::bool", str2term s')];
1.224
1.225 @@ -787,11 +787,11 @@
1.226 term2str s;
1.227 "Substitute\n [(a = (rhs o hd) [a = 2 * r * sin alpha]),\
1.228 \ (b = (rhs o hd) [b = 2 * r * cos alpha])] (A = a * b)";
1.229 -val SOME (s',_) = rewrite_set_ thy false list_rls s;
1.230 +val SOME (s',_) = rewrite_set_ thy false prog_expr s;
1.231 val s'' = term2str s';
1.232 (*=== inhibit exn 110726=============================================================
1.233 if s'' =
1.234 "Substitute [a = 2 * r * sin alpha, b = 2 * r * cos alpha] (A = a * b)"
1.235 -then () else error "new behaviour with list_rls 3.10.";
1.236 +then () else error "new behaviour with prog_expr 3.10.";
1.237 ===== inhibit exn 110722===========================================================*)
1.238