1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Mon Apr 19 11:45:43 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Mon Apr 19 15:02:00 2021 +0200
1.3 @@ -52,54 +52,54 @@
1.4 (* Rewrite.trace_on:=true;
1.5 Rewrite.trace_on:=false;
1.6 *)
1.7 - val t1 = (Thm.term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
1.8 + val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
1.9 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
1.10 if ((UnparseC.term t) = "-8 - 2 * x + x ^^^ 2") then ()
1.11 else error "polyeq.sml: diff.behav. in lhs";
1.12
1.13 - val t2 = (Thm.term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
1.14 + val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
1.15 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
1.16 if (UnparseC.term t) = "True" then ()
1.17 else error "polyeq.sml: diff.behav. 1 in is_expended_in";
1.18
1.19 - val t0 = (Thm.term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x";
1.20 + val t0 = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)) is_poly_in x";
1.21 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
1.22 if (UnparseC.term t) = "False" then ()
1.23 else error "polyeq.sml: diff.behav. 2 in is_poly_in";
1.24
1.25 - val t3 = (Thm.term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x";
1.26 + val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x";
1.27 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
1.28 if (UnparseC.term t) = "True" then ()
1.29 else error "polyeq.sml: diff.behav. 3 in is_poly_in";
1.30
1.31 - val t4 = (Thm.term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x";
1.32 + val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x";
1.33 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
1.34 if (UnparseC.term t) = "True" then ()
1.35 else error "polyeq.sml: diff.behav. 4 in is_expended_in";
1.36
1.37
1.38 - val t6 = (Thm.term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
1.39 + val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
1.40 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
1.41 if (UnparseC.term t) = "True" then ()
1.42 else error "polyeq.sml: diff.behav. 5 in is_expended_in";
1.43
1.44 - val t3 = (Thm.term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
1.45 + val t3 = (Thm.term_of o the o (TermC.parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
1.46 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
1.47 if (UnparseC.term t) = "True" then ()
1.48 else error "polyeq.sml: diff.behav. in has_degree_in_in";
1.49
1.50 - val t3 = (Thm.term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2";
1.51 + val t3 = (Thm.term_of o the o (TermC.parse thy)) "((sqrt(x)) has_degree_in x) = 2";
1.52 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
1.53 if (UnparseC.term t) = "False" then ()
1.54 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
1.55
1.56 - val t4 = (Thm.term_of o the o (parse thy))
1.57 + val t4 = (Thm.term_of o the o (TermC.parse thy))
1.58 "((-8 - 2*x + x^^^2) has_degree_in x) = 1";
1.59 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
1.60 if (UnparseC.term t) = "False" then ()
1.61 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
1.62
1.63 - val t5 = (Thm.term_of o the o (parse thy))
1.64 + val t5 = (Thm.term_of o the o (TermC.parse thy))
1.65 "((-8 - 2*x + x^^^2) has_degree_in x) = 2";
1.66 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
1.67 if (UnparseC.term t) = "True" then ()
1.68 @@ -113,7 +113,7 @@
1.69 M_Match.Matches' {Find = [Correct "solutions L"],
1.70 With = [],
1.71 Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
1.72 - Where = [Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)",
1.73 + Where = [Correct "TermC.matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)",
1.74 Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) is_expanded_in x"],
1.75 Relate = []}
1.76 then () else error "M_Match.match_pbl [expanded,univariate,equation]";
1.77 @@ -134,7 +134,7 @@
1.78 -----------28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
1.79
1.80 (*Aufgabe zum Einstieg in die Arbeit...*)
1.81 - val t = (Thm.term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2 = 0";
1.82 + val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x^^^2 = 0";
1.83 (*ein 'ruleset' aus Poly.ML wird angewandt...*)
1.84 val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
1.85 UnparseC.term t;
1.86 @@ -164,9 +164,9 @@
1.87 *)
1.88
1.89 "------15.11.02 --------------------------";
1.90 - val t = (Thm.term_of o the o (parse thy)) "1 + a * x + b * x";
1.91 - val bdv = (Thm.term_of o the o (parse thy)) "bdv";
1.92 - val a = (Thm.term_of o the o (parse thy)) "a";
1.93 + val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * x + b * x";
1.94 + val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv";
1.95 + val a = (Thm.term_of o the o (TermC.parse thy)) "a";
1.96
1.97 Rewrite.trace_on := false;
1.98 (* Anwenden einer Regelmenge aus Termorder.ML: *)
1.99 @@ -178,7 +178,7 @@
1.100 UnparseC.term t;
1.101 "1 + b * x + x * a";
1.102
1.103 - val t = (Thm.term_of o the o (parse thy)) "1 + a * (x + b * x) + a^^^2";
1.104 + val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * (x + b * x) + a^^^2";
1.105 val SOME (t,_) =
1.106 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
1.107 UnparseC.term t;
1.108 @@ -187,7 +187,7 @@
1.109 UnparseC.term t;
1.110 "1 + (x + b * x) * a + a ^^^ 2";
1.111
1.112 - val t = (Thm.term_of o the o (parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2";
1.113 + val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2";
1.114 val SOME (t,_) =
1.115 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
1.116 UnparseC.term t;
1.117 @@ -207,7 +207,7 @@
1.118 get_thm Termorder.thy "bdv_n_collect";
1.119 get_thm (theory "Isac_Knowledge") "bdv_n_collect";
1.120 *)
1.121 - val t = (Thm.term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2";
1.122 + val t = (Thm.term_of o the o (TermC.parse thy)) "a ^^^2 * x + 7 * a^^^2";
1.123 val SOME (t,_) =
1.124 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
1.125 UnparseC.term t;
1.126 @@ -216,7 +216,7 @@
1.127 UnparseC.term t;
1.128 "(7 + x) * a ^^^ 2";
1.129
1.130 - val t = (Thm.term_of o the o (parse Termorder.thy)) "Pi";
1.131 + val t = (Thm.term_of o the o (TermC.parse Termorder.thy)) "Pi";
1.132
1.133 val t = (Thm.term_of o the o (parseold thy)) "7";
1.134 ##################################################################################*)
1.135 @@ -225,14 +225,14 @@
1.136 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
1.137 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
1.138 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
1.139 - val substa = [(TermC.empty, (Thm.term_of o the o (parse thy)) "a")];
1.140 - val substb = [(TermC.empty, (Thm.term_of o the o (parse thy)) "b")];
1.141 - val substx = [(TermC.empty, (Thm.term_of o the o (parse thy)) "x")];
1.142 + val substa = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "a")];
1.143 + val substb = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "b")];
1.144 + val substx = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "x")];
1.145
1.146 - val x1 = (Thm.term_of o the o (parse thy)) "a + b + x";
1.147 - val x2 = (Thm.term_of o the o (parse thy)) "a + x + b";
1.148 - val x3 = (Thm.term_of o the o (parse thy)) "a + x + b";
1.149 - val x4 = (Thm.term_of o the o (parse thy)) "x + a + b";
1.150 + val x1 = (Thm.term_of o the o (TermC.parse thy)) "a + b + x";
1.151 + val x2 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
1.152 + val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
1.153 + val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b";
1.154
1.155 if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
1.156 else error "termorder.sml diff.behav ord_make_polynomial_in #1";
1.157 @@ -243,22 +243,22 @@
1.158 if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
1.159 else error "termorder.sml diff.behav ord_make_polynomial_in #3";
1.160
1.161 - val aa = (Thm.term_of o the o (parse thy)) "-1 * a * x";
1.162 - val bb = (Thm.term_of o the o (parse thy)) "x^^^3";
1.163 + val aa = (Thm.term_of o the o (TermC.parse thy)) "-1 * a * x";
1.164 + val bb = (Thm.term_of o the o (TermC.parse thy)) "x^^^3";
1.165 ord_make_polynomial_in true thy substx (aa, bb);
1.166 true; (* => LESS *)
1.167
1.168 - val aa = (Thm.term_of o the o (parse thy)) "-1 * a * x";
1.169 - val bb = (Thm.term_of o the o (parse thy)) "x^^^3";
1.170 + val aa = (Thm.term_of o the o (TermC.parse thy)) "-1 * a * x";
1.171 + val bb = (Thm.term_of o the o (TermC.parse thy)) "x^^^3";
1.172 ord_make_polynomial_in true thy substa (aa, bb);
1.173 false; (* => GREATER *)
1.174
1.175 (* und nach dem Re-engineering der Termorders in den 'rulesets'
1.176 kannst Du die 'gr"osste' Variable frei w"ahlen: *)
1.177 - val bdv= (Thm.term_of o the o (parse thy)) "''bdv''";
1.178 - val x = (Thm.term_of o the o (parse thy)) "x";
1.179 - val a = (Thm.term_of o the o (parse thy)) "a";
1.180 - val b = (Thm.term_of o the o (parse thy)) "b";
1.181 + val bdv= (Thm.term_of o the o (TermC.parse thy)) "''bdv''";
1.182 + val x = (Thm.term_of o the o (TermC.parse thy)) "x";
1.183 + val a = (Thm.term_of o the o (TermC.parse thy)) "a";
1.184 + val b = (Thm.term_of o the o (TermC.parse thy)) "b";
1.185 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
1.186 if UnparseC.term t' = "b + x + a" then ()
1.187 else error "termorder.sml diff.behav ord_make_polynomial_in #11";
1.188 @@ -270,7 +270,7 @@
1.189 else error "termorder.sml diff.behav ord_make_polynomial_in #13";
1.190
1.191 val ppp' = "-6 + -5*x + x^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2";
1.192 - val ppp = (Thm.term_of o the o (parse thy)) ppp';
1.193 + val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp';
1.194 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
1.195 if UnparseC.term t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
1.196 else error "termorder.sml diff.behav ord_make_polynomial_in #14";
1.197 @@ -280,7 +280,7 @@
1.198 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
1.199
1.200 val ttt' = "(3*x + 5)/18";
1.201 - val ttt = (Thm.term_of o the o (parse thy)) ttt';
1.202 + val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt';
1.203 val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
1.204 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
1.205 else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
1.206 @@ -941,7 +941,7 @@
1.207 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
1.208 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
1.209 "---- test the erls ----";
1.210 - val t1 = (Thm.term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1";
1.211 + val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2)^^^2 - 1";
1.212 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
1.213 val t' = UnparseC.term t;
1.214 (*if t'= "HOL.True" then ()