1.1 --- a/src/Tools/isac/Test_Isac.thy	Tue Oct 05 09:17:48 2010 +0200
     1.2 +++ b/src/Tools/isac/Test_Isac.thy	Tue Oct 05 14:41:16 2010 +0200
     1.3 @@ -80,24 +80,26 @@
     1.4  val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
     1.5  Envir.subst_term subst (*pres?*);
     1.6  *}
     1.7 -ML {*print_depth 5*}
     1.8  use"../../../test/Tools/isac/Knowledge/poly.sml"; (*part.*)
     1.9 -
    1.10 -ML {*theory "Isac";
    1.11 -theory "Poly";
    1.12 -theory "Rational";
    1.13 -theory "Equation";
    1.14 +ML {*
    1.15 +the o (parse thy);
    1.16 +((parse thy)) "9 = 3 ^^^ 2";
    1.17 +(the o (parse thy)) "9 = 3 ^^^ 2";
    1.18 +(term_of o the o (parse thy)) "9 = 3 ^^^ 2";
    1.19 +Trueprop $ (term_of o the o (parse thy)) "9 = 3 ^^^ 2";
    1.20 +cterm_of (theory "Isac") (Trueprop $ (term_of o the o (parse thy)) "9 = 3 ^^^ 2");
    1.21 +(make_thm o (cterm_of (theory "Isac")))
    1.22 +  (Trueprop $ (term_of o the o (parse thy)) "9 = 3 ^^^ 2");
    1.23  *}
    1.24  
    1.25 -ML {*theory "Isac";
    1.26 -assoc_thy;
    1.27 -cancel;
    1.28 -assoc_thy "Poly";
    1.29 -assoc_thy "Rational";
    1.30 -assoc_thy "Equation";
    1.31 +ML {*
    1.32 +str2term "1 < (2 :: real)";
    1.33  *}
    1.34  
    1.35  use"../../../test/Tools/isac/Knowledge/rational.sml"
    1.36 +
    1.37 +ML {*111*}
    1.38 +
    1.39  (*
    1.40  	use"equation.sml";
    1.41   	use"root.sml";

     2.1 --- a/test/Tools/isac/Knowledge/rational.sml	Tue Oct 05 09:17:48 2010 +0200
     2.2 +++ b/test/Tools/isac/Knowledge/rational.sml	Tue Oct 05 14:41:16 2010 +0200
     2.3 @@ -482,6 +482,8 @@
     2.4  val e186a = the (rewrite_set thy' false "cancel" e186a');
     2.5    is_expanded (parse_rat "14 * x * y");
     2.6    is_expanded (parse_rat "x * y");
     2.7 +if e186a = ("14 / 1", "[\"y * x ~= 0\"]") then ()
     2.8 +else error "rational.sml cancel Schalk e186a";
     2.9  
    2.10  writeln("b)");
    2.11  val e186b'="(60 * a * b) / ( 15 * a  * b )";
    2.12 @@ -489,9 +491,10 @@
    2.13  writeln("c)");
    2.14  val e186c'="(144 * a^^^2 * b * c) / (12 * a * b * c )";
    2.15  val e186c = (the (rewrite_set thy' false "cancel" e186c'))
    2.16 -    handle e => OldGoals.OldGoals.print_exn e;
    2.17 +    handle e => OldGoals.print_exn e;
    2.18  val t = (term_of o the o (parse thy)) e186c';
    2.19 -atomt t;
    2.20 +if e186c = ("12 * a / 1", "[\"12 * (c * (b * a)) ~= 0\"]") then ()
    2.21 +else error "rational.sml cancel Schalk e186c";
    2.22  
    2.23  writeln ("example 187:");
    2.24  writeln("a)");
    2.25 @@ -501,21 +504,24 @@
    2.26  val e187b'="(8 * x^^^2 * y * z ) / (18 * x * y^^^2 * z )";
    2.27  val e187b = the (rewrite_set thy' false "cancel" e187b');
    2.28  writeln("c)");
    2.29 -val e187c'="(9 * x^^^5 * y^^^2 * z^^^4) / (15 * x^^^6 * y^^^3 * z )";(*SRC*)
    2.30 -val e187c = the (rewrite_set thy' false "cancel" e187c');
    2.31 +val e187d'="(9 * x^^^5 * y^^^2 * z^^^4) / (15 * x^^^6 * y^^^3 * z )";(*SRC*)
    2.32 +val e187d = the (rewrite_set thy' false "cancel" e187d');
    2.33 +if e187d = ("3 * z ^^^ 3 / (5 * (y * x))",
    2.34 +            "[\"3 * (z * (y ^^^ 2 * x ^^^ 5)) ~= 0\"]") then ()
    2.35 +else error "rational.sml cancel Schalk e186d";
    2.36  
    2.37 -"example 188:";
    2.38 +writeln "example 188:";
    2.39  val e188a'="(-8 + 8 * x) / (-9 + 9 * x)";(*SRC*)
    2.40  val e188a = the (rewrite_set thy' false "cancel" e188a');
    2.41    is_expanded (parse_rat "8 * x + -8");
    2.42  (* e188a = ("8 / 9",["not ((-1) + x = 0)"]) then () 13.3.03*)
    2.43 -if e188a = ("8 / 9",["-1 + x ~= 0"]) then ()
    2.44 +if e188a = ("8 / 9", "[\"-1 + x ~= 0\"]") then ()
    2.45  else error "rational.sml: e188a new behaviour";
    2.46 -val SOME (t,_) = rewrite_set thy' false mp 
    2.47 -			     "(8*((-1) + x))/(9*((-1) + x))";
    2.48 +
    2.49 +val SOME (t,_) = rewrite_set thy' false mp "(8*((-1) + x))/(9*((-1) + x))";
    2.50  writeln("b)");
    2.51  val e188b'="(-15 + 5 * x) / (-18 + 6 * x)";(*SRC*)
    2.52 -val SOME (t,_) = rewrite_set thy' false "cancel" e188b';
    2.53 +val SOME (t, asm) = rewrite_set thy' false "cancel" e188b';
    2.54  t = "5 / 6" (*true*);
    2.55  writeln("c)");
    2.56  
    2.57 @@ -577,7 +583,7 @@
    2.58  then () else error "rational.sml: 'e192b' new behaviour";
    2.59  (*^^^ works with MG's simplifier vvv*)
    2.60  val t =str2term"((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
    2.61 -val SOME (t',_) = rewrite_set_ Isac.thy false make_polynomial t;
    2.62 +val SOME (t',_) = rewrite_set_ thy false make_polynomial t;
    2.63  if term2str t' = "(7 * x ^^^ 3 + -1 * x ^^^ 2 * y) / (7 * x * y ^^^ 2 + -1 * y ^^^ 3)" then () else error "rational.sml: 'e192b'MG new behaviour";
    2.64  
    2.65  
    2.66 @@ -597,9 +603,9 @@
    2.67  -------------------*)
    2.68  
    2.69  val wn01 = "(-25 + 9*x^^^2)/(5 + 3*x)";
    2.70 -val SOME (t,_) = rewrite_set thy' false "cancel" wn01;
    2.71 +val SOME (t, asm) = rewrite_set thy' false "cancel" wn01;
    2.72  (* t = "((-5) + 3 * x) / 1" then () WN.13.3.03*)
    2.73 -if t = "(-5 + 3 * x) / 1" then ()
    2.74 +if t = "(-5 + 3 * x) / 1" andalso asm = "[\"5 + 3 * x ~= 0\"]" then ()
    2.75  else error "rational.sml: new behav. in cancel wn01";
    2.76  
    2.77  
    2.78 @@ -615,6 +621,8 @@
    2.79  writeln("b)");
    2.80  val e204b'="5 / x + -3 / x + -1 / x";
    2.81  val e204b = the (rewrite_set thy' false "common_nominator_p" e204b');
    2.82 +if e204b = ("1 / x", "[]") then ()
    2.83 +else error "rational.sml common_nominator_p example e204b";
    2.84  
    2.85  writeln ("example 205:");
    2.86  writeln("a)");
    2.87 @@ -623,6 +631,8 @@
    2.88  writeln("b)");
    2.89  val e205b'="((5 * x + 2) / 3) + ((-2 * x + 1) / 3)";
    2.90  val e205b = the (rewrite_set thy' false "common_nominator_p" e205b');
    2.91 +if e205b = ("(1 + x) / 1", "[]") then ()
    2.92 +else error "rational.sml common_nominator_p example e204b";
    2.93  
    2.94  writeln ("example 206:");
    2.95  writeln("a)");
    2.96 @@ -697,6 +707,8 @@
    2.97  writeln ("example 218:"); 
    2.98  val e218'="((9 * a^^^3 - 5 * a^^^2 + 2 * a + 8) / (108 * a^^^4)) + ((-5 * a + 3 * a^^^2 + 4) / (8 * a^^^3)) + ((-261 * a^^^3 + 19 * a^^^2 + -112 * a + 16) / (216 * a^^^4))";
    2.99  val e218 = the (rewrite_set thy' false "common_nominator" e218'); 
   2.100 +if e218 = ("(16 - 63 * a ^^^ 2 - 81 * a ^^^ 3) / (108 * a ^^^ 4)", "[]") then ()
   2.101 +else error "rationa.sml common_nominator example e218";
   2.102  
   2.103  writeln ("example 219:");
   2.104  writeln("a)");
   2.105 @@ -705,6 +717,8 @@
   2.106  writeln("b)");
   2.107  val e219b'="((1) / (x + 1)) + ((1) / (x + 2)) + ((-2) / (x + 3))";
   2.108  val e219b = the (rewrite_set thy' false "common_nominator" e219b'); 
   2.109 +if e219b = ("(5 + 3 * x) / (6 + 11 * x + 6 * x ^^^ 2 + x ^^^ 3)", "[]") then ()
   2.110 +else error "rationa.sml common_nominator example e219b";
   2.111  
   2.112  writeln ("example 220:");
   2.113  writeln("a)");
   2.114 @@ -837,14 +851,14 @@
   2.115  writeln ("example stiefel:");
   2.116  val est1'="(7) / (-14) + (-2) / (4)";
   2.117  val est1 = the (rewrite_set thy' false "common_nominator_p" est1');
   2.118 -if est1 = ("-1 / 1",[]) then ()
   2.119 +if est1 = ("-1 / 1", "[]") then ()
   2.120  else error "new behaviour in rational.sml: est1'";
   2.121      
   2.122  val t = (term_of o the o (parse thy))
   2.123  "(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
   2.124  val SOME (t',_) = factout_ thy t;
   2.125 -term2str t';
   2.126 -"(3 + x) * (3 - x) / ((3 - x) * (3 - x))";
   2.127 +if term2str t' = "(3 + x) * (3 - x) / ((3 - x) * (3 - x))" then ()
   2.128 +else error "rational.sml factout_ (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
   2.129      
   2.130  
   2.131  "-------- reverse rewrite -------------------------------";
   2.132 @@ -862,54 +876,65 @@
   2.133  
   2.134  (*normal_form produces the result in ONE step*)
   2.135    val SOME (t',_) = nor t;
   2.136 -  term2str t';
   2.137 +if term2str t' = "(3 - x) / (3 + x)" then ()
   2.138 +else error "rational.sml normal_form (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
   2.139  
   2.140  (*initialize the interpreter state used by the 'me'*)
   2.141    val (t,_,revsets,_) = ini t;
   2.142  
   2.143  (*find the rule 'r' to apply to term 't'*)
   2.144 -  val SOME r = nex revsets t;
   2.145 -  (*val r = Thm ("sym_#mult_2_3","6 = 2 * 3") : rule*)
   2.146 +  val SOME (r as (Thm (str, thm))) = nex revsets t;
   2.147 +if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))"
   2.148 +   andalso string_of_thm thm = 
   2.149 +           (string_of_thm o make_thm o (cterm_of (theory "Isac")))
   2.150 +               (Trueprop $ (term_of o the o (parse thy)) "9 = 3 ^^^ 2") then ()
   2.151 +else error "rational.sml next_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
   2.152 +(* before Isa02->09-2 was not checked automatically, ?was different?:
   2.153 +val SOME r = nex revsets t;
   2.154 +val r = Thm ("sym_#mult_2_3","6 = 2 * 3") : rule*)
   2.155  
   2.156 -(*check, if the rule 'r' applied by the user to 't' belongs to the ruleset;
   2.157 +(* check, if the rule 'r' applied by the user to 't' belongs to the ruleset;
   2.158    if the rule is OK, the term resulting from applying the rule is returned,too;
   2.159    there might be several rule applications inbetween,
   2.160 -  which are listed after the head in reverse order*)
   2.161 -  val (r,(t,asm))::_ = loc revsets t r;
   2.162 -  term2str t;
   2.163 -  "(9 - x ^^^ 2) / (3 ^^^ 2 + 6 * x + x ^^^ 2)";
   2.164 +  which are listed after the head in reverse order *)
   2.165 +  val (r, (t, asm))::_ = loc revsets t r;
   2.166 +if term2str t = "(9 - x ^^^ 2) / (3 ^^^ 2 + 6 * x + x ^^^ 2)" andalso asm = []
   2.167 +then () 
   2.168 +else error "rational.sml locate_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
   2.169  
   2.170 -(*find the next rule to apply*)
   2.171 -  val SOME r = nex revsets t;
   2.172 -  (*val r = Thm ("sym_#power_3_2","9 = 3 ^^^ 2") : rule*)
   2.173 +(* find the next rule to apply *)
   2.174 +  val SOME (r as (Thm (str, thm))) = nex revsets t;
   2.175 +if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))" andalso
   2.176 +   string_of_thm thm = (string_of_thm o make_thm o (cterm_of (theory "Isac")))
   2.177 +                (Trueprop $ (term_of o the o (parse thy)) "9 = 3 ^^^ 2") then ()
   2.178 +else error "rational.sml next_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
   2.179  
   2.180  (*check the next rule*)
   2.181 -  val (r,(t,asm))::_ = loc revsets t r;
   2.182 -  term2str t;
   2.183 -  "(3 ^^^ 2 - x ^^^ 2) / (3 ^^^ 2 + 6 * x + x ^^^ 2)";
   2.184 +  val (r, (t, asm)) :: _ = loc revsets t r;
   2.185 +if term2str t = "(3 ^^^ 2 - x ^^^ 2) / (3 ^^^ 2 + 6 * x + x ^^^ 2)" then ()
   2.186 +else error "rational.sml locate_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2) II";
   2.187  
   2.188  (*find and check the next rules, rewrite*)
   2.189    val SOME r = nex revsets t;
   2.190    val (r,(t,asm))::_ = loc revsets t r;
   2.191 -  term2str t;
   2.192 -  "(3 ^^^ 2 - x ^^^ 2) / (3 ^^^ 2 + 2 * 3 * x + x ^^^ 2)";
   2.193 +if term2str t = "(3 ^^^ 2 - x ^^^ 2) / (3 ^^^ 2 + 2 * 3 * x + x ^^^ 2)" then ()
   2.194 +else error "rational.sml locate_rule II";
   2.195  
   2.196    val SOME r = nex revsets t;
   2.197    val (r,(t,asm))::_ = loc revsets t r;
   2.198 -  term2str t;
   2.199 -  "(3 - x) * (3 + x) / (3 ^^^ 2 + 2 * 3 * x + x ^^^ 2)";
   2.200 +if term2str t = "(3 - x) * (3 + x) / (3 ^^^ 2 + 2 * 3 * x + x ^^^ 2)" then ()
   2.201 +else error "rational.sml next_rule II";
   2.202  
   2.203    val SOME r = nex revsets t;
   2.204    val (r,(t,asm))::_ = loc revsets t r;
   2.205 -  term2str t;
   2.206 -  "(3 - x) * (3 + x) / ((3 + x) * (3 + x))";
   2.207 +if term2str t = "(3 - x) * (3 + x) / ((3 + x) * (3 + x))" then ()
   2.208 +else error "rational.sml next_rule III";
   2.209  
   2.210    val SOME r = nex revsets t;
   2.211 -  val (r,(t,asm))::_ = loc revsets t r;
   2.212 +  val (r, (t, asm)) :: _ = loc revsets t r;
   2.213    val ss = term2str t;
   2.214 -  if ss = "(3 - x) / (3 + x)" then ()
   2.215 -  else error "rational.sml: new behav. in rev-set cancel";
   2.216 -  terms2str asm; 
   2.217 +if ss = "(3 - x) / (3 + x)" andalso terms2str asm = "[\"3 + x ~= 0\"]" then ()
   2.218 +else error "rational.sml: new behav. in rev-set cancel";
   2.219  
   2.220  
   2.221  "-------- 'reverse-ruleset' cancel_p --------------------";
   2.222 @@ -979,6 +1004,12 @@
   2.223  val SOME (t',_) = rewrite_set_ thy false powers_erls t; term2str t';
   2.224  "True";
   2.225  val t = str2term "1 < 2";
   2.226 +
   2.227 +trace_rewrite:=true; tracing "=== begin 1<2";
   2.228 +rewrite_set_ thy false powers_erls t; term2str t';
   2.229 +trace_rewrite:=false; tracing "=== end 1<2";
   2.230 +
   2.231 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
   2.232  val SOME (t',_) = rewrite_set_ thy false powers_erls t; term2str t';
   2.233  "True";
   2.234  val t = str2term "(6*x)^^^2";
   2.235 @@ -2057,3 +2088,6 @@
   2.236  "   t_t)"
   2.237  );
   2.238  val --------------------------------------------------++ = "22222";
   2.239 +
   2.240 +
   2.241 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)