1.1 --- a/src/Doc/isac/mat-eng.sml Mon Sep 16 12:27:20 2013 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,519 +0,0 @@
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 -