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 term_of_poly ---------------------------------------------------------------------";
15 "-------- fun cancel_p special cases -----------------------------------------------------------";
16 "-------- complex examples: rls norm_Rational --------------------------------------------------";
17 "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";
18 "-----------------------------------------------------------------------------------------------";
19 "-----------------------------------------------------------------------------------------------";
22 "-------- fun poly_of_term ---------------------------------------------------------------------";
23 "-------- fun poly_of_term ---------------------------------------------------------------------";
24 "-------- fun poly_of_term ---------------------------------------------------------------------";
25 val thy = @{theory Isac_Knowledge};
26 val vs = TermC.vars_of (TermC.str2term "12 * x \<up> 3 * y \<up> 4 * z \<up> 6");
28 val t = TermC.str2term "0 ::real";
29 if poly_of_term vs t = SOME [(0, [0, 0, 0])]
30 then () else error "poly_of_term 0 changed";
32 val t = TermC.str2term "-3 + - 2 * x ::real";
33 if poly_of_term vs t = SOME [(~3, [0, 0, 0]), (~2, [1, 0, 0])]
34 then () else error "poly_of_term uminus changed";
36 if poly_of_term vs (TermC.str2term "12::real") = SOME [(12, [0, 0, 0])]
37 then () else error "poly_of_term 1 changed";
39 if poly_of_term vs (TermC.str2term "x::real") = SOME [(1, [1, 0, 0])]
40 then () else error "poly_of_term 2 changed";
42 if poly_of_term vs (TermC.str2term "12 * x \<up> 3") = SOME [(12, [3, 0, 0])]
43 then () else error "poly_of_term 3 changed";
44 "~~~~~ fun poly_of_term , args:"; val (vs, t) =
45 (vs, (TermC.str2term "12 * x \<up> 3"));
47 monom_of_term vs (1, replicate (length vs) 0) t;(*poly malformed 1 with x \<up> 3*)
48 "~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const (\<^const_name>\<open>times\<close>, _) $ m1 $ m2)) =
49 (vs, (1, replicate (length vs) 0), t);
52 monom_of_term vs (c, es) m1;
53 "~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const (\<^const_name>\<open>powr\<close>, _) $ (t as Free _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ num)) ) =
56 (*+*)(num |> HOLogic.dest_numeral |> list_update es (find_index (curry op = t) vs)) = [3, 0, 0];
58 if (c, num |> HOLogic.dest_numeral |> list_update es (find_index (curry op = t) vs)) = (12, [3, 0, 0])
59 then () else error "monom_of_term (powr): return value CHANGED";
61 if poly_of_term vs (TermC.str2term "12 * x \<up> 3 * y \<up> 4 * z \<up> 6") = SOME [(12, [3, 4, 6])]
62 then () else error "poly_of_term 4 changed";
64 if poly_of_term vs (TermC.str2term "1 + 2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + y") =
65 SOME [(1, [0, 0, 0]), (1, [0, 1, 0]), (2, [3, 4, 6])]
66 then () else error "poly_of_term 5 changed";
68 (*poly_of_term is quite liberal:*)
69 (*the coefficient may be somewhere, the order of variables and the parentheses
70 within a monomial are arbitrary*)
71 if poly_of_term vs (TermC.str2term "y \<up> 4 * (x \<up> 3 * 12 * z \<up> 6)") = SOME [(12, [3, 4, 6])]
72 then () else error "poly_of_term 6 changed";
74 (*there may even be more than 1 coefficient:*)
75 if poly_of_term vs (TermC.str2term "2 * y \<up> 4 * (x \<up> 3 * 6 * z \<up> 6)") = SOME [(12, [3, 4, 6])]
76 then () else error "poly_of_term 7 changed";
78 (*the order and the parentheses within monomials are arbitrary:*)
79 if poly_of_term vs (TermC.str2term "2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + (7 * y \<up> 8 + 1)")
80 = SOME [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 6])]
81 then () else error "poly_of_term 8 changed";
83 (*from --- rls norm_Rational downto fun gcd_poly ---*)
84 val t = TermC.str2term (*copy from above: "::real" is not required due to " \<up> "*)
85 ("(- 12 + 4 * y + 3 * x \<up> 2 + - 1 * (x \<up> 2 * y)) /" ^
86 "(- 18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)");
87 "~~~~~ fun cancel_p_, args:"; val (t) = (t);
88 val opt = check_fraction t;
89 val SOME (numerator, denominator) = opt;
90 (*+*)UnparseC.term numerator = "- 12 + 4 * y + 3 * x \<up> 2 + - 1 * (x \<up> 2 * y)"; (*isa -- isa2*);
91 (*+*)UnparseC.term denominator = "- 18 + - 9 * x + 2 * y \<up> 2 + x * y \<up> 2"; (*isa -- isa2*);
92 val vs = TermC.vars_of t;
93 (*+*)UnparseC.terms vs = "[\"x\", \"y\"]";
94 val baseT = type_of numerator
95 val expT = HOLogic.realT;
96 val (SOME _, SOME _) = (poly_of_term vs numerator, poly_of_term vs denominator); (*isa <> isa2*)
98 "-------- fun is_poly --------------------------------------------------------------------------";
99 "-------- fun is_poly --------------------------------------------------------------------------";
100 "-------- fun is_poly --------------------------------------------------------------------------";
101 if is_poly (TermC.str2term "2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + 7 * y \<up> 8 + 1")
102 then () else error "is_poly 1 changed";
103 if not (is_poly (TermC.str2term "2 * (x \<up> 3 * y \<up> 4 * z \<up> 6 + 7) * y \<up> 8 + 1"))
104 then () else error "is_poly 2 changed";
106 "-------- fun term_of_poly ---------------------------------------------------------------------";
107 "-------- fun term_of_poly ---------------------------------------------------------------------";
108 "-------- fun term_of_poly ---------------------------------------------------------------------";
109 val expT = HOLogic.realT
110 val Free (_, baseT) = (hd o vars o TermC.str2term) "12 * x \<up> 3 * y \<up> 4 * z \<up> 6";
111 val p = [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 5])]
112 val vs = TermC.vars_of (the (parseNEW ctxt "12 * x \<up> 3 * y \<up> 4 * z \<up> 6"))
113 (*precondition for [(c, es),...]: legth es = length vs*)
115 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"
116 then () else error "term_of_poly 1 changed";
118 "-------- fun cancel_p special cases -----------------------------------------------------------";
119 "-------- fun cancel_p special cases -----------------------------------------------------------";
120 "-------- fun cancel_p special cases -----------------------------------------------------------";
121 val thy = @{theory Isac_Knowledge};
123 (*------- standard case: *)
124 val t = TermC.str2term "2 / 3 + 1 / 6 ::real";
125 "~~~~~ fun add_fraction_p_ , args:"; val ((_: theory), t) = (thy, t);
126 val SOME ((n1, d1), (n2, d2)) =
127 (*case*) check_frac_sum t (*of*);
128 val vs = TermC.vars_of t;
130 val (SOME n1', SOME a, SOME n2', SOME b) =
131 (*case*) (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) (*of*);
132 val ((a', b'), c) = gcd_poly a b
133 val (baseT, expT) = (type_of n1, HOLogic.realT);
134 (*+*)val [(1, [])] = a'; (* 6 * _1_ = 6 *)
135 (*+*)val [(2, [])] = b'; (* 3 * _2_ = 6 *)
136 (*+*)val [(3, [])] = c; (* 3 / 6 \<and> 3 / 3 ..gcd *)
138 val nomin = term_of_poly baseT expT vs
139 (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'));
141 (*+*)val "5" = UnparseC.term nomin; (* = "3" ERROR*)
143 (*+*)val [(2, [])] = the (poly_of_term vs n1); (*---v----------------------v----*)
144 (*+*)val [(4, [])] = ((the (poly_of_term vs n1)) %%*%% b'); (* = 2 * _2_ new nomin for 2 / 3*)
146 (*+*)val [(1, [])] = the (poly_of_term vs n2); (*---v----------------------v----*)
147 (*+*)val [(1, [])] = ((the (poly_of_term vs n2)) %%*%% a'); (* = 1 * _1_ new nomin for 1 / 6*)
149 (*+*)val [(5, [])] = (* = 4 + 1 new nomin for sum *)
150 (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'));
152 val denom = (* = 3 * 1 * 2 new denom for sum *)
153 term_of_poly baseT expT vs ((c %%*%% a') %%*%% b');
154 (*+*)val "6" = UnparseC.term denom;
156 val t' = HOLogic.mk_binop \<^const_name>\<open>divide\<close> (nomin, denom);
157 (*+*)val "5 / 6" = UnparseC.term t'
160 (*------- 0 / m + 0 / n
161 20 years old bug found here: *)
162 val t = TermC.str2term "0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + - 1 * q_0 / 24 * 0 \<up> 4)";
163 val SOME (t', _) = rewrite_set_ thy true norm_Rational t;
166 ## rls: cancel_p_rls on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24)
167 ### rls: cancel_p on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24)
168 ------------------------------------------------------------these are missing now -----\
169 /## rls: cancel_p on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 1) from isa2: strange behaviour
170 /## rls: cancel_p on: 0 = c_2 + 1 / EI * (0 / 1 + 0 / 1) from isa2: strange behaviour
171 ------------------------------------------------------------these are missing now -----/
172 ## rls: norm_Rational_rls on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24)
173 ### rls: add_fractions_p_rls on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24)
174 #### rls: add_fractions_p on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24)
175 --------------------------------------------------^v^v^v^v^v^v^v^v^--undetected bug
176 #### rls: add_fractions_p on: 0 = c_2 + 1 / EI * (3 / 24) =3: ERROR
177 ### rls: rat_mult_div_pow on: 0 = c_2 + 1 / EI * (3 / 24)
180 if UnparseC.term t' = "0 = c_2" then () else error "norm_Rational CHANGED"; (*isa2*)
182 val t = TermC.str2term "0 / 12 + 0 / 24 ::real";
183 add_fraction_p_ @{theory} t;
184 "~~~~~ fun add_fraction_p_ , args:"; val ((_: theory), t) = (thy, t);
185 val SOME ((n1, d1), (n2, d2)) =
186 (*case*) check_frac_sum t (*of*);
188 (*+*)val Const ("Groups.zero_class.zero", _) = n1;
189 (*+*)val Const ("Groups.zero_class.zero", _) = n2;
191 val vs = TermC.vars_of t;
194 val (SOME n1', SOME a, SOME n2', SOME b) =
195 (*case*) (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) (*of*);
197 (*+*)if n1' = [(0, [])] then () else error "correction w.r.t zero polynomial CHANGED";
199 val ((a', b'), c) = gcd_poly a b
200 val (baseT, expT) = (type_of n1, HOLogic.realT);
201 (*+*)val [(1, [])] = a'; (* 1 * _1_ = 24 *)
202 (*+*)val [(2, [])] = b'; (* 2 * _2_ = 12 *)
203 (*+*)val [(12, [])] = c; (* 12 / 24 \<and> 12 / 12 ..gcd *)
205 (*/------------------ TOODOO broken with "repair cancellation with zero polynomial" -----------\* )
206 val nomin = term_of_poly baseT expT vs
207 (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'));
209 (*+*)UnparseC.term nomin; (* = "3" ERROR*)
210 (* correct ERROR ------------------------------------------------------------------\\*)
211 (*+*)val SOME [(0, [])] = poly_of_term vs n1 (* ERROR WAS [(1, [])] *)
212 (* correct ERROR ------------------------------------------------------------------//*)
214 (*+*)val [(0, [])] = the (poly_of_term vs n1); (*---v----------------------v-----*)
215 (*+*)val [(0, [])] = ((the (poly_of_term vs n1)) %%*%% b'); (* = 0 * _0_ new nomin for 0 / 12*)
217 (*+*)val [(0, [])] = the (poly_of_term vs n2); (*---v----------------------v-----*)
218 (*+*)val [(0, [])] = ((the (poly_of_term vs n2)) %%*%% a'); (* = 0 * _0_ new nomin for 0 / 24*)
220 (*+*)val [(0, [])] = (* = 0 + 0 new nomin for sum *)
221 (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'));
223 val denom = (* = 12 * 1 * 2 new denom for sum *)
224 term_of_poly baseT expT vs ((c %%*%% a') %%*%% b');
225 (*+*)val "24" = UnparseC.term denom;
227 val t' = HOLogic.mk_binop \<^const_name>\<open>divide\<close> (nomin, denom);
228 (*+*)val "0 / 24" = UnparseC.term t'
229 ( *\------------------ TOODOO broken with "repair cancellation with zero polynomial" -----------/*)
231 (*---------- fun cancel_p with Const AA *)
232 val thy = @{theory Partial_Fractions};
233 val ctxt = Proof_Context.init_global @{theory}
234 val SOME t = TermC.parseNEW ctxt "2 * AA / 2"; (* Const (\<^const_name>\<open>AA\<close>, "real") *)
236 val SOME (t', _) = rewrite_set_ thy true cancel_p t;
238 Const (\<^const_name>\<open>divide\<close>, _) $ Const (\<^const_name>\<open>AA\<close>, _) $
239 Const (\<^const_name>\<open>one_class.one\<close>, _) => ()
240 | _ => error "WRONG rewrite_set_ cancel_p (2 * AA / 2) \<longrightarrow> AA changed";
242 "~~~~~ fun cancel_p , args:"; val (t) = (t);
243 val opt = check_fraction t
244 val SOME (numerator, denominator) = (*case*) opt (*of*);
246 if UnparseC.term numerator = "2 * AA" andalso UnparseC.term denominator = "2"
247 then () else error "check_fraction (2 * AA / 2) changed";
248 val vs = TermC.vars_of t;
250 [Const (\<^const_name>\<open>AA\<close>, _)] => ()
251 | _ => error "rewrite_set_ cancel_p (2 * AA / 2) \<longrightarrow> AA/1 changed";
254 "-------- complex examples: rls norm_Rational --------------------------------------------------";
255 "-------- complex examples: rls norm_Rational --------------------------------------------------";
256 "-------- complex examples: rls norm_Rational --------------------------------------------------";
257 val t = TermC.str2term "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0";
258 val SOME (t', _) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
259 if UnparseC.term t' = "1 / 18 = 0" then () else error "rational.sml 1";
261 val t = TermC.str2term "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";
262 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
263 if UnparseC.term t' = "(237 + 65 * x) / 36 = 0" then ()
264 else error "rational.sml 2";
266 val t = TermC.str2term "(1/2 + (5*x)/2) \<up> 2 - ((13*x)/2 - 5/2) \<up> 2 - (6*x) \<up> 2 + 29";
267 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
268 if UnparseC.term t' = "23 + 35 * x + - 72 * x \<up> 2" then ()
269 else error "rational.sml 3";
271 "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";
272 "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";
273 "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";
274 (*Schalk I, p.60 Nr. 215c *)
275 val t = TermC.str2term "(a + b) \<up> 4 * (x - y) / ((x - y) \<up> 3 * (a + b) \<up> 2)";
276 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
277 if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + - 2 * x * y + y \<up> 2)"
278 then () else error "rational.sml: diff.behav. in norm_Rational_mg 7";
280 (*SRC Schalk I, p.66 Nr. 381b *)
281 val t = TermC.str2term
282 "(4*x \<up> 2 - 20*x + 25)/(2*x - 5) \<up> 3";
283 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
284 if UnparseC.term t = "1 / (- 5 + 2 * x)"
285 then () else error "rational.sml: diff.behav. in norm_Rational_mg 9";
287 (*Schalk I, p.60 Nr. 215c *)
288 val t = TermC.str2term "(a + b) \<up> 4 * (x - y) / ((x - y) \<up> 3 * (a + b) \<up> 2)";
289 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
290 if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + - 2 * x * y + y \<up> 2)"
291 then () else error "Schalk I, p.60 Nr. 215c: with Isabelle2002 cancellation incomplete, changed";