1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Wed Apr 01 12:42:39 2020 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Wed Apr 01 14:14:46 2020 +0200
1.3 @@ -12,6 +12,8 @@
1.4 "------ polyeq-1.sml ---------------------------------------------";
1.5 "----------- tests on predicates in problems ---------------------";
1.6 "----------- test matching problems ------------------------------";
1.7 +"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
1.8 +"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
1.9 "----------- lin.eq degree_0 -------------------------------------";
1.10 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
1.11 "----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
1.12 @@ -124,6 +126,172 @@
1.13 Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
1.14 then () else error "match_pbl [degree_2,expanded,univariate,equation]";
1.15
1.16 +
1.17 +"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
1.18 +"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
1.19 +"----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
1.20 +(*##################################################################################
1.21 +-----------28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
1.22 +
1.23 + (*Aufgabe zum Einstieg in die Arbeit...*)
1.24 + val t = (Thm.term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2 = 0";
1.25 + (*ein 'ruleset' aus Poly.ML wird angewandt...*)
1.26 + val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
1.27 + term2str t;
1.28 + "a * b + (-1 * (a * x) + (-1 * (b * x) + x ^^^ 2)) = 0";
1.29 + val SOME (t,_) =
1.30 + rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;
1.31 + term2str t;
1.32 + "x ^^^ 2 + (-1 * (b * x) + (-1 * (x * a) + b * a)) = 0";
1.33 +(* bei Verwendung von "size_of-term" nach MG :*)
1.34 +(*"x ^^^ 2 + (-1 * (b * x) + (b * a + -1 * (x * a))) = 0" !!! *)
1.35 +
1.36 + (*wir holen 'a' wieder aus der Klammerung heraus...*)
1.37 + val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;
1.38 + term2str t;
1.39 + "x ^^^ 2 + -1 * b * x + -1 * x * a + b * a = 0";
1.40 +(* "x ^^^ 2 + -1 * b * x + b * a + -1 * x * a = 0" !!! *)
1.41 +
1.42 + val SOME (t,_) =
1.43 + rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;
1.44 + term2str t;
1.45 + "x ^^^ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0";
1.46 + (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
1.47 + "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)
1.48 +
1.49 + (*das rewriting l"asst sich beobachten mit
1.50 +trace_rewrite := false;
1.51 + *)
1.52 +
1.53 +"------15.11.02 --------------------------";
1.54 + val t = (Thm.term_of o the o (parse thy)) "1 + a * x + b * x";
1.55 + val bdv = (Thm.term_of o the o (parse thy)) "bdv";
1.56 + val a = (Thm.term_of o the o (parse thy)) "a";
1.57 +
1.58 +trace_rewrite := false;
1.59 + (* Anwenden einer Regelmenge aus Termorder.ML: *)
1.60 + val SOME (t,_) =
1.61 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
1.62 + term2str t;
1.63 + val SOME (t,_) =
1.64 + rewrite_set_ thy false discard_parentheses t;
1.65 + term2str t;
1.66 +"1 + b * x + x * a";
1.67 +
1.68 + val t = (Thm.term_of o the o (parse thy)) "1 + a * (x + b * x) + a^^^2";
1.69 + val SOME (t,_) =
1.70 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
1.71 + term2str t;
1.72 + val SOME (t,_) =
1.73 + rewrite_set_ thy false discard_parentheses t;
1.74 + term2str t;
1.75 +"1 + (x + b * x) * a + a ^^^ 2";
1.76 +
1.77 + val t = (Thm.term_of o the o (parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2";
1.78 + val SOME (t,_) =
1.79 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
1.80 + term2str t;
1.81 + val SOME (t,_) =
1.82 + rewrite_set_ thy false discard_parentheses t;
1.83 + term2str t;
1.84 +"1 + b * a + (7 + x) * a ^^^ 2";
1.85 +
1.86 +(* MG2003
1.87 + Prog_Expr.thy grundlegende Algebra
1.88 + Poly.thy Polynome
1.89 + Rational.thy Br"uche
1.90 + Root.thy Wurzeln
1.91 + RootRat.thy Wurzen + Br"uche
1.92 + Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03)
1.93 +
1.94 + get_thm Termorder.thy "bdv_n_collect";
1.95 + get_thm (theory "Isac_Knowledge") "bdv_n_collect";
1.96 +*)
1.97 + val t = (Thm.term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2";
1.98 + val SOME (t,_) =
1.99 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
1.100 + term2str t;
1.101 + val SOME (t,_) =
1.102 + rewrite_set_ thy false discard_parentheses t;
1.103 + term2str t;
1.104 +"(7 + x) * a ^^^ 2";
1.105 +
1.106 + val t = (Thm.term_of o the o (parse Termorder.thy)) "Pi";
1.107 +
1.108 + val t = (Thm.term_of o the o (parseold thy)) "7";
1.109 +##################################################################################*)
1.110 +
1.111 +
1.112 +"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
1.113 +"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
1.114 +"----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
1.115 + val substa = [(e_term, (Thm.term_of o the o (parse thy)) "a")];
1.116 + val substb = [(e_term, (Thm.term_of o the o (parse thy)) "b")];
1.117 + val substx = [(e_term, (Thm.term_of o the o (parse thy)) "x")];
1.118 +
1.119 + val x1 = (Thm.term_of o the o (parse thy)) "a + b + x";
1.120 + val x2 = (Thm.term_of o the o (parse thy)) "a + x + b";
1.121 + val x3 = (Thm.term_of o the o (parse thy)) "a + x + b";
1.122 + val x4 = (Thm.term_of o the o (parse thy)) "x + a + b";
1.123 +
1.124 +if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
1.125 +else error "termorder.sml diff.behav ord_make_polynomial_in #1";
1.126 +
1.127 +if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then ()
1.128 +else error "termorder.sml diff.behav ord_make_polynomial_in #2";
1.129 +
1.130 +if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
1.131 +else error "termorder.sml diff.behav ord_make_polynomial_in #3";
1.132 +
1.133 + val aa = (Thm.term_of o the o (parse thy)) "-1 * a * x";
1.134 + val bb = (Thm.term_of o the o (parse thy)) "x^^^3";
1.135 + ord_make_polynomial_in true thy substx (aa, bb);
1.136 + true; (* => LESS *)
1.137 +
1.138 + val aa = (Thm.term_of o the o (parse thy)) "-1 * a * x";
1.139 + val bb = (Thm.term_of o the o (parse thy)) "x^^^3";
1.140 + ord_make_polynomial_in true thy substa (aa, bb);
1.141 + false; (* => GREATER *)
1.142 +
1.143 +(* und nach dem Re-engineering der Termorders in den 'rulesets'
1.144 + kannst Du die 'gr"osste' Variable frei w"ahlen: *)
1.145 + val bdv= (Thm.term_of o the o (parse thy)) "''bdv''";
1.146 + val x = (Thm.term_of o the o (parse thy)) "x";
1.147 + val a = (Thm.term_of o the o (parse thy)) "a";
1.148 + val b = (Thm.term_of o the o (parse thy)) "b";
1.149 +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
1.150 +if term2str t' = "b + x + a" then ()
1.151 +else error "termorder.sml diff.behav ord_make_polynomial_in #11";
1.152 +
1.153 +val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
1.154 +
1.155 +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
1.156 +if term2str t' = "a + b + x" then ()
1.157 +else error "termorder.sml diff.behav ord_make_polynomial_in #13";
1.158 +
1.159 + val ppp' = "-6 + -5*x + x^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2";
1.160 + val ppp = (Thm.term_of o the o (parse thy)) ppp';
1.161 +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
1.162 +if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
1.163 +else error "termorder.sml diff.behav ord_make_polynomial_in #14";
1.164 +
1.165 +val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
1.166 +if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
1.167 +else error "termorder.sml diff.behav ord_make_polynomial_in #15";
1.168 +
1.169 + val ttt' = "(3*x + 5)/18";
1.170 + val ttt = (Thm.term_of o the o (parse thy)) ttt';
1.171 +val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
1.172 +if term2str uuu = "(5 + 3 * x) / 18" then ()
1.173 +else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
1.174 +
1.175 +(*============ inhibit exn WN120316 ==============================================
1.176 +val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
1.177 +if term2str uuu = "(5 + 3 * x) / 18" then ()
1.178 +else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
1.179 +============ inhibit exn WN120316 ==============================================*)
1.180 +
1.181 +
1.182 "----------- lin.eq degree_0 -------------------------------------";
1.183 "----------- lin.eq degree_0 -------------------------------------";
1.184 "----------- lin.eq degree_0 -------------------------------------";