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