1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-isac/mat-eng.sml Tue Sep 17 09:50:52 2013 +0200
1.3 @@ -0,0 +1,519 @@
1.4 +(* cut and paste for math.tex
1.5 +*)
1.6 +
1.7 +(*2.2. *)
1.8 +"a + b * 3";
1.9 +str2term "a + b * 3";
1.10 +val term = str2term "a + b * 3";
1.11 +atomt term;
1.12 +atomty term;
1.13 +
1.14 +(*2.3. Theories and parsing*)
1.15 +
1.16 + > Isac.thy;
1.17 +val it =
1.18 + {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
1.19 + Sum_Type, Relation, Record, Inductive, Transitive_Closure,
1.20 + Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
1.21 + SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
1.22 + Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
1.23 + IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
1.24 + Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
1.25 + RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
1.26 + Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
1.27 + Float, ComplexI, Descript, Atools, Simplify, Poly, Rational, PolyMinus,
1.28 + Equation, LinEq, Root, RootEq, RatEq, RootRat, RootRatEq, PolyEq, Vect,
1.29 + Calculus, Trig, LogExp, Diff, DiffApp, Integrate, EqSystem, Biegelinie,
1.30 + AlgEin, Test, Isac} : Theory.theory
1.31 +
1.32 +Group.thy
1.33 +suche nach '*' Link: http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/Groups.html
1.34 +locale semigroup =
1.35 + fixes f :: "'a => 'a => 'a" (infixl "*" 70)
1.36 + assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
1.37 +
1.38 +> parse;
1.39 +val it = fn : Theory.theory -> string -> Thm.cterm Library.option
1.40 +
1.41 +
1.42 +
1.43 +> (*-1-*);
1.44 +> parse HOL.thy "2^^^3";
1.45 +*** Inner lexical error at: "^^^3"
1.46 +val it = None : Thm.cterm Library.option
1.47 +> (*-2-*);
1.48 +> parse HOL.thy "d_d x (a + x)";
1.49 +val it = None : Thm.cterm Library.option
1.50 +> (*-3-*);
1.51 +> parse Rational.thy "2^^^3";
1.52 +val it = Some "2 ^^^ 3" : Thm.cterm Library.option
1.53 +> (*-4-*);
1.54 +val Some t4 = parse Rational.thy "d_d x (a + x)";
1.55 +val t4 = "d_d x (a + x)" : Thm.cterm
1.56 +> (*-5-*);
1.57 +val Some t5 = parse Diff.thy "d_d x (a + x)";
1.58 +val t5 = "d_d x (a + x)" : Thm.cterm
1.59 +
1.60 +
1.61 +> term_of;
1.62 +val it = fn : Thm.cterm -> Term.term
1.63 +> term_of t4;
1.64 +val it =
1.65 + Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $
1.66 + Free ("x", "RealDef.real") $
1.67 + (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
1.68 + Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))
1.69 +: Term.term
1.70 +> term_of t5;
1.71 +val it =
1.72 + Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $
1.73 + Free ("x", "RealDef.real") $
1.74 + (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
1.75 + Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))
1.76 +: Term.term
1.77 +
1.78 +> print_depth;
1.79 +val it = fn : int -> unit
1.80 +
1.81 +
1.82 +
1.83 +
1.84 +
1.85 +> (*-4-*) val thy = Rational.thy;
1.86 +val thy =
1.87 + {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
1.88 + Sum_Type, Relation, Record, Inductive, Transitive_Closure,
1.89 + Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
1.90 + SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
1.91 + Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
1.92 + IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
1.93 + Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
1.94 + RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
1.95 + Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
1.96 + Float, ComplexI, Descript, Atools, Simplify, Poly, Rational}
1.97 +: Theory.theory
1.98 +> ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";
1.99 +
1.100 +***
1.101 +*** Free (d_d, [real, real] => real)
1.102 +*** . Free (x, real)
1.103 +*** . Const (op +, [real, real] => real)
1.104 +*** . . Free (a, real)
1.105 +*** . . Free (x, real)
1.106 +***
1.107 +
1.108 +val it = () : unit
1.109 +> (*-5-*) val thy = Diff.thy;
1.110 +val thy =
1.111 + {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
1.112 + Sum_Type, Relation, Record, Inductive, Transitive_Closure,
1.113 + Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
1.114 + SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
1.115 + Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
1.116 + IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
1.117 + Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
1.118 + RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
1.119 + Ring_and_Field, Complex_Numbers, Real, Calculus, Trig, ListG, Tools,
1.120 + Script, Typefix, Float, ComplexI, Descript, Atools, Simplify, Poly,
1.121 + Equation, LinEq, Root, RootEq, Rational, RatEq, RootRat, RootRatEq,
1.122 + PolyEq, LogExp, Diff} : Theory.theory
1.123 +
1.124 +> ((atomty) o term_of o the o (parse thy)) "d_d x (a + x)";
1.125 +
1.126 +***
1.127 +*** Const (Diff.d_d, [real, real] => real)
1.128 +*** . Free (x, real)
1.129 +*** . Const (op +, [real, real] => real)
1.130 +*** . . Free (a, real)
1.131 +*** . . Free (x, real)
1.132 +***
1.133 +
1.134 +val it = () : unit
1.135 +
1.136 +
1.137 +
1.138 +> print_depth 1;
1.139 +val it = () : unit
1.140 +> term_of t4;
1.141 +val it =
1.142 + Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $ ...
1.143 +: Term.term
1.144 +
1.145 +
1.146 +> print_depth 1;
1.147 +val it = () : unit
1.148 +> term_of t5;
1.149 +val it =
1.150 + Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
1.151 + ... : Term.term
1.152 +
1.153 +
1.154 +
1.155 +-------------------------------------------ALT...
1.156 +explode it;
1.157 + \footnote{
1.158 + print_depth 9;
1.159 + explode "a + b * 3";
1.160 + }
1.161 +
1.162 +(*unschoen*)
1.163 +
1.164 +-------------------------------------------ALT...
1.165 + HOL.thy;
1.166 + parse;
1.167 + parse thy "a + b * 3";
1.168 + val t = (term_of o the) it;
1.169 + term_of;
1.170 +
1.171 +(*2.3. Displaying terms*)
1.172 + print_depth;
1.173 + ////Compiler.Control.Print.printDepth;
1.174 +? Compiler.Control.Print.printDepth:= 2;
1.175 + t;
1.176 + ?Compiler.Control.Print.printDepth:= 6;
1.177 + t;
1.178 + ?Compiler.Control.Print.printLength;
1.179 + ?Compiler.Control.Print.stringDepth;
1.180 + atomt;
1.181 + atomt t;
1.182 + atomty;
1.183 + atomty thy t;
1.184 +(*Give it a try: the mathematics knowledge grows*)
1.185 + parse HOL.thy "2^^^3";
1.186 + parse HOL.thy "d_d x (a + x)";
1.187 + ?parse RatArith.thy "#2^^^#3";
1.188 + ?parse RatArith.thy "d_d x (a + x)";
1.189 + parse Differentiate.thy "d_d x (a + x)";
1.190 + ?parse Differentiate.thy "#2^^^#3";
1.191 +(*don't trust the string representation*)
1.192 + ?val thy = RatArith.thy;
1.193 + ((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)";
1.194 + ?val thy = Differentiate.thy;
1.195 + ((atomty thy) o term_of o the o (parse thy)) "d_d x (a + x)";
1.196 +
1.197 +(*2.4. Converting terms*)
1.198 + term_of;
1.199 + the;
1.200 + val t = (term_of o the o (parse thy)) "a + b * 3";
1.201 +
1.202 + sign_of;
1.203 + cterm_of;
1.204 + val ct = cterm_of (sign_of thy) t;
1.205 +
1.206 + Sign.string_of_term;
1.207 + Sign.string_of_term (sign_of thy) t;
1.208 +
1.209 + string_of_cterm;
1.210 + string_of_cterm ct;
1.211 +
1.212 +(*2.5. Theorems *)
1.213 + ?theorem' := overwritel (!theorem',
1.214 + [("diff_const",num_str diff_const)
1.215 + ]);
1.216 +
1.217 +(** 3. Rewriting **)
1.218 +(*3.1. The arguments for rewriting*)
1.219 + HOL.thy;
1.220 + "HOL.thy" : theory';
1.221 + sqrt_right;
1.222 + "sqrt_right" : rew_ord';
1.223 + eval_rls;
1.224 + "eval_rls" : rls';
1.225 + diff_sum;
1.226 + ("diff_sum", "") : thm';
1.227 +
1.228 +(*3.2. The functions for rewriting*)
1.229 + rewrite_;
1.230 + rewrite;
1.231 +
1.232 +> val thy' = "Diff.thy";
1.233 +val thy' = "Diff.thy" : string
1.234 +> val ct = "d_d x (a * 3 + b)";
1.235 +val ct = "d_d x (a * 3 + b)" : string
1.236 +> val thm = ("diff_sum","");
1.237 +val thm = ("diff_sum", "") : string * string
1.238 +> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
1.239 + [("bdv","x::real")] thm ct;
1.240 +val ct = "d_d x (a * 3) + d_d x b" : cterm'
1.241 +> val thm = ("diff_prod_const","");
1.242 +val thm = ("diff_prod_const", "") : string * string
1.243 +> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
1.244 + [("bdv","x::real")] thm ct;
1.245 +val ct = "a * d_d x 3 + d_d x b" : cterm'
1.246 +
1.247 +
1.248 +
1.249 +> val thy' = "Diff.thy";
1.250 +val thy' = "Diff.thy" : string
1.251 +> val ct = "d_d x (a + a * (2 + b))";
1.252 +val ct = "d_d x (a + a * (2 + b))" : string
1.253 +> val thm = ("diff_sum","");
1.254 +val thm = ("diff_sum", "") : string * string
1.255 +> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
1.256 + [("bdv","x::real")] thm ct;
1.257 +val ct = "d_d x a + d_d x (a * (2 + b))" : cterm'
1.258 +
1.259 +> val thm = ("diff_prod_const","");
1.260 +val thm = ("diff_prod_const", "") : string * string
1.261 +> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
1.262 + [("bdv","x::real")] thm ct;
1.263 +val ct = "d_d x a + a * d_d x (2 + b)" : cterm'
1.264 +
1.265 +
1.266 +
1.267 +(*Give it a try: rewriting*)
1.268 + val thy' = "Diff.thy";
1.269 + val ct = "d_d x (x ^^^ 2 + 3 * x + 4)";
1.270 + val thm = ("diff_sum","");
1.271 + val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true [("bdv","x::real")] thm ct;
1.272 + val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true [("bdv","x::real")] thm ct;
1.273 + val thm = ("diff_prod_const","");
1.274 + val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true [("bdv","x::real")] thm ct;
1.275 +(*Give it a try: conditional rewriting*)
1.276 + val thy' = "Isac.thy";
1.277 + val ct' = "3 * a + 2 * (a + 1)";
1.278 + val thm' = ("radd_mult_distrib2","?k * (?m + ?n) = ?k * ?m + ?k * ?n");
1.279 + (*1*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1.280 + val thm' = ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1");
1.281 + ?(*2*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1.282 + ?val thm' = ("rcollect_right",
1.283 + "[| ?l is_const; ?m is_const |] ==> ?l * ?n + ?m * ?n = (?l + ?m) * ?n");
1.284 + ?(*3*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1.285 + ?(*4*) val Some (ct',_) = calculate thy' "plus" ct';
1.286 + ?(*5*) val Some (ct',_) = calculate thy' "times" ct';
1.287 +
1.288 +(*Give it a try: functional programming*)
1.289 + val thy' = "InsSort.thy";
1.290 + val ct = "sort [#1,#3,#2]" : cterm';
1.291 +
1.292 + val thm = ("sort_def","");
1.293 + ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
1.294 +
1.295 + val thm = ("foldr_rec","");
1.296 + ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
1.297 +
1.298 + val thm = ("ins_base","");
1.299 + ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
1.300 +
1.301 + val thm = ("foldr_rec","");
1.302 + ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
1.303 +
1.304 + val thm = ("ins_rec","");
1.305 + ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
1.306 +
1.307 + ?val (ct,_) = the (calculate thy' "le" ct);
1.308 +
1.309 + val thm = ("if_True","(if True then ?x else ?y) = ?x");
1.310 + ?val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
1.311 +
1.312 +(*3.3. Variants of rewriting*)
1.313 + rewrite_inst_;
1.314 + rewrite_inst;
1.315 +
1.316 + rewrite_set_;
1.317 + rewrite_set;
1.318 +
1.319 + rewrite_set_inst_;
1.320 + rewrite_set_inst;
1.321 +
1.322 + toggle;
1.323 + toggle trace_rewrite;
1.324 +
1.325 +(*3.4. Rule sets*)
1.326 + sym;
1.327 + rearrange_assoc;
1.328 +
1.329 +(*Give it a try: remove parentheses*)
1.330 + ?val ct = (string_of_cterm o the o (parse RatArith.thy))
1.331 + "a + (b * (c * d) + e)";
1.332 + ?rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct;
1.333 +
1.334 + toggle trace_rewrite;
1.335 + ?rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct;
1.336 +
1.337 +(*3.5. Calculate numeric constants*)
1.338 + calculate;
1.339 + calculate_;
1.340 +
1.341 + ?calc_list;
1.342 + ?calculate "Isac.thy" "plus" "#1 + #2";
1.343 + ?calculate "Isac.thy" "times" "#2 * #3";
1.344 + ?calculate "Isac.thy" "power" "#2 ^^^ #3";
1.345 + ?calculate "Isac.thy" "cancel_" "#9 // #12";
1.346 +
1.347 +
1.348 +(** 4. Term orders **)
1.349 +(*4.1. Exmpales for term orders*)
1.350 + sqrt_right;
1.351 + tless_true;
1.352 +
1.353 + val t1 = (term_of o the o (parse thy)) "(sqrt a) + b";
1.354 + val t2 = (term_of o the o (parse thy)) "b + (sqrt a)";
1.355 + ?sqrt_right false SqRoot.thy (t1, t2);
1.356 + ?sqrt_right false SqRoot.thy (t2, t1);
1.357 +
1.358 + val t1 = (term_of o the o (parse thy)) "a + b*(sqrt c) + d";
1.359 + val t2 = (term_of o the o (parse thy)) "a + (sqrt b)*c + d";
1.360 + ?sqrt_right true SqRoot.thy (t1, t2);
1.361 +
1.362 +(*4.2. Ordered rewriting*)
1.363 + ac_plus_times;
1.364 +
1.365 +(*Give it a try: polynomial (normal) form*)
1.366 + val ct' = "#3 * a + b + #2 * a";
1.367 + val thm' = ("radd_commute","") : thm';
1.368 + ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1.369 + val thm' = ("rdistr_right_assoc_p","") : thm';
1.370 + ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1.371 + ?val Some (ct',_) = calculate thy' "plus" ct';
1.372 +
1.373 + val ct' = "3 * a + b + 2 * a" : cterm';
1.374 + val thm' = ("radd_commute","") : thm';
1.375 + ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1.376 + ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1.377 + ?val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
1.378 +
1.379 + toggle trace_rewrite;
1.380 + ?rewrite_set "RatArith.thy" "eval_rls" false "ac_plus_times" ct;
1.381 +
1.382 +
1.383 +(** 5. The hierarchy of problem types **)
1.384 +(*5.1. The standard-function for 'matching'*)
1.385 + matches;
1.386 +
1.387 + val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
1.388 + val p = (term_of o the o (parse thy)) "a * b^^^2 = c";
1.389 + atomt p;
1.390 + free2var;
1.391 + val pat = free2var p;
1.392 + matches thy t pat;
1.393 +
1.394 + val t2 = (term_of o the o (parse thy)) "x^^^2 = 1";
1.395 + matches thy t2 pat;
1.396 +
1.397 + val pat2 = (term_of o the o (parse thy)) "?u^^^2 = ?v";
1.398 + matches thy t2 pat2;
1.399 +
1.400 +(*5.2. Accessing the hierarchy*)
1.401 + show_ptyps;
1.402 + show_ptyps();
1.403 + get_pbt;
1.404 + ?get_pbt ["squareroot", "univariate", "equation"];
1.405 +
1.406 + store_pbt;
1.407 + ?store_pbt
1.408 + (prep_pbt SqRoot.thy
1.409 + (["newtype","univariate","equation"],
1.410 + [("#Given" ,["equality e_","solveFor v_","errorBound err_"]),
1.411 + ("#Where" ,["contains_root (e_::bool)"]),
1.412 + ("#Find" ,["solutions v_i_"])
1.413 + ],
1.414 + [("SqRoot.thy","square_equation")]));
1.415 + show_ptyps();
1.416 +
1.417 +(*5.3. Internals of the datastructure*)
1.418 +(*5.4. Match a problem with a problem type*)
1.419 + ?val fmz = ["equality (#1 + #2 * x = #0)",
1.420 + "solveFor x",
1.421 + "solutions L"] : fmz;
1.422 + match_pbl;
1.423 + ?match_pbl fmz (get_pbt ["univariate","equation"]);
1.424 + ?match_pbl fmz (get_pbt ["linear","univariate","equation"]);
1.425 + ?match_pbl fmz (get_pbt ["squareroot","univariate","equation"]);
1.426 +
1.427 +(*5.5. Refine a problem specification *)
1.428 + refine;
1.429 + ?val fmz = ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))",
1.430 + "solveFor x","errorBound (eps=#0)",
1.431 + "solutions L"];
1.432 + ?refine fmz ["univariate","equation"];
1.433 +
1.434 + ?val fmz = ["equality (x+#1=#2)",
1.435 + "solveFor x","errorBound (eps=#0)",
1.436 + "solutions L"];
1.437 + ?refine fmz ["univariate","equation"];
1.438 +
1.439 +
1.440 +(* 6. Do a calculational proof *)
1.441 + ?val fmz = ["equality ((x+#1) * (x+#2) = x^^^#2+#8)","solveFor x",
1.442 + "errorBound (eps=#0)","solutions L"];
1.443 + val spec as (dom, pbt, met) = ("SqRoot.thy",["univariate","equation"],
1.444 + ("SqRoot.thy","no_met"));
1.445 +
1.446 +(*6.1. Initialize the calculation*)
1.447 + val p = e_pos'; val c = [];
1.448 + ?val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met)));
1.449 + ?val (p,_,f,nxt,_,pt) = me (mID,m) p c EmptyPtree;
1.450 +
1.451 + ?Compiler.Control.Print.printDepth:=8;
1.452 + ?f;
1.453 + ?Compiler.Control.Print.printDepth:=4;
1.454 +
1.455 + ?nxt;
1.456 + ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.457 + ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.458 +
1.459 +(*6.2. The phase of modeling*)
1.460 + ?nxt;
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 +
1.465 + ?Compiler.Control.Print.printDepth:=8;
1.466 + ?f;
1.467 + ?Compiler.Control.Print.printDepth:=4;
1.468 +
1.469 +(*6.3. The phase of specification*)
1.470 + ?nxt;
1.471 + ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.472 +
1.473 +
1.474 + val nxt = ("Specify_Problem",
1.475 + Specify_Problem ["polynomial","univariate","equation"]);
1.476 + ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.477 +
1.478 + val nxt = ("Specify_Problem",
1.479 + Specify_Problem ["linear","univariate","equation"]);
1.480 + ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.481 + ?Compiler.Control.Print.printDepth:=8;f;Compiler.Control.Print.printDepth:=4;
1.482 +
1.483 + val nxt = ("Refine_Problem",
1.484 + Refine_Problem ["linear","univariate","equation"]);
1.485 + ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.486 + ?Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
1.487 +
1.488 + val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation"]);
1.489 + ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.490 + ?Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
1.491 +
1.492 + ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.493 + ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.494 +
1.495 +(*6.4. The phase of solving*)
1.496 + nxt;
1.497 + ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.498 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.499 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.500 +
1.501 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.502 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.503 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.504 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.505 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.506 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.507 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.508 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.509 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.510 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.511 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.512 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.513 +
1.514 +(*6.5. The final phase: check the postcondition*)
1.515 + ?val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.516 + val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.517 +
1.518 +
1.519 +
1.520 +
1.521 +
1.522 +