1.1 --- a/test/Tools/isac/Knowledge/rational-1.sml Sun Oct 09 06:53:03 2022 +0200
1.2 +++ b/test/Tools/isac/Knowledge/rational-1.sml Sun Oct 09 07:44:22 2022 +0200
1.3 @@ -24,26 +24,26 @@
1.4 "-------- fun poly_of_term ---------------------------------------------------------------------";
1.5 "-------- fun poly_of_term ---------------------------------------------------------------------";
1.6 val thy = @{theory Isac_Knowledge};
1.7 -val vs = TermC.vars_of (TermC.str2term "12 * x \<up> 3 * y \<up> 4 * z \<up> 6");
1.8 +val vs = TermC.vars_of (TermC.parse_test @{context} "12 * x \<up> 3 * y \<up> 4 * z \<up> 6");
1.9
1.10 -val t = TermC.str2term "0 ::real";
1.11 +val t = TermC.parse_test @{context} "0 ::real";
1.12 if poly_of_term vs t = SOME [(0, [0, 0, 0])]
1.13 then () else error "poly_of_term 0 changed";
1.14
1.15 -val t = TermC.str2term "-3 + - 2 * x ::real";
1.16 +val t = TermC.parse_test @{context} "-3 + - 2 * x ::real";
1.17 if poly_of_term vs t = SOME [(~3, [0, 0, 0]), (~2, [1, 0, 0])]
1.18 then () else error "poly_of_term uminus changed";
1.19
1.20 -if poly_of_term vs (TermC.str2term "12::real") = SOME [(12, [0, 0, 0])]
1.21 +if poly_of_term vs (TermC.parse_test @{context} "12::real") = SOME [(12, [0, 0, 0])]
1.22 then () else error "poly_of_term 1 changed";
1.23
1.24 -if poly_of_term vs (TermC.str2term "x::real") = SOME [(1, [1, 0, 0])]
1.25 +if poly_of_term vs (TermC.parse_test @{context} "x::real") = SOME [(1, [1, 0, 0])]
1.26 then () else error "poly_of_term 2 changed";
1.27
1.28 -if poly_of_term vs (TermC.str2term "12 * x \<up> 3") = SOME [(12, [3, 0, 0])]
1.29 +if poly_of_term vs (TermC.parse_test @{context} "12 * x \<up> 3") = SOME [(12, [3, 0, 0])]
1.30 then () else error "poly_of_term 3 changed";
1.31 "~~~~~ fun poly_of_term , args:"; val (vs, t) =
1.32 - (vs, (TermC.str2term "12 * x \<up> 3"));
1.33 + (vs, (TermC.parse_test @{context} "12 * x \<up> 3"));
1.34
1.35 monom_of_term vs (1, replicate (length vs) 0) t;(*poly malformed 1 with x \<up> 3*)
1.36 "~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const (\<^const_name>\<open>times\<close>, _) $ m1 $ m2)) =
1.37 @@ -59,30 +59,30 @@
1.38 if (c, num |> HOLogic.dest_numeral |> list_update es (find_index (curry op = t) vs)) = (12, [3, 0, 0])
1.39 then () else error "monom_of_term (realpow): return value CHANGED";
1.40
1.41 -if poly_of_term vs (TermC.str2term "12 * x \<up> 3 * y \<up> 4 * z \<up> 6") = SOME [(12, [3, 4, 6])]
1.42 +if poly_of_term vs (TermC.parse_test @{context} "12 * x \<up> 3 * y \<up> 4 * z \<up> 6") = SOME [(12, [3, 4, 6])]
1.43 then () else error "poly_of_term 4 changed";
1.44
1.45 -if poly_of_term vs (TermC.str2term "1 + 2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + y") =
1.46 +if poly_of_term vs (TermC.parse_test @{context} "1 + 2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + y") =
1.47 SOME [(1, [0, 0, 0]), (1, [0, 1, 0]), (2, [3, 4, 6])]
1.48 then () else error "poly_of_term 5 changed";
1.49
1.50 (*poly_of_term is quite liberal:*)
1.51 (*the coefficient may be somewhere, the order of variables and the parentheses
1.52 within a monomial are arbitrary*)
1.53 -if poly_of_term vs (TermC.str2term "y \<up> 4 * (x \<up> 3 * 12 * z \<up> 6)") = SOME [(12, [3, 4, 6])]
1.54 +if poly_of_term vs (TermC.parse_test @{context} "y \<up> 4 * (x \<up> 3 * 12 * z \<up> 6)") = SOME [(12, [3, 4, 6])]
1.55 then () else error "poly_of_term 6 changed";
1.56
1.57 (*there may even be more than 1 coefficient:*)
1.58 -if poly_of_term vs (TermC.str2term "2 * y \<up> 4 * (x \<up> 3 * 6 * z \<up> 6)") = SOME [(12, [3, 4, 6])]
1.59 +if poly_of_term vs (TermC.parse_test @{context} "2 * y \<up> 4 * (x \<up> 3 * 6 * z \<up> 6)") = SOME [(12, [3, 4, 6])]
1.60 then () else error "poly_of_term 7 changed";
1.61
1.62 (*the order and the parentheses within monomials are arbitrary:*)
1.63 -if poly_of_term vs (TermC.str2term "2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + (7 * y \<up> 8 + 1)")
1.64 +if poly_of_term vs (TermC.parse_test @{context} "2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + (7 * y \<up> 8 + 1)")
1.65 = SOME [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 6])]
1.66 then () else error "poly_of_term 8 changed";
1.67
1.68 (*from --- rls norm_Rational downto fun gcd_poly ---*)
1.69 -val t = TermC.str2term (*copy from above: "::real" is not required due to " \<up> "*)
1.70 +val t = TermC.parse_test @{context} (*copy from above: "::real" is not required due to " \<up> "*)
1.71 ("(- 12 + 4 * y + 3 * x \<up> 2 + - 1 * (x \<up> 2 * y)) /" ^
1.72 "(- 18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)");
1.73 "~~~~~ fun cancel_p_, args:"; val (t) = (t);
1.74 @@ -99,9 +99,9 @@
1.75 "-------- fun is_poly --------------------------------------------------------------------------";
1.76 "-------- fun is_poly --------------------------------------------------------------------------";
1.77 "-------- fun is_poly --------------------------------------------------------------------------";
1.78 -if is_poly (TermC.str2term "2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + 7 * y \<up> 8 + 1")
1.79 +if is_poly (TermC.parse_test @{context} "2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + 7 * y \<up> 8 + 1")
1.80 then () else error "is_poly 1 changed";
1.81 -if not (is_poly (TermC.str2term "2 * (x \<up> 3 * y \<up> 4 * z \<up> 6 + 7) * y \<up> 8 + 1"))
1.82 +if not (is_poly (TermC.parse_test @{context} "2 * (x \<up> 3 * y \<up> 4 * z \<up> 6 + 7) * y \<up> 8 + 1"))
1.83 then () else error "is_poly 2 changed";
1.84
1.85 "-------- fun is_ratpolyexp --------------------------------------------------------------------";
1.86 @@ -122,7 +122,7 @@
1.87 "-------- fun term_of_poly ---------------------------------------------------------------------";
1.88 "-------- fun term_of_poly ---------------------------------------------------------------------";
1.89 val expT = HOLogic.realT
1.90 -val Free (_, baseT) = (hd o vars o TermC.str2term) "12 * x \<up> 3 * y \<up> 4 * z \<up> 6";
1.91 +val Free (_, baseT) = (hd o vars o TermC.parse_test @{context}) "12 * x \<up> 3 * y \<up> 4 * z \<up> 6";
1.92 val p = [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 5])]
1.93 val vs = TermC.vars_of (the (parseNEW ctxt "12 * x \<up> 3 * y \<up> 4 * z \<up> 6"))
1.94 (*precondition for [(c, es),...]: legth es = length vs*)
1.95 @@ -137,7 +137,7 @@
1.96 val ctxt = Proof_Context.init_global thy
1.97
1.98 (*------- standard case: *)
1.99 -val t = TermC.str2term "2 / 3 + 1 / 6 ::real";
1.100 +val t = TermC.parse_test @{context} "2 / 3 + 1 / 6 ::real";
1.101 "~~~~~ fun add_fraction_p_ , args:"; val ((_: theory), t) = (thy, t);
1.102 val SOME ((n1, d1), (n2, d2)) =
1.103 (*case*) check_frac_sum t (*of*);
1.104 @@ -175,7 +175,7 @@
1.105
1.106 (*------- 0 / m + 0 / n
1.107 20 years old bug found here: *)
1.108 -val t = TermC.str2term "0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + - 1 * q_0 / 24 * 0 \<up> 4)";
1.109 +val t = TermC.parse_test @{context} "0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + - 1 * q_0 / 24 * 0 \<up> 4)";
1.110 val SOME (t', _) = rewrite_set_ ctxt true norm_Rational t;
1.111 (*
1.112 :
1.113 @@ -195,7 +195,7 @@
1.114 *)
1.115 if UnparseC.term t' = "0 = c_2" then () else error "norm_Rational CHANGED"; (*isa2*)
1.116
1.117 -val t = TermC.str2term "0 / 12 + 0 / 24 ::real";
1.118 +val t = TermC.parse_test @{context} "0 / 12 + 0 / 24 ::real";
1.119 add_fraction_p_ @{theory} t;
1.120 "~~~~~ fun add_fraction_p_ , args:"; val ((_: theory), t) = (thy, t);
1.121 val SOME ((n1, d1), (n2, d2)) =
1.122 @@ -268,16 +268,16 @@
1.123 "-------- complex examples: rls norm_Rational --------------------------------------------------";
1.124 "-------- complex examples: rls norm_Rational --------------------------------------------------";
1.125 "-------- complex examples: rls norm_Rational --------------------------------------------------";
1.126 -val t = TermC.str2term "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0";
1.127 +val t = TermC.parse_test @{context} "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0";
1.128 val SOME (t', _) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t';
1.129 if UnparseC.term t' = "1 / 18 = 0" then () else error "rational.sml 1";
1.130
1.131 -val t = TermC.str2term "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";
1.132 +val t = TermC.parse_test @{context} "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";
1.133 val SOME (t',_) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t';
1.134 if UnparseC.term t' = "(237 + 65 * x) / 36 = 0" then ()
1.135 else error "rational.sml 2";
1.136
1.137 -val t = TermC.str2term "(1/2 + (5*x)/2) \<up> 2 - ((13*x)/2 - 5/2) \<up> 2 - (6*x) \<up> 2 + 29";
1.138 +val t = TermC.parse_test @{context} "(1/2 + (5*x)/2) \<up> 2 - ((13*x)/2 - 5/2) \<up> 2 - (6*x) \<up> 2 + 29";
1.139 val SOME (t',_) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t';
1.140 if UnparseC.term t' = "23 + 35 * x + - 72 * x \<up> 2" then ()
1.141 else error "rational.sml 3";
1.142 @@ -286,20 +286,20 @@
1.143 "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";
1.144 "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";
1.145 (*Schalk I, p.60 Nr. 215c *)
1.146 -val t = TermC.str2term "(a + b) \<up> 4 * (x - y) / ((x - y) \<up> 3 * (a + b) \<up> 2)";
1.147 +val t = TermC.parse_test @{context} "(a + b) \<up> 4 * (x - y) / ((x - y) \<up> 3 * (a + b) \<up> 2)";
1.148 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t;
1.149 if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + - 2 * x * y + y \<up> 2)"
1.150 then () else error "rational.sml: diff.behav. in norm_Rational_mg 7";
1.151
1.152 (*SRC Schalk I, p.66 Nr. 381b *)
1.153 -val t = TermC.str2term
1.154 +val t = TermC.parse_test @{context}
1.155 "(4*x \<up> 2 - 20*x + 25)/(2*x - 5) \<up> 3";
1.156 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t;
1.157 if UnparseC.term t = "1 / (- 5 + 2 * x)"
1.158 then () else error "rational.sml: diff.behav. in norm_Rational_mg 9";
1.159
1.160 (*Schalk I, p.60 Nr. 215c *)
1.161 -val t = TermC.str2term "(a + b) \<up> 4 * (x - y) / ((x - y) \<up> 3 * (a + b) \<up> 2)";
1.162 +val t = TermC.parse_test @{context} "(a + b) \<up> 4 * (x - y) / ((x - y) \<up> 3 * (a + b) \<up> 2)";
1.163 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t;
1.164 if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + - 2 * x * y + y \<up> 2)"
1.165 then () else error "Schalk I, p.60 Nr. 215c: with Isabelle2002 cancellation incomplete, changed";