1.1 --- a/test/Tools/isac/IsacKnowledge/polyeq.sml Wed Aug 18 13:53:15 2010 +0200
1.2 +++ b/test/Tools/isac/IsacKnowledge/polyeq.sml Wed Aug 18 13:55:23 2010 +0200
1.3 @@ -39,60 +39,60 @@
1.4 trace_rewrite:=false;
1.5 *)
1.6 val t1 = (term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
1.7 - val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t1;
1.8 + val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t1;
1.9 if ((term2str t) = "-8 - 2 * x + x ^^^ 2") then ()
1.10 else raise error "polyeq.sml: diff.behav. in lhs";
1.11
1.12
1.13 val t2 = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
1.14 - val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t2;
1.15 + val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t2;
1.16 if (term2str t) = "True" then ()
1.17 else raise error "polyeq.sml: diff.behav. 1 in is_expended_in";
1.18
1.19 val t0 = (term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x";
1.20 - val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t0;
1.21 + val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t0;
1.22 if (term2str t) = "False" then ()
1.23 else raise error "polyeq.sml: diff.behav. 2 in is_poly_in";
1.24
1.25
1.26 val t3 = (term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x";
1.27 - val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
1.28 + val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
1.29 if (term2str t) = "True" then ()
1.30 else raise error "polyeq.sml: diff.behav. 3 in is_poly_in";
1.31
1.32
1.33 val t4 = (term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x";
1.34 - val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t4;
1.35 + val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t4;
1.36 if (term2str t) = "True" then ()
1.37 else raise error "polyeq.sml: diff.behav. 4 in is_expended_in";
1.38
1.39
1.40 val t6 = (term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
1.41 - val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t6;
1.42 + val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t6;
1.43 if (term2str t) = "True" then ()
1.44 else raise error "polyeq.sml: diff.behav. 5 in is_expended_in";
1.45
1.46 val t3 = (term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
1.47 - val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
1.48 + val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
1.49 if (term2str t) = "True" then ()
1.50 else raise error "polyeq.sml: diff.behav. in has_degree_in_in";
1.51
1.52
1.53 val t3 = (term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2";
1.54 - val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
1.55 + val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
1.56 if (term2str t) = "False" then ()
1.57 else raise error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
1.58
1.59 val t4 = (term_of o the o (parse thy))
1.60 "((-8 - 2*x + x^^^2) has_degree_in x) = 1";
1.61 - val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t4;
1.62 + val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t4;
1.63 if (term2str t) = "False" then ()
1.64 else raise error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
1.65
1.66
1.67 val t5 = (term_of o the o (parse thy))
1.68 "((-8 - 2*x + x^^^2) has_degree_in x) = 2";
1.69 - val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t5;
1.70 + val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t5;
1.71 if (term2str t) = "True" then ()
1.72 else raise error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
1.73
1.74 @@ -846,7 +846,7 @@
1.75 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
1.76 "---- test the erls ----";
1.77 val t1 = (term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1";
1.78 - val Some (t,_) = rewrite_set_ PolyEq.thy false PolyEq_erls t1;
1.79 + val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_erls t1;
1.80 val t' = term2str t;
1.81 (*if t'= "True" then ()
1.82 else raise error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
1.83 @@ -1129,31 +1129,31 @@
1.84 (*WN.19.3.03 ---v-*)
1.85 (*3(b)*)val (bdv,v) = (str2term "bdv", str2term "R1");
1.86 val t = str2term "-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0";
1.87 -val Some (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.88 +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.89 term2str t';
1.90 "-1 * R * R2 + (R2 + -1 * R) * R1 = 0";
1.91 (*WN.19.3.03 ---^-*)
1.92
1.93 (*3(c)*)val (bdv,v) = (str2term "bdv", str2term "p");
1.94 val t = str2term "y ^^^ 2 + -2 * (x * p) = 0";
1.95 -val Some (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.96 +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.97 term2str t';
1.98 "y ^^^ 2 + -2 * x * p = 0";
1.99
1.100 (*3(d)*)val (bdv,v) = (str2term "bdv", str2term "x2");
1.101 val t = str2term
1.102 "A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1 * (x1 * (y2 * (1 / 2))) + -1 * (x3 * (y1 * (1 / 2 ))) + y1 * (1 / 2 * x2) + -1 * (y3 * (1 / 2 * x2)) = 0";
1.103 -val Some (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.104 +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.105 term2str t';
1.106 "A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + - x1 * y2 * (1 / 2) + - x3 * y1 * (1 / 2) + (y1 * (1 / 2) + - y3 * (1 / 2)) * x2 = 0";
1.107 -val Some (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t;
1.108 +val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t;
1.109 term2str t';
1.110 "A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + -1 * x1 * y2 * (1 / 2) + -1 * x3 * y1 * (1 / 2) + (y1 * (1 / 2) + -1 * y3 * (1 / 2)) * x2 = 0";
1.111
1.112 (*3(e)*)val (bdv,v) = (str2term "bdv", str2term "a");
1.113 val t = str2term
1.114 "A ^^^ 2 + c ^^^ 2 * (c / d) ^^^ 2 + (-4 * (c / d) ^^^ 2) * a ^^^ 2 = 0";
1.115 -val None = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.116 +val NONE = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.117 (*die _unsichtbare_ Klammern sind genau wie gew"unscht*)
1.118
1.119