1.1 --- a/src/Tools/isac/TODO.txt Sat Mar 17 11:06:46 2012 +0100
1.2 +++ b/src/Tools/isac/TODO.txt Sat Mar 17 12:52:30 2012 +0100
1.3 @@ -154,13 +154,23 @@
1.4 WN120314 changeset a393bb9f5e9f drops root equations.
1.5 see test/Tools/isac/Knowledge/rootrateq.sml
1.6 --------------------------------------------------------------------------------
1.7 -WN120317.TODO dropped rateq:
1.8 +WN120317.TODO changeset 977788dfed26 dropped rateq:
1.9 # test --- repair NO asms from rls RatEq_eliminate --- shows error from 2002
1.10 # test --- solve (1/x = 5, x) by me --- and --- x / (x ^ 2 - 6 * x + 9) - ...:
1.11 investigation Check_elementwise stopped due to too much effort finding out,
1.12 why Check_elementwise worked in 2002 in spite of the error.
1.13 --------------------------------------------------------------------------------
1.14 +WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeind
1.15 --------------------------------------------------------------------------------
1.16 +WN120317.TODO found by test --- interSteps for Schalk 299a --- that
1.17 + NO test with 'interSteps' is checked properly (exn on changed behaviour)
1.18 --------------------------------------------------------------------------------
1.19 --------------------------------------------------------------------------------
1.20 --------------------------------------------------------------------------------
1.21 +--------------------------------------------------------------------------------
1.22 +--------------------------------------------------------------------------------
1.23 +uncomment test/../root,equation,poly.sml (Isabelle 2002 --> 2011)
1.24 +
1.25 +# WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeind
1.26 +# WN120317.TODO found by test --- interSteps for Schalk 299a --- that
1.27 +NO test with 'interSteps' is checked properly (exn on changed behaviour)
2.1 --- a/test/Tools/isac/Knowledge/equation.sml Sat Mar 17 11:06:46 2012 +0100
2.2 +++ b/test/Tools/isac/Knowledge/equation.sml Sat Mar 17 12:52:30 2012 +0100
2.3 @@ -11,8 +11,8 @@
2.4 "-----------------------------------------------------------------";
2.5 "-----------------------------------------------------------------";
2.6
2.7 -(*=== inhibit exn ?=============================================================
2.8 -val thy = (theory "Isac");
2.9 +val thy = @{theory "Equation"}
2.10 +val ctxt = ProofContext.init_global thy;
2.11
2.12 "----------- CAS input -------------------------------------------";
2.13 "----------- CAS input -------------------------------------------";
2.14 @@ -28,4 +28,4 @@
2.15 show_pt pt;
2.16 if p = ([], Res) andalso term2str res = "[x = 1]" then ()
2.17 else error "equation.sml behav.changed for CAS solve (x+1=2, x))";
2.18 -===== inhibit exn ?===========================================================*)
2.19 +
3.1 --- a/test/Tools/isac/Knowledge/poly.sml Sat Mar 17 11:06:46 2012 +0100
3.2 +++ b/test/Tools/isac/Knowledge/poly.sml Sat Mar 17 12:52:30 2012 +0100
3.3 @@ -4,22 +4,20 @@
3.4
3.5 12345678901234567890123456789012345678901234567890123456789012345678901234567890
3.6 10 20 30 40 50 60 70 80
3.7 +LEGEND:
3.8 +WN060104: examples marked with 'SPB' came into 'exp_IsacCore_Simp_Poly_Book.xml'
3.9 + examples marked with 'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml'
3.10 *)
3.11 -(*******************************************************************************
3.12 - WN060104 'SPB' came into 'exp_IsacCore_Simp_Poly_Book.xml'
3.13 - 'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml'
3.14 -*******************************************************************************)
3.15 +
3.16 "--------------------------------------------------------";
3.17 "--------------------------------------------------------";
3.18 "table of contents --------------------------------------";
3.19 "--------------------------------------------------------";
3.20 "-------- check is'_polyexp is_polyexp ------------------";
3.21 -"-------- build Script Expand_binoms --------------------";
3.22 -"-------- investigate (new) uniary minus ----------------";
3.23 +"-------- investigate (new 2002) uniary minus -----------";
3.24 "-------- check make_polynomial with simple terms -------";
3.25 "-------- fun is_multUnordered --------------------------";
3.26 "-------- examples from textbook Schalk I ---------------";
3.27 -"-------- Script 'simplification for_polynomials' -------";
3.28 "-------- check pbl 'polynomial simplification' --------";
3.29 "-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
3.30 "-------- interSteps for Schalk 299a --------------------";
3.31 @@ -29,7 +27,6 @@
3.32 "--------------------------------------------------------";
3.33 "--------------------------------------------------------";
3.34
3.35 -(*=== inhibit exn ?=============================================================
3.36
3.37 "-------- check is'_polyexp is_polyexp ------------------";
3.38 "-------- check is'_polyexp is_polyexp ------------------";
3.39 @@ -37,53 +34,10 @@
3.40 if is_polyexp @{term "x / x"}
3.41 then error "poly.sml: check is'_polyexp is_polyexp" else ();
3.42
3.43 -
3.44 -"-------- build Script Expand_binoms -----------------------------";
3.45 -"-------- build Script Expand_binoms -----------------------------";
3.46 -"-------- build Script Expand_binoms -----------------------------";
3.47 -val scr_expand_binoms =
3.48 -"Script Expand_binoms t_t =" ^
3.49 -"(Repeat " ^
3.50 -"((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ " ^
3.51 -" (Try (Repeat (Rewrite real_plus_binom_times False))) @@ " ^
3.52 -" (Try (Repeat (Rewrite real_minus_binom_pow2 False))) @@ " ^
3.53 -" (Try (Repeat (Rewrite real_minus_binom_times False))) @@ " ^
3.54 -" (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ " ^
3.55 -" (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ " ^
3.56 -
3.57 -" (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
3.58 -" (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
3.59 -" (Try (Repeat (Rewrite add_0_left False))) @@ " ^
3.60 -
3.61 -" (Try (Repeat (Calculate PLUS ))) @@ " ^
3.62 -" (Try (Repeat (Calculate TIMES ))) @@ " ^
3.63 -" (Try (Repeat (Calculate POWER))) @@ " ^
3.64 -
3.65 -" (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
3.66 -" (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
3.67 -" (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
3.68 -" (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
3.69 -
3.70 -" (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
3.71 -" (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
3.72 -
3.73 -" (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
3.74 -" (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
3.75 -
3.76 -" (Try (Repeat (Calculate PLUS ))) @@ " ^
3.77 -" (Try (Repeat (Calculate TIMES ))) @@ " ^
3.78 -" (Try (Repeat (Calculate POWER)))) " ^
3.79 -" t_t)";
3.80 -(*
3.81 -val scr_expand_binoms =
3.82 -"Script Expand_binoms t_t = t_t";
3.83 -*)
3.84 -parse thy scr_expand_binoms;
3.85 -
3.86 -
3.87 -"-------- investigate (new) uniary minus ----------------";
3.88 -"-------- investigate (new) uniary minus ----------------";
3.89 -"-------- investigate (new) uniary minus ----------------";
3.90 +"-------- investigate (new 2002) uniary minus -----------";
3.91 +"-------- investigate (new 2002) uniary minus -----------";
3.92 +"-------- investigate (new 2002) uniary minus -----------";
3.93 +(*---------------------------------------------- vvvvvvvvvvvvvv -----------------------*)
3.94 val t = (#prop o rep_thm) @{thm real_diff_0}; (*"0 - ?x = - ?x"*)
3.95 atomty t;
3.96 (*** -------------
3.97 @@ -94,32 +48,58 @@
3.98 *** . . . Var ((x, 0), real)
3.99 *** . . Const ( uminus, real => real)
3.100 *** . . . Var ((x, 0), real) *)
3.101 +case t of
3.102 + Const ("HOL.Trueprop", _) $
3.103 + (Const ("HOL.eq", _) $
3.104 + (Const ("Groups.minus_class.minus", _) $ Const ("Groups.zero_class.zero", _) $
3.105 + Var (("x", 0), _)) $
3.106 + (Const ("Groups.uminus_class.uminus", _) $ Var (("x", 0), _))) => ()
3.107 +| _ => error "internal representation of \"0 - ?x = - ?x\" changed";
3.108
3.109 +(*----------------------------------- vvvv --------------------------------------------*)
3.110 val t = (term_of o the o (parse thy)) "-1";
3.111 atomty t;
3.112 (*** -------------
3.113 *** Free ( -1, real) *)
3.114 +case t of
3.115 + Free ("-1", _) => ()
3.116 +| _ => error "internal representation of \"-1\" changed";
3.117 +(*----------------------------------- vvvvv -------------------------------------------*)
3.118 val t = (term_of o the o (parse thy)) "- 1";
3.119 atomty t;
3.120 (*** -------------
3.121 *** Const ( uminus, real => real)
3.122 *** . Free ( 1, real) *)
3.123 +case t of
3.124 + Const ("Groups.uminus_class.uminus", _) $ Free ("1", _) => ()
3.125 +| _ => error "internal representation of \"- 1\" changed";
3.126
3.127 -val t = (term_of o the o (parse thy)) "-x"; (*1-x syntyx error !!!*)
3.128 +"======= these external values all have the same internal representation";
3.129 +(* "1-x" causes syntyx error --- binary minus detected by blank inbetween !!!*)
3.130 +(*----------------------------------- vvvvv -------------------------------------------*)
3.131 +val t = (term_of o the o (parse thy)) "-x";
3.132 atomty t;
3.133 (**** -------------
3.134 *** Free ( -x, real)*)
3.135 +case t of
3.136 + Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()
3.137 +| _ => error "internal representation of \"-x\" changed";
3.138 +(*----------------------------------- vvvvv -------------------------------------------*)
3.139 val t = (term_of o the o (parse thy)) "- x";
3.140 atomty t;
3.141 (**** -------------
3.142 *** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)
3.143 +case t of
3.144 + Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()
3.145 +| _ => error "internal representation of \"- x\" changed";
3.146 +(*----------------------------------- vvvvvv ------------------------------------------*)
3.147 val t = (term_of o the o (parse thy)) "-(x)";
3.148 atomty t;
3.149 (**** -------------
3.150 *** Free ( -x, real)*)
3.151 -
3.152 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
3.153 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
3.154 +case t of
3.155 + Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()
3.156 +| _ => error "internal representation of \"-(x)\" changed";
3.157
3.158 "-------- check make_polynomial with simple terms -------";
3.159 "-------- check make_polynomial with simple terms -------";
3.160 @@ -154,7 +134,6 @@
3.161 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
3.162 if term2str t = "4 * a ^^^ 2" then () else error "check make_polynomial 6";
3.163
3.164 -
3.165 "-------- fun is_multUnordered --------------------------";
3.166 "-------- fun is_multUnordered --------------------------";
3.167 "-------- fun is_multUnordered --------------------------";
3.168 @@ -195,108 +174,77 @@
3.169 val SOME (t, _) = rewrite_set_ thy true order_mult_ t;
3.170 term2str t;
3.171
3.172 -
3.173 "-------- examples from textbook Schalk I ---------------";
3.174 "-------- examples from textbook Schalk I ---------------";
3.175 "-------- examples from textbook Schalk I ---------------";
3.176 "-----SPB Schalk I p.63 No.267b ---";
3.177 -trace_rewrite := true; tracing "-----SPB Schalk I p.63 No.267b ---begin";
3.178 -val t = str2term
3.179 - "(5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1)";
3.180 +val t = str2term "(5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1)";
3.181 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
3.182 -term2str t;
3.183 -trace_rewrite := false; tracing "-----SPB Schalk I p.63 No.267b ---end";
3.184 -if (term2str t) =
3.185 -"17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"
3.186 -then ()
3.187 -else error "poly.sml: diff.behav. in make_polynomial 1";
3.188 +if (term2str t) = "17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"
3.189 +then () else error "poly.sml: diff.behav. in make_polynomial 1";
3.190
3.191 "-----SPB Schalk I p.63 No.275b ---";
3.192 - val t = str2term
3.193 - "(3*x^^^2 - 2*x*y + y^^^2) * (x^^^2 - 2*y^^^2)";
3.194 - val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
3.195 - term2str t;
3.196 -if (term2str t) =
3.197 -"3 * x ^^^ 4 + -2 * x ^^^ 3 * y + -5 * x ^^^ 2 * y ^^^ 2 + \
3.198 -\4 * x * y ^^^ 3 +\n-2 * y ^^^ 4"
3.199 -then ()
3.200 -else error "poly.sml: diff.behav. in make_polynomial 2";
3.201 +val t = str2term "(3*x^^^2 - 2*x*y + y^^^2) * (x^^^2 - 2*y^^^2)";
3.202 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
3.203 +if (term2str t) = ("3 * x ^^^ 4 + -2 * x ^^^ 3 * y + -5 * x ^^^ 2 * y ^^^ 2 + " ^
3.204 + "4 * x * y ^^^ 3 +\n-2 * y ^^^ 4")
3.205 +then () else error "poly.sml: diff.behav. in make_polynomial 2";
3.206
3.207 "-----SPB Schalk I p.63 No.279b ---";
3.208 - val t = str2term
3.209 - "(x-a)*(x-b)*(x-c)*(x-d)";
3.210 - val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
3.211 - term2str t;
3.212 -(* Richtig! *)
3.213 +val t = str2term "(x-a)*(x-b)*(x-c)*(x-d)";
3.214 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
3.215 if (term2str t) =
3.216 -"a * b * c * d + -1 * a * b * c * x + -1 * a * b * d * x + a * b * x ^^^ 2 +\n-1 * a * c * d * x +\na * c * x ^^^ 2 +\na * d * x ^^^ 2 +\n-1 * a * x ^^^ 3 +\n-1 * b * c * d * x +\nb * c * x ^^^ 2 +\nb * d * x ^^^ 2 +\n-1 * b * x ^^^ 3 +\nc * d * x ^^^ 2 +\n-1 * c * x ^^^ 3 +\n-1 * d * x ^^^ 3 +\nx ^^^ 4"
3.217 -then ()
3.218 -else error "poly.sml: diff.behav. in make_polynomial 3";
3.219 + ("a * b * c * d + -1 * a * b * c * x + -1 * a * b * d * x + a * b * x ^^^ 2 +\n" ^
3.220 + "-1 * a * c * d * x +\na * c * x ^^^ 2 +\na * d * x ^^^ 2 +\n-1 * a * x ^^^ 3 +\n" ^
3.221 + "-1 * b * c * d * x +\nb * c * x ^^^ 2 +\nb * d * x ^^^ 2 +\n-1 * b * x ^^^ 3 +\n" ^
3.222 + "c * d * x ^^^ 2 +\n-1 * c * x ^^^ 3 +\n-1 * d * x ^^^ 3 +\nx ^^^ 4")
3.223 +then () else error "poly.sml: diff.behav. in make_polynomial 3";
3.224
3.225 "-----SPB Schalk I p.63 No.291 ---";
3.226 - val t = str2term
3.227 - "(5+96*x^^^3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (-15*x*(-8*x- 5)))";
3.228 - val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
3.229 - term2str t;
3.230 -if (term2str t) =
3.231 -"50 + -770 * x + 4520 * x ^^^ 2 + -16320 * x ^^^ 3 + -26880 * x ^^^ 4"
3.232 -then ()
3.233 -else error "poly.sml: diff.behav. in make_polynomial 4";
3.234 +val t = str2term "(5+96*x^^^3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (-15*x*(-8*x- 5)))";
3.235 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
3.236 +if (term2str t) = "50 + -770 * x + 4520 * x ^^^ 2 + -16320 * x ^^^ 3 + -26880 * x ^^^ 4"
3.237 +then () else error "poly.sml: diff.behav. in make_polynomial 4";
3.238
3.239 "-----SPB Schalk I p.64 No.295c ---";
3.240 - val t = str2term
3.241 - "(13*a^^^4*b^^^9*c - 12*a^^^3*b^^^6*c^^^9)^^^2";
3.242 - val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
3.243 - term2str t;
3.244 -if (term2str t) =
3.245 -"169 * a ^^^ 8 * b ^^^ 18 * c ^^^ 2 + -312 * a ^^^ 7 * b ^^^ 15 * c ^^^ 10\
3.246 -\ +\n144 * a ^^^ 6 * b ^^^ 12 * c ^^^ 18"
3.247 -then ()
3.248 -else error "poly.sml: diff.behav. in make_polynomial 5";
3.249 +val t = str2term "(13*a^^^4*b^^^9*c - 12*a^^^3*b^^^6*c^^^9)^^^2";
3.250 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
3.251 +if (term2str t) = ("169 * a ^^^ 8 * b ^^^ 18 * c ^^^ 2 + -312 * a ^^^ 7 * b ^^^ 15 * c ^^^ 10" ^
3.252 + " +\n144 * a ^^^ 6 * b ^^^ 12 * c ^^^ 18")
3.253 +then ()else error "poly.sml: diff.behav. in make_polynomial 5";
3.254
3.255 "-----SPB Schalk I p.64 No.299a ---";
3.256 - val t = str2term
3.257 - "(x - y)*(x + y)";
3.258 - val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
3.259 - term2str t;
3.260 -(*
3.261 -if (term2str t) = "x ^^^ 2 + -1 * y ^^^ 2" then ()
3.262 -else error "poly.sml: diff.behav. in make_polynomial 6";
3.263 -*)
3.264 +val t = str2term "(x - y)*(x + y)";
3.265 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
3.266 +if (term2str t) = "x ^^^ 2 + -1 * y ^^^ 2"
3.267 +then () else error "poly.sml: diff.behav. in make_polynomial 6";
3.268
3.269 "-----SPB Schalk I p.64 No.300c ---";
3.270 - val t = str2term
3.271 - "(3*x^^^2*y - 1)*(3*x^^^2*y + 1)";
3.272 - val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
3.273 - term2str t;
3.274 -if (term2str t) =
3.275 -"-1 + 9 * x ^^^ 4 * y ^^^ 2"
3.276 -then ()
3.277 -else error "poly.sml: diff.behav. in make_polynomial 7";
3.278 +val t = str2term "(3*x^^^2*y - 1)*(3*x^^^2*y + 1)";
3.279 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
3.280 +if (term2str t) = "-1 + 9 * x ^^^ 4 * y ^^^ 2"
3.281 +then () else error "poly.sml: diff.behav. in make_polynomial 7";
3.282
3.283 "-----SPB Schalk I p.64 No.302 ---";
3.284 val t = str2term
3.285 - "(13*x^^^2 + 5)*(13*x^^^2 - 5) - (5*x^^^2 + 3)*(5*x^^^2 - 3) - (12*x^^^2 + 4)*(12*x^^^2 - 4)";
3.286 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
3.287 -if term2str t = "0" then ()
3.288 -else error "poly.sml: diff.behav. in make_polynomial 8";
3.289 -(* Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *)
3.290 -
3.291 + "(13*x^^^2 + 5)*(13*x^^^2 - 5) - (5*x^^^2 + 3)*(5*x^^^2 - 3) - (12*x^^^2 + 4)*(12*x^^^2 - 4)";
3.292 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
3.293 +if term2str t = "0"
3.294 +then () else error "poly.sml: diff.behav. in make_polynomial 8";
3.295 +(* RL?MG?: Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *)
3.296
3.297 "-----SPB Schalk I p.64 No.306a ---";
3.298 val t = str2term "((x^^^2 + 1)*(x^^^2 - 1))^^^2";
3.299 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
3.300 if (term2str t) = "1 + 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 + x ^^^ 8" then ()
3.301 -else error "poly.sml: diff.behav. in make_polynomial: not confluent \
3.302 - \2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 = -2 * x ^^^ 4 works again";
3.303 -
3.304 +else error "poly.sml: diff.behav. in 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 = -2 * x ^^^ 4";
3.305
3.306 (*WN071729 when reducing "rls reduce_012_" for Schaerding,
3.307 the above resulted in the term below ... but reduces from then correctly*)
3.308 val t = str2term "1 + 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 + x ^^^ 8";
3.309 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
3.310 -if (term2str t) = "1 + -2 * x ^^^ 4 + x ^^^ 8" then ()
3.311 -else error "poly.sml: diff.behav. in make_polynomial 9b";
3.312 +if (term2str t) = "1 + -2 * x ^^^ 4 + x ^^^ 8"
3.313 +then () else error "poly.sml: diff.behav. in make_polynomial 9b";
3.314
3.315 "-----SPB Schalk I p.64 No.296a ---";
3.316 val t = str2term "(x - a)^^^3";
3.317 @@ -307,40 +255,37 @@
3.318 "-----SPB Schalk I p.64 No.296c ---";
3.319 val t = str2term "(-3*x - 4*y)^^^3";
3.320 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
3.321 -if (term2str t) =
3.322 -"-27 * x ^^^ 3 + -108 * x ^^^ 2 * y + -144 * x * y ^^^ 2 + -64 * y ^^^ 3"
3.323 +if (term2str t) = "-27 * x ^^^ 3 + -108 * x ^^^ 2 * y + -144 * x * y ^^^ 2 + -64 * y ^^^ 3"
3.324 then () else error "poly.sml: diff.behav. in make_polynomial 11";
3.325
3.326 "-----SPB Schalk I p.62 No.242c ---";
3.327 val t = str2term "x^^^(-4)*(x^^^(-4)*y^^^(-2))^^^(-1)*y^^^(-2)";
3.328 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
3.329 -if (term2str t) = "1" then ()
3.330 -else error "poly.sml: diff.behav. in make_polynomial 12";
3.331 +if (term2str t) = "1"
3.332 +then () else error "poly.sml: diff.behav. in make_polynomial 12";
3.333
3.334 "-----SPB Schalk I p.60 No.209a ---";
3.335 val t = str2term "a^^^(7-x) * a^^^x";
3.336 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
3.337 -if term2str t = "a ^^^ 7" then ()
3.338 -else error "poly.sml: diff.behav. in make_polynomial 13";
3.339 +if term2str t = "a ^^^ 7"
3.340 +then () else error "poly.sml: diff.behav. in make_polynomial 13";
3.341
3.342 "-----SPB Schalk I p.60 No.209d ---";
3.343 val t = str2term "d^^^x * d^^^(x+1) * d^^^(2 - 2*x)";
3.344 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
3.345 -if term2str t = "d ^^^ 3" then ()
3.346 -else error "poly.sml: diff.behav. in make_polynomial 14";
3.347 +if term2str t = "d ^^^ 3"
3.348 +then () else error "poly.sml: diff.behav. in make_polynomial 14";
3.349
3.350 (*---------------------------------------------------------------------*)
3.351 -(*------------------ Bsple bei denen es Probleme gibt------------------*)
3.352 +(*---------------- ?RL?Bsple bei denen es Probleme gibt----------------*)
3.353 (*---------------------------------------------------------------------*)
3.354 -
3.355 "-----Schalk I p.64 No.303 ---";
3.356 val t = str2term "(a + 2*b)*(a^^^2 + 4*b^^^2)*(a - 2*b) - (a - 6*b)*(a^^^2 + 36*b^^^2)*(a + 6*b)";
3.357 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
3.358 -if term2str t = "1280 * b ^^^ 4" then ()
3.359 -else error "poly.sml: diff.behav. in make_polynomial 14b";
3.360 +if term2str t = "1280 * b ^^^ 4"
3.361 +then () else error "poly.sml: diff.behav. in make_polynomial 14b";
3.362 (* Richtig - aber Binomische Formel wurde nicht verwendet! *)
3.363
3.364 -
3.365 (*--------------------------------------------------------------------*)
3.366 (*----------------------- Eigene Beispiele ---------------------------*)
3.367 (*--------------------------------------------------------------------*)
3.368 @@ -405,40 +350,23 @@
3.369 if (term2str t) = "3 * a + 5 * b ^^^ (1 + 2 * n) * c + a * b ^^^ (2 * n) * c"
3.370 then () else error "poly.sml: diff.behav. in make_polynomial 26";
3.371
3.372 -
3.373 -(*MG.27.6.03 -------------vvv-: Verschachtelte Terme -----------*)
3.374 +(*MG030627 -------------vvv-: Verschachtelte Terme -----------*)
3.375 "-----SPO ---";
3.376 val t = str2term "(1 + (x*y*a) + x)^^^(1 + (x*y*a) + x)";
3.377 - val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
3.378 - term2str t;
3.379 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
3.380 if term2str t = "(1 + x + a * x * y) ^^^ (1 + x + a * x * y)"
3.381 - then () else error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*)
3.382 +then () else error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*)
3.383 +
3.384 val t = str2term "(1 + x*(y*z)*zz)^^^(1 + x*(y*z)*zz)";
3.385 - val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
3.386 - term2str t;
3.387 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
3.388 if term2str t = "(1 + x * y * z * zz) ^^^ (1 + x * y * z * zz)"
3.389 - then () else error "poly.sml: diff.behav. in make_polynomial 28";
3.390 -
3.391 -"-------- Script 'simplification for_polynomials' -------";
3.392 -"-------- Script 'simplification for_polynomials' -------";
3.393 -"-------- Script 'simplification for_polynomials' -------";
3.394 -val str =
3.395 -"Script SimplifyScript (t_t::real) = \
3.396 -\ ((Rewrite_Set norm_Poly False) t_t)";
3.397 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
3.398 -atomty sc;
3.399 -
3.400 +then () else error "poly.sml: diff.behav. in make_polynomial 28";
3.401
3.402 "-------- check pbl 'polynomial simplification' --------";
3.403 "-------- check pbl 'polynomial simplification' --------";
3.404 "-------- check pbl 'polynomial simplification' --------";
3.405 -val fmz = ["Term ((5*x^^^2 + 3) * (2*x^^^7 + 3) \
3.406 - \- (3*x^^^5 + 8) * (6*x^^^4 - 1))",
3.407 - "normalform N"];
3.408 +val fmz = ["Term ((5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1))", "normalform N"];
3.409 "-----0 ---";
3.410 -(*===== inhibit exn ============================================================
3.411 -STOPPED.WN10xx
3.412 -
3.413 case refine fmz ["polynomial","simplification"]of
3.414 [Matches (["polynomial", "simplification"], _)] => ()
3.415 | _ => error "poly.sml diff.behav. in check pbl, refine";
3.416 @@ -453,40 +381,34 @@
3.417 ... then trace_rewrite:*)
3.418
3.419 "-----2 ---";
3.420 -trace_rewrite:=true;
3.421 +trace_rewrite := true;
3.422 match_pbl fmz pbt;
3.423 -trace_rewrite:=false;
3.424 +trace_rewrite := false;
3.425 (*... if there is no rewrite, then there is something wrong with prls*)
3.426
3.427 "-----3 ---";
3.428 print_depth 7;
3.429 val prls = (#prls o get_pbt) ["polynomial","simplification"];
3.430 print_depth 3;
3.431 -val t = str2term "((5*x^^^2 + 3) * (2*x^^^7 + 3) \
3.432 - \- (3*x^^^5 + 8) * (6*x^^^4 - 1)) is_polyexp";
3.433 -trace_rewrite:=true;
3.434 +val t = str2term "((5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1)) is_polyexp";
3.435 val SOME (t',_) = rewrite_set_ thy false prls t;
3.436 -trace_rewrite:=false;
3.437 if t' = HOLogic.true_const then ()
3.438 else error "poly.sml: diff.behav. in check pbl 'polynomial..";
3.439 -(*... if this works, but (*1*) does still NOT work, check types:*)
3.440 +(*... if this works, but --1-- does still NOT work, check types:*)
3.441
3.442 "-----4 ---";
3.443 -show_types:=true;
3.444 +(*show_types:=true;*)
3.445 (*
3.446 > val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt;
3.447 val wh = [False "(t_::real => real) (is_polyexp::real)"]
3.448 ......................^^^^^^^^^^^^...............^^^^*)
3.449 val Matches' _ = match_pbl fmz pbt;
3.450 -show_types:=false;
3.451 -
3.452 +(*show_types:=false;*)
3.453
3.454 "-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
3.455 "-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
3.456 "-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
3.457 -val fmz = ["Term ((5*x^^^2 + 3) * (2*x^^^7 + 3) \
3.458 - \- (3*x^^^5 + 8) * (6*x^^^4 - 1))",
3.459 - "normalform N"];
3.460 +val fmz = ["Term ((5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1))", "normalform N"];
3.461 val (dI',pI',mI') =
3.462 ("Poly",["polynomial","simplification"],
3.463 ["simplification","for_polynomials"]);
3.464 @@ -502,17 +424,15 @@
3.465 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.466 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.467 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
3.468 -if f2str f =
3.469 -"17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"
3.470 +if f2str f = "17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"
3.471 then () else error "poly.sml diff.behav. in me Schalk I p.63 No.267b";
3.472
3.473 -
3.474 "-------- interSteps for Schalk 299a --------------------";
3.475 "-------- interSteps for Schalk 299a --------------------";
3.476 "-------- interSteps for Schalk 299a --------------------";
3.477 states:=[];
3.478 CalcTree
3.479 -[(["Term ((x - y)*(x + y))", "normalform N"],
3.480 +[(["Term ((x - y)*(x + (y::real)))", "normalform N"],
3.481 ("Poly",["polynomial","simplification"],
3.482 ["simplification","for_polynomials"]))];
3.483 Iterator 1;
3.484 @@ -527,19 +447,19 @@
3.485
3.486 interSteps 1 ([1,1],Res)(*<ERROR> syserror in detailstep </ERROR>*);
3.487 val ((pt,p),_) = get_calc 1; show_pt pt;
3.488 +(*============ inhibit exn WN120316 ==============================================
3.489 if existpt' ([1,1,1], Frm) pt then ()
3.490 else error "poly.sml: interSteps doesnt work again 2";
3.491 -
3.492 +============ inhibit exn WN120316 ==============================================*)
3.493
3.494 "-------- norm_Poly NOT COMPLETE ------------------------";
3.495 "-------- norm_Poly NOT COMPLETE ------------------------";
3.496 "-------- norm_Poly NOT COMPLETE ------------------------";
3.497 -trace_rewrite:=true;
3.498 val SOME (f',_) = rewrite_set_ thy false norm_Poly
3.499 -(str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben")(*see poly.sml: -- norm_Poly NOT COMPLETE -- TODO MG*);
3.500 -trace_rewrite:=false;
3.501 -term2str f';
3.502 -
3.503 +(str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");
3.504 +if term2str f' = "L = 2 * 2 * k + oben + 2 * -4 * q + senkrecht"
3.505 +then ((*norm_Poly NOT COMPLETE -- TODO MG*))
3.506 +else error "norm_Poly changed behavior";
3.507
3.508 "-------- ord_make_polynomial ---------------------------";
3.509 "-------- ord_make_polynomial ---------------------------";
3.510 @@ -547,7 +467,7 @@
3.511 val t1 = str2term "2 * b + (3 * a + 3 * b)";
3.512 val t2 = str2term "3 * a + 3 * b + 2 * b";
3.513
3.514 -if ord_make_polynomial true Poly.thy [] (t1, t2) then ()
3.515 +if ord_make_polynomial true thy [] (t1, t2) then ()
3.516 else error "poly.sml: diff.behav. in ord_make_polynomial";
3.517
3.518 (*WN071202: ^^^ why then is there no rewriting ...*)
3.519 @@ -558,5 +478,3 @@
3.520 val t1 = str2term "2 * b + (3 * a + 3 * b)";
3.521 val t2 = str2term "3 * a + (2 * b + 3 * b)";
3.522
3.523 -===== inhibit exn ============================================================*)
3.524 -===== inhibit exn ?===========================================================*)
4.1 --- a/test/Tools/isac/Knowledge/rational.sml Sat Mar 17 11:06:46 2012 +0100
4.2 +++ b/test/Tools/isac/Knowledge/rational.sml Sat Mar 17 12:52:30 2012 +0100
4.3 @@ -5,21 +5,15 @@
4.4
4.5 12345678901234567890123456789012345678901234567890123456789012345678901234567890
4.6 10 20 30 40 50 60 70 80
4.7 -
4.8 -LEGEND WN070906
4.9 +LEGEND
4.10 +WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeind
4.11 +WN070906
4.12 nonterm.SK marks non-terminating examples
4.13 ord.SK PARTIALLY marks crucial ordering examples
4.14 *SK* of some (secondary) interest (on 070906)
4.15 -*******************************************************************)
4.16 +WN060104 transfer examples marked with (*SR..*) to the exp-collection
4.17 +*)
4.18
4.19 -(******************************************************************
4.20 -WN060104 transfer marked (*SR..*)examples to the exp-collection
4.21 - # exp_IsacCore_Simp_Rat_Cancel.xml from rational.sml (*SRC*) 10 exp
4.22 - # exp_IsacCore_Simp_Rat_Add.xml from rational.sml (*SRA*) 11 exp
4.23 - # exp_IsacCore_Simp_Rat_Mult.xml from rational.sml (*SRM*) 5 exp
4.24 - # exp_IsacCore_Simp_Rat_AddMult.xml from rational.sml (*SRAM*) 11 exp
4.25 - # exp_IsacCore_Simp_Rat_Double.xml from rational.sml (*SRD*) 12 exp
4.26 -*******************************************************************)
4.27 "--------------------------------------------------------";
4.28 "--------------------------------------------------------";
4.29 "table of contents --------------------------------------";
5.1 --- a/test/Tools/isac/Knowledge/root.sml Sat Mar 17 11:06:46 2012 +0100
5.2 +++ b/test/Tools/isac/Knowledge/root.sml Sat Mar 17 12:52:30 2012 +0100
5.3 @@ -5,22 +5,24 @@
5.4 "--------------------------------------------------------";
5.5 "table of contents --------------------------------------";
5.6 "--------------------------------------------------------";
5.7 -"----------- TODO ---------------------------------------";
5.8 +"----------- rls Root_erls ------------------------------";
5.9 "--------------------------------------------------------";
5.10 "--------------------------------------------------------";
5.11
5.12 -(*=== inhibit exn ?=============================================================
5.13 +val thy = @{theory "Root"};
5.14 +val ctxt = ProofContext.init_global thy;
5.15
5.16 -val thy = Root.thy;
5.17 -
5.18 +"----------- rls Root_erls ------------------------------";
5.19 +"----------- rls Root_erls ------------------------------";
5.20 +"----------- rls Root_erls ------------------------------";
5.21 val t = str2term "sqrt 1";
5.22 val SOME (t',_) = rewrite_set_ thy false Root_erls t;
5.23 if term2str t' = "1" then () else error "root.sml: diff.behav. sqrt 1";
5.24 +
5.25 val t = str2term "sqrt -1";
5.26 val NONE = rewrite_set_ thy false Root_erls t;
5.27
5.28 val t = str2term "sqrt 0";
5.29 val SOME (t',_) = rewrite_set_ thy false Root_erls t;
5.30 -term2str t';
5.31 if term2str t' = "0" then () else error "root.sml: diff.behav. sqrt 1";
5.32 -===== inhibit exn ?===========================================================*)
5.33 +
6.1 --- a/test/Tools/isac/Test_Isac.thy Sat Mar 17 11:06:46 2012 +0100
6.2 +++ b/test/Tools/isac/Test_Isac.thy Sat Mar 17 12:52:30 2012 +0100
6.3 @@ -151,18 +151,18 @@
6.4 use "Knowledge/descript.sml"
6.5 (*use "Knowledge/atools.sml" 2002, added termorder.sml 2011*)
6.6 use "Knowledge/simplify.sml" (*part.*)
6.7 -(*use "Knowledge/poly.sml" 2002*)
6.8 -(*use "Knowledge/rational.sml" part.; diff.emacs--jedit*)
6.9 -(*use "Knowledge/equation.sml" 2002*)
6.10 -(*use "Knowledge/root.sml" 2002*)
6.11 - use "Knowledge/lineq.sml" (*new 2011*) (*part.*)
6.12 -(*use "Knowledge/rooteq.sml" some complicated equations not recovered from 2002*)
6.13 - use "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002*)
6.14 + use "Knowledge/poly.sml"
6.15 +(*use "Knowledge/rational.sml" WN120317.TODO postponed to joint work with dmeind*)
6.16 + use "Knowledge/equation.sml"
6.17 + use "Knowledge/root.sml"
6.18 + use "Knowledge/lineq.sml"
6.19 +(*use "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
6.20 + use "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *)
6.21 use "Knowledge/rootrat.sml"
6.22 - use "Knowledge/rootrateq.sml"(*some complicated equations not recovered from 2002*)
6.23 + use "Knowledge/rootrateq.sml"(*some complicated equations not recovered from 2002 *)
6.24 use "Knowledge/partial_fractions.sml"
6.25 use "Knowledge/polyeq.sml"
6.26 -(*use "Knowledge/rlang.sml" much cleaning required, not urgent due to other tests*)
6.27 +(*use "Knowledge/rlang.sml" much to clean up, not urgent due to other tests *)
6.28 use "Knowledge/calculus.sml"
6.29 use "Knowledge/trig.sml"
6.30 (*use "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
7.1 --- a/test/Tools/isac/Test_Some.thy Sat Mar 17 11:06:46 2012 +0100
7.2 +++ b/test/Tools/isac/Test_Some.thy Sat Mar 17 12:52:30 2012 +0100
7.3 @@ -1,10 +1,10 @@
7.4
7.5 theory Test_Some imports Isac begin
7.6
7.7 -use"../../../test/Tools/isac/Interpret/ctree.sml"
7.8 +use"../../../test/Tools/isac/Knowledge/poly.sml"
7.9
7.10 ML {*
7.11 -val thy = @{theory "RatEq"};
7.12 +val thy = @{theory "Poly"}
7.13 val ctxt = ProofContext.init_global thy;
7.14 print_depth 999;
7.15 *}
7.16 @@ -20,12 +20,6 @@
7.17 *}
7.18 ML {*
7.19 *}
7.20 -ML {*
7.21 -*}
7.22 -ML {*
7.23 -*}
7.24 -ML {*
7.25 -*}
7.26 ML {* (*==================*)
7.27 *}
7.28 ML {*