1.1 --- a/test/Tools/isac/Knowledge/poly-1.sml Thu Jul 28 11:43:27 2022 +0200
1.2 +++ b/test/Tools/isac/Knowledge/poly-1.sml Sat Jul 30 16:47:45 2022 +0200
1.3 @@ -263,9 +263,9 @@
1.4 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
1.5 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
1.6 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
1.7 +val ctxt = Proof_Context.init_global @{theory}
1.8 val t = TermC.str2term "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";
1.9 -Rewrite.trace_on := false; (*true false*)
1.10 -val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.11 +val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.12 UnparseC.term t = "x \<up> 2 * y \<up> 2 + x \<up> 3 * y";
1.13 if UnparseC.term t = "x \<up> 3 * y + x \<up> 2 * y \<up> 2" then ()
1.14 else error "poly.sml: diff.behav. in make_polynomial 23";
1.15 @@ -413,32 +413,32 @@
1.16 "-------- check make_polynomial with simple terms ----------------------------------------------";
1.17 "----- check 1 ---";
1.18 val t = TermC.str2term "2*3*a";
1.19 -val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
1.20 +val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
1.21 if UnparseC.term t = "6 * a" then () else error "check make_polynomial 1";
1.22
1.23 "----- check 2 ---";
1.24 val t = TermC.str2term "2*a + 3*a";
1.25 -val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
1.26 +val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
1.27 if UnparseC.term t = "5 * a" then () else error "check make_polynomial 2";
1.28
1.29 "----- check 3 ---";
1.30 val t = TermC.str2term "2*a + 3*a + 3*a";
1.31 -val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
1.32 +val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
1.33 if UnparseC.term t = "8 * a" then () else error "check make_polynomial 3";
1.34
1.35 "----- check 4 ---";
1.36 val t = TermC.str2term "3*a - 2*a";
1.37 -val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
1.38 +val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
1.39 if UnparseC.term t = "a" then () else error "check make_polynomial 4";
1.40
1.41 "----- check 5 ---";
1.42 val t = TermC.str2term "4*(3*a - 2*a)";
1.43 -val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
1.44 +val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
1.45 if UnparseC.term t = "4 * a" then () else error "check make_polynomial 5";
1.46
1.47 "----- check 6 ---";
1.48 val t = TermC.str2term "4*(3*a \<up> 2 - 2*a \<up> 2)";
1.49 -val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
1.50 +val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
1.51 if UnparseC.term t = "4 * a \<up> 2" then () else error "check make_polynomial 6";
1.52
1.53 "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
1.54 @@ -447,7 +447,7 @@
1.55 val thy = @{theory "Isac_Knowledge"};
1.56 "===== works for a simple example, see rewrite.sml -- fun app_rev ===";
1.57 val t = TermC.str2term "x \<up> 2 * x";
1.58 -val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
1.59 +val SOME (t', _) = rewrite_set_ ctxt true order_mult_ t;
1.60 if UnparseC.term t' = "x * x \<up> 2" then ()
1.61 else error "poly.sml Poly.is_multUnordered doesn't work";
1.62
1.63 @@ -478,7 +478,7 @@
1.64 | _ => error "poly.sml diff. eval_is_multUnordered";
1.65
1.66 "----- rewrite_set_ STILL DIDN'T WORK";
1.67 -val SOME (t, _) = rewrite_set_ thy true order_mult_ t;
1.68 +val SOME (t, _) = rewrite_set_ ctxt true order_mult_ t;
1.69 UnparseC.term t;
1.70
1.71
1.72 @@ -637,7 +637,7 @@
1.73 "-------- fun is_multUnordered b * a * a ------------------------------------------------------";
1.74 "-------- fun is_multUnordered b * a * a ------------------------------------------------------";
1.75 val t = TermC.str2term "b * a * a";
1.76 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.77 +val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.78 if UnparseC.term t = "a \<up> 2 * b" then ()
1.79 else error "poly.sml: diff.behav. in make_polynomial 21";
1.80
1.81 @@ -660,7 +660,7 @@
1.82 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
1.83 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
1.84 val t = TermC.str2term "2*3*a";
1.85 -val SOME (t', _) = rewrite_set_ thy false make_polynomial t;
1.86 +val SOME (t', _) = rewrite_set_ ctxt false make_polynomial t;
1.87 (*+*)if UnparseC.term t' = "6 * a" then () else error "rewrite_set_ 2*3*a CHANGED";
1.88 (*
1.89 ## try calc: "Groups.times_class.times"
1.90 @@ -701,7 +701,7 @@
1.91 val thy = @{theory AlgEin};
1.92 val ctxt = Proof_Context.init_global thy;
1.93
1.94 -val SOME (f',_) = rewrite_set_ thy false norm_Poly
1.95 +val SOME (f',_) = rewrite_set_ ctxt false norm_Poly
1.96 (TermC.str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");
1.97 if UnparseC.term f' = "L = 2 * 2 * k + 2 * - 4 * q + senkrecht + oben"
1.98 then ((*norm_Poly NOT COMPLETE -- TODO MG*))
1.99 @@ -730,37 +730,37 @@
1.100 "-------- complex examples from textbook Schalk I ----------------------------------------------";
1.101 "-------- complex examples from textbook Schalk I ----------------------------------------------";
1.102 val t = TermC.str2term "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8";
1.103 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.104 +val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.105 if (UnparseC.term t) = "1 + - 2 * x \<up> 4 + x \<up> 8"
1.106 then () else error "poly.sml: diff.behav. in make_polynomial 9b";
1.107
1.108 "-----SPB Schalk I p.64 No.296a ---";
1.109 val t = TermC.str2term "(x - a) \<up> 3";
1.110 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.111 +val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.112 if (UnparseC.term t) = "- 1 * a \<up> 3 + 3 * a \<up> 2 * x + - 3 * a * x \<up> 2 + x \<up> 3"
1.113 then () else error "poly.sml: diff.behav. in make_polynomial 10";
1.114
1.115 "-----SPB Schalk I p.64 No.296c ---";
1.116 val t = TermC.str2term "(-3*x - 4*y) \<up> 3";
1.117 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.118 +val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.119 if (UnparseC.term t) = "- 27 * x \<up> 3 + - 108 * x \<up> 2 * y + - 144 * x * y \<up> 2 +\n- 64 * y \<up> 3"
1.120 then () else error "poly.sml: diff.behav. in make_polynomial 11";
1.121
1.122 "-----SPB Schalk I p.62 No.242c ---";
1.123 val t = TermC.str2term "x \<up> (- 4)*(x \<up> (- 4)*y \<up> (- 2)) \<up> (- 1)*y \<up> (- 2)";
1.124 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.125 +val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.126 if (UnparseC.term t) = "1"
1.127 then () else error "poly.sml: diff.behav. in make_polynomial 12";
1.128
1.129 "-----SPB Schalk I p.60 No.209a ---";
1.130 val t = TermC.str2term "a \<up> (7-x) * a \<up> x";
1.131 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.132 +val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.133 if UnparseC.term t = "a \<up> 7"
1.134 then () else error "poly.sml: diff.behav. in make_polynomial 13";
1.135
1.136 "-----SPB Schalk I p.60 No.209d ---";
1.137 val t = TermC.str2term "d \<up> x * d \<up> (x+1) * d \<up> (2 - 2*x)";
1.138 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.139 +val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.140 if UnparseC.term t = "d \<up> 3"
1.141 then () else error "poly.sml: diff.behav. in make_polynomial 14";
1.142
1.143 @@ -770,28 +770,28 @@
1.144 "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
1.145 "-----SPO ---";
1.146 val t = TermC.str2term "a \<up> 2*a \<up> (- 2)";
1.147 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.148 +val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.149 if UnparseC.term t = "1" then ()
1.150 else error "poly.sml: diff.behav. in make_polynomial 15";
1.151
1.152 "-----SPO ---";
1.153 val t = TermC.str2term "a \<up> 2*b*b \<up> (- 1)";
1.154 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.155 +val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.156 if UnparseC.term t = "a \<up> 2" then ()
1.157 else error "poly.sml: diff.behav. in make_polynomial 18";
1.158 "-----SPO ---";
1.159 val t = TermC.str2term "a \<up> 2*a \<up> (- 2)";
1.160 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.161 +val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.162 if (UnparseC.term t) = "1" then ()
1.163 else error "poly.sml: diff.behav. in make_polynomial 19";
1.164 "-----SPO ---";
1.165 val t = TermC.str2term "b + a - b";
1.166 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.167 +val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.168 if (UnparseC.term t) = "a" then ()
1.169 else error "poly.sml: diff.behav. in make_polynomial 20";
1.170
1.171 "-----SPO ---";
1.172 val t = TermC.parseNEW' ctxt "a \<up> 2 * (-a) \<up> 2";
1.173 -val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t;
1.174 +val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.175 if (UnparseC.term t) = "a \<up> 4" then ()
1.176 else error "poly.sml: diff.behav. in make_polynomial 24";