1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/systest/details.sml Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,280 @@
1.4 +(* use"../systest/details.sml";
1.5 + use"systest/details.sml";
1.6 + use"details.sml";
1.7 +
1.8 +########################################################
1.9 +is NOT dependent on Test, but on other thys:
1.10 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1.11 +uses from Rational.ML: Rrls cancel_p, Rrls cancel
1.12 +which in turn
1.13 +uses from Poly.ML: Rls make_polynomial, Rls expand_binom
1.14 +########################################################
1.15 +*)
1.16 +"-------- cancel, without detail ------------------------------";
1.17 +"-------- cancel, detail rev-rew (cancel) afterwards ----------";
1.18 +"-------------- cancel_p, without detail ------------------------------";
1.19 +"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
1.20 +
1.21 +store_pbt
1.22 + (prep_pbt Test.thy
1.23 + (["test"],
1.24 + [],
1.25 + e_rls, None, []));
1.26 +store_pbt
1.27 + (prep_pbt Test.thy
1.28 + (["detail","test"],
1.29 + [("#Given" ,["realTestGiven t_"]),
1.30 + ("#Find" ,["realTestFind s_"])
1.31 + ],
1.32 + e_rls, None, [("Test.thy","test_detail")]));
1.33 +
1.34 +methods:= overwritel (!methods,
1.35 +[
1.36 + prep_met
1.37 + (("Test.thy","test_detail_binom"):metID,
1.38 + [("#Given" ,["realTestGiven t_"]),
1.39 + ("#Find" ,["realTestFind s_"])
1.40 + ],
1.41 + {rew_ord'="sqrt_right",rls'=tval_rls,calc = [],srls=e_rls,prls=e_rls,
1.42 + asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]},
1.43 + "Script Testterm (g_::real) = \
1.44 + \(((Rewrite_Set expand_binoms False) @@\
1.45 + \ (Rewrite_Set cancel False)) g_)"
1.46 + ),
1.47 + prep_met
1.48 + (("Test.thy","test_detail_poly"):metID,
1.49 + [("#Given" ,["realTestGiven t_"]),
1.50 + ("#Find" ,["realTestFind s_"])
1.51 + ],
1.52 + {rew_ord'="sqrt_right",rls'=tval_rls,calc=[],srls=e_rls,prls=e_rls,
1.53 + asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]},
1.54 + "Script Testterm (g_::real) = \
1.55 + \(((Rewrite_Set make_polynomial False) @@\
1.56 + \ (Rewrite_Set cancel_p False)) g_)"
1.57 + )]);
1.58 +
1.59 +(*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*)
1.60 +
1.61 +"-------- cancel, without detail ------------------------------";
1.62 +"-------- cancel, without detail ------------------------------";
1.63 +"-------- cancel, without detail ------------------------------";
1.64 +val fmz = ["realTestGiven (((3 + x) * (3 - x)) / ((3 + x) * (3 + x)))",
1.65 + "realTestFind s"];
1.66 +val (dI',pI',mI') =
1.67 + ("Test.thy",["detail","test"],("Test.thy","test_detail_binom"));
1.68 +
1.69 +val p = e_pos'; val c = [];
1.70 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.71 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
1.72 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.73 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.74 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.75 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.76 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.77 +(*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*)
1.78 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.79 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.80 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.81 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.82 +(*"(3 + -1 * x) / (3 + x)"*)
1.83 +if nxt = ("End_Proof'",End_Proof') then ()
1.84 +else raise error "details.sml, changed behaviour in: without detail";
1.85 +
1.86 +
1.87 +"-------- cancel, detail rev-rew (cancel) afterwards ----------";
1.88 +"-------- cancel, detail rev-rew (cancel) afterwards ----------";
1.89 +"-------- cancel, detail rev-rew (cancel) afterwards ----------";
1.90 + val p = e_pos'; val c = [];
1.91 + val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.92 + val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
1.93 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.94 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.95 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.96 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.97 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.98 + (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*)
1.99 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.100 + (*val nxt = ("Rewrite_Set",Rewrite_Set "expand_binoms")*)
1.101 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
1.102 + val nxt = ("Detail",Detail);"----------------------";
1.103 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.104 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.105 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.106 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.107 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.108 + (*val nxt = ("End_Detail",End_Detail)*)
1.109 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.110 + (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel")*)
1.111 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
1.112 + val nxt = ("Detail",Detail);"----------------------";
1.113 + val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e;
1.114 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.115 +(*15.10.02*)
1.116 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.117 +(*
1.118 +rewrite "Rationals.thy" "tless_true""e_rls"true("sym_real_plus_minus_binom","")
1.119 + "3 ^^^ 2 - x ^^^ 2";
1.120 +*)
1.121 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.122 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.123 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.124 + val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e;
1.125 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.126 +if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 - x) / (3 + x)"))
1.127 + andalso nxt = ("End_Proof'",End_Proof') then ()
1.128 +else raise error "new behaviour in details.sml, \
1.129 + \cancel, rev-rew (cancel) afterwards";
1.130 +
1.131 +(*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*)
1.132 +
1.133 +"-------------- cancel_p, without detail ------------------------------";
1.134 +"-------------- cancel_p, without detail ------------------------------";
1.135 +"-------------- cancel_p, without detail ------------------------------";
1.136 +val fmz = ["realTestGiven (((3 + x)*(3+(-1)*x)) / ((3+x) * (3+x)))",
1.137 + "realTestFind s"];
1.138 +val (dI',pI',mI') =
1.139 + ("Test.thy",["detail","test"],("Test.thy","test_detail_poly"));
1.140 +
1.141 +val p = e_pos'; val c = [];
1.142 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.143 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
1.144 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.145 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.146 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.147 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.148 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.149 +(*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*)
1.150 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.151 +"(3 + x) * (3 + -1 * x) / ((3 + x) * (3 + x))";
1.152 +
1.153 + (*14.3.03*)
1.154 + val t = str2term "(3 + x) * (3 + -1 * x) / ((3 + x) * (3 + x))";
1.155 + val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.156 + "(9 + - (x ^^^ 2)) / (9 + 6 * x + x ^^^ 2)";
1.157 + val Some (t,_) = rewrite_set_ thy false cancel_p t; term2str t;
1.158 + cancel_p_ thy t;
1.159 +
1.160 + val t = str2term "(3 + x) * (3 + -1 * x)";
1.161 + val Some (t,_) = rewrite_set_ thy false expand_poly t; term2str t;
1.162 + "3 * 3 + 3 * (-1 * x) + (x * 3 + x * (-1 * x))";
1.163 + val Some (t,_) = rewrite_set_ thy false order_add_mult t; term2str t;
1.164 + "3 * 3 + (3 * x + (-1 * (3 * x) + -1 * (x * x)))";
1.165 + val Some (t,_) = rewrite_set_ thy false simplify_power t; term2str t;
1.166 + "3 ^^^ 2 + (3 * x + (-1 * (3 * x) + -1 * x ^^^ 2))";
1.167 + val Some (t,_) = rewrite_set_ thy false collect_numerals t; term2str t;
1.168 + "9 + (0 * x + -1 * x ^^^ 2)";
1.169 + val Some (t,_) = rewrite_set_ thy false reduce_012 t; term2str t;
1.170 + "9 + - (x ^^^ 2)";
1.171 + (*14.3.03*)
1.172 +
1.173 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.174 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.175 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.176 +(*"(3 + -1 * x) / (3 + x)"*)
1.177 +if nxt = ("End_Proof'",End_Proof') then ()
1.178 +else raise error "details.sml, changed behaviour in: cancel_p, without detail";
1.179 +
1.180 +"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
1.181 +"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
1.182 +"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
1.183 + val p = e_pos'; val c = [];
1.184 + val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.185 + val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
1.186 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.187 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.188 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.189 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.190 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.191 + (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail_poly"))*)
1.192 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.193 + (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*)
1.194 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
1.195 +
1.196 +(*14.3.03.FIXXXXXME since Isa02/reverse-rew.sml:
1.197 + fun make_deriv ... Rls_ not yet impl. (| Thm | Calc)
1.198 + Rls_ needed for make_polynomial ----------------------
1.199 + val nxt = ("Detail",Detail);"----------------------";
1.200 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.201 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.202 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.203 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.204 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.205 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.206 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.207 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.208 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.209 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.210 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.211 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.212 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.213 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.214 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.215 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.216 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.217 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.218 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.219 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.220 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.221 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.222 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.223 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.224 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.225 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.226 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.227 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.228 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.229 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.230 + if nxt = ("End_Detail",End_Detail) then ()
1.231 + else raise error "details.sml: new behav. in Detail make_polynomial";
1.232 +----------------------------------------------------------------------*)
1.233 +
1.234 +(*---------------
1.235 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.236 + (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel_p")*)
1.237 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
1.238 + val nxt = ("Detail",Detail);"----------------------";
1.239 + val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e;
1.240 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.241 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.242 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.243 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.244 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.245 + val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e;
1.246 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.247 +if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 + x) / (3 - x)"))
1.248 + andalso nxt = ("End_Proof'",End_Proof') then ()
1.249 +else raise error "new behaviour in details.sml, cancel_p afterwards";
1.250 +
1.251 +----------------*)
1.252 +
1.253 +
1.254 +
1.255 +
1.256 +
1.257 +val fmz = ["realTestGiven ((x+3)+(-1)*(2+6*x))",
1.258 + "realTestFind s"];
1.259 +val (dI',pI',mI') =
1.260 + ("Test.thy",["detail","test"],("Test.thy","test_detail_poly"));
1.261 +
1.262 + val p = e_pos'; val c = [];
1.263 + val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.264 + val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
1.265 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.266 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.267 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.268 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.269 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.270 + (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail_poly"))*)
1.271 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.272 +(*16.10.02 --- kommt auf POLY_EXCEPTION ?!??? ----------------------------
1.273 + (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*)
1.274 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
1.275 + val nxt = ("Detail",Detail);"----------------------";
1.276 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.277 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.278 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.279 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.280 +-------------------------------------------------------------------------*)
1.281 +
1.282 +
1.283 +