1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Mon Jul 19 18:39:02 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Tue Jul 20 14:37:56 2021 +0200
1.3 @@ -51,33 +51,33 @@
1.4 "----------- tests on predicates in problems ---------------------";
1.5 Rewrite.trace_on:=true; (*true false*)
1.6
1.7 - val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";
1.8 + val t1 = TermC.parseNEW'' thy "lhs (-8 - 2*x + x \<up> 2 = 0)";
1.9 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
1.10 if ((UnparseC.term t) = "-8 - 2 * x + x \<up> 2") then ()
1.11 else error "polyeq.sml: diff.behav. in lhs";
1.12
1.13 - val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
1.14 + val t2 = TermC.parseNEW'' thy "(-8 - 2*x + x \<up> 2) is_expanded_in x";
1.15 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
1.16 if (UnparseC.term t) = "True" then ()
1.17 else error "polyeq.sml: diff.behav. 1 in is_expended_in";
1.18
1.19 - val t0 = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)) is_poly_in x";
1.20 + val t0 = TermC.parseNEW'' thy "(sqrt(x)) is_poly_in x";
1.21 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
1.22 if (UnparseC.term t) = "False" then ()
1.23 else error "polyeq.sml: diff.behav. 2 in is_poly_in";
1.24
1.25 - val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";
1.26 + val t3 = TermC.parseNEW'' thy "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";
1.27 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
1.28 if (UnparseC.term t) = "True" then ()
1.29 else error "polyeq.sml: diff.behav. 3 in is_poly_in";
1.30
1.31 - val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x";
1.32 + val t4 = TermC.parseNEW'' thy "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x";
1.33 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
1.34 if (UnparseC.term t) = "True" then ()
1.35 else error "polyeq.sml: diff.behav. 4 in is_expended_in";
1.36
1.37
1.38 - val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
1.39 + val t6 = TermC.parseNEW'' thy "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
1.40 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
1.41 if (UnparseC.term t) = "True" then ()
1.42 else error "polyeq.sml: diff.behav. 5 in is_expended_in";
1.43 @@ -87,18 +87,18 @@
1.44 if (UnparseC.term t) = "True" then ()
1.45 else error "polyeq.sml: diff.behav. in has_degree_in_in";
1.46
1.47 - val t3 = (Thm.term_of o the o (TermC.parse thy)) "((sqrt(x)) has_degree_in x) = 2";
1.48 + val t3 = TermC.parseNEW'' thy "((sqrt(x)) has_degree_in x) = 2";
1.49 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
1.50 if (UnparseC.term t) = "False" then ()
1.51 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
1.52
1.53 - val t4 = (Thm.term_of o the o (TermC.parse thy))
1.54 + val t4 = TermC.parseNEW'' thy
1.55 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 1";
1.56 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
1.57 if (UnparseC.term t) = "False" then ()
1.58 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
1.59
1.60 - val t5 = (Thm.term_of o the o (TermC.parse thy))
1.61 + val t5 = TermC.parseNEW'' thy
1.62 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
1.63 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
1.64 if (UnparseC.term t) = "True" then ()
1.65 @@ -133,7 +133,7 @@
1.66 ----------- 28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
1.67
1.68 (*Aufgabe zum Einstieg in die Arbeit...*)
1.69 - val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x \<up> 2 = 0";
1.70 + val t = TermC.parseNEW'' thy "a*b - (a+b)*x + x \<up> 2 = 0";
1.71 (*ein 'ruleset' aus Poly.ML wird angewandt...*)
1.72 val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
1.73 UnparseC.term t;
1.74 @@ -163,9 +163,9 @@
1.75 *)
1.76
1.77 "------ 15.11.02 --------------------------";
1.78 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * x + b * x";
1.79 - val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv";
1.80 - val a = (Thm.term_of o the o (TermC.parse thy)) "a";
1.81 + val t = TermC.parseNEW'' thy "1 + a * x + b * x";
1.82 + val bdv = TermC.parseNEW'' thy "bdv";
1.83 + val a = TermC.parseNEW'' thy "a";
1.84
1.85 Rewrite.trace_on := false; (*true false*)
1.86 (* Anwenden einer Regelmenge aus Termorder.ML: *)
1.87 @@ -177,7 +177,7 @@
1.88 UnparseC.term t;
1.89 "1 + b * x + x * a";
1.90
1.91 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * (x + b * x) + a \<up> 2";
1.92 + val t = TermC.parseNEW'' thy "1 + a * (x + b * x) + a \<up> 2";
1.93 val SOME (t,_) =
1.94 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
1.95 UnparseC.term t;
1.96 @@ -186,7 +186,7 @@
1.97 UnparseC.term t;
1.98 "1 + (x + b * x) * a + a \<up> 2";
1.99
1.100 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a \<up> 2 * x + b * a + 7*a \<up> 2";
1.101 + val t = TermC.parseNEW'' thy "1 + a \<up> 2 * x + b * a + 7*a \<up> 2";
1.102 val SOME (t,_) =
1.103 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
1.104 UnparseC.term t;
1.105 @@ -206,7 +206,7 @@
1.106 get_thm Termorder.thy "bdv_n_collect";
1.107 get_thm (theory "Isac_Knowledge") "bdv_n_collect";
1.108 *)
1.109 - val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * x + 7 * a \<up> 2";
1.110 + val t = TermC.parseNEW'' thy "a \<up> 2 * x + 7 * a \<up> 2";
1.111 val SOME (t,_) =
1.112 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
1.113 UnparseC.term t;
1.114 @@ -224,14 +224,14 @@
1.115 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
1.116 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
1.117 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
1.118 - val substa = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "a")];
1.119 - val substb = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "b")];
1.120 - val substx = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "x")];
1.121 + val substa = [(TermC.empty, TermC.parseNEW'' thy "a")];
1.122 + val substb = [(TermC.empty, TermC.parseNEW'' thy "b")];
1.123 + val substx = [(TermC.empty, TermC.parseNEW'' thy "x")];
1.124
1.125 - val x1 = (Thm.term_of o the o (TermC.parse thy)) "a + b + x";
1.126 - val x2 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
1.127 - val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
1.128 - val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b";
1.129 + val x1 = TermC.parseNEW'' thy "a + b + x";
1.130 + val x2 = TermC.parseNEW'' thy "a + x + b";
1.131 + val x3 = TermC.parseNEW'' thy "a + x + b";
1.132 + val x4 = TermC.parseNEW'' thy "x + a + b";
1.133
1.134 if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
1.135 else error "termorder.sml diff.behav ord_make_polynomial_in #1";
1.136 @@ -242,22 +242,22 @@
1.137 if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
1.138 else error "termorder.sml diff.behav ord_make_polynomial_in #3";
1.139
1.140 - val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
1.141 - val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
1.142 + val aa = TermC.parseNEW'' thy "- 1 * a * x";
1.143 + val bb = TermC.parseNEW'' thy "x \<up> 3";
1.144 ord_make_polynomial_in true thy substx (aa, bb);
1.145 true; (* => LESS *)
1.146
1.147 - val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
1.148 - val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
1.149 + val aa = TermC.parseNEW'' thy "- 1 * a * x";
1.150 + val bb = TermC.parseNEW'' thy "x \<up> 3";
1.151 ord_make_polynomial_in true thy substa (aa, bb);
1.152 false; (* => GREATER *)
1.153
1.154 (* und nach dem Re-engineering der Termorders in den 'rulesets'
1.155 kannst Du die 'gr"osste' Variable frei w"ahlen: *)
1.156 - val bdv= (Thm.term_of o the o (TermC.parse thy)) "''bdv''";
1.157 - val x = (Thm.term_of o the o (TermC.parse thy)) "x";
1.158 - val a = (Thm.term_of o the o (TermC.parse thy)) "a";
1.159 - val b = (Thm.term_of o the o (TermC.parse thy)) "b";
1.160 + val bdv= TermC.parseNEW'' thy "''bdv''";
1.161 + val x = TermC.parseNEW'' thy "x";
1.162 + val a = TermC.parseNEW'' thy "a";
1.163 + val b = TermC.parseNEW'' thy "b";
1.164 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
1.165 if UnparseC.term t' = "b + x + a" then ()
1.166 else error "termorder.sml diff.behav ord_make_polynomial_in #11";
1.167 @@ -269,7 +269,7 @@
1.168 else error "termorder.sml diff.behav ord_make_polynomial_in #13";
1.169
1.170 val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
1.171 - val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp';
1.172 + val ppp = TermC.parseNEW'' thy ppp';
1.173 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
1.174 if UnparseC.term t' = "-6 + -5 * x + - 15 * x \<up> 2 + 0" then ()
1.175 else error "termorder.sml diff.behav ord_make_polynomial_in #14";
1.176 @@ -279,7 +279,7 @@
1.177 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
1.178
1.179 val ttt' = "(3*x + 5)/18";
1.180 - val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt';
1.181 + val ttt = TermC.parseNEW'' thy ttt';
1.182 val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
1.183 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
1.184 else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
1.185 @@ -940,7 +940,7 @@
1.186 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
1.187 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
1.188 "---- test the erls ----";
1.189 - val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2) \<up> 2 - 1";
1.190 + val t1 = TermC.parseNEW'' thy "0 <= (10/3/2) \<up> 2 - 1";
1.191 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
1.192 val t' = UnparseC.term t;
1.193 (*if t'= \<^const_name>\<open>True\<close> then ()