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