1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Sat Mar 10 14:53:18 2012 +0100
1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Tue Mar 13 15:04:09 2012 +0100
1.3 @@ -129,12 +129,11 @@
1.4 " a kleiner b ==> (b + a) = (a + b)";
1.5 str2term "aaa";
1.6 str2term "222 * aaa";
1.7 -(*
1.8 +
1.9 case eval_kleiner 0 0 (str2term "123 kleiner 32") 0 of
1.10 - SOME ("12 kleiner 9 = False", _) => ()
1.11 + SOME ("123 kleiner 32 = False", _) => ()
1.12 | _ => error "polyminus.sml: 12 kleiner 9 = False";
1.13 -*)
1.14 -(*========== inhibit exn =======================================================
1.15 +
1.16 case eval_kleiner 0 0 (str2term "a kleiner b") 0 of
1.17 SOME ("a kleiner b = True", _) => ()
1.18 | _ => error "polyminus.sml: a kleiner b = True";
1.19 @@ -159,10 +158,7 @@
1.20 SOME ("3 * a * b kleiner c = True", _) => ()
1.21 | _ => error "polyminus.sml: 3 * a * b kleiner b = True";
1.22
1.23 -============ inhibit exn =====================================================*)
1.24 -
1.25 -
1.26 -"----- compare tausche_plus with real_num_collect";
1.27 +"======= compare tausche_plus with real_num_collect";
1.28 val od = dummy_ord;
1.29
1.30 val erls = erls_ordne_alphabetisch;
1.31 @@ -175,7 +171,7 @@
1.32 val t = str2term "2*a + 3*a";
1.33 val SOME (t,_) = rewrite_ thy od erls false @{thm real_num_collect} t; term2str t;
1.34
1.35 -"----- test rewrite_, rewrite_set_";
1.36 +"======= test rewrite_, rewrite_set_";
1.37 trace_rewrite:=true;
1.38 val erls = erls_ordne_alphabetisch;
1.39 val t = str2term "b + a";
1.40 @@ -193,7 +189,7 @@
1.41 if term2str t = "a + b + c" then ()
1.42 else error "polyminus.sml: ordne_alphabetisch a + b + c";
1.43
1.44 -"----- rewrite goes into subterms";
1.45 +"======= rewrite goes into subterms";
1.46 val t = str2term "a + c + b + d";
1.47 val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus_plus} t; term2str t;
1.48 if term2str t = "a + b + c + d" then ()
1.49 @@ -204,13 +200,13 @@
1.50 if term2str t = "a + b + c + d" then ()
1.51 else error "polyminus.sml: ordne_alphabetisch2 a + b + c + d";
1.52
1.53 -"----- here we see rew_sub going into subterm with cond.rew....";
1.54 +"======= here we see rew_sub going into subterm with cond.rew....";
1.55 val t = str2term "b + a + c + d";
1.56 val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus} t; term2str t;
1.57 if term2str t = "a + b + c + d" then ()
1.58 else error "polyminus.sml: ordne_alphabetisch3 a + b + c + d";
1.59
1.60 -"----- compile rls for the most complicated terms";
1.61 +"======= compile rls for the most complicated terms";
1.62 val t = str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
1.63 "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12";
1.64 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t;
1.65 @@ -248,7 +244,6 @@
1.66 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.67 atomty sc;
1.68
1.69 -
1.70 "----------- me simplification.for_polynomials.with_minus";
1.71 "----------- me simplification.for_polynomials.with_minus";
1.72 "----------- me simplification.for_polynomials.with_minus";
1.73 @@ -274,7 +269,6 @@
1.74 if f2str f = "3 - 2 * e + 2 * f + 2 * g" andalso #1 nxt = "End_Proof'" then ()
1.75 else error "polyminus.sml: me simplification.for_polynomials.with_minus";
1.76
1.77 -
1.78 "----------- pbl polynom vereinfachen p.33 -----------------------";
1.79 "----------- pbl polynom vereinfachen p.33 -----------------------";
1.80 "----------- pbl polynom vereinfachen p.33 -----------------------";
1.81 @@ -291,7 +285,7 @@
1.82 term2str (get_obj g_res pt (fst p)) = "3 - 2 * e + 2 * f + 2 * g"
1.83 then () else error "polyminus.sml: Vereinfache (3 - 2 * e + 2 * f...";
1.84
1.85 -"----------- 140 d ---";
1.86 +"======= 140 d ---";
1.87 states:=[];
1.88 CalcTree [(["Term (-r - 2*s - 3*t + 5 + 4*r + 8*s - 5*t - 2)",
1.89 "normalform N"],
1.90 @@ -304,8 +298,7 @@
1.91 term2str (get_obj g_res pt (fst p)) = "3 + 3 * r + 6 * s - 8 * t"
1.92 then () else error "polyminus.sml: Vereinfache 140 d)";
1.93
1.94 -
1.95 -"----------- 139 c ---";
1.96 +"======= 139 c ---";
1.97 states:=[];
1.98 CalcTree [(["Term (3*e - 6*f - 8*e - 4*f + 5*e + 7*f)",
1.99 "normalform N"],
1.100 @@ -318,7 +311,7 @@
1.101 term2str (get_obj g_res pt (fst p)) = "- (3 * f)"
1.102 then () else error "polyminus.sml: Vereinfache 139 c)";
1.103
1.104 -"----------- 139 b ---";
1.105 +"======= 139 b ---";
1.106 states:=[];
1.107 CalcTree [(["Term (8*u - 5*v - 5*u + 7*v - 6*u - 3*v)",
1.108 "normalform N"],
1.109 @@ -331,7 +324,7 @@
1.110 term2str (get_obj g_res pt (fst p)) = "-3 * u - v"
1.111 then () else error "polyminus.sml: Vereinfache 139 b)";
1.112
1.113 -"----------- 138 a ---";
1.114 +"======= 138 a ---";
1.115 states:=[];
1.116 CalcTree [(["Term (2*u - 3*v - 6*u + 5*v)",
1.117 "normalform N"],
1.118 @@ -344,7 +337,6 @@
1.119 term2str (get_obj g_res pt (fst p)) = "-4 * u + 2 * v"
1.120 then () else error "polyminus.sml: Vereinfache 138 a)";
1.121
1.122 -
1.123 "----------- met probe fuer_polynom ------------------------------";
1.124 "----------- met probe fuer_polynom ------------------------------";
1.125 "----------- met probe fuer_polynom ------------------------------";
1.126 @@ -358,7 +350,6 @@
1.127 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.128 atomty sc;
1.129
1.130 -
1.131 "----------- pbl polynom probe -----------------------------------";
1.132 "----------- pbl polynom probe -----------------------------------";
1.133 "----------- pbl polynom probe -----------------------------------";
1.134 @@ -382,8 +373,6 @@
1.135 then () else error "polyminus.sml: Probe 11 = 11";
1.136 show_pt pt;
1.137
1.138 -
1.139 -
1.140 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
1.141 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
1.142 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
1.143 @@ -400,7 +389,7 @@
1.144 then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
1.145 show_pt pt;
1.146
1.147 -"----- probe p.34 -----";
1.148 +"======= probe p.34 -----";
1.149 states:=[];
1.150 CalcTree [(["Pruefe (2*u - 5 - (3 - 4*u) + (8*u + 9) = 1 + 14 * u)",
1.151 "mitWert [u = 2]",
1.152 @@ -413,8 +402,6 @@
1.153 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "29 = 29"
1.154 then () else error "polyminus.sml: Probe 29 = 29";
1.155 show_pt pt;
1.156 -(*========== inhibit exn 110719 ================================================
1.157 -
1.158
1.159 "----------- try fun applyTactics --------------------------------";
1.160 "----------- try fun applyTactics --------------------------------";
1.161 @@ -471,7 +458,6 @@
1.162 val ((pt,p),_) = get_calc 1; show_pt pt;
1.163 "----- 7 ^^^";
1.164 *)
1.165 -============ inhibit exn 110719 ==============================================*)
1.166 autoCalculate 1 CompleteCalc;
1.167 val ((pt,p),_) = get_calc 1; show_pt pt;
1.168 (*independent from failure above: met_simp_poly_minus not confluent:
1.169 @@ -505,8 +491,6 @@
1.170 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "f + 2 * g"
1.171 then () else error "polyminus.sml: tausche_vor_plus";
1.172
1.173 -(*========== inhibit exn 110719 ================================================
1.174 -
1.175 "----------- pbl binom polynom vereinfachen p.39 -----------------";
1.176 "----------- pbl binom polynom vereinfachen p.39 -----------------";
1.177 "----------- pbl binom polynom vereinfachen p.39 -----------------";
1.178 @@ -539,12 +523,7 @@
1.179 val SOME (t,_) = rewrite_set_ thy false rls t; term2str t;
1.180 *)
1.181
1.182 -
1.183 -trace_rewrite := true;
1.184 -trace_rewrite := false;
1.185 -
1.186 (*@@@@@@@*)
1.187 -============ inhibit exn 110719 ==============================================*)
1.188 states:=[];
1.189 CalcTree [(["Term ((3*a + 2) * (4*a - 1))",
1.190 "normalform N"],
1.191 @@ -557,8 +536,6 @@
1.192 term2str (get_obj g_res pt (fst p)) = "-2 + 12 * a ^^^ 2 + 5 * a"
1.193 then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
1.194
1.195 -
1.196 -
1.197 "----------- pbl binom polynom vereinfachen: cube ----------------";
1.198 "----------- pbl binom polynom vereinfachen: cube ----------------";
1.199 "----------- pbl binom polynom vereinfachen: cube ----------------";
1.200 @@ -572,24 +549,18 @@
1.201 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "12 * a - 16 * q"
1.202 then () else error "pbl binom polynom vereinfachen: cube";
1.203
1.204 -(*========== inhibit exn 110719 ================================================
1.205 -
1.206 "----------- refine Vereinfache ----------------------------------";
1.207 "----------- refine Vereinfache ----------------------------------";
1.208 "----------- refine Vereinfache ----------------------------------";
1.209 -val fmz = ["Term (8*(a - q) + a - 2*q + 3*(a - 2*q))",
1.210 - "normalform N"];
1.211 +val fmz = ["Term (8*(a - q) + a - 2*q + 3*(a - 2*(q::real)))", "normalform (N::real)"];
1.212 print_depth 11;
1.213 val matches = refine fmz ["vereinfachen"];
1.214 print_depth 3;
1.215
1.216 "----- go into details, if it seems not to work -----";
1.217 "--- does the predicate evaluate correctly ?";
1.218 -(*=== inhibit exn ==============================================================
1.219 -!!!!! no '?a' ............
1.220 val t = str2term
1.221 - "matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q + \
1.222 - \3 * (a - 2 * q))";
1.223 + "matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q + 3 * (a - 2 * (q::real)))";
1.224 val ma = eval_matchsub "" "Tools.matchsub" t thy;
1.225 case ma of
1.226 SOME ("matchsub (?a * (?b - ?c)) (8 * (a - q) + \
1.227 @@ -621,10 +592,8 @@
1.228 trace_rewrite := true;
1.229 val SOME (t', _) = rewrite_set_ thy false prls t;
1.230 trace_rewrite := false;
1.231 -if term2str t' = "HOL.False" then ()
1.232 +if term2str t' = "False" then ()
1.233 else error "polyminus.sml Not (matchsub (?a * (?b + ?c)) (8 ...";
1.234 -============ inhibit exn =====================================================*)
1.235 -
1.236
1.237 "----------- *** prep_pbt: syntax error in '#Where' of [v";
1.238 "----------- *** prep_pbt: syntax error in '#Where' of [v";
1.239 @@ -635,11 +604,11 @@
1.240 " matchsub (?a + (?b - ?c)) t_t | " ^
1.241 " matchsub (?a - (?b + ?c)) t_t | " ^
1.242 " matchsub (?a + (?b - ?c)) t_t )");
1.243 -show_types := true;
1.244 +(*show_types := true;
1.245 if term2str t = "~ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) |\n matchsub (?a + (?b - ?c)) t_t |\n matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)"
1.246 then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1";
1.247 -show_types := false;
1.248 +show_types := false;*)
1.249 +if term2str t = "~ (matchsub (?a + (?b + ?c)) t_t |\n matchsub (?a + (?b - ?c)) t_t |\n" ^
1.250 +" matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)"
1.251 +then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1";
1.252
1.253 -
1.254 -============ inhibit exn 110719 ==============================================*)
1.255 -