1.1 --- a/test/Tools/isac/Knowledge/poly-2.sml Sun Jan 29 14:31:56 2023 +0100
1.2 +++ b/test/Tools/isac/Knowledge/poly-2.sml Mon Jan 30 09:47:18 2023 +0100
1.3 @@ -255,7 +255,7 @@
1.4 "~~~~~~~~~~~~~ fun get_basStr used twice --^^
1.5 "~~~~~~~~~~~~~ fun get_potStr used twice --^^
1.6 *)
1.7 -val t = TermC.parse_test @{context} "(1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) is_addUnordered";
1.8 +val t = ParseC.parse_test @{context} "(1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) is_addUnordered";
1.9
1.10 eval_is_addUnordered "xxx" "yyy" t @{context};
1.11 "~~~~~ fun eval_is_addUnordered , args:"; val ((thmid:string), _,
1.12 @@ -420,20 +420,20 @@
1.13 "-------- examples from textbook Schalk I ------------------------------------------------------";
1.14 "-------- examples from textbook Schalk I ------------------------------------------------------";
1.15 "-----SPB Schalk I p.63 No.267b ---";
1.16 -val t = TermC.parse_test @{context} "(5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)";
1.17 +val t = ParseC.parse_test @{context} "(5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)";
1.18 val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.19 if UnparseC.term t = "17 + 15 * x \<up> 2 + - 48 * x \<up> 4 + 3 * x \<up> 5 + 6 * x \<up> 7 +\n- 8 * x \<up> 9"
1.20 then () else error "poly.sml: diff.behav. in make_polynomial 1";
1.21
1.22 "-----SPB Schalk I p.63 No.275b ---";
1.23 -val t = TermC.parse_test @{context} "(3*x \<up> 2 - 2*x*y + y \<up> 2) * (x \<up> 2 - 2*y \<up> 2)";
1.24 +val t = ParseC.parse_test @{context} "(3*x \<up> 2 - 2*x*y + y \<up> 2) * (x \<up> 2 - 2*y \<up> 2)";
1.25 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.26 if UnparseC.term t =
1.27 "3 * x \<up> 4 + - 2 * x \<up> 3 * y + - 5 * x \<up> 2 * y \<up> 2 +\n4 * x * y \<up> 3 +\n- 2 * y \<up> 4"
1.28 then () else error "poly.sml: diff.behav. in make_polynomial 2";
1.29
1.30 "-----SPB Schalk I p.63 No.279b ---";
1.31 -val t = TermC.parse_test @{context} "(x-a)*(x-b)*(x-c)*(x-d)";
1.32 +val t = ParseC.parse_test @{context} "(x-a)*(x-b)*(x-c)*(x-d)";
1.33 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.34 if UnparseC.term t =
1.35 ("a * b * c * d + - 1 * a * b * c * x + - 1 * a * b * d * x +\na * b * x \<up> 2 +\n" ^
1.36 @@ -444,32 +444,32 @@
1.37 (*associate poly*)
1.38
1.39 "-----SPB Schalk I p.63 No.291 ---";
1.40 -val t = TermC.parse_test @{context} "(5+96*x \<up> 3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (- 15*x*(-8*x- 5)))";
1.41 +val t = ParseC.parse_test @{context} "(5+96*x \<up> 3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (- 15*x*(-8*x- 5)))";
1.42 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.43 if UnparseC.term t = "50 + - 770 * x + 4520 * x \<up> 2 + - 16320 * x \<up> 3 +\n- 26880 * x \<up> 4"
1.44 then () else error "poly.sml: diff.behav. in make_polynomial 4";
1.45
1.46 "-----SPB Schalk I p.64 No.295c ---";
1.47 -val t = TermC.parse_test @{context} "(13*a \<up> 4*b \<up> 9*c - 12*a \<up> 3*b \<up> 6*c \<up> 9) \<up> 2";
1.48 +val t = ParseC.parse_test @{context} "(13*a \<up> 4*b \<up> 9*c - 12*a \<up> 3*b \<up> 6*c \<up> 9) \<up> 2";
1.49 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.50 if UnparseC.term t =
1.51 "169 * a \<up> 8 * b \<up> 18 * c \<up> 2 +\n- 312 * a \<up> 7 * b \<up> 15 * c \<up> 10 +\n144 * a \<up> 6 * b \<up> 12 * c \<up> 18"
1.52 then ()else error "poly.sml: diff.behav. in make_polynomial 5";
1.53
1.54 "-----SPB Schalk I p.64 No.299a ---";
1.55 -val t = TermC.parse_test @{context} "(x - y)*(x + y)";
1.56 +val t = ParseC.parse_test @{context} "(x - y)*(x + y)";
1.57 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.58 if UnparseC.term t = "x \<up> 2 + - 1 * y \<up> 2"
1.59 then () else error "poly.sml: diff.behav. in make_polynomial 6";
1.60
1.61 "-----SPB Schalk I p.64 No.300c ---";
1.62 -val t = TermC.parse_test @{context} "(3*x \<up> 2*y - 1)*(3*x \<up> 2*y + 1)";
1.63 +val t = ParseC.parse_test @{context} "(3*x \<up> 2*y - 1)*(3*x \<up> 2*y + 1)";
1.64 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.65 if UnparseC.term t = "- 1 + 9 * x \<up> 4 * y \<up> 2"
1.66 then () else error "poly.sml: diff.behav. in make_polynomial 7";
1.67
1.68 "-----SPB Schalk I p.64 No.302 ---";
1.69 -val t = TermC.parse_test @{context}
1.70 +val t = ParseC.parse_test @{context}
1.71 "(13*x \<up> 2 + 5)*(13*x \<up> 2 - 5) - (5*x \<up> 2 + 3)*(5*x \<up> 2 - 3) - (12*x \<up> 2 + 4)*(12*x \<up> 2 - 4)";
1.72 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.73 if UnparseC.term t = "0"
1.74 @@ -477,47 +477,47 @@
1.75 (* RL?MG?: Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *)
1.76
1.77 "-----SPB Schalk I p.64 No.306a ---";
1.78 -val t = TermC.parse_test @{context} "((x \<up> 2 + 1)*(x \<up> 2 - 1)) \<up> 2";
1.79 +val t = ParseC.parse_test @{context} "((x \<up> 2 + 1)*(x \<up> 2 - 1)) \<up> 2";
1.80 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.81 if UnparseC.term t = "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8" then ()
1.82 else error "poly.sml: diff.behav. in 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 = - 2 * x \<up> 4";
1.83
1.84 (*WN071729 when reducing "rls reduce_012_" for Schaerding,
1.85 the above resulted in the term below ... but reduces from then correctly*)
1.86 -val t = TermC.parse_test @{context} "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8";
1.87 +val t = ParseC.parse_test @{context} "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8";
1.88 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.89 if UnparseC.term t = "1 + - 2 * x \<up> 4 + x \<up> 8"
1.90 then () else error "poly.sml: diff.behav. in make_polynomial 9b";
1.91
1.92 "-----SPB Schalk I p.64 No.296a ---";
1.93 -val t = TermC.parse_test @{context} "(x - a) \<up> 3";
1.94 +val t = ParseC.parse_test @{context} "(x - a) \<up> 3";
1.95 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.96
1.97 -val NONE = eval_is_even "aaa" "bbb" (TermC.parse_test @{context} "3::real") "ccc";
1.98 +val NONE = eval_is_even "aaa" "bbb" (ParseC.parse_test @{context} "3::real") "ccc";
1.99
1.100 if UnparseC.term t = "- 1 * a \<up> 3 + 3 * a \<up> 2 * x + - 3 * a * x \<up> 2 + x \<up> 3"
1.101 then () else error "poly.sml: diff.behav. in make_polynomial 10";
1.102
1.103 "-----SPB Schalk I p.64 No.296c ---";
1.104 -val t = TermC.parse_test @{context} "(-3*x - 4*y) \<up> 3";
1.105 +val t = ParseC.parse_test @{context} "(-3*x - 4*y) \<up> 3";
1.106 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.107 if UnparseC.term t = "- 27 * x \<up> 3 + - 108 * x \<up> 2 * y + - 144 * x * y \<up> 2 +\n- 64 * y \<up> 3"
1.108 then () else error "poly.sml: diff.behav. in make_polynomial 11";
1.109
1.110 "-----SPB Schalk I p.62 No.242c ---";
1.111 -val t = TermC.parse_test @{context} "x \<up> (-4)*(x \<up> (-4)*y \<up> (- 2)) \<up> (- 1)*y \<up> (- 2)";
1.112 +val t = ParseC.parse_test @{context} "x \<up> (-4)*(x \<up> (-4)*y \<up> (- 2)) \<up> (- 1)*y \<up> (- 2)";
1.113 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.114 if UnparseC.term t = "1"
1.115 then () else error "poly.sml: diff.behav. in make_polynomial 12";
1.116
1.117 "-----SPB Schalk I p.60 No.209a ---";
1.118 -val t = TermC.parse_test @{context} "a \<up> (7-x) * a \<up> x";
1.119 +val t = ParseC.parse_test @{context} "a \<up> (7-x) * a \<up> x";
1.120 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.121 if UnparseC.term t = "a \<up> 7"
1.122 then () else error "poly.sml: diff.behav. in make_polynomial 13";
1.123
1.124 "-----SPB Schalk I p.60 No.209d ---";
1.125 -val t = TermC.parse_test @{context} "d \<up> x * d \<up> (x+1) * d \<up> (2 - 2*x)";
1.126 +val t = ParseC.parse_test @{context} "d \<up> x * d \<up> (x+1) * d \<up> (2 - 2*x)";
1.127 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.128 if UnparseC.term t = "d \<up> 3"
1.129 then () else error "poly.sml: diff.behav. in make_polynomial 14";
1.130 @@ -526,7 +526,7 @@
1.131 "-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
1.132 "-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
1.133 "-----Schalk I p.64 No.303 ---";
1.134 -val t = TermC.parse_test @{context} "(a + 2*b)*(a \<up> 2 + 4*b \<up> 2)*(a - 2*b) - (a - 6*b)*(a \<up> 2 + 36*b \<up> 2)*(a + 6*b)";
1.135 +val t = ParseC.parse_test @{context} "(a + 2*b)*(a \<up> 2 + 4*b \<up> 2)*(a - 2*b) - (a - 6*b)*(a \<up> 2 + 36*b \<up> 2)*(a + 6*b)";
1.136 (*SOMETIMES LOOPS---------------------------------------------------------------------------\\*)
1.137 val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.138 if UnparseC.term t = "1280 * b \<up> 4"
1.139 @@ -538,49 +538,49 @@
1.140 "-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
1.141 "-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
1.142 "-----SPO ---";
1.143 -val t = TermC.parse_test @{context} "a + a + a";
1.144 +val t = ParseC.parse_test @{context} "a + a + a";
1.145 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.146 if UnparseC.term t = "3 * a" then ()
1.147 else error "poly.sml: diff.behav. in make_polynomial 16";
1.148 "-----SPO ---";
1.149 -val t = TermC.parse_test @{context} "a + b + b + b";
1.150 +val t = ParseC.parse_test @{context} "a + b + b + b";
1.151 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.152 if UnparseC.term t = "a + 3 * b" then ()
1.153 else error "poly.sml: diff.behav. in make_polynomial 17";
1.154 "-----SPO ---";
1.155 -val t = TermC.parse_test @{context} "b * a * a";
1.156 +val t = ParseC.parse_test @{context} "b * a * a";
1.157 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.158 if UnparseC.term t = "a \<up> 2 * b" then ()
1.159 else error "poly.sml: diff.behav. in make_polynomial 21";
1.160 "-----SPO ---";
1.161 -val t = TermC.parse_test @{context} "(a \<up> 2) \<up> 3";
1.162 +val t = ParseC.parse_test @{context} "(a \<up> 2) \<up> 3";
1.163 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.164 if UnparseC.term t = "a \<up> 6" then ()
1.165 else error "poly.sml: diff.behav. in make_polynomial 22";
1.166 "-----SPO ---";
1.167 -val t = TermC.parse_test @{context} "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";
1.168 +val t = ParseC.parse_test @{context} "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";
1.169 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.170 if UnparseC.term t = "x \<up> 3 * y + x \<up> 2 * y \<up> 2" then ()
1.171 else error "poly.sml: diff.behav. in make_polynomial 23";
1.172 "-----SPO ---";
1.173 -val t = TermC.parse_test @{context} "a * b * b \<up> (- 1) + a";
1.174 +val t = ParseC.parse_test @{context} "a * b * b \<up> (- 1) + a";
1.175 val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t; UnparseC.term t;
1.176 if UnparseC.term t = "2 * a" then ()
1.177 else error "poly.sml: diff.behav. in make_polynomial 25";
1.178 "-----SPO ---";
1.179 -val t = TermC.parse_test @{context} "a*c*b \<up> (2*n) + 3*a + 5*b \<up> (2*n)*c*b";
1.180 +val t = ParseC.parse_test @{context} "a*c*b \<up> (2*n) + 3*a + 5*b \<up> (2*n)*c*b";
1.181 val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t; UnparseC.term t;
1.182 if UnparseC.term t = "3 * a + 5 * b \<up> (1 + 2 * n) * c + a * b \<up> (2 * n) * c"
1.183 then () else error "poly.sml: diff.behav. in make_polynomial 26";
1.184
1.185 (*MG030627 -------------vvv-: Verschachtelte Terme -----------*)
1.186 "-----SPO ---";
1.187 -val t = TermC.parse_test @{context} "(1 + (x*y*a) + x) \<up> (1 + (x*y*a) + x)";
1.188 +val t = ParseC.parse_test @{context} "(1 + (x*y*a) + x) \<up> (1 + (x*y*a) + x)";
1.189 val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t;
1.190 if UnparseC.term t = "(1 + x + a * x * y) \<up> (1 + x + a * x * y)"
1.191 then () else error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*)
1.192
1.193 -val t = TermC.parse_test @{context} "(1 + x*(y*z)*zz) \<up> (1 + x*(y*z)*zz)";
1.194 +val t = ParseC.parse_test @{context} "(1 + x*(y*z)*zz) \<up> (1 + x*(y*z)*zz)";
1.195 val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t;
1.196 if UnparseC.term t = "(1 + x * y * z * zz) \<up> (1 + x * y * z * zz)"
1.197 then () else error "poly.sml: diff.behav. in make_polynomial 28";
1.198 @@ -611,7 +611,7 @@
1.199 (*default_print_depth 7;*)
1.200 val where_rls = (#where_rls o Problem.from_store @{context}) ["polynomial", "simplification"];
1.201 (*default_print_depth 3;*)
1.202 -val t = TermC.parse_test @{context} "((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)) is_polyexp";
1.203 +val t = ParseC.parse_test @{context} "((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)) is_polyexp";
1.204 val SOME (t',_) = rewrite_set_ thy false where_rls t;
1.205 if t' = @{term True} then ()
1.206 else error "poly.sml: diff.behav. in check pbl 'polynomial..";
1.207 @@ -690,14 +690,14 @@
1.208 "-------- ord_make_polynomial ------------------------------------------------------------------";
1.209 "-------- ord_make_polynomial ------------------------------------------------------------------";
1.210 "-------- ord_make_polynomial ------------------------------------------------------------------";
1.211 -val t1 = TermC.parse_test @{context} "2 * b + (3 * a + 3 * b)";
1.212 -val t2 = TermC.parse_test @{context} "(3 * a + 3 * b) + 2 * b";
1.213 +val t1 = ParseC.parse_test @{context} "2 * b + (3 * a + 3 * b)";
1.214 +val t2 = ParseC.parse_test @{context} "(3 * a + 3 * b) + 2 * b";
1.215
1.216 if ord_make_polynomial true @{context} [] (t1, t2) then ()
1.217 else error "poly.sml: diff.behav. in ord_make_polynomial";
1.218 (*SO: WHY IS THERE NO REWRITING ...*)
1.219
1.220 -val term = TermC.parse_test @{context} "2*b + (3*a + 3*b)";
1.221 +val term = ParseC.parse_test @{context} "2*b + (3*a + 3*b)";
1.222 (*+++*)val NONE = rewrite_set_ (Proof_Context.init_global @{theory "Isac_Knowledge"}) false order_add_mult term;
1.223 (*
1.224 WHY IS THERE NO REWRITING ?!?