1.1 --- a/src/sml/IsacKnowledge/Rational.ML	Tue Aug 29 10:07:24 2006 +0200
     1.2 +++ b/src/sml/IsacKnowledge/Rational.ML	Tue Aug 29 11:43:53 2006 +0200
     1.3 @@ -2772,9 +2772,9 @@
     1.4  cancels a single fraction consisting of two (uni- or multivariate)
     1.5  polynomials WN0609???SK[2] into another such a fraction; examples:
     1.6  
     1.7 -	   a^2 + (-1)*b^2        a + b
     1.8 +	   a^2 + -1*b^2         a + b
     1.9          -------------------- = ---------
    1.10 -	a^2 + (-2)*a*b + b^2   a + (-1)*b
    1.11 +	a^2 + -2*a*b + b^2     a + -1*b
    1.12  
    1.13          a^2    a
    1.14          --- = ---

     2.1 --- a/src/sml/ME/rewtools.sml	Tue Aug 29 10:07:24 2006 +0200
     2.2 +++ b/src/sml/ME/rewtools.sml	Tue Aug 29 11:43:53 2006 +0200
     2.3 @@ -184,7 +184,18 @@
     2.4  		     None => rew_once lim rts t apno rs'
     2.5  		   | Some (t',a') =>
     2.6  		     rew_once (lim-1) (rts @ [(t,r,(t',a'))]) t' Appl rrs');
     2.7 -
     2.8 +(*WN060829    | Rls_ rls => 
     2.9 +		(case rewrite_set_ thy true rls t of
    2.10 +		     None => rew_once lim rts t apno rs'
    2.11 +		   | Some (t',a') =>
    2.12 +		     if ro [] (t, t') then rew_once lim rts t apno rs'
    2.13 +		     else rew_once (lim-1) (rts@[(t,r,(t',a'))]) t' Appl rrs');
    2.14 +...lead to deriv = [] with make_polynomial.
    2.15 +THERE IS SOMETHING DIFFERENT beetween rewriting with the code above
    2.16 +and between rewriting with rewrite_set: with rules from make_polynomial and 
    2.17 +t = "(a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)" the actual code
    2.18 +leads to cycling  Rls_ order_mult_rls_..Rls_ discard_parentheses_..Rls_ order..
    2.19 +*)
    2.20      in rew_once (!lim_deriv) [] tt Noap rs end;
    2.21  (*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
    2.22  

     3.1 --- a/src/smltest/IsacKnowledge/rational.sml	Tue Aug 29 10:07:24 2006 +0200
     3.2 +++ b/src/smltest/IsacKnowledge/rational.sml	Tue Aug 29 11:43:53 2006 +0200
     3.3 @@ -33,6 +33,7 @@
     3.4  "-------- me Schalk I No.186 -------------------------------------";
     3.5  "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------";
     3.6  "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------";
     3.7 +"-------- investigate rulesets for cancel_p ----------------------";
     3.8  "-------- investigate format of factout_ and factout_p_ ----------";
     3.9  "-----------------------------------------------------------------";
    3.10  "-----------------------------------------------------------------";
    3.11 @@ -2039,10 +2040,65 @@
    3.12  val ((pt,p),_) = get_calc 1; show_pt pt;
    3.13  
    3.14  (*WN060823 cancel_p_ init_state does not terminate, see Rational.ML
    3.15 +  @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
    3.16  interSteps 1 ([1,2,1],Res);
    3.17  val ((pt,p),_) = get_calc 1; show_pt pt;
    3.18  *)
    3.19  
    3.20 +"-------- investigate rulesets for cancel_p ----------------------";
    3.21 +"-------- investigate rulesets for cancel_p ----------------------";
    3.22 +"-------- investigate rulesets for cancel_p ----------------------";
    3.23 +val thy = Rational.thy;
    3.24 +"---------------- (a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)";
    3.25 +val t = str2term "(a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)";
    3.26 +val tt = str2term "(1 * a + 1 * b) * (1 * a + -1 * b)"(*numerator only*);
    3.27 +"----- with rewrite_set_";
    3.28 +val Some (tt',asm) = rewrite_set_ thy false make_polynomial tt;
    3.29 +term2str tt'= "a ^^^ 2 + -1 * b ^^^ 2" (*true*);
    3.30 +val tt = str2term "((1 * a + -1 * b) * (1 * a + -1 * b))"(*denominator only*);
    3.31 +val Some (tt',asm) = rewrite_set_ thy false make_polynomial tt;
    3.32 +term2str tt' = "a ^^^ 2 + -2 * a * b + b ^^^ 2" (*true*);
    3.33 +"----- with make_deriv under rls before 060829";
    3.34 +(*
    3.35 +val {rules, rew_ord=(_,ro),...} =
    3.36 +    rep_rls (assoc_rls "make_polynomial");
    3.37 +val der = make_deriv thy Atools_erls rules ro None t;
    3.38 +print_depth 99; map (term2str o #1) der; print_depth 3;
    3.39 +print_depth 99; map (rule2str o #2) der; print_depth 3;
    3.40 +... did not terminate"*)
    3.41 +
    3.42 +(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
    3.43 +
    3.44 +(*-----
    3.45 +(term2str o #1 o the o (cancel_p_ Isac.thy)) t = 
    3.46 +"(1 * a + 1 * b) / (1 * a + -1 * b)";
    3.47 +val Some (tt, _) = factout_p_ Isac.thy t; term2str tt;
    3.48 +"(1 * a + 1 * b) * (1 * a + -1 * b) / ((1 * a + -1 * b) * (1 * a + -1 * b))";
    3.49 +
    3.50 +val deriv = make_deriv reverse_rewriting tt;
    3.51 +writeln (deriv2str deriv);
    3.52 +(*
    3.53 +if (term2str o #1 o #3 o last_elem) deriv = (*TODO!!!!!!........*)
    3.54 +   "(a ^^^ 2 + a * (-1 * b) + b * a + b * (-1 * b)) /\n\
    3.55 +   \(a ^^^ 2 + 2 * a * (-1 * b) + b ^^^ 2)" then ()
    3.56 +else raise error "rewtools.sml: make_deriv, expand_binoms changed";
    3.57 +*)
    3.58 +
    3.59 +"---------------- (1 * a + 1 * b) * (1 * a + -1 * b)";
    3.60 +val t = str2term "(1 * a + 1 * b) * (1 * a + -1 * b)";
    3.61 +
    3.62 +val deriv = make_deriv reverse_rewriting  t;
    3.63 +writeln (deriv2str deriv);
    3.64 +(term2str o #1 o #3 o last_elem) deriv;
    3.65 +
    3.66 +print_depth 99; map (term2str o #1) deriv; print_depth 3;
    3.67 +print_depth 9; map #2 deriv; print_depth 3;
    3.68 +-----*)
    3.69 +
    3.70 +
    3.71 +
    3.72 +
    3.73 +
    3.74  "-------- investigate format of factout_ and factout_p_ ----------";
    3.75  "-------- investigate format of factout_ and factout_p_ ----------";
    3.76  "-------- investigate format of factout_ and factout_p_ ----------";