1.1 --- a/src/Tools/isac/Knowledge/Rational.thy Mon Sep 02 14:56:57 2013 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Mon Sep 02 15:17:34 2013 +0200
1.3 @@ -435,7 +435,8 @@
1.4 end
1.5
1.6 (* add fractions
1.7 - assumes: is a term with outmost "+" and at least one outmost "/" in respective summands*)
1.8 + assumes: is a term with outmost "+" and at least one outmost "/" in respective summands
1.9 + NOTE: the case "(_ + _) + _" need not be considered due to iterated addition.*)
1.10 fun add_fraction_p_ (thy: theory) t =
1.11 let val opt = norm_frac_sum t
1.12 in
1.13 @@ -447,8 +448,8 @@
1.14 val baseT = type_of n1
1.15 val expT = HOLogic.realT
1.16 in
1.17 - case (poly_of_term vs d1, poly_of_term vs d2) of
1.18 - (SOME a, SOME b) =>
1.19 + (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) of
1.20 + (SOME _, SOME a, SOME _, SOME b) =>
1.21 let
1.22 val ((a', b'), c) = gcd_poly a b
1.23 val nomin = term_of_poly baseT expT vs
1.24 @@ -3570,15 +3571,15 @@
1.25 ],
1.26 scr = EmptyScr});
1.27 (* ------------------------------------------------------------------- *)
1.28 +(* "Rls" causes repeated application of cancel_p to one and the same term *)
1.29 val cancel_p_rls = prep_rls(
1.30 - Rls {id = "cancel_p_rls", preconds = [],
1.31 - rew_ord = ("dummy_ord",dummy_ord),
1.32 - erls = e_rls, srls = Erls, calc = [], errpatts = [],
1.33 - rules =
1.34 - [Rls_ cancel_p
1.35 - (*FIXME.WN.0401 ? redesign Rrls - use exhaustively on a term ?*)
1.36 - ],
1.37 - scr = EmptyScr});
1.38 + Rls
1.39 + {id = "cancel_p_rls", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
1.40 + erls = e_rls, srls = Erls, calc = [], errpatts = [],
1.41 + rules =
1.42 + [Rls_ cancel_p (*FIXME.WN.0401 ? redesign Rrls - use exhaustively on a term ?*)
1.43 + ],
1.44 + scr = EmptyScr});
1.45 (* -------------------------------------------------------------------- *)
1.46 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;
1.47 used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*)
1.48 @@ -3661,18 +3662,20 @@
1.49 (* ------------------------------------------------------------------ *)
1.50 (*040109 'norm_Rational'(by RL) replaced by 'norm_Rational_mg'(MG)
1.51 just be renaming:*)
1.52 -val norm_Rational(*_mg*) = prep_rls(
1.53 - Seq {id = "norm_Rational"(*_mg*), preconds = [],
1.54 - rew_ord = ("dummy_ord",dummy_ord),
1.55 - erls = norm_rat_erls, srls = Erls, calc = [], errpatts = [],
1.56 - rules = [Rls_ discard_minus,
1.57 - Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
1.58 - Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
1.59 - Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)
1.60 - Rls_ norm_Rational_rls, (* the main rls, looping (#) *)
1.61 - Rls_ discard_parentheses1 (* mult only *)
1.62 - ],
1.63 - scr = EmptyScr}:rls);
1.64 +val norm_Rational (*_mg*) = prep_rls(
1.65 + Seq
1.66 + {id = "norm_Rational"(*_mg*), preconds = [],
1.67 + rew_ord = ("dummy_ord",dummy_ord),
1.68 + erls = norm_rat_erls, srls = Erls, calc = [], errpatts = [],
1.69 + rules = [Rls_ discard_minus,
1.70 + Rls_ rat_mult_poly, (* removes double fractions like a/b/c *)
1.71 + Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
1.72 + Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)
1.73 + Rls_ norm_Rational_rls, (* the main rls, looping (#) *)
1.74 + Rls_ discard_parentheses1 (* mult only *)
1.75 + ],
1.76 + scr = EmptyScr}:rls);
1.77 +"-------- rls norm_Rational --------------------------------------------------";
1.78 (* ------------------------------------------------------------------ *)
1.79
1.80 *}
2.1 --- a/test/Tools/isac/Knowledge/rational.sml Mon Sep 02 14:56:57 2013 +0200
2.2 +++ b/test/Tools/isac/Knowledge/rational.sml Mon Sep 02 15:17:34 2013 +0200
2.3 @@ -30,6 +30,7 @@
2.4 "-------- external calculating functions test -----------";
2.5 "-------- cancel from: Mathematik 1 Schalk Reniets Verlag";
2.6 "-------- common_nominator_p ----------------------------";
2.7 +"-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
2.8 "-------- reverse rewrite -------------------------------";
2.9 "-------- 'reverse-ruleset' cancel_p --------------------";
2.10 "-------- norm_Rational ---------------------------------";
2.11 @@ -1059,6 +1060,69 @@
2.12 if term2str t' = "(3 + x) * (3 - x) / ((3 - x) * (3 - x))" then ()
2.13 else error "rational.sml factout_ (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
2.14
2.15 +"-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
2.16 +"-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
2.17 +"-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
2.18 +val t = str2term ("123 = (a*x)/(b*x) + (c*x)/(d*x) + (e*x)/(f*x::real)");
2.19 +"-------- gcd_poly integration level 1: works on exact term";
2.20 +if NONE = cancel_p_ thy t then () else error "cancel_p_ works on exact fraction";
2.21 +if NONE = add_fraction_p_ thy t then () else error "add_fraction_p_ works on exact fraction";
2.22 +
2.23 +"-------- gcd_poly integration level 2: picks out ONE appropriate subterm";
2.24 +val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
2.25 +if term2str t' = "123 = a * x / (b * x) + c * x / (d * x) + e / f"
2.26 +then () else error "level 2, rewrite_set_ cancel_p: changed";
2.27 +val SOME (t', asm) = rewrite_set_ thy false add_fractions_p t;
2.28 +if term2str t' = "123 = (b * c * x + a * d * x) / (b * d * x) + e * x / (f * x)"
2.29 +then () else error "level 2, rewrite_set_ add_fractions_p: changed";
2.30 +
2.31 +"-------- gcd_poly integration level 3: rewrites all appropriate subterms";
2.32 +val SOME (t', asm) = rewrite_set_ thy false cancel_p_rls t;
2.33 +if term2str t' = "123 = a / b + c / d + e / f"
2.34 +then () else error "level 3, rewrite_set_ cancel_p_rls: changed";
2.35 +val SOME (t', asm) = rewrite_set_ thy false common_nominator_p_rls t; (*CREATE add_fractions_p_rls*)
2.36 +if term2str t' = "123 = (b * d * e * x + b * c * f * x + a * d * f * x) / (b * d * f * x)"
2.37 +then () else error "level 3, rewrite_set_ add_fractions_p_rls: changed";
2.38 +
2.39 +"-------- gcd_poly integration level 4: iteration cancel_p -- add_fraction_p";
2.40 +(* simpler variant *)
2.41 +val testrls = append_rls "testrls" e_rls [Rls_ cancel_p, Rls_ add_fractions_p]
2.42 +val SOME (t', asm) = rewrite_set_ thy false testrls t;
2.43 +(*trace_rewrite := false;
2.44 +# rls: testrls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
2.45 +## rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
2.46 +## rls: common_nominator_p on: 123 = a * x / (b * x) + c * x / (d * x) + e / f
2.47 +## rls: cancel_p on: 123 = (b * c * x + a * d * x) / (b * d * x) + e / f
2.48 +## rls: common_nominator_p on: 123 = (b * c + a * d) / (b * d) + e / f
2.49 +## rls: cancel_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
2.50 +## rls: common_nominator_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) *)
2.51 +if term2str t' = "123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)"
2.52 +then () else error "level 4, rewrite_set_ *_p: changed";
2.53 +
2.54 +(* complicated variant *)
2.55 +val testrls_rls = append_rls "testrls_rls" e_rls [Rls_ cancel_p_rls, Rls_ common_nominator_p_rls];
2.56 +val SOME (t', asm) = rewrite_set_ thy false testrls_rls t;
2.57 +(*# rls: testrls_rls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
2.58 +## rls: cancel_p_rls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
2.59 +### rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
2.60 +### rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e / f
2.61 +### rls: cancel_p on: 123 = a * x / (b * x) + c / d + e / f
2.62 +### rls: cancel_p on: 123 = a / b + c / d + e / f
2.63 +## rls: common_nominator_p_rls on: 123 = a / b + c / d + e / f
2.64 +### rls: common_nominator_p on: 123 = a / b + c / d + e / f
2.65 +### rls: common_nominator_p on: 123 = (b * c + a * d) / (b * d) + e / f
2.66 +### rls: common_nominator_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
2.67 +## rls: cancel_p_rls on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
2.68 +### rls: cancel_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
2.69 +## rls: common_nominator_p_rls on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
2.70 +### rls: common_nominator_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) *)
2.71 +if term2str t' = "123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)"
2.72 +then () else error "level 4, rewrite_set_ *_p_rls: changed"
2.73 +
2.74 +"-------- gcd_poly integration level 5: cancel_p & add_fraction_p within norm_Rational";
2.75 +val SOME (t', asm) = rewrite_set_ thy false norm_Rational t;
2.76 +if term2str t' = "123 = (a * d * f + b * c * f + b * d * e) / (b * d * f)"
2.77 +then () else error "level 5, rewrite_set_ norm_Rational: changed"
2.78
2.79 "-------- reverse rewrite -------------------------------";
2.80 "-------- reverse rewrite -------------------------------";