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  *}