1 (* Title: tests for rationals
3 Use is subject to license terms.
6 "-----------------------------------------------------------------------------";
7 "-----------------------------------------------------------------------------";
8 "table of contents -----------------------------------------------------------";
9 "-----------------------------------------------------------------------------";
10 "-------- fun poly_of_term ---------------------------------------------------";
11 "-------- fun is_poly --------------------------------------------------------";
12 "-------- fun term_of_poly ---------------------------------------------------";
13 "-------- integration lev.1 fun factout_p_ -----------------------------------";
14 "-------- integration lev.1 fun cancel_p_ ------------------------------------";
15 "-------- integration lev.1 fun common_nominator_p_ --------------------------";
16 "-------- integration lev.1 fun add_fraction_p_ ------------------------------";
17 "Rfuns-------- and app_rev ...traced down from rewrite_set_ until prepats ---------";
18 "Rfuns-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------";
19 "-------- rls norm_Rational downto fun gcd_poly ------------------------------";
20 "Rfuns-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";
21 "----------- rewrite_set_ Partial_Fractions norm_Rational --------------------------------------";
22 "----------- fun check_frac_sum with Free A and Const AA ---------------------------------------";
23 "----------- fun cancel_p with Const AA --------------------------------------------------------";
24 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
25 "-------- rewrite_set_ add_fractions_p from: Mathematik 1 Schalk -------------";
26 "-------- integration lev.1 -- lev.5: cancel_p_ & add_fractions_p_ -----------";
27 "Rfuns-------- reverse rewrite ----------------------------------------------------";
28 "Rfuns-------- 'reverse-ruleset' cancel_p -----------------------------------------";
29 "-------- investigate rls norm_Rational --------------------------------------";
30 "-------- examples: rls norm_Rational ----------------------------------------";
31 "-------- rational numerals --------------------------------------------------";
32 "-------- examples cancellation from: Mathematik 1 Schalk --------------------";
33 "-------- examples common denominator from: Mathematik 1 Schalk --------------";
34 "-------- examples multiply and cancel from: Mathematik 1 Schalk -------------";
35 "-------- examples common denominator and multiplication from: Schalk --------";
36 "-------- examples double fractions from: Mathematik 1 Schalk ----------------";
37 "-------- me Schalk I No.186 -------------------------------------------------";
38 "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------------------";
39 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------------------";
40 "-------- investigate rulesets for cancel_p ----------------------------------";
41 "-------- fun eval_get_denominator -------------------------------------------";
42 "-------- several errpats in complicated term --------------------------------";
43 "-------- WN1309xx non-terminating rls norm_Rational -------------------------";
44 "-----------------------------------------------------------------------------";
45 "-----------------------------------------------------------------------------";
48 "-------- fun poly_of_term ---------------------------------------------------";
49 "-------- fun poly_of_term ---------------------------------------------------";
50 "-------- fun poly_of_term ---------------------------------------------------";
51 val thy = @{theory Partial_Fractions};
52 val vs = TermC.vars_of (TermC.str2term "12 * x \<up> 3 * y \<up> 4 * z \<up> 6");
54 val t = TermC.str2term "-3 + -2 * x ::real";
55 if poly_of_term vs t = SOME [(~3, [0, 0, 0]), (~2, [1, 0, 0])]
56 then () else error "poly_of_term uminus changed";
58 if poly_of_term vs (TermC.str2term "12::real") = SOME [(12, [0, 0, 0])]
59 then () else error "poly_of_term 1 changed";
61 if poly_of_term vs (TermC.str2term "x::real") = SOME [(1, [1, 0, 0])]
62 then () else error "poly_of_term 2 changed";
64 if poly_of_term vs (TermC.str2term "12 * x \<up> 3") = SOME [(12, [3, 0, 0])]
65 then () else error "poly_of_term 3 changed";
66 "~~~~~ fun poly_of_term , args:"; val (vs, t) =
67 (vs, (TermC.str2term "12 * x \<up> 3"));
69 monom_of_term vs (1, replicate (length vs) 0) t;(*poly malformed 1 with x \<up> 3*)
70 "~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const ("Groups.times_class.times", _) $ m1 $ m2)) =
71 (vs, (1, replicate (length vs) 0), t);
74 monom_of_term vs (c, es) m1;
75 "~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const ("Transcendental.powr", _) $ (t as Free _) $ (Const ("Num.numeral_class.numeral", _) $ num)) ) =
78 (*+*)(num |> HOLogic.dest_numeral |> list_update es (find_index (curry op = t) vs)) = [3, 0, 0];
80 if (c, num |> HOLogic.dest_numeral |> list_update es (find_index (curry op = t) vs)) = (12, [3, 0, 0])
81 then () else error "monom_of_term (powr): return value CHANGED";
83 if poly_of_term vs (TermC.str2term "12 * x \<up> 3 * y \<up> 4 * z \<up> 6") = SOME [(12, [3, 4, 6])]
84 then () else error "poly_of_term 4 changed";
86 if poly_of_term vs (TermC.str2term "1 + 2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + y") =
87 SOME [(1, [0, 0, 0]), (1, [0, 1, 0]), (2, [3, 4, 6])]
88 then () else error "poly_of_term 5 changed";
90 (*poly_of_term is quite liberal:*)
91 (*the coefficient may be somewhere, the order of variables and the parentheses
92 within a monomial are arbitrary*)
93 if poly_of_term vs (TermC.str2term "y \<up> 4 * (x \<up> 3 * 12 * z \<up> 6)") = SOME [(12, [3, 4, 6])]
94 then () else error "poly_of_term 6 changed";
96 (*there may even be more than 1 coefficient:*)
97 if poly_of_term vs (TermC.str2term "2 * y \<up> 4 * (x \<up> 3 * 6 * z \<up> 6)") = SOME [(12, [3, 4, 6])]
98 then () else error "poly_of_term 7 changed";
100 (*the order and the parentheses within monomials are arbitrary:*)
101 if poly_of_term vs (TermC.str2term "2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + (7 * y \<up> 8 + 1)")
102 = SOME [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 6])]
103 then () else error "poly_of_term 8 changed";
105 (*from --- rls norm_Rational downto fun gcd_poly ---*)
106 val t = TermC.str2term (*copy from above: "::real" is not required due to " \<up> "*)
107 ("(-12 + 4 * y + 3 * x \<up> 2 + -1 * (x \<up> 2 * y)) /" ^
108 "(-18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)");
109 "~~~~~ fun cancel_p_, args:"; val (t) = (t);
110 val opt = check_fraction t;
111 val SOME (numerator, denominator) = opt;
112 (*+*)UnparseC.term numerator = "- 12 + 4 * y + 3 * x \<up> 2 + - 1 * (x \<up> 2 * y)"; (*isa -- isa2*);
113 (*+*)UnparseC.term denominator = "- 18 + - 9 * x + 2 * y \<up> 2 + x * y \<up> 2"; (*isa -- isa2*);
114 val vs = TermC.vars_of t;
115 (*+*)UnparseC.terms vs = "[\"x\", \"y\"]";
116 val baseT = type_of numerator
117 val expT = HOLogic.realT;
118 val (SOME _, SOME _) = (poly_of_term vs numerator, poly_of_term vs denominator); (*isa <> isa2*)
120 "-------- fun is_poly --------------------------------------------------------";
121 "-------- fun is_poly --------------------------------------------------------";
122 "-------- fun is_poly --------------------------------------------------------";
123 if is_poly (TermC.str2term "2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + 7 * y \<up> 8 + 1")
124 then () else error "is_poly 1 changed";
125 if not (is_poly (TermC.str2term "2 * (x \<up> 3 * y \<up> 4 * z \<up> 6 + 7) * y \<up> 8 + 1"))
126 then () else error "is_poly 2 changed";
128 "-------- fun term_of_poly ---------------------------------------------------";
129 "-------- fun term_of_poly ---------------------------------------------------";
130 "-------- fun term_of_poly ---------------------------------------------------";
131 val expT = HOLogic.realT
132 val Free (_, baseT) = (hd o vars o TermC.str2term) "12 * x \<up> 3 * y \<up> 4 * z \<up> 6";
133 val p = [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 5])]
134 val vs = TermC.vars_of (the (parseNEW ctxt "12 * x \<up> 3 * y \<up> 4 * z \<up> 6"))
135 (*precondition for [(c, es),...]: legth es = length vs*)
137 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"
138 then () else error "term_of_poly 1 changed";
140 "-------- integration lev.1 fun factout_p_ -----------------------------------";
141 "-------- integration lev.1 fun factout_p_ -----------------------------------";
142 "-------- integration lev.1 fun factout_p_ -----------------------------------";
143 val t = TermC.str2term "(x \<up> 2 + -1*y \<up> 2) / (x \<up> 2 + -1*x*y)"
144 val SOME (t', asm) = factout_p_ thy t;
145 if UnparseC.term t' = "(x + y) * (x + - 1 * y) / (x * (x + - 1 * y))"
146 then () else error ("factout_p_ term 1 changed: " ^ UnparseC.term t')
148 if UnparseC.terms asm = "[\"x \<noteq> 0\", \"x + - 1 * y \<noteq> 0\"]"
149 then () else error "factout_p_ asm 1 changed"
151 val t = TermC.str2term "nothing + to_cancel ::real";
152 if NONE = factout_p_ thy t then () else error "factout_p_ doesn't report non-applicable";
154 val t = TermC.str2term "((3 * x \<up> 2 + 6 *x + 3) / (2*x + 2))";
155 val SOME (t', asm) = factout_p_ thy t;
156 if UnparseC.term t' = "(3 + 3 * x) * (1 + x) / (2 * (1 + x))" andalso
157 UnparseC.terms asm = "[\"1 + x \<noteq> 0\"]"
158 then () else error "factout_p_ 1 changed";
160 "-------- integration lev.1 fun cancel_p_ ------------------------------------";
161 "-------- integration lev.1 fun cancel_p_ ------------------------------------";
162 "-------- integration lev.1 fun cancel_p_ ------------------------------------";
163 val t = TermC.str2term "(x \<up> 2 + -1*y \<up> 2) / (x \<up> 2 + -1*x*y)"
164 val SOME (t', asm) = cancel_p_ thy t;
165 if (UnparseC.term t', UnparseC.terms asm) = ("(x + y) / x", "[\"x \<noteq> 0\"]")
166 then () else error ("cancel_p_ (t', asm) 1 changed: " ^ UnparseC.term t')
168 val t = TermC.str2term "nothing + to_cancel ::real";
169 if NONE = cancel_p_ thy t then () else error "cancel_p_ doesn't report non-applicable";
171 val t = TermC.str2term "((3 * x \<up> 2 + 6 *x + 3) / (2*x + 2))";
172 val SOME (t', asm) = cancel_p_ thy t;
173 if UnparseC.term t' = "(3 + 3 * x) / 2" andalso UnparseC.terms asm = "[]"
174 then () else error "cancel_p_ 1 changed";
176 "-------- integration lev.1 fun common_nominator_p_ --------------------------";
177 "-------- integration lev.1 fun common_nominator_p_ --------------------------";
178 "-------- integration lev.1 fun common_nominator_p_ --------------------------";
179 val t = TermC.str2term ("y / (a*x + b*x + c*x) " ^
183 val SOME (t', asm) = common_nominator_p_ thy t;
184 if UnparseC.term t' =
185 ("y * y / (x * ((a + b + c) * y)) " ^
186 (* n1 *d2'/ (c'* ( d1' *d2')) *)
187 "+ a * (a + b + c) / (x * ((a + b + c) * y))")
188 (* n2 * d1' / (c'* ( d1' *d2')) *)
189 then () else error "common_nominator_p_ term 1 changed";
190 if UnparseC.terms asm = "[\"a + b + c \<noteq> 0\", \"y \<noteq> 0\", \"x \<noteq> 0\"]"
191 then () else error "common_nominator_p_ asm 1 changed"
193 "-------- example in mail Nipkow";
194 val t = TermC.str2term "x/(x \<up> 2 + -1*y \<up> 2) + y/(x \<up> 2 + -1*x*y)";
195 val SOME (t', asm) = common_nominator_p_ thy t;
196 if UnparseC.term t' =
197 "x * x / ((x + - 1 * y) * ((x + y) * x)) +\ny * (x + y) / ((x + - 1 * y) * ((x + y) * x))"
198 then () else error "common_nominator_p_ term 2 changed"
200 if UnparseC.terms asm = "[\"x + y \<noteq> 0\", \"x \<noteq> 0\", \"x + - 1 * y \<noteq> 0\"]"
201 then () else error "common_nominator_p_ asm 2 changed"
203 "-------- example: applicable tested by SML code";
204 val t = TermC.str2term "nothing / to_add";
205 if NONE = common_nominator_p_ thy t then () else error "common_nominator_p_ term 3 changed";
207 val t = TermC.str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
208 val SOME (t', asm) = common_nominator_p_ thy t;
209 if UnparseC.term t' =
210 "(x + - 1) * (- 1 + x) / ((1 + x) * (- 1 + x)) +\n(x + 1) * (1 + x) / ((1 + x) * (- 1 + x))"
211 andalso UnparseC.terms asm = "[\"1 + x \<noteq> 0\", \"- 1 + x \<noteq> 0\"]"
212 then () else error "common_nominator_p_ 3 changed";
214 "-------- integration lev.1 fun add_fraction_p_ ------------------------------";
215 "-------- integration lev.1 fun add_fraction_p_ ------------------------------";
216 "-------- integration lev.1 fun add_fraction_p_ ------------------------------";
217 val t = TermC.str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
218 val SOME (t', asm) = add_fraction_p_ thy t;
219 if UnparseC.term t' = "(2 + 2 * x \<up> 2) / (- 1 + x \<up> 2)"
220 then () else error "add_fraction_p_ 3 changed";
222 if UnparseC.terms asm = "[\"- 1 + x \<up> 2 \<noteq> 0\"]"
223 then () else error "add_fraction_p_ 3 changed";
225 val t = TermC.str2term "nothing / to_add";
226 if NONE = add_fraction_p_ thy t then () else error "add_fraction_p_ term 3 changed";
228 val t = TermC.str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
229 val SOME (t', asm) = add_fraction_p_ thy t;
230 if UnparseC.term t' = "(2 + 2 * x \<up> 2) / (- 1 + x \<up> 2)" andalso
231 UnparseC.terms asm = "[\"- 1 + x \<up> 2 \<noteq> 0\"]"
232 then () else error "add_fraction_p_ 3 changed";
234 "-------- and app_rev ...traced down from rewrite_set_ until prepats ---------";
235 "-------- and app_rev ...traced down from rewrite_set_ until prepats ---------";
236 "-------- and app_rev ...traced down from rewrite_set_ until prepats ---------";
237 (* trace down until prepats are evaluated
238 (which does not to work, because substitution is not done -- compare rew_sub!);
239 keep this sequence for the case, factout_p, cancel_p, common_nominator_p, add_fraction_p
240 (again) get prepat = [] changed to <>[]. *)
241 val t = TermC.str2term "(x \<up> 2 + -1*y \<up> 2) / (x \<up> 2 + -1*x*y)";
243 (*rewrite_set_ @{theory Isac_Knowledge} true cancel t = NONE; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
244 "~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (thy, false, cancel_p, t);
245 "~~~~~ fun rewrite__set_, args:"; val (thy, i, _, _, (rrls as Rrls _), t) =
246 (thy, 1, bool, [], rls, term);
247 (*val (t', asm, rew) = app_rev thy (i+1) rrls t; rew = false!!!!!!!!!!!!!!!!!!!!!*)
248 "~~~~~ and app_rev, args:"; val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
249 fun chk_prepat thy erls [] t = true
250 | chk_prepat thy erls prepat t =
252 fun chk (pres, pat) =
254 val subst: Type.tyenv * Envir.tenv =
255 Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
257 snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
258 end) handle Pattern.MATCH => false
259 fun scan_ f [] = false (*scan_ NEVER called by []*)
260 | scan_ f (pp::pps) =
261 if f pp then true else scan_ f pps;
262 in scan_ chk prepat end;
263 (* apply the normal_form of a rev-set *)
264 fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
265 if chk_prepat thy erls prepat t
266 then ((*tracing("### app_rev': t = "^UnparseC.term t);*) normal_form t)
268 (* val opt = app_rev' thy rrls t ..NONE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
269 "~~~~~ and app_rev', args:"; val (thy, (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}), t) =
271 (* chk_prepat thy erls prepat t = false!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
272 (* app_sub thy i rrls t = false!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
273 "~~~~~ fun chk_prepat, args:"; val (thy, erls, prepat, t) = (thy, erls, prepat, t);
274 fun chk (pres, pat) =
276 val subst: Type.tyenv * Envir.tenv =
277 Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
279 snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
280 end) handle Pattern.MATCH => false
281 fun scan_ f [] = false (*scan_ NEVER called by []*)
282 | scan_ f (pp::pps) =
283 if f pp then true else scan_ f pps;
285 (*========== inhibit exn WN130823: prepat is empty ====================================
286 (* scan_ chk prepat = false!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
287 "~~~~~ fun , args:"; val (f, (pp::pps)) = (chk, prepat);
289 val ([t1, t2], t) = pp;
290 UnparseC.term t1 = "?r is_expanded";
291 UnparseC.term t2 = "?s is_expanded";
292 UnparseC.term t = "?r / ?s";
293 (* f pp = false!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
294 "~~~~~ fun chk, args:"; val (pres, pat) = (pp);
295 val subst: Type.tyenv * Envir.tenv =
296 Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
298 ({}, {(("r", 0), ("real", Var (("r", 0), "real"))),
299 (("s", 0), ("real", Var (("s", 0), "real")))}*)
301 snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
302 "~~~~~ fun eval__true, args:"; val (thy, i, asms, bdv, rls) =
303 (thy, (i + 1), (map (Envir.subst_term subst) pres), [], erls);
304 UnparseC.terms asms; (* = "[\"?r is_expanded\",\"?s is_expanded\"]"*)
305 asms = [@{term True}] orelse asms = []; (* = false*)
306 asms = [@{term False}] ; (* = false*)
307 "~~~~~ fun chk, args:"; val (indets, (a::asms)) = ([], asms);
308 bdv (*= []: _a list*);
309 val bdv : (term * term) list = [];
310 rewrite__set_ thy (i+1) false;
311 UnparseC.term a = "?r is_expanded"; (*hier m"usste doch der Numerator eingesetzt sein ??????????????*)
312 val SOME (Const ("HOL.False", _), []) = rewrite__set_ thy (i+1) false bdv rls a
313 ============ inhibit exn WN130823: prepat is empty ===================================*)
315 "-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------";
316 "-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------";
317 "-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------";
318 val t = TermC.str2term "(12 * x * y) / (8 * y \<up> 2 )";
319 (* "-------- example 187a": exception Div raised...
320 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;*)
321 val t = TermC.str2term "(8 * x \<up> 2 * y * z ) / (18 * x * y \<up> 2 * z )";
322 (* "-------- example 187b": doesn't terminate...
323 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;*)
324 val t = TermC.str2term "(9 * x \<up> 5 * y \<up> 2 * z \<up> 4) / (15 * x \<up> 6 * y \<up> 3 * z )";
325 (* "-------- example 187c": doesn't terminate...
326 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;*)
327 "~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (@{theory Isac_Knowledge}, false, cancel_p, t);
328 (* WN130827: exception Div raised...
329 rewrite__set_ thy 1 bool [] rls term
331 "~~~~~ and rewrite__set_, args:"; val (thy, i, _, _, (rrls as Rrls _), t) =
332 (thy, 1, bool, [], rls, term);
333 (* WN130827: exception Div raised...
334 val (t', asm, rew) = app_rev thy (i+1) rrls t
336 "~~~~~ fun app_rev, args:"; val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
337 (* WN130827: exception Div raised...
338 val opt = app_rev' thy rrls t
340 "~~~~~ fun app_rev', args:"; val (thy, (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}), t) =
342 chk_prepat thy erls prepat t = true;
343 (* WN130827: exception Div raised...
346 (* lookup Rational.thy, cancel_p: normal_form = cancel_p_ thy*)
347 "~~~~~ fun cancel_p_, args:"; val (t) = (t);
348 val opt = check_fraction t;
349 val SOME (numerator, denominator) = opt
350 val vs = TermC.vars_of t
351 val baseT = type_of numerator
352 val expT = HOLogic.realT
353 val (SOME a, SOME b) = (poly_of_term vs numerator, poly_of_term vs denominator);
354 (*"-------- example 187a": exception Div raised...
355 val a = [(12, [1, 1])]: poly
356 val b = [(8, [0, 2])]: poly
357 val ((a', b'), c) = gcd_poly a b
359 (* "-------- example 187b": doesn't terminate...
360 val a = [(8, [2, 1, 1])]: poly
361 val b = [(18, [1, 2, 1])]: poly
362 val ((a', b'), c) = gcd_poly a b
364 (* "-------- example 187c": doesn't terminate...
365 val a = [(9, [5, 2, 4])]: poly
366 val b = [(15, [6, 3, 1])]: poly
367 val ((a', b'), c) = gcd_poly a b
370 "-------- rls norm_Rational downto fun gcd_poly ------------------------------";
371 "-------- rls norm_Rational downto fun gcd_poly ------------------------------";
372 "-------- rls norm_Rational downto fun gcd_poly ------------------------------";
373 val t = TermC.str2term "(x \<up> 2 - 4)*(3 - y) / ((y \<up> 2 - 9)*(2+x))";
374 Rewrite.trace_on := false (*true false*);
375 (* trace stops with ...: (and then jEdit hangs)..
376 rewrite_set_ thy false norm_Rational t;
378 ### rls: cancel_p on: (-12 + 4 * y + 3 * x \<up> 2 + -1 * (x \<up> 2 * y)) /
379 (-18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)
381 val t = TermC.str2term (*copy from above: "::real" is not required due to " \<up> "*)
382 ("(-12 + 4 * y + 3 * x \<up> 2 + -1 * (x \<up> 2 * y)) /" ^
383 "(-18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)");
385 exception Div raised*)
387 "~~~~~ fun cancel_p_, args:"; val (t) = (t);
388 val opt = check_fraction t;
389 val SOME (numerator, denominator) = opt
390 val vs = TermC.vars_of t
391 val baseT = type_of numerator
392 val expT = HOLogic.realT;
393 (*default_print_depth 3; 999*)
394 val (SOME a, SOME b) = (poly_of_term vs numerator, poly_of_term vs denominator);
395 (*default_print_depth 3; 999*)
396 (* does not terminate instead of returning ?:
397 val ((a', b'), c) = gcd_poly a b
398 val a = [(~12, [0, 0]), (3, [2, 0]), (4, [0, 1]), (~1, [2, 1])]: poly
399 val b = [(~18, [0, 0]), (~9, [1, 0]), (2, [0, 2]), (1, [1, 2])]: poly
402 "-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";
403 "-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";
404 "-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";
405 val thy = @{theory Isac_Knowledge};
406 "----- SK060904-2a non-termination of add_fraction_p_";
407 val t = TermC.str2term (" (a + b * x) / (a + -1 * (b * x)) + " ^
408 " (-1 * a + b * x) / (a + b * x) ");
409 (* rewrite_set_ thy false norm_Rational t
410 exception Div raised*)
411 (* rewrite_set_ thy false add_fractions_p t;
412 exception Div raised*)
413 "~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) =
414 (@{theory Isac_Knowledge}, false, add_fractions_p, t);
415 "~~~~~ and rewrite__set_, args:"; val (thy, i, _, _, (rrls as Rrls _), t) =
416 (thy, 1, bool, [], rls, term);
417 (* app_rev thy (i+1) rrls t;
418 exception Div raised*)
419 "~~~~~ and app_rev, args:"; val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
420 fun chk_prepat thy erls [] t = true
421 | chk_prepat thy erls prepat t =
423 fun chk (pres, pat) =
425 val subst: Type.tyenv * Envir.tenv =
426 Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
428 snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
429 end) handle Pattern.MATCH => false
430 fun scan_ f [] = false (*scan_ NEVER called by []*)
431 | scan_ f (pp::pps) =
432 if f pp then true else scan_ f pps;
433 in scan_ chk prepat end;
434 (* apply the normal_form of a rev-set *)
435 fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
436 if chk_prepat thy erls prepat t
437 then ((*tracing("### app_rev': t = "^UnparseC.term t);*) normal_form t)
439 (* val opt = app_rev' thy rrls t;
440 exception Div raised*)
441 (* val opt = app_rev' thy rrls t;
442 exception Div raised*)
443 "~~~~~ and app_rev', args:"; val (thy, (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}), t) =
445 chk_prepat thy erls prepat t = true = true;
447 exception Div raised*)
448 (* lookup Rational.thy, val add_fractions_p: normal_form = add_fraction_p_ thy*)
449 (*add_fraction_p_ thy t
450 exception Div raised*)
451 "~~~~~ fun add_fraction_p_, args:"; val ((_: theory), t) = (thy, t);
452 val SOME ((n1, d1), (n2, d2)) = check_frac_sum t;
453 UnparseC.term n1; UnparseC.term d1; UnparseC.term n2; UnparseC.term d2;
454 val vs = TermC.vars_of t;
455 (*default_print_depth 3; 999*)
456 val (SOME _, SOME a, SOME _, SOME b) =
457 (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2);
458 (*default_print_depth 3; 999*)
460 val a = [(1, [1, 0, 0]), (~1, [0, 1, 1])]: poly
461 val b = [(1, [1, 0, 0]), (1, [0, 1, 1])]: poly
462 val ((a', b'), c) = gcd_poly a b
465 "----------- fun check_frac_sum with Free A and Const AA ---------------------------------------";
466 "----------- fun check_frac_sum with Free A and Const AA ---------------------------------------";
467 "----------- fun check_frac_sum with Free A and Const AA ---------------------------------------";
468 val thy = @{theory Isac_Knowledge(*Partial_Fractions*)}
469 val ctxt = Proof_Context.init_global thy;
471 (*---------- (1) with Free A, B ----------------------------------------------------------------*)
472 val t = (the o (parseNEW ctxt)) "3 = A / 2 + A / 4 + (B / 2 + -1 * B / (2::real))";
473 (* required for applying thms in rewriting \<up> ^*)
474 (* we get details from here..*)
476 Rewrite.trace_on := false;
477 val SOME (t', _) = Rewrite.rewrite_set_ thy true add_fractions_p t;
478 Rewrite.trace_on := false;
480 add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
481 (* |||||||||||||||||||||||||||||||||||| *)
483 val t = (the o (parseNEW ctxt))(* ||||||||||||||||||||||||| GUESS 1 GUESS 1 GUESS 1 GUESS 1 *)
484 "A / 2 + A / 4 + (B / 2 + -1 * B / (2::real))";
485 "~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
486 val NONE = (*case*) check_frac_sum t (*of*)
489 add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
490 (* |||||||||||||||||||||||||||| *)
491 val t = (the o (parseNEW ctxt))(* ||||||||||||||||||||||||| GUESS 2 GUESS 2 GUESS 2 GUESS 2 *)
492 "A / 4 + (B / 2 + -1 * B / (2::real))";
493 "~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
494 val SOME ((n1, d1), (n2, d2)) = (*case*) check_frac_sum t (*of*);
495 (*+*)if (UnparseC.term n1, UnparseC.term d1) = ("A" , "4") andalso
496 (*+*) (UnparseC.term n2, UnparseC.term d2) = ("B / 2 + - 1 * B / 2", "1")
497 (*+*)then () else error "check_frac_sum (A / 4 + (B / 2 + -1 * B / (2::real))) changed";
499 val vs = TermC.vars_of t;
500 val (SOME [(1, [1, 0])], SOME [(4, [0, 0])], NONE, SOME [(1, [0, 0])]) =
501 (*case*) (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) (*of*);
503 "~~~~~ fun poly_of_term , args:"; val (vs, t) = (vs, n1);
504 val SOME [(1, [xxx, 0])] = SOME [monom_of_term vs (1, replicate (length vs) 0) t];
505 (*+*)if xxx = 1 then () else error "monom_of_term changed"
507 "~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Free (id, _))) =
508 (vs, (1, replicate (length vs) 0), t);
509 case vs of [Free ("A", _), Free ("B", _)] =>
510 if c = 1 andalso id = "A"
511 then () else error "monom_of_term Free changed 1"
512 | _ => error "monom_of_term Free changed 2";
514 (*---------- (2) with Const AA, BB --------------------------------------------------------------*)
515 val t = (the o (parseNEW ctxt)) "3 = AA / 2 + AA / 4 + (BB / 2 + -1 * BB / 2)";
517 (* we get details from here..*)
519 Rewrite.trace_on := false;
520 val SOME (t', _) = Rewrite.rewrite_set_ thy true add_fractions_p t;
521 Rewrite.trace_on := false;
523 add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
524 (* |||||||||||||||||||||||||||||||||||| *)
525 val t = (the o (parseNEW ctxt))(* ||||||||||||||||||||||||| *)
526 "AA / 2 + AA / 4 + (BB / 2 + -1 * BB / 2)";
527 "~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
528 val NONE = (*case*) check_frac_sum t (*of*)
531 add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
532 (* |||||||||||||||||||||||||||| *)
533 val t = (the o (parseNEW ctxt))(* ||||||||||||||||||||||||| *)
534 "AA / 4 + (BB / 2 + -1 * BB / 2)";
535 "~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
536 val SOME ((n1, d1), (n2, d2)) = (*case*) check_frac_sum t (*of*);
537 (*+*)if (UnparseC.term n1, UnparseC.term d1) = ("AA" , "4") andalso
538 (*+*) (UnparseC.term n2, UnparseC.term d2) = ("BB / 2 + - 1 * BB / 2", "1")
539 (*+*)then () else error "check_frac_sum (AA / 4 + (BB / 2 + -1 * BB / 2)) changed";
541 val vs = TermC.vars_of t;
542 val (SOME [(1, [1, 0])], SOME [(4, [0, 0])], NONE, SOME [(1, [0, 0])]) =
543 (*case*) (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) (*of*);
545 "~~~~~ fun poly_of_term , args:"; val (vs, t) = (vs, n1);
546 val SOME [(1, [xxx, 0])] = SOME [monom_of_term vs (1, replicate (length vs) 0) t];
547 (*+*)if xxx = 1 then () else error "monom_of_term changed"
549 "~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const (id, _))) =
550 (vs, (1, replicate (length vs) 0), t);
551 case vs of [Const ("Partial_Fractions.AA", _), Const ("Partial_Fractions.BB", _)] =>
552 if c = 1 andalso id = "Partial_Fractions.AA"
553 then () else error "monom_of_term Const changed 1"
554 | _ => error "monom_of_term Const changed 2";
556 "----------- fun cancel_p with Const AA --------------------------------------------------------";
557 "----------- fun cancel_p with Const AA --------------------------------------------------------";
558 "----------- fun cancel_p with Const AA --------------------------------------------------------";
559 val thy = @{theory Partial_Fractions};
560 val ctxt = Proof_Context.init_global @{theory}
561 val SOME t = TermC.parseNEW ctxt "2 * AA / 2"; (* Const ("Free ("AA", "real") *)
563 val SOME (t', _) = rewrite_set_ thy true cancel_p t;
565 Const ("Rings.divide_class.divide", _) $ Const ("Partial_Fractions.AA", _) $
566 Const ("Groups.one_class.one", _) => ()
567 | _ => error "WRONG rewrite_set_ cancel_p (2 * AA / 2) \<longrightarrow> AA changed";
569 "~~~~~ fun cancel_p , args:"; val (t) = (t);
570 val opt = check_fraction t
571 val SOME (numerator, denominator) = (*case*) opt (*of*);
573 if UnparseC.term numerator = "2 * AA" andalso UnparseC.term denominator = "2"
574 then () else error "check_fraction (2 * AA / 2) changed";
575 val vs = TermC.vars_of t;
577 [Const ("Partial_Fractions.AA", _)] => ()
578 | _ => error "rewrite_set_ cancel_p (2 * AA / 2) \<longrightarrow> AA/1 changed";
581 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
582 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
583 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
584 val thy = @{theory "Rational"};
586 val t = TermC.str2term "(2 + -3 * x) / 9";
587 if NONE = rewrite_set_ thy false cancel_p t then ()
588 else error "rewrite_set_ cancel_p must return NONE, if the term cannot be cancelled";
590 "-------- example 186a";
591 val t = TermC.str2term "(14 * x * y) / (x * y)";
592 is_expanded (TermC.str2term "14 * x * y");
593 is_expanded (TermC.str2term "x * y");
594 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
595 if (UnparseC.term t', UnparseC.terms asm) = ("14 / 1", "[]")
596 then () else error "rational.sml cancel Schalk 186a";
598 "-------- example 186b";
599 val t = TermC.str2term "(60 * a * b) / ( 15 * a * b )";
600 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
601 if (UnparseC.term t', UnparseC.terms asm) = ("4 / 1", "[]")
602 then () else error "rational.sml cancel Schalk 186b";
604 "-------- example 186c";
605 val t = TermC.str2term "(144 * a \<up> 2 * b * c) / (12 * a * b * c)";
606 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
607 if (UnparseC.term t', UnparseC.terms asm) = ("12 * a / 1", "[]")
608 then () else error "rational.sml cancel Schalk 186c";
610 (* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! exception Div raised !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
611 see --- fun rewrite_set_ downto fun gcd_poly ---
612 "-------- example 187a";
613 val t = TermC.str2term "(12 * x * y) / (8 * y \<up> 2 )";
614 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
615 if (UnparseC.term t', UnparseC.terms asm) = ("3 * x / (2 * y)", "[\"4 * y ~= 0\"]")
616 then () else error "rational.sml cancel Schalk 187a";
619 (* doesn't terminate !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
620 see --- fun rewrite_set_ downto fun gcd_poly ---
621 "-------- example 187b";
622 val t = TermC.str2term "(8 * x \<up> 2 * y * z ) / (18 * x * y \<up> 2 * z )";
623 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
624 if (UnparseC.term t', UnparseC.terms asm) = ("4 * x / (9 * y)", "[\"2 * (z * (y * x)) ~= 0\"]")
625 then () else error "rational.sml cancel Schalk 187b";
628 (* doesn't terminate !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
629 see --- fun rewrite_set_ downto fun gcd_poly ---
630 "-------- example 187c";
631 val t = TermC.str2term "(9 * x \<up> 5 * y \<up> 2 * z \<up> 4) / (15 * x \<up> 6 * y \<up> 3 * z )";
632 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
633 if (UnparseC.term t', UnparseC.terms asm) =
634 ("3 * z \<up> 3 / (5 * (y * x))", "[\"3 * (z * (y \<up> 2 * x \<up> 5)) ~= 0\"]")
635 then () else error "rational.sml cancel Schalk 187c";
638 "-------- example 188a";
639 val t = TermC.str2term "(-8 + 8 * x) / (-9 + 9 * x)";
640 is_expanded (TermC.str2term "8 * x + -8");
641 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
642 if (UnparseC.term t', UnparseC.terms asm) = ("8 / 9", "[]")
643 then () else error "rational.sml cancel Schalk 188a";
645 val t = TermC.str2term "(8*((-1) + x))/(9*((-1) + x))";
646 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
647 if (UnparseC.term t', UnparseC.terms asm) = ("8 / 9", "[]")
648 then () else error "rational.sml cancel Schalk make_polynomial 1";
650 "-------- example 188b";
651 val t = TermC.str2term "(-15 + 5 * x) / (-18 + 6 * x)";
652 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
653 if (UnparseC.term t', UnparseC.terms asm) = ("5 / 6", "[]")
654 then () else error "rational.sml cancel Schalk 188b";
656 "-------- example 188c";
657 val t = TermC.str2term "(a + -1 * b) / (b + -1 * a)";
658 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
659 if (UnparseC.term t', UnparseC.terms asm) = ("- 1 / 1", "[]")
660 then () else error "rational.sml cancel Schalk 188c";
662 is_expanded (TermC.str2term "a + -1 * b") = true;
663 val t = TermC.str2term "((- 1)*(b + (-1) * a))/(1*(b + (- 1) * a))";
664 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
665 if (UnparseC.term t', UnparseC.terms asm) = ("(a + - 1 * b) / (- 1 * a + b)", "[]")
666 then () else error "rational.sml cancel Schalk make_polynomial 2";
668 "-------- example 190a";
669 val t = TermC.str2term "( 27 * a \<up> 3 + 9 * a \<up> 2 + 3 * a + 1 ) / ( 27 * a \<up> 3 + 18 * a \<up> 2 + 3 * a )";
670 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
671 if (UnparseC.term t', UnparseC.terms asm) =
672 ("(1 + 9 * a \<up> 2) / (3 * a + 9 * a \<up> 2)", "[\"3 * a + 9 * a \<up> 2 \<noteq> 0\"]")
673 then () else error "rational.sml cancel Schalk 190a";
675 "-------- example 190c";
676 val t = TermC.str2term "((1 + 9 * a \<up> 2)*(1 + 3 * a))/((3 * a + 9 * a \<up> 2)*(1 + 3 * a))";
677 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
678 if (UnparseC.term t', UnparseC.terms asm) =
679 ("(1 + 3 * a + 9 * a \<up> 2 + 27 * a \<up> 3) /\n(3 * a + 18 * a \<up> 2 + 27 * a \<up> 3)", "[]")
680 then () else error "rational.sml make_polynomial Schalk 190c";
682 "-------- example 191a";
683 val t = TermC.str2term "( x \<up> 2 + -1 * y \<up> 2 ) / ( x + y )";
684 is_expanded (TermC.str2term "x \<up> 2 + - 1 * y \<up> 2") = false; (*!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
685 is_expanded (TermC.str2term "x + y") = true;
686 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
687 if (UnparseC.term t', UnparseC.terms asm) = ("(x + - 1 * y) / 1", "[]")
688 then () else error "rational.sml make_polynomial Schalk 191a";
690 "-------- example 191b";
691 val t = TermC.str2term "((x + (- 1) * y)*(x + y))/((1)*(x + y))";
692 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
693 if (UnparseC.term t', UnparseC.terms asm) = ("(x \<up> 2 + - 1 * y \<up> 2) / (x + y)", "[]")
694 then () else error "rational.sml make_polynomial Schalk 191b";
696 "-------- example 191c";
697 val t = TermC.str2term "( 9 * x \<up> 2 + -30 * x + 25 ) / ( 9 * x \<up> 2 + -25 )";
698 is_expanded (TermC.str2term "9 * x \<up> 2 + -30 * x + 25") = true;
699 is_expanded (TermC.str2term "25 + -30*x + 9*x \<up> 2") = true;
700 is_expanded (TermC.str2term "-25 + 9*x \<up> 2") = true;
702 val t = TermC.str2term "(((-5) + 3 * x)*((-5) + 3 * x))/((5 + 3 * x)*((-5) + 3 * x))";
703 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
704 if (UnparseC.term t', UnparseC.terms asm) = ("(25 + - 30 * x + 9 * x \<up> 2) / (- 25 + 9 * x \<up> 2)", "[]")
705 then () else error "rational.sml make_polynomial Schalk 191c";
707 "-------- example 192b";
708 val t = TermC.str2term "( 7 * x \<up> 3 + - 1 * x \<up> 2 * y ) / ( 7 * x * y \<up> 2 + - 1 * y \<up> 3 )";
709 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
710 if (UnparseC.term t', UnparseC.terms asm) = ("x \<up> 2 / y \<up> 2", "[\"y \<up> 2 \<noteq> 0\"]")
711 then () else error "rational.sml cancel_p Schalk 192b";
713 val t = TermC.str2term "((x \<up> 2)*(7 * x + (-1) * y))/((y \<up> 2)*(7 * x + (-1) * y))";
714 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
715 if (UnparseC.term t', UnparseC.terms asm) =
716 ("(7 * x \<up> 3 + - 1 * x \<up> 2 * y) /\n(7 * x * y \<up> 2 + - 1 * y \<up> 3)", "[]")
717 then () else error "rational.sml make_polynomial Schalk 192b";
719 val t = TermC.str2term "((x \<up> 2)*(7 * x + (-1) * y))/((y \<up> 2)*(7 * x + (-1) * y))";
720 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
721 if (UnparseC.term t', UnparseC.terms asm) =
722 ("(7 * x \<up> 3 + - 1 * x \<up> 2 * y) /\n(7 * x * y \<up> 2 + - 1 * y \<up> 3)", "[]")
723 then () else error "rational.sml make_polynomial Schalk WN050929 not working";
725 "-------- example 193a";
726 val t = TermC.str2term "( x \<up> 2 + -6 * x + 9 ) / ( x \<up> 2 + -9 )";
727 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
728 if (UnparseC.term t', UnparseC.terms asm) = ("(- 3 + x) / (3 + x)", "[\"3 + x \<noteq> 0\"]")
729 then () else error "rational.sml cancel_p Schalk 193a";
731 "-------- example 193b";
732 val t = TermC.str2term "( x \<up> 2 + -8 * x + 16 ) / ( 2 * x \<up> 2 + -32 )";
733 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
734 if (UnparseC.term t', UnparseC.terms asm) = ("(- 4 + x) / (8 + 2 * x)", "[\"8 + 2 * x \<noteq> 0\"]")
735 then () else error "rational.sml cancel_p Schalk 193b";
737 "-------- example 193c";
738 val t = TermC.str2term "( 2 * x + -50 * x \<up> 3 ) / ( 25 * x \<up> 2 + -10 * x + 1 )";
739 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
740 if (UnparseC.term t', UnparseC.terms asm) =
741 ("(2 * x + 10 * x \<up> 2) / (1 + - 5 * x)", "[\"1 + - 5 * x \<noteq> 0\"]")
742 then () else error "rational.sml cancel_p Schalk 193c";
744 (*WN: improved with new numerals*)
745 val t = TermC.str2term "(-25 + 9*x \<up> 2)/(5 + 3*x)";
746 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
747 if (UnparseC.term t', UnparseC.terms asm) = ("(- 5 + 3 * x) / 1", "[]")
748 then () else error "rational.sml cancel WN 1";
750 "-------- example heuberger";
751 val t = TermC.str2term ("(x \<up> 4 + x * y + x \<up> 3 * y + y \<up> 2) / " ^
752 "(x + 5 * x \<up> 2 + y + 5 * x * y + x \<up> 2 * y \<up> 3 + x * y \<up> 4)");
753 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
754 if (UnparseC.term t', UnparseC.terms asm) =
755 ("(x \<up> 3 + y) / (1 + 5 * x + x * y \<up> 3)", "[\"1 + 5 * x + x * y \<up> 3 \<noteq> 0\"]")
756 then () else error "rational.sml cancel_p heuberger";
758 "-------- rewrite_set_ add_fractions_p from: Mathematik 1 Schalk -------------";
759 "-------- rewrite_set_ add_fractions_p from: Mathematik 1 Schalk -------------";
760 "-------- rewrite_set_ add_fractions_p from: Mathematik 1 Schalk -------------";
761 (*deleted example 204 ... 236b at update Isabelle2012-->2013*)
763 "-------- integration lev.1 -- lev.5: cancel_p_ & add_fractions_p_ -----------";
764 "-------- integration lev.1 -- lev.5: cancel_p_ & add_fractions_p_ -----------";
765 "-------- integration lev.1 -- lev.5: cancel_p_ & add_fractions_p_ -----------";
766 val t = TermC.str2term ("123 = (a*x)/(b*x) + (c*x)/(d*x) + (e*x)/(f*x::real)");
767 "-------- gcd_poly integration level 1: works on exact term";
768 if NONE = cancel_p_ thy t then () else error "cancel_p_ works on exact fraction";
769 if NONE = add_fraction_p_ thy t then () else error "add_fraction_p_ works on exact fraction";
771 "-------- gcd_poly integration level 2: picks out ONE appropriate subterm";
772 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
773 if UnparseC.term t' = "123 = a * x / (b * x) + c * x / (d * x) + e / f"
774 then () else error "level 2, rewrite_set_ cancel_p: changed";
775 val SOME (t', asm) = rewrite_set_ thy false add_fractions_p t;
776 if UnparseC.term t' = "123 = (b * c * x + a * d * x) / (b * d * x) + e * x / (f * x)"
777 then () else error "level 2, rewrite_set_ add_fractions_p: changed";
779 "-------- gcd_poly integration level 3: rewrites all appropriate subterms";
780 val SOME (t', asm) = rewrite_set_ thy false cancel_p_rls t;
781 if UnparseC.term t' = "123 = a / b + c / d + e / f"
782 then () else error "level 3, rewrite_set_ cancel_p_rls: changed";
783 val SOME (t', asm) = rewrite_set_ thy false add_fractions_p_rls t; (*CREATE add_fractions_p_rls*)
784 if UnparseC.term t' = "123 = (b * d * e * x + b * c * f * x + a * d * f * x) / (b * d * f * x)"
785 then () else error "level 3, rewrite_set_ add_fractions_p_rls: changed";
787 "-------- gcd_poly integration level 4: iteration cancel_p -- add_fraction_p";
788 (* simpler variant *)
789 val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty [Rls_ cancel_p, Rls_ add_fractions_p]
790 val SOME (t', asm) = rewrite_set_ thy false testrls t;
791 (*Rewrite.trace_on := false;
792 # rls: testrls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
793 ## rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
794 ## rls: add_fractions_p on: 123 = a * x / (b * x) + c * x / (d * x) + e / f
795 ## rls: cancel_p on: 123 = (b * c * x + a * d * x) / (b * d * x) + e / f
796 ## rls: add_fractions_p on: 123 = (b * c + a * d) / (b * d) + e / f
797 ## rls: cancel_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
798 ## rls: add_fractions_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) *)
799 if UnparseC.term t' = "123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)"
800 then () else error "level 4, rewrite_set_ *_p: changed";
802 (* complicated variant *)
803 val testrls_rls = Rule_Set.append_rules "testrls_rls" Rule_Set.empty [Rls_ cancel_p_rls, Rls_ add_fractions_p_rls];
804 val SOME (t', asm) = rewrite_set_ thy false testrls_rls t;
805 (*# rls: testrls_rls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
806 ## rls: cancel_p_rls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
807 ### rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
808 ### rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e / f
809 ### rls: cancel_p on: 123 = a * x / (b * x) + c / d + e / f
810 ### rls: cancel_p on: 123 = a / b + c / d + e / f
811 ## rls: add_fractions_p_rls on: 123 = a / b + c / d + e / f
812 ### rls: add_fractions_p on: 123 = a / b + c / d + e / f
813 ### rls: add_fractions_p on: 123 = (b * c + a * d) / (b * d) + e / f
814 ### rls: add_fractions_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
815 ## rls: cancel_p_rls on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
816 ### rls: cancel_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
817 ## rls: add_fractions_p_rls on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
818 ### rls: add_fractions_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) *)
819 if UnparseC.term t' = "123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)"
820 then () else error "level 4, rewrite_set_ *_p_rls: changed"
822 "-------- gcd_poly integration level 5: cancel_p & add_fraction_p within norm_Rational";
823 val SOME (t', asm) = rewrite_set_ thy false norm_Rational t;
824 if UnparseC.term t' = "123 = (a * d * f + b * c * f + b * d * e) / (b * d * f)"
825 then () else error "level 5, rewrite_set_ norm_Rational: changed"
827 "-------- reverse rewrite ----------------------------------------------------";
828 "-------- reverse rewrite ----------------------------------------------------";
829 "-------- reverse rewrite ----------------------------------------------------";
830 (** the term for which reverse rewriting is demonstrated **)
831 val t = TermC.str2term "(9 + -1 * x \<up> 2) / (9 + 6 * x + x \<up> 2)";
832 val Rrls {scr = Rfuns {init_state = ini, locate_rule = loc,
833 next_rule = nex, normal_form = nor, ...},...} = cancel_p;
835 (** normal_form produces the result in ONE step **)
836 val SOME (t', _) = nor t;
837 if UnparseC.term t' = "(3 + - 1 * x) / (3 + x)" then ()
838 else error "rational.sml normal_form (9 - x \<up> 2) / (9 - 6 * x + x \<up> 2)";
840 (** initialize the interpreter state used by the 'me' **)
841 val (t, _, revsets, _) = ini t;
843 if length (hd revsets) = 11 then () else error "length of revset changed";
844 (*//----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)
845 if (revsets |> nth 1 |> nth 1 |> id_of_thm) =
846 (@{thm realpow_twoI} |> Thm.get_name_hint |> ThmC.cut_id)
847 then () else error "first element of revset changed";
849 (revsets |> nth 1 |> nth 1 |> Rule.to_string) = "Thm (\"realpow_twoI\",?r1 \<up> 2 = ?r1 * ?r1)" andalso
850 (revsets |> nth 1 |> nth 2 |> Rule.to_string) = "Thm (\"#: 9 = 3 \<up> 2\",9 = 3 \<up> 2)" andalso
851 (revsets |> nth 1 |> nth 3 |> Rule.to_string) = "Thm (\"#: 6 * x = 2 * (3 * x)\",6 * x = 2 * (3 * x))"
853 (revsets |> nth 1 |> nth 4 |> Rule.to_string) = "Thm (\"#: -3 * x = -1 * (3 * x)\",-3 * x = -1 * (3 * x))"
855 (revsets |> nth 1 |> nth 5 |> Rule.to_string) = "Thm (\"#: 9 = 3 * 3\",9 = 3 * 3)" andalso
856 (revsets |> nth 1 |> nth 6 |> Rule.to_string) = "Rls_ (\"sym_order_mult_rls_\")" andalso
857 (revsets |> nth 1 |> nth 7 |> Rule.to_string) =
858 "Thm (\"sym_mult.assoc\",?a * (?b * ?c) = ?a * ?b * ?c)"
859 then () else error "first 7 elements in revset changed"
860 \\----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)*)
862 (** find the rule 'r' to apply to term 't' **)
863 (*/------- WN1309: since cancel_ (accepted "-" between monomials) has been replaced by cancel_p_
864 for Isabelle2013, we don't get a working revset, but non-termination:
866 val SOME (r as (Thm (str, thm))) = nex revsets t;
868 ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x),
869 Rls_ ("sym_order_mult_rls_"), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x), []))", "
870 ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x),
871 Thm ("sym_mult.assoc", ""), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * 3 * x + x * x), []))", "
872 ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * 3 * x + x * x),
873 Thm ("sym_mult.assoc", ""), ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x), []))", "
874 ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x), Rls_ ("sym_order_mult_rls_"), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x), []))", "
877 Thm ("sym_#mult_2_3", "6 = 2 * 3")
878 ### Isabelle2009-2 for cancel_ (not cancel_p_):
879 if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))"
880 andalso ThmC.string_of_thm thm =
881 (string_of_thm (Thm.make_thm @{theory "Isac_Knowledge"}
882 (Trueprop $ (Thm.term_of o the o (TermC.parse thy)) "9 = 3 \<up> 2"))) then ()
883 else error "rational.sml next_rule (9 - x \<up> 2) / (9 - 6 * x + x \<up> 2)";
884 \---------------------------------------------------------------------------------------/*)
886 (** check, if the rule 'r' applied by the user to 't' belongs to the ruleset;
887 if the rule is OK, the term resulting from applying the rule is returned,too;
888 there might be several rule applications inbetween,
889 which are listed after the head in reverse order **)
890 (*/-------------------------------------------- Isabelle2013: this gives "error id_of_thm";
891 we don't repair this, because interaction within "reverse rewriting" never worked properly:
893 val (r, (t, asm))::_ = loc revsets t r;
894 if UnparseC.term t = "(9 - x \<up> 2) / (3 \<up> 2 + 6 * x + x \<up> 2)" andalso asm = []
895 then () else error "rational.sml locate_rule (9 - x \<up> 2) / (9 - 6 * x + x \<up> 2)";
897 (* find the next rule to apply *)
898 val SOME (r as (Thm (str, thm))) = nex revsets t;
899 if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))" andalso
900 ThmC.string_of_thm thm = (string_of_thm (ThmC_Def.make_thm @{theory "Isac_Knowledge"}
901 (Trueprop $ (Thm.term_of o the o (TermC.parse thy)) "9 = 3 \<up> 2"))) then ()
902 else error "rational.sml next_rule (9 - x \<up> 2) / (9 - 6 * x + x \<up> 2)";
904 (*check the next rule*)
905 val (r, (t, asm)) :: _ = loc revsets t r;
906 if UnparseC.term t = "(3 \<up> 2 - x \<up> 2) / (3 \<up> 2 + 6 * x + x \<up> 2)" then ()
907 else error "rational.sml locate_rule (9 - x \<up> 2) / (9 - 6 * x + x \<up> 2) II";
909 (*find and check the next rules, rewrite*)
910 val SOME r = nex revsets t;
911 val (r,(t,asm))::_ = loc revsets t r;
912 if UnparseC.term t = "(3 \<up> 2 - x \<up> 2) / (3 \<up> 2 + 2 * 3 * x + x \<up> 2)" then ()
913 else error "rational.sml locate_rule II";
915 val SOME r = nex revsets t;
916 val (r,(t,asm))::_ = loc revsets t r;
917 if UnparseC.term t = "(3 - x) * (3 + x) / (3 \<up> 2 + 2 * 3 * x + x \<up> 2)" then ()
918 else error "rational.sml next_rule II";
920 val SOME r = nex revsets t;
921 val (r,(t,asm))::_ = loc revsets t r;
922 if UnparseC.term t = "(3 - x) * (3 + x) / ((3 + x) * (3 + x))" then ()
923 else error "rational.sml next_rule III";
925 val SOME r = nex revsets t;
926 val (r, (t, asm)) :: _ = loc revsets t r;
927 val ss = UnparseC.term t;
928 if ss = "(3 - x) / (3 + x)" andalso UnparseC.terms asm = "[\"3 + x ~= 0\"]" then ()
929 else error "rational.sml: new behav. in rev-set cancel";
930 \--------------------------------------------------------------------------------------/*)
932 "-------- 'reverse-ruleset' cancel_p -----------------------------------------";
933 "-------- 'reverse-ruleset' cancel_p -----------------------------------------";
934 "-------- 'reverse-ruleset' cancel_p -----------------------------------------";
935 (*WN130909: the example below shows, why "reverse rewriting" only worked for
938 (*the term for which reverse rewriting is demonstrated*)
939 val t = TermC.str2term "(9 + (-1)*x \<up> 2) / (9 + ((-6)*x + x \<up> 2))";
940 val Rrls {scr=Rfuns {init_state=ini,locate_rule=loc,
941 next_rule=nex,normal_form=nor,...},...} = cancel_p;
943 (*normal_form produces the result in ONE step*)
944 val SOME (t', _) = nor t;
945 if UnparseC.term t' = "(3 + x) / (3 + - 1 * x)"
946 then () else error "cancel_p normal_form CHANGED";;
948 (*initialize the interpreter state used by the 'me'*)
949 val SOME (t', asm) = cancel_p_ thy t;
950 if (UnparseC.term t', UnparseC.terms asm) = ("(3 + x) / (3 + - 1 * x)", "[\"3 + - 1 * x \<noteq> 0\"]")
951 then () else error "cancel_p CHANGED";;
953 val (t,_,revsets,_) = ini t;
955 (* WN.10.10.02: dieser Fall terminiert nicht
956 (make_polynomial enth"alt zu viele rules)
957 WN060823 'init_state' requires rewriting on specified location in the term
958 default_print_depth 99; Rfuns; default_print_depth 3;
959 WN060831 cycling "sym_order_mult_rls_" "sym_mult.assoc"
960 as was with make_polynomial before ?!?* )
962 val SOME r = nex revsets t;
963 eq_Thm (r, Thm ("sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))",
964 mk_thm thy "9 = 3 \<up> 2"));
965 ( *WN060831 *** id_of_thm
966 Exception- ERROR raised ...
967 val (r,(t,asm))::_ = loc revsets t r;
970 val SOME r = nex revsets t;
971 val (r,(t,asm))::_ = loc revsets t r;
975 "-------- examples: rls norm_Rational ----------------------------------------";
976 "-------- examples: rls norm_Rational ----------------------------------------";
977 "-------- examples: rls norm_Rational ----------------------------------------";
978 val t = TermC.str2term "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0";
979 val SOME (t', _) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
980 if UnparseC.term t' = "1 / 18 = 0" then () else error "rational.sml 1";
982 val t = TermC.str2term "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";
983 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
984 if UnparseC.term t' = "(237 + 65 * x) / 36 = 0" then ()
985 else error "rational.sml 2";
987 val t = TermC.str2term "(1/2 + (5*x)/2) \<up> 2 - ((13*x)/2 - 5/2) \<up> 2 - (6*x) \<up> 2 + 29";
988 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
989 if UnparseC.term t' = "23 + 35 * x + - 72 * x \<up> 2" then ()
990 else error "rational.sml 3";
992 (*Rewrite.trace_on:=true;*)
993 val t = TermC.str2term "Not (6*x is_atom)";
994 val SOME (t',_) = rewrite_set_ thy false powers_erls t; UnparseC.term t';
996 val t = TermC.str2term "1 < 2";
997 val SOME (t',_) = rewrite_set_ thy false powers_erls t; UnparseC.term t';
1000 val t = TermC.str2term "(6*x) \<up> 2";
1001 val SOME (t',_) = rewrite_ thy dummy_ord powers_erls false
1002 (ThmC.numerals_to_Free @{thm realpow_def_atom}) t;
1003 if UnparseC.term t' = "6 * x * (6 * x) \<up> (2 + - 1)" then ()
1004 else error "rational.sml powers_erls (6*x) \<up> 2";
1006 val t = TermC.str2term "-1 * (-2 * (5 / 2 * (13 * x / 2)))";
1007 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
1008 if UnparseC.term t' = "65 * x / 2" then () else error "rational.sml 4";
1010 val t = TermC.str2term "1 - ((13*x)/2 - 5/2) \<up> 2";
1011 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
1012 if UnparseC.term t' = "(- 21 + 130 * x + - 169 * x \<up> 2) / 4" then ()
1013 else error "rational.sml 5";
1015 (*SRAM Schalk I, p.92 Nr. 609a*)
1016 val t = TermC.str2term "2*(3 - x/5)/3 - 4*(1 - x/3) - x/3 - 2*(x/2 - 1/4)/27 +5/54";
1017 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
1018 if UnparseC.term t' = "(- 255 + 112 * x) / 135" then ()
1019 else error "rational.sml 6";
1021 (*SRAM Schalk I, p.92 Nr. 610c*)
1022 val t = TermC.str2term "((x- 1)/(x+1) + 1) / ((x- 1)/(x+1) - (x+1)/(x- 1)) - 2";
1023 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
1024 if UnparseC.term t' = "(3 + x) / - 2" then () else error "rational.sml 7";
1026 (*SRAM Schalk I, p.92 Nr. 476a*)
1027 val t = TermC.str2term "(x \<up> 2/(1 - x \<up> 2) + 1)/(x/(1 - x) + 1) * (1 + x)";
1028 (*. a/b : c/d translated to a/b * d/c .*)
1029 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
1030 if UnparseC.term t' = "1" then () else error "rational.sml 8";
1032 (*Schalk I, p.92 Nr. 472a*)
1033 val t = TermC.str2term "((8*x \<up> 2 - 32*y \<up> 2)/(2*x + 4*y))/((4*x - 8*y)/(x + y))";
1034 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
1035 if UnparseC.term t' = "x + y" then () else error "rational.sml p.92 Nr. 472a";
1037 (*Schalk I, p.70 Nr. 480b: SEE rational.sml --- nonterminating rls norm_Rational ---*)
1039 (*WN130910 add_fractions_p exception Div raised + history:
1040 ### WN.2.6.03 from rlang.sml 56a
1041 val t = TermC.str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x) = 4 * (a * b) / (a \<up> 2 + -1 * b \<up> 2)";
1042 val NONE = rewrite_set_ thy false add_fractions_p t;
1044 THE ERROR ALREADY OCCURS IN THIS PART:
1045 val t = TermC.str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)";
1046 val NONE = add_fraction_p_ thy t;
1048 SEE Test_Some.thy: section {* add_fractions_p downto exception Div raised ===
1051 "-------- rational numerals --------------------------------------------------";
1052 "-------- rational numerals --------------------------------------------------";
1053 "-------- rational numerals --------------------------------------------------";
1054 (*SRA Schalk I, p.40 Nr. 164b *)
1055 val t = TermC.str2term "(47/6 - 76/9 + 13/4)/(35/12)";
1056 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1057 if UnparseC.term t = "19 / 21" then ()
1058 else error "rational.sml: diff.behav. in norm_Rational_mg 1";
1060 (*SRA Schalk I, p.40 Nr. 166a *)
1061 val t = TermC.str2term "((5/4)/(4+22/7) + 37/20)*(110/3 - 110/9 * 23/11)";
1062 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1063 if UnparseC.term t = "45 / 2" then ()
1064 else error "rational.sml: diff.behav. in norm_Rational_mg 2";
1066 "-------- examples cancellation from: Mathematik 1 Schalk --------------------";
1067 "-------- examples cancellation from: Mathematik 1 Schalk --------------------";
1068 "-------- examples cancellation from: Mathematik 1 Schalk --------------------";
1069 (* e190c Stefan K.*)
1070 val t = TermC.str2term "((1 + 9*a \<up> 2) * (1 + 3*a)) / ((3*a + 9*a \<up> 2) * (1 + 3*a))";
1071 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1072 if UnparseC.term t = "(1 + 9 * a \<up> 2) / (3 * a + 9 * a \<up> 2)"
1073 then () else error "rational.sml: diff.behav. in norm_Rational_mg 3";
1075 (* e192b Stefan K.*)
1076 val t = TermC.str2term "(x \<up> 2 * (7*x + (-1)*y)) / (y \<up> 2 * (7*x + (-1)*y))";
1077 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1078 if UnparseC.term t = "x \<up> 2 / y \<up> 2"
1079 then () else error "rational.sml: diff.behav. in norm_Rational_mg 4";
1081 (*SRC Schalk I, p.66 Nr. 379c *)
1082 val t = TermC.str2term "(a - b)/(b - a)";
1083 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1084 if UnparseC.term t = "- 1"
1085 then () else error "rational.sml: diff.behav. in norm_Rational_mg 5";
1087 (*SRC Schalk I, p.66 Nr. 380b *)
1088 val t = TermC.str2term "15*(3*x + 3) * (4*x + 9) / (12*(2*x + 7) * (5*x + 5))";
1089 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1090 if UnparseC.term t = "(27 + 12 * x) / (28 + 8 * x)"
1091 then () else error "rational.sml: diff.behav. in norm_Rational_mg 6";
1093 (*Schalk I, p.60 Nr. 215c *)
1094 val t = TermC.str2term "(a + b) \<up> 4 * (x - y) / ((x - y) \<up> 3 * (a + b) \<up> 2)";
1095 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1096 if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + - 2 * x * y + y \<up> 2)"
1097 then () else error "rational.sml: diff.behav. in norm_Rational_mg 7";
1099 (*SRC Schalk I, p.66 Nr. 381b *)
1100 val t = TermC.str2term
1101 "(4*x \<up> 2 - 20*x + 25)/(2*x - 5) \<up> 3";
1102 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1103 if UnparseC.term t = "1 / (- 5 + 2 * x)"
1104 then () else error "rational.sml: diff.behav. in norm_Rational_mg 9";
1106 (* e190c Stefan K.*)
1107 val t = TermC.str2term "((1 + 9*a \<up> 2) * (1 + 3*a)) / ((3*a + 9*a \<up> 2) * (1 + 3 * a))";
1108 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1109 if UnparseC.term t = "(1 + 9 * a \<up> 2) / (3 * a + 9 * a \<up> 2)"
1110 then () else error "rational.sml: diff.behav. in norm_Rational_mg 3";
1112 (* e192b Stefan K.*)
1113 val t = TermC.str2term "(x \<up> 2 * (7*x + (-1)*y)) / (y \<up> 2 * (7*x + (-1)*y))";
1114 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1115 if UnparseC.term t = "x \<up> 2 / y \<up> 2"
1116 then () else error "rational.sml: diff.behav. in norm_Rational_mg 4";
1118 (*SRC Schalk I, p.66 Nr. 379c *)
1119 val t = TermC.str2term "(a - b) / (b - a)";
1120 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1121 if UnparseC.term t = "- 1"
1122 then () else error "rational.sml: diff.behav. in norm_Rational_mg 5";
1124 (*SRC Schalk I, p.66 Nr. 380b *)
1125 val t = TermC.str2term "15*(3*x + 3) * (4*x + 9) / (12*(2*x + 7) * (5*x + 5))";
1126 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1127 if UnparseC.term t = "(27 + 12 * x) / (28 + 8 * x)"
1128 then () else error "rational.sml: diff.behav. in norm_Rational_mg 6";
1130 (*Schalk I, p.60 Nr. 215c *)
1131 val t = TermC.str2term "(a + b) \<up> 4 * (x - y) / ((x - y) \<up> 3 * (a + b) \<up> 2)";
1132 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1133 if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + - 2 * x * y + y \<up> 2)"
1134 then () else error "Schalk I, p.60 Nr. 215c: with Isabelle2002 cancellation incomplete, changed";
1136 (* extreme example from somewhere *)
1137 val t = TermC.str2term
1138 ("(a \<up> 4 * x + -1*a \<up> 4 * y + 4*a \<up> 3 * b * x + -4*a \<up> 3 * b * y + " ^
1139 "6*a \<up> 2 * b \<up> 2 * x + -6*a \<up> 2 * b \<up> 2 * y + 4*a * b \<up> 3 * x + -4*a * b \<up> 3 * y + " ^
1140 "b \<up> 4 * x + -1*b \<up> 4 * y) " ^
1141 " / (a \<up> 2 * x \<up> 3 + -3*a \<up> 2 * x \<up> 2 * y + 3*a \<up> 2 * x * y \<up> 2 + -1*a \<up> 2 * y \<up> 3 + " ^
1142 "2*a * b * x \<up> 3 + -6*a * b * x \<up> 2 * y + 6*a * b * x * y \<up> 2 + -2*a * b * y \<up> 3 + " ^
1143 "b \<up> 2 * x \<up> 3 + -3*b \<up> 2 * x \<up> 2 * y + 3*b \<up> 2 * x * y \<up> 2 + -1*b \<up> 2 * y \<up> 3)")
1144 val SOME (t, _) = rewrite_set_ thy false cancel_p t;
1145 if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + - 2 * x * y + y \<up> 2)"
1146 then () else error "with Isabelle2002: NONE -- now SOME changed";
1148 (*Schalk I, p.66 Nr. 381a *)
1149 (* ATTENTION: here the rls is very slow. In Isabelle2002 this required 2 min *)
1150 val t = TermC.str2term "18*(a + b) \<up> 3 * (a - b) \<up> 2 / (72*(a - b) \<up> 3 * (a + b) \<up> 2)";
1151 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1152 if UnparseC.term t = "(a + b) / (4 * a + - 4 * b)"
1153 then () else error "rational.sml: diff.behav. in norm_Rational_mg 8";
1155 (*SRC Schalk I, p.66 Nr. 381b *)
1156 val t = TermC.str2term "(4*x \<up> 2 - 20*x + 25) / (2*x - 5) \<up> 3";
1157 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1158 if UnparseC.term t = "1 / (- 5 + 2 * x)"
1159 then () else error "rational.sml: diff.behav. in norm_Rational_mg 9";
1161 (*SRC Schalk I, p.66 Nr. 381c *)
1162 val t = TermC.str2term "(27*a \<up> 3 + 9*a \<up> 2+3*a+1) / (27*a \<up> 3 + 18*a \<up> 2+3*a)";
1163 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1164 if UnparseC.term t = "(1 + 9 * a \<up> 2) / (3 * a + 9 * a \<up> 2)"
1165 then () else error "rational.sml: diff.behav. in norm_Rational_mg 10";
1167 (*SRC Schalk I, p.66 Nr. 383a *)
1168 val t = TermC.str2term "(5*a \<up> 2 - 5*a*b) / (a - b) \<up> 2";
1169 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1170 if UnparseC.term t = "- 5 * a / (- 1 * a + b)"
1171 then () else error "rational.sml: diff.behav. in norm_Rational_mg 11";
1173 "----- NOT TERMINATING ?: worked before 0707xx";
1174 val t = TermC.str2term "(a \<up> 2 - 1)*(b + 1) / ((b \<up> 2 - 1)*(a+1))";
1175 (* WN130911 "exception Div raised" by
1176 cancel_p_ thy (TermC.str2term ("(-1 + -1 * b + a \<up> 2 + a \<up> 2 * b) /" ^
1177 "(-1 + -1 * a + b \<up> 2 + a * b \<up> 2)"))
1179 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1180 if UnparseC.term t = "(1 + -1 * a) / (1 + -1 * b)" then ()
1181 else error "rational.sml MG tests 3e";
1184 "-------- examples common denominator from: Mathematik 1 Schalk --------------";
1185 "-------- examples common denominator from: Mathematik 1 Schalk --------------";
1186 "-------- examples common denominator from: Mathematik 1 Schalk --------------";
1187 (*SRA Schalk I, p.67 Nr. 403a *)
1188 val t = TermC.str2term "4/x - 3/y - 1";
1189 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1190 if UnparseC.term t = "(- 3 * x + 4 * y + - 1 * x * y) / (x * y)"
1191 then () else error "rational.sml: diff.behav. in norm_Rational_mg 12";
1193 val t = TermC.str2term "(2*a+3*b)/(b*c) + (3*c+a)/(a*c) - (2*a \<up> 2+3*b*c)/(a*b*c)";
1194 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1195 if UnparseC.term t = "4 / c"
1196 then () else error "rational.sml: diff.behav. in norm_Rational_mg 13";
1198 (*SRA Schalk I, p.67 Nr. 410b *)
1199 val t = TermC.str2term "1/(x+1) + 1/(x+2) - 2/(x+3)";
1200 (* WN130911 non-termination due to non-termination of
1201 cancel_p_ thy (TermC.str2term "(5 + 3 * x) / (6 + 11 * x + 6 * x \<up> 2 + x \<up> 3)")
1203 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1204 if UnparseC.term t = "(5 + 3 * x) / (6 + 11 * x + 6 * x \<up> 2 + x \<up> 3)"
1205 then () else error "rational.sml: diff.behav. in norm_Rational_mg 14";
1208 (*SRA Schalk I, p.67 Nr. 413b *)
1209 val t = TermC.str2term "(1 + x)/(1 - x) - (1 - x)/(1 + x) + 2*x/(1 - x \<up> 2)";
1210 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1211 if UnparseC.term t = "6 * x / (1 + - 1 * x \<up> 2)"
1212 then () else error "rational.sml: diff.behav. in norm_Rational_mg 15";
1214 (*SRA Schalk I, p.68 Nr. 414a *)
1215 val t = TermC.str2term "(x + 2)/(x - 1) + (x - 3)/(x - 2) - (x + 1)/((x - 1)*(x - 2))";
1216 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1217 if UnparseC.term t ="(- 2 + - 5 * x + 2 * x \<up> 2) / (2 + - 3 * x + x \<up> 2)"
1218 then () else error "rational.sml: diff.behav. in norm_Rational_mg 16";
1220 (*SRA Schalk I, p.68 Nr. 428b *)
1221 val t = TermC.str2term
1222 "1/(a - b) \<up> 2 + 1/(a + b) \<up> 2 - 2/(a \<up> 2 - b \<up> 2) - 4*(b \<up> 2 - 1)/(a \<up> 2 - b \<up> 2) \<up> 2";
1223 (* WN130911 non-termination due to non-termination of
1224 cancel_p_ thy (TermC.str2term "(4 + -4 * b \<up> 2) / (a \<up> 4 + -2 * (a \<up> 2 * b \<up> 2) + b \<up> 4)")
1226 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1227 if UnparseC.term t = "4 / (a \<up> 4 + -2 * a \<up> 2 * b \<up> 2 + b \<up> 4)"
1228 then () else error "rational.sml: diff.behav. in norm_Rational_mg 18";
1231 (*SRA Schalk I, p.68 Nr. 430b *)
1232 val t = TermC.str2term
1233 "a \<up> 2/(a - 3*b) - 108*a*b \<up> 3/((a+3*b)*(a \<up> 2 - 9*b \<up> 2)) - 9*b \<up> 2*(a - 3*b)/(a+3*b) \<up> 2";
1234 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1235 if UnparseC.term t = "a + 3 * b"
1236 then () else error "rational.sml: diff.behav. in norm_Rational_mg 19";
1238 (*SRA Schalk I, p.68 Nr. 432 *)
1239 val t = TermC.str2term
1240 ("(a \<up> 2 + a*b) / (a \<up> 2 - b \<up> 2) - (b \<up> 2 - a*b) / (b \<up> 2 - a \<up> 2) + " ^
1241 "a \<up> 2*(a - b) / (a \<up> 3 - a \<up> 2*b) - 2*a*(a \<up> 2 - b \<up> 2) / (a \<up> 3 - a*b \<up> 2) - " ^
1242 "2*b \<up> 2 / (a \<up> 2 - b \<up> 2)");
1243 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1244 if UnparseC.term t = (*"0" ..isabisac15 | Isabelle2017..*) "0 / (a \<up> 2 + - 1 * b \<up> 2)"
1245 then () else error "rational.sml: diff.behav. in norm_Rational_mg 20";
1248 val t = TermC.str2term "3*a / (a*b) + x/y";
1249 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1250 if UnparseC.term t = "(3 * y + b * x) / (b * y)"
1251 then () else error "rational.sml: diff.behav. in norm_Rational_mg 21";
1254 "-------- examples multiply and cancel from: Mathematik 1 Schalk -------------";
1255 "-------- examples multiply and cancel from: Mathematik 1 Schalk -------------";
1256 "-------- examples multiply and cancel from: Mathematik 1 Schalk -------------";
1257 (*------- SRM Schalk I, p.68 Nr. 436a *)
1258 val t = TermC.str2term "3*(x+y) / (15*(x - y)) * 25*(x - y) \<up> 2 / (18*(x + y) \<up> 2)";
1259 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1260 if UnparseC.term t = "(- 5 * x + 5 * y) / (- 18 * x + - 18 * y)"
1261 then () else error "rational.sml: diff.behav. in norm_Rational_mg 22";
1263 (*------- SRM.test Schalk I, p.68 Nr. 436b *)
1264 val t = TermC.str2term "5*a*(a - b) \<up> 2*(a + b) \<up> 3/(7*b*(a - b) \<up> 3) * 7*b/(a + b) \<up> 3";
1265 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1266 if UnparseC.term t = "5 * a / (a + - 1 * b)"
1267 then () else error "rational.sml: diff.behav. in norm_Rational_mg 23";
1269 (*------- Schalk I, p.68 Nr. 437a *)
1270 val t = TermC.str2term "(3*a - 4*b) / (4*c+3*e) * (3*a+4*b)/(9*a \<up> 2 - 16*b \<up> 2)";
1271 (* raises an exception for unclear reasons:
1272 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1274 ### rls: cancel_p on: (9 * a \<up> 2 + -16 * b \<up> 2) / (4 * c + 3 * e) /
1275 (9 * a \<up> 2 + -16 * b \<up> 2)
1276 exception Div raised
1279 val t = TermC.str2term
1280 ("(9 * a \<up> 2 + -16 * b \<up> 2) / (4 * c + 3 * e) /" ^
1281 "(9 * a \<up> 2 + -16 * b \<up> 2)");
1282 NONE = cancel_p_ thy t;
1284 if UnparseC.term t = "1 / (4 * c + 3 * e)" then ()
1285 else error "rational.sml: diff.behav. in norm_Rational_mg 24";
1288 "----- S.K. corrected non-termination 060904";
1289 val t = TermC.str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a \<up> 2 - 16*b \<up> 2))";
1290 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
1291 if UnparseC.term t =
1292 "(9 * a \<up> 2 + - 16 * b \<up> 2) /\n(36 * a \<up> 2 * c + 27 * a \<up> 2 * e + - 64 * b \<up> 2 * c +\n - 48 * b \<up> 2 * e)"
1293 then () else error "rational.sml: S.K.8..corrected 060904-6";
1295 "----- S.K. corrected non-termination of cancel_p_";
1296 val t'' = TermC.str2term ("(9 * a \<up> 2 + -16 * b \<up> 2) /" ^
1297 "(36 * a \<up> 2 * c + (27 * a \<up> 2 * e + (-64 * b \<up> 2 * c + -48 * b \<up> 2 * e)))");
1298 (* /--- DOES NOT TERMINATE AT TRANSITION isabisac15 --> Isabelle2017 --------------------------\
1299 val SOME (t',_) = rewrite_set_ thy false cancel_p t'';
1300 if UnparseC.term t' = "1 / (4 * c + 3 * e)"
1301 then () else error "rational.sml: diff.behav. in cancel_p S.K.8";
1302 \--- DOES NOT TERMINATE AT TRANSITION isabisac15 --> Isabelle2017 --------------------------/*)
1304 (*------- Schalk I, p.68 Nr. 437b*)
1305 val t = TermC.str2term "(a + b)/(x \<up> 2 - y \<up> 2) * ((x - y) \<up> 2/(a \<up> 2 - b \<up> 2))";
1306 (*val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1308 #### rls: cancel_p on: (a * x \<up> 2 + -2 * (a * (x * y)) + a * y \<up> 2 + b * x \<up> 2 +
1309 -2 * (b * (x * y)) +
1311 (a \<up> 2 * x \<up> 2 + -1 * (a \<up> 2 * y \<up> 2) + -1 * (b \<up> 2 * x \<up> 2) +
1312 b \<up> 2 * y \<up> 2)
1313 exception Div raised
1316 (*------- SRM Schalk I, p.68 Nr. 438a *)
1317 val t = TermC.str2term "x*y / (x*y - y \<up> 2) * (x \<up> 2 - x*y)";
1318 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1319 if UnparseC.term t = "x \<up> 2"
1320 then () else error "rational.sml: diff.behav. in norm_Rational_mg 24";
1322 (*------- SRM Schalk I, p.68 Nr. 439b *)
1323 val t = TermC.str2term "(4*x \<up> 2 + 4*x + 1) * ((x \<up> 2 - 2*x \<up> 3) / (4*x \<up> 2 + 2*x))";
1324 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1325 if UnparseC.term t = "(x + - 4 * x \<up> 3) / 2"
1326 then () else error "rational.sml: diff.behav. in norm_Rational_mg 25";
1328 (*------- SRM Schalk I, p.68 Nr. 440a *)
1329 val t = TermC.str2term "(x \<up> 2 - 2*x) / (x \<up> 2 - 3*x) * (x - 3) \<up> 2 / (x \<up> 2 - 4)";
1330 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1331 if UnparseC.term t = "(- 3 + x) / (2 + x)"
1332 then () else error "rational.sml: diff.behav. in norm_Rational_mg 26";
1334 "----- Schalk I, p.68 Nr. 440b SK11 works since 0707xx";
1335 val t = TermC.str2term "(a \<up> 3 - 9*a) / (a \<up> 3*b - a*b \<up> 3) * (a \<up> 2*b + a*b \<up> 2) / (a+3)";
1336 (* WN130911 non-termination for unclear reasons:
1337 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1339 ... ENDS WITH THIS TRACE:
1341 ### rls: cancel_p on: (-9 * (a \<up> 3 * b) + -9 * (a \<up> 2 * b \<up> 2) + a \<up> 5 * b +
1342 a \<up> 4 * b \<up> 2) /
1343 (a \<up> 3 * b + -1 * (a * b \<up> 3)) /
1345 BUT THIS IS CORRECTLY RECOGNISED
1346 val t = TermC.str2term
1347 ("(-9 * (a \<up> 3 * b) + -9 * (a \<up> 2 * b \<up> 2) + a \<up> 5 * b + a \<up> 4 * b \<up> 2) /" ^
1348 "(a \<up> 3 * b + -1 * (a * b \<up> 3)) / (3 + (a::real))");
1350 NONE = cancel_p_ thy t;
1352 if UnparseC.term t = "(-3 * a + a \<up> 2) / (a + -1 * b)" then ()
1353 else error "rational.sml: diff.behav. in norm_Rational 27";
1356 "----- SK12 works since 0707xx";
1357 val t = TermC.str2term "(a \<up> 3 - 9*a) * (a \<up> 2*b+a*b \<up> 2) / ((a \<up> 3*b - a*b \<up> 3) * (a+3))";
1358 (* WN130911 non-termination due to non-termination of
1359 cancel_p_ thy (TermC.str2term "(4 + -4 * b \<up> 2) / (a \<up> 4 + -2 * (a \<up> 2 * b \<up> 2) + b \<up> 4)")
1361 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1362 if UnparseC.term t' = "(-3 * a + a \<up> 2) / (a + -1 * b)" then ()
1363 else error "rational.sml: diff.behav. in norm_Rational 28";
1366 "-------- examples common denominator and multiplication from: Schalk --------";
1367 "-------- examples common denominator and multiplication from: Schalk --------";
1368 "-------- examples common denominator and multiplication from: Schalk --------";
1369 (*------- SRAM Schalk I, p.69 Nr. 441b *)
1370 val t = TermC.str2term "(4*a/3 + 3*b \<up> 2/a \<up> 3 + b/(4*a))*(4*b/(3*a))";
1371 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1372 if UnparseC.term t = "(36 * b \<up> 3 + 3 * a \<up> 2 * b \<up> 2 + 16 * a \<up> 4 * b) /\n(9 * a \<up> 4)"
1373 then () else error "rational.sml: diff.behav. in norm_Rational_mg 28";
1375 (*------- SRAM Schalk I, p.69 Nr. 442b *)
1376 val t = TermC.str2term ("(15*a \<up> 2/x \<up> 3 - 5*b \<up> 4/x \<up> 2 + 25*c \<up> 2/x) * " ^
1377 "(x \<up> 3/(5*a*b \<up> 3*c \<up> 3)) + 1/c \<up> 3 * (b*x/a - 3*a/b \<up> 3)");
1378 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1379 if UnparseC.term t = "5 * x \<up> 2 / (a * b \<up> 3 * c)"
1380 then () else error "rational.sml: diff.behav. in norm_Rational_mg 29";
1382 (*------- SRAM Schalk I, p.69 Nr. 443b *)
1383 val t = TermC.str2term "(a/2 + b/3) * (b/3 - a/2)";
1384 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1385 if UnparseC.term t = "(- 9 * a \<up> 2 + 4 * b \<up> 2) / 36"
1386 then () else error "rational.sml: diff.behav. in norm_Rational_mg 30";
1388 (*------- SRAM Schalk I, p.69 Nr. 445b *)
1389 val t = TermC.str2term "(a \<up> 2/9 + 2*a/(3*b) + 4/b \<up> 2)*(a/3 - 2/b) + 8/b \<up> 3";
1390 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1391 if UnparseC.term t = "a \<up> 3 / 27"
1392 then () else error "rational.sml: diff.behav. in norm_Rational_mg 31";
1394 (*------- SRAM Schalk I, p.69 Nr. 446b *)
1395 val t = TermC.str2term "(x/(5*x + 4*y) - y/(5*x - 4*y) + 1)*(25*x \<up> 2 - 16*y \<up> 2)";
1396 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1397 if UnparseC.term t = (*"30 * x \<up> 2 + -9 * x * y + -20 * y \<up> 2" ..isabisac15 | Isabelle2017..*)
1398 "(- 30 * x \<up> 2 + 9 * x * y + 20 * y \<up> 2) / - 1"
1399 then () else error "rational.sml: diff.behav. in norm_Rational_mg 32";
1401 (*------- SRAM Schalk I, p.69 Nr. 449a *)(*Achtung: rechnet ca 8 Sekunden*)
1402 val t = TermC.str2term
1403 "(2*x \<up> 2/(3*y)+x/y \<up> 2)*(4*x \<up> 4/(9*y \<up> 2)+x \<up> 2/y \<up> 4)*(2*x \<up> 2/(3*y) - x/y \<up> 2)";
1404 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1405 if UnparseC.term t = "(- 81 * x \<up> 4 + 16 * x \<up> 8 * y \<up> 4) / (81 * y \<up> 8)"
1406 then () else error "rational.sml: diff.behav. in norm_Rational_mg 33";
1408 (*------- SRAM Schalk I, p.69 Nr. 450a *)
1409 val t = TermC.str2term
1410 "(4*x/(3*y)+2*y/(3*x)) \<up> 2 - (2*y/(3*x) - 2*x/y)*(2*y/(3*x)+2*x/y)";
1411 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1412 if UnparseC.term t = "(52 * x \<up> 2 + 16 * y \<up> 2) / (9 * y \<up> 2)"
1413 then () else error "rational.sml: diff.behav. in norm_Rational_mg 34";
1415 (*------- SRAM Schalk I, p.69 Nr. 442b --- abgewandelt*)
1416 val t = TermC.str2term
1417 ("(15*a \<up> 4/(a*x \<up> 3) - 5*a*((b \<up> 4 - 5*c \<up> 2*x) / x \<up> 2)) * " ^
1418 "(x \<up> 3/(5*a*b \<up> 3*c \<up> 3)) + a/c \<up> 3 * (x*(b/a) - 3*b*(a/b \<up> 4))");
1419 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1420 if UnparseC.term t = "5 * x \<up> 2 / (b \<up> 3 * c)"
1421 then () else error "rational.sml: diff.behav. in norm_Rational_mg 53";
1424 "-------- examples double fractions from: Mathematik 1 Schalk ----------------";
1425 "-------- examples double fractions from: Mathematik 1 Schalk ----------------";
1426 "-------- examples double fractions from: Mathematik 1 Schalk ----------------";
1427 "----- SRD Schalk I, p.69 Nr. 454b";
1428 val t = TermC.str2term "((2 - x)/(2*a)) / (2*a/(x - 2))";
1429 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1430 if UnparseC.term t = "(- 4 + 4 * x + - 1 * x \<up> 2) / (4 * a \<up> 2)"
1431 then () else error "rational.sml: diff.behav. in norm_Rational_mg 35";
1433 "----- SRD Schalk I, p.69 Nr. 455a";
1434 val t = TermC.str2term "(a \<up> 2 + 1)/(a \<up> 2 - 1) / ((a+1)/(a - 1))";
1435 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1436 if UnparseC.term t = "(1 + a \<up> 2) / (1 + 2 * a + a \<up> 2)" then ()
1437 else error "rational.sml: diff.behav. in norm_Rational_mg 36";
1439 "----- Schalk I, p.69 Nr. 455b";
1440 val t = TermC.str2term "(x \<up> 2 - 4)/(y \<up> 2 - 9)/((2+x)/(3 - y))";
1441 (* WN130911 non-termination due to non-termination of
1442 cancel_p_ thy (TermC.str2term ("(-12 + 4 * y + 3 * x \<up> 2 + -1 * (x \<up> 2 * y)) /" ^
1443 "(-18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)"))
1445 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1446 if UnparseC.term t = "(2 + -1 * x) / (3 + y)" then ()
1447 else error "rational.sml: diff.behav. in norm_Rational_mg 37";
1450 "----- SK060904-1a non-termination of cancel_p_ ?: worked before 0707xx";
1451 val t = TermC.str2term "(x \<up> 2 - 4)*(3 - y) / ((y \<up> 2 - 9)*(2+x))";
1452 (* WN130911 non-termination due to non-termination of
1453 cancel_p_ thy (TermC.str2term ("(-12 + 4 * y + 3 * x \<up> 2 + -1 * (x \<up> 2 * y)) /" ^
1454 "(-18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)"))
1456 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1457 if UnparseC.term t = "(2 + -1 * x) / (3 + y)" then ()
1458 else error "rational.sml: diff.behav. in norm_Rational_mg 37b";
1461 "----- ?: worked before 0707xx";
1462 val t = TermC.str2term "(3 + -1 * y) / (-9 + y \<up> 2)";
1463 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1464 if UnparseC.term t = "- 1 / (3 + y)"
1465 then () else error "rational.sml: -1 / (3 + y) norm_Rational";
1467 "----- SRD Schalk I, p.69 Nr. 456b";
1468 val t = TermC.str2term "(b \<up> 3 - b \<up> 2) / (b \<up> 2+b) / (b \<up> 2 - 1)";
1469 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1470 if UnparseC.term t = "b / (1 + 2 * b + b \<up> 2)"
1471 then () else error "rational.sml: diff.behav. in norm_Rational_mg 38";
1473 "----- SRD Schalk I, p.69 Nr. 457b";
1474 val t = TermC.str2term "(16*a \<up> 2 - 9*b \<up> 2)/(2*a+3*a*b) / ((4*a+3*b)/(4*a \<up> 2 - 9*a \<up> 2*b \<up> 2))";
1475 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1476 if UnparseC.term t = "8 * a \<up> 2 + - 6 * a * b + - 12 * a \<up> 2 * b + 9 * a * b \<up> 2"
1477 then () else error "rational.sml: diff.behav. in norm_Rational_mg 39";
1479 "----- Schalk I, p.69 Nr. 458b works since 0707";
1480 val t = TermC.str2term "(2*a \<up> 2*x - a \<up> 2) / (a*x - b*x) / (b \<up> 2*(2*x - 1) / (x*(a - b)))";
1481 (*val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1483 ### rls: cancel_p on: (-1 * a \<up> 2 + 2 * (a \<up> 2 * x)) / (a * x + -1 * (b * x)) /
1484 ((-1 * b \<up> 2 + 2 * (b \<up> 2 * x)) / (a * x + -1 * (b * x)))
1485 exception Div raised
1488 val t = TermC.str2term
1489 ("(-1 * a \<up> 2 + 2 * (a \<up> 2 * x)) / (a * x + -1 * (b * x)) /" ^
1490 "((-1 * b \<up> 2 + 2 * (b \<up> 2 * x)) / (a * x + -1 * (b * x)))");
1491 NONE = cancel_p_ thy t;
1493 if UnparseC.term t = "a \<up> 2 / b \<up> 2" then ()
1494 else error "rational.sml: diff.behav. in norm_Rational_mg 39b";
1497 "----- SRD Schalk I, p.69 Nr. 459b";
1498 val t = TermC.str2term "(a \<up> 2 - b \<up> 2)/(a*b) / (4*(a+b) \<up> 2/a)";
1499 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1500 if UnparseC.term t = "(a + - 1 * b) / (4 * a * b + 4 * b \<up> 2)" then ()
1501 else error "rational.sml: diff.behav. in norm_Rational_mg 41";
1503 "----- Schalk I, p.69 Nr. 460b nonterm.SK";
1504 val t = TermC.str2term "(9*(x \<up> 2 - 8*x + 16) / (4*(y \<up> 2 - 2*y + 1))) / ((3*x - 12) / (16*y - 16))";
1505 (*val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1506 exception Div raised
1509 val t = TermC.str2term
1510 ("(144 + -72 * x + 9 * x \<up> 2) / (4 + -8 * y + 4 * y \<up> 2) /" ^
1511 "((-12 + 3 * x) / (-16 + 16 * y))");
1512 NONE = cancel_p_ thy t;
1514 if UnparseC.term t = !!!!!!!!!!!!!!!!!!!!!!!!!
1515 then () else error "rational.sml: diff.behav. in norm_Rational_mg 42";
1518 "----- some variant of the above; was non-terminating before";
1519 val t = TermC.str2term "9*(x \<up> 2 - 8*x+16)*(16*y - 16)/(4*(y \<up> 2 - 2*y+1)*(3*x - 12))";
1520 val SOME (t , _) = rewrite_set_ thy false norm_Rational t;
1521 if UnparseC.term t = "(48 + - 12 * x) / (1 + - 1 * y)"
1522 then () else error "some variant of the above; was non-terminating before";
1524 "----- SRD Schalk I, p.70 Nr. 472a";
1525 val t = TermC.str2term ("((8*x \<up> 2 - 32*y \<up> 2) / (2*x + 4*y)) / ((4*x - 8*y) / (x + y))");
1526 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1527 if UnparseC.term t = "x + y"
1528 then () else error "rational.sml: diff.behav. in norm_Rational_mg 43";
1530 "----- Schalk I, p.70 Nr. 478b ----- Rechenzeit: 5 sec";
1531 val t = TermC.str2term ("(a - (a*b + b \<up> 2)/(a+b))/(b+(a - b)/(1+(a+b)/(a - b))) / " ^
1532 "((a - a \<up> 2/(a+b))/(a+(a*b)/(a - b)))");
1533 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1534 if UnparseC.term t = "(2 * a \<up> 3 + 2 * a \<up> 2 * b) / (a \<up> 2 * b + b \<up> 3)"
1535 then () else error "rational.sml: diff.behav. in norm_Rational_mg 51";
1537 (*SRD Schalk I, p.69 Nr. 461a *)
1538 val t = TermC.str2term "(2/(x+3) + 2/(x - 3)) / (8*x/(x \<up> 2 - 9))";
1539 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1540 if UnparseC.term t = "1 / 2"
1541 then () else error "rational.sml: diff.behav. in norm_Rational_mg 44";
1543 (*SRD Schalk I, p.69 Nr. 464b *)
1544 val t = TermC.str2term "(a - a/(a - 2)) / (a + a/(a - 2))";
1545 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1546 if UnparseC.term t = "(- 3 + a) / (- 1 + a)"
1547 then () else error "rational.sml: diff.behav. in norm_Rational_mg 45";
1549 (*SRD Schalk I, p.69 Nr. 465b *)
1550 val t = TermC.str2term "((x+3*y)/9 + (4*y \<up> 2 - 9*z \<up> 2)/(16*x)) / (x/9 + y/6 + z/4)";
1551 (* WN130911 non-termination due to non-termination of
1552 cancel_p_ thy (TermC.str2term
1553 ("("(576 * x \<up> 2 + 1728 * (x * y) + 1296 * y \<up> 2 + -2916 * z \<up> 2) /" ^
1554 "(576 * x \<up> 2 + 864 * (x * y) + 1296 * (x * z))"))
1556 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1557 if UnparseC.term t = "(4 * x + 6 * y + -9 * z) / (4 * x)"
1558 then () else error "rational.sml: diff.behav. in norm_Rational_mg 46";
1561 (*SRD Schalk I, p.69 Nr. 466b *)
1562 val t = TermC.str2term "((1 - 7*(x - 2)/(x \<up> 2 - 4)) / (6/(x+2))) / (3/(x+5)+30/(x \<up> 2 - 25))";
1563 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1564 if UnparseC.term t = "(25 + - 10 * x + x \<up> 2) / 18"
1565 then () else error "rational.sml: diff.behav. in norm_Rational_mg 47";
1567 (*SRD Schalk I, p.70 Nr. 469 *)
1568 val t = TermC.str2term ("3*b \<up> 2 / (4*a \<up> 2 - 8*a*b + 4*b \<up> 2) / " ^
1569 "(a / (a \<up> 2*b - b \<up> 3) + (a - b) / (4*a*b \<up> 2 + 4*b \<up> 3) - 1 / (4*b \<up> 2))");
1570 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1571 if UnparseC.term t = "- 3 * b \<up> 3 / (- 2 * a + 2 * b)"
1572 then () else error "rational.sml: diff.behav. in norm_Rational_mg 48";
1574 (*//----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)
1575 "-------- me Schalk I No.186 -------------------------------------------------";
1576 "-------- me Schalk I No.186 -------------------------------------------------";
1577 "-------- me Schalk I No.186 -------------------------------------------------";
1578 val fmz = ["Term ((14 * x * y) / ( x * y ))", "normalform N"];
1580 ("Rational",["rational", "simplification"],
1581 ["simplification", "of_rationals"]);
1582 val p = e_pos'; val c = [];
1583 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1584 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1585 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1586 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1587 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1588 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1589 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1590 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1591 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1592 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1593 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;(*++ for explicit script*)
1594 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;(*++ for explicit script*)
1595 case (f2str f, nxt) of
1596 ("14", ("End_Proof'", _)) => ()
1597 | _ => error "rational.sml diff.behav. in me Schalk I No.186";
1598 \\----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)*)
1600 (*//----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)
1601 "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------------------";
1602 "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------------------";
1603 "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------------------";
1605 CalcTree [(["Term (((2 - x)/(2*a)) / (2*a/(x - 2)))", "normalform N"],
1606 ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
1609 autoCalculate 1 CompleteCalc;
1610 val ((pt, p), _) = get_calc 1;
1612 Test_Tool.show_pt pt;
1614 (([], Frm), Simplify ((2 - x) / (2 * a) / (2 * a / (x - 2)))),
1615 (([1], Frm), (2 - x) / (2 * a) / (2 * a / (x - 2))),
1616 (([1], Res), (2 + -1 * x) / (2 * a) / (2 * a / (x + -1 * 2))),
1617 (([2], Res), (2 + -1 * x) / (2 * a) / (2 * a / (-2 + x))),
1618 (([3], Res), (2 + -1 * x) * (-2 + x) / (2 * a * (2 * a))),
1619 (([4], Res), (-4 + 4 * x + -1 * x \<up> 2) / (4 * a \<up> 2)),
1620 (([], Res), (-4 + 4 * x + -1 * x \<up> 2) / (4 * a \<up> 2))]
1622 interSteps 1 ([1], Res);
1623 val ((pt, p), _) = get_calc 1;
1624 (*Test_Tool.show_pt pt;
1626 (([], Frm), Simplify ((2 - x) / (2 * a) / (2 * a / (x - 2)))),
1627 (([1], Frm), (2 - x) / (2 * a) / (2 * a / (x - 2))),
1628 (([1,1], Frm), (2 - x) / (2 * a) / (2 * a / (x - 2))),
1629 (([1,1], Res), (2 - x) / (2 * a) / (2 * a / (x + -1 * 2))),
1630 (([1,2], Res), (2 + -1 * x) / (2 * a) / (2 * a / (x + -1 * 2))),
1631 (([1], Res), (2 + -1 * x) / (2 * a) / (2 * a / (x + -1 * 2))),
1632 (([2], Res), (2 + -1 * x) / (2 * a) / (2 * a / (-2 + x))),
1633 (([3], Res), (2 + -1 * x) * (-2 + x) / (2 * a * (2 * a))),
1634 (([4], Res), (-4 + 4 * x + -1 * x \<up> 2) / (4 * a \<up> 2)),
1635 (([], Res), (-4 + 4 * x + -1 * x \<up> 2) / (4 * a \<up> 2))]
1637 val (t, asm) = get_obj g_result pt [1, 1];
1638 if UnparseC.term t = "(2 - x) / (2 * a) / (2 * a / (x + -1 * 2))" andalso UnparseC.terms asm = "[]"
1639 then () else error "2nd interSteps ..Simp_Rat_Double_No-1 changed on [1, 1]";
1640 val (t, asm) = get_obj g_result pt [1, 2];
1641 if UnparseC.term t = "(2 + -1 * x) / (2 * a) / (2 * a / (x + -1 * 2))" andalso UnparseC.terms asm = "[]"
1642 then () else error "3rd interSteps ..Simp_Rat_Double_No-1 changed on [1, 2]";
1643 \\----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)*)
1646 (*//----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)
1647 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------------------";
1648 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------------------";
1649 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------------------";
1651 CalcTree [(["Term ((a^2 + -1*b^2) / (a^2 + -2*a*b + b^2))", "normalform N"],
1652 ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
1655 autoCalculate 1 CompleteCalc;
1656 val ((pt, p), _) = get_calc 1;
1657 (*Test_Tool.show_pt pt;
1659 (([], Frm), Simplify ((a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * a * b + b \<up> 2))),
1660 (([1], Frm), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * a * b + b \<up> 2)),
1661 (([1], Res), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * (a * b) + b \<up> 2)),
1662 (([2], Res), (a + b) / (a + -1 * b)),
1663 (([], Res), (a + b) / (a + -1 * b))]
1665 interSteps 1 ([2], Res);
1666 val ((pt, p), _) = get_calc 1;
1667 (*Test_Tool.show_pt pt;
1669 (([], Frm), Simplify ((a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * a * b + b \<up> 2))),
1670 (([1], Frm), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * a * b + b \<up> 2)),
1671 (([1], Res), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * (a * b) + b \<up> 2)),
1672 (([2,1], Frm), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * (a * b) + b \<up> 2)),
1673 (([2,1], Res), (a + b) / (a + -1 * b)),
1674 (([2], Res), (a + b) / (a + -1 * b)),
1675 (([], Res), (a + b) / (a + -1 * b))]
1677 interSteps 1 ([2,1],Res);
1678 val ((pt, p), _) = get_calc 1;
1679 (*Test_Tool.show_pt pt;
1681 (([], Frm), Simplify ((a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * a * b + b \<up> 2))),
1682 (([1], Frm), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * a * b + b \<up> 2)),
1683 (([1], Res), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * (a * b) + b \<up> 2)),
1684 (([2,1], Frm), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * (a * b) + b \<up> 2)),
1685 (([2,1,1], Frm), (a \<up> 2 + -1 * b \<up> 2) / (a \<up> 2 + -2 * (a * b) + b \<up> 2)),
1686 (([2,1,1], Res), (a \<up> 2 + -1 * (a * b) + a * b + -1 * b \<up> 2) /
1687 (a \<up> 2 + -2 * (a * b) + 1 * b \<up> 2)),
1688 (([2,1,2], Res), (a \<up> 2 + -1 * (a * b) + a * b + -1 * b \<up> 2) /
1689 (a \<up> 2 + -2 * (a * b) + -1 \<up> 2 * b \<up> 2)),
1690 (([2,1,3], Res), (a \<up> 2 + -1 * (a * b) + a * b + -1 * b \<up> 2) /
1691 (a \<up> 2 + -2 * (a * b) + (-1 * b) \<up> 2)),
1692 (([2,1,4], Res), (a * a + -1 * (a * b) + a * b + -1 * b \<up> 2) /
1693 (a \<up> 2 + -2 * (a * b) + (-1 * b) \<up> 2)),
1694 (([2,1,5], Res), (a * a + -1 * (a * b) + a * b + -1 * (b * b)) /
1695 (a \<up> 2 + -2 * (a * b) + (-1 * b) \<up> 2)),
1696 (([2,1,6], Res), (a * a + -1 * (a * b) + a * b + -1 * (b * b)) /
1697 (a \<up> 2 + -1 * (2 * (a * b)) + (-1 * b) \<up> 2)),
1698 (([2,1,7], Res), (a * a + a * (-1 * b) + (b * a + b * (-1 * b))) /
1699 (a \<up> 2 + 2 * (a * (-1 * b)) + (-1 * b) \<up> 2)),
1700 (([2,1,8], Res), (a * a + a * (-1 * b) + (b * a + b * (-1 * b))) /
1701 (a \<up> 2 + 2 * a * (-1 * b) + (-1 * b) \<up> 2)),
1702 (([2,1,9], Res), (a * (a + -1 * b) + (b * a + b * (-1 * b))) /
1703 (a \<up> 2 + 2 * a * (-1 * b) + (-1 * b) \<up> 2)),
1704 (([2,1,10], Res), (a * (a + -1 * b) + b * (a + -1 * b)) /
1705 (a \<up> 2 + 2 * a * (-1 * b) + (-1 * b) \<up> 2)),
1706 (([2,1,11], Res), (a + b) * (a + -1 * b) / (a \<up> 2 + 2 * a * (-1 * b) + (-1 * b) \<up> 2)),
1707 (([2,1,12], Res), (a + b) * (a + -1 * b) / ((a + -1 * b) * (a + -1 * b))),
1708 (([2,1,13], Res), (a + b) / (a + -1 * b)),
1709 (([2,1], Res), (a + b) / (a + -1 * b)),
1710 (([2], Res), (a + b) / (a + -1 * b)),
1711 (([], Res), (a + b) / (a + -1 * b))]
1713 val newnds = children (get_nd pt [2,1]) (*see "fun detailrls"*);
1714 if length newnds = 13 then () else error "rational.sml: interSteps cancel_p rev_rew_p";
1716 val p = ([2,1,9],Res);
1718 val (_, tac, _) = ME_Misc.pt_extract (pt, p);
1719 case tac of SOME (Rewrite ("sym_distrib_left", _)) => ()
1720 | _ => error "rational.sml: getTactic, sym_real_plus_binom_times1";
1721 \\----------------------------------TOODOO (*Rfuns revsets \<longrightarrow> broken*)*)
1724 "-------- investigate rulesets for cancel_p ----------------------------------";
1725 "-------- investigate rulesets for cancel_p ----------------------------------";
1726 "-------- investigate rulesets for cancel_p ----------------------------------";
1727 val thy = @{theory "Rational"};
1728 val t = TermC.str2term "(a \<up> 2 + -1*b \<up> 2) / (a \<up> 2 + -2*a*b + b \<up> 2)";
1729 val tt = TermC.str2term "(1 * a + 1 * b) * (1 * a + -1 * b)"(*numerator only*);
1731 "----- with rewrite_set_";
1732 val SOME (tt',asm) = rewrite_set_ thy false make_polynomial tt;
1733 if UnparseC.term tt'= "a \<up> 2 + - 1 * b \<up> 2" then () else error "rls chancel_p 1";
1734 val tt = TermC.str2term "((1 * a + -1 * b) * (1 * a + -1 * b))"(*denominator only*);
1735 val SOME (tt',asm) = rewrite_set_ thy false make_polynomial tt;
1736 if UnparseC.term tt' = "a \<up> 2 + - 2 * a * b + b \<up> 2" then () else error "rls chancel_p 2";
1738 "----- with Derive.do_one; WN1130912 not investigated further, will be discontinued";
1739 val SOME (tt, _) = factout_p_ thy t;
1740 if UnparseC.term tt = "(a + b) * (a + - 1 * b) / ((a + - 1 * b) * (a + - 1 * b))"
1741 then () else error "rls chancel_p 3";
1743 "--- with simpler ruleset";
1744 val {rules, rew_ord= (_, ro), ...} = Rule_Set.rep (assoc_rls "rev_rew_p");
1745 val der = Derive.do_one thy Atools_erls rules ro NONE tt;
1746 if length der = 12 then () else error "WN1130912 rls chancel_p 4";
1747 (*default_print_depth 99;*) writeln (Derive.deriv2str der); (*default_print_depth 3;*)
1749 (*default_print_depth 99;*) map (UnparseC.term o #1) der; (*default_print_depth 3;*)
1750 "...,(-1 * b \<up> 2 + a \<up> 2) / (-2 * (a * b) + a \<up> 2 + (-1 * b) \<up> 2) ]";
1751 (*default_print_depth 99;*) map (Rule.to_string o #2) der; (*default_print_depth 3;*)
1752 (*default_print_depth 99;*) map (UnparseC.term o #1 o #3) der; (*default_print_depth 3;*)
1754 val der = Derive.do_one thy Atools_erls rules ro NONE
1755 (TermC.str2term "(1 * a + 1 * b) * (1 * a + -1 * b)");
1756 (*default_print_depth 99;*) writeln (Derive.deriv2str der); (*default_print_depth 3;*)
1758 val {rules, rew_ord=(_,ro),...} = Rule_Set.rep (assoc_rls "rev_rew_p");
1759 val der = Derive.do_one thy Atools_erls rules ro NONE
1760 (TermC.str2term "(1 * a + -1 * b) * (1 * a + -1 * b)");
1761 (*default_print_depth 99;*) writeln (Derive.deriv2str der); (*default_print_depth 3;*)
1762 (*default_print_depth 99;*) map (UnparseC.term o #1) der; (*default_print_depth 3;*)
1763 (*WN060829 ...postponed*)
1766 "-------- fun eval_get_denominator -------------------------------------------";
1767 "-------- fun eval_get_denominator -------------------------------------------";
1768 "-------- fun eval_get_denominator -------------------------------------------";
1769 val thy = @{theory Isac_Knowledge};
1770 val t = Thm.term_of (the (TermC.parse thy "get_denominator ((a +x)/b)"));
1771 val SOME (_, t') = eval_get_denominator "" 0 t thy;
1772 if UnparseC.term t' = "get_denominator ((a + x) / b) = b"
1773 then () else error "get_denominator ((a + x) / b) = b"
1776 "-------- several errpats in complicated term --------------------------------";
1777 "-------- several errpats in complicated term --------------------------------";
1778 "-------- several errpats in complicated term --------------------------------";
1779 (*WN12xxxx TODO: instead of Gabriella's example here (27.Jul.12) find a simpler one
1780 WN130912: kept this test, although not clear what for*)
1782 CalcTree [(["Term ((5*b + 25)/(a^2 - b^2) * (a - b)/(5*b))", "normalform N"],
1783 ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
1786 autoCalculate 1 CompleteCalc;
1787 val ((pt, p), _) = get_calc 1;
1788 (*Test_Tool.show_pt pt;
1790 (([], Frm), Simplify ((5 * b + 25) / (a \<up> 2 - b \<up> 2) * (a - b) / (5 * b))),
1791 (([1], Frm), (5 * b + 25) / (a \<up> 2 - b \<up> 2) * (a - b) / (5 * b)),
1792 (([1], Res), (5 * b + 25) / (a \<up> 2 + -1 * b \<up> 2) * (a + -1 * b) / (5 * b)),
1793 (([2], Res), (5 * b + 25) * (a + -1 * b) / (a \<up> 2 + -1 * b \<up> 2) / (5 * b)),
1794 (([3], Res), (25 * a + -25 * b + 5 * (a * b) + -5 * b \<up> 2) / (a \<up> 2 + -1 * b \<up> 2) /
1796 (([4], Res), (25 + 5 * b) / (a + b) / (5 * b)),
1797 (([5], Res), (25 + 5 * b) / ((a + b) * (5 * b))),
1798 (([6], Res), (25 + 5 * b) / (5 * (a * b) + 5 * b \<up> 2)),
1799 (([7], Res), (5 + b) / (a * b + b \<up> 2)),
1800 (([], Res), (5 + b) / (a * b + b \<up> 2))] *)
1803 "-------- WN1309xx non-terminating rls norm_Rational -------------------------";
1804 "-------- WN1309xx non-terminating rls norm_Rational -------------------------";
1805 "-------- WN1309xx non-terminating rls norm_Rational -------------------------";
1806 (*------- Schalk I, p.70 Nr. 480b; a/b : c/d translated to a/b * d/c*)
1807 val t = TermC.str2term
1808 ("((12*x*y / (9*x \<up> 2 - y \<up> 2)) / (1 / (3*x - y) \<up> 2 - 1 / (3*x + y) \<up> 2)) * " ^
1809 "((1/(x - 5*y) \<up> 2 - 1/(x + 5*y) \<up> 2) / (20*x*y / (x \<up> 2 - 25*y \<up> 2)))");
1811 (*1st factor separately simplified *)
1812 val t = TermC.str2term "((12*x*y / (9*x \<up> 2 - y \<up> 2)) / (1 / (3*x - y) \<up> 2 - 1 / (3*x + y) \<up> 2))";
1813 val SOME (t', _) = rewrite_set_ thy false norm_Rational t;
1814 if UnparseC.term t' = "(- 9 * x \<up> 2 + y \<up> 2) / - 1" then () else error "Nr. 480b lhs changed";
1815 (*2nd factor separately simplified *)
1816 val t = TermC.str2term "((1/(x - 5*y) \<up> 2 - 1/(x + 5*y) \<up> 2) / (20*x*y / (x \<up> 2 - 25*y \<up> 2)))";
1817 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
1818 if UnparseC.term t' = "- 1 / (- 1 * x \<up> 2 + 25 * y \<up> 2)" then () else error "Nr. 480b rhs changed";
1820 "-------- Schalk I, p.70 Nr. 477a: terms are exploding ?!?";
1821 val t = TermC.str2term ("b*y/(b - 2*y)/((b \<up> 2 - y \<up> 2)/(b+2*y)) /" ^
1822 "(b \<up> 2*y + b*y \<up> 2) * (a+x) \<up> 2 / ((b \<up> 2 - 4*y \<up> 2) * (a+2*x) \<up> 2)");
1823 (*val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
1825 ### rls: cancel_p on: (a \<up> 2 * (b * y) + 2 * (a * (b * (x * y))) + b * (x \<up> 2 * y)) /
1827 ((b \<up> 2 + -1 * y \<up> 2) / (b + 2 * y)) /
1828 (b \<up> 2 * y + b * y \<up> 2) /
1829 (a \<up> 2 * b \<up> 2 + -4 * (a \<up> 2 * y \<up> 2) + 4 * (a * (b \<up> 2 * x)) +
1830 -16 * (a * (x * y \<up> 2)) +
1831 4 * (b \<up> 2 * x \<up> 2) +
1832 -16 * (x \<up> 2 * y \<up> 2))
1833 exception Div raised
1836 val t = TermC.str2term
1837 ("(a \<up> 2 * (b * y) + 2 * (a * (b * (x * y))) + b * (x \<up> 2 * y)) /" ^
1839 "((b \<up> 2 + -1 * y \<up> 2) / (b + 2 * y)) /" ^
1840 "(b \<up> 2 * y + b * y \<up> 2) /" ^
1841 "(a \<up> 2 * b \<up> 2 + -4 * (a \<up> 2 * y \<up> 2) + 4 * (a * (b \<up> 2 * x)) +" ^
1842 "-16 * (a * (x * y \<up> 2)) +" ^
1843 "4 * (b \<up> 2 * x \<up> 2) +" ^
1844 "-16 * (x \<up> 2 * y \<up> 2))");
1845 NONE = cancel_p_ thy t;
1848 (*------- Schalk I, p.70 Nr. 476b in 2003 this worked using 10 sec. *)
1849 val t = TermC.str2term
1850 ("((a \<up> 2 - b \<up> 2)/(2*a*b) + 2*a*b/(a \<up> 2 - b \<up> 2)) / ((a \<up> 2 + b \<up> 2)/(2*a*b) + 1) / " ^
1851 "((a \<up> 2 + b \<up> 2) \<up> 2 / (a + b) \<up> 2)");
1852 (* Rewrite.trace_on := true;
1853 rewrite_set_ thy false norm_Rational t;
1855 #### rls: cancel_p on: (2 * (a \<up> 7 * b) + 4 * (a \<up> 6 * b \<up> 2) + 6 * (a \<up> 5 * b \<up> 3) +
1856 8 * (a \<up> 4 * b \<up> 4) +
1857 6 * (a \<up> 3 * b \<up> 5) +
1858 4 * (a \<up> 2 * b \<up> 6) +
1859 2 * (a * b \<up> 7)) /
1860 (2 * (a \<up> 9 * b) + 4 * (a \<up> 8 * b \<up> 2) +
1861 2 * (2 * (a \<up> 7 * b \<up> 3)) +
1862 4 * (a \<up> 6 * b \<up> 4) +
1863 -4 * (a \<up> 4 * b \<up> 6) +
1864 -4 * (a \<up> 3 * b \<up> 7) +
1865 -4 * (a \<up> 2 * b \<up> 8) +
1866 -2 * (a * b \<up> 9))
1868 if UnparseC.term t = "1 / (a \<up> 2 + -1 * b \<up> 2)" then ()
1869 else error "rational.sml: diff.behav. in norm_Rational_mg 49";
1872 "-------- Schalk I, p.70 Nr. 480a: terms are exploding ?!?";
1873 val t = TermC.str2term ("(1/x + 1/y + 1/z) / (1/x - 1/y - 1/z) / " ^
1874 "(2*x \<up> 2 / (x \<up> 2 - z \<up> 2) / (x / (x + z) + x / (x - z)))");
1875 (* Rewrite.trace_on := true;
1876 rewrite_set_ thy false norm_Rational t;
1878 #### rls: cancel_p on: (2 * (x \<up> 6 * (y \<up> 2 * z)) + 2 * (x \<up> 6 * (y * z \<up> 2)) +
1879 2 * (x \<up> 5 * (y \<up> 2 * z \<up> 2)) +
1880 -2 * (x \<up> 4 * (y \<up> 2 * z \<up> 3)) +
1881 -2 * (x \<up> 4 * (y * z \<up> 4)) +
1882 -2 * (x \<up> 3 * (y \<up> 2 * z \<up> 4))) /
1883 (-2 * (x \<up> 6 * (y \<up> 2 * z)) + -2 * (x \<up> 6 * (y * z \<up> 2)) +
1884 2 * (x \<up> 5 * (y \<up> 2 * z \<up> 2)) +
1885 2 * (x \<up> 4 * (y \<up> 2 * z \<up> 3)) +
1886 2 * (x \<up> 4 * (y * z \<up> 4)) +
1887 -2 * (x \<up> 3 * (y \<up> 2 * z \<up> 4)))
1890 "-------- Schalk I, p.60 Nr. 215d: terms are exploding, internal loop does not terminate";
1891 val t = TermC.str2term "(a-b) \<up> 3 * (x+y) \<up> 4 / ((x+y) \<up> 2 * (a-b) \<up> 5)";
1892 (* Kein Wunder, denn Z???ler und Nenner extra als Polynom dargestellt ergibt:
1894 val t = TermC.str2term "(a-b) \<up> 3 * (x+y) \<up> 4";
1895 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1897 "a \<up> 3 * x \<up> 4 + 4 * a \<up> 3 * x \<up> 3 * y +6 * a \<up> 3 * x \<up> 2 * y \<up> 2 +4 * a \<up> 3 * x * y \<up> 3 +a \<up> 3 * y \<up> 4 +-3 * a \<up> 2 * b * x \<up> 4 +-12 * a \<up> 2 * b * x \<up> 3 * y +-18 * a \<up> 2 * b * x \<up> 2 * y \<up> 2 +-12 * a \<up> 2 * b * x * y \<up> 3 +-3 * a \<up> 2 * b * y \<up> 4 +3 * a * b \<up> 2 * x \<up> 4 +12 * a * b \<up> 2 * x \<up> 3 * y +18 * a * b \<up> 2 * x \<up> 2 * y \<up> 2 +12 * a * b \<up> 2 * x * y \<up> 3 +3 * a * b \<up> 2 * y \<up> 4 +-1 * b \<up> 3 * x \<up> 4 +-4 * b \<up> 3 * x \<up> 3 * y +-6 * b \<up> 3 * x \<up> 2 * y \<up> 2 +-4 * b \<up> 3 * x * y \<up> 3 +-1 * b \<up> 3 * y \<up> 4";
1898 val t = TermC.str2term "((x+y) \<up> 2 * (a-b) \<up> 5)";
1899 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1901 "a \<up> 5 * x \<up> 2 + 2 * a \<up> 5 * x * y + a \<up> 5 * y \<up> 2 +-5 * a \<up> 4 * b * x \<up> 2 +-10 * a \<up> 4 * b * x * y +-5 * a \<up> 4 * b * y \<up> 2 +10 * a \<up> 3 * b \<up> 2 * x \<up> 2 +20 * a \<up> 3 * b \<up> 2 * x * y +10 * a \<up> 3 * b \<up> 2 * y \<up> 2 +-10 * a \<up> 2 * b \<up> 3 * x \<up> 2 +-20 * a \<up> 2 * b \<up> 3 * x * y +-10 * a \<up> 2 * b \<up> 3 * y \<up> 2 +5 * a * b \<up> 4 * x \<up> 2 +10 * a * b \<up> 4 * x * y +5 * a * b \<up> 4 * y \<up> 2 +-1 * b \<up> 5 * x \<up> 2 +-2 * b \<up> 5 * x * y +-1 * b \<up> 5 * y \<up> 2";
1903 anscheinend macht dem Rechner das Krzen diese Bruches keinen Spass mehr ...*)
1905 "-------- Schalk I, p.70 Nr. 480b: terms are exploding, Rewrite.trace_on stops at";
1906 val t = TermC.str2term ("((12*x*y/(9*x \<up> 2 - y \<up> 2))/" ^
1907 "(1/(3*x - y) \<up> 2 - 1/(3*x + y) \<up> 2)) *" ^
1908 "(1/(x - 5*y) \<up> 2 - 1/(x + 5*y) \<up> 2)/" ^
1909 "(20*x*y/(x \<up> 2 - 25*y \<up> 2))");
1910 (*val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1912 #### rls: cancel_p on: (19440 * (x \<up> 8 * y \<up> 2) + -490320 * (x \<up> 6 * y \<up> 4) +
1913 108240 * (x \<up> 4 * y \<up> 6) +
1914 -6000 * (x \<up> 2 * y \<up> 8)) /
1915 (2160 * (x \<up> 8 * y \<up> 2) + -108240 * (x \<up> 6 * y \<up> 4) +
1916 1362000 * (x \<up> 4 * y \<up> 6) +
1917 -150000 * (x \<up> 2 * y \<up> 8))