wneuper/isa: comparison test/Tools/isac/Knowledge/polyeq-1.sml

equal deleted inserted replaced

-:762098243261
+:0ca0f9363ad3
 "----------- tests on predicates in problems ---------------------";
 "----------- tests on predicates in problems ---------------------";
 (* Rewrite.trace_on:=true;
 Rewrite.trace_on:=false;
 *)
-val t1 = (Thm.term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
+val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
 if ((UnparseC.term t) = "-8 - 2 * x + x ^^^ 2") then ()
 else  error "polyeq.sml: diff.behav. in lhs";
-val t2 = (Thm.term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
+val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
 if (UnparseC.term t) = "True" then ()
 else  error "polyeq.sml: diff.behav. 1 in is_expended_in";
-val t0 = (Thm.term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x";
+val t0 = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)) is_poly_in x";
 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
 if (UnparseC.term t) = "False" then ()
 else  error "polyeq.sml: diff.behav. 2 in is_poly_in";
-val t3 = (Thm.term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x";
+val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x";
 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
 if (UnparseC.term t) = "True" then ()
 else  error "polyeq.sml: diff.behav. 3 in is_poly_in";
-val t4 = (Thm.term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x";
+val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x";
 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
 if (UnparseC.term t) = "True" then ()
 else  error "polyeq.sml: diff.behav. 4 in is_expended_in";
-val t6 = (Thm.term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
+val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
 if (UnparseC.term t) = "True" then ()
 else  error "polyeq.sml: diff.behav. 5 in is_expended_in";
-val t3 = (Thm.term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
+val t3 = (Thm.term_of o the o (TermC.parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
 if (UnparseC.term t) = "True" then ()
 else  error "polyeq.sml: diff.behav. in has_degree_in_in";
-val t3 = (Thm.term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2";
+val t3 = (Thm.term_of o the o (TermC.parse thy)) "((sqrt(x)) has_degree_in x) = 2";
 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
 if (UnparseC.term t) = "False" then ()
 else  error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
-val t4 = (Thm.term_of o the o (parse thy))
+val t4 = (Thm.term_of o the o (TermC.parse thy))
 	      "((-8 - 2*x + x^^^2) has_degree_in x) = 1";
 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
 if (UnparseC.term t) = "False" then ()
 else  error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
-val t5 = (Thm.term_of o the o (parse thy))
+val t5 = (Thm.term_of o the o (TermC.parse thy))
 	      "((-8 - 2*x + x^^^2) has_degree_in x) = 2";
 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
 if (UnparseC.term t) = "True" then ()
 else  error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
 val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", "solveFor x", "solutions L"];
 if M_Match.match_pbl fmz (Problem.from_store ["expanded", "univariate", "equation"]) =
 M_Match.Matches' {Find = [Correct "solutions L"],
 With = [],
 Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
-Where = [Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)",
+Where = [Correct "TermC.matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)",
 Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) is_expanded_in x"],
 Relate = []}
 then () else error "M_Match.match_pbl [expanded,univariate,equation]";
 if M_Match.match_pbl fmz (Problem.from_store ["degree_2", "expanded", "univariate", "equation"]) =
 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
 (*##################################################################################
 -----------28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
 (*Aufgabe zum Einstieg in die Arbeit...*)
-val t = (Thm.term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2 = 0";
+val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x^^^2 = 0";
 (*ein 'ruleset' aus Poly.ML wird angewandt...*)
 val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
 UnparseC.term t;
 "a * b + (-1 * (a * x) + (-1 * (b * x) + x ^^^ 2)) = 0";
 val SOME (t,_) =
 (*das rewriting l"asst sich beobachten mit
 Rewrite.trace_on := false;
 *)
 "------15.11.02 --------------------------";
-val t = (Thm.term_of o the o (parse thy)) "1 + a * x + b * x";
+val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * x + b * x";
-val bdv = (Thm.term_of o the o (parse thy)) "bdv";
+val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv";
-val a = (Thm.term_of o the o (parse thy)) "a";
+val a = (Thm.term_of o the o (TermC.parse thy)) "a";
 Rewrite.trace_on := false;
 (* Anwenden einer Regelmenge aus Termorder.ML: *)
 val SOME (t,_) =
 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
 val SOME (t,_) =
 rewrite_set_ thy false discard_parentheses t;
 UnparseC.term t;
 "1 + b * x + x * a";
-val t = (Thm.term_of o the o (parse thy)) "1 + a * (x + b * x) + a^^^2";
+val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * (x + b * x) + a^^^2";
 val SOME (t,_) =
 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
 UnparseC.term t;
 val SOME (t,_) =
 rewrite_set_ thy false discard_parentheses t;
 UnparseC.term t;
 "1 + (x + b * x) * a + a ^^^ 2";
-val t = (Thm.term_of o the o (parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2";
+val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2";
 val SOME (t,_) =
 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
 UnparseC.term t;
 val SOME (t,_) =
 rewrite_set_ thy false discard_parentheses t;
 Termorder.thy    BITTE NUR HIERHER SCHREIBEN (...WN03)
 get_thm Termorder.thy "bdv_n_collect";
 get_thm (theory "Isac_Knowledge") "bdv_n_collect";
 *)
-val t = (Thm.term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2";
+val t = (Thm.term_of o the o (TermC.parse thy)) "a ^^^2 * x + 7 * a^^^2";
 val SOME (t,_) =
 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
 UnparseC.term t;
 val SOME (t,_) =
 rewrite_set_ thy false discard_parentheses t;
 UnparseC.term t;
 "(7 + x) * a ^^^ 2";
-val t = (Thm.term_of o the o (parse Termorder.thy)) "Pi";
+val t = (Thm.term_of o the o (TermC.parse Termorder.thy)) "Pi";
 val t = (Thm.term_of o the o (parseold thy)) "7";
 ##################################################################################*)
 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
-val substa = [(TermC.empty, (Thm.term_of o the o (parse thy)) "a")];
+val substa = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "a")];
-val substb = [(TermC.empty, (Thm.term_of o the o (parse thy)) "b")];
+val substb = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "b")];
-val substx = [(TermC.empty, (Thm.term_of o the o (parse thy)) "x")];
+val substx = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "x")];
-val x1 = (Thm.term_of o the o (parse thy)) "a + b + x";
+val x1 = (Thm.term_of o the o (TermC.parse thy)) "a + b + x";
-val x2 = (Thm.term_of o the o (parse thy)) "a + x + b";
+val x2 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
-val x3 = (Thm.term_of o the o (parse thy)) "a + x + b";
+val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
-val x4 = (Thm.term_of o the o (parse thy)) "x + a + b";
+val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b";
 if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
 else error "termorder.sml diff.behav ord_make_polynomial_in #1";
 if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then ()
 else error "termorder.sml diff.behav ord_make_polynomial_in #2";
 if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
 else error "termorder.sml diff.behav ord_make_polynomial_in #3";
-val aa = (Thm.term_of o the o (parse thy)) "-1 * a * x";
+val aa = (Thm.term_of o the o (TermC.parse thy)) "-1 * a * x";
-val bb = (Thm.term_of o the o (parse thy)) "x^^^3";
+val bb = (Thm.term_of o the o (TermC.parse thy)) "x^^^3";
 ord_make_polynomial_in true thy substx (aa, bb);
 true; (* => LESS *)
-val aa = (Thm.term_of o the o (parse thy)) "-1 * a * x";
+val aa = (Thm.term_of o the o (TermC.parse thy)) "-1 * a * x";
-val bb = (Thm.term_of o the o (parse thy)) "x^^^3";
+val bb = (Thm.term_of o the o (TermC.parse thy)) "x^^^3";
 ord_make_polynomial_in true thy substa (aa, bb);
 false; (* => GREATER *)
 (* und nach dem Re-engineering der Termorders in den 'rulesets'
 kannst Du die 'gr"osste' Variable frei w"ahlen: *)
-val bdv= (Thm.term_of o the o (parse thy)) "''bdv''";
+val bdv= (Thm.term_of o the o (TermC.parse thy)) "''bdv''";
-val x  = (Thm.term_of o the o (parse thy)) "x";
+val x  = (Thm.term_of o the o (TermC.parse thy)) "x";
-val a  = (Thm.term_of o the o (parse thy)) "a";
+val a  = (Thm.term_of o the o (TermC.parse thy)) "a";
-val b  = (Thm.term_of o the o (parse thy)) "b";
+val b  = (Thm.term_of o the o (TermC.parse thy)) "b";
 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
 if UnparseC.term t' = "b + x + a" then ()
 else error "termorder.sml diff.behav ord_make_polynomial_in #11";
 val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
 if UnparseC.term t' = "a + b + x" then ()
 else error "termorder.sml diff.behav ord_make_polynomial_in #13";
 val ppp' = "-6 + -5*x + x^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2";
-val ppp  = (Thm.term_of o the o (parse thy)) ppp';
+val ppp  = (Thm.term_of o the o (TermC.parse thy)) ppp';
 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
 if UnparseC.term t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
 else error "termorder.sml diff.behav ord_make_polynomial_in #14";
 val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
 if UnparseC.term t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
 val ttt' = "(3*x + 5)/18";
-val ttt = (Thm.term_of o the o (parse thy)) ttt';
+val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt';
 val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
 else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
 (*============ inhibit exn WN120316 ==============================================
 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
 "---- test the erls ----";
-val t1 = (Thm.term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1";
+val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2)^^^2 - 1";
 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
 val t' = UnparseC.term t;
 (*if t'= "HOL.True" then ()
 else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
 (* *)

changeset 60230	0ca0f9363ad3
parent 59997	46fe5a8c3911
child 60237	e534316f9e07