1.1 --- a/test/Tools/isac/Knowledge/poly.sml	Fri Oct 01 17:27:55 2010 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/poly.sml	Fri Oct 01 18:25:06 2010 +0200
     1.3 @@ -5,7 +5,6 @@
     1.4  12345678901234567890123456789012345678901234567890123456789012345678901234567890
     1.5          10        20        30        40        50        60        70        80
     1.6  *)
     1.7 -
     1.8  (*******************************************************************************
     1.9    WN060104 'SPB' came into 'exp_IsacCore_Simp_Poly_Book.xml'
    1.10  	   'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml'
    1.11 @@ -30,8 +29,6 @@
    1.12  "--------------------------------------------------------";
    1.13  "--------------------------------------------------------";
    1.14  
    1.15 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    1.16 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
    1.17  
    1.18  "-------- check is'_polyexp is_polyexp ------------------";
    1.19  "-------- check is'_polyexp is_polyexp ------------------";
    1.20 @@ -80,9 +77,7 @@
    1.21  val scr_expand_binoms =
    1.22  "Script Expand_binoms t_t = t_t";
    1.23  *)
    1.24 -val ---------------------------------------------- = "11111";
    1.25  parse thy scr_expand_binoms;
    1.26 -val ---------------------------------------------- = "22222";
    1.27  
    1.28  
    1.29  "-------- investigate (new) uniary minus ----------------";
    1.30 @@ -163,8 +158,13 @@
    1.31  "-------- fun is_multUnordered --------------------------";
    1.32  "-------- fun is_multUnordered --------------------------";
    1.33  val thy = theory "Isac";
    1.34 -(* 100928 trace_rewrite gives the following (first occurring) difference:
    1.35 -:
    1.36 +"===== works for a simple example, see rewrite.sml -- fun app_rev ===";
    1.37 +val t = str2term "x^^^2 * x";
    1.38 +val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
    1.39 +if term2str t' = "x * x ^^^ 2" then ()
    1.40 +else error "poly.sml Poly.is'_multUnordered doesn't work";
    1.41 +
    1.42 +(* 100928 trace_rewrite shows the first occurring difference in 267b:
    1.43  ###  rls: order_mult_ on: 5 * x ^^^ 2 * (2 * x ^^^ 7) + 5 * x ^^^ 2 * 3 + (6 * x ^^^ 7 + 9) + (-1 * (3 * x ^^^ 5 * (6 * x ^^^ 4)) + -1 * (3 * x ^^^ 5 * -1) +
    1.44   (-48 * x ^^^ 4 + 8))
    1.45  ######  rls: e_rls-is_multUnordered on: p is_multUnordered
    1.46 @@ -190,18 +190,9 @@
    1.47                            Const ("True", _))) => ()
    1.48    | _ => error "poly.sml diff. eval_is_multUnordered";
    1.49  
    1.50 -"----- rewrite_set_ ---";
    1.51 -val SOME (t, _) = rewrite_set_ thy true order_mult_ tm;
    1.52 -
    1.53 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    1.54 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
    1.55 -
    1.56 -
    1.57 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    1.58 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
    1.59 -
    1.60 -(*===== inhibit exn ?===========================================================
    1.61 -
    1.62 +"----- rewrite_set_ STILL DIDN'T WORK";
    1.63 +val SOME (t, _) = rewrite_set_ thy true order_mult_ t;
    1.64 +term2str t;
    1.65  
    1.66  
    1.67  "-------- examples from textbook Schalk I ---------------";
    1.68 @@ -337,7 +328,6 @@
    1.69  if term2str t = "d ^^^ 3" then ()
    1.70  else error "poly.sml: diff.behav. in make_polynomial 14";
    1.71  
    1.72 -
    1.73  (*---------------------------------------------------------------------*)
    1.74  (*------------------ Bsple bei denen es Probleme gibt------------------*)
    1.75  (*---------------------------------------------------------------------*)
    1.76 @@ -432,8 +422,8 @@
    1.77  "-------- Script 'simplification for_polynomials' -------";
    1.78  "-------- Script 'simplification for_polynomials' -------";
    1.79  val str = 
    1.80 -"Script SimplifyScript (t_::real) =                \
    1.81 -\  ((Rewrite_Set norm_Poly False) t_)";
    1.82 +"Script SimplifyScript (t_t::real) =                \
    1.83 +\  ((Rewrite_Set norm_Poly False) t_t)";
    1.84  val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
    1.85  atomty sc;
    1.86  
    1.87 @@ -445,6 +435,9 @@
    1.88  	   \- (3*x^^^5 + 8) * (6*x^^^4 - 1))",
    1.89  	   "normalform N"];
    1.90  "-----0 ---";
    1.91 +(*===== inhibit exn ============================================================
    1.92 +GOON
    1.93 +
    1.94  case refine fmz ["polynomial","simplification"]of
    1.95      [Matches (["polynomial", "simplification"], _)] => ()
    1.96    | _ => error "poly.sml diff.behav. in check pbl, refine";
    1.97 @@ -564,7 +557,6 @@
    1.98  val t1 = str2term "2 * b + (3 * a + 3 * b)";
    1.99  val t2 = str2term "3 * a + (2 * b + 3 * b)";
   1.100  
   1.101 -
   1.102  ===== inhibit exn ?===========================================================*)
   1.103  
   1.104