1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/systest/subp-rooteq.sml Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,492 @@
1.4 +(* use"tests/subp-rooteq.sml";
1.5 + use"subp-rooteq.sml";
1.6 + *)
1.7 +
1.8 +
1.9 +"---------------- miniscript with mini-subpbl -------------";
1.10 +"---------------- solve_linear as rootpbl -----------------";
1.11 +"---------------- solve_plain_square as rootpbl -----------";
1.12 +"---------------- root-eq + subpbl: solve_linear ----------";
1.13 +"---------------- root-eq + subpbl: solve_plain_square ----";
1.14 +"---------------- root-eq + subpbl: no_met: linear ----";
1.15 +"---------------- root-eq + subpbl: no_met: square ----";
1.16 +"---------------- no_met in rootpbl -> linear --------------";
1.17 +
1.18 +
1.19 +
1.20 +
1.21 +
1.22 +"---------------- miniscript with mini-subpbl -------------";
1.23 +"---------------- miniscript with mini-subpbl -------------";
1.24 +"---------------- miniscript with mini-subpbl -------------";
1.25 +val fmz = ["equality (x+1=2)",
1.26 + "solveFor x","errorBound (eps=0)",
1.27 + "solutions L"];
1.28 +val (dI',pI',mI') =
1.29 + ("Test.thy",["sqroot-test","univariate","equation","test"],
1.30 + ("Test.thy","squ-equ-test-subpbl1"));
1.31 + val Script sc = (#scr o get_met) ("Test.thy","squ-equ-test-subpbl1");
1.32 + (writeln o term2str) sc;
1.33 +
1.34 +val p = e_pos'; val c = [];
1.35 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.36 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
1.37 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.38 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.39 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.40 +(*val nxt = ("Add_Find",Add_Find "solutions L") : string * mstep*)
1.41 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.42 +(*val nxt = ("Specify_Domain",Specify_Domain "Test.thy") : string * mstep*)
1.43 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.44 +(*("Specify_Problem",Specify_Problem ["sqroot-test","univariate","equation"]*)
1.45 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.46 +(*("Specify_Method",Specify_Method ("Test.thy","squ-equ-test-subpbl1"))*)
1.47 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.48 +(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","squ-equ-test-subpbl1"*)
1.49 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.50 +(*val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation") : string * mstep*)
1.51 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.52 +(*val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify")*)
1.53 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.54 +(*val nxt = ("Subproblem",Subproblem ("Test.thy",[#,#,#])) : string * mstep
1.55 + ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.56 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.57 + p;
1.58 + writeln(istate2str (get_istate pt ([3],Frm)));
1.59 +(*val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"]*)
1.60 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.61 +(*val nxt = ("Add_Given",Add_Given "equality (-1 + x = 0)") *)
1.62 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.63 +(*val nxt = ("Add_Given",Add_Given "solveFor x") : string * mstep*)
1.64 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.65 +(*val nxt = ("Add_Find",Add_Find "solutions x_i") : string * mstep*)
1.66 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.67 +(*val nxt = ("Specify_Domain",Specify_Domain "Test.thy")*)
1.68 +
1.69 +
1.70 +(*-----30.9.02----------------------------------------------*)
1.71 +
1.72 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.73 +(*("Specify_Problem",Specify_Problem ["linear","univariate","equation"])*)
1.74 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.75 +(*val nxt = ("Specify_Method",Specify_Method ("Test.thy","solve_linear"))*)
1.76 + val Script sc = (#scr o get_met) ("Test.thy","solve_linear");
1.77 + (writeln o term2str) sc;
1.78 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.79 +(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","solve_linear"))*)
1.80 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.81 +(*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)
1.82 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.83 +(*val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify")*)
1.84 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.85 +(*val nxt = ("Check_Postcond",Check_Postcond ["linear","univariate","eq*)
1.86 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.87 + p;
1.88 + writeln(istate2str (get_istate pt ([3],Res)));
1.89 +
1.90 +(*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
1.91 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.92 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.93 +val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
1.94 +if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()
1.95 +else raise error "new behaviour in test: miniscript with mini-subpbl";
1.96 +
1.97 +
1.98 +"---------------- solve_linear as rootpbl -----------------";
1.99 +"---------------- solve_linear as rootpbl -----------------";
1.100 +"---------------- solve_linear as rootpbl -----------------";
1.101 +val fmz = ["equality (1+-1*2+x=0)",
1.102 + "solveFor x","solutions L"];
1.103 +val (dI',pI',mI') =
1.104 + ("Test.thy",["linear","univariate","equation","test"],
1.105 + ("Test.thy","solve_linear"));
1.106 +val p = e_pos'; val c = [];
1.107 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.108 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
1.109 +(*val nxt = ("Add_Given",Add_Given "equality (x + #1 + #-1 * #2 = #0)")*)
1.110 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.111 +(*val nxt = ("Add_Given",Add_Given "solveFor x") : string * mstep*)
1.112 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.113 +(*val nxt = ("Add_Find",Add_Find "solutions L") : string * mstep*)
1.114 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.115 +(*val nxt = ("Specify_Domain",Specify_Domain "Test.thy") : string * mstep*)
1.116 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.117 +(*val nxt = ("Specify_Problem",Specify_Problem ["univariate","equation"])*)
1.118 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.119 +(*val nxt = ("Specify_Method",Specify_Method ("Test.thy","solve_linear"))*)
1.120 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.121 +(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","solve_linear"))*)
1.122 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.123 +(*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#1 + #-1 * #2 + x = #0"))
1.124 + val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)
1.125 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.126 +(*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = #0 + #-1 * (#1 + #-1 * #2)"))
1.127 + val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify") : string * mstep*)
1.128 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.129 +(*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = #1")) : mout val nxt = ("Check_Postcond",Check_Postcond ["univariate","equation"])*)
1.130 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.131 +(*val f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = #1]")) : mout
1.132 + val nxt = ("End_Proof'",End_Proof') : string * mstep*)
1.133 +val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
1.134 +if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()
1.135 +else raise error "new behaviour in test: solve_linear as rootpbl";
1.136 +
1.137 +
1.138 +"---------------- solve_plain_square as rootpbl -----------";
1.139 +"---------------- solve_plain_square as rootpbl -----------";
1.140 +"---------------- solve_plain_square as rootpbl -----------";
1.141 +val fmz = ["equality (9 + -1 * x ^^^ 2 = 0)","solveFor x",
1.142 + "solutions L"];
1.143 +val (dI',pI',mI') =
1.144 + ("Test.thy",["plain_square","univariate","equation","test"],
1.145 + ("Test.thy","solve_plain_square"));
1.146 +val p = e_pos'; val c = [];
1.147 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.148 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
1.149 +
1.150 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.151 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.152 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.153 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.154 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.155 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.156 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.157 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.158 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.159 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.160 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.161 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.162 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.163 +val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
1.164 +if snd nxt=End_Proof' andalso res="[x = -3, x = 3]" then ()
1.165 +else raise error "new behaviour in test: solve_plain_square as rootpbl";
1.166 +
1.167 +
1.168 +
1.169 +
1.170 +"---------------- root-eq + subpbl: solve_linear ----------";
1.171 +"---------------- root-eq + subpbl: solve_linear ----------";
1.172 +"---------------- root-eq + subpbl: solve_linear ----------";
1.173 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.174 + "solveFor x","errorBound (eps=0)",
1.175 + "solutions L"];
1.176 +val (dI',pI',mI') =
1.177 + ("Test.thy",["sqroot-test","univariate","equation","test"],
1.178 + ("Test.thy","square_equation1"));
1.179 +val p = e_pos'; val c = [];
1.180 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.181 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
1.182 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.183 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.184 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.185 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.186 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.187 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.188 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.189 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.190 +(*"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"
1.191 +square_equation_left*)
1.192 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.193 +(*"9 + 4 * x = (sqrt x + sqrt (5 + x)) ^^^ 2"
1.194 +Test_simplify*)
1.195 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.196 +(*"9 + 4 * x = 5 + (2 * x + 2 * sqrt (x ^^^ 2 + 5 * x))"
1.197 +rearrange_assoc*)
1.198 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.199 +(*"9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)"
1.200 +isolate_root*)
1.201 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.202 +(*"sqrt (x ^^^ 2 + 5 * x) = (5 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)"
1.203 +Test_simplify*)
1.204 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.205 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.206 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.207 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.208 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.209 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.210 +(*"x ^^^ 2 + 5 * x + -1 * (4 + (x ^^^ 2 + 4 * x)) = 0"*)
1.211 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.212 +(*"-4 + x = 0"
1.213 + val nxt =("Subproblem",Subproblem ("Test.thy",["linear","univariate"...*)
1.214 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.215 +(*val nxt =("Model_Problem",Model_Problem ["linear","univariate"...*)
1.216 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.217 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.218 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.219 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.220 +(*val nxt = ("Specify_Domain",Specify_Domain "Test.thy")*)
1.221 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.222 +(*("Specify_Problem",Specify_Problem ["linear","univariate","equation"])*)
1.223 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.224 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.225 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.226 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.227 +(*"x = 0 + -1 * -4", nxt Test_simplify*)
1.228 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.229 +(*"x = 4", nxt Check_Postcond ["linear","univariate","equation","test"]*)
1.230 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.231 +(*"[x = 4]", nxt Check_elementwise "Assumptions"*)
1.232 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.233 +(*"[]", nxt Check_Postcond ["sqroot-test","univariate","equation","test"]*)
1.234 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.235 +val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
1.236 +if (snd nxt)=End_Proof' andalso res="[x = 4]" then ()
1.237 +else raise error "new behaviour in test: root-eq + subpbl: solve_linear";
1.238 +
1.239 +
1.240 +
1.241 +"---------------- root-eq + subpbl: solve_plain_square ----";
1.242 +"---------------- root-eq + subpbl: solve_plain_square ----";
1.243 +"---------------- root-eq + subpbl: solve_plain_square ----";
1.244 +val fmz = ["equality (sqrt(5+x)+sqrt(5-x)=sqrt 18)",
1.245 + "solveFor x","errorBound (eps=0)",
1.246 + "solutions L"];
1.247 +val (dI',pI',mI') =
1.248 + ("Test.thy",["sqroot-test","univariate","equation","test"],
1.249 + ("Test.thy","square_equation2"));
1.250 +val Script sc = (#scr o get_met) ("Test.thy","square_equation2");
1.251 +(writeln o term2str) sc;
1.252 +
1.253 +val p = e_pos'; val c = [];
1.254 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.255 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
1.256 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.257 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.258 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.259 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.260 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.261 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.262 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.263 +(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","square_equation1"))*)
1.264 +val (p,_,f,nxt,_,pt) =
1.265 +
1.266 +me nxt p [1] pt;
1.267 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.268 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.269 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.270 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.271 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.272 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.273 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.274 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.275 +(*"9 + -1 * x ^^^ 2 = 0"
1.276 + Subproblem ("Test.thy",["plain_square","univariate","equation"]))*)
1.277 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.278 +(*Model_Problem ["plain_square","univariate","equation"]*)
1.279 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.280 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.281 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.282 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.283 +(*val nxt = ("Specify_Domain",Specify_Domain "Test.thy")*)
1.284 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.285 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.286 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.287 +(*Apply_Method ("Test.thy","solve_plain_square")*)
1.288 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.289 +(*"9 + -1 * x ^^^ 2 = 0", nxt Rewrite_Set "isolate_bdv"*)
1.290 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.291 +(*"x ^^^ 2 = (0 + -1 * 9) / -1", nxt Rewrite_Set "Test_simplify"*)
1.292 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.293 +(*"x ^^^ 2 = 9", nxt Rewrite ("square_equality"*)
1.294 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.295 +(*"x = sqrt 9 | x = -1 * sqrt 9", nxt Rewrite_Set "tval_rls"*)
1.296 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.297 +(*"x = -3 | x = 3", nxt Or_to_List*)
1.298 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.299 +(*"[x = -3, x = 3]",
1.300 + nxt Check_Postcond ["plain_square","univariate","equation","test"]*)
1.301 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.302 +
1.303 +
1.304 +
1.305 +(*"[x = -3, x = 3]", nxt Check_elementwise "Assumptions"*)
1.306 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.307 +(*"[]", nxt Check_Postcond ["sqroot-test","univariate","equation","test"]*)
1.308 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.309 +val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
1.310 +if (snd nxt)=End_Proof' andalso res="[x = -3, x = 3]" then ()
1.311 +else raise error "new behaviour in test: root-eq + subpbl: solve_plain_square";
1.312 +
1.313 +
1.314 +writeln (pr_ptree pr_short pt);
1.315 +
1.316 +
1.317 +
1.318 +val Script s = (#scr o get_met) ("Test.thy","square_equation");
1.319 +atomt s;
1.320 +
1.321 +
1.322 +
1.323 +
1.324 +"---------------- root-eq + subpbl: no_met: linear ----";
1.325 +"---------------- root-eq + subpbl: no_met: linear ----";
1.326 +"---------------- root-eq + subpbl: no_met: linear ----";
1.327 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.328 + "solveFor x","errorBound (eps=0)",
1.329 + "solutions L"];
1.330 +val (dI',pI',mI') =
1.331 + ("Test.thy",["squareroot","univariate","equation","test"],
1.332 + ("Test.thy","square_equation"));
1.333 +val p = e_pos'; val c = [];
1.334 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.335 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
1.336 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.337 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.338 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.339 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.340 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.341 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.342 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.343 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.344 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.345 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.346 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.347 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.348 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.349 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.350 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.351 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.352 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.353 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.354 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.355 +(*"-4 + x = 0", nxt Subproblem ("Test.thy",["univariate","equation"]))*)
1.356 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.357 +(*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*)
1.358 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.359 +(*val nxt =("Model_Problem",Model_Problem ["linear","univar...*)
1.360 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.361 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.362 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.363 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.364 +(*val nxt = ("Specify_Domain",Specify_Domain "Test.thy")*)
1.365 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.366 +(*val nxt = ("Specify_Problem",Specify_Problem ["linear","univariate","equ*)
1.367 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.368 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.369 +(*Apply_Method ("Test.thy","norm_univar_equation")*)
1.370 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.371 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.372 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.373 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.374 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.375 +if p = ([13],Res) then ()
1.376 +else raise error ("new behaviour in test: \
1.377 + \root-eq + subpbl: solve_linear, p ="^(pos'2str p));
1.378 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.379 +val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
1.380 +if (snd nxt)=End_Proof' andalso res="[x = 4]" then ()
1.381 +else raise error "new behaviour in test: root-eq + subpbl: solve_plain_square";
1.382 +
1.383 +
1.384 +
1.385 +
1.386 +"---------------- root-eq + subpbl: no_met: square ----";
1.387 +"---------------- root-eq + subpbl: no_met: square ----";
1.388 +"---------------- root-eq + subpbl: no_met: square ----";
1.389 +val fmz = ["equality (sqrt(5+x)+sqrt(5-x)=sqrt 18)",
1.390 + "solveFor x","errorBound (eps=0)",
1.391 + "solutions L"];
1.392 +val (dI',pI',mI') =
1.393 + ("Test.thy",["squareroot","univariate","equation","test"],
1.394 + ("Test.thy","square_equation"));
1.395 + val Script sc = (#scr o get_met) ("Test.thy","square_equation");
1.396 + (writeln o term2str) sc;
1.397 +
1.398 +val p = e_pos'; val c = [];
1.399 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.400 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
1.401 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.402 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.403 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.404 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.405 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.406 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.407 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.408 +(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","square_equation1"))*)
1.409 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.410 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.411 +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 (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.414 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.415 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.416 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.417 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.418 +(*Subproblem ("Test.thy",["univariate","equation"]))*)
1.419 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.420 +(*("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*)
1.421 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.422 +(*Model_Problem ["plain_square","univariate","equation"]*)
1.423 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.424 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.425 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.426 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.427 +(*val nxt = ("Specify_Domain",Specify_Domain "Test.thy")*)
1.428 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.429 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.430 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.431 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.432 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.433 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.434 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.435 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.436 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.437 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.438 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.439 +(*val nxt = ("Check_Postcond",Check_Postcond ["squareroot","univariate","equ*)
1.440 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.441 +val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
1.442 +if (snd nxt)=End_Proof' andalso res="[x = -3, x = 3]" then ()
1.443 +else raise error "new behaviour in test: root-eq + subpbl: no_met: square";
1.444 +
1.445 +
1.446 +
1.447 +"---------------- no_met in rootpbl -> linear --------------";
1.448 +"---------------- no_met in rootpbl -> linear --------------";
1.449 +"---------------- no_met in rootpbl -> linear --------------";
1.450 +val fmz = ["equality (1+2*x+3=4*x- 6)",
1.451 + "solveFor x","solutions L"];
1.452 +val (dI',pI',mI') =
1.453 + ("Test.thy",["univariate","equation","test"],
1.454 + ("Test.thy","no_met"));
1.455 +val p = e_pos'; val c = [];
1.456 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.457 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
1.458 +(*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*)
1.459 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.460 +(*val nxt = ("Model_Problem",Model_Problem ["normalize","univariate","equati*)
1.461 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.462 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.463 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.464 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.465 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.466 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.467 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.468 +(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","norm_univar_equation"*)
1.469 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.470 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.471 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.472 +(*val nxt = ("Subproblem",Subproblem ("Test.thy",["univariate","equation"])*)
1.473 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.474 +(*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*)
1.475 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.476 +(*val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"]*)
1.477 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.478 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.479 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.480 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.481 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.482 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.483 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.484 +(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","solve_linear"))*)
1.485 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.486 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.487 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.488 +(*val nxt = ("Check_Postcond",Check_Postcond ["linear","univariate","equatio*)
1.489 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.490 +(*val nxt = ("Check_Postcond",Check_Postcond ["normalize","univariate","equa*)
1.491 +val (p,_,Form' (FormKF (_,_,_,_,f)),nxt,_,_) =
1.492 + me nxt p [1] pt;
1.493 +if f="[x = 5]" andalso nxt=("End_Proof'",End_Proof') then ()
1.494 +else raise error "new behaviour in test: no_met in rootpbl -> linear ---";
1.495 +