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