1 (* Title: test/Tools/isac/Knowledge/rational-1.sml
3 Use is subject to license terms.
5 Test of basic functions and application to complex examples.
8 "-----------------------------------------------------------------------------------------------";
9 "-----------------------------------------------------------------------------------------------";
10 "table of contents -----------------------------------------------------------------------------";
11 "-----------------------------------------------------------------------------------------------";
12 "-------- fun poly_of_term ---------------------------------------------------------------------";
13 "-------- fun is_poly --------------------------------------------------------------------------";
14 "-------- fun is_ratpolyexp --------------------------------------------------------------------";
15 "-------- fun term_of_poly ---------------------------------------------------------------------";
16 "-------- fun cancel_p special cases -----------------------------------------------------------";
17 "-------- complex examples: rls norm_Rational --------------------------------------------------";
18 "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";
19 "-----------------------------------------------------------------------------------------------";
20 "-----------------------------------------------------------------------------------------------";
23 "-------- fun poly_of_term ---------------------------------------------------------------------";
24 "-------- fun poly_of_term ---------------------------------------------------------------------";
25 "-------- fun poly_of_term ---------------------------------------------------------------------";
26 val thy = @{theory Isac_Knowledge};
27 val vs = TermC.vars_of (TermC.parse_test @{context} "12 * x \<up> 3 * y \<up> 4 * z \<up> 6");
29 val t = TermC.parse_test @{context} "0 ::real";
30 if poly_of_term vs t = SOME [(0, [0, 0, 0])]
31 then () else error "poly_of_term 0 changed";
33 val t = TermC.parse_test @{context} "-3 + - 2 * x ::real";
34 if poly_of_term vs t = SOME [(~3, [0, 0, 0]), (~2, [1, 0, 0])]
35 then () else error "poly_of_term uminus changed";
37 if poly_of_term vs (TermC.parse_test @{context} "12::real") = SOME [(12, [0, 0, 0])]
38 then () else error "poly_of_term 1 changed";
40 if poly_of_term vs (TermC.parse_test @{context} "x::real") = SOME [(1, [1, 0, 0])]
41 then () else error "poly_of_term 2 changed";
43 if poly_of_term vs (TermC.parse_test @{context} "12 * x \<up> 3") = SOME [(12, [3, 0, 0])]
44 then () else error "poly_of_term 3 changed";
45 "~~~~~ fun poly_of_term , args:"; val (vs, t) =
46 (vs, (TermC.parse_test @{context} "12 * x \<up> 3"));
48 monom_of_term vs (1, replicate (length vs) 0) t;(*poly malformed 1 with x \<up> 3*)
49 "~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const (\<^const_name>\<open>times\<close>, _) $ m1 $ m2)) =
50 (vs, (1, replicate (length vs) 0), t);
53 monom_of_term vs (c, es) m1;
54 "~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const (\<^const_name>\<open>realpow\<close>, _) $ (t as Free _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ num)) ) =
57 (*+*)(num |> HOLogic.dest_numeral |> list_update es (find_index (curry op = t) vs)) = [3, 0, 0];
59 if (c, num |> HOLogic.dest_numeral |> list_update es (find_index (curry op = t) vs)) = (12, [3, 0, 0])
60 then () else error "monom_of_term (realpow): return value CHANGED";
62 if poly_of_term vs (TermC.parse_test @{context} "12 * x \<up> 3 * y \<up> 4 * z \<up> 6") = SOME [(12, [3, 4, 6])]
63 then () else error "poly_of_term 4 changed";
65 if poly_of_term vs (TermC.parse_test @{context} "1 + 2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + y") =
66 SOME [(1, [0, 0, 0]), (1, [0, 1, 0]), (2, [3, 4, 6])]
67 then () else error "poly_of_term 5 changed";
69 (*poly_of_term is quite liberal:*)
70 (*the coefficient may be somewhere, the order of variables and the parentheses
71 within a monomial are arbitrary*)
72 if poly_of_term vs (TermC.parse_test @{context} "y \<up> 4 * (x \<up> 3 * 12 * z \<up> 6)") = SOME [(12, [3, 4, 6])]
73 then () else error "poly_of_term 6 changed";
75 (*there may even be more than 1 coefficient:*)
76 if poly_of_term vs (TermC.parse_test @{context} "2 * y \<up> 4 * (x \<up> 3 * 6 * z \<up> 6)") = SOME [(12, [3, 4, 6])]
77 then () else error "poly_of_term 7 changed";
79 (*the order and the parentheses within monomials are arbitrary:*)
80 if poly_of_term vs (TermC.parse_test @{context} "2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + (7 * y \<up> 8 + 1)")
81 = SOME [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 6])]
82 then () else error "poly_of_term 8 changed";
84 (*from --- rls norm_Rational downto fun gcd_poly ---*)
85 val t = TermC.parse_test @{context} (*copy from above: "::real" is not required due to " \<up> "*)
86 ("(- 12 + 4 * y + 3 * x \<up> 2 + - 1 * (x \<up> 2 * y)) /" ^
87 "(- 18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)");
88 "~~~~~ fun cancel_p_, args:"; val (t) = (t);
89 val opt = check_fraction t;
90 val SOME (numerator, denominator) = opt;
91 (*+*)UnparseC.term numerator = "- 12 + 4 * y + 3 * x \<up> 2 + - 1 * (x \<up> 2 * y)"; (*isa -- isa2*);
92 (*+*)UnparseC.term denominator = "- 18 + - 9 * x + 2 * y \<up> 2 + x * y \<up> 2"; (*isa -- isa2*);
93 val vs = TermC.vars_of t;
94 (*+*)UnparseC.terms vs = "[\"x\", \"y\"]";
95 val baseT = type_of numerator
96 val expT = HOLogic.realT;
97 val (SOME _, SOME _) = (poly_of_term vs numerator, poly_of_term vs denominator); (*isa <> isa2*)
99 "-------- fun is_poly --------------------------------------------------------------------------";
100 "-------- fun is_poly --------------------------------------------------------------------------";
101 "-------- fun is_poly --------------------------------------------------------------------------";
102 if is_poly (TermC.parse_test @{context} "2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + 7 * y \<up> 8 + 1")
103 then () else error "is_poly 1 changed";
104 if not (is_poly (TermC.parse_test @{context} "2 * (x \<up> 3 * y \<up> 4 * z \<up> 6 + 7) * y \<up> 8 + 1"))
105 then () else error "is_poly 2 changed";
107 "-------- fun is_ratpolyexp --------------------------------------------------------------------";
108 "-------- fun is_ratpolyexp --------------------------------------------------------------------";
109 "-------- fun is_ratpolyexp --------------------------------------------------------------------";
110 if is_ratpolyexp @{term "14 * x * y / (x * y)"}
111 then () else error "is_ratpolyexp (14 * x * y / (x * y)) CHANGED";
112 if is_ratpolyexp @{term "2 * (x \<up> 3 * y \<up> 4 * z \<up> 6 + 7) * y \<up> 8 + 1"}
113 then () else error "is_ratpolyexp (2 * (x \<up> 3 * y \<up> 4 * z \<up> 6 + 7) * y \<up> 8 + 1) CHANGED";
115 if is_ratpolyexp @{term "((sin x) \<up> 2 - (cos x) \<up> 2)/ ((sin x)+ (cos x))"}
116 then error "is_ratpolyexp (((sin x) \<up> 2 - (cos x) \<up> 2)/ ((sin x)+ (cos x)) CHANGED" else ();
117 if is_ratpolyexp @{term "1 + sqrt x + sqrt y"}
118 then error "is_ratpolyexp (1 + sqrt x + sqrt y) CHANGED" else ();
121 "-------- fun term_of_poly ---------------------------------------------------------------------";
122 "-------- fun term_of_poly ---------------------------------------------------------------------";
123 "-------- fun term_of_poly ---------------------------------------------------------------------";
124 val expT = HOLogic.realT
125 val Free (_, baseT) = (hd o vars o TermC.parse_test @{context}) "12 * x \<up> 3 * y \<up> 4 * z \<up> 6";
126 val p = [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 5])]
127 val vs = TermC.vars_of (the (parseNEW ctxt "12 * x \<up> 3 * y \<up> 4 * z \<up> 6"))
128 (*precondition for [(c, es),...]: legth es = length vs*)
130 if UnparseC.term (term_of_poly baseT expT vs p) = "1 + 7 * y \<up> 8 + 2 * x \<up> 3 * y \<up> 4 * z \<up> 5"
131 then () else error "term_of_poly 1 changed";
133 "-------- fun cancel_p special cases -----------------------------------------------------------";
134 "-------- fun cancel_p special cases -----------------------------------------------------------";
135 "-------- fun cancel_p special cases -----------------------------------------------------------";
136 val thy = @{theory Isac_Knowledge};
137 val ctxt = Proof_Context.init_global thy
139 (*------- standard case: *)
140 val t = TermC.parse_test @{context} "2 / 3 + 1 / 6 ::real";
141 "~~~~~ fun add_fraction_p_ , args:"; val ((_: theory), t) = (thy, t);
142 val SOME ((n1, d1), (n2, d2)) =
143 (*case*) check_frac_sum t (*of*);
144 val vs = TermC.vars_of t;
146 val (SOME n1', SOME a, SOME n2', SOME b) =
147 (*case*) (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) (*of*);
148 val ((a', b'), c) = gcd_poly a b
149 val (baseT, expT) = (type_of n1, HOLogic.realT);
150 (*+*)val [(1, [])] = a'; (* 6 * _1_ = 6 *)
151 (*+*)val [(2, [])] = b'; (* 3 * _2_ = 6 *)
152 (*+*)val [(3, [])] = c; (* 3 / 6 \<and> 3 / 3 ..gcd *)
154 val nomin = term_of_poly baseT expT vs
155 (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'));
157 (*+*)val "5" = UnparseC.term nomin; (* = "3" ERROR*)
159 (*+*)val [(2, [])] = the (poly_of_term vs n1); (*---v----------------------v----*)
160 (*+*)val [(4, [])] = ((the (poly_of_term vs n1)) %%*%% b'); (* = 2 * _2_ new nomin for 2 / 3*)
162 (*+*)val [(1, [])] = the (poly_of_term vs n2); (*---v----------------------v----*)
163 (*+*)val [(1, [])] = ((the (poly_of_term vs n2)) %%*%% a'); (* = 1 * _1_ new nomin for 1 / 6*)
165 (*+*)val [(5, [])] = (* = 4 + 1 new nomin for sum *)
166 (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'));
168 val denom = (* = 3 * 1 * 2 new denom for sum *)
169 term_of_poly baseT expT vs ((c %%*%% a') %%*%% b');
170 (*+*)val "6" = UnparseC.term denom;
172 val t' = HOLogic.mk_binop \<^const_name>\<open>divide\<close> (nomin, denom);
173 (*+*)val "5 / 6" = UnparseC.term t'
176 (*------- 0 / m + 0 / n
177 20 years old bug found here: *)
178 val t = TermC.parse_test @{context} "0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + - 1 * q_0 / 24 * 0 \<up> 4)";
179 val SOME (t', _) = rewrite_set_ ctxt true norm_Rational t;
182 ## rls: cancel_p_rls on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24)
183 ### rls: cancel_p on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24)
184 ------------------------------------------------------------these are missing now -----\
185 /## rls: cancel_p on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 1) from isa2: strange behaviour
186 /## rls: cancel_p on: 0 = c_2 + 1 / EI * (0 / 1 + 0 / 1) from isa2: strange behaviour
187 ------------------------------------------------------------these are missing now -----/
188 ## rls: norm_Rational_rls on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24)
189 ### rls: add_fractions_p_rls on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24)
190 #### rls: add_fractions_p on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24)
191 --------------------------------------------------^v^v^v^v^v^v^v^v^--undetected bug
192 #### rls: add_fractions_p on: 0 = c_2 + 1 / EI * (3 / 24) =3: ERROR
193 ### rls: rat_mult_div_pow on: 0 = c_2 + 1 / EI * (3 / 24)
196 if UnparseC.term t' = "0 = c_2" then () else error "norm_Rational CHANGED"; (*isa2*)
198 val t = TermC.parse_test @{context} "0 / 12 + 0 / 24 ::real";
199 add_fraction_p_ @{theory} t;
200 "~~~~~ fun add_fraction_p_ , args:"; val ((_: theory), t) = (thy, t);
201 val SOME ((n1, d1), (n2, d2)) =
202 (*case*) check_frac_sum t (*of*);
204 (*+*)val Const ("Groups.zero_class.zero", _) = n1;
205 (*+*)val Const ("Groups.zero_class.zero", _) = n2;
207 val vs = TermC.vars_of t;
210 val (SOME n1', SOME a, SOME n2', SOME b) =
211 (*case*) (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) (*of*);
213 (*+*)if n1' = [(0, [])] then () else error "correction w.r.t zero polynomial CHANGED";
215 val ((a', b'), c) = gcd_poly a b
216 val (baseT, expT) = (type_of n1, HOLogic.realT);
217 (*+*)val [(1, [])] = a'; (* 1 * _1_ = 24 *)
218 (*+*)val [(2, [])] = b'; (* 2 * _2_ = 12 *)
219 (*+*)val [(12, [])] = c; (* 12 / 24 \<and> 12 / 12 ..gcd *)
221 val nomin = term_of_poly baseT expT vs
222 (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'));
224 (*+*)UnparseC.term nomin; (* = "3" ERROR*)
225 (* correct ERROR ------------------------------------------------------------------\\*)
226 (*+*)val SOME [(0, [])] = poly_of_term vs n1 (* ERROR WAS [(1, [])] *)
227 (* correct ERROR ------------------------------------------------------------------//*)
229 (*+*)val [(0, [])] = the (poly_of_term vs n1); (*---v----------------------v-----*)
230 (*+*)val [(0, [])] = ((the (poly_of_term vs n1)) %%*%% b'); (* = 0 * _0_ new nomin for 0 / 12*)
232 (*+*)val [(0, [])] = the (poly_of_term vs n2); (*---v----------------------v-----*)
233 (*+*)val [(0, [])] = ((the (poly_of_term vs n2)) %%*%% a'); (* = 0 * _0_ new nomin for 0 / 24*)
235 (*+*)val [(0, [])] = (* = 0 + 0 new nomin for sum *)
236 (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'));
238 val denom = (* = 12 * 1 * 2 new denom for sum *)
239 term_of_poly baseT expT vs ((c %%*%% a') %%*%% b');
240 (*+*)val "24" = UnparseC.term denom;
242 val t' = HOLogic.mk_binop \<^const_name>\<open>divide\<close> (nomin, denom);
243 (*+*)val "0 / 24" = UnparseC.term t'
245 (*---------- fun cancel_p with Const AA *)
246 val thy = @{theory Partial_Fractions};
247 val ctxt = Proof_Context.init_global @{theory}
248 val SOME t = TermC.parseNEW ctxt "2 * AA / 2"; (* Const (\<^const_name>\<open>AA\<close>, "real") *)
250 val SOME (t', _) = rewrite_set_ ctxt true cancel_p t;
252 Const (\<^const_name>\<open>divide\<close>, _) $ Const (\<^const_name>\<open>AA\<close>, _) $
253 Const (\<^const_name>\<open>one_class.one\<close>, _) => ()
254 | _ => error "WRONG rewrite_set_ cancel_p (2 * AA / 2) \<longrightarrow> AA changed";
256 "~~~~~ fun cancel_p , args:"; val (t) = (t);
257 val opt = check_fraction t
258 val SOME (numerator, denominator) = (*case*) opt (*of*);
260 if UnparseC.term numerator = "2 * AA" andalso UnparseC.term denominator = "2"
261 then () else error "check_fraction (2 * AA / 2) changed";
262 val vs = TermC.vars_of t;
264 [Const (\<^const_name>\<open>AA\<close>, _)] => ()
265 | _ => error "rewrite_set_ cancel_p (2 * AA / 2) \<longrightarrow> AA/1 changed";
268 "-------- complex examples: rls norm_Rational --------------------------------------------------";
269 "-------- complex examples: rls norm_Rational --------------------------------------------------";
270 "-------- complex examples: rls norm_Rational --------------------------------------------------";
271 val t = TermC.parse_test @{context} "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0";
272 val SOME (t', _) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t';
273 if UnparseC.term t' = "1 / 18 = 0" then () else error "rational.sml 1";
275 val t = TermC.parse_test @{context} "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";
276 val SOME (t',_) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t';
277 if UnparseC.term t' = "(237 + 65 * x) / 36 = 0" then ()
278 else error "rational.sml 2";
280 val t = TermC.parse_test @{context} "(1/2 + (5*x)/2) \<up> 2 - ((13*x)/2 - 5/2) \<up> 2 - (6*x) \<up> 2 + 29";
281 val SOME (t',_) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t';
282 if UnparseC.term t' = "23 + 35 * x + - 72 * x \<up> 2" then ()
283 else error "rational.sml 3";
285 "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";
286 "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";
287 "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";
288 (*Schalk I, p.60 Nr. 215c *)
289 val t = TermC.parse_test @{context} "(a + b) \<up> 4 * (x - y) / ((x - y) \<up> 3 * (a + b) \<up> 2)";
290 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t;
291 if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + - 2 * x * y + y \<up> 2)"
292 then () else error "rational.sml: diff.behav. in norm_Rational_mg 7";
294 (*SRC Schalk I, p.66 Nr. 381b *)
295 val t = TermC.parse_test @{context}
296 "(4*x \<up> 2 - 20*x + 25)/(2*x - 5) \<up> 3";
297 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t;
298 if UnparseC.term t = "1 / (- 5 + 2 * x)"
299 then () else error "rational.sml: diff.behav. in norm_Rational_mg 9";
301 (*Schalk I, p.60 Nr. 215c *)
302 val t = TermC.parse_test @{context} "(a + b) \<up> 4 * (x - y) / ((x - y) \<up> 3 * (a + b) \<up> 2)";
303 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t;
304 if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + - 2 * x * y + y \<up> 2)"
305 then () else error "Schalk I, p.60 Nr. 215c: with Isabelle2002 cancellation incomplete, changed";