22 |
22 |
23 "-------- fun poly_of_term ---------------------------------------------------------------------"; |
23 "-------- fun poly_of_term ---------------------------------------------------------------------"; |
24 "-------- fun poly_of_term ---------------------------------------------------------------------"; |
24 "-------- fun poly_of_term ---------------------------------------------------------------------"; |
25 "-------- fun poly_of_term ---------------------------------------------------------------------"; |
25 "-------- fun poly_of_term ---------------------------------------------------------------------"; |
26 val thy = @{theory Isac_Knowledge}; |
26 val thy = @{theory Isac_Knowledge}; |
27 val vs = TermC.vars_of (TermC.str2term "12 * x \<up> 3 * y \<up> 4 * z \<up> 6"); |
27 val vs = TermC.vars_of (TermC.parse_test @{context} "12 * x \<up> 3 * y \<up> 4 * z \<up> 6"); |
28 |
28 |
29 val t = TermC.str2term "0 ::real"; |
29 val t = TermC.parse_test @{context} "0 ::real"; |
30 if poly_of_term vs t = SOME [(0, [0, 0, 0])] |
30 if poly_of_term vs t = SOME [(0, [0, 0, 0])] |
31 then () else error "poly_of_term 0 changed"; |
31 then () else error "poly_of_term 0 changed"; |
32 |
32 |
33 val t = TermC.str2term "-3 + - 2 * x ::real"; |
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])] |
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"; |
35 then () else error "poly_of_term uminus changed"; |
36 |
36 |
37 if poly_of_term vs (TermC.str2term "12::real") = SOME [(12, [0, 0, 0])] |
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"; |
38 then () else error "poly_of_term 1 changed"; |
39 |
39 |
40 if poly_of_term vs (TermC.str2term "x::real") = SOME [(1, [1, 0, 0])] |
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"; |
41 then () else error "poly_of_term 2 changed"; |
42 |
42 |
43 if poly_of_term vs (TermC.str2term "12 * x \<up> 3") = SOME [(12, [3, 0, 0])] |
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"; |
44 then () else error "poly_of_term 3 changed"; |
45 "~~~~~ fun poly_of_term , args:"; val (vs, t) = |
45 "~~~~~ fun poly_of_term , args:"; val (vs, t) = |
46 (vs, (TermC.str2term "12 * x \<up> 3")); |
46 (vs, (TermC.parse_test @{context} "12 * x \<up> 3")); |
47 |
47 |
48 monom_of_term vs (1, replicate (length vs) 0) t;(*poly malformed 1 with 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)) = |
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); |
50 (vs, (1, replicate (length vs) 0), t); |
51 val (c', es') = |
51 val (c', es') = |
57 (*+*)(num |> HOLogic.dest_numeral |> list_update es (find_index (curry op = t) vs)) = [3, 0, 0]; |
57 (*+*)(num |> HOLogic.dest_numeral |> list_update es (find_index (curry op = t) vs)) = [3, 0, 0]; |
58 |
58 |
59 if (c, num |> HOLogic.dest_numeral |> list_update es (find_index (curry op = t) vs)) = (12, [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"; |
60 then () else error "monom_of_term (realpow): return value CHANGED"; |
61 |
61 |
62 if poly_of_term vs (TermC.str2term "12 * x \<up> 3 * y \<up> 4 * z \<up> 6") = SOME [(12, [3, 4, 6])] |
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"; |
63 then () else error "poly_of_term 4 changed"; |
64 |
64 |
65 if poly_of_term vs (TermC.str2term "1 + 2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + y") = |
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])] |
66 SOME [(1, [0, 0, 0]), (1, [0, 1, 0]), (2, [3, 4, 6])] |
67 then () else error "poly_of_term 5 changed"; |
67 then () else error "poly_of_term 5 changed"; |
68 |
68 |
69 (*poly_of_term is quite liberal:*) |
69 (*poly_of_term is quite liberal:*) |
70 (*the coefficient may be somewhere, the order of variables and the parentheses |
70 (*the coefficient may be somewhere, the order of variables and the parentheses |
71 within a monomial are arbitrary*) |
71 within a monomial are arbitrary*) |
72 if poly_of_term vs (TermC.str2term "y \<up> 4 * (x \<up> 3 * 12 * z \<up> 6)") = SOME [(12, [3, 4, 6])] |
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"; |
73 then () else error "poly_of_term 6 changed"; |
74 |
74 |
75 (*there may even be more than 1 coefficient:*) |
75 (*there may even be more than 1 coefficient:*) |
76 if poly_of_term vs (TermC.str2term "2 * y \<up> 4 * (x \<up> 3 * 6 * z \<up> 6)") = SOME [(12, [3, 4, 6])] |
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"; |
77 then () else error "poly_of_term 7 changed"; |
78 |
78 |
79 (*the order and the parentheses within monomials are arbitrary:*) |
79 (*the order and the parentheses within monomials are arbitrary:*) |
80 if poly_of_term vs (TermC.str2term "2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + (7 * y \<up> 8 + 1)") |
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])] |
81 = SOME [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 6])] |
82 then () else error "poly_of_term 8 changed"; |
82 then () else error "poly_of_term 8 changed"; |
83 |
83 |
84 (*from --- rls norm_Rational downto fun gcd_poly ---*) |
84 (*from --- rls norm_Rational downto fun gcd_poly ---*) |
85 val t = TermC.str2term (*copy from above: "::real" is not required due to " \<up> "*) |
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)) /" ^ |
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)"); |
87 "(- 18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)"); |
88 "~~~~~ fun cancel_p_, args:"; val (t) = (t); |
88 "~~~~~ fun cancel_p_, args:"; val (t) = (t); |
89 val opt = check_fraction t; |
89 val opt = check_fraction t; |
90 val SOME (numerator, denominator) = opt; |
90 val SOME (numerator, denominator) = opt; |
97 val (SOME _, SOME _) = (poly_of_term vs numerator, poly_of_term vs denominator); (*isa <> isa2*) |
97 val (SOME _, SOME _) = (poly_of_term vs numerator, poly_of_term vs denominator); (*isa <> isa2*) |
98 |
98 |
99 "-------- fun is_poly --------------------------------------------------------------------------"; |
99 "-------- fun is_poly --------------------------------------------------------------------------"; |
100 "-------- fun is_poly --------------------------------------------------------------------------"; |
100 "-------- fun is_poly --------------------------------------------------------------------------"; |
101 "-------- fun is_poly --------------------------------------------------------------------------"; |
101 "-------- fun is_poly --------------------------------------------------------------------------"; |
102 if is_poly (TermC.str2term "2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + 7 * y \<up> 8 + 1") |
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"; |
103 then () else error "is_poly 1 changed"; |
104 if not (is_poly (TermC.str2term "2 * (x \<up> 3 * y \<up> 4 * z \<up> 6 + 7) * y \<up> 8 + 1")) |
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"; |
105 then () else error "is_poly 2 changed"; |
106 |
106 |
107 "-------- fun is_ratpolyexp --------------------------------------------------------------------"; |
107 "-------- fun is_ratpolyexp --------------------------------------------------------------------"; |
108 "-------- fun is_ratpolyexp --------------------------------------------------------------------"; |
108 "-------- fun is_ratpolyexp --------------------------------------------------------------------"; |
109 "-------- fun is_ratpolyexp --------------------------------------------------------------------"; |
109 "-------- fun is_ratpolyexp --------------------------------------------------------------------"; |
120 |
120 |
121 "-------- fun term_of_poly ---------------------------------------------------------------------"; |
121 "-------- fun term_of_poly ---------------------------------------------------------------------"; |
122 "-------- fun term_of_poly ---------------------------------------------------------------------"; |
122 "-------- fun term_of_poly ---------------------------------------------------------------------"; |
123 "-------- fun term_of_poly ---------------------------------------------------------------------"; |
123 "-------- fun term_of_poly ---------------------------------------------------------------------"; |
124 val expT = HOLogic.realT |
124 val expT = HOLogic.realT |
125 val Free (_, baseT) = (hd o vars o TermC.str2term) "12 * x \<up> 3 * y \<up> 4 * z \<up> 6"; |
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])] |
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")) |
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*) |
128 (*precondition for [(c, es),...]: legth es = length vs*) |
129 ; |
129 ; |
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" |
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" |
135 "-------- fun cancel_p special cases -----------------------------------------------------------"; |
135 "-------- fun cancel_p special cases -----------------------------------------------------------"; |
136 val thy = @{theory Isac_Knowledge}; |
136 val thy = @{theory Isac_Knowledge}; |
137 val ctxt = Proof_Context.init_global thy |
137 val ctxt = Proof_Context.init_global thy |
138 |
138 |
139 (*------- standard case: *) |
139 (*------- standard case: *) |
140 val t = TermC.str2term "2 / 3 + 1 / 6 ::real"; |
140 val t = TermC.parse_test @{context} "2 / 3 + 1 / 6 ::real"; |
141 "~~~~~ fun add_fraction_p_ , args:"; val ((_: theory), t) = (thy, t); |
141 "~~~~~ fun add_fraction_p_ , args:"; val ((_: theory), t) = (thy, t); |
142 val SOME ((n1, d1), (n2, d2)) = |
142 val SOME ((n1, d1), (n2, d2)) = |
143 (*case*) check_frac_sum t (*of*); |
143 (*case*) check_frac_sum t (*of*); |
144 val vs = TermC.vars_of t; |
144 val vs = TermC.vars_of t; |
145 (*+*)val [] = vs; |
145 (*+*)val [] = vs; |
193 ### rls: rat_mult_div_pow on: 0 = c_2 + 1 / EI * (3 / 24) |
193 ### rls: rat_mult_div_pow on: 0 = c_2 + 1 / EI * (3 / 24) |
194 : |
194 : |
195 *) |
195 *) |
196 if UnparseC.term t' = "0 = c_2" then () else error "norm_Rational CHANGED"; (*isa2*) |
196 if UnparseC.term t' = "0 = c_2" then () else error "norm_Rational CHANGED"; (*isa2*) |
197 |
197 |
198 val t = TermC.str2term "0 / 12 + 0 / 24 ::real"; |
198 val t = TermC.parse_test @{context} "0 / 12 + 0 / 24 ::real"; |
199 add_fraction_p_ @{theory} t; |
199 add_fraction_p_ @{theory} t; |
200 "~~~~~ fun add_fraction_p_ , args:"; val ((_: theory), t) = (thy, t); |
200 "~~~~~ fun add_fraction_p_ , args:"; val ((_: theory), t) = (thy, t); |
201 val SOME ((n1, d1), (n2, d2)) = |
201 val SOME ((n1, d1), (n2, d2)) = |
202 (*case*) check_frac_sum t (*of*); |
202 (*case*) check_frac_sum t (*of*); |
203 |
203 |
266 |
266 |
267 |
267 |
268 "-------- complex examples: rls norm_Rational --------------------------------------------------"; |
268 "-------- complex examples: rls norm_Rational --------------------------------------------------"; |
269 "-------- complex examples: rls norm_Rational --------------------------------------------------"; |
269 "-------- complex examples: rls norm_Rational --------------------------------------------------"; |
270 "-------- complex examples: rls norm_Rational --------------------------------------------------"; |
270 "-------- complex examples: rls norm_Rational --------------------------------------------------"; |
271 val t = TermC.str2term "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0"; |
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'; |
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"; |
273 if UnparseC.term t' = "1 / 18 = 0" then () else error "rational.sml 1"; |
274 |
274 |
275 val t = TermC.str2term "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0"; |
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'; |
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 () |
277 if UnparseC.term t' = "(237 + 65 * x) / 36 = 0" then () |
278 else error "rational.sml 2"; |
278 else error "rational.sml 2"; |
279 |
279 |
280 val t = TermC.str2term "(1/2 + (5*x)/2) \<up> 2 - ((13*x)/2 - 5/2) \<up> 2 - (6*x) \<up> 2 + 29"; |
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'; |
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 () |
282 if UnparseC.term t' = "23 + 35 * x + - 72 * x \<up> 2" then () |
283 else error "rational.sml 3"; |
283 else error "rational.sml 3"; |
284 |
284 |
285 "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------"; |
285 "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------"; |
286 "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------"; |
286 "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------"; |
287 "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------"; |
287 "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------"; |
288 (*Schalk I, p.60 Nr. 215c *) |
288 (*Schalk I, p.60 Nr. 215c *) |
289 val t = TermC.str2term "(a + b) \<up> 4 * (x - y) / ((x - y) \<up> 3 * (a + b) \<up> 2)"; |
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; |
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)" |
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"; |
292 then () else error "rational.sml: diff.behav. in norm_Rational_mg 7"; |
293 |
293 |
294 (*SRC Schalk I, p.66 Nr. 381b *) |
294 (*SRC Schalk I, p.66 Nr. 381b *) |
295 val t = TermC.str2term |
295 val t = TermC.parse_test @{context} |
296 "(4*x \<up> 2 - 20*x + 25)/(2*x - 5) \<up> 3"; |
296 "(4*x \<up> 2 - 20*x + 25)/(2*x - 5) \<up> 3"; |
297 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
297 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
298 if UnparseC.term t = "1 / (- 5 + 2 * x)" |
298 if UnparseC.term t = "1 / (- 5 + 2 * x)" |
299 then () else error "rational.sml: diff.behav. in norm_Rational_mg 9"; |
299 then () else error "rational.sml: diff.behav. in norm_Rational_mg 9"; |
300 |
300 |
301 (*Schalk I, p.60 Nr. 215c *) |
301 (*Schalk I, p.60 Nr. 215c *) |
302 val t = TermC.str2term "(a + b) \<up> 4 * (x - y) / ((x - y) \<up> 3 * (a + b) \<up> 2)"; |
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; |
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)" |
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"; |
305 then () else error "Schalk I, p.60 Nr. 215c: with Isabelle2002 cancellation incomplete, changed"; |
306 |
306 |