1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Thu Apr 09 12:03:14 2020 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Thu Apr 09 17:13:17 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 ((term2str t) = "-8 - 2 * x + x ^^^ 2") then ()
1.8 + if ((UnparseC.term2str 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 (term2str t) = "True" then ()
1.14 + if (UnparseC.term2str 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 (term2str t) = "False" then ()
1.20 + if (UnparseC.term2str 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 (term2str t) = "True" then ()
1.26 + if (UnparseC.term2str 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 (term2str t) = "True" then ()
1.32 + if (UnparseC.term2str 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 (term2str t) = "True" then ()
1.39 + if (UnparseC.term2str 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 (term2str t) = "True" then ()
1.45 + if (UnparseC.term2str 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 (term2str t) = "False" then ()
1.51 + if (UnparseC.term2str 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 (term2str t) = "False" then ()
1.58 + if (UnparseC.term2str 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 (term2str t) = "True" then ()
1.65 + if (UnparseC.term2str 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 - term2str t;
1.74 + UnparseC.term2str 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 - term2str t;
1.79 + UnparseC.term2str 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 - term2str t;
1.87 + UnparseC.term2str 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 - term2str t;
1.94 + UnparseC.term2str 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 - term2str t;
1.103 + UnparseC.term2str t;
1.104 val SOME (t,_) =
1.105 rewrite_set_ thy false discard_parentheses t;
1.106 - term2str t;
1.107 + UnparseC.term2str 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 - term2str t;
1.114 + UnparseC.term2str t;
1.115 val SOME (t,_) =
1.116 rewrite_set_ thy false discard_parentheses t;
1.117 - term2str t;
1.118 + UnparseC.term2str 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 - term2str t;
1.125 + UnparseC.term2str t;
1.126 val SOME (t,_) =
1.127 rewrite_set_ thy false discard_parentheses t;
1.128 - term2str t;
1.129 + UnparseC.term2str 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 - term2str t;
1.138 + UnparseC.term2str t;
1.139 val SOME (t,_) =
1.140 rewrite_set_ thy false discard_parentheses t;
1.141 - term2str t;
1.142 + UnparseC.term2str 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 @@ -225,9 +225,9 @@
1.147 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
1.148 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
1.149 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
1.150 - val substa = [(e_term, (Thm.term_of o the o (parse thy)) "a")];
1.151 - val substb = [(e_term, (Thm.term_of o the o (parse thy)) "b")];
1.152 - val substx = [(e_term, (Thm.term_of o the o (parse thy)) "x")];
1.153 + val substa = [(TermC.empty, (Thm.term_of o the o (parse thy)) "a")];
1.154 + val substb = [(TermC.empty, (Thm.term_of o the o (parse thy)) "b")];
1.155 + val substx = [(TermC.empty, (Thm.term_of o the o (parse thy)) "x")];
1.156
1.157 val x1 = (Thm.term_of o the o (parse thy)) "a + b + x";
1.158 val x2 = (Thm.term_of o the o (parse thy)) "a + x + b";
1.159 @@ -260,34 +260,34 @@
1.160 val a = (Thm.term_of o the o (parse thy)) "a";
1.161 val b = (Thm.term_of o the o (parse thy)) "b";
1.162 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
1.163 -if term2str t' = "b + x + a" then ()
1.164 +if UnparseC.term2str t' = "b + x + a" then ()
1.165 else error "termorder.sml diff.behav ord_make_polynomial_in #11";
1.166
1.167 val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
1.168
1.169 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
1.170 -if term2str t' = "a + b + x" then ()
1.171 +if UnparseC.term2str t' = "a + b + x" then ()
1.172 else error "termorder.sml diff.behav ord_make_polynomial_in #13";
1.173
1.174 val ppp' = "-6 + -5*x + x^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2";
1.175 val ppp = (Thm.term_of o the o (parse thy)) ppp';
1.176 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
1.177 -if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
1.178 +if UnparseC.term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
1.179 else error "termorder.sml diff.behav ord_make_polynomial_in #14";
1.180
1.181 val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
1.182 -if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
1.183 +if UnparseC.term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
1.184 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
1.185
1.186 val ttt' = "(3*x + 5)/18";
1.187 val ttt = (Thm.term_of o the o (parse thy)) ttt';
1.188 val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
1.189 -if term2str uuu = "(5 + 3 * x) / 18" then ()
1.190 +if UnparseC.term2str uuu = "(5 + 3 * x) / 18" then ()
1.191 else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
1.192
1.193 (*============ inhibit exn WN120316 ==============================================
1.194 val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
1.195 -if term2str uuu = "(5 + 3 * x) / 18" then ()
1.196 +if UnparseC.term2str uuu = "(5 + 3 * x) / 18" then ()
1.197 else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
1.198 ============ inhibit exn WN120316 ==============================================*)
1.199
1.200 @@ -354,10 +354,10 @@
1.201 "~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
1.202 val Appl m = applicable_in p pt tac;
1.203 val Check_elementwise' (trm1, str, (trm2, trms)) = m;
1.204 -term2str trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
1.205 +UnparseC.term2str trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
1.206 str = "Assumptions";
1.207 -term2str trm2 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
1.208 -terms2str trms = "[\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n "^
1.209 +UnparseC.term2str trm2 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
1.210 +UnparseC.terms2str trms = "[\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n "^
1.211 " (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) is_poly_in 1 / 8 + sqrt (9 / 16) / 2\","^
1.212 "\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) "^
1.213 "has_degree_in 1 / 8 + sqrt (9 / 16) / 2 =\n2\","^
1.214 @@ -386,7 +386,7 @@
1.215 ((thy',ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
1.216 1 < length l (*true*);
1.217 val up = drop_last l;
1.218 - term2str (at_location up sc);
1.219 + UnparseC.term2str (at_location up sc);
1.220 (at_location up sc);
1.221 (*WAS val Term_Val1 _ = scan_up1 ys ((E,up,a,v,S,b),ss) (at_location up sc)
1.222 ... ???? ... is correct*)
1.223 @@ -410,8 +410,8 @@
1.224 ... Associated ... is correct*)
1.225 "~~~~~ fun associate, args:"; val (pt, _, (m as Check_elementwise' (consts,_,(consts_chkd,_))),
1.226 (Const ("Prog_Tac.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
1.227 -term2str consts;
1.228 -term2str consts';
1.229 +UnparseC.term2str consts;
1.230 +UnparseC.term2str consts';
1.231 if consts = consts' (*WAS false*) then () else error "Check_elementwise changed";
1.232 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
1.233 ( *----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------//*)
1.234 @@ -437,7 +437,7 @@
1.235 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.236 val asm = Ctree.get_assumptions pt p;
1.237 if f2str f = "[]" andalso
1.238 - terms2str asm = "[\"lhs (2 + -1 * x + x ^^^ 2 = 0) is_poly_in x\"," ^
1.239 + UnparseC.terms2str asm = "[\"lhs (2 + -1 * x + x ^^^ 2 = 0) is_poly_in x\"," ^
1.240 "\"lhs (2 + -1 * x + x ^^^ 2 = 0) has_degree_in x = 2\"]" then ()
1.241 else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
1.242
1.243 @@ -962,40 +962,40 @@
1.244
1.245 val rls = complete_square;
1.246 val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
1.247 -term2str t = "-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2";
1.248 +UnparseC.term2str t = "-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2";
1.249
1.250 val thm = num_str @{thm square_explicit1};
1.251 val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t;
1.252 -term2str t = "(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8";
1.253 +UnparseC.term2str t = "(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8";
1.254
1.255 val thm = num_str @{thm root_plus_minus};
1.256 val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
1.257 -term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
1.258 +UnparseC.term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
1.259 "\n2 / 2 - x = -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
1.260
1.261 (*the thm bdv_explicit2* here required to be constrained to ::real*)
1.262 val thm = num_str @{thm bdv_explicit2};
1.263 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1.264 -term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
1.265 +UnparseC.term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
1.266 "\n-1 * x = - (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
1.267
1.268 val thm = num_str @{thm bdv_explicit3};
1.269 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1.270 -term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
1.271 +UnparseC.term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
1.272 "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
1.273
1.274 val thm = num_str @{thm bdv_explicit2};
1.275 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1.276 -term2str t = "-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |"^
1.277 +UnparseC.term2str t = "-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |"^
1.278 "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
1.279
1.280 val rls = calculate_RootRat;
1.281 val SOME (t,asm) = rewrite_set_ thy true rls t;
1.282 -if term2str t =
1.283 +if UnparseC.term2str t =
1.284 "-1 * x = -1 + sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8) \<or>\nx = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))"
1.285 (*"-1 * x = -1 + sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8) |\nx = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))"..isabisac15*)
1.286 then () else error "(-8 - 2*x + x^^^2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT";
1.287 -(*SHOULD BE: term2str = "x = -2 | x = 4;*)
1.288 +(*SHOULD BE: UnparseC.term2str = "x = -2 | x = 4;*)
1.289
1.290
1.291 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
1.292 @@ -1004,7 +1004,7 @@
1.293 "---- test the erls ----";
1.294 val t1 = (Thm.term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1";
1.295 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
1.296 - val t' = term2str t;
1.297 + val t' = UnparseC.term2str t;
1.298 (*if t'= "HOL.True" then ()
1.299 else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
1.300 (* *)