1.1 --- a/src/Tools/isac/TODO.thy Wed Apr 01 12:42:39 2020 +0200
1.2 +++ b/src/Tools/isac/TODO.thy Wed Apr 01 14:14:46 2020 +0200
1.3 @@ -32,38 +32,6 @@
1.4 \item xxx
1.5 \item xxx
1.6 \item xxx
1.7 - \item xxx
1.8 - \item xxx
1.9 - \item xxx
1.10 - \item xxx
1.11 - \item xxx
1.12 - \item xxx
1.13 - \item xxx
1.14 - \item xxx
1.15 - \item xxx
1.16 - \item xxx
1.17 - \item xxx
1.18 - \item xxx
1.19 - \item xxx
1.20 - \item xxx
1.21 - \item xxx
1.22 - \item xxx
1.23 - \item xxx
1.24 - \item xxx
1.25 - \item xxx
1.26 - \item xxx
1.27 - \item xxx
1.28 - \item xxx
1.29 - \item xxx
1.30 - \item xxx
1.31 - \item Istate_Def.empty -> Istate.empty
1.32 - \item xxx
1.33 - \item xxx
1.34 - \item xxx
1.35 - \item distribute test/../scrtools.sml: WAIT FOR FINAL CLEANUP OF src/../Interpret
1.36 - \item cleanup test-files: test/.. tools.sml, atools.sml, ...
1.37 - \item xxx
1.38 - \item xxx
1.39 \end{itemize}
1.40 \<close>
1.41 subsection \<open>Postponed from current changeset\<close>
2.1 --- a/test/Tools/isac/Knowledge/atools.sml Wed Apr 01 12:42:39 2020 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,414 +0,0 @@
2.4 -(* tests on Prog_Expr.thy and Prog_Expr.ML
2.5 - author: Walther Neuper
2.6 - 050814, 08:51
2.7 - (c) due to copyright terms
2.8 -
2.9 -use"../smltest/IsacKnowledge/atools.sml";
2.10 -use"atools.sml";
2.11 -*)
2.12 -
2.13 -(*default_print_depth 5;*)
2.14 -"--------------------------------------------------------";
2.15 -"table of contents --------------------------------------";
2.16 -"--------------------------------------------------------";
2.17 -"----------- occurs_in ----------------------------------";
2.18 -"----------- fun occurs_in ---------------------------------------------------------------------";
2.19 -"----------- argument_of --------------------------------";
2.20 -"----------- sameFunId ----------------------------------";
2.21 -"----------- filter_sameFunId ---------------------------";
2.22 -"----------- boollist2sum -------------------------------";
2.23 -"----------- Matthias Goldgruber 2003 rewrite orders ----";
2.24 -(*"----------- introduction by MG 2003 --------------------";*)
2.25 -"----------- fun eval_binop -----------------------------";
2.26 -"--------------------------------------------------------";
2.27 -
2.28 -
2.29 -val thy = @{theory "Prog_Expr"};
2.30 -
2.31 -"----------- occurs_in -------------------------------------------";
2.32 -"----------- occurs_in -------------------------------------------";
2.33 -"----------- occurs_in -------------------------------------------";
2.34 -(*=========================================================================*)
2.35 -fun str2t str = (Thm.term_of o the o (parse thy)) str;
2.36 -fun term2s t = term_to_string''' thy t;
2.37 -(*=========================================================================*)
2.38 -
2.39 -val t = str2t "x";
2.40 -if occurs_in t t then "OK" else error "occurs_in x x -> f ..changed";
2.41 -
2.42 -val t = str2term "x occurs_in x";
2.43 -val SOME (str, t') = eval_occurs_in 0 "Prog_Expr.occurs'_in" t 0;
2.44 -if term2str t' = "x occurs_in x = True" then ()
2.45 -else error "x occurs_in x = True ..changed";
2.46 -
2.47 -"------- some_occur_in";
2.48 -some_occur_in [str2t"c",str2t"c_2"] (str2t"a + b + c");
2.49 -val t = str2t "some_of [c, c_2, c_3, c_4] occur_in \
2.50 - \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
2.51 -val SOME (str,t') = eval_some_occur_in 0 "Prog_Expr.some'_occur'_in" t 0;
2.52 -if term2str t' =
2.53 - "some_of [c, c_2, c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 =\nTrue" then ()
2.54 -else error "atools.sml: some_occur_in true";
2.55 -
2.56 -val t = str2t "some_of [c_3, c_4] occur_in \
2.57 - \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
2.58 -val SOME (str,t') = eval_some_occur_in 0 "Prog_Expr.some'_occur'_in" t 0;
2.59 -if term2str t' =
2.60 - "some_of [c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False" then ()
2.61 -else error "atools.sml: some_occur_in false";
2.62 -
2.63 -"----------- fun occurs_in ---------------------------------------------------------------------";
2.64 -"----------- fun occurs_in ---------------------------------------------------------------------";
2.65 -"----------- fun occurs_in ---------------------------------------------------------------------";
2.66 -val v = (Thm.term_of o the o (parse thy)) "x";
2.67 -val t = (Thm.term_of o the o (parse thy)) "1";
2.68 -if occurs_in v t then error "factor_right_deg (1) x ..changed" else ();
2.69 -
2.70 -val v = (Thm.term_of o the o (parse thy)) "AA";
2.71 -val t = (Thm.term_of o the o (parse thy)) "1";
2.72 -if occurs_in v t then error "factor_right_deg (1) AA ..changed" else ();
2.73 -
2.74 -(*----------*)
2.75 -val v = (Thm.term_of o the o (parse thy)) "x";
2.76 -val t = (Thm.term_of o the o (parse thy)) "a*b+c";
2.77 -if occurs_in v t then error "factor_right_deg (a*b+c) x ..changed" else ();
2.78 -
2.79 -val v = (Thm.term_of o the o (parse thy)) "AA";
2.80 -val t = (Thm.term_of o the o (parse thy)) "a*b+c";
2.81 -if occurs_in v t then error "factor_right_deg (a*b+c) AA ..changed" else ();
2.82 -
2.83 -(*----------*)
2.84 -val v = (Thm.term_of o the o (parse thy)) "x";
2.85 -val t = (Thm.term_of o the o (parse thy)) "a*x+c";
2.86 -if occurs_in v t then () else error "factor_right_deg (a*x+c) x ..changed";
2.87 -
2.88 -val v = (Thm.term_of o the o (parse thy)) "AA";
2.89 -val t = (Thm.term_of o the o (parse thy)) "a*AA+c";
2.90 -if occurs_in v t then () else error "factor_right_deg (a*AA+c) AA ..changed";
2.91 -
2.92 -(*----------*)
2.93 -val v = (Thm.term_of o the o (parse thy)) "x";
2.94 -val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*x^^^7";
2.95 -if occurs_in v t then () else error "factor_right_deg (a*b+c)*x^^^7) x ..changed";
2.96 -
2.97 -val v = (Thm.term_of o the o (parse thy)) "AA";
2.98 -val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*AA^^^7";
2.99 -if occurs_in v t then () else error "factor_right_deg (a*b+c)*AA^^^7) AA ..changed";
2.100 -
2.101 -(*----------*)
2.102 -val v = (Thm.term_of o the o (parse thy)) "x";
2.103 -val t = (Thm.term_of o the o (parse thy)) "x^^^7";
2.104 -if occurs_in v t then () else error "factor_right_deg (x^^^7) x ..changed";
2.105 -
2.106 -val v = (Thm.term_of o the o (parse thy)) "AA";
2.107 -val t = (Thm.term_of o the o (parse thy)) "AA^^^7";
2.108 -if occurs_in v t then () else error "factor_right_deg (AA^^^7) AA ..changed";
2.109 -
2.110 -(*----------*)
2.111 -val v = (Thm.term_of o the o (parse thy)) "x";
2.112 -val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*x";
2.113 -if occurs_in v t then () else error "factor_right_deg ((a*b+c)*x) x ..changed";
2.114 -
2.115 -val v = (Thm.term_of o the o (parse thy)) "AA";
2.116 -val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*AA";
2.117 -if occurs_in v t then () else error "factor_right_deg ((a*b+c)*AA) AA ..changed";
2.118 -
2.119 -(*----------*)
2.120 -val v = (Thm.term_of o the o (parse thy)) "x";
2.121 -val t = (Thm.term_of o the o (parse thy)) "(a*b+x)*x";
2.122 -if occurs_in v t then () else error "factor_right_deg ((a*b+x)*x) x ..changed";
2.123 -
2.124 -val v = (Thm.term_of o the o (parse thy)) "AA";
2.125 -val t = (Thm.term_of o the o (parse thy)) "(a*b+AA)*AA";
2.126 -if occurs_in v t then () else error "factor_right_deg ((a*b+AA)*AA) AA ..changed";
2.127 -
2.128 -(*----------*)
2.129 -val v = (Thm.term_of o the o (parse thy)) "x";
2.130 -val t = (Thm.term_of o the o (parse thy)) "x";
2.131 -if occurs_in v t then () else error "factor_right_deg (x) x ..changed";
2.132 -
2.133 -val v = (Thm.term_of o the o (parse thy)) "AA";
2.134 -val t = (Thm.term_of o the o (parse thy)) "AA";
2.135 -if occurs_in v t then () else error "factor_right_deg (AA) AA ..changed";
2.136 -
2.137 -(*----------*)
2.138 -val v = (Thm.term_of o the o (parse thy)) "x";
2.139 -val t = (Thm.term_of o the o (parse thy)) "ab - (a*b)*x";
2.140 -if occurs_in v t then () else error "factor_right_deg (ab - (a*b)*x) x ..changed";
2.141 -
2.142 -val v = (Thm.term_of o the o (parse thy)) "AA";
2.143 -val t = (Thm.term_of o the o (parse thy)) "ab - (a*b)*AA";
2.144 -if occurs_in v t then () else error "factor_right_deg (ab - (a*b)*AA) AA ..changed";
2.145 -
2.146 -"----------- argument_of -----------------------------------------";
2.147 -"----------- argument_of -----------------------------------------";
2.148 -"----------- argument_of -----------------------------------------";
2.149 -val t = str2term "argument_in (M_b x)";
2.150 -val SOME (str, t') = eval_argument_in "0" "Prog_Expr.argument'_in" t 0;
2.151 -if term2str t' = "(argument_in M_b x) = x" then ()
2.152 -else error "atools.sml:(argument_in M_b x) = x ???";
2.153 -
2.154 -"----------- sameFunId -------------------------------------------";
2.155 -"----------- sameFunId -------------------------------------------";
2.156 -"----------- sameFunId -------------------------------------------";
2.157 -val t = str2t "M_b L"; atomty t;
2.158 -val t as f1 $ _ = str2t "M_b L";
2.159 -val t as Const ("HOL.eq", _) $ (f2 $ _) $ _ = str2t "M_b x = c + L*x";
2.160 -f1 = f2 (*true*);
2.161 -val (p as Const ("Prog_Expr.sameFunId",_) $
2.162 - (f1 $ _) $
2.163 - (Const ("HOL.eq", _) $ (f2 $ _) $ _)) =
2.164 - str2t "sameFunId (M_b L) (M_b x = c + L*x)";
2.165 -f1 = f2 (*true*);
2.166 -eval_sameFunId "" "Prog_Expr.sameFunId"
2.167 - (str2t "sameFunId (M_b L) (M_b x = c + L*x)")""(*true*);
2.168 -eval_sameFunId "" "Prog_Expr.sameFunId"
2.169 - (str2t "sameFunId (M_b L) ( y' x = c + L*x)")""(*false*);
2.170 -eval_sameFunId "" "Prog_Expr.sameFunId"
2.171 - (str2t "sameFunId (M_b L) ( y x = c + L*x)")""(*false*);
2.172 -eval_sameFunId "" "Prog_Expr.sameFunId"
2.173 - (str2t "sameFunId ( y L) (M_b x = c + L*x)")""(*false*);
2.174 -eval_sameFunId "" "Prog_Expr.sameFunId"
2.175 - (str2t "sameFunId ( y L) ( y x = c + L*x)")""(*true*);
2.176 -
2.177 -"----------- filter_sameFunId ------------------------------------";
2.178 -"----------- filter_sameFunId ------------------------------------";
2.179 -"----------- filter_sameFunId ------------------------------------";
2.180 -val flhs as (fid $ _) = str2t "y' L";
2.181 -val fs = str2t "[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]";
2.182 -val (p as Const ("Prog_Expr.filter'_sameFunId",_) $ (fid $ _) $ fs) =
2.183 - str2t "filter_sameFunId (y' L) \
2.184 - \[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]";
2.185 -val SOME (str, es) = eval_filter_sameFunId "" "Prog_Expr.filter'_sameFunId" p "";
2.186 -if term2str es = "(filter_sameFunId y' L [M_b x = c + L * x, y' x = c + L * x,\n y x = c + L * x]) =\n[y' x = c + L * x]" then ()
2.187 -else error "atools.slm diff.behav. in filter_sameFunId";
2.188 -
2.189 -
2.190 -"----------- boollist2sum ----------------------------------------";
2.191 -"----------- boollist2sum ----------------------------------------";
2.192 -"----------- boollist2sum ----------------------------------------";
2.193 -fun lhs (Const ("HOL.eq",_) $ l $ _) = l
2.194 - | lhs t = error("lhs called with (" ^ term2str t ^ ")");
2.195 -"-----------^^^redefined due to overwritten identifier -----------";
2.196 -val u_ = str2t "[]";
2.197 -val u_ = str2t "[b1 = k - 2*q]";
2.198 -val u_ = str2t "[b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";
2.199 -val ut_ = isalist2list u_;
2.200 -val sum_ = map lhs ut_;
2.201 -val t = list2sum sum_;
2.202 -term2str t;
2.203 -
2.204 -val t = str2t
2.205 - "boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";
2.206 -
2.207 -val p as Const ("Prog_Expr.boollist2sum", _) $ (Const ("List.list.Cons", _) $
2.208 - _ $ _) = t;
2.209 -
2.210 -
2.211 -val SOME (str, pred) = eval_boollist2sum "" "Prog_Expr.boollist2sum" t "";
2.212 -if term2str pred = "boollist2sum\n [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q] =\nb1 + b2 + b3 + b4" then ()
2.213 -else error "atools.sml diff.behav. in eval_boollist2sum";
2.214 -
2.215 -trace_rewrite := false;
2.216 -val srls_ = append_rls "srls_..Berechnung-erstSymbolisch" e_rls
2.217 - [Num_Calc ("Prog_Expr.boollist2sum", eval_boollist2sum "")];
2.218 -val t = str2t
2.219 - "boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";
2.220 -case rewrite_set_ thy false srls_ t of SOME _ => ()
2.221 -| _ => error "atools.sml diff.rewrite boollist2sum";
2.222 -trace_rewrite:=false;
2.223 -
2.224 -
2.225 -"----------- Matthias Goldgruber 2003 rewrite orders ----";
2.226 -"----------- Matthias Goldgruber 2003 rewrite orders ----";
2.227 -"----------- Matthias Goldgruber 2003 rewrite orders ----";
2.228 -(* MK die ersten Tests *)
2.229 - val substa = [(e_term, (Thm.term_of o the o (parse thy)) "a")];
2.230 - val substb = [(e_term, (Thm.term_of o the o (parse thy)) "b")];
2.231 - val substx = [(e_term, (Thm.term_of o the o (parse thy)) "x")];
2.232 -
2.233 - val x1 = (Thm.term_of o the o (parse thy)) "a + b + x";
2.234 - val x2 = (Thm.term_of o the o (parse thy)) "a + x + b";
2.235 - val x3 = (Thm.term_of o the o (parse thy)) "a + x + b";
2.236 - val x4 = (Thm.term_of o the o (parse thy)) "x + a + b";
2.237 -
2.238 -if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
2.239 -else error "termorder.sml diff.behav ord_make_polynomial_in #1";
2.240 -
2.241 -if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then ()
2.242 -else error "termorder.sml diff.behav ord_make_polynomial_in #2";
2.243 -
2.244 -if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
2.245 -else error "termorder.sml diff.behav ord_make_polynomial_in #3";
2.246 -
2.247 - val aa = (Thm.term_of o the o (parse thy)) "-1 * a * x";
2.248 - val bb = (Thm.term_of o the o (parse thy)) "x^^^3";
2.249 - ord_make_polynomial_in true thy substx (aa, bb);
2.250 - true; (* => LESS *)
2.251 -
2.252 - val aa = (Thm.term_of o the o (parse thy)) "-1 * a * x";
2.253 - val bb = (Thm.term_of o the o (parse thy)) "x^^^3";
2.254 - ord_make_polynomial_in true thy substa (aa, bb);
2.255 - false; (* => GREATER *)
2.256 -
2.257 -(* und nach dem Re-engineering der Termorders in den 'rulesets'
2.258 - kannst Du die 'gr"osste' Variable frei w"ahlen: *)
2.259 - val bdv= (Thm.term_of o the o (parse thy)) "''bdv''";
2.260 - val x = (Thm.term_of o the o (parse thy)) "x";
2.261 - val a = (Thm.term_of o the o (parse thy)) "a";
2.262 - val b = (Thm.term_of o the o (parse thy)) "b";
2.263 -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
2.264 -if term2str t' = "b + x + a" then ()
2.265 -else error "termorder.sml diff.behav ord_make_polynomial_in #11";
2.266 -
2.267 -val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
2.268 -
2.269 -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
2.270 -if term2str t' = "a + b + x" then ()
2.271 -else error "termorder.sml diff.behav ord_make_polynomial_in #13";
2.272 -
2.273 - val ppp' = "-6 + -5*x + x^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2";
2.274 - val ppp = (Thm.term_of o the o (parse thy)) ppp';
2.275 -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
2.276 -if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
2.277 -else error "termorder.sml diff.behav ord_make_polynomial_in #14";
2.278 -
2.279 -val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
2.280 -if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
2.281 -else error "termorder.sml diff.behav ord_make_polynomial_in #15";
2.282 -
2.283 - val ttt' = "(3*x + 5)/18";
2.284 - val ttt = (Thm.term_of o the o (parse thy)) ttt';
2.285 -val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
2.286 -if term2str uuu = "(5 + 3 * x) / 18" then ()
2.287 -else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
2.288 -
2.289 -(*============ inhibit exn WN120316 ==============================================
2.290 -val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
2.291 -if term2str uuu = "(5 + 3 * x) / 18" then ()
2.292 -else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
2.293 -============ inhibit exn WN120316 ==============================================*)
2.294 -
2.295 -
2.296 -"----------- introduction by MG 2003 --------------------";
2.297 -"----------- introduction by MG 2003 --------------------";
2.298 -"----------- introduction by MG 2003 --------------------";
2.299 -(*##################################################################################
2.300 ------------28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
2.301 -
2.302 - (*Aufgabe zum Einstieg in die Arbeit...*)
2.303 - val t = (Thm.term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2 = 0";
2.304 - (*ein 'ruleset' aus Poly.ML wird angewandt...*)
2.305 - val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
2.306 - term2str t;
2.307 - "a * b + (-1 * (a * x) + (-1 * (b * x) + x ^^^ 2)) = 0";
2.308 - val SOME (t,_) =
2.309 - rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;
2.310 - term2str t;
2.311 - "x ^^^ 2 + (-1 * (b * x) + (-1 * (x * a) + b * a)) = 0";
2.312 -(* bei Verwendung von "size_of-term" nach MG :*)
2.313 -(*"x ^^^ 2 + (-1 * (b * x) + (b * a + -1 * (x * a))) = 0" !!! *)
2.314 -
2.315 - (*wir holen 'a' wieder aus der Klammerung heraus...*)
2.316 - val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;
2.317 - term2str t;
2.318 - "x ^^^ 2 + -1 * b * x + -1 * x * a + b * a = 0";
2.319 -(* "x ^^^ 2 + -1 * b * x + b * a + -1 * x * a = 0" !!! *)
2.320 -
2.321 - val SOME (t,_) =
2.322 - rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;
2.323 - term2str t;
2.324 - "x ^^^ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0";
2.325 - (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
2.326 - "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)
2.327 -
2.328 - (*das rewriting l"asst sich beobachten mit
2.329 -trace_rewrite := false;
2.330 - *)
2.331 -
2.332 -"------15.11.02 --------------------------";
2.333 - val t = (Thm.term_of o the o (parse thy)) "1 + a * x + b * x";
2.334 - val bdv = (Thm.term_of o the o (parse thy)) "bdv";
2.335 - val a = (Thm.term_of o the o (parse thy)) "a";
2.336 -
2.337 -trace_rewrite := false;
2.338 - (* Anwenden einer Regelmenge aus Termorder.ML: *)
2.339 - val SOME (t,_) =
2.340 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
2.341 - term2str t;
2.342 - val SOME (t,_) =
2.343 - rewrite_set_ thy false discard_parentheses t;
2.344 - term2str t;
2.345 -"1 + b * x + x * a";
2.346 -
2.347 - val t = (Thm.term_of o the o (parse thy)) "1 + a * (x + b * x) + a^^^2";
2.348 - val SOME (t,_) =
2.349 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
2.350 - term2str t;
2.351 - val SOME (t,_) =
2.352 - rewrite_set_ thy false discard_parentheses t;
2.353 - term2str t;
2.354 -"1 + (x + b * x) * a + a ^^^ 2";
2.355 -
2.356 - val t = (Thm.term_of o the o (parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2";
2.357 - val SOME (t,_) =
2.358 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
2.359 - term2str t;
2.360 - val SOME (t,_) =
2.361 - rewrite_set_ thy false discard_parentheses t;
2.362 - term2str t;
2.363 -"1 + b * a + (7 + x) * a ^^^ 2";
2.364 -
2.365 -(* MG2003
2.366 - Prog_Expr.thy grundlegende Algebra
2.367 - Poly.thy Polynome
2.368 - Rational.thy Br"uche
2.369 - Root.thy Wurzeln
2.370 - RootRat.thy Wurzen + Br"uche
2.371 - Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03)
2.372 -
2.373 - get_thm Termorder.thy "bdv_n_collect";
2.374 - get_thm (theory "Isac_Knowledge") "bdv_n_collect";
2.375 -*)
2.376 - val t = (Thm.term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2";
2.377 - val SOME (t,_) =
2.378 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
2.379 - term2str t;
2.380 - val SOME (t,_) =
2.381 - rewrite_set_ thy false discard_parentheses t;
2.382 - term2str t;
2.383 -"(7 + x) * a ^^^ 2";
2.384 -
2.385 - val t = (Thm.term_of o the o (parse Termorder.thy)) "Pi";
2.386 -
2.387 - val t = (Thm.term_of o the o (parseold thy)) "7";
2.388 -##################################################################################*)
2.389 -
2.390 -"----------- fun eval_binop -----------------------------";
2.391 -"----------- fun eval_binop -----------------------------";
2.392 -"----------- fun eval_binop -----------------------------";
2.393 -val (op_, ef) = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "TIMES"));
2.394 -val t = (Thm.term_of o the o (parse thy)) "2 * 3";
2.395 -(*val SOME (thmid,t') = *)get_pair thy op_ ef t;
2.396 -;
2.397 -"~~~~~ fun get_pair, args:"; val (thy, op_, ef, (t as (Const (op0,_) $ t1 $ t2))) =
2.398 - (thy, op_, ef, t);
2.399 -op_ = op0 = true;
2.400 -ef op_ t thy
2.401 -;
2.402 -"~~~~~ fun eval_binop, args:"; val ((thmid : string), (op_: string),
2.403 - (t as (Const (op0, t0) $ t1 $ t2)), _) = ("#mult_", op_, t, thy); (* binary . n1.(n2.v) *)
2.404 -val (SOME n1, SOME n2) = (numeral t1, numeral t2)
2.405 - val (_, _, Trange) = dest_binop_typ t0;
2.406 - val res = calcul op0 n1 n2;
2.407 - val rhs = term_of_float Trange res;
2.408 - val prop = HOLogic.Trueprop $ (mk_equality (t, rhs));
2.409 -val SOME (thmid, tm) = SOME ("#: " ^ term2str prop, prop)
2.410 -;
2.411 -if thmid = "#: 2 * 3 = 6" andalso term2str prop = "2 * 3 = 6" then ()
2.412 -else error "eval_binop changed"
2.413 -;
2.414 -val SOME (thmid, tm) = eval_binop "#mult_" op_ t thy;
2.415 -if thmid = "#: 2 * 3 = 6" andalso term2str prop = "2 * 3 = 6" then ()
2.416 -else error "eval_binop changed 2"
2.417 -
3.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Wed Apr 01 12:42:39 2020 +0200
3.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Wed Apr 01 14:14:46 2020 +0200
3.3 @@ -12,6 +12,8 @@
3.4 "------ polyeq-1.sml ---------------------------------------------";
3.5 "----------- tests on predicates in problems ---------------------";
3.6 "----------- test matching problems ------------------------------";
3.7 +"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
3.8 +"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
3.9 "----------- lin.eq degree_0 -------------------------------------";
3.10 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
3.11 "----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
3.12 @@ -124,6 +126,172 @@
3.13 Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
3.14 then () else error "match_pbl [degree_2,expanded,univariate,equation]";
3.15
3.16 +
3.17 +"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
3.18 +"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
3.19 +"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
3.20 +(*##################################################################################
3.21 +-----------28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
3.22 +
3.23 + (*Aufgabe zum Einstieg in die Arbeit...*)
3.24 + val t = (Thm.term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2 = 0";
3.25 + (*ein 'ruleset' aus Poly.ML wird angewandt...*)
3.26 + val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
3.27 + term2str t;
3.28 + "a * b + (-1 * (a * x) + (-1 * (b * x) + x ^^^ 2)) = 0";
3.29 + val SOME (t,_) =
3.30 + rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;
3.31 + term2str t;
3.32 + "x ^^^ 2 + (-1 * (b * x) + (-1 * (x * a) + b * a)) = 0";
3.33 +(* bei Verwendung von "size_of-term" nach MG :*)
3.34 +(*"x ^^^ 2 + (-1 * (b * x) + (b * a + -1 * (x * a))) = 0" !!! *)
3.35 +
3.36 + (*wir holen 'a' wieder aus der Klammerung heraus...*)
3.37 + val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;
3.38 + term2str t;
3.39 + "x ^^^ 2 + -1 * b * x + -1 * x * a + b * a = 0";
3.40 +(* "x ^^^ 2 + -1 * b * x + b * a + -1 * x * a = 0" !!! *)
3.41 +
3.42 + val SOME (t,_) =
3.43 + rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;
3.44 + term2str t;
3.45 + "x ^^^ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0";
3.46 + (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
3.47 + "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)
3.48 +
3.49 + (*das rewriting l"asst sich beobachten mit
3.50 +trace_rewrite := false;
3.51 + *)
3.52 +
3.53 +"------15.11.02 --------------------------";
3.54 + val t = (Thm.term_of o the o (parse thy)) "1 + a * x + b * x";
3.55 + val bdv = (Thm.term_of o the o (parse thy)) "bdv";
3.56 + val a = (Thm.term_of o the o (parse thy)) "a";
3.57 +
3.58 +trace_rewrite := false;
3.59 + (* Anwenden einer Regelmenge aus Termorder.ML: *)
3.60 + val SOME (t,_) =
3.61 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
3.62 + term2str t;
3.63 + val SOME (t,_) =
3.64 + rewrite_set_ thy false discard_parentheses t;
3.65 + term2str t;
3.66 +"1 + b * x + x * a";
3.67 +
3.68 + val t = (Thm.term_of o the o (parse thy)) "1 + a * (x + b * x) + a^^^2";
3.69 + val SOME (t,_) =
3.70 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
3.71 + term2str t;
3.72 + val SOME (t,_) =
3.73 + rewrite_set_ thy false discard_parentheses t;
3.74 + term2str t;
3.75 +"1 + (x + b * x) * a + a ^^^ 2";
3.76 +
3.77 + val t = (Thm.term_of o the o (parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2";
3.78 + val SOME (t,_) =
3.79 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
3.80 + term2str t;
3.81 + val SOME (t,_) =
3.82 + rewrite_set_ thy false discard_parentheses t;
3.83 + term2str t;
3.84 +"1 + b * a + (7 + x) * a ^^^ 2";
3.85 +
3.86 +(* MG2003
3.87 + Prog_Expr.thy grundlegende Algebra
3.88 + Poly.thy Polynome
3.89 + Rational.thy Br"uche
3.90 + Root.thy Wurzeln
3.91 + RootRat.thy Wurzen + Br"uche
3.92 + Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03)
3.93 +
3.94 + get_thm Termorder.thy "bdv_n_collect";
3.95 + get_thm (theory "Isac_Knowledge") "bdv_n_collect";
3.96 +*)
3.97 + val t = (Thm.term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2";
3.98 + val SOME (t,_) =
3.99 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
3.100 + term2str t;
3.101 + val SOME (t,_) =
3.102 + rewrite_set_ thy false discard_parentheses t;
3.103 + term2str t;
3.104 +"(7 + x) * a ^^^ 2";
3.105 +
3.106 + val t = (Thm.term_of o the o (parse Termorder.thy)) "Pi";
3.107 +
3.108 + val t = (Thm.term_of o the o (parseold thy)) "7";
3.109 +##################################################################################*)
3.110 +
3.111 +
3.112 +"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
3.113 +"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
3.114 +"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
3.115 + val substa = [(e_term, (Thm.term_of o the o (parse thy)) "a")];
3.116 + val substb = [(e_term, (Thm.term_of o the o (parse thy)) "b")];
3.117 + val substx = [(e_term, (Thm.term_of o the o (parse thy)) "x")];
3.118 +
3.119 + val x1 = (Thm.term_of o the o (parse thy)) "a + b + x";
3.120 + val x2 = (Thm.term_of o the o (parse thy)) "a + x + b";
3.121 + val x3 = (Thm.term_of o the o (parse thy)) "a + x + b";
3.122 + val x4 = (Thm.term_of o the o (parse thy)) "x + a + b";
3.123 +
3.124 +if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
3.125 +else error "termorder.sml diff.behav ord_make_polynomial_in #1";
3.126 +
3.127 +if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then ()
3.128 +else error "termorder.sml diff.behav ord_make_polynomial_in #2";
3.129 +
3.130 +if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
3.131 +else error "termorder.sml diff.behav ord_make_polynomial_in #3";
3.132 +
3.133 + val aa = (Thm.term_of o the o (parse thy)) "-1 * a * x";
3.134 + val bb = (Thm.term_of o the o (parse thy)) "x^^^3";
3.135 + ord_make_polynomial_in true thy substx (aa, bb);
3.136 + true; (* => LESS *)
3.137 +
3.138 + val aa = (Thm.term_of o the o (parse thy)) "-1 * a * x";
3.139 + val bb = (Thm.term_of o the o (parse thy)) "x^^^3";
3.140 + ord_make_polynomial_in true thy substa (aa, bb);
3.141 + false; (* => GREATER *)
3.142 +
3.143 +(* und nach dem Re-engineering der Termorders in den 'rulesets'
3.144 + kannst Du die 'gr"osste' Variable frei w"ahlen: *)
3.145 + val bdv= (Thm.term_of o the o (parse thy)) "''bdv''";
3.146 + val x = (Thm.term_of o the o (parse thy)) "x";
3.147 + val a = (Thm.term_of o the o (parse thy)) "a";
3.148 + val b = (Thm.term_of o the o (parse thy)) "b";
3.149 +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
3.150 +if term2str t' = "b + x + a" then ()
3.151 +else error "termorder.sml diff.behav ord_make_polynomial_in #11";
3.152 +
3.153 +val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
3.154 +
3.155 +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
3.156 +if term2str t' = "a + b + x" then ()
3.157 +else error "termorder.sml diff.behav ord_make_polynomial_in #13";
3.158 +
3.159 + val ppp' = "-6 + -5*x + x^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2";
3.160 + val ppp = (Thm.term_of o the o (parse thy)) ppp';
3.161 +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
3.162 +if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
3.163 +else error "termorder.sml diff.behav ord_make_polynomial_in #14";
3.164 +
3.165 +val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
3.166 +if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
3.167 +else error "termorder.sml diff.behav ord_make_polynomial_in #15";
3.168 +
3.169 + val ttt' = "(3*x + 5)/18";
3.170 + val ttt = (Thm.term_of o the o (parse thy)) ttt';
3.171 +val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
3.172 +if term2str uuu = "(5 + 3 * x) / 18" then ()
3.173 +else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
3.174 +
3.175 +(*============ inhibit exn WN120316 ==============================================
3.176 +val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
3.177 +if term2str uuu = "(5 + 3 * x) / 18" then ()
3.178 +else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
3.179 +============ inhibit exn WN120316 ==============================================*)
3.180 +
3.181 +
3.182 "----------- lin.eq degree_0 -------------------------------------";
3.183 "----------- lin.eq degree_0 -------------------------------------";
3.184 "----------- lin.eq degree_0 -------------------------------------";
4.1 --- a/test/Tools/isac/ProgLang/prog_expr.sml Wed Apr 01 12:42:39 2020 +0200
4.2 +++ b/test/Tools/isac/ProgLang/prog_expr.sml Wed Apr 01 14:14:46 2020 +0200
4.3 @@ -8,6 +8,15 @@
4.4 "table of contents -----------------------------------------------------------------------------";
4.5 "-----------------------------------------------------------------------------------------------";
4.6 "-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
4.7 +"-------- occurs_in ----------------------------------------------------------------------------";
4.8 +"-------- fun eval_occurs_in -------------------------------------------------------------------";
4.9 +"-------- fun eval_argument_of -----------------------------------------------------------------";
4.10 +"-------- fun eval_sameFunId -------------------------------------------------------------------";
4.11 +"-------- fun eval_filter_sameFunId ------------------------------------------------------------";
4.12 +"-------- fun eval_boollist2sum ----------------------------------------------------------------";
4.13 +"-------- fun eval_binop -----------------------------------------------------------------------";
4.14 +"-------- fun matchsub -------------------------------------------------------------------------";
4.15 +"-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
4.16 "-----------------------------------------------------------------------------------------------";
4.17 "-----------------------------------------------------------------------------------------------";
4.18 "-----------------------------------------------------------------------------------------------";
4.19 @@ -34,3 +43,253 @@
4.20 val t = str2term "0 = 0";
4.21 val SOME ("equal_(0)_(0)", t') = eval_equal "equal_" "HOL.eq" t thy;
4.22 if term2str t' = "(0 = 0) = True" then () else error "0 = 0 CHANGED";
4.23 +
4.24 +
4.25 +"-------- occurs_in ----------------------------------------------------------------------------";
4.26 +"-------- occurs_in ----------------------------------------------------------------------------";
4.27 +"-------- occurs_in ----------------------------------------------------------------------------";
4.28 +(*=========================================================================*)
4.29 +fun str2t str = (Thm.term_of o the o (parse thy)) str;
4.30 +fun term2s t = term_to_string''' thy t;
4.31 +(*=========================================================================*)
4.32 +
4.33 +val t = str2t "x";
4.34 +if occurs_in t t then "OK" else error "occurs_in x x -> f ..changed";
4.35 +
4.36 +val t = str2term "x occurs_in x";
4.37 +val SOME (str, t') = eval_occurs_in 0 "Prog_Expr.occurs'_in" t 0;
4.38 +if term2str t' = "x occurs_in x = True" then ()
4.39 +else error "x occurs_in x = True ..changed";
4.40 +
4.41 +"------- some_occur_in";
4.42 +some_occur_in [str2t"c",str2t"c_2"] (str2t"a + b + c");
4.43 +val t = str2t "some_of [c, c_2, c_3, c_4] occur_in \
4.44 + \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
4.45 +val SOME (str,t') = eval_some_occur_in 0 "Prog_Expr.some'_occur'_in" t 0;
4.46 +if term2str t' =
4.47 + "some_of [c, c_2, c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 =\nTrue" then ()
4.48 +else error "atools.sml: some_occur_in true";
4.49 +
4.50 +val t = str2t "some_of [c_3, c_4] occur_in \
4.51 + \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
4.52 +val SOME (str,t') = eval_some_occur_in 0 "Prog_Expr.some'_occur'_in" t 0;
4.53 +if term2str t' =
4.54 + "some_of [c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False" then ()
4.55 +else error "atools.sml: some_occur_in false";
4.56 +
4.57 +
4.58 +"-------- fun eval_occurs_in -------------------------------------------------------------------";
4.59 +"-------- fun eval_occurs_in -------------------------------------------------------------------";
4.60 +"-------- fun eval_occurs_in -------------------------------------------------------------------";
4.61 +val v = (Thm.term_of o the o (parse thy)) "x";
4.62 +val t = (Thm.term_of o the o (parse thy)) "1";
4.63 +if occurs_in v t then error "factor_right_deg (1) x ..changed" else ();
4.64 +
4.65 +val v = (Thm.term_of o the o (parse thy)) "AA";
4.66 +val t = (Thm.term_of o the o (parse thy)) "1";
4.67 +if occurs_in v t then error "factor_right_deg (1) AA ..changed" else ();
4.68 +
4.69 +(*----------*)
4.70 +val v = (Thm.term_of o the o (parse thy)) "x";
4.71 +val t = (Thm.term_of o the o (parse thy)) "a*b+c";
4.72 +if occurs_in v t then error "factor_right_deg (a*b+c) x ..changed" else ();
4.73 +
4.74 +val v = (Thm.term_of o the o (parse thy)) "AA";
4.75 +val t = (Thm.term_of o the o (parse thy)) "a*b+c";
4.76 +if occurs_in v t then error "factor_right_deg (a*b+c) AA ..changed" else ();
4.77 +
4.78 +(*----------*)
4.79 +val v = (Thm.term_of o the o (parse thy)) "x";
4.80 +val t = (Thm.term_of o the o (parse thy)) "a*x+c";
4.81 +if occurs_in v t then () else error "factor_right_deg (a*x+c) x ..changed";
4.82 +
4.83 +val v = (Thm.term_of o the o (parse thy)) "AA";
4.84 +val t = (Thm.term_of o the o (parse thy)) "a*AA+c";
4.85 +if occurs_in v t then () else error "factor_right_deg (a*AA+c) AA ..changed";
4.86 +
4.87 +(*----------*)
4.88 +val v = (Thm.term_of o the o (parse thy)) "x";
4.89 +val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*x^^^7";
4.90 +if occurs_in v t then () else error "factor_right_deg (a*b+c)*x^^^7) x ..changed";
4.91 +
4.92 +val v = (Thm.term_of o the o (parse thy)) "AA";
4.93 +val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*AA^^^7";
4.94 +if occurs_in v t then () else error "factor_right_deg (a*b+c)*AA^^^7) AA ..changed";
4.95 +
4.96 +(*----------*)
4.97 +val v = (Thm.term_of o the o (parse thy)) "x";
4.98 +val t = (Thm.term_of o the o (parse thy)) "x^^^7";
4.99 +if occurs_in v t then () else error "factor_right_deg (x^^^7) x ..changed";
4.100 +
4.101 +val v = (Thm.term_of o the o (parse thy)) "AA";
4.102 +val t = (Thm.term_of o the o (parse thy)) "AA^^^7";
4.103 +if occurs_in v t then () else error "factor_right_deg (AA^^^7) AA ..changed";
4.104 +
4.105 +(*----------*)
4.106 +val v = (Thm.term_of o the o (parse thy)) "x";
4.107 +val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*x";
4.108 +if occurs_in v t then () else error "factor_right_deg ((a*b+c)*x) x ..changed";
4.109 +
4.110 +val v = (Thm.term_of o the o (parse thy)) "AA";
4.111 +val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*AA";
4.112 +if occurs_in v t then () else error "factor_right_deg ((a*b+c)*AA) AA ..changed";
4.113 +
4.114 +(*----------*)
4.115 +val v = (Thm.term_of o the o (parse thy)) "x";
4.116 +val t = (Thm.term_of o the o (parse thy)) "(a*b+x)*x";
4.117 +if occurs_in v t then () else error "factor_right_deg ((a*b+x)*x) x ..changed";
4.118 +
4.119 +val v = (Thm.term_of o the o (parse thy)) "AA";
4.120 +val t = (Thm.term_of o the o (parse thy)) "(a*b+AA)*AA";
4.121 +if occurs_in v t then () else error "factor_right_deg ((a*b+AA)*AA) AA ..changed";
4.122 +
4.123 +(*----------*)
4.124 +val v = (Thm.term_of o the o (parse thy)) "x";
4.125 +val t = (Thm.term_of o the o (parse thy)) "x";
4.126 +if occurs_in v t then () else error "factor_right_deg (x) x ..changed";
4.127 +
4.128 +val v = (Thm.term_of o the o (parse thy)) "AA";
4.129 +val t = (Thm.term_of o the o (parse thy)) "AA";
4.130 +if occurs_in v t then () else error "factor_right_deg (AA) AA ..changed";
4.131 +
4.132 +(*----------*)
4.133 +val v = (Thm.term_of o the o (parse thy)) "x";
4.134 +val t = (Thm.term_of o the o (parse thy)) "ab - (a*b)*x";
4.135 +if occurs_in v t then () else error "factor_right_deg (ab - (a*b)*x) x ..changed";
4.136 +
4.137 +val v = (Thm.term_of o the o (parse thy)) "AA";
4.138 +val t = (Thm.term_of o the o (parse thy)) "ab - (a*b)*AA";
4.139 +if occurs_in v t then () else error "factor_right_deg (ab - (a*b)*AA) AA ..changed";
4.140 +
4.141 +
4.142 +"---------fun eval_argument_of -----------------------------------------------------------------";
4.143 +"---------fun eval_argument_of -----------------------------------------------------------------";
4.144 +"---------fun eval_argument_of -----------------------------------------------------------------";
4.145 +val t = str2term "argument_in (M_b x)";
4.146 +val SOME (str, t') = eval_argument_in "0" "Prog_Expr.argument'_in" t 0;
4.147 +if term2str t' = "(argument_in M_b x) = x" then ()
4.148 +else error "atools.sml:(argument_in M_b x) = x ???";
4.149 +
4.150 +
4.151 +"---------fun eval_sameFunId -------------------------------------------------------------------";
4.152 +"---------fun eval_sameFunId -------------------------------------------------------------------";
4.153 +"---------fun eval_sameFunId -------------------------------------------------------------------";
4.154 +val t = str2t "M_b L"; atomty t;
4.155 +val t as f1 $ _ = str2t "M_b L";
4.156 +val t as Const ("HOL.eq", _) $ (f2 $ _) $ _ = str2t "M_b x = c + L*x";
4.157 +f1 = f2 (*true*);
4.158 +val (p as Const ("Prog_Expr.sameFunId",_) $
4.159 + (f1 $ _) $
4.160 + (Const ("HOL.eq", _) $ (f2 $ _) $ _)) =
4.161 + str2t "sameFunId (M_b L) (M_b x = c + L*x)";
4.162 +f1 = f2 (*true*);
4.163 +eval_sameFunId "" "Prog_Expr.sameFunId"
4.164 + (str2t "sameFunId (M_b L) (M_b x = c + L*x)")""(*true*);
4.165 +eval_sameFunId "" "Prog_Expr.sameFunId"
4.166 + (str2t "sameFunId (M_b L) ( y' x = c + L*x)")""(*false*);
4.167 +eval_sameFunId "" "Prog_Expr.sameFunId"
4.168 + (str2t "sameFunId (M_b L) ( y x = c + L*x)")""(*false*);
4.169 +eval_sameFunId "" "Prog_Expr.sameFunId"
4.170 + (str2t "sameFunId ( y L) (M_b x = c + L*x)")""(*false*);
4.171 +eval_sameFunId "" "Prog_Expr.sameFunId"
4.172 + (str2t "sameFunId ( y L) ( y x = c + L*x)")""(*true*);
4.173 +
4.174 +
4.175 +"---------fun eval_filter_sameFunId ------------------------------------------------------------";
4.176 +"---------fun eval_filter_sameFunId ------------------------------------------------------------";
4.177 +"---------fun eval_filter_sameFunId ------------------------------------------------------------";
4.178 +val flhs as (fid $ _) = str2t "y' L";
4.179 +val fs = str2t "[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]";
4.180 +val (p as Const ("Prog_Expr.filter'_sameFunId",_) $ (fid $ _) $ fs) =
4.181 + str2t "filter_sameFunId (y' L) \
4.182 + \[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]";
4.183 +val SOME (str, es) = eval_filter_sameFunId "" "Prog_Expr.filter'_sameFunId" p "";
4.184 +if term2str es = "(filter_sameFunId y' L [M_b x = c + L * x, y' x = c + L * x,\n y x = c + L * x]) =\n[y' x = c + L * x]" then ()
4.185 +else error "atools.slm diff.behav. in filter_sameFunId";
4.186 +
4.187 +
4.188 +"---------fun eval_boollist2sum ----------------------------------------------------------------";
4.189 +"---------fun eval_boollist2sum ----------------------------------------------------------------";
4.190 +"---------fun eval_boollist2sum ----------------------------------------------------------------";
4.191 +fun lhs (Const ("HOL.eq",_) $ l $ _) = l
4.192 + | lhs t = error("lhs called with (" ^ term2str t ^ ")");
4.193 +"-----------^^^redefined due to overwritten identifier -----------";
4.194 +val u_ = str2t "[]";
4.195 +val u_ = str2t "[b1 = k - 2*q]";
4.196 +val u_ = str2t "[b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";
4.197 +val ut_ = isalist2list u_;
4.198 +val sum_ = map lhs ut_;
4.199 +val t = list2sum sum_;
4.200 +term2str t;
4.201 +
4.202 +val t = str2t "boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";
4.203 +
4.204 +val p as Const ("Prog_Expr.boollist2sum", _) $ (Const ("List.list.Cons", _) $ _ $ _) = t;
4.205 +
4.206 +val SOME (str, pred) = eval_boollist2sum "" "Prog_Expr.boollist2sum" t "";
4.207 +if term2str pred = "boollist2sum\n [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q] =\nb1 + b2 + b3 + b4" then ()
4.208 +else error "atools.sml diff.behav. in eval_boollist2sum";
4.209 +
4.210 +trace_rewrite := false;
4.211 +val srls_ = append_rls "srls_..Berechnung-erstSymbolisch" e_rls
4.212 + [Num_Calc ("Prog_Expr.boollist2sum", eval_boollist2sum "")];
4.213 +val t = str2t
4.214 + "boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";
4.215 +case rewrite_set_ thy false srls_ t of SOME _ => ()
4.216 +| _ => error "atools.sml diff.rewrite boollist2sum";
4.217 +trace_rewrite := false;
4.218 +
4.219 +
4.220 +"---------fun eval_binop -----------------------------------------------------------------------";
4.221 +"---------fun eval_binop -----------------------------------------------------------------------";
4.222 +"---------fun eval_binop -----------------------------------------------------------------------";
4.223 +val (op_, ef) = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "TIMES"));
4.224 +val t = (Thm.term_of o the o (parse thy)) "2 * 3";
4.225 +(*val SOME (thmid,t') = *)get_pair thy op_ ef t;
4.226 +;
4.227 +"~~~~~ fun get_pair, args:"; val (thy, op_, ef, (t as (Const (op0,_) $ t1 $ t2))) =
4.228 + (thy, op_, ef, t);
4.229 +op_ = op0 = true;
4.230 +ef op_ t thy
4.231 +;
4.232 +"~~~~~ fun eval_binop, args:"; val ((thmid : string), (op_: string),
4.233 + (t as (Const (op0, t0) $ t1 $ t2)), _) = ("#mult_", op_, t, thy); (* binary . n1.(n2.v) *)
4.234 +val (SOME n1, SOME n2) = (numeral t1, numeral t2)
4.235 + val (_, _, Trange) = dest_binop_typ t0;
4.236 + val res = calcul op0 n1 n2;
4.237 + val rhs = term_of_float Trange res;
4.238 + val prop = HOLogic.Trueprop $ (mk_equality (t, rhs));
4.239 +val SOME (thmid, tm) = SOME ("#: " ^ term2str prop, prop)
4.240 +;
4.241 +if thmid = "#: 2 * 3 = 6" andalso term2str prop = "2 * 3 = 6" then ()
4.242 +else error "eval_binop changed"
4.243 +;
4.244 +val SOME (thmid, tm) = eval_binop "#mult_" op_ t thy;
4.245 +if thmid = "#: 2 * 3 = 6" andalso term2str prop = "2 * 3 = 6" then ()
4.246 +else error "eval_binop changed 2"
4.247 +
4.248 +
4.249 +"-------- fun matchsub -------------------------------------------------------------------------";
4.250 +"-------- fun matchsub -------------------------------------------------------------------------";
4.251 +"-------- fun matchsub -------------------------------------------------------------------------";
4.252 +if matchsub thy (str2term "(a + (b + c))") (str2term "?x + (?y + ?z)")
4.253 +then () else error "tools.sml matchsub a + (b + c)";
4.254 +
4.255 +if matchsub thy (str2term "(a + (b + c)) + d") (str2term "?x + (?y + ?z)")
4.256 +then () else error "tools.sml matchsub (a + (b + c)) + d";
4.257 +
4.258 +
4.259 +"-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
4.260 +"-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
4.261 +"-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
4.262 +"see: --------- search for Or_to_List ---";
4.263 +case or2list @{term True} of Const ("ListC.UniversalList", _) => ()
4.264 + | _ => error "TermC.UniversalList changed 1";
4.265 +case or2list @{term False} of Const ("List.list.Nil", _) => ()
4.266 + | _ => error "TermC.UniversalList changed 2";
4.267 +val t = (str2term "x=3");
4.268 +if term2str (or2list t) = "[x = 3]" then ()
4.269 +else error "or2list changed";
4.270 +val t = (str2term "x=3 | x=-3 | x=0");
4.271 +if term2str (or2list t) = "[x = 3, x = -3, x = 0]" then ()
4.272 +else error "HOL.eq ? HOL.disj ? changed";
5.1 --- a/test/Tools/isac/ProgLang/tools.sml Wed Apr 01 12:42:39 2020 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,41 +0,0 @@
5.4 -(* Title: tests on Tools
5.5 - Author: Walther Neuper WN071229,
5.6 - (c) due to copyright terms
5.7 -*)
5.8 -val thy = @{theory "Real"};
5.9 -
5.10 -"-----------------------------------------------------------------";
5.11 -"table of contents -----------------------------------------------";
5.12 -"-----------------------------------------------------------------";
5.13 -"----------- fun matchsub ----------------------------------------";
5.14 -"----------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc -";
5.15 -"-----------------------------------------------------------------";
5.16 -"-----------------------------------------------------------------";
5.17 -"-----------------------------------------------------------------";
5.18 -
5.19 -
5.20 -"----------- fun matchsub ----------------------------------------";
5.21 -"----------- fun matchsub ----------------------------------------";
5.22 -"----------- fun matchsub ----------------------------------------";
5.23 -if matchsub thy (str2term "(a + (b + c))") (str2term "?x + (?y + ?z)")
5.24 -then () else error "tools.sml matchsub a + (b + c)";
5.25 -
5.26 -if matchsub thy (str2term "(a + (b + c)) + d") (str2term "?x + (?y + ?z)")
5.27 -then () else error "tools.sml matchsub (a + (b + c)) + d";
5.28 -
5.29 -
5.30 -"----------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc -";
5.31 -"----------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc -";
5.32 -"----------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc -";
5.33 -"see: --------- search for Or_to_List ---";
5.34 -case or2list @{term True} of Const ("ListC.UniversalList", _) => ()
5.35 - | _ => error "TermC.UniversalList changed 1";
5.36 -case or2list @{term False} of Const ("List.list.Nil", _) => ()
5.37 - | _ => error "TermC.UniversalList changed 2";
5.38 -val t = (str2term "x=3");
5.39 -if term2str (or2list t) = "[x = 3]" then ()
5.40 -else error "or2list changed";
5.41 -val t = (str2term "x=3 | x=-3 | x=0");
5.42 -if term2str (or2list t) = "[x = 3, x = -3, x = 0]" then ()
5.43 -else error "HOL.eq ? HOL.disj ? changed";
5.44 -