1.1 --- a/test/Tools/isac/Knowledge/rlang.sml Wed Sep 08 16:45:27 2010 +0200
1.2 +++ b/test/Tools/isac/Knowledge/rlang.sml Wed Sep 08 16:47:22 2010 +0200
1.3 @@ -57,7 +57,7 @@
1.4 (*EP*)
1.5 val fmz = ["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)",
1.6 "solveFor x","solutions L"];
1.7 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1.8 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.9 (*val p = e_pos';
1.10 val c = [];
1.11 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.12 @@ -88,7 +88,7 @@
1.13 (*EP*)
1.14 val fmz = ["equality ((x - 5)*(10 - x) = (3 - x)*(2 + x) + 2*(x + 20))",
1.15 "solveFor x","solutions L"];
1.16 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1.17 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.18 (*val p = e_pos';
1.19 val c = [];
1.20 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.21 @@ -118,7 +118,7 @@
1.22 (*EP*)
1.23 val fmz = ["equality ((2*x+5)^^^2+(3*x+4)^^^2=(13*x+2)*(x+1)+2*(15+14*x))",
1.24 "solveFor x","solutions L"];
1.25 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1.26 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.27 (*val p = e_pos';
1.28 val c = [];
1.29 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.30 @@ -148,7 +148,7 @@
1.31 (*EP*)
1.32 val fmz = ["equality ((2*x+1)^^^3+(x+1)^^^3=(2*x+1)^^^2*2*x+(x+2)^^^3+x^^^2)",
1.33 "solveFor x","solutions L"];
1.34 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1.35 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.36 (*val p = e_pos';
1.37 val c = [];
1.38 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.39 @@ -178,7 +178,7 @@
1.40 (*ER-2*)
1.41 val fmz = ["equality ((3*x+5)/18 - x/2 = -((3*x - 2)/9))",
1.42 "solveFor x","solutions L"];
1.43 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1.44 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.45 (*val p = e_pos'; val c = [];
1.46 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.47 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.48 @@ -220,7 +220,7 @@
1.49 (*ER-1*)
1.50 val fmz = ["equality ((17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0)",
1.51 "solveFor x","solutions L"];
1.52 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1.53 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.54 (*val p = e_pos';
1.55 val c = [];
1.56 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.57 @@ -260,7 +260,7 @@
1.58 (*ER-3*)
1.59 val fmz = ["equality (-2/x + 3/(2*x) - 4/(3*x) + 5/(4*x) + 6/(5*x) = 65/8)",
1.60 "solveFor x","solutions L"];
1.61 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
1.62 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
1.63 (*val p = e_pos';
1.64 val c = [];
1.65 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.66 @@ -300,7 +300,7 @@
1.67 (*ER-4*)
1.68 val fmz = ["equality ((x+3)/(2*x - 4)=3)",
1.69 "solveFor x","solutions L"];
1.70 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
1.71 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
1.72 (*val p = e_pos';
1.73 val c = [];
1.74 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.75 @@ -342,7 +342,7 @@
1.76 (*ER-5*)
1.77 val fmz = ["equality ((1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 = -1*(6*x)^^^2 + 29)",
1.78 "solveFor x","solutions L"];
1.79 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1.80 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.81 (*val p = e_pos';
1.82 val c = [];
1.83 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.84 @@ -388,7 +388,7 @@
1.85 (*ER-6*)
1.86 val fmz = ["equality ((5*x)/(x - 2) - x/(x+2)=4)",
1.87 "solveFor x","solutions L"];
1.88 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
1.89 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
1.90 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.91 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.92 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.93 @@ -425,7 +425,7 @@
1.94 (*ER-7*)
1.95 val fmz = ["equality (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)",
1.96 "solveFor x","solutions L"];
1.97 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
1.98 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
1.99 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.100 (*val nxt = ("Model_Problem",Model_Problem["rational","univariate","equation"*)
1.101 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.102 @@ -445,7 +445,7 @@
1.103 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.104 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.105 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; 040209 MGs norm_Rational*)
1.106 -(* val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"])*)
1.107 +(* val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"])*)
1.108 if f= Form' (FormKF (~1, EdUndef, 0, Nundef, "-6 * x + 5 * x ^^^ 2 = 0"))then()
1.109 else raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b";
1.110 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.111 @@ -511,7 +511,7 @@
1.112 (*ER-8*)
1.113 val fmz = ["equality (((x - 1)/(x+1)+1)/((x - 1)/(x+1) - (x+1)/(x - 1))=2)",
1.114 "solveFor x","solutions L"];
1.115 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
1.116 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
1.117
1.118 (*val p = e_pos'; val c = [];
1.119 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.120 @@ -551,7 +551,7 @@
1.121 (*ER-10*)
1.122 val fmz = ["equality (m1*v1+m2*v2=0)",
1.123 "solveFor m1","solutions L"];
1.124 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1.125 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.126
1.127 (*val p = e_pos'; val c = [];
1.128 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.129 @@ -580,7 +580,7 @@
1.130 (*ER-11*)
1.131 val fmz = ["equality (f=((w+u)/(w+v))*v0)",
1.132 "solveFor v","solutions L"];
1.133 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
1.134 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
1.135
1.136 (*val p = e_pos'; val c = [];
1.137 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.138 @@ -595,7 +595,7 @@
1.139 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.140 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.141 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.142 -(*nxt = Subproblem ("RatEq.thy",["univariate","equation"])) *)
1.143 +(*nxt = Subproblem ("RatEq",["univariate","equation"])) *)
1.144 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.145 (*val nxt =Model_Problem ["normalize","polynomial","univariate","equation"])*)
1.146 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.147 @@ -605,7 +605,7 @@
1.148 (*val nxt = ("Apply_Method",Apply_Method ["PolyEq","normalize_poly"])*)
1.149 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.150 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.151 -(*val nxt =Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
1.152 +(*val nxt =Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
1.153 if f = Form'
1.154 (FormKF
1.155 (~1,
1.156 @@ -659,7 +659,7 @@
1.157 (*ER-12*)
1.158 val fmz = ["equality (f=((w+u)/(w+v))*v0)",
1.159 "solveFor w","solutions L"];
1.160 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
1.161 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
1.162 (*val p = e_pos';val c = [];
1.163 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.164 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.165 @@ -707,7 +707,7 @@
1.166 (*ER-9*)
1.167 val fmz = ["equality (1/R=1/R1+1/R2)",
1.168 "solveFor R1","solutions L"];
1.169 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
1.170 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
1.171 (*val p = e_pos'; val c = [];
1.172 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.173 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.174 @@ -752,7 +752,7 @@
1.175 (*ER-13 + EO-11 ?!?*)
1.176 val fmz = ["equality (y^^^2=2*p*x)",
1.177 "solveFor p","solutions L"];
1.178 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1.179 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.180 (*val p = e_pos'; val c = [];
1.181 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.182 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.183 @@ -785,7 +785,7 @@
1.184 (*EO ??*)
1.185 val fmz = ["equality (y^^^2=2*p*x)",
1.186 "solveFor y","solutions L"];
1.187 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1.188 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.189 (*val p = e_pos';
1.190 val c = [];
1.191 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.192 @@ -818,7 +818,7 @@
1.193 (*EO-8*)
1.194 val fmz = ["equality (b^^^2*x^^^2 + a^^^2*y^^^2 = a^^^2*b^^^2)",
1.195 "solveFor x","solutions L"];
1.196 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1.197 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.198 (*val p = e_pos';
1.199 val c = [];
1.200 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.201 @@ -868,7 +868,7 @@
1.202 (*ER-14*)
1.203 val fmz = ["equality (A = (1/2)*(x1*(y2 - y3)+x2*(y3 - y1)+x3*(y1 - y2)))",
1.204 "solveFor x2","solutions L"];
1.205 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1.206 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.207 (*val p = e_pos';
1.208 val c = [];
1.209 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.210 @@ -907,7 +907,7 @@
1.211 (*EO*)
1.212 val fmz = ["equality (4*sqrt(4*x+1)=3*sqrt(7*x+2))",
1.213 "solveFor x","solutions L"];
1.214 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
1.215 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
1.216 (*val p = e_pos';
1.217 val c = [];
1.218 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.219 @@ -945,7 +945,7 @@
1.220 "Schalk II s.56 Bsp 68a (5*sqrt(x) - 1 = 7*sqrt(x) - 5)";
1.221 val fmz = ["equality (5*sqrt(x) - 1 = 7*sqrt(x) - 5)",
1.222 "solveFor x","solutions L"];
1.223 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
1.224 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
1.225 (*val p = e_pos';
1.226 val c = [];
1.227 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.228 @@ -1028,7 +1028,7 @@
1.229 (*EO-2*)
1.230 val fmz = ["equality (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))",
1.231 "solveFor x","solutions L"];
1.232 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
1.233 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
1.234
1.235 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.236 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.237 @@ -1039,7 +1039,7 @@
1.238 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.239 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.240 (*"13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"
1.241 --> Subproblem ("RootEq.thy", ["univariate", ...])*)
1.242 +-> Subproblem ("RootEq", ["univariate", ...])*)
1.243 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.244 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.245 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.246 @@ -1048,7 +1048,7 @@
1.247 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.248 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.249 (*"144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"
1.250 --> Subproblem ("RootEq.thy", ["univariate", ...])*)
1.251 +-> Subproblem ("RootEq", ["univariate", ...])*)
1.252 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.253 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.254 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.255 @@ -1078,7 +1078,7 @@
1.256 (*EO-3*)
1.257 val fmz = ["equality (sqrt(4*x+1) - sqrt(x+3) = sqrt(x - 2))",
1.258 "solveFor x","solutions L"];
1.259 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
1.260 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
1.261
1.262 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.263 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.264 @@ -1089,7 +1089,7 @@
1.265 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.266 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.267 (*4 + 5 * x + -2 * sqrt (3 + 13 * x + 4 * x ^^^ 2) = -2 + x"
1.268 --> Subproblem ("RootEq.thy", ["univariate", ...])*)
1.269 +-> Subproblem ("RootEq", ["univariate", ...])*)
1.270 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.271 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.272 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.273 @@ -1099,7 +1099,7 @@
1.274 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.275 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.276 (*"12 + 52 * x + 16 * x ^^^ 2 = 36 + x ^^^ 2 + 48 * x + 15 * x ^^^ 2"
1.277 --> Subproblem ("RootEq.thy", ["univariate", ...])*)
1.278 +-> Subproblem ("RootEq", ["univariate", ...])*)
1.279 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.280 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.281 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.282 @@ -1108,7 +1108,7 @@
1.283 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.284 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-24 + 4 * x = 0")) then ()
1.285 else raise error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 74a";
1.286 -(*-> ubproblem ("PolyEq.thy", ["degree_1", ...]*)
1.287 +(*-> ubproblem ("PolyEq", ["degree_1", ...]*)
1.288 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.289 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.290 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.291 @@ -1130,7 +1130,7 @@
1.292 (*EO-4*)
1.293 val fmz = ["equality (sqrt(x+12)+sqrt(x - 3) = sqrt(x + 32) - sqrt(5+x))",
1.294 "solveFor x","solutions L"];
1.295 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
1.296 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
1.297
1.298 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.299 (* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *)
1.300 @@ -1193,7 +1193,7 @@
1.301 (*EP*)
1.302 val fmz = ["equality ((6*x - 9)*(5*x+7) - (4*x+7)*(3*x - 6) = 429)",
1.303 "solveFor x","solutions L"];
1.304 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1.305 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.306 (*val p = e_pos';
1.307 val c = [];
1.308 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.309 @@ -1222,7 +1222,7 @@
1.310 (*ER-15*)
1.311 val fmz = ["equality ((x - 4)/(x+4) = (1 - x)/(1+x))",
1.312 "solveFor x","solutions L"];
1.313 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
1.314 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
1.315
1.316 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.317 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.318 @@ -1233,7 +1233,7 @@
1.319 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.320 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;
1.321 (*"(-4 + x) * (1 + x) = (1 + -1 * x) * (4 + x)"
1.322 --> Subproblem ("RatEq.thy", ["univariate", ...])*)
1.323 +-> Subproblem ("RatEq", ["univariate", ...])*)
1.324 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.325 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.326 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.327 @@ -1243,7 +1243,7 @@
1.328 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.329 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-8 + 2 * x ^^^ 2 = 0")) then ()
1.330 else raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 8a";
1.331 -(*-> Subproblem ("PolyEq.thy", ["polynomial", ...])*)
1.332 +(*-> Subproblem ("PolyEq", ["polynomial", ...])*)
1.333 (*
1.334 val Form' (FormKF (~1, EdUndef, 0, Nundef, str)) = f;
1.335 *)
1.336 @@ -1265,7 +1265,7 @@
1.337 "Schalk II s.66 Bsp 10b (1/(x^^^2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))";
1.338 val fmz = ["equality (1/(x^^^2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))",
1.339 "solveFor x","solutions L"];
1.340 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
1.341 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
1.342 (*val p = e_pos';
1.343 val c = [];
1.344 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.345 @@ -1307,7 +1307,7 @@
1.346 "Schalk II s.66 Bsp 20a (sqrt(29 - sqrt (x^^^2 - 9))=5)";
1.347 val fmz = ["equality (sqrt(29 - sqrt(x^^^2 - 9))=5)",
1.348 "solveFor x","solutions L"];
1.349 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
1.350 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
1.351 (*val p = e_pos';
1.352 val c = [];
1.353 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.354 @@ -1358,7 +1358,7 @@
1.355 *)
1.356 val fmz = ["equality (2*sqrt(261 - x) - sqrt(2+2*x)=sqrt(2)*sqrt(5 - 3*x))",
1.357 "solveFor x","solutions L"];
1.358 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
1.359 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
1.360
1.361 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.362 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.363 @@ -1401,7 +1401,7 @@
1.364 "Schalk II s.66 Bsp 28a (A=(c/d)*sqrt(4*a^^^2 - c^^^2))";
1.365 val fmz = ["equality (A=(c/d)*sqrt(4*a^^^2 - c^^^2))",
1.366 "solveFor a","solutions L"];
1.367 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
1.368 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
1.369 (*val p = e_pos';
1.370 val c = [];
1.371 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.372 @@ -1446,23 +1446,23 @@
1.373 "Schalk II s.68 Bsp 52b (1/(x - a+b)=1/x - 1/a + 1/b)";
1.374 val fmz = ["equality (1/(x - a+b)=1/x - 1/a + 1/b)",
1.375 "solveFor x","solutions L"];
1.376 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
1.377 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
1.378 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.379 (* val nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"])*)
1.380 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.381 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.382 -(*val nxt = ("Specify_Theory",Specify_Theory "RatEq.thy")*)
1.383 +(*val nxt = ("Specify_Theory",Specify_Theory "RatEq")*)
1.384 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.385 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.386 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.387 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.388 (*val p = ([3],Res)
1.389 val f="1 * (a * (b * x)) = (a * b + (a * x + -1 * (b * x))) * (b + (x + -1 * a)
1.390 -val nxt = Subproblem ("RatEq.thy",["univariate","equation"]))*)
1.391 +val nxt = Subproblem ("RatEq",["univariate","equation"]))*)
1.392 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.393 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.394 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.395 -(*val nxt = ("Specify_Theory",Specify_Theory "PolyEq.thy")*)
1.396 +(*val nxt = ("Specify_Theory",Specify_Theory "PolyEq")*)
1.397 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.398 (* nxt = Specify_Problem ["normalize","polynomial","univariate","equation"])*)
1.399 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.400 @@ -1471,7 +1471,7 @@
1.401 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.402 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; at introducing of MGs norm_Rational*)
1.403 (*val p = ([4,5],Res) val f ="b * a ^^^ 2 + -1 * a * b ^^^ 2 + (a ^^^ 2 + b ^^^ 2 + -2 * a * b) * x +\n(b + -1 * a) * x ^^^ 2 =\n0"))
1.404 -val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
1.405 +val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
1.406 if f = Form'
1.407 (FormKF
1.408 (~1,
1.409 @@ -1483,7 +1483,7 @@
1.410 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.411 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.412 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.413 -(*val nxt = ("Specify_Theory",Specify_Theory "PolyEq.thy")*)
1.414 +(*val nxt = ("Specify_Theory",Specify_Theory "PolyEq")*)
1.415 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.416 (*Specify_Problem["abcFormula","degree_2","polynomial","univariate","equation*)
1.417 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.418 @@ -1507,7 +1507,7 @@
1.419 (*----------------- Schalk II s.68 Bsp 56a ------------------------*)
1.420 "Schalk II s.68 Bsp 56a ((a+b*x)/(a-b*x) - (a - b*x)/(a+b*x)= (4*a*b)/(a^^^2 - b^^^2))";
1.421 val fmz = ["equality ((a+b*x)/(a-b*x) - (a - b*x)/(a+b*x)= (4*a*b)/(a^^^2 - b^^^2))","solveFor x","solutions L"];
1.422 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
1.423 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
1.424 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.425 (* val nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"]) *)
1.426 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.427 @@ -1595,7 +1595,7 @@
1.428 "Schalk II s.68 Bsp 61b (sqrt(x+a)+sqrt(b - x)=sqrt(a+b))";
1.429 val fmz = ["equality (sqrt(x+a)+sqrt(b - x)=sqrt(a+b))",
1.430 "solveFor x","solutions L"];
1.431 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
1.432 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
1.433
1.434 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.435 (* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"])*)
1.436 @@ -1657,7 +1657,7 @@
1.437 "Schalk II s.68 Bsp 62b (sqrt((x+a)^^^2+(x - 2*b)^^^2)=a+2*b)";
1.438 val fmz = ["equality (sqrt((x+a)^^^2+(x - 2*b)^^^2)=a+2*b)",
1.439 "solveFor x","solutions L"];
1.440 -val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
1.441 +val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
1.442 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.443 (*val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *)
1.444 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.445 @@ -1718,7 +1718,7 @@
1.446 (*EO-7*)
1.447 val fmz = ["equality ((2*x+1)*x^^^2 = 0)",
1.448 "solveFor x","solutions L"];
1.449 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1.450 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.451 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.452 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.453 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.454 @@ -1769,7 +1769,7 @@
1.455 (*EO-9*)
1.456 val fmz = ["equality ((a/2)^^^2 + (b/2)^^^2 = r^^^2)",
1.457 "solveFor a","solutions L"];
1.458 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1.459 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.460 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.461 (* Model_Problem ["normalize","polynomial","univariate","equation"])*)
1.462 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.463 @@ -1779,7 +1779,7 @@
1.464 (*val nxt = ("Apply_Method",Apply_Method ["PolyEq","normalize_poly"])*)
1.465 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.466 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.467 -(*val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"])*)
1.468 +(*val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"])*)
1.469 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.470 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.471 (*val nxt =Model_Problem ["sq_only","degree_2","polynomial","univariate","equation"])*)
1.472 @@ -1815,7 +1815,7 @@
1.473 (*EO-10*)
1.474 val fmz = ["equality (2*sqrt(r^^^2 - (u/2)^^^2) - u^^^2/(2*sqrt(r^^^2 - (u/2)^^^2))= 0)",
1.475 "solveFor u","solutions L"];
1.476 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1.477 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.478
1.479 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.480 (* Model_Problem ["normalize","root'","univariate","equation"])*)
1.481 @@ -1825,7 +1825,7 @@
1.482 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.483 (*val nxt = Apply_Method ["RootEq","norm_sq_root_equation"]) *)
1.484 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.485 -(*val nxt = Subproblem ("RootEq.thy",["univariate","equation"]))*)
1.486 +(*val nxt = Subproblem ("RootEq",["univariate","equation"]))*)
1.487 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.488 (*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *)
1.489 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.490 @@ -1836,7 +1836,7 @@
1.491 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.492 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.493 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.494 -(*val nxt = Subproblem ("RootEq.thy",["univariate","equation"]))*)
1.495 +(*val nxt = Subproblem ("RootEq",["univariate","equation"]))*)
1.496 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.497 (*val nxt = Model_Problem ["rational","univariate","equation"]) *)
1.498 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.499 @@ -1846,7 +1846,7 @@
1.500 (*val nxt = Apply_Method ["RootEq","solve_rat_equation"]) *)
1.501 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.502 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.503 -(*val nxt = Subproblem ("RootEq.thy",["univariate","equation"]))*)
1.504 +(*val nxt = Subproblem ("RootEq",["univariate","equation"]))*)
1.505 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.506 (*val nxt = Model_Problem ["normalize","polynomial","univariate","equation"]) *)
1.507 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.508 @@ -1856,7 +1856,7 @@
1.509 (*val nxt = Apply_Method ["PolyEq","normalize_poly"]) *)
1.510 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.511 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.512 -(*val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
1.513 +(*val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
1.514 if f = Form'
1.515 (FormKF
1.516 (~1,