1.1 --- a/test/Tools/isac/Knowledge/poly-1.sml Tue May 24 16:47:31 2022 +0200
1.2 +++ b/test/Tools/isac/Knowledge/poly-1.sml Thu May 26 12:44:51 2022 +0200
1.3 @@ -45,135 +45,138 @@
1.4 "-------- fun has_degree_in --------------------------------------------------------------------";
1.5 "-------- fun has_degree_in --------------------------------------------------------------------";
1.6 "-------- fun has_degree_in --------------------------------------------------------------------";
1.7 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
1.8 -val t = (Thm.term_of o the o (TermC.parse thy)) "1";
1.9 +val thy = @{theory}
1.10 +val ctxt = Proof_Context.init_global thy
1.11 +val v = TermC.parseNEW' ctxt "x";
1.12 +val t = TermC.parseNEW' ctxt "1";
1.13 if has_degree_in t v = 0 then () else error "has_degree_in (1) x";
1.14
1.15 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.16 -val t = (Thm.term_of o the o (TermC.parse thy)) "1";
1.17 +val v = TermC.parseNEW' ctxt "AA";
1.18 +val t = TermC.parseNEW' ctxt "1";
1.19 if has_degree_in t v = 0 then () else error "has_degree_in (1) AA";
1.20
1.21 (*----------*)
1.22 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
1.23 -val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";
1.24 +val v = TermC.parseNEW' ctxt "x";
1.25 +val t = TermC.parseNEW' ctxt "a*b+c";
1.26 if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) x";
1.27
1.28 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.29 -val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";
1.30 +val v = TermC.parseNEW' ctxt "AA";
1.31 +val t = TermC.parseNEW' ctxt "a*b+c";
1.32 if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) AA";
1.33
1.34 (*----------*)
1.35 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
1.36 -val t = (Thm.term_of o the o (TermC.parse thy)) "a*x+c";
1.37 +val v = TermC.parseNEW' ctxt "x";
1.38 +val t = TermC.parseNEW' ctxt "a*x+c";
1.39 if has_degree_in t v = ~1 then () else error "has_degree_in (a*x+c) x";
1.40
1.41 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.42 -val t = (Thm.term_of o the o (TermC.parse thy)) "a*AA+c";
1.43 +val v = TermC.parseNEW' ctxt "AA";
1.44 +val t = TermC.parseNEW' ctxt "a*AA+c";
1.45 if has_degree_in t v = ~1 then () else error "has_degree_in (a*AA+c) AA";
1.46
1.47 (*----------*)
1.48 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
1.49 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";
1.50 +val v = TermC.parseNEW' ctxt "x::real";
1.51 +val t = TermC.parseNEW' ctxt "((a::real)*b+c)*x \<up> 7";
1.52 if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*x \<up> 7) x";
1.53
1.54 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.55 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";
1.56 +val v = TermC.parseNEW' ctxt "AA";
1.57 +val t = TermC.parseNEW' ctxt "(a*b+c)*AA \<up> 7";
1.58 if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*AA \<up> 7) AA";
1.59
1.60 (*----------*)
1.61 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
1.62 -val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";
1.63 +val v = TermC.parseNEW' ctxt "x::real";
1.64 +val t = TermC.parseNEW' ctxt "x \<up> 7";
1.65 if has_degree_in t v = 7 then () else error "has_degree_in (x \<up> 7) x";
1.66
1.67 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.68 -val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";
1.69 +val v = TermC.parseNEW' ctxt "AA";
1.70 +val t = TermC.parseNEW' ctxt "AA \<up> 7";
1.71 if has_degree_in t v = 7 then () else error "has_degree_in (AA \<up> 7) AA";
1.72
1.73 (*----------*)
1.74 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
1.75 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";
1.76 +val v = TermC.parseNEW' ctxt "x::real";
1.77 +val t = TermC.parseNEW' ctxt "(a*b+c)*x::real";
1.78 if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*x) x";
1.79
1.80 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.81 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";
1.82 +val v = TermC.parseNEW' ctxt "AA";
1.83 +val t = TermC.parseNEW' ctxt "(a*b+c)*AA";
1.84 if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*AA) AA";
1.85
1.86 (*----------*)
1.87 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
1.88 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";
1.89 +val v = TermC.parseNEW' ctxt "x::real";
1.90 +val t = TermC.parseNEW' ctxt "(a*b+x)*x";
1.91 if has_degree_in t v = ~1 then () else error "has_degree_in (a*b+x)*x() x";
1.92
1.93 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.94 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";
1.95 +val v = TermC.parseNEW' ctxt "AA";
1.96 +val t = TermC.parseNEW' ctxt "(a*b+AA)*AA";
1.97 if has_degree_in t v = ~1 then () else error "has_degree_in ((a*b+AA)*AA) AA";
1.98
1.99 (*----------*)
1.100 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
1.101 -val t = (Thm.term_of o the o (TermC.parse thy)) "x";
1.102 +val v = TermC.parseNEW' ctxt "x";
1.103 +val t = TermC.parseNEW' ctxt "x";
1.104 if has_degree_in t v = 1 then () else error "has_degree_in (x) x";
1.105
1.106 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.107 -val t = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.108 +val v = TermC.parseNEW' ctxt "AA";
1.109 +val t = TermC.parseNEW' ctxt "AA";
1.110 if has_degree_in t v = 1 then () else error "has_degree_in (AA) AA";
1.111
1.112 (*----------*)
1.113 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
1.114 -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";
1.115 +val v = TermC.parseNEW' ctxt "x::real";
1.116 +val t = TermC.parseNEW' ctxt "ab - (a*b)*(x::real)";
1.117 if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*x) x";
1.118
1.119 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.120 -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";
1.121 +val v = TermC.parseNEW' ctxt "AA";
1.122 +val t = TermC.parseNEW' ctxt "ab - (a*b)*AA";
1.123 if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*AA) AA";
1.124
1.125 "-------- fun mono_deg_in ----------------------------------------------------------------------";
1.126 "-------- fun mono_deg_in ----------------------------------------------------------------------";
1.127 "-------- fun mono_deg_in ----------------------------------------------------------------------";
1.128 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
1.129 +val v = TermC.parseNEW' ctxt "x::real";
1.130
1.131 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";
1.132 +val t = TermC.parseNEW' ctxt "(a*b+c)*x \<up> 7";
1.133 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*x \<up> 7) x changed";
1.134
1.135 -val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";
1.136 +val t = TermC.parseNEW' ctxt "(x::real) \<up> 7";
1.137 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (x \<up> 7) x changed";
1.138
1.139 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";
1.140 +val t = TermC.parseNEW' ctxt "(a*b+c)*x::real";
1.141 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*x) x changed";
1.142
1.143 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";
1.144 +val t = TermC.parseNEW' ctxt "(a*b+x)*x";
1.145 if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+x)*x) x changed";
1.146
1.147 -val t = (Thm.term_of o the o (TermC.parse thy)) "x";
1.148 +val t = TermC.parseNEW' ctxt "x::real";
1.149 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (x) x changed";
1.150
1.151 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)";
1.152 +val t = TermC.parseNEW' ctxt "(a*b+c)";
1.153 if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) x changed";
1.154
1.155 -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";
1.156 +val t = TermC.parseNEW' ctxt "ab - (a*b)*x";
1.157 if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*x) x changed";
1.158
1.159 (*. . . . . . . . . . . . the same with Const (\<^const_name>\<open>AA\<close>, _) . . . . . . . . . . . *)
1.160 val thy = @{theory Partial_Fractions}
1.161 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.162 +val ctxt = Proof_Context.init_global thy
1.163 +val v = TermC.parseNEW' ctxt "AA";
1.164
1.165 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";
1.166 +val t = TermC.parseNEW' ctxt "(a*b+c)*AA \<up> 7";
1.167 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*AA \<up> 7) AA changed";
1.168
1.169 -val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";
1.170 +val t = TermC.parseNEW' ctxt "AA \<up> 7";
1.171 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (AA \<up> 7) AA changed";
1.172
1.173 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";
1.174 +val t = TermC.parseNEW' ctxt "(a*b+c)*AA";
1.175 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*AA) AA changed";
1.176
1.177 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";
1.178 +val t = TermC.parseNEW' ctxt "(a*b+AA)*AA";
1.179 if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+AA)*AA) AA changed";
1.180
1.181 -val t = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.182 +val t = TermC.parseNEW' ctxt "AA";
1.183 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (AA) AA changed";
1.184
1.185 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)";
1.186 +val t = TermC.parseNEW' ctxt "(a*b+c)";
1.187 if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) AA changed";
1.188
1.189 -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";
1.190 +val t = TermC.parseNEW' ctxt "ab - (a*b)*AA";
1.191 if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*AA) AA changed";
1.192
1.193
1.194 @@ -696,6 +699,7 @@
1.195 "-------- norm_Poly with AlgEin ----------------------------------------------------------------";
1.196 "-------- norm_Poly with AlgEin ----------------------------------------------------------------";
1.197 val thy = @{theory AlgEin};
1.198 +val ctxt = Proof_Context.init_global thy;
1.199
1.200 val SOME (f',_) = rewrite_set_ thy false norm_Poly
1.201 (TermC.str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");
1.202 @@ -787,7 +791,7 @@
1.203 else error "poly.sml: diff.behav. in make_polynomial 20";
1.204
1.205 "-----SPO ---";
1.206 -val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * (-a) \<up> 2";
1.207 +val t = TermC.parseNEW' ctxt "a \<up> 2 * (-a) \<up> 2";
1.208 val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t;
1.209 if (UnparseC.term t) = "a \<up> 4" then ()
1.210 else error "poly.sml: diff.behav. in make_polynomial 24";