1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Fri Apr 10 16:16:09 2020 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Fri Apr 10 18:32:36 2020 +0200
1.3 @@ -54,55 +54,55 @@
1.4 *)
1.5 val t1 = (Thm.term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
1.6 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
1.7 - if ((UnparseC.term2str t) = "-8 - 2 * x + x ^^^ 2") then ()
1.8 + if ((UnparseC.term t) = "-8 - 2 * x + x ^^^ 2") then ()
1.9 else error "polyeq.sml: diff.behav. in lhs";
1.10
1.11 val t2 = (Thm.term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
1.12 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
1.13 - if (UnparseC.term2str t) = "True" then ()
1.14 + if (UnparseC.term t) = "True" then ()
1.15 else error "polyeq.sml: diff.behav. 1 in is_expended_in";
1.16
1.17 val t0 = (Thm.term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x";
1.18 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
1.19 - if (UnparseC.term2str t) = "False" then ()
1.20 + if (UnparseC.term t) = "False" then ()
1.21 else error "polyeq.sml: diff.behav. 2 in is_poly_in";
1.22
1.23 val t3 = (Thm.term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x";
1.24 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
1.25 - if (UnparseC.term2str t) = "True" then ()
1.26 + if (UnparseC.term t) = "True" then ()
1.27 else error "polyeq.sml: diff.behav. 3 in is_poly_in";
1.28
1.29 val t4 = (Thm.term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x";
1.30 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
1.31 - if (UnparseC.term2str t) = "True" then ()
1.32 + if (UnparseC.term t) = "True" then ()
1.33 else error "polyeq.sml: diff.behav. 4 in is_expended_in";
1.34
1.35
1.36 val t6 = (Thm.term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
1.37 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
1.38 - if (UnparseC.term2str t) = "True" then ()
1.39 + if (UnparseC.term t) = "True" then ()
1.40 else error "polyeq.sml: diff.behav. 5 in is_expended_in";
1.41
1.42 val t3 = (Thm.term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
1.43 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
1.44 - if (UnparseC.term2str t) = "True" then ()
1.45 + if (UnparseC.term t) = "True" then ()
1.46 else error "polyeq.sml: diff.behav. in has_degree_in_in";
1.47
1.48 val t3 = (Thm.term_of o the o (parse 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.term2str t) = "False" then ()
1.51 + if (UnparseC.term t) = "False" then ()
1.52 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
1.53
1.54 val t4 = (Thm.term_of o the o (parse thy))
1.55 "((-8 - 2*x + x^^^2) has_degree_in x) = 1";
1.56 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
1.57 - if (UnparseC.term2str t) = "False" then ()
1.58 + if (UnparseC.term t) = "False" then ()
1.59 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
1.60
1.61 val t5 = (Thm.term_of o the o (parse thy))
1.62 "((-8 - 2*x + x^^^2) has_degree_in x) = 2";
1.63 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
1.64 - if (UnparseC.term2str t) = "True" then ()
1.65 + if (UnparseC.term t) = "True" then ()
1.66 else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
1.67
1.68 "----------- test matching problems --------------------------0---";
1.69 @@ -137,24 +137,24 @@
1.70 val t = (Thm.term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^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.term2str t;
1.74 + UnparseC.term t;
1.75 "a * b + (-1 * (a * x) + (-1 * (b * x) + x ^^^ 2)) = 0";
1.76 val SOME (t,_) =
1.77 rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;
1.78 - UnparseC.term2str t;
1.79 + UnparseC.term t;
1.80 "x ^^^ 2 + (-1 * (b * x) + (-1 * (x * a) + b * a)) = 0";
1.81 (* bei Verwendung von "size_of-term" nach MG :*)
1.82 (*"x ^^^ 2 + (-1 * (b * x) + (b * a + -1 * (x * a))) = 0" !!! *)
1.83
1.84 (*wir holen 'a' wieder aus der Klammerung heraus...*)
1.85 val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;
1.86 - UnparseC.term2str t;
1.87 + UnparseC.term t;
1.88 "x ^^^ 2 + -1 * b * x + -1 * x * a + b * a = 0";
1.89 (* "x ^^^ 2 + -1 * b * x + b * a + -1 * x * a = 0" !!! *)
1.90
1.91 val SOME (t,_) =
1.92 rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;
1.93 - UnparseC.term2str t;
1.94 + UnparseC.term t;
1.95 "x ^^^ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0";
1.96 (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
1.97 "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)
1.98 @@ -172,28 +172,28 @@
1.99 (* Anwenden einer Regelmenge aus Termorder.ML: *)
1.100 val SOME (t,_) =
1.101 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
1.102 - UnparseC.term2str t;
1.103 + UnparseC.term t;
1.104 val SOME (t,_) =
1.105 rewrite_set_ thy false discard_parentheses t;
1.106 - UnparseC.term2str t;
1.107 + UnparseC.term t;
1.108 "1 + b * x + x * a";
1.109
1.110 val t = (Thm.term_of o the o (parse thy)) "1 + a * (x + b * x) + a^^^2";
1.111 val SOME (t,_) =
1.112 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
1.113 - UnparseC.term2str t;
1.114 + UnparseC.term t;
1.115 val SOME (t,_) =
1.116 rewrite_set_ thy false discard_parentheses t;
1.117 - UnparseC.term2str t;
1.118 + UnparseC.term t;
1.119 "1 + (x + b * x) * a + a ^^^ 2";
1.120
1.121 val t = (Thm.term_of o the o (parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2";
1.122 val SOME (t,_) =
1.123 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
1.124 - UnparseC.term2str t;
1.125 + UnparseC.term t;
1.126 val SOME (t,_) =
1.127 rewrite_set_ thy false discard_parentheses t;
1.128 - UnparseC.term2str t;
1.129 + UnparseC.term t;
1.130 "1 + b * a + (7 + x) * a ^^^ 2";
1.131
1.132 (* MG2003
1.133 @@ -210,10 +210,10 @@
1.134 val t = (Thm.term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2";
1.135 val SOME (t,_) =
1.136 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
1.137 - UnparseC.term2str t;
1.138 + UnparseC.term t;
1.139 val SOME (t,_) =
1.140 rewrite_set_ thy false discard_parentheses t;
1.141 - UnparseC.term2str t;
1.142 + UnparseC.term t;
1.143 "(7 + x) * a ^^^ 2";
1.144
1.145 val t = (Thm.term_of o the o (parse Termorder.thy)) "Pi";
1.146 @@ -260,34 +260,34 @@
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 UnparseC.term2str t' = "b + x + a" then ()
1.151 +if UnparseC.term t' = "b + x + a" then ()
1.152 else error "termorder.sml diff.behav ord_make_polynomial_in #11";
1.153
1.154 val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
1.155
1.156 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
1.157 -if UnparseC.term2str t' = "a + b + x" then ()
1.158 +if UnparseC.term t' = "a + b + x" then ()
1.159 else error "termorder.sml diff.behav ord_make_polynomial_in #13";
1.160
1.161 val ppp' = "-6 + -5*x + x^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2";
1.162 val ppp = (Thm.term_of o the o (parse thy)) ppp';
1.163 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
1.164 -if UnparseC.term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
1.165 +if UnparseC.term t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
1.166 else error "termorder.sml diff.behav ord_make_polynomial_in #14";
1.167
1.168 val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
1.169 -if UnparseC.term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
1.170 +if UnparseC.term t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
1.171 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
1.172
1.173 val ttt' = "(3*x + 5)/18";
1.174 val ttt = (Thm.term_of o the o (parse thy)) ttt';
1.175 val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
1.176 -if UnparseC.term2str uuu = "(5 + 3 * x) / 18" then ()
1.177 +if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
1.178 else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
1.179
1.180 (*============ inhibit exn WN120316 ==============================================
1.181 val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
1.182 -if UnparseC.term2str uuu = "(5 + 3 * x) / 18" then ()
1.183 +if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
1.184 else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
1.185 ============ inhibit exn WN120316 ==============================================*)
1.186
1.187 @@ -354,10 +354,10 @@
1.188 "~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
1.189 val Appl m = applicable_in p pt tac;
1.190 val Check_elementwise' (trm1, str, (trm2, trms)) = m;
1.191 -UnparseC.term2str trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
1.192 +UnparseC.term trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
1.193 str = "Assumptions";
1.194 -UnparseC.term2str trm2 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
1.195 -UnparseC.terms2str trms = "[\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n "^
1.196 +UnparseC.term trm2 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
1.197 +UnparseC.terms trms = "[\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n "^
1.198 " (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) is_poly_in 1 / 8 + sqrt (9 / 16) / 2\","^
1.199 "\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) "^
1.200 "has_degree_in 1 / 8 + sqrt (9 / 16) / 2 =\n2\","^
1.201 @@ -386,7 +386,7 @@
1.202 ((thy',ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
1.203 1 < length l (*true*);
1.204 val up = drop_last l;
1.205 - UnparseC.term2str (at_location up sc);
1.206 + UnparseC.term (at_location up sc);
1.207 (at_location up sc);
1.208 (*WAS val Term_Val1 _ = scan_up1 ys ((E,up,a,v,S,b),ss) (at_location up sc)
1.209 ... ???? ... is correct*)
1.210 @@ -410,8 +410,8 @@
1.211 ... Associated ... is correct*)
1.212 "~~~~~ fun associate, args:"; val (pt, _, (m as Check_elementwise' (consts,_,(consts_chkd,_))),
1.213 (Const ("Prog_Tac.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
1.214 -UnparseC.term2str consts;
1.215 -UnparseC.term2str consts';
1.216 +UnparseC.term consts;
1.217 +UnparseC.term consts';
1.218 if consts = consts' (*WAS false*) then () else error "Check_elementwise changed";
1.219 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
1.220 ( *----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------//*)
1.221 @@ -437,7 +437,7 @@
1.222 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.223 val asm = Ctree.get_assumptions pt p;
1.224 if f2str f = "[]" andalso
1.225 - UnparseC.terms2str asm = "[\"lhs (2 + -1 * x + x ^^^ 2 = 0) is_poly_in x\"," ^
1.226 + UnparseC.terms asm = "[\"lhs (2 + -1 * x + x ^^^ 2 = 0) is_poly_in x\"," ^
1.227 "\"lhs (2 + -1 * x + x ^^^ 2 = 0) has_degree_in x = 2\"]" then ()
1.228 else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
1.229
1.230 @@ -962,40 +962,40 @@
1.231
1.232 val rls = complete_square;
1.233 val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
1.234 -UnparseC.term2str t = "-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2";
1.235 +UnparseC.term t = "-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2";
1.236
1.237 val thm = num_str @{thm square_explicit1};
1.238 val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t;
1.239 -UnparseC.term2str t = "(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8";
1.240 +UnparseC.term t = "(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8";
1.241
1.242 val thm = num_str @{thm root_plus_minus};
1.243 val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
1.244 -UnparseC.term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
1.245 +UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
1.246 "\n2 / 2 - x = -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
1.247
1.248 (*the thm bdv_explicit2* here required to be constrained to ::real*)
1.249 val thm = num_str @{thm bdv_explicit2};
1.250 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1.251 -UnparseC.term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
1.252 +UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
1.253 "\n-1 * x = - (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
1.254
1.255 val thm = num_str @{thm bdv_explicit3};
1.256 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1.257 -UnparseC.term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
1.258 +UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
1.259 "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
1.260
1.261 val thm = num_str @{thm bdv_explicit2};
1.262 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1.263 -UnparseC.term2str t = "-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |"^
1.264 +UnparseC.term t = "-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |"^
1.265 "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
1.266
1.267 val rls = calculate_RootRat;
1.268 val SOME (t,asm) = rewrite_set_ thy true rls t;
1.269 -if UnparseC.term2str t =
1.270 +if UnparseC.term t =
1.271 "-1 * x = -1 + sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8) \<or>\nx = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))"
1.272 (*"-1 * x = -1 + sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8) |\nx = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))"..isabisac15*)
1.273 then () else error "(-8 - 2*x + x^^^2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT";
1.274 -(*SHOULD BE: UnparseC.term2str = "x = -2 | x = 4;*)
1.275 +(*SHOULD BE: UnparseC.term = "x = -2 | x = 4;*)
1.276
1.277
1.278 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
1.279 @@ -1004,7 +1004,7 @@
1.280 "---- test the erls ----";
1.281 val t1 = (Thm.term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1";
1.282 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
1.283 - val t' = UnparseC.term2str t;
1.284 + val t' = UnparseC.term t;
1.285 (*if t'= "HOL.True" then ()
1.286 else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
1.287 (* *)