# HG changeset patch # User Walther Neuper # Date 1378127854 -7200 # Node ID 0831a4a6ec8a1664c5d622347eb9d5137e02ea87 # Parent 2a95fc276d0a0d91281a3d1b70982a0950a441de GCD_Poly_ML: survey on levels integrating gcd_poly in Rational.thy diff -r 2a95fc276d0a -r 0831a4a6ec8a src/Tools/isac/Knowledge/Rational.thy --- a/src/Tools/isac/Knowledge/Rational.thy Mon Sep 02 14:56:57 2013 +0200 +++ b/src/Tools/isac/Knowledge/Rational.thy Mon Sep 02 15:17:34 2013 +0200 @@ -435,7 +435,8 @@ end (* add fractions - assumes: is a term with outmost "+" and at least one outmost "/" in respective summands*) + assumes: is a term with outmost "+" and at least one outmost "/" in respective summands + NOTE: the case "(_ + _) + _" need not be considered due to iterated addition.*) fun add_fraction_p_ (thy: theory) t = let val opt = norm_frac_sum t in @@ -447,8 +448,8 @@ val baseT = type_of n1 val expT = HOLogic.realT in - case (poly_of_term vs d1, poly_of_term vs d2) of - (SOME a, SOME b) => + (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) of + (SOME _, SOME a, SOME _, SOME b) => let val ((a', b'), c) = gcd_poly a b val nomin = term_of_poly baseT expT vs @@ -3570,15 +3571,15 @@ ], scr = EmptyScr}); (* ------------------------------------------------------------------- *) +(* "Rls" causes repeated application of cancel_p to one and the same term *) val cancel_p_rls = prep_rls( - Rls {id = "cancel_p_rls", preconds = [], - rew_ord = ("dummy_ord",dummy_ord), - erls = e_rls, srls = Erls, calc = [], errpatts = [], - rules = - [Rls_ cancel_p - (*FIXME.WN.0401 ? redesign Rrls - use exhaustively on a term ?*) - ], - scr = EmptyScr}); + Rls + {id = "cancel_p_rls", preconds = [], rew_ord = ("dummy_ord", dummy_ord), + erls = e_rls, srls = Erls, calc = [], errpatts = [], + rules = + [Rls_ cancel_p (*FIXME.WN.0401 ? redesign Rrls - use exhaustively on a term ?*) + ], + scr = EmptyScr}); (* -------------------------------------------------------------------- *) (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions; used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*) @@ -3661,18 +3662,20 @@ (* ------------------------------------------------------------------ *) (*040109 'norm_Rational'(by RL) replaced by 'norm_Rational_mg'(MG) just be renaming:*) -val norm_Rational(*_mg*) = prep_rls( - Seq {id = "norm_Rational"(*_mg*), preconds = [], - rew_ord = ("dummy_ord",dummy_ord), - erls = norm_rat_erls, srls = Erls, calc = [], errpatts = [], - rules = [Rls_ discard_minus, - Rls_ rat_mult_poly,(* removes double fractions like a/b/c *) - Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*) - Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*) - Rls_ norm_Rational_rls, (* the main rls, looping (#) *) - Rls_ discard_parentheses1 (* mult only *) - ], - scr = EmptyScr}:rls); +val norm_Rational (*_mg*) = prep_rls( + Seq + {id = "norm_Rational"(*_mg*), preconds = [], + rew_ord = ("dummy_ord",dummy_ord), + erls = norm_rat_erls, srls = Erls, calc = [], errpatts = [], + rules = [Rls_ discard_minus, + Rls_ rat_mult_poly, (* removes double fractions like a/b/c *) + Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*) + Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*) + Rls_ norm_Rational_rls, (* the main rls, looping (#) *) + Rls_ discard_parentheses1 (* mult only *) + ], + scr = EmptyScr}:rls); +"-------- rls norm_Rational --------------------------------------------------"; (* ------------------------------------------------------------------ *) *} diff -r 2a95fc276d0a -r 0831a4a6ec8a test/Tools/isac/Knowledge/rational.sml --- a/test/Tools/isac/Knowledge/rational.sml Mon Sep 02 14:56:57 2013 +0200 +++ b/test/Tools/isac/Knowledge/rational.sml Mon Sep 02 15:17:34 2013 +0200 @@ -30,6 +30,7 @@ "-------- external calculating functions test -----------"; "-------- cancel from: Mathematik 1 Schalk Reniets Verlag"; "-------- common_nominator_p ----------------------------"; +"-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------"; "-------- reverse rewrite -------------------------------"; "-------- 'reverse-ruleset' cancel_p --------------------"; "-------- norm_Rational ---------------------------------"; @@ -1059,6 +1060,69 @@ if term2str t' = "(3 + x) * (3 - x) / ((3 - x) * (3 - x))" then () else error "rational.sml factout_ (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)"; +"-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------"; +"-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------"; +"-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------"; +val t = str2term ("123 = (a*x)/(b*x) + (c*x)/(d*x) + (e*x)/(f*x::real)"); +"-------- gcd_poly integration level 1: works on exact term"; +if NONE = cancel_p_ thy t then () else error "cancel_p_ works on exact fraction"; +if NONE = add_fraction_p_ thy t then () else error "add_fraction_p_ works on exact fraction"; + +"-------- gcd_poly integration level 2: picks out ONE appropriate subterm"; +val SOME (t', asm) = rewrite_set_ thy false cancel_p t; +if term2str t' = "123 = a * x / (b * x) + c * x / (d * x) + e / f" +then () else error "level 2, rewrite_set_ cancel_p: changed"; +val SOME (t', asm) = rewrite_set_ thy false add_fractions_p t; +if term2str t' = "123 = (b * c * x + a * d * x) / (b * d * x) + e * x / (f * x)" +then () else error "level 2, rewrite_set_ add_fractions_p: changed"; + +"-------- gcd_poly integration level 3: rewrites all appropriate subterms"; +val SOME (t', asm) = rewrite_set_ thy false cancel_p_rls t; +if term2str t' = "123 = a / b + c / d + e / f" +then () else error "level 3, rewrite_set_ cancel_p_rls: changed"; +val SOME (t', asm) = rewrite_set_ thy false common_nominator_p_rls t; (*CREATE add_fractions_p_rls*) +if term2str t' = "123 = (b * d * e * x + b * c * f * x + a * d * f * x) / (b * d * f * x)" +then () else error "level 3, rewrite_set_ add_fractions_p_rls: changed"; + +"-------- gcd_poly integration level 4: iteration cancel_p -- add_fraction_p"; +(* simpler variant *) +val testrls = append_rls "testrls" e_rls [Rls_ cancel_p, Rls_ add_fractions_p] +val SOME (t', asm) = rewrite_set_ thy false testrls t; +(*trace_rewrite := false; +# rls: testrls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x) +## rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x) +## rls: common_nominator_p on: 123 = a * x / (b * x) + c * x / (d * x) + e / f +## rls: cancel_p on: 123 = (b * c * x + a * d * x) / (b * d * x) + e / f +## rls: common_nominator_p on: 123 = (b * c + a * d) / (b * d) + e / f +## rls: cancel_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) +## rls: common_nominator_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) *) +if term2str t' = "123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)" +then () else error "level 4, rewrite_set_ *_p: changed"; + +(* complicated variant *) +val testrls_rls = append_rls "testrls_rls" e_rls [Rls_ cancel_p_rls, Rls_ common_nominator_p_rls]; +val SOME (t', asm) = rewrite_set_ thy false testrls_rls t; +(*# rls: testrls_rls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x) +## rls: cancel_p_rls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x) +### rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x) +### rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e / f +### rls: cancel_p on: 123 = a * x / (b * x) + c / d + e / f +### rls: cancel_p on: 123 = a / b + c / d + e / f +## rls: common_nominator_p_rls on: 123 = a / b + c / d + e / f +### rls: common_nominator_p on: 123 = a / b + c / d + e / f +### rls: common_nominator_p on: 123 = (b * c + a * d) / (b * d) + e / f +### rls: common_nominator_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) +## rls: cancel_p_rls on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) +### rls: cancel_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) +## rls: common_nominator_p_rls on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) +### rls: common_nominator_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) *) +if term2str t' = "123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)" +then () else error "level 4, rewrite_set_ *_p_rls: changed" + +"-------- gcd_poly integration level 5: cancel_p & add_fraction_p within norm_Rational"; +val SOME (t', asm) = rewrite_set_ thy false norm_Rational t; +if term2str t' = "123 = (a * d * f + b * c * f + b * d * e) / (b * d * f)" +then () else error "level 5, rewrite_set_ norm_Rational: changed" "-------- reverse rewrite -------------------------------"; "-------- reverse rewrite -------------------------------";